-
Notifications
You must be signed in to change notification settings - Fork 643
/
ShellParser.hs
73 lines (61 loc) · 2.64 KB
/
ShellParser.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
module Core.ShellParser(parseCommand, parseTactic) where
import Core.Core
import Core.Elaborate
import Core.CoreParser
import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as PTok
import Debug.Trace
type TokenParser a = PTok.TokenParser a
lexer :: TokenParser ()
lexer = PTok.makeTokenParser haskellDef
whiteSpace= PTok.whiteSpace lexer
lexeme = PTok.lexeme lexer
symbol = PTok.symbol lexer
natural = PTok.natural lexer
parens = PTok.parens lexer
semi = PTok.semi lexer
comma = PTok.comma lexer
identifier= PTok.identifier lexer
reserved = PTok.reserved lexer
operator = PTok.operator lexer
reservedOp= PTok.reservedOp lexer
lchar = lexeme.char
parseCommand = parse pCommand "(input)"
parseTactic = parse (pTactic >>= return . Tac) "(input)"
pCommand :: Parser Command
pCommand = do reserved "theorem"; n <- iName; lchar ':'; ty <- pTerm
return (Theorem n ty)
<|> do reserved "eval"; tm <- pTerm
return (Eval tm)
<|> do reserved "print"; n <- iName; return (Print n)
<|> do reserved "quit";
return Quit
pTactic :: Parser (Elab ())
pTactic = do reserved "attack"; return attack
<|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
return (claim n ty)
<|> do reserved "regret"; return regret
<|> do reserved "exact"; tm <- pTerm; return (exact tm)
<|> do reserved "fill"; tm <- pTerm; return (fill tm)
<|> do reserved "apply"; tm <- pTerm; args <- many pArgType;
return (apply tm args)
<|> do reserved "solve"; return solve
<|> do reserved "compute"; return compute
<|> do reserved "intro"; n <- iName; return (intro n)
<|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm
return (forall n ty)
-- <|> do reserved "arg"; n <- iName; t <- iName; return (arg n t)
<|> do reserved "patvar"; n <- iName; return (patvar n)
-- <|> do reserved "patarg"; n <- iName; t <- iName; return (patarg n t)
<|> do reserved "eval"; t <- pTerm; return (eval_in t)
<|> do reserved "check"; t <- pTerm; return (check_in t)
<|> do reserved "focus"; n <- iName; return (focus n)
<|> do reserved "state"; return proofstate
<|> do reserved "undo"; return undo
<|> do reserved "qed"; return qed
pArgType :: Parser Bool
pArgType = do lchar '_'; return True -- implicit (machine fills in)
<|> do lchar '?'; return False -- user fills in