From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 20 Sep 2011 14:00:34 +0000 (+0000)
Subject: The Blob is not abstracted on the context any more.
X-Git-Tag: make_still_working~2274
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=97e59118f8cc0d98c51c0d41e8e7704344666cdb

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 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)