@@ -5,7 +5,7 @@ module Idris.Prover (prover, showProof, showRunElab) where
55-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
66import Prelude (Eq(..), Show(..),
77 Bool(..), Either(..), Maybe(..), String,
8− (.), ($), (++),
8+ (.), ($), (++), (||),
99 concatMap, id, elem, error, fst, flip, foldl, foldr, init,
1010 length, lines, map, not, null, repeat, reverse, tail, zip)
1111
@@ -150,7 +150,7 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
150150 let OK ty = goalAtFocus ps
151151 let OK env = envAtFocus ps
152152 let state = prettyOtherGoals hs <> line <>
153− prettyAssumptions env <> line <>
153+ prettyAssumptions ty env <> line <>
154154 prettyMetaValues (reverse menv) <>
155155 prettyGoal (zip (assumptionNames env) (repeat False)) ty
156156 rendered <- iRender state
@@ -168,18 +168,18 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
168168 assumptionNames :: Env -> [Name]
169169 assumptionNames = map fst
170170
171− prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
172− prettyPs bnd [] = empty
173− prettyPs bnd ((n@(MN _ r), _) : bs)
174− | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
175− prettyPs bnd ((n@(MN _ _), _) : bs)
176− | not (n `elem` freeEnvNames bs) = prettyPs bnd bs
177− prettyPs bnd ((n, Let t v) : bs) =
171+ prettyPs :: Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
172+ prettyPs g bnd [] = empty
173+ prettyPs g bnd ((n@(MN _ r), _) : bs)
174+ | r == txt "rewrite_rule" = prettyPs g ((n, False):bnd) bs
175+ prettyPs g bnd ((n@(MN _ _), _) : bs)
176+ | not (n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs g bnd bs
177+ prettyPs g bnd ((n, Let t v) : bs) =
178178 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
179− align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs
180− prettyPs bnd ((n, b) : bs) =
179+ align (tPretty bnd t) <> prettyPs g ((n, False):bnd) bs
180+ prettyPs g bnd ((n, b) : bs) =
181181 line <> bindingOf n False <+> colon <+>
182− align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
182+ align (tPretty bnd (binderTy b)) <> prettyPs g ((n, False):bnd) bs
183183
184184 prettyMetaValues [] = empty
185185 prettyMetaValues mvs =
@@ -196,6 +196,9 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
196196
197197 kwd = annotate AnnKeyword . text
198198
199+ goalNames (Guess t v) = freeNames t ++ freeNames v
200+ goalNames b = freeNames (binderTy b)
201+
199202 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
200203 prettyG bnd b = tPretty bnd $ binderTy b
201204
@@ -203,12 +206,12 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
203206 text "---------- Goal: ----------" <$$>
204207 bindingOf h False <+> colon <+> align (prettyG bnd ty)
205208
206− prettyAssumptions env =
209+ prettyAssumptions g env =
207210 if length env == 0 then
208211 empty
209212 else
210213 text "---------- Assumptions: ----------" <>
211− nest nestingSize (prettyPs [] $ reverse env)
214+ nest nestingSize (prettyPs g [] $ reverse env)
212215
213216 prettyOtherGoals hs =
214217 if length hs == 0 then