git.iko.soy/Idris-dev
on 63afafa help sign in
Idris-dev/src/Core/ProofShell.hs
73 lines 3.2 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3module Core.ProofShell where
5import Core.Typecheck
6import Core.Evaluate
7import Core.TT
8import Core.ShellParser
9import Core.Elaborate
11import Control.Monad.State
12import System.Console.Haskeline
14data ShellState = ShellState
15 { ctxt :: Context,
16 prf :: Maybe ProofState,
17 deferred :: [(Name, ProofState)],
18 exitNow :: Bool
19 }
21initState c = ShellState c Nothing [] False
23processCommand :: Command -> ShellState -> (ShellState, String)
24processCommand (Theorem n ty) state
25 = case check (ctxt state) [] ty of
26 OK (gl, t) ->
27 case isSet (ctxt state) [] t of
28 OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
29 _ -> (state, "Goal is not a type")
30 err -> (state, show err)
31processCommand Quit state = (state { exitNow = True }, "Bye bye")
32processCommand (Eval t) state =
33 case check (ctxt state) [] t of
34 OK (val, ty) ->
35 let nf = normalise (ctxt state) [] val
36 tnf = normalise (ctxt state) [] ty in
37 (state, show nf ++ " : " ++ show ty)
38 err -> (state, show err)
39processCommand (Print n) state =
40 case lookupDef Nothing n (ctxt state) of
41 [tm] -> (state, show tm)
42 _ -> (state, "No such name")
43processCommand (Tac e) state
44 | Just ps <- prf state = case execElab () e ps of
45 OK (ES (ps', _) resp _) ->
46 if (not (done ps'))
47 then (state { prf = Just ps' }, resp)
48 else (state { prf = Nothing,
49 ctxt = addToCtxt (thname ps')
50 (pterm ps')
51 (ptype ps')
52 (context ps') }, resp)
53 err -> (state, show err)
54 | otherwise = (state, "No proof in progress")
56runShell :: ShellState -> InputT IO ShellState
57runShell st = do (prompt, parser) <-
58 maybe (return ("TT# ", parseCommand))
59 (\st -> do outputStrLn (show st)
60 return (show (thname st) ++ "# ", parseTactic))
61 (prf st)
62 x <- getInputLine prompt
63 cmd <- case x of
64 Nothing -> return $ Right Quit
65 Just input -> return (parser input)
66 case cmd of
67 Left err -> do outputStrLn (show err)
68 runShell st
69 Right cmd -> do let (st', r) = processCommand cmd st
70 outputStrLn r
71 if (not (exitNow st')) then runShell st'
72 else return st'