git.iko.soy/Idris-dev
on bbaa193 help sign in
Idris-dev/src/Idris/Parser.hs
817 lines 30 kB history raw
1module Idris.Parser where
3import Idris.AbsSyntax
4import Idris.Imports
5import Idris.Error
6import Idris.ElabDecls
7import Paths_idris
9import Core.CoreParser
10import Core.TT
11import Core.Evaluate
13import Text.ParserCombinators.Parsec
14import Text.ParserCombinators.Parsec.Error
15import Text.ParserCombinators.Parsec.Expr
16import Text.ParserCombinators.Parsec.Language
17import qualified Text.ParserCombinators.Parsec.Token as PTok
19import Data.List
20import Control.Monad.State
21import Debug.Trace
22import Data.Maybe
23import System.FilePath
25type TokenParser a = PTok.TokenParser a
27type IParser = GenParser Char IState
29lexer :: TokenParser IState
30lexer = PTok.makeTokenParser idrisDef
32whiteSpace= PTok.whiteSpace lexer
33lexeme = PTok.lexeme lexer
34symbol = PTok.symbol lexer
35natural = PTok.natural lexer
36parens = PTok.parens lexer
37semi = PTok.semi lexer
38comma = PTok.comma lexer
39identifier= PTok.identifier lexer
40reserved = PTok.reserved lexer
41operator = PTok.operator lexer
42reservedOp= PTok.reservedOp lexer
43integer = PTok.integer lexer
44float = PTok.float lexer
45strlit = PTok.stringLiteral lexer
46chlit = PTok.charLiteral lexer
47lchar = lexeme.char
49-- Loading modules
51loadModule :: FilePath -> Idris String
52loadModule f
53 = idrisCatch (do datadir <- lift $ getDataDir
54 fp <- lift $ findImport [".", datadir] f
55 i <- getIState
56 if (f `elem` imported i)
57 then iLOG $ "Already read " ++ f
58 else do putIState (i { imported = f : imported i })
59 case fp of
60 IDR fn -> loadSource fn
61 IBC fn -> error "Not implemented"
62 let (dir, fh) = splitFileName f
63 return (dropExtension fh))
64 (\e -> do let msg = report e
65 setErrLine (getErrLine msg)
66 iputStrLn msg
67 return "")
69loadSource :: FilePath -> Idris ()
70loadSource f = do iLOG ("Reading " ++ f)
71 file <- lift $ readFile f
72 (modules, rest, pos) <- parseImports f file
73 mapM_ loadModule modules
74 ds <- parseProg defaultSyntax f rest pos
75 logLvl 3 (dumpDecls ds)
76 i <- getIState
77 logLvl 10 (show (toAlist (idris_implicits i)))
78 logLvl 3 (show (idris_infixes i))
79 -- Now add all the declarations to the context
80 mapM_ (elabDecl toplevel) ds
81 iLOG ("Finished " ++ f)
82 return ()
84parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
85parseTac i = runParser (do t <- pTactic defaultSyntax
86 eof
87 return t) i "(proof)"
89parseImports :: FilePath -> String -> Idris ([String], String, SourcePos)
90parseImports fname input
91 = do i <- get
92 case (runParser (do ps <- many pImport
93 rest <- getInput
94 pos <- getPosition
95 return ((ps, rest, pos), i)) i fname input) of
96 Left err -> fail (ishow err)
97 Right (x, i) -> do put i
98 return x
99 where ishow err = let ln = sourceLine (errorPos err) in
100 fname ++ ":" ++ show ln ++ ":parse error"
101-- show (map messageString (errorMessages err))
104pfc :: IParser FC
105pfc = do s <- getPosition
106 let (dir, file) = splitFileName (sourceName s)
107 let f = case dir of
108 "./" -> file
109 _ -> sourceName s
110 return $ FC f (sourceLine s)
112pImport :: IParser String
113pImport = do reserved "import"
114 f <- identifier
115 lchar ';'
116 return f
118parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
119parseProg syn fname input pos
120 = do i <- get
121 case (runParser (do setPosition pos
122 whiteSpace
123 ps <- many1 (pDecl syn)
124 eof
125 i' <- getState
126 return (concat ps, i')) i fname input) of
127 Left err -> fail (ishow err)
128 Right (x, i) -> do put i
129 return (collect x)
130 where ishow err = let ln = sourceLine (errorPos err) in
131 fname ++ ":" ++ show ln ++ ":parse error"
132-- show (map messageString (errorMessages err))
134-- Collect PClauses with the same function name
136collect :: [PDecl] -> [PDecl]
137collect (c@(PClauses _ o _ _) : ds)
138 = clauses (cname c) [] (c : ds)
139 where clauses n acc (PClauses fc _ _ [PClause n' l ws r w] : ds)
140 | n == n' = clauses n (PClause n' l ws r (collect w) : acc) ds
141 clauses n acc (PClauses fc _ _ [PWith n' l ws r w] : ds)
142 | n == n' = clauses n (PWith n' l ws r (collect w) : acc) ds
143 clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs
145 cname (PClauses fc _ _ [PClause n _ _ _ _]) = n
146 cname (PClauses fc _ _ [PWith n _ _ _ _]) = n
147 getfc (PClauses fc _ _ _) = fc
149collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
150collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'
151collect (PInstance f s cs n ps t ds : ds')
152 = PInstance f s cs n ps t (collect ds) : collect ds'
153collect (d : ds) = d : collect ds
154collect [] = []
156pFullExpr :: SyntaxInfo -> IParser PTerm
157pFullExpr syn
158 = do x <- pExpr syn; eof;
159 i <- getState
160 return $ desugar syn i x
162pDecl :: SyntaxInfo -> IParser [PDecl]
163pDecl syn
164 = do d <- pDecl' syn
165 i <- getState
166 let d' = fmap (desugar syn i) d
167 return [d']
168 <|> pUsing syn
169 <|> pParams syn
170 <|> pClass syn
171 <|> pInstance syn
172 <|> pDirective
173 <|> try (do reserved "import"
174 fp <- identifier
175 lchar ';'
176 fail "imports must be at the top of file")
178pFunDecl :: SyntaxInfo -> IParser [PDecl]
179pFunDecl syn
180 = try (do d <- pFunDecl' syn
181 i <- getState
182 let d' = fmap (desugar syn i) d
183 return [d'])
185--------- Top Level Declarations ---------
187pDecl' :: SyntaxInfo -> IParser PDecl
188pDecl' syn
189 = try pFixity
190 <|> pFunDecl' syn
191 <|> try (pData syn)
192 <|> try (pSyntaxDecl syn)
194pSyntaxDecl :: SyntaxInfo -> IParser PDecl
195pSyntaxDecl syn
196 = do s <- pSyntaxRule syn
197 i <- getState
198 let rs = syntax_rules i
199 let ns = syntax_keywords i
200 let ks = map show (names s)
201 setState (i { syntax_rules = s : rs,
202 syntax_keywords = ks ++ ns })
203 fc <- pfc
204 return (PSyntax fc s)
205 where
206 names (Rule syms _ _) = mapMaybe ename syms
207 ename (Keyword n) = Just n
208 ename _ = Nothing
210pSyntaxRule :: SyntaxInfo -> IParser Syntax
211pSyntaxRule syn
212 = do sty <- option AnySyntax (do reserved "term"; return TermSyntax
213 <|> do reserved "pattern"; return PatternSyntax)
214 reserved "syntax"
215 syms <- many1 pSynSym
216 when (all expr syms) $ fail "No keywords in syntax rule"
217 let ns = mapMaybe name syms
218 when (length ns /= length (nub ns))
219 $ fail "Repeated variable in syntax rule"
220 lchar '='
221 tm <- pExpr syn
222 lchar ';'
223 return (Rule syms tm sty)
224 where
225 expr (Expr _) = True
226 expr _ = False
227 name (Expr n) = Just n
228 name _ = Nothing
230pSynSym :: IParser SSymbol
231pSynSym = try (do lchar '['; n <- pName; lchar ']'
232 return (Expr n))
233 <|> do n <- iName []
234 return (Keyword n)
235 <|> do sym <- strlit
236 return (Symbol sym)
238pFunDecl' :: SyntaxInfo -> IParser PDecl
239pFunDecl' syn = try (do n <- pfName;
240 ty <- pTSig syn
241 fc <- pfc
242 lchar ';'
243-- ty' <- implicit syn n ty
244 return (PTy syn fc n ty))
245 <|> try (pPattern syn)
247pUsing :: SyntaxInfo -> IParser [PDecl]
248pUsing syn =
249 do reserved "using";
250 lchar '('
251 ns <- tyDeclList syn
252 lchar ')'
253 lchar '{'
254 let uvars = using syn
255 ds <- many1 (pDecl (syn { using = uvars ++ ns }))
256 lchar '}'
257 return (concat ds)
259pParams :: SyntaxInfo -> IParser [PDecl]
260pParams syn =
261 do reserved "params";
262 lchar '('
263 ns <- tyDeclList syn
264 lchar ')'
265 lchar '{'
266 let pvars = syn_params syn
267 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
268 lchar '}'
269 fc <- pfc
270 return [PParams fc ns (concat ds)]
272--------- Fixity ---------
274pFixity :: IParser PDecl
275pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
276 lchar ';'
277 let prec = fromInteger i
278 istate <- getState
279 let fs = map (Fix (f prec)) ops
280 setState (istate {
281 idris_infixes = sort (fs ++ idris_infixes istate) })
282 fc <- pfc
283 return (PFix fc (f prec) ops)
285fixity :: IParser (Int -> Fixity)
286fixity = try (do reserved "infixl"; return Infixl)
287 <|> try (do reserved "infixr"; return Infixr)
288 <|> try (do reserved "infix"; return InfixN)
289 <|> try (do reserved "prefix"; return PrefixN)
291--------- Tyoe classes ---------
293pClass :: SyntaxInfo -> IParser [PDecl]
294pClass syn = do reserved "class"
295 fc <- pfc
296 cons <- pConstList syn
297 n <- pName
298 cs <- many1 carg
299 reserved "where"; lchar '{'
300 ds <- many1 $ pFunDecl syn;
301 lchar '}'
302 return [PClass syn fc cons n cs (concat ds)]
303 where
304 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
305 return (i, ty)
306 <|> do i <- pName;
307 return (i, PSet)
309pInstance :: SyntaxInfo -> IParser [PDecl]
310pInstance syn = do reserved "instance"
311 fc <- pfc
312 cs <- pConstList syn
313 cn <- pName
314 args <- many1 (pSimpleExpr syn)
315 let sc = PApp fc (PRef fc cn) (map pexp args)
316 let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
317 reserved "where"; lchar '{'
318 ds <- many1 $ pFunDecl syn;
319 lchar '}'
320 return [PInstance syn fc cs cn args t (concat ds)]
322--------- Expressions ---------
324pExpr syn = do i <- getState
325 buildExpressionParser (table (idris_infixes i)) (pExpr' syn)
327pExpr' :: SyntaxInfo -> IParser PTerm
328pExpr' syn
329 = try (pExtExpr syn)
330 <|> pNoExtExpr syn
332pExtExpr :: SyntaxInfo -> IParser PTerm
333pExtExpr syn = do i <- getState
334 pExtensions syn (syntax_rules i)
336pSimpleExtExpr :: SyntaxInfo -> IParser PTerm
337pSimpleExtExpr syn = do i <- getState
338 pExtensions syn (filter simple (syntax_rules i))
339 where
340 simple (Rule (Expr x:xs) _ _) = False
341 simple (Rule (_:xs) _ _) = case (last xs) of
342 Keyword _ -> True
343 Symbol _ -> True
344 _ -> False
345 simple _ = False
347pNoExtExpr syn =
348 try (pApp syn)
349 <|> pSimpleExpr syn
350 <|> pLambda syn
351 <|> pLet syn
352 <|> pPi syn
353 <|> pDoBlock syn
355pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm
356pExtensions syn rules = choice (map (\x -> try (pExt syn x)) (filter valid rules))
357 where
358 valid (Rule _ _ AnySyntax) = True
359 valid (Rule _ _ PatternSyntax) = inPattern syn
360 valid (Rule _ _ TermSyntax) = not (inPattern syn)
363pExt :: SyntaxInfo -> Syntax -> IParser PTerm
364pExt syn (Rule (s:ssym) ptm _)
365 = do s1 <- pSymbol pSimpleExpr s
366 smap <- mapM (pSymbol pExpr') ssym
367 let ns = mapMaybe id (s1:smap)
368 return (update ns ptm) -- updated with smap
369 where
370 pSymbol p (Keyword n) = do reserved (show n); return Nothing
371 pSymbol p (Expr n) = do tm <- p syn
372 return $ Just (n, tm)
373 pSymbol p (Symbol s) = do symbol s
374 return Nothing
375 dropn n [] = []
376 dropn n ((x,t) : xs) | n == x = xs
377 | otherwise = (x,t):dropn n xs
379 update ns (PRef fc n) = case lookup n ns of
380 Just t -> t
381 _ -> PRef fc n
382 update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)
383 update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc)
384 update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)
385 (update (dropn n ns) sc)
386 update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
387 update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
388 update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
389 update ns (PHidden t) = PHidden (update ns t)
390 update ns (PDoBlock ds) = PDoBlock $ upd ns ds
391 where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
392 upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
393 upd ns (DoLet fc n t : ds) = DoLet fc n (update ns t) : upd (dropn n ns) ds
394 update ns t = t
396pName = do i <- getState
397 iName (syntax_keywords i)
398 <|> do reserved "instance"
399 i <- getState
400 UN n <- iName (syntax_keywords i)
401 return (UN ('@':n))
403pfName = try pName
404 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)
406pSimpleExpr syn =
407 try (do symbol "!["; t <- pTerm; lchar ']'
408 return $ PQuote t)
409 <|> do lchar '?'; x <- pName; return (PMetavar x)
410 <|> do reserved "refl"; fc <- pfc; return (PRefl fc)
411-- <|> do reserved "return"; fc <- pfc; return (PReturn fc)
412 <|> do reserved "proof"; lchar '{';
413 ts <- endBy (pTactic syn) (lchar ';')
414 lchar '}'
415 return (PProof ts)
416 <|> do reserved "tactics"; lchar '{';
417 ts <- endBy (pTactic syn) (lchar ';')
418 lchar '}'
419 return (PTactics ts)
420 <|> try (do x <- pfName; fc <- pfc; return (PRef fc x))
421 <|> try (pPair syn)
422 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)
423 <|> try (do c <- pConstant; fc <- pfc
424 return (modifyConst syn fc (PConstant c)))
425 <|> do reserved "Set"; return PSet
426 <|> try (do symbol "()"; fc <- pfc; return (PTrue fc))
427 <|> try (do symbol "_|_"; fc <- pfc; return (PFalse fc))
428 <|> do lchar '_'; return Placeholder
429 <|> pSimpleExtExpr syn
431modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
432modifyConst syn fc (PConstant (I x))
433 | not (inPattern syn)
434 = PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I x))]
435modifyConst syn fc x = x
437pPair syn = try (do lchar '('; l <- pExpr syn; op <- pairOp
438 fc <- pfc
439 r <- pExpr syn; lchar ')';
440 return (op fc l r))
441 <|> do lchar '('; ln <- pName; lchar ':'; lty <- pExpr syn;
442 reservedOp "**";
443 fc <- pfc
444 r <- pExpr syn; lchar ')';
445 return (PDPair fc (PRef fc ln) lty r)
446 where
447 pairOp = do lchar ','; return PPair
448 <|> do reservedOp "**"; return (\f x y -> PDPair f x Placeholder y)
451pHSimpleExpr syn
452 = do lchar '.'
453 e <- pSimpleExpr syn
454 return $ PHidden e
455 <|> pSimpleExpr syn
457pApp syn = do f <- pSimpleExpr syn
458 fc <- pfc
459 args <- many1 (pArg syn)
460 return (PApp fc f args)
462pArg :: SyntaxInfo -> IParser PArg
463pArg syn = try (pImplicitArg syn)
464 <|> try (pConstraintArg syn)
465 <|> do e <- pSimpleExpr syn
466 return (pexp e)
468pImplicitArg syn = do lchar '{'; n <- pName
469 fc <- pfc
470 v <- option (PRef fc n) (do lchar '='; pExpr syn)
471 lchar '}'
472 return (pimp n v)
474pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
475 return (pconst e)
477pTSig syn = do lchar ':'
478 cs <- pConstList syn
479 sc <- pExpr syn
480 return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
482pLambda syn = do lchar '\\';
483 xt <- tyOptDeclList syn
484 symbol "=>"
485 sc <- pExpr syn
486 return (bindList PLam xt sc)
488pLet syn = do reserved "let"; n <- pName;
489 ty <- option Placeholder (do lchar ':'; pExpr' syn)
490 lchar '='; v <- pExpr syn
491 reserved "in"; sc <- pExpr syn
492 return (PLet n ty v sc)
494pPi syn =
495 try (do lazy <- option False (do lchar '|'; return True)
496 st <- pStatic
497 lchar '('; xt <- tyDeclList syn; lchar ')'
498 symbol "->"
499 sc <- pExpr syn
500 return (bindList (PPi (Exp lazy st)) xt sc))
501 <|> try (do lazy <- option False (do lchar '|'; return True)
502 st <- pStatic
503 lchar '{'; xt <- tyDeclList syn; lchar '}'
504 symbol "->"
505 sc <- pExpr syn
506 return (bindList (PPi (Imp lazy st)) xt sc))
507 <|> do --lazy <- option False (do lchar '|'; return True)
508 lchar '['; reserved "static"; lchar ']'
509 t <- pExpr' syn
510 symbol "->"
511 sc <- pExpr syn
512 return (PPi (Exp False Static) (MN 0 "X") t sc)
514pConstList :: SyntaxInfo -> IParser [PTerm]
515pConstList syn = try (do lchar '('
516 tys <- sepBy1 (pExpr' syn) (lchar ',')
517 lchar ')'
518 reservedOp "=>"
519 return tys)
520 <|> try (do t <- pExpr syn
521 reservedOp "=>"
522 return [t])
523 <|> return []
525tyDeclList syn = try (sepBy1 (do x <- pfName; t <- pTSig syn; return (x,t))
526 (lchar ','))
527 <|> do ns <- sepBy1 pName (lchar ',')
528 t <- pTSig syn
529 return (map (\x -> (x, t)) ns)
531tyOptDeclList syn = sepBy1 (do x <- pfName; t <- option Placeholder (pTSig syn)
532 return (x,t))
533 (lchar ',')
535bindList b [] sc = sc
536bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
538pDoBlock syn
539 = do reserved "do"; lchar '{'
540 ds <- endBy1 (pDo syn) (lchar ';')
541 lchar '}'
542 return (PDoBlock ds)
544pDo syn
545 = do reserved "let"; i <- pName; reservedOp "="; fc <- pfc
546 e <- pExpr syn
547 return (DoLet fc i e)
548 <|> try (do i <- pName; symbol "<-"; fc <- pfc
549 e <- pExpr syn;
550 return (DoBind fc i e))
551 <|> try (do e <- pExpr syn; fc <- pfc
552 return (DoExp fc e))
554pConstant :: IParser Const
555pConstant = do reserved "Integer";return BIType
556 <|> do reserved "Int"; return IType
557 <|> do reserved "Char"; return ChType
558 <|> do reserved "Float"; return FlType
559 <|> do reserved "String"; return StrType
560 <|> do reserved "Ptr"; return PtrType
561 <|> try (do f <- float; return $ Fl f)
562 <|> try (do i <- natural; lchar 'L'; return $ BI i)
563 <|> try (do i <- natural; return $ I (fromInteger i))
564 <|> try (do s <- strlit; return $ Str s)
565 <|> try (do c <- chlit; return $ Ch c)
567pStatic :: IParser Static
568pStatic = do lchar '['; reserved "static"; lchar ']';
569 return Static
570 <|> return Dynamic
572table fixes
573 = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
574 [pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (I 0))]), pexp x])]]
575 ++ toTable (reverse fixes) ++
576 [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],
577 [binary "->" (\fc x y -> PPi expl (MN 0 "X") x y) AssocRight]]
579toTable fs = map (map toBin)
580 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
581 where toBin (Fix (PrefixN _) op) = prefix op
582 (\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
583 toBin (Fix f op)
584 = binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
585 assoc (Infixl _) = AssocLeft
586 assoc (Infixr _) = AssocRight
587 assoc (InfixN _) = AssocNone
589binary name f assoc = Infix (do { reservedOp name; fc <- pfc;
590 return (f fc) }) assoc
591prefix name f = Prefix (do { reservedOp name; fc <- pfc;
592 return (f fc) })
594--------- Data declarations ---------
596pData :: SyntaxInfo -> IParser PDecl
597pData syn = try (do reserved "data"; fc <- pfc
598 tyn <- pfName; ty <- pTSig syn
599 reserved "where"
600-- ty' <- implicit syn tyn ty
601 cons <- sepBy (pConstructor syn) (lchar '|')
602 lchar ';'
603 return $ PData syn fc (PDatadecl tyn ty cons))
604 <|> do reserved "data"; fc <- pfc
605 tyn <- pfName; args <- many pName
606 lchar '='
607 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
608 lchar ';'
609 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
610 let ty = bindArgs (map (\a -> PSet) args) PSet
611-- ty' <- implicit syn tyn ty
612 cons' <- mapM (\ (x, cargs, cfc) ->
613 do let cty = bindArgs cargs conty
614-- cty' <- implicit syn x cty
615 return (x, cty, cfc)) cons
616 return $ PData syn fc (PDatadecl tyn ty cons')
617 where
618 mkPApp fc t [] = t
619 mkPApp fc t xs = PApp fc t (map pexp xs)
621bindArgs :: [PTerm] -> PTerm -> PTerm
622bindArgs [] t = t
623bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
625pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
626pConstructor syn
627 = do cn <- pfName; fc <- pfc
628 ty <- pTSig syn
629-- ty' <- implicit syn cn ty
630 return (cn, ty, fc)
632pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
633pSimpleCon syn
634 = do cn <- pfName
635 fc <- pfc
636 args <- many (pSimpleExpr syn)
637 return (cn, args, fc)
639--------- Pattern match clauses ---------
641pPattern :: SyntaxInfo -> IParser PDecl
642pPattern syn = do clause <- pClause syn
643 fc <- pfc
644 return (PClauses fc False (MN 2 "_") [clause]) -- collect together later
646whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo
647whereSyn n syn args = let ns = concatMap allNamesIn args
648 ni = no_imp syn in
649 syn { decoration = \x -> decorate n (decoration syn x),
650 no_imp = nub (ni ++ ns) }
651 where decorate n x = UN (show n ++ "_" ++ show x)
653pArgExpr syn = let syn' = syn { inPattern = True } in
654 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
656pRHS :: SyntaxInfo -> Name -> IParser PTerm
657pRHS syn n = do lchar '='; pExpr syn
658 <|> do symbol "?="; rhs <- pExpr syn;
659 return (PLet (UN "value") Placeholder rhs (PMetavar n'))
660 where n' = case n of
661 UN x -> UN (x++"_lemma_1")
662 x -> x
664pClause :: SyntaxInfo -> IParser PClause
665pClause syn
666 = try (do n <- pfName
667 cargs <- many (pConstraintArg syn)
668 iargs <- many (pImplicitArg syn)
669 fc <- pfc
670 args <- many (pArgExpr syn)
671 wargs <- many (pWExpr syn)
672 rhs <- pRHS syn n
673 ist <- getState
674 let ctxt = tt_ctxt ist
675 let wsyn = whereSyn n syn (map getTm iargs ++
676 map getTm cargs ++
677 args ++ wargs)
678 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
679 return ([], [])]
680 return $ PClause n (PApp fc (PRef fc n)
681 (iargs ++ cargs ++ map pexp args)) wargs rhs wheres)
682 <|> try (do n <- pfName
683 cargs <- many (pConstraintArg syn)
684 iargs <- many (pImplicitArg syn)
685 fc <- pfc
686 args <- many (pArgExpr syn)
687 wargs <- many (pWExpr syn)
688 reserved "with"
689 wval <- pExpr syn
690 lchar '{'
691 ds <- many1 $ pFunDecl syn
692 let withs = concat ds
693 lchar '}'
694 return $ PWith n (PApp fc (PRef fc n)
695 (iargs ++ cargs ++ map pexp args)) wargs wval withs)
697 <|> do l <- pArgExpr syn
698 op <- operator
699 let n = UN op
700 r <- pArgExpr syn
701 fc <- pfc
702 wargs <- many (pWExpr syn)
703 rhs <- pRHS syn n
704 let wsyn = whereSyn n syn []
705 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
706 return ([], [])]
707 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])
708 wargs rhs wheres
710 <|> do l <- pArgExpr syn
711 op <- operator
712 let n = UN op
713 r <- pArgExpr syn
714 fc <- pfc
715 wargs <- many (pWExpr syn)
716 reserved "with"
717 wval <- pExpr syn
718 lchar '{'
719 ds <- many1 $ pFunDecl syn
720 let withs = concat ds
721 lchar '}'
722 return $ PWith n (PApp fc (PRef fc n) [pexp l, pexp r]) wargs wval withs
724pWExpr :: SyntaxInfo -> IParser PTerm
725pWExpr syn = do lchar '|'; pExpr' syn
727pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
728pWhereblock n syn
729 = do reserved "where"; lchar '{'
730 ds <- many1 $ pFunDecl syn;
731 let dns = concatMap (concatMap declared) ds
732 lchar '}';
733 return (concat ds, map (\x -> (x, decoration syn x)) dns)
735pDirective :: IParser [PDecl]
736pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
737 return [PDirective (addLib lib)])
738 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
739 return [PDirective (do datadir <- lift $ getDataDir
740 o <- lift $ findInPath [".", datadir] obj
741 addObjectFile o)])
742 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
743 return [PDirective (addHdr hdr)])
744 <|> do lchar '%'; reserved "logging"; i <- natural;
745 return [PDirective (setLogLevel (fromInteger i))]
747pTactic :: SyntaxInfo -> IParser PTactic
748pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
749 return $ Intro ns
750 <|> try (do reserved "refine"; n <- pName
751 imps <- many1 imp
752 return $ Refine n imps)
753 <|> do reserved "refine"; n <- pName
754 i <- getState
755 return $ Refine n []
756 <|> do reserved "rewrite"; t <- pExpr syn;
757 i <- getState
758 return $ Rewrite (desugar syn i t)
759 <|> do reserved "let"; n <- pName; lchar '=';
760 t <- pExpr syn;
761 i <- getState
762 return $ LetTac n (desugar syn i t)
763 <|> do reserved "focus"; n <- pName
764 return $ Focus n
765 <|> do reserved "exact"; t <- pExpr syn;
766 i <- getState
767 return $ Exact (desugar syn i t)
768 <|> do reserved "try"; t <- pTactic syn;
769 lchar '|';
770 t1 <- pTactic syn
771 return $ Try t t1
772 <|> do lchar '{'
773 t <- pTactic syn;
774 lchar ';';
775 t1 <- pTactic syn;
776 lchar '}'
777 return $ TSeq t t1
778 <|> do reserved "compute"; return Compute
779 <|> do reserved "trivial"; return Trivial
780 <|> do reserved "solve"; return Solve
781 <|> do reserved "attack"; return Attack
782 <|> do reserved "state"; return ProofState
783 <|> do reserved "term"; return ProofTerm
784 <|> do reserved "undo"; return Undo
785 <|> do reserved "qed"; return Qed
786 where
787 imp = do lchar '?'; return False
788 <|> do lchar '_'; return True
790desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
791desugar syn i t = let t' = expandDo (dsl_info syn) t in
792 t' -- addImpl i t'
794expandDo :: DSL -> PTerm -> PTerm
795expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
796expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
797expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
798 (map (fmap (expandDo dsl)) args)
799expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
800expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
801 (expandDo dsl r)
802expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
803expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)
804expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
805 where
806 block b [DoExp fc tm] = tm
807 block b [a] = PElabError "Last statement in do block must be an expression"
808 block b (DoBind fc n tm : rest)
809 = PApp fc (PRef fc b) [pexp tm, pexp (PLam n Placeholder (block b rest))]
810 block b (DoExp fc tm : rest)
811 = PApp fc (PRef fc b)
812 [pexp tm,
813 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
814expandDo dsl t = t