X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Fequality.ml;h=5248a6a924c84bf6f2b06c1d36c5f16bff12dd4a;hb=cbcd34fe15122eb9835a5226b98be1050b097d6a;hp=953635dbd8e65df346c11dbc45c0f683f4c3d42f;hpb=d5950e1810f3a6d89328f18c2c5796e54a907473;p=helm.git diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 953635dbd..5248a6a92 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -264,6 +264,12 @@ let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) = eq ;; +let mk_tmp_equality (weight,(ty,l,r,o),m) = + let id = -1 in + uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id +;; + + let open_equality (_,weight,proof,(ty,l,r,o),m,id) = (weight,proof,(ty,l,r,o),m,id) @@ -309,8 +315,8 @@ let rec string_of_proof_old ?(names=[]) = function let proof_of_id id = try - let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in - p,m,l,r + let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + p,l,r with Not_found -> assert false @@ -325,7 +331,7 @@ let string_of_proof_new ?(names=[]) p gp = | Utils.Left -> "left" | Utils.Right -> "right" in - let fst4 (x,_,_,_) = x in + let fst3 (x,_,_) = x in let rec aux margin name = let prefix = String.make margin ' ' ^ name ^ ": " in function | Exact t -> @@ -335,8 +341,8 @@ let string_of_proof_new ?(names=[]) p gp = Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n" prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos) (CicPp.pp pred names)^ - aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^ - aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2)) + aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ + aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) in aux 0 "" p ^ String.concat "\n" @@ -345,15 +351,26 @@ let string_of_proof_new ?(names=[]) p gp = (Printf.sprintf "GOAL: %s %d %s %s\n" (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^ - aux 1 (Printf.sprintf "%d " i) (fst4 (proof_of_id i))) + aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i))) gp) ;; +let rec depend eq id = + let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in + if id = ideq then true else + match p with + Exact _ -> false + | Step (_,(_,id1,(_,id2),_)) -> + let eq1 = Hashtbl.find id_to_eq id1 in + let eq2 = Hashtbl.find id_to_eq id2 in + depend eq1 id || depend eq1 id2 +;; + let ppsubst = ppsubst ~names:[] (* returns an explicit named subst and a list of arguments for sym_eq_URI *) -let build_ens_for_sym_eq sym_eq_URI termlist = - let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in +let build_ens uri termlist = + let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match obj with | Cic.Constant (_, _, _, uris, _) -> assert (List.length uris <= List.length termlist); @@ -380,7 +397,7 @@ let build_proof_term_old ?(noproof=Cic.Implicit None) proof = do_build_goal_proof proofbit proof | ProofSymBlock (termlist, proof) -> let proof = do_build_proof proof in - let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in + let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof]) | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) -> let t' = Cic.Lambda (name, ty, bo) in @@ -423,66 +440,337 @@ let build_proof_term_old ?(noproof=Cic.Implicit None) proof = do_build_proof proof ;; +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 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) + | _ -> t + in + let rec canonical t = + match t with + | 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 build_proof_step subst p1 p2 pos l r pred = + let p1 = apply_subst subst p1 in + let p2 = apply_subst subst p2 in + let l = apply_subst subst l in + let r = apply_subst subst r in + let pred = apply_subst subst pred in + let ty,body = (* Cic.Implicit None *) + match pred with + | Cic.Lambda (_,ty,body) -> ty,body + | _ -> assert false + in + let what, other = (* Cic.Implicit None, Cic.Implicit None *) + if pos = Utils.Left then l,r else r,l + in + let is_not_fixed t = + CicSubstitution.subst (Cic.Implicit None) t <> + CicSubstitution.subst (Cic.Rel 1) t + in + match body,pos with +(* + |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left -> + let third = CicSubstitution.subst (Cic.Implicit None) third in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + let uri_sym = LibraryObjects.sym_eq_URI ~eq in + mk_trans uri_trans ty other what third + (mk_sym uri_sym ty what other p2) p1 + |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right -> + let third = CicSubstitution.subst (Cic.Implicit None) third in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + mk_trans uri_trans ty other what third p2 p1 + |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left -> + let third = CicSubstitution.subst (Cic.Implicit None) third in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + mk_trans uri_trans ty third what other p1 p2 + |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right -> + let third = CicSubstitution.subst (Cic.Implicit None) third in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + let uri_sym = LibraryObjects.sym_eq_URI ~eq in + mk_trans uri_trans ty third what other p1 + (mk_sym uri_sym ty other what p2) + | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs + -> + let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + let pred_of t = CicSubstitution.subst t lhs in + let pred_of_what = pred_of what in + let pred_of_other = pred_of other in + (* p2 : what = other + * ==================================== + * inject p2: P(what) = P(other) + *) + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) + (inject ty lhs m r pmr) (inject ty lhs l m plm) + | _ -> + let liftedty = CicSubstitution.lift 1 ty in + let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in + let refl_eq_part = + Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] + in + (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other + (Cic.Lambda (Cic.Name "foo",ty, + (Cic.Appl + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) + refl_eq_part what p2) + in + mk_trans uri_trans ty pred_of_other pred_of_what rhs + (inject ty lhs what other p2) p1 + | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs + -> + let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + let pred_of t = CicSubstitution.subst t lhs in + let pred_of_what = pred_of what in + let pred_of_other = pred_of other in + (* p2 : what = other + * ==================================== + * inject p2: P(what) = P(other) + *) + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) + (inject ty lhs m l plm) + (inject ty lhs r m pmr) + | _ -> + let liftedty = CicSubstitution.lift 1 ty in + let lifted_pred_of_other = + CicSubstitution.lift 1 (pred_of other) in + let refl_eq_part = + Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] + in + mk_eq_ind (Utils.eq_ind_URI ()) ty other + (Cic.Lambda (Cic.Name "foo",ty, + (Cic.Appl + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) + refl_eq_part what p2 + in + mk_trans uri_trans ty pred_of_other pred_of_what rhs + (inject ty lhs what other p2) p1 + | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs + -> + let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + let pred_of t = CicSubstitution.subst t rhs in + let pred_of_what = pred_of what in + let pred_of_other = pred_of other in + (* p2 : what = other + * ==================================== + * inject p2: P(what) = P(other) + *) + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) + (inject ty lhs m r pmr) + (inject ty lhs l m plm) + | _ -> + let liftedty = CicSubstitution.lift 1 ty in + let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in + let refl_eq_part = + Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] + in + (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other + (Cic.Lambda (Cic.Name "foo",ty, + (Cic.Appl + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) + refl_eq_part what p2) + in + mk_trans uri_trans ty lhs pred_of_what pred_of_other + p1 (inject ty rhs other what p2) + | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs + -> + let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in + let uri_trans = LibraryObjects.trans_eq_URI ~eq in + let pred_of t = CicSubstitution.subst t rhs in + let pred_of_what = pred_of what in + let pred_of_other = pred_of other in + (* p2 : what = other + * ==================================== + * inject p2: P(what) = P(other) + *) + let rec inject ty lhs what other p2 = + match p2 with + | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) + when LibraryObjects.is_trans_eq_URI uri_trans -> + let ty,l,m,r,plm,pmr = open_trans ens tl in + (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) + (inject ty lhs m l plm) + (inject ty lhs r m pmr)) + | _ -> + let liftedty = CicSubstitution.lift 1 ty in + let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in + let refl_eq_part = + Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] + in + mk_eq_ind (Utils.eq_ind_URI ()) ty other + (Cic.Lambda (Cic.Name "foo",ty, + (Cic.Appl + [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) + refl_eq_part what p2 + in + mk_trans uri_trans ty lhs pred_of_what pred_of_other + p1 (inject ty rhs other what p2) +*) + | _, Utils.Left -> + mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2 + | _, Utils.Right -> + mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2 +;; + let build_proof_term_new proof = - let rec aux extra = function + let rec aux = function | Exact term -> term | Step (subst,(_, id1, (pos,id2), pred)) -> - let p,m1,_,_ = proof_of_id id1 in - let p1 = aux [] p in - let p,m3,l,r = proof_of_id id2 in - let p2 = aux [] p in - let p1 = apply_subst subst p1 in - let p2 = apply_subst subst p2 in - let l = apply_subst subst l in - let r = apply_subst subst r in - let pred = apply_subst subst pred in - let ty = (* Cic.Implicit None *) - match pred with - | Cic.Lambda (_,ty,_) -> ty - | _ -> assert false - in - let what, other = (* Cic.Implicit None, Cic.Implicit None *) - if pos = Utils.Left then l,r else r,l - in - let eq_URI = - match pos with - | Utils.Left -> Utils.eq_ind_URI () - | Utils.Right -> Utils.eq_ind_r_URI () - in - (Cic.Appl [ - Cic.Const (eq_URI, []); - ty; what; pred; p1; other; p2]) + let p,_,_ = proof_of_id id1 in + let p1 = aux p in + let p,l,r = proof_of_id id2 in + let p2 = aux p in + build_proof_step subst p1 p2 pos l r pred in - aux [] proof + aux proof +;; + +let wfo goalproof proof = + let rec aux acc id = + let p,_,_ = proof_of_id id in + match p with + | Exact _ -> if (List.mem id acc) then acc else id :: acc + | Step (_,(_,id1, (_,id2), _)) -> + let acc = if not (List.mem id1 acc) then aux acc id1 else acc in + let acc = if not (List.mem id2 acc) then aux acc id2 else acc in + id :: acc + in + let acc = + match proof with + | Exact _ -> [] + | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2 + in + List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof +;; -let build_goal_proof l refl= - let proof, subst = +let string_of_id names id = + try + let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + match p with + | Exact t -> + Printf.sprintf "%d = %s: %s = %s" id + (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) + | Step (_,(step,id1, (_,id2), _) ) -> + Printf.sprintf "%6d: %s %6d %6d %s = %s" id + (if step = SuperpositionRight then "SupR" else "Demo") + id1 id2 (CicPp.pp l names) (CicPp.pp r names) + with + Not_found -> assert false + +let pp_proof names goalproof proof = + String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ + "\ngoal is demodulated with " ^ + (String.concat " " + ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof))) +;; + +let build_goal_proof l initial = + let proof = List.fold_left - (fun (current_proof,current_subst) (pos,id,subst,pred) -> - let p,m,l,r = proof_of_id id in + (fun current_proof (pos,id,subst,pred) -> + let p,l,r = proof_of_id id in let p = build_proof_term_new p in - let p = apply_subst subst p in - let l = apply_subst subst l in - let r = apply_subst subst r in - let pred = apply_subst subst pred in - let ty = (* Cic.Implicit None *) - match pred with - | Cic.Lambda (_,ty,_) -> ty - | _ -> assert false - in - let what, other = (* Cic.Implicit None, Cic.Implicit None *) - if pos = Utils.Right then l,r else r,l - in - let eq_URI = - match pos with - | Utils.Left -> Utils.eq_ind_r_URI () - | Utils.Right -> Utils.eq_ind_URI () - in - ((Cic.Appl [Cic.Const (eq_URI, []); - ty; what; pred; current_proof; other; p]), subst @ current_subst)) - (refl,[]) l + let pos = if pos = Utils.Left then Utils.Right else Utils.Left in + build_proof_step subst current_proof p pos l r pred) + initial l in - proof + canonical proof ;; let refl_proof ty term =