(* $Id$ *)
exception LibraryOutOfSync of string Lazy.t
+exception IncludedFileNotCompiled of string * string
let magic = 2;;
dump
;;
-let require0 ~baseuri = require_path (path_of_baseuri baseuri);;
+let require0 ~baseuri =
+ require_path (path_of_baseuri baseuri)
+;;
let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
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 =
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
-module Serializer =
+ type 'a register_type =
+ 'a ->
+ refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
+ refresh_uri_in_term:(NCic.term -> NCic.term) ->
+ 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(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) ->
+ dumpable_status -> dumpable_status
+
+ let require1 = ref (fun _ -> assert false) (* unknown data*)
let already_registered = ref []
let register =
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
+ else
+ old_require1 x);
(fun x -> tag,Obj.repr x)
end
let serialize = serialize
+ let require2 ~baseuri status =
+ try
+ includes := baseuri::!includes;
+ let dump = require0 ~baseuri in
+ 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 =
+ (* memorizzo baseuri in una tabella; *)
+ require2 ~baseuri
+ in
+ register#run "include" aux
+
let require ~baseuri status =
- includes := baseuri::!includes;
- let dump = require0 ~baseuri in
- List.fold_right !require1#run dump status
+ let status = require2 ~baseuri status in
+ status,record_include baseuri
end