git.iko.soy/Idris-dev
on cd7e553 help sign in
Idris-dev/src/Idris/Parser/Ops.hs
241 lines 8.8 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 Control.Monad.State.Strict
21import Data.Char (isAlpha)
22import Data.List
23import Data.List.NonEmpty (fromList)
24import Text.Megaparsec ((<?>))
25import qualified Text.Megaparsec as P
26import qualified Text.Megaparsec.Char 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) <- withExtent 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) <- withExtent backtickOperator
77 guard $ show (nsroot n) == name
78 return $ f fc n
79 | otherwise = ctor $ do
80 indentGt
81 fc <- extent $ reservedOp 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 fc <- extent $ reservedOp name
88 indentGt
89 return (f fc)
91{- | Parses a function used as an operator -- enclosed in backticks
94 BacktickOperator ::=
95 '`' Name '`'
96 ;
98-}
99backtickOperator :: (Parsing m, MonadState IState m) => m Name
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 :: (Parsing m, MonadState IState m) => m Name
112operatorName = sUN <$> symbolicOperator
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 :: Parsing m => m Name
127operatorFront = do P.try $ lchar '(' *> (eqTy <$ reservedOp "=") <* lchar ')'
128 <|> maybeWithNS (lchar '(' *> symbolicOperator <* lchar ')') []
130{- | Parses a function (either normal name or operator)
133 FnName ::= Name | OperatorFront;
135-}
136fnName :: (Parsing m, MonadState IState m) => m Name
137fnName = P.try operatorFront <|> name <?> "function name"
139{- | Parses a fixity declaration
141Fixity ::=
142 FixityType Natural_t OperatorList Terminator
143 ;
145-}
146fixity :: IdrisParser PDecl
147fixity = do ((f, i, ops), fc) <- withExtent $ do
148 pushIndent
149 f <- fixityType; i <- natural
150 ops <- P.sepBy1 (show . nsroot <$> operatorName) (lchar ',')
151 terminator
152 return (f, i, ops)
153 let prec = fromInteger i
154 istate <- get
155 let infixes = idris_infixes istate
156 let fs = map (Fix (f prec)) ops
157 let redecls = map (alreadyDeclared infixes) fs
158 let ill = filter (not . checkValidity) redecls
159 if null ill
160 then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
161 , ibc_write = map IBCFix fs ++ ibc_write istate
162 })
163 return (PFix fc (f prec) ops)
164 else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
165 ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
166 <?> "fixity declaration"
167 where
168 alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
169 alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
171 checkValidity :: (FixDecl, [FixDecl]) -> Bool
172 checkValidity (f, fs) = all (== f) fs
174 extractName :: FixDecl -> String
175 extractName (Fix _ n) = n
177-- | Check that a declaration of an operator also has fixity declared
178checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl
179checkDeclFixity p = do decl <- p
180 case getDeclName decl of
181 Nothing -> return decl
182 Just n -> do checkNameFixity n
183 return decl
184 where getDeclName (PTy _ _ _ _ _ n _ _ ) = Just n
185 getDeclName (PData _ _ _ _ _ (PDatadecl n _ _ _)) = Just n
186 getDeclName _ = Nothing
188-- | Checks that an operator name also has a fixity declaration
189checkNameFixity :: Name -> IdrisParser ()
190checkNameFixity n = do fOk <- fixityOk n
191 unless fOk . fail $
192 "Missing fixity declaration for " ++ show n
193 where fixityOk (NS n' _) = fixityOk n'
194 fixityOk (UN n') | all (flip elem opChars) (str n') =
195 do fixities <- fmap idris_infixes get
196 return . elem (str n') . map (\ (Fix _ op) -> op) $ fixities
197 | otherwise = return True
198 fixityOk _ = return True
200{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
202 FixityType ::=
203 'infixl'
204 | 'infixr'
205 | 'infix'
206 | 'prefix'
207 ;
209 -}
210fixityType :: IdrisParser (Int -> Fixity)
211fixityType = do reserved "infixl"; return Infixl
212 <|> do reserved "infixr"; return Infixr
213 <|> do reserved "infix"; return InfixN
214 <|> do reserved "prefix"; return PrefixN
215 <?> "fixity type"
217opChars :: String
218opChars = ":!#$%&*+./<=>?@\\^|-~"
220operatorLetter :: Parsing m => m Char
221operatorLetter = P.oneOf opChars
223commentMarkers :: [String]
224commentMarkers = [ "--", "|||" ]
226invalidOperators :: [String]
227invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]
229-- | Parses an operator
230symbolicOperator :: Parsing m => m String
231symbolicOperator = do op <- token . some $ operatorLetter
232 when (op `elem` (invalidOperators ++ commentMarkers)) $
233 fail $ op ++ " is not a valid operator"
234 return op
236-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
237-- | Parses a reserved operator
238reservedOp :: Parsing m => String -> m ()
239reservedOp name = token $ P.try $
240 do string name
241 P.notFollowedBy operatorLetter <?> ("end of " ++ show name)