git.iko.soy/Idris-dev
on eac558e help sign in
Idris-dev/src/Idris/Parser/Ops.hs
179 lines 6.3 kB history raw
1{-|
2Module : Idris.Parser.Ops
3Description : Parser for operators and fixity declarations.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
9module Idris.Parser.Ops where
11import Prelude hiding (pi)
13import Text.Trifecta.Delta
14import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
15import Text.Parser.LookAhead
16import Text.Parser.Expression
17import qualified Text.Parser.Token as Tok
18import qualified Text.Parser.Char as Chr
19import qualified Text.Parser.Token.Highlight as Hi
21import Idris.AbsSyntax
22import Idris.Parser.Helpers
24import Idris.Core.TT
26import Control.Applicative
27import Control.Monad
28import Control.Monad.State.Strict
30import Data.Maybe
31import qualified Data.List.Split as Spl
32import Data.List
33import Data.Monoid
34import Data.Char
35import qualified Data.HashSet as HS
36import qualified Data.Text as T
37import qualified Data.ByteString.UTF8 as UTF8
39import Debug.Trace
41-- | Creates table for fixity declarations to build expression parser
42-- using pre-build and user-defined operator/fixity declarations
43table :: [FixDecl] -> OperatorTable IdrisParser PTerm
44table fixes
45 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++
46 toTable (reverse fixes) ++
47 [[backtick],
48 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],
49 [binary "=" (\fc x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]) AssocLeft],
50 [nofixityoperator]]
51 where
52 flatten :: PTerm -> PTerm -- flatten application
53 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
54 flatten t = t
57-- | Calculates table for fixity declarations
58toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
59toTable fs = map (map toBin)
60 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
61 where toBin (Fix (PrefixN _) op) = prefix op
62 (\fc x -> PApp fc (PRef fc [] (sUN op)) [pexp x])
63 toBin (Fix f op)
64 = binary op (\fc x y -> PApp fc (PRef fc [] (sUN op)) [pexp x,pexp y]) (assoc f)
65 assoc (Infixl _) = AssocLeft
66 assoc (Infixr _) = AssocRight
67 assoc (InfixN _) = AssocNone
69-- | Binary operator
70binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
71binary name f = Infix (do indentPropHolds gtProp
72 fc <- reservedOpFC name
73 indentPropHolds gtProp
74 return (f fc))
76-- | Prefix operator
77prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
78prefix name f = Prefix (do reservedOp name
79 fc <- getFC
80 indentPropHolds gtProp
81 return (f fc))
83-- | Backtick operator
84backtick :: Operator IdrisParser PTerm
85backtick = Infix (do indentPropHolds gtProp
86 lchar '`'; (n, fc) <- fnName
87 lchar '`'
88 indentPropHolds gtProp
89 return (\x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y])) AssocNone
91-- | Operator without fixity (throws an error)
92nofixityoperator :: Operator IdrisParser PTerm
93nofixityoperator = Infix (do indentPropHolds gtProp
94 op <- try operator
95 unexpected $ "Operator without known fixity: " ++ op) AssocNone
98{- | Parses an operator in function position i.e. enclosed by `()', with an
99 optional namespace
102 OperatorFront ::=
103 '(' '=' ')'
104 | (Identifier_t '.')? '(' Operator_t ')'
105 ;
108-}
109operatorFront :: IdrisParser (Name, FC)
110operatorFront = try (do (FC f (l, c) _) <- getFC
111 op <- lchar '(' *> reservedOp "=" <* lchar ')'
112 return (eqTy, FC f (l, c) (l, c+3)))
113 <|> maybeWithNS (do (FC f (l, c) _) <- getFC
114 op <- lchar '(' *> operator
115 (FC _ _ (l', c')) <- getFC
116 lchar ')'
117 return (op, (FC f (l, c) (l', c' + 1)))) False []
119{- | Parses a function (either normal name or operator)
122 FnName ::= Name | OperatorFront;
124-}
125fnName :: IdrisParser (Name, FC)
126fnName = try operatorFront <|> name <?> "function name"
128{- | Parses a fixity declaration
130Fixity ::=
131 FixityType Natural_t OperatorList Terminator
132 ;
134-}
135fixity :: IdrisParser PDecl
136fixity = do pushIndent
137 f <- fixityType; i <- fst <$> natural;
138 ops <- sepBy1 operator (lchar ',')
139 terminator
140 let prec = fromInteger i
141 istate <- get
142 let infixes = idris_infixes istate
143 let fs = map (Fix (f prec)) ops
144 let redecls = map (alreadyDeclared infixes) fs
145 let ill = filter (not . checkValidity) redecls
146 if null ill
147 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
148 , ibc_write = map IBCFix fs ++ ibc_write istate
149 })
150 fc <- getFC
151 return (PFix fc (f prec) ops)
152 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
153 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
154 <?> "fixity declaration"
155 where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
156 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
158 checkValidity :: (FixDecl, [FixDecl]) -> Bool
159 checkValidity (f, fs) = all (== f) fs
161 extractName :: FixDecl -> String
162 extractName (Fix _ n) = n
164{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
166 FixityType ::=
167 'infixl'
168 | 'infixr'
169 | 'infix'
170 | 'prefix'
171 ;
173 -}
174fixityType :: IdrisParser (Int -> Fixity)
175fixityType = do reserved "infixl"; return Infixl
176 <|> do reserved "infixr"; return Infixr
177 <|> do reserved "infix"; return InfixN
178 <|> do reserved "prefix"; return PrefixN
179 <?> "fixity type"