git.iko.soy/Idris-dev
on 93946fc help sign in
Idris-dev/src/Idris/Parser.hs
816 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:ns) <- iName (syntax_keywords i)
401 return (UN (('@':n) : ns))
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 ["-"])) [pexp (PConstant (I 0)), pexp x])]]
574 ++ toTable (reverse fixes) ++
575 [[binary "=" (\fc x y -> PEq fc x y) AssocLeft],
576 [binary "->" (\fc x y -> PPi expl (MN 0 "X") x y) AssocRight]]
578toTable fs = map (map toBin)
579 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
580 where toBin (Fix (PrefixN _) op) = prefix op
581 (\fc x -> PApp fc (PRef fc (UN [op])) [pexp x])
582 toBin (Fix f op)
583 = binary op (\fc x y -> PApp fc (PRef fc (UN [op])) [pexp x,pexp y]) (assoc f)
584 assoc (Infixl _) = AssocLeft
585 assoc (Infixr _) = AssocRight
586 assoc (InfixN _) = AssocNone
588binary name f assoc = Infix (do { reservedOp name; fc <- pfc;
589 return (f fc) }) assoc
590prefix name f = Prefix (do { reservedOp name; fc <- pfc;
591 return (f fc) })
593--------- Data declarations ---------
595pData :: SyntaxInfo -> IParser PDecl
596pData syn = try (do reserved "data"; fc <- pfc
597 tyn <- pfName; ty <- pTSig syn
598 reserved "where"
599-- ty' <- implicit syn tyn ty
600 cons <- sepBy (pConstructor syn) (lchar '|')
601 lchar ';'
602 return $ PData syn fc (PDatadecl tyn ty cons))
603 <|> do reserved "data"; fc <- pfc
604 tyn <- pfName; args <- many pName
605 lchar '='
606 cons <- sepBy1 (pSimpleCon syn) (lchar '|')
607 lchar ';'
608 let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
609 let ty = bindArgs (map (\a -> PSet) args) PSet
610-- ty' <- implicit syn tyn ty
611 cons' <- mapM (\ (x, cargs, cfc) ->
612 do let cty = bindArgs cargs conty
613-- cty' <- implicit syn x cty
614 return (x, cty, cfc)) cons
615 return $ PData syn fc (PDatadecl tyn ty cons')
616 where
617 mkPApp fc t [] = t
618 mkPApp fc t xs = PApp fc t (map pexp xs)
620bindArgs :: [PTerm] -> PTerm -> PTerm
621bindArgs [] t = t
622bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
624pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
625pConstructor syn
626 = do cn <- pfName; fc <- pfc
627 ty <- pTSig syn
628-- ty' <- implicit syn cn ty
629 return (cn, ty, fc)
631pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
632pSimpleCon syn
633 = do cn <- pfName
634 fc <- pfc
635 args <- many (pSimpleExpr syn)
636 return (cn, args, fc)
638--------- Pattern match clauses ---------
640pPattern :: SyntaxInfo -> IParser PDecl
641pPattern syn = do clause <- pClause syn
642 fc <- pfc
643 return (PClauses fc False (MN 2 "_") [clause]) -- collect together later
645whereSyn :: Name -> SyntaxInfo -> [PTerm] -> SyntaxInfo
646whereSyn n syn args = let ns = concatMap allNamesIn args
647 ni = no_imp syn in
648 syn { decoration = \x -> decorate n (decoration syn x),
649 no_imp = nub (ni ++ ns) }
650 where decorate n x = UN [(show n ++ "_" ++ show x)]
652pArgExpr syn = let syn' = syn { inPattern = True } in
653 try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'
655pRHS :: SyntaxInfo -> Name -> IParser PTerm
656pRHS syn n = do lchar '='; pExpr syn
657 <|> do symbol "?="; rhs <- pExpr syn;
658 return (PLet (UN ["value"]) Placeholder rhs (PMetavar n'))
659 where n' = case n of
660 UN [x] -> UN [x++"_lemma_1"]
661 x -> x
663pClause :: SyntaxInfo -> IParser PClause
664pClause syn
665 = try (do n <- pfName
666 cargs <- many (pConstraintArg syn)
667 iargs <- many (pImplicitArg syn)
668 fc <- pfc
669 args <- many (pArgExpr syn)
670 wargs <- many (pWExpr syn)
671 rhs <- pRHS syn n
672 ist <- getState
673 let ctxt = tt_ctxt ist
674 let wsyn = whereSyn n syn (map getTm iargs ++
675 map getTm cargs ++
676 args ++ wargs)
677 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
678 return ([], [])]
679 return $ PClause n (PApp fc (PRef fc n)
680 (iargs ++ cargs ++ map pexp args)) wargs rhs wheres)
681 <|> try (do n <- pfName
682 cargs <- many (pConstraintArg syn)
683 iargs <- many (pImplicitArg syn)
684 fc <- pfc
685 args <- many (pArgExpr syn)
686 wargs <- many (pWExpr syn)
687 reserved "with"
688 wval <- pExpr syn
689 lchar '{'
690 ds <- many1 $ pFunDecl syn
691 let withs = concat ds
692 lchar '}'
693 return $ PWith n (PApp fc (PRef fc n)
694 (iargs ++ cargs ++ map pexp args)) wargs wval withs)
696 <|> do l <- pArgExpr syn
697 op <- operator
698 let n = UN [op]
699 r <- pArgExpr syn
700 fc <- pfc
701 wargs <- many (pWExpr syn)
702 rhs <- pRHS syn n
703 let wsyn = whereSyn n syn []
704 (wheres, nmap) <- choice [pWhereblock n syn, do lchar ';'
705 return ([], [])]
706 return $ PClause n (PApp fc (PRef fc n) [pexp l,pexp r])
707 wargs rhs wheres
709 <|> do l <- pArgExpr syn
710 op <- operator
711 let n = UN [op]
712 r <- pArgExpr syn
713 fc <- pfc
714 wargs <- many (pWExpr syn)
715 reserved "with"
716 wval <- pExpr syn
717 lchar '{'
718 ds <- many1 $ pFunDecl syn
719 let withs = concat ds
720 lchar '}'
721 return $ PWith n (PApp fc (PRef fc n) [pexp l, pexp r]) wargs wval withs
723pWExpr :: SyntaxInfo -> IParser PTerm
724pWExpr syn = do lchar '|'; pExpr' syn
726pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])
727pWhereblock n syn
728 = do reserved "where"; lchar '{'
729 ds <- many1 $ pFunDecl syn;
730 let dns = concatMap (concatMap declared) ds
731 lchar '}';
732 return (concat ds, map (\x -> (x, decoration syn x)) dns)
734pDirective :: IParser [PDecl]
735pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;
736 return [PDirective (addLib lib)])
737 <|> try (do lchar '%'; reserved "link"; obj <- strlit;
738 return [PDirective (do datadir <- lift $ getDataDir
739 o <- lift $ findInPath [".", datadir] obj
740 addObjectFile o)])
741 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;
742 return [PDirective (addHdr hdr)])
743 <|> do lchar '%'; reserved "logging"; i <- natural;
744 return [PDirective (setLogLevel (fromInteger i))]
746pTactic :: SyntaxInfo -> IParser PTactic
747pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')
748 return $ Intro ns
749 <|> try (do reserved "refine"; n <- pName
750 imps <- many1 imp
751 return $ Refine n imps)
752 <|> do reserved "refine"; n <- pName
753 i <- getState
754 return $ Refine n []
755 <|> do reserved "rewrite"; t <- pExpr syn;
756 i <- getState
757 return $ Rewrite (desugar syn i t)
758 <|> do reserved "let"; n <- pName; lchar '=';
759 t <- pExpr syn;
760 i <- getState
761 return $ LetTac n (desugar syn i t)
762 <|> do reserved "focus"; n <- pName
763 return $ Focus n
764 <|> do reserved "exact"; t <- pExpr syn;
765 i <- getState
766 return $ Exact (desugar syn i t)
767 <|> do reserved "try"; t <- pTactic syn;
768 lchar '|';
769 t1 <- pTactic syn
770 return $ Try t t1
771 <|> do lchar '{'
772 t <- pTactic syn;
773 lchar ';';
774 t1 <- pTactic syn;
775 lchar '}'
776 return $ TSeq t t1
777 <|> do reserved "compute"; return Compute
778 <|> do reserved "trivial"; return Trivial
779 <|> do reserved "solve"; return Solve
780 <|> do reserved "attack"; return Attack
781 <|> do reserved "state"; return ProofState
782 <|> do reserved "term"; return ProofTerm
783 <|> do reserved "undo"; return Undo
784 <|> do reserved "qed"; return Qed
785 where
786 imp = do lchar '?'; return False
787 <|> do lchar '_'; return True
789desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
790desugar syn i t = let t' = expandDo (dsl_info syn) t in
791 t' -- addImpl i t'
793expandDo :: DSL -> PTerm -> PTerm
794expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)
795expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)
796expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)
797 (map (fmap (expandDo dsl)) args)
798expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
799expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
800 (expandDo dsl r)
801expandDo dsl (PHidden t) = PHidden (expandDo dsl t)
802expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)
803expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds
804 where
805 block b [DoExp fc tm] = tm
806 block b [a] = PElabError "Last statement in do block must be an expression"
807 block b (DoBind fc n tm : rest)
808 = PApp fc (PRef fc b) [pexp tm, pexp (PLam n Placeholder (block b rest))]
809 block b (DoExp fc tm : rest)
810 = PApp fc (PRef fc b)
811 [pexp tm,
812 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]
813expandDo dsl t = t