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
NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
;;
-let path_of_baseuri ?(no_suffix=false) baseuri =
+let ng_path_of_baseuri ?(no_suffix=false) baseuri =
let uri = NUri.string_of_uri baseuri in
let path = String.sub uri 4 (String.length uri - 4) in
let path = Helm_registry.get "matita.basedir" ^ path in
dump
;;
-let require0 ~baseuri =
- require_path (path_of_baseuri baseuri)
-;;
+let require0 ~baseuri = require_path (ng_path_of_baseuri baseuri)
let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
-
type timestamp =
[ `Obj of NUri.uri * NCic.obj
| `Constr of NCic.universe * NCic.universe] list *
let cache = ref NUri.UriMap.empty;;
let includes = ref [];;
+let get_already_included () = !includes;;
+
let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
let global_aliases = ref [] in
let rev_includes_map = ref NUri.UriMap.empty in
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
+ object
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 =
storage := sto; local_aliases := ali; cache := cac; includes := inc
;;
-let serialize ~baseuri dump =
- let ch = open_out (path_of_baseuri baseuri) in
- Marshal.to_channel ch (magic,dump) [];
+let serialize ~baseuri ~dependencies dump =
+ let ch = open_out (ng_path_of_baseuri baseuri) in
+ Marshal.to_channel ch (magic,(dependencies,dump)) [];
close_out ch;
List.iter
(function
| `Obj (uri,obj) ->
- let ch = open_out (path_of_baseuri uri) in
+ let ch = open_out (ng_path_of_baseuri uri) in
Marshal.to_channel ch (magic,obj) [];
close_out ch
| `Constr _ -> ()
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
+ object
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 -> dependencies:string list -> 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
+ val dependencies_of: baseuri:NUri.uri -> string list
+ 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 =
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
let require2 ~baseuri status =
try
includes := baseuri::!includes;
- let dump = require0 ~baseuri in
- List.fold_right !require1#run dump status
+ let _dependencies,dump = require0 ~baseuri in
+ List.fold_right !require1 dump status
with
Sys_error _ ->
- raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+ raise (IncludedFileNotCompiled(ng_path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+
+ let dependencies_of ~baseuri = fst (require0 ~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
let baseuris = get_deps baseuri in
List.iter (fun baseuri ->
remove_deps baseuri;
- HExtlib.safe_remove (path_of_baseuri baseuri);
- let basepath = path_of_baseuri ~no_suffix:true baseuri in
+ HExtlib.safe_remove (ng_path_of_baseuri baseuri);
+ let basepath = ng_path_of_baseuri ~no_suffix:true baseuri in
try
let od = Unix.opendir basepath in
let rec aux names =
projects / helm.git / blobdiff