git.iko.soy/Idris-dev
on 809c283 help sign in
Idris-dev/src/Core/ProofState.hs
602 lines 25 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, PatternGuards #-}
3{- Implements a proof state, some primitive tactics for manipulating
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
7module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), Goal(..), processTactic, dropGiven) where
10import Core.Typecheck
11import Core.Evaluate
12import Core.TT
13import Core.Unify
15import Control.Monad.State
16import Control.Applicative hiding (empty)
17import Data.List
18import Debug.Trace
20import Util.Pretty
22data ProofState = PS { thname :: Name,
23 holes :: [Name], -- holes still to be solved
24 usedns :: [Name], -- used names, don't use again
25 nextname :: Int, -- name supply
26 pterm :: Term, -- current proof term
27 ptype :: Type, -- original goal
28 dontunify :: [Name], -- explicitly given by programmer, leave it
29 unified :: (Name, [(Name, Term)]),
30 solved :: Maybe (Name, Term),
31 problems :: Fails,
32 injective :: [(Term, Term, Term)],
33 deferred :: [Name], -- names we'll need to define
34 instances :: [Name], -- instance arguments (for type classes)
35 previous :: Maybe ProofState, -- for undo
36 context :: Context,
37 plog :: String,
38 done :: Bool
39 }
41data Goal = GD { premises :: Env,
42 goalType :: Binder Term
43 }
45data Tactic = Attack
46 | Claim Name Raw
47 | Reorder Name
48 | Exact Raw
49 | Fill Raw
50 | PrepFill Name [Name]
51 | CompleteFill
52 | Regret
53 | Solve
54 | StartUnify Name
55 | EndUnify
56 | Compute
57 | EvalIn Raw
58 | CheckIn Raw
59 | Intro (Maybe Name)
60 | IntroTy Raw (Maybe Name)
61 | Forall Name Raw
62 | LetBind Name Raw Raw
63 | Rewrite Raw
64 | PatVar Name
65 | PatBind Name
66 | Focus Name
67 | Defer Name
68 | Instance Name
69 | MoveLast Name
70 | ProofState
71 | Undo
72 | QED
73 deriving Show
75-- Some utilites on proof and tactic states
77instance Show ProofState where
78 show (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _) = show nm ++ ": no more goals"
79 show (PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _)
80 = let OK g = goal (Just h) tm
81 wkenv = premises g in
82 "Other goals: " ++ show hs ++ "\n" ++
83 showPs wkenv (reverse wkenv) ++ "\n" ++
84 "-------------------------------- (" ++ show nm ++
85 ") -------\n " ++
86 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
87 where showPs env [] = ""
88 showPs env ((n, Let t v):bs)
89 = " " ++ show n ++ " : " ++
90 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
91 showEnv env ({- normalise ctxt env -} v) ++
92 "\n" ++ showPs env bs
93 showPs env ((n, b):bs)
94 = " " ++ show n ++ " : " ++
95 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
96 "\n" ++ showPs env bs
97 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
98 " =?= " ++ showEnv ps v
99 showG ps b = showEnv ps (binderTy b)
101instance Pretty ProofState where
102 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _) =
103 if size nm > breakingSize then
104 pretty nm <> colon $$ nest nestingSize (text " no more goals.")
105 else
106 pretty nm <> colon <+> text " no more goals."
107 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ i _ _ ctxt _ _) =
108 let OK g = goal (Just h) tm in
109 let wkEnv = premises g in
110 text "Other goals" <+> colon <+> pretty hs $$
111 prettyPs wkEnv (reverse wkEnv) $$
112 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
113 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
114 where
115 prettyGoal ps (Guess t v) =
116 if size v > breakingSize then
117 prettyEnv ps t <+> text "=?=" $$
118 nest nestingSize (prettyEnv ps v)
119 else
120 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
121 prettyGoal ps b = prettyEnv ps $ binderTy b
123 prettyPs env [] = empty
124 prettyPs env ((n, Let t v):bs) =
125 nest nestingSize (pretty n <+> colon <+>
126 if size v > breakingSize then
127 prettyEnv env t <+> text "=" $$
128 nest nestingSize (prettyEnv env v) $$
129 nest nestingSize (prettyPs env bs)
130 else
131 prettyEnv env t <+> text "=" <+> prettyEnv env v $$
132 nest nestingSize (prettyPs env bs))
133 prettyPs env ((n, b):bs) =
134 if size (binderTy b) > breakingSize then
135 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
136 else
137 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
138 nest nestingSize (prettyPs env bs))
140same Nothing n = True
141same (Just x) n = x == n
143hole (Hole _) = True
144hole (Guess _ _) = True
145hole _ = False
147holeName i = MN i "hole"
149unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]
150unify' ctxt env topx topy = do (u, inj, fails) <- lift $ unify ctxt env topx topy
151 addInj inj
152 case fails of
153 [] -> return u
154 err ->
155 do ps <- get
156 put (ps { problems = err ++ problems ps })
157 return []
159getName :: Monad m => String -> StateT TState m Name
160getName tag = do ps <- get
161 let n = nextname ps
162 put (ps { nextname = n+1 })
163 return $ MN n tag
165action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
166action a = do ps <- get
167 put (a ps)
169addLog :: Monad m => String -> StateT TState m ()
170addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
172newProof :: Name -> Context -> Type -> ProofState
173newProof n ctxt ty = let h = holeName 0
174 ty' = vToP ty in
175 PS n [h] [] 1 (Bind h (Hole ty')
176 (P Bound h ty')) ty [] (h, [])
177 Nothing [] []
178 [] []
179 Nothing ctxt "" False
181type TState = ProofState -- [TacticAction])
182type RunTactic = Context -> Env -> Term -> StateT TState TC Term
183type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
185envAtFocus :: ProofState -> TC Env
186envAtFocus ps
187 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
188 return (premises g)
189 | otherwise = fail "No holes"
191goalAtFocus :: ProofState -> TC (Binder Type)
192goalAtFocus ps
193 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
194 return (goalType g)
196goal :: Hole -> Term -> TC Goal
197goal h tm = g [] tm where
198 g env (Bind n b sc) | hole b && same h n = return $ GD env b
199 | otherwise
200 = gb env b `mplus` g ((n, b):env) sc
201 g env (App f a) = g env f `mplus` g env a
202 g env t = fail "Can't find hole"
204 gb env (Let t v) = g env t `mplus` g env v
205 gb env (Guess t v) = g env t `mplus` g env v
206 gb env t = g env (binderTy t)
208tactic :: Hole -> RunTactic -> StateT TState TC ()
209tactic h f = do ps <- get
210 tm' <- atH (context ps) [] (pterm ps)
211 ps <- get -- might have changed while processing
212 put (ps { pterm = tm' })
213 where
214 atH c env binder@(Bind n b sc)
215 | hole b && same h n = f c env binder
216 | otherwise
217 = liftM2 (Bind n) (atHb c env b) (atH c ((n, b) : env) sc)
218 atH c env (App f a) = liftM2 App (atH c env f) (atH c env a)
219 atH c env t = return t
221 atHb c env (Let t v) = liftM2 Let (atH c env t) (atH c env v)
222 atHb c env (Guess t v) = liftM2 Guess (atH c env t) (atH c env v)
223 atHb c env t = do ty' <- atH c env (binderTy t)
224 return $ t { binderTy = ty' }
226attack :: RunTactic
227attack ctxt env (Bind x (Hole t) sc)
228 = do h <- getName "hole"
229 action (\ps -> ps { holes = h : holes ps })
230 return $ Bind x (Guess t (newtm h)) sc
231 where
232 newtm h = Bind h (Hole t) (P Bound h t)
233attack ctxt env _ = fail "Not an attackable hole"
235claim :: Name -> Raw -> RunTactic
236claim n ty ctxt env t =
237 do (tyv, tyt) <- lift $ check ctxt env ty
238 lift $ isSet ctxt env tyt
239 action (\ps -> let (g:gs) = holes ps in
240 ps { holes = g : n : gs } )
241 return $ Bind n (Hole tyv) t -- (weakenTm 1 t)
243reorder_claims :: RunTactic
244reorder_claims ctxt env t
245 = -- trace (showSep "\n" (map show (scvs t))) $
246 let (bs, sc) = scvs t []
247 newbs = reverse (sortB (reverse bs)) in
248 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
249 return (bindAll newbs sc)
250 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
251 scvs sc acc = (reverse acc, sc)
253 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
254 sortB [] = []
255 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
256 | otherwise = sortB (insertB x xs)
258 insertB x [] = [x]
259 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
260 | otherwise = y : insertB x ys
262 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
263 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
264 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
266focus :: Name -> RunTactic
267focus n ctxt env t = do action (\ps -> let hs = holes ps in
268 if n `elem` hs
269 then ps { holes = n : (hs \\ [n]) }
270 else ps)
271 ps <- get
272 return t
274movelast :: Name -> RunTactic
275movelast n ctxt env t = do action (\ps -> let hs = holes ps in
276 if n `elem` hs
277 then ps { holes = (hs \\ [n]) ++ [n] }
278 else ps)
279 return t
281instanceArg :: Name -> RunTactic
282instanceArg n ctxt env (Bind x (Hole t) sc)
283 = do action (\ps -> let hs = holes ps
284 is = instances ps in
285 ps { holes = (hs \\ [x]) ++ [x],
286 instances = x:is })
287 return (Bind x (Hole t) sc)
289defer :: Name -> RunTactic
290defer n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
291 do action (\ps -> let hs = holes ps in
292 ps { holes = hs \\ [x] })
293 return (Bind n (GHole (mkTy (reverse env) t))
294 (mkApp (P Ref n ty) (map getP (reverse env))))
295 where
296 mkTy [] t = t
297 mkTy ((n,b) : bs) t = Bind n (Pi (binderTy b)) (mkTy bs t)
299 getP (n, b) = P Bound n (binderTy b)
301regret :: RunTactic
302regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
303 do action (\ps -> let hs = holes ps in
304 ps { holes = hs \\ [x] })
305 return sc
306regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"
308addInj :: [(Term, Term, Term)] -> StateT TState TC ()
309addInj inj = do ps <- get
310 put (ps { injective = inj ++ injective ps })
312exact :: Raw -> RunTactic
313exact guess ctxt env (Bind x (Hole ty) sc) =
314 do (val, valty) <- lift $ check ctxt env guess
315 lift $ converts ctxt env valty ty
316 return $ Bind x (Guess ty val) sc
317exact _ _ _ _ = fail "Can't fill here."
319-- As exact, but attempts to solve other goals by unification
321fill :: Raw -> RunTactic
322fill guess ctxt env (Bind x (Hole ty) sc) =
323 do (val, valty) <- lift $ check ctxt env guess
324 s <- get
325-- let valtyn = normalise ctxt env valty
326-- let tyn = normalise ctxt env ty
327 ns <- unify' ctxt env valty ty
328 ps <- get
329 let (uh, uns) = unified ps
330 put (ps { unified = (uh, uns ++ ns) })
331-- addLog (show (uh, uns ++ ns))
332 return $ Bind x (Guess ty val) sc
333fill _ _ _ _ = fail "Can't fill here."
335prep_fill :: Name -> [Name] -> RunTactic
336prep_fill f as ctxt env (Bind x (Hole ty) sc) =
337 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
338 return $ Bind x (Guess ty val) sc
339prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
341complete_fill :: RunTactic
342complete_fill ctxt env (Bind x (Guess ty val) sc) =
343 do let guess = forget val
344 (val', valty) <- lift $ check ctxt env guess
345 ns <- unify' ctxt env valty ty
346 ps <- get
347 let (uh, uns) = unified ps
348 put (ps { unified = (uh, uns ++ ns) })
349 return $ Bind x (Guess ty val) sc
350complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
352solve :: RunTactic
353solve ctxt env (Bind x (Guess ty val) sc)
354 | pureTerm val = do ps <- get
355 let (uh, uns) = unified ps
356 action (\ps -> ps { holes = holes ps \\ [x],
357 solved = Just (x, val),
358 -- dontunify = dontunify ps \\ [x],
359 -- unified = (uh, uns ++ [(x, val)]),
360 instances = instances ps \\ [x] })
361 return $ {- Bind x (Let ty val) sc -}
362 instantiate val (pToV x sc)
363 | otherwise = lift $ tfail $ IncompleteTerm val
364solve _ _ h = do ps <- get
365 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)
367introTy :: Raw -> Maybe Name -> RunTactic
368introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
369 do let n = case mn of
370 Just name -> name
371 Nothing -> x
372 let t' = case t of
373 x@(Bind y (Pi s) _) -> x
374 _ -> normalise ctxt env t
375 (tyv, tyt) <- lift $ check ctxt env ty
376-- ns <- lift $ unify ctxt env tyv t'
377 case t' of
378 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
379 do ns <- unify' ctxt env s tyv
380 ps <- get
381 let (uh, uns) = unified ps
382 put (ps { unified = (uh, uns ++ ns) })
383 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
384 _ -> fail "Nothing to introduce"
385introTy ty n ctxt env _ = fail "Can't introduce here."
387intro :: Maybe Name -> RunTactic
388intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
389 do let n = case mn of
390 Just name -> name
391 Nothing -> x
392 let t' = case t of
393 x@(Bind y (Pi s) _) -> x
394 _ -> normalise ctxt env t
395 case t' of
396 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
397 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
398 _ -> fail "Nothing to introduce"
399intro n ctxt env _ = fail "Can't introduce here."
401forall :: Name -> Raw -> RunTactic
402forall n ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
403 do (tyv, tyt) <- lift $ check ctxt env ty
404 lift $ isSet ctxt env tyt
405 lift $ isSet ctxt env t
406 return $ Bind n (Pi tyv) (Bind x (Hole t) (P Bound x t))
407forall n ty ctxt env _ = fail "Can't pi bind here"
409patvar :: Name -> RunTactic
410patvar n ctxt env (Bind x (Hole t) sc) =
411 do action (\ps -> ps { holes = holes ps \\ [x] })
412 return $ Bind n (PVar t) (instantiate (P Bound n t) (pToV x sc))
413patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
415letbind :: Name -> Raw -> Raw -> RunTactic
416letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
417 do (tyv, tyt) <- lift $ check ctxt env ty
418 (valv, valt) <- lift $ check ctxt env val
419 lift $ isSet ctxt env tyt
420 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
421letbind n ty val ctxt env _ = fail "Can't let bind here"
423rewrite :: Raw -> RunTactic
424rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
425 do (tmv, tmt) <- lift $ check ctxt env tm
426 let tmt' = normalise ctxt env tmt
427 case unApply tmt' of
428 (P _ (UN "=") _, [lt,rt,l,r]) ->
429 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
430 let newt = mkP l r l t
431 let sc = forget $ (Bind x (Hole newt)
432 (mkApp (P Ref (UN "replace") (Set (UVal 0)))
433 [lt, l, r, p, tmv, xp]))
434 (scv, sct) <- lift $ check ctxt env sc
435 return scv
436 _ -> fail "Not an equality type"
437 where
438 -- to make the P for rewrite, replace syntactic occurrences of l in ty with
439 -- an x, and put \x : lt in front
440 mkP lt l r ty | l == ty = lt
441 mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
442 a' = if (r /= a) then mkP lt l r a else a in
443 App f' a'
444 mkP lt l r (Bind n b sc)
445 = let b' = mkPB b
446 sc' = if (r /= sc) then mkP lt l r sc else sc in
447 Bind n b' sc'
448 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
449 v' = if (r /= v) then mkP lt l r v else v in
450 Let t' v'
451 mkPB b = let ty = binderTy b
452 ty' = if (r /= ty) then mkP lt l r ty else ty in
453 b { binderTy = ty' }
454 mkP lt l r x = x
456 rname = MN 0 "replaced"
457rewrite _ _ _ _ = fail "Can't rewrite here"
459patbind :: Name -> RunTactic
460patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
461 do let t' = case t of
462 x@(Bind y (PVTy s) t) -> x
463 _ -> normalise ctxt env t
464 case t' of
465 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
466 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
467 _ -> fail "Nothing to pattern bind"
468patbind n ctxt env _ = fail "Can't pattern bind here"
470compute :: RunTactic
471compute ctxt env (Bind x (Hole ty) sc) =
472 do return $ Bind x (Hole (normalise ctxt env ty)) sc
474check_in :: Raw -> RunTactic
475check_in t ctxt env tm =
476 do (val, valty) <- lift $ check ctxt env t
477 addLog (showEnv env val ++ " : " ++ showEnv env valty)
478 return tm
480eval_in :: Raw -> RunTactic
481eval_in t ctxt env tm =
482 do (val, valty) <- lift $ check ctxt env t
483 let val' = normalise ctxt env val
484 let valty' = normalise ctxt env valty
485 addLog (showEnv env val ++ " : " ++
486 showEnv env valty ++
487-- " in " ++ show env ++
488 " ==>\n " ++
489 showEnv env val' ++ " : " ++
490 showEnv env valty')
491 return tm
493start_unify :: Name -> RunTactic
494start_unify n ctxt env tm = do action (\ps -> ps { unified = (n, []) })
495 return tm
497tmap f (a, b, c) = (f a, b, c)
499solve_unified :: RunTactic
500solve_unified ctxt env tm =
501 do ps <- get
502 let (_, ns) = unified ps
503 let unify = dropGiven (dontunify ps) ns
504 action (\ps -> ps { holes = holes ps \\ map fst unify })
505 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
506 action (\ps -> ps { injective = map (tmap (updateSolved unify)) (injective ps) })
507 return (updateSolved unify tm)
508 where
510dropGiven du [] = []
511dropGiven du ((n, P Bound t ty) : us) | n `elem` du && not (t `elem` du)
512 = (t, P Bound n ty) : dropGiven du us
513dropGiven du (u@(n, _) : us) | n `elem` du = dropGiven du us
514-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
515dropGiven du (u : us) = u : dropGiven du us
517updateSolved xs x = -- trace ("Updating " ++ show xs ++ " in " ++ show x) $
518 updateSolved' xs x
519updateSolved' xs (Bind n (Hole ty) t)
520 | Just v <- lookup n xs = instantiate v (pToV n (updateSolved' xs t))
521updateSolved' xs (Bind n b t)
522 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)
523updateSolved' xs (App f a) = App (updateSolved' xs f) (updateSolved' xs a)
524updateSolved' xs (P _ n _)
525 | Just v <- lookup n xs = v
526updateSolved' xs t = t
528updateProblems ns [] = []
529updateProblems ns ((x, y, env, err) : ps) =
530 let x' = updateSolved ns x
531 y' = updateSolved ns y in
532 (x',y',env,err) : updateProblems ns ps
534processTactic :: Tactic -> ProofState -> TC (ProofState, String)
535processTactic QED ps = case holes ps of
536 [] -> do let tm = {- normalise (context ps) [] -} (pterm ps)
537 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
538 return (ps { done = True, pterm = tm' },
539 "Proof complete: " ++ showEnv [] tm')
540 _ -> fail "Still holes to fill."
541processTactic ProofState ps = return (ps, showEnv [] (pterm ps))
542processTactic Undo ps = case previous ps of
543 Nothing -> fail "Nothing to undo."
544 Just pold -> return (pold, "")
545processTactic EndUnify ps
546 = let (h, ns_in) = unified ps
547 ns = dropGiven (dontunify ps) ns_in
548 ns' = map (\ (n, t) -> (n, updateSolved ns t)) ns
549 tm' = -- trace ("Updating " ++ show ns') $ -- ++ " in " ++ show (pterm ps)) $
550 updateSolved ns' (pterm ps)
551 probs' = updateProblems ns' (problems ps) in
552 case probs' of
553 [] -> return (ps { pterm = tm',
554 unified = (h, []),
555 injective = map (tmap (updateSolved ns'))
556 (injective ps),
557 holes = holes ps \\ map fst ns' }, "")
558 errs@((_,_,_,err):_) -> tfail err
559processTactic (Reorder n) ps
560 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
561 return (ps' { previous = Just ps, plog = "" }, plog ps')
562processTactic t ps
563 = case holes ps of
564 [] -> fail "Nothing to fill in."
565 (h:_) -> do ps' <- execStateT (process t h) ps
566 let pterm' = case solved ps' of
567 Just s -> updateSolved [s] (pterm ps')
568 _ -> pterm ps'
569 return (ps' { pterm = pterm',
570 solved = Nothing,
571 previous = Just ps, plog = "" }, plog ps')
573process :: Tactic -> Name -> StateT TState TC ()
574process EndUnify _
575 = do ps <- get
576 let (h, _) = unified ps
577 tactic (Just h) solve_unified
578process t h = tactic (Just h) (mktac t)
579 where mktac Attack = attack
580 mktac (Claim n r) = claim n r
581 mktac (Exact r) = exact r
582 mktac (Fill r) = fill r
583 mktac (PrepFill n ns) = prep_fill n ns
584 mktac CompleteFill = complete_fill
585 mktac Regret = regret
586 mktac Solve = solve
587 mktac (StartUnify n) = start_unify n
588 mktac Compute = compute
589 mktac (Intro n) = intro n
590 mktac (IntroTy ty n) = introTy ty n
591 mktac (Forall n t) = forall n t
592 mktac (LetBind n t v) = letbind n t v
593 mktac (Rewrite t) = rewrite t
594 mktac (PatVar n) = patvar n
595 mktac (PatBind n) = patbind n
596 mktac (CheckIn r) = check_in r
597 mktac (EvalIn r) = eval_in r
598 mktac (Focus n) = focus n
599 mktac (Defer n) = defer n
600 mktac (Instance n) = instanceArg n
601 mktac (MoveLast n) = movelast n