git.iko.soy/Idris-dev
on fdfcdd3 help sign in
Idris-dev/src/Idris/Parser/Ops.hs
219 lines 8.0 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 ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9 PatternGuards #-}
10module Idris.Parser.Ops where
12import Idris.AbsSyntax
13import Idris.Core.TT
14import Idris.Parser.Helpers
16import Prelude hiding (pi)
18import Control.Applicative
19import Control.Arrow (first)
20import Control.Monad
21import Control.Monad.State.Strict
22import Data.Char (isAlpha)
23import Data.List
24import Text.Parser.Expression
25import Text.Trifecta ((<?>))
26import qualified Text.Trifecta as P
28-- | Creates table for fixity declarations to build expression parser
29-- using pre-build and user-defined operator/fixity declarations
30table :: [FixDecl] -> OperatorTable IdrisParser PTerm
31table fixes
32 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++
33 toTable (reverse fixes) ++
34 [[noFixityBacktickOperator],
35 [binary "$" AssocRight $ \fc _ x y -> flatten $ PApp fc x [pexp y]],
36 [binary "=" AssocLeft $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],
37 [noFixityOperator]]
38 where
39 flatten :: PTerm -> PTerm -- flatten application
40 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
41 flatten t = t
43 noFixityBacktickOperator :: Operator IdrisParser PTerm
44 noFixityBacktickOperator = flip Infix AssocNone $ do
45 (n, fc) <- backtickOperator
46 return $ \x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y]
48 -- | Operator without fixity (throws an error)
49 noFixityOperator :: Operator IdrisParser PTerm
50 noFixityOperator = flip Infix AssocNone $ do
51 indentGt
52 op <- P.try symbolicOperator
53 P.unexpected $ "Operator without known fixity: " ++ op
55 -- | Calculates table for fixity declarations
56 toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
57 toTable fs = map (map toBin) (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
59 toBin (Fix (PrefixN _) op) = prefix op $ \fc x ->
60 PApp fc (PRef fc [] (sUN op)) [pexp x]
61 toBin (Fix f op) = binary op (assoc f) $ \fc n x y ->
62 PApp fc (PRef fc [] n) [pexp x,pexp y]
64 assoc (Infixl _) = AssocLeft
65 assoc (Infixr _) = AssocRight
66 assoc (InfixN _) = AssocNone
68 isBacktick :: String -> Bool
69 isBacktick (c : _) = c == '_' || isAlpha c
70 isBacktick _ = False
72 binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
73 binary name assoc f
74 | isBacktick name = flip Infix assoc $ P.try $ do
75 (n, fc) <- backtickOperator
76 guard $ show (nsroot n) == name
77 return $ f fc n
78 | otherwise = flip Infix assoc $ do
79 indentGt
80 fc <- reservedOpFC name
81 indentGt
82 return $ f fc (sUN name)
84 prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
85 prefix name f = Prefix (do reservedOp name
86 fc <- getFC
87 indentGt
88 return (f fc))
90{- | Parses a function used as an operator -- enclosed in backticks
93 BacktickOperator ::=
94 '`' Name '`'
95 ;
97-}
98backtickOperator :: IdrisParser (Name, FC)
99backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name
101{- | Parses an operator name (either a symbolic name or a backtick-quoted name)
104 OperatorName ::=
105 SymbolicOperator
106 | BacktickOperator
107 ;
109-}
110operatorName :: IdrisParser (Name, FC)
111operatorName = first sUN <$> symbolicOperatorFC
112 <|> backtickOperator
114{- | Parses an operator in function position i.e. enclosed by `()', with an
115 optional namespace
118 OperatorFront ::=
119 '(' '=' ')'
120 | (Identifier_t '.')? '(' Operator_t ')'
121 ;
124-}
125operatorFront :: IdrisParser (Name, FC)
126operatorFront = P.try (do (FC f (l, c) _) <- getFC
127 op <- lchar '(' *> reservedOp "=" <* lchar ')'
128 return (eqTy, FC f (l, c) (l, c+3)))
129 <|> maybeWithNS (do (FC f (l, c) _) <- getFC
130 op <- lchar '(' *> symbolicOperator
131 (FC _ _ (l', c')) <- getFC
132 lchar ')'
133 return (op, (FC f (l, c) (l', c' + 1)))) False []
135{- | Parses a function (either normal name or operator)
138 FnName ::= Name | OperatorFront;
140-}
141fnName :: IdrisParser (Name, FC)
142fnName = P.try operatorFront <|> name <?> "function name"
144{- | Parses a fixity declaration
146Fixity ::=
147 FixityType Natural_t OperatorList Terminator
148 ;
150-}
151fixity :: IdrisParser PDecl
152fixity = do pushIndent
153 f <- fixityType; i <- fst <$> natural;
154 ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')
155 terminator
156 let prec = fromInteger i
157 istate <- get
158 let infixes = idris_infixes istate
159 let fs = map (Fix (f prec)) ops
160 let redecls = map (alreadyDeclared infixes) fs
161 let ill = filter (not . checkValidity) redecls
162 if null ill
163 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
164 , ibc_write = map IBCFix fs ++ ibc_write istate
165 })
166 fc <- getFC
167 return (PFix fc (f prec) ops)
168 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
169 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
170 <?> "fixity declaration"
171 where
172 alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
173 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
175 checkValidity :: (FixDecl, [FixDecl]) -> Bool
176 checkValidity (f, fs) = all (== f) fs
178 extractName :: FixDecl -> String
179 extractName (Fix _ n) = n
181-- | Check that a declaration of an operator also has fixity declared
182checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
183checkDeclFixity p = do decl <- p
184 case getDeclName decl of
185 Nothing -> return decl
186 Just n -> do checkNameFixity n
187 return decl
188 where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n
189 getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n
190 getDeclName _ = Nothing
192-- | Checks that an operator name also has a fixity declaration
193checkNameFixity :: Name -> IdrisParser ()
194checkNameFixity n = do fOk <- fixityOk n
195 unless fOk . fail $
196 "Missing fixity declaration for " ++ show n
197 where fixityOk (NS n' _) = fixityOk n'
198 fixityOk (UN n') | all (flip elem opChars) (str n') =
199 do fixities <- fmap idris_infixes get
200 return . elem (str n') . map (\ (Fix _ op) -> op) $ fixities
201 | otherwise = return True
202 fixityOk _ = return True
204{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
206 FixityType ::=
207 'infixl'
208 | 'infixr'
209 | 'infix'
210 | 'prefix'
211 ;
213 -}
214fixityType :: IdrisParser (Int -> Fixity)
215fixityType = do reserved "infixl"; return Infixl
216 <|> do reserved "infixr"; return Infixr
217 <|> do reserved "infix"; return InfixN
218 <|> do reserved "prefix"; return PrefixN
219 <?> "fixity type"