git.iko.soy/Idris-dev
on master help sign in
Beginning of proof shell
ccd64c7Edwin Brady
src/Parser.hs → src/CoreParser.hsrenamed+1−1
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module Parser(parseTerm, parseFile, parseDef) where
3+module CoreParser(parseTerm, parseFile, parseDef, pTerm) where
4
4
5import Core
5import Core
6
6
src/ProofShell.hsnew file+49
@@ -0,0 +1,49 @@
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2+
3+module ProofShell where
4+
5+import Typecheck
6+import Evaluate
7+import Core
8+import ProofState
9+import ShellParser
10+
11+import Control.Monad.State
12+import System.Console.Readline
13+
14+data ShellState = State { ctxt :: Context,
15+ prf :: Maybe ProofState,
16+ exitNow :: Bool
17+ }
18+
19+initState c = State c Nothing False
20+
21+processCommand :: Command -> ShellState -> (ShellState, String)
22+processCommand (Theorem n ty) state
23+ = case check (ctxt state) [] ty of
24+ OK (gl, Set _) -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
25+ OK _ -> (state, "Goal is not a type")
26+ err -> (state, show err)
27+processCommand Quit state = (state { exitNow = True }, "Bye bye")
28+processCommand (Tac t) state
29+ | Just ps <- prf state = let (ps', resp) = processTactic t ps in
30+ (state { prf = Just ps' }, resp)
31+ | otherwise = (state, "No proof in progress")
32+
33+runShell :: ShellState -> IO ShellState
34+runShell st = do prompt <- maybe (return "> ")
35+ (\st -> do print st; return (show (thname st) ++ "> "))
36+ (prf st)
37+ x <- readline prompt
38+ cmd <- case x of
39+ Nothing -> return $ Right Quit
40+ Just input -> do addHistory input
41+ return (parseCommand input)
42+ case cmd of
43+ Left err -> do putStrLn (show err)
44+ runShell st
45+ Right cmd -> do let (st', r) = processCommand cmd st
46+ putStrLn r
47+ if (not (exitNow st')) then runShell st'
48+ else return st'
49+
src/ShellParser.hsnew file+51
@@ -0,0 +1,51 @@
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2+
3+module ShellParser(parseCommand, parseTactic) where
4+
5+import Core
6+import ProofState
7+import CoreParser
8+
9+import Text.ParserCombinators.Parsec
10+import Text.ParserCombinators.Parsec.Expr
11+import Text.ParserCombinators.Parsec.Language
12+import qualified Text.ParserCombinators.Parsec.Token as PTok
13+
14+import Debug.Trace
15+
16+type TokenParser a = PTok.TokenParser a
17+
18+lexer :: TokenParser ()
19+lexer = PTok.makeTokenParser haskellDef
20+
21+whiteSpace= PTok.whiteSpace lexer
22+lexeme = PTok.lexeme lexer
23+symbol = PTok.symbol lexer
24+natural = PTok.natural lexer
25+parens = PTok.parens lexer
26+semi = PTok.semi lexer
27+comma = PTok.comma lexer
28+identifier= PTok.identifier lexer
29+reserved = PTok.reserved lexer
30+operator = PTok.operator lexer
31+reservedOp= PTok.reservedOp lexer
32+lchar = lexeme.char
33+
34+parseCommand = parse pCommand "(input)"
35+parseTactic = parse pTactic "(input)"
36+
37+pCommand :: Parser Command
38+pCommand = do reserved "theorem"; n <- identifier; lchar ':'; ty <- pTerm
39+ return (Theorem (UN [n]) ty)
40+ <|> do reserved "eval"; tm <- pTerm
41+ return (Eval tm)
42+ <|> do reserved "quit";
43+ return Quit
44+
45+pTactic :: Parser Tactic
46+pTactic = do reserved "attack"; return Attack
47+ <|> do reserved "claim"; ty <- pTerm; return (Claim ty)
48+ <|> do reserved "try"; tm <- pTerm; return (Try tm)
49+ <|> do reserved "regret"; return Regret
50+ <|> do reserved "solve"; return Solve
51+ <|> do reserved "fill"; tm <- pTerm; return (Fill tm)