git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/src/Core/ProofShell.hs
79 lines 3.4 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
14import Idris.AbsSyntaxTree (Idris)
16import Util.Pretty
18data ShellState = ShellState
19 { ctxt :: Context,
20 prf :: Maybe ProofState,
21 deferred :: [(Name, ProofState)],
22 exitNow :: Bool
23 }
25initState c = ShellState c Nothing [] False
27processCommand :: Command -> ShellState -> (ShellState, String)
28processCommand (Theorem n ty) state
29 = case check (ctxt state) [] ty of
30 OK (gl, t) ->
31 case isType (ctxt state) [] t of
32 OK _ -> (state { prf = Just (newProof n (ctxt state) gl) }, "")
33 _ -> (state, "Goal is not a type")
34 err -> (state, show err)
35processCommand Quit state = (state { exitNow = True }, "Bye bye")
36processCommand (Eval t) state =
37 case check (ctxt state) [] t of
38 OK (val, ty) ->
39 let nf = normalise (ctxt state) [] val
40 tnf = normalise (ctxt state) [] ty in
41 (state, show nf ++ " : " ++ show ty)
42 err -> (state, show err)
43processCommand (Print n) state =
44 case lookupDef n (ctxt state) of
45 [tm] -> (state, show tm)
46 _ -> (state, "No such name")
47processCommand (Tac e) state
48 | Just ps <- prf state = case execElab () e ps of
49 OK (ES (ps', _) resp _) ->
50 if (not (done ps'))
51 then (state { prf = Just ps' }, resp)
52 else (state { prf = Nothing,
53 ctxt = addToCtxt (thname ps')
54 (pterm ps')
55 (ptype ps')
56 (context ps') }, resp)
57 err -> (state, show err)
58 | otherwise = (state, "No proof in progress")
60runShell :: ShellState -> Idris ShellState
61runShell st = runInputT defaultSettings $ runShell' st
62 where
63 runShell' st = do (prompt, parser) <-
64 maybe (return ("TT# ", parseCommand))
65 (\st -> do outputStrLn . render . pretty $ st
66 return (show (thname st) ++ "# ", parseTactic))
67 (prf st)
68 x <- getInputLine prompt
69 cmd <- case x of
70 Nothing -> return $ Right Quit
71 Just input -> return (parser input)
72 case cmd of
73 Left err -> do outputStrLn (show err)
74 runShell' st
75 Right cmd -> do let (st', r) = processCommand cmd st
76 outputStrLn r
77 if (not (exitNow st')) then runShell' st'
78 else return st'