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