git.iko.soy/Idris-dev
on 77be0d0 help sign in
Idris-dev/src/ShellParser.hs
61 lines 2.0 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module ShellParser(parseCommand, parseTactic) where
5import Core
6import ProofState
7import 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 Tactic
47pTactic = do reserved "attack"; return Attack
48 <|> do reserved "claim"; n <- iName; lchar ':'; ty <- pTerm
49 return (Claim n ty)
50 <|> do reserved "fill"; tm <- pTerm; return (Fill tm)
51 <|> do reserved "regret"; return Regret
52 <|> do reserved "solve"; return Solve
53 <|> do reserved "compute"; return Compute
54 <|> do reserved "intro"; n <- iName; return (Intro n)
55 <|> do reserved "eval"; t <- pTerm; return (EvalIn t)
56 <|> do reserved "check"; t <- pTerm; return (CheckIn t)
57 <|> do reserved "focus"; n <- iName; return (Focus n)
58 <|> do reserved "state"; return ProofState
59 <|> do reserved "qed"; return QED