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