+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 =
+ let ens, args = build_ens uri [ty; what; pred; p1; other; p2] in
+ Cic.Appl (Cic.Const (uri, ens) :: args)
+;;
+
+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 (_,_,(Cic.Appl [Cic.MutInd (uri, 0,_);ty;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 context menv =
+ 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 context t =
+ match t with
+ | Cic.LetIn(name,bo,rest) ->
+ let context' = (Some (name,Cic.Def (bo,None)))::context in
+ Cic.LetIn(name,canonical context bo,canonical context' 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 context (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 context (mk_sym uri_sym ty m r p2))
+ (canonical context (mk_sym uri_sym ty l m p1))
+ | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) ->
+ let eq = LibraryObjects.eq_URI_of_eq_f_URI uri_feq in
+ let eq_f_sym =
+ Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
+ in
+ Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))
+ | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
+ when LibraryObjects.is_eq_URI uri -> t
+ | _ -> Cic.Appl (List.map (canonical context) args))
+ | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
+ | _ -> t
+ in
+ remove_refl (canonical context t)
+;;
+
+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 =
+ let ens, args = build_ens uri [ty; l; r] in
+ Cic.Appl (Cic.MutInd(uri,0,ens) :: args)
+;;
+
+let mk_refl uri ty t =
+ let ens, args = build_ens uri [ty; t] in
+ Cic.Appl (Cic.MutConstruct(uri,0,1,ens) :: args)
+;;
+
+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 mk_feq uri_feq ty ty1 left pred right t =
+ let ens, args = build_ens uri_feq [ty;ty1;pred;left;right;t] in
+ Cic.Appl (Cic.Const(uri_feq,ens) :: args)
+;;
+
+let rec look_ahead aux = function
+ | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) as t
+ 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 hole = Cic.Implicit (Some `Hole) in
+ let ty2 = CicSubstitution.subst hole ty2 in
+ aux ty1 (CicSubstitution.subst other lp) (CicSubstitution.subst other rp) hole ty2 t
+ | Cic.Lambda (n,s,t) -> Cic.Lambda (n,s,look_ahead aux t)
+ | t -> t
+;;
+
+let contextualize uri ty left right t =
+ let hole = Cic.Implicit (Some `Hole) in
+ (* aux [uri] [ty] [left] [right] [ctx] [ctx_ty] [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
+ * ctx_ty is the type of ctx
+ *)
+ let rec aux uri ty left right ctx_d ctx_ty t =
+ match t with
+ | 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 ctx_ty p)
+ | Cic.LetIn (name,body,rest) ->
+ Cic.LetIn (name,look_ahead (aux uri) body, aux uri ty left right ctx_d ctx_ty 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, ty2 =
+ 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 hole m in
+ let ctx_c = CicSubstitution.subst hole ctx_c in
+ let ty2 = CicSubstitution.subst hole ty2 in
+ m, ctx_c, ty2
+ 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 ty2 c_what m ctx_d ctx_ty p1
+ else
+ mk_sym uri_sym ctx_ty d_m dc_what
+ (aux uri ty2 m c_what ctx_d ctx_ty p1)
+ in
+ let p2 = (* p2: dc_other = dc_what *)
+ if avoid_eq_ind then
+ mk_sym uri_sym ctx_ty dc_what dc_other
+ (aux uri ty1 what other ctx_dc ctx_ty p2)
+ else
+ aux uri ty1 other what ctx_dc ctx_ty 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 ctx_ty dc_what d_m p1),
+ (mk_sym uri_sym ctx_ty dc_other dc_what p2)
+ in
+ mk_trans uri_trans ctx_ty a b c paeqb pbeqc
+ | t when ctx_d = hole -> t
+ | t ->
+(* let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in *)
+(* let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in *)
+
+ let uri_feq = LibraryObjects.eq_f_URI ~eq:uri in
+ let pred =
+(* 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 ctx_ty in *)
+(* Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) *)
+ Cic.Lambda (Cic.Name "foo",ty,l)