+let mk_sym uri ty t1 t2 p =
+ let ens, args = build_ens uri [ty;t1;t2;p] in
+ Cic.Appl (Cic.Const(uri, ens) :: args)
+;;
+
+let mk_trans uri ty t1 t2 t3 p12 p23 =
+ let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
+ Cic.Appl (Cic.Const (uri, ens) :: args)
+;;
+
+let mk_eq_ind uri ty what pred p1 other p2 =
+ Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
+;;
+
+let p_of_sym ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [_;_;_;p] -> p
+ | _ -> assert false
+;;
+
+let open_trans ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
+ | _ -> assert false
+;;
+
+let open_sym ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [ty;l;r;p] -> ty,l,r,p
+ | _ -> assert false
+;;
+
+let open_eq_ind args =
+ match args with
+ | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
+ | _ -> assert false
+;;
+
+let open_pred pred =
+ match pred with
+ | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r]))
+ when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
+ | _ -> prerr_endline (CicPp.ppterm pred); assert false
+;;
+
+let is_not_fixed t =
+ CicSubstitution.subst (Cic.Implicit None) t <>
+ CicSubstitution.subst (Cic.Rel 1) t
+;;
+
+
+let canonical t =
+ let rec remove_refl t =
+ match t with
+ | Cic.Appl (((Cic.Const(uri_trans,ens))::tl) as args)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,p1,p2 = open_trans ens tl in
+ (match p1,p2 with
+ | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
+ remove_refl p2
+ | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
+ remove_refl p1
+ | _ -> Cic.Appl (List.map remove_refl args))
+ | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
+ | Cic.LetIn (name,bo,rest) ->
+ Cic.LetIn (name,remove_refl bo,remove_refl rest)
+ | _ -> t
+ in
+ let rec canonical t =
+ match t with
+ | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
+ | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
+ when LibraryObjects.is_sym_eq_URI uri_sym ->
+ (match p_of_sym ens tl with
+ | Cic.Appl ((Cic.Const(uri,ens))::tl)
+ when LibraryObjects.is_sym_eq_URI uri ->
+ canonical (p_of_sym ens tl)
+ | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,p1,p2 = open_trans ens tl in
+ mk_trans uri_trans ty r m l
+ (canonical (mk_sym uri_sym ty m r p2))
+ (canonical (mk_sym uri_sym ty l m p1))
+ | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
+ when LibraryObjects.is_eq_ind_URI uri_ind ||
+ LibraryObjects.is_eq_ind_r_URI uri_ind ->
+ let ty, what, pred, p1, other, p2 =
+ match tl with
+ | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
+ | _ -> assert false
+ in
+ let pred,l,r =
+ match pred with
+ | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
+ when LibraryObjects.is_eq_URI uri ->
+ Cic.Lambda
+ (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
+ | _ ->
+ prerr_endline (CicPp.ppterm pred);
+ assert false
+ in
+ let l = CicSubstitution.subst what l in
+ let r = CicSubstitution.subst what r in
+ Cic.Appl
+ [he;ty;what;pred;
+ canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+ | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
+ when LibraryObjects.is_eq_URI uri -> t
+ | _ -> Cic.Appl (List.map canonical args))
+ | Cic.Appl l -> Cic.Appl (List.map canonical l)
+ | _ -> t
+ in
+ remove_refl (canonical t)
+;;
+
+let ty_of_lambda = function
+ | Cic.Lambda (_,ty,_) -> ty
+ | _ -> assert false
+;;
+
+let compose_contexts ctx1 ctx2 =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+;;
+
+let put_in_ctx ctx t =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
+;;
+
+let mk_eq uri ty l r =
+ Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
+;;
+
+let mk_refl uri ty t =
+ Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
+;;
+
+let open_eq = function
+ | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri ->
+ uri, ty, l ,r
+ | _ -> assert false
+;;
+
+let contextualize uri ty left right t =
+ let hole = Cic.Implicit (Some `Hole) in
+ (* aux [uri] [ty] [left] [right] [ctx] [t]
+ *
+ * the parameters validate this invariant
+ * t: eq(uri) ty left right
+ * that is used only by the base case
+ *
+ * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
+ *)
+ let rec aux uri ty left right ctx_d = function
+ | Cic.Appl ((Cic.Const(uri_sym,ens))::tl)
+ when LibraryObjects.is_sym_eq_URI uri_sym ->
+ let ty,l,r,p = open_sym ens tl in
+ mk_sym uri_sym ty l r (aux uri ty l r ctx_d p)
+ | Cic.LetIn (name,body,rest) ->
+ (* we should go in body *)
+ Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
+ | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
+ when LibraryObjects.is_eq_ind_URI uri_ind ||
+ LibraryObjects.is_eq_ind_r_URI uri_ind ->
+ let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+ let ty2,eq,lp,rp = open_pred pred in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+ let is_not_fixed_lp = is_not_fixed lp in
+ let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
+ (* extract the context and the fixed term from the predicate *)
+ let m, ctx_c =
+ let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
+ (* they were under a lambda *)
+ let m = CicSubstitution.subst (Cic.Implicit None) m in
+ let ctx_c = CicSubstitution.subst hole ctx_c in
+ m, ctx_c
+ in
+ (* create the compound context and put the terms under it *)
+ let ctx_dc = compose_contexts ctx_d ctx_c in
+ let dc_what = put_in_ctx ctx_dc what in
+ let dc_other = put_in_ctx ctx_dc other in
+ (* m is already in ctx_c so it is put in ctx_d only *)
+ let d_m = put_in_ctx ctx_d m in
+ (* we also need what in ctx_c *)
+ let c_what = put_in_ctx ctx_c what in
+ (* now put the proofs in the compound context *)
+ let p1 = (* p1: dc_what = d_m *)
+ if is_not_fixed_lp then
+ aux uri ty1 c_what m ctx_d p1
+ else
+ mk_sym uri_sym ty d_m dc_what
+ (aux uri ty1 m c_what ctx_d p1)
+ in
+ let p2 = (* p2: dc_other = dc_what *)
+ if avoid_eq_ind then
+ mk_sym uri_sym ty dc_what dc_other
+ (aux uri ty1 what other ctx_dc p2)
+ else
+ aux uri ty1 other what ctx_dc p2
+ in
+ (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
+ if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
+ let a,b,c,paeqb,pbeqc =
+ if is_not_fixed_lp then
+ dc_other,dc_what,d_m,p2,p1
+ else
+ d_m,dc_what,dc_other,
+ (mk_sym uri_sym ty dc_what d_m p1),
+ (mk_sym uri_sym ty dc_other dc_what p2)
+ in
+ mk_trans uri_trans ty a b c paeqb pbeqc
+ | t ->
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+ let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
+ let pred =
+ (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
+ let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in
+ let l =
+ let ctx_d = CicSubstitution.lift 1 ctx_d in
+ put_in_ctx ctx_d (Cic.Rel 1)
+ in
+ let lty = CicSubstitution.lift 1 ty in
+ Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))