(* 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) *) (* *) (*****************************************************************************) (* ************************************************************************** * 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 (* ************************************************************************** * 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;; exception CouldNotFreeze of string;; exception CouldNotUnfreeze of string;; exception Term_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 option) -> Cic.obj * CicUniv.universe_graph 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 -> unit val find_cooked : key:UriManager.uri -> Cic.obj * CicUniv.universe_graph val add_cooked : key:UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> 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 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 [];; (* 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 _ 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) -> 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') | C.CurrentProof (name,conjs,bo,ty,params) -> 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') | C.Variable (name,bo,ty,params) -> 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') | C.InductiveDefinition (tl,params,paramsno) -> 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) ;; 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 -> callback (UriManager.string_of_uri k); HT.add cacheOfCookedObjects (UriManager.uri_of_string (UriManager.string_of_uri k)) (*********************************************** TSSI: FIXME add channel stuff for universes ************************************************) ((restore_uris v),CicUniv.empty_ugraph)) 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 jet 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 = List.assq uri !unchecked_list in match g 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' 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 (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 = get_object_to_add uri in let ugraph_real = match ugraph with (* FIXME: not sure it is OK*) None -> CicUniv.empty_ugraph | Some g -> g in unchecked_list := (uri,(obj,ugraph))::!unchecked_list ; obj,ugraph_real ;; let unchecked_to_frozen uri = try let obj,ugraph = List.assq uri !unchecked_list in unchecked_list := List.remove_assq uri !unchecked_list ; frozen_list := (uri,(obj,ugraph))::!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 = List.assq uri !frozen_list in match ugraph with None -> assert false (* only NON dummy universes can be committed *) | Some g -> frozen_list := List.remove_assq uri !frozen_list ; HT.add cacheOfCookedObjects uri (obj,g) with Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri)) ;; let can_be_cooked uri = try let obj,ugraph = 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 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 = 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 -> prerr_endline ( "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 -> prerr_endline ( "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) ;; (* 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 (!unchecked_list <> []) || (!frozen_list <> []) then failwith "CicEnvironment.remove while type checking" else HT.remove cacheOfCookedObjects uri ;; 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 get_object_to_add uri = let filename = Http_getter.getxml' uri in let bodyfilename = match UriManager.bodyuri_of_uri uri with None -> None | Some bodyuri -> try ignore (Http_getter.resolve' bodyuri) ; (* The body exists ==> it is not an axiom *) Some (Http_getter.getxml' bodyuri) with Http_getter_types.Key_not_found _ -> (* The body does not exist ==> we consider it an axiom *) None in let cleanup () = Unix.unlink filename ; (* begin match filename_univ with Some f -> Unix.unlink f | None -> () end; *) begin match bodyfilename with Some f -> Unix.unlink f | None -> () end in (* this brakes something : * let _ = CicUniv.restart_numbering () in *) let obj = try CicParser.obj_of_xml filename bodyfilename with exn -> cleanup (); raise exn in let ugraph,filename_univ = (* FIXME: decomment this when the universes will be part of the library try let filename_univ = Http_getter.getxml' ( UriManager.uri_of_string ( (UriManager.string_of_uri uri) ^ ".univ")) in (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ) with Failure s -> prerr_endline ( "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) in cleanup(); obj,ugraph ;; (* 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=None) uri = if Cache.can_be_cooked uri && replace_ugraph <> None then invalid_arg ( "?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)."); if not (Cache.can_be_cooked uri) && replace_ugraph = None then invalid_arg ( "?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"); begin match replace_ugraph with None -> () | Some g -> Cache.hack_univ uri g end; 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 o,u = 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 ?(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) 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) else (* we don't trust the uri, so we fail *) begin prerr_endline ("CACHE MISS: " ^ (UriManager.string_of_uri uri)); raise Not_found end (* 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 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... *) if trust_obj uri then (* trusting we add it to the unchecked list *) let o,u = find_or_add_to_unchecked uri in o,(CicUniv.merge_ugraphs base_univ u) else raise Not_found ;; exception OnlyPutOfInductiveDefinitionsIsAllowed let put_inductive_definition uri (obj,ugraph) = match obj with Cic.InductiveDefinition _ -> Cache.add_cooked uri (obj,ugraph) | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed ;; let in_cache uri = if Cache.is_in_cooked uri then (prerr_endline "TROVATO NELLA CHECKED";true) else if Cache.is_in_frozen uri then (prerr_endline "TROVATO NELLA FROZEN";true) else if Cache.is_in_unchecked uri then (prerr_endline "TROVATO NELLA UNCHECKED";true) else (prerr_endline ("NON TROVATO:" ^ (UriManager.string_of_uri uri) );false) ;; let add_type_checked_term uri (obj,ugraph) = match obj with Cic.Constant (s,(Some bo),ty,ul) -> Cache.add_cooked ~key:uri (obj,ugraph) | _ -> assert false ;; let remove_term = Cache.remove