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
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
in
let rec restore_in_term =
function
- (C.Rel _) as t -> t
+ | (C.Rel _) as t -> t
| C.Var (uri,exp_named_subst) ->
let uri' = recons uri in
let exp_named_subst' =
*)
empty ();
HT.iter
- (fun k (v,u) ->
+ (fun k (v,u,l) ->
callback (UriManager.string_of_uri k);
+ let reconsed_entry =
+ restore_uris 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
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 (lazy (
- "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 (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"^
+ 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
+ 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
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 ->
-
+ 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)));
- Inix.unlink
- None,None
- *)
- (**********************************************
- TASSI: should fail when universes will be ON
- ***********************************************)
- (Some CicUniv.empty_ugraph,None)
+ (* 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 (lazy (
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 (lazy (
"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 o,u,_ = 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_univ 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_univ u),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_univ u),l
else
(* we don't trust the uri, so we fail *)
begin
debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
raise Not_found
end
+
+let get_cooked_obj ?trust base_univ uri =
+ let o,g,_ = get_cooked_obj_with_univlist ?trust base_univ uri in
+ o,g
(* This has not the old semantic :( but is what the name suggests
*
*)
let is_type_checked ?(trust=true) base_univ uri =
try
- let o,u = Cache.find_cooked uri in
+ let o,u,_ = Cache.find_cooked uri in
CheckedObj (o,(CicUniv.merge_ugraphs base_univ u))
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
+ let o,u,_ = add_trusted_uri_to_cache uri in
CheckedObj ( o, CicUniv.merge_ugraphs u base_univ )
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
;;
let get_obj base_univ uri =
try
(* the object should be in the cacheOfCookedObjects *)
- let o,u = Cache.find_cooked uri in
+ let o,u,_ = Cache.find_cooked uri in
o,(CicUniv.merge_ugraphs base_univ u)
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
+ let o,u,_ = find_or_add_to_unchecked uri in
o,(CicUniv.merge_ugraphs base_univ u)
;;
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
let rec aux = function
| C.Const (u,exp_named_subst)
| C.Var (u,exp_named_subst) when is_not_visited u ->
+ aux_uri u;
visited u;
- aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u));
List.iter (fun (_,t) -> aux t) exp_named_subst
| C.Const (u,exp_named_subst)
| C.Var (u,exp_named_subst) ->
List.iter (fun (_,t) -> aux t) exp_named_subst
| C.Meta (n,l1) ->
List.iter (fun t -> match t with Some t' -> aux t' | _ -> ()) l1
- | C.Sort ( C.Type i) -> add_result i
+ | C.Sort ( C.Type i) -> add_result [i]
| C.Rel _
| C.Sort _
| C.Implicit _ -> ()
aux ty; aux te; (List.iter (fun t -> aux t) patterns)
| C.Fix (no, funs) -> List.iter (fun (_,_,b,c) -> aux b; aux c) funs
| C.CoFix (no,funs) -> List.iter (fun (_,b,c) -> aux b; aux c) funs
+ | _ -> ()
+ and aux_uri u =
+ if is_not_visited u then
+ let _, _, l =
+ CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in
+ add_result l
and aux_obj = function
| C.Constant (_,Some te,ty,v,_)
| C.Variable (_,Some te,ty,v,_) ->
aux te;
aux ty;
- List.iter
- (fun u ->
- if is_not_visited u then
- (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
- v
+ List.iter aux_uri v
| C.Constant (_,None, ty, v,_)
| C.Variable (_,None, ty, v,_) ->
aux ty;
- List.iter
- (fun u ->
- if is_not_visited u then
- (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
- v
+ List.iter aux_uri v
| C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
| C.InductiveDefinition (l,v,_,_) ->
List.iter
aux t;
List.iter (fun (_,t) -> aux t) l')
l;
- List.iter
- (fun u ->
- if is_not_visited u then
- (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
- v
+ List.iter aux_uri v
in
aux_obj t;
- !results
+ List.flatten !results
+
+let rec list_uniq = function
+ | [] -> []
+ | h::[] -> [h]
+ | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl)
+ | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
+let list_uniq l =
+ list_uniq (List.fast_sort CicUniv.compare l)
+
let clean_and_fill uri obj ugraph =
let list_of_universes = universes_of_obj uri obj in
+ let list_of_universes = list_uniq list_of_universes in
let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
- let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
- ugraph
+ let ugraph, list_of_universes =
+ CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri
+ in
+ ugraph, list_of_universes
projects / helm.git / commitdiff