git.iko.soy/Idris-dev
on bb6bba2 help sign in
Idris-dev/src/ShellParser.hs
57 lines 1.8 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 "quit";
43 return Quit
45pTactic :: Parser Tactic
46pTactic = do reserved "attack"; return Attack
47 <|> do reserved "claim"; n <- iname; lchar ':'; ty <- pTerm
48 return (Claim n ty)
49 <|> do reserved "fill"; tm <- pTerm; return (Fill tm)
50 <|> do reserved "regret"; return Regret
51 <|> do reserved "solve"; return Solve
52 <|> do reserved "intro"; n <- iname; return (Intro n)
53 <|> do reserved "state"; return ProofState
54 <|> do reserved "qed"; return QED
56iname :: Parser Name
57iname = identifier >>= (\n -> return (UN [n]))