X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicEnvironment.ml;h=fde76a60b2882f17a85ab060c9a25f5500535518;hb=d2d20cd33c42d0897765387042c3779109bbf4fd;hp=1f6789e76895156311b0cc7470f89fb1b8fb7813;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml index 1f6789e76..fde76a60b 100644 --- a/helm/software/components/cic_proof_checking/cicEnvironment.ml +++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml @@ -41,20 +41,20 @@ 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;; @@ -81,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 @@ -104,6 +103,7 @@ module Cache : 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 @@ -142,6 +142,15 @@ module Cache : (* 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 := [] ; @@ -200,29 +209,21 @@ 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 (* 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 @@ -232,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 = @@ -252,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) = @@ -363,7 +301,7 @@ let get_object_to_add uri = 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 @@ -394,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) @@ -413,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 ;; @@ -456,13 +378,13 @@ let get_cooked_obj_with_univlist ?(trust=true) 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 + 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 @@ -474,34 +396,20 @@ 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,_ = 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, @@ -511,11 +419,13 @@ 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_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 = @@ -524,7 +434,7 @@ 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 @@ -543,3 +453,7 @@ let list_obj () = debug_print (lazy "Who has removed the uri in the meanwhile?"); raise Not_found ;; + +let invalidate _ = + Cache.invalidate () +;;