From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 17 Jun 2009 11:47:59 +0000 (+0000)
Subject: Initial implementation of statuses using objects in place of nested records.
X-Git-Tag: make_still_working~3856
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;p=helm.git

Initial implementation of statuses using objects in place of nested records.
So nicer!

The only major problem is that the NCicLibrary functor does not return a
function #status as 'status -> 'status, but a function status -> status.
Thus I have to painfully wrap NCicLibrary.Realizer(...).require in NRstatus.


TO REMEMBER:
- every function that works on a data type that used to be put in the status
  (e.g. a db) must now work on a functional class with just two members
  (db and set_db). Moreover, every function in the module must work on the
  open variants of the class type, i.e. #status
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 6e6a5bc73..e0bcd031e 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -471,10 +471,7 @@ let coercion_moo_statement_of (uri,arity, saturations,_) =
    (HExtlib.dummy_floc, CicUtil.term_of_uri uri, false, arity, saturations)
 
 let basic_eval_unification_hint (t,n) status =
- let hstatus =
-  NCicUnifHint.add_user_provided_hint (status.NRstatus.uhint_db) t n
- in
-  { status with NRstatus.uhint_db = hstatus }
+ NCicUnifHint.add_user_provided_hint status t n
 ;;
 
 let inject_unification_hint =
@@ -491,11 +488,11 @@ let eval_unification_hint status t n =
  assert (metasenv=[]);
  let t = NCicUntrusted.apply_subst subst [] t in
  let status = GrafiteTypes.set_estatus estatus status in
- let rstatus =
-  basic_eval_unification_hint (t,n) (GrafiteTypes.get_rstatus status) in
- let status = GrafiteTypes.set_rstatus rstatus status in
- let dump = inject_unification_hint (t,n)::(GrafiteTypes.get_dump status) in
- let status = GrafiteTypes.set_dump dump status in
+ let dstatus =
+  basic_eval_unification_hint (t,n) (GrafiteTypes.get_dstatus status) in
+ let dump = inject_unification_hint (t,n)::dstatus#dump in
+ let dstatus = dstatus#set_dump dump in
+ let status = GrafiteTypes.set_dstatus dstatus status in
   status,`Old []
 ;;
 
@@ -748,11 +745,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
      in
      let status = eval_from_moo.efm_go status moopath in
-     let rstatus = GrafiteTypes.get_rstatus status in
-     let rstatus =
-      NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) rstatus
-     in
-     let status = GrafiteTypes.set_rstatus rstatus status in
+     let dstatus = GrafiteTypes.get_dstatus status in
+     let dstatus =
+       NRstatus.Serializer.require ~baseuri:(NUri.uri_of_string baseuri)
+        dstatus in
+     let status = GrafiteTypes.set_dstatus dstatus status in
 (* debug
      let lt_uri = UriManager.uri_of_string "cic:/matita/nat/orders/lt.con" in
      let nat_uri = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
@@ -830,17 +827,18 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
               in
               let obj = uri,height,[],[],obj_kind in
                NCicTypeChecker.typecheck_obj obj;
-               let timestamp = NCicLibrary.add_obj uri obj in
+               let dstatus = estatus.NEstatus.rstatus in
+               let dstatus = NCicLibrary.add_obj dstatus uri obj in
                let objs = NCicElim.mk_elims obj in
                let timestamp,uris_rev =
                  List.fold_left
-                  (fun (timestamp,uris_rev) (uri,_,_,_,_) as obj ->
+                  (fun (dstatus,uris_rev) (uri,_,_,_,_) as obj ->
                     NCicTypeChecker.typecheck_obj obj;
-                    let timestamp = NCicLibrary.add_obj uri obj in
-                     timestamp,uri::uris_rev
-                  ) (timestamp,[]) objs in
+                    let dstatus = NCicLibrary.add_obj dstatus uri obj in
+                     dstatus,uri::uris_rev
+                  ) (dstatus,[]) objs in
                let uris = uri::List.rev uris_rev in
-                GrafiteTypes.set_library_db timestamp
+                GrafiteTypes.set_dstatus dstatus
                  {status with 
                   GrafiteTypes.ng_status = 
                    GrafiteTypes.CommandMode estatus },`New uris
diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index de578d7ca..94170493b 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -147,12 +147,11 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity
    objects = lemmas @ status.GrafiteTypes.objects;
   }
  in
- let db = 
+ let dstatus = 
    NCicCoercion.index_old_db (CoercDb.dump ()) 
-    (GrafiteTypes.get_coercions status) 
- in
- let status = GrafiteTypes.set_coercions db status in 
- status, lemmas
+    (GrafiteTypes.get_dstatus status) in
+ let status = GrafiteTypes.set_dstatus dstatus status in
+  status, lemmas
 
 let prefer_coercion s u = 
   CoercDb.prefer u;
@@ -171,7 +170,7 @@ let time_travel ~present ~past =
    uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in
   List.iter LibrarySync.remove_obj objs_to_remove;
   CoercDb.restore past.GrafiteTypes.coercions;
-  NCicLibrary.time_travel (GrafiteTypes.get_library_db past)
+  NCicLibrary.time_travel (GrafiteTypes.get_dstatus past)
 ;;
 
 let initial_status lexicon_status baseuri = {
@@ -183,14 +182,8 @@ let initial_status lexicon_status baseuri = {
     baseuri = baseuri;
     ng_status = GrafiteTypes.CommandMode { 
       NEstatus.lstatus = lexicon_status;
-      NEstatus.rstatus = {
-       NRstatus.refiner_status = {
-        NRstatus.uhint_db = NCicUnifHint.empty_db;
-        NRstatus.coerc_db = NCicCoercion.empty_db;
-        NRstatus.library_db = NCicLibrary.time0 };
-       NRstatus.dump = []
-      };
-  }
+      NEstatus.rstatus = new NRstatus.dumpable_status
+    };
 }
 
 
diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 0b9a4a7da..6033be8c2 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -96,49 +96,11 @@ let set_estatus e x =
 
 let get_dstatus x = (get_estatus x).NEstatus.rstatus;;
 
-let get_rstatus x = (get_dstatus x).NRstatus.refiner_status;;
-
-let get_hstatus x = (get_rstatus x).NRstatus.uhint_db;;
-
-let get_library_db x = (get_rstatus x).NRstatus.library_db;;
-
-let get_dump x = (get_dstatus x).NRstatus.dump;;
-
 let set_dstatus h x =
  let estatus = get_estatus x in
   set_estatus { estatus with NEstatus.rstatus = h } x
 ;;
 
-let set_rstatus h x =
- let dstatus = get_dstatus x in
-  set_dstatus { dstatus with NRstatus.refiner_status = h } x
-;;
-
-let set_coercions db x = 
- let rstatus = get_rstatus x in
-  set_rstatus { rstatus with NRstatus.coerc_db = db } x
-;;
-
-
-let set_hstatus h x =
- let rstatus = get_rstatus x in
-  set_rstatus { rstatus with NRstatus.uhint_db = h} x
-;;
-
-let set_library_db h x =
- let rstatus = get_rstatus x in
-  set_rstatus { rstatus with NRstatus.library_db = h} x
-;;
-
-let set_dump h x =
- let estatus = get_estatus x in
-  set_estatus
-  { estatus with NEstatus.rstatus =
-     { estatus.NEstatus.rstatus with
-        NRstatus.dump = h}}
-  x
-;;
-
 let get_current_proof status =
   match status.proof_status with
   | Incomplete_proof { proof = p } -> p
@@ -271,5 +233,3 @@ let dump_status status =
   HLog.message "status.objects:\n";
   List.iter 
     (fun u -> HLog.message (UriManager.string_of_uri u)) status.objects 
-  
-let get_coercions x = (get_rstatus x).NRstatus.coerc_db;;
diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index 4caba49d1..8ed9fe489 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -75,19 +75,10 @@ val get_proof_context : status -> int -> Cic.context
 val get_proof_conclusion : status -> int -> Cic.term
 val get_lexicon : status -> LexiconEngine.status
 val get_estatus : status -> NEstatus.extra_status
-val get_rstatus : status -> NRstatus.refiner_status
-val get_hstatus : status -> NCicUnifHint.db
-val get_library_db : status -> NCicLibrary.timestamp
-val get_dump : status -> NRstatus.Serializer.obj list
-val get_coercions: status -> NCicCoercion.db
+val get_dstatus : status -> NRstatus.dumpable_status
 
 val set_stack: Continuationals.Stack.t -> status -> status
 val set_metasenv: Cic.metasenv -> status -> status
 val set_lexicon : LexiconEngine.status -> status -> status
-val set_coercions: NCicCoercion.db -> status -> status 
 val set_estatus : NEstatus.extra_status -> status -> status
-val set_rstatus : NRstatus.refiner_status -> status -> status
-val set_hstatus : NCicUnifHint.db -> status -> status
-val set_library_db : NCicLibrary.timestamp -> status -> status
-val set_dump : NRstatus.Serializer.obj list -> status -> status
-
+val set_dstatus : NRstatus.dumpable_status -> status -> status
diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 0dfab7a37..4aadd7077 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -200,7 +200,7 @@ let disambiguate_nterm expty estatus context metasenv subst thing
   let diff, metasenv, subst, cic =
     singleton "first"
       (NCicDisambiguate.disambiguate_term
-        ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
+        ~rdb:estatus.NEstatus.rstatus
         ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
         ~expty 
         ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases)
@@ -688,7 +688,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
+           ~rdb:estatus.NEstatus.rstatus
            ~lookup_in_library:nlookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
@@ -783,7 +783,7 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
       ~mk_choice:ncic_mk_choice
       ~mk_implicit
       ~uri:(OCic2NCic.nuri_of_ouri uri)
-      ~rdb:estatus.NEstatus.rstatus.NRstatus.refiner_status
+      ~rdb:estatus.NEstatus.rstatus
       ~aliases:estatus.NEstatus.lstatus.LexiconEngine.aliases
       ~universe:(Some estatus.NEstatus.lstatus.LexiconEngine.multi_aliases) 
       (text,prefix_len,obj)) in
diff --git a/helm/software/components/grafite_parser/nEstatus.ml b/helm/software/components/grafite_parser/nEstatus.ml
index a49174b11..2ae7d01e4 100644
--- a/helm/software/components/grafite_parser/nEstatus.ml
+++ b/helm/software/components/grafite_parser/nEstatus.ml
@@ -13,6 +13,6 @@
 
 type extra_status = {
         lstatus : LexiconEngine.status;
-        rstatus : NRstatus.dumpable_refiner_status;
+        rstatus : NRstatus.dumpable_status;
 }
 
diff --git a/helm/software/components/grafite_parser/nEstatus.mli b/helm/software/components/grafite_parser/nEstatus.mli
index a49174b11..2ae7d01e4 100644
--- a/helm/software/components/grafite_parser/nEstatus.mli
+++ b/helm/software/components/grafite_parser/nEstatus.mli
@@ -13,6 +13,6 @@
 
 type extra_status = {
         lstatus : LexiconEngine.status;
-        rstatus : NRstatus.dumpable_refiner_status;
+        rstatus : NRstatus.dumpable_status;
 }
 
diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 108c845c6..5fa3b8188 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -47,9 +47,8 @@ let refine_term
     in
     let metasenv, subst, term, _ = 
       NCicRefiner.typeof 
-        { rdb with NRstatus.coerc_db = 
-           if use_coercions then rdb.NRstatus.coerc_db 
-           else NCicCoercion.empty_db }
+        (rdb#set_coerc_db 
+          (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db))
         metasenv subst context term expty ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
@@ -79,9 +78,9 @@ let refine_obj
   try
     let obj =
       NCicRefiner.typeof_obj
-        { rdb with NRstatus.coerc_db = 
-           if use_coercions then rdb.NRstatus.coerc_db 
-           else NCicCoercion.empty_db }
+        (rdb#set_coerc_db
+           (if use_coercions then rdb#coerc_db 
+            else NCicCoercion.empty_db))
         obj ~localise 
     in
       Disambiguate.Ok (obj, [], [], ())
diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
index 0eb018b9d..b86849f35 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.mli
@@ -21,7 +21,7 @@ val disambiguate_term :
   mk_choice:('alias -> NCic.term DisambiguateTypes.codomain_item) ->
   aliases:'alias DisambiguateTypes.Environment.t ->
   universe:'alias list DisambiguateTypes.Environment.t option ->
-  rdb:NRstatus.refiner_status ->
+  rdb:#NRstatus.status ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
@@ -40,7 +40,7 @@ val disambiguate_obj :
     mk_choice:('a -> NCic.term DisambiguateTypes.codomain_item) ->
     aliases:'a DisambiguateTypes.Environment.t ->
     universe:'a list DisambiguateTypes.Environment.t option ->
-    rdb:NRstatus.refiner_status ->
+    rdb:#NRstatus.status ->
     lookup_in_library:(DisambiguateTypes.interactive_user_uri_choice_type ->
                        DisambiguateTypes.input_or_locate_uri_type ->
                        DisambiguateTypes.Environment.key -> 'a list) ->
diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index cc13dde6e..1cb3a118b 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -23,7 +23,17 @@ let storage = ref [];;
 let aliases = ref [];;
 let cache = ref NUri.UriMap.empty;;
 
-let time_travel (sto,ali,cac) = storage := sto; aliases := ali; cache := cac;;
+class status =
+ object
+  val timestamp = (time0 : timestamp)
+  method timestamp = timestamp
+  method set_timestamp v = {< timestamp = v >}
+ end
+
+let time_travel status =
+ let sto,ali,cac = status#timestamp in
+  storage := sto; aliases := ali; cache := cac
+;;
 
 let path_of_baseuri baseuri =
  let uri = NUri.string_of_uri baseuri in
@@ -56,7 +66,7 @@ let serialize ~baseuri dump =
     Marshal.to_channel ch (magic,obj) [];
     close_out ch
   ) !storage;
- time_travel time0
+ time_travel (new status)
 ;;
 
 let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
@@ -139,7 +149,7 @@ let aliases_of uri =
   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
 ;;
 
-let add_obj u obj =
+let add_obj status u obj =
  storage := (u,obj)::!storage;
   let _,height,_,_,obj = obj in
   let references =
@@ -170,7 +180,7 @@ let add_obj u obj =
          ) il)
   in
   aliases := references @ !aliases;
-  !storage,!aliases,!cache
+  status#set_timestamp (!storage,!aliases,!cache)
 ;;
 
 let get_obj u =
diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index 526632565..dfd17f15b 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -14,9 +14,14 @@
 exception LibraryOutOfSync of string Lazy.t
 
 type timestamp
-val time0: timestamp
 
-val add_obj: NUri.uri -> NCic.obj -> timestamp
+class status :
+ object ('self)
+  method timestamp: timestamp
+  method set_timestamp: timestamp -> 'self
+ end
+
+val add_obj: #status as 'status -> NUri.uri -> NCic.obj -> 'status
 val aliases_of: NUri.uri -> NReference.reference list
 val resolve: string -> NReference.reference list
 (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *)
@@ -24,7 +29,7 @@ val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *)
 
 val clear_cache : unit -> unit
 
-val time_travel: timestamp -> unit
+val time_travel: #status -> unit
 val decompile: baseuri:NUri.uri -> unit
 
 module type Serializer =
diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index dd866f8db..69299b13f 100644
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -1,5 +1,5 @@
 val nparamod : 
-  NRstatus.refiner_status ->
+  #NRstatus.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
     (NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
      unit
diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 6aba5a993..2ab8185ab 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -271,11 +271,7 @@ let _ =
           prerr_endline ("start: " ^ NUri.string_of_uri u);
           let bo = curryfy [] bo in
           (try 
-            let rdb = { 
-               NRstatus.uhint_db = NCicUnifHint.empty_db; 
-               NRstatus.coerc_db = NCicCoercion.empty_db;
-               NRstatus.library_db = NCicLibrary.time0
-            } in 
+            let rdb = new NRstatus.status in
             let metasenv, subst, bo, infty = 
               NCicRefiner.typeof rdb [] [] [] bo None
             in
diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml
index e62d4eed3..29f28ba5c 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.ml
+++ b/helm/software/components/ng_refiner/nCicCoercion.ml
@@ -24,7 +24,17 @@ module DB =
 
 type db = DB.t * DB.t
 
-let index_coercion (db_src,db_tgt) c src tgt arity arg =
+let empty_db = DB.empty,DB.empty
+
+class status =
+ object
+  val db = empty_db
+  method coerc_db = db
+  method set_coerc_db v = {< db = v >}
+ end
+
+let index_coercion status c src tgt arity arg =
+  let db_src,db_tgt = status#coerc_db in
   let data = (c,arity,arg) in
 (*
   prerr_endline ("INDEX:" ^ 
@@ -34,14 +44,14 @@ let index_coercion (db_src,db_tgt) c src tgt arity arg =
 *)
   let db_src = DB.index db_src src data in
   let db_tgt = DB.index db_tgt tgt data in
-  db_src, db_tgt
+  status#set_coerc_db (db_src, db_tgt)
 ;;
 
-let index_old_db odb db =
+let index_old_db odb (status : #status) =
   List.fold_left 
-    (fun db (_,tgt,clist) -> 
+    (fun status (_,tgt,clist) -> 
        List.fold_left 
-         (fun db (uri,_,arg) ->
+         (fun status (uri,_,arg) ->
            try
             let c=fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)) in
             let arity = match tgt with | CoercDb.Fun i -> i | _ -> 0 in
@@ -67,18 +77,16 @@ let index_old_db odb db =
                     NCicPp.ppterm ~metasenv ~subst:[] ~context:[] t);
                   assert false
             in
-            index_coercion db c src tgt arity arg
+            index_coercion status c src tgt arity arg
            with 
            | NCicEnvironment.BadDependency _ 
-           | NCicTypeChecker.TypeCheckerFailure _ -> db)
-         db clist)
-    db (CoercDb.to_list odb)
+           | NCicTypeChecker.TypeCheckerFailure _ -> status)
+         status clist)
+    status (CoercDb.to_list odb)
 ;;
 
-let empty_db = (DB.empty,DB.empty) ;;
-
-
-let look_for_coercion (db_src,db_tgt) metasenv subst context infty expty =
+let look_for_coercion status metasenv subst context infty expty =
+ let db_src,db_tgt = status#coerc_db in
   match infty, expty with
   | (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)), 
     (NCic.Meta _ | NCic.Appl (NCic.Meta _::_)) -> [] 
diff --git a/helm/software/components/ng_refiner/nCicCoercion.mli b/helm/software/components/ng_refiner/nCicCoercion.mli
index 73c88005c..1a31172d2 100644
--- a/helm/software/components/ng_refiner/nCicCoercion.mli
+++ b/helm/software/components/ng_refiner/nCicCoercion.mli
@@ -13,19 +13,26 @@
 
 type db
 
+class status :
+ object ('self)
+  method coerc_db: db
+  method set_coerc_db: db -> 'self
+ end
+
+val empty_db: db
+
 (* index (\x.c ?? x ??): A -> B
    index_coercion db c A B \arity_left(c ??x??) \position(x,??x??) 
 *)
 val index_coercion: 
-  db -> NCic.term -> NCic.term -> NCic.term -> int -> int -> db
+  #status as 'status ->
+   NCic.term -> NCic.term -> NCic.term -> int -> int -> 'status
 
   (* gets the old imperative coercion DB (list format) *)
-val index_old_db: CoercDb.coerc_db -> db -> db
-
-val empty_db : db
+val index_old_db: CoercDb.coerc_db -> (#status as 'status) -> 'status
 
 val look_for_coercion:
-    db ->
+    #status ->
     NCic.metasenv -> NCic.substitution -> NCic.context -> 
     (* inferred type, expected type *)
     NCic.term -> NCic.term -> 
diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 0f835961e..ffa2422e4 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -376,8 +376,7 @@ and try_coercions rdb
       | NCicUnification.Uncertain _ as exc -> first exc tl
   in 
     first exc
-      (NCicCoercion.look_for_coercion 
-        rdb.NRstatus.coerc_db metasenv subst context infty expty)
+      (NCicCoercion.look_for_coercion rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
   match NCicReduction.whd ~subst context ty with
diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli
index b601db963..b75ee3a81 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.mli
+++ b/helm/software/components/ng_refiner/nCicRefiner.mli
@@ -16,7 +16,7 @@ exception Uncertain of (Stdpp.location * string) Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val typeof :
- NRstatus.refiner_status ->
+ #NRstatus.status ->
  ?localise:(NCic.term -> Stdpp.location) ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   NCic.term -> NCic.term option -> (* term, expected type *)
@@ -24,7 +24,7 @@ val typeof :
     (*  menv, subst,refined term, type *)
 
 val typeof_obj :
- NRstatus.refiner_status ->
+ #NRstatus.status ->
  ?localise:(NCic.term -> Stdpp.location) ->
   NCic.obj -> NCic.obj
 
diff --git a/helm/software/components/ng_refiner/nCicUnifHint.ml b/helm/software/components/ng_refiner/nCicUnifHint.ml
index c09e08d3c..ccccfca88 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.ml
+++ b/helm/software/components/ng_refiner/nCicUnifHint.ml
@@ -24,6 +24,13 @@ module DB =
 
 type db = DB.t
 
+class status =
+ object
+  val db = DB.empty
+  method uhint_db = db
+  method set_uhint_db v = {< db = v >}
+ end
+
 let dummy = NCic.Const (NReference.reference_of_string "cic:/dummy_conv.dec");;
 let pair t1 t2 = (NCic.Appl [dummy;t1;t2]) ;;
 
@@ -57,11 +64,9 @@ let index_hint hdb context t1 t2 precedence =
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " |==> " ^
     NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] data);
 *)
-  DB.index hdb src (precedence, data)
+  hdb#set_uhint_db (DB.index hdb#uhint_db src (precedence, data))
 ;;
 
-let empty_db = DB.empty ;;
-
 let add_user_provided_hint db t precedence =
   let c, a, b = 
     let rec aux ctx = function
@@ -176,8 +181,8 @@ let look_for_hint hdb metasenv subst context t1 t2 =
       String.concat "|" (List.map (NCicPp.ppterm ~metasenv:[] ~subst:[]
       ~context:[]) (HintSet.elements ds))));
 *)
-  let candidates1 = DB.retrieve_unifiables hdb (pair t1 t2) in
-  let candidates2 = DB.retrieve_unifiables hdb (pair t2 t1) in
+  let candidates1 = DB.retrieve_unifiables hdb#uhint_db (pair t1 t2) in
+  let candidates2 = DB.retrieve_unifiables hdb#uhint_db (pair t2 t1) in
   let candidates1 = 
     List.map (fun (prec,ty) -> 
        prec,true,saturate ~delta:max_int metasenv subst context ty 0) 
diff --git a/helm/software/components/ng_refiner/nCicUnifHint.mli b/helm/software/components/ng_refiner/nCicUnifHint.mli
index 21820ace4..f7257d8f8 100644
--- a/helm/software/components/ng_refiner/nCicUnifHint.mli
+++ b/helm/software/components/ng_refiner/nCicUnifHint.mli
@@ -13,15 +13,20 @@
 
 type db
 
-val index_hint: 
-  db -> NCic.context -> NCic.term -> NCic.term -> int -> db
+class status :
+ object ('self)
+  method uhint_db: db
+  method set_uhint_db: db -> 'self
+ end
 
-val add_user_provided_hint : db -> NCic.term -> int -> db 
+val index_hint: 
+  #status as 'status -> NCic.context -> NCic.term -> NCic.term -> int -> 'status
 
-val empty_db : db
+val add_user_provided_hint :
+  #status as 'status -> NCic.term -> int -> 'status
 
 val look_for_hint:
-    db ->
+    #status ->
     NCic.metasenv -> NCic.substitution -> NCic.context -> 
     NCic.term -> NCic.term -> 
       (NCic.metasenv * 
diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 9ee056aed..bfa1388a9 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -490,8 +490,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
         NCicPp.ppterm ~metasenv ~subst ~context t2);
 *)
       let candidates = 
-        NCicUnifHint.look_for_hint 
-          rdb.NRstatus.uhint_db metasenv subst context t1 t2
+        NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
       in
       let rec cand_iter = function
         | [] -> None (* raise exc *)
diff --git a/helm/software/components/ng_refiner/nCicUnification.mli b/helm/software/components/ng_refiner/nCicUnification.mli
index 23728e4f8..a6ddfaeed 100644
--- a/helm/software/components/ng_refiner/nCicUnification.mli
+++ b/helm/software/components/ng_refiner/nCicUnification.mli
@@ -16,7 +16,7 @@ exception Uncertain of string Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val unify :
-  NRstatus.refiner_status ->
+  #NRstatus.status ->
   ?test_eq_only:bool -> (* default: false *)
   NCic.metasenv -> NCic.substitution -> NCic.context -> 
   NCic.term -> NCic.term ->
diff --git a/helm/software/components/ng_refiner/nRstatus.ml b/helm/software/components/ng_refiner/nRstatus.ml
index 26ef2684c..736de4aa0 100644
--- a/helm/software/components/ng_refiner/nRstatus.ml
+++ b/helm/software/components/ng_refiner/nRstatus.ml
@@ -11,16 +11,31 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-type refiner_status = {
-        coerc_db : NCicCoercion.db;
-        uhint_db : NCicUnifHint.db;
-        library_db : NCicLibrary.timestamp;
-}
+class status =
+ object
+  inherit NCicUnifHint.status
+  inherit NCicCoercion.status
+  inherit NCicLibrary.status
+ end
+
+type sstatus = status
 
 module Serializer =
- NCicLibrary.Serializer(struct type status = refiner_status end)
+ struct
+  include NCicLibrary.Serializer(struct type status = sstatus end)
+
+  let require ~baseuri status = 
+   let rstatus = require ~baseuri (status : #status :> status) in
+   let status = status#set_uhint_db (rstatus#uhint_db) in
+   let status = status#set_coerc_db (rstatus#coerc_db) in
+   let status = status#set_timestamp (rstatus#timestamp) in
+    status 
+ end
 
-type dumpable_refiner_status = {
-        refiner_status : refiner_status;
-        dump: Serializer.obj list
-}
+class dumpable_status =
+ object
+  inherit status
+  val dump = ([] : Serializer.obj list)
+  method dump = dump
+  method set_dump v = {< dump = v >}
+ end
diff --git a/helm/software/components/ng_refiner/nRstatus.mli b/helm/software/components/ng_refiner/nRstatus.mli
index 729f6ba6e..522d7e901 100644
--- a/helm/software/components/ng_refiner/nRstatus.mli
+++ b/helm/software/components/ng_refiner/nRstatus.mli
@@ -11,15 +11,22 @@
 
 (* $Id: nCicRefiner.ml 9802 2009-05-25 15:39:26Z tassi $ *)
 
-type refiner_status = {
-        coerc_db : NCicCoercion.db;
-        uhint_db : NCicUnifHint.db;
-        library_db : NCicLibrary.timestamp;
-}
+class status :
+ object
+  inherit NCicUnifHint.status
+  inherit NCicCoercion.status
+  inherit NCicLibrary.status
+ end
 
-module Serializer: NCicLibrary.Serializer with type status = refiner_status
+module Serializer:
+ sig
+  include NCicLibrary.Serializer with type status = status 
+  val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
+ end
 
-type dumpable_refiner_status = {
-        refiner_status : refiner_status;
-        dump: Serializer.obj list
-}
+class dumpable_status :
+ object ('self)
+  inherit status
+  method dump: Serializer.obj list
+  method set_dump: Serializer.obj list -> 'self
+ end
diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml
index ba0308068..6aaf4a4a8 100644
--- a/helm/software/components/ng_tactics/nTacStatus.ml
+++ b/helm/software/components/ng_tactics/nTacStatus.ml
@@ -84,7 +84,7 @@ let relocate status destination (name,source,t as orig) =
     NCicMetaSubst.delift 
        ~unify:(fun m s c t1 t2 -> 
          try Some (NCicUnification.unify 
-           status.estatus.NEstatus.rstatus.NRstatus.refiner_status m s c t1 t2)
+           status.estatus.NEstatus.rstatus m s c t1 t2)
          with 
           | NCicUnification.UnificationFailure _ 
           | NCicUnification.Uncertain _ -> None) 
@@ -147,7 +147,7 @@ let unify status ctx a b =
   let status, (_,_,b) = relocate status ctx b in
   let n,h,metasenv,subst,o = status.pstatus in
   let metasenv, subst = 
-    NCicUnification.unify status.estatus.NEstatus.rstatus.NRstatus.refiner_status metasenv subst ctx a b
+    NCicUnification.unify status.estatus.NEstatus.rstatus metasenv subst ctx a b
   in
   { status with pstatus = n,h,metasenv,subst,o }
 ;;
@@ -160,7 +160,7 @@ let refine status ctx term expty =
         let status, (n,_, e) = relocate status ctx e in status, n, Some e
   in
   let name,height,metasenv,subst,obj = status.pstatus in
-  let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
+  let rdb = status.estatus.NEstatus.rstatus in
   let metasenv, subst, t, ty = 
    NCicRefiner.typeof rdb metasenv subst ctx term expty
   in
diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index b6b933211..e751cca58 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -568,7 +568,7 @@ let auto ~params:(l,_) status goal =
         (status, (t,ty) :: l))
       (status,[]) l
   in
-  let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
+  let rdb = status.estatus.NEstatus.rstatus in
   Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;      
     status
 ;;
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 8acc424a9..e71eb4104 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -90,7 +90,7 @@ let save_moo grafite_status =
      LexiconMarshal.save_lexicon lexicon_fname
        (GrafiteTypes.get_lexicon grafite_status).LexiconEngine.lexicon_content_rev;
      NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
-      (GrafiteTypes.get_dump grafite_status)
+      (GrafiteTypes.get_dstatus grafite_status)#dump
   | _ -> clean_current_baseuri grafite_status 
 ;;
     
diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml
index 5ed1d41b4..7575eca10 100644
--- a/helm/software/matita/matitaWiki.ml
+++ b/helm/software/matita/matitaWiki.ml
@@ -227,7 +227,7 @@ let main () =
       |  s::_ ->
          s.proof_status, s.moo_content_rev,
           (GrafiteTypes.get_lexicon s).LexiconEngine.lexicon_content_rev,
-          GrafiteTypes.get_dump s
+          (GrafiteTypes.get_dstatus s)#dump
       | _ -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index c0c3d0941..e26a3f89d 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -275,7 +275,7 @@ let compile atstart options fname =
         GrafiteMarshal.save_moo moo_fname moo_content_rev;
         LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
         NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
-         (GrafiteTypes.get_dump grafite_status)
+         (GrafiteTypes.get_dstatus grafite_status)#dump
      end;
      let tm = Unix.gmtime elapsed in
      let sec = string_of_int tm.Unix.tm_sec ^ "''" in