(* *)
(*****************************************************************************)
+(* $Id$ *)
(* ************************************************************************** *
CicEnvironment SETTINGS (trust and clean_tmp)
let trust = ref (fun _ -> true);;
let set_trust f = trust := f
let trust_obj uri = !trust uri
-let debug_print = fun _ -> ()
+let debug_print = fun x -> prerr_endline (Lazy.force x)
(* ************************************************************************** *
TYPES
;;
exception AlreadyCooked of string;;
-exception CircularDependency of string;;
+exception CircularDependency of string Lazy.t;;
exception CouldNotFreeze of string;;
exception CouldNotUnfreeze of string;;
exception Object_not_found of UriManager.uri;;
val find_or_add_to_unchecked :
UriManager.uri ->
get_object_to_add:
- (UriManager.uri -> Cic.obj * CicUniv.universe_graph option) ->
- Cic.obj * CicUniv.universe_graph
+ (UriManager.uri ->
+ Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option) ->
+ Cic.obj * CicUniv.universe_graph * CicUniv.universe list
val can_be_cooked:
UriManager.uri -> bool
val unchecked_to_frozen :
val frozen_to_cooked :
uri:UriManager.uri -> unit
val hack_univ:
- UriManager.uri -> CicUniv.universe_graph -> unit
+ UriManager.uri -> CicUniv.universe_graph * CicUniv.universe list -> unit
val find_cooked :
- key:UriManager.uri -> Cic.obj * CicUniv.universe_graph
+ key:UriManager.uri ->
+ Cic.obj * CicUniv.universe_graph * CicUniv.universe list
val add_cooked :
- key:UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
+ key:UriManager.uri ->
+ (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
val remove: UriManager.uri -> unit
val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
(* unchecked is used to store objects just fetched, nothing more. *)
let unchecked_list = ref [];;
- (* FIXED: should be ok even if not touched *)
- (* used to hash cons uris on restore to grant URI structure unicity *)
- let restore_uris =
- let module C = Cic in
- let recons uri =
- UriManager.uri_of_string (UriManager.string_of_uri uri)
- in
- let rec restore_in_term =
- function
- (C.Rel _) as t -> t
- | C.Var (uri,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) ->(recons uri,restore_in_term t))
- exp_named_subst
- in
- C.Var (uri',exp_named_subst')
- | C.Meta (i,l) ->
- let l' =
- List.map
- (function
- None -> None
- | Some t -> Some (restore_in_term t)
- ) l
- in
- C.Meta(i,l')
- | C.Sort (C.Type u) ->
- CicUniv.assert_univ u;
- C.Sort (C.Type (CicUniv.recons_univ u))
- | C.Sort _ as t -> t
- | C.Implicit _ as t -> t
- | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
- | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
- | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)
- | C.LetIn (n,s,t) -> C.LetIn (n, restore_in_term s, restore_in_term t)
- | C.Appl l -> C.Appl (List.map restore_in_term l)
- | C.Const (uri,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
- in
- C.Const (uri',exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
- in
- C.MutInd (uri',tyno,exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let uri' = recons uri in
- let exp_named_subst' =
- List.map
- (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
- in
- C.MutConstruct (uri',tyno,consno,exp_named_subst')
- | C.MutCase (uri,i,outty,t,pl) ->
- C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t,
- List.map restore_in_term pl)
- | C.Fix (i, fl) ->
- let len = List.length fl in
- let liftedfl =
- List.map
- (fun (name, i, ty, bo) ->
- (name, i, restore_in_term ty, restore_in_term bo))
- fl
- in
- C.Fix (i, liftedfl)
- | C.CoFix (i, fl) ->
- let len = List.length fl in
- let liftedfl =
- List.map
- (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo))
- fl
- in
- C.CoFix (i, liftedfl)
- in
- function
- C.Constant (name,bo,ty,params,attrs) ->
- let bo' =
- match bo with
- None -> None
- | Some bo -> Some (restore_in_term bo)
- in
- let ty' = restore_in_term ty in
- let params' = List.map recons params in
- C.Constant (name, bo', ty', params',attrs)
- | C.CurrentProof (name,conjs,bo,ty,params,attrs) ->
- let conjs' =
- List.map
- (function (i,hyps,ty) ->
- (i,
- List.map (function
- None -> None
- | Some (name,C.Decl t) ->
- Some (name,C.Decl (restore_in_term t))
- | Some (name,C.Def (bo,ty)) ->
- let ty' =
- match ty with
- None -> None
- | Some ty'' -> Some (restore_in_term ty'')
- in
- Some (name,C.Def (restore_in_term bo, ty'))) hyps,
- restore_in_term ty))
- conjs
- in
- let bo' = restore_in_term bo in
- let ty' = restore_in_term ty in
- let params' = List.map recons params in
- C.CurrentProof (name, conjs', bo', ty', params',attrs)
- | C.Variable (name,bo,ty,params,attrs) ->
- let bo' =
- match bo with
- None -> None
- | Some bo -> Some (restore_in_term bo)
- in
- let ty' = restore_in_term ty in
- let params' = List.map recons params in
- C.Variable (name, bo', ty', params',attrs)
- | C.InductiveDefinition (tl,params,paramsno,attrs) ->
- let params' = List.map recons params in
- let tl' =
- List.map (function (name, inductive, ty, constructors) ->
- name,
- inductive,
- restore_in_term ty,
- (List.map
- (function (name, ty) -> name, restore_in_term ty)
- constructors))
- tl
- in
- C.InductiveDefinition (tl', params', paramsno, attrs)
- ;;
-
let empty () =
HT.clear cacheOfCookedObjects;
unchecked_list := [] ;
*)
empty ();
HT.iter
- (fun k (v,u) ->
+ (fun k (v,u,l) ->
callback (UriManager.string_of_uri k);
+ let reconsed_entry =
+ CicUtil.rehash_obj v,
+ CicUniv.recons_graph u,
+ List.map CicUniv.recons_univ l
+ in
HT.add cacheOfCookedObjects
- (UriManager.uri_of_string (UriManager.string_of_uri k))
- (***********************************************
- TSSI: FIXME add channel stuff for universes
- ************************************************)
- (restore_uris v, CicUniv.recons_graph u))
+ (UriManager.uri_of_string (UriManager.string_of_uri k))
+ reconsed_entry)
restored
;;
let find_or_add_to_unchecked uri ~get_object_to_add =
try
- let o,g = List.assq uri !unchecked_list in
- match g with
+ 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' -> o,g'
+ | None -> o,CicUniv.empty_ugraph,[]
+ | Some (g,l) -> o,g,l
with
Not_found ->
if List.mem_assq uri !frozen_list then
let univ = if o = None then "NO_UNIV" else "" in
print_endline (su^" "^univ))
!frozen_list;
- raise (CircularDependency (UriManager.string_of_uri uri))
+ raise (CircularDependency (lazy (UriManager.string_of_uri uri)))
end
else
if HT.mem cacheOfCookedObjects uri then
raise (AlreadyCooked (UriManager.string_of_uri uri))
else
(* OK, it is not already frozen nor cooked *)
- let obj,ugraph = get_object_to_add uri in
- let ugraph_real =
- match ugraph with
+ 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 -> g
+ None -> CicUniv.empty_ugraph, []
+ | Some ((g,l) as g_and_l) -> g_and_l
in
- unchecked_list := (uri,(obj,ugraph))::!unchecked_list ;
- obj,ugraph_real
+ unchecked_list :=
+ (uri,(obj,ugraph_and_univlist))::!unchecked_list ;
+ obj, ugraph_real, univlist_real
;;
let unchecked_to_frozen uri =
try
- let obj,ugraph = List.assq uri !unchecked_list in
+ let obj,ugraph_and_univlist = List.assq uri !unchecked_list in
unchecked_list := List.remove_assq uri !unchecked_list ;
- frozen_list := (uri,(obj,ugraph))::!frozen_list
+ frozen_list := (uri,(obj,ugraph_and_univlist))::!frozen_list
with
Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
;;
*************************************************************)
let frozen_to_cooked ~uri =
try
- let obj,ugraph = List.assq uri !frozen_list in
- match ugraph with
- None ->
- assert false (* only NON dummy universes can be committed *)
- | Some g ->
- CicUniv.assert_univs_have_uri g;
- frozen_list := List.remove_assq uri !frozen_list ;
- HT.add cacheOfCookedObjects uri (obj,g)
+ 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))
+ Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
;;
let can_be_cooked uri =
try
- let obj,ugraph = List.assq uri !frozen_list in
+ 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 with
- None -> false
- | Some _ -> true
+ match ugraph_and_univlist with
+ None -> false
+ | Some _ -> true
with
- Not_found -> false
+ Not_found -> false
;;
(* this function injects a real universe graph in a (uri, (obj, None))
* FIXME: another thing to remove if univ generation phase and lib
* exportation are unified.
*)
- let hack_univ uri real_ugraph =
+ let hack_univ uri (real_ugraph, real_univlist) =
try
- let o,g = List.assq uri !frozen_list in
- match g with
- None ->
- frozen_list := List.remove_assoc uri !frozen_list;
- frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
- | Some g ->
- debug_print (
- "You are probably hacking an object already hacked or an"^
- " object that has the universe file but is not"^
- " yet committed.");
- assert false
+ 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 (
- "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
+ 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) =
- HT.add cacheOfCookedObjects uri (obj,ugraph)
+ let add_cooked ~key:uri (obj,ugraph,univlist) =
+ HT.add cacheOfCookedObjects uri (obj,ugraph,univlist)
;;
(* invariant
if !frozen_list <> [] then
failwith "CicEnvironment.remove while type checking"
else
- HT.remove cacheOfCookedObjects uri
+ begin
+ HT.remove cacheOfCookedObjects uri;
+ unchecked_list :=
+ List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
+ end
;;
let list_all_cooked_uris () =
else
None
in
- (* restarts the numbering of named universes (the ones inside the cic) *)
- let _ = CicUniv.restart_numbering () in
let obj =
try
let time = Unix.gettimeofday() in
raise (Object_not_found (UriManager.uri_of_string uri))
| _ -> raise exn)
in
- let ugraph,filename_univ =
- (* FIXME: decomment this when the universes will be part of the library
+ let ugraph_and_univlist,filename_univ =
try
let filename_univ =
- Http_getter.getxml' (
- UriManager.uri_of_string (
- (UriManager.string_of_uri uri) ^ ".univ"))
+ let univ_uri = UriManager.univgraphuri_of_uri uri in
+ Http_getter.getxml' univ_uri
in
- (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
- with Failure s ->
-
- debug_print (
- "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
- Inix.unlink
- None,None
- *)
- (**********************************************
- TASSI: should fail when universes will be ON
- ***********************************************)
- (Some CicUniv.empty_ugraph,None)
+ Some (CicUniv.ugraph_and_univlist_of_xml filename_univ),
+ Some filename_univ
+ with
+ | Http_getter_types.Key_not_found _
+ | 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
in
- obj,ugraph
+ 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=None) uri =
+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 (
+ 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).");
+ "(can happen only in the fase of universes graphs generation)."));
assert false
else
*)
- match Cache.can_be_cooked uri, replace_ugraph with
+ match Cache.can_be_cooked uri, replace_ugraph_and_univlist with
| true, Some _
| false, None ->
- debug_print (
+ 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");
+ "proper arguments"));
assert false
| _ ->
- (match replace_ugraph with
+ (match replace_ugraph_and_univlist with
| None -> ()
- | Some g -> Cache.hack_univ uri g);
+ | Some g_and_l -> Cache.hack_univ uri g_and_l);
Cache.frozen_to_cooked uri
;;
* return the object,ugraph
*)
let add_trusted_uri_to_cache uri =
- let o,u = find_or_add_to_unchecked uri in
+ let _ = find_or_add_to_unchecked uri in
Cache.unchecked_to_frozen uri;
set_type_checking_info uri;
try
;;
(* get the uri, if we trust it will be added to the cacheOfCookedObjects *)
-let get_cooked_obj ?(trust=true) base_univ uri =
+let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
try
(* the object should be in the cacheOfCookedObjects *)
- let o,u = Cache.find_cooked uri in
- o,(CicUniv.merge_ugraphs base_univ u)
+ let o,u,l = Cache.find_cooked uri in
+ o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),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 = add_trusted_uri_to_cache uri in
- o,(CicUniv.merge_ugraphs base_univ u)
+ let o,u,l = add_trusted_uri_to_cache uri in
+ o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
else
(* we don't trust the uri, so we fail *)
begin
- debug_print ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
+ debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
raise Not_found
end
+
+let get_cooked_obj ?trust base_ugraph uri =
+ 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
*
* as the get_cooked_obj but returns a type_checked_obj
*
*)
-let is_type_checked ?(trust=true) base_univ uri =
+let is_type_checked ?(trust=true) base_ugraph uri =
try
- let o,u = Cache.find_cooked uri in
- CheckedObj (o,(CicUniv.merge_ugraphs base_univ u))
+ let o,u,_ = Cache.find_cooked uri in
+ CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)))
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 u base_univ )
+ let o,u,_ = add_trusted_uri_to_cache uri in
+ CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
else
- let o,u = find_or_add_to_unchecked uri in
+ let o,u,_ = find_or_add_to_unchecked uri in
Cache.unchecked_to_frozen uri;
UncheckedObj o
;;
(* as the get cooked, but if not present the object is only fetched,
* not unfreezed and committed
*)
-let get_obj base_univ uri =
+let get_obj base_ugraph uri =
try
(* the object should be in the cacheOfCookedObjects *)
- let o,u = Cache.find_cooked uri in
- o,(CicUniv.merge_ugraphs base_univ u)
+ let o,u,_ = Cache.find_cooked uri in
+ 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_univ u)
+ let o,u,_ = find_or_add_to_unchecked uri in
+ o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
;;
let in_cache uri =
Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
-let add_type_checked_obj uri (obj,ugraph) =
- Cache.add_cooked ~key:uri (obj,ugraph)
+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
(list_uri ())
with
Not_found ->
- debug_print "Who has removed the uri in the meanwhile?";
+ debug_print (lazy "Who has removed the uri in the meanwhile?");
raise Not_found
;;
projects / helm.git / blobdiff