git.iko.soy/Idris-dev
on 008fb1f help sign in
Idris-dev/src/Idris/Parser/Expr.hs
1643 lines 57 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.Parser.Helpers
16import Idris.Parser.Ops
18import Prelude hiding (pi)
20import Control.Applicative
21import Control.Monad
22import Control.Monad.State.Strict
23import qualified Data.ByteString.UTF8 as UTF8
24import Data.Char
25import Data.Function (on)
26import qualified Data.HashSet as HS
27import Data.List
28import qualified Data.List.Split as Spl
29import Data.Maybe
30import Data.Monoid
31import qualified Data.Text as T
32import Debug.Trace
33import qualified Text.Parser.Char as Chr
34import Text.Parser.Expression
35import Text.Parser.LookAhead
36import qualified Text.Parser.Token as Tok
37import qualified Text.Parser.Token.Highlight as Hi
38import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
39 stringLiteral, symbol, whiteSpace)
40import Text.Trifecta.Delta
42-- | Allow implicit type declarations
43allowImp :: SyntaxInfo -> SyntaxInfo
44allowImp syn = syn { implicitAllowed = True,
45 constraintAllowed = False }
47-- | Disallow implicit type declarations
48disallowImp :: SyntaxInfo -> SyntaxInfo
49disallowImp syn = syn { implicitAllowed = False,
50 constraintAllowed = False }
52-- | Allow scoped constraint arguments
53allowConstr :: SyntaxInfo -> SyntaxInfo
54allowConstr syn = syn { constraintAllowed = True }
56{-| Parses an expression as a whole
58 FullExpr ::= Expr EOF_t;
60 -}
61fullExpr :: SyntaxInfo -> IdrisParser PTerm
62fullExpr syn = do x <- expr syn
63 eof
64 i <- get
65 return $ debindApp syn (desugar syn i x)
67tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
68tryFullExpr syn st input =
69 case runparser (fullExpr syn) st "" input of
70 Success tm -> Right tm
71 Failure e -> Left (Msg (show e))
73{- | Parses an expression
75 Expr ::= Pi
77 -}
78expr :: SyntaxInfo -> IdrisParser PTerm
79expr = pi
81{- | Parses an expression with possible operator applied
83 OpExpr ::= {- Expression Parser with Operators based on Expr' -};
85-}
86opExpr :: SyntaxInfo -> IdrisParser PTerm
87opExpr syn = do i <- get
88 buildExpressionParser (table (idris_infixes i))
89 (expr' syn)
91{- | Parses either an internally defined expression or
92 a user-defined one
94Expr' ::= "External (User-defined) Syntax"
95 | InternalExpr;
97 -}
98expr' :: SyntaxInfo -> IdrisParser PTerm
99expr' syn = try (externalExpr syn)
100 <|> internalExpr syn
101 <?> "expression"
103{- | Parses a user-defined expression -}
104externalExpr :: SyntaxInfo -> IdrisParser PTerm
105externalExpr syn = do i <- get
106 (FC fn start _) <- getFC
107 expr <- extensions syn (syntaxRulesList $ syntax_rules i)
108 (FC _ _ end) <- getFC
109 let outerFC = FC fn start end
110 return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)
111 <?> "user-defined expression"
112 where -- Fix non-highlighting FCs by approximating with the span of the syntax application
113 fixFC outer inner | inner `fcIn` outer = inner
114 | otherwise = outer
115 -- Fix highlighting FCs by making them useless, to avoid spurious highlights
116 fixFCH fn outer inner | inner `fcIn` outer = inner
117 | otherwise = FileFC fn
119{- | Parses a simple user-defined expression -}
120simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
121simpleExternalExpr syn = do i <- get
122 extensions syn (filter isSimple (syntaxRulesList $ syntax_rules i))
123 where
124 isSimple (Rule (Expr x:xs) _ _) = False
125 isSimple (Rule (SimpleExpr x:xs) _ _) = False
126 isSimple (Rule [Keyword _] _ _) = True
127 isSimple (Rule [Symbol _] _ _) = True
128 isSimple (Rule (_:xs) _ _) = case last xs of
129 Keyword _ -> True
130 Symbol _ -> True
131 _ -> False
132 isSimple _ = False
134{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
135extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
136extensions syn rules = extension syn [] (filter isValid rules)
137 <?> "user-defined expression"
138 where
139 isValid :: Syntax -> Bool
140 isValid (Rule _ _ AnySyntax) = True
141 isValid (Rule _ _ PatternSyntax) = inPattern syn
142 isValid (Rule _ _ TermSyntax) = not (inPattern syn)
143 isValid (DeclRule _ _) = False
145data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information
146 deriving Show
148extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
149extension syn ns rules =
150 choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->
151 case head rs of -- can never be []
152 Rule (symb:_) _ _ -> try $ do
153 n <- extensionSymbol symb
154 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]
155 -- If we have more than one Rule in this bucket, our grammar is
156 -- nondeterministic.
157 Rule [] ptm _ -> return (flatten (updateSynMatch (mapMaybe id ns) ptm))
158 where
159 ruleGroup [] [] = True
160 ruleGroup (s1:_) (s2:_) = s1 == s2
161 ruleGroup _ _ = False
163 extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
164 extensionSymbol (Keyword n) = do fc <- reservedFC (show n)
165 highlightP fc AnnKeyword
166 return Nothing
167 extensionSymbol (Expr n) = do tm <- expr syn
168 return $ Just (n, SynTm tm)
169 extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
170 return $ Just (n, SynTm tm)
171 extensionSymbol (Binding n) = do (b, fc) <- name
172 return $ Just (n, SynBind fc b)
173 extensionSymbol (Symbol s) = do fc <- symbolFC s
174 highlightP fc AnnKeyword
175 return Nothing
177 flatten :: PTerm -> PTerm -- flatten application
178 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))
179 flatten t = t
181updateSynMatch = update
182 where
183 updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
184 updateB ns (n, fc) = case lookup n ns of
185 Just (SynBind tfc t) -> (t, tfc)
186 _ -> (n, fc)
188 update :: [(Name, SynMatch)] -> PTerm -> PTerm
189 update ns (PRef fc hls n) = case lookup n ns of
190 Just (SynTm t) -> t
191 _ -> PRef fc hls n
192 update ns (PPatvar fc n) = uncurry (flip PPatvar) $ updateB ns (n, fc)
193 update ns (PLam fc n nfc ty sc)
194 = let (n', nfc') = updateB ns (n, nfc)
195 in PLam fc n' nfc' (update ns ty) (update (dropn n ns) sc)
196 update ns (PPi p n fc ty sc)
197 = let (n', nfc') = updateB ns (n, fc)
198 in PPi (updTacImp ns p) n' nfc'
199 (update ns ty) (update (dropn n ns) sc)
200 update ns (PLet fc n nfc ty val sc)
201 = let (n', nfc') = updateB ns (n, nfc)
202 in PLet fc n' nfc' (update ns ty)
203 (update ns val) (update (dropn n ns) sc)
204 update ns (PApp fc t args)
205 = PApp fc (update ns t) (map (fmap (update ns)) args)
206 update ns (PAppBind fc t args)
207 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
208 update ns (PMatchApp fc n) = let (n', nfc') = updateB ns (n, fc)
209 in PMatchApp nfc' n'
210 update ns (PIfThenElse fc c t f)
211 = PIfThenElse fc (update ns c) (update ns t) (update ns f)
212 update ns (PCase fc c opts)
213 = PCase fc (update ns c) (map (pmap (update ns)) opts)
214 update ns (PRewrite fc by eq tm mty)
215 = PRewrite fc by (update ns eq) (update ns tm) (fmap (update ns) mty)
216 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
217 update ns (PDPair fc hls p l t r)
218 = PDPair fc hls p (update ns l) (update ns t) (update ns r)
219 update ns (PAs fc n t) = PAs fc (fst $ updateB ns (n, NoFC)) (update ns t)
220 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
221 update ns (PHidden t) = PHidden (update ns t)
222 update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
223 update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds
224 where upd :: [(Name, SynMatch)] -> PDo -> PDo
225 upd ns (DoExp fc t) = DoExp fc (update ns t)
226 upd ns (DoBind fc n nfc t) = DoBind fc n nfc (update ns t)
227 upd ns (DoLet fc n nfc ty t) = DoLet fc n nfc (update ns ty) (update ns t)
228 upd ns (DoBindP fc i t ts)
229 = DoBindP fc (update ns i) (update ns t)
230 (map (\(l,r) -> (update ns l, update ns r)) ts)
231 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
232 update ns (PIdiom fc t) = PIdiom fc $ update ns t
233 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)
234 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
235 update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs
236 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
237 update ns (PUnifyLog t) = PUnifyLog $ update ns t
238 update ns (PNoImplicits t) = PNoImplicits $ update ns t
239 update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)
240 update ns (PUnquote t) = PUnquote $ update ns t
241 update ns (PQuoteName n res fc) = let (n', fc') = (updateB ns (n, fc))
242 in PQuoteName n' res fc'
243 update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp
244 update ns (PConstSugar fc t) = PConstSugar fc $ update ns t
245 -- PConstSugar probably can't contain anything substitutable, but it's hard to track
246 update ns t = t
248 updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
249 -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
250 updTactic ns (Intro ns') = Intro $ map (fst . updateB ns . (, NoFC)) ns'
251 updTactic ns (Focus n) = Focus . fst $ updateB ns (n, NoFC)
252 updTactic ns (Refine n bs) = Refine (fst $ updateB ns (n, NoFC)) bs
253 updTactic ns (Claim n t) = Claim (fst $ updateB ns (n, NoFC)) (update ns t)
254 updTactic ns (MatchRefine n) = MatchRefine (fst $ updateB ns (n, NoFC))
255 updTactic ns (LetTac n t) = LetTac (fst $ updateB ns (n, NoFC)) (update ns t)
256 updTactic ns (LetTacTy n ty tm) = LetTacTy (fst $ updateB ns (n, NoFC)) (update ns ty) (update ns tm)
257 updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth
258 (fmap (fst . updateB ns . (, NoFC)) top) (map (fst . updateB ns . (, NoFC)) psns) (map (fst . updateB ns . (, NoFC)) hints)
259 updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)
260 updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)
261 updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac
262 updTactic ns (TDocStr (Left n)) = TDocStr . Left . fst $ updateB ns (n, NoFC)
263 updTactic ns t = fmap (update ns) t
265 updTacImp ns (TacImp o st scr r) = TacImp o st (update ns scr) r
266 updTacImp _ x = x
268 dropn :: Name -> [(Name, a)] -> [(Name, a)]
269 dropn n [] = []
270 dropn n ((x,t) : xs) | n == x = xs
271 | otherwise = (x,t):dropn n xs
274{- | Parses a (normal) built-in expression
276InternalExpr ::=
277 UnifyLog
278 | RecordType
279 | SimpleExpr
280 | Lambda
281 | QuoteGoal
282 | Let
283 | If
284 | RewriteTerm
285 | CaseExpr
286 | DoBlock
287 | App
288 ;
290-}
291internalExpr :: SyntaxInfo -> IdrisParser PTerm
292internalExpr syn =
293 unifyLog syn
294 <|> runElab syn
295 <|> disamb syn
296 <|> noImplicits syn
297 <|> recordType syn
298 <|> if_ syn
299 <|> lambda syn
300 <|> quoteGoal syn
301 <|> let_ syn
302 <|> rewriteTerm syn
303 <|> doBlock syn
304 <|> caseExpr syn
305 <|> app syn
306 <?> "expression"
308{- | Parses the "impossible" keyword
310Impossible ::= 'impossible'
312-}
313impossible :: IdrisParser PTerm
314impossible = do fc <- reservedFC "impossible"
315 highlightP fc AnnKeyword
316 return PImpossible
318{- | Parses a case expression
320CaseExpr ::=
321 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
323-}
324caseExpr :: SyntaxInfo -> IdrisParser PTerm
325caseExpr syn = do kw1 <- reservedFC "case"; fc <- getFC
326 scr <- expr syn; kw2 <- reservedFC "of";
327 opts <- indentedBlock1 (caseOption syn)
328 highlightP kw1 AnnKeyword
329 highlightP kw2 AnnKeyword
330 return (PCase fc scr opts)
331 <?> "case expression"
333{- | Parses a case in a case expression
335CaseOption ::=
336 Expr (Impossible | '=>' Expr) Terminator
337 ;
339-}
340caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
341caseOption syn = do lhs <- expr (disallowImp (syn { inPattern = True }))
342 r <- impossible <|> symbol "=>" *> expr syn
343 return (lhs, r)
344 <?> "case option"
346warnTacticDeprecation :: FC -> IdrisParser ()
347warnTacticDeprecation fc =
348 parserWarning fc (Just NoOldTacticDeprecationWarnings) (Msg "This style of tactic proof is deprecated. See %runElab for the replacement.")
350{- | Parses a proof block
352ProofExpr ::=
353 'proof' OpenBlock Tactic'* CloseBlock
354 ;
356-}
357proofExpr :: SyntaxInfo -> IdrisParser PTerm
358proofExpr syn = do kw <- reservedFC "proof"
359 ts <- indentedBlock1 (tactic syn)
360 highlightP kw AnnKeyword
361 warnTacticDeprecation kw
362 return $ PProof ts
363 <?> "proof block"
365{- | Parses a tactics block
367TacticsExpr :=
368 'tactics' OpenBlock Tactic'* CloseBlock
371-}
372tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
373tacticsExpr syn = do kw <- reservedFC "tactics"
374 ts <- indentedBlock1 (tactic syn)
375 highlightP kw AnnKeyword
376 warnTacticDeprecation kw
377 return $ PTactics ts
378 <?> "tactics block"
380{- | Parses a simple expression
382SimpleExpr ::=
383 {- External (User-defined) Simple Expression -}
384 | '?' Name
385 | % 'implementation'
386 | 'Refl' ('{' Expr '}')?
387 | ProofExpr
388 | TacticsExpr
389 | FnName
390 | Idiom
391 | List
392 | Alt
393 | Bracketed
394 | Constant
395 | Type
396 | 'Void'
397 | Quasiquote
398 | NameQuote
399 | Unquote
400 | '_'
401 ;
403-}
404simpleExpr :: SyntaxInfo -> IdrisParser PTerm
405simpleExpr syn =
406 try (simpleExternalExpr syn)
407 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)
408 return (PMetavar (FC f (l, c-1) end) x)
409 <|> do lchar '%'; fc <- getFC; reserved "implementation"; return (PResolveTC fc)
410 <|> do lchar '%'; fc <- getFC; reserved "instance"
411 parserWarning fc Nothing $ Msg "The use of %instance is deprecated, use %implementation instead."
412 return (PResolveTC fc)
413 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))
414 <|> proofExpr syn
415 <|> tacticsExpr syn
416 <|> try (do fc <- reservedFC "Type*"; return $ PUniverse fc AllTypes)
417 <|> do fc <- reservedFC "AnyType"; return $ PUniverse fc AllTypes
418 <|> PType <$> reservedFC "Type"
419 <|> do fc <- reservedFC "UniqueType"; return $ PUniverse fc UniqueType
420 <|> do fc <- reservedFC "NullType"; return $ PUniverse fc NullType
421 <|> do (c, cfc) <- constant
422 fc <- getFC
423 return (modifyConst syn fc (PConstant cfc c))
424 <|> do symbol "'"; fc <- getFC; str <- fst <$> name
425 return (PApp fc (PRef fc [] (sUN "Symbol_"))
426 [pexp (PConstant NoFC (Str (show str)))])
427 <|> do (x, fc) <- fnName
428 if inPattern syn
429 then option (PRef fc [fc] x)
430 (do reservedOp "@"
431 s <- simpleExpr syn
432 fcIn <- getFC
433 return (PAs fcIn x s))
434 else return (PRef fc [fc] x)
435 <|> idiom syn
436 <|> listExpr syn
437 <|> alt syn
438 <|> do reservedOp "!"
439 s <- simpleExpr syn
440 fc <- getFC
441 return (PAppBind fc s [])
442 <|> bracketed (disallowImp syn)
443 <|> quasiquote syn
444 <|> namequote syn
445 <|> unquote syn
446 <|> do lchar '_'; return Placeholder
447 <?> "expression"
449{- |Parses an expression in parentheses
451Bracketed ::= '(' Bracketed'
453 -}
454bracketed :: SyntaxInfo -> IdrisParser PTerm
455bracketed syn = do (FC fn (sl, sc) _) <- getFC
456 lchar '(' <?> "parenthesized expression"
457 bracketed' (FC fn (sl, sc) (sl, sc+1)) (syn { withAppAllowed = True })
459{- |Parses the rest of an expression in braces
461Bracketed' ::=
462 ')'
463 | Expr ')'
464 | ExprList ')'
465 | DependentPair ')'
466 | Operator Expr ')'
467 | Expr Operator ')'
468 ;
470-}
471bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm
472bracketed' open syn =
473 do (FC f start (l, c)) <- getFC
474 lchar ')'
475 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm
476 <|> try (dependentPair TypeOrTerm [] open syn)
477 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
478 -- No prefix operators! (bit of a hack here...)
479 if (o == "-" || o == "!")
480 then fail "minus not allowed in section"
481 else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder
482 (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),
483 pexp e]))
484 <|> try (do l <- simpleExpr syn
485 op <- option Nothing (do o <- operator
486 lchar ')'
487 return (Just o))
488 fc0 <- getFC
489 case op of
490 Nothing -> bracketedExpr syn open l
491 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder
492 (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,
493 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))
494 <|> do l <- expr (allowConstr syn)
495 bracketedExpr (allowConstr syn) open l
499{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
500dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
501dependentPair pun prev openFC syn =
502 if null prev then
503 nametypePart <|> namePart
504 else
505 case pun of
506 IsType -> nametypePart <|> namePart <|> exprPart True
507 IsTerm -> exprPart False
508 TypeOrTerm -> nametypePart <|> namePart <|> exprPart False
509 where nametypePart = do
510 (ln, lnfc, colonFC) <- try $ do
511 (ln, lnfc) <- name
512 colonFC <- lcharFC ':'
513 return (ln, lnfc, colonFC)
514 lty <- expr' syn
515 starsFC <- reservedOpFC "**"
516 dependentPair IsType ((PRef lnfc [] ln, Just (colonFC, lty), starsFC):prev) openFC syn
517 namePart = try $ do
518 (ln, lnfc) <- name
519 starsFC <- reservedOpFC "**"
520 dependentPair pun ((PRef lnfc [] ln, Nothing, starsFC):prev) openFC syn
521 exprPart isEnd = do
522 e <- expr syn
523 sepFCE <-
524 let stars = (Left <$> reservedOpFC "**")
525 ending = (Right <$> lcharFC ')')
526 in if isEnd then ending else stars <|> ending
527 case sepFCE of
528 Left starsFC -> dependentPair IsTerm ((e, Nothing, starsFC):prev) openFC syn
529 Right closeFC ->
530 return (mkPDPairs pun openFC closeFC (reverse prev) e)
531 mkPDPairs pun openFC closeFC ((e, cfclty, starsFC):bnds) r =
532 (PDPair openFC ([openFC] ++ maybe [] ((: []) . fst) cfclty ++ [starsFC, closeFC] ++ (=<<) (\(_,cfclty,sfc) -> maybe [] ((: []) . fst) cfclty ++ [sfc]) bnds)
533 pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r))
534 mergePDPairs pun starsFC' [] r = r
535 mergePDPairs pun starsFC' ((e, cfclty, starsFC):bnds) r =
536 PDPair starsFC' [] pun e (maybe Placeholder snd cfclty) (mergePDPairs pun starsFC bnds r)
538-- | Parse the contents of parentheses, after an expression has been parsed.
539bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
540bracketedExpr syn openParenFC e =
541 do lchar ')'; return e
542 <|> do exprs <- some (do comma <- lcharFC ','
543 r <- expr syn
544 return (r, comma))
545 closeParenFC <- lcharFC ')'
546 let hilite = [openParenFC, closeParenFC] ++ map snd exprs
547 return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)
548 <|> do starsFC <- reservedOpFC "**"
549 dependentPair IsTerm [(e, Nothing, starsFC)] openParenFC syn
550 <?> "end of bracketed expression"
551 where mergePairs :: [(PTerm, FC)] -> PTerm
552 mergePairs [(t, fc)] = t
553 mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)
555-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
556-- big integer, otherwise try fromInteger and the constants as alternatives.
557-- a better solution would be to fix fromInteger to work with Integer, as the
558-- name suggests, rather than Int
559{-| Finds optimal type for integer constant -}
560modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
561modifyConst syn fc (PConstant inFC (BI x))
562 | not (inPattern syn)
563 = PConstSugar inFC $ -- wrap in original location for highlighting
564 PAlternative [] FirstSuccess
565 (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]
566 : consts)
567 | otherwise = PConstSugar inFC $
568 PAlternative [] FirstSuccess consts
569 where
570 consts = [ PConstant inFC (BI x)
571 , PConstant inFC (I (fromInteger x))
572 , PConstant inFC (B8 (fromInteger x))
573 , PConstant inFC (B16 (fromInteger x))
574 , PConstant inFC (B32 (fromInteger x))
575 , PConstant inFC (B64 (fromInteger x))
576 ]
577modifyConst syn fc x = x
579{- | Parses an alternative expression
581 Alt ::= '(|' Expr_List '|)';
583 Expr_List ::=
584 Expr'
585 | Expr' ',' Expr_List
586 ;
588-}
589alt :: SyntaxInfo -> IdrisParser PTerm
590alt syn = do symbol "(|"; alts <- sepBy1 (expr' (syn { withAppAllowed = False })) (lchar ','); symbol "|)"
591 return (PAlternative [] FirstSuccess alts)
593{- | Parses a possibly hidden simple expression
595HSimpleExpr ::=
596 '.' SimpleExpr
597 | SimpleExpr
598 ;
600-}
601hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
602hsimpleExpr syn =
603 do lchar '.'
604 e <- simpleExpr syn
605 return $ PHidden e
606 <|> simpleExpr syn
607 <?> "expression"
609{- | Parses a unification log expression
610UnifyLog ::=
611 '%' 'unifyLog' SimpleExpr
612 ;
613-}
614unifyLog :: SyntaxInfo -> IdrisParser PTerm
615unifyLog syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "unifyLog")
616 tm <- simpleExpr syn
617 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
618 return (PUnifyLog tm)
619 <?> "unification log expression"
621{- | Parses a new-style tactics expression
622RunTactics ::=
623 '%' 'runElab' SimpleExpr
624 ;
625-}
626runElab :: SyntaxInfo -> IdrisParser PTerm
627runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab")
628 fc <- getFC
629 tm <- simpleExpr syn
630 highlightP (FC fn (sl, sc-1) kwEnd) AnnKeyword
631 return $ PRunElab fc tm (syn_namespace syn)
632 <?> "new-style tactics expression"
634{- | Parses a disambiguation expression
635Disamb ::=
636 'with' NameList Expr
637 ;
638-}
639disamb :: SyntaxInfo -> IdrisParser PTerm
640disamb syn = do kw <- reservedFC "with"
641 ns <- sepBy1 (fst <$> name) (lchar ',')
642 tm <- expr' syn
643 highlightP kw AnnKeyword
644 return (PDisamb (map tons ns) tm)
645 <?> "namespace disambiguation expression"
646 where tons (NS n s) = txt (show n) : s
647 tons n = [txt (show n)]
648{- | Parses a no implicits expression
650NoImplicits ::=
651 '%' 'noImplicits' SimpleExpr
652 ;
654-}
655noImplicits :: SyntaxInfo -> IdrisParser PTerm
656noImplicits syn = do try (lchar '%' *> reserved "noImplicits")
657 tm <- simpleExpr syn
658 return (PNoImplicits tm)
659 <?> "no implicits expression"
661{- | Parses a function application expression
663App ::=
664 'mkForeign' Arg Arg*
665 | MatchApp
666 | SimpleExpr Arg*
667 ;
668MatchApp ::=
669 SimpleExpr '<==' FnName
670 ;
672-}
673app :: SyntaxInfo -> IdrisParser PTerm
674app syn = do f <- simpleExpr syn
675 (do try $ reservedOp "<=="
676 fc <- getFC
677 ff <- fst <$> fnName
678 return (PLet fc (sMN 0 "match") NoFC
679 f
680 (PMatchApp fc ff)
681 (PRef fc [] (sMN 0 "match")))
682 <?> "matching application expression") <|>
683 (do fc <- getFC
684 i <- get
685 args <- many (do notEndApp; arg syn)
686 wargs <- if withAppAllowed syn && not (inPattern syn)
687 then many (do notEndApp; reservedOp "|"; expr' syn)
688 else return []
689 case args of
690 [] -> return f
691 _ -> return (withApp fc (flattenFromInt fc f args) wargs))
692 <?> "function application"
693 where
694 -- bit of a hack to deal with the situation where we're applying a
695 -- literal to an argument, which we may want for obscure applications
696 -- of fromInteger, and this will help disambiguate better.
697 -- We know, at least, it won't be one of the constants!
698 flattenFromInt fc (PAlternative _ x alts) args
699 | Just i <- getFromInt alts
700 = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)
701 flattenFromInt fc f args = PApp fc f args
703 withApp fc tm [] = tm
704 withApp fc tm (a : as) = withApp fc (PWithApp fc tm a) as
706 getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a
707 getFromInt (_ : xs) = getFromInt xs
708 getFromInt _ = Nothing
710{-| Parses a function argument
712Arg ::=
713 ImplicitArg
714 | ConstraintArg
715 | SimpleExpr
716 ;
718-}
719arg :: SyntaxInfo -> IdrisParser PArg
720arg syn = implicitArg syn
721 <|> constraintArg syn
722 <|> do e <- simpleExpr syn
723 return (pexp e)
724 <?> "function argument"
726{-| Parses an implicit function argument
728ImplicitArg ::=
729 '{' Name ('=' Expr)? '}'
730 ;
732-}
733implicitArg :: SyntaxInfo -> IdrisParser PArg
734implicitArg syn = do lchar '{'
735 (n, nfc) <- name
736 fc <- getFC
737 v <- option (PRef nfc [nfc] n) (do lchar '='
738 expr syn)
739 lchar '}'
740 return (pimp n v True)
741 <?> "implicit function argument"
743{-| Parses a constraint argument (for selecting a named interface implementation)
745> ConstraintArg ::=
746> '@{' Expr '}'
747> ;
749-}
750constraintArg :: SyntaxInfo -> IdrisParser PArg
751constraintArg syn = do symbol "@{"
752 e <- expr syn
753 symbol "}"
754 return (pconst e)
755 <?> "constraint argument"
757{-| Parses a quasiquote expression (for building reflected terms using the elaborator)
759> Quasiquote ::= '`(' Expr ')'
761-}
762quasiquote :: SyntaxInfo -> IdrisParser PTerm
763quasiquote syn = do startFC <- symbolFC "`("
764 e <- expr syn { syn_in_quasiquote = (syn_in_quasiquote syn) + 1 ,
765 inPattern = False }
766 g <- optional $
767 do fc <- symbolFC ":"
768 ty <- expr syn { inPattern = False } -- don't allow antiquotes
769 return (ty, fc)
770 endFC <- symbolFC ")"
771 mapM_ (uncurry highlightP) [(startFC, AnnKeyword), (endFC, AnnKeyword), (spanFC startFC endFC, AnnQuasiquote)]
772 case g of
773 Just (_, fc) -> highlightP fc AnnKeyword
774 _ -> return ()
775 return $ PQuasiquote e (fst <$> g)
776 <?> "quasiquotation"
778{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)
780> Unquote ::= ',' Expr
782-}
783unquote :: SyntaxInfo -> IdrisParser PTerm
784unquote syn = do guard (syn_in_quasiquote syn > 0)
785 startFC <- symbolFC "~"
786 e <- simpleExpr syn { syn_in_quasiquote = syn_in_quasiquote syn - 1 }
787 endFC <- getFC
788 highlightP startFC AnnKeyword
789 highlightP (spanFC startFC endFC) AnnAntiquote
790 return $ PUnquote e
791 <?> "unquotation"
793{-| Parses a quotation of a name (for using the elaborator to resolve boring details)
795> NameQuote ::= '`{' Name '}'
797-}
798namequote :: SyntaxInfo -> IdrisParser PTerm
799namequote syn = do (startFC, res) <-
800 try (do fc <- symbolFC "`{{"
801 return (fc, False)) <|>
802 (do fc <- symbolFC "`{"
803 return (fc, True))
804 (n, nfc) <- fnName
805 endFC <- if res then symbolFC "}" else symbolFC "}}"
806 mapM_ (uncurry highlightP)
807 [ (startFC, AnnKeyword)
808 , (endFC, AnnKeyword)
809 , (spanFC startFC endFC, AnnQuasiquote)
810 ]
811 return $ PQuoteName n res nfc
812 <?> "quoted name"
815{-| Parses a record field setter expression
817RecordType ::=
818 'record' '{' FieldTypeList '}';
821FieldTypeList ::=
822 FieldType
823 | FieldType ',' FieldTypeList
824 ;
827FieldType ::=
828 FnName '=' Expr
829 ;
831-}
833data SetOrUpdate = FieldSet PTerm | FieldUpdate PTerm
835recordType :: SyntaxInfo -> IdrisParser PTerm
836recordType syn =
837 do kw <- reservedFC "record"
838 lchar '{'
839 fgs <- fieldGetOrSet
840 lchar '}'
841 fc <- getFC
842 rec <- optional (do notEndApp; simpleExpr syn)
843 highlightP kw AnnKeyword
844 case fgs of
845 Left fields ->
846 case rec of
847 Nothing ->
848 return (PLam fc (sMN 0 "fldx") NoFC Placeholder
849 (applyAll fc fields (PRef fc [] (sMN 0 "fldx"))))
850 Just v -> return (applyAll fc fields v)
851 Right fields ->
852 case rec of
853 Nothing ->
854 return (PLam fc (sMN 0 "fldx") NoFC Placeholder
855 (getAll fc (reverse fields)
856 (PRef fc [] (sMN 0 "fldx"))))
857 Just v -> return (getAll fc (reverse fields) v)
859 <?> "record setting expression"
860 where fieldSet :: IdrisParser ([Name], SetOrUpdate)
861 fieldSet = do ns <- fieldGet
862 (do lchar '='
863 e <- expr syn
864 return (ns, FieldSet e))
865 <|> do symbol "$="
866 e <- expr syn
867 return (ns, FieldUpdate e)
868 <?> "field setter"
870 fieldGet :: IdrisParser [Name]
871 fieldGet = sepBy1 (fst <$> fnName) (symbol "->")
873 fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
874 fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')
875 return (Left fs))
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 <- try $ tyOptDeclList (disallowImp syn)
943 fc <- getFC
944 sc <- lambdaTail
945 return (bindList (\r -> PLam fc) xt sc))
946 <|>
947 (do ps <- 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 = 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 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 <- option Placeholder (do lchar ':'; expr' syn)
1011 lchar '='
1012 v <- expr (syn { withAppAllowed = isVar pat })
1013 ts <- option [] (do lchar '|'
1014 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 <- 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 notFollowedBy $ reservedOp "=>"
1148 return (PPi binder (sUN "__pi_arg") NoFC x sc))
1149 <|> do 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 <|> try (do lchar '{'; implicitPi opts st syn)
1159 <|> if constraintAllowed syn
1160 then 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 = try (constraintList1 syn)
1187 <|> return []
1189constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
1190constraintList1 syn = try (do lchar '('
1191 tys <- sepBy1 nexpr (lchar ',')
1192 lchar ')'
1193 reservedOp "=>"
1194 return tys)
1195 <|> try (do t <- opExpr (disallowImp syn)
1196 reservedOp "=>"
1197 return [(RigW, defname, NoFC, t)])
1198 <?> "type constraint list"
1199 where nexpr = 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 = try (sepBy1 (do rig <- 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 <- 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 = sepBy1 (do (x, fc) <- nameOrPlaceholder
1251 t <- 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 (try . 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 try (lchar '|') <?> "list comprehension"
1291 qs <- 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 | Name '<-' Expr
1342 | Expr' '<-' Expr
1343 | Expr
1347do_ :: SyntaxInfo -> IdrisParser PDo
1348do_ syn
1349 = try (do kw <- reservedFC "let"
1350 (i, ifc) <- name
1351 ty <- option Placeholder (do lchar ':'
1352 expr' syn)
1353 reservedOp "="
1354 fc <- getFC
1355 e <- expr syn
1356 highlightP kw AnnKeyword
1357 return (DoLet fc i ifc ty e))
1358 <|> try (do kw <- reservedFC "let"
1359 i <- expr' syn
1360 reservedOp "="
1361 fc <- getFC
1362 sc <- expr syn
1363 highlightP kw AnnKeyword
1364 return (DoLetP fc i sc))
1365 <|> try (do (i, ifc) <- name
1366 symbol "<-"
1367 fc <- getFC
1368 e <- expr (syn { withAppAllowed = False });
1369 option (DoBind fc i ifc e)
1370 (do lchar '|'
1371 ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
1372 return (DoBindP fc (PRef ifc [ifc] i) e ts)))
1373 <|> try (do i <- expr' syn
1374 symbol "<-"
1375 fc <- getFC
1376 e <- expr (syn { withAppAllowed = False });
1377 option (DoBindP fc i e [])
1378 (do lchar '|'
1379 ts <- sepBy1 (do_alt (syn { withAppAllowed = False })) (lchar '|')
1380 return (DoBindP fc i e ts)))
1381 <|> do e <- expr syn
1382 fc <- getFC
1383 return (DoExp fc e)
1384 <?> "do block expression"
1386do_alt syn = do l <- expr' syn
1387 option (Placeholder, l)
1388 (do symbol "=>"
1389 r <- expr' syn
1390 return (l, r))
1392{- | Parses an expression in idiom brackets
1394Idiom ::= '[|' Expr '|]';
1397idiom :: SyntaxInfo -> IdrisParser PTerm
1398idiom syn
1399 = do symbol "[|"
1400 fc <- getFC
1401 e <- expr (syn { withAppAllowed = False })
1402 symbol "|]"
1403 return (PIdiom fc e)
1404 <?> "expression in idiom brackets"
1406{- |Parses a constant or literal expression
1409Constant ::=
1410 'Integer'
1411 | 'Int'
1412 | 'Char'
1413 | 'Double'
1414 | 'String'
1415 | 'Bits8'
1416 | 'Bits16'
1417 | 'Bits32'
1418 | 'Bits64'
1419 | Float_t
1420 | Natural_t
1421 | VerbatimString_t
1422 | String_t
1423 | Char_t
1428constants :: [(String, Idris.Core.TT.Const)]
1429constants =
1430 [ ("Integer", AType (ATInt ITBig))
1431 , ("Int", AType (ATInt ITNative))
1432 , ("Char", AType (ATInt ITChar))
1433 , ("Double", AType ATFloat)
1434 , ("String", StrType)
1435 , ("prim__WorldType", WorldType)
1436 , ("prim__TheWorld", TheWorld)
1437 , ("Bits8", AType (ATInt (ITFixed IT8)))
1438 , ("Bits16", AType (ATInt (ITFixed IT16)))
1439 , ("Bits32", AType (ATInt (ITFixed IT32)))
1440 , ("Bits64", AType (ATInt (ITFixed IT64)))
1443-- | Parse a constant and its source span
1444constant :: IdrisParser (Idris.Core.TT.Const, FC)
1445constant = choice [ do fc <- reservedFC name; return (ty, fc)
1446 | (name, ty) <- constants
1448 <|> do (f, fc) <- try float; return (Fl f, fc)
1449 <|> do (i, fc) <- natural; return (BI i, fc)
1450 <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)
1451 <|> do (s, fc) <- stringLiteral; return (Str s, fc)
1452 <|> do (c, fc) <- try charLiteral; return (Ch c, fc) --Currently ambigous with symbols
1453 <?> "constant or literal"
1455{- | Parses a verbatim multi-line string literal (triple-quoted)
1458VerbatimString_t ::=
1459 '\"\"\"' ~'\"\"\"' '\"\"\"'
1462 -}
1463verbatimStringLiteral :: MonadicParsing m => m (String, FC)
1464verbatimStringLiteral = token $ do (FC f start _) <- getFC
1465 try $ string "\"\"\""
1466 str <- manyTill anyChar $ try (string "\"\"\"")
1467 (FC _ _ end) <- getFC
1468 return (str, FC f start end)
1470{- | Parses a static modifier
1473Static ::=
1474 '%static'
1478static :: IdrisParser Static
1479static = do reserved "%static"; return Static
1480 <|> do reserved "[static]"
1481 fc <- getFC
1482 parserWarning fc Nothing (Msg "The use of [static] is deprecated, use %static instead.")
1483 return Static
1484 <|> return Dynamic
1485 <?> "static modifier"
1487{- | Parses a tactic script
1490Tactic ::= 'intro' NameList?
1491 | 'intros'
1492 | 'refine' Name Imp+
1493 | 'mrefine' Name
1494 | 'rewrite' Expr
1495 | 'induction' Expr
1496 | 'equiv' Expr
1497 | 'let' Name ':' Expr' '=' Expr
1498 | 'let' Name '=' Expr
1499 | 'focus' Name
1500 | 'exact' Expr
1501 | 'applyTactic' Expr
1502 | 'reflect' Expr
1503 | 'fill' Expr
1504 | 'try' Tactic '|' Tactic
1505 | '{' TacticSeq '}'
1506 | 'compute'
1507 | 'trivial'
1508 | 'solve'
1509 | 'attack'
1510 | 'state'
1511 | 'term'
1512 | 'undo'
1513 | 'qed'
1514 | 'abandon'
1515 | ':' 'q'
1518Imp ::= '?' | '_';
1520TacticSeq ::=
1521 Tactic ';' Tactic
1522 | Tactic ';' TacticSeq
1527-- | A specification of the arguments that tactics can take
1528data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
1529 | ExprTArg
1530 | AltsTArg
1531 | StringLitTArg
1533-- The FIXMEs are Issue #1766 in the issue tracker.
1534-- https://github.com/idris-lang/Idris-dev/issues/1766
1535-- | A list of available tactics and their argument requirements
1536tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
1537tactics =
1538 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)
1539 do ns <- sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)
1540 , noArgs ["intros"] Intros
1541 , noArgs ["unfocus"] Unfocus
1542 , (["refine"], Just ExprTArg, const $
1543 do n <- spaced (fst <$> fnName)
1544 imps <- many imp
1545 return $ Refine n imps)
1546 , (["claim"], Nothing, \syn ->
1547 do n <- indentPropHolds gtProp *> (fst <$> name)
1548 goal <- indentPropHolds gtProp *> expr syn
1549 return $ Claim n goal)
1550 , (["mrefine"], Just ExprTArg, const $
1551 do n <- spaced (fst <$> fnName)
1552 return $ MatchRefine n)
1553 , expressionTactic ["rewrite"] Rewrite
1554 , expressionTactic ["case"] CaseTac
1555 , expressionTactic ["induction"] Induction
1556 , expressionTactic ["equiv"] Equiv
1557 , (["let"], Nothing, \syn -> -- FIXME syntax for let
1558 do n <- (indentPropHolds gtProp *> (fst <$> name))
1559 (do indentPropHolds gtProp *> lchar ':'
1560 ty <- indentPropHolds gtProp *> expr' syn
1561 indentPropHolds gtProp *> lchar '='
1562 t <- indentPropHolds gtProp *> expr syn
1563 i <- get
1564 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1565 <|> (do indentPropHolds gtProp *> lchar '='
1566 t <- indentPropHolds gtProp *> expr syn
1567 i <- get
1568 return $ LetTac n (desugar syn i t)))
1570 , (["focus"], Just ExprTArg, const $
1571 do n <- spaced (fst <$> name)
1572 return $ Focus n)
1573 , expressionTactic ["exact"] Exact
1574 , expressionTactic ["applyTactic"] ApplyTactic
1575 , expressionTactic ["byReflection"] ByReflection
1576 , expressionTactic ["reflect"] Reflect
1577 , expressionTactic ["fill"] Fill
1578 , (["try"], Just AltsTArg, \syn ->
1579 do t <- spaced (tactic syn)
1580 lchar '|'
1581 t1 <- spaced (tactic syn)
1582 return $ Try t t1)
1583 , noArgs ["compute"] Compute
1584 , noArgs ["trivial"] Trivial
1585 , noArgs ["unify"] DoUnify
1586 , (["search"], Nothing, const $
1587 do depth <- option 10 $ fst <$> natural
1588 return (ProofSearch True True (fromInteger depth) Nothing [] []))
1589 , noArgs ["implementation"] TCImplementation
1590 , noArgs ["solve"] Solve
1591 , noArgs ["attack"] Attack
1592 , noArgs ["state", ":state"] ProofState
1593 , noArgs ["term", ":term"] ProofTerm
1594 , noArgs ["undo", ":undo"] Undo
1595 , noArgs ["qed", ":qed"] Qed
1596 , noArgs ["abandon", ":q"] Abandon
1597 , noArgs ["skip"] Skip
1598 , noArgs ["sourceLocation"] SourceFC
1599 , expressionTactic [":e", ":eval"] TEval
1600 , expressionTactic [":t", ":type"] TCheck
1601 , expressionTactic [":search"] TSearch
1602 , (["fail"], Just StringLitTArg, const $
1603 do msg <- fst <$> stringLiteral
1604 return $ TFail [Idris.Core.TT.TextPart msg])
1605 , ([":doc"], Just ExprTArg, const $
1606 do whiteSpace
1607 doc <- (Right . fst <$> constant) <|> (Left . fst <$> fnName)
1608 eof
1609 return (TDocStr doc))
1611 where
1612 expressionTactic names tactic = (names, Just ExprTArg, \syn ->
1613 do t <- spaced (expr syn)
1614 i <- get
1615 return $ tactic (desugar syn i t))
1616 noArgs names tactic = (names, Nothing, const (return tactic))
1617 spaced parser = indentPropHolds gtProp *> parser
1618 imp :: IdrisParser Bool
1619 imp = do lchar '?'; return False
1620 <|> do lchar '_'; return True
1623tactic :: SyntaxInfo -> IdrisParser PTactic
1624tactic syn = choice [ do choice (map reserved names); parser syn
1625 | (names, _, parser) <- tactics ]
1626 <|> do lchar '{'
1627 t <- tactic syn;
1628 lchar ';';
1629 ts <- sepBy1 (tactic syn) (lchar ';')
1630 lchar '}'
1631 return $ TSeq t (mergeSeq ts)
1632 <|> ((lchar ':' >> empty) <?> "prover command")
1633 <?> "tactic"
1634 where
1635 mergeSeq :: [PTactic] -> PTactic
1636 mergeSeq [t] = t
1637 mergeSeq (t:ts) = TSeq t (mergeSeq ts)
1639-- | Parses a tactic as a whole
1640fullTactic :: SyntaxInfo -> IdrisParser PTactic
1641fullTactic syn = do t <- tactic syn
1642 eof
1643 return t