-let rec injection_tac ~first_time ~term ~liftno ~continuation =
- let module C = Cic in
- let module CR = CicReduction in
- let module U = UriManager in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let module PST = ProofEngineStructuralRules in
- let module PET = ProofEngineTypes in
- let are_convertible hd1 hd2 metasenv context =
- fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
- in
- let injection_tac ~term status =
- let (proof, goal) = status in
- let _,metasenv,_subst, _,_, _ = proof in
- let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term = CicSubstitution.lift liftno term in
- let termty,_ =
- CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
- in
- debug_print (lazy ("\ninjection su: " ^ pp context termty));
- let tac =
- match termty with
- | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
- when LibraryObjects.is_eq_URI equri -> begin
- match (CicReduction.whd ~delta:true context tty) with
- | C.MutInd (turi,typeno,ens)
- | C.Appl (C.MutInd (turi,typeno,ens)::_) -> begin
- match t1,t2 with
- | C.MutConstruct (uri1,typeno1,consno1,ens1),
- C.MutConstruct (uri2,typeno2,consno2,ens2)
- when (uri1 = uri2) && (typeno1 = typeno2) &&
- (consno1 = consno2) && (ens1 = ens2) ->
- if first_time then raise exn_nothingtodo
- else continuation ~liftno
- | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
- C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
- when (uri1 = uri2) && (typeno1 = typeno2) &&
- (consno1 = consno2) && (ens1 = ens2) ->
- let rec traverse_list i l1 l2 =
- match l1,l2 with
- | [],[] when first_time -> continuation
- | [],[] -> begin
- match term with
- | C.Rel n -> begin
- match List.nth context (n-1) with
- | Some (C.Name id,_) ->
- fun ~liftno ->
- T.then_ ~start:(PST.clear ~hyps:[id])
- ~continuation:(continuation ~liftno)
- | _ -> assert false
- end
- | _ -> assert false
- end
- | hd1::tl1,hd2::tl2 ->
- if are_convertible hd1 hd2 metasenv context then
- traverse_list (i+1) tl1 tl2
- else
- injection1_tac ~i ~term
- ~continuation:(traverse_list (i+1) tl1 tl2)
- | _ -> assert false
- (* i 2 termini hanno in testa lo stesso costruttore,
- * ma applicato a un numero diverso di termini *)
- in
- traverse_list 1 applist1 applist2 ~liftno
- | C.MutConstruct (uri1,typeno1,consno1,ens1),
- C.MutConstruct (uri2,typeno2,consno2,ens2)
- | C.MutConstruct (uri1,typeno1,consno1,ens1),
- C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
- | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
- C.MutConstruct (uri2,typeno2,consno2,ens2)
- | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
- C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
- when (consno1 <> consno2) || (ens1 <> ens2) ->
- discriminate_tac ~term
- | _ when not first_time -> continuation ~liftno
- | _ (* when first_time *) ->
- match term with
- | Cic.Rel i ->
- let name =
- match List.nth context (i-1) with
- | Some (Cic.Name s, Cic.Def _) -> s
- | Some (Cic.Name s, Cic.Decl _) -> s
- | _ -> assert false
- in
- Tacticals.then_
- ~start:(ReductionTactics.simpl_tac
- ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None))
- ~continuation:(injection_tac ~first_time:false ~term ~liftno
- ~continuation)
- | _ -> raise exn_nonproj
- end
- | _ when not first_time -> continuation ~liftno
- | _ (* when first_time *) -> raise exn_nonproj
- end
- | _ -> raise exn_nonproj
- in
- PET.apply_tactic tac status
- in
- PET.mk_tactic (injection_tac ~term)
-
-and injection1_tac ~term ~i ~liftno ~continuation =
- let module C = Cic in
- let module CTC = CicTypeChecker in
- let module CU = CicUniv in
- let module S = CicSubstitution in
- let module U = UriManager in
- let module P = PrimitiveTactics in
- let module PET = ProofEngineTypes in
- let module T = Tacticals in