From: Alberto Griggio Date: Thu, 29 Sep 2005 12:25:45 +0000 (+0000) Subject: upgraded code to work with non-default equalities X-Git-Tag: V_0_7_2_3~278 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d2b3f3c816a651cbed998976a343f83cad1be69c;p=helm.git upgraded code to work with non-default equalities --- diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index e30d44034..a7b2c3039 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -228,8 +228,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty = (candidate, eq_URI)) in let c, other, eq_URI = - if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI - else right, left, HL.Logic.eq_ind_r_URI + if pos = Utils.Left then left, right, Utils.eq_ind_URI () + else right, left, Utils.eq_ind_r_URI () in if o <> U.Incomparable then try @@ -317,8 +317,8 @@ let rec find_all_matches ?(unif_fun=Inference.unification) (candidate, eq_URI)) in let c, other, eq_URI = - if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI - else right, left, HL.Logic.eq_ind_r_URI + if pos = Utils.Left then left, right, Utils.eq_ind_URI () + else right, left, Utils.eq_ind_r_URI () in if o <> U.Incomparable then try @@ -507,16 +507,6 @@ let rec demodulation_aux metasenv context ugraph table lift_amount term = ;; -let build_ens_for_sym_eq ty x y = - [(UriManager.uri_of_string - "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); - (UriManager.uri_of_string - "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); - (UriManager.uri_of_string - "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] -;; - - let build_newtarget_time = ref 0.;; @@ -555,7 +545,7 @@ let rec demodulation_equality newmeta env table sign target = incr demod_counter; let bo' = let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in - C.Appl [C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); + C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); S.lift 1 eq_ty; l; r] in if sign = Utils.Positive then @@ -574,13 +564,16 @@ let rec demodulation_equality newmeta env table sign target = (* let target' = *) let eq_found = let proof' = - let ens = - if pos = Utils.Left then - build_ens_for_sym_eq ty what other - else - build_ens_for_sym_eq ty other what +(* let ens = *) +(* if pos = Utils.Left then *) +(* build_ens_for_sym_eq ty what other *) +(* else *) +(* build_ens_for_sym_eq ty other what *) + let termlist = + if pos = Utils.Left then [ty; what; other] + else [ty; other; what] in - Inference.ProofSymBlock (ens, proof') + Inference.ProofSymBlock (termlist, proof') in let what, other = if pos = Utils.Left then what, other else other, what @@ -606,7 +599,7 @@ let rec demodulation_equality newmeta env table sign target = (* in *) let refl = C.Appl [C.MutConstruct (* reflexivity *) - (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + (LibraryObjects.eq_URI (), 0, 1, []); eq_ty; if is_left then right else left] in (bo, @@ -828,7 +821,8 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let bo'' = let l, r = if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r] + C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); + S.lift 1 eq_ty; l; r] in incr maxmeta; let metaproof = @@ -839,13 +833,17 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = (* let target' = *) let eq_found = let proof' = - let ens = - if pos = Utils.Left then - build_ens_for_sym_eq ty what other - else - build_ens_for_sym_eq ty other what +(* let ens = *) +(* if pos = Utils.Left then *) +(* build_ens_for_sym_eq ty what other *) +(* else *) +(* build_ens_for_sym_eq ty other what *) +(* in *) + let termlist = + if pos = Utils.Left then [ty; what; other] + else [ty; other; what] in - Inference.ProofSymBlock (ens, proof') + Inference.ProofSymBlock (termlist, proof') in let what, other = if pos = Utils.Left then what, other else other, what @@ -870,7 +868,7 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = (* in *) let refl = C.Appl [C.MutConstruct (* reflexivity *) - (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); + (LibraryObjects.eq_URI (), 0, 1, []); eq_ty; if ordering = U.Gt then right else left] in (bo', @@ -940,7 +938,8 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let bo'' = let l, r = if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in - C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty; l; r] + C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); + S.lift 1 eq_ty; l; r] in bo', Inference.ProofBlock ( @@ -1029,11 +1028,15 @@ let rec demodulation_goal newmeta env table goal = in let eq_found = let proof' = - let ens = - if pos = Utils.Left then build_ens_for_sym_eq ty what other - else build_ens_for_sym_eq ty other what +(* let ens = *) +(* if pos = Utils.Left then build_ens_for_sym_eq ty what other *) +(* else build_ens_for_sym_eq ty other what *) +(* in *) + let termlist = + if pos = Utils.Left then [ty; what; other] + else [ty; other; what] in - Inference.ProofSymBlock (ens, proof') + Inference.ProofSymBlock (termlist, proof') in let what, other = if pos = Utils.Left then what, other else other, what diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 474f0a4d1..ac9934000 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -21,7 +21,8 @@ and proof = (* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) (Utils.pos * equality) * proof | ProofGoalBlock of proof * proof (* equality *) - | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof +(* | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *) + | ProofSymBlock of Cic.term list * proof | SubProof of Cic.term * int * proof ;; @@ -45,6 +46,29 @@ let string_of_equality ?env = ;; +let build_ens_for_sym_eq sym_eq_URI termlist = + let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in + match obj with + | Cic.Constant (_, _, _, uris, _) -> + assert (List.length uris <= List.length termlist); + let rec aux = function + | [], tl -> [], tl + | (uri::uris), (term::tl) -> + let ens, args = aux (uris, tl) in + (uri, term)::ens, args + | _, _ -> assert false + in + aux (uris, termlist) + | _ -> assert false +(* [(UriManager.uri_of_string *) +(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); *) +(* (UriManager.uri_of_string *) +(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); *) +(* (UriManager.uri_of_string *) +(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] *) +;; + + let build_proof_term proof = let rec do_build_proof proof = match proof with @@ -55,12 +79,16 @@ let build_proof_term proof = | ProofGoalBlock (proofbit, proof) -> print_endline "found ProofGoalBlock, going up..."; do_build_goal_proof proofbit proof - | ProofSymBlock (ens, proof) -> +(* | ProofSymBlock (ens, proof) -> *) +(* let proof = do_build_proof proof in *) +(* Cic.Appl [ *) +(* Cic.Const (Utils.sym_eq_URI (), ens); (\* symmetry *\) *) +(* proof *) +(* ] *) + | ProofSymBlock (termlist, proof) -> let proof = do_build_proof proof in - Cic.Appl [ - Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *) - proof - ] + let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in + Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof]) | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) -> let t' = Cic.Lambda (name, ty, bo) in let proof' = @@ -1019,10 +1047,11 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) ;; -let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = +let find_equalities context proof = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in + let eq_uri = LibraryObjects.eq_URI () in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in let ok_types ty menv = List.for_all (fun (_, _, mt) -> mt = ty) menv @@ -1121,11 +1150,18 @@ let find_library_equalities dbd context status maxmeta = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in + let blacklist = + List.fold_left + (fun s u -> UriManager.UriSet.add u s) + equations_blacklist + [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); + eq_ind_r_URI ()] + in let candidates = List.fold_left (fun l uri -> let suri = UriManager.string_of_uri uri in - if UriManager.UriSet.mem uri equations_blacklist then + if UriManager.UriSet.mem uri blacklist then l else let t = CicUtil.term_of_uri uri in @@ -1136,8 +1172,8 @@ let find_library_equalities dbd context status maxmeta = [] (MetadataQuery.equations_for_goal ~dbd status) in - let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI - and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in + let eq_uri1 = eq_XURI () (* UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI *) + and eq_uri2 = LibraryObjects.eq_URI () in (* HelmLibraryObjects.Logic.eq_URI in *) let iseq uri = (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2) in @@ -1214,8 +1250,13 @@ let find_library_theorems dbd env status equalities_uris = let blacklist = let refl_equal = UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in - UriManager.UriSet.remove refl_equal - (UriManager.UriSet.union equalities_uris equations_blacklist) + let s = + UriManager.UriSet.remove refl_equal + (UriManager.UriSet.union equalities_uris equations_blacklist) + in + List.fold_left + (fun s u -> UriManager.UriSet.add u s) + s [sym_eq_URI (); trans_eq_URI (); eq_ind_URI (); eq_ind_r_URI ()] in let metasenv, context, ugraph = env in let candidates = @@ -1348,8 +1389,8 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = ;; -let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term = - let iseq uri = UriManager.eq uri eq_uri in +let term_is_equality term = + let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in match term with | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true | _ -> false @@ -1358,7 +1399,8 @@ let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term = exception TermIsNotAnEquality;; -let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term = +let equality_of_term proof term = + let eq_uri = LibraryObjects.eq_URI () in let iseq uri = UriManager.eq uri eq_uri in match term with | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri -> diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index d0556dd54..560af55da 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -18,7 +18,8 @@ and proof = (* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) (Utils.pos * equality) * proof | ProofGoalBlock of proof * proof (* equality *) - | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof +(* | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *) + | ProofSymBlock of Cic.term list * proof | SubProof of Cic.term * int * proof type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph @@ -54,8 +55,7 @@ val beta_expand: fresh metas... *) val find_equalities: - ?eq_uri:UriManager.uri -> Cic.context -> ProofEngineTypes.proof -> - int list * equality list * int + Cic.context -> ProofEngineTypes.proof -> int list * equality list * int exception TermIsNotAnEquality;; @@ -64,10 +64,9 @@ exception TermIsNotAnEquality;; raises TermIsNotAnEquality if term is not an equation. The first Cic.term is a proof of the equation *) -val equality_of_term: ?eq_uri:UriManager.uri -> Cic.term -> Cic.term -> - equality +val equality_of_term: Cic.term -> Cic.term -> equality -val term_is_equality: ?eq_uri:UriManager.uri -> Cic.term -> bool +val term_is_equality: Cic.term -> bool (** superposition_left env target source diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index bf9ec6897..ab39ff3de 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -1,6 +1,6 @@ -let configuration_file = ref "../helm/matita/matita.conf.xml";; +let configuration_file = ref "../../matita/matita.conf.xml";; -let core_notation_script = "../helm/matita/core_notation.moo";; +let core_notation_script = "../../matita/core_notation.moo";; let get_from_user ~(dbd:HMysql.dbd) = let rec get () = @@ -59,7 +59,7 @@ let _ = in Helm_registry.load_from !configuration_file; CicNotation.load_notation core_notation_script; -CicNotation.load_notation "../helm/matita/coq.ma"; +CicNotation.load_notation "../../matita/coq.ma"; let dbd = HMysql.quick_connect ~host:(Helm_registry.get "db.host") ~user:(Helm_registry.get "db.user") diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index bc935d7f7..4cf14ae18 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -875,7 +875,8 @@ let apply_equality_to_goal env equality goal = let module I = Inference in let metasenv, context, ugraph = env in let _, proof, (ty, left, right, _), metas, args = equality in - let eqterm = C.Appl [C.MutInd (HL.Logic.eq_URI, 0, []); ty; left; right] in + let eqterm = + C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in let gproof, gmetas, gterm = goal in try let subst, metasenv', _ = @@ -1969,7 +1970,8 @@ let saturate context_hyp @ thms else let refl_equal = - UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" + let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (us ^ "#xpointer(1/1/1)") in let t = CicUtil.term_of_uri refl_equal in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 2d5ee24ce..279346748 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -513,3 +513,12 @@ let string_of_pos = function | Left -> "Left" | Right -> "Right" ;; + + +let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ()) +let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ()) +let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ()) +let eq_XURI () = + let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in + UriManager.uri_of_string (s ^ "#xpointer(1/1/1)") +let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ()) diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 7814a4b88..910c4a651 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -45,3 +45,9 @@ val string_of_pos: pos -> string val compute_equality_weight: Cic.term -> Cic.term -> Cic.term -> int val debug_print: string Lazy.t -> unit + +val eq_ind_URI: unit -> UriManager.uri +val eq_ind_r_URI: unit -> UriManager.uri +val sym_eq_URI: unit -> UriManager.uri +val eq_XURI: unit -> UriManager.uri +val trans_eq_URI: unit -> UriManager.uri