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