@@ -1,5 +1,8 @@
11{-# 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
36
47import Prelude hiding (pi)
58
@@ -21,6 +24,11 @@ import Idris.Coverage
2124import Idris.IBC
2225import Idris.Unlit
2326import Idris.Providers
27+
28+import Idris.ParseHelpers
29+import Idris.ParseOps
30+import Idris.ParseExpr
31+
2432import Paths_idris
2533
2634import Util.DynamicLinker
@@ -54,295 +62,6 @@ import System.FilePath
5462 RULE{n} = rule repeated n times
5563-}
5664
57−
58−-- | Idris parser with state used during parsing
59−type IdrisParser = StateT IState IdrisInnerParser
60−
61−newtype IdrisInnerParser a = IdrisInnerParser { runInnerParser :: Parser a }
62− deriving (Monad, Functor, MonadPlus, Applicative, Alternative, CharParsing, LookAheadParsing, Parsing, DeltaParsing, MarkParsing Delta, Monoid)
63−
64−instance TokenParsing IdrisInnerParser where
65− someSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
66−
67−-- | Generalized monadic parsing constraint type
68−type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
69−
70−{- * Space, comments and literals (token/lexing like parsers) -}
71−
72−-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
73−simpleWhiteSpace :: MonadicParsing m => m ()
74−simpleWhiteSpace = satisfy isSpace *> pure ()
75−
76−-- | Checks if a charcter is end of line
77−isEol :: Char -> Bool
78−isEol '\n' = True
79−isEol _ = False
80−
81−eol :: MonadicParsing m => m ()
82−eol = (satisfy isEol *> pure ()) <|> lookAhead eof <?> "end of line"
83−
84−-- | Checks if a character is a documentation comment marker
85−isDocCommentMarker :: Char -> Bool
86−isDocCommentMarker '|' = True
87−isDocCommentMarker '^' = True
88−isDocCommentMarker _ = False
89−
90−{- | Consumes a single-line comment
91− SingleLineComment_t ::= '--' EOL_t
92− | '--' ~DocCommentMarker_t ~EOL_t* EOL_t
93− ;
94− -}
95−singleLineComment :: MonadicParsing m => m ()
96−singleLineComment = try (string "--" *> eol *> pure ())
97− <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> eol *> pure ()
98− <?> ""
99−
100−{- | Consumes a multi-line comment
101− MultiLineComment_t ::=
102− '{ -- }'
103− | '{ -' ~DocCommentMarker_t InCommentChars_t
104− ;
105−
106− InCommentChars_t ::=
107− '- }'
108− | MultiLineComment_t InCommentChars_t
109− | ~'- }'+ InCommentChars_t
110− ;
111− -}
112−
113−multiLineComment :: MonadicParsing m => m ()
114−multiLineComment = try (string "{-" *> (string "-}") *> pure ())
115− <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars
116− <?> ""
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"
125− startEnd :: String
126− startEnd = "{}-"
127−
128−{-| Parses a documentation comment (similar to haddoc) given a marker character
129− DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
130− | '{ -' DocCommentMarket_t ~'- }'* '- }'
131− ;
132− -}
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")
139− <?> ""
140−
141−-- | Parses some white space
142−whiteSpace :: MonadicParsing m => m ()
143−whiteSpace = Tok.whiteSpace
144−
145−-- | Parses a string literal
146−stringLiteral :: MonadicParsing m => m String
147−stringLiteral = Tok.stringLiteral
148−
149−-- | Parses a char literal
150−charLiteral :: MonadicParsing m => m Char
151−charLiteral = Tok.charLiteral
152−
153−-- | Parses a natural number
154−natural :: MonadicParsing m => m Integer
155−natural = Tok.natural
156−
157−-- | Parses an integral number
158−integer :: MonadicParsing m => m Integer
159−integer = Tok.integer
160−
161−-- | Parses a floating point number
162−float :: MonadicParsing m => m Double
163−float = Tok.double
164−
165−{- * Symbols, identifiers, names and operators -}
166−
167−
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",
181− "quoteGoal",
182− "Int", "Integer", "Float", "Char", "String", "Ptr",
183− "Bits8", "Bits16", "Bits32", "Bits64",
184− "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
185−
186−char :: MonadicParsing m => Char -> m Char
187−char = Chr.char
188−
189−string :: MonadicParsing m => String -> m String
190−string = Chr.string
191−
192−-- | Parses a character as a token
193−lchar :: MonadicParsing m => Char -> m Char
194−lchar = token . char
195−
196−-- | Parses string as a token
197−symbol :: MonadicParsing m => String -> m String
198−symbol = Tok.symbol
199−
200−-- | Parses a reserved identifier
201−reserved :: MonadicParsing m => String -> m ()
202−reserved = Tok.reserve idrisStyle
203−
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 $
208− do string name
209− notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
210−
211−-- | Parses an identifier as a token
212−identifier :: MonadicParsing m => m String
213−identifier = token $ Tok.ident idrisStyle
214−
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"
218−
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)]
233−
234−-- | Parses a name
235−name :: IdrisParser Name
236−name = do i <- get
237− iName (syntax_keywords i)
238− <?> "name"
239−
240−
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
243− condition.
244−-}
245−initsEndAt :: (a -> Bool) -> [a] -> [[a]]
246−initsEndAt p [] = []
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]
250−
251−
252−{- | Create a `Name' from a pair of strings representing a base name and its
253− namespace.
254−-}
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
259− (x, "") -> [x]
260− (x, '.':y) -> x : parseNS y
261−
262−operatorLetter :: MonadicParsing m => m Char
263−operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
264−
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"
269− return op
270−
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)"
276−
277−{- | Get line number from position -}
278−lineNum :: Delta -> Int
279−lineNum (Lines l _ _ _) = fromIntegral l + 1
280−lineNum (Directed _ l _ _ _) = fromIntegral l + 1
281−
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)
288−
289−{-* Syntax helpers-}
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)
294−
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
298−table fixes
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) ++
302− [[backtick],
303− [binary "=" PEq AssocLeft],
304− [binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
305−
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])
312− toBin (Fix f op)
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
317−
318−{- |Binary operator -}
319−binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
320−binary name f = Infix (do fc <- getFC
321− reservedOp name
322− doc <- option "" (docComment '^')
323− return (f fc))
324−
325−{- |Prefix operator -}
326−prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
327−prefix name f = Prefix (do reservedOp name
328− fc <- getFC
329− return (f fc))
330−
331−{- |Backtick operator -}
332−backtick :: Operator IdrisParser PTerm
333−backtick = Infix (do lchar '`'; n <- fnName
334− lchar '`'
335− fc <- getFC
336− return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
337−
338−-- | Allow implicit type declarations
339−allowImp :: SyntaxInfo -> SyntaxInfo
340−allowImp syn = syn { implicitAllowed = True }
341−
342−-- | Disallow implicit type declarations
343−disallowImp :: SyntaxInfo -> SyntaxInfo
344−disallowImp syn = syn { implicitAllowed = False }
345−
34665-- | Adds accessibility option for function
34766addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
34867addAcc n a = do i <- get
@@ -362,140 +81,6 @@ accData a n ns = do addAcc n a
36281fixErrorMsg :: String -> [String] -> String
36382fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
36483
365−{- * Layout helpers -}
366−
367−-- | Push indentation to stack
368−pushIndent :: IdrisParser ()
369−pushIndent = do pos <- position
370− ist <- get
371− put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
372−
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 })
378−
379−-- | Gets current indentation
380−indent :: IdrisParser Int
381−indent = liftM ((+1) . fromIntegral . column) position
382−
383−-- | Gets last indentation
384−lastIndent :: IdrisParser Int
385−lastIndent = do ist <- get
386− case indent_stack ist of
387− (x : xs) -> return x
388− _ -> return 1
389−
390−-- | Applies parser in an indented position
391−indented :: IdrisParser a -> IdrisParser a
392−indented p = notEndBlock *> p <* keepTerminator
393−
394−-- | Applies parser to get a block (which has possibly indented statements)
395−indentedBlock :: IdrisParser a -> IdrisParser [a]
396−indentedBlock p = do openBlock
397− pushIndent
398− res <- many (indented p)
399− popIndent
400− closeBlock
401− return res
402−
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
406− pushIndent
407− res <- some (indented p)
408− popIndent
409− closeBlock
410− return res
411−
412−-- | Applies parser to get a block with exactly one (possibly indented) statement
413−indentedBlockS :: IdrisParser a -> IdrisParser a
414−indentedBlockS p = do openBlock
415− pushIndent
416− res <- indented p
417− popIndent
418− closeBlock
419− return res
420−
421−
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
426−
427−-- | Parses a start of block
428−openBlock :: IdrisParser ()
429−openBlock = do lchar '{'
430− ist <- get
431− put (ist { brace_stack = Nothing : brace_stack ist })
432− <|> do ist <- get
433− lvl' <- indent
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
437− Just lvl_old : _ ->
438− if lvl' <= lvl_old then lvl_old+1
439− else lvl'
440− [] -> if lvl' == 1 then 2 else lvl'
441− _ -> lvl'
442− put (ist { brace_stack = Just lvl : brace_stack ist })
443− <?> "start of block"
444−
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"
455− else return xs)
456− <|> (do notOpenBraces
457− eof
458− return [])
459− put (ist { brace_stack = bs })
460−
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"
468− <|> lookAhead eof
469−
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"
477− <|> lookAhead eof
478−
479−-- | Checks if application expression does not end
480−notEndApp :: IdrisParser ()
481−notEndApp = do c <- indent; l <- lastIndent
482− when (c <= l) (fail "terminator")
483−
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")
491− _ -> return ()
492−
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
498−
49984{- * Main grammar -}
50085
50186{- | Parses module definition
@@ -757,20 +342,6 @@ fnOpts opts
757342 return (Just (fromInteger reds)))
758343 return (n, t)
759344
760−{- | Parses an operator in function position i.e. enclosed by `()', with an
761− optional namespace
762−
763− OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
764−-}
765−operatorFront :: IdrisParser Name
766−operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
767−
768−{- | Parses a function (either normal name or operator)
769− FnName ::= Name | OperatorFront;
770−-}
771−fnName :: IdrisParser Name
772−fnName = try operatorFront <|> name <?> "function name"
773−
774345{- | Parses an accessibilty modifier (e.g. public, private) -}
775346accessibility :: IdrisParser Accessibility
776347accessibility = do reserved "public"; return Public
@@ -989,695 +560,6 @@ instance_ syn = do reserved "instance"; fc <- getFC
989560 <?> "instance name"
990561
991562
992−{- | Parses an expression as a whole
993− FullExpr ::= Expr EOF_t;
994− -}
995−fullExpr :: SyntaxInfo -> IdrisParser PTerm
996−fullExpr syn = do x <- expr syn
997− eof
998− i <- get
999− return $ desugar syn i x
1000−
1001−
1002−{- |Parses an expression
1003− Expr ::= Expr';
1004−-}
1005−expr :: SyntaxInfo -> IdrisParser PTerm
1006−expr syn = do i <- get
1007− buildExpressionParser (table (idris_infixes i)) (expr' syn)
1008−
1009−{- | Parses either an internally defined expression or
1010− a user-defined one
1011−
1012−Expr' ::= "External (User-defined) Syntax"
1013− | InternalExpr;
1014−
1015− -}
1016−expr' :: SyntaxInfo -> IdrisParser PTerm
1017−expr' syn = try (externalExpr syn)
1018− <|> internalExpr syn
1019− <?> "expression"
1020−
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"
1026−
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))
1031− where
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
1037− Keyword _ -> True
1038− Symbol _ -> True
1039− _ -> False
1040− isSimple _ = False
1041−
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"
1046− where
1047− isValid :: Syntax -> Bool
1048− isValid (Rule _ _ AnySyntax) = True
1049− isValid (Rule _ _ PatternSyntax) = inPattern syn
1050− isValid (Rule _ _ TermSyntax) = not (inPattern syn)
1051−
1052−
1053−data SynMatch = SynTm PTerm | SynBind Name
1054−
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
1061− where
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
1071− return Nothing
1072− dropn :: Name -> [(Name, a)] -> [(Name, a)]
1073− dropn n [] = []
1074− dropn n ((x,t) : xs) | n == x = xs
1075− | otherwise = (x,t):dropn n xs
1076−
1077− updateB :: [(Name, SynMatch)] -> Name -> Name
1078− updateB ns n = case lookup n ns of
1079− Just (SynBind t) -> t
1080− _ -> n
1081−
1082− update :: [(Name, SynMatch)] -> PTerm -> PTerm
1083− update ns (PRef fc n) = case lookup n ns of
1084− Just (SynTm t) -> t
1085− _ -> PRef fc n
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)
1103− : upd ns ds
1104− upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
1105− : upd ns ds
1106− update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
1107− update ns t = t
1108−
1109−{- |Parses a (normal) built-in expression
1110−
1111−InternalExpr ::=
1112− App
1113− | MatchApp
1114− | UnifyLog
1115− | RecordType
1116− | SimpleExpr
1117− | Lambda
1118− | QuoteGoal
1119− | Let
1120− | RewriteTerm
1121− | Pi
1122− | DoBlock
1123− ;
1124−-}
1125−internalExpr :: SyntaxInfo -> IdrisParser PTerm
1126−internalExpr syn =
1127− try (app syn)
1128− <|> try (matchApp syn)
1129− <|> try (unifyLog syn)
1130− <|> recordType syn
1131− <|> try (simpleExpr syn)
1132− <|> lambda syn
1133− <|> quoteGoal syn
1134− <|> let_ syn
1135− <|> rewriteTerm syn
1136− <|> pi syn
1137− <|> doBlock syn
1138− <?> "expression"
1139−
1140−{- | Parses a case expression
1141−CaseExpr ::=
1142− 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
1143−-}
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"
1150−
1151−{- | Parses a case in a case expression
1152−CaseOption ::=
1153− Expr '=>' Expr Terminator
1154− ;
1155−-}
1156−caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
1157−caseOption syn = do lhs <- expr (syn { inPattern = True })
1158− symbol "=>"; r <- expr syn
1159− return (lhs, r)
1160− <?> "case option"
1161−
1162−{- | Parses a proof block
1163−ProofExpr ::=
1164− 'proof' OpenBlock Tactic'* CloseBlock
1165− ;
1166−-}
1167−proofExpr :: SyntaxInfo -> IdrisParser PTerm
1168−proofExpr syn = do reserved "proof"
1169− ts <- indentedBlock (tactic syn)
1170− return $ PProof ts
1171− <?> "proof block"
1172−
1173−{- | Parses a tactics block
1174−TacticsExpr :=
1175− 'tactics' OpenBlock Tactic'* CloseBlock
1176−;
1177−-}
1178−tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
1179−tacticsExpr syn = do reserved "tactics"
1180− ts <- indentedBlock (tactic syn)
1181− return $ PTactics ts
1182− <?> "tactics block"
1183−
1184−{- | Parses a simple expresion
1185−SimpleExpr ::=
1186− '![' Term ']'
1187− | '?' Name
1188− | % 'instance'
1189− | 'refl' ('{' Expr '}')?
1190− | ProofExpr
1191− | TacticsExpr
1192− | CaseExpr
1193− | FnName
1194− | List
1195− | Comprehension
1196− | Alt
1197− | Idiom
1198− | '(' Bracketed
1199− | Constant
1200− | Type
1201− | '_|_'
1202− | '_'
1203− | {- External (User-defined) Simple Expression -}
1204− ;
1205−-}
1206−simpleExpr :: SyntaxInfo -> IdrisParser PTerm
1207−simpleExpr syn =
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 '}';
1213− return t)
1214− return (PRefl fc tm)
1215− <|> proofExpr syn
1216− <|> tacticsExpr syn
1217− <|> caseExpr syn
1218− <|> try (do fc <- getFC
1219− x <- fnName
1220− return (PRef fc x))
1221− <|> try (listExpr syn)
1222− <|> try (comprehension syn)
1223− <|> try (alt syn)
1224− <|> try (idiom syn)
1225− <|> do lchar '('
1226− bracketed (disallowImp syn)
1227− <|> try (do c <- constant
1228− fc <- getFC
1229− return (modifyConst syn fc (PConstant c)))
1230− <|> do reserved "Type"; return PType
1231− <|> try (do symbol "_|_"
1232− fc <- getFC
1233− return (PFalse fc))
1234− <|> do lchar '_'; return Placeholder
1235− <|> simpleExternalExpr syn
1236− <?> "expression"
1237−
1238−
1239−{- |Parses the rest of an expression in braces
1240−Bracketed ::=
1241− ')'
1242− | Expr ')'
1243− | ExprList ')'
1244− | Expr '**' Expr ')'
1245− | Operator Expr ')'
1246− | Expr Operator ')'
1247− | Name ':' Expr '**' Expr ')'
1248− ;
1249−-}
1250−bracketed :: SyntaxInfo -> IdrisParser PTerm
1251−bracketed syn =
1252− do lchar ')'
1253− fc <- getFC
1254− return $ PTrue fc
1255− <|>
1256− try (do l <- expr syn
1257− lchar ')'
1258− return l)
1259− <|> do (l, fc) <- try (do
1260− l <- expr syn
1261− fc <- getFC
1262− lchar ','
1263− return (l, fc))
1264− rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')
1265− lchar ')'
1266− return $ PPair fc l (mergePairs rs)
1267− <|> do (l, fc) <- try (do
1268− l <- expr syn
1269− fc <- getFC
1270− reservedOp "**"
1271− return (l, fc))
1272− r <- expr syn
1273− lchar ')'
1274− return (PDPair fc l Placeholder r)
1275− <|> try(do fc0 <- getFC
1276− l <- simpleExpr syn
1277− o <- operator
1278− lchar ')'
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")),
1285− pexp e]))
1286− <|> try (do ln <- name; lchar ':'
1287− lty <- expr syn
1288− reservedOp "**"
1289− fc <- getFC
1290− r <- expr syn
1291− 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)
1297−
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)))]
1308− : consts)
1309− | otherwise = PAlternative False consts
1310− where
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))
1317− ]
1318−modifyConst syn fc x = x
1319−
1320−{- | Parses a list literal expression e.g. [1,2,3]
1321−ListExpr ::=
1322− '[' ExprList? ']'
1323−;
1324−
1325−ExprList ::=
1326− Expr
1327− | Expr ',' ExprList
1328− ;
1329−
1330− -}
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"
1335− where
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)]
1339−
1340−
1341−{- | Parses an alternative expression
1342− Alt ::= '(|' Expr_List '|)';
1343−
1344− Expr_List ::=
1345− Expr'
1346− | Expr' ',' Expr_List
1347− ;
1348−-}
1349−alt :: SyntaxInfo -> IdrisParser PTerm
1350−alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
1351− return (PAlternative False alts)
1352−
1353−{- | Parses a possibly hidden simple expression
1354−HSimpleExpr ::=
1355− '.' SimpleExpr
1356− | SimpleExpr
1357− ;
1358−-}
1359−hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
1360−hsimpleExpr syn =
1361− do lchar '.'
1362− e <- simpleExpr syn
1363− return $ PHidden e
1364− <|> simpleExpr syn
1365− <?> "expression"
1366−
1367−{- | Parses a matching application expression
1368−MatchApp ::=
1369− SimpleExpr '<==' FnName
1370− ;
1371−-}
1372−matchApp :: SyntaxInfo -> IdrisParser PTerm
1373−matchApp syn = do ty <- simpleExpr syn
1374− symbol "<=="
1375− fc <- getFC
1376− f <- fnName
1377− return (PLet (MN 0 "match")
1378− ty
1379− (PMatchApp fc f)
1380− (PRef fc (MN 0 "match")))
1381− <?> "matching application expression"
1382−
1383−{- | Parses a unification log expression
1384−UnifyLog ::=
1385− '%' 'unifyLog' SimpleExpr
1386− ;
1387−-}
1388−unifyLog :: SyntaxInfo -> IdrisParser PTerm
1389−unifyLog syn = do lchar '%'; reserved "unifyLog";
1390− tm <- simpleExpr syn
1391− return (PUnifyLog tm)
1392− <?> "unification log expression"
1393−
1394−{- | Parses a function application expression
1395−App ::=
1396− 'mkForeign' Arg Arg*
1397− | SimpleExpr Arg+
1398− ;
1399−-}
1400−app :: SyntaxInfo -> IdrisParser PTerm
1401−app syn = do f <- reserved "mkForeign"
1402− fc <- getFC
1403− fn <- arg syn
1404− args <- many (do notEndApp; arg syn)
1405− i <- get
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")
1410− Placeholder
1411− (PApp fc (PRef fc (UN "mkForeignPrim"))
1412− (fn : args ++
1413− [pexp (PRef fc (MN 0 "w"))])))]
1414− return (dslify i ap)
1415−
1416− <|> do f <- simpleExpr syn
1417− fc <- getFC
1418− args <- some (do notEndApp; arg syn)
1419− i <- get
1420− return (dslify i $ PApp fc f args)
1421− <?> "function application"
1422− where
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)
1427− dslify i t = t
1428−
1429−{- |Parses a function argument
1430−Arg ::=
1431− ImplicitArg
1432− | ConstraintArg
1433− | SimpleExpr
1434− ;
1435−-}
1436−arg :: SyntaxInfo -> IdrisParser PArg
1437−arg syn = implicitArg syn
1438− <|> constraintArg syn
1439− <|> do e <- simpleExpr syn
1440− return (pexp e)
1441− <?> "function argument"
1442−
1443−{- |Parses an implicit function argument
1444−ImplicitArg ::=
1445− '{' Name ('=' Expr)? '}'
1446− ;
1447−-}
1448−implicitArg :: SyntaxInfo -> IdrisParser PArg
1449−implicitArg syn = do lchar '{'
1450− n <- name
1451− fc <- getFC
1452− v <- option (PRef fc n) (do lchar '='
1453− expr syn)
1454− lchar '}'
1455− return (pimp n v)
1456− <?> "implicit function argument"
1457−
1458−{- |Parses a constraint argument (for selecting a named type class instance)
1459−ConstraintArg ::=
1460− '@{' Expr '}'
1461− ;
1462−-}
1463−constraintArg :: SyntaxInfo -> IdrisParser PArg
1464−constraintArg syn = do symbol "@{"
1465− e <- expr syn
1466− symbol "}"
1467− return (pconst e)
1468− <?> "constraint argument"
1469−
1470−
1471−{- |Parses a record field setter expression
1472−RecordType ::=
1473− 'record' '{' FieldTypeList '}';
1474−
1475−FieldTypeList ::=
1476− FieldType
1477− | FieldType ',' FieldTypeList
1478− ;
1479−
1480−FieldType ::=
1481− FnName '=' Expr
1482− ;
1483−-}
1484−recordType :: SyntaxInfo -> IdrisParser PTerm
1485−recordType syn
1486− = do reserved "record"
1487− lchar '{'
1488− fields <- sepBy1 fieldType (lchar ',')
1489− lchar '}'
1490− fc <- getFC
1491− rec <- optional (simpleExpr syn)
1492− case rec of
1493− Nothing ->
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
1500− lchar '='
1501− e <- expr syn
1502− return (n, e)
1503− <?> "field setter"
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])
1508−
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
1514−
1515−{- |Parses a type signature
1516−TypeSig ::=
1517− ':' Expr
1518− ;
1519−TypeExpr ::= ConstraintList? Expr;
1520− -}
1521−typeExpr :: SyntaxInfo -> IdrisParser PTerm
1522−typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
1523− sc <- expr syn
1524− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
1525− <?> "type signature"
1526−
1527−{- |Parses a lambda expression
1528−Lambda ::=
1529− '\\' TypeOptDeclList '=>' Expr
1530− | '\\' SimpleExprList '=>' Expr
1531− ;
1532−SimpleExprList ::=
1533− SimpleExpr
1534− | SimpleExpr ',' SimpleExprList
1535− ;
1536−-}
1537−lambda :: SyntaxInfo -> IdrisParser PTerm
1538−lambda syn = do lchar '\\'
1539− try (do xt <- tyOptDeclList syn
1540− symbol "=>"
1541− sc <- expr syn
1542− return (bindList PLam xt sc)
1543− <|> (do ps <- sepBy (do fc <- getFC
1544− e <- simpleExpr syn
1545− return (fc, e)) (lchar ',')
1546− symbol "=>"
1547− sc <- expr syn
1548− return (pmList (zip [0..] ps) sc)))
1549− <?> "lambda expression"
1550− where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
1551− pmList [] sc = sc
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)])
1556−
1557−{- |Parses a term rewrite expression
1558−RewriteTerm ::=
1559− 'rewrite' Expr ('==>' Expr)? 'in' Expr
1560− ;
1561−-}
1562−rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
1563−rewriteTerm syn = do reserved "rewrite"
1564− fc <- getFC
1565− prf <- expr syn
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
1570− giving)
1571− <?> "term rewrite expression"
1572−
1573−{- |Parses a let binding
1574−Let ::=
1575− 'let' Name TypeSig'? '=' Expr 'in' Expr
1576−| 'let' Expr' '=' Expr' 'in' Expr
1577−
1578−TypeSig' ::=
1579− ':' Expr'
1580− ;
1581− -}
1582−let_ :: SyntaxInfo -> IdrisParser PTerm
1583−let_ syn = try (do reserved "let"; n <- name;
1584− ty <- option Placeholder (do lchar ':'; expr' syn)
1585− lchar '='
1586− v <- 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)]))
1593− <?> "let binding"
1594−
1595−{- |Parses a quote goal
1596−QuoteGoal ::=
1597− 'quoteGoal' Name 'by' Expr 'in' Expr
1598− ;
1599− -}
1600−quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1601−quoteGoal syn = do reserved "quoteGoal"; n <- name;
1602− reserved "by"
1603− r <- expr syn
1604− reserved "in"
1605− fc <- getFC
1606− sc <- expr syn
1607− return (PGoal fc r n sc)
1608− <?> "quote goal expression"
1609−
1610−{- |Parses a dependent type signature
1611−Pi ::=
1612− '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
1613− | '|'? Static? '{' TypeDeclList '}' '->' Expr
1614− | '{' 'auto' TypeDeclList '}' '->' Expr
1615− | '{' 'default' TypeDeclList '}' '->' Expr
1616− | '{' 'static' '}' Expr' '->' Expr
1617− ;
1618− -}
1619−
1620−pi :: SyntaxInfo -> IdrisParser PTerm
1621−pi syn =
1622− do lazy <- if implicitAllowed syn -- laziness is top level only
1623− then option False (do lchar '|'; return True)
1624− else return False
1625− st <- static
1626− (do try(lchar '('); xt <- typeDeclList syn; lchar ')'
1627− doc <- option "" (docComment '^')
1628− symbol "->"
1629− sc <- expr syn
1630− return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do
1631− lchar '{'
1632− (do reserved "auto"
1633− when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"
1634− xt <- typeDeclList syn
1635− lchar '}'
1636− symbol "->"
1637− sc <- expr syn
1638− return (bindList (PPi
1639− (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc)) <|> (do
1640− reserved "default"
1641− when (lazy || (st == Static)) $ fail "default tactic constraints can not be lazy or static"
1642− script <- simpleExpr syn
1643− xt <- typeDeclList syn
1644− lchar '}'
1645− symbol "->"
1646− sc <- expr syn
1647− return (bindList (PPi (TacImp False Dynamic script "")) xt sc)) <|> (do
1648− reserved "static"
1649− lchar '}'
1650− t <- expr' syn
1651− symbol "->"
1652− sc <- expr syn
1653− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)) <|> (
1654− if implicitAllowed syn then do
1655− xt <- typeDeclList syn
1656− lchar '}'
1657− symbol "->"
1658− sc <- expr syn
1659− return (bindList (PPi (Imp lazy st "")) xt sc)
1660− else do fail "no implicit arguments allowed here"))
1661− <?> "dependent type signature"
1662−
1663−{- | Parses a type constraint list
1664−ConstraintList ::=
1665− '(' Expr_List ')' '=>'
1666− | Expr '=>'
1667− ;
1668−-}
1669−constraintList :: SyntaxInfo -> IdrisParser [PTerm]
1670−constraintList syn = try (do lchar '('
1671− tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')
1672− lchar ')'
1673− reservedOp "=>"
1674− return tys)
1675− <|> try (do t <- expr (disallowImp syn)
1676− reservedOp "=>"
1677− return [t])
1678− <|> return []
1679− <?> "type constraint list"
1680−
1681563{- | Parses a using declaration list
1682564UsingDeclList ::=
1683565 UsingDeclList'
@@ -1719,194 +601,6 @@ usingDecl syn = try (do x <- fnName
1719601 return (UConstraint c xs)
1720602 <?> "using declaration"
1721603
1722−{- |Parses a type declaration list
1723−TypeDeclList ::=
1724− FunctionSignatureList
1725− | NameList TypeSig
1726− ;
1727−
1728−FunctionSignatureList ::=
1729− Name TypeSig
1730− | Name TypeSig ',' FunctionSignatureList
1731− ;
1732−-}
1733−typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1734−typeDeclList syn = try (sepBy1 (do x <- fnName
1735− lchar ':'
1736− t <- typeExpr (disallowImp syn)
1737− return (x,t))
1738− (lchar ','))
1739− <|> do ns <- sepBy1 name (lchar ',')
1740− lchar ':'
1741− t <- typeExpr (disallowImp syn)
1742− return (map (\x -> (x, t)) ns)
1743− <?> "type declaration list"
1744−
1745−{- |Parses a type declaration list with optional parameters
1746−TypeOptDeclList ::=
1747− NameOrPlaceholder TypeSig?
1748− | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1749− ;
1750−
1751−NameOrPlaceHolder ::= Name | '_';
1752−-}
1753−tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1754−tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
1755− t <- option Placeholder (do lchar ':'
1756− expr syn)
1757− return (x,t))
1758− (lchar ',')
1759− <?> "type declaration list"
1760− where nameOrPlaceholder :: IdrisParser Name
1761− nameOrPlaceholder = fnName
1762− <|> do symbol "_"
1763− return (MN 0 "underscore")
1764− <?> "name or placeholder"
1765−
1766−{- |Parses a list comprehension
1767−Comprehension ::= '[' Expr '|' DoList ']';
1768−
1769−DoList ::=
1770− Do
1771− | Do ',' DoList
1772− ;
1773−-}
1774−comprehension :: SyntaxInfo -> IdrisParser PTerm
1775−comprehension syn
1776− = do lchar '['
1777− fc <- getFC
1778− pat <- expr syn
1779− lchar '|'
1780− qs <- sepBy1 (do_ syn) (lchar ',')
1781− lchar ']'
1782− return (PDoBlock (map addGuard qs ++
1783− [DoExp fc (PApp fc (PRef fc (UN "return"))
1784− [pexp pat])]))
1785− <?> "list comprehension"
1786− where addGuard :: PDo -> PDo
1787− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
1788− [pexp e])
1789− addGuard x = x
1790−
1791−{- |Parses a do-block
1792−Do' ::= Do KeepTerminator;
1793−
1794−DoBlock ::=
1795− 'do' OpenBlock Do'+ CloseBlock
1796− ;
1797− -}
1798−doBlock :: SyntaxInfo -> IdrisParser PTerm
1799−doBlock syn
1800− = do reserved "do"
1801− ds <- indentedBlock (do_ syn)
1802− return (PDoBlock ds)
1803− <?> "do block"
1804−
1805−{- |Parses an expression inside a do block
1806−Do ::=
1807− 'let' Name TypeSig'? '=' Expr
1808− | 'let' Expr' '=' Expr
1809− | Name '<-' Expr
1810− | Expr' '<-' Expr
1811− | Expr
1812− ;
1813−-}
1814−do_ :: SyntaxInfo -> IdrisParser PDo
1815−do_ syn
1816− = try (do reserved "let"
1817− i <- name
1818− ty <- option Placeholder (do lchar ':'
1819− expr' syn)
1820− reservedOp "="
1821− fc <- getFC
1822− e <- expr syn
1823− return (DoLet fc i ty e))
1824− <|> try (do reserved "let"
1825− i <- expr' syn
1826− reservedOp "="
1827− fc <- getFC
1828− sc <- expr syn
1829− return (DoLetP fc i sc))
1830− <|> try (do i <- name
1831− symbol "<-"
1832− fc <- getFC
1833− e <- expr syn;
1834− return (DoBind fc i e))
1835− <|> try (do i <- expr' syn
1836− symbol "<-"
1837− fc <- getFC
1838− e <- expr syn;
1839− return (DoBindP fc i e))
1840− <|> do e <- expr syn
1841− fc <- getFC
1842− return (DoExp fc e)
1843− <?> "do block expression"
1844−
1845−{- |Parses an expression in idiom brackets
1846−Idiom ::= '[|' Expr '|]';
1847−-}
1848−idiom :: SyntaxInfo -> IdrisParser PTerm
1849−idiom syn
1850− = do symbol "[|"
1851− fc <- getFC
1852− e <- expr syn
1853− symbol "|]"
1854− return (PIdiom fc e)
1855− <?> "expression in idiom brackets"
1856−
1857−{- |Parses a constant or literal expression
1858−Constant ::=
1859− 'Integer'
1860− | 'Int'
1861− | 'Char'
1862− | 'Float'
1863− | 'String'
1864− | 'Ptr'
1865− | 'Bits8'
1866− | 'Bits16'
1867− | 'Bits32'
1868− | 'Bits64'
1869− | 'Bits8x16'
1870− | 'Bits16x8'
1871− | 'Bits32x4'
1872− | 'Bits64x2'
1873− | Float_t
1874− | Natural_t
1875− | String_t
1876− | Char_t
1877− ;
1878−-}
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"
1899−
1900−{- |Parses a static modifier
1901−Static ::=
1902− '[' static ']'
1903−;
1904−-}
1905−static :: IdrisParser Static
1906−static = do lchar '['; reserved "static"; lchar ']'; return Static
1907− <|> return Dynamic
1908− <?> "static modifier"
1909−
1910604{- |Parses a record type declaration
1911605Record ::=
1912606 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
@@ -2423,118 +1117,6 @@ transform syn = do try (lchar '%' *> reserved "transform")
24231117 return [PTransform fc False l r]
24241118 <?> "transform"
24251119
2426−{- | Parses a tactic script
2427−Tactic ::= 'intro' NameList?
2428− | 'intros'
2429− | 'refine' Name Imp+
2430− | 'mrefine' Name
2431− | 'rewrite' Expr
2432− | 'equiv' Expr
2433− | 'let' Name ':' Expr' '=' Expr
2434− | 'let' Name '=' Expr
2435− | 'focus' Name
2436− | 'exact' Expr
2437− | 'applyTactic' Expr
2438− | 'reflect' Expr
2439− | 'fill' Expr
2440− | 'try' Tactic '|' Tactic
2441− | '{' TacticSeq '}'
2442− | 'compute'
2443− | 'trivial'
2444− | 'solve'
2445− | 'attack'
2446− | 'state'
2447− | 'term'
2448− | 'undo'
2449− | 'qed'
2450− | 'abandon'
2451− | ':' 'q'
2452− ;
2453−
2454−Imp ::= '?' | '_';
2455−
2456−TacticSeq ::=
2457− Tactic ';' Tactic
2458− | Tactic ';' TacticSeq
2459− ;
2460−
2461−-}
2462−
2463−tactic :: SyntaxInfo -> IdrisParser PTactic
2464−tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
2465− return $ Intro ns
2466− <|> do reserved "intros"; return Intros
2467− <|> try (do reserved "refine"; n <- name
2468− imps <- some imp
2469− return $ Refine n imps)
2470− <|> do reserved "refine"; n <- name
2471− i <- get
2472− return $ Refine n []
2473− <|> do reserved "mrefine"; n <- name
2474− i <- get
2475− return $ MatchRefine n
2476− <|> do reserved "rewrite"; t <- expr syn;
2477− i <- get
2478− return $ Rewrite (desugar syn i t)
2479− <|> do reserved "equiv"; t <- expr syn;
2480− i <- get
2481− return $ Equiv (desugar syn i t)
2482− <|> try (do reserved "let"; n <- name; lchar ':';
2483− ty <- expr' syn; lchar '='; t <- expr syn;
2484− i <- get
2485− return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
2486− <|> try (do reserved "let"; n <- name; lchar '=';
2487− t <- expr syn;
2488− i <- get
2489− return $ LetTac n (desugar syn i t))
2490− <|> do reserved "focus"; n <- name
2491− return $ Focus n
2492− <|> do reserved "exact"; t <- expr syn;
2493− i <- get
2494− return $ Exact (desugar syn i t)
2495− <|> do reserved "applyTactic"; t <- expr syn;
2496− i <- get
2497− return $ ApplyTactic (desugar syn i t)
2498− <|> do reserved "reflect"; t <- expr syn;
2499− i <- get
2500− return $ Reflect (desugar syn i t)
2501− <|> do reserved "fill"; t <- expr syn;
2502− i <- get
2503− return $ Fill (desugar syn i t)
2504− <|> do reserved "try"; t <- tactic syn;
2505− lchar '|';
2506− t1 <- tactic syn
2507− return $ Try t t1
2508− <|> do lchar '{'
2509− t <- tactic syn;
2510− lchar ';';
2511− ts <- sepBy1 (tactic syn) (lchar ';')
2512− 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
2524− <?> "tactic"
2525− where
2526− imp :: IdrisParser Bool
2527− imp = do lchar '?'; return False
2528− <|> do lchar '_'; return True
2529− mergeSeq :: [PTactic] -> PTactic
2530− mergeSeq [t] = t
2531− mergeSeq (t:ts) = TSeq t (mergeSeq ts)
2532−
2533−{- | Parses a tactic as a whole -}
2534−fullTactic :: SyntaxInfo -> IdrisParser PTactic
2535−fullTactic syn = do t <- tactic syn
2536− eof
2537− return t
25381120
25391121{- * Loading and parsing -}
25401122{- | Parses an expression from input -}