exception LibraryOutOfSync of string Lazy.t
+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)
+ inherit g_eq_status
+ method set_eq_cache: unit_eq_cache -> 'self
+ method set_eq_status: #g_eq_status -> 'self
+ end
+
+class type g_auto_status =
+ object
+ method auto_cache : automation_cache
+ end
+
+class auto_status :
+ object('self)
+ inherit g_auto_status
+ method set_auto_cache: automation_cache -> 'self
+ method set_auto_status: #g_auto_status -> 'self
+ end
+
type timestamp
class type g_status =
val time_travel: #status -> unit
val decompile: baseuri:NUri.uri -> unit
-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
- end
-
val init: unit -> unit
-module Serializer:
- sig
- include SerializerT with type status = status
- val require: baseuri:NUri.uri -> (#status as 'status) -> 'status
- end
+type obj
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
+ inherit auto_status
+ inherit eq_status
inherit g_dumpable_status
- method set_dump: Serializer.obj list -> 'self
+ method set_dump: obj list -> 'self
method set_dumpable_status: #g_dumpable_status -> 'self
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:
+ sig
+ val register: < run: 'a. string -> 'a register_type -> ('a -> obj) >
+ val serialize: baseuri:NUri.uri -> obj list -> unit
+ val require: baseuri:NUri.uri -> (#dumpable_status as 'status) -> 'status
+ end
+
(* CSC: only required during old-to-NG phase, to be deleted *)
val refresh_uri: NUri.uri -> NUri.uri