@@ -6,7 +6,7 @@ module Idris.Prover (prover, showProof, showRunElab) where
6-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
6-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
7import Prelude (Eq(..), Show(..),
7import Prelude (Eq(..), Show(..),
8 Bool(..), Either(..), Maybe(..), String,
8 Bool(..), Either(..), Maybe(..), String,
9− (.), ($), (++), (||),
9+ (.), ($), (++), (||), (&&),
10 concatMap, id, elem, error, fst, flip, foldl, foldr, init,
10 concatMap, id, elem, error, fst, flip, foldl, foldr, init,
11 length, lines, map, not, null, repeat, reverse, tail, zip)
11 length, lines, map, not, null, repeat, reverse, tail, zip)
@@ -149,16 +149,16 @@ elabStep st e =
149 return (res, ctxt)
149 return (res, ctxt)
150 ((_,_,_,_,e,_,_):_) -> lift $ Error e
150 ((_,_,_,_,e,_,_):_) -> lift $ Error e
152−dumpState :: IState -> [(Name, Type, Term)] -> ProofState -> Idris ()
152+dumpState :: IState -> Bool -> [(Name, Type, Term)] -> ProofState -> Idris ()
153−dumpState ist menv ps | [] <- holes ps =
153+dumpState ist inElab menv ps | [] <- holes ps =
154 do let nm = thname ps
154 do let nm = thname ps
155 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
155 rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
156 iputGoal rendered
156 iputGoal rendered
157−dumpState ist menv ps | (h : hs) <- holes ps = do
157+dumpState ist inElab menv ps | (h : hs) <- holes ps = do
158 let OK ty = goalAtFocus ps
158 let OK ty = goalAtFocus ps
159 let OK env = envAtFocus ps
159 let OK env = envAtFocus ps
160 let state = prettyOtherGoals hs <> line <>
160 let state = prettyOtherGoals hs <> line <>
161− prettyAssumptions ty env <> line <>
161+ prettyAssumptions inElab ty env <> line <>
162 prettyMetaValues (reverse menv) <>
162 prettyMetaValues (reverse menv) <>
163 prettyGoal (zip (assumptionNames env) (repeat False)) ty
163 prettyGoal (zip (assumptionNames env) (repeat False)) ty
164 rendered <- iRender state
164 rendered <- iRender state
@@ -176,18 +176,18 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
176 assumptionNames :: Env -> [Name]
176 assumptionNames :: Env -> [Name]
177 assumptionNames = map fst
177 assumptionNames = map fst
179− prettyPs :: Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
179+ prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation
180− prettyPs g bnd [] = empty
180+ prettyPs all g bnd [] = empty
181− prettyPs g bnd ((n@(MN _ r), _) : bs)
181+ prettyPs all g bnd ((n@(MN _ r), _) : bs)
182− | r == txt "rewrite_rule" = prettyPs g ((n, False):bnd) bs
182+ | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs
183− prettyPs g bnd ((n@(MN _ _), _) : bs)
183+ prettyPs all g bnd ((n@(MN _ _), _) : bs)
184− | not (n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs g bnd bs
184+ | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs
185− prettyPs g bnd ((n, Let t v) : bs) =
185+ prettyPs all g bnd ((n, Let t v) : bs) =
186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
187− align (tPretty bnd t) <> prettyPs g ((n, False):bnd) bs
187+ align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs
188− prettyPs g bnd ((n, b) : bs) =
188+ prettyPs all g bnd ((n, b) : bs) =
189 line <> bindingOf n False <+> colon <+>
189 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
192 prettyMetaValues [] = empty
192 prettyMetaValues [] = empty
193 prettyMetaValues mvs =
193 prettyMetaValues mvs =
@@ -214,12 +214,12 @@ dumpState ist menv ps | (h : hs) <- holes ps = do
214 text "---------- Goal: ----------" <$$>
214 text "---------- Goal: ----------" <$$>
215 bindingOf h False <+> colon <+> align (prettyG bnd ty)
215 bindingOf h False <+> colon <+> align (prettyG bnd ty)
217− prettyAssumptions g env =
217+ prettyAssumptions inElab g env =
218 if length env == 0 then
218 if length env == 0 then
221 text "---------- Assumptions: ----------" <>
221 text "---------- Assumptions: ----------" <>
222− nest nestingSize (prettyPs g [] $ reverse env)
222+ nest nestingSize (prettyPs inElab g [] $ reverse env)
224 prettyOtherGoals hs =
224 prettyOtherGoals hs =
225 if length hs == 0 then
225 if length hs == 0 then
@@ -277,7 +277,7 @@ undoElab prf env st (h:hs) = do (prf', env', st') <- undoStep prf env st h
277elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
277elabloop :: Name -> Bool -> String -> [String] -> ElabState EState -> [ElabShellHistory] -> Maybe History -> [(Name, Type, Term)] -> Idris (Term, [String])
278elabloop fn d prompt prf e prev h env
278elabloop fn d prompt prf e prev h env
279 = do ist <- getIState
279 = do ist <- getIState
280− when d $ dumpState ist env (proof e)
280+ when d $ dumpState ist True env (proof e)
281 (x, h') <-
281 (x, h') <-
282 case idris_outputmode ist of
282 case idris_outputmode ist of
283 RawOutput _ ->
283 RawOutput _ ->
@@ -394,7 +394,7 @@ ploop :: Name -> Bool -> String -> [String] -> ElabState EState -> Maybe History
394ploop fn d prompt prf e h
394ploop fn d prompt prf e h
395 = do i <- getIState
395 = do i <- getIState
396 let autoSolve = opt_autoSolve (idris_options i)
396 let autoSolve = opt_autoSolve (idris_options i)
397− when d $ dumpState i [] (proof e)
397+ when d $ dumpState i False [] (proof e)
398 (x, h') <-
398 (x, h') <-
399 case idris_outputmode i of
399 case idris_outputmode i of
400 RawOutput _ ->
400 RawOutput _ ->