git.iko.soy/Idris-dev
on ccd64c7 help sign in
Idris-dev/src/ProofShell.hs
49 lines 1.9 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module ProofShell where
5import Typecheck
6import Evaluate
7import Core
8import ProofState
9import ShellParser
11import Control.Monad.State
12import System.Console.Readline
14data ShellState = State { ctxt :: Context,
15 prf :: Maybe ProofState,
16 exitNow :: Bool
17 }
19initState c = State c Nothing False
21processCommand :: Command -> ShellState -> (ShellState, String)
22processCommand (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)
27processCommand Quit state = (state { exitNow = True }, "Bye bye")
28processCommand (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")
33runShell :: ShellState -> IO ShellState
34runShell 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'