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