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