X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;fp=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=22845725ac05e983aec69d23bc133bd5265e2274;hp=0000000000000000000000000000000000000000;hb=792b5d29ebae8f917043d9dd226692919b5d6ca1;hpb=a14a8c7637fd0b95e9d4deccb20c6abc98e8f953 diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml new file mode 100644 index 000000000..22845725a --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -0,0 +1,545 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 24/01/2000 *) +(* *) +(* This module implements a trival cache system (an hash-table) for cic *) +(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml) *) +(* *) +(*****************************************************************************) + +(* $Id$ *) + +(* ************************************************************************** * + CicEnvironment SETTINGS (trust and clean_tmp) + * ************************************************************************** *) + +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) + +(* ************************************************************************** * + TYPES + * ************************************************************************** *) + +type type_checked_obj = + CheckedObj of (Cic.obj * CicUniv.universe_graph) (* cooked obj *) + | UncheckedObj of Cic.obj (* uncooked obj to proof-check *) +;; + +exception AlreadyCooked of string;; +exception CircularDependency of string Lazy.t;; +exception CouldNotFreeze of string;; +exception CouldNotUnfreeze of string;; +exception Object_not_found of UriManager.uri;; + + +(* ************************************************************************** * + HERE STARTS THE CACHE MODULE + * ************************************************************************** *) + +(* I think this should be the right place to implement mecanisms and + * invasriants + *) + +(* Cache that uses == instead of = for testing equality *) +(* Invariant: an object is always in at most one of the *) +(* following states: unchecked, frozen and cooked. *) +module Cache : + sig + val find_or_add_to_unchecked : + UriManager.uri -> + get_object_to_add: + (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 : + UriManager.uri -> unit + val frozen_to_cooked : + uri:UriManager.uri -> unit + val hack_univ: + UriManager.uri -> CicUniv.universe_graph * CicUniv.universe list -> unit + val find_cooked : + key:UriManager.uri -> + Cic.obj * CicUniv.universe_graph * CicUniv.universe list + val add_cooked : + 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 + val empty : unit -> unit + val is_in_frozen: UriManager.uri -> bool + val is_in_unchecked: UriManager.uri -> bool + val is_in_cooked: UriManager.uri -> bool + val list_all_cooked_uris: unit -> UriManager.uri list + end += + struct + (************************************************************************* + TASSI: invariant + The cacheOfCookedObjects will contain only objects with a valid universe + graph. valid means that not None (used if there is no universe file + in the universe generation phase). + **************************************************************************) + + (* DATA: the data structure that implements the CACHE *) + module HashedType = + struct + type t = UriManager.uri + let equal = UriManager.eq + let hash = Hashtbl.hash + end + ;; + + module HT = Hashtbl.Make(HashedType);; + + let cacheOfCookedObjects = HT.create 1009;; + + (* DATA: The parking lists + * the lists elements are (uri * (obj * universe_graph option)) + * ( u, ( o, None )) means that the object has no universes file, this + * should happen only in the universe generation phase. + * FIXME: if the universe generation is integrated in the library + * exportation phase, the 'option' MUST be removed. + * ( u, ( o, Some g)) means that the object has a universes file, + * the usual case. + *) + + (* frozen is used to detect circular dependency. *) + let frozen_list = ref [];; + (* unchecked is used to store objects just fetched, nothing more. *) + let unchecked_list = ref [];; + + let empty () = + HT.clear cacheOfCookedObjects; + unchecked_list := [] ; + frozen_list := [] + ;; + + (* FIX: universe stuff?? *) + let dump_to_channel ?(callback = ignore) oc = + HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri)) + cacheOfCookedObjects; + Marshal.to_channel oc cacheOfCookedObjects [] + ;; + + (* FIX: universes stuff?? *) + let restore_from_channel ?(callback = ignore) ic = + let restored = Marshal.from_channel ic in + (* FIXME: should this empty clean the frozen and unchecked? + * if not, the only-one-empty-end-not-3 patch is wrong + *) + empty (); + HT.iter + (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)) + reconsed_entry) + restored + ;; + + + let is_in_frozen uri = + List.mem_assoc uri !frozen_list + ;; + + let is_in_unchecked uri = + List.mem_assoc uri !unchecked_list + ;; + + let is_in_cooked uri = + HT.mem cacheOfCookedObjects uri + ;; + + + (******************************************************************* + TASSI: invariant + we need, in the universe generation phase, to traverse objects + that are not yet committed, so we search them in the frozen list. + Only uncommitted objects without a universe file (see the assertion) + can be searched with method + *******************************************************************) + + 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 + 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"; + 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)) + !frozen_list; + raise (CircularDependency (lazy (UriManager.string_of_uri uri))) + end + else + if HT.mem cacheOfCookedObjects uri then + (* DOUBLE COOK DETECTED, raise the exception *) + raise (AlreadyCooked (UriManager.string_of_uri uri)) + 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 + ;; + + let unchecked_to_frozen uri = + try + let obj,ugraph_and_univlist = List.assq uri !unchecked_list in + unchecked_list := List.remove_assq uri !unchecked_list ; + frozen_list := (uri,(obj,ugraph_and_univlist))::!frozen_list + with + 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 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 + ;; + + (* 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) = + HT.add cacheOfCookedObjects uri (obj,ugraph,univlist) + ;; + + (* invariant + * + * an object can be romeved from the cache only if we are not typechecking + * something. this means check and frozen must be empty. + *) + let remove uri = + if !frozen_list <> [] then + failwith "CicEnvironment.remove while type checking" + else + begin + HT.remove cacheOfCookedObjects uri; + unchecked_list := + List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list + end + ;; + + let list_all_cooked_uris () = + HT.fold (fun u _ l -> u::l) cacheOfCookedObjects [] + ;; + + end +;; + +(* ************************************************************************ + HERE ENDS THE CACHE MODULE + * ************************************************************************ *) + +(* exported cache functions *) +let dump_to_channel = Cache.dump_to_channel;; +let restore_from_channel = Cache.restore_from_channel;; +let empty = Cache.empty;; + +let total_parsing_time = ref 0.0 + +let get_object_to_add uri = + try + let filename = Http_getter.getxml' uri in + let bodyfilename = + match UriManager.bodyuri_of_uri uri with + None -> None + | Some bodyuri -> + if Http_getter.exists' bodyuri then + Some (Http_getter.getxml' bodyuri) + else + None + in + let obj = + try + let time = Unix.gettimeofday() in + let rc = CicParser.obj_of_xml uri filename bodyfilename in + total_parsing_time := + !total_parsing_time +. ((Unix.gettimeofday()) -. time ); + rc + with exn -> + (match exn with + | CicParser.Getter_failure ("key_not_found", uri) -> + raise (Object_not_found (UriManager.uri_of_string uri)) + | _ -> raise exn) + in + let ugraph_and_univlist,filename_univ = + try + let filename_univ = + let univ_uri = UriManager.univgraphuri_of_uri uri in + Http_getter.getxml' univ_uri + in + 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_and_univlist + with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri) +;; + +(* this is the function to fetch the object in the unchecked list and + * nothing more (except returning it) + *) +let find_or_add_to_unchecked uri = + Cache.find_or_add_to_unchecked uri ~get_object_to_add + +(* set_type_checking_info uri *) +(* must be called once the type-checking of uri is finished *) +(* The object whose uri is uri is unfreezed *) +(* *) +(* 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 +;; + +(* 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 + Cache.unchecked_to_frozen uri; + set_type_checking_info uri; + try + Cache.find_cooked uri + with Not_found -> assert false +;; + +(* get the uri, if we trust it will be added to the cacheOfCookedObjects *) +let get_cooked_obj_with_univlist ?(trust=true) base_univ uri = + try + (* the object should be in the cacheOfCookedObjects *) + 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,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) 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_univ uri = + try + 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 + CheckedObj ( o, CicUniv.merge_ugraphs u base_univ ) + else + 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 = + try + (* the object should be in the cacheOfCookedObjects *) + 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 + 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,univlist) = + Cache.add_cooked ~key:uri (obj,ugraph,univlist) + +let in_library uri = in_cache uri || Http_getter.exists' uri + +let remove_obj = Cache.remove + +let list_uri () = + Cache.list_all_cooked_uris () +;; + +let list_obj () = + try + List.map (fun u -> + let o,ug = get_obj CicUniv.empty_ugraph u in + (u,o,ug)) + (list_uri ()) + with + Not_found -> + debug_print (lazy "Who has removed the uri in the meanwhile?"); + raise Not_found +;;