@@ -49,6 +49,7 @@ data Tactic = Attack
4949 | EvalIn Raw
5050 | CheckIn Raw
5151 | Intro (Maybe Name)
52+ | IntroTy Raw (Maybe Name)
5253 | Forall Name Raw
5354 | LetBind Name Raw Raw
5455 | Rewrite Raw
@@ -264,6 +265,24 @@ solve ctxt env (Bind x (Guess ty val) sc)
264265 | otherwise = fail $ "I see a hole in your solution. " ++ showEnv env val
265266solve _ _ h = fail $ "Not a guess " ++ show h
266267
268+introTy :: Raw -> Maybe Name -> RunTactic
269+introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
270+ do let n = case mn of
271+ Just name -> name
272+ Nothing -> x
273+ let t' = normalise ctxt env t
274+ (tyv, tyt) <- lift $ check ctxt env ty
275+-- ns <- lift $ unify ctxt env tyv t'
276+ case t' of
277+ Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in
278+ do ns <- lift $ unify ctxt env s tyv
279+ ps <- get
280+ let (uh, uns) = unified ps
281+ put (ps { unified = (uh, uns ++ ns) })
282+ return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
283+ _ -> fail "Nothing to introduce"
284+introTy ty n ctxt env _ = fail "Can't introduce here."
285+
267286intro :: Maybe Name -> RunTactic
268287intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
269288 do let n = case mn of
@@ -406,25 +425,27 @@ process EndUnify _
406425 let (h, _) = unified ps
407426 tactic (Just h) solve_unified
408427process t h = tactic (Just h) (mktac t)
409− where mktac Attack = attack
410− mktac (Claim n r) = claim n r
411− mktac (Exact r) = exact r
412− mktac (Fill r) = fill r
428+ where mktac Attack = attack
429+ mktac (Claim n r) = claim n r
430+ mktac (Exact r) = exact r
431+ mktac (Fill r) = fill r
413432 mktac (PrepFill n ns) = prep_fill n ns
414− mktac CompleteFill = complete_fill
415− mktac Regret = regret
416− mktac Solve = solve
417− mktac (StartUnify n) = start_unify n
418− mktac Compute = compute
419− mktac (Intro n) = intro n
420− mktac (Forall n t) = forall n t
433+ mktac CompleteFill = complete_fill
434+ mktac Regret = regret
435+ mktac Solve = solve
436+ mktac (StartUnify n) = start_unify n
437+ mktac Compute = compute
438+ mktac (Intro n) = intro n
439+ mktac (IntroTy ty n) = introTy ty n
440+ mktac (Forall n t) = forall n t
421441 mktac (LetBind n t v) = letbind n t v
422− mktac (Rewrite t) = rewrite t
423− mktac (PatVar n) = patvar n
424− mktac (PatBind n) = patbind n
425− mktac (CheckIn r) = check_in r
426− mktac (EvalIn r) = eval_in r
427− mktac (Focus n) = focus n
428− mktac (Defer n) = defer n
429− mktac (Instance n) = instanceArg n
430− mktac (MoveLast n) = movelast n
442+ mktac (Rewrite t) = rewrite t
443+ mktac (PatVar n) = patvar n
444+ mktac (PatBind n) = patbind n
445+ mktac (CheckIn r) = check_in r
446+ mktac (EvalIn r) = eval_in r
447+ mktac (Focus n) = focus n
448+ mktac (Defer n) = defer n
449+ mktac (Instance n) = instanceArg n
450+ mktac (MoveLast n) = movelast n
451+