let magic = 2;;
+let prerr_endline _ = ()
+
let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
let refresh_uri_in_universe =
NCicUntrusted.map_obj_kind (refresh_uri_in_term status) obj_kind
;;
-let ng_path_of_baseuri ?(no_suffix=false) baseuri =
+let ng_path_of_baseuri ?(no_suffix=false) user baseuri =
let uri = NUri.string_of_uri baseuri in
let path = String.sub uri 4 (String.length uri - 4) in
+ let path = match user with
+ | Some u -> "/" ^ u ^ path
+ | _ -> prerr_endline "WARNING: ng_path_of_baseuri called without a uid"; path
+ in
let path = Helm_registry.get "matita.basedir" ^ path in
let dirname = Filename.dirname path in
HExtlib.mkdir dirname;
dump
;;
-let require0 ~baseuri = require_path (ng_path_of_baseuri baseuri)
+let require0 user ~baseuri = require_path (ng_path_of_baseuri user baseuri)
-let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
+let db_path user =
+ let midpath = match user with
+ | None -> ""
+ | Some u -> "/" ^ u
+ in
+ Helm_registry.get "matita.basedir" ^ midpath ^ "/ng_db.ng";;
type timestamp =
[ `Obj of NUri.uri * NCic.obj
;;
let time0 = [],[];;
-let storage = ref [];;
-let local_aliases = ref [];;
+
+let global_aliases_db = ref [];;
+let rev_includes_map_db = ref [];;
+
+let global_aliases u =
+ try List.assoc u !global_aliases_db
+ with Not_found ->
+ let db = ref [] in
+ global_aliases_db := (u,db)::!global_aliases_db;
+ db
+;;
+
+let rev_includes_map u =
+ try List.assoc u !rev_includes_map_db
+ with Not_found ->
+ let db = ref NUri.UriMap.empty in
+ rev_includes_map_db := (u,db)::!rev_includes_map_db;
+ db
+;;
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 store_db () =
- let ch = open_out (db_path ()) in
- Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) [];
+ let store_db user =
+ let ch = open_out (db_path user) in
+ Marshal.to_channel ch (magic,(!(global_aliases user),!(rev_includes_map user))) [];
close_out ch in
- let load_db () =
+ let load_db user =
HExtlib.mkdir (Helm_registry.get "matita.basedir");
+ if user <> None then HExtlib.mkdir ((Helm_registry.get "matita.basedir") ^ "/" ^ HExtlib.unopt user);
try
- let ga,im = require_path (db_path ()) in
+ let ga,im = require_path (db_path user) in
let ga =
List.map
(fun (uri,name,NReference.Ref (uri2,spec)) ->
(fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im
) im NUri.UriMap.empty
in
- global_aliases := ga;
- rev_includes_map := im
+ global_aliases user := ga;
+ rev_includes_map user := im
with
Sys_error _ -> () in
- let get_deps u =
+ let get_deps user u =
let get_deps_one_step u =
- try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in
+ try NUri.UriMap.find u !(rev_includes_map user) with Not_found -> [] in
let rec aux res =
function
[] -> res
aux (he::res) (get_deps_one_step he @ tl)
in
aux [] [u] in
- let remove_deps u =
- rev_includes_map := NUri.UriMap.remove u !rev_includes_map;
- rev_includes_map :=
+ let remove_deps user u =
+ rev_includes_map user := NUri.UriMap.remove u !(rev_includes_map user);
+ rev_includes_map user :=
NUri.UriMap.map
- (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map;
- store_db ()
+ (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !(rev_includes_map user);
+ store_db user
in
load_db,
- (fun ga -> global_aliases := ga; store_db ()),
- (fun () -> !global_aliases),
- (fun u l ->
- rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map;
- store_db ()),
+ (fun user ga -> global_aliases user := ga; store_db user),
+ (fun user -> !(global_aliases user)),
+ (fun user u l ->
+ rev_includes_map user := NUri.UriMap.add u (l @ get_deps user u) !(rev_includes_map user);
+ store_db user),
get_deps,
remove_deps
;;
let init = load_db;;
-class virtual status =
+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
+ inherit NCicEnvironment.g_status
+ method lib_db : db
+ end
+
+class virtual status uid =
object
- inherit NCic.status
+ 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 print_timestamp () =
+ prerr_endline ("length(lib_db.storage) = " ^
+ string_of_int (List.length !(lib_db.storage)));
+ prerr_endline ("length(timestamp.storage) = " ^
+ string_of_int (List.length (fst 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 >}#set_env_status o
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) =
+ prerr_endline ("length of lib_db.storage = " ^ (string_of_int (List.length !(st#lib_db.storage))));
+ prerr_endline ("length of sto = " ^ (string_of_int (List.length sto)));
+ 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 *)
method dump: dump
end
-class dumpable_status =
+(* uid = None --> single user mode *)
+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
val require:
baseuri:NUri.uri -> fname:string -> alias_only:bool ->
dumpable_status -> dumpable_status
- val dependencies_of: baseuri:NUri.uri -> string list
+ val dependencies_of: string option -> baseuri:NUri.uri -> string list
end
-module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status val set: dumpable_s -> dumpable_status -> dumpable_s 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) =
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 status = D.get status in
- let ch = open_out (ng_path_of_baseuri baseuri) in
- Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) [];
+ 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 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 ());
- List.iter (fun u -> add_deps u [baseuri]) status#dump.includes;
- time_travel0 time0
+ ) !((D.get status)#lib_db.storage);
+ let user = D.user status in
+ set_global_aliases user (!((D.get status)#lib_db.local_aliases) @ get_global_aliases user);
+ List.iter (fun u -> add_deps (D.user status) u [baseuri]) (D.get status)#dump.includes;
+ 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 ~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 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 ~baseuri = fst (require0 ~baseuri)
+ let dependencies_of user ~baseuri = fst (require0 user ~baseuri)
let record_include =
let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
objs = record_include (baseuri,fname)::s#dump.objs })
end
-let fetch_obj status uri =
- let obj = require0 ~baseuri:uri in
+let fetch_obj user status uri =
+ let obj = require0 user ~baseuri:uri in
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 st#user)
with
- Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
+ Not_found ->
+ (prerr_endline ("can't resolve object " ^ name);
+ 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 ->
- try fetch_obj status u
+ !(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)))
+ (prerr_endline ("can't fetch object " ^ NUri.string_of_uri u);
+ 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