@@ -9,6 +9,7 @@ import Core
99import Control.Monad.State
1010import Control.Applicative
1111import Data.List
12+import Debug.Trace
1213
1314data ProofState = PS { thname :: Name,
1415 holes :: [Name], -- holes still to be solved
@@ -36,11 +37,14 @@ data Tactic = Attack
3637 | EvalIn Raw
3738 | CheckIn Raw
3839 | Intro Name
40+ | Focus Name
3941 | ProofState
4042 | QED
4143-- Next: add 'EvalHere' and 'CheckHere' tactics
4244
43−data TacticAction = AddGoal Name
45+data TacticAction = AddGoal Name -- add a new goal, solve immediately
46+ | NextGoal Name -- add a new goal, solve it after current one
47+ | FocusGoal Name -- focus on this goal next
4448 | Solved Name
4549 | Log String
4650
@@ -50,21 +54,23 @@ instance Show ProofState where
5054 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
5155 show (PS nm (h:hs) _ tm _ ctxt _)
5256 = let OK g = goal (Just h) tm ctxt
53− wkenv = weakenEnv (premises g) in
57+ wkenv = premises g in
5458 showPs wkenv (reverse wkenv) ++ "\n" ++
5559 "-------------------------------- (" ++ show nm ++
5660 ") -------\n" ++
5761 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
5862 where showPs env [] = ""
5963 showPs env ((n, b):bs)
60− = " " ++ show n ++ " : " ++ showEnv env (binderTy b) ++
64+ = " " ++ show n ++ " : " ++
65+ showEnv env (normalise ctxt env (binderTy b)) ++
6166 "\n" ++ showPs env bs
62− showG ps (Guess t v) = showEnv ps t ++ " =?= " ++ showEnv ps v
67+ showG ps (Guess t v) = showEnv ps (normalise ctxt ps t) ++
68+ " =?= " ++ showEnv ps v
6369 showG ps b = showEnv ps (binderTy b)
6470
6571same Nothing n = True
6672same (Just x) n = x == n
67−
73+
6874hole (Hole _) = True
6975hole (Guess _ _) = True
7076hole _ = False
@@ -91,7 +97,8 @@ type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
9197goal :: Hole -> Term -> Context -> TC Goal
9298goal h tm ctxt = g [] tm where
9399 g env (Bind n b sc) | hole b && same h n = return $ GD env b
94− | otherwise = gb env b `mplus` g ((n,b):env) sc
100+ | otherwise
101+ = gb env b `mplus` g ((n,fmap (weakenTm 1) b):weakenTmEnv 1 env) sc
95102 g env (App f a) = g env f `mplus` g env a
96103 g env t = Error "Can't find hole"
97104
@@ -105,8 +112,10 @@ tactic h ps ctxt f = do let tm = pterm ps
105112 return (ps { pterm = tm' })
106113 where
107114 atH env binder@(Bind n b sc)
108− | hole b && same h n = f ctxt (weakenEnv env) binder
109− | otherwise = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b):env) sc
115+ | hole b && same h n = f ctxt env binder
116+ | otherwise
117+ = pure Bind <*> pure n <*> atHb env b <*>
118+ atH ((n,fmap (weakenTm 1) b):weakenTmEnv 1 env) sc
110119 atH env (App f a) = pure App <*> atH env f <*> atH env a
111120 atH env t = return t
112121
@@ -125,7 +134,15 @@ attack ctxt env (Bind x (Hole t) sc)
125134attack ctxt env _ = fail "Not an attackable hole"
126135
127136claim :: Name -> Raw -> RunTactic
128−claim = undefined
137+claim n ty ctxt env t =
138+ do (tyv, tyt) <- lift $ check ctxt env ty
139+ lift $ isSet ctxt env tyt
140+ action (NextGoal n)
141+ return $ Bind n (Hole tyv) t
142+
143+focus :: Name -> RunTactic
144+focus n ctxt env t = do action (FocusGoal n)
145+ return t
129146
130147regret :: RunTactic
131148regret = undefined
@@ -182,9 +199,11 @@ processTactic t ps = case holes ps of
182199 logs (_ : xs) = logs xs
183200
184201 goals g [] = g
185− goals g (AddGoal n : xs) = goals (n : g) xs
186− goals g (Solved n : xs) = goals (g \\ [n]) xs
187− goals g (_ : xs) = goals g xs
202+ goals g (AddGoal n : xs) = goals (n : g) xs
203+ goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs
204+ goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs
205+ goals g (Solved n : xs) = goals (g \\ [n]) xs
206+ goals g (_ : xs) = goals g xs
188207
189208
190209process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
@@ -197,3 +216,4 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)
197216 mktac (Intro n) = intro n
198217 mktac (CheckIn r) = check_in r
199218 mktac (EvalIn r) = eval_in r
219+ mktac (Focus n) = focus n