1
1
{-# LANGUAGE DeriveDataTypeable #-}
2
{-# LANGUAGE DeriveFoldable #-}
3
{-# LANGUAGE DeriveFunctor #-}
4
{-# LANGUAGE DeriveTraversable #-}
2
{-# LANGUAGE DeriveFoldable #-}
3
{-# LANGUAGE DeriveFunctor #-}
4
{-# LANGUAGE DeriveTraversable #-}
6
{-| Definitions for fixity and precedence levels.
6
{-| Definitions for fixity, precedence levels, and declared syntax.
8
8
module Agda.Syntax.Fixity where
10
import Data.Typeable (Typeable)
11
10
import Data.Foldable
11
import Data.List as List
12
12
import Data.Traversable
13
import Data.Typeable (Typeable)
14
15
import Agda.Syntax.Position
15
16
import Agda.Syntax.Common
16
17
import Agda.Syntax.Concrete.Name
17
18
import Agda.Syntax.Notation
20
import Agda.Utils.List
22
-- * Notation coupled with 'Fixity'
24
-- | The notation is handled as the fixity in the renamer.
25
-- Hence, they are grouped together in this type.
19
26
data Fixity' = Fixity'
21
theNotation :: Notation}
28
, theNotation :: Notation
22
30
deriving (Typeable, Show, Eq)
24
data ThingWithFixity x = ThingWithFixity x Fixity' deriving (Functor,Foldable,Traversable,Typeable,Show)
32
-- | Decorating something with @Fixity'@.
33
data ThingWithFixity x = ThingWithFixity x Fixity'
34
deriving (Functor, Foldable, Traversable, Typeable, Show)
25
36
-- | All the notation information related to a name.
26
type NewNotation = (QName, Fixity, Notation)
37
data NewNotation = NewNotation
39
-- ^ The concrete name the syntax or fixity belongs to.
40
, notaFixity :: Fixity
41
-- ^ Associativity and precedence (fixity) of the name.
42
, notation :: Notation
43
-- ^ Syntax associated with the name.
44
} deriving (Typeable, Show)
28
46
-- | If an operator has no specific notation, recover it from its name.
29
47
oldToNewNotation :: (QName, Fixity') -> NewNotation
30
oldToNewNotation (name, Fixity' f []) = (name, f, syntaxOf $ unqualify name)
31
oldToNewNotation (name, Fixity' f syn) = (name, f, syn)
48
oldToNewNotation (name, Fixity' f syn) = NewNotation
51
, notation = if null syn then syntaxOf $ unqualify name else syn
54
-- | Return the 'IdPart's of a notation, the first part qualified,
55
-- the other parts unqualified.
56
-- This allows for qualified use of operators, e.g.,
57
-- @M.for x ∈ xs return e@, or @x ℕ.+ y@.
58
notationNames :: NewNotation -> [QName]
59
notationNames (NewNotation q _ parts) =
60
zipWith ($) (reQualify : repeat QName) [Name noRange [Id x] | IdPart x <- parts ]
62
-- The qualification of @q@.
63
modules = init (qnameParts q)
64
-- Putting the qualification onto @x@.
65
reQualify x = List.foldr Qual (QName x) modules
67
-- | Create a 'Notation' (without binders) from a concrete 'Name'.
68
-- Does the obvious thing:
69
-- 'Hole's become 'NormalHole's, 'Id's become 'IdParts'.
70
-- If 'Name' has no 'Hole's, it returns 'noNotation'.
33
71
syntaxOf :: Name -> Notation
34
syntaxOf (NoName _ _) = []
35
syntaxOf (Name _ [_]) = []
72
syntaxOf (NoName _ _) = noNotation
73
syntaxOf (Name _ [_]) = noNotation
36
74
syntaxOf (Name _ xs) = mkSyn 0 xs
37
where mkSyn :: Int -> [NamePart] -> Notation
39
mkSyn n (Hole:xs) = NormalHole (defaultNamedArg n) : mkSyn (1+n) xs
40
mkSyn n (Id x:xs) = IdPart x : mkSyn n xs
76
-- Turn a concrete name into a Notation,
77
-- numbering the holes from left to right.
78
-- Result will have no 'BindingHole's.
79
mkSyn :: Int -> [NamePart] -> Notation
81
mkSyn n (Hole : xs) = NormalHole (defaultNamedArg n) : mkSyn (1 + n) xs
82
mkSyn n (Id x : xs) = IdPart x : mkSyn n xs
84
defaultFixity' :: Fixity'
43
85
defaultFixity' = Fixity' defaultFixity defaultNotation
45
noFixity = NonAssoc noRange (negate 666) -- ts,ts,ts, why the number of the beast? Revelation 13, 18
46
-- It's not the number of the beast, it's the negation of the
47
-- number of the beast, which must be a divine number, right?
87
-- | Removes copies of @defaultFixity'@ from a list of fixities.
88
-- Never returns an empty list, though, rather a singleton list
89
-- consisting of @defaultFixity'@.
90
interestingFixities :: [Fixity'] -> [Fixity']
91
interestingFixities fixs = if null fixs' then [defaultFixity'] else fixs'
92
where fixs' = filter (not . (== defaultFixity')) fixs
94
-- | If different interesting fixities are available for the same symbol,
95
-- we take none of them.
96
chooseFixity :: [Fixity'] -> Fixity'
97
chooseFixity fixs = if allEqual fixs' then head fixs' else defaultFixity'
98
where fixs' = interestingFixities fixs
49
102
-- | Fixity of operators.
50
data Fixity = LeftAssoc Range Integer
51
| RightAssoc Range Integer
52
| NonAssoc Range Integer
53
deriving (Typeable, Show)
105
= LeftAssoc { fixityRange :: Range, fixityLevel :: Integer }
106
| RightAssoc { fixityRange :: Range, fixityLevel :: Integer }
107
| NonAssoc { fixityRange :: Range, fixityLevel :: Integer }
108
deriving (Typeable, Show)
55
110
instance Eq Fixity where
56
LeftAssoc _ n == LeftAssoc _ m = n == m
57
RightAssoc _ n == RightAssoc _ m = n == m
58
NonAssoc _ n == NonAssoc _ m = n == m
111
LeftAssoc _ n == LeftAssoc _ m = n == m
112
RightAssoc _ n == RightAssoc _ m = n == m
113
NonAssoc _ n == NonAssoc _ m = n == m
61
fixityLevel :: Fixity -> Integer
62
fixityLevel (LeftAssoc _ n) = n
63
fixityLevel (RightAssoc _ n) = n
64
fixityLevel (NonAssoc _ n) = n
116
-- For @instance Pretty Fixity@, see Agda.Syntax.Concrete.Pretty
66
118
-- | The default fixity. Currently defined to be @'NonAssoc' 20@.
67
119
defaultFixity :: Fixity
68
120
defaultFixity = NonAssoc noRange 20
122
-- | Hack used for @syntax@ facility.
124
noFixity = NonAssoc noRange (negate 666)
125
-- Ts,ts,ts, why the number of the beast? Revelation 13, 18
127
-- It's not the number of the beast, it's the negation of the
128
-- number of the beast, which must be a divine number, right?
130
-- The divine is not the negation of evil.
131
-- Evil is only the absense of the good and divine.
70
136
-- | Precedence is associated with a context.
71
137
data Precedence = TopCtx | FunctionSpaceDomainCtx
72
| LeftOperandCtx Fixity | RightOperandCtx Fixity
73
| FunctionCtx | ArgumentCtx | InsideOperandCtx
138
| LeftOperandCtx Fixity | RightOperandCtx Fixity
139
| FunctionCtx | ArgumentCtx | InsideOperandCtx
74
140
| WithFunCtx | WithArgCtx | DotPatternCtx
75
141
deriving (Show,Typeable)
added
removed
src/full/Agda/Syntax/Fixity.hs
