git.iko.soy/Idris-dev
on master help sign in
Manually track prover history
bdf07beDavid Christiansen
src/Idris/Prover.hs+13−5
compare with master
unifiedsplit
@@ -16,6 +16,7 @@ import Idris.DataOpts
16import Idris.Completion
16import Idris.Completion
17
17
18import System.Console.Haskeline
18import System.Console.Haskeline
19+import System.Console.Haskeline.History
19import Control.Monad.State
20import Control.Monad.State
20
21
21import Util.Pretty
22import Util.Pretty
@@ -49,7 +50,7 @@ proverSettings e = setComplete (proverCompletion assumptionNames) defaultSetting
49prove :: Context -> Bool -> Name -> Type -> Idris ()
50prove :: Context -> Bool -> Name -> Type -> Idris ()
50prove ctxt lit n ty
51prove ctxt lit n ty
51 = do let ps = initElaborator n ctxt ty
52 = do let ps = initElaborator n ctxt ty
52− (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)
53+ (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing) Nothing
53 iLOG $ "Adding " ++ show tm
54 iLOG $ "Adding " ++ show tm
54 iputStrLn $ showProof lit n prf
55 iputStrLn $ showProof lit n prf
55 i <- getIState
56 i <- getIState
@@ -117,11 +118,18 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a
117lifte st e = do (v, _) <- elabStep st e
118lifte st e = do (v, _) <- elabStep st e
118 return v
119 return v
119
120
120−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])
121+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Maybe History -> Idris (Term, [String])
121−ploop d prompt prf e
122+ploop d prompt prf e h
122 = do i <- getIState
123 = do i <- getIState
123 when d $ liftIO $ dumpState i (proof e)
124 when d $ liftIO $ dumpState i (proof e)
124− x <- runInputT (proverSettings e) $ getInputLine (prompt ++ "> ")
125+ (x, h') <- runInputT (proverSettings e) $
126+ -- Manually track the history so that we can use the proof state
127+ do _ <- case h of
128+ Just history -> putHistory history
129+ Nothing -> return ()
130+ l <- getInputLine (prompt ++ "> ")
131+ h' <- getHistory
132+ return (l, Just h')
125 (cmd, step) <- case x of
133 (cmd, step) <- case x of
126 Nothing -> fail "Abandoned"
134 Nothing -> fail "Abandoned"
127 Just input -> do return (parseTac i input, input)
135 Just input -> do return (parseTac i input, input)
@@ -151,5 +159,5 @@ ploop d prompt prf e
151 return (False, e, False, prf))
159 return (False, e, False, prf))
152 if done then do (tm, _) <- elabStep st get_term
160 if done then do (tm, _) <- elabStep st get_term
153 return (tm, prf')
161 return (tm, prf')
154− else ploop d prompt prf' st
162+ else ploop d prompt prf' st h'
155
163