4ae829c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1450 from david-christiansen/dont-show-mn-in-proof

Don't show irrelevant MNs in prover

commit4ae829cb7a99b21aa492c111dccb6ac5968f9aaf authorDavid Christiansen <david@davidchristiansen.dk> dateFri 1 Aug 2014, 07:20 (12 years ago) parentc578372 8f7d848

2 files changed+6

compare with master

unifiedsplit

CHANGELOG+1 src/Idris/Prover.hs+5

CHANGELOG+1

@@ -2,6 +2,7 @@ New in 0.9.15:

22--------------

33* Two new tactics: skip and fail. Skip does nothing, and fail takes a string as an argument and produces it as an error.

44* 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

67New in 0.9.14:

78--------------

src/Idris/Prover.hs+5

@@ -140,6 +140,8 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

140140 prettyPs bnd [] = empty

141141 prettyPs bnd ((n@(MN _ r), _) : bs)

142142 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs

143+ prettyPs bnd ((n@(MN _ _), _) : bs)

144+ | not (n `elem` freeEnvNames bs) = prettyPs bnd bs

143145 prettyPs bnd ((n, Let t v) : bs) =

144146 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

145147 align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs

@@ -168,6 +170,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

168170 text "---------- Other goals: ----------" <$$>

169171 nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)

170172

173+ freeEnvNames :: Env -> [Name]

174+ freeEnvNames = foldl (++) [] . map (\(n, b) -> freeNames (Bind n b Erased))

175+

171176lifte :: ElabState [PDecl] -> ElabD a -> Idris a

172177lifte st e = do (v, _) <- elabStep st e

173178 return v