git.iko.soy/Idris-dev
on 04abcae help sign in
Idris-dev/src/Idris/Parser/Ops.hs
249 lines 9.3 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 MultiParamTypeClasses, 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.Monad
20import qualified Control.Monad.Combinators.Expr as P
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
28-- | Creates table for fixity declarations to build expression parser
29-- using pre-build and user-defined operator/fixity declarations
30table :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]
31table fixes
32 = [[prefix "-" negateExpr]] ++
33 toTable (reverse fixes) ++
34 [[noFixityBacktickOperator],
35 [binary "$" P.InfixR $ \fc _ x y -> flatten $ PApp fc x [pexp y]],
36 [binary "=" P.InfixL $ \fc _ x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]],
37 [noFixityOperator]]
38 where
40 negateExpr :: FC -> PTerm -> PTerm
41 negateExpr _ (PConstant fc (I int)) = PConstant fc $ I $ negate int
42 negateExpr _ (PConstant fc (BI bigInt)) = PConstant fc $ BI $ negate bigInt
43 negateExpr _ (PConstant fc (Fl dbl)) = PConstant fc $ Fl $ negate dbl
44 negateExpr _ (PConstSugar fc term) = negateExpr fc term
45 negateExpr fc (PAlternative ns tp terms) = PAlternative ns tp $ map (negateExpr fc) terms
46 negateExpr fc x = PApp fc (PRef fc [fc] (sUN "negate")) [pexp x]
48 flatten :: PTerm -> PTerm -- flatten application
49 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
50 flatten t = t
52 noFixityBacktickOperator :: P.Operator IdrisParser PTerm
53 noFixityBacktickOperator = P.InfixN $ do
54 (n, fc) <- withExtent backtickOperator
55 return $ \x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y]
57 -- | Operator without fixity (throws an error)
58 noFixityOperator :: P.Operator IdrisParser PTerm
59 noFixityOperator = P.InfixN $ do
60 indentGt
61 op <- P.try symbolicOperator
62 P.unexpected . P.Label . fromList $ "Operator without known fixity: " ++ op
64 -- | Calculates table for fixity declarations
65 toTable :: [FixDecl] -> [[P.Operator IdrisParser PTerm]]
66 toTable fs = map (map toBin) (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
68 toBin (Fix (PrefixN _) op) = prefix op $ \fc x ->
69 PApp fc (PRef fc [] (sUN op)) [pexp x]
70 toBin (Fix f op) = binary op (assoc f) $ \fc n x y ->
71 PApp fc (PRef fc [] n) [pexp x,pexp y]
73 assoc (Infixl _) = P.InfixL
74 assoc (Infixr _) = P.InfixR
75 assoc (InfixN _) = P.InfixN
77 isBacktick :: String -> Bool
78 isBacktick (c : _) = c == '_' || isAlpha c
79 isBacktick _ = False
81 binary :: String -> (IdrisParser (PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm) -> (FC -> Name -> PTerm -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
82 binary name ctor f
83 | isBacktick name = ctor $ P.try $ do
84 (n, fc) <- withExtent backtickOperator
85 guard $ show (nsroot n) == name
86 return $ f fc n
87 | otherwise = ctor $ do
88 indentGt
89 fc <- extent $ reservedOp name
90 indentGt
91 return $ f fc (sUN name)
93 prefix :: String -> (FC -> PTerm -> PTerm) -> P.Operator IdrisParser PTerm
94 prefix name f = P.Prefix $ do
95 fc <- extent $ reservedOp name
96 indentGt
97 return (f fc)
99{- | Parses a function used as an operator -- enclosed in backticks
102 BacktickOperator ::=
103 '`' Name '`'
104 ;
106-}
107backtickOperator :: (Parsing m, MonadState IState m) => m Name
108backtickOperator = P.between (indentGt *> lchar '`') (indentGt *> lchar '`') name
110{- | Parses an operator name (either a symbolic name or a backtick-quoted name)
113 OperatorName ::=
114 SymbolicOperator
115 | BacktickOperator
116 ;
118-}
119operatorName :: (Parsing m, MonadState IState m) => m Name
120operatorName = sUN <$> symbolicOperator
121 <|> backtickOperator
123{- | Parses an operator in function position i.e. enclosed by `()', with an
124 optional namespace
127 OperatorFront ::=
128 '(' '=' ')'
129 | (Identifier_t '.')? '(' Operator_t ')'
130 ;
133-}
134operatorFront :: Parsing m => m Name
135operatorFront = do P.try $ lchar '(' *> (eqTy <$ reservedOp "=") <* lchar ')'
136 <|> maybeWithNS (lchar '(' *> symbolicOperator <* lchar ')') []
138{- | Parses a function (either normal name or operator)
141 FnName ::= Name | OperatorFront;
143-}
144fnName :: (Parsing m, MonadState IState m) => m Name
145fnName = P.try operatorFront <|> name <?> "function name"
147{- | Parses a fixity declaration
149Fixity ::=
150 FixityType Natural_t OperatorList Terminator
151 ;
153-}
154fixity :: IdrisParser PDecl
155fixity = do ((f, i, ops), fc) <- withExtent $ do
156 pushIndent
157 f <- fixityType; i <- natural
158 ops <- P.sepBy1 (show . nsroot <$> operatorName) (lchar ',')
159 terminator
160 return (f, i, ops)
161 let prec = fromInteger i
162 istate <- get
163 let infixes = idris_infixes istate
164 let fs = map (Fix (f prec)) ops
165 let redecls = map (alreadyDeclared infixes) fs
166 let ill = filter (not . checkValidity) redecls
167 if null ill
168 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
169 , ibc_write = map IBCFix fs ++ ibc_write istate
170 })
171 return (PFix fc (f prec) ops)
172 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
173 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
174 <?> "fixity declaration"
175 where
176 alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
177 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
179 checkValidity :: (FixDecl, [FixDecl]) -> Bool
180 checkValidity (f, fs) = all (== f) fs
182 extractName :: FixDecl -> String
183 extractName (Fix _ n) = n
185-- | Check that a declaration of an operator also has fixity declared
186checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
187checkDeclFixity p = do decl <- p
188 case getDeclName decl of
189 Nothing -> return decl
190 Just n -> do checkNameFixity n
191 return decl
192 where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n
193 getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n
194 getDeclName _ = Nothing
196-- | Checks that an operator name also has a fixity declaration
197checkNameFixity :: Name -> IdrisParser ()
198checkNameFixity n = do fOk <- fixityOk n
199 unless fOk . fail $
200 "Missing fixity declaration for " ++ show n
201 where fixityOk (NS n' _) = fixityOk n'
202 fixityOk (UN n') | all (flip elem opChars) (str n') =
203 do fixities <- fmap idris_infixes get
204 return . elem (str n') . map (\ (Fix _ op) -> op) $ fixities
205 | otherwise = return True
206 fixityOk _ = return True
208{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
210 FixityType ::=
211 'infixl'
212 | 'infixr'
213 | 'infix'
214 | 'prefix'
215 ;
217 -}
218fixityType :: IdrisParser (Int -> Fixity)
219fixityType = do reserved "infixl"; return Infixl
220 <|> do reserved "infixr"; return Infixr
221 <|> do reserved "infix"; return InfixN
222 <|> do reserved "prefix"; return PrefixN
223 <?> "fixity type"
225opChars :: String
226opChars = ":!#$%&*+./<=>?@\\^|-~"
228operatorLetter :: Parsing m => m Char
229operatorLetter = P.oneOf opChars
231commentMarkers :: [String]
232commentMarkers = [ "--", "|||" ]
234invalidOperators :: [String]
235invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]
237-- | Parses an operator
238symbolicOperator :: Parsing m => m String
239symbolicOperator = do op <- token . some $ operatorLetter
240 when (op `elem` (invalidOperators ++ commentMarkers)) $
241 fail $ op ++ " is not a valid operator"
242 return op
244-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
245-- | Parses a reserved operator
246reservedOp :: Parsing m => String -> m ()
247reservedOp name = token $ P.try $
248 do string name
249 P.notFollowedBy operatorLetter <?> ("end of " ++ show name)