git.iko.soy/Idris-dev
on bc8da8d help sign in
Idris-dev/src/Idris/Parser/Ops.hs
221 lines 8.1 kB history raw
1{-|
2Module : Idris.Parser.Ops
3Description : Parser for operators and fixity declarations.
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 Data.List.NonEmpty (fromList)
25import Text.Megaparsec ((<?>))
26import qualified Text.Megaparsec as P
27import qualified Text.Megaparsec.Expr as P
29-- | Creates table for fixity declarations to build expression parser
30-- using pre-build and user-defined operator/fixity declarations
31table :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]
32table fixes
33 = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++
34 toTable (reverse fixes) ++
35 [[noFixityBacktickOperator],
36 [binary "$" P.InfixR $ \fc _ x y -> flatten $ PApp fc x [pexp y]],
37 [binary "=" P.InfixL $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],
38 [noFixityOperator]]
39 where
40 flatten :: PTerm -> PTerm -- flatten application
41 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
42 flatten t = t
44 noFixityBacktickOperator :: P.Operator IdrisParser PTerm
45 noFixityBacktickOperator = P.InfixN $ do
46 (n, fc) <- backtickOperator
47 return $ \x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y]
49 -- | Operator without fixity (throws an error)
50 noFixityOperator :: P.Operator IdrisParser PTerm
51 noFixityOperator = P.InfixN $ do
52 indentGt
53 op <- P.try symbolicOperator
54 P.unexpected . P.Label . fromList $ "Operator without known fixity: " ++ op
56 -- | Calculates table for fixity declarations
57 toTable :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]
58 toTable fs = map (map toBin) (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
60 toBin (Fix (PrefixN _) op) = prefix op $ \fc x ->
61 PApp fc (PRef fc [] (sUN op)) [pexp x]
62 toBin (Fix f op) = binary op (assoc f) $ \fc n x y ->
63 PApp fc (PRef fc [] n) [pexp x,pexp y]
65 assoc (Infixl _) = P.InfixL
66 assoc (Infixr _) = P.InfixR
67 assoc (InfixN _) = P.InfixN
69 isBacktick :: String -> Bool
70 isBacktick (c : _) = c == '_' || isAlpha c
71 isBacktick _ = False
73 binary :: String -> (IdrisParser (PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm) -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
74 binary name ctor f
75 | isBacktick name = ctor $ P.try $ do
76 (n, fc) <- backtickOperator
77 guard $ show (nsroot n) == name
78 return $ f fc n
79 | otherwise = ctor $ do
80 indentGt
81 fc <- reservedOpFC name
82 indentGt
83 return $ f fc (sUN name)
85 prefix :: String -> (FC -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
86 prefix name f = P.Prefix $ do
87 reservedOp name
88 fc <- getFC
89 indentGt
90 return (f fc)
92{- | Parses a function used as an operator -- enclosed in backticks
95 BacktickOperator ::=
96 '`' Name '`'
97 ;
99-}
100backtickOperator :: IdrisParser (Name, FC)
101backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name
103{- | Parses an operator name (either a symbolic name or a backtick-quoted name)
106 OperatorName ::=
107 SymbolicOperator
108 | BacktickOperator
109 ;
111-}
112operatorName :: IdrisParser (Name, FC)
113operatorName = first sUN <$> symbolicOperatorFC
114 <|> backtickOperator
116{- | Parses an operator in function position i.e. enclosed by `()', with an
117 optional namespace
120 OperatorFront ::=
121 '(' '=' ')'
122 | (Identifier_t '.')? '(' Operator_t ')'
123 ;
126-}
127operatorFront :: IdrisParser (Name, FC)
128operatorFront = P.try (do (FC f (l, c) _) <- getFC
129 op <- lchar '(' *> reservedOp "=" <* lchar ')'
130 return (eqTy, FC f (l, c) (l, c+3)))
131 <|> maybeWithNS (do (FC f (l, c) _) <- getFC
132 op <- lchar '(' *> symbolicOperator
133 (FC _ _ (l', c')) <- getFC
134 lchar ')'
135 return (op, (FC f (l, c) (l', c' + 1)))) False []
137{- | Parses a function (either normal name or operator)
140 FnName ::= Name | OperatorFront;
142-}
143fnName :: IdrisParser (Name, FC)
144fnName = P.try operatorFront <|> name <?> "function name"
146{- | Parses a fixity declaration
148Fixity ::=
149 FixityType Natural_t OperatorList Terminator
150 ;
152-}
153fixity :: IdrisParser PDecl
154fixity = do pushIndent
155 f <- fixityType; i <- fst <$> natural;
156 ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')
157 terminator
158 let prec = fromInteger i
159 istate <- get
160 let infixes = idris_infixes istate
161 let fs = map (Fix (f prec)) ops
162 let redecls = map (alreadyDeclared infixes) fs
163 let ill = filter (not . checkValidity) redecls
164 if null ill
165 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
166 , ibc_write = map IBCFix fs ++ ibc_write istate
167 })
168 fc <- getFC
169 return (PFix fc (f prec) ops)
170 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
171 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
172 <?> "fixity declaration"
173 where
174 alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
175 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
177 checkValidity :: (FixDecl, [FixDecl]) -> Bool
178 checkValidity (f, fs) = all (== f) fs
180 extractName :: FixDecl -> String
181 extractName (Fix _ n) = n
183-- | Check that a declaration of an operator also has fixity declared
184checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
185checkDeclFixity p = do decl <- p
186 case getDeclName decl of
187 Nothing -> return decl
188 Just n -> do checkNameFixity n
189 return decl
190 where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n
191 getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n
192 getDeclName _ = Nothing
194-- | Checks that an operator name also has a fixity declaration
195checkNameFixity :: Name -> IdrisParser ()
196checkNameFixity n = do fOk <- fixityOk n
197 unless fOk . fail $
198 "Missing fixity declaration for " ++ show n
199 where fixityOk (NS n' _) = fixityOk n'
200 fixityOk (UN n') | all (flip elem opChars) (str n') =
201 do fixities <- fmap idris_infixes get
202 return . elem (str n') . map (\ (Fix _ op) -> op) $ fixities
203 | otherwise = return True
204 fixityOk _ = return True
206{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
208 FixityType ::=
209 'infixl'
210 | 'infixr'
211 | 'infix'
212 | 'prefix'
213 ;
215 -}
216fixityType :: IdrisParser (Int -> Fixity)
217fixityType = do reserved "infixl"; return Infixl
218 <|> do reserved "infixr"; return Infixr
219 <|> do reserved "infix"; return InfixN
220 <|> do reserved "prefix"; return PrefixN
221 <?> "fixity type"