From d5950e1810f3a6d89328f18c2c5796e54a907473 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 26 Apr 2006 14:53:03 +0000 Subject: [PATCH] Build_proof_goal does not return the metasenv any more. --- components/tactics/paramodulation/equality.ml | 26 ++++++++----------- .../tactics/paramodulation/equality.mli | 5 ++-- components/tactics/paramodulation/indexing.ml | 3 ++- .../tactics/paramodulation/saturation.ml | 8 ++---- components/tactics/tactics.mli | 2 +- 5 files changed, 18 insertions(+), 26 deletions(-) diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 70f8f850f..953635dbd 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -425,12 +425,12 @@ let build_proof_term_old ?(noproof=Cic.Implicit None) proof = let build_proof_term_new proof = let rec aux extra = function - | Exact term -> term, [] + | Exact term -> term | Step (subst,(_, id1, (pos,id2), pred)) -> let p,m1,_,_ = proof_of_id id1 in - let p1,m2 = aux [] p in + let p1 = aux [] p in let p,m3,l,r = proof_of_id id2 in - let p2,m4 = aux [] p 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 @@ -451,23 +451,20 @@ let build_proof_term_new proof = in (Cic.Appl [ Cic.Const (eq_URI, []); - ty; what; pred; p1; other; p2]), - (apply_subst_metasenv subst (m1@m2@m3@m4)) + ty; what; pred; p1; other; p2]) in aux [] proof - -let build_goal_proof l (refl,reflmenv) = - let proof, menv, subst = +let build_goal_proof l refl= + let proof, subst = List.fold_left - (fun (current_proof,current_menv,current_subst) (pos,id,subst,pred) -> + (fun (current_proof,current_subst) (pos,id,subst,pred) -> let p,m,l,r = proof_of_id id in - let p,m1 = build_proof_term_new p 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 newm = apply_subst_metasenv subst (m@m1) in let ty = (* Cic.Implicit None *) match pred with | Cic.Lambda (_,ty,_) -> ty @@ -482,11 +479,10 @@ let build_goal_proof l (refl,reflmenv) = | Utils.Right -> Utils.eq_ind_URI () in ((Cic.Appl [Cic.Const (eq_URI, []); - ty; what; pred; current_proof; other; p]), - current_menv @ newm, subst @ current_subst)) - (refl,reflmenv,[]) l + ty; what; pred; current_proof; other; p]), subst @ current_subst)) + (refl,[]) l in - proof, menv + proof ;; let refl_proof ty term = diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index 9ef8d2197..4d48f22aa 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -80,10 +80,9 @@ val string_of_equality : ?env:Utils.environment -> equality -> string val string_of_proof_old : ?names:(Cic.name option)list -> old_proof -> string val string_of_proof_new : ?names:(Cic.name option)list -> new_proof -> goal_proof -> string -val build_proof_term_new: new_proof -> Cic.term * Cic.metasenv +val build_proof_term_new: new_proof -> Cic.term val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term -val build_goal_proof: - goal_proof -> (Cic.term * Cic.metasenv) -> Cic.term * Cic.metasenv +val build_goal_proof: goal_proof -> Cic.term -> Cic.term val refl_proof: Cic.term -> Cic.term -> Cic.term (** ensures that metavariables in equality are unique *) val fix_metas: int -> equality -> int * equality diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 1f9f5d576..f3314bfa0 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -602,7 +602,7 @@ let rec demodulation_equality ?from newmeta env table sign target = let order = !Utils.compare_terms left right in let stat = (eq_ty, left, right, order) in let w = Utils.compute_equality_weight stat in - let target = Equality.mk_equality (w, proof, stat, metas) in + (* let target = Equality.mk_equality (w, proof, stat, metas) in *) if Utils.debug_metas then ignore(check_target context target "demod equalities input"); let metasenv' = (* metasenv @ *) metas in @@ -745,6 +745,7 @@ let rec demodulation_equality ?from newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in + assert (not (Equality.meta_convertibility_eq target newtarget)); if (Equality.is_weak_identity newtarget) || (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index d5da5485f..4423661b0 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -857,7 +857,7 @@ let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = repl proof in let newcicp,np,subst,cicmenv = - cicproof,np, subst, (m @ menv) + cicproof,np, subst, Equality.apply_subst_metasenv subst (m @ menv) in Some ((newcicp,np,subst,cicmenv), @@ -1492,14 +1492,10 @@ let saturate let cic_proof = Equality.build_proof_term_old proof in (* generation of the new proof *) - let cic_proof_new,cic_proof_new_menv = + let cic_proof_new = Equality.build_goal_proof goalproof (Equality.build_proof_term_new newproof) in - let newproof_menv = - Equality.apply_subst_metasenv subsumption_subst - (newproof_menv @ cic_proof_new_menv) - in let cic_proof_new = Equality.apply_subst subsumption_subst cic_proof_new in diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 7d55e7589..67127e640 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 5 15:04:24 CEST 2006 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Apr 12 11:46:23 CEST 2006 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val assumption : ProofEngineTypes.tactic -- 2.39.2