git.iko.soy/Idris-dev
on 546e9f5 help sign in
Idris-dev/src/ShellParser.hs
64 lines 2.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module ShellParser(parseCommand, parseTactic) where
5import Core
6import Elaborate
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 (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 "fill"; tm <- pTerm; return (fill tm)
52 <|> do reserved "unify"; tm <- pTerm; return (unify_fill tm)
53 <|> do reserved "solve"; return solve
54 <|> do reserved "compute"; return compute
55 <|> do reserved "intro"; n <- iName; return (intro n)
56 <|> do reserved "forall"; n <- iName; lchar ':'; ty <- pTerm
57 return (forall n ty)
58 <|> do reserved "eval"; t <- pTerm; return (eval_in t)
59 <|> do reserved "check"; t <- pTerm; return (check_in t)
60 <|> do reserved "focus"; n <- iName; return (focus n)
61 <|> do reserved "state"; return proofstate
62 <|> do reserved "qed"; return qed