git.iko.soy/Idris-dev
on c112ebc help sign in
Idris-dev/src/Idris/Parser/Ops.hs
220 lines 8.1 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 Data.List.NonEmpty (fromList)
25import Text.Parser.Expression
26import Text.Megaparsec ((<?>))
27import qualified Text.Megaparsec as P
29-- | Creates table for fixity declarations to build expression parser
30-- using pre-build and user-defined operator/fixity declarations
31table :: [FixDecl] -> OperatorTable 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 "$" AssocRight $ \fc _ x y -> flatten $ PApp fc x [pexp y]],
37 [binary "=" AssocLeft $ \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 :: Operator IdrisParser PTerm
45 noFixityBacktickOperator = flip Infix AssocNone $ 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 :: Operator IdrisParser PTerm
51 noFixityOperator = flip Infix AssocNone $ 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] -> OperatorTable 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 _) = AssocLeft
66 assoc (Infixr _) = AssocRight
67 assoc (InfixN _) = AssocNone
69 isBacktick :: String -> Bool
70 isBacktick (c : _) = c == '_' || isAlpha c
71 isBacktick _ = False
73 binary :: String -> Assoc -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> Operator IdrisParser PTerm
74 binary name assoc f
75 | isBacktick name = flip Infix assoc $ P.try $ do
76 (n, fc) <- backtickOperator
77 guard $ show (nsroot n) == name
78 return $ f fc n
79 | otherwise = flip Infix assoc $ do
80 indentGt
81 fc <- reservedOpFC name
82 indentGt
83 return $ f fc (sUN name)
85 prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
86 prefix name f = Prefix (do reservedOp name
87 fc <- getFC
88 indentGt
89 return (f fc))
91{- | Parses a function used as an operator -- enclosed in backticks
94 BacktickOperator ::=
95 '`' Name '`'
96 ;
98-}
99backtickOperator :: IdrisParser (Name, FC)
100backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name
102{- | Parses an operator name (either a symbolic name or a backtick-quoted name)
105 OperatorName ::=
106 SymbolicOperator
107 | BacktickOperator
108 ;
110-}
111operatorName :: IdrisParser (Name, FC)
112operatorName = first sUN <$> symbolicOperatorFC
113 <|> backtickOperator
115{- | Parses an operator in function position i.e. enclosed by `()', with an
116 optional namespace
119 OperatorFront ::=
120 '(' '=' ')'
121 | (Identifier_t '.')? '(' Operator_t ')'
122 ;
125-}
126operatorFront :: IdrisParser (Name, FC)
127operatorFront = P.try (do (FC f (l, c) _) <- getFC
128 op <- lchar '(' *> reservedOp "=" <* lchar ')'
129 return (eqTy, FC f (l, c) (l, c+3)))
130 <|> maybeWithNS (do (FC f (l, c) _) <- getFC
131 op <- lchar '(' *> symbolicOperator
132 (FC _ _ (l', c')) <- getFC
133 lchar ')'
134 return (op, (FC f (l, c) (l', c' + 1)))) False []
136{- | Parses a function (either normal name or operator)
139 FnName ::= Name | OperatorFront;
141-}
142fnName :: IdrisParser (Name, FC)
143fnName = P.try operatorFront <|> name <?> "function name"
145{- | Parses a fixity declaration
147Fixity ::=
148 FixityType Natural_t OperatorList Terminator
149 ;
151-}
152fixity :: IdrisParser PDecl
153fixity = do pushIndent
154 f <- fixityType; i <- fst <$> natural;
155 ops <- P.sepBy1 (show . nsroot . fst <$> operatorName) (lchar ',')
156 terminator
157 let prec = fromInteger i
158 istate <- get
159 let infixes = idris_infixes istate
160 let fs = map (Fix (f prec)) ops
161 let redecls = map (alreadyDeclared infixes) fs
162 let ill = filter (not . checkValidity) redecls
163 if null ill
164 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
165 , ibc_write = map IBCFix fs ++ ibc_write istate
166 })
167 fc <- getFC
168 return (PFix fc (f prec) ops)
169 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
170 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
171 <?> "fixity declaration"
172 where
173 alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
174 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
176 checkValidity :: (FixDecl, [FixDecl]) -> Bool
177 checkValidity (f, fs) = all (== f) fs
179 extractName :: FixDecl -> String
180 extractName (Fix _ n) = n
182-- | Check that a declaration of an operator also has fixity declared
183checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
184checkDeclFixity p = do decl <- p
185 case getDeclName decl of
186 Nothing -> return decl
187 Just n -> do checkNameFixity n
188 return decl
189 where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n
190 getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n
191 getDeclName _ = Nothing
193-- | Checks that an operator name also has a fixity declaration
194checkNameFixity :: Name -> IdrisParser ()
195checkNameFixity n = do fOk <- fixityOk n
196 unless fOk . fail $
197 "Missing fixity declaration for " ++ show n
198 where fixityOk (NS n' _) = fixityOk n'
199 fixityOk (UN n') | all (flip elem opChars) (str n') =
200 do fixities <- fmap idris_infixes get
201 return . elem (str n') . map (\ (Fix _ op) -> op) $ fixities
202 | otherwise = return True
203 fixityOk _ = return True
205{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
207 FixityType ::=
208 'infixl'
209 | 'infixr'
210 | 'infix'
211 | 'prefix'
212 ;
214 -}
215fixityType :: IdrisParser (Int -> Fixity)
216fixityType = do reserved "infixl"; return Infixl
217 <|> do reserved "infixr"; return Infixr
218 <|> do reserved "infix"; return InfixN
219 <|> do reserved "prefix"; return PrefixN
220 <?> "fixity type"