git.iko.soy/Idris-dev
on b4dbebd help sign in
Idris-dev/src/Idris/Core/ProofState.hs
1073 lines 48 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 Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,
9 doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where
11import Idris.Core.Typecheck
12import Idris.Core.Evaluate
13import Idris.Core.TT
14import Idris.Core.Unify
15import Idris.Core.ProofTerm
17import Control.Monad.State.Strict
18import Control.Applicative hiding (empty)
19import Control.Arrow ((***))
20import Data.List
21import Debug.Trace
23import Util.Pretty hiding (fill)
25data ProofState = PS { thname :: Name,
26 holes :: [Name], -- ^ holes still to be solved
27 usedns :: [Name], -- ^ used names, don't use again
28 nextname :: Int, -- ^ name supply
29 pterm :: ProofTerm, -- ^ current proof term
30 ptype :: Type, -- ^ original goal
31 dontunify :: [Name], -- ^ explicitly given by programmer, leave it
32 unified :: (Name, [(Name, Term)]),
33 notunified :: [(Name, Term)],
34 dotted :: [(Name, [Name])], -- ^ dot pattern holes + environment
35 -- either hole or something in env must turn up in the 'notunified' list during elaboration
36 solved :: Maybe (Name, Term),
37 problems :: Fails,
38 injective :: [Name],
39 deferred :: [Name], -- ^ names we'll need to define
40 instances :: [Name], -- ^ instance arguments (for type classes)
41 autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes
42 previous :: Maybe ProofState, -- ^ for undo
43 context :: Context,
44 datatypes :: Ctxt TypeInfo,
45 plog :: String,
46 unifylog :: Bool,
47 done :: Bool,
48 recents :: [Name],
49 while_elaborating :: [FailContext]
50 }
52data Tactic = Attack
53 | Claim Name Raw
54 | ClaimFn Name Name Raw
55 | Reorder Name
56 | Exact Raw
57 | Fill Raw
58 | MatchFill Raw
59 | PrepFill Name [Name]
60 | CompleteFill
61 | Regret
62 | Solve
63 | StartUnify Name
64 | EndUnify
65 | UnifyAll
66 | Compute
67 | ComputeLet Name
68 | Simplify
69 | HNF_Compute
70 | EvalIn Raw
71 | CheckIn Raw
72 | Intro (Maybe Name)
73 | IntroTy Raw (Maybe Name)
74 | Forall Name (Maybe ImplicitInfo) Raw
75 | LetBind Name Raw Raw
76 | ExpandLet Name Term
77 | Rewrite Raw
78 | Induction Raw
79 | CaseTac Raw
80 | Equiv Raw
81 | PatVar Name
82 | PatBind Name
83 | Focus Name
84 | Defer [Name] Name
85 | DeferType Name Raw [Name]
86 | Instance Name
87 | AutoArg Name
88 | SetInjective Name
89 | MoveLast Name
90 | MatchProblems Bool
91 | UnifyProblems
92 | UnifyGoal Raw
93 | ProofState
94 | Undo
95 | QED
96 deriving Show
98-- Some utilites on proof and tactic states
100instance Show ProofState where
101 show ps | [] <- holes ps
102 = show (thname ps) ++ ": no more goals"
103 show ps | (h : hs) <- holes ps
104 = let tm = pterm ps
105 nm = thname ps
106 OK g = goal (Just h) tm
107 wkenv = premises g in
108 "Other goals: " ++ show hs ++ "\n" ++
109 showPs wkenv (reverse wkenv) ++ "\n" ++
110 "-------------------------------- (" ++ show nm ++
111 ") -------\n " ++
112 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
113 where showPs env [] = ""
114 showPs env ((n, Let t v):bs)
115 = " " ++ show n ++ " : " ++
116 showEnv env ({- normalise ctxt env -} t) ++ " = " ++
117 showEnv env ({- normalise ctxt env -} v) ++
118 "\n" ++ showPs env bs
119 showPs env ((n, b):bs)
120 = " " ++ show n ++ " : " ++
121 showEnv env ({- normalise ctxt env -} (binderTy b)) ++
122 "\n" ++ showPs env bs
123 showG ps (Guess t v) = showEnv ps ({- normalise ctxt ps -} t) ++
124 " =?= " ++ showEnv ps v
125 showG ps b = showEnv ps (binderTy b)
127instance Pretty ProofState OutputAnnotation where
128 pretty ps | [] <- holes ps =
129 pretty (thname ps) <+> colon <+> text " no more goals."
130 pretty ps | (h : hs) <- holes ps =
131 let tm = pterm ps
132 OK g = goal (Just h) tm
133 nm = thname ps in
134 let wkEnv = premises g in
135 text "Other goals" <+> colon <+> pretty hs <+>
136 prettyPs wkEnv (reverse wkEnv) <+>
137 text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>
138 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
139 where
140 prettyGoal ps (Guess t v) =
141 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
142 prettyGoal ps b = prettyEnv ps $ binderTy b
144 prettyPs env [] = empty
145 prettyPs env ((n, Let t v):bs) =
146 nest nestingSize (pretty n <+> colon <+>
147 prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
148 nest nestingSize (prettyPs env bs))
149 prettyPs env ((n, b):bs) =
150 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
151 nest nestingSize (prettyPs env bs))
153holeName i = sMN i "hole"
155qshow :: Fails -> String
156qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)
158match_unify' :: Context -> Env ->
159 (TT Name, Maybe Provenance) ->
160 (TT Name, Maybe Provenance) ->
161 StateT TState TC [(Name, TT Name)]
162match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
163 do ps <- get
164 let while = while_elaborating ps
165 let dont = dontunify ps
166 let inj = injective ps
167 traceWhen (unifylog ps)
168 ("Matching " ++ show (topx, topy) ++
169 " in " ++ show env ++
170 "\nHoles: " ++ show (holes ps)
171 ++ "\n"
172 ++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"
173 ) $
174 case match_unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps) while of
175 OK u -> traceWhen (unifylog ps)
176 ("Matched " ++ show u) $
177 do let (h, ns) = unified ps
178 put (ps { unified = (h, u ++ ns) })
179 return u
180 Error e -> traceWhen (unifylog ps)
181 ("No match " ++ show e) $
182 do put (ps { problems = (topx, topy, True,
183 env, e, while, Match) :
184 problems ps })
185 return []
186-- traceWhen (unifylog ps)
187-- ("Matched " ++ show (topx, topy) ++ " without " ++ show dont ++
188-- "\nSolved: " ++ show u
189-- ++ "\nCurrent problems:\n" ++ qshow (problems ps)
190-- -- ++ show (pterm ps)
191-- ++ "\n----------") $
193mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]
194mergeSolutions env ns = merge [] ns
195 where
196 merge acc [] = return (reverse acc)
197 merge acc ((n, t) : ns)
198 | Just t' <- lookup n ns
199 = do ps <- get
200 let probs = problems ps
201 put (ps { problems = probs ++ [(t,t',True,env,
202 CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,
203 [], Unify)] })
204 merge acc ns
205 | otherwise = merge ((n, t): acc) ns
207unify' :: Context -> Env ->
208 (TT Name, Maybe Provenance) ->
209 (TT Name, Maybe Provenance) ->
210 StateT TState TC [(Name, TT Name)]
211unify' ctxt env (topx, xfrom) (topy, yfrom) =
212 do ps <- get
213 let while = while_elaborating ps
214 let dont = dontunify ps
215 let inj = injective ps
216 (u, fails) <- traceWhen (unifylog ps)
217 ("Trying " ++ show (topx, topy) ++
218 "\nNormalised " ++ show (normalise ctxt env topx,
219 normalise ctxt env topy) ++
220 " in " ++ show env ++
221 "\nHoles: " ++ show (holes ps)
222 ++ "\nInjective: " ++ show (injective ps)
223 ++ "\n") $
224 lift $ unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps)
225 (map fst (notunified ps)) while
226 let notu = filter (\ (n, t) -> case t of
227-- P _ _ _ -> False
228 _ -> n `elem` dont) u
229 traceWhen (unifylog ps)
230 ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
231 "\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
232 ++ "\nNot unified:\n" ++ show (notunified ps)
233 ++ "\nCurrent problems:\n" ++ qshow (problems ps)
234-- ++ show (pterm ps)
235 ++ "\n----------") $
236 do let (h, ns) = unified ps
237 -- solve in results (maybe unify should do this itself...)
238 let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u
239 -- if a metavar has multiple solutions, make a new unification
240 -- problem for each.
241 uns <- mergeSolutions env (u' ++ ns)
242 ps <- get
243 let (ns', probs') = updateProblems ps uns (fails ++ problems ps)
244 let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)
245 traceWhen (unifylog ps)
246 ("Now solved: " ++ show ns' ++
247 "\nNow problems: " ++ qshow (probs' ++ probs_notu)) $
248 put (ps { problems = probs' ++ probs_notu,
249 unified = (h, ns'),
250 injective = updateInj u (injective ps),
251 notunified = notu' })
252 return u
253 where updateInj ((n, a) : us) inj
254 | (P _ n' _, _) <- unApply a,
255 n `elem` inj = updateInj us (n':inj)
256 | (P _ n' _, _) <- unApply a,
257 n' `elem` inj = updateInj us (n:inj)
258 updateInj (_ : us) inj = updateInj us inj
259 updateInj [] inj = inj
261nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
262nowElaboratingPS fc f arg ps = ps { while_elaborating = FailContext fc f arg : while_elaborating ps }
264dropUntil :: (a -> Bool) -> [a] -> [a]
265dropUntil p [] = []
266dropUntil p (x:xs) | p x = xs
267 | otherwise = dropUntil p xs
269doneElaboratingAppPS :: Name -> ProofState -> ProofState
270doneElaboratingAppPS f ps = let while = while_elaborating ps
271 while' = dropUntil (\ (FailContext _ f' _) -> f == f') while
272 in ps { while_elaborating = while' }
274doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
275doneElaboratingArgPS f x ps = let while = while_elaborating ps
276 while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while
277 in ps { while_elaborating = while' }
279getName :: Monad m => String -> StateT TState m Name
280getName tag = do ps <- get
281 let n = nextname ps
282 put (ps { nextname = n+1 })
283 return $ sMN n tag
285action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
286action a = do ps <- get
287 put (a ps)
289query :: Monad m => (ProofState -> r) -> StateT TState m r
290query q = do ps <- get
291 return $ q ps
293addLog :: Monad m => String -> StateT TState m ()
294addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
296newProof :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState
297newProof n ctxt datatypes ty =
298 let h = holeName 0
299 ty' = vToP ty
300 in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
301 (P Bound h ty'))) ty [] (h, []) [] []
302 Nothing [] []
303 [] [] []
304 Nothing ctxt datatypes "" False False [] []
306type TState = ProofState -- [TacticAction])
307type RunTactic = RunTactic' TState
309envAtFocus :: ProofState -> TC Env
310envAtFocus ps
311 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
312 return (premises g)
313 | otherwise = fail "No holes"
315goalAtFocus :: ProofState -> TC (Binder Type)
316goalAtFocus ps
317 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
318 return (goalType g)
319 | otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (getProofTerm (pterm ps))
321tactic :: Hole -> RunTactic -> StateT TState TC ()
322tactic h f = do ps <- get
323 (tm', _) <- atHole h f (context ps) [] (pterm ps)
324 ps <- get -- might have changed while processing
325 put (ps { pterm = tm' })
327computeLet :: Context -> Name -> Term -> Term
328computeLet ctxt n tm = cl [] tm where
329 cl env (Bind n' (Let t v) sc)
330 | n' == n = let v' = normalise ctxt env v in
331 Bind n' (Let t v') sc
332 cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
333 cl env (App s f a) = App s (cl env f) (cl env a)
334 cl env t = t
336attack :: RunTactic
337attack ctxt env (Bind x (Hole t) sc)
338 = do h <- getName "hole"
339 action (\ps -> ps { holes = h : holes ps })
340 return $ Bind x (Guess t (newtm h)) sc
341 where
342 newtm h = Bind h (Hole t) (P Bound h t)
343attack ctxt env _ = fail "Not an attackable hole"
345claim :: Name -> Raw -> RunTactic
346claim n ty ctxt env t =
347 do (tyv, tyt) <- lift $ check ctxt env ty
348 lift $ isType ctxt env tyt
349 action (\ps -> let (g:gs) = holes ps in
350 ps { holes = g : n : gs } )
351 return $ Bind n (Hole tyv) t
353-- If the current goal is 'retty', make a claim which is a function that
354-- can compute a retty from argty (i.e a claim 'argty -> retty')
355claimFn :: Name -> Name -> Raw -> RunTactic
356claimFn n bn argty ctxt env t@(Bind x (Hole retty) sc) =
357 do (tyv, tyt) <- lift $ check ctxt env argty
358 lift $ isType ctxt env tyt
359 action (\ps -> let (g:gs) = holes ps in
360 ps { holes = g : n : gs } )
361 return $ Bind n (Hole (Bind bn (Pi Nothing tyv tyt) retty)) t
362claimFn _ _ _ ctxt env _ = fail "Can't make function type here"
364reorder_claims :: RunTactic
365reorder_claims ctxt env t
366 = -- trace (showSep "\n" (map show (scvs t))) $
367 let (bs, sc) = scvs t []
368 newbs = reverse (sortB (reverse bs)) in
369 traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
370 return (bindAll newbs sc)
371 where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
372 scvs sc acc = (reverse acc, sc)
374 sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
375 sortB [] = []
376 sortB (x:xs) | all (noOcc x) xs = x : sortB xs
377 | otherwise = sortB (insertB x xs)
379 insertB x [] = [x]
380 insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
381 | otherwise = y : insertB x ys
383 noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
384 noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
385 noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
387focus :: Name -> RunTactic
388focus n ctxt env t = do action (\ps -> let hs = holes ps in
389 if n `elem` hs
390 then ps { holes = n : (hs \\ [n]) }
391 else ps)
392 ps <- get
393 return t
395movelast :: Name -> RunTactic
396movelast n ctxt env t = do action (\ps -> let hs = holes ps in
397 if n `elem` hs
398 then ps { holes = (hs \\ [n]) ++ [n] }
399 else ps)
400 return t
402instanceArg :: Name -> RunTactic
403instanceArg n ctxt env (Bind x (Hole t) sc)
404 = do action (\ps -> let hs = holes ps
405 is = instances ps in
406 ps { holes = (hs \\ [x]) ++ [x],
407 instances = x:is })
408 return (Bind x (Hole t) sc)
410autoArg :: Name -> RunTactic
411autoArg n ctxt env (Bind x (Hole t) sc)
412 = do action (\ps -> case lookup x (autos ps) of
413 Nothing ->
414 let hs = holes ps in
415 ps { holes = (hs \\ [x]) ++ [x],
416 autos = (x, refsIn t) : autos ps }
417 Just _ -> ps)
418 return (Bind x (Hole t) sc)
420setinj :: Name -> RunTactic
421setinj n ctxt env (Bind x b sc)
422 = do action (\ps -> let is = injective ps in
423 ps { injective = n : is })
424 return (Bind x b sc)
426defer :: [Name] -> Name -> RunTactic
427defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
428 do let env' = filter (\(n, t) -> n `notElem` dropped) env
429 action (\ps -> let hs = holes ps in
430 ps { holes = hs \\ [x] })
431 return (Bind n (GHole (length env') (mkTy (reverse env') t))
432 (mkApp (P Ref n ty) (map getP (reverse env'))))
433 where
434 mkTy [] t = t
435 mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
437 getP (n, b) = P Bound n (binderTy b)
439-- as defer, but build the type and application explicitly
440deferType :: Name -> Raw -> [Name] -> RunTactic
441deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
442 do (fty, _) <- lift $ check ctxt env fty_in
443 action (\ps -> let hs = holes ps
444 ds = deferred ps in
445 ps { holes = hs \\ [x],
446 deferred = n : ds })
447 return (Bind n (GHole 0 fty)
448 (mkApp (P Ref n ty) (map getP args)))
449 where
450 getP n = case lookup n env of
451 Just b -> P Bound n (binderTy b)
452 Nothing -> error ("deferType can't find " ++ show n)
454regret :: RunTactic
455regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
456 do action (\ps -> let hs = holes ps in
457 ps { holes = hs \\ [x] })
458 return sc
459regret ctxt env (Bind x (Hole t) _)
460 = fail $ show x ++ " : " ++ show t ++ " is not solved..."
462unifyGoal :: Raw -> RunTactic
463unifyGoal tm ctxt env h@(Bind x b sc) =
464 do (tmv, _) <- lift $ check ctxt env tm
465 ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
466 return h
468exact :: Raw -> RunTactic
469exact guess ctxt env (Bind x (Hole ty) sc) =
470 do (val, valty) <- lift $ check ctxt env guess
471 lift $ converts ctxt env valty ty
472 return $ Bind x (Guess ty val) sc
473exact _ _ _ _ = fail "Can't fill here."
475-- As exact, but attempts to solve other goals by unification
477fill :: Raw -> RunTactic
478fill guess ctxt env (Bind x (Hole ty) sc) =
479 do (val, valty) <- lift $ check ctxt env guess
480-- let valtyn = normalise ctxt env valty
481-- let tyn = normalise ctxt env ty
482 ns <- unify' ctxt env (valty, Just $ SourceTerm val)
483 (ty, Just (chkPurpose val ty))
484 ps <- get
485 let (uh, uns) = unified ps
486-- put (ps { unified = (uh, uns ++ ns) })
487-- addLog (show (uh, uns ++ ns))
488 return $ Bind x (Guess ty val) sc
489 where
490 -- some expected types show up commonly in errors and indicate a
491 -- specific problem.
492 -- argTy -> retTy suggests a function applied to too many arguments
493 chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))
494 = TooManyArgs val
495 chkPurpose _ _ = ExpectedType
496fill _ _ _ _ = fail "Can't fill here."
498-- As fill, but attempts to solve other goals by matching
500match_fill :: Raw -> RunTactic
501match_fill guess ctxt env (Bind x (Hole ty) sc) =
502 do (val, valty) <- lift $ check ctxt env guess
503-- let valtyn = normalise ctxt env valty
504-- let tyn = normalise ctxt env ty
505 ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)
506 (ty, Just ExpectedType)
507 ps <- get
508 let (uh, uns) = unified ps
509-- put (ps { unified = (uh, uns ++ ns) })
510-- addLog (show (uh, uns ++ ns))
511 return $ Bind x (Guess ty val) sc
512match_fill _ _ _ _ = fail "Can't fill here."
514prep_fill :: Name -> [Name] -> RunTactic
515prep_fill f as ctxt env (Bind x (Hole ty) sc) =
516 do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
517 return $ Bind x (Guess ty val) sc
518prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
520complete_fill :: RunTactic
521complete_fill ctxt env (Bind x (Guess ty val) sc) =
522 do let guess = forget val
523 (val', valty) <- lift $ check ctxt env guess
524 ns <- unify' ctxt env (valty, Just $ SourceTerm val')
525 (ty, Just ExpectedType)
526 ps <- get
527 let (uh, uns) = unified ps
528-- put (ps { unified = (uh, uns ++ ns) })
529 return $ Bind x (Guess ty val) sc
530complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
532-- When solving something in the 'dont unify' set, we should check
533-- that the guess we are solving it with unifies with the thing unification
534-- found for it, if anything.
536solve :: RunTactic
537solve ctxt env (Bind x (Guess ty val) sc)
538 = do ps <- get
539 let (uh, uns) = unified ps
540 dropdots <-
541 case lookup x (notunified ps) of
542 Just tm -> -- trace ("NEED MATCH: " ++ show (x, tm, val) ++ "\nIN " ++ show (pterm ps)) $
543 do match_unify' ctxt env (tm, Just InferredVal)
544 (val, Just GivenVal)
545 return [x]
546 _ -> return []
547 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
548 holes ps \\ [x],
549 solved = Just (x, val),
550 dontunify = filter (/= x) (dontunify ps),
551 notunified = updateNotunified [(x,val)]
552 (notunified ps),
553 recents = x : recents ps,
554 instances = instances ps \\ [x],
555 dotted = dropUnified dropdots (dotted ps) })
556 let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in
557 return locked
558 where dropUnified ddots [] = []
559 dropUnified ddots ((x, es) : ds)
560 | x `elem` ddots || any (\e -> e `elem` ddots) es
561 = dropUnified ddots ds
562 | otherwise = (x, es) : dropUnified ddots ds
564 tryLock :: [Name] -> Term -> (Term, Bool)
565 tryLock hs tm@(App Complete _ _) = (tm, True)
566 tryLock hs tm@(App s f a) =
567 let (f', fl) = tryLock hs f
568 (a', al) = tryLock hs a in
569 if fl && al then (App Complete f' a', True)
570 else (App s f' a', False)
571 tryLock hs t@(P _ n _) = (t, not $ n `elem` hs)
572 tryLock hs t@(Bind n (Hole _) sc) = (t, False)
573 tryLock hs t@(Bind n (Guess _ _) sc) = (t, False)
574 tryLock hs t@(Bind n (Let ty val) sc)
575 = let (ty', tyl) = tryLock hs ty
576 (val', vall) = tryLock hs val
577 (sc', scl) = tryLock hs sc in
578 (Bind n (Let ty' val') sc', tyl && vall && scl)
579 tryLock hs t@(Bind n b sc)
580 = let (bt', btl) = tryLock hs (binderTy b)
581 (val', vall) = tryLock hs val
582 (sc', scl) = tryLock hs sc in
583 (Bind n (b { binderTy = bt' }) sc', btl && scl)
584 tryLock hs t = (t, True)
586solve _ _ h@(Bind x t sc)
587 = do ps <- get
588 case findType x sc of
589 Just t -> lift $ tfail (CantInferType (show t))
590 _ -> lift $ tfail (IncompleteTerm h)
591 where findType x (Bind n (Let t v) sc)
592 = findType x v `mplus` findType x sc
593 findType x (Bind n t sc)
594 | P _ x' _ <- binderTy t, x == x' = Just n
595 | otherwise = findType x sc
596 findType x _ = Nothing
598introTy :: Raw -> Maybe Name -> RunTactic
599introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
600 do let n = case mn of
601 Just name -> name
602 Nothing -> x
603 let t' = case t of
604 x@(Bind y (Pi _ s _) _) -> x
605 _ -> hnf ctxt env t
606 (tyv, tyt) <- lift $ check ctxt env ty
607-- ns <- lift $ unify ctxt env tyv t'
608 case t' of
609 Bind y (Pi _ s _) t -> let t' = updsubst y (P Bound n s) t in
610 do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
611 ps <- get
612 let (uh, uns) = unified ps
613-- put (ps { unified = (uh, uns ++ ns) })
614 return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
615 _ -> lift $ tfail $ CantIntroduce t'
616introTy ty n ctxt env _ = fail "Can't introduce here."
618intro :: Maybe Name -> RunTactic
619intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
620 do let n = case mn of
621 Just name -> name
622 Nothing -> x
623 let t' = case t of
624 x@(Bind y (Pi _ s _) _) -> x
625 _ -> hnf ctxt env t
626 case t' of
627 Bind y (Pi _ s _) t -> -- trace ("in type " ++ show t') $
628 let t' = updsubst y (P Bound n s) t in
629 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
630 _ -> lift $ tfail $ CantIntroduce t'
631intro n ctxt env _ = fail "Can't introduce here."
633forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic
634forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
635 do (tyv, tyt) <- lift $ check ctxt env ty
636 unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)
637 unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)
638 return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))
639forall n impl ty ctxt env _ = fail "Can't pi bind here"
641patvar :: Name -> RunTactic
642patvar n ctxt env (Bind x (Hole t) sc) =
643 do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
644 holes ps \\ [x],
645 solved = Just (x, P Bound n t),
646 dontunify = filter (/=x) (dontunify ps),
647 notunified = updateNotunified [(x,P Bound n t)]
648 (notunified ps),
649 injective = addInj n x (injective ps)
650 })
651 return $ Bind n (PVar t) (updsubst x (P Bound n t) sc)
652 where addInj n x ps | x `elem` ps = n : ps
653 | otherwise = ps
654patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
656letbind :: Name -> Raw -> Raw -> RunTactic
657letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
658 do (tyv, tyt) <- lift $ check ctxt env ty
659 (valv, valt) <- lift $ check ctxt env val
660 lift $ isType ctxt env tyt
661 return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
662letbind n ty val ctxt env _ = fail "Can't let bind here"
664expandLet :: Name -> Term -> RunTactic
665expandLet n v ctxt env tm =
666 return $ updsubst n v tm
668rewrite :: Raw -> RunTactic
669rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
670 do (tmv, tmt) <- lift $ check ctxt env tm
671 let tmt' = normalise ctxt env tmt
672 case unApply tmt' of
673 (P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->
674 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
675 let newt = mkP l r l t
676 let sc = forget $ (Bind x (Hole newt)
677 (mkApp (P Ref (sUN "replace") (TType (UVal 0)))
678 [lt, l, r, p, tmv, xp]))
679 (scv, sct) <- lift $ check ctxt env sc
680 return scv
681 _ -> lift $ tfail (NotEquality tmv tmt')
682 where rname = sMN 0 "replaced"
683rewrite _ _ _ _ = fail "Can't rewrite here"
685-- To make the P for rewrite, replace syntactic occurrences of l in ty with
686-- an x, and put \x : lt in front
687mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
688mkP lt l r ty | l == ty = lt
689mkP lt l r (App s f a) = let f' = if (r /= f) then mkP lt l r f else f
690 a' = if (r /= a) then mkP lt l r a else a in
691 App s f' a'
692mkP lt l r (Bind n b sc)
693 = let b' = mkPB b
694 sc' = if (r /= sc) then mkP lt l r sc else sc in
695 Bind n b' sc'
696 where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
697 v' = if (r /= v) then mkP lt l r v else v in
698 Let t' v'
699 mkPB b = let ty = binderTy b
700 ty' = if (r /= ty) then mkP lt l r ty else ty in
701 b { binderTy = ty' }
702mkP lt l r x = x
704casetac :: Raw -> Bool -> RunTactic
705casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
706 (tmv, tmt) <- lift $ check ctxt env tm
707 let tmt' = normalise ctxt env tmt
708 let (tacn, tacstr, tactt) = if induction
709 then (ElimN, "eliminator", "Induction")
710 else (CaseN, "case analysis", "Case analysis")
711 case unApply tmt' of
712 (P _ tnm _, tyargs) -> do
713 case lookupTy (SN (tacn tnm)) ctxt of
714 [elimTy] -> do
715 param_pos <- case lookupMetaInformation tnm ctxt of
716 [DataMI param_pos] -> return param_pos
717 m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)
718 _ -> return []
719 let (params, indicies) = splitTyArgs param_pos tyargs
720 let args = getArgTys elimTy
721 let pmargs = take (length params) args
722 let args' = drop (length params) args
723 let propTy = head args'
724 let restargs = init $ tail args'
725 let consargs = take (length restargs - length indicies) $ restargs
726 let indxargs = drop (length restargs - length indicies) $ restargs
727 let scr = last $ tail args'
728 let indxnames = makeIndexNames indicies
729 currentNames <- query $ allTTNames . getProofTerm . pterm
730 let tmnm = case tm of
731 Var nm -> uniqueNameCtxt ctxt nm currentNames
732 _ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
733 let tmvar = P Bound tmnm tmt'
734 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
735 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)
736 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
737 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
738 action (\ps -> ps {holes = holes ps \\ [x],
739 recents = x : recents ps })
740 mapM_ addConsHole (reverse consargs')
741 let res' = forget $ res
742 (scv, sct) <- lift $ check ctxt env res'
743 let (scv', _) = specialise ctxt env [] scv
744 return scv'
745 [] -> lift $ tfail $ NoEliminator tacstr tmt'
746 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
747 _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")
748 tmt'
749 where scname = sMN 0 "scarg"
750 makeConsArg (nm, ty) = P Bound nm ty
751 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
752 bindConsArgs [] v = v
753 addConsHole (nm, ty) =
754 action (\ps -> ps { holes = nm : holes ps })
755 splitTyArgs param_pos tyargs =
756 let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs
757 in (map snd params, map snd indicies)
758 makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []
759 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
760 let var = P Bound idnm idxt
761 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
762induction tm induction ctxt env _ = do fail "Can't do induction here"
765equiv :: Raw -> RunTactic
766equiv tm ctxt env (Bind x (Hole t) sc) =
767 do (tmv, tmt) <- lift $ check ctxt env tm
768 lift $ converts ctxt env tmv t
769 return $ Bind x (Hole tmv) sc
770equiv tm ctxt env _ = fail "Can't equiv here"
772patbind :: Name -> RunTactic
773patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
774 do let t' = case t of
775 x@(Bind y (PVTy s) t) -> x
776 _ -> hnf ctxt env t
777 case t' of
778 Bind y (PVTy s) t -> let t' = updsubst y (P Bound n s) t in
779 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
780 _ -> fail "Nothing to pattern bind"
781patbind n ctxt env _ = fail "Can't pattern bind here"
783compute :: RunTactic
784compute ctxt env (Bind x (Hole ty) sc) =
785 do return $ Bind x (Hole (normalise ctxt env ty)) sc
786compute ctxt env t = return t
788hnf_compute :: RunTactic
789hnf_compute ctxt env (Bind x (Hole ty) sc) =
790 do let ty' = hnf ctxt env ty in
791-- trace ("HNF " ++ show (ty, ty')) $
792 return $ Bind x (Hole ty') sc
793hnf_compute ctxt env t = return t
795-- reduce let bindings only
796simplify :: RunTactic
797simplify ctxt env (Bind x (Hole ty) sc) =
798 do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc
799simplify ctxt env t = return t
801check_in :: Raw -> RunTactic
802check_in t ctxt env tm =
803 do (val, valty) <- lift $ check ctxt env t
804 addLog (showEnv env val ++ " : " ++ showEnv env valty)
805 return tm
807eval_in :: Raw -> RunTactic
808eval_in t ctxt env tm =
809 do (val, valty) <- lift $ check ctxt env t
810 let val' = normalise ctxt env val
811 let valty' = normalise ctxt env valty
812 addLog (showEnv env val ++ " : " ++
813 showEnv env valty ++
814-- " in " ++ show env ++
815 " ==>\n " ++
816 showEnv env val' ++ " : " ++
817 showEnv env valty')
818 return tm
820start_unify :: Name -> RunTactic
821start_unify n ctxt env tm = do -- action (\ps -> ps { unified = (n, []) })
822 return tm
824tmap f (a, b, c) = (f a, b, c)
826solve_unified :: RunTactic
827solve_unified ctxt env tm =
828 do ps <- get
829 let (_, ns) = unified ps
830 let unify = dropGiven (dontunify ps) ns (holes ps)
831 action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
832 holes ps \\ map fst unify,
833 recents = recents ps ++ map fst unify })
834 action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
835 return (updateSolvedTerm unify tm)
837dropGiven du [] hs = []
838dropGiven du ((n, P Bound t ty) : us) hs
839 | n `elem` du && not (t `elem` du)
840 && n `elem` hs && t `elem` hs
841 = (t, P Bound n ty) : dropGiven du us hs
842dropGiven du (u@(n, _) : us) hs
843 | n `elem` du = dropGiven du us hs
844-- dropGiven du (u@(_, P a n ty) : us) | n `elem` du = dropGiven du us
845dropGiven du (u : us) hs = u : dropGiven du us hs
847keepGiven du [] hs = []
848keepGiven du ((n, P Bound t ty) : us) hs
849 | n `elem` du && not (t `elem` du)
850 && n `elem` hs && t `elem` hs
851 = keepGiven du us hs
852keepGiven du (u@(n, _) : us) hs
853 | n `elem` du = u : keepGiven du us hs
854keepGiven du (u : us) hs = keepGiven du us hs
856updateEnv [] e = e
857updateEnv ns [] = []
858updateEnv ns ((n, b) : env)
859 = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
861updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t
862updateProv ns p = p
864updateError [] err = err
865updateError ns (At f e) = At f (updateError ns e)
866updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
867updateError ns (ElaboratingArg f a env e)
868 = ElaboratingArg f a env (updateError ns e)
869updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
870 = CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)
871 (updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
872updateError ns e = e
874solveInProblems x val [] = []
875solveInProblems x val ((l, r, env, err) : ps)
876 = ((psubst x val l, psubst x val r,
877 updateEnv [(x, val)] env, err) : solveInProblems x val ps)
879mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
880mergeNotunified env holes ns = mnu ns [] [] where
881 mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
882 mnu ((n, t):ns) ns_acc ps_acc
883 | Just t' <- lookup n ns, t /= t'
884 = mnu ns ((n,t') : ns_acc)
885 ((t,t',True, env,CantUnify True (t, Nothing) (t', Nothing) (Msg "") [] 0, [],Match) : ps_acc)
886 | otherwise = mnu ns ((n,t) : ns_acc) ps_acc
888updateNotunified [] nu = nu
889updateNotunified ns nu = up nu where
890 up [] = []
891 up ((n, t) : nus) = let t' = updateSolvedTerm ns t in
892 ((n, t') : up nus)
894getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
895getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)
896getProvenance _ = (Nothing, Nothing)
898updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
899 -> ([(Name, TT Name)], Fails)
900-- updateProblems ctxt [] ps inj holes = ([], ps)
901updateProblems ps updates probs = up updates probs where
902 hs = holes ps
903 inj = injective ps
904 ctxt = context ps
905 ulog = unifylog ps
906 usupp = map fst (notunified ps)
907 dont = dontunify ps
909 up ns [] = (ns, [])
910 up ns (prob@(x, y, ready, env, err, while, um) : ps) =
911 let (x', newx) = updateSolvedTerm' ns x
912 (y', newy) = updateSolvedTerm' ns y
913 (lp, rp) = getProvenance err
914 err' = updateError ns err
915 env' = updateEnv ns env in
916 if newx || newy || ready ||
917 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
918 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of
919 OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $
920 let v' = filter (\(n, _) -> n `notElem` dont) v in
921 up (ns ++ v') ps
922 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $
923 let (ns', ps') = up ns ps in
924 (ns', (x',y', False, env',err', while, um) : ps')
925 else -- trace ("SKIPPING " ++ show (x,y,ready)) $
926 let (ns', ps') = up ns ps in
927 (ns', (x',y', False, env',err', while, um) : ps')
929-- attempt to solve remaining problems with match_unify
930matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
931 -> ([(Name, TT Name)], Fails)
932matchProblems all ps updates probs = up updates probs where
933 hs = holes ps
934 inj = injective ps
935 ctxt = context ps
937 up ns [] = (ns, [])
938 up ns ((x, y, ready, env, err, while, um) : ps)
939 | all || um == Match =
940 let x' = updateSolvedTerm ns x
941 y' = updateSolvedTerm ns y
942 (lp, rp) = getProvenance err
943 err' = updateError ns err
944 env' = updateEnv ns env in
945 case match_unify ctxt env' (x', lp) (y', rp) inj hs while of
946 OK v -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
947 up (ns ++ v) ps
948 _ -> let (ns', ps') = up ns ps in
949 (ns', (x', y', True, env', err', while, um) : ps')
950 up ns (p : ps) = let (ns', ps') = up ns ps in
951 (ns', p : ps')
953processTactic :: Tactic -> ProofState -> TC (ProofState, String)
954processTactic QED ps = case holes ps of
955 [] -> do let tm = {- normalise (context ps) [] -} getProofTerm (pterm ps)
956 (tm', ty', _) <- recheck (context ps) [] (forget tm) tm
957 return (ps { done = True, pterm = mkProofTerm tm' },
958 "Proof complete: " ++ showEnv [] tm')
959 _ -> fail "Still holes to fill."
960processTactic ProofState ps = return (ps, showEnv [] (getProofTerm (pterm ps)))
961processTactic Undo ps = case previous ps of
962 Nothing -> Error . Msg $ "Nothing to undo."
963 Just pold -> return (pold, "")
964processTactic EndUnify ps
965 = let (h, ns_in) = unified ps
966 ns = dropGiven (dontunify ps) ns_in (holes ps)
967 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
968 (ns'', probs') = updateProblems ps ns' (problems ps)
969 tm' = updateSolved ns'' (pterm ps) in
970 traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $
971 return (ps { pterm = tm',
972 unified = (h, []),
973 problems = probs',
974 notunified = updateNotunified ns'' (notunified ps),
975 recents = recents ps ++ map fst ns'',
976 holes = holes ps \\ map fst ns'' }, "")
977processTactic UnifyAll ps
978 = let tm' = updateSolved (notunified ps) (pterm ps) in
979 return (ps { pterm = tm',
980 notunified = [],
981 recents = recents ps ++ map fst (notunified ps),
982 holes = holes ps \\ map fst (notunified ps) }, "")
983processTactic (Reorder n) ps
984 = do ps' <- execStateT (tactic (Just n) reorder_claims) ps
985 return (ps' { previous = Just ps, plog = "" }, plog ps')
986processTactic (ComputeLet n) ps
987 = return (ps { pterm = mkProofTerm $
988 computeLet (context ps) n
989 (getProofTerm (pterm ps)) }, "")
990processTactic UnifyProblems ps
991 = do let (ns', probs') = updateProblems ps [] (problems ps)
992 pterm' = updateSolved ns' (pterm ps)
993 traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $
994 return (ps { pterm = pterm', solved = Nothing, problems = probs',
995 previous = Just ps, plog = "",
996 notunified = updateNotunified ns' (notunified ps),
997 recents = recents ps ++ map fst ns',
998 holes = holes ps \\ (map fst ns') }, plog ps)
999processTactic (MatchProblems all) ps
1000 = do let (ns', probs') = matchProblems all ps [] (problems ps)
1001 (ns'', probs'') = matchProblems all ps ns' probs'
1002 pterm' = updateSolved ns'' (pterm ps)
1003 traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show (map fst ns'')) $
1004 return (ps { pterm = pterm', solved = Nothing, problems = probs'',
1005 previous = Just ps, plog = "",
1006 notunified = updateNotunified ns'' (notunified ps),
1007 recents = recents ps ++ map fst ns'',
1008 holes = holes ps \\ (map fst ns'') }, plog ps)
1009processTactic t ps
1010 = case holes ps of
1011 [] -> fail "Nothing to fill in."
1012 (h:_) -> do ps' <- execStateT (process t h) ps
1013 let (ns_in, probs')
1014 = case solved ps' of
1015 Just s -> traceWhen (unifylog ps)
1016 ("SOLVED " ++ show s ++ " " ++ show (dontunify ps')) $
1017 updateProblems ps' [s] (problems ps')
1018 _ -> ([], problems ps')
1019 -- rechecking problems may find more solutions, so
1020 -- apply them here
1021 let ns' = dropGiven (dontunify ps') ns_in (holes ps')
1022 let pterm'' = updateSolved ns' (pterm ps')
1023 traceWhen (unifylog ps)
1024 ("Updated problems after solve " ++ qshow probs' ++ "\n" ++
1025 "(Toplevel) Dropping holes: " ++ show (map fst ns')) $
1026 return (ps' { pterm = pterm'',
1027 solved = Nothing,
1028 problems = probs',
1029 notunified = updateNotunified ns' (notunified ps'),
1030 previous = Just ps, plog = "",
1031 recents = recents ps' ++ map fst ns',
1032 holes = holes ps' \\ (map fst ns')}, plog ps')
1034process :: Tactic -> Name -> StateT TState TC ()
1035process EndUnify _
1036 = do ps <- get
1037 let (h, _) = unified ps
1038 tactic (Just h) solve_unified
1039process t h = tactic (Just h) (mktac t)
1040 where mktac Attack = attack
1041 mktac (Claim n r) = claim n r
1042 mktac (ClaimFn n bn r) = claimFn n bn r
1043 mktac (Exact r) = exact r
1044 mktac (Fill r) = fill r
1045 mktac (MatchFill r) = match_fill r
1046 mktac (PrepFill n ns) = prep_fill n ns
1047 mktac CompleteFill = complete_fill
1048 mktac Solve = solve
1049 mktac (StartUnify n) = start_unify n
1050 mktac Compute = compute
1051 mktac Simplify = Idris.Core.ProofState.simplify
1052 mktac HNF_Compute = hnf_compute
1053 mktac (Intro n) = intro n
1054 mktac (IntroTy ty n) = introTy ty n
1055 mktac (Forall n i t) = forall n i t
1056 mktac (LetBind n t v) = letbind n t v
1057 mktac (ExpandLet n b) = expandLet n b
1058 mktac (Rewrite t) = rewrite t
1059 mktac (Induction t) = casetac t True
1060 mktac (CaseTac t) = casetac t False
1061 mktac (Equiv t) = equiv t
1062 mktac (PatVar n) = patvar n
1063 mktac (PatBind n) = patbind n
1064 mktac (CheckIn r) = check_in r
1065 mktac (EvalIn r) = eval_in r
1066 mktac (Focus n) = focus n
1067 mktac (Defer ns n) = defer ns n
1068 mktac (DeferType n t a) = deferType n t a
1069 mktac (Instance n) = instanceArg n
1070 mktac (AutoArg n) = autoArg n
1071 mktac (SetInjective n) = setinj n
1072 mktac (MoveLast n) = movelast n
1073 mktac (UnifyGoal r) = unifyGoal r