git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1450 from david-christiansen/dont-show-mn-in-proof
4ae829cDavid Christiansen
CHANGELOG+1
compare with master
unifiedsplit
@@ -2,6 +2,7 @@ New in 0.9.15:
2--------------
2--------------
3* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.
3* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.
4* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer.
4* Corresponding reflected tactics Skip and Fail. Reflected Fail takes a list of ErrorReportParts as an argument, like error handlers produce, allowing access to the pretty-printer.
5+* Stop showing irrelevant and inaccessible internal names in the interactive prover
5
6
6New in 0.9.14:
7New in 0.9.14:
7--------------
8--------------
src/Idris/Prover.hs+5
@@ -140,6 +140,8 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
140 prettyPs bnd [] = empty
140 prettyPs bnd [] = empty
141 prettyPs bnd ((n@(MN _ r), _) : bs)
141 prettyPs bnd ((n@(MN _ r), _) : bs)
142 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
142 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
143+ prettyPs bnd ((n@(MN _ _), _) : bs)
144+ | not (n `elem` freeEnvNames bs) = prettyPs bnd bs
143 prettyPs bnd ((n, Let t v) : bs) =
145 prettyPs bnd ((n, Let t v) : bs) =
144 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
146 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
145 align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs
147 align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs
@@ -168,6 +170,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
168 text "---------- Other goals: ----------" <$$>
170 text "---------- Other goals: ----------" <$$>
169 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
171 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
170
172
173+ freeEnvNames :: Env -> [Name]
174+ freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))
175+
171lifte :: ElabState [PDecl] -> ElabD a -> Idris a
176lifte :: ElabState [PDecl] -> ElabD a -> Idris a
172lifte st e = do (v, _) <- elabStep st e
177lifte st e = do (v, _) <- elabStep st e
173 return v
178 return v