@@ -22,9 +22,11 @@ data ProofState = PS { thname :: Name,
2222 nextname :: Int, -- name supply
2323 pterm :: Term, -- current proof term
2424 ptype :: Type, -- original goal
25+ unified :: (Name, [(Name, Term)]),
2526 defer :: [(Name, Type)], -- names we'll need to define
2627 previous :: Maybe ProofState, -- for undo
2728 context :: Context,
29+ plog :: String,
2830 done :: Bool
2931 }
3032
@@ -38,6 +40,8 @@ data Tactic = Attack
3840 | Fill Raw
3941 | Regret
4042 | Solve
43+ | StartUnify Name
44+ | EndUnify
4145 | Compute
4246 | EvalIn Raw
4347 | CheckIn Raw
@@ -55,14 +59,14 @@ data TacticAction = AddGoal Name -- add a new goal, solve immediately
5559 | FocusGoal Name -- focus on this goal next
5660 | MoveGoal Name -- move this goal to the end of the hole queue
5761 | Solved Name
58− | AlsoSolved Name Term -- goals solved by unification
62+ | AlsoSolved [(Name, Term)] -- variables solved by unification
5963 | Log String
6064
6165-- Some utilites on proof and tactic states
6266
6367instance Show ProofState where
64− show (PS nm [] _ tm _ _ _ _ _) = show nm ++ ": no more goals"
65− show (PS nm (h:hs) _ tm _ i _ ctxt _)
68+ show (PS nm [] _ tm _ _ _ _ _ _ _) = show nm ++ ": no more goals"
69+ show (PS nm (h:hs) _ tm _ _ i _ ctxt _ _)
6670 = let OK g = goal (Just h) tm
6771 wkenv = premises g in
6872 showPs wkenv (reverse wkenv) ++ "\n" ++
@@ -93,21 +97,25 @@ hole _ = False
9397holeName i = MN i "hole"
9498
9599getName :: Monad m => String -> StateT TState m Name
96−getName tag = do (n, ts) <- get
97− put (n+1, ts)
100+getName tag = do ps <- get
101+ let n = nextname ps
102+ put (ps { nextname = n+1 })
98103 return $ MN n tag
99104
100−action :: Monad m => TacticAction -> StateT TState m ()
101−action a = do (n, ts) <- get
102− put (n, a:ts)
105+action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
106+action a = do ps <- get
107+ put (a ps)
108+
109+addLog :: Monad m => String -> StateT TState m ()
110+addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
103111
104112newProof :: Name -> Context -> Type -> ProofState
105113newProof n ctxt ty = let h = holeName 0
106114 ty' = vToP ty in
107− PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty []
108− Nothing ctxt False
115+ PS n [h] 1 (Bind h (Hole ty') (P Bound h ty')) ty (h, []) []
116+ Nothing ctxt "" False
109117
110−type TState = (Int, [TacticAction])
118+type TState = ProofState -- [TacticAction])
111119type RunTactic = Context -> Env -> Term -> StateT TState TC Term
112120type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
113121
@@ -134,27 +142,28 @@ goal h tm = g [] tm where
134142 gb env (Guess t v) = g env t `mplus` g env v
135143 gb env t = g env (binderTy t)
136144
137−tactic :: Hole -> ProofState -> Context -> RunTactic -> StateT TState TC ProofState
138−tactic h ps ctxt f = do let tm = pterm ps
139− tm' <- atH [] tm
140− return (ps { pterm = tm' })
145+tactic :: Hole -> RunTactic -> StateT TState TC ()
146+tactic h f = do ps <- get
147+ tm' <- atH (context ps) [] (pterm ps)
148+ ps <- get -- might have changed while processing
149+ put (ps { pterm = tm' })
141150 where
142− atH env binder@(Bind n b sc)
143− | hole b && same h n = f ctxt env binder
151+ atH c env binder@(Bind n b sc)
152+ | hole b && same h n = f c env binder
144153 | otherwise
145− = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b) : env) sc
146− atH env (App f a) = pure App <*> atH env f <*> atH env a
147− atH env t = return t
154+ = pure Bind <*> pure n <*> atHb c env b <*> atH c ((n,b) : env) sc
155+ atH c env (App f a) = pure App <*> atH c env f <*> atH c env a
156+ atH c env t = return t
148157
149− atHb env (Let t v) = pure Let <*> atH env t <*> atH env v
150− atHb env (Guess t v) = pure Guess <*> atH env t <*> atH env v
151− atHb env t = do ty' <- atH env (binderTy t)
152− return $ t { binderTy = ty' }
158+ atHb c env (Let t v) = pure Let <*> atH c env t <*> atH c env v
159+ atHb c env (Guess t v) = pure Guess <*> atH c env t <*> atH c env v
160+ atHb c env t = do ty' <- atH c env (binderTy t)
161+ return $ t { binderTy = ty' }
153162
154163attack :: RunTactic
155164attack ctxt env (Bind x (Hole t) sc)
156165 = do h <- getName "hole"
157− action (AddGoal h)
166+ action (\ps -> ps { holes = h : holes ps })
158167 return $ Bind x (Guess t (newtm h)) sc
159168 where
160169 newtm h = Bind h (Hole t) (P Bound h t)
@@ -164,15 +173,22 @@ claim :: Name -> Raw -> RunTactic
164173claim n ty ctxt env t =
165174 do (tyv, tyt) <- lift $ check ctxt env ty
166175 lift $ isSet ctxt env tyt
167− action (NextGoal n)
176+ action (\ps -> let (g:gs) = holes ps in
177+ ps { holes = g : n : gs } )
168178 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
169179
170180focus :: Name -> RunTactic
171−focus n ctxt env t = do action (FocusGoal n)
181+focus n ctxt env t = do action (\ps -> let hs = holes ps in
182+ if n `elem` hs
183+ then ps { holes = n : (hs \\ [n]) }
184+ else ps)
172185 return t
173186
174187movelast :: Name -> RunTactic
175−movelast n ctxt env t = do action (MoveGoal n)
188+movelast n ctxt env t = do action (\ps -> let hs = holes ps in
189+ if n `elem` hs
190+ then ps { holes = (hs \\ [n]) ++ [n] }
191+ else ps)
176192 return t
177193
178194-- Hmmm. YAGNI?
@@ -192,17 +208,16 @@ fill :: Raw -> RunTactic
192208fill guess ctxt env (Bind x (Hole ty) sc) =
193209 do (val, valty) <- lift $ check ctxt env guess
194210 ns <- lift $ unify ctxt env valty ty
195− solve_all ns
211+ ps <- get
212+ let (uh, uns) = unified ps
213+ put (ps { unified = (uh, uns ++ ns) })
214+ addLog (show (uh, uns ++ ns))
196215 return $ Bind x (Guess ty val) sc
197− where
198− solve_all [] = return ()
199− solve_all ((n, tm): ns) = do action (AlsoSolved n tm)
200− solve_all ns
201216fill _ _ _ _ = fail "Can't fill here."
202217
203218solve :: RunTactic
204219solve ctxt env (Bind x (Guess ty val) sc)
205− | pureTerm val = do action (Solved x)
220+ | pureTerm val = do action (\ps -> ps { holes = holes ps \\ [x] })
206221 return $ Bind x (Let ty val) sc -- instantiate val (pToV x sc)
207222 | otherwise = fail "I see a hole in your solution."
208223solve _ _ _ = fail "Not a guess."
@@ -236,7 +251,7 @@ compute ctxt env (Bind x (Hole ty) sc) =
236251check_in :: Raw -> RunTactic
237252check_in t ctxt env tm =
238253 do (val, valty) <- lift $ check ctxt env t
239− action (Log (showEnv env val ++ " : " ++ showEnv env valty))
254+ addLog (showEnv env val ++ " : " ++ showEnv env valty)
240255 return tm
241256
242257eval_in :: Raw -> RunTactic
@@ -244,14 +259,34 @@ eval_in t ctxt env tm =
244259 do (val, valty) <- lift $ check ctxt env t
245260 let val' = normalise ctxt env val
246261 let valty' = normalise ctxt env valty
247− action (Log (showEnv env val ++ " : " ++
248− showEnv env valty ++
262+ addLog (showEnv env val ++ " : " ++
263+ showEnv env valty ++
249264-- " in " ++ show env ++
250− " ==>\n " ++
251− showEnv env val' ++ " : " ++
252− showEnv env valty'))
265+ " ==>\n " ++
266+ showEnv env val' ++ " : " ++
267+ showEnv env valty')
253268 return tm
254269
270+start_unify :: Name -> RunTactic
271+start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
272+ return tm
273+
274+solve_unified :: RunTactic
275+solve_unified ctxt env tm =
276+ do ps <- get
277+ let (_, ns) = unified ps
278+ action (\ps -> ps { holes = holes ps \\ map fst ns })
279+ return (updateSolved ns tm)
280+ where
281+ updateSolved xs (Bind n b@(Hole _) t)
282+ | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
283+ updateSolved xs (Bind n b t)
284+ | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
285+ updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
286+ updateSolved xs (P _ n _)
287+ | Just v <- lookup n xs = v
288+ updateSolved xs t = t
289+
255290-- shuffleHoles :: Term -> Term
256291-- shuffleHoles tm = shuffle [] tm
257292-- where
@@ -273,48 +308,22 @@ processTactic t ps
273308 = case holes ps of
274309 [] -> Error "Nothing to fill in."
275310 (h:_) -> do let n = nextname ps
276− (ps', (n', actions)) <- runStateT (process t h ps) (n, [])
277− return (ps' { nextname = n',
278− pterm = updateSolved (getSolved actions) (pterm ps'),
279− holes = goals (holes ps') actions,
280− previous = Just ps },
281− logs actions)
282− where logs [] = ""
283− logs (Log x : xs) = x ++ "\n" ++ logs xs
284− logs (_ : xs) = logs xs
285−
286− goals g [] = g
287− goals g (AddGoal n : xs) = goals (n : g) xs
288− goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs
289− goals g (FocusGoal n : xs)
290− | n `elem` g = goals (n : (g \\ [n])) xs
291− goals g (MoveGoal n : xs)
292− | n `elem` g = goals ((g \\ [n]) ++ [n]) xs
293− goals g (Solved n : xs) = goals (g \\ [n]) xs
294− goals g (AlsoSolved n tm : xs) = goals (g \\ [n]) xs
295− goals g (_ : xs) = goals g xs
296−
297− getSolved [] = []
298− getSolved (AlsoSolved n tm : xs) = (n, tm) : getSolved xs
299− getSolved (_ : xs) = getSolved xs
300−
301− updateSolved xs (Bind n b@(Hole _) t)
302− | Just v <- lookup n xs = instantiate v (pToV n (updateSolved xs t))
303− updateSolved xs (Bind n b t)
304− | otherwise = Bind n (fmap (updateSolved xs) b) (updateSolved xs t)
305− updateSolved xs (App f a) = App (updateSolved xs f) (updateSolved xs a)
306− updateSolved xs (P _ n _)
307− | Just v <- lookup n xs = v
308− updateSolved xs t = t
309−
310−process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
311−process t h ps = tactic (Just h) ps (context ps) (mktac t)
311+ ps' <- execStateT (process t h) ps
312+ return (ps' { previous = Just ps, plog = "" }, plog ps')
313+
314+process :: Tactic -> Name -> StateT TState TC ()
315+process EndUnify _
316+ = do ps <- get
317+ let (h, _) = unified ps
318+ tactic (Just h) solve_unified
319+process t h = tactic (Just h) (mktac t)
312320 where mktac Attack = attack
313321 mktac (Claim n r) = claim n r
314322 mktac (Exact r) = exact r
315323 mktac (Fill r) = fill r
316324 mktac Regret = regret
317325 mktac Solve = solve
326+ mktac (StartUnify n) = start_unify n
318327 mktac Compute = compute
319328 mktac (Intro n) = intro n
320329 mktac (Forall n t) = forall n t