X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_library%2FnCicLibrary.ml;h=7cef1e3de66fb2ad68ad2684b973527f878cb06b;hb=5439626efe5ed3aa4b6ac01f2116a6a8ab6a3f92;hp=6987ec1aa698e8b9560854754acc22063947eb43;hpb=a18562238677261e3d0b590e046290a14fe62e74;p=helm.git

diff --git a/helm/software/components/ng_library/nCicLibrary.ml b/helm/software/components/ng_library/nCicLibrary.ml
index 6987ec1aa..7cef1e3de 100644
--- a/helm/software/components/ng_library/nCicLibrary.ml
+++ b/helm/software/components/ng_library/nCicLibrary.ml
@@ -143,6 +143,39 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
+type automation_cache = NDiscriminationTree.DiscriminationTree.t
+type unit_eq_cache = NCicParamod.state
+
+class type g_eq_status =
+ object
+   method eq_cache : unit_eq_cache 
+ end
+
+class eq_status =
+ object(self)
+  val eq_cache = NCicParamod.empty_state
+  method eq_cache = eq_cache
+  method set_eq_cache v = {< eq_cache = v >}
+  method set_eq_status
+   : 'status. #g_eq_status as 'status -> 'self
+   = fun o -> self#set_eq_cache o#eq_cache
+ end
+
+class type g_auto_status =
+ object
+   method auto_cache : automation_cache
+ end
+
+class auto_status =
+ object(self)
+  val auto_cache = NDiscriminationTree.DiscriminationTree.empty
+  method auto_cache = auto_cache
+  method set_auto_cache v = {< auto_cache = v >}
+  method set_auto_status
+   : 'status. #g_auto_status as 'status -> 'self
+   = fun o -> self#set_auto_cache o#auto_cache
+ end
+
 class type g_status =
  object
   inherit NRstatus.g_status
@@ -150,27 +183,14 @@ class type g_status =
  end
 
 class status =
- object
+ object(self)
   inherit NRstatus.status
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
   method set_timestamp v = {< timestamp = v >}
   method set_library_status
    : 'status. #g_status as 'status -> 'self
-   = fun o -> {< timestamp = o#timestamp >}
- end
-
-
-module type SerializerT =
- sig
-  type status
-  type obj
-  val register:
-   string ->
-    ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
-    ('a -> obj)
-  val serialize: baseuri:NUri.uri -> obj list -> unit
-  val require: baseuri:NUri.uri -> status -> status
+   = fun o -> self#set_timestamp o#timestamp
  end
 
 let time_travel status =
@@ -198,65 +218,69 @@ let serialize ~baseuri dump =
  List.iter (fun u -> add_deps u [baseuri]) !includes;
  time_travel (new status)
 ;;
+  
+type obj = string * Obj.t
 
-module SerializerF(S: sig type status end) =
- struct
-  type status = S.status
-  type obj = string * Obj.t
-
-  let require1 = ref (fun _ -> assert false (* unknown data*))
-  let already_registered = ref []
-
-  let register tag require =
-   assert (not (List.mem tag !already_registered));
-   already_registered := tag :: !already_registered;
-   let old_require1 = !require1 in
-   require1 :=
-     (fun (tag',data) as x ->
-      if tag=tag' then
-       require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term 
-      else
-       old_require1 x);
-   (fun x -> tag,Obj.repr x)
-
-  let serialize = serialize
-
-  let require ~baseuri status =
-   includes := baseuri::!includes;
-   let dump = require0 ~baseuri in
-    List.fold_right !require1 dump status
-end
-
-type sstatus = status
-
-module Serializer =
- struct
-  include SerializerF(struct type status = sstatus end)
-
-  let require ~baseuri status = 
-   let rstatus = require ~baseuri (status : #status :> status) in
-   let status = status#set_coerc_db (rstatus#coerc_db) in
-   let status = status#set_uhint_db (rstatus#uhint_db) in
-   let status = status#set_timestamp (rstatus#timestamp) in
-    status 
- end
 
 class type g_dumpable_status =
  object
   inherit g_status
-  method dump: Serializer.obj list
+  inherit g_auto_status
+  inherit g_eq_status
+  method dump: obj list
  end
 
 class dumpable_status =
  object(self)
   inherit status
-  val dump = ([] : Serializer.obj list)
+  inherit auto_status
+  inherit eq_status
+  val dump = ([] : obj list)
   method dump = dump
   method set_dump v = {< dump = v >}
   method set_dumpable_status : 'status. #g_dumpable_status as 'status -> 'self
-   = fun o -> (self#set_dump o#dump)#set_coercion_status o
+   = fun o -> 
+     (((self#set_dump o#dump)#set_coercion_status o)#set_auto_status o)#set_eq_status o
  end
 
+type 'a register_type =
+ < run: 'status.
+    'a -> refresh_uri_in_universe:(NCic.universe ->
+      NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) ->
+       (#dumpable_status as 'status) -> 'status >
+
+module Serializer =
+ struct
+  let require1 = ref (object method run : 'status. obj -> (#dumpable_status as 'status) -> 'status  = fun _ -> assert false end (* unknown data*))
+  let already_registered = ref []
+
+  let register =
+   object
+    method run : 'a.  string -> 'a register_type -> ('a -> obj)
+    = fun tag require ->
+     assert (not (List.mem tag !already_registered));
+     already_registered := tag :: !already_registered;
+     let old_require1 = !require1 in
+     require1 :=
+       object
+        method run : 'status. obj -> (#dumpable_status as 'status) -> 'status =
+         fun ((tag',data) as x) ->
+         if tag=tag' then
+          require#run (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
+         else
+          old_require1#run x
+       end;
+     (fun x -> tag,Obj.repr x)
+   end
+
+  let serialize = serialize
+
+  let require ~baseuri status =
+   includes := baseuri::!includes;
+   let dump = require0 ~baseuri in
+    List.fold_right !require1#run dump status
+end
+
 
 let decompile ~baseuri =
  let baseuris = get_deps baseuri in