git.iko.soy/Idris-dev
on 12f9368 help sign in
Idris-dev/src/ProofShell.hs
72 lines 3.1 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module ProofShell where
5import Typecheck
6import Evaluate
7import Core
8import ShellParser
9import Elaborate
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, t) ->
25 case isSet (ctxt state) [] t of
26 OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
27 _ -> (state, "Goal is not a type")
28 err -> (state, show err)
29processCommand Quit state = (state { exitNow = True }, "Bye bye")
30processCommand (Eval t) state =
31 case check (ctxt state) [] t of
32 OK (val, ty) ->
33 let nf = normalise (ctxt state) [] val
34 tnf = normalise (ctxt state) [] ty in
35 (state, show nf ++ " : " ++ show ty)
36 err -> (state, show err)
37processCommand (Print n) state =
38 case lookupDef n (ctxt state) of
39 Just tm -> (state, show tm)
40 Nothing -> (state, "No such name")
41processCommand (Tac e) state
42 | Just ps <- prf state = case runElab e ps of
43 OK (ps', resp) ->
44 if (not (done ps'))
45 then (state { prf = Just ps' }, resp)
46 else (state { prf = Nothing,
47 ctxt = addToCtxt (thname ps')
48 (pterm ps')
49 (ptype ps')
50 (context ps') }, resp)
51 err -> (state, show err)
52 | otherwise = (state, "No proof in progress")
54runShell :: ShellState -> IO ShellState
55runShell st = do (prompt, parser) <-
56 maybe (return ("> ", parseCommand))
57 (\st -> do print st
58 return (show (thname st) ++ "> ", parseTactic))
59 (prf st)
60 x <- readline prompt
61 cmd <- case x of
62 Nothing -> return $ Right Quit
63 Just input -> do addHistory input
64 return (parser input)
65 case cmd of
66 Left err -> do putStrLn (show err)
67 runShell st
68 Right cmd -> do let (st', r) = processCommand cmd st
69 putStrLn r
70 if (not (exitNow st')) then runShell st'
71 else return st'