CicEnvironment SETTINGS (trust and clean_tmp)
* ************************************************************************** *)
+let debug = false;;
let cleanup_tmp = true;;
let trust = ref (fun _ -> true);;
let set_trust f = trust := f
let trust_obj uri = !trust uri
-let debug_print = fun x -> prerr_endline (Lazy.force x)
+let debug_print = if debug then fun x -> prerr_endline (Lazy.force x) else ignore
(* ************************************************************************** *
TYPES
* ************************************************************************** *)
type type_checked_obj =
- CheckedObj of (Cic.obj * CicUniv.universe_graph) (* cooked obj *)
- | UncheckedObj of Cic.obj (* uncooked obj to proof-check *)
-;;
+ | CheckedObj of (Cic.obj * CicUniv.universe_graph)
+ | UncheckedObj of Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
exception AlreadyCooked of string;;
exception CircularDependency of string Lazy.t;;
get_object_to_add:
(UriManager.uri ->
Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option) ->
- Cic.obj * CicUniv.universe_graph * CicUniv.universe list
+ Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
val can_be_cooked:
UriManager.uri -> bool
val unchecked_to_frozen :
UriManager.uri -> unit
val frozen_to_cooked :
- uri:UriManager.uri -> unit
- val hack_univ:
- UriManager.uri -> CicUniv.universe_graph * CicUniv.universe list -> unit
+ uri:UriManager.uri ->
+ Cic.obj -> CicUniv.universe_graph -> CicUniv.universe list -> unit
val find_cooked :
key:UriManager.uri ->
Cic.obj * CicUniv.universe_graph * CicUniv.universe list
val is_in_unchecked: UriManager.uri -> bool
val is_in_cooked: UriManager.uri -> bool
val list_all_cooked_uris: unit -> UriManager.uri list
+ val invalidate: unit -> unit
end
=
struct
(* unchecked is used to store objects just fetched, nothing more. *)
let unchecked_list = ref [];;
+ let invalidate _ =
+ let l = HT.fold (fun k (o,g,gl) acc -> (k,(o,Some (g,gl)))::acc) cacheOfCookedObjects [] in
+ unchecked_list :=
+ HExtlib.list_uniq ~eq:(fun (x,_) (y,_) -> UriManager.eq x y)
+ (List.sort (fun (x,_) (y,_) -> UriManager.compare x y) (l @ !unchecked_list));
+ frozen_list := [];
+ HT.clear cacheOfCookedObjects;
+ ;;
+
let empty () =
HT.clear cacheOfCookedObjects;
unchecked_list := [] ;
let find_or_add_to_unchecked uri ~get_object_to_add =
try
- let o,g_and_l = List.assq uri !unchecked_list in
- match g_and_l with
- (* FIXME: we accept both cases, as at the end of this function
- * maybe the None universe outside the cache module should be
- * avoided elsewhere.
- *
- * another thing that should be removed if univ generation phase
- * and lib exportation are unified.
- *)
- | None -> o,CicUniv.empty_ugraph,[]
- | Some (g,l) -> o,g,l
+ List.assq uri !unchecked_list
with
Not_found ->
if List.mem_assq uri !frozen_list then
(* CIRCULAR DEPENDENCY DETECTED, print the error and raise *)
begin
- print_endline "\nCircularDependency!\nfrozen list: \n";
+(*
+ prerr_endline "\nCircularDependency!\nfrozen list: \n";
List.iter (
fun (u,(_,o)) ->
let su = UriManager.string_of_uri u in
let univ = if o = None then "NO_UNIV" else "" in
- print_endline (su^" "^univ))
+ prerr_endline (su^" "^univ))
!frozen_list;
+*)
raise (CircularDependency (lazy (UriManager.string_of_uri uri)))
end
else
else
(* OK, it is not already frozen nor cooked *)
let obj,ugraph_and_univlist = get_object_to_add uri in
- let ugraph_real, univlist_real =
- match ugraph_and_univlist with
- (* FIXME: not sure it is OK*)
- None -> CicUniv.empty_ugraph, []
- | Some ((g,l) as g_and_l) -> g_and_l
- in
- unchecked_list :=
- (uri,(obj,ugraph_and_univlist))::!unchecked_list ;
- obj, ugraph_real, univlist_real
+ unchecked_list := (uri,(obj,ugraph_and_univlist))::!unchecked_list;
+ obj, ugraph_and_univlist
;;
let unchecked_to_frozen uri =
Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
;;
-
- (************************************************************
- TASSI: invariant
- only object with a valid universe graph can be committed
-
- this should disappear if the universe generation phase and the
- library exportation are unified.
- *************************************************************)
- let frozen_to_cooked ~uri =
- try
- let obj,ugraph_and_univlist = List.assq uri !frozen_list in
- match ugraph_and_univlist with
- | None -> assert false (* only NON dummy universes can be committed *)
- | Some (g,l) ->
- CicUniv.assert_univs_have_uri g l;
- frozen_list := List.remove_assq uri !frozen_list ;
- HT.add cacheOfCookedObjects uri (obj,g,l)
- with
- Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
+ let frozen_to_cooked ~uri o ug ul =
+ CicUniv.assert_univs_have_uri ug ul;
+ frozen_list := List.remove_assq uri !frozen_list ;
+ HT.add cacheOfCookedObjects uri (o,ug,ul)
;;
- let can_be_cooked uri =
- try
- let obj,ugraph_and_univlist = List.assq uri !frozen_list in
- (* FIXME: another thing to remove if univ generation phase and lib
- * exportation are unified.
- *)
- match ugraph_and_univlist with
- None -> false
- | Some _ -> true
- with
- Not_found -> false
- ;;
+ let can_be_cooked uri = List.mem_assq uri !frozen_list;;
- (* this function injects a real universe graph in a (uri, (obj, None))
- * element of the frozen list.
- *
- * FIXME: another thing to remove if univ generation phase and lib
- * exportation are unified.
- *)
- let hack_univ uri (real_ugraph, real_univlist) =
- try
- let o,ugraph_and_univlist = List.assq uri !frozen_list in
- match ugraph_and_univlist with
- None ->
- frozen_list := List.remove_assoc uri !frozen_list;
- frozen_list :=
- (uri,(o,Some (real_ugraph, real_univlist)))::!frozen_list;
- | Some g ->
- debug_print (lazy (
- "You are probably hacking an object already hacked or an"^
- " object that has the universe file but is not"^
- " yet committed."));
- assert false
- with
- Not_found ->
- debug_print (lazy (
- "You are hacking an object that is not in the"^
- " frozen_list, this means you are probably generating an"^
- " universe file for an object that already"^
- " as an universe file"));
- assert false
- ;;
-
let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;;
let add_cooked ~key:uri (obj,ugraph,univlist) =
match UriManager.bodyuri_of_uri uri with
None -> None
| Some bodyuri ->
- if Http_getter.exists' bodyuri then
+ if Http_getter.exists' ~local:false bodyuri then
Some (Http_getter.getxml' bodyuri)
else
None
| Http_getter_types.Unresolvable_URI _ ->
debug_print (lazy (
"WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
- (* WE SHOULD FAIL (or return None, None *)
- Some (CicUniv.empty_ugraph, []), None
+ None, None
in
obj, ugraph_and_univlist
with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
(* *)
(* the replacement ugraph must be the one returned by the *)
(* typechecker, restricted with the CicUnivUtils.clean_and_fill *)
-let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri =
-(*
- if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
- debug_print (lazy (
- "?replace_ugraph must be None if you are not committing an "^
- "object that has a universe graph associated "^
- "(can happen only in the fase of universes graphs generation)."));
- assert false
- else
-*)
- match Cache.can_be_cooked uri, replace_ugraph_and_univlist with
- | true, Some _
- | false, None ->
- debug_print (lazy (
- "?replace_ugraph must be (Some ugraph) when committing an object that "^
- "has no associated universe graph. If this is in make_univ phase you "^
- "should drop this exception and let univ_make commit thi object with "^
- "proper arguments"));
- assert false
- | _ ->
- (match replace_ugraph_and_univlist with
- | None -> ()
- | Some g_and_l -> Cache.hack_univ uri g_and_l);
- Cache.frozen_to_cooked uri
+let set_type_checking_info uri (o,ug,ul) =
+ if not (Cache.can_be_cooked uri) then assert false
+ else
+ Cache.frozen_to_cooked ~uri o ug ul
;;
(* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and
* return the object,ugraph
*)
let add_trusted_uri_to_cache uri =
- let _ = find_or_add_to_unchecked uri in
+ let o,u_and_ul = find_or_add_to_unchecked uri in
Cache.unchecked_to_frozen uri;
- set_type_checking_info uri;
- try
- Cache.find_cooked uri
+ let u,ul =
+ match u_and_ul with
+ (* for backward compat with Coq *)
+ | None -> CicUniv.empty_ugraph, []
+ | Some (ug,ul) -> ug, ul
+ in
+ set_type_checking_info uri (o,u,ul);
+ try Cache.find_cooked uri
with Not_found -> assert false
;;
try
(* the object should be in the cacheOfCookedObjects *)
let o,u,l = Cache.find_cooked uri in
- o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
+ o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
with Not_found ->
(* this should be an error case, but if we trust the uri... *)
if trust && trust_obj uri then
(* trusting means that we will fetch cook it on the fly *)
let o,u,l = add_trusted_uri_to_cache uri in
- o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
+ o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
else
(* we don't trust the uri, so we fail *)
begin
let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in
o,g
-(* This has not the old semantic :( but is what the name suggests
- *
- * let is_type_checked ?(trust=true) uri =
- * try
- * let _ = Cache.find_cooked uri in
- * true
- * with
- * Not_found ->
- * trust && trust_obj uri
- * ;;
- *
- * as the get_cooked_obj but returns a type_checked_obj
- *
- *)
let is_type_checked ?(trust=true) base_ugraph uri =
try
- let o,u,_ = Cache.find_cooked uri in
- CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)))
+ let o,u,l = Cache.find_cooked uri in
+ CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))))
with Not_found ->
(* this should return UncheckedObj *)
if trust && trust_obj uri then
(* trusting means that we will fetch cook it on the fly *)
- let o,u,_ = add_trusted_uri_to_cache uri in
- CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+ let o,u,l = add_trusted_uri_to_cache uri in
+ CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
else
- let o,u,_ = find_or_add_to_unchecked uri in
+ let o,u_and_ul = find_or_add_to_unchecked uri in
Cache.unchecked_to_frozen uri;
- UncheckedObj o
+ UncheckedObj (o,u_and_ul)
;;
(* as the get cooked, but if not present the object is only fetched,
try
(* the object should be in the cacheOfCookedObjects *)
let o,u,_ = Cache.find_cooked uri in
- o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+ o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)
with Not_found ->
(* this should be an error case, but if we trust the uri... *)
- let o,u,_ = find_or_add_to_unchecked uri in
- o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+ let o,u_and_l = find_or_add_to_unchecked uri in
+ match u_and_l with
+ | None -> o, base_ugraph
+ | Some (ug,_) -> o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(ug,uri)
;;
let in_cache uri =
let add_type_checked_obj uri (obj,ugraph,univlist) =
Cache.add_cooked ~key:uri (obj,ugraph,univlist)
-let in_library uri = in_cache uri || Http_getter.exists' uri
+let in_library uri = in_cache uri || Http_getter.exists' ~local:false uri
let remove_obj = Cache.remove
debug_print (lazy "Who has removed the uri in the meanwhile?");
raise Not_found
;;
+
+let invalidate _ =
+ Cache.invalidate ()
+;;
projects / helm.git / blobdiff