From 97e59118f8cc0d98c51c0d41e8e7704344666cdb Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 20 Sep 2011 14:00:34 +0000 Subject: [PATCH] The Blob is not abstracted on the context any more. The saturate function (that requires the environment now contained in the status) is now external to the module. It is defined in NCicBlob. The functions mk_passive and mk_goals are now expecting input terms already saturated. --- .../components/ng_paramodulation/nCicBlob.ml | 41 +++++++---------- .../components/ng_paramodulation/nCicBlob.mli | 9 +++- .../ng_paramodulation/nCicParamod.ml | 45 ++++++++----------- .../ng_paramodulation/nCicParamod.mli | 10 ++++- .../components/ng_paramodulation/nCicProof.ml | 11 +---- .../components/ng_paramodulation/paramod.ml | 11 ++--- .../components/ng_paramodulation/paramod.mli | 1 + matitaB/components/ng_paramodulation/terms.ml | 2 +- .../components/ng_paramodulation/terms.mli | 2 +- matitaB/components/ng_tactics/nnAuto.ml | 2 +- 10 files changed, 62 insertions(+), 72 deletions(-) diff --git a/matitaB/components/ng_paramodulation/nCicBlob.ml b/matitaB/components/ng_paramodulation/nCicBlob.ml index cd944c43d..beef0ae45 100644 --- a/matitaB/components/ng_paramodulation/nCicBlob.ml +++ b/matitaB/components/ng_paramodulation/nCicBlob.ml @@ -33,14 +33,20 @@ let setoid_eq = let set_default_eqP() = eqPref := default_eqP -module type NCicContext = - sig - val metasenv : NCic.metasenv - val subst : NCic.substitution - val context : NCic.context - end - -module NCicBlob(C : NCicContext) : Terms.Blob +let saturate status metasenv subst context t ty = + let sty, _, args = + (* CSC: NCicPp.status is the best I can put here *) + NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0 + in + let proof = + if args = [] then t + else NCic.Appl (t :: args) + in + proof, sty +;; + + +module NCicBlob: Terms.Blob with type t = NCic.term and type input = NCic.term = struct type t = NCic.term @@ -100,9 +106,7 @@ with type t = NCic.term and type input = NCic.term = struct let pp t = (* CSC: NCicPp.status is the best I can put here *) - (* WR: and I can't guess a user id, so I must put None *) - (new NCicPp.status None)#ppterm ~context:C.context - ~metasenv:C.metasenv ~subst:C.subst t;; + (new NCicPp.status None)#ppterm ~context:[] ~metasenv:[] ~subst:[] t type input = NCic.term @@ -121,19 +125,4 @@ with type t = NCic.term and type input = NCic.term = struct let embed t = fst (embed t) ;; - let saturate t ty = - let sty, _, args = - (* CSC: NCicPp.status is the best I can put here *) - (* WR: and I can't guess a user id, so I must put None *) - NCicMetaSubst.saturate (new NCicPp.status None) ~delta:0 C.metasenv C.subst - C.context ty 0 - in - let proof = - if args = [] then Terms.Leaf t - else Terms.Node (Terms.Leaf t :: List.map embed args) - in - let sty = embed sty in - proof, sty - ;; - end diff --git a/matitaB/components/ng_paramodulation/nCicBlob.mli b/matitaB/components/ng_paramodulation/nCicBlob.mli index 5d0c7ae2b..6adb20421 100644 --- a/matitaB/components/ng_paramodulation/nCicBlob.mli +++ b/matitaB/components/ng_paramodulation/nCicBlob.mli @@ -13,14 +13,21 @@ val set_eqP: NCic.term -> unit val set_default_eqP: unit -> unit +val saturate: + #NCicEnvironment.status -> + NCic.metasenv -> + NCic.substitution -> + NCic.context -> NCic.term -> NCic.term -> NCic.term * NCic.term +(* module type NCicContext = sig val metasenv : NCic.metasenv val subst : NCic.substitution val context : NCic.context end +*) -module NCicBlob(C : NCicContext) : Terms.Blob +module NCicBlob: Terms.Blob with type t = NCic.term and type input = NCic.term diff --git a/matitaB/components/ng_paramodulation/nCicParamod.ml b/matitaB/components/ng_paramodulation/nCicParamod.ml index 6e91b9028..0f92c6620 100644 --- a/matitaB/components/ng_paramodulation/nCicParamod.ml +++ b/matitaB/components/ng_paramodulation/nCicParamod.ml @@ -20,11 +20,11 @@ let noprint _ = ();; let print s = prerr_endline (Lazy.force s);; let debug = noprint;; -module B(C : NCicBlob.NCicContext): Orderings.Blob +module B : Orderings.Blob with type t = NCic.term and type input = NCic.term - = Orderings.LPO(NCicBlob.NCicBlob(C)) + = Orderings.LPO(NCicBlob.NCicBlob) -module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C)) +module NCicParamod = Paramod.Paramod(B) let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) = (* @@ -64,22 +64,18 @@ let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) = proofterm, prooftype, metasenv, subst let nparamod status metasenv subst context t table = - let module C = - struct - let metasenv = metasenv - let subst = subst - let context = context - end - in - let module B = B(C) in - let module P = NCicParamod(C) in + let module P = NCicParamod in let module Pp = Pp.Pp(B) in let bag, maxvar = Terms.empty_bag, 0 in + let saturate (t,ty) = + NCicBlob.saturate status metasenv subst context t ty in let (bag,maxvar), goals = - HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t] + HExtlib.list_mapi_acc + (fun x _ a -> P.mk_goal a (saturate x)) (bag,maxvar) [t] in - let (bag,maxvar), passives = - HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table + let (bag,maxvar), passives = + HExtlib.list_mapi_acc + (fun x _ a -> P.mk_passive a (saturate x)) (bag,maxvar) table in match P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) @@ -90,21 +86,16 @@ let nparamod status metasenv subst context t table = List.map (readback status metasenv subst context) solutions ;; -module EmptyC = - struct - let metasenv = [] - let subst = [] - let context = [] - end - -module CB = NCicBlob.NCicBlob(EmptyC) -module P = NCicParamod(EmptyC) +module CB = NCicBlob.NCicBlob +module P = NCicParamod type state = P.state let empty_state = P.empty_state -let forward_infer_step s t ty = +let forward_infer_step status metasenv subst context s t ty = let bag = P.bag_of_state s in + let saturate (t,ty) = + NCicBlob.saturate status metasenv subst context t ty in let bag,clause = P.mk_passive bag (t,ty) in if Terms.is_eq_clause clause then P.forward_infer_step (P.replace_bag s bag) clause 0 @@ -118,10 +109,10 @@ let index_obj status s uri = match obj with | (_,_,[],[],NCic.Constant(_,_,None,ty,_)) -> let nref = NReference.reference_of_spec uri NReference.Decl in - forward_infer_step s (NCic.Const nref) ty + forward_infer_step status [] [] [] s (NCic.Const nref) ty | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) -> let nref = NReference.reference_of_spec uri (NReference.Def d) in - forward_infer_step s (NCic.Const nref) ty + forward_infer_step status [] [] [] s (NCic.Const nref) ty | _ -> s ;; diff --git a/matitaB/components/ng_paramodulation/nCicParamod.mli b/matitaB/components/ng_paramodulation/nCicParamod.mli index 2856ebac9..b46d0ade0 100644 --- a/matitaB/components/ng_paramodulation/nCicParamod.mli +++ b/matitaB/components/ng_paramodulation/nCicParamod.mli @@ -19,7 +19,15 @@ val nparamod : type state val empty_state: state -val forward_infer_step: state -> NCic.term -> NCic.term -> state +val forward_infer_step: + #NCicCoercion.status -> + NCic.metasenv -> + NCic.substitution -> + NCic.context -> + state -> + NCic.term -> + NCic.term -> + state val index_obj: #NCicEnvironment.status -> state -> NUri.uri -> state val is_equation: #NCicEnvironment.status -> NCic.metasenv -> NCic.substitution -> NCic.context -> diff --git a/matitaB/components/ng_paramodulation/nCicProof.ml b/matitaB/components/ng_paramodulation/nCicProof.ml index cabca8259..50c25315f 100644 --- a/matitaB/components/ng_paramodulation/nCicProof.ml +++ b/matitaB/components/ng_paramodulation/nCicProof.ml @@ -73,11 +73,7 @@ let debug c _ = c;; match t with | Terms.Leaf _ | Terms.Var _ -> - let module NCicBlob = NCicBlob.NCicBlob( - struct - let metasenv = [] let subst = [] let context = [] - end) - in + let module NCicBlob = NCicBlob.NCicBlob in let module Pp = Pp.Pp(NCicBlob) in prerr_endline ("term: " ^ Pp.pp_foterm ft); prerr_endline ("path: " ^ String.concat "," @@ -194,10 +190,7 @@ let debug c _ = c;; let mk_proof status ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps= let module NCicBlob = - NCicBlob.NCicBlob( - struct - let metasenv = [] let subst = [] let context = [] - end) + NCicBlob.NCicBlob in let module Pp = Pp.Pp(NCicBlob) in diff --git a/matitaB/components/ng_paramodulation/paramod.ml b/matitaB/components/ng_paramodulation/paramod.ml index 86a964c14..33f802f7f 100644 --- a/matitaB/components/ng_paramodulation/paramod.ml +++ b/matitaB/components/ng_paramodulation/paramod.ml @@ -208,16 +208,17 @@ module Paramod (B : Orderings.Blob) = struct (bag, maxvar), c ;; - let mk_clause bag maxvar (t,ty) = - let (proof,ty) = B.saturate t ty in +(* + let mk_clause bag maxvar (proof,ty) = + let (proof,ty) = B.saturate t ty in let c, maxvar = Utils.mk_unit_clause maxvar ty proof in let bag, c = Terms.add_to_bag c bag in (bag, maxvar), c - ;; + ;; *) - let mk_passive (bag,maxvar) = mk_clause bag maxvar;; + let mk_passive (bag,maxvar) = mk_unit_clause bag maxvar;; - let mk_goal (bag,maxvar) = mk_clause bag maxvar;; + let mk_goal (bag,maxvar) = mk_unit_clause bag maxvar;; let initialize_goal (bag,maxvar,actives,passives,_,_) t = let (bag,maxvar), g = mk_unit_clause bag maxvar t in diff --git a/matitaB/components/ng_paramodulation/paramod.mli b/matitaB/components/ng_paramodulation/paramod.mli index 367d79394..60691a57c 100644 --- a/matitaB/components/ng_paramodulation/paramod.mli +++ b/matitaB/components/ng_paramodulation/paramod.mli @@ -26,6 +26,7 @@ module type Paramod = val empty_state : state val bag_of_state :state -> bag val replace_bag : state -> bag -> state + (* we suppose input has been already saturated *) val mk_passive : bag -> input * input -> bag * t Terms.unit_clause val mk_goal : bag -> input * input -> bag * t Terms.unit_clause val forward_infer_step : diff --git a/matitaB/components/ng_paramodulation/terms.ml b/matitaB/components/ng_paramodulation/terms.ml index 87b4f383b..e0fcad181 100644 --- a/matitaB/components/ng_paramodulation/terms.ml +++ b/matitaB/components/ng_paramodulation/terms.ml @@ -100,6 +100,6 @@ module type Blob = val pp : t -> string type input val embed : input -> t foterm - val saturate : input -> input -> t foterm * t foterm +(* val saturate : input -> input -> t foterm * t foterm *) end diff --git a/matitaB/components/ng_paramodulation/terms.mli b/matitaB/components/ng_paramodulation/terms.mli index 93f106a4f..020eefecd 100644 --- a/matitaB/components/ng_paramodulation/terms.mli +++ b/matitaB/components/ng_paramodulation/terms.mli @@ -93,7 +93,7 @@ module type Blob = type input val embed : input -> t foterm (* saturate [proof] [type] -> [proof] * [type] *) - val saturate : input -> input -> t foterm * t foterm + (* val saturate : input -> input -> t foterm * t foterm *) end diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml index f3cd17caf..387e644b0 100644 --- a/matitaB/components/ng_tactics/nnAuto.ml +++ b/matitaB/components/ng_tactics/nnAuto.ml @@ -302,7 +302,7 @@ let index_local_equations eq_cache status = let ty = NCicTypeChecker.typeof status [] [] ctx t in if is_a_fact status (mk_cic_term ctx ty) then (debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty))); - NCicParamod.forward_infer_step eq_cache t ty) + NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty) else (debug_print (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty))); eq_cache) -- 2.39.2