;;
let time0 = [],[];;
-let storage = ref [];;
-let local_aliases = ref [];;
let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
let global_aliases = ref [] in
let init = load_db;;
+type db = {
+ storage :
+ [ `Obj of NUri.uri * NCic.obj
+ | `Constr of NCic.universe * NCic.universe] list ref;
+ local_aliases :
+ (NUri.uri * string * NReference.reference) list ref
+}
+
+class type g_status =
+ object
+ method lib_db : db
+ end
+
class virtual status uid =
object
- inherit NCic.status uid
+ inherit NCicEnvironment.status uid
+
+ val lib_db = {
+ storage = ref [];
+ local_aliases = ref []
+ }
+ method lib_db = lib_db
+
val timestamp = (time0 : timestamp)
method timestamp = timestamp
+
method set_timestamp v = {< timestamp = v >}
+ method set_lib_db v = {< lib_db = v >}
+ method set_lib_status : 's.#g_status as 's -> 'self
+ = fun o -> {< lib_db = o#lib_db >}
end
-let time_travel0 (sto,ali) =
- let diff_len = List.length !storage - List.length sto in
- let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in
+let reset_timestamp st =
+ st#lib_db.storage := [];
+ st#lib_db.local_aliases := []
+;;
+
+let time_travel0 st (sto,ali) =
+ let diff_len = List.length !(st#lib_db.storage) - List.length sto in
+ let to_be_deleted,_ = HExtlib.split_nth diff_len !(st#lib_db.storage) in
if List.length to_be_deleted > 0 then
- List.iter NCicEnvironment.invalidate_item to_be_deleted;
- storage := sto; local_aliases := ali
+ List.iter (NCicEnvironment.invalidate_item st) to_be_deleted;
+ st#lib_db.storage := sto; st#lib_db.local_aliases := ali
;;
-let time_travel status = time_travel0 status#timestamp;;
+let time_travel status = time_travel0 status status#timestamp;;
type obj = string * Obj.t
(* includes are transitively closed; dependencies are only immediate *)
end
(* uid = None --> single user mode *)
-class dumpable_status =
+class dumpable_status uid =
object
+ inherit NCicPp.status uid
+ inherit status uid
+
val db = { objs = []; includes = []; dependencies = [] }
method dump = db
method set_dump v = {< db = v >}
type 'a register_type =
'a ->
refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
- refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+ refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
alias_only:bool ->
dumpable_status -> dumpable_status
end
module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
- val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s ->
- string option end) =
+ val set: dumpable_s -> dumpable_status -> dumpable_s (*val user : dumpable_s ->
+ string option*) end) =
struct
type dumpable_status = D.dumpable_s
type 'a register_type =
'a ->
refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
- refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+ refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
alias_only:bool ->
dumpable_status -> dumpable_status
end
let serialize ~baseuri status =
- let ch = open_out (ng_path_of_baseuri (D.user status) baseuri) in
+ let ch = open_out (ng_path_of_baseuri (D.get status)#user baseuri) in
Marshal.to_channel ch (magic,((D.get status)#dump.dependencies,(D.get status)#dump.objs)) [];
close_out ch;
+ let deps = String.concat ", " ((D.get status)#dump.dependencies) in
+ prerr_endline ("dumping dependencies:\n" ^ deps ^ "\nend of deps");
List.iter
(function
| `Obj (uri,obj) ->
- let ch = open_out (ng_path_of_baseuri (D.user status) uri) in
+ let ch = open_out (ng_path_of_baseuri (D.get status)#user uri) in
Marshal.to_channel ch (magic,obj) [];
close_out ch
| `Constr _ -> ()
- ) !storage;
- set_global_aliases (!local_aliases @ get_global_aliases ());
+ ) !((D.get status)#lib_db.storage);
+ set_global_aliases (!((D.get status)#lib_db.local_aliases) @ get_global_aliases ());
List.iter (fun u -> add_deps u [baseuri]) (D.get status)#dump.includes;
- time_travel0 time0
+ reset_timestamp (D.get status)
let require2 ~baseuri ~alias_only status =
try
(s#set_dump
{s#dump with
includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in
- let _dependencies,dump = require0 (D.user status) ~baseuri in
+ let _dependencies,dump = require0 (D.get status)#user ~baseuri in
List.fold_right (!require1 ~alias_only) dump status
with
Sys_error _ ->
- raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.user status) baseuri,NUri.string_of_uri baseuri))
+ raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.get status)#user baseuri,NUri.string_of_uri baseuri))
let dependencies_of user ~baseuri = fst (require0 user ~baseuri)
refresh_uri_in_obj status obj
;;
-let resolve name =
+let resolve st name =
try
HExtlib.filter_map
(fun (_,name',nref) -> if name'=name then Some nref else None)
- (!local_aliases @ get_global_aliases ())
+ (!(st#lib_db.local_aliases) @ get_global_aliases ())
with
Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
;;
-let aliases_of uri =
+let aliases_of st uri =
HExtlib.filter_map
(fun (uri',_,nref) ->
- if NUri.eq uri' uri then Some nref else None) !local_aliases
+ if NUri.eq uri' uri then Some nref else None) !(st#lib_db.local_aliases)
;;
let add_obj status ((u,_,_,_,_) as obj) =
NCicEnvironment.check_and_add_obj status obj;
- storage := (`Obj (u,obj))::!storage;
+ status#lib_db.storage := (`Obj (u,obj))::!(status#lib_db.storage);
let _,height,_,_,obj = obj in
let references =
match obj with
(NReference.Ind (inductive,i,leftno))]
) il)
in
- local_aliases := references @ !local_aliases;
- status#set_timestamp (!storage,!local_aliases)
+ status#lib_db.local_aliases := references @ !(status#lib_db.local_aliases);
+ status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases))
;;
let add_constraint status u1 u2 =
if
List.exists
(function `Constr (u1',u2') when u1=u1' && u2=u2' -> true | _ -> false)
- !storage
+ !(status#lib_db.storage)
then
(*CSC: raise an exception here! *)
(prerr_endline "CANNOT ADD A CONSTRAINT TWICE"; assert false);
- NCicEnvironment.add_lt_constraint u1 u2;
- storage := (`Constr (u1,u2)) :: !storage;
- status#set_timestamp (!storage,!local_aliases)
+ NCicEnvironment.add_lt_constraint status u1 u2;
+ status#lib_db.storage := (`Constr (u1,u2)) :: !(status#lib_db.storage);
+ status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases))
;;
let get_obj status u =
+(*
try
List.assq u
(HExtlib.filter_map
(function `Obj (u,o) -> Some (u,o) | _ -> None )
- !storage)
- with Not_found ->
+ !(status#lib_db.storage))
+ with Not_found ->*)
try fetch_obj (status#user) status u
with Sys_error _ ->
raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
;;
-NCicEnvironment.set_get_obj get_obj;;
+NCicEnvironment.set_get_obj
+ (get_obj :> NCicEnvironment.status -> NUri.uri -> NCic.obj);;
projects / helm.git / blobdiff