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.

diff --git a/matitaB/components/ng_paramodulation/nCicBlob.ml b/matitaB/components/ng_paramodulation/nCicBlob.ml
index cd944c43d5d63cdf9e013f8fc6f009dfec79569d..beef0ae453ba6ce55a80b1bd411b3603effb7630 100644 (file)
--- 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 5d0c7ae2ba0e5fad112522aa0ca3f6f1bffe864a..6adb2042160029ece1462c6a50ef9dd2ec7fcb81 100644 (file)
--- 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 6e91b902830a166b7963b3d21aced7f1664e421f..0f92c66209f08838469c5ded84e0284ad56b1005 100644 (file)
--- 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 2856ebac9e99a38474b67b11a2bed0fda98a38b1..b46d0ade0d0b650764322e8d73d2023f1e5a65de 100644 (file)
--- 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 cabca8259aefc524e89ed5b0e8e74f27049df70e..50c25315f91bd7ab1758892c857d6d7c6b854fde 100644 (file)
--- 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 86a964c1487f36a7f72deb0c8f2608f621ec2aac..33f802f7f036caf9152d65de93a4c3cabce55842 100644 (file)
--- 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 367d7939448f269ebedd755cb688cbc887155c9c..60691a57c0bd843bdbde2c114d5b8cb9147fb5a9 100644 (file)
--- 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 87b4f383bc53bf13885069592eaf896ad9f58a0e..e0fcad181d199f8d143373215b35fab67a2bf98e 100644 (file)
--- 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 93f106a4f1c9e8c8464a1582a13d6d0a4c79d6c8..020eefecdb74e58fc63ed4d5c96f157c6403febc 100644 (file)
--- 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 f3cd17caf1c05b5463f014d7f5d46cd463034754..387e644b0d61a574fac76c2b220a64fd465b7ebd 100644 (file)
--- 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)