From 04dc7b17e463fa9c75ac91e1df88bf37ed009914 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 19 Sep 2008 06:41:27 +0000 Subject: [PATCH] A temporary patch to demodulation theorem. --- .../tactics/paramodulation/equality.mli | 10 ++++ .../tactics/paramodulation/indexing.ml | 60 +++++++++---------- .../tactics/paramodulation/indexing.mli | 8 +-- .../tactics/paramodulation/saturation.ml | 4 +- 4 files changed, 46 insertions(+), 36 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli index 6eb48a036..20428af41 100644 --- a/helm/software/components/tactics/paramodulation/equality.mli +++ b/helm/software/components/tactics/paramodulation/equality.mli @@ -51,6 +51,16 @@ val draw_proof: (Cic.name option) list -> goal_proof -> proof -> int -> unit val pp_proofterm: Cic.term -> string + +val mk_eq_ind : + UriManager.uri -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term -> + Cic.term val mk_equality : equality_bag -> int * proof * diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 6942a6884..89bb0462b 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -919,50 +919,50 @@ let superposition_right bag ;; (** demodulation, when the target is a theorem *) -let rec demodulation_theorem bag newmeta env table theorem = +let rec demodulation_theorem bag env table theorem = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + let eq_uri = + match LibraryObjects.eq_URI() with + | Some u -> u + | None -> assert false in let metasenv, context, ugraph = env in - let maxmeta = ref newmeta in - let term, termty, metas = theorem in - let metasenv' = metas in - + let proof, theo, metas = theorem in let build_newtheorem (t, subst, menv, ug, eq_found) = let pos, equality = eq_found in let (_, proof', (ty, what, other, _), menv',id) = Equality.open_equality equality in - let what, other = if pos = Utils.Left then what, other else other, what in - let newterm, newty = - let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in -(* let bo' = apply_subst subst t in *) -(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*) -(* - let newproofold = - Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, - Equality.BasicProof (Equality.empty_subst,term)) - in - (Equality.build_proof_term_old newproofold, bo) -*) - (* TODO, not ported to the new proofs *) - if true then assert false; term, bo - in - !maxmeta, (newterm, newty, menv) - in - let res = - demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty + let peq = + match proof' with + | Equality.Exact p -> p + | _ -> assert false in + let what, other = + if pos = Utils.Left then what, other else other, what in + let newtheo = apply_subst subst (S.subst other t) in + let name = C.Name "x" in + let body = apply_subst subst t in + let pred = C.Lambda(name,ty,body) in + let newproof = + match pos with + | Utils.Left -> + Equality.mk_eq_ind eq_uri ty what pred proof other peq + | Utils.Right -> + Equality.mk_eq_ind eq_uri ty what pred proof other peq + in + newproof,newtheo in + let res = demodulation_aux bag metas context ugraph table 0 theo in match res with | Some t -> - let newmeta, newthm = build_newtheorem t in - let newt, newty, _ = newthm in - if Equality.meta_convertibility termty newty then - newmeta, newthm + let newproof, newtheo = build_newtheorem t in + if Equality.meta_convertibility theo newtheo then + newproof, newtheo else - demodulation_theorem bag newmeta env table newthm + demodulation_theorem bag env table (newproof,newtheo,[]) | None -> - newmeta, theorem + proof,theo ;; (*****************************************************************************) diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 7f464d248..bb8bbd295 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -90,11 +90,11 @@ val demodulation_goal : bool * Equality.goal val demodulation_theorem : Equality.equality_bag -> - 'a -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> - Index.t -> - Cic.term * Cic.term * Cic.metasenv -> - 'a * (Cic.term * Cic.term * Cic.metasenv) + Index.t -> + Cic.term * Cic.term * Cic.metasenv + -> Cic.term * Cic.term + val check_target: Equality.equality_bag -> Cic.context -> diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index 5df1d7d6f..a52109e46 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -711,7 +711,7 @@ let activate_theorem (active, passive) = ;; - +(* let simplify_theorems bag env theorems ?passive (active_list, active_table) = let pl, passive_table = match passive with @@ -741,7 +741,7 @@ let simplify_theorems bag env theorems ?passive (active_list, active_table) = let p_theorems = List.map (mapfun passive_table) p_theorems in List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems ;; - +*) let rec simpl bag eq_uri env e others others_simpl = let active = others @ others_simpl in -- 2.39.2