From 9559b53134624dbee523cf6406a9852665c0ff77 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 14 May 2006 13:53:37 +0000 Subject: [PATCH] - Removed old proofs - Equality.ml splittend in to subst.ml and equality.ml, the former only for substs - patch to kill passive generated from an active that is dropped - fixed deep subsumption --- components/tactics/.depend | 11 +- components/tactics/Makefile | 1 + components/tactics/paramodulation/equality.ml | 677 +++++------------- .../tactics/paramodulation/equality.mli | 52 +- components/tactics/paramodulation/indexing.ml | 114 +-- .../tactics/paramodulation/indexing.mli | 6 +- .../tactics/paramodulation/inference.ml | 30 +- .../tactics/paramodulation/inference.mli | 4 +- .../tactics/paramodulation/saturation.ml | 248 +++---- components/tactics/paramodulation/subst.ml | 215 ++++++ components/tactics/paramodulation/subst.mli | 43 ++ 11 files changed, 619 insertions(+), 782 deletions(-) create mode 100644 components/tactics/paramodulation/subst.ml create mode 100644 components/tactics/paramodulation/subst.mli diff --git a/components/tactics/.depend b/components/tactics/.depend index 41cc4bb67..360128fce 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -5,7 +5,8 @@ reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi -paramodulation/equality.cmi: paramodulation/utils.cmi +paramodulation/equality.cmi: paramodulation/utils.cmi \ + paramodulation/subst.cmi paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \ paramodulation/equality.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ @@ -58,10 +59,14 @@ 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/subst.cmo: paramodulation/subst.cmi +paramodulation/subst.cmx: paramodulation/subst.cmi paramodulation/equality.cmo: paramodulation/utils.cmi \ - proofEngineReduction.cmi paramodulation/equality.cmi + paramodulation/subst.cmi proofEngineReduction.cmi \ + paramodulation/equality.cmi paramodulation/equality.cmx: paramodulation/utils.cmx \ - proofEngineReduction.cmx paramodulation/equality.cmi + paramodulation/subst.cmx proofEngineReduction.cmx \ + paramodulation/equality.cmi paramodulation/inference.cmo: paramodulation/utils.cmi proofEngineHelpers.cmi \ metadataQuery.cmi paramodulation/equality.cmi \ paramodulation/inference.cmi diff --git a/components/tactics/Makefile b/components/tactics/Makefile index 2cecc0401..1fe925282 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/subst.mli\ paramodulation/equality.mli\ paramodulation/inference.mli\ paramodulation/equality_indexing.mli\ diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 5248a6a92..b921f78c1 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -25,194 +25,6 @@ (* $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 = @@ -225,21 +37,11 @@ type equality = Utils.comparison) * (* ordering *) Cic.metasenv * (* environment for metas *) int (* id *) -and proof = new_proof * old_proof - -and new_proof = +and 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 + | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term) + (* subst, (rule,eq1, eq2,predicate) *) +and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list ;; (* globals *) @@ -257,16 +59,16 @@ let reset () = let uncomparable = fun _ -> 0 -let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) = +let mk_equality (weight,p,(ty,l,r,o),m) = let id = freshid () in - let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in + let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in Hashtbl.add id_to_eq id eq; eq ;; let mk_tmp_equality (weight,(ty,l,r,o),m) = let id = -1 in - uncomparable,weight,(Exact (Cic.Implicit None),NoProof),(ty,l,r,o),m,id + uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id ;; @@ -294,34 +96,15 @@ 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,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in p,l,r with Not_found -> assert false -let string_of_proof_new ?(names=[]) p gp = +let string_of_proof ?(names=[]) p gp = let str_of_rule = function | SuperpositionRight -> "SupR" | SuperpositionLeft -> "SupL" @@ -339,7 +122,7 @@ let string_of_proof_new ?(names=[]) p gp = 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) + prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) (CicPp.pp pred names)^ aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) @@ -350,23 +133,23 @@ let string_of_proof_new ?(names=[]) p gp = (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)) ^ + (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i))) gp) ;; let rec depend eq id = - let (_,(p,_),(_,_,_,_),_,ideq) = open_equality eq in + let (_,p,(_,_,_,_),_,ideq) = open_equality eq in if id = ideq then true else match p with Exact _ -> false | Step (_,(_,id1,(_,id2),_)) -> - let eq1 = Hashtbl.find id_to_eq id1 in - let eq2 = Hashtbl.find id_to_eq id2 in - depend eq1 id || depend eq1 id2 + let eq1 = Hashtbl.find id_to_eq id1 in + let eq2 = Hashtbl.find id_to_eq id2 in + depend eq1 id || depend eq2 id2 ;; - -let ppsubst = ppsubst ~names:[] + +let ppsubst = Subst.ppsubst ~names:[];; (* returns an explicit named subst and a list of arguments for sym_eq_URI *) let build_ens uri termlist = @@ -385,61 +168,6 @@ let build_ens uri 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 (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 mk_sym uri ty t1 t2 p = let ens, args = build_ens uri [ty;t1;t2;p] in Cic.Appl (Cic.Const(uri, ens) :: args) @@ -468,6 +196,25 @@ let open_trans ens tl = | _ -> assert false ;; +let open_eq_ind args = + match args with + | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr + | _ -> assert false +;; + +let open_pred pred = + match pred with + | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r])) + when LibraryObjects.is_eq_URI uri -> ty,uri,l,r + | _ -> prerr_endline (CicPp.ppterm pred); assert false +;; + +let is_not_fixed t = + CicSubstitution.subst (Cic.Implicit None) t <> + CicSubstitution.subst (Cic.Rel 1) t +;; + + let canonical t = let rec remove_refl t = match t with @@ -526,189 +273,147 @@ let canonical t = | Cic.Appl l -> Cic.Appl (List.map canonical l) | _ -> t in - remove_refl (canonical t) + remove_refl (canonical t) +;; + +let ty_of_lambda = function + | Cic.Lambda (_,ty,_) -> ty + | _ -> assert false +;; + +let compose_contexts ctx1 ctx2 = + ProofEngineReduction.replace_lifting + ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1 +;; + +let put_in_ctx ctx t = + ProofEngineReduction.replace_lifting + ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx +;; + +let mk_eq uri ty l r = + Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] +;; + +let mk_refl uri ty t = + Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t] +;; + +let open_eq = function + | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri -> + uri, ty, l ,r + | _ -> assert false +;; + +let contextualize uri ty left right t = + (* aux [uri] [ty] [left] [right] [ctx] [t] + * + * the parameters validate this invariant + * t: eq(uri) ty left right + * that is used only by the base case + * + * ctx is a term with an open (Rel 1). (Rel 1) is the empty context + *) + let rec aux uri ty left right ctx_d = function + | Cic.Appl ((Cic.Const(uri_ind,ens))::tl) + when LibraryObjects.is_eq_ind_URI uri_ind || + LibraryObjects.is_eq_ind_r_URI uri_ind -> + let ty1,what,pred,p1,other,p2 = open_eq_ind tl in + let ty2,eq,lp,rp = open_pred pred in + let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in + let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in + let is_not_fixed_lp = is_not_fixed lp in + let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in + (* extract the context and the fixed term from the predicate *) + let m, ctx_c = + let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in + (* they were under a lambda *) + let m = CicSubstitution.subst (Cic.Implicit None) m in + let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in + m, ctx_c + in + (* create the compound context and put the terms under it *) + let ctx_dc = compose_contexts ctx_d ctx_c in + let dc_what = put_in_ctx ctx_dc what in + let dc_other = put_in_ctx ctx_dc other in + (* m is already in ctx_c so it is put in ctx_d only *) + let d_m = put_in_ctx ctx_d m in + (* we also need what in ctx_c *) + let c_what = put_in_ctx ctx_c what in + (* now put the proofs in the compound context *) + let p1 = (* p1: dc_what = d_m *) + if is_not_fixed_lp then + aux uri ty1 c_what m ctx_d p1 + else + mk_sym uri_sym ty d_m dc_what + (aux uri ty1 m c_what ctx_d p1) + in + let p2 = (* p2: dc_other = dc_what *) + if avoid_eq_ind then + mk_sym uri_sym ty dc_what dc_other + (aux uri ty1 what other ctx_dc p2) + else + aux uri ty1 other what ctx_dc p2 + in + (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m + if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *) + let a,b,c,paeqb,pbeqc = + if is_not_fixed_lp then + dc_other,dc_what,d_m,p2,p1 + else + d_m,dc_what,dc_other, + (mk_sym uri_sym ty dc_what d_m p1), + (mk_sym uri_sym ty dc_other dc_what p2) + in + mk_trans uri_trans ty a b c paeqb pbeqc + | t -> + let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in + let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in + let pred = + (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *) + let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *) + let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in + let l = ctx_d in + let lty = CicSubstitution.lift 1 ty in + Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r)) + in + let d_left = put_in_ctx ctx_d left in + let d_right = put_in_ctx ctx_d right in + let refl_eq = mk_refl uri ty d_left in + mk_sym uri_sym ty d_right d_left + (mk_eq_ind uri_ind ty left pred refl_eq right t) + in + let empty_context = Cic.Rel 1 in + aux uri ty left right empty_context t ;; +let contextualize_rewrites t ty = + let eq,ty,l,r = open_eq ty in + contextualize eq ty l r t +;; + let build_proof_step subst p1 p2 pos l r pred = - 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,body = (* Cic.Implicit None *) + let p1 = Subst.apply_subst subst p1 in + let p2 = Subst.apply_subst subst p2 in + let l = Subst.apply_subst subst l in + let r = Subst.apply_subst subst r in + let pred = Subst.apply_subst subst pred in + let ty,body = match pred with | Cic.Lambda (_,ty,body) -> ty,body | _ -> assert false in - let what, other = (* Cic.Implicit None, Cic.Implicit None *) + let what, other = if pos = Utils.Left then l,r else r,l in - let is_not_fixed t = - CicSubstitution.subst (Cic.Implicit None) t <> - CicSubstitution.subst (Cic.Rel 1) t - in - match body,pos with -(* - |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in - mk_trans uri_trans ty other what third - (mk_sym uri_sym ty what other p2) p1 - |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - mk_trans uri_trans ty other what third p2 p1 - |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - mk_trans uri_trans ty third what other p1 p2 - |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right -> - let third = CicSubstitution.subst (Cic.Implicit None) third in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let uri_sym = LibraryObjects.sym_eq_URI ~eq in - mk_trans uri_trans ty third what other p1 - (mk_sym uri_sym ty other what p2) - | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs - -> - let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t lhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) - (inject ty lhs m r pmr) (inject ty lhs l m plm) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2) - in - mk_trans uri_trans ty pred_of_other pred_of_what rhs - (inject ty lhs what other p2) p1 - | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs - -> - let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t lhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) - (inject ty lhs m l plm) - (inject ty lhs r m pmr) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = - CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - mk_eq_ind (Utils.eq_ind_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2 - in - mk_trans uri_trans ty pred_of_other pred_of_what rhs - (inject ty lhs what other p2) p1 - | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs - -> - let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t rhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l) - (inject ty lhs m r pmr) - (inject ty lhs l m plm) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2) - in - mk_trans uri_trans ty lhs pred_of_what pred_of_other - p1 (inject ty rhs other what p2) - | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs - -> - let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in - let uri_trans = LibraryObjects.trans_eq_URI ~eq in - let pred_of t = CicSubstitution.subst t rhs in - let pred_of_what = pred_of what in - let pred_of_other = pred_of other in - (* p2 : what = other - * ==================================== - * inject p2: P(what) = P(other) - *) - let rec inject ty lhs what other p2 = - match p2 with - | Cic.Appl ((Cic.Const(uri_trans,ens))::tl) - when LibraryObjects.is_trans_eq_URI uri_trans -> - let ty,l,m,r,plm,pmr = open_trans ens tl in - (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r) - (inject ty lhs m l plm) - (inject ty lhs r m pmr)) - | _ -> - let liftedty = CicSubstitution.lift 1 ty in - let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in - let refl_eq_part = - Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other] - in - mk_eq_ind (Utils.eq_ind_URI ()) ty other - (Cic.Lambda (Cic.Name "foo",ty, - (Cic.Appl - [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs]))) - refl_eq_part what p2 - in - mk_trans uri_trans ty lhs pred_of_what pred_of_other - p1 (inject ty rhs other what p2) -*) - | _, Utils.Left -> + match pos with + | Utils.Left -> mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2 - | _, Utils.Right -> + | Utils.Right -> mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2 ;; -let build_proof_term_new proof = +let build_proof_term proof = let rec aux = function | Exact term -> term | Step (subst,(_, id1, (pos,id2), pred)) -> @@ -741,7 +446,7 @@ let wfo goalproof proof = let string_of_id names id = try - let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in + let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in match p with | Exact t -> Printf.sprintf "%d = %s: %s = %s" id @@ -760,17 +465,17 @@ let pp_proof names goalproof proof = ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof))) ;; -let build_goal_proof l initial = +let build_goal_proof l initial ty = let proof = List.fold_left (fun current_proof (pos,id,subst,pred) -> let p,l,r = proof_of_id id in - let p = build_proof_term_new p in + let p = build_proof_term p in let pos = if pos = Utils.Left then Utils.Right else Utils.Left in build_proof_step subst current_proof p pos l r pred) initial l in - canonical proof + canonical (contextualize_rewrites proof ty) ;; let refl_proof ty term = @@ -780,7 +485,9 @@ let refl_proof ty term = ty; term] ;; -let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;; +let metas_of_proof p = + Utils.metas_of_term (build_proof_term p) +;; let relocate newmeta menv = let subst, metasenv, newmeta = @@ -789,49 +496,33 @@ let relocate newmeta menv = let irl = [] (* CicMkImplicit.identity_relocation_list_for_metavariable context *) in - let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in + let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in let newmeta = maxmeta, context, ty in newsubst, newmeta::menv, maxmeta+1) - menv ([], [], newmeta+1) + menv (Subst.empty_subst, [], newmeta+1) in - let metasenv = apply_subst_metasenv subst metasenv in - let subst = flatten_subst subst in + let metasenv = Subst.apply_subst_metasenv subst metasenv in + let subst = 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 + let w, p, (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 ty = Subst.apply_subst subst ty in + let left = Subst.apply_subst subst left in + let right = Subst.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) + | Exact p -> Exact (Subst.apply_subst subst p) | Step (s,(r,id1,(pos,id2),pred)) -> - Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred)) + Step (Subst.concat_substs s subst,(r,id1,(pos,id2), 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 + let p = fix_proof p in + let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in (* debug prerr_endline (string_of_equality eq); *) newmeta+1, eq @@ -979,7 +670,7 @@ let equality_of_term proof term = 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 + let e = mk_equality (w, Exact proof, stat,[]) in e | _ -> raise TermIsNotAnEquality diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index 1a2a3a280..d2c58041d 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -23,45 +23,17 @@ * http://helm.cs.unibo.it/ *) -type substitution - -type rule = SuperpositionRight | SuperpositionLeft |Demodulation +type rule = SuperpositionRight | SuperpositionLeft | Demodulation type equality -and proof = new_proof * old_proof - -and new_proof = +and 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 + | Step of Subst.substitution * (rule * int * (Utils.pos * int) * Cic.term) -and goal_proof = (Utils.pos * int * substitution * Cic.term) list +and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list -val pp_proof: (Cic.name option) list -> goal_proof -> new_proof -> string - -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 pp_proof: (Cic.name option) list -> goal_proof -> proof -> string val reset : unit -> unit @@ -80,14 +52,15 @@ val open_equality : int * proof * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv * int +val depend : equality -> int -> bool 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 -val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term -val build_goal_proof: goal_proof -> Cic.term -> Cic.term +val string_of_proof : + ?names:(Cic.name option)list -> proof -> goal_proof -> string +val build_proof_term: proof -> Cic.term +(* build_goal_proof [goal_proof] [initial_proof] [ty] + * [ty] is the type of the goal *) +val build_goal_proof: goal_proof -> Cic.term -> Cic.term-> Cic.term val refl_proof: Cic.term -> Cic.term -> Cic.term (** ensures that metavariables in equality are unique *) val fix_metas: int -> equality -> int * equality @@ -116,4 +89,3 @@ 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/indexing.ml b/components/tactics/paramodulation/indexing.ml index 4ac1c94e2..e3ef59d9b 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -93,7 +93,7 @@ let print_candidates ?env mode term res = let indexing_retrieval_time = ref 0.;; -let apply_subst = Equality.apply_subst +let apply_subst = Subst.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,_,_) -> (Equality.is_in_subst i subst)) metasenv) + (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv) then begin prerr_endline ("not disjoint: " ^ msg); @@ -250,7 +250,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty = 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" + (CicPp.ppterm(Equality.build_proof_term proof))^"\n" in check_for_duplicates metas "gia nella metas"; check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p) @@ -445,7 +445,7 @@ let subsumption env table target = match_unif_time_no := !match_unif_time_no +. (t2 -. t1); raise e in - (match Equality.merge_subst_if_possible subst subst' with + (match Subst.merge_subst_if_possible subst subst' with | None -> ok what tl | Some s -> Some (s, equation)) with Inference.MatchingFailure -> @@ -593,9 +593,9 @@ 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_new, proof_old) (*as proof*)), - (eq_ty, left, right, order), metas, id = - Equality.open_equality target in + let w, 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 *) @@ -615,11 +615,11 @@ 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 = Equality.ppsubst subst in + let substs = Subst.ppsubst subst in ignore(check_target context (snd eq_found) ("input3" ^ substs)) end; let pos, equality = eq_found in - let (_, (proof'_new,proof'_old), + let (_, proof', (ty, what, other, _), menv',id') = Equality.open_equality equality in let ty = try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) @@ -638,12 +638,8 @@ let rec demodulation_equality ?from newmeta env table sign target = S.lift 1 eq_ty; l; r] in if sign = Utils.Positive then - (bo, - (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))) + (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'), + (Cic.Lambda (name, ty, bo')))))) else assert false (* @@ -707,17 +703,17 @@ let rec demodulation_equality ?from newmeta env table sign target = if Utils.debug_metas then try ignore(CicTypeChecker.type_of_aux' newmenv context - (Equality.build_proof_term_old (snd newproof)) ugraph); + (Equality.build_proof_term newproof) ugraph); () with exc -> prerr_endline "sempre lui"; - prerr_endline (Equality.ppsubst subst); + prerr_endline (Subst.ppsubst subst); prerr_endline (CicPp.ppterm - (Equality.build_proof_term_old (snd newproof))); + (Equality.build_proof_term newproof)); prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t)); prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what)); prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other)); - prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst)); + prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst)); prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv [] newmenv)); raise exc; @@ -1027,7 +1023,7 @@ 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, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id = + let w, eqproof, (eq_ty, left, right, ordering), newmetas,id = Equality.open_equality target in if Utils.debug_metas then @@ -1079,11 +1075,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = S.lift 1 eq_ty; l; r] in bo', - (Equality.Step - (s,(Equality.SuperpositionRight, - id,(pos,id'),(Cic.Lambda(name,ty,bo'')))), - Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2)) - + Equality.Step + (s,(Equality.SuperpositionRight, + id,(pos,id'),(Cic.Lambda(name,ty,bo'')))) in let newmeta, newequality = let left, right = @@ -1125,78 +1119,32 @@ 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 (cicproof,proof), metas, term = goal in + let goalproof, metas, term = goal in let term = Utils.guarded_simpl (~debug:true) context term in - let goal = (cicproof,proof), metas, term in + let goal = goalproof, metas, term in let metasenv' = metas in let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) = let pos, equality = eq_found in - let (_, (proofnew',proof'), (ty, what, other, _), menv',id) = + 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 ty = try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph) with CicUtil.Meta_not_found _ -> ty in - let newterm, newproof, newcicproof = + let newterm, newgoalproof = 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 bo' = (*apply_subst subst*) t in let name = C.Name "x" in incr demod_counter; - let metaproof = - incr maxmeta; - 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 eq_found_proof = - let termlist = - if pos = Utils.Left then [ty; what; other] - else [ty; other; what] - in - Equality.ProofSymBlock (termlist, proof') - in - let what, other = - if pos = Utils.Left then what, other else other, what - in - pos, - Equality.mk_equality - (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv') - in - let goal_proof = - let pb = - Equality.ProofBlock - (subst, eq_URI, (name, ty), bo', - eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) - in - let rec repl = function - | Equality.NoProof -> -(* debug_print (lazy "replacing a NoProof"); *) - pb - | Equality.BasicProof _ -> -(* debug_print (lazy "replacing a BasicProof"); *) - pb - | Equality.ProofGoalBlock (_, parent_proof) -> -(* debug_print (lazy "replacing another ProofGoalBlock"); *) - Equality.ProofGoalBlock (pb, parent_proof) - | Equality.SubProof (term, meta_index, p) -> - prerr_endline "subproof!"; - Equality.SubProof (term, meta_index, repl p) - | _ -> assert false - in repl proof - in - let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in - bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof), - (newcicproofstep::cicproof) + let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in + bo, (newgoalproofstep::goalproof) in let newmetasenv = (* Inference.filter subst *) menv in - !maxmeta, ((newcicproof,newproof), newmetasenv, newterm) + !maxmeta, (newgoalproof, newmetasenv, newterm) in let res = demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term @@ -1234,14 +1182,18 @@ let rec demodulation_theorem newmeta env table theorem = let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newty = let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in - let bo' = apply_subst subst t in - let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in +(* let bo' = apply_subst subst t in *) +(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*) incr demod_counter; +(* let newproofold = Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, Equality.BasicProof (Equality.empty_subst,term)) in (Equality.build_proof_term_old newproofold, bo) +*) + (* TODO, not ported to the new proofs *) + if true then assert false; term, bo in !maxmeta, (newterm, newty, menv) in diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli index 1c6102a07..8af265f90 100644 --- a/components/tactics/paramodulation/indexing.mli +++ b/components/tactics/paramodulation/indexing.mli @@ -47,7 +47,7 @@ val subsumption : Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> Equality.equality -> - (Equality.substitution * Equality.equality) option + (Subst.substitution * Equality.equality) option val superposition_left : int -> Cic.conjecture list * Cic.context * CicUniv.universe_graph -> @@ -72,9 +72,9 @@ val demodulation_goal : int -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> - (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key -> + Equality.goal_proof * Cic.metasenv * Index.key -> bool * int * - ((Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key) + (Equality.goal_proof * Cic.metasenv * Index.key) val demodulation_theorem : 'a -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index f088d5454..272a81003 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -30,7 +30,7 @@ open Printf;; let check_disjoint_invariant subst metasenv msg = if (List.exists - (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv) + (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv) then begin prerr_endline ("not disjoint: " ^ msg); @@ -65,7 +65,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = let module C = Cic in let module M = CicMetaSubst in let module U = CicUnification in - let lookup = Equality.lookup_subst in + let lookup = Subst.lookup_subst in let rec occurs_check subst what where = match where with | t when what = t -> true @@ -99,8 +99,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in - assert (not (Equality.is_in_subst i subst)); - let subst = Equality.buildsubst i context t ty subst in + assert (not (Subst.is_in_subst i subst)); + let subst = Subst.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 -> @@ -126,8 +126,8 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph = | _, _ -> raise (U.UnificationFailure (lazy "Inference.unification.unif")) in - let subst, menv = unif Equality.empty_subst metasenv t1 t2 in - let menv = Equality.filter subst menv in + let subst, menv = unif Subst.empty_subst metasenv t1 t2 in + let menv = Subst.filter subst menv in subst, menv, ugraph ;; @@ -234,10 +234,7 @@ 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_old = - Equality.BasicProof (Equality.empty_subst,p) in - let proof_new = Equality.Exact p in - let proof = proof_new , proof_old in + let proof = Equality.Exact p in let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta @@ -251,9 +248,7 @@ let find_equalities context proof = let stat = (ty,t1,t2,o) in let w = compute_equality_weight 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 proof = Equality.Exact p in let e = Equality.mk_equality (w, proof,stat,[]) in Some e, (newmeta+1) | _ -> None, newmeta @@ -391,10 +386,7 @@ 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 proof_old = - Equality.BasicProof (Equality.empty_subst,p) in - let proof_new = Equality.Exact p in - let proof = proof_new, proof_old in + let proof = Equality.Exact p in let e = Equality.mk_equality (w, proof, stat, newmetas) in Some e, (newmeta+1) | _ -> None, newmeta @@ -404,9 +396,7 @@ 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 old_proof = Equality.BasicProof (Equality.empty_subst,term) in - let new_proof = Equality.Exact term in - let proof = new_proof, old_proof in + let proof = Equality.Exact term in let e = Equality.mk_equality (w, proof, stat, []) in Some e, (newmeta+1) | _ -> None, newmeta diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli index 08d1c8f26..9bfb84cb2 100644 --- a/components/tactics/paramodulation/inference.mli +++ b/components/tactics/paramodulation/inference.mli @@ -30,7 +30,7 @@ val matching: Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> - Equality.substitution * Cic.metasenv * CicUniv.universe_graph + Subst.substitution * Cic.metasenv * CicUniv.universe_graph (** special unification that checks if the two terms are "simple", and in @@ -40,7 +40,7 @@ val unification: Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> - Equality.substitution * Cic.metasenv * CicUniv.universe_graph + Subst.substitution * Cic.metasenv * CicUniv.universe_graph (** diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 6b1b65e27..f8c20d0e3 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -71,14 +71,13 @@ 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 + Equality.goal_proof * Equality.proof * Subst.substitution * Cic.metasenv type result = | ParamodulationFailure - | ParamodulationSuccess of (new_proof * old_proof) option + | ParamodulationSuccess of new_proof option ;; -type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;; +type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; @@ -153,12 +152,22 @@ let rec select env goals passive = match !weight_age_counter with | 0 -> ( weight_age_counter := !weight_age_ratio; - match pos_list with - | (hd:EqualitySet.elt)::tl -> - let passive_table = - Indexing.remove_index passive_table hd - in hd, ((tl, EqualitySet.remove hd pos_set), passive_table) - | _ -> assert false) + let rec skip_giant pos_list pos_set passive_table = + match pos_list with + | (hd:EqualitySet.elt)::tl -> + let w,_,_,_,_ = Equality.open_equality hd in + let passive_table = + Indexing.remove_index passive_table hd + in + let pos_set = EqualitySet.remove hd pos_set in + if w < 50 then + hd, ((tl, pos_set), passive_table) + else + (prerr_endline ("\n\n\nGIANT SKIPPED: "^string_of_int w^"\n\n\n"); + skip_giant tl pos_set passive_table) + | _ -> assert false + in + skip_giant pos_list pos_set passive_table) | _ when (!symbols_counter > 0) -> (symbols_counter := !symbols_counter - 1; let cardinality map = @@ -211,6 +220,27 @@ let rec select env goals passive = passive_table) ;; +let filter_dependent passive id = + prerr_endline ("+++++++++++++++passives "^ + ( string_of_int (size_of_passive passive))); + let (pos_list, pos_set), passive_table = passive in + let passive = + List.fold_right + (fun eq ((list,set),table) -> + if Equality.depend eq id then + (let _,_,_,_,id_eq = Equality.open_equality eq in + if id_eq = 9228 then + prerr_endline ("\n\n--------filtering "^(string_of_int id_eq)); + ((list, + EqualitySet.remove eq set), + Indexing.remove_index table eq)) + else ((eq::list, set),table)) + pos_list (([],pos_set),passive_table) in + prerr_endline ("+++++++++++++++passives "^ + ( string_of_int (size_of_passive passive))); + passive +;; + (* initializes the passive set of equalities *) let make_passive pos = @@ -374,18 +404,35 @@ let check_for_deep_subsumption env active_table eq = match t1,t2 with | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used | t1, t2 when subsumption_used -> t1 = t2, subsumption_used +(* VERSIONE ERRATA | Cic.Appl (h1::l),Cic.Appl (h2::l') when h1 = h2 -> let rc = check_subsumed b t1 t1 in if rc then true, true + else if h1 = h2 then + (try + List.fold_left2 + (fun (ok_so_far, subsumption_used) t t' -> + aux true (ok_so_far, subsumption_used) t t') + (ok_so_far, subsumption_used) l l' + with Invalid_argument _ -> false,subsumption_used) else + false, subsumption_used + | _ -> false, subsumption_used *) + | Cic.Appl (h1::l),Cic.Appl (h2::l') -> + let rc = check_subsumed b t1 t2 in + if rc then + true, true + else if h1 = h2 then (try List.fold_left2 (fun (ok_so_far, subsumption_used) t t' -> aux true (ok_so_far, subsumption_used) t t') (ok_so_far, subsumption_used) l l' with Invalid_argument _ -> false,subsumption_used) - | _ -> false, subsumption_used + else + false, subsumption_used + | _ -> false, subsumption_used in fst (aux false (true,false) left right) ;; @@ -481,7 +528,10 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) = (* if Indexing.subsumption env active_table c = None then*) (match Indexing.subsumption env passive_table c with | None -> res - | Some (_,c') -> None (*Some c'*)) + | Some (_,c') -> + None + (*prerr_endline "\n\nPESCO DALLE PASSIVE LA PIU' GENERALE\n\n"; + Some c'*)) (* else None @@ -643,26 +693,31 @@ let backward_simplify_active env new_pos new_table min_weight active = let find eq1 where = List.exists (Equality.meta_convertibility_eq eq1) where in - let active, newa = + let id_of_eq eq = + let _, _, _, _,id = Equality.open_equality eq in id + in + let ((active1,pruned),tbl), newa = List.fold_right - (fun eq (res, tbl) -> + (fun eq ((res,pruned), tbl) -> if List.mem eq res then - res, tbl + (res, (id_of_eq eq)::pruned),tbl else if (Equality.is_identity env eq) || (find eq res) then ( - res, tbl + (res, (id_of_eq eq)::pruned),tbl ) else - eq::res, Indexing.index tbl eq) - active_list ([], Indexing.empty), + (eq::res,pruned), Indexing.index tbl eq) + active_list (([],pruned), Indexing.empty), List.fold_right (fun eq p -> if (Equality.is_identity env eq) then p else eq::p) newa [] in + if List.length active1 <> List.length (fst active) then + prerr_endline "\n\n\nMANCAVANO DELLE PRUNED!!!!\n\n\n"; match newa with - | [] -> active, None - | _ -> active, Some newa + | [] -> (active1,tbl), None, pruned + | _ -> (active1,tbl), Some newa, pruned ;; @@ -712,13 +767,13 @@ let backward_simplify env new' ?passive active = ([], Indexing.empty, 1000000) new' in *) - let active, newa = + let active, newa, pruned = backward_simplify_active env new_pos new_table min_weight active in match passive with | None -> - active, (make_passive []), newa, None + active, (make_passive []), newa, None, pruned | Some passive -> - active, passive, newa, None + active, passive, newa, None, pruned (* prova let passive, newp = backward_simplify_passive env new_pos new_table min_weight passive in @@ -896,48 +951,21 @@ let print_goals goals = Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) ;; -let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table = +let check_if_goal_is_subsumed env (goalproof,menv,ty) table = prerr_endline "check_goal_subsumed"; match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when UriManager.eq uri (LibraryObjects.eq_URI ()) -> (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 - prerr_endline "1"; - let p = Equality.apply_subst subst - (Equality.build_proof_term_old p) in - prerr_endline "2"; - 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 - prerr_endline "3"; - let newcicp,np,subst,cicmenv = - cicproof,np, subst, - Equality.apply_subst_metasenv subst (m @ menv) - in - prerr_endline "."; - Some - ((newcicp,np,subst,cicmenv), - (newp, Equality.apply_subst_metasenv subst m @ menv )) - | None -> None) + (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) + in + match Indexing.subsumption env table goal_equation with + | Some (subst, equality ) -> + let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in + let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in + Some (goalproof, p, subst, cicmenv) + | None -> None) | _ -> None ;; @@ -969,35 +997,12 @@ let rec given_clause_fullred dbd env goals theorems ~passive active = (* apply_goal_to_theorems dbd env theorems ~passive active goals in *) let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in match (fst goals) with - | (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ + | (_,[goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_ when left = right && iseq uri -> - let p = - Cic.Appl [Cic.MutConstruct (* reflexivity *) - (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left] - 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 (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 + let reflproof = Equality.Exact (Equality.refl_proof eq_ty left) in + true, Some (goalproof, reflproof, Subst.empty_subst,m) + | (_, [goal])::_ -> + (match check_if_goal_is_subsumed env goal (snd active) with | None -> false,None | Some p -> prerr_endline "Proof found by subsumption!"; @@ -1159,8 +1164,10 @@ and given_clause_fullred_aux dbd env goals theorems passive active = forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1); let t1 = Unix.gettimeofday () in - let active, passive, newa, retained = + let active, passive, newa, retained, pruned = backward_simplify env new' ~passive active in + let passive = + List.fold_left filter_dependent passive pruned in let t2 = Unix.gettimeofday () in backward_simpl_time := !backward_simpl_time +. (t2 -. t1); match newa, retained with @@ -1177,7 +1184,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | Some p, Some rp -> simplify (new' @ p @ rp) active passive in - let active, _, new' = simplify new' active passive in + let active, passive, new' = simplify new' active passive in let goals = let a,b,_ = build_table new' in simplify_goals env goals ~passive (a,b) @@ -1258,8 +1265,10 @@ let rec saturate_equations env goal accept_fun passive active = in let rec simplify new' active passive = let new' = forward_simplify_new env new' ~passive active in - let active, passive, newa, retained = + let active, passive, newa, retained, pruned = backward_simplify env new' ~passive active in + let passive = + List.fold_left filter_dependent passive pruned in match newa, retained with | None, None -> active, passive, new' | Some p, None @@ -1504,9 +1513,7 @@ let saturate in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in - let goal = - ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal - in + let goal = [], [], goal in let res, time = let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = @@ -1563,9 +1570,7 @@ let saturate in match res with | ParamodulationSuccess - (Some - ((goalproof,newproof,subsumption_subst, newproof_menv), (* NEW *) - (proof, proof_menv))) (* OLD *) + (Some (goalproof,newproof,subsumption_subst, proof_menv)) -> prerr_endline "OK, found a proof!"; @@ -1574,16 +1579,13 @@ let saturate * goalproof);*) prerr_endline (Equality.pp_proof names goalproof newproof); - (* generation of the old proof *) - let cic_proof = Equality.build_proof_term_old proof in - - (* generation of the new proof *) + (* generation of the proof *) let cic_proof_new = Equality.build_goal_proof - goalproof (Equality.build_proof_term_new newproof) + goalproof (Equality.build_proof_term newproof) type_of_goal in let cic_proof_new = - Equality.apply_subst subsumption_subst cic_proof_new + Subst.apply_subst subsumption_subst cic_proof_new in (* replacing fake mets with real ones *) @@ -1593,21 +1595,6 @@ let saturate | _ -> false in let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in - prerr_endline "replacing metas (old)"; - let proof_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) - ([],[],[]) proof_menv - in - 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 @@ -1616,7 +1603,7 @@ let saturate (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl)) ::acc3) - ([],[],[]) newproof_menv + ([],[],[]) proof_menv in let cic_proof_new = ProofEngineReduction.replace_lifting ~equality:(=) @@ -1625,10 +1612,6 @@ let saturate in (* pp new/old proof *) -(* prerr_endline "OLDPROOF";*) -(* prerr_endline (Equality.string_of_proof_old proof);*) -(* prerr_endline "OLDPROOFCIC";*) -(* prerr_endline (CicPp.pp cic_proof names); *) (* prerr_endline "NEWPROOFCIC";*) (* prerr_endline (CicPp.pp cic_proof_new names); *) @@ -1641,20 +1624,9 @@ let saturate List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv in let newmetasenv_new = newmetasenv@newproof_menv in - let newmetasenv = newmetasenv@proof_menv in (* check/refine/... build the new proof *) let newstatus = let cic_proof,newmetasenv,proof_menv,ty, ug = - prerr_endline "type checking ... (old) "; - let _old_ty, _oldug = - try - CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph - with - CicTypeChecker.TypeCheckerFailure s -> - prerr_endline "THE *OLD* PROOF DOESN'T TYPECHECK!!!"; - prerr_endline (Lazy.force s); - Cic.Implicit None, CicUniv.empty_ugraph - in let cic_proof_new,new_ty,newmetasenv_new,newug = try (* @@ -1869,8 +1841,7 @@ let main_demod_equalities dbd term metasenv ugraph = in let env = (metasenv, context, ugraph) in (*try*) - let goal = - ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal + let goal = [], [], goal in let equalities = simplify_equalities env (equalities@library_equalities) in let active = make_active () in @@ -1930,10 +1901,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = if library_equalities = [] then prerr_endline "VUOTA!!!"; 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 = - ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty - in + let initgoal = [], [], ty in let env = (metasenv, context, CicUniv.empty_ugraph) in let equalities = simplify_equalities env (equalities@library_equalities) in let table = @@ -1949,7 +1917,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = begin let opengoal = Cic.Meta(maxm,irl) in let proofterm = - Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in + Equality.build_goal_proof newproof opengoal ty 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/subst.ml b/components/tactics/paramodulation/subst.ml new file mode 100644 index 000000000..f738d2f63 --- /dev/null +++ b/components/tactics/paramodulation/subst.ml @@ -0,0 +1,215 @@ +(* 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 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 = [];; + +let concat_substs x y = x @ y;; + diff --git a/components/tactics/paramodulation/subst.mli b/components/tactics/paramodulation/subst.mli new file mode 100644 index 000000000..3bbf7d00c --- /dev/null +++ b/components/tactics/paramodulation/subst.mli @@ -0,0 +1,43 @@ +(* 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 + +val empty_subst : substitution +val apply_subst : substitution -> Cic.term -> Cic.term +val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv +val ppsubst : ?names:(Cic.name option list) -> 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 concat_substs: substitution -> substitution -> substitution + -- 2.39.2