X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_library%2FnCicLibrary.ml;h=ad8084692fd11f3951546183b36d65083da22b7b;hb=098e3728bb1d993145b893b83ac6e01173b58486;hp=1ed016e771035df34cc37920d498e2df468dcaeb;hpb=47a9eb47d4215450230840bc66570ce412d0ce79;p=helm.git

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index 1ed016e77..ad8084692 100644
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -22,13 +22,15 @@ let refresh_uri_in_universe =
  List.map (fun (x,u) -> x, refresh_uri u)
 ;;
 
+let refresh_uri_in_reference (NReference.Ref (uri,spec)) =
+ NReference.reference_of_spec (refresh_uri uri) spec
+
 let rec refresh_uri_in_term =
  function
   | NCic.Meta (i,(n,NCic.Ctx l)) ->
      NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l)))
   | NCic.Meta _ as t -> t
-  | NCic.Const (NReference.Ref (u,spec)) ->
-     NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
+  | NCic.Const ref -> NCic.Const (refresh_uri_in_reference ref)
   | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l))
   | NCic.Match (NReference.Ref (uri,spec),outtype,term,pl) ->
      let r = NReference.reference_of_spec (refresh_uri uri) spec in
@@ -146,54 +148,11 @@ 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
-  method timestamp: timestamp
- end
-
 class status =
  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 -> self#set_timestamp o#timestamp
  end
 
 let time_travel status =
@@ -224,37 +183,41 @@ let serialize ~baseuri dump =
   
 type obj = string * Obj.t
 
-
-class type g_dumpable_status =
- object
-  inherit g_status
-  inherit g_auto_status
-  inherit g_eq_status
-  method dump: obj list
- end
-
 class dumpable_status =
  object(self)
-  inherit status
-  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)#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 type SerializerType =
+ sig
+  type dumpable_status
+
+  type 'a register_type =
+   'a ->
+    refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
+    refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+     dumpable_status -> dumpable_status
+
+  val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >
+  val serialize: baseuri:NUri.uri -> obj list -> unit
+   (* the obj is the "include" command to be added to the dump list *)
+  val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj
+ end
 
-module Serializer =
+module Serializer(D: sig type dumpable_status end) =
  struct
-  let require1 = ref (object method run : 'status. obj -> (#dumpable_status as 'status) -> 'status  = fun _ -> assert false end (* unknown data*))
+  type dumpable_status = D.dumpable_status
+  type 'a register_type =
+   'a ->
+    refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
+    refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+     dumpable_status -> dumpable_status
+
+  let require1 = ref (fun _ -> assert false) (* unknown data*)
   let already_registered = ref []
 
   let register =
@@ -265,14 +228,12 @@ module Serializer =
      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 ((tag',data) as x) ->
+        if tag=tag' then
+         require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
+          ~refresh_uri_in_reference
+        else
+         old_require1 x);
      (fun x -> tag,Obj.repr x)
    end
 
@@ -282,25 +243,22 @@ module Serializer =
    try
     includes := baseuri::!includes;
     let dump = require0 ~baseuri in
-     List.fold_right !require1#run dump status
+     List.fold_right !require1 dump status
    with
     Sys_error _ ->
      raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri))
 
   let record_include =
-   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term =
+   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term
+   ~refresh_uri_in_reference =
      (* memorizzo baseuri in una tabella; *)
      require2 ~baseuri
    in
-    register#run "include"
-     object(self : 'a register_type)
-      method run = aux
-     end
+    register#run "include" aux
 
   let require ~baseuri status =
    let status = require2 ~baseuri status in
-   let dump = record_include baseuri :: status#dump in
-    status#set_dump dump
+    status,record_include baseuri
 end