@@ -1,5 +1,8 @@
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2−module Idris.Parser where
2+module Idris.Parser(module Idris.Parser,
3+ module Idris.ParseExpr,
4+ module Idris.ParseHelpers,
5+ module Idris.ParseOps) where
4import Prelude hiding (pi)
7import Prelude hiding (pi)
@@ -21,6 +24,11 @@ import Idris.Coverage
21import Idris.IBC
24import Idris.IBC
22import Idris.Unlit
25import Idris.Unlit
23import Idris.Providers
26import Idris.Providers
28+import Idris.ParseHelpers
30+import Idris.ParseExpr
24import Paths_idris
32import Paths_idris
26import Util.DynamicLinker
34import Util.DynamicLinker
@@ -54,295 +62,6 @@ import System.FilePath
54 RULE{n} = rule repeated n times
62 RULE{n} = rule repeated n times
58−-- | Idris parser with state used during parsing
59−type IdrisParser = StateT IState IdrisInnerParser
61−newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }
62− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)
64−instance TokenParsing IdrisInnerParser where
65− someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
67−-- | Generalized monadic parsing constraint type
68−type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
70−{- * Space, comments and literals (token/lexing like parsers) -}
72−-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
73−simpleWhiteSpace :: MonadicParsing m => m ()
74−simpleWhiteSpace = satisfy isSpace *> pure ()
76−-- | Checks if a charcter is end of line
81−eol :: MonadicParsing m => m ()
82−eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
84−-- | Checks if a character is a documentation comment marker
85−isDocCommentMarker :: Char -> Bool
86−isDocCommentMarker '|' = True
87−isDocCommentMarker '^' = True
88−isDocCommentMarker _ = False
90−{- | Consumes a single-line comment
91− SingleLineComment_t ::= '--' EOL_t
92− | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
95−singleLineComment :: MonadicParsing m => m ()
96−singleLineComment = try (string "--" *> eol *> pure ())
97− <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> eol *> pure ()
100−{- | Consumes a multi-line comment
101− MultiLineComment_t ::=
103− | '{ -' ~DocCommentMarker_t InCommentChars_t
106− InCommentChars_t ::=
108− | MultiLineComment_t InCommentChars_t
109− | ~'- }'+ InCommentChars_t
113−multiLineComment :: MonadicParsing m => m ()
114−multiLineComment = try (string "{-" *> (string "-}") *> pure ())
115− <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars
117− where inCommentChars :: MonadicParsing m => m ()
118− inCommentChars = string "-}" *> pure ()
119− <|> try (multiLineComment) *> inCommentChars
120− <|> try (docComment '|') *> inCommentChars
121− <|> try (docComment '^') *> inCommentChars
122− <|> skipSome (noneOf startEnd) *> inCommentChars
123− <|> oneOf startEnd *> inCommentChars
124− <?> "end of comment"
128−{-| Parses a documentation comment (similar to haddoc) given a marker character
129− DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
130− | '{ -' DocCommentMarket_t ~'- }'* '- }'
133−docComment :: MonadicParsing m => Char -> m String
134−docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)
135− | otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"
136− where docComment' :: MonadicParsing m => Char -> m String
137− docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* eol
138− <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
141−-- | Parses some white space
142−whiteSpace :: MonadicParsing m => m ()
143−whiteSpace = Tok.whiteSpace
145−-- | Parses a string literal
146−stringLiteral :: MonadicParsing m => m String
147−stringLiteral = Tok.stringLiteral
149−-- | Parses a char literal
150−charLiteral :: MonadicParsing m => m Char
151−charLiteral = Tok.charLiteral
153−-- | Parses a natural number
154−natural :: MonadicParsing m => m Integer
155−natural = Tok.natural
157−-- | Parses an integral number
158−integer :: MonadicParsing m => m Integer
159−integer = Tok.integer
161−-- | Parses a floating point number
162−float :: MonadicParsing m => m Double
165−{- * Symbols, identifiers, names and operators -}
168−-- | Idris Style for parsing identifiers/reserved keywords
169−idrisStyle :: MonadicParsing m => IdentifierStyle m
170−idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
171− where _styleName = "Idris"
172− _styleStart = satisfy isAlpha
173− _styleLetter = satisfy isAlphaNum <|> oneOf "_'" <|> (lchar '.')
174− _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",
175− "do", "dsl", "import", "impossible",
176− "case", "of", "total", "partial", "mutual",
177− "infix", "infixl", "infixr", "rewrite",
178− "where", "with", "syntax", "proof", "postulate",
179− "using", "namespace", "class", "instance",
180− "public", "private", "abstract", "implicit",
182− "Int", "Integer", "Float", "Char", "String", "Ptr",
183− "Bits8", "Bits16", "Bits32", "Bits64",
184− "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
186−char :: MonadicParsing m => Char -> m Char
189−string :: MonadicParsing m => String -> m String
192−-- | Parses a character as a token
193−lchar :: MonadicParsing m => Char -> m Char
196−-- | Parses string as a token
197−symbol :: MonadicParsing m => String -> m String
200−-- | Parses a reserved identifier
201−reserved :: MonadicParsing m => String -> m ()
202−reserved = Tok.reserve idrisStyle
204−-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
205−-- | Parses a reserved operator
206−reservedOp :: MonadicParsing m => String -> m ()
207−reservedOp name = token $ try $
209− notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
211−-- | Parses an identifier as a token
212−identifier :: MonadicParsing m => m String
213−identifier = token $ Tok.ident idrisStyle
215−-- | Parses an identifier with possible namespace as a name
216−iName :: MonadicParsing m => [String] -> m Name
217−iName bad = maybeWithNS identifier False bad <?> "name"
219−-- | Parses an string possibly prefixed by a namespace
220−maybeWithNS :: MonadicParsing m => m String -> Bool -> [String] -> m Name
221−maybeWithNS parser ascend bad = do
222− i <- option "" (lookAhead identifier)
223− when (i `elem` bad) $ unexpected "reserved identifier"
224− let transf = if ascend then id else reverse
225− (x, xs) <- choice (transf (parserNoNS parser : parsersNS parser i))
226− return $ mkName (x, xs)
227− where parserNoNS :: MonadicParsing m => m String -> m (String, String)
228− parserNoNS parser = do x <- parser; return (x, "")
229− parserNS :: MonadicParsing m => m String -> String -> m (String, String)
230− parserNS parser ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
231− parsersNS :: MonadicParsing m => m String -> String -> [m (String, String)]
232− parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
235−name :: IdrisParser Name
237− iName (syntax_keywords i)
241−{- | List of all initial segments in ascending order of a list. Every such
242− initial segment ends right before an element satisfying the given
245−initsEndAt :: (a -> Bool) -> [a] -> [[a]]
247−initsEndAt p (x:xs) | p x = [] : x_inits_xs
248− | otherwise = x_inits_xs
249− where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
252−{- | Create a `Name' from a pair of strings representing a base name and its
255−mkName :: (String, String) -> Name
256−mkName (n, "") = UN n
257−mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
258− where parseNS x = case span (/= '.') x of
260− (x, '.':y) -> x : parseNS y
262−operatorLetter :: MonadicParsing m => m Char
263−operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
265−-- | Parses an operator
266−operator :: MonadicParsing m => m String
267−operator = do op <- token . some $ operatorLetter
268− when (op == ":") $ fail "(:) is not a valid operator"
271−{- * Position helpers -}
272−{- | Get filename from position (returns "(interactive)" when no source file is given) -}
273−fileName :: Delta -> String
274−fileName (Directed fn _ _ _ _) = UTF8.toString fn
275−fileName _ = "(interactive)"
277−{- | Get line number from position -}
278−lineNum :: Delta -> Int
279−lineNum (Lines l _ _ _) = fromIntegral l + 1
280−lineNum (Directed _ l _ _ _) = fromIntegral l + 1
282−{- | Get file position as FC -}
283−getFC :: MonadicParsing m => m FC
284−getFC = do s <- position
285− let (dir, file) = splitFileName (fileName s)
286− let f = if dir == addTrailingPathSeparator "." then file else fileName s
287− return $ FC f (lineNum s)
290−-- | Bind constraints to term
291−bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm
292−bindList b [] sc = sc
293−bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
295−{- |Creates table for fixtiy declarations to build expression parser using
296− pre-build and user-defined operator/fixity declarations -}
297−table :: [FixDecl] -> OperatorTable IdrisParser PTerm
299− = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
300− [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
301− ++ toTable (reverse fixes) ++
303− [binary "=" PEq AssocLeft],
304− [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
306−{- |Calculates table for fixtiy declarations -}
307−toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
308−toTable fs = map (map toBin)
309− (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
310− where toBin (Fix (PrefixN _) op) = prefix op
311− (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
313− = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
314− assoc (Infixl _) = AssocLeft
315− assoc (Infixr _) = AssocRight
316− assoc (InfixN _) = AssocNone
318−{- |Binary operator -}
319−binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
320−binary name f = Infix (do fc <- getFC
322− doc <- option "" (docComment '^')
325−{- |Prefix operator -}
326−prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
327−prefix name f = Prefix (do reservedOp name
331−{- |Backtick operator -}
332−backtick :: Operator IdrisParser PTerm
333−backtick = Infix (do lchar '`'; n <- fnName
336− return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
338−-- | Allow implicit type declarations
339−allowImp :: SyntaxInfo -> SyntaxInfo
340−allowImp syn = syn { implicitAllowed = True }
342−-- | Disallow implicit type declarations
343−disallowImp :: SyntaxInfo -> SyntaxInfo
344−disallowImp syn = syn { implicitAllowed = False }
346-- | Adds accessibility option for function
65-- | Adds accessibility option for function
347addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
66addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
348addAcc n a = do i <- get
67addAcc n a = do i <- get
@@ -362,140 +81,6 @@ accData a n ns = do addAcc n a
362fixErrorMsg :: String -> [String] -> String
81fixErrorMsg :: String -> [String] -> String
363fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
82fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
365−{- * Layout helpers -}
367−-- | Push indentation to stack
368−pushIndent :: IdrisParser ()
369−pushIndent = do pos <- position
371− put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
373−-- | Pops indentation from stack
374−popIndent :: IdrisParser ()
375−popIndent = do ist <- get
376− let (x : xs) = indent_stack ist
377− put (ist { indent_stack = xs })
379−-- | Gets current indentation
380−indent :: IdrisParser Int
381−indent = liftM ((+1) . fromIntegral . column) position
383−-- | Gets last indentation
384−lastIndent :: IdrisParser Int
385−lastIndent = do ist <- get
386− case indent_stack ist of
387− (x : xs) -> return x
390−-- | Applies parser in an indented position
391−indented :: IdrisParser a -> IdrisParser a
392−indented p = notEndBlock *> p <* keepTerminator
394−-- | Applies parser to get a block (which has possibly indented statements)
395−indentedBlock :: IdrisParser a -> IdrisParser [a]
396−indentedBlock p = do openBlock
398− res <- many (indented p)
403−-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
404−indentedBlock1 :: IdrisParser a -> IdrisParser [a]
405−indentedBlock1 p = do openBlock
407− res <- some (indented p)
412−-- | Applies parser to get a block with exactly one (possibly indented) statement
413−indentedBlockS :: IdrisParser a -> IdrisParser a
414−indentedBlockS p = do openBlock
422−-- | Checks if the following character matches provided parser
423−lookAheadMatches :: MonadicParsing m => m a -> m Bool
424−lookAheadMatches p = do match <- lookAhead (optional p)
425− return $ isJust match
427−-- | Parses a start of block
428−openBlock :: IdrisParser ()
429−openBlock = do lchar '{'
431− put (ist { brace_stack = Nothing : brace_stack ist })
434− -- if we're not indented further, it's an empty block, so
435− -- increment lvl to ensure we get to the end
436− let lvl = case brace_stack ist of
438− if lvl' <= lvl_old then lvl_old+1
440− [] -> if lvl' == 1 then 2 else lvl'
442− put (ist { brace_stack = Just lvl : brace_stack ist })
443− <?> "start of block"
445−-- | Parses an end of block
446−closeBlock :: IdrisParser ()
447−closeBlock = do ist <- get
448− bs <- case brace_stack ist of
449− [] -> eof >> return []
450− Nothing : xs -> lchar '}' >> return xs <?> "end of block"
451− Just lvl : xs -> (do i <- indent
452− isParen <- lookAheadMatches (char ')')
453− if i >= lvl && not isParen
454− then fail "not end of block"
456− <|> (do notOpenBraces
459− put (ist { brace_stack = bs })
461−-- | Parses a terminator
462−terminator :: IdrisParser ()
463−terminator = do lchar ';'; popIndent
464− <|> do c <- indent; l <- lastIndent
465− if c <= l then popIndent else fail "not a terminator"
466− <|> do isParen <- lookAheadMatches (oneOf ")}")
467− if isParen then popIndent else fail "not a termiantor"
470−-- | Parses and keeps a terminator
471−keepTerminator :: IdrisParser ()
472−keepTerminator = do lchar ';'; return ()
473− <|> do c <- indent; l <- lastIndent
474− unless (c <= l) $ fail "not a terminator"
475− <|> do isParen <- lookAheadMatches (oneOf ")}|")
476− unless isParen $ fail "not a terminator"
479−-- | Checks if application expression does not end
480−notEndApp :: IdrisParser ()
481−notEndApp = do c <- indent; l <- lastIndent
482− when (c <= l) (fail "terminator")
484−-- | Checks that it is not end of block
485−notEndBlock :: IdrisParser ()
486−notEndBlock = do ist <- get
487− case brace_stack ist of
488− Just lvl : xs -> do i <- indent
489− isParen <- lookAheadMatches (char ')')
490− when (i < lvl || isParen) (fail "end of block")
493−notOpenBraces :: IdrisParser ()
494−notOpenBraces = do ist <- get
495− when (hasNothing $ brace_stack ist) $ fail "end of input"
496− where hasNothing :: [Maybe a] -> Bool
497− hasNothing = any isNothing
499{- * Main grammar -}
84{- * Main grammar -}
501{- | Parses module definition
86{- | Parses module definition
@@ -757,20 +342,6 @@ fnOpts opts
757 return (Just (fromInteger reds)))
342 return (Just (fromInteger reds)))
758 return (n, t)
343 return (n, t)
760−{- | Parses an operator in function position i.e. enclosed by `()', with an
763− OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
765−operatorFront :: IdrisParser Name
766−operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
768−{- | Parses a function (either normal name or operator)
769− FnName ::= Name | OperatorFront;
771−fnName :: IdrisParser Name
772−fnName = try operatorFront <|> name <?> "function name"
774{- | Parses an accessibilty modifier (e.g. public, private) -}
345{- | Parses an accessibilty modifier (e.g. public, private) -}
775accessibility :: IdrisParser Accessibility
346accessibility :: IdrisParser Accessibility
776accessibility = do reserved "public"; return Public
347accessibility = do reserved "public"; return Public
@@ -989,695 +560,6 @@ instance_ syn = do reserved "instance"; fc <- getFC
989 <?> "instance name"
560 <?> "instance name"
992−{- | Parses an expression as a whole
993− FullExpr ::= Expr EOF_t;
995−fullExpr :: SyntaxInfo -> IdrisParser PTerm
996−fullExpr syn = do x <- expr syn
999− return $ desugar syn i x
1002−{- |Parses an expression
1005−expr :: SyntaxInfo -> IdrisParser PTerm
1006−expr syn = do i <- get
1007− buildExpressionParser (table (idris_infixes i)) (expr' syn)
1009−{- | Parses either an internally defined expression or
1012−Expr' ::= "External (User-defined) Syntax"
1016−expr' :: SyntaxInfo -> IdrisParser PTerm
1017−expr' syn = try (externalExpr syn)
1018− <|> internalExpr syn
1021−{- | Parses a user-defined expression -}
1022−externalExpr :: SyntaxInfo -> IdrisParser PTerm
1023−externalExpr syn = do i <- get
1024− extensions syn (syntax_rules i)
1025− <?> "user-defined expression"
1027−{- | Parses a simple user-defined expression -}
1028−simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
1029−simpleExternalExpr syn = do i <- get
1030− extensions syn (filter isSimple (syntax_rules i))
1032− isSimple (Rule (Expr x:xs) _ _) = False
1033− isSimple (Rule (SimpleExpr x:xs) _ _) = False
1034− isSimple (Rule [Keyword _] _ _) = True
1035− isSimple (Rule [Symbol _] _ _) = True
1036− isSimple (Rule (_:xs) _ _) = case last xs of
1042−{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
1043−extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
1044−extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
1045− <?> "user-defined expression"
1047− isValid :: Syntax -> Bool
1048− isValid (Rule _ _ AnySyntax) = True
1049− isValid (Rule _ _ PatternSyntax) = inPattern syn
1050− isValid (Rule _ _ TermSyntax) = not (inPattern syn)
1053−data SynMatch = SynTm PTerm | SynBind Name
1055−{- | Tries to parse an expression given a user-defined rule -}
1056−extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm
1057−extension syn (Rule ssym ptm _)
1058− = do smap <- mapM extensionSymbol ssym
1059− let ns = mapMaybe id smap
1060− return (update ns ptm) -- updated with smap
1062− extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
1063− extensionSymbol (Keyword n) = do reserved (show n); return Nothing
1064− extensionSymbol (Expr n) = do tm <- expr syn
1065− return $ Just (n, SynTm tm)
1066− extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
1067− return $ Just (n, SynTm tm)
1068− extensionSymbol (Binding n) = do b <- name
1069− return $ Just (n, SynBind b)
1070− extensionSymbol (Symbol s) = do symbol s
1072− dropn :: Name -> [(Name, a)] -> [(Name, a)]
1074− dropn n ((x,t) : xs) | n == x = xs
1075− | otherwise = (x,t):dropn n xs
1077− updateB :: [(Name, SynMatch)] -> Name -> Name
1078− updateB ns n = case lookup n ns of
1079− Just (SynBind t) -> t
1082− update :: [(Name, SynMatch)] -> PTerm -> PTerm
1083− update ns (PRef fc n) = case lookup n ns of
1084− Just (SynTm t) -> t
1086− update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1087− update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
1088− update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
1089− (update (dropn n ns) sc)
1090− update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
1091− update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
1092− update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
1093− update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
1094− update ns (PAlternative a as) = PAlternative a (map (update ns) as)
1095− update ns (PHidden t) = PHidden (update ns t)
1096− update ns (PDoBlock ds) = PDoBlock $ upd ns ds
1097− where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]
1098− upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
1099− upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
1100− upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
1101− : upd (dropn n ns) ds
1102− upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
1104− upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
1106− update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
1109−{- |Parses a (normal) built-in expression
1125−internalExpr :: SyntaxInfo -> IdrisParser PTerm
1128− <|> try (matchApp syn)
1129− <|> try (unifyLog syn)
1131− <|> try (simpleExpr syn)
1135− <|> rewriteTerm syn
1140−{- | Parses a case expression
1142− 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
1144−caseExpr :: SyntaxInfo -> IdrisParser PTerm
1145−caseExpr syn = do reserved "case"; fc <- getFC
1146− scr <- expr syn; reserved "of";
1147− opts <- indentedBlock1 (caseOption syn)
1148− return (PCase fc scr opts)
1149− <?> "case expression"
1151−{- | Parses a case in a case expression
1153− Expr '=>' Expr Terminator
1156−caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
1157−caseOption syn = do lhs <- expr (syn { inPattern = True })
1158− symbol "=>"; r <- expr syn
1162−{- | Parses a proof block
1164− 'proof' OpenBlock Tactic'* CloseBlock
1167−proofExpr :: SyntaxInfo -> IdrisParser PTerm
1168−proofExpr syn = do reserved "proof"
1169− ts <- indentedBlock (tactic syn)
1173−{- | Parses a tactics block
1175− 'tactics' OpenBlock Tactic'* CloseBlock
1178−tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
1179−tacticsExpr syn = do reserved "tactics"
1180− ts <- indentedBlock (tactic syn)
1181− return $ PTactics ts
1182− <?> "tactics block"
1184−{- | Parses a simple expresion
1189− | 'refl' ('{' Expr '}')?
1203− | {- External (User-defined) Simple Expression -}
1206−simpleExpr :: SyntaxInfo -> IdrisParser PTerm
1208− {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
1209− <|>-} do lchar '?'; x <- name; return (PMetavar x)
1210− <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
1211− <|> do reserved "refl"; fc <- getFC;
1212− tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
1214− return (PRefl fc tm)
1216− <|> tacticsExpr syn
1218− <|> try (do fc <- getFC
1220− return (PRef fc x))
1221− <|> try (listExpr syn)
1222− <|> try (comprehension syn)
1224− <|> try (idiom syn)
1226− bracketed (disallowImp syn)
1227− <|> try (do c <- constant
1229− return (modifyConst syn fc (PConstant c)))
1230− <|> do reserved "Type"; return PType
1231− <|> try (do symbol "_|_"
1233− return (PFalse fc))
1234− <|> do lchar '_'; return Placeholder
1235− <|> simpleExternalExpr syn
1239−{- |Parses the rest of an expression in braces
1244− | Expr '**' Expr ')'
1245− | Operator Expr ')'
1246− | Expr Operator ')'
1247− | Name ':' Expr '**' Expr ')'
1250−bracketed :: SyntaxInfo -> IdrisParser PTerm
1256− try (do l <- expr syn
1259− <|> do (l, fc) <- try (do
1264− rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')
1266− return $ PPair fc l (mergePairs rs)
1267− <|> do (l, fc) <- try (do
1274− return (PDPair fc l Placeholder r)
1275− <|> try(do fc0 <- getFC
1276− l <- simpleExpr syn
1279− return $ PLam (MN 1000 "ARG") Placeholder
1280− (PApp fc0 (PRef fc0 (UN o)) [pexp l,
1281− pexp (PRef fc0 (MN 1000 "ARG"))]))
1282− <|> try(do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
1283− return $ PLam (MN 1000 "ARG") Placeholder
1284− (PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
1286− <|> try (do ln <- name; lchar ':'
1292− return (PDPair fc (PRef fc ln) lty r))
1293− <?> "end of braced expression"
1294− where mergePairs :: [(PTerm, FC)] -> PTerm
1295− mergePairs [(t, fc)] = t
1296− mergePairs ((t, fc):rs) = PPair fc t (mergePairs rs)
1298−-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
1299−-- big integer, otherwise try fromInteger and the constants as alternatives.
1300−-- a better solution would be to fix fromInteger to work with Integer, as the
1301−-- name suggests, rather than Int
1302−{-| Finds optimal type for integer constant -}
1303−modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
1304−modifyConst syn fc (PConstant (BI x))
1305− | not (inPattern syn)
1306− = PAlternative False
1307− (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
1309− | otherwise = PAlternative False consts
1311− consts = [ PConstant (BI x)
1312− , PConstant (I (fromInteger x))
1313− , PConstant (B8 (fromInteger x))
1314− , PConstant (B16 (fromInteger x))
1315− , PConstant (B32 (fromInteger x))
1316− , PConstant (B64 (fromInteger x))
1318−modifyConst syn fc x = x
1320−{- | Parses a list literal expression e.g. [1,2,3]
1327− | Expr ',' ExprList
1331−listExpr :: SyntaxInfo -> IdrisParser PTerm
1332−listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
1333− return (mkList fc xs)
1334− <?> "list expression"
1336− mkList :: FC -> [PTerm] -> PTerm
1337− mkList fc [] = PRef fc (UN "Nil")
1338− mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
1341−{- | Parses an alternative expression
1342− Alt ::= '(|' Expr_List '|)';
1346− | Expr' ',' Expr_List
1349−alt :: SyntaxInfo -> IdrisParser PTerm
1350−alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
1351− return (PAlternative False alts)
1353−{- | Parses a possibly hidden simple expression
1359−hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
1362− e <- simpleExpr syn
1367−{- | Parses a matching application expression
1369− SimpleExpr '<==' FnName
1372−matchApp :: SyntaxInfo -> IdrisParser PTerm
1373−matchApp syn = do ty <- simpleExpr syn
1377− return (PLet (MN 0 "match")
1380− (PRef fc (MN 0 "match")))
1381− <?> "matching application expression"
1383−{- | Parses a unification log expression
1385− '%' 'unifyLog' SimpleExpr
1388−unifyLog :: SyntaxInfo -> IdrisParser PTerm
1389−unifyLog syn = do lchar '%'; reserved "unifyLog";
1390− tm <- simpleExpr syn
1391− return (PUnifyLog tm)
1392− <?> "unification log expression"
1394−{- | Parses a function application expression
1396− 'mkForeign' Arg Arg*
1400−app :: SyntaxInfo -> IdrisParser PTerm
1401−app syn = do f <- reserved "mkForeign"
1404− args <- many (do notEndApp; arg syn)
1406− -- mkForeign f args ==>
1407− -- liftPrimIO (\w => mkForeignPrim f args w)
1408− let ap = PApp fc (PRef fc (UN "liftPrimIO"))
1409− [pexp (PLam (MN 0 "w")
1411− (PApp fc (PRef fc (UN "mkForeignPrim"))
1413− [pexp (PRef fc (MN 0 "w"))])))]
1414− return (dslify i ap)
1416− <|> do f <- simpleExpr syn
1418− args <- some (do notEndApp; arg syn)
1420− return (dslify i $ PApp fc f args)
1421− <?> "function application"
1423− dslify :: IState -> PTerm -> PTerm
1424− dslify i (PApp fc (PRef _ f) [a])
1425− | [d] <- lookupCtxt f (idris_dsls i)
1426− = desugar (syn { dsl_info = d }) i (getTm a)
1429−{- |Parses a function argument
1436−arg :: SyntaxInfo -> IdrisParser PArg
1437−arg syn = implicitArg syn
1438− <|> constraintArg syn
1439− <|> do e <- simpleExpr syn
1441− <?> "function argument"
1443−{- |Parses an implicit function argument
1445− '{' Name ('=' Expr)? '}'
1448−implicitArg :: SyntaxInfo -> IdrisParser PArg
1449−implicitArg syn = do lchar '{'
1452− v <- option (PRef fc n) (do lchar '='
1456− <?> "implicit function argument"
1458−{- |Parses a constraint argument (for selecting a named type class instance)
1463−constraintArg :: SyntaxInfo -> IdrisParser PArg
1464−constraintArg syn = do symbol "@{"
1468− <?> "constraint argument"
1471−{- |Parses a record field setter expression
1473− 'record' '{' FieldTypeList '}';
1477− | FieldType ',' FieldTypeList
1484−recordType :: SyntaxInfo -> IdrisParser PTerm
1486− = do reserved "record"
1488− fields <- sepBy1 fieldType (lchar ',')
1491− rec <- optional (simpleExpr syn)
1494− return (PLam (MN 0 "fldx") Placeholder
1495− (applyAll fc fields (PRef fc (MN 0 "fldx"))))
1496− Just v -> return (applyAll fc fields v)
1497− <?> "record setting expression"
1498− where fieldType :: IdrisParser (Name, PTerm)
1499− fieldType = do n <- fnName
1504− applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
1505− applyAll fc [] x = x
1506− applyAll fc ((n, e) : es) x
1507− = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
1509−{- |Creates setters for record types on necessary functions -}
1510−mkType :: Name -> Name
1511−mkType (UN n) = UN ("set_" ++ n)
1512−mkType (MN 0 n) = MN 0 ("set_" ++ n)
1513−mkType (NS n s) = NS (mkType n) s
1515−{- |Parses a type signature
1519−TypeExpr ::= ConstraintList? Expr;
1521−typeExpr :: SyntaxInfo -> IdrisParser PTerm
1522−typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
1524− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1525− <?> "type signature"
1527−{- |Parses a lambda expression
1529− '\\' TypeOptDeclList '=>' Expr
1530− | '\\' SimpleExprList '=>' Expr
1534− | SimpleExpr ',' SimpleExprList
1537−lambda :: SyntaxInfo -> IdrisParser PTerm
1538−lambda syn = do lchar '\\'
1539− try (do xt <- tyOptDeclList syn
1542− return (bindList PLam xt sc)
1543− <|> (do ps <- sepBy (do fc <- getFC
1544− e <- simpleExpr syn
1545− return (fc, e)) (lchar ',')
1548− return (pmList (zip [0..] ps) sc)))
1549− <?> "lambda expression"
1550− where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
1552− pmList ((i, (fc, x)) : xs) sc
1553− = PLam (MN i "lamp") Placeholder
1554− (PCase fc (PRef fc (MN i "lamp"))
1555− [(x, pmList xs sc)])
1557−{- |Parses a term rewrite expression
1559− 'rewrite' Expr ('==>' Expr)? 'in' Expr
1562−rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
1563−rewriteTerm syn = do reserved "rewrite"
1566− giving <- optional (do symbol "==>"; expr' syn)
1567− reserved "in"; sc <- expr syn
1568− return (PRewrite fc
1569− (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
1571− <?> "term rewrite expression"
1573−{- |Parses a let binding
1575− 'let' Name TypeSig'? '=' Expr 'in' Expr
1576−| 'let' Expr' '=' Expr' 'in' Expr
1582−let_ :: SyntaxInfo -> IdrisParser PTerm
1583−let_ syn = try (do reserved "let"; n <- name;
1584− ty <- option Placeholder (do lchar ':'; expr' syn)
1587− reserved "in"; sc <- expr syn
1588− return (PLet n ty v sc))
1589− <|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
1590− symbol "="; v <- expr syn
1591− reserved "in"; sc <- expr syn
1592− return (PCase fc v [(pat, sc)]))
1595−{- |Parses a quote goal
1597− 'quoteGoal' Name 'by' Expr 'in' Expr
1600−quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1601−quoteGoal syn = do reserved "quoteGoal"; n <- name;
1607− return (PGoal fc r n sc)
1608− <?> "quote goal expression"
1610−{- |Parses a dependent type signature
1612− '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
1613− | '|'? Static? '{' TypeDeclList '}' '->' Expr
1614− | '{' 'auto' TypeDeclList '}' '->' Expr
1615− | '{' 'default' TypeDeclList '}' '->' Expr
1616− | '{' 'static' '}' Expr' '->' Expr
1620−pi :: SyntaxInfo -> IdrisParser PTerm
1622− do lazy <- if implicitAllowed syn -- laziness is top level only
1623− then option False (do lchar '|'; return True)
1626− (do try(lchar '('); xt <- typeDeclList syn; lchar ')'
1627− doc <- option "" (docComment '^')
1630− return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do
1632− (do reserved "auto"
1633− when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"
1634− xt <- typeDeclList syn
1638− return (bindList (PPi
1639− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do
1641− when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"
1642− script <- simpleExpr syn
1643− xt <- typeDeclList syn
1647− return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do
1653− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)) <|> (
1654− if implicitAllowed syn then do
1655− xt <- typeDeclList syn
1659− return (bindList (PPi (Imp lazy st "")) xt sc)
1660− else do fail "no implicit arguments allowed here"))
1661− <?> "dependent type signature"
1663−{- | Parses a type constraint list
1665− '(' Expr_List ')' '=>'
1669−constraintList :: SyntaxInfo -> IdrisParser [PTerm]
1670−constraintList syn = try (do lchar '('
1671− tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')
1675− <|> try (do t <- expr (disallowImp syn)
1679− <?> "type constraint list"
1681{- | Parses a using declaration list
563{- | Parses a using declaration list
1682UsingDeclList ::=
564UsingDeclList ::=
1683 UsingDeclList'
565 UsingDeclList'
@@ -1719,194 +601,6 @@ usingDecl syn = try (do x <- fnName
1719 return (UConstraint c xs)
601 return (UConstraint c xs)
1720 <?> "using declaration"
602 <?> "using declaration"
1722−{- |Parses a type declaration list
1724− FunctionSignatureList
1728−FunctionSignatureList ::=
1730− | Name TypeSig ',' FunctionSignatureList
1733−typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1734−typeDeclList syn = try (sepBy1 (do x <- fnName
1736− t <- typeExpr (disallowImp syn)
1739− <|> do ns <- sepBy1 name (lchar ',')
1741− t <- typeExpr (disallowImp syn)
1742− return (map (\x -> (x, t)) ns)
1743− <?> "type declaration list"
1745−{- |Parses a type declaration list with optional parameters
1747− NameOrPlaceholder TypeSig?
1748− | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1751−NameOrPlaceHolder ::= Name | '_';
1753−tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1754−tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
1755− t <- option Placeholder (do lchar ':'
1759− <?> "type declaration list"
1760− where nameOrPlaceholder :: IdrisParser Name
1761− nameOrPlaceholder = fnName
1763− return (MN 0 "underscore")
1764− <?> "name or placeholder"
1766−{- |Parses a list comprehension
1767−Comprehension ::= '[' Expr '|' DoList ']';
1774−comprehension :: SyntaxInfo -> IdrisParser PTerm
1780− qs <- sepBy1 (do_ syn) (lchar ',')
1782− return (PDoBlock (map addGuard qs ++
1783− [DoExp fc (PApp fc (PRef fc (UN "return"))
1785− <?> "list comprehension"
1786− where addGuard :: PDo -> PDo
1787− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1791−{- |Parses a do-block
1792−Do' ::= Do KeepTerminator;
1795− 'do' OpenBlock Do'+ CloseBlock
1798−doBlock :: SyntaxInfo -> IdrisParser PTerm
1801− ds <- indentedBlock (do_ syn)
1802− return (PDoBlock ds)
1805−{- |Parses an expression inside a do block
1807− 'let' Name TypeSig'? '=' Expr
1808− | 'let' Expr' '=' Expr
1814−do_ :: SyntaxInfo -> IdrisParser PDo
1816− = try (do reserved "let"
1818− ty <- option Placeholder (do lchar ':'
1823− return (DoLet fc i ty e))
1824− <|> try (do reserved "let"
1829− return (DoLetP fc i sc))
1830− <|> try (do i <- name
1834− return (DoBind fc i e))
1835− <|> try (do i <- expr' syn
1839− return (DoBindP fc i e))
1840− <|> do e <- expr syn
1842− return (DoExp fc e)
1843− <?> "do block expression"
1845−{- |Parses an expression in idiom brackets
1846−Idiom ::= '[|' Expr '|]';
1848−idiom :: SyntaxInfo -> IdrisParser PTerm
1854− return (PIdiom fc e)
1855− <?> "expression in idiom brackets"
1857−{- |Parses a constant or literal expression
1879−constant :: IdrisParser Core.TT.Const
1880−constant = do reserved "Integer";return (AType (ATInt ITBig))
1881− <|> do reserved "Int"; return (AType (ATInt ITNative))
1882− <|> do reserved "Char"; return (AType (ATInt ITChar))
1883− <|> do reserved "Float"; return (AType ATFloat)
1884− <|> do reserved "String"; return StrType
1885− <|> do reserved "Ptr"; return PtrType
1886− <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
1887− <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
1888− <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
1889− <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
1890− <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
1891− <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
1892− <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
1893− <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
1894− <|> try (do f <- float; return $ Fl f)
1895− <|> try (do i <- natural; return $ BI i)
1896− <|> try (do s <- stringLiteral; return $ Str s)
1897− <|> try (do c <- charLiteral; return $ Ch c)
1898− <?> "constant or literal"
1900−{- |Parses a static modifier
1905−static :: IdrisParser Static
1906−static = do lchar '['; reserved "static"; lchar ']'; return Static
1908− <?> "static modifier"
1910{- |Parses a record type declaration
604{- |Parses a record type declaration
1911Record ::=
605Record ::=
1912 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
606 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
@@ -2423,118 +1117,6 @@ transform syn = do try (lchar '%' *> reserved "transform")
2423 return [PTransform fc False l r]
1117 return [PTransform fc False l r]
2424 <?> "transform"
1118 <?> "transform"
2426−{- | Parses a tactic script
2427−Tactic ::= 'intro' NameList?
2429− | 'refine' Name Imp+
2433− | 'let' Name ':' Expr' '=' Expr
2434− | 'let' Name '=' Expr
2437− | 'applyTactic' Expr
2440− | 'try' Tactic '|' Tactic
2441− | '{' TacticSeq '}'
2458− | Tactic ';' TacticSeq
2463−tactic :: SyntaxInfo -> IdrisParser PTactic
2464−tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
2466− <|> do reserved "intros"; return Intros
2467− <|> try (do reserved "refine"; n <- name
2469− return $ Refine n imps)
2470− <|> do reserved "refine"; n <- name
2472− return $ Refine n []
2473− <|> do reserved "mrefine"; n <- name
2475− return $ MatchRefine n
2476− <|> do reserved "rewrite"; t <- expr syn;
2478− return $ Rewrite (desugar syn i t)
2479− <|> do reserved "equiv"; t <- expr syn;
2481− return $ Equiv (desugar syn i t)
2482− <|> try (do reserved "let"; n <- name; lchar ':';
2483− ty <- expr' syn; lchar '='; t <- expr syn;
2485− return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
2486− <|> try (do reserved "let"; n <- name; lchar '=';
2489− return $ LetTac n (desugar syn i t))
2490− <|> do reserved "focus"; n <- name
2492− <|> do reserved "exact"; t <- expr syn;
2494− return $ Exact (desugar syn i t)
2495− <|> do reserved "applyTactic"; t <- expr syn;
2497− return $ ApplyTactic (desugar syn i t)
2498− <|> do reserved "reflect"; t <- expr syn;
2500− return $ Reflect (desugar syn i t)
2501− <|> do reserved "fill"; t <- expr syn;
2503− return $ Fill (desugar syn i t)
2504− <|> do reserved "try"; t <- tactic syn;
2511− ts <- sepBy1 (tactic syn) (lchar ';')
2513− return $ TSeq t (mergeSeq ts)
2514− <|> do reserved "compute"; return Compute
2515− <|> do reserved "trivial"; return Trivial
2516− <|> do reserved "solve"; return Solve
2517− <|> do reserved "attack"; return Attack
2518− <|> do reserved "state"; return ProofState
2519− <|> do reserved "term"; return ProofTerm
2520− <|> do reserved "undo"; return Undo
2521− <|> do reserved "qed"; return Qed
2522− <|> do reserved "abandon"; return Abandon
2523− <|> do lchar ':'; reserved "q"; return Abandon
2526− imp :: IdrisParser Bool
2527− imp = do lchar '?'; return False
2528− <|> do lchar '_'; return True
2529− mergeSeq :: [PTactic] -> PTactic
2531− mergeSeq (t:ts) = TSeq t (mergeSeq ts)
2533−{- | Parses a tactic as a whole -}
2534−fullTactic :: SyntaxInfo -> IdrisParser PTactic
2535−fullTactic syn = do t <- tactic syn
2539{- * Loading and parsing -}
1121{- * Loading and parsing -}
2540{- | Parses an expression from input -}
1122{- | Parses an expression from input -}