@@ -6,7 +6,7 @@ module Idris.Prover (prover, showProof, showRunElab) where
66-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
77import Prelude (Eq(..), Show(..),
88 Bool(..), Either(..), Maybe(..), String,
9− (.), ($), (++), (||),
9+ (.), ($), (++), (||), (&&),
1010 concatMap, id, elem, error, fst, flip, foldl, foldr, init,
1111 length, lines, map, not, null, repeat, reverse, tail, zip)
1212
@@ -149,16 +149,16 @@ elabStep st e =
149149 return (res, ctxt)
150150 ((_,_,_,_,e,_,_):_) -> lift $ Error e
151151
152−dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
153−dumpState ist menv ps | [] <- holes ps =
152+dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()
153+dumpState ist inElab menv ps | [] <- holes ps =
154154 do let nm = thname ps
155155 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
156156 iputGoal rendered
157−dumpState ist menv ps | (h : hs) <- holes ps = do
157+dumpState ist inElab menv ps | (h : hs) <- holes ps = do
158158 let OK ty = goalAtFocus ps
159159 let OK env = envAtFocus ps
160160 let state = prettyOtherGoals hs <> line <>
161− prettyAssumptions ty env <> line <>
161+ prettyAssumptions inElab ty env <> line <>
162162 prettyMetaValues (reverse menv) <>
163163 prettyGoal (zip (assumptionNames env) (repeat False)) ty
164164 rendered <- iRender state
@@ -176,18 +176,18 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
176176 assumptionNames :: Env -> [Name]
177177 assumptionNames = map fst
178178
179− prettyPs :: Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
180− prettyPs g bnd [] = empty
181− prettyPs g bnd ((n@(MN _ r), _) : bs)
182− | r == txt "rewrite_rule" = prettyPs g ((n, False):bnd) bs
183− prettyPs g bnd ((n@(MN _ _), _) : bs)
184− | not (n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs g bnd bs
185− 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) =
186186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
187− align (tPretty bnd t) <> prettyPs g ((n, False):bnd) bs
188− 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) =
189189 line <> bindingOf n False <+> colon <+>
190− align (tPretty bnd (binderTy b)) <> prettyPs g ((n, False):bnd) bs
190+ align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs
191191
192192 prettyMetaValues [] = empty
193193 prettyMetaValues mvs =
@@ -214,12 +214,12 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
214214 text "---------- Goal: ----------" <$$>
215215 bindingOf h False <+> colon <+> align (prettyG bnd ty)
216216
217− prettyAssumptions g env =
217+ prettyAssumptions inElab g env =
218218 if length env == 0 then
219219 empty
220220 else
221221 text "---------- Assumptions: ----------" <>
222− nest nestingSize (prettyPs g [] $ reverse env)
222+ nest nestingSize (prettyPs inElab g [] $ reverse env)
223223
224224 prettyOtherGoals hs =
225225 if length hs == 0 then
@@ -277,7 +277,7 @@ undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
277277elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
278278elabloop fn d prompt prf e prev h env
279279 = do ist <- getIState
280− when d $ dumpState ist env (proof e)
280+ when d $ dumpState ist True env (proof e)
281281 (x, h') <-
282282 case idris_outputmode ist of
283283 RawOutput _ ->
@@ -394,7 +394,7 @@ ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History
394394ploop fn d prompt prf e h
395395 = do i <- getIState
396396 let autoSolve = opt_autoSolve (idris_options i)
397− when d $ dumpState i [] (proof e)
397+ when d $ dumpState i False [] (proof e)
398398 (x, h') <-
399399 case idris_outputmode i of
400400 RawOutput _ ->