@@ -1,3 +1,4 @@
1+
12{-# LANGUAGE PatternGuards #-}
23module Idris.Prover (prover, showProof, showRunElab) where
34
@@ -5,7 +6,7 @@ module Idris.Prover (prover, showProof, showRunElab) where
56-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
67import Prelude (Eq(..), Show(..),
78 Bool(..), Either(..), Maybe(..), String,
8− (.), ($), (++), (||),
9+ (.), ($), (++), (||), (&&),
910 concatMap, id, elem, error, fst, flip, foldl, foldr, init,
1011 length, lines, map, not, null, repeat, reverse, tail, zip)
1112
@@ -89,7 +90,10 @@ prove mode opt ctxt lit n ty
8990 (tm, prf) <-
9091 if mode
9192 then elabloop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) [] Nothing []
92− else ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
93+ else do iputStrLn $ "Warning: this interactive prover is deprecated and will be removed " ++
94+ "in a future release. Please see :elab for a similar feature that "++
95+ "will replace it."
96+ ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
9397 logLvl 1 $ "Adding " ++ show tm
9498 i <- getIState
9599 let shower = if mode
@@ -145,16 +149,16 @@ elabStep st e =
145149 return (res, ctxt)
146150 ((_,_,_,_,e,_,_):_) -> lift $ Error e
147151
148−dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
149−dumpState ist menv ps | [] <- holes ps =
152+dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()
153+dumpState ist inElab menv ps | [] <- holes ps =
150154 do let nm = thname ps
151155 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
152156 iputGoal rendered
153−dumpState ist menv ps | (h : hs) <- holes ps = do
157+dumpState ist inElab menv ps | (h : hs) <- holes ps = do
154158 let OK ty = goalAtFocus ps
155159 let OK env = envAtFocus ps
156160 let state = prettyOtherGoals hs <> line <>
157− prettyAssumptions ty env <> line <>
161+ prettyAssumptions inElab ty env <> line <>
158162 prettyMetaValues (reverse menv) <>
159163 prettyGoal (zip (assumptionNames env) (repeat False)) ty
160164 rendered <- iRender state
@@ -172,18 +176,18 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
172176 assumptionNames :: Env -> [Name]
173177 assumptionNames = map fst
174178
175− prettyPs :: Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
176− prettyPs g bnd [] = empty
177− prettyPs g bnd ((n@(MN _ r), _) : bs)
178− | r == txt "rewrite_rule" = prettyPs g ((n, False):bnd) bs
179− prettyPs g bnd ((n@(MN _ _), _) : bs)
180− | not (n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs g bnd bs
181− prettyPs g bnd ((n, Let t v) : bs) =
179+ prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
180+ prettyPs all g bnd [] = empty
181+ prettyPs all g bnd ((n@(MN _ r), _) : bs)
182+ | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs
183+ prettyPs all g bnd ((n@(MN _ _), _) : bs)
184+ | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs
185+ prettyPs all g bnd ((n, Let t v) : bs) =
182186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
183− align (tPretty bnd t) <> prettyPs g ((n, False):bnd) bs
184− prettyPs g bnd ((n, b) : bs) =
187+ align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs
188+ prettyPs all g bnd ((n, b) : bs) =
185189 line <> bindingOf n False <+> colon <+>
186− align (tPretty bnd (binderTy b)) <> prettyPs g ((n, False):bnd) bs
190+ align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs
187191
188192 prettyMetaValues [] = empty
189193 prettyMetaValues mvs =
@@ -210,12 +214,12 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
210214 text "---------- Goal: ----------" <$$>
211215 bindingOf h False <+> colon <+> align (prettyG bnd ty)
212216
213− prettyAssumptions g env =
217+ prettyAssumptions inElab g env =
214218 if length env == 0 then
215219 empty
216220 else
217221 text "---------- Assumptions: ----------" <>
218− nest nestingSize (prettyPs g [] $ reverse env)
222+ nest nestingSize (prettyPs inElab g [] $ reverse env)
219223
220224 prettyOtherGoals hs =
221225 if length hs == 0 then
@@ -273,7 +277,7 @@ undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
273277elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
274278elabloop fn d prompt prf e prev h env
275279 = do ist <- getIState
276− when d $ dumpState ist env (proof e)
280+ when d $ dumpState ist True env (proof e)
277281 (x, h') <-
278282 case idris_outputmode ist of
279283 RawOutput _ ->
@@ -390,7 +394,7 @@ ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History
390394ploop fn d prompt prf e h
391395 = do i <- getIState
392396 let autoSolve = opt_autoSolve (idris_options i)
393− when d $ dumpState i [] (proof e)
397+ when d $ dumpState i False [] (proof e)
394398 (x, h') <-
395399 case idris_outputmode i of
396400 RawOutput _ ->