git.iko.soy/Idris-dev
on 6923ac1 help sign in
Idris-dev/src/ProofShell.hs
52 lines 2.1 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 = case processTactic t ps of
30 OK (ps', resp) -> (state { prf = Just ps' }, resp)
31 err -> (state, show err)
32 | otherwise = (state, "No proof in progress")
34runShell :: ShellState -> IO ShellState
35runShell st = do (prompt, parser) <-
36 maybe (return ("> ", parseCommand))
37 (\st -> do print st
38 return (show (thname st) ++ "> ", parseTactic))
39 (prf st)
40 x <- readline prompt
41 cmd <- case x of
42 Nothing -> return $ Right Quit
43 Just input -> do addHistory input
44 return (parser input)
45 case cmd of
46 Left err -> do putStrLn (show err)
47 runShell st
48 Right cmd -> do let (st', r) = processCommand cmd st
49 putStrLn r
50 if (not (exitNow st')) then runShell st'
51 else return st'