git.iko.soy/Idris-dev
on 5dadd08 help sign in
Idris-dev/src/ProofShell.hs
73 lines 3.2 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 deferred :: [(Name, ProofState)],
17 exitNow :: Bool
18 }
20initState c = State c Nothing [] False
22processCommand :: Command -> ShellState -> (ShellState, String)
23processCommand (Theorem n ty) state
24 = case check (ctxt state) [] ty of
25 OK (gl, t) ->
26 case isSet (ctxt state) [] t of
27 OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
28 _ -> (state, "Goal is not a type")
29 err -> (state, show err)
30processCommand Quit state = (state { exitNow = True }, "Bye bye")
31processCommand (Eval t) state =
32 case check (ctxt state) [] t of
33 OK (val, ty) ->
34 let nf = normalise (ctxt state) [] val
35 tnf = normalise (ctxt state) [] ty in
36 (state, show nf ++ " : " ++ show ty)
37 err -> (state, show err)
38processCommand (Print n) state =
39 case lookupDef n (ctxt state) of
40 Just tm -> (state, show tm)
41 Nothing -> (state, "No such name")
42processCommand (Tac e) state
43 | Just ps <- prf state = case runElab e ps of
44 OK (ps', resp) ->
45 if (not (done ps'))
46 then (state { prf = Just ps' }, resp)
47 else (state { prf = Nothing,
48 ctxt = addToCtxt (thname ps')
49 (pterm ps')
50 (ptype ps')
51 (context ps') }, resp)
52 err -> (state, show err)
53 | otherwise = (state, "No proof in progress")
55runShell :: ShellState -> IO ShellState
56runShell st = do (prompt, parser) <-
57 maybe (return ("> ", parseCommand))
58 (\st -> do print st
59 return (show (thname st) ++ "> ", parseTactic))
60 (prf st)
61 x <- readline prompt
62 cmd <- case x of
63 Nothing -> return $ Right Quit
64 Just input -> do addHistory input
65 return (parser input)
66 case cmd of
67 Left err -> do putStrLn (show err)
68 runShell st
69 Right cmd -> do let (st', r) = processCommand cmd st
70 putStrLn r
71 if (not (exitNow st')) then runShell st'
72 else return st'