git.iko.soy/Idris-dev
on master help sign in
Removing matching on PS

This makes it less boring to modify what's in the proof state...

commitba51147137f7b7a2f79a0886c68468bedf4601cf authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 20 Dec 2014, 12:31 (12 years ago) parentc506e9f
2 files changed+19−11
compare with master
unifiedsplit
src/Idris/Core/ProofState.hs+12−8 src/Idris/Prover.hs+7−3
src/Idris/Core/ProofState.hs+12−8
@@ -93,10 +93,12 @@ data Tactic = Attack
9393-- Some utilites on proof and tactic states
9494
9595instance Show ProofState where
96− show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _)
97− = show nm ++ ": no more goals"
98− show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ _ ctxt _ _ _ _ _)
99− = let OK g = goal (Just h) tm
96+ show ps | [] <- holes ps
97+ = show (thname ps) ++ ": no more goals"
98+ show ps | (h : hs) <- holes ps
99+ = let tm = pterm ps
100+ nm = thname ps
101+ OK g = goal (Just h) tm
100102 wkenv = premises g in
101103 "Other goals: " ++ show hs ++ "\n" ++
102104 showPs wkenv (reverse wkenv) ++ "\n" ++
@@ -118,10 +120,12 @@ instance Show ProofState where
118120 showG ps b = showEnv ps (binderTy b)
119121
120122instance Pretty ProofState OutputAnnotation where
121− pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
122− pretty nm <+> colon <+> text " no more goals."
123− pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ _ ctxt _ _ _ _ _) =
124− let OK g = goal (Just h) tm in
123+ pretty ps | [] <- holes ps =
124+ pretty (thname ps) <+> colon <+> text " no more goals."
125+ pretty ps | (h : hs) <- holes ps =
126+ let tm = pterm ps
127+ OK g = goal (Just h) tm
128+ nm = thname ps in
125129 let wkEnv = premises g in
126130 text "Other goals" <+> colon <+> pretty hs <+>
127131 prettyPs wkEnv (reverse wkEnv) <+>
src/Idris/Prover.hs+7−3
@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
12module Idris.Prover where
23
34import Idris.Core.Elaborate hiding (Tactic(..))
@@ -114,10 +115,11 @@ elabStep st e = case runStateT eCheck st of
114115 ((_,_,_,_,e,_,_):_) -> lift $ Error e
115116
116117dumpState :: IState -> ProofState -> Idris ()
117−dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
118− do rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
118+dumpState ist ps | [] <- holes ps =
119+ do let nm = thname ps
120+ rendered <- iRender $ prettyName True False [] nm <> colon <+> text "No more goals."
119121 iputGoal rendered
120−dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ _ ctxt _ _ _ _ _) = do
122+dumpState ist ps | (h : hs) <- holes ps = do
121123 let OK ty = goalAtFocus ps
122124 let OK env = envAtFocus ps
123125 let state = prettyOtherGoals hs <> line <>
@@ -127,6 +129,8 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ _ ctxt _ _ _ _
127129 iputGoal rendered
128130
129131 where
132+ (h : hs) = holes ps -- apparently the pattern guards don't give us this
133+
130134 ppo = ppOptionIst ist
131135
132136 tPretty bnd t = annotate (AnnTerm bnd t) .