+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 (_,_,(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 head_of_apply = function | Cic.Appl (hd::_) -> hd | t -> t;;
+let tail_of_apply = function | Cic.Appl (_::tl) -> tl | t -> [];;
+let count_args t = List.length (tail_of_apply t);;
+let rec build_nat =
+ let u = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
+ function
+ | 0 -> Cic.MutConstruct(u,0,1,[])
+ | n ->
+ Cic.Appl [Cic.MutConstruct(u,0,2,[]);build_nat (n-1)]
+;;
+let tyof context menv t =
+ try
+ fst(CicTypeChecker.type_of_aux' menv context t CicUniv.empty_ugraph)
+ with
+ | CicTypeChecker.TypeCheckerFailure _
+ | CicTypeChecker.AssertFailure _ -> assert false
+;;
+let rec lambdaof left context = function
+ | Cic.Prod (n,s,t) ->
+ Cic.Lambda (n,s,lambdaof left context t)
+ | Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r]
+ when LibraryObjects.is_eq_URI uri -> if left then l else r
+ | t ->
+ let names = Utils.names_of_context context in
+ prerr_endline ("lambdaof: " ^ (CicPp.pp t names));
+ assert false
+;;
+
+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_f_sym =
+ Cic.Const (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_f1.con",[])
+ in
+ Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))
+
+(*
+ let sym_eq = Cic.Const(uri_sym,ens) in
+ let eq_f = Cic.Const(uri_feq,[]) in
+ let b = Cic.MutConstruct (UriManager.uri_of_string
+ "cic:/matita/datatypes/bool/bool.ind",0,1,[])
+ in
+ let u = ty1 in
+ let ctx = f in
+ let n = build_nat (count_args p) in
+ let h = head_of_apply p in
+ let predl = lambdaof true context (tyof context menv h) in
+ let predr = lambdaof false context (tyof context menv h) in
+ let args = tail_of_apply p in
+ let appl =
+ Cic.Appl
+ ([Cic.Const(UriManager.uri_of_string
+ "cic:/matita/paramodulation/rewrite.con",[]);
+ eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @
+ args)
+ in
+ appl
+*)
+(*
+ | 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 context) args))
+ | Cic.Appl l -> Cic.Appl (List.map (canonical context) l)
+ | _ -> t
+ in
+ remove_refl (canonical context 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 mk_feq uri_feq ty ty1 left pred right t =
+ Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
+;;
+
+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
+ * ty_ctx is the type of ctx_d
+ *)
+ let rec aux uri ty left right ctx_d ctx_ty = 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 ctx_ty p)
+ | Cic.LetIn (name,body,rest) ->
+ (* we should go in body *)
+ Cic.LetIn (name,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 =
+ UriManager.uri_of_string "cic:/matita/logic/equality/eq_f.con"