From ba2372bd35aec412f5a7b61e5431236505567c43 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 26 Apr 2006 09:21:07 +0000 Subject: [PATCH] added a new type for proofs. --- components/tactics/.depend | 36 +- components/tactics/Makefile | 1 + components/tactics/autoTactic.ml | 2 +- components/tactics/paramodulation/equality.ml | 738 +++++++++++++++++ .../tactics/paramodulation/equality.mli | 115 +++ .../paramodulation/equality_indexing.ml | 36 +- .../paramodulation/equality_indexing.mli | 8 +- components/tactics/paramodulation/indexing.ml | 298 +++---- .../tactics/paramodulation/indexing.mli | 33 +- .../tactics/paramodulation/inference.ml | 751 ++---------------- .../tactics/paramodulation/inference.mli | 95 +-- .../tactics/paramodulation/saturation.ml | 423 +++++++--- components/tactics/paramodulation/utils.ml | 31 +- components/tactics/paramodulation/utils.mli | 5 + 14 files changed, 1474 insertions(+), 1098 deletions(-) create mode 100644 components/tactics/paramodulation/equality.ml create mode 100644 components/tactics/paramodulation/equality.mli diff --git a/components/tactics/.depend b/components/tactics/.depend index 10862a5b0..41cc4bb67 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -5,11 +5,13 @@ reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi -paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi +paramodulation/equality.cmi: paramodulation/utils.cmi +paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ + paramodulation/equality.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ - paramodulation/inference.cmi + paramodulation/equality.cmi paramodulation/indexing.cmi: paramodulation/utils.cmi \ - paramodulation/inference.cmi paramodulation/equality_indexing.cmi + paramodulation/equality_indexing.cmi paramodulation/equality.cmi paramodulation/saturation.cmi: proofEngineTypes.cmi variousTactics.cmi: proofEngineTypes.cmi autoTactic.cmi: proofEngineTypes.cmi @@ -56,30 +58,34 @@ metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi -paramodulation/inference.cmo: paramodulation/utils.cmi \ - proofEngineReduction.cmi proofEngineHelpers.cmi metadataQuery.cmi \ +paramodulation/equality.cmo: paramodulation/utils.cmi \ + proofEngineReduction.cmi paramodulation/equality.cmi +paramodulation/equality.cmx: paramodulation/utils.cmx \ + proofEngineReduction.cmx paramodulation/equality.cmi +paramodulation/inference.cmo: paramodulation/utils.cmi proofEngineHelpers.cmi \ + metadataQuery.cmi paramodulation/equality.cmi \ paramodulation/inference.cmi -paramodulation/inference.cmx: paramodulation/utils.cmx \ - proofEngineReduction.cmx proofEngineHelpers.cmx metadataQuery.cmx \ +paramodulation/inference.cmx: paramodulation/utils.cmx proofEngineHelpers.cmx \ + metadataQuery.cmx paramodulation/equality.cmx \ paramodulation/inference.cmi paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ - paramodulation/inference.cmi paramodulation/equality_indexing.cmi + paramodulation/equality.cmi paramodulation/equality_indexing.cmi paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ - paramodulation/inference.cmx paramodulation/equality_indexing.cmi + paramodulation/equality.cmx paramodulation/equality_indexing.cmi paramodulation/indexing.cmo: paramodulation/utils.cmi \ paramodulation/inference.cmi paramodulation/equality_indexing.cmi \ - paramodulation/indexing.cmi + paramodulation/equality.cmi paramodulation/indexing.cmi paramodulation/indexing.cmx: paramodulation/utils.cmx \ paramodulation/inference.cmx paramodulation/equality_indexing.cmx \ - paramodulation/indexing.cmi + paramodulation/equality.cmx paramodulation/indexing.cmi paramodulation/saturation.cmo: paramodulation/utils.cmi reductionTactics.cmi \ proofEngineTypes.cmi proofEngineReduction.cmi primitiveTactics.cmi \ paramodulation/inference.cmi paramodulation/indexing.cmi \ - paramodulation/saturation.cmi + paramodulation/equality.cmi paramodulation/saturation.cmi paramodulation/saturation.cmx: paramodulation/utils.cmx reductionTactics.cmx \ proofEngineTypes.cmx proofEngineReduction.cmx primitiveTactics.cmx \ paramodulation/inference.cmx paramodulation/indexing.cmx \ - paramodulation/saturation.cmi + paramodulation/equality.cmx paramodulation/saturation.cmi variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ variousTactics.cmi @@ -88,10 +94,10 @@ variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \ variousTactics.cmi autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \ proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \ - paramodulation/inference.cmi autoTactic.cmi + paramodulation/equality.cmi autoTactic.cmi autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \ - paramodulation/inference.cmx autoTactic.cmi + paramodulation/equality.cmx autoTactic.cmi introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ introductionTactics.cmi introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ diff --git a/components/tactics/Makefile b/components/tactics/Makefile index cb38579e1..2cecc0401 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -7,6 +7,7 @@ INTERFACE_FILES = \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ paramodulation/utils.mli \ + paramodulation/equality.mli\ paramodulation/inference.mli\ paramodulation/equality_indexing.mli\ paramodulation/indexing.mli \ diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index 42df90768..9db6ed1c9 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -334,7 +334,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation | Some _ -> let _, metasenv, _, _ = proof in let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - full || (Inference.term_is_equality meta_goal) + full || (Equality.term_is_equality meta_goal) in if paramodulation_ok then ( debug_print (lazy "USO PARAMODULATION..."); diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml new file mode 100644 index 000000000..70f8f850f --- /dev/null +++ b/components/tactics/paramodulation/equality.ml @@ -0,0 +1,738 @@ +(* cOpyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *) + + +(******* CIC substitution ***************************************************) + +type cic_substitution = Cic.substitution +let cic_apply_subst = CicMetaSubst.apply_subst +let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv +let cic_ppsubst = CicMetaSubst.ppsubst +let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail +let cic_flatten_subst subst = + List.map + (fun (i, (context, term, ty)) -> + let context = (* cic_apply_subst_context subst*) context in + let term = cic_apply_subst subst term in + let ty = cic_apply_subst subst ty in + (i, (context, term, ty))) subst +let rec cic_lookup_subst meta subst = + match meta with + | Cic.Meta (i, _) -> ( + try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst + in cic_lookup_subst t subst + with Not_found -> meta + ) + | _ -> meta +;; + +let cic_merge_subst_if_possible s1 s2 = + let already_in = Hashtbl.create 13 in + let rec aux acc = function + | ((i,_,x) as s)::tl -> + (try + let x' = Hashtbl.find already_in i in + if x = x' then aux acc tl else None + with + | Not_found -> + Hashtbl.add already_in i x; + aux (s::acc) tl) + | [] -> Some acc + in + aux [] (s1@s2) +;; + +(******** NAIF substitution **************************************************) +(* + * naif version of apply subst; the local context of metas is ignored; + * we assume the substituted term must be lifted according to the nesting + * depth of the meta. + * Alternatively, we could used implicit instead of metas + *) + +type naif_substitution = (int * Cic.term) list + +let naif_apply_subst subst term = + let rec aux k t = + match t with + Cic.Rel _ -> t + | Cic.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst + in + Cic.Var (uri, exp_named_subst') + | Cic.Meta (i, l) -> + (try + aux k (CicSubstitution.lift k (List.assoc i subst)) + with Not_found -> t) + | Cic.Sort _ + | Cic.Implicit _ -> t + | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty) + | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t) + | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t) + | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t) + | Cic.Appl [] -> assert false + | Cic.Appl l -> Cic.Appl (List.map (aux k) l) + | Cic.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst + in + if exp_named_subst' != exp_named_subst then + Cic.Const (uri, exp_named_subst') + else + t (* TODO: provare a mantenere il piu' possibile sharing *) + | Cic.MutInd (uri,typeno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst + in + Cic.MutInd (uri,typeno,exp_named_subst') + | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst + in + Cic.MutConstruct (uri,typeno,consno,exp_named_subst') + | Cic.MutCase (sp,i,outty,t,pl) -> + let pl' = List.map (aux k) pl in + Cic.MutCase (sp, i, aux k outty, aux k t, pl') + | Cic.Fix (i, fl) -> + let len = List.length fl in + let fl' = + List.map + (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl + in + Cic.Fix (i, fl') + | Cic.CoFix (i, fl) -> + let len = List.length fl in + let fl' = + List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl + in + Cic.CoFix (i, fl') +in + aux 0 term +;; + +(* naif version of apply_subst_metasenv: we do not apply the +substitution to the context *) + +let naif_apply_subst_metasenv subst metasenv = + List.map + (fun (n, context, ty) -> + (n, context, naif_apply_subst subst ty)) + (List.filter + (fun (i, _, _) -> not (List.mem_assoc i subst)) + metasenv) + +let naif_ppsubst names subst = + "{" ^ String.concat "; " + (List.map + (fun (idx, t) -> + Printf.sprintf "%d:= %s" idx (CicPp.pp t names)) + subst) ^ "}" +;; + +let naif_buildsubst n context t ty tail = (n,t) :: tail ;; + +let naif_flatten_subst subst = + List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst +;; + +let rec naif_lookup_subst meta subst = + match meta with + | Cic.Meta (i, _) -> + (try + naif_lookup_subst (List.assoc i subst) subst + with + Not_found -> meta) + | _ -> meta +;; + +let naif_merge_subst_if_possible s1 s2 = + let already_in = Hashtbl.create 13 in + let rec aux acc = function + | ((i,x) as s)::tl -> + (try + let x' = Hashtbl.find already_in i in + if x = x' then aux acc tl else None + with + | Not_found -> + Hashtbl.add already_in i x; + aux (s::acc) tl) + | [] -> Some acc + in + aux [] (s1@s2) +;; + +(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************) + +type substitution = naif_substitution +let apply_subst = naif_apply_subst +let apply_subst_metasenv = naif_apply_subst_metasenv +let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l +let buildsubst = naif_buildsubst +let flatten_subst = naif_flatten_subst +let lookup_subst = naif_lookup_subst + +(* filter out from metasenv the variables in substs *) +let filter subst metasenv = + List.filter + (fun (m, _, _) -> + try let _ = List.find (fun (i, _) -> m = i) subst in false + with Not_found -> true) + metasenv +;; + +let is_in_subst i subst = List.mem_assoc i subst;; + +let merge_subst_if_possible = naif_merge_subst_if_possible;; + +let empty_subst = [];; + +(********* EQUALITY **********************************************************) + +type rule = SuperpositionRight | SuperpositionLeft | Demodulation +type uncomparable = int -> int +type equality = + uncomparable * (* trick to break structural equality *) + int * (* weight *) + proof * + (Cic.term * (* type *) + Cic.term * (* left side *) + Cic.term * (* right side *) + Utils.comparison) * (* ordering *) + Cic.metasenv * (* environment for metas *) + int (* id *) +and proof = new_proof * old_proof + +and new_proof = + | Exact of Cic.term + | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *) +and old_proof = + | NoProof (* term is the goal missing a proof *) + | BasicProof of substitution * Cic.term + | ProofBlock of + substitution * UriManager.uri * + (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof + | ProofGoalBlock of old_proof * old_proof + | ProofSymBlock of Cic.term list * old_proof + | SubProof of Cic.term * int * old_proof +and goal_proof = (Utils.pos * int * substitution * Cic.term) list +;; + +(* globals *) +let maxid = ref 0;; +let id_to_eq = Hashtbl.create 1024;; + +let freshid () = + incr maxid; !maxid +;; + +let reset () = + maxid := 0; + Hashtbl.clear id_to_eq +;; + +let uncomparable = fun _ -> 0 + +let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) = + let id = freshid () in + let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in + Hashtbl.add id_to_eq id eq; + eq +;; + +let open_equality (_,weight,proof,(ty,l,r,o),m,id) = + (weight,proof,(ty,l,r,o),m,id) + +let string_of_equality ?env eq = + match env with + | None -> + let w, _, (ty, left, right, o), _ , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + id w (CicPp.ppterm ty) + (CicPp.ppterm left) + (Utils.string_of_comparison o) (CicPp.ppterm right) + | Some (_, context, _) -> + let names = Utils.names_of_context context in + let w, _, (ty, left, right, o), _ , id = open_equality eq in + Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" + id w (CicPp.pp ty names) + (CicPp.pp left names) (Utils.string_of_comparison o) + (CicPp.pp right names) +;; + +let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = + Pervasives.compare s1 s2 +;; + +let rec string_of_proof_old ?(names=[]) = function + | NoProof -> "NoProof " + | BasicProof (s, t) -> "BasicProof(" ^ + ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")" + | SubProof (t, i, p) -> + Printf.sprintf "SubProof(%s, %s, %s)" + (CicPp.pp t names) (string_of_int i) (string_of_proof_old p) + | ProofSymBlock (_,p) -> + Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p) + | ProofBlock (subst, _, _, _ ,(_,eq),old) -> + let _,(_,p),_,_,_ = open_equality eq in + "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^ + string_of_proof_old p ^ ")" + | ProofGoalBlock (p1, p2) -> + Printf.sprintf "ProofGoalBlock(%s, %s)" + (string_of_proof_old p1) (string_of_proof_old p2) +;; + + +let proof_of_id id = + try + let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in + p,m,l,r + with + Not_found -> assert false + + +let string_of_proof_new ?(names=[]) p gp = + let str_of_rule = function + | SuperpositionRight -> "SupR" + | SuperpositionLeft -> "SupL" + | Demodulation -> "Demod" + in + let str_of_pos = function + | Utils.Left -> "left" + | Utils.Right -> "right" + in + let fst4 (x,_,_,_) = x in + let rec aux margin name = + let prefix = String.make margin ' ' ^ name ^ ": " in function + | Exact t -> + Printf.sprintf "%sExact (%s)\n" + prefix (CicPp.pp t names) + | Step (subst,(rule,eq1,(pos,eq2),pred)) -> + 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)) + in + aux 0 "" p ^ + String.concat "\n" + (List.map + (fun (pos,i,s,t) -> + (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))) + gp) +;; + +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 + 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 +;; + +let build_proof_term_old ?(noproof=Cic.Implicit None) proof = + let rec do_build_proof proof = + match proof with + | NoProof -> + Printf.fprintf stderr "WARNING: no proof!\n"; + noproof + | BasicProof (s,term) -> apply_subst s term + | ProofGoalBlock (proofbit, proof) -> + print_endline "found ProofGoalBlock, going up..."; + 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 + 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 + let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in + let proof' = do_build_proof proof in + let eqproof = do_build_proof eqproof in + let what, other = + if pos = Utils.Left then what, other else other, what + in + apply_subst subst + (Cic.Appl [Cic.Const (eq_URI, []); ty; + what; t'; eqproof; other; proof']) + | SubProof (term, meta_index, proof) -> + let proof = do_build_proof proof in + let eq i = function + | Cic.Meta (j, _) -> i = j + | _ -> false + in + ProofEngineReduction.replace + ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term + + and do_build_goal_proof proofbit proof = + match proof with + | ProofGoalBlock (pb, p) -> + do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p)) + | _ -> do_build_proof (replace_proof proofbit proof) + + and replace_proof newproof = function + | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) -> + let eqproof' = replace_proof newproof eqproof in + ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof') + | ProofGoalBlock (pb, p) -> + let pb' = replace_proof newproof pb in + ProofGoalBlock (pb', p) + | BasicProof _ -> newproof + | SubProof (term, meta_index, p) -> + SubProof (term, meta_index, replace_proof newproof p) + | p -> p + in + do_build_proof proof +;; + +let build_proof_term_new proof = + let rec aux extra = function + | Exact term -> term, [] + | Step (subst,(_, id1, (pos,id2), pred)) -> + let p,m1,_,_ = proof_of_id id1 in + let p1,m2 = aux [] p in + let p,m3,l,r = proof_of_id id2 in + let p2,m4 = 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]), + (apply_subst_metasenv subst (m1@m2@m3@m4)) + in + aux [] proof + + +let build_goal_proof l (refl,reflmenv) = + let proof, menv, subst = + List.fold_left + (fun (current_proof,current_menv,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 = 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 + | _ -> 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]), + current_menv @ newm, subst @ current_subst)) + (refl,reflmenv,[]) l + in + proof, menv +;; + +let refl_proof ty term = + Cic.Appl + [Cic.MutConstruct + (LibraryObjects.eq_URI (), 0, 1, []); + ty; term] +;; + +let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;; + +let relocate newmeta menv = + let subst, metasenv, newmeta = + List.fold_right + (fun (i, context, ty) (subst, menv, maxmeta) -> + let irl = [] (* + CicMkImplicit.identity_relocation_list_for_metavariable context *) + in + let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in + let newmeta = maxmeta, context, ty in + newsubst, newmeta::menv, maxmeta+1) + menv ([], [], newmeta+1) + in + let metasenv = apply_subst_metasenv subst metasenv in + let subst = flatten_subst subst in + subst, metasenv, newmeta + + +let fix_metas newmeta eq = + let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in + (* debug + let _ , eq = + fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in + prerr_endline (string_of_equality eq); *) + let subst, metasenv, newmeta = relocate newmeta menv in + let ty = apply_subst subst ty in + let left = apply_subst subst left in + let right = apply_subst subst right in + let fix_proof = function + | NoProof -> NoProof + | BasicProof (subst',term) -> BasicProof (subst@subst',term) + | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) -> + (* + let newsubst = + List.map + (fun (i, (context, term, ty)) -> + let context = apply_subst_context subst context in + let term = apply_subst subst term in + let ty = apply_subst subst ty in + (i, (context, term, ty))) subst' in *) + ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p) + | p -> assert false + in + let fix_new_proof = function + | Exact p -> Exact (apply_subst subst p) + | Step (s,(r,id1,(pos,id2),pred)) -> + Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred)) + in + let new_p = fix_new_proof p1 in + let old_p = fix_proof p2 in + let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in + (* debug prerr_endline (string_of_equality eq); *) + newmeta+1, eq + +exception NotMetaConvertible;; + +let meta_convertibility_aux table t1 t2 = + let module C = Cic in + let rec aux ((table_l, table_r) as table) t1 t2 = + match t1, t2 with + | C.Meta (m1, tl1), C.Meta (m2, tl2) -> + let m1_binding, table_l = + try List.assoc m1 table_l, table_l + with Not_found -> m2, (m1, m2)::table_l + and m2_binding, table_r = + try List.assoc m2 table_r, table_r + with Not_found -> m1, (m2, m1)::table_r + in + if (m1_binding <> m2) || (m2_binding <> m1) then + raise NotMetaConvertible + else ( + try + List.fold_left2 + (fun res t1 t2 -> + match t1, t2 with + | None, Some _ | Some _, None -> raise NotMetaConvertible + | None, None -> res + | Some t1, Some t2 -> (aux res t1 t2)) + (table_l, table_r) tl1 tl2 + with Invalid_argument _ -> + raise NotMetaConvertible + ) + | C.Var (u1, ens1), C.Var (u2, ens2) + | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) -> + aux_ens table ens1 ens2 + | C.Cast (s1, t1), C.Cast (s2, t2) + | C.Prod (_, s1, t1), C.Prod (_, s2, t2) + | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) + | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) -> + let table = aux table s1 s2 in + aux table t1 t2 + | C.Appl l1, C.Appl l2 -> ( + try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2) + when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2 + | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2) + when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 -> + aux_ens table ens1 ens2 + | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2) + when (UriManager.eq u1 u2) && i1 = i2 -> + let table = aux table s1 s2 in + let table = aux table t1 t2 in ( + try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> ( + try + List.fold_left2 + (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) -> + if i1 <> i2 then raise NotMetaConvertible + else + let res = (aux res s1 s2) in aux res t1 t2) + table il1 il2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> ( + try + List.fold_left2 + (fun res (n1, s1, t1) (n2, s2, t2) -> + let res = aux res s1 s2 in aux res t1 t2) + table il1 il2 + with Invalid_argument _ -> raise NotMetaConvertible + ) + | t1, t2 when t1 = t2 -> table + | _, _ -> raise NotMetaConvertible + + and aux_ens table ens1 ens2 = + let cmp (u1, t1) (u2, t2) = + Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) + in + let ens1 = List.sort cmp ens1 + and ens2 = List.sort cmp ens2 in + try + List.fold_left2 + (fun res (u1, t1) (u2, t2) -> + if not (UriManager.eq u1 u2) then raise NotMetaConvertible + else aux res t1 t2) + table ens1 ens2 + with Invalid_argument _ -> raise NotMetaConvertible + in + aux table t1 t2 +;; + + +let meta_convertibility_eq eq1 eq2 = + let _, _, (ty, left, right, _), _,_ = open_equality eq1 in + let _, _, (ty', left', right', _), _,_ = open_equality eq2 in + if ty <> ty' then + false + else if (left = left') && (right = right') then + true + else if (left = right') && (right = left') then + true + else + try + let table = meta_convertibility_aux ([], []) left left' in + let _ = meta_convertibility_aux table right right' in + true + with NotMetaConvertible -> + try + let table = meta_convertibility_aux ([], []) left right' in + let _ = meta_convertibility_aux table right left' in + true + with NotMetaConvertible -> + false +;; + + +let meta_convertibility t1 t2 = + if t1 = t2 then + true + else + try + ignore(meta_convertibility_aux ([], []) t1 t2); + true + with NotMetaConvertible -> + false +;; + +exception TermIsNotAnEquality;; + +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 +;; + +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 -> + let o = !Utils.compare_terms t1 t2 in + let stat = (ty,t1,t2,o) in + let w = Utils.compute_equality_weight stat in + let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in + e + | _ -> + raise TermIsNotAnEquality +;; + +let is_weak_identity eq = + let _,_,(_,left, right,_),_,_ = open_equality eq in + left = right || meta_convertibility left right +;; + +let is_identity (_, context, ugraph) eq = + let _,_,(ty,left,right,_),menv,_ = open_equality eq in + left = right || + (* (meta_convertibility left right)) *) + fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph) +;; + + +let term_of_equality equality = + let _, _, (ty, left, right, _), menv, _= open_equality equality in + let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in + let argsno = List.length menv in + let t = + CicSubstitution.lift argsno + (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right]) + in + snd ( + List.fold_right + (fun (i,_,ty) (n, t) -> + let name = Cic.Name ("X" ^ (string_of_int n)) in + let ty = CicSubstitution.lift (n-1) ty in + let t = + ProofEngineReduction.replace + ~equality:eq ~what:[i] + ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t + in + (n-1, Cic.Prod (name, ty, t))) + menv (argsno, t)) +;; + diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli new file mode 100644 index 000000000..9ef8d2197 --- /dev/null +++ b/components/tactics/paramodulation/equality.mli @@ -0,0 +1,115 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +type substitution + +type rule = SuperpositionRight | SuperpositionLeft |Demodulation + +type equality + +and proof = new_proof * old_proof + +and new_proof = + Exact of Cic.term + | Step of substitution * (rule * int * (Utils.pos * int) * Cic.term) + +and old_proof = + NoProof + | BasicProof of substitution * Cic.term + | ProofBlock of substitution * UriManager.uri * (Cic.name * Cic.term) * + Cic.term * (Utils.pos * equality) * old_proof + | ProofGoalBlock of old_proof * old_proof + | ProofSymBlock of Cic.term list * old_proof + | SubProof of Cic.term * int * old_proof + +and goal_proof = (Utils.pos * int * substitution * Cic.term) list + + +val empty_subst : substitution +val apply_subst : substitution -> Cic.term -> Cic.term +val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv +val ppsubst : substitution -> string +val buildsubst : + int -> Cic.context -> Cic.term -> Cic.term -> substitution -> + substitution +val flatten_subst : substitution -> substitution +val lookup_subst : Cic.term -> substitution -> Cic.term +val filter : substitution -> Cic.metasenv -> Cic.metasenv +val is_in_subst : int -> substitution -> bool +val merge_subst_if_possible: + substitution -> substitution -> + substitution option + +val reset : unit -> unit + +val mk_equality : + int * proof * + (Cic.term * Cic.term * Cic.term * Utils.comparison) * + Cic.metasenv -> + equality + +val open_equality : + equality -> + int * proof * + (Cic.term * Cic.term * Cic.term * Utils.comparison) * + Cic.metasenv * int +val compare : equality -> equality -> int +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_old: ?noproof:Cic.term -> old_proof -> Cic.term +val build_goal_proof: + goal_proof -> (Cic.term * Cic.metasenv) -> Cic.term * Cic.metasenv +val refl_proof: Cic.term -> Cic.term -> Cic.term +(** ensures that metavariables in equality are unique *) +val fix_metas: int -> equality -> int * equality +val metas_of_proof: proof -> int list + +exception TermIsNotAnEquality;; + +(** + raises TermIsNotAnEquality if term is not an equation. + The first Cic.term is a proof of the equation +*) +val equality_of_term: Cic.term -> Cic.term -> equality + +(** + Re-builds the term corresponding to this equality +*) +val term_of_equality: equality -> Cic.term +val term_is_equality: Cic.term -> bool + +(** tests a sort of alpha-convertibility between the two terms, but on the + metavariables *) +val meta_convertibility: Cic.term -> Cic.term -> bool + +(** meta convertibility between two equations *) +val meta_convertibility_eq: equality -> equality -> bool + +val is_weak_identity: equality -> bool +val is_identity: Utils.environment -> equality -> bool + diff --git a/components/tactics/paramodulation/equality_indexing.ml b/components/tactics/paramodulation/equality_indexing.ml index 4c07731d5..d5e5353e9 100644 --- a/components/tactics/paramodulation/equality_indexing.ml +++ b/components/tactics/paramodulation/equality_indexing.ml @@ -27,7 +27,7 @@ module type EqualityIndex = sig - module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality + module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality val arities : (Cic.term, int) Hashtbl.t type key = Cic.term type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t @@ -35,16 +35,18 @@ module type EqualityIndex = val retrieve_generalizations : t -> key -> PosEqSet.t val retrieve_unifiables : t -> key -> PosEqSet.t val init_index : unit -> unit - val remove_index : t -> Inference.equality -> t - val index : t -> Inference.equality -> t - val in_index : t -> Inference.equality -> bool + val remove_index : t -> Equality.equality -> t + val index : t -> Equality.equality -> t + val in_index : t -> Equality.equality -> bool end module DT = struct module OrderedPosEquality = struct - type t = Utils.pos * Inference.equality - let compare = Pervasives.compare + type t = Utils.pos * Equality.equality + let compare (p1,e1) (p2,e2) = + let rc = Pervasives.compare p1 p2 in + if rc = 0 then Equality.compare e1 e2 else rc end module PosEqSet = Set.Make(OrderedPosEquality);; @@ -58,7 +60,7 @@ struct ;; let remove_index tree equality = - let _, _, (_, l, r, ordering), _ = equality in + let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in match ordering with | Utils.Gt -> remove_index tree l (Utils.Left, equality) | Utils.Lt -> remove_index tree r (Utils.Right, equality) @@ -67,7 +69,7 @@ struct remove_index tree l (Utils.Left, equality) let index tree equality = - let _, _, (_, l, r, ordering), _ = equality in + let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in match ordering with | Utils.Gt -> index tree l (Utils.Left, equality) | Utils.Lt -> index tree r (Utils.Right, equality) @@ -77,9 +79,9 @@ struct let in_index tree equality = - let _, _, (_, l, r, ordering), _ = equality in + let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in let meta_convertibility (pos,equality') = - Inference.meta_convertibility_eq equality equality' + Equality.meta_convertibility_eq equality equality' in in_index tree l meta_convertibility || in_index tree r meta_convertibility @@ -88,8 +90,10 @@ struct module PT = struct module OrderedPosEquality = struct - type t = Utils.pos * Inference.equality - let compare = Pervasives.compare + type t = Utils.pos * Equality.equality + let compare (p1,e1) (p2,e2) = + let rc = Pervasives.compare p1 p2 in + if rc = 0 then Equality.compare e1 e2 else rc end module PosEqSet = Set.Make(OrderedPosEquality);; @@ -103,7 +107,7 @@ module PT = ;; let remove_index tree equality = - let _, _, (_, l, r, ordering), _ = equality in + let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in match ordering with | Utils.Gt -> remove_index tree l (Utils.Left, equality) | Utils.Lt -> remove_index tree r (Utils.Right, equality) @@ -112,7 +116,7 @@ module PT = remove_index tree l (Utils.Left, equality) let index tree equality = - let _, _, (_, l, r, ordering), _ = equality in + let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in match ordering with | Utils.Gt -> index tree l (Utils.Left, equality) | Utils.Lt -> index tree r (Utils.Right, equality) @@ -122,9 +126,9 @@ module PT = let in_index tree equality = - let _, _, (_, l, r, ordering), _ = equality in + let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in let meta_convertibility (pos,equality') = - Inference.meta_convertibility_eq equality equality' + Equality.meta_convertibility_eq equality equality' in in_index tree l meta_convertibility || in_index tree r meta_convertibility end diff --git a/components/tactics/paramodulation/equality_indexing.mli b/components/tactics/paramodulation/equality_indexing.mli index d7c3bec5e..58b28458d 100644 --- a/components/tactics/paramodulation/equality_indexing.mli +++ b/components/tactics/paramodulation/equality_indexing.mli @@ -25,7 +25,7 @@ module type EqualityIndex = sig - module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality + module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality val arities : (Cic.term, int) Hashtbl.t type key = Cic.term type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t @@ -33,9 +33,9 @@ module type EqualityIndex = val retrieve_generalizations : t -> key -> PosEqSet.t val retrieve_unifiables : t -> key -> PosEqSet.t val init_index : unit -> unit - val remove_index : t -> Inference.equality -> t - val index : t -> Inference.equality -> t - val in_index : t -> Inference.equality -> bool + val remove_index : t -> Equality.equality -> t + val index : t -> Equality.equality -> t + val in_index : t -> Equality.equality -> bool end module DT : EqualityIndex diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index 873cc5698..d71e7c5a7 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -62,7 +62,7 @@ let string_of_res ?env = | Some (t, s, m, u, ((p,e), eq_URI)) -> Printf.sprintf "Some: (%s, %s, %s)" (Utils.string_of_pos p) - (Inference.string_of_equality ?env e) + (Equality.string_of_equality ?env e) (CicPp.ppterm t) ;; @@ -85,7 +85,7 @@ let print_candidates ?env mode term res = (List.map (fun (p, e) -> Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p) - (Inference.string_of_equality ?env e)) + (Equality.string_of_equality ?env e)) res)); ;; @@ -93,7 +93,7 @@ let print_candidates ?env mode term res = let indexing_retrieval_time = ref 0.;; -let apply_subst = Inference.apply_subst +let apply_subst = Equality.apply_subst let index = Index.index let remove_index = Index.remove_index @@ -103,7 +103,7 @@ let init_index = Index.init_index let check_disjoint_invariant subst metasenv msg = if (List.exists - (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv) + (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv) then begin prerr_endline ("not disjoint: " ^ msg); @@ -124,19 +124,20 @@ let check_for_duplicates metas msg = let check_res res msg = match res with Some (t, subst, menv, ug, (eq_found, eq_URI)) -> - let eqs = Inference.string_of_equality (snd eq_found) in + let eqs = Equality.string_of_equality (snd eq_found) in check_disjoint_invariant subst menv msg; check_for_duplicates menv (msg ^ "\nchecking " ^ eqs); | None -> () ;; let check_target context target msg = - let w, proof, (eq_ty, left, right, order), metas = target in + let w, proof, (eq_ty, left, right, order), metas,_ = + Equality.open_equality target in (* check that metas does not contains duplicates *) - let eqs = Inference.string_of_equality target in + let eqs = Equality.string_of_equality target in let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in - let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right) - @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in + let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right) + @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in let _ = if menv <> metas then begin @@ -177,13 +178,6 @@ let check_target context target msg = the position will always be Left, and if the ordering is left < right, position will be Right. *) -let local_max = ref 100;; - -let make_variant (p,eq) = - let maxmeta, eq = Inference.fix_metas !local_max eq in - local_max := maxmeta; - p, eq -;; let get_candidates ?env mode tree term = let t1 = Unix.gettimeofday () in @@ -245,17 +239,21 @@ let rec find_matches metasenv context ugraph lift_amount term termty = function | [] -> None | candidate::tl -> - let pos, (_, proof, (ty, left, right, o), metas) = candidate in + let pos, equality = candidate in + let (_, proof, (ty, left, right, o), metas,_) = + Equality.open_equality equality in if Utils.debug_metas then ignore(check_target context (snd candidate) "find_matches"); if Utils.debug_res then begin - let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in - let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in - let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in - let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in + let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in + let t="t = " ^ (CicPp.ppterm term) ^ "\n" in + let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in + let p="proof = "^ + (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n" + in check_for_duplicates metas "gia nella metas"; - check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p) + check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p) end; if check && not (fst (CicReduction.are_convertible ~metasenv context termty ty ugraph)) then ( @@ -332,7 +330,8 @@ let rec find_all_matches ?(unif_fun=Inference.unification) function | [] -> [] | candidate::tl -> - let pos, (_, _, (ty, left, right, o), metas) = candidate in + let pos, equality = candidate in + let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in let do_match c eq_URI = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in @@ -414,24 +413,9 @@ let subsumption env table target = ((pos,equation),_)) -> Inference.string_of_equality equation)l)) in *) - let _, _, (ty, left, right, _), tmetas = target in + let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in let metasenv, context, ugraph = env in let metasenv = tmetas in - let merge_if_possible s1 s2 = - let already_in = Hashtbl.create 13 in - let rec aux acc = function - | ((i,x) as s)::tl -> - (try - let x' = Hashtbl.find already_in i in - if x = x' then aux acc tl else None - with - | Not_found -> - Hashtbl.add already_in i x; - aux (s::acc) tl) - | [] -> Some acc - in - aux [] (s1@s2) - in let leftr = match left with | Cic.Meta _ -> [] @@ -444,7 +428,7 @@ let subsumption env table target = let rec ok what = function | [] -> None | (_, subst, menv, ug, ((pos,equation),_))::tl -> - let _, _, (_, l, r, o), m = equation in + let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in try let other = if pos = Utils.Left then r else l in let subst', menv', ug' = @@ -461,7 +445,7 @@ let subsumption env table target = match_unif_time_no := !match_unif_time_no +. (t2 -. t1); raise e in - (match merge_if_possible subst subst' with + (match Equality.merge_subst_if_possible subst subst' with | None -> ok what tl | Some s -> Some (s, equation)) with Inference.MatchingFailure -> @@ -499,11 +483,10 @@ let rec demodulation_aux ?from ?(typecheck=false) if List.exists (fun (i,_,_) -> i = 2840) metasenv then (prerr_endline ("term: " ^(CicPp.ppterm term)); - List.iter (fun (_,x) -> prerr_endline (Inference.string_of_equality x)) + List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x)) candidates; prerr_endline ("-------"); prerr_endline ("+++++++")); -(* let candidates = List.map make_variant candidates in *) let res = match term with | C.Meta _ -> None @@ -610,14 +593,16 @@ let rec demodulation_equality ?from newmeta env table sign target = let module HL = HelmLibraryObjects in let module U = Utils in let metasenv, context, ugraph = env in - let w, proof, (eq_ty, left, right, order), metas = target in + let w, ((proof_new, proof_old) as proof), + (eq_ty, left, right, order), metas, id = + Equality.open_equality target in (* first, we simplify *) let right = U.guarded_simpl context right in let left = U.guarded_simpl context left in 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 = 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 @@ -630,18 +615,22 @@ let rec demodulation_equality ?from newmeta env table sign target = begin ignore(check_for_duplicates menv "input1"); ignore(check_disjoint_invariant subst menv "input2"); - let substs = Inference.ppsubst subst in + let substs = Equality.ppsubst subst in ignore(check_target context (snd eq_found) ("input3" ^ substs)) end; - let pos, (_, proof', (ty, what, other, _), menv') = eq_found in + let pos, equality = eq_found in + let (_, (proof'_new,proof'_old), + (ty, what, other, _), menv',id') = Equality.open_equality equality in let ty = - try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) + try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) with CicUtil.Meta_not_found _ -> ty in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = - let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in - let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in + let bo = + Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in +(* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*) + let name = C.Name "x" in incr demod_counter; let bo' = let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in @@ -650,46 +639,55 @@ let rec demodulation_equality ?from newmeta env table sign target = in if sign = Utils.Positive then (bo, - Inference.ProofBlock ( - subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof)) + (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'), + (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))), + Equality.ProofBlock ( + subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old))) else + assert false +(* begin prerr_endline "***************************************negative"; let metaproof = incr maxmeta; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in -(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) -(* print_newline (); *) +(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) +(* print_newline (); *) C.Meta (!maxmeta, irl) in let eq_found = - let proof' = + let proof'_old' = let termlist = if pos = Utils.Left then [ty; what; other] else [ty; other; what] in - Inference.ProofSymBlock (termlist, proof') + Equality.ProofSymBlock (termlist, proof'_old) in + let proof'_new' = assert false (* not implemented *) in let what, other = if pos = Utils.Left then what, other else other, what in - pos, (0, proof', (ty, other, what, Utils.Incomparable),menv') + pos, + Equality.mk_equality + (0, (proof'_new',proof'_old'), + (ty, other, what, Utils.Incomparable),menv') in let target_proof = let pb = - Inference.ProofBlock + Equality.ProofBlock (subst, eq_URI, (name, ty), bo', - eq_found, Inference.BasicProof ([],metaproof)) + eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) in - match proof with - | Inference.BasicProof _ -> + assert false, (* not implemented *) + (match snd proof with + | Equality.BasicProof _ -> (* print_endline "replacing a BasicProof"; *) pb - | Inference.ProofGoalBlock (_, parent_proof) -> + | Equality.ProofGoalBlock (_, parent_proof) -> (* print_endline "replacing another ProofGoalBlock"; *) - Inference.ProofGoalBlock (pb, parent_proof) - | _ -> assert false + Equality.ProofGoalBlock (pb, parent_proof) + | _ -> assert false) in let refl = C.Appl [C.MutConstruct (* reflexivity *) @@ -697,23 +695,28 @@ let rec demodulation_equality ?from newmeta env table sign target = eq_ty; if is_left then right else left] in (bo, - Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof)) - end + (assert false, (* not implemented *) + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof))) + end +*) in let newmenv = (* Inference.filter subst *) menv in let _ = if Utils.debug_metas then try ignore(CicTypeChecker.type_of_aux' - newmenv context (Inference.build_proof_term newproof) ugraph); + newmenv context + (Equality.build_proof_term_old (snd newproof)) ugraph); () with exc -> prerr_endline "sempre lui"; - prerr_endline (Inference.ppsubst subst); - prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof)); + prerr_endline (Equality.ppsubst subst); + prerr_endline (CicPp.ppterm + (Equality.build_proof_term_old (snd newproof))); prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t)); prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what)); prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other)); - prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst)); + prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst)); prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv [] newmenv)); raise exc; @@ -726,7 +729,8 @@ let rec demodulation_equality ?from newmeta env table sign target = build_newtarget_time := !build_newtarget_time +. (time2 -. time1); let res = let w = Utils.compute_equality_weight stat in - (w, newproof, stat,newmenv) in + Equality.mk_equality (w, newproof, stat,newmenv) + in if Utils.debug_metas then ignore(check_target context res "buildnew_target output"); !maxmeta, res @@ -741,8 +745,8 @@ let rec demodulation_equality ?from newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget true t in - if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || - (Inference.meta_convertibility_eq target newtarget) then + if (Equality.is_weak_identity newtarget) || + (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else demodulation_equality newmeta env table sign newtarget @@ -752,8 +756,8 @@ let rec demodulation_equality ?from newmeta env table sign target = match res with | Some t -> let newmeta, newtarget = build_newtarget false t in - if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) || - (Inference.meta_convertibility_eq target newtarget) then + if (Equality.is_weak_identity newtarget) || + (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else demodulation_equality newmeta env table sign newtarget @@ -903,6 +907,9 @@ let sup_l_counter = ref 1;; returns a list of new clauses inferred with a left superposition step the negative equation "target" and one of the positive equations in "table" *) +let superposition_left newmeta (metasenv, context, ugraph) table target = + assert false +(* let superposition_left newmeta (metasenv, context, ugraph) table target = let module C = Cic in let module S = CicSubstitution in @@ -910,25 +917,23 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in - let weight, proof, (eq_ty, left, right, ordering), menv = target in + let weight, proof, (eq_ty, left, right, ordering), menv, id = + Equality.open_equality target + in if Utils.debug_metas then ignore(check_target context target "superpositionleft"); let expansions, _ = let term = if ordering = U.Gt then left else right in - begin - let t1 = Unix.gettimeofday () in - let res = betaexpand_term metasenv context ugraph table 0 term in - let t2 = Unix.gettimeofday () in - beta_expand_time := !beta_expand_time +. (t2 -. t1); - res - end + betaexpand_term metasenv context ugraph table 0 term in let maxmeta = ref newmeta in let build_new (bo, s, m, ug, (eq_found, eq_URI)) = (* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *) let time1 = Unix.gettimeofday () in - let pos, (_, proof', (ty, what, other, _), menv') = eq_found in + let pos, equality = eq_found in + let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in + let proof'_new, proof'_old = proof' in let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in @@ -952,26 +957,30 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = if pos = Utils.Left then [ty; what; other] else [ty; other; what] in - Inference.ProofSymBlock (termlist, proof') + proof'_new, (* MAH????? *) + Equality.ProofSymBlock (termlist, proof'_old) in let what, other = if pos = Utils.Left then what, other else other, what in - pos, (0, proof', (ty, other, what, Utils.Incomparable), menv') + pos, + Equality.mk_equality + (0, proof', (ty, other, what, Utils.Incomparable), menv') in - let target_proof = + let target_proof = assert false (* let pb = - Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, - Inference.BasicProof ([],metaproof)) + Equality.ProofBlock + (s, eq_URI, (name, ty), bo'', eq_found, + Equality.BasicProof (Equality.empty_subst,metaproof)) in match proof with - | Inference.BasicProof _ -> + | Equality.BasicProof _ -> (* debug_print (lazy "replacing a BasicProof"); *) pb - | Inference.ProofGoalBlock (_, parent_proof) -> + | Equality.ProofGoalBlock (_, parent_proof) -> (* debug_print (lazy "replacing another ProofGoalBlock"); *) - Inference.ProofGoalBlock (pb, parent_proof) - | _ -> assert false + Equality.ProofGoalBlock (pb, parent_proof) + | _ -> assert false*) in let refl = C.Appl [C.MutConstruct (* reflexivity *) @@ -979,7 +988,10 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = eq_ty; if ordering = U.Gt then right else left] in (bo', - Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof)) + (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'), + assert false), (* il predicato della beta expand non viene tenuto? *) + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,refl), target_proof))) in let left, right = if ordering = U.Gt then newgoal, right else left, newgoal in @@ -990,12 +1002,12 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = build_newtarget_time := !build_newtarget_time +. (time2 -. time1); let w = Utils.compute_equality_weight stat in - (w, newproof, stat, newmenv) + Equality.mk_equality (w, newproof, stat, newmenv) in !maxmeta, List.map build_new expansions ;; - +*) let sup_r_counter = ref 1;; @@ -1013,7 +1025,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let module HL = HelmLibraryObjects in let module CR = CicReduction in let module U = Utils in - let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in + let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id = + Equality.open_equality target + in if Utils.debug_metas then ignore (check_target context target "superpositionright"); let metasenv' = newmetas in @@ -1045,12 +1059,15 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = ignore (check_target context (snd eq_found) "buildnew1" ); let time1 = Unix.gettimeofday () in - let pos, (_, proof', (ty, what, other, _), menv') = eq_found in + 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 newgoal, newproof = (* qua *) let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in - let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in +(* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*) + let name = C.Name "x" in incr sup_r_counter; let bo'' = let l, r = @@ -1059,7 +1076,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = S.lift 1 eq_ty; l; r] in bo', - Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof) + ( Equality.Step (s,(Equality.SuperpositionRight, + id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))), + Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2)) + in let newmeta, newequality = let left, right = @@ -1070,10 +1090,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let stat = (eq_ty, left, right, neworder) in let eq' = let w = Utils.compute_equality_weight stat in - (w, newproof, stat, newmenv) in + Equality.mk_equality (w, newproof, stat, newmenv) in if Utils.debug_metas then ignore (check_target context eq' "buildnew3"); - let newm, eq' = Inference.fix_metas !maxmeta eq' in + let newm, eq' = Equality.fix_metas !maxmeta eq' in if Utils.debug_metas then ignore (check_target context eq' "buildnew4"); newm, eq' @@ -1087,7 +1107,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = in let new1 = List.map (build_new U.Gt) res1 and new2 = List.map (build_new U.Lt) res2 in - let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in + let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in (!maxmeta, (List.filter ok (new1 @ new2))) ;; @@ -1101,68 +1121,78 @@ let rec demodulation_goal newmeta env table goal = let module HL = HelmLibraryObjects in let metasenv, context, ugraph = env in let maxmeta = ref newmeta in - let proof, metas, term = goal in + let (cicproof,proof), metas, term = goal in let term = Utils.guarded_simpl (~debug:true) context term in - let goal = proof, metas, term in + let goal = (cicproof,proof), metas, term in let metasenv' = metas in let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = - let pos, (_, proof', (ty, what, other, _), menv') = eq_found in + let pos, equality = eq_found in + let (_, (proofnew',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 ty = try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) with CicUtil.Meta_not_found _ -> ty in - let newterm, newproof = - let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in + let newterm, newproof, newcicproof = + 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_DemodGoal_" ^ (string_of_int !demod_counter)) in +(* let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*) + let name = C.Name "x" in incr demod_counter; let metaproof = incr maxmeta; - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in + let irl = [] (* + CicMkImplicit.identity_relocation_list_for_metavariable context *) in (* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) C.Meta (!maxmeta, irl) in let eq_found = - let proof' = + let eq_found_proof = let termlist = if pos = Utils.Left then [ty; what; other] else [ty; other; what] in - Inference.ProofSymBlock (termlist, proof') + Equality.ProofSymBlock (termlist, proof') in let what, other = if pos = Utils.Left then what, other else other, what in - pos, (0, proof', (ty, other, what, Utils.Incomparable), menv') + pos, + Equality.mk_equality + (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv') in let goal_proof = let pb = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo', - eq_found, Inference.BasicProof ([],metaproof)) + Equality.ProofBlock + (subst, eq_URI, (name, ty), bo', + eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) in let rec repl = function - | Inference.NoProof -> + | Equality.NoProof -> (* debug_print (lazy "replacing a NoProof"); *) pb - | Inference.BasicProof _ -> + | Equality.BasicProof _ -> (* debug_print (lazy "replacing a BasicProof"); *) pb - | Inference.ProofGoalBlock (_, parent_proof) -> + | Equality.ProofGoalBlock (_, parent_proof) -> (* debug_print (lazy "replacing another ProofGoalBlock"); *) - Inference.ProofGoalBlock (pb, parent_proof) - | Inference.SubProof (term, meta_index, p) -> + Equality.ProofGoalBlock (pb, parent_proof) + | Equality.SubProof (term, meta_index, p) -> prerr_endline "subproof!"; - Inference.SubProof (term, meta_index, repl p) + Equality.SubProof (term, meta_index, repl p) | _ -> assert false in repl proof in - bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof) + let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in + bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof), + (newcicproofstep::cicproof) in let newmetasenv = (* Inference.filter subst *) menv in - !maxmeta, (newproof, newmetasenv, newterm) + !maxmeta, ((newcicproof,newproof), newmetasenv, newterm) in let res = demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term @@ -1171,12 +1201,12 @@ let rec demodulation_goal newmeta env table goal = | Some t -> let newmeta, newgoal = build_newgoal t in let _, _, newg = newgoal in - if Inference.meta_convertibility term newg then - newmeta, newgoal + if Equality.meta_convertibility term newg then + true, newmeta, newgoal else demodulation_goal newmeta env table newgoal | None -> - newmeta, goal + false, newmeta, goal ;; (** demodulation, when the target is a theorem *) @@ -1191,18 +1221,20 @@ let rec demodulation_theorem newmeta env table theorem = let metasenv' = metas in let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) = - let pos, (_, proof', (ty, what, other, _), menv') = eq_found in + 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 incr demod_counter; - let newproof = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, - Inference.BasicProof ([],term)) + let newproofold = + Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, + Equality.BasicProof (Equality.empty_subst,term)) in - (Inference.build_proof_term newproof, bo) + (Equality.build_proof_term_old newproofold, bo) in !maxmeta, (newterm, newty, menv) in @@ -1213,7 +1245,7 @@ let rec demodulation_theorem newmeta env table theorem = | Some t -> let newmeta, newthm = build_newtheorem t in let newt, newty, _ = newthm in - if Inference.meta_convertibility termty newty then + if Equality.meta_convertibility termty newty then newmeta, newthm else demodulation_theorem newmeta env table newthm diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli index 5af20df5c..1c6102a07 100644 --- a/components/tactics/paramodulation/indexing.mli +++ b/components/tactics/paramodulation/indexing.mli @@ -25,20 +25,18 @@ (* $Id$ *) -val beta_expand_time : float ref - module Index : sig module PosEqSet : Set.S - with type elt = Utils.pos * Inference.equality + with type elt = Utils.pos * Equality.equality and type t = Equality_indexing.DT.PosEqSet.t type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t type key = Cic.term end -val index : Index.t -> Inference.equality -> Index.t -val remove_index : Index.t -> Inference.equality -> Index.t -val in_index : Index.t -> Inference.equality -> bool +val index : Index.t -> Equality.equality -> Index.t +val remove_index : Index.t -> Equality.equality -> Index.t +val in_index : Index.t -> Equality.equality -> bool val empty : Index.t val match_unif_time_ok : float ref val match_unif_time_no : float ref @@ -48,34 +46,35 @@ val build_newtarget_time : float ref val subsumption : Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> - Inference.equality -> - (Inference.substitution * Inference.equality) option + Equality.equality -> + (Equality.substitution * Equality.equality) option val superposition_left : int -> Cic.conjecture list * Cic.context * CicUniv.universe_graph -> Index.t -> - Inference.equality -> - int * Inference.equality list + Equality.equality -> + int * Equality.equality list val superposition_right : int -> 'a * Cic.context * CicUniv.universe_graph -> Index.t -> - Inference.equality -> - int * Inference.equality list + Equality.equality -> + int * Equality.equality list val demodulation_equality : ?from:string -> int -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> - Utils.equality_sign -> Inference.equality -> int * Inference.equality + Utils.equality_sign -> Equality.equality -> int * Equality.equality val demodulation_goal : int -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> - Inference.proof * Cic.metasenv * Index.key -> - int * (Inference.proof * Cic.metasenv * Index.key) + (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key -> + bool * int * + ((Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key) val demodulation_theorem : 'a -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> @@ -84,7 +83,5 @@ val demodulation_theorem : 'a * (Cic.term * Index.key * Cic.metasenv) val check_target: Cic.context -> - Inference.equality -> string -> unit + Equality.equality -> string -> unit -(* maxmeta for relocate *) -val local_max : int ref diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index a3894fd84..f088d5454 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -28,192 +28,9 @@ open Utils;; open Printf;; -let metas_of_proof_time = ref 0.;; -let metas_of_term_time = ref 0.;; -(* -type substitution = Cic.substitution -let apply_subst = CicMetaSubst.apply_subst -let apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv -let ppsubst = CicMetaSubst.ppsubst -let buildsubst n context t ty = (n,(context,t,ty)) -let flatten_subst subst = - List.map - (fun (i, (context, term, ty)) -> - let context = (*` apply_subst_context subst*) context in - let term = apply_subst subst term in - let ty = apply_subst subst ty in - (i, (context, term, ty))) subst -let rec lookup_subst meta subst = - match meta with - | Cic.Meta (i, _) -> ( - try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst - in lookup_subst t subst - with Not_found -> meta - ) - | _ -> meta -;; -*) - -(* naif version of apply subst; the local context of metas is ignored; -we assume the substituted term must be lifted according to the nesting -depth of the meta. Alternatively, ee could used implicit instead of -metas *) - - -type substitution = (int * Cic.term) list - -let apply_subst subst term = - let rec aux k t = - match t with - Cic.Rel _ -> t - | Cic.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - Cic.Var (uri, exp_named_subst') - | Cic.Meta (i, l) -> - (try - aux k (CicSubstitution.lift k (List.assoc i subst)) - with Not_found -> t) - | Cic.Sort _ - | Cic.Implicit _ -> t - | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty) - | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t) - | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t) - | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t) - | Cic.Appl [] -> assert false - | Cic.Appl l -> Cic.Appl (List.map (aux k) l) - | Cic.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - if exp_named_subst' != exp_named_subst then - Cic.Const (uri, exp_named_subst') - else - t (* TODO: provare a mantenere il piu' possibile sharing *) - | Cic.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - Cic.MutInd (uri,typeno,exp_named_subst') - | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst - in - Cic.MutConstruct (uri,typeno,consno,exp_named_subst') - | Cic.MutCase (sp,i,outty,t,pl) -> - let pl' = List.map (aux k) pl in - Cic.MutCase (sp, i, aux k outty, aux k t, pl') - | Cic.Fix (i, fl) -> - let len = List.length fl in - let fl' = - List.map - (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl - in - Cic.Fix (i, fl') - | Cic.CoFix (i, fl) -> - let len = List.length fl in - let fl' = - List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl - in - Cic.CoFix (i, fl') -in - aux 0 term -;; - -(* naif version of apply_subst_metasenv: we do not apply the -substitution to the context *) - -let apply_subst_metasenv subst metasenv = - List.map - (fun (n, context, ty) -> - (n, context, apply_subst subst ty)) - (List.filter - (fun (i, _, _) -> not (List.mem_assoc i subst)) - metasenv) - -let ppsubst subst = - String.concat "\n" - (List.map - (fun (idx, t) -> - sprintf "%d:= %s" idx (CicPp.ppterm t)) - subst) -;; - -let buildsubst n context t ty = (n,t) ;; - -let flatten_subst subst = - List.map (fun (i,t) -> i, apply_subst subst t ) subst -;; - -let rec lookup_subst meta subst = - match meta with - | Cic.Meta (i, _) -> - (try - lookup_subst (List.assoc i subst) subst - with - Not_found -> meta) - | _ -> meta -;; - -type equality = - int * (* weight *) - proof * - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term * (* right side *) - Utils.comparison) * (* ordering *) - Cic.metasenv (* environment for metas *) - -and proof = - | NoProof (* term is the goal missing a proof *) - | BasicProof of substitution * Cic.term - | ProofBlock of - substitution * UriManager.uri * - (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof - | ProofGoalBlock of proof * proof - | ProofSymBlock of Cic.term list * proof - | SubProof of Cic.term * int * proof -;; - -let string_of_equality ?env = - match env with - | None -> ( - function - | w, _, (ty, left, right, o), _ -> - Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty) - (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right) - ) - | Some (_, context, _) -> ( - let names = names_of_context context in - function - | w, _, (ty, left, right, o), _ -> - Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names) - (CicPp.pp left names) (string_of_comparison o) - (CicPp.pp right names) - ) -;; - - -let rec string_of_proof = function - | NoProof -> "NoProof " - | BasicProof (s, t) -> "BasicProof " ^ - (CicPp.ppterm (apply_subst s t)) - | SubProof (t, i, p) -> - Printf.sprintf "SubProof(%s, %s, %s)" - (CicPp.ppterm t) (string_of_int i) (string_of_proof p) - | ProofSymBlock _ -> "ProofSymBlock" - | ProofBlock (subst, _, _, _ ,_,_) -> - "ProofBlock" ^ (ppsubst subst) - | ProofGoalBlock (p1, p2) -> - Printf.sprintf "ProofGoalBlock(%s, %s)" - (string_of_proof p1) (string_of_proof p2) -;; - - let check_disjoint_invariant subst metasenv msg = if (List.exists - (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv) + (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv) then begin prerr_endline ("not disjoint: " ^ msg); @@ -221,257 +38,6 @@ let check_disjoint_invariant subst metasenv msg = end ;; -(* filter out from metasenv the variables in substs *) -let filter subst metasenv = - List.filter - (fun (m, _, _) -> - try let _ = List.find (fun (i, _) -> m = i) subst in false - with Not_found -> true) - metasenv -;; - -(* 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 - 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 -;; - - -let build_proof_term ?(noproof=Cic.Implicit None) proof = - let rec do_build_proof proof = - match proof with - | NoProof -> - Printf.fprintf stderr "WARNING: no proof!\n"; - noproof - | BasicProof (s,term) -> apply_subst s term - | ProofGoalBlock (proofbit, proof) -> - print_endline "found ProofGoalBlock, going up..."; - 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 - 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 - let proof' = - let _, proof', _, _ = eq in - do_build_proof proof' - in - let eqproof = do_build_proof eqproof in - let _, _, (ty, what, other, _), menv' = eq in - let what, other = - if pos = Utils.Left then what, other else other, what - in - apply_subst subst - (Cic.Appl [Cic.Const (eq_URI, []); ty; - what; t'; eqproof; other; proof']) - | SubProof (term, meta_index, proof) -> - let proof = do_build_proof proof in - let eq i = function - | Cic.Meta (j, _) -> i = j - | _ -> false - in - ProofEngineReduction.replace - ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term - - and do_build_goal_proof proofbit proof = - match proof with - | ProofGoalBlock (pb, p) -> - do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p)) - | _ -> do_build_proof (replace_proof proofbit proof) - - and replace_proof newproof = function - | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) -> - let eqproof' = replace_proof newproof eqproof in - ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof') - | ProofGoalBlock (pb, p) -> - let pb' = replace_proof newproof pb in - ProofGoalBlock (pb', p) - | BasicProof _ -> newproof - | SubProof (term, meta_index, p) -> - SubProof (term, meta_index, replace_proof newproof p) - | p -> p - in - do_build_proof proof -;; - -let rec metas_of_term = function - | Cic.Meta (i, c) -> [i] - | Cic.Var (_, ens) - | Cic.Const (_, ens) - | Cic.MutInd (_, _, ens) - | Cic.MutConstruct (_, _, _, ens) -> - List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) - | Cic.Cast (s, t) - | Cic.Prod (_, s, t) - | Cic.Lambda (_, s, t) - | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) - | Cic.Appl l -> List.flatten (List.map metas_of_term l) - | Cic.MutCase (uri, i, s, t, l) -> - (metas_of_term s) @ (metas_of_term t) @ - (List.flatten (List.map metas_of_term l)) - | Cic.Fix (i, il) -> - List.flatten - (List.map (fun (s, i, t1, t2) -> - (metas_of_term t1) @ (metas_of_term t2)) il) - | Cic.CoFix (i, il) -> - List.flatten - (List.map (fun (s, t1, t2) -> - (metas_of_term t1) @ (metas_of_term t2)) il) - | _ -> [] -;; - -let rec metas_of_proof p = - if Utils.debug then - let t1 = Unix.gettimeofday () in - let res = metas_of_term (build_proof_term p) in - let t2 = Unix.gettimeofday () in - metas_of_proof_time := !metas_of_proof_time +. (t2 -. t1); - res - else - metas_of_term (build_proof_term p) -;; - - -exception NotMetaConvertible;; - -let meta_convertibility_aux table t1 t2 = - let module C = Cic in - let rec aux ((table_l, table_r) as table) t1 t2 = - match t1, t2 with - | C.Meta (m1, tl1), C.Meta (m2, tl2) -> - let m1_binding, table_l = - try List.assoc m1 table_l, table_l - with Not_found -> m2, (m1, m2)::table_l - and m2_binding, table_r = - try List.assoc m2 table_r, table_r - with Not_found -> m1, (m2, m1)::table_r - in - if (m1_binding <> m2) || (m2_binding <> m1) then - raise NotMetaConvertible - else ( - try - List.fold_left2 - (fun res t1 t2 -> - match t1, t2 with - | None, Some _ | Some _, None -> raise NotMetaConvertible - | None, None -> res - | Some t1, Some t2 -> (aux res t1 t2)) - (table_l, table_r) tl1 tl2 - with Invalid_argument _ -> - raise NotMetaConvertible - ) - | C.Var (u1, ens1), C.Var (u2, ens2) - | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) -> - aux_ens table ens1 ens2 - | C.Cast (s1, t1), C.Cast (s2, t2) - | C.Prod (_, s1, t1), C.Prod (_, s2, t2) - | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2) - | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) -> - let table = aux table s1 s2 in - aux table t1 t2 - | C.Appl l1, C.Appl l2 -> ( - try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2) - when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2 - | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2) - when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 -> - aux_ens table ens1 ens2 - | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2) - when (UriManager.eq u1 u2) && i1 = i2 -> - let table = aux table s1 s2 in - let table = aux table t1 t2 in ( - try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> ( - try - List.fold_left2 - (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) -> - if i1 <> i2 then raise NotMetaConvertible - else - let res = (aux res s1 s2) in aux res t1 t2) - table il1 il2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> ( - try - List.fold_left2 - (fun res (n1, s1, t1) (n2, s2, t2) -> - let res = aux res s1 s2 in aux res t1 t2) - table il1 il2 - with Invalid_argument _ -> raise NotMetaConvertible - ) - | t1, t2 when t1 = t2 -> table - | _, _ -> raise NotMetaConvertible - - and aux_ens table ens1 ens2 = - let cmp (u1, t1) (u2, t2) = - compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) - in - let ens1 = List.sort cmp ens1 - and ens2 = List.sort cmp ens2 in - try - List.fold_left2 - (fun res (u1, t1) (u2, t2) -> - if not (UriManager.eq u1 u2) then raise NotMetaConvertible - else aux res t1 t2) - table ens1 ens2 - with Invalid_argument _ -> raise NotMetaConvertible - in - aux table t1 t2 -;; - - -let meta_convertibility_eq eq1 eq2 = - let _, _, (ty, left, right, _), _ = eq1 - and _, _, (ty', left', right', _), _ = eq2 in - if ty <> ty' then - false - else if (left = left') && (right = right') then - true - else if (left = right') && (right = left') then - true - else - try - let table = meta_convertibility_aux ([], []) left left' in - let _ = meta_convertibility_aux table right right' in - true - with NotMetaConvertible -> - try - let table = meta_convertibility_aux ([], []) left right' in - let _ = meta_convertibility_aux table right left' in - true - with NotMetaConvertible -> - false -;; - - -let meta_convertibility t1 t2 = - if t1 = t2 then - true - else - try - ignore(meta_convertibility_aux ([], []) t1 t2); - true - with NotMetaConvertible -> - false -;; - - let rec check_irl start = function | [] -> true | None::tl -> check_irl (start+1) tl @@ -480,7 +46,6 @@ let rec check_irl start = function | _ -> false ;; - let rec is_simple_term = function | Cic.Appl ((Cic.Meta _)::_) -> false | Cic.Appl l -> List.for_all is_simple_term l @@ -497,11 +62,10 @@ let locked menv i = ;; let unification_simple locked_menv metasenv context t1 t2 ugraph = - let debug_print x = prerr_endline (Lazy.force x) in let module C = Cic in let module M = CicMetaSubst in let module U = CicUnification in - let lookup = lookup_subst in + let lookup = Equality.lookup_subst in let rec occurs_check subst what where = match where with | t when what = t -> true @@ -519,24 +83,24 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = match s, t with | s, t when s = t -> subst, menv | C.Meta (i, _), C.Meta (j, _) - when (locked locked_menv i) &&(locked locked_menv j) -> - raise + when (locked locked_menv i) &&(locked locked_menv j) -> + raise (U.UnificationFailure (lazy "Inference.unification.unif")) - | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) -> - unif subst menv t s + | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) -> + unif subst menv t s | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) -> unif subst menv t s | C.Meta _, t when occurs_check subst s t -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t when (locked locked_menv i) -> - raise + raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in - assert (not (List.mem_assoc i subst)); - let subst = (buildsubst i context t ty)::subst in + assert (not (Equality.is_in_subst i subst)); + let subst = Equality.buildsubst i context t ty subst in let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *) subst, menv with CicUtil.Meta_not_found m -> @@ -562,9 +126,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = | _, _ -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) in - let subst, menv = unif [] metasenv t1 t2 in - let menv = filter subst menv in - List.rev subst, menv, ugraph + let subst, menv = unif Equality.empty_subst metasenv t1 t2 in + let menv = Equality.filter subst menv in + subst, menv, ugraph ;; let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]" @@ -583,21 +147,21 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph = raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif")) ) else if b then - (* full unification *) - unification_simple [] metasenv context t1 t2 ugraph + (* full unification *) + unification_simple [] metasenv context t1 t2 ugraph else - (* matching: metasenv1 is locked *) - unification_simple metasenv1 metasenv context t1 t2 ugraph + (* matching: metasenv1 is locked *) + unification_simple metasenv1 metasenv context t1 t2 ugraph in if Utils.debug_res then - ignore(check_disjoint_invariant subst menv "unif"); + ignore(check_disjoint_invariant subst menv "unif"); (* let flatten subst = List.map (fun (i, (context, term, ty)) -> - let context = apply_subst_context subst context in - let term = apply_subst subst term in - let ty = apply_subst subst ty in - (i, (context, term, ty))) subst + let context = apply_subst_context subst context in + let term = apply_subst subst term in + let ty = apply_subst subst ty in + (i, (context, term, ty))) subst in let flatten subst = profiler.HExtlib.profile flatten subst in let subst = flatten subst in *) @@ -670,8 +234,11 @@ let find_equalities context proof = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let proof = BasicProof ([],p) in - let e = (w, proof, stat, newmetas) in + let proof_old = + Equality.BasicProof (Equality.empty_subst,p) in + let proof_new = Equality.Exact p in + let proof = proof_new , proof_old in + let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -683,15 +250,19 @@ let find_equalities context proof = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let e = (w, BasicProof ([],(C.Rel index)), stat, []) in + let p = C.Rel index in + let proof_old = Equality.BasicProof (Equality.empty_subst,p) in + let proof_new = Equality.Exact p in + let proof = proof_new, proof_old in + let e = Equality.mk_equality (w, proof,stat,[]) in Some e, (newmeta+1) | _ -> None, newmeta in ( match do_find context term with | Some p, newmeta -> let tl, newmeta' = (aux (index+1) newmeta tl) in - if newmeta' < newmeta then - prerr_endline "big trouble"; + if newmeta' < newmeta then + prerr_endline "big trouble"; (index, p)::tl, newmeta' (* max???? *) | None, _ -> aux (index+1) newmeta tl @@ -701,7 +272,7 @@ let find_equalities context proof = in let il, maxm = aux 1 newmeta context in let indexes, equalities = List.split il in - ignore (List.iter (check_eq context "find") equalities); + (* ignore (List.iter (check_eq context "find") equalities); *) indexes, equalities, maxm ;; @@ -811,17 +382,20 @@ let find_library_equalities dbd context status maxmeta = else C.Appl (term::args) in ( - match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when (iseq uri) && (ok_types ty newmetas) -> + match head with + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when (iseq uri) && (ok_types ty newmetas) -> debug_print (lazy (Printf.sprintf "OK: %s" (CicPp.ppterm term))); let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let proof = BasicProof ([],p) in - let e = (w, proof, stat, newmetas) in + let proof_old = + Equality.BasicProof (Equality.empty_subst,p) in + let proof_new = Equality.Exact p in + let proof = proof_new, proof_old in + let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta ) @@ -830,28 +404,32 @@ let find_library_equalities dbd context status maxmeta = let o = !Utils.compare_terms t1 t2 in let stat = (ty,t1,t2,o) in let w = compute_equality_weight stat in - let e = (w, BasicProof ([],term), stat, []) in + let old_proof = Equality.BasicProof (Equality.empty_subst,term) in + let new_proof = Equality.Exact term in + let proof = new_proof, old_proof in + let e = Equality.mk_equality (w, proof, stat, []) in Some e, (newmeta+1) | _ -> None, newmeta in match res with | Some e -> let tl, newmeta' = aux newmeta tl in - if newmeta' < newmeta then - prerr_endline "big trouble"; + if newmeta' < newmeta then + prerr_endline "big trouble"; (uri, e)::tl, newmeta' (* max???? *) | None -> aux newmeta tl in let found, maxm = aux maxmeta candidates in let uriset, eqlist = + let mceq = Equality.meta_convertibility_eq in (List.fold_left (fun (s, l) (u, e) -> - if List.exists (meta_convertibility_eq e) (List.map snd l) then ( + if List.exists (mceq e) (List.map snd l) then ( debug_print (lazy (Printf.sprintf "NO!! %s already there!" - (string_of_equality e))); + (Equality.string_of_equality e))); (UriManager.UriSet.add u s, l) ) else (UriManager.UriSet.add u s, (u, e)::l)) (UriManager.UriSet.empty, []) found) @@ -917,230 +495,3 @@ let find_context_hypotheses env equalities_indexes = res ;; -(* -let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) = - let table = Hashtbl.create (List.length args) in - - let newargs, newmeta = - List.fold_right - (fun t (newargs, index) -> - match t with - | Cic.Meta (i, l) -> - if Hashtbl.mem table i then - let idx = Hashtbl.find table i in - ((Cic.Meta (idx, l))::newargs, index+1) - else - let _ = Hashtbl.add table i index in - ((Cic.Meta (index, l))::newargs, index+1) - | _ -> assert false) - args ([], newmeta+1) - in - - let repl where = - ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs - ~where - in - let menv' = - List.fold_right - (fun (i, context, term) menv -> - try - let index = Hashtbl.find table i in - (index, context, term)::menv - with Not_found -> - (i, context, term)::menv) - menv [] - in - let ty = repl ty - and left = repl left - and right = repl right in - let metas = - (metas_of_term left) @ - (metas_of_term right) @ - (metas_of_term ty) @ (metas_of_proof p) in - let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in - let newargs = - List.filter - (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs - in - let _ = - if List.length metas > 0 then - let first = List.hd metas in - (* this new equality might have less variables than its parents: here - we fill the gap with a dummy arg. Example: - with (f X Y) = X we can simplify - (g X) = (f X Y) in - (g X) = X. - So the new equation has only one variable, but it still has type like - \lambda X,Y:..., so we need to pass a dummy arg for Y - (I hope this makes some sense...) - *) - Hashtbl.iter - (fun k v -> - if not (List.exists - (function Cic.Meta (i, _) -> i = v | _ -> assert false) - newargs) then - Hashtbl.replace table k first) - (Hashtbl.copy table) - in - let rec fix_proof = function - | NoProof -> NoProof - | BasicProof term -> BasicProof (repl term) - | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) -> - let subst' = - List.fold_left - (fun s arg -> - match arg with - | Cic.Meta (i, l) -> ( - try - let j = Hashtbl.find table i in - if List.mem_assoc i subst then - s - else - let _, context, ty = CicUtil.lookup_meta i menv in - (i, (context, Cic.Meta (j, l), ty))::s - with Not_found | CicUtil.Meta_not_found _ -> - s - ) - | _ -> assert false) - [] args - in - ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p) - | p -> assert false - in - let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in - (newmeta +1, neweq) -;; -*) - -let relocate newmeta menv = - let subst, metasenv, newmeta = - List.fold_right - (fun (i, context, ty) (subst, menv, maxmeta) -> - let irl = [] (* - CicMkImplicit.identity_relocation_list_for_metavariable context *) - in - let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty in - let newmeta = maxmeta, context, ty in - newsubst::subst, newmeta::menv, maxmeta+1) - menv ([], [], newmeta+1) - in - let metasenv = apply_subst_metasenv subst metasenv in - let subst = flatten_subst subst in - subst, metasenv, newmeta - - -let fix_metas newmeta (w, p, (ty, left, right, o), menv) = - (* - let metas = (metas_of_term left)@(metas_of_term right) - @(metas_of_term ty)@(metas_of_proof p) in - let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in - *) - (* debug - let _ , eq = - fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in - prerr_endline (string_of_equality eq); *) - let subst, metasenv, newmeta = relocate newmeta menv in -(* - if newmeta > 2839 then - begin - prerr_endline (CicPp.ppterm left ^ " = " ^ CicPp.ppterm right); - prerr_endline (CicMetaSubst.ppsubst subst); - prerr_endline (CicMetaSubst.ppmetasenv [] metasenv); - assert false; - end; -*) - let ty = apply_subst subst ty in - let left = apply_subst subst left in - let right = apply_subst subst right in - let fix_proof = function - | NoProof -> NoProof - | BasicProof (subst',term) -> BasicProof (subst@subst',term) - | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) -> - (* - let newsubst = - List.map - (fun (i, (context, term, ty)) -> - let context = apply_subst_context subst context in - let term = apply_subst subst term in - let ty = apply_subst subst ty in - (i, (context, term, ty))) subst' in *) - ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p) - | p -> assert false - in - let p = fix_proof p in - (* - let metas = (metas_of_term left)@(metas_of_term right) - @(metas_of_term ty)@(metas_of_proof p) in - let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in - *) - let eq = (w, p, (ty, left, right, o), metasenv) in - (* debug prerr_endline (string_of_equality eq); *) - newmeta+1, eq - -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 -;; - - -exception TermIsNotAnEquality;; - -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 -> - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - let w = compute_equality_weight stat in - let e = (w, BasicProof ([],proof), stat, []) in - e - | _ -> - raise TermIsNotAnEquality -;; - - -type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; - -let is_weak_identity (metasenv, context, ugraph) = function - | (_, _, (ty, left, right, _), menv) -> - (left = right || - (meta_convertibility left right)) - (* the test below is not a good idea since it stops - demodulation too early *) - (* (fst (CicReduction.are_convertible - ~metasenv:(metasenv @ menv) context left right ugraph)))*) -;; - -let is_identity (metasenv, context, ugraph) = function - | (_, _, (ty, left, right, _), menv) -> - (left = right || - (* (meta_convertibility left right)) *) - (fst (CicReduction.are_convertible - ~metasenv:(metasenv @ menv) context left right ugraph))) -;; - - -let term_of_equality equality = - let _, _, (ty, left, right, _), menv = equality in - let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in - let argsno = List.length menv in - let t = - CicSubstitution.lift argsno - (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right]) - in - snd ( - List.fold_right - (fun (i,_,ty) (n, t) -> - let name = Cic.Name ("X" ^ (string_of_int n)) in - let ty = CicSubstitution.lift (n-1) ty in - let t = - ProofEngineReduction.replace - ~equality:eq ~what:[i] - ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t - in - (n-1, Cic.Prod (name, ty, t))) - menv (argsno, t)) -;; diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli index b08054ca4..08d1c8f26 100644 --- a/components/tactics/paramodulation/inference.mli +++ b/components/tactics/paramodulation/inference.mli @@ -23,57 +23,24 @@ * http://cs.unibo.it/helm/. *) -val metas_of_proof_time : float ref - -(* type substitution = Cic.substitution *) -type substitution = (int * Cic.term) list - -type equality = - int * (* weight *) - proof * (* proof *) - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term * (* right side *) - Utils.comparison) * (* ordering *) - Cic.metasenv (* environment for metas *) - -and proof = - | NoProof (* no proof *) - | BasicProof of substitution * Cic.term (* already a proof of a goal *) - | ProofBlock of (* proof of a rewrite step *) - substitution * UriManager.uri * (* eq_ind or eq_ind_r *) - (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof - | ProofGoalBlock of proof * proof - (* proof of the new meta, proof of the goal from which this comes *) - | ProofSymBlock of Cic.term list * proof (* expl.named subst, proof *) - | SubProof of Cic.term * int * proof - (* parent proof, subgoal, proof of the subgoal *) - -type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph - -(** builds the Cic.term encoded by proof *) -val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term - -val string_of_proof: proof -> string - -val filter : substitution -> Cic.metasenv -> Cic.metasenv - exception MatchingFailure (** matching between two terms. Can raise MatchingFailure *) val matching: - Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> + Cic.metasenv -> Cic.metasenv -> Cic.context -> + Cic.term -> Cic.term -> CicUniv.universe_graph -> - substitution * Cic.metasenv * CicUniv.universe_graph + Equality.substitution * Cic.metasenv * CicUniv.universe_graph (** special unification that checks if the two terms are "simple", and in such case should be significantly faster than CicUnification.fo_unif *) val unification: - Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> + Cic.metasenv -> Cic.metasenv -> Cic.context -> + Cic.term -> Cic.term -> CicUniv.universe_graph -> - substitution * Cic.metasenv * CicUniv.universe_graph + Equality.substitution * Cic.metasenv * CicUniv.universe_graph (** @@ -83,64 +50,28 @@ val unification: fresh metas... *) val find_equalities: - Cic.context -> ProofEngineTypes.proof -> int list * equality list * int + Cic.context -> ProofEngineTypes.proof -> + int list * Equality.equality list * int (** searches the library for equalities that can be applied to the current goal *) val find_library_equalities: HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> - UriManager.UriSet.t * (UriManager.uri * equality) list * int + UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int (** searches the library for theorems that are not equalities (returned by the function above) *) val find_library_theorems: - HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t -> - (Cic.term * Cic.term * Cic.metasenv) list + HMysql.dbd -> Utils.environment -> ProofEngineTypes.status -> + UriManager.UriSet.t -> + (Cic.term * Cic.term * Cic.metasenv) list (** searches the context for hypotheses that are not equalities *) val find_context_hypotheses: - environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list - - -exception TermIsNotAnEquality;; - -(** - raises TermIsNotAnEquality if term is not an equation. - The first Cic.term is a proof of the equation -*) -val equality_of_term: Cic.term -> Cic.term -> equality - -(** - Re-builds the term corresponding to this equality -*) -val term_of_equality: equality -> Cic.term - -val term_is_equality: Cic.term -> bool - -(** tests a sort of alpha-convertibility between the two terms, but on the - metavariables *) -val meta_convertibility: Cic.term -> Cic.term -> bool - -(** meta convertibility between two equations *) -val meta_convertibility_eq: equality -> equality -> bool - -val is_weak_identity: environment -> equality -> bool -val is_identity: environment -> equality -> bool - -val string_of_equality: ?env:environment -> equality -> string - - -val metas_of_term: Cic.term -> int list -val metas_of_proof: proof -> int list - -(** ensures that metavariables in equality are unique *) -val fix_metas: int -> equality -> int * equality + Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list -val apply_subst: substitution -> Cic.term -> Cic.term -val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv -val ppsubst: substitution -> string diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 5b5121e86..59b06ef29 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -70,16 +70,20 @@ let maxmeta = ref 0;; let maxdepth = ref 3;; let maxwidth = ref 3;; +type new_proof = + Equality.goal_proof * Equality.new_proof * Equality.substitution * Cic.metasenv +type old_proof = Equality.old_proof * Cic.metasenv type result = | ParamodulationFailure - | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option + | ParamodulationSuccess of (new_proof * old_proof) option ;; -type goal = proof * Cic.metasenv * Cic.term;; +type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; -let symbols_of_equality (_, _, (_, left, right, _), _) = +let symbols_of_equality equality = + let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in let m1 = symbols_of_term left in let m = TermMap.fold @@ -96,14 +100,14 @@ let symbols_of_equality (_, _, (_, left, right, _), _) = (* griggio *) module OrderedEquality = struct - type t = Inference.equality + type t = Equality.equality let compare eq1 eq2 = - match meta_convertibility_eq eq1 eq2 with + match Equality.meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> - let w1, _, (ty, left, right, _), m1 = eq1 - and w2, _, (ty', left', right', _), m2 = eq2 in + let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in + let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in match Pervasives.compare w1 w2 with | 0 -> let res = (List.length m1) - (List.length m2) in @@ -142,7 +146,7 @@ let rec select env goals passive = match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false in let (pos_list, pos_set), passive_table = passive in - let remove eq l = List.filter (fun e -> e <> eq) l in + let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in if !weight_age_ratio > 0 then weight_age_counter := !weight_age_counter - 1; match !weight_age_counter with @@ -192,7 +196,7 @@ let rec select env goals passive = let passive_table = Indexing.remove_index passive_table current in - current, + current, ((remove current pos_list, EqualitySet.remove current pos_set), passive_table)) | _ -> @@ -255,8 +259,6 @@ let prune_passive howmany (active, _) passive = and in_age = round (howmany /. (ratio +. 1.)) in debug_print (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age)); - let symbols, card = None, 0 - in let counter = ref !symbols_ratio in let rec pickw w ps = if w > 0 then @@ -264,7 +266,7 @@ let prune_passive howmany (active, _) passive = let _ = counter := !counter - 1; if !counter = 0 then counter := !symbols_ratio in - let e = EqualitySet.min_elt ps in + let e = EqualitySet.min_elt ps in let ps' = pickw (w-1) (EqualitySet.remove e ps) in EqualitySet.add e ps' else @@ -300,7 +302,7 @@ let prune_passive howmany (active, _) passive = (** inference of new equalities between current and some in active *) -let infer env current ((active_list:Inference.equality list), active_table) = +let infer env current (active_list, active_table) = let (_,c,_) = env in if Utils.debug_metas then (ignore(Indexing.check_target c current "infer1"); @@ -325,9 +327,9 @@ let infer env current ((active_list:Inference.equality list), active_table) = (function current -> Indexing.check_target c current "sup2") res); let pos = infer_positive table tl in - res @ pos + res @ pos in - let maxm, copy_of_current = Inference.fix_metas !maxmeta current in + let maxm, copy_of_current = Equality.fix_metas !maxmeta current in maxmeta := maxm; let curr_table = Indexing.index Indexing.empty current in let pos = infer_positive curr_table (copy_of_current::active_list) @@ -336,7 +338,7 @@ let infer env current ((active_list:Inference.equality list), active_table) = ignore(List.map (function current -> Indexing.check_target c current "sup3") pos); - res @ pos + res @ pos in derived_clauses := !derived_clauses + (List.length new_pos); match !maximal_retained_equality with @@ -365,7 +367,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = let newmeta, newcurrent = Indexing.demodulation_equality !maxmeta env table sign current in maxmeta := newmeta; - if is_identity env newcurrent then + if Equality.is_identity env newcurrent then (* debug_print *) (* (lazy *) (* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *) @@ -396,7 +398,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = match demodulate passive_table newcurrent with | None -> None | Some newnewcurrent -> - if newcurrent <> newnewcurrent then + if Equality.compare newcurrent newnewcurrent <> 0 then demod newnewcurrent else Some newnewcurrent in @@ -404,6 +406,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = match res with | None -> None | Some c -> + (* immagino non funzioni piu'... *) if Indexing.in_index active_table c then None else @@ -471,7 +474,7 @@ let forward_simplify_new env new_pos ?passive active = let new_pos_set = List.fold_left (fun s e -> - if not (Inference.is_identity env e) then + if not (Equality.is_identity env e) then if EqualitySet.mem e s then s else EqualitySet.add e s else s) @@ -510,12 +513,11 @@ let rec simplify_goal env goal ?passive (active_list, active_table) = | None -> None | Some ((_, _), pt) -> Some pt in - let demodulate table goal = - let newmeta, newgoal = + let changed, newmeta, newgoal = Indexing.demodulation_goal !maxmeta env table goal in maxmeta := newmeta; - goal <> newgoal, newgoal + changed, newgoal in let changed, goal = match passive_table with @@ -565,28 +567,28 @@ let backward_simplify_active env new_pos new_table min_weight active = let active_list, newa = List.fold_right (fun equality (res, newn) -> - let ew, _, _, _ = equality in + let ew, _, _, _,_ = Equality.open_equality equality in if ew < min_weight then equality::res, newn else match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with | None -> res, newn | Some e -> - if equality = e then + if Equality.compare equality e = 0 then e::res, newn else res, e::newn) active_list ([], []) in let find eq1 where = - List.exists (meta_convertibility_eq eq1) where + List.exists (Equality.meta_convertibility_eq eq1) where in let active, newa = List.fold_right (fun eq (res, tbl) -> if List.mem eq res then res, tbl - else if (is_identity env eq) || (find eq res) then ( + else if (Equality.is_identity env eq) || (find eq res) then ( res, tbl ) else @@ -594,8 +596,8 @@ let backward_simplify_active env new_pos new_table min_weight active = active_list ([], Indexing.empty), List.fold_right (fun eq p -> - if (is_identity env eq) then p - else eq::p) + if (Equality.is_identity env eq) then p + else eq::p) newa [] in match newa with @@ -608,7 +610,7 @@ let backward_simplify_active env new_pos new_table min_weight active = let backward_simplify_passive env new_pos new_table min_weight passive = let (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = - let ew, _, _, _ = equality in + let ew, _, _, _ , _ = Equality.open_equality equality in if ew < min_weight then equality::resl, ress, newn else @@ -636,7 +638,7 @@ let backward_simplify env new' ?passive active = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> - let ew, _, _, _ = e in + let ew, _, _, _ , _ = Equality.open_equality e in e::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) new' in @@ -658,7 +660,7 @@ let close env new' given = let new_pos, new_table, min_weight = List.fold_left (fun (l, t, w) e -> - let ew, _, _, _ = e in + let ew, _, _, _ , _ = Equality.open_equality e in e::l, Indexing.index t e, min ew w) ([], Indexing.empty, 1000000) (snd new') in @@ -670,7 +672,9 @@ let close env new' given = ;; let is_commutative_law eq = - let w, proof, (eq_ty, left, right, order), metas = eq in + let w, proof, (eq_ty, left, right, order), metas , _ = + Equality.open_equality eq + in match left,right with Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] -> @@ -686,7 +690,7 @@ let prova env new' active = (Printf.sprintf "symmetric:\n%s\n" (String.concat "\n" (List.map - (fun e -> string_of_equality ~env e) + (fun e -> Equality.string_of_equality ~env e) given)))) in close env new' given ;; @@ -794,7 +798,7 @@ let simplify_equalities env equalities = (lazy (Printf.sprintf "equalities:\n%s\n" (String.concat "\n" - (List.map string_of_equality equalities)))); + (List.map Equality.string_of_equality equalities)))); debug_print (lazy "SIMPLYFYING EQUALITIES..."); match equalities with | [] -> [] @@ -806,7 +810,7 @@ let simplify_equalities env equalities = (lazy (Printf.sprintf "equalities AFTER:\n%s\n" (String.concat "\n" - (List.map string_of_equality res)))); + (List.map Equality.string_of_equality res)))); res ;; @@ -822,28 +826,42 @@ let print_goals goals = Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) ;; -let check_if_goal_is_subsumed env (proof,menv,ty) table = +let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when UriManager.eq uri (LibraryObjects.eq_URI ()) -> - (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in - match Indexing.subsumption env table goal_equation with - | Some (subst, (_,p,_,m)) -> - let p = Inference.apply_subst subst (Inference.build_proof_term p) in - let newp = - let rec repl = function - | Inference.ProofGoalBlock (_, gp) -> - Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) - | Inference.NoProof -> Inference.BasicProof ([],p) - | Inference.BasicProof _ -> Inference.BasicProof ([],p) - | Inference.SubProof (t, i, p2) -> - Inference.SubProof (t, i, repl p2) - | _ -> assert false - in - repl proof - in - Some (newp,Inference.apply_subst_metasenv subst m @ menv) - | None -> None) + (let goal_equation = + Equality.mk_equality + (0,(Equality.Exact (Cic.Rel (-1)),proof),(eq_ty,left,right,Eq),menv) + in + match Indexing.subsumption env table goal_equation with + | Some (subst, equality ) -> + let (_,(np,p),(ty,l,r,_),m,id) = + Equality.open_equality equality in + let p = Equality.apply_subst subst + (Equality.build_proof_term_old p) in + let newp = + let rec repl = function + | Equality.ProofGoalBlock (_, gp) -> + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,p), gp) + | Equality.NoProof -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.BasicProof _ -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.SubProof (t, i, p2) -> + Equality.SubProof (t, i, repl p2) + | _ -> assert false + in + repl proof + in + let newcicp,np,subst,cicmenv = + cicproof,np, subst, (m @ menv) + in + Some + ((newcicp,np,subst,cicmenv), + (newp, Equality.apply_subst_metasenv subst m @ menv )) + | None -> None) | _ -> None ;; @@ -883,22 +901,31 @@ let rec given_clause_fullred dbd env goals theorems ~passive active = in let newp = let rec repl = function - | Inference.ProofGoalBlock (_, gp) -> - Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp) - | Inference.NoProof -> Inference.BasicProof ([],p) - | Inference.BasicProof _ -> Inference.BasicProof ([],p) - | Inference.SubProof (t, i, p2) -> - Inference.SubProof (t, i, repl p2) + | Equality.ProofGoalBlock (_, gp) -> + Equality.ProofGoalBlock + (Equality.BasicProof (Equality.empty_subst,p), gp) + | Equality.NoProof -> + + Equality.BasicProof (Equality.empty_subst,p) + | Equality.BasicProof _ -> + Equality.BasicProof (Equality.empty_subst,p) + | Equality.SubProof (t, i, p2) -> + Equality.SubProof (t, i, repl p2) | _ -> assert false in - repl proof - in true, Some (newp,m) + repl (snd proof) + in + let reflproof = Equality.refl_proof eq_ty left in + true, + Some ((fst proof,Equality.Exact reflproof, + Equality.empty_subst,m), + (newp,m)) | (_, [proof,m,ty])::_ -> (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with | None -> false,None - | Some (newproof,m) -> + | Some p -> prerr_endline "Proof found by subsumption!"; - true, Some (newproof,m)) + true, Some p) | _ -> false, None in if ok then @@ -940,7 +967,6 @@ let rec given_clause_fullred dbd env goals theorems ~passive active = and given_clause_fullred_aux dbd env goals theorems passive active = prerr_endline (string_of_int !counter ^ " MAXMETA: " ^ string_of_int !maxmeta ^ - " LOCALMAX: " ^ string_of_int !Indexing.local_max ^ " #ACTIVES: " ^ string_of_int (size_of_active active) ^ " #PASSIVES: " ^ string_of_int (size_of_passive passive)); incr counter; @@ -1008,7 +1034,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | false -> let current, passive = select env (fst goals) passive in prerr_endline - ("Selected = " ^ string_of_equality ~env current); + ("Selected = " ^ Equality.string_of_equality ~env current); (* ^ (let w,p,(t,l,r,o),m = current in " size w: " ^ string_of_int (HExtlib.estimate_size w)^ @@ -1029,8 +1055,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (* weight_age_counter := !weight_age_counter + 1; *) given_clause_fullred dbd env goals theorems passive active | Some current -> - debug_print (lazy (Printf.sprintf "selected: %s" - (string_of_equality ~env current))); + prerr_endline (Printf.sprintf "selected sipl: %s" + (Equality.string_of_equality ~env current)); let t1 = Unix.gettimeofday () in let new' = infer env current active in let _ = @@ -1040,12 +1066,12 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (String.concat "\n" (List.map (fun e -> "Positive " ^ - (string_of_equality ~env e)) new')))) + (Equality.string_of_equality ~env e)) new')))) in let t2 = Unix.gettimeofday () in infer_time := !infer_time +. (t2 -. t1); let active = - if is_identity env current then active + if Equality.is_identity env current then active else let al, tbl = active in al @ [current], Indexing.index tbl current @@ -1065,14 +1091,13 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | None, None -> active, passive, new' | Some p, None | None, Some p -> - let np = new' in - if Utils.debug_metas then - begin - List.iter - (fun x->Indexing.check_target context x "simplify1") - p; - end; - simplify (new' @ p) active passive + if Utils.debug_metas then + begin + List.iter + (fun x->Indexing.check_target context x "simplify1") + p; + end; + simplify (new' @ p) active passive | Some p, Some rp -> simplify (new' @ p @ rp) active passive in @@ -1105,7 +1130,7 @@ end prova *) (Printf.sprintf "active:\n%s\n" (String.concat "\n" ((List.map - (fun e -> (string_of_equality ~env e)) + (fun e -> (Equality.string_of_equality ~env e)) (fst active)))))) in let _ = @@ -1115,7 +1140,7 @@ end prova *) (String.concat "\n" ((List.map (fun e -> "Negative " ^ - (string_of_equality ~env e)) new'))))) + (Equality.string_of_equality ~env e)) new'))))) in let passive = add_to_passive passive new' in given_clause_fullred dbd env goals theorems passive active @@ -1142,10 +1167,10 @@ let rec saturate_equations env goal accept_fun passive active = saturate_equations env goal accept_fun passive active | Some current -> debug_print (lazy (Printf.sprintf "selected: %s" - (string_of_equality ~env current))); + (Equality.string_of_equality ~env current))); let new' = infer env current active in let active = - if is_identity env current then active + if Equality.is_identity env current then active else let al, tbl = active in al @ [current], Indexing.index tbl current @@ -1167,24 +1192,25 @@ let rec saturate_equations env goal accept_fun passive active = (Printf.sprintf "active:\n%s\n" (String.concat "\n" (List.map - (fun e -> string_of_equality ~env e) + (fun e -> Equality.string_of_equality ~env e) (fst active))))) in - let _ = + let _ = debug_print (lazy (Printf.sprintf "new':\n%s\n" (String.concat "\n" (List.map (fun e -> "Negative " ^ - (string_of_equality ~env e)) new')))) + (Equality.string_of_equality ~env e)) new')))) in let new' = List.filter accept_fun new' in let passive = add_to_passive passive new' in saturate_equations env goal accept_fun passive active ;; - +let main dbd full term metasenv ugraph = () +(* let main dbd full term metasenv ugraph = let module C = Cic in let module T = CicTypeChecker in @@ -1246,7 +1272,9 @@ let main dbd full term metasenv ugraph = (fst theorems))))) in (*try*) - let goal = Inference.BasicProof ([],new_meta_goal), [], goal in + let goal = + ([],Equality.BasicProof (Equality.empty_subst ,new_meta_goal)), [], goal + in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in @@ -1258,7 +1286,7 @@ let main dbd full term metasenv ugraph = Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map - (string_of_equality ~env) equalities)); + (Equality.string_of_equality ~env) equalities)); (* (equalities @ library_equalities))); *) print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in @@ -1274,17 +1302,27 @@ let main dbd full term metasenv ugraph = match res with | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some (proof, env)) -> - let proof = Inference.build_proof_term proof in + | ParamodulationSuccess (Some ((cicproof,cicmenv),(proof, env))) -> Printf.printf "OK, found a proof!\n"; + let oldproof = Equation.build_proof_term proof in + let newproof,_,newenv,_ = + CicRefine.type_of_aux' + cicmenv context cicproof CicUniv.empty_ugraph + in (* REMEMBER: we have to instantiate meta_proof, we should use apply the "apply" tactic to proof and status *) let names = names_of_context context in + prerr_endline "OLD PROOF"; print_endline (PP.pp proof names); + prerr_endline "NEW PROOF"; + print_endline (PP.pp newproof names); let newmetasenv = List.fold_left - (fun m (_, _, _, menv) -> m @ menv) metasenv equalities + (fun m eq -> + let (_, _, _, menv,_) = Equality.open_equality eq in + m @ menv) + metasenv equalities in let _ = (*try*) @@ -1316,8 +1354,6 @@ let main dbd full term metasenv ugraph = "backward_simpl_time: %.9f\n") !infer_time !forward_simpl_time !forward_simpl_new_time !backward_simpl_time) ^ - (Printf.sprintf "beta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ (Printf.sprintf "passive_maintainance_time: %.9f\n" !passive_maintainance_time) ^ (Printf.sprintf " successful unification/matching time: %.9f\n" @@ -1337,14 +1373,13 @@ let main dbd full term metasenv ugraph = raise exc *) ;; - +*) let default_depth = !maxdepth and default_width = !maxwidth;; let reset_refs () = maxmeta := 0; - Indexing.local_max := 100; symbols_counter := 0; weight_age_counter := !weight_age_ratio; processed_clauses := 0; @@ -1358,10 +1393,50 @@ let reset_refs () = passive_maintainance_time := 0.; derived_clauses := 0; kept_clauses := 0; - Indexing.beta_expand_time := 0.; - Inference.metas_of_proof_time := 0.; + Equality.reset (); +;; + +let interactive_comparison context t1 t2 = + let rc = ref [] in + let module P = Printf in + let rec aux n context t1 t2 = +(* let names = names_of_context context in*) + let pp t1 t2 = () (* + P.eprintf "%s%s === %s\n" (String.make n ' ') + (CicPp.pp t1 names) (CicPp.pp t2 names) *) + in + match t1,t2 with + | _, Cic.Appl [Cic.Const(uri,_);t2] when + UriManager.eq uri (UriManager.uri_of_string + "cic:/Coq/Init/Logic/sym_eq.con")-> aux n context t1 t2 + | Cic.Implicit _, _ -> pp t1 t2 + | Cic.Meta (n,_), _ -> + rc := (n,t2,context) :: !rc; + pp (Cic.Meta(n,[])) t2 + | Cic.Rel n1, Cic.Rel n2 when n1 = n2 -> pp t1 t2 + | Cic.Appl l1,Cic.Appl l2 -> + if List.length l1 <> List.length l2 then + begin + prerr_endline "ERROR: application with diff num of args"; + pp t1 t2 + end + else + List.iter2 (aux (n+1) context) l1 l2 + | Cic.Lambda (name,s,t1),Cic.Lambda(_,_,t2) -> + let context = (Some (name,(Cic.Decl s)))::context in + aux (n+1) context t1 t2 + | Cic.Const (u1,_), Cic.Const (u2,_) when UriManager.eq u1 u2 -> + pp t1 t2 + | _,_ -> pp t1 t2 + in + aux 0 context t1 t2; + List.iter (fun (n,t,ctx) -> + let names = names_of_context ctx in + Printf.eprintf "%d := %s\n" n (CicPp.pp t names)) + (HExtlib.list_uniq (List.sort (fun (x,_,_) (y,_,_) -> x-y) !rc)) ;; + let saturate dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = let module C = Cic in @@ -1375,7 +1450,6 @@ let saturate let goal' = goal in let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in - prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context)); let eq_indexes, equalities, maxm = find_equalities context proof in let new_meta_goal, metasenv, type_of_goal = let irl = @@ -1389,7 +1463,9 @@ let saturate in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in - let goal = Inference.BasicProof ([],new_meta_goal), [], goal in + let goal = + ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal + in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -1445,20 +1521,31 @@ let saturate (res, finish -. start) in match res with - | ParamodulationSuccess (Some (proof, proof_menv)) -> + | ParamodulationSuccess + (Some ((goalproof,newproof,subsumption_subst, newproof_menv),(proof, proof_menv))) -> prerr_endline "OK, found a proof!"; - debug_print (lazy "OK, found a proof!"); - let proof = Inference.build_proof_term proof in + prerr_endline (Equality.string_of_proof_old proof); + + let cic_proof = Equality.build_proof_term_old proof in + + let cic_proof_new,cic_proof_new_menv = + 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 + let equality_for_replace i t1 = match t1 with | C.Meta (n, _) -> n = i | _ -> false in - prerr_endline "replacing metas"; + let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in + prerr_endline "replacing metas (old)"; let proof_menv, what, with_what = - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in + let irl = mkirl context in List.fold_left (fun (acc1,acc2,acc3) (i,_,ty) -> (i,context,ty)::acc1, @@ -1466,13 +1553,35 @@ let saturate (Cic.Meta(i,irl)) ::acc3) ([],[],[]) proof_menv in - let proof = ProofEngineReduction.replace_lifting + let cic_proof = ProofEngineReduction.replace_lifting + ~equality:(=) + ~what ~with_what + ~where:cic_proof + in + prerr_endline "replacing metas (new)"; + let newproof_menv, what, with_what = + let irl = mkirl context in + List.fold_left + (fun (acc1,acc2,acc3) (i,_,ty) -> + (i,context,ty)::acc1, + (Cic.Meta(i,[]))::acc2, + (Cic.Meta(i,irl)) ::acc3) + ([],[],[]) newproof_menv + in + let cic_proof_new = ProofEngineReduction.replace_lifting ~equality:(=) ~what ~with_what - ~where:proof + ~where:cic_proof_new in - (* prerr_endline (CicPp.ppterm proof); *) let names = names_of_context context in + prerr_endline "OLDPROOF"; + prerr_endline (Equality.string_of_proof_old proof); + prerr_endline "OLDPROOFCIC"; + prerr_endline (CicPp.pp cic_proof names); + prerr_endline "NEWPROOF"; + prerr_endline (Equality.string_of_proof_new ~names newproof goalproof); + prerr_endline "NEWPROOFCIC"; + prerr_endline (CicPp.pp cic_proof_new names); let newmetasenv = let i1 = match new_meta_goal with @@ -1481,13 +1590,70 @@ let saturate List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv in let newmetasenv = newmetasenv@proof_menv in + let newmetasenv_new = newmetasenv@newproof_menv in let newstatus = try - let ty, ug = - prerr_endline "type checking ... "; - CicTypeChecker.type_of_aux' newmetasenv context proof ugraph + let cic_proof,newmetasenv,proof_menv,ty, ug = + prerr_endline "type checking ... (old) "; +(* let old_ty, oldug = *) +(* CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph *) +(* in*) + let cic_proof_new,new_ty,newmetasenv_new,newug = + try + (* + prerr_endline "refining ... (new) "; + CicRefine.type_of_aux' + newmetasenv_new context cic_proof_new ugraph*) + let ty,ug = + prerr_endline "typechecking ... (new) "; + CicTypeChecker.type_of_aux' + newmetasenv_new context cic_proof_new ugraph + in + cic_proof_new, ty, newmetasenv_new, ug + with + | CicTypeChecker.TypeCheckerFailure s -> + prerr_endline "FAILURE IN TYPECHECKING"; + prerr_endline (Lazy.force s); + assert false + | CicRefine.RefineFailure s + | CicRefine.Uncertain s + | CicRefine.AssertFailure s -> + prerr_endline "FAILURE IN REFINE"; + prerr_endline (Lazy.force s); + interactive_comparison context cic_proof_new cic_proof; + assert false + in +(* + prerr_endline "check unif ... (old vs new) "; + (try + ignore(CicUnification.fo_unif + newmetasenv_new context cic_proof_new cic_proof CicUniv.empty_ugraph) + with CicUnification.UnificationFailure _ -> + prerr_endline "WARNING, new and old proofs are not unifiable"); + prerr_endline "unif ... (new) "; + let subst, newmetasenv_new, newug = + CicUnification.fo_unif + newmetasenv_new context new_ty type_of_goal newug + in + if subst <> [] then + prerr_endline "UNIF SERVE ################################"; +*) + let subst = [] in + if List.length newmetasenv_new <> 0 then + prerr_endline + ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv + [] newmetasenv_new); + (CicMetaSubst.apply_subst subst cic_proof_new), + newmetasenv_new, + (CicMetaSubst.apply_subst_metasenv subst newmetasenv_new), + (CicMetaSubst.apply_subst subst new_ty), + newug +(* cic_proof,newmetasenv,proof_menv,oldty,oldug*) in - prerr_endline (CicPp.pp proof [](* names *)); + prerr_endline "FINAL PROOF"; + prerr_endline (CicPp.pp cic_proof names); + prerr_endline "ENDOFPROOFS"; + debug_print (lazy (Printf.sprintf @@ -1499,7 +1665,7 @@ let saturate let real_proof = ProofEngineReduction.replace ~equality:equality_for_replace - ~what:[goal'] ~with_what:[proof] + ~what:[goal'] ~with_what:[cic_proof] ~where:meta_proof in debug_print @@ -1514,7 +1680,7 @@ let saturate List.map (fun (i,_,_) -> i) proof_menv) with CicTypeChecker.TypeCheckerFailure _ -> debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!"); - debug_print (lazy (CicPp.pp proof names)); + debug_print (lazy (CicPp.pp cic_proof names)); raise (ProofEngineTypes.Fail (lazy "Found a proof, but it doesn't typecheck")) in @@ -1529,10 +1695,6 @@ let saturate (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^ - (Printf.sprintf "\nbeta_expand_time: %.9f\n" - !Indexing.beta_expand_time) ^ - (Printf.sprintf "\nmetas_of_proof: %.9f\n" - !Inference.metas_of_proof_time) ^ (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^ (Printf.sprintf "\nforward_simpl_new_times: %.9f" !forward_simpl_new_time) ^ @@ -1629,7 +1791,7 @@ let retrieve_and_print dbd term metasenv ugraph = (fun (u, e) -> Printf.sprintf "%s: %s" (UriManager.string_of_uri u) - (string_of_equality e) + (Equality.string_of_equality e) ) res)))); res in @@ -1669,7 +1831,9 @@ let main_demod_equalities dbd term metasenv ugraph = in let env = (metasenv, context, ugraph) in (*try*) - let goal = Inference.BasicProof ([],new_meta_goal), [], goal in + let goal = + ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal + in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in let passive = make_passive equalities in @@ -1678,7 +1842,7 @@ let main_demod_equalities dbd term metasenv ugraph = Printf.printf "\nequalities:\n%s\n" (String.concat "\n" (List.map - (string_of_equality ~env) equalities)); + (Equality.string_of_equality ~env) equalities)); print_endline "--------------------------------------------------"; print_endline "GO!"; start_time := Unix.gettimeofday (); @@ -1705,12 +1869,12 @@ let main_demod_equalities dbd term metasenv ugraph = EqualitySet.elements (List.fold_left addfun EqualitySet.empty l) in Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n" - (String.concat "\n" (List.map (string_of_equality ~env) active)) + (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) (* (String.concat "\n" (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *) (* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *) (String.concat "\n" - (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive)); + (List.map (fun e -> CicPp.ppterm (Equality.term_of_equality e)) passive)); print_newline (); (* with e -> @@ -1729,7 +1893,9 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in let goalterm = Cic.Meta (metano,irl) in - let initgoal = Inference.BasicProof ([],goalterm), [], ty in + let initgoal = + ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty + in let env = (metasenv, context, CicUniv.empty_ugraph) in let equalities = simplify_equalities env (equalities@library_equalities) in let table = @@ -1737,14 +1903,15 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = (fun tbl eq -> Indexing.index tbl eq) Indexing.empty equalities in - let newmeta,(newproof,newmetasenv, newty) = Indexing.demodulation_goal - maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal + let _, newmeta,(newproof,newmetasenv, newty) = + Indexing.demodulation_goal + maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal in if newmeta != maxm then begin let opengoal = Cic.Meta(maxm,irl) in let proofterm = - Inference.build_proof_term ~noproof:opengoal newproof in + Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in let extended_metasenv = (maxm,context,newty)::metasenv in let extended_status = (curi,extended_metasenv,pbo,pty),goal in diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml index db19e87d1..18ccd5f79 100644 --- a/components/tactics/paramodulation/utils.ml +++ b/components/tactics/paramodulation/utils.ml @@ -60,6 +60,8 @@ let string_of_comparison = function | Eq -> "=" | Incomparable -> "I" +type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph + module OrderedTerm = struct type t = Cic.term @@ -291,7 +293,7 @@ end module IntSet = Set.Make(OrderedInt) let compute_equality_weight (ty,left,right,o) = - let factor = 1 in + let factor = 2 in match o with | Lt -> let w, m = (weight_of_term @@ -731,3 +733,30 @@ 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 ()) + +let rec metas_of_term = function + | Cic.Meta (i, c) -> [i] + | Cic.Var (_, ens) + | Cic.Const (_, ens) + | Cic.MutInd (_, _, ens) + | Cic.MutConstruct (_, _, _, ens) -> + List.flatten (List.map (fun (u, t) -> metas_of_term t) ens) + | Cic.Cast (s, t) + | Cic.Prod (_, s, t) + | Cic.Lambda (_, s, t) + | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t) + | Cic.Appl l -> List.flatten (List.map metas_of_term l) + | Cic.MutCase (uri, i, s, t, l) -> + (metas_of_term s) @ (metas_of_term t) @ + (List.flatten (List.map metas_of_term l)) + | Cic.Fix (i, il) -> + List.flatten + (List.map (fun (s, i, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | Cic.CoFix (i, il) -> + List.flatten + (List.map (fun (s, t1, t2) -> + (metas_of_term t1) @ (metas_of_term t2)) il) + | _ -> [] +;; + diff --git a/components/tactics/paramodulation/utils.mli b/components/tactics/paramodulation/utils.mli index bef03b141..f44cab460 100644 --- a/components/tactics/paramodulation/utils.mli +++ b/components/tactics/paramodulation/utils.mli @@ -34,6 +34,8 @@ type weight = int * (int * int) list;; type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;; +type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph + val print_metasenv: Cic.metasenv -> string val print_subst: ?prefix:string -> Cic.substitution -> string @@ -90,3 +92,6 @@ 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 + +val metas_of_term: Cic.term -> int list + -- 2.39.2