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