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