From 5ca3189127b10847b4986330482f34157661bbcf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 29 Sep 2006 14:41:27 +0000 Subject: [PATCH] renamed inference in founif that is more appropriate --- helm/software/components/tactics/.depend | 22 ++++++------- helm/software/components/tactics/Makefile | 2 +- .../{inference.ml => founif.ml} | 0 .../{inference.mli => founif.mli} | 0 .../tactics/paramodulation/indexing.ml | 32 +++++++++---------- .../tactics/paramodulation/saturation.ml | 4 +-- 6 files changed, 30 insertions(+), 30 deletions(-) rename helm/software/components/tactics/paramodulation/{inference.ml => founif.ml} (100%) rename helm/software/components/tactics/paramodulation/{inference.mli => founif.mli} (100%) diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 5f8f9060e..2a44e78cc 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -11,7 +11,7 @@ paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/equality_retrieval.cmi: proofEngineTypes.cmi \ paramodulation/equality.cmi autoTypes.cmi autoCache.cmi -paramodulation/inference.cmi: paramodulation/subst.cmi +paramodulation/founif.cmi: paramodulation/subst.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/indexing.cmi: paramodulation/utils.cmi \ @@ -88,31 +88,31 @@ paramodulation/equality_retrieval.cmx: paramodulation/utils.cmx \ proofEngineTypes.cmx proofEngineHelpers.cmx metadataQuery.cmx \ paramodulation/equality.cmx autoTypes.cmx autoCache.cmx \ paramodulation/equality_retrieval.cmi -paramodulation/inference.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi paramodulation/inference.cmi -paramodulation/inference.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx paramodulation/inference.cmi +paramodulation/founif.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \ + paramodulation/founif.cmi +paramodulation/founif.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \ + paramodulation/founif.cmi paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/equality_indexing.cmi paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ paramodulation/equality.cmx paramodulation/equality_indexing.cmi paramodulation/indexing.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi paramodulation/inference.cmi \ + paramodulation/subst.cmi paramodulation/founif.cmi \ paramodulation/equality_indexing.cmi paramodulation/equality.cmi \ paramodulation/indexing.cmi paramodulation/indexing.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx paramodulation/inference.cmx \ + paramodulation/subst.cmx paramodulation/founif.cmx \ paramodulation/equality_indexing.cmx paramodulation/equality.cmx \ paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi \ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ - proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \ - paramodulation/indexing.cmi paramodulation/equality_retrieval.cmi \ + proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/indexing.cmi \ + paramodulation/founif.cmi paramodulation/equality_retrieval.cmi \ paramodulation/equality.cmi autoCache.cmi paramodulation/saturation.cmi paramodulation/saturation.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ - proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \ - paramodulation/indexing.cmx paramodulation/equality_retrieval.cmx \ + proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/indexing.cmx \ + paramodulation/founif.cmx paramodulation/equality_retrieval.cmx \ paramodulation/equality.cmx autoCache.cmx paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index 08df7d546..dee83c756 100644 --- a/helm/software/components/tactics/Makefile +++ b/helm/software/components/tactics/Makefile @@ -12,7 +12,7 @@ INTERFACE_FILES = \ paramodulation/subst.mli\ paramodulation/equality.mli\ paramodulation/equality_retrieval.mli\ - paramodulation/inference.mli\ + paramodulation/founif.mli\ paramodulation/equality_indexing.mli\ paramodulation/indexing.mli \ paramodulation/saturation.mli \ diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/founif.ml similarity index 100% rename from helm/software/components/tactics/paramodulation/inference.ml rename to helm/software/components/tactics/paramodulation/founif.ml diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/founif.mli similarity index 100% rename from helm/software/components/tactics/paramodulation/inference.mli rename to helm/software/components/tactics/paramodulation/founif.mli diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 34c601b35..546fff631 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -151,11 +151,11 @@ let check_target bag context target msg = (* try ignore(CicTypeChecker.type_of_aux' - metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph) + metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph) with e -> prerr_endline msg; - prerr_endline (Inference.string_of_proof proof); - prerr_endline (CicPp.ppterm (Inference.build_proof_term proof)); + prerr_endline (Founif.string_of_proof proof); + prerr_endline (CicPp.ppterm (Founif.build_proof_term proof)); prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left)); prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right)); raise e @@ -246,7 +246,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = ) else let do_match c = let subst', metasenv', ugraph' = - Inference.matching + Founif.matching metasenv metas context term (S.lift lift_amount c) ugraph in Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) @@ -259,7 +259,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = let res = try do_match c - with Inference.MatchingFailure -> + with Founif.MatchingFailure -> find_matches bag metasenv context ugraph lift_amount term termty tl in if Utils.debug_res then ignore (check_res res "find1"); @@ -267,7 +267,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = else let res = try do_match c - with Inference.MatchingFailure -> None + with Founif.MatchingFailure -> None in if Utils.debug_res then ignore (check_res res "find2"); match res with @@ -292,9 +292,9 @@ let find_matches metasenv context ugraph lift_amount term termty = (* as above, but finds all the matching equalities, and the matching condition - can be either Inference.matching or Inference.unification + can be either Founif.matching or Inference.unification *) -let rec find_all_matches ?(unif_fun=Inference.unification) +let rec find_all_matches ?(unif_fun=Founif.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in @@ -323,7 +323,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) res::(find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -343,7 +343,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification) find_all_matches ~unif_fun metasenv context ugraph lift_amount term termty tl with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> find_all_matches ~unif_fun metasenv context ugraph @@ -356,7 +356,7 @@ let find_all_matches find_all_matches ?unif_fun metasenv context ugraph lift_amount term termty l (*prerr_endline "CANDIDATES:"; - List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l; + List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l; prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int (List.length rc));*) ;; @@ -374,9 +374,9 @@ let subsumption_aux use_unification env table target = let metasenv = tmetas in let predicate, unif_fun = if use_unification then - Unification, Inference.unification + Unification, Founif.unification else - Matching, Inference.matching + Matching, Founif.matching in let leftr = match left with @@ -401,7 +401,7 @@ let subsumption_aux use_unification env table target = | None -> ok what leftorright tl | Some s -> Some (s, equation, leftorright <> pos )) with - | Inference.MatchingFailure + | Founif.MatchingFailure | CicUnification.UnificationFailure _ -> ok what leftorright tl in match ok right Utils.Left leftr with @@ -824,7 +824,7 @@ let superposition_right bag if ordering = U.Gt then newgoal, apply_subst s right else apply_subst s left, newgoal in let neworder = !Utils.compare_terms left right in - let newmenv = (* Inference.filter s *) m in + let newmenv = (* Founif.filter s *) m in let stat = (eq_ty, left, right, neworder) in let eq' = let w = Utils.compute_equality_weight stat in @@ -953,7 +953,7 @@ let build_newgoal bag context goal posu rule expansion = let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in bo, (newgoalproofstep::goalproof) in - let newmetasenv = (* Inference.filter subst *) menv in + let newmetasenv = (* Founif.filter subst *) menv in (newgoalproof, newmetasenv, newterm) ;; diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml index da4ef7826..b52e074fd 100644 --- a/helm/software/components/tactics/paramodulation/saturation.ml +++ b/helm/software/components/tactics/paramodulation/saturation.ml @@ -850,7 +850,7 @@ let check_if_goal_is_identity env = function (let _,context,_ = env in try let s,m,_ = - Inference.unification m m context left right CicUniv.empty_ugraph + Founif.unification m m context left right CicUniv.empty_ugraph in let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in let m = Subst.apply_subst_metasenv s m in @@ -1712,7 +1712,7 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let get_stats () = "" (* - <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ + <:show> ^ Indexing.get_stats () ^ Founif.get_stats () ^ Equality.get_stats () ;; *) -- 2.39.2