git.iko.soy/Idris-dev
on 63afafa help sign in
Idris-dev/src/Core/ShellParser.hs
73 lines 2.8 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Core.ShellParser(parseCommand, parseTactic) where
5import Core.TT
6import Core.Elaborate
7import Core.CoreParser
9import Text.ParserCombinators.Parsec
10import Text.ParserCombinators.Parsec.Expr
11import Text.ParserCombinators.Parsec.Language
12import qualified Text.ParserCombinators.Parsec.Token as PTok
14import Debug.Trace
16type TokenParser a = PTok.TokenParser a
18lexer :: TokenParser ()
19lexer = PTok.makeTokenParser haskellDef
21whiteSpace= PTok.whiteSpace lexer
22lexeme = PTok.lexeme lexer
23symbol = PTok.symbol lexer
24natural = PTok.natural lexer
25parens = PTok.parens lexer
26semi = PTok.semi lexer
27comma = PTok.comma lexer
28identifier= PTok.identifier lexer
29reserved = PTok.reserved lexer
30operator = PTok.operator lexer
31reservedOp= PTok.reservedOp lexer
32lchar = lexeme.char
34parseCommand = parse pCommand "(input)"
35parseTactic = parse (pTactic >>= return . Tac) "(input)"
37pCommand :: Parser Command
38pCommand = do reserved "theorem"; n <- iName []; lchar ':'; ty <- pTerm
39 return (Theorem n ty)
40 <|> do reserved "eval"; tm <- pTerm
41 return (Eval tm)
42 <|> do reserved "print"; n <- iName []; return (Print n)
43 <|> do reserved "quit";
44 return Quit
46pTactic :: Parser (Elab ())
47pTactic = do reserved "attack"; return attack
48 <|> do reserved "claim"; n <- iName []; lchar ':'; ty <- pTerm
49 return (claim n ty)
50 <|> do reserved "regret"; return regret
51 <|> do reserved "exact"; tm <- pTerm; return (exact tm)
52 <|> do reserved "fill"; tm <- pTerm; return (fill tm)
53 <|> do reserved "apply"; tm <- pTerm; args <- many pArgType;
54 return (discard (apply tm (map (\x -> (x,0)) args)))
55 <|> do reserved "solve"; return solve
56 <|> do reserved "compute"; return compute
57 <|> do reserved "intro"; n <- iName []; return (intro (Just n))
58 <|> do reserved "forall"; n <- iName []; lchar ':'; ty <- pTerm
59 return (forall n ty)
60 <|> do reserved "arg"; n <- iName []; t <- iName []; return (arg n t)
61 <|> do reserved "patvar"; n <- iName []; return (patvar n)
62-- <|> do reserved "patarg"; n <- iName []; t <- iName []; return (patarg n t)
63 <|> do reserved "eval"; t <- pTerm; return (eval_in t)
64 <|> do reserved "check"; t <- pTerm; return (check_in t)
65 <|> do reserved "focus"; n <- iName []; return (focus n)
66 <|> do reserved "state"; return proofstate
67 <|> do reserved "undo"; return undo
68 <|> do reserved "qed"; return (discard qed)
70pArgType :: Parser Bool
71pArgType = do lchar '_'; return True -- implicit (machine fills in)
72 <|> do lchar '?'; return False -- user fills in