git.iko.soy/Idris-dev
on c112ebc help sign in
Idris-dev/src/Idris/Parser/Expr.hs
1651 lines 58 kB history raw
1{-|
2Module : Idris.Parser.Expr
3Description : Parse Expressions.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
9 PatternGuards, TupleSections #-}
10module Idris.Parser.Expr where
12import Idris.AbsSyntax
13import Idris.Core.TT
14import Idris.DSL
15import Idris.Options
16import Idris.Parser.Helpers
17import Idris.Parser.Ops
19import Prelude hiding (pi)
21import Control.Applicative
22import Control.Arrow (left)
23import Control.Monad
24import Control.Monad.State.Strict
25import Data.Function (on)
26import Data.List
27import Data.Maybe
28import qualified Text.Parser.Token as Tok
29import Text.Parser.Expression
30import Text.Megaparsec ((<?>))
31import qualified Text.Megaparsec as P
32import qualified Text.Megaparsec.Char as P
34-- | Allow implicit type declarations
35allowImp :: SyntaxInfo -> SyntaxInfo
36allowImp syn = syn { implicitAllowed = True,
37 constraintAllowed = False }
39-- | Disallow implicit type declarations
40disallowImp :: SyntaxInfo -> SyntaxInfo
41disallowImp = scopedImp
43-- | Implicits hare are scoped rather than top level
44scopedImp :: SyntaxInfo -> SyntaxInfo
45scopedImp syn = syn { implicitAllowed = False,
46 constraintAllowed = False }
48-- | Allow scoped constraint arguments
49allowConstr :: SyntaxInfo -> SyntaxInfo
50allowConstr syn = syn { constraintAllowed = True }
52{-| Parses an expression as a whole
54 FullExpr ::= Expr EOF_t;
56 -}
57fullExpr :: SyntaxInfo -> IdrisParser PTerm
58fullExpr syn = do x <- expr syn
59 P.eof
60 i <- get
61 return $ debindApp syn (desugar syn i x)
63tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
64tryFullExpr syn st = left (Msg . show . parseErrorDoc) . runparser (fullExpr syn) st ""
66{- | Parses an expression
68 Expr ::= Pi
70 -}
71expr :: SyntaxInfo -> IdrisParser PTerm
72expr = pi
74{- | Parses an expression with possible operator applied
76 OpExpr ::= {- Expression Parser with Operators based on Expr' -};
78-}
79opExpr :: SyntaxInfo -> IdrisParser PTerm
80opExpr syn = do i <- get
81 buildExpressionParser (table (idris_infixes i))
82 (expr' syn)
84{- | Parses either an internally defined expression or
85 a user-defined one
87Expr' ::= "External (User-defined) Syntax"
88 | InternalExpr;
90 -}
91expr' :: SyntaxInfo -> IdrisParser PTerm
92expr' syn = P.try (externalExpr syn)
93 <|> internalExpr syn
94 <?> "expression"
96{- | Parses a user-defined expression -}
97externalExpr :: SyntaxInfo -> IdrisParser PTerm
98externalExpr syn = do i <- get
99 (FC fn start _) <- getFC
100 expr <- extensions syn (syntaxRulesList $ syntax_rules i)
101 (FC _ _ end) <- getFC
102 let outerFC = FC fn start end
103 return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)
104 <?> "user-defined expression"
105 where -- Fix non-highlighting FCs by approximating with the span of the syntax application
106 fixFC outer inner | inner `fcIn` outer = inner
107 | otherwise = outer
108 -- Fix highlighting FCs by making them useless, to avoid spurious highlights
109 fixFCH fn outer inner | inner `fcIn` outer = inner
110 | otherwise = FileFC fn
112{- | Parses a simple user-defined expression -}
113simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
114simpleExternalExpr syn = do i <- get
115 extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))
116 where
117 isSimple (Rule (Expr x:xs) _ _) = False
118 isSimple (Rule (SimpleExpr x:xs) _ _) = False
119 isSimple (Rule [Keyword _] _ _) = True
120 isSimple (Rule [Symbol _] _ _) = True
121 isSimple (Rule (_:xs) _ _) = case last xs of
122 Keyword _ -> True
123 Symbol _ -> True
124 _ -> False
125 isSimple _ = False
127{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
128extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
129extensions syn rules = extension syn [] (filter isValid rules)
130 <?> "user-defined expression"
131 where
132 isValid :: Syntax -> Bool
133 isValid (Rule _ _ AnySyntax) = True
134 isValid (Rule _ _ PatternSyntax) = inPattern syn
135 isValid (Rule _ _ TermSyntax) = not (inPattern syn)
136 isValid (DeclRule _ _) = False
138data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information
139 deriving Show
141extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
142extension syn ns rules =
143 P.choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
144 case head rs of -- can never be []
145 Rule (symb:_) _ _ -> P.try $ do
146 n <- extensionSymbol symb
147 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]
148 -- If we have more than one Rule in this bucket, our grammar is
149 -- nondeterministic.
150 Rule [] ptm _ -> return (flatten (updateSynMatch (mapMaybe id ns) ptm))
151 where
152 ruleGroup [] [] = True
153 ruleGroup (s1:_) (s2:_) = s1 == s2
154 ruleGroup _ _ = False
156 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
157 extensionSymbol (Keyword n) = do fc <- reservedFC (show n)
158 highlightP fc AnnKeyword
159 return Nothing
160 extensionSymbol (Expr n) = do tm <- expr syn
161 return $ Just (n, SynTm tm)
162 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
163 return $ Just (n, SynTm tm)
164 extensionSymbol (Binding n) = do (b, fc) <- name
165 return $ Just (n, SynBind fc b)
166 extensionSymbol (Symbol s) = do fc <- symbolFC s
167 highlightP fc AnnKeyword
168 return Nothing
170 flatten :: PTerm -> PTerm -- flatten application
171 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
172 flatten t = t
174updateSynMatch = update
175 where
176 updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
177 updateB ns (n, fc) = case lookup n ns of
178 Just (SynBind tfc t) -> (t, tfc)
179 _ -> (n, fc)
181 update :: [(Name, SynMatch)] -> PTerm -> PTerm
182 update ns (PRef fc hls n) = case lookup n ns of
183 Just (SynTm t) -> t
184 _ -> PRef fc hls n
185 update ns (PPatvar fc n) = uncurry (flip PPatvar) $ updateB ns (n, fc)
186 update ns (PLam fc n nfc ty sc)
187 = let (n', nfc') = updateB ns (n, nfc)
188 in PLam fc n' nfc' (update ns ty) (update (dropn n ns) sc)
189 update ns (PPi p n fc ty sc)
190 = let (n', nfc') = updateB ns (n, fc)
191 in PPi (updTacImp ns p) n' nfc'
192 (update ns ty) (update (dropn n ns) sc)
193 update ns (PLet fc rc n nfc ty val sc)
194 = let (n', nfc') = updateB ns (n, nfc)
195 in PLet fc rc n' nfc' (update ns ty)
196 (update ns val) (update (dropn n ns) sc)
197 update ns (PApp fc t args)
198 = PApp fc (update ns t) (map (fmap (update ns)) args)
199 update ns (PAppBind fc t args)
200 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
201 update ns (PMatchApp fc n) = let (n', nfc') = updateB ns (n, fc)
202 in PMatchApp nfc' n'
203 update ns (PIfThenElse fc c t f)
204 = PIfThenElse fc (update ns c) (update ns t) (update ns f)
205 update ns (PCase fc c opts)
206 = PCase fc (update ns c) (map (pmap (update ns)) opts)
207 update ns (PRewrite fc by eq tm mty)
208 = PRewrite fc by (update ns eq) (update ns tm) (fmap (update ns) mty)
209 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
210 update ns (PDPair fc hls p l t r)
211 = PDPair fc hls p (update ns l) (update ns t) (update ns r)
212 update ns (PAs fc n t) = PAs fc (fst $ updateB ns (n, NoFC)) (update ns t)
213 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
214 update ns (PHidden t) = PHidden (update ns t)
215 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
216 update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds
217 where upd :: [(Name, SynMatch)] -> PDo -> PDo
218 upd ns (DoExp fc t) = DoExp fc (update ns t)
219 upd ns (DoBind fc n nfc t) = DoBind fc n nfc (update ns t)
220 upd ns (DoLet fc rc n nfc ty t) = DoLet fc rc n nfc (update ns ty) (update ns t)
221 upd ns (DoBindP fc i t ts)
222 = DoBindP fc (update ns i) (update ns t)
223 (map (\(l,r) -> (update ns l, update ns r)) ts)
224 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
225 upd ns (DoRewrite fc h) = DoRewrite fc (update ns h)
226 update ns (PIdiom fc t) = PIdiom fc $ update ns t
227 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
228 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
229 update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs
230 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
231 update ns (PUnifyLog t) = PUnifyLog $ update ns t
232 update ns (PNoImplicits t) = PNoImplicits $ update ns t
233 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)
234 update ns (PUnquote t) = PUnquote $ update ns t
235 update ns (PQuoteName n res fc) = let (n', fc') = (updateB ns (n, fc))
236 in PQuoteName n' res fc'
237 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp
238 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t
239 -- PConstSugar probably can't contain anything substitutable, but it's hard to track
240 update ns t = t
242 updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
243 -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
244 updTactic ns (Intro ns') = Intro $ map (fst . updateB ns . (, NoFC)) ns'
245 updTactic ns (Focus n) = Focus . fst $ updateB ns (n, NoFC)
246 updTactic ns (Refine n bs) = Refine (fst $ updateB ns (n, NoFC)) bs
247 updTactic ns (Claim n t) = Claim (fst $ updateB ns (n, NoFC)) (update ns t)
248 updTactic ns (MatchRefine n) = MatchRefine (fst $ updateB ns (n, NoFC))
249 updTactic ns (LetTac n t) = LetTac (fst $ updateB ns (n, NoFC)) (update ns t)
250 updTactic ns (LetTacTy n ty tm) = LetTacTy (fst $ updateB ns (n, NoFC)) (update ns ty) (update ns tm)
251 updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth
252 (fmap (fst . updateB ns . (, NoFC)) top) (map (fst . updateB ns . (, NoFC)) psns) (map (fst . updateB ns . (, NoFC)) hints)
253 updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)
254 updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)
255 updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac
256 updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)
257 updTactic ns t = fmap (update ns) t
259 updTacImp ns (TacImp o st scr r) = TacImp o st (update ns scr) r
260 updTacImp _ x = x
262 dropn :: Name -> [(Name, a)] -> [(Name, a)]
263 dropn n [] = []
264 dropn n ((x,t) : xs) | n == x = xs
265 | otherwise = (x,t):dropn n xs
268{- | Parses a (normal) built-in expression
270InternalExpr ::=
271 UnifyLog
272 | RecordType
273 | SimpleExpr
274 | Lambda
275 | QuoteGoal
276 | Let
277 | If
278 | RewriteTerm
279 | CaseExpr
280 | DoBlock
281 | App
282 ;
284-}
285internalExpr :: SyntaxInfo -> IdrisParser PTerm
286internalExpr syn =
287 unifyLog syn
288 <|> runElab syn
289 <|> disamb syn
290 <|> noImplicits syn
291 <|> recordType syn
292 <|> if_ syn
293 <|> lambda syn
294 <|> quoteGoal syn
295 <|> let_ syn
296 <|> rewriteTerm syn
297 <|> doBlock syn
298 <|> caseExpr syn
299 <|> app syn
300 <?> "expression"
302{- | Parses the "impossible" keyword
304Impossible ::= 'impossible'
306-}
307impossible :: IdrisParser PTerm
308impossible = do fc <- reservedFC "impossible"
309 highlightP fc AnnKeyword
310 return PImpossible
312{- | Parses a case expression
314CaseExpr ::=
315 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
317-}
318caseExpr :: SyntaxInfo -> IdrisParser PTerm
319caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC
320 scr <- expr syn; kw2 <- reservedFC "of";
321 opts <- indentedBlock1 (caseOption syn)
322 highlightP kw1 AnnKeyword
323 highlightP kw2 AnnKeyword
324 return (PCase fc scr opts)
325 <?> "case expression"
327{- | Parses a case in a case expression
329CaseOption ::=
330 Expr (Impossible | '=>' Expr) Terminator
331 ;
333-}
334caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
335caseOption syn = do lhs <- expr (disallowImp (syn { inPattern = True }))
336 r <- impossible <|> symbol "=>" *> expr syn
337 return (lhs, r)
338 <?> "case option"
340warnTacticDeprecation :: FC -> IdrisParser ()
341warnTacticDeprecation fc =
342 parserWarning fc (Just NoOldTacticDeprecationWarnings) (Msg "This style of tactic proof is deprecated. See %runElab for the replacement.")
344{- | Parses a proof block
346ProofExpr ::=
347 'proof' OpenBlock Tactic'* CloseBlock
348 ;
350-}
351proofExpr :: SyntaxInfo -> IdrisParser PTerm
352proofExpr syn = do kw <- reservedFC "proof"
353 ts <- indentedBlock1 (tactic syn)
354 highlightP kw AnnKeyword
355 warnTacticDeprecation kw
356 return $ PProof ts
357 <?> "proof block"
359{- | Parses a tactics block
361TacticsExpr :=
362 'tactics' OpenBlock Tactic'* CloseBlock
365-}
366tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
367tacticsExpr syn = do kw <- reservedFC "tactics"
368 ts <- indentedBlock1 (tactic syn)
369 highlightP kw AnnKeyword
370 warnTacticDeprecation kw
371 return $ PTactics ts
372 <?> "tactics block"
374{- | Parses a simple expression
376SimpleExpr ::=
377 {- External (User-defined) Simple Expression -}
378 | '?' Name
379 | % 'implementation'
380 | 'Refl' ('{' Expr '}')?
381 | ProofExpr
382 | TacticsExpr
383 | FnName
384 | Idiom
385 | List
386 | Alt
387 | Bracketed
388 | Constant
389 | Type
390 | 'Void'
391 | Quasiquote
392 | NameQuote
393 | Unquote
394 | '_'
395 ;
397-}
398simpleExpr :: SyntaxInfo -> IdrisParser PTerm
399simpleExpr syn =
400 P.try (simpleExternalExpr syn)
401 <|> do (x, FC f (l, c) end) <- P.try (lchar '?' *> name)
402 return (PMetavar (FC f (l, c-1) end) x)
403 <|> do lchar '%'; fc <- getFC; reserved "implementation"; return (PResolveTC fc)
404 <|> do lchar '%'; fc <- getFC; reserved "instance"
405 parserWarning fc Nothing $ Msg "The use of %instance is deprecated, use %implementation instead."
406 return (PResolveTC fc)
407 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
408 <|> proofExpr syn
409 <|> tacticsExpr syn
410 <|> P.try (do fc <- reservedFC "Type*"; return $ PUniverse fc AllTypes)
411 <|> do fc <- reservedFC "AnyType"; return $ PUniverse fc AllTypes
412 <|> PType <$> reservedFC "Type"
413 <|> do fc <- reservedFC "UniqueType"; return $ PUniverse fc UniqueType
414 <|> do fc <- reservedFC "NullType"; return $ PUniverse fc NullType
415 <|> do (c, cfc) <- constant
416 fc <- getFC
417 return (modifyConst syn fc (PConstant cfc c))
418 <|> do symbol "'"; fc <- getFC; str <- fst <$> name
419 return (PApp fc (PRef fc [] (sUN "Symbol_"))
420 [pexp (PConstant NoFC (Str (show str)))])
421 <|> do (x, fc) <- fnName
422 if inPattern syn
423 then P.option (PRef fc [fc] x)
424 (do reservedOp "@"
425 s <- simpleExpr syn
426 fcIn <- getFC
427 return (PAs fcIn x s))
428 else return (PRef fc [fc] x)
429 <|> idiom syn
430 <|> listExpr syn
431 <|> alt syn
432 <|> do reservedOp "!"
433 s <- simpleExpr syn
434 fc <- getFC
435 return (PAppBind fc s [])
436 <|> bracketed (disallowImp syn)
437 <|> quasiquote syn
438 <|> namequote syn
439 <|> unquote syn
440 <|> do lchar '_'; return Placeholder
441 <?> "expression"
443{- |Parses an expression in parentheses
445Bracketed ::= '(' Bracketed'
447 -}
448bracketed :: SyntaxInfo -> IdrisParser PTerm
449bracketed syn = do (FC fn (sl, sc) _) <- getFC
450 lchar '(' <?> "parenthesized expression"
451 bracketed' (FC fn (sl, sc) (sl, sc+1)) (syn { withAppAllowed = True })
453{- |Parses the rest of an expression in braces
455Bracketed' ::=
456 ')'
457 | Expr ')'
458 | ExprList ')'
459 | DependentPair ')'
460 | Operator Expr ')'
461 | Expr Operator ')'
462 ;
464-}
465bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm
466bracketed' open syn =
467 do (FC f start (l, c)) <- getFC
468 lchar ')'
469 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
470 <|> P.try (dependentPair TypeOrTerm [] open syn)
471 <|> P.try (do (opName, fc) <- operatorName
472 guardNotPrefix opName
474 e <- expr syn
475 lchar ')'
476 return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
477 (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),
478 pexp e]))
479 <|> P.try (simpleExpr syn >>= \l ->
480 P.try (do (opName, _) <- operatorName
481 lchar ')'
482 fc <- getFC
483 return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
484 (PApp fc (PRef fc [] opName) [pexp l,
485 pexp (PRef fc [] (sMN 1000 "ARG"))]))
486 <|> bracketedExpr syn open l)
487 <|> do l <- expr (allowConstr syn)
488 bracketedExpr (allowConstr syn) open l
489 where
490 justPrefix :: FixDecl -> Maybe Name
491 justPrefix (Fix (PrefixN _) opName) = Just (sUN opName)
492 justPrefix _ = Nothing
494 guardNotPrefix :: Name -> IdrisParser ()
495 guardNotPrefix opName = do
496 guard $ opName /= sUN "-"
497 guard $ opName /= sUN "!"
499 ops <- idris_infixes <$> get
500 guard . not . (opName `elem`) . mapMaybe justPrefix $ ops
502{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
503dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
504dependentPair pun prev openFC syn =
505 if null prev then
506 nametypePart <|> namePart
507 else
508 case pun of
509 IsType -> nametypePart <|> namePart <|> exprPart True
510 IsTerm -> exprPart False
511 TypeOrTerm -> nametypePart <|> namePart <|> exprPart False
512 where nametypePart = do
513 (ln, lnfc, colonFC) <- P.try $ do
514 (ln, lnfc) <- name
515 colonFC <- lcharFC ':'
516 return (ln, lnfc, colonFC)
517 lty <- expr' syn
518 starsFC <- reservedOpFC "**"
519 dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn
520 namePart = P.try $ do
521 (ln, lnfc) <- name
522 starsFC <- reservedOpFC "**"
523 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
524 exprPart isEnd = do
525 e <- expr syn
526 sepFCE <-
527 let stars = (Left <$> reservedOpFC "**")
528 ending = (Right <$> lcharFC ')')
529 in if isEnd then ending else stars <|> ending
530 case sepFCE of
531 Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
532 Right closeFC ->
533 return (mkPDPairs pun openFC closeFC (reverse prev) e)
534 mkPDPairs pun openFC closeFC ((e, cfclty, starsFC):bnds) r =
535 (PDPair openFC ([openFC] ++ maybe [] ((: []) . fst) cfclty ++ [starsFC, closeFC] ++ (=<<) (\(_,cfclty,sfc) -> maybe [] ((: []) . fst) cfclty ++ [sfc]) bnds)
536 pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))
537 mergePDPairs pun starsFC' [] r = r
538 mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =
539 PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)
541-- | Parse the contents of parentheses, after an expression has been parsed.
542bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
543bracketedExpr syn openParenFC e =
544 do lchar ')'; return e
545 <|> do exprs <- some (do comma <- lcharFC ','
546 r <- expr syn
547 return (r, comma))
548 closeParenFC <- lcharFC ')'
549 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
550 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
551 <|> do starsFC <- reservedOpFC "**"
552 dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn
553 <?> "end of bracketed expression"
554 where mergePairs :: [(PTerm, FC)] -> PTerm
555 mergePairs [(t, fc)] = t
556 mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)
558-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
559-- big integer, otherwise try fromInteger and the constants as alternatives.
560-- a better solution would be to fix fromInteger to work with Integer, as the
561-- name suggests, rather than Int
562{-| Finds optimal type for integer constant -}
563modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
564modifyConst syn fc (PConstant inFC (BI x))
565 | not (inPattern syn)
566 = PConstSugar inFC $ -- wrap in original location for highlighting
567 PAlternative [] FirstSuccess
568 (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]
569 : consts)
570 | otherwise = PConstSugar inFC $
571 PAlternative [] FirstSuccess consts
572 where
573 consts = [ PConstant inFC (BI x)
574 , PConstant inFC (I (fromInteger x))
575 , PConstant inFC (B8 (fromInteger x))
576 , PConstant inFC (B16 (fromInteger x))
577 , PConstant inFC (B32 (fromInteger x))
578 , PConstant inFC (B64 (fromInteger x))
579 ]
580modifyConst syn fc x = x
582{- | Parses an alternative expression
584 Alt ::= '(|' Expr_List '|)';
586 Expr_List ::=
587 Expr'
588 | Expr' ',' Expr_List
589 ;
591-}
592alt :: SyntaxInfo -> IdrisParser PTerm
593alt syn = do symbol "(|"; alts <- P.sepBy1 (expr' (syn { withAppAllowed = False })) (lchar ','); symbol "|)"
594 return (PAlternative [] FirstSuccess alts)
596{- | Parses a possibly hidden simple expression
598HSimpleExpr ::=
599 '.' SimpleExpr
600 | SimpleExpr
601 ;
603-}
604hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
605hsimpleExpr syn =
606 do lchar '.'
607 e <- simpleExpr syn
608 return $ PHidden e
609 <|> simpleExpr syn
610 <?> "expression"
612{- | Parses a unification log expression
613UnifyLog ::=
614 '%' 'unifyLog' SimpleExpr
615 ;
616-}
617unifyLog :: SyntaxInfo -> IdrisParser PTerm
618unifyLog syn = do (FC fn (sl, sc) kwEnd) <- P.try (lchar '%' *> reservedFC "unifyLog")
619 tm <- simpleExpr syn
620 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
621 return (PUnifyLog tm)
622 <?> "unification log expression"
624{- | Parses a new-style tactics expression
625RunTactics ::=
626 '%' 'runElab' SimpleExpr
627 ;
628-}
629runElab :: SyntaxInfo -> IdrisParser PTerm
630runElab syn = do (FC fn (sl, sc) kwEnd) <- P.try (lchar '%' *> reservedFC "runElab")
631 fc <- getFC
632 tm <- simpleExpr syn
633 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
634 return $ PRunElab fc tm (syn_namespace syn)
635 <?> "new-style tactics expression"
637{- | Parses a disambiguation expression
638Disamb ::=
639 'with' NameList Expr
640 ;
641-}
642disamb :: SyntaxInfo -> IdrisParser PTerm
643disamb syn = do kw <- reservedFC "with"
644 ns <- P.sepBy1 (fst <$> name) (lchar ',')
645 tm <- expr' syn
646 highlightP kw AnnKeyword
647 return (PDisamb (map tons ns) tm)
648 <?> "namespace disambiguation expression"
649 where tons (NS n s) = txt (show n) : s
650 tons n = [txt (show n)]
651{- | Parses a no implicits expression
653NoImplicits ::=
654 '%' 'noImplicits' SimpleExpr
655 ;
657-}
658noImplicits :: SyntaxInfo -> IdrisParser PTerm
659noImplicits syn = do P.try (lchar '%' *> reserved "noImplicits")
660 tm <- simpleExpr syn
661 return (PNoImplicits tm)
662 <?> "no implicits expression"
664{- | Parses a function application expression
666App ::=
667 'mkForeign' Arg Arg*
668 | MatchApp
669 | SimpleExpr Arg*
670 ;
671MatchApp ::=
672 SimpleExpr '<==' FnName
673 ;
675-}
676app :: SyntaxInfo -> IdrisParser PTerm
677app syn = do f <- simpleExpr syn
678 (do P.try $ reservedOp "<=="
679 fc <- getFC
680 ff <- fst <$> fnName
681 return (PLet fc RigW (sMN 0 "match") NoFC
682 f
683 (PMatchApp fc ff)
684 (PRef fc [] (sMN 0 "match")))
685 <?> "matching application expression") <|>
686 (do fc <- getFC
687 i <- get
688 args <- many (do notEndApp; arg syn)
689 wargs <- if withAppAllowed syn && not (inPattern syn)
690 then many (do notEndApp; reservedOp "|"; expr' syn)
691 else return []
692 case args of
693 [] -> return f
694 _ -> return (withApp fc (flattenFromInt fc f args) wargs))
695 <?> "function application"
696 where
697 -- bit of a hack to deal with the situation where we're applying a
698 -- literal to an argument, which we may want for obscure applications
699 -- of fromInteger, and this will help disambiguate better.
700 -- We know, at least, it won't be one of the constants!
701 flattenFromInt fc (PAlternative _ x alts) args
702 | Just i <- getFromInt alts
703 = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)
704 flattenFromInt fc f args = PApp fc f args
706 withApp fc tm [] = tm
707 withApp fc tm (a : as) = withApp fc (PWithApp fc tm a) as
709 getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a
710 getFromInt (_ : xs) = getFromInt xs
711 getFromInt _ = Nothing
713{-| Parses a function argument
715Arg ::=
716 ImplicitArg
717 | ConstraintArg
718 | SimpleExpr
719 ;
721-}
722arg :: SyntaxInfo -> IdrisParser PArg
723arg syn = implicitArg syn
724 <|> constraintArg syn
725 <|> do e <- simpleExpr syn
726 return (pexp e)
727 <?> "function argument"
729{-| Parses an implicit function argument
731ImplicitArg ::=
732 '{' Name ('=' Expr)? '}'
733 ;
735-}
736implicitArg :: SyntaxInfo -> IdrisParser PArg
737implicitArg syn = do lchar '{'
738 (n, nfc) <- name
739 fc <- getFC
740 v <- P.option (PRef nfc [nfc] n) (do lchar '='
741 expr syn)
742 lchar '}'
743 return (pimp n v True)
744 <?> "implicit function argument"
746{-| Parses a constraint argument (for selecting a named interface implementation)
748> ConstraintArg ::=
749> '@{' Expr '}'
750> ;
752-}
753constraintArg :: SyntaxInfo -> IdrisParser PArg
754constraintArg syn = do symbol "@{"
755 e <- expr syn
756 symbol "}"
757 return (pconst e)
758 <?> "constraint argument"
760{-| Parses a quasiquote expression (for building reflected terms using the elaborator)
762> Quasiquote ::= '`(' Expr ')'
764-}
765quasiquote :: SyntaxInfo -> IdrisParser PTerm
766quasiquote syn = do startFC <- symbolFC "`("
767 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,
768 inPattern = False }
769 g <- optional $
770 do fc <- symbolFC ":"
771 ty <- expr syn { inPattern = False } -- don't allow antiquotes
772 return (ty, fc)
773 endFC <- symbolFC ")"
774 mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]
775 case g of
776 Just (_, fc) -> highlightP fc AnnKeyword
777 _ -> return ()
778 return $ PQuasiquote e (fst <$> g)
779 <?> "quasiquotation"
781{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)
783> Unquote ::= ',' Expr
785-}
786unquote :: SyntaxInfo -> IdrisParser PTerm
787unquote syn = do guard (syn_in_quasiquote syn > 0)
788 startFC <- symbolFC "~"
789 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
790 endFC <- getFC
791 highlightP startFC AnnKeyword
792 highlightP (spanFC startFC endFC) AnnAntiquote
793 return $ PUnquote e
794 <?> "unquotation"
796{-| Parses a quotation of a name (for using the elaborator to resolve boring details)
798> NameQuote ::= '`{' Name '}'
800-}
801namequote :: SyntaxInfo -> IdrisParser PTerm
802namequote syn = do (startFC, res) <-
803 P.try (do fc <- symbolFC "`{{"
804 return (fc, False)) <|>
805 (do fc <- symbolFC "`{"
806 return (fc, True))
807 (n, nfc) <- fnName
808 endFC <- if res then symbolFC "}" else symbolFC "}}"
809 mapM_ (uncurry highlightP)
810 [ (startFC, AnnKeyword)
811 , (endFC, AnnKeyword)
812 , (spanFC startFC endFC, AnnQuasiquote)
813 ]
814 return $ PQuoteName n res nfc
815 <?> "quoted name"
818{-| Parses a record field setter expression
820RecordType ::=
821 'record' '{' FieldTypeList '}';
824FieldTypeList ::=
825 FieldType
826 | FieldType ',' FieldTypeList
827 ;
830FieldType ::=
831 FnName '=' Expr
832 ;
834-}
836data SetOrUpdate = FieldSet PTerm | FieldUpdate PTerm
838recordType :: SyntaxInfo -> IdrisParser PTerm
839recordType syn =
840 do kw <- reservedFC "record"
841 lchar '{'
842 fgs <- fieldGetOrSet
843 lchar '}'
844 fc <- getFC
845 rec <- optional (do notEndApp; simpleExpr syn)
846 highlightP kw AnnKeyword
847 case fgs of
848 Left fields ->
849 case rec of
850 Nothing ->
851 return (PLam fc (sMN 0 "fldx") NoFC Placeholder
852 (applyAll fc fields (PRef fc [] (sMN 0 "fldx"))))
853 Just v -> return (applyAll fc fields v)
854 Right fields ->
855 case rec of
856 Nothing ->
857 return (PLam fc (sMN 0 "fldx") NoFC Placeholder
858 (getAll fc (reverse fields)
859 (PRef fc [] (sMN 0 "fldx"))))
860 Just v -> return (getAll fc (reverse fields) v)
862 <?> "record setting expression"
863 where fieldSet :: IdrisParser ([Name], SetOrUpdate)
864 fieldSet = do ns <- fieldGet
865 (do lchar '='
866 e <- expr syn
867 return (ns, FieldSet e))
868 <|> do symbol "$="
869 e <- expr syn
870 return (ns, FieldUpdate e)
871 <?> "field setter"
873 fieldGet :: IdrisParser [Name]
874 fieldGet = P.sepBy1 (fst <$> fnName) (symbol "->")
876 fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
877 fieldGetOrSet = P.try (Left <$> P.sepBy1 fieldSet (lchar ','))
878 <|> do f <- fieldGet
879 return (Right f)
881 applyAll :: FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
882 applyAll fc [] x = x
883 applyAll fc ((ns, e) : es) x
884 = applyAll fc es (doUpdate fc ns e x)
886 doUpdate fc ns (FieldUpdate e) get
887 = let get' = getAll fc (reverse ns) get in
888 doUpdate fc ns (FieldSet (PApp fc e [pexp get'])) get
889 doUpdate fc [n] (FieldSet e) get
890 = PApp fc (PRef fc [] (mkType n)) [pexp e, pexp get]
891 doUpdate fc (n : ns) e get
892 = PApp fc (PRef fc [] (mkType n))
893 [pexp (doUpdate fc ns e (PApp fc (PRef fc [] n) [pexp get])),
894 pexp get]
896 getAll :: FC -> [Name] -> PTerm -> PTerm
897 getAll fc [n] e = PApp fc (PRef fc [] n) [pexp e]
898 getAll fc (n:ns) e = PApp fc (PRef fc [] n) [pexp (getAll fc ns e)]
901-- | Creates setters for record types on necessary functions
902mkType :: Name -> Name
903mkType (UN n) = sUN ("set_" ++ str n)
904mkType (MN 0 n) = sMN 0 ("set_" ++ str n)
905mkType (NS n s) = NS (mkType n) s
907{- | Parses a type signature
909TypeSig ::=
910 ':' Expr
911 ;
914TypeExpr ::= ConstraintList? Expr;
916 -}
917typeExpr :: SyntaxInfo -> IdrisParser PTerm
918typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
919 sc <- expr (allowConstr syn)
920 return (bindList (\r -> PPi (constraint { pcount = r })) cs sc)
921 <?> "type signature"
923{- | Parses a lambda expression
925Lambda ::=
926 '\\' TypeOptDeclList LambdaTail
927 | '\\' SimpleExprList LambdaTail
928 ;
931SimpleExprList ::=
932 SimpleExpr
933 | SimpleExpr ',' SimpleExprList
934 ;
937LambdaTail ::=
938 Impossible
939 | '=>' Expr
941-}
942lambda :: SyntaxInfo -> IdrisParser PTerm
943lambda syn = do lchar '\\' <?> "lambda expression"
944 ((do xt <- P.try $ tyOptDeclList (disallowImp syn)
945 fc <- getFC
946 sc <- lambdaTail
947 return (bindList (\r -> PLam fc) xt sc))
948 <|>
949 (do ps <- P.sepBy (do fc <- getFC
950 e <- simpleExpr (disallowImp (syn { inPattern = True }))
951 return (fc, e))
952 (lchar ',')
953 sc <- lambdaTail
954 return (pmList (zip [0..] ps) sc)))
955 <?> "lambda expression"
956 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
957 pmList [] sc = sc
958 pmList ((i, (fc, x)) : xs) sc
959 = PLam fc (sMN i "lamp") NoFC Placeholder
960 (PCase fc (PRef fc [] (sMN i "lamp"))
961 [(x, pmList xs sc)])
962 lambdaTail :: IdrisParser PTerm
963 lambdaTail = impossible <|> symbol "=>" *> expr syn
965{- | Parses a term rewrite expression
967RewriteTerm ::=
968 'rewrite' Expr ('==>' Expr)? 'in' Expr
969 ;
971-}
972rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
973rewriteTerm syn = do kw <- reservedFC "rewrite"
974 fc <- getFC
975 prf <- expr syn
976 giving <- optional (do symbol "==>"; expr' syn)
977 using <- optional (do reserved "using"
978 (n, _) <- name
979 return n)
980 kw' <- reservedFC "in"; sc <- expr syn
981 highlightP kw AnnKeyword
982 highlightP kw' AnnKeyword
983 return (PRewrite fc using prf sc giving)
984 <?> "term rewrite expression"
986{- |Parses a let binding
988Let ::=
989 'let' Name TypeSig'? '=' Expr 'in' Expr
990| 'let' Expr' '=' Expr' 'in' Expr
992TypeSig' ::=
993 ':' Expr'
994 ;
996 -}
997let_ :: SyntaxInfo -> IdrisParser PTerm
998let_ syn = P.try (do kw <- reservedFC "let"
999 ls <- indentedBlock (let_binding syn)
1000 kw' <- reservedFC "in"; sc <- expr syn
1001 highlightP kw AnnKeyword; highlightP kw' AnnKeyword
1002 return (buildLets ls sc))
1003 <?> "let binding"
1004 where buildLets [] sc = sc
1005 buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc
1006 = PLet fc RigW n nfc ty v (buildLets ls sc)
1007 buildLets ((fc, pat, ty, v, alts) : ls) sc
1008 = PCase fc v ((pat, buildLets ls sc) : alts)
1010let_binding syn = do fc <- getFC;
1011 pat <- expr' (syn { inPattern = True })
1012 ty <- P.option Placeholder (do lchar ':'; expr' syn)
1013 lchar '='
1014 v <- expr (syn { withAppAllowed = isVar pat })
1015 ts <- P.option [] (do lchar '|'
1016 P.sepBy1 (do_alt syn) (lchar '|'))
1017 return (fc,pat,ty,v,ts)
1018 where isVar (PRef _ _ _) = True
1019 isVar _ = False
1021{- | Parses a conditional expression
1023If ::= 'if' Expr 'then' Expr 'else' Expr
1027if_ :: SyntaxInfo -> IdrisParser PTerm
1028if_ syn = (do ifFC <- reservedFC "if"
1029 fc <- getFC
1030 c <- expr syn
1031 thenFC <- reservedFC "then"
1032 t <- expr syn
1033 elseFC <- reservedFC "else"
1034 f <- expr syn
1035 mapM_ (flip highlightP AnnKeyword) [ifFC, thenFC, elseFC]
1036 return (PIfThenElse fc c t f))
1037 <?> "conditional expression"
1040{- | Parses a quote goal
1043QuoteGoal ::=
1044 'quoteGoal' Name 'by' Expr 'in' Expr
1047 -}
1048quoteGoal :: SyntaxInfo -> IdrisParser PTerm
1049quoteGoal syn = do kw1 <- reservedFC "quoteGoal"; n <- fst <$> name;
1050 kw2 <- reservedFC "by"
1051 r <- expr syn
1052 kw3 <- reservedFC "in"
1053 fc <- getFC
1054 sc <- expr syn
1055 mapM_ (flip highlightP AnnKeyword) [kw1, kw2, kw3]
1056 return (PGoal fc r n sc)
1057 <?> "quote goal expression"
1059{- | Parses a dependent type signature
1062Pi ::= PiOpts Static? Pi'
1066Pi' ::=
1067 OpExpr ('->' Pi)?
1068 | '(' TypeDeclList ')' '->' Pi
1069 | '{' TypeDeclList '}' '->' Pi
1070 | '{' 'auto' TypeDeclList '}' '->' Pi
1071 | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi
1074 -}
1076bindsymbol opts st syn
1077 = do symbol "->"
1078 return (Exp opts st False RigW)
1080explicitPi opts st syn
1081 = do xt <- P.try (lchar '(' *> typeDeclList syn <* lchar ')')
1082 binder <- bindsymbol opts st syn
1083 sc <- expr (allowConstr syn)
1084 return (bindList (\r -> PPi (binder { pcount = r })) xt sc)
1086autoImplicit opts st syn
1087 = do kw <- reservedFC "auto"
1088 when (st == Static) $ fail "auto implicits can not be static"
1089 xt <- typeDeclList syn
1090 lchar '}'
1091 symbol "->"
1092 sc <- expr (allowConstr syn)
1093 highlightP kw AnnKeyword
1094 return (bindList (\r -> PPi
1095 (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]) r)) xt sc)
1097defaultImplicit opts st syn = do
1098 kw <- reservedFC "default"
1099 when (st == Static) $ fail "default implicits can not be static"
1100 ist <- get
1101 script' <- simpleExpr syn
1102 let script = debindApp syn . desugar syn ist $ script'
1103 xt <- typeDeclList syn
1104 lchar '}'
1105 symbol "->"
1106 sc <- expr (allowConstr syn)
1107 highlightP kw AnnKeyword
1108 return (bindList (\r -> PPi (TacImp [] Dynamic script r)) xt sc)
1110normalImplicit opts st syn = do
1111 xt <- typeDeclList syn <* lchar '}'
1112 symbol "->"
1113 cs <- constraintList syn
1114 sc <- expr syn
1115 let (im,cl)
1116 = if implicitAllowed syn
1117 then (Imp opts st False (Just (Impl False True False)) True RigW,
1118 constraint)
1119 else (Imp opts st False (Just (Impl False False False)) True RigW,
1120 Imp opts st False (Just (Impl True False False)) True RigW)
1121 return (bindList (\r -> PPi (im { pcount = r })) xt
1122 (bindList (\r -> PPi (cl { pcount = r })) cs sc))
1124constraintPi opts st syn =
1125 do cs <- constraintList1 syn
1126 sc <- expr syn
1127 if implicitAllowed syn
1128 then return (bindList (\r -> PPi constraint { pcount = r }) cs sc)
1129 else return (bindList (\r -> PPi (Imp opts st False (Just (Impl True False False)) True r))
1130 cs sc)
1132implicitPi opts st syn =
1133 autoImplicit opts st syn
1134 <|> defaultImplicit opts st syn
1135 <|> normalImplicit opts st syn
1137unboundPi opts st syn = do
1138 x <- opExpr syn
1139 (do binder <- bindsymbol opts st syn
1140 sc <- expr syn
1141 return (PPi binder (sUN "__pi_arg") NoFC x sc))
1142 <|> return x
1144-- This is used when we need to disambiguate from a constraint list
1145unboundPiNoConstraint opts st syn = do
1146 x <- opExpr syn
1147 (do binder <- bindsymbol opts st syn
1148 sc <- expr syn
1149 P.notFollowedBy $ reservedOp "=>"
1150 return (PPi binder (sUN "__pi_arg") NoFC x sc))
1151 <|> do P.notFollowedBy $ reservedOp "=>"
1152 return x
1155pi :: SyntaxInfo -> IdrisParser PTerm
1156pi syn =
1157 do opts <- piOpts syn
1158 st <- static
1159 explicitPi opts st syn
1160 <|> P.try (do lchar '{'; implicitPi opts st syn)
1161 <|> if constraintAllowed syn
1162 then P.try (unboundPiNoConstraint opts st syn)
1163 <|> constraintPi opts st syn
1164 else unboundPi opts st syn
1165 <?> "dependent type signature"
1167{- | Parses Possible Options for Pi Expressions
1169 PiOpts ::= '.'?
1172piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
1173piOpts syn | implicitAllowed syn =
1174 lchar '.' *> return [InaccessibleArg]
1175 <|> return []
1176piOpts syn = return []
1178{- | Parses a type constraint list
1181ConstraintList ::=
1182 '(' Expr_List ')' '=>'
1183 | Expr '=>'
1187constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1188constraintList syn = P.try (constraintList1 syn)
1189 <|> return []
1191constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1192constraintList1 syn = P.try (do lchar '('
1193 tys <- P.sepBy1 nexpr (lchar ',')
1194 lchar ')'
1195 reservedOp "=>"
1196 return tys)
1197 <|> P.try (do t <- opExpr (disallowImp syn)
1198 reservedOp "=>"
1199 return [(RigW, defname, NoFC, t)])
1200 <?> "type constraint list"
1201 where nexpr = P.try (do (n, fc) <- name; lchar ':'
1202 e <- expr (disallowImp syn)
1203 return (RigW, n, fc, e))
1204 <|> do e <- expr (disallowImp syn)
1205 return (RigW, defname, NoFC, e)
1206 defname = sMN 0 "constraint"
1208{- | Parses a type declaration list
1210TypeDeclList ::=
1211 FunctionSignatureList
1212 | NameList TypeSig
1217FunctionSignatureList ::=
1218 Name TypeSig
1219 | Name TypeSig ',' FunctionSignatureList
1223typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1224typeDeclList syn = P.try (P.sepBy1 (do rig <- P.option RigW rigCount
1225 (x, xfc) <- fnName
1226 lchar ':'
1227 t <- typeExpr (disallowImp syn)
1228 return (rig, x, xfc, t))
1229 (lchar ','))
1230 <|> do ns <- P.sepBy1 name (lchar ',')
1231 lchar ':'
1232 t <- typeExpr (disallowImp syn)
1233 return (map (\(x, xfc) -> (RigW, x, xfc, t)) ns)
1234 <?> "type declaration list"
1235 where
1236 rigCount = do lchar '1'; return Rig1
1237 <|> do lchar '0'; return Rig0
1239{- | Parses a type declaration list with optional parameters
1241TypeOptDeclList ::=
1242 NameOrPlaceholder TypeSig?
1243 | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
1248NameOrPlaceHolder ::= Name | '_';
1251tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1252tyOptDeclList syn = P.sepBy1 (do (x, fc) <- nameOrPlaceholder
1253 t <- P.option Placeholder (do lchar ':'
1254 expr syn)
1255 return (RigW, x, fc, t))
1256 (lchar ',')
1257 <?> "type declaration list"
1258 where nameOrPlaceholder :: IdrisParser (Name, FC)
1259 nameOrPlaceholder = fnName
1260 <|> do symbol "_"
1261 return (sMN 0 "underscore", NoFC)
1262 <?> "name or placeholder"
1264{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]
1266ListExpr ::=
1267 '[' ']'
1268 | '[' Expr '|' DoList ']'
1269 | '[' ExprList ']'
1273DoList ::=
1274 Do
1275 | Do ',' DoList
1279ExprList ::=
1280 Expr
1281 | Expr ',' ExprList
1284 -}
1285listExpr :: SyntaxInfo -> IdrisParser PTerm
1286listExpr syn = do (FC f (l, c) _) <- getFC
1287 lchar '['; fc <- getFC;
1288 (P.try . Tok.token $ do (char ']' <?> "end of list expression")
1289 (FC _ _ (l', c')) <- getFC
1290 return (mkNil (FC f (l, c) (l', c'))))
1291 <|> (do x <- expr (syn { withAppAllowed = False }) <?> "expression"
1292 (do P.try (lchar '|') <?> "list comprehension"
1293 qs <- P.sepBy1 (do_ syn) (lchar ',')
1294 lchar ']'
1295 return (PDoBlock (map addGuard qs ++
1296 [DoExp fc (PApp fc (PRef fc [] (sUN "pure"))
1297 [pexp x])]))) <|>
1298 (do xs <- many (do (FC fn (sl, sc) _) <- getFC
1299 lchar ',' <?> "list element"
1300 let commaFC = FC fn (sl, sc) (sl, sc + 1)
1301 elt <- expr syn
1302 return (elt, commaFC))
1303 (FC fn (sl, sc) _) <- getFC
1304 lchar ']' <?> "end of list expression"
1305 let rbrackFC = FC fn (sl, sc) (sl, sc+1)
1306 return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))
1307 <?> "list expression"
1308 where
1309 mkNil :: FC -> PTerm
1310 mkNil fc = PRef fc [fc] (sUN "Nil")
1311 mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm
1312 mkList errFC nilFC [] = PRef nilFC [nilFC] (sUN "Nil")
1313 mkList errFC nilFC ((x, fc) : xs) = PApp errFC (PRef fc [fc] (sUN "::")) [pexp x, pexp (mkList errFC nilFC xs)]
1314 addGuard :: PDo -> PDo
1315 addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc [] (sUN "guard"))
1316 [pexp e])
1317 addGuard x = x
1319{- | Parses a do-block
1321Do' ::= Do KeepTerminator;
1325DoBlock ::=
1326 'do' OpenBlock Do'+ CloseBlock
1329 -}
1330doBlock :: SyntaxInfo -> IdrisParser PTerm
1331doBlock syn
1332 = do kw <- reservedFC "do"
1333 ds <- indentedBlock1 (do_ syn)
1334 highlightP kw AnnKeyword
1335 return (PDoBlock ds)
1336 <?> "do block"
1338{- | Parses an expression inside a do block
1340Do ::=
1341 'let' Name TypeSig'? '=' Expr
1342 | 'let' Expr' '=' Expr
1343 | 'rewrite Expr
1344 | Name '<-' Expr
1345 | Expr' '<-' Expr
1346 | Expr
1350do_ :: SyntaxInfo -> IdrisParser PDo
1351do_ syn
1352 = P.try (do kw <- reservedFC "let"
1353 (i, ifc) <- name
1354 ty <- P.option Placeholder (do lchar ':'
1355 expr' syn)
1356 reservedOp "="
1357 fc <- getFC
1358 e <- expr syn
1359 highlightP kw AnnKeyword
1360 return (DoLet fc RigW i ifc ty e))
1361 <|> P.try (do kw <- reservedFC "let"
1362 i <- expr' syn
1363 reservedOp "="
1364 fc <- getFC
1365 sc <- expr syn
1366 highlightP kw AnnKeyword
1367 return (DoLetP fc i sc))
1368 <|> P.try (do kw <- reservedFC "rewrite"
1369 fc <- getFC
1370 sc <- expr syn
1371 highlightP kw AnnKeyword
1372 return (DoRewrite fc sc))
1373 <|> P.try (do (i, ifc) <- name
1374 symbol "<-"
1375 fc <- getFC
1376 e <- expr (syn { withAppAllowed = False });
1377 P.option (DoBind fc i ifc e)
1378 (do lchar '|'
1379 ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
1380 return (DoBindP fc (PRef ifc [ifc] i) e ts)))
1381 <|> P.try (do i <- expr' syn
1382 symbol "<-"
1383 fc <- getFC
1384 e <- expr (syn { withAppAllowed = False });
1385 P.option (DoBindP fc i e [])
1386 (do lchar '|'
1387 ts <- P.sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
1388 return (DoBindP fc i e ts)))
1389 <|> do e <- expr syn
1390 fc <- getFC
1391 return (DoExp fc e)
1392 <?> "do block expression"
1394do_alt syn = do l <- expr' syn
1395 P.option (Placeholder, l)
1396 (do symbol "=>"
1397 r <- expr' syn
1398 return (l, r))
1400{- | Parses an expression in idiom brackets
1402Idiom ::= '[|' Expr '|]';
1405idiom :: SyntaxInfo -> IdrisParser PTerm
1406idiom syn
1407 = do symbol "[|"
1408 fc <- getFC
1409 e <- expr (syn { withAppAllowed = False })
1410 symbol "|]"
1411 return (PIdiom fc e)
1412 <?> "expression in idiom brackets"
1414{- |Parses a constant or literal expression
1417Constant ::=
1418 'Integer'
1419 | 'Int'
1420 | 'Char'
1421 | 'Double'
1422 | 'String'
1423 | 'Bits8'
1424 | 'Bits16'
1425 | 'Bits32'
1426 | 'Bits64'
1427 | Float_t
1428 | Natural_t
1429 | VerbatimString_t
1430 | String_t
1431 | Char_t
1436constants :: [(String, Idris.Core.TT.Const)]
1437constants =
1438 [ ("Integer", AType (ATInt ITBig))
1439 , ("Int", AType (ATInt ITNative))
1440 , ("Char", AType (ATInt ITChar))
1441 , ("Double", AType ATFloat)
1442 , ("String", StrType)
1443 , ("prim__WorldType", WorldType)
1444 , ("prim__TheWorld", TheWorld)
1445 , ("Bits8", AType (ATInt (ITFixed IT8)))
1446 , ("Bits16", AType (ATInt (ITFixed IT16)))
1447 , ("Bits32", AType (ATInt (ITFixed IT32)))
1448 , ("Bits64", AType (ATInt (ITFixed IT64)))
1451-- | Parse a constant and its source span
1452constant :: IdrisParser (Idris.Core.TT.Const, FC)
1453constant = P.choice [ do fc <- reservedFC name; return (ty, fc)
1454 | (name, ty) <- constants
1456 <|> do (f, fc) <- P.try float; return (Fl f, fc)
1457 <|> do (i, fc) <- natural; return (BI i, fc)
1458 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)
1459 <|> do (s, fc) <- stringLiteral; return (Str s, fc)
1460 <|> do (c, fc) <- P.try charLiteral; return (Ch c, fc) --Currently ambigous with symbols
1461 <?> "constant or literal"
1463{- | Parses a verbatim multi-line string literal (triple-quoted)
1466VerbatimString_t ::=
1467 '\"\"\"' ~'\"\"\"' '\"\"\"'
1470 -}
1471verbatimStringLiteral :: IdrisParser (String, FC)
1472verbatimStringLiteral = Tok.token $ do (FC f start _) <- getFC
1473 P.try $ string "\"\"\""
1474 str <- P.manyTill P.anyChar $ P.try (string "\"\"\"")
1475 (FC _ _ end) <- getFC
1476 return (str, FC f start end)
1478{- | Parses a static modifier
1481Static ::=
1482 '%static'
1486static :: IdrisParser Static
1487static = do reserved "%static"; return Static
1488 <|> do reserved "[static]"
1489 fc <- getFC
1490 parserWarning fc Nothing (Msg "The use of [static] is deprecated, use %static instead.")
1491 return Static
1492 <|> return Dynamic
1493 <?> "static modifier"
1495{- | Parses a tactic script
1498Tactic ::= 'intro' NameList?
1499 | 'intros'
1500 | 'refine' Name Imp+
1501 | 'mrefine' Name
1502 | 'rewrite' Expr
1503 | 'induction' Expr
1504 | 'equiv' Expr
1505 | 'let' Name ':' Expr' '=' Expr
1506 | 'let' Name '=' Expr
1507 | 'focus' Name
1508 | 'exact' Expr
1509 | 'applyTactic' Expr
1510 | 'reflect' Expr
1511 | 'fill' Expr
1512 | 'try' Tactic '|' Tactic
1513 | '{' TacticSeq '}'
1514 | 'compute'
1515 | 'trivial'
1516 | 'solve'
1517 | 'attack'
1518 | 'state'
1519 | 'term'
1520 | 'undo'
1521 | 'qed'
1522 | 'abandon'
1523 | ':' 'q'
1526Imp ::= '?' | '_';
1528TacticSeq ::=
1529 Tactic ';' Tactic
1530 | Tactic ';' TacticSeq
1535-- | A specification of the arguments that tactics can take
1536data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
1537 | ExprTArg
1538 | AltsTArg
1539 | StringLitTArg
1541-- The FIXMEs are Issue #1766 in the issue tracker.
1542-- https://github.com/idris-lang/Idris-dev/issues/1766
1543-- | A list of available tactics and their argument requirements
1544tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
1545tactics =
1546 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)
1547 do ns <- P.sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)
1548 , noArgs ["intros"] Intros
1549 , noArgs ["unfocus"] Unfocus
1550 , (["refine"], Just ExprTArg, const $
1551 do n <- spaced (fst <$> fnName)
1552 imps <- many imp
1553 return $ Refine n imps)
1554 , (["claim"], Nothing, \syn ->
1555 do n <- indentGt *> (fst <$> name)
1556 goal <- indentGt *> expr syn
1557 return $ Claim n goal)
1558 , (["mrefine"], Just ExprTArg, const $
1559 do n <- spaced (fst <$> fnName)
1560 return $ MatchRefine n)
1561 , expressionTactic ["rewrite"] Rewrite
1562 , expressionTactic ["case"] CaseTac
1563 , expressionTactic ["induction"] Induction
1564 , expressionTactic ["equiv"] Equiv
1565 , (["let"], Nothing, \syn -> -- FIXME syntax for let
1566 do n <- (indentGt *> (fst <$> name))
1567 (do indentGt *> lchar ':'
1568 ty <- indentGt *> expr' syn
1569 indentGt *> lchar '='
1570 t <- indentGt *> expr syn
1571 i <- get
1572 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1573 <|> (do indentGt *> lchar '='
1574 t <- indentGt *> expr syn
1575 i <- get
1576 return $ LetTac n (desugar syn i t)))
1578 , (["focus"], Just ExprTArg, const $
1579 do n <- spaced (fst <$> name)
1580 return $ Focus n)
1581 , expressionTactic ["exact"] Exact
1582 , expressionTactic ["applyTactic"] ApplyTactic
1583 , expressionTactic ["byReflection"] ByReflection
1584 , expressionTactic ["reflect"] Reflect
1585 , expressionTactic ["fill"] Fill
1586 , (["try"], Just AltsTArg, \syn ->
1587 do t <- spaced (tactic syn)
1588 lchar '|'
1589 t1 <- spaced (tactic syn)
1590 return $ Try t t1)
1591 , noArgs ["compute"] Compute
1592 , noArgs ["trivial"] Trivial
1593 , noArgs ["unify"] DoUnify
1594 , (["search"], Nothing, const $
1595 do depth <- P.option 10 $ fst <$> natural
1596 return (ProofSearch True True (fromInteger depth) Nothing [] []))
1597 , noArgs ["implementation"] TCImplementation
1598 , noArgs ["solve"] Solve
1599 , noArgs ["attack"] Attack
1600 , noArgs ["state", ":state"] ProofState
1601 , noArgs ["term", ":term"] ProofTerm
1602 , noArgs ["undo", ":undo"] Undo
1603 , noArgs ["qed", ":qed"] Qed
1604 , noArgs ["abandon", ":q"] Abandon
1605 , noArgs ["skip"] Skip
1606 , noArgs ["sourceLocation"] SourceFC
1607 , expressionTactic [":e", ":eval"] TEval
1608 , expressionTactic [":t", ":type"] TCheck
1609 , expressionTactic [":search"] TSearch
1610 , (["fail"], Just StringLitTArg, const $
1611 do msg <- fst <$> stringLiteral
1612 return $ TFail [Idris.Core.TT.TextPart msg])
1613 , ([":doc"], Just ExprTArg, const $
1614 do whiteSpace
1615 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1616 P.eof
1617 return (TDocStr doc))
1619 where
1620 expressionTactic names tactic = (names, Just ExprTArg, \syn ->
1621 do t <- spaced (expr syn)
1622 i <- get
1623 return $ tactic (desugar syn i t))
1624 noArgs names tactic = (names, Nothing, const (return tactic))
1625 spaced parser = indentGt *> parser
1626 imp :: IdrisParser Bool
1627 imp = do lchar '?'; return False
1628 <|> do lchar '_'; return True
1631tactic :: SyntaxInfo -> IdrisParser PTactic
1632tactic syn = P.choice [ do P.choice (map reserved names); parser syn
1633 | (names, _, parser) <- tactics ]
1634 <|> do lchar '{'
1635 t <- tactic syn;
1636 lchar ';';
1637 ts <- P.sepBy1 (tactic syn) (lchar ';')
1638 lchar '}'
1639 return $ TSeq t (mergeSeq ts)
1640 <|> ((lchar ':' >> empty) <?> "prover command")
1641 <?> "tactic"
1642 where
1643 mergeSeq :: [PTactic] -> PTactic
1644 mergeSeq [t] = t
1645 mergeSeq (t:ts) = TSeq t (mergeSeq ts)
1647-- | Parses a tactic as a whole
1648fullTactic :: SyntaxInfo -> IdrisParser PTactic
1649fullTactic syn = do t <- tactic syn
1650 P.eof
1651 return t