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