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
+ | _ -> 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 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;;
-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
+ 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 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 *)
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
assert (not (List.mem tag !already_registered));
already_registered := tag :: !already_registered;
let old_require1 = !require1 in
+ prerr_endline "let old_require 1 superata";
require1 :=
(fun ~alias_only ((tag',data) as x) ->
if tag=tag' then
+ (prerr_endline ("requiring tag': " ^ tag');
require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
- ~refresh_uri_in_reference ~alias_only
+ ~refresh_uri_in_reference ~alias_only)
else
old_require1 ~alias_only x);
+ prerr_endline ("added require tag" ^ tag);
(fun x -> tag,Obj.repr x)
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);
+ 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;
+ 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 ())
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 ->
- 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)))
;;
-NCicEnvironment.set_get_obj get_obj;;
+NCicEnvironment.set_get_obj
+ (get_obj :> NCicEnvironment.status -> NUri.uri -> NCic.obj);;
projects / helm.git / blobdiff