git.iko.soy/Idris-dev
on 56309a5 help sign in
Idris-dev/src/ProofShell.hs
65 lines 2.8 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 (Eval t) state =
29 case check (ctxt state) [] t of
30 OK (val, _) ->
31 let nf = normalise (ctxt state) [] val in
32 (state, show nf)
33 err -> (state, show err)
34processCommand (Tac t) state
35 | Just ps <- prf state = case processTactic t ps of
36 OK (ps', resp) ->
37 if (not (done ps'))
38 then (state { prf = Just ps' }, resp)
39 else (state { prf = Nothing,
40 ctxt = addToCtxt (thname ps')
41 (pterm ps')
42 (ptype ps')
43 (context ps') }, resp)
44 err -> (state, show err)
45 | otherwise = (state, "No proof in progress")
47runShell :: ShellState -> IO ShellState
48runShell st = do (prompt, parser) <-
49 maybe (return ("> ", parseCommand))
50 (\st -> do print st
51 return (show (thname st) ++ "> ", parseTactic))
52 (prf st)
53 x <- readline prompt
54 cmd <- case x of
55 Nothing -> return $ Right Quit
56 Just input -> do addHistory input
57 return (parser input)
58 case cmd of
59 Left err -> do putStrLn (show err)
60 runShell st
61 Right cmd -> do let (st', r) = processCommand cmd st
62 putStrLn r
63 if (not (exitNow st')) then runShell st'
64 else return st'