X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicEnvironment.ml;h=fde76a60b2882f17a85ab060c9a25f5500535518;hb=887916a4791bba656b1dec730d3315239d3c1f21;hp=9875f17f6f722b7c5674a018cba684ab378e616a;hpb=92ff0c811f55b37004e2ee45dff0859c31857128;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml index 9875f17f6..fde76a60b 100644 --- a/helm/software/components/cic_proof_checking/cicEnvironment.ml +++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml @@ -53,9 +53,8 @@ let debug_print = if debug then fun x -> prerr_endline (Lazy.force x) else ignor * ************************************************************************** *) 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;; @@ -82,15 +81,14 @@ module Cache : 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 @@ -146,7 +144,9 @@ module Cache : let invalidate _ = let l = HT.fold (fun k (o,g,gl) acc -> (k,(o,Some (g,gl)))::acc) cacheOfCookedObjects [] in - unchecked_list := l ; + 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; ;; @@ -209,17 +209,7 @@ module Cache : 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 @@ -243,15 +233,8 @@ module Cache : 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 = @@ -263,70 +246,14 @@ module Cache : 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) = @@ -405,8 +332,7 @@ let get_object_to_add uri = | 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) @@ -424,41 +350,26 @@ let find_or_add_to_unchecked 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 ;; @@ -485,20 +396,6 @@ 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 - * - * 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,l = Cache.find_cooked uri in @@ -510,9 +407,9 @@ let is_type_checked ?(trust=true) base_ugraph 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, @@ -521,12 +418,14 @@ let is_type_checked ?(trust=true) base_ugraph uri = let get_obj base_ugraph uri = 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*))) + 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,l = find_or_add_to_unchecked uri in - o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))) + 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 =