git.iko.soy/Idris-dev
on master help sign in
Removing matching on PS
ba51147Edwin Brady
src/Idris/Core/ProofState.hs+12−8
compare with master
unifiedsplit
@@ -93,10 +93,12 @@ data Tactic = Attack
93-- Some utilites on proof and tactic states
93-- Some utilites on proof and tactic states
94
94
95instance Show ProofState where
95instance Show ProofState where
96− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
96+ show ps | [] <- holes ps
97− = show nm ++ ": no more goals"
97+ = show (thname ps) ++ ": no more goals"
98− show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ _ ctxt _ _ _ _ _)
98+ show ps | (h : hs) <- holes ps
99+ = let tm = pterm ps
100+ nm = thname ps
99− = let OK g = goal (Just h) tm
101+ OK g = goal (Just h) tm
100 wkenv = premises g in
102 wkenv = premises g in
101 "Other goals: " ++ show hs ++ "\n" ++
103 "Other goals: " ++ show hs ++ "\n" ++
102 showPs wkenv (reverse wkenv) ++ "\n" ++
104 showPs wkenv (reverse wkenv) ++ "\n" ++
@@ -118,10 +120,12 @@ instance Show ProofState where
118 showG ps b = showEnv ps (binderTy b)
120 showG ps b = showEnv ps (binderTy b)
119
121
120instance Pretty ProofState OutputAnnotation where
122instance Pretty ProofState OutputAnnotation where
121− pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
123+ pretty ps | [] <- holes ps =
122− pretty nm <+> colon <+> text " no more goals."
124+ pretty (thname ps) <+> colon <+> text " no more goals."
123− pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ _ ctxt _ _ _ _ _) =
125+ pretty ps | (h : hs) <- holes ps =
126+ let tm = pterm ps
124− let OK g = goal (Just h) tm in
127+ OK g = goal (Just h) tm
128+ nm = thname ps in
125 let wkEnv = premises g in
129 let wkEnv = premises g in
126 text "Other goals" <+> colon <+> pretty hs <+>
130 text "Other goals" <+> colon <+> pretty hs <+>
127 prettyPs wkEnv (reverse wkEnv) <+>
131 prettyPs wkEnv (reverse wkEnv) <+>
src/Idris/Prover.hs+7−3
@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
1module Idris.Prover where
2module Idris.Prover where
2
3
3import Idris.Core.Elaborate hiding (Tactic(..))
4import Idris.Core.Elaborate hiding (Tactic(..))
@@ -114,10 +115,11 @@ elabStep st e = case runStateT eCheck st of
114 ((_,_,_,_,e,_,_):_) -> lift $ Error e
115 ((_,_,_,_,e,_,_):_) -> lift $ Error e
115
116
116dumpState :: IState -> ProofState -> Idris ()
117dumpState :: IState -> ProofState -> Idris ()
117−dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
118+dumpState ist ps | [] <- holes ps =
119+ do let nm = thname ps
118− do rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
120+ rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
119 iputGoal rendered
121 iputGoal rendered
120−dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ _ ctxt _ _ _ _ _) = do
122+dumpState ist ps | (h : hs) <- holes ps = do
121 let OK ty = goalAtFocus ps
123 let OK ty = goalAtFocus ps
122 let OK env = envAtFocus ps
124 let OK env = envAtFocus ps
123 let state = prettyOtherGoals hs <> line <>
125 let state = prettyOtherGoals hs <> line <>
@@ -127,6 +129,8 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ _ ctxt _ _ _ _
127 iputGoal rendered
129 iputGoal rendered
128
130
129 where
131 where
132+ (h : hs) = holes ps -- apparently the pattern guards don't give us this
133+
130 ppo = ppOptionIst ist
134 ppo = ppOptionIst ist
131
135
132 tPretty bnd t = annotate (AnnTerm bnd t) .
136 tPretty bnd t = annotate (AnnTerm bnd t) .