git.iko.soy/Idris-dev
on fd6898e help sign in
Idris-dev/src/Idris/Parser/Expr.hs
1584 lines 54 kB history raw
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, TupleSections #-}
2module Idris.Parser.Expr where
4import Prelude hiding (pi)
6import Text.Trifecta.Delta
7import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)
8import Text.Parser.LookAhead
9import Text.Parser.Expression
10import qualified Text.Parser.Token as Tok
11import qualified Text.Parser.Char as Chr
12import qualified Text.Parser.Token.Highlight as Hi
14import Idris.AbsSyntax
15import Idris.Parser.Helpers
16import Idris.Parser.Ops
17import Idris.DSL
19import Idris.Core.TT
21import Control.Applicative
22import Control.Monad
23import Control.Monad.State.Strict
25import Data.Function (on)
26import Data.Maybe
27import qualified Data.List.Split as Spl
28import Data.List
29import Data.Monoid
30import Data.Char
31import qualified Data.HashSet as HS
32import qualified Data.Text as T
33import qualified Data.ByteString.UTF8 as UTF8
35import Debug.Trace
37-- | Allow implicit type declarations
38allowImp :: SyntaxInfo -> SyntaxInfo
39allowImp syn = syn { implicitAllowed = True }
41-- | Disallow implicit type declarations
42disallowImp :: SyntaxInfo -> SyntaxInfo
43disallowImp syn = syn { implicitAllowed = False }
45{-| Parses an expression as a whole
47 FullExpr ::= Expr EOF_t;
49 -}
50fullExpr :: SyntaxInfo -> IdrisParser PTerm
51fullExpr syn = do x <- expr syn
52 eof
53 i <- get
54 return $ debindApp syn (desugar syn i x)
56tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
57tryFullExpr syn st input =
58 case runparser (fullExpr syn) st "" input of
59 Success tm -> Right tm
60 Failure e -> Left (Msg (show e))
62{- | Parses an expression
64 Expr ::= Pi
66 -}
67expr :: SyntaxInfo -> IdrisParser PTerm
68expr = pi
70{- | Parses an expression with possible operator applied
72 OpExpr ::= {- Expression Parser with Operators based on Expr' -};
74-}
75opExpr :: SyntaxInfo -> IdrisParser PTerm
76opExpr syn = do i <- get
77 buildExpressionParser (table (idris_infixes i)) (expr' syn)
79{- | Parses either an internally defined expression or
80 a user-defined one
82Expr' ::= "External (User-defined) Syntax"
83 | InternalExpr;
85 -}
86expr' :: SyntaxInfo -> IdrisParser PTerm
87expr' syn = try (externalExpr syn)
88 <|> internalExpr syn
89 <?> "expression"
91{- | Parses a user-defined expression -}
92externalExpr :: SyntaxInfo -> IdrisParser PTerm
93externalExpr syn = do i <- get
94 (FC fn start _) <- getFC
95 expr <- extensions syn (syntaxRulesList $ syntax_rules i)
96 (FC _ _ end) <- getFC
97 let outerFC = FC fn start end
98 return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)
99 <?> "user-defined expression"
100 where -- Fix non-highlighting FCs by approximating with the span of the syntax application
101 fixFC outer inner | inner `fcIn` outer = inner
102 | otherwise = outer
103 -- Fix highlighting FCs by making them useless, to avoid spurious highlights
104 fixFCH fn outer inner | inner `fcIn` outer = inner
105 | otherwise = FileFC fn
107{- | Parses a simple user-defined expression -}
108simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
109simpleExternalExpr syn = do i <- get
110 extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))
111 where
112 isSimple (Rule (Expr x:xs) _ _) = False
113 isSimple (Rule (SimpleExpr x:xs) _ _) = False
114 isSimple (Rule [Keyword _] _ _) = True
115 isSimple (Rule [Symbol _] _ _) = True
116 isSimple (Rule (_:xs) _ _) = case last xs of
117 Keyword _ -> True
118 Symbol _ -> True
119 _ -> False
120 isSimple _ = False
122{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
123extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
124extensions syn rules = extension syn [] (filter isValid rules)
125 <?> "user-defined expression"
126 where
127 isValid :: Syntax -> Bool
128 isValid (Rule _ _ AnySyntax) = True
129 isValid (Rule _ _ PatternSyntax) = inPattern syn
130 isValid (Rule _ _ TermSyntax) = not (inPattern syn)
131 isValid (DeclRule _ _) = False
133data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information
134 deriving Show
136extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
137extension syn ns rules =
138 choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
139 case head rs of -- can never be []
140 Rule (symb:_) _ _ -> try $ do
141 n <- extensionSymbol symb
142 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]
143 -- If we have more than one Rule in this bucket, our grammar is
144 -- nondeterministic.
145 Rule [] ptm _ -> return (flatten (updateSynMatch (mapMaybe id ns) ptm))
146 where
147 ruleGroup [] [] = True
148 ruleGroup (s1:_) (s2:_) = s1 == s2
149 ruleGroup _ _ = False
151 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
152 extensionSymbol (Keyword n) = do fc <- reservedFC (show n)
153 highlightP fc AnnKeyword
154 return Nothing
155 extensionSymbol (Expr n) = do tm <- expr syn
156 return $ Just (n, SynTm tm)
157 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
158 return $ Just (n, SynTm tm)
159 extensionSymbol (Binding n) = do (b, fc) <- name
160 return $ Just (n, SynBind fc b)
161 extensionSymbol (Symbol s) = do fc <- symbolFC s
162 highlightP fc AnnKeyword
163 return Nothing
165 flatten :: PTerm -> PTerm -- flatten application
166 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
167 flatten t = t
169updateSynMatch = update
170 where
171 updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
172 updateB ns (n, fc) = case lookup n ns of
173 Just (SynBind tfc t) -> (t, tfc)
174 _ -> (n, fc)
176 update :: [(Name, SynMatch)] -> PTerm -> PTerm
177 update ns (PRef fc hls n) = case lookup n ns of
178 Just (SynTm t) -> t
179 _ -> PRef fc hls n
180 update ns (PPatvar fc n) = uncurry (flip PPatvar) $ updateB ns (n, fc)
181 update ns (PLam fc n nfc ty sc)
182 = let (n', nfc') = updateB ns (n, nfc)
183 in PLam fc n' nfc' (update ns ty) (update (dropn n ns) sc)
184 update ns (PPi p n fc ty sc)
185 = let (n', nfc') = updateB ns (n, fc)
186 in PPi (updTacImp ns p) n' nfc'
187 (update ns ty) (update (dropn n ns) sc)
188 update ns (PLet fc n nfc ty val sc)
189 = let (n', nfc') = updateB ns (n, nfc)
190 in PLet fc n' nfc' (update ns ty)
191 (update ns val) (update (dropn n ns) sc)
192 update ns (PApp fc t args)
193 = PApp fc (update ns t) (map (fmap (update ns)) args)
194 update ns (PAppBind fc t args)
195 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
196 update ns (PMatchApp fc n) = let (n', nfc') = updateB ns (n, fc)
197 in PMatchApp nfc' n'
198 update ns (PIfThenElse fc c t f)
199 = PIfThenElse fc (update ns c) (update ns t) (update ns f)
200 update ns (PCase fc c opts)
201 = PCase fc (update ns c) (map (pmap (update ns)) opts)
202 update ns (PRewrite fc eq tm mty)
203 = PRewrite fc (update ns eq) (update ns tm) (fmap (update ns) mty)
204 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
205 update ns (PDPair fc hls p l t r)
206 = PDPair fc hls p (update ns l) (update ns t) (update ns r)
207 update ns (PAs fc n t) = PAs fc (fst $ updateB ns (n, NoFC)) (update ns t)
208 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
209 update ns (PHidden t) = PHidden (update ns t)
210 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
211 update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds
212 where upd :: [(Name, SynMatch)] -> PDo -> PDo
213 upd ns (DoExp fc t) = DoExp fc (update ns t)
214 upd ns (DoBind fc n nfc t) = DoBind fc n nfc (update ns t)
215 upd ns (DoLet fc n nfc ty t) = DoLet fc n nfc (update ns ty) (update ns t)
216 upd ns (DoBindP fc i t ts)
217 = DoBindP fc (update ns i) (update ns t)
218 (map (\(l,r) -> (update ns l, update ns r)) ts)
219 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
220 update ns (PIdiom fc t) = PIdiom fc $ update ns t
221 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
222 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
223 update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs
224 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
225 update ns (PUnifyLog t) = PUnifyLog $ update ns t
226 update ns (PNoImplicits t) = PNoImplicits $ update ns t
227 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)
228 update ns (PUnquote t) = PUnquote $ update ns t
229 update ns (PQuoteName n res fc) = let (n', fc') = (updateB ns (n, fc))
230 in PQuoteName n' res fc'
231 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp
232 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t
233 -- PConstSugar probably can't contain anything substitutable, but it's hard to track
234 update ns t = t
236 updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
237 -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
238 updTactic ns (Intro ns') = Intro $ map (fst . updateB ns . (, NoFC)) ns'
239 updTactic ns (Focus n) = Focus . fst $ updateB ns (n, NoFC)
240 updTactic ns (Refine n bs) = Refine (fst $ updateB ns (n, NoFC)) bs
241 updTactic ns (Claim n t) = Claim (fst $ updateB ns (n, NoFC)) (update ns t)
242 updTactic ns (MatchRefine n) = MatchRefine (fst $ updateB ns (n, NoFC))
243 updTactic ns (LetTac n t) = LetTac (fst $ updateB ns (n, NoFC)) (update ns t)
244 updTactic ns (LetTacTy n ty tm) = LetTacTy (fst $ updateB ns (n, NoFC)) (update ns ty) (update ns tm)
245 updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth
246 (fmap (fst . updateB ns . (, NoFC)) top) (map (fst . updateB ns . (, NoFC)) psns) (map (fst . updateB ns . (, NoFC)) hints)
247 updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)
248 updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)
249 updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac
250 updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)
251 updTactic ns t = fmap (update ns) t
253 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
254 updTacImp _ x = x
256 dropn :: Name -> [(Name, a)] -> [(Name, a)]
257 dropn n [] = []
258 dropn n ((x,t) : xs) | n == x = xs
259 | otherwise = (x,t):dropn n xs
262{- | Parses a (normal) built-in expression
264InternalExpr ::=
265 UnifyLog
266 | RecordType
267 | SimpleExpr
268 | Lambda
269 | QuoteGoal
270 | Let
271 | If
272 | RewriteTerm
273 | CaseExpr
274 | DoBlock
275 | App
276 ;
278-}
279internalExpr :: SyntaxInfo -> IdrisParser PTerm
280internalExpr syn =
281 unifyLog syn
282 <|> runElab syn
283 <|> disamb syn
284 <|> noImplicits syn
285 <|> recordType syn
286 <|> if_ syn
287 <|> lambda syn
288 <|> quoteGoal syn
289 <|> let_ syn
290 <|> rewriteTerm syn
291 <|> doBlock syn
292 <|> caseExpr syn
293 <|> app syn
294 <?> "expression"
296{- | Parses the "impossible" keyword
298Impossible ::= 'impossible'
300-}
301impossible :: IdrisParser PTerm
302impossible = do fc <- reservedFC "impossible"
303 highlightP fc AnnKeyword
304 return PImpossible
306{- | Parses a case expression
308CaseExpr ::=
309 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
311-}
312caseExpr :: SyntaxInfo -> IdrisParser PTerm
313caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC
314 scr <- expr syn; kw2 <- reservedFC "of";
315 opts <- indentedBlock1 (caseOption syn)
316 highlightP kw1 AnnKeyword
317 highlightP kw2 AnnKeyword
318 return (PCase fc scr opts)
319 <?> "case expression"
321{- | Parses a case in a case expression
323CaseOption ::=
324 Expr (Impossible | '=>' Expr) Terminator
325 ;
327-}
328caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
329caseOption syn = do lhs <- expr (syn { inPattern = True })
330 r <- impossible <|> symbol "=>" *> expr syn
331 return (lhs, r)
332 <?> "case option"
334warnTacticDeprecation :: FC -> IdrisParser ()
335warnTacticDeprecation fc =
336 parserWarning fc (Just NoOldTacticDeprecationWarnings) (Msg "This style of tactic proof is deprecated. See %runElab for the replacement.")
338{- | Parses a proof block
340ProofExpr ::=
341 'proof' OpenBlock Tactic'* CloseBlock
342 ;
344-}
345proofExpr :: SyntaxInfo -> IdrisParser PTerm
346proofExpr syn = do kw <- reservedFC "proof"
347 ts <- indentedBlock1 (tactic syn)
348 highlightP kw AnnKeyword
349 warnTacticDeprecation kw
350 return $ PProof ts
351 <?> "proof block"
353{- | Parses a tactics block
355TacticsExpr :=
356 'tactics' OpenBlock Tactic'* CloseBlock
359-}
360tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
361tacticsExpr syn = do kw <- reservedFC "tactics"
362 ts <- indentedBlock1 (tactic syn)
363 highlightP kw AnnKeyword
364 warnTacticDeprecation kw
365 return $ PTactics ts
366 <?> "tactics block"
368{- | Parses a simple expression
370SimpleExpr ::=
371 {- External (User-defined) Simple Expression -}
372 | '?' Name
373 | % 'instance'
374 | 'Refl' ('{' Expr '}')?
375 | ProofExpr
376 | TacticsExpr
377 | FnName
378 | Idiom
379 | List
380 | Alt
381 | Bracketed
382 | Constant
383 | Type
384 | 'Void'
385 | Quasiquote
386 | NameQuote
387 | Unquote
388 | '_'
389 ;
391-}
392simpleExpr :: SyntaxInfo -> IdrisParser PTerm
393simpleExpr syn =
394 try (simpleExternalExpr syn)
395 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)
396 return (PMetavar (FC f (l, c-1) end) x)
397 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
398 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
399 <|> proofExpr syn
400 <|> tacticsExpr syn
401 <|> try (do reserved "Type*"; return $ PUniverse AllTypes)
402 <|> do reserved "AnyType"; return $ PUniverse AllTypes
403 <|> PType <$> reservedFC "Type"
404 <|> do reserved "UniqueType"; return $ PUniverse UniqueType
405 <|> do reserved "NullType"; return $ PUniverse NullType
406 <|> do (c, cfc) <- constant
407 fc <- getFC
408 return (modifyConst syn fc (PConstant cfc c))
409 <|> do symbol "'"; fc <- getFC; str <- fst <$> name
410 return (PApp fc (PRef fc [] (sUN "Symbol_"))
411 [pexp (PConstant NoFC (Str (show str)))])
412 <|> do (x, fc) <- fnName
413 if inPattern syn
414 then option (PRef fc [fc] x)
415 (do reservedOp "@"
416 s <- simpleExpr syn
417 fcIn <- getFC
418 return (PAs fcIn x s))
419 else return (PRef fc [fc] x)
420 <|> idiom syn
421 <|> listExpr syn
422 <|> alt syn
423 <|> do reservedOp "!"
424 s <- simpleExpr syn
425 fc <- getFC
426 return (PAppBind fc s [])
427 <|> bracketed (disallowImp syn)
428 <|> quasiquote syn
429 <|> namequote syn
430 <|> unquote syn
431 <|> do lchar '_'; return Placeholder
432 <?> "expression"
434{- |Parses an expression in braces
436Bracketed ::= '(' Bracketed'
438 -}
439bracketed :: SyntaxInfo -> IdrisParser PTerm
440bracketed syn = do (FC fn (sl, sc) _) <- getFC
441 lchar '(' <?> "parenthesized expression"
442 bracketed' (FC fn (sl, sc) (sl, sc+1)) syn
444{- |Parses the rest of an expression in braces
446Bracketed' ::=
447 ')'
448 | Expr ')'
449 | ExprList ')'
450 | DependentPair ')'
451 | Operator Expr ')'
452 | Expr Operator ')'
453 ;
455-}
456bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm
457bracketed' open syn =
458 do (FC f start (l, c)) <- getFC
459 lchar ')'
460 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
461 <|> try (dependentPair TypeOrTerm [] open syn)
462 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
463 -- No prefix operators! (bit of a hack here...)
464 if (o == "-" || o == "!")
465 then fail "minus not allowed in section"
466 else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
467 (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),
468 pexp e]))
469 <|> try (do l <- simpleExpr syn
470 op <- option Nothing (do o <- operator
471 lchar ')'
472 return (Just o))
473 fc0 <- getFC
474 case op of
475 Nothing -> bracketedExpr syn open l
476 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder
477 (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,
478 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
479 <|> do l <- expr syn
480 bracketedExpr syn open l
484{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
485dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
486dependentPair pun prev openFC syn =
487 if prev == [] then
488 nametypePart <|> namePart
489 else
490 case pun of
491 IsType -> nametypePart <|> namePart <|> exprPart True
492 IsTerm -> exprPart False
493 TypeOrTerm -> nametypePart <|> namePart <|> exprPart False
494 where nametypePart = do
495 (ln, lnfc, colonFC) <- try $ do
496 (ln, lnfc) <- name
497 colonFC <- lcharFC ':'
498 return (ln, lnfc, colonFC)
499 lty <- expr' syn
500 starsFC <- reservedOpFC "**"
501 dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn
502 namePart = try $ do
503 (ln, lnfc) <- name
504 starsFC <- reservedOpFC "**"
505 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
506 exprPart isEnd = do
507 e <- expr syn
508 sepFCE <-
509 let stars = (Left <$> reservedOpFC "**")
510 ending = (Right <$> lcharFC ')')
511 in if isEnd then ending else stars <|> ending
512 case sepFCE of
513 Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
514 Right closeFC ->
515 return (mkPDPairs pun openFC closeFC (reverse prev) e)
516 mkPDPairs pun openFC closeFC ((e, cfclty, starsFC):bnds) r =
517 (PDPair openFC ([openFC] ++ maybe [] ((: []) . fst) cfclty ++ [starsFC, closeFC] ++ (=<<) (\(_,cfclty,sfc) -> maybe [] ((: []) . fst) cfclty ++ [sfc]) bnds)
518 pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))
519 mergePDPairs pun starsFC' [] r = r
520 mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =
521 PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)
523-- | Parse the contents of parentheses, after an expression has been parsed.
524bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
525bracketedExpr syn openParenFC e =
526 do lchar ')'; return e
527 <|> do exprs <- some (do comma <- lcharFC ','
528 r <- expr syn
529 return (r, comma))
530 closeParenFC <- lcharFC ')'
531 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
532 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
533 <|> do starsFC <- reservedOpFC "**"
534 dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn
535 <?> "end of bracketed expression"
536 where mergePairs :: [(PTerm, FC)] -> PTerm
537 mergePairs [(t, fc)] = t
538 mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)
540-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
541-- big integer, otherwise try fromInteger and the constants as alternatives.
542-- a better solution would be to fix fromInteger to work with Integer, as the
543-- name suggests, rather than Int
544{-| Finds optimal type for integer constant -}
545modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
546modifyConst syn fc (PConstant inFC (BI x))
547 | not (inPattern syn)
548 = PConstSugar inFC $ -- wrap in original location for highlighting
549 PAlternative [] FirstSuccess
550 (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]
551 : consts)
552 | otherwise = PConstSugar inFC $
553 PAlternative [] FirstSuccess consts
554 where
555 consts = [ PConstant inFC (BI x)
556 , PConstant inFC (I (fromInteger x))
557 , PConstant inFC (B8 (fromInteger x))
558 , PConstant inFC (B16 (fromInteger x))
559 , PConstant inFC (B32 (fromInteger x))
560 , PConstant inFC (B64 (fromInteger x))
561 ]
562modifyConst syn fc x = x
564{- | Parses an alternative expression
566 Alt ::= '(|' Expr_List '|)';
568 Expr_List ::=
569 Expr'
570 | Expr' ',' Expr_List
571 ;
573-}
574alt :: SyntaxInfo -> IdrisParser PTerm
575alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
576 return (PAlternative [] FirstSuccess alts)
578{- | Parses a possibly hidden simple expression
580HSimpleExpr ::=
581 '.' SimpleExpr
582 | SimpleExpr
583 ;
585-}
586hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
587hsimpleExpr syn =
588 do lchar '.'
589 e <- simpleExpr syn
590 return $ PHidden e
591 <|> simpleExpr syn
592 <?> "expression"
594{- | Parses a unification log expression
595UnifyLog ::=
596 '%' 'unifyLog' SimpleExpr
597 ;
598-}
599unifyLog :: SyntaxInfo -> IdrisParser PTerm
600unifyLog syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "unifyLog")
601 tm <- simpleExpr syn
602 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
603 return (PUnifyLog tm)
604 <?> "unification log expression"
606{- | Parses a new-style tactics expression
607RunTactics ::=
608 '%' 'runElab' SimpleExpr
609 ;
610-}
611runElab :: SyntaxInfo -> IdrisParser PTerm
612runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab")
613 fc <- getFC
614 tm <- simpleExpr syn
615 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
616 return $ PRunElab fc tm (syn_namespace syn)
617 <?> "new-style tactics expression"
619{- | Parses a disambiguation expression
620Disamb ::=
621 'with' NameList Expr
622 ;
623-}
624disamb :: SyntaxInfo -> IdrisParser PTerm
625disamb syn = do kw <- reservedFC "with"
626 ns <- sepBy1 (fst <$> name) (lchar ',')
627 tm <- expr' syn
628 highlightP kw AnnKeyword
629 return (PDisamb (map tons ns) tm)
630 <?> "namespace disambiguation expression"
631 where tons (NS n s) = txt (show n) : s
632 tons n = [txt (show n)]
633{- | Parses a no implicits expression
635NoImplicits ::=
636 '%' 'noImplicits' SimpleExpr
637 ;
639-}
640noImplicits :: SyntaxInfo -> IdrisParser PTerm
641noImplicits syn = do try (lchar '%' *> reserved "noImplicits")
642 tm <- simpleExpr syn
643 return (PNoImplicits tm)
644 <?> "no implicits expression"
646{- | Parses a function application expression
648App ::=
649 'mkForeign' Arg Arg*
650 | MatchApp
651 | SimpleExpr Arg*
652 ;
653MatchApp ::=
654 SimpleExpr '<==' FnName
655 ;
657-}
658app :: SyntaxInfo -> IdrisParser PTerm
659app syn = do f <- simpleExpr syn
660 (do try $ reservedOp "<=="
661 fc <- getFC
662 ff <- fst <$> fnName
663 return (PLet fc (sMN 0 "match") NoFC
664 f
665 (PMatchApp fc ff)
666 (PRef fc [] (sMN 0 "match")))
667 <?> "matching application expression") <|> (do
668 fc <- getFC
669 i <- get
670 args <- many (do notEndApp; arg syn)
671 case args of
672 [] -> return f
673 _ -> return (flattenFromInt fc f args))
674 <?> "function application"
675 where
676 -- bit of a hack to deal with the situation where we're applying a
677 -- literal to an argument, which we may want for obscure applications
678 -- of fromInteger, and this will help disambiguate better.
679 -- We know, at least, it won't be one of the constants!
680 flattenFromInt fc (PAlternative _ x alts) args
681 | Just i <- getFromInt alts
682 = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)
683 flattenFromInt fc f args = PApp fc f args
685 getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a
686 getFromInt (_ : xs) = getFromInt xs
687 getFromInt _ = Nothing
689{-| Parses a function argument
691Arg ::=
692 ImplicitArg
693 | ConstraintArg
694 | SimpleExpr
695 ;
697-}
698arg :: SyntaxInfo -> IdrisParser PArg
699arg syn = implicitArg syn
700 <|> constraintArg syn
701 <|> do e <- simpleExpr syn
702 return (pexp e)
703 <?> "function argument"
705{-| Parses an implicit function argument
707ImplicitArg ::=
708 '{' Name ('=' Expr)? '}'
709 ;
711-}
712implicitArg :: SyntaxInfo -> IdrisParser PArg
713implicitArg syn = do lchar '{'
714 (n, nfc) <- name
715 fc <- getFC
716 v <- option (PRef nfc [nfc] n) (do lchar '='
717 expr syn)
718 lchar '}'
719 return (pimp n v True)
720 <?> "implicit function argument"
722{-| Parses a constraint argument (for selecting a named type class instance)
724> ConstraintArg ::=
725> '@{' Expr '}'
726> ;
728-}
729constraintArg :: SyntaxInfo -> IdrisParser PArg
730constraintArg syn = do symbol "@{"
731 e <- expr syn
732 symbol "}"
733 return (pconst e)
734 <?> "constraint argument"
736{-| Parses a quasiquote expression (for building reflected terms using the elaborator)
738> Quasiquote ::= '`(' Expr ')'
740-}
741quasiquote :: SyntaxInfo -> IdrisParser PTerm
742quasiquote syn = do startFC <- symbolFC "`("
743 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,
744 inPattern = False }
745 g <- optional $
746 do fc <- symbolFC ":"
747 ty <- expr syn { inPattern = False } -- don't allow antiquotes
748 return (ty, fc)
749 endFC <- symbolFC ")"
750 mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]
751 case g of
752 Just (_, fc) -> highlightP fc AnnKeyword
753 _ -> return ()
754 return $ PQuasiquote e (fst <$> g)
755 <?> "quasiquotation"
757{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)
759> Unquote ::= ',' Expr
761-}
762unquote :: SyntaxInfo -> IdrisParser PTerm
763unquote syn = do guard (syn_in_quasiquote syn > 0)
764 startFC <- symbolFC "~"
765 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
766 endFC <- getFC
767 highlightP startFC AnnKeyword
768 highlightP (spanFC startFC endFC) AnnAntiquote
769 return $ PUnquote e
770 <?> "unquotation"
772{-| Parses a quotation of a name (for using the elaborator to resolve boring details)
774> NameQuote ::= '`{' Name '}'
776-}
777namequote :: SyntaxInfo -> IdrisParser PTerm
778namequote syn = do (startFC, res) <-
779 try (do fc <- symbolFC "`{{"
780 return (fc, False)) <|>
781 (do fc <- symbolFC "`{"
782 return (fc, True))
783 (n, nfc) <- fnName
784 endFC <- if res then symbolFC "}" else symbolFC "}}"
785 mapM_ (uncurry highlightP)
786 [ (startFC, AnnKeyword)
787 , (endFC, AnnKeyword)
788 , (spanFC startFC endFC, AnnQuasiquote)
789 ]
790 return $ PQuoteName n res nfc
791 <?> "quoted name"
794{-| Parses a record field setter expression
796RecordType ::=
797 'record' '{' FieldTypeList '}';
800FieldTypeList ::=
801 FieldType
802 | FieldType ',' FieldTypeList
803 ;
806FieldType ::=
807 FnName '=' Expr
808 ;
810-}
811recordType :: SyntaxInfo -> IdrisParser PTerm
812recordType syn =
813 do kw <- reservedFC "record"
814 lchar '{'
815 fgs <- fieldGetOrSet
816 lchar '}'
817 fc <- getFC
818 rec <- optional (simpleExpr syn)
819 highlightP kw AnnKeyword
820 case fgs of
821 Left fields ->
822 case rec of
823 Nothing ->
824 return (PLam fc (sMN 0 "fldx") NoFC Placeholder
825 (applyAll fc fields (PRef fc [] (sMN 0 "fldx"))))
826 Just v -> return (applyAll fc fields v)
827 Right fields ->
828 case rec of
829 Nothing ->
830 return (PLam fc (sMN 0 "fldx") NoFC Placeholder
831 (getAll fc (reverse fields)
832 (PRef fc [] (sMN 0 "fldx"))))
833 Just v -> return (getAll fc (reverse fields) v)
835 <?> "record setting expression"
836 where fieldSet :: IdrisParser ([Name], PTerm)
837 fieldSet = do ns <- fieldGet
838 lchar '='
839 e <- expr syn
840 return (ns, e)
841 <?> "field setter"
843 fieldGet :: IdrisParser [Name]
844 fieldGet = sepBy1 (fst <$> fnName) (symbol "->")
846 fieldGetOrSet :: IdrisParser (Either [([Name], PTerm)] [Name])
847 fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')
848 return (Left fs))
849 <|> do f <- fieldGet
850 return (Right f)
852 applyAll :: FC -> [([Name], PTerm)] -> PTerm -> PTerm
853 applyAll fc [] x = x
854 applyAll fc ((ns, e) : es) x
855 = applyAll fc es (doUpdate fc ns e x)
857 doUpdate fc [n] e get
858 = PApp fc (PRef fc [] (mkType n)) [pexp e, pexp get]
859 doUpdate fc (n : ns) e get
860 = PApp fc (PRef fc [] (mkType n))
861 [pexp (doUpdate fc ns e (PApp fc (PRef fc [] n) [pexp get])),
862 pexp get]
864 getAll :: FC -> [Name] -> PTerm -> PTerm
865 getAll fc [n] e = PApp fc (PRef fc [] n) [pexp e]
866 getAll fc (n:ns) e = PApp fc (PRef fc [] n) [pexp (getAll fc ns e)]
869-- | Creates setters for record types on necessary functions
870mkType :: Name -> Name
871mkType (UN n) = sUN ("set_" ++ str n)
872mkType (MN 0 n) = sMN 0 ("set_" ++ str n)
873mkType (NS n s) = NS (mkType n) s
875{- | Parses a type signature
877TypeSig ::=
878 ':' Expr
879 ;
882TypeExpr ::= ConstraintList? Expr;
884 -}
885typeExpr :: SyntaxInfo -> IdrisParser PTerm
886typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
887 sc <- expr syn
888 return (bindList (PPi constraint) cs sc)
889 <?> "type signature"
891{- | Parses a lambda expression
893Lambda ::=
894 '\\' TypeOptDeclList LambdaTail
895 | '\\' SimpleExprList LambdaTail
896 ;
899SimpleExprList ::=
900 SimpleExpr
901 | SimpleExpr ',' SimpleExprList
902 ;
905LambdaTail ::=
906 Impossible
907 | '=>' Expr
909-}
910lambda :: SyntaxInfo -> IdrisParser PTerm
911lambda syn = do lchar '\\' <?> "lambda expression"
912 ((do xt <- try $ tyOptDeclList syn
913 fc <- getFC
914 sc <- lambdaTail
915 return (bindList (PLam fc) xt sc))
916 <|>
917 (do ps <- sepBy (do fc <- getFC
918 e <- simpleExpr (syn { inPattern = True })
919 return (fc, e))
920 (lchar ',')
921 sc <- lambdaTail
922 return (pmList (zip [0..] ps) sc)))
923 <?> "lambda expression"
924 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
925 pmList [] sc = sc
926 pmList ((i, (fc, x)) : xs) sc
927 = PLam fc (sMN i "lamp") NoFC Placeholder
928 (PCase fc (PRef fc [] (sMN i "lamp"))
929 [(x, pmList xs sc)])
930 lambdaTail :: IdrisParser PTerm
931 lambdaTail = impossible <|> symbol "=>" *> expr syn
933{- | Parses a term rewrite expression
935RewriteTerm ::=
936 'rewrite' Expr ('==>' Expr)? 'in' Expr
937 ;
939-}
940rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
941rewriteTerm syn = do kw <- reservedFC "rewrite"
942 fc <- getFC
943 prf <- expr syn
944 giving <- optional (do symbol "==>"; expr' syn)
945 kw' <- reservedFC "in"; sc <- expr syn
946 highlightP kw AnnKeyword
947 highlightP kw' AnnKeyword
948 return (PRewrite fc
949 (PApp fc (PRef fc [] (sUN "sym")) [pexp prf]) sc
950 giving)
951 <?> "term rewrite expression"
953{- |Parses a let binding
955Let ::=
956 'let' Name TypeSig'? '=' Expr 'in' Expr
957| 'let' Expr' '=' Expr' 'in' Expr
959TypeSig' ::=
960 ':' Expr'
961 ;
963 -}
964let_ :: SyntaxInfo -> IdrisParser PTerm
965let_ syn = try (do kw <- reservedFC "let"
966 ls <- indentedBlock (let_binding syn)
967 kw' <- reservedFC "in"; sc <- expr syn
968 highlightP kw AnnKeyword; highlightP kw' AnnKeyword
969 return (buildLets ls sc))
970 <?> "let binding"
971 where buildLets [] sc = sc
972 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc
973 = PLet fc n nfc ty v (buildLets ls sc)
974 buildLets ((fc, pat, ty, v, alts) : ls) sc
975 = PCase fc v ((pat, buildLets ls sc) : alts)
977let_binding syn = do fc <- getFC;
978 pat <- expr' (syn { inPattern = True })
979 ty <- option Placeholder (do lchar ':'; expr' syn)
980 lchar '='
981 v <- expr syn
982 ts <- option [] (do lchar '|'
983 sepBy1 (do_alt syn) (lchar '|'))
984 return (fc,pat,ty,v,ts)
986{- | Parses a conditional expression
988If ::= 'if' Expr 'then' Expr 'else' Expr
991-}
992if_ :: SyntaxInfo -> IdrisParser PTerm
993if_ syn = (do ifFC <- reservedFC "if"
994 fc <- getFC
995 c <- expr syn
996 thenFC <- reservedFC "then"
997 t <- expr syn
998 elseFC <- reservedFC "else"
999 f <- expr syn
1000 mapM_ (flip highlightP AnnKeyword) [ifFC, thenFC, elseFC]
1001 return (PIfThenElse fc c t f))
1002 <?> "conditional expression"
1005{- | Parses a quote goal
1008QuoteGoal ::=
1009 'quoteGoal' Name 'by' Expr 'in' Expr
1012 -}
1013quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1014quoteGoal syn = do kw1 <- reservedFC "quoteGoal"; n <- fst <$> name;
1015 kw2 <- reservedFC "by"
1016 r <- expr syn
1017 kw3 <- reservedFC "in"
1018 fc <- getFC
1019 sc <- expr syn
1020 mapM_ (flip highlightP AnnKeyword) [kw1, kw2, kw3]
1021 return (PGoal fc r n sc)
1022 <?> "quote goal expression"
1024{- | Parses a dependent type signature
1027Pi ::= PiOpts Static? Pi'
1031Pi' ::=
1032 OpExpr ('->' Pi)?
1033 | '(' TypeDeclList ')' '->' Pi
1034 | '{' TypeDeclList '}' '->' Pi
1035 | '{' 'auto' TypeDeclList '}' '->' Pi
1036 | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi
1039 -}
1041bindsymbol opts st syn
1042 = do symbol "->"
1043 return (Exp opts st False)
1045explicitPi opts st syn
1046 = do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')
1047 binder <- bindsymbol opts st syn
1048 sc <- expr syn
1049 return (bindList (PPi binder) xt sc)
1051autoImplicit opts st syn
1052 = do kw <- reservedFC "auto"
1053 when (st == Static) $ fail "auto implicits can not be static"
1054 xt <- typeDeclList syn
1055 lchar '}'
1056 symbol "->"
1057 sc <- expr syn
1058 highlightP kw AnnKeyword
1059 return (bindList (PPi
1060 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)
1062defaultImplicit opts st syn = do
1063 kw <- reservedFC "default"
1064 when (st == Static) $ fail "default implicits can not be static"
1065 ist <- get
1066 script' <- simpleExpr syn
1067 let script = debindApp syn . desugar syn ist $ script'
1068 xt <- typeDeclList syn
1069 lchar '}'
1070 symbol "->"
1071 sc <- expr syn
1072 highlightP kw AnnKeyword
1073 return (bindList (PPi (TacImp [] Dynamic script)) xt sc)
1075normalImplicit opts st syn = do
1076 xt <- typeDeclList syn <* lchar '}'
1077 symbol "->"
1078 cs <- constraintList syn
1079 sc <- expr syn
1080 let (im,cl)
1081 = if implicitAllowed syn
1082 then (Imp opts st False (Just (Impl False True)) True,
1083 constraint)
1084 else (Imp opts st False (Just (Impl False False)) True,
1085 Imp opts st False (Just (Impl True False)) True)
1086 return (bindList (PPi im) xt
1087 (bindList (PPi cl) cs sc))
1089implicitPi opts st syn =
1090 autoImplicit opts st syn
1091 <|> defaultImplicit opts st syn
1092 <|> normalImplicit opts st syn
1094unboundPi opts st syn = do
1095 x <- opExpr syn
1096 (do binder <- bindsymbol opts st syn
1097 sc <- expr syn
1098 return (PPi binder (sUN "__pi_arg") NoFC x sc))
1099 <|> return x
1101pi :: SyntaxInfo -> IdrisParser PTerm
1102pi syn =
1103 do opts <- piOpts syn
1104 st <- static
1105 explicitPi opts st syn
1106 <|> try (do lchar '{'; implicitPi opts st syn)
1107 <|> unboundPi opts st syn
1108 <?> "dependent type signature"
1110{- | Parses Possible Options for Pi Expressions
1112 PiOpts ::= '.'?
1115piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
1116piOpts syn | implicitAllowed syn =
1117 lchar '.' *> return [InaccessibleArg]
1118 <|> return []
1119piOpts syn = return []
1121{- | Parses a type constraint list
1124ConstraintList ::=
1125 '(' Expr_List ')' '=>'
1126 | Expr '=>'
1130constraintList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1131constraintList syn = try (constraintList1 syn)
1132 <|> return []
1134constraintList1 :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1135constraintList1 syn = try (do lchar '('
1136 tys <- sepBy1 nexpr (lchar ',')
1137 lchar ')'
1138 reservedOp "=>"
1139 return tys)
1140 <|> try (do t <- opExpr (disallowImp syn)
1141 reservedOp "=>"
1142 return [(defname, NoFC, t)])
1143 <?> "type constraint list"
1144 where nexpr = try (do (n, fc) <- name; lchar ':'
1145 e <- expr syn
1146 return (n, fc, e))
1147 <|> do e <- expr syn
1148 return (defname, NoFC, e)
1149 defname = sMN 0 "constraint"
1151{- | Parses a type declaration list
1153TypeDeclList ::=
1154 FunctionSignatureList
1155 | NameList TypeSig
1160FunctionSignatureList ::=
1161 Name TypeSig
1162 | Name TypeSig ',' FunctionSignatureList
1166typeDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1167typeDeclList syn = try (sepBy1 (do (x, xfc) <- fnName
1168 lchar ':'
1169 t <- typeExpr (disallowImp syn)
1170 return (x, xfc, t))
1171 (lchar ','))
1172 <|> do ns <- sepBy1 name (lchar ',')
1173 lchar ':'
1174 t <- typeExpr (disallowImp syn)
1175 return (map (\(x, xfc) -> (x, xfc, t)) ns)
1176 <?> "type declaration list"
1178{- | Parses a type declaration list with optional parameters
1180TypeOptDeclList ::=
1181 NameOrPlaceholder TypeSig?
1182 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1187NameOrPlaceHolder ::= Name | '_';
1190tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1191tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder
1192 t <- option Placeholder (do lchar ':'
1193 expr syn)
1194 return (x, fc, t))
1195 (lchar ',')
1196 <?> "type declaration list"
1197 where nameOrPlaceholder :: IdrisParser (Name, FC)
1198 nameOrPlaceholder = fnName
1199 <|> do symbol "_"
1200 return (sMN 0 "underscore", NoFC)
1201 <?> "name or placeholder"
1203{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]
1205ListExpr ::=
1206 '[' ']'
1207 | '[' Expr '|' DoList ']'
1208 | '[' ExprList ']'
1212DoList ::=
1213 Do
1214 | Do ',' DoList
1218ExprList ::=
1219 Expr
1220 | Expr ',' ExprList
1223 -}
1224listExpr :: SyntaxInfo -> IdrisParser PTerm
1225listExpr syn = do (FC f (l, c) _) <- getFC
1226 lchar '['; fc <- getFC;
1227 (try . token $ do (char ']' <?> "end of list expression")
1228 (FC _ _ (l', c')) <- getFC
1229 return (mkNil (FC f (l, c) (l', c'))))
1230 <|> (do x <- expr syn <?> "expression"
1231 (do try (lchar '|') <?> "list comprehension"
1232 qs <- sepBy1 (do_ syn) (lchar ',')
1233 lchar ']'
1234 return (PDoBlock (map addGuard qs ++
1235 [DoExp fc (PApp fc (PRef fc [] (sUN "return"))
1236 [pexp x])]))) <|>
1237 (do xs <- many (do (FC fn (sl, sc) _) <- getFC
1238 lchar ',' <?> "list element"
1239 let commaFC = FC fn (sl, sc) (sl, sc + 1)
1240 elt <- expr syn
1241 return (elt, commaFC))
1242 (FC fn (sl, sc) _) <- getFC
1243 lchar ']' <?> "end of list expression"
1244 let rbrackFC = FC fn (sl, sc) (sl, sc+1)
1245 return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))
1246 <?> "list expression"
1247 where
1248 mkNil :: FC -> PTerm
1249 mkNil fc = PRef fc [fc] (sUN "Nil")
1250 mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm
1251 mkList errFC nilFC [] = PRef nilFC [nilFC] (sUN "Nil")
1252 mkList errFC nilFC ((x, fc) : xs) = PApp errFC (PRef fc [fc] (sUN "::")) [pexp x, pexp (mkList errFC nilFC xs)]
1253 addGuard :: PDo -> PDo
1254 addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc [] (sUN "guard"))
1255 [pexp e])
1256 addGuard x = x
1258{- | Parses a do-block
1260Do' ::= Do KeepTerminator;
1264DoBlock ::=
1265 'do' OpenBlock Do'+ CloseBlock
1268 -}
1269doBlock :: SyntaxInfo -> IdrisParser PTerm
1270doBlock syn
1271 = do kw <- reservedFC "do"
1272 ds <- indentedBlock1 (do_ syn)
1273 highlightP kw AnnKeyword
1274 return (PDoBlock ds)
1275 <?> "do block"
1277{- | Parses an expression inside a do block
1279Do ::=
1280 'let' Name TypeSig'? '=' Expr
1281 | 'let' Expr' '=' Expr
1282 | Name '<-' Expr
1283 | Expr' '<-' Expr
1284 | Expr
1288do_ :: SyntaxInfo -> IdrisParser PDo
1289do_ syn
1290 = try (do kw <- reservedFC "let"
1291 (i, ifc) <- name
1292 ty <- option Placeholder (do lchar ':'
1293 expr' syn)
1294 reservedOp "="
1295 fc <- getFC
1296 e <- expr syn
1297 highlightP kw AnnKeyword
1298 return (DoLet fc i ifc ty e))
1299 <|> try (do kw <- reservedFC "let"
1300 i <- expr' syn
1301 reservedOp "="
1302 fc <- getFC
1303 sc <- expr syn
1304 highlightP kw AnnKeyword
1305 return (DoLetP fc i sc))
1306 <|> try (do (i, ifc) <- name
1307 symbol "<-"
1308 fc <- getFC
1309 e <- expr syn;
1310 option (DoBind fc i ifc e)
1311 (do lchar '|'
1312 ts <- sepBy1 (do_alt syn) (lchar '|')
1313 return (DoBindP fc (PRef ifc [ifc] i) e ts)))
1314 <|> try (do i <- expr' syn
1315 symbol "<-"
1316 fc <- getFC
1317 e <- expr syn;
1318 option (DoBindP fc i e [])
1319 (do lchar '|'
1320 ts <- sepBy1 (do_alt syn) (lchar '|')
1321 return (DoBindP fc i e ts)))
1322 <|> do e <- expr syn
1323 fc <- getFC
1324 return (DoExp fc e)
1325 <?> "do block expression"
1327do_alt syn = do l <- expr' syn
1328 option (Placeholder, l)
1329 (do symbol "=>"
1330 r <- expr' syn
1331 return (l, r))
1333{- | Parses an expression in idiom brackets
1335Idiom ::= '[|' Expr '|]';
1338idiom :: SyntaxInfo -> IdrisParser PTerm
1339idiom syn
1340 = do symbol "[|"
1341 fc <- getFC
1342 e <- expr syn
1343 symbol "|]"
1344 return (PIdiom fc e)
1345 <?> "expression in idiom brackets"
1347{- |Parses a constant or literal expression
1350Constant ::=
1351 'Integer'
1352 | 'Int'
1353 | 'Char'
1354 | 'Double'
1355 | 'String'
1356 | 'Bits8'
1357 | 'Bits16'
1358 | 'Bits32'
1359 | 'Bits64'
1360 | Float_t
1361 | Natural_t
1362 | VerbatimString_t
1363 | String_t
1364 | Char_t
1369constants :: [(String, Idris.Core.TT.Const)]
1370constants =
1371 [ ("Integer", AType (ATInt ITBig))
1372 , ("Int", AType (ATInt ITNative))
1373 , ("Char", AType (ATInt ITChar))
1374 , ("Double", AType ATFloat)
1375 , ("String", StrType)
1376 , ("prim__WorldType", WorldType)
1377 , ("prim__TheWorld", TheWorld)
1378 , ("Bits8", AType (ATInt (ITFixed IT8)))
1379 , ("Bits16", AType (ATInt (ITFixed IT16)))
1380 , ("Bits32", AType (ATInt (ITFixed IT32)))
1381 , ("Bits64", AType (ATInt (ITFixed IT64)))
1384-- | Parse a constant and its source span
1385constant :: IdrisParser (Idris.Core.TT.Const, FC)
1386constant = choice [ do fc <- reservedFC name; return (ty, fc)
1387 | (name, ty) <- constants
1389 <|> do (f, fc) <- try float; return (Fl f, fc)
1390 <|> do (i, fc) <- natural; return (BI i, fc)
1391 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)
1392 <|> do (s, fc) <- stringLiteral; return (Str s, fc)
1393 <|> do (c, fc) <- try charLiteral; return (Ch c, fc) --Currently ambigous with symbols
1394 <?> "constant or literal"
1396{- | Parses a verbatim multi-line string literal (triple-quoted)
1399VerbatimString_t ::=
1400 '\"\"\"' ~'\"\"\"' '\"\"\"'
1403 -}
1404verbatimStringLiteral :: MonadicParsing m => m (String, FC)
1405verbatimStringLiteral = token $ do (FC f start _) <- getFC
1406 try $ string "\"\"\""
1407 str <- manyTill anyChar $ try (string "\"\"\"")
1408 (FC _ _ end) <- getFC
1409 return (str, FC f start end)
1411{- | Parses a static modifier
1414Static ::=
1415 '[' static ']'
1419static :: IdrisParser Static
1420static = do reserved "%static"; return Static
1421 <|> do reserved "[static]"
1422 fc <- getFC
1423 parserWarning fc Nothing (Msg "The use of [static] is deprecated, use %static instead.")
1424 return Static
1425 <|> return Dynamic
1426 <?> "static modifier"
1428{- | Parses a tactic script
1431Tactic ::= 'intro' NameList?
1432 | 'intros'
1433 | 'refine' Name Imp+
1434 | 'mrefine' Name
1435 | 'rewrite' Expr
1436 | 'induction' Expr
1437 | 'equiv' Expr
1438 | 'let' Name ':' Expr' '=' Expr
1439 | 'let' Name '=' Expr
1440 | 'focus' Name
1441 | 'exact' Expr
1442 | 'applyTactic' Expr
1443 | 'reflect' Expr
1444 | 'fill' Expr
1445 | 'try' Tactic '|' Tactic
1446 | '{' TacticSeq '}'
1447 | 'compute'
1448 | 'trivial'
1449 | 'solve'
1450 | 'attack'
1451 | 'state'
1452 | 'term'
1453 | 'undo'
1454 | 'qed'
1455 | 'abandon'
1456 | ':' 'q'
1459Imp ::= '?' | '_';
1461TacticSeq ::=
1462 Tactic ';' Tactic
1463 | Tactic ';' TacticSeq
1468-- | A specification of the arguments that tactics can take
1469data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
1470 | ExprTArg
1471 | AltsTArg
1472 | StringLitTArg
1474-- The FIXMEs are Issue #1766 in the issue tracker.
1475-- https://github.com/idris-lang/Idris-dev/issues/1766
1476-- | A list of available tactics and their argument requirements
1477tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
1478tactics =
1479 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)
1480 do ns <- sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)
1481 , noArgs ["intros"] Intros
1482 , noArgs ["unfocus"] Unfocus
1483 , (["refine"], Just ExprTArg, const $
1484 do n <- spaced (fst <$> fnName)
1485 imps <- many imp
1486 return $ Refine n imps)
1487 , (["claim"], Nothing, \syn ->
1488 do n <- indentPropHolds gtProp *> (fst <$> name)
1489 goal <- indentPropHolds gtProp *> expr syn
1490 return $ Claim n goal)
1491 , (["mrefine"], Just ExprTArg, const $
1492 do n <- spaced (fst <$> fnName)
1493 return $ MatchRefine n)
1494 , expressionTactic ["rewrite"] Rewrite
1495 , expressionTactic ["case"] CaseTac
1496 , expressionTactic ["induction"] Induction
1497 , expressionTactic ["equiv"] Equiv
1498 , (["let"], Nothing, \syn -> -- FIXME syntax for let
1499 do n <- (indentPropHolds gtProp *> (fst <$> name))
1500 (do indentPropHolds gtProp *> lchar ':'
1501 ty <- indentPropHolds gtProp *> expr' syn
1502 indentPropHolds gtProp *> lchar '='
1503 t <- indentPropHolds gtProp *> expr syn
1504 i <- get
1505 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1506 <|> (do indentPropHolds gtProp *> lchar '='
1507 t <- indentPropHolds gtProp *> expr syn
1508 i <- get
1509 return $ LetTac n (desugar syn i t)))
1511 , (["focus"], Just ExprTArg, const $
1512 do n <- spaced (fst <$> name)
1513 return $ Focus n)
1514 , expressionTactic ["exact"] Exact
1515 , expressionTactic ["applyTactic"] ApplyTactic
1516 , expressionTactic ["byReflection"] ByReflection
1517 , expressionTactic ["reflect"] Reflect
1518 , expressionTactic ["fill"] Fill
1519 , (["try"], Just AltsTArg, \syn ->
1520 do t <- spaced (tactic syn)
1521 lchar '|'
1522 t1 <- spaced (tactic syn)
1523 return $ Try t t1)
1524 , noArgs ["compute"] Compute
1525 , noArgs ["trivial"] Trivial
1526 , noArgs ["unify"] DoUnify
1527 , (["search"], Nothing, const $
1528 do depth <- option 10 $ fst <$> natural
1529 return (ProofSearch True True (fromInteger depth) Nothing [] []))
1530 , noArgs ["instance"] TCInstance
1531 , noArgs ["solve"] Solve
1532 , noArgs ["attack"] Attack
1533 , noArgs ["state", ":state"] ProofState
1534 , noArgs ["term", ":term"] ProofTerm
1535 , noArgs ["undo", ":undo"] Undo
1536 , noArgs ["qed", ":qed"] Qed
1537 , noArgs ["abandon", ":q"] Abandon
1538 , noArgs ["skip"] Skip
1539 , noArgs ["sourceLocation"] SourceFC
1540 , expressionTactic [":e", ":eval"] TEval
1541 , expressionTactic [":t", ":type"] TCheck
1542 , expressionTactic [":search"] TSearch
1543 , (["fail"], Just StringLitTArg, const $
1544 do msg <- fst <$> stringLiteral
1545 return $ TFail [Idris.Core.TT.TextPart msg])
1546 , ([":doc"], Just ExprTArg, const $
1547 do whiteSpace
1548 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1549 eof
1550 return (TDocStr doc))
1552 where
1553 expressionTactic names tactic = (names, Just ExprTArg, \syn ->
1554 do t <- spaced (expr syn)
1555 i <- get
1556 return $ tactic (desugar syn i t))
1557 noArgs names tactic = (names, Nothing, const (return tactic))
1558 spaced parser = indentPropHolds gtProp *> parser
1559 imp :: IdrisParser Bool
1560 imp = do lchar '?'; return False
1561 <|> do lchar '_'; return True
1564tactic :: SyntaxInfo -> IdrisParser PTactic
1565tactic syn = choice [ do choice (map reserved names); parser syn
1566 | (names, _, parser) <- tactics ]
1567 <|> do lchar '{'
1568 t <- tactic syn;
1569 lchar ';';
1570 ts <- sepBy1 (tactic syn) (lchar ';')
1571 lchar '}'
1572 return $ TSeq t (mergeSeq ts)
1573 <|> ((lchar ':' >> empty) <?> "prover command")
1574 <?> "tactic"
1575 where
1576 mergeSeq :: [PTactic] -> PTactic
1577 mergeSeq [t] = t
1578 mergeSeq (t:ts) = TSeq t (mergeSeq ts)
1580-- | Parses a tactic as a whole
1581fullTactic :: SyntaxInfo -> IdrisParser PTactic
1582fullTactic syn = do t <- tactic syn
1583 eof
1584 return t