(* 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) *) (* *) (*****************************************************************************) let cleanup_tmp = true;; let trust = ref (fun _ -> true);; let set_trust f = trust := f let trust_obj uri = !trust uri 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;; (* 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_unchecked : UriManager.uri -> get_object_to_add:(unit -> 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 not_jet_cooked: UriManager.uri -> Cic.obj * CicUniv.universe_graph 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 end = struct (************************************************************************* TASSI: invariant The CacheOfCookedObjects will contain only objects with a valid universe graph. valid means that non None (used if there is no universe file in the universe generation phase). **************************************************************************) module CacheOfCookedObjects : sig val mem : UriManager.uri -> bool val find : UriManager.uri -> Cic.obj * CicUniv.universe_graph val add : UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit val remove : UriManager.uri -> unit (** (de)serialization of type checker cache *) val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit val empty : unit -> unit end = struct module HashedType = struct type t = UriManager.uri let equal = UriManager.eq let hash = Hashtbl.hash end ;; module HT = Hashtbl.Make(HashedType);; let hashtable = HT.create 1009;; let mem uri = try HT.mem hashtable uri with Not_found -> false ;; let find uri = HT.find hashtable uri ;; let add uri (obj,ugraph) = HT.add hashtable uri (obj,ugraph) ;; let remove uri = if mem uri then HT.remove hashtable uri else raise (Term_not_found uri); ;; (* 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 dump_to_channel ?(callback = ignore) oc = HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri)) hashtable; Marshal.to_channel oc hashtable [] ;; let empty () = HT.clear hashtable ;; let restore_from_channel ?(callback = ignore) ic = let restored = Marshal.from_channel ic in empty (); HT.iter (fun k v -> callback (UriManager.string_of_uri k); HT.add hashtable (UriManager.uri_of_string (UriManager.string_of_uri k)) (************************************************ TASSI: FIXME add channel stuff for universes *************************************************) ((restore_uris v),CicUniv.empty_ugraph)) restored ;; end ;; let frozen_list = ref [];; let unchecked_list = ref [];; let is_in_frozen uri = List.mem_assoc uri !frozen_list ;; let is_in_unchecked uri = List.mem_assoc uri !unchecked_list ;; (******************************************************************* 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 not_jet_cooked uri = try let o,u = List.assoc uri !frozen_list in match u with None -> o, CicUniv.empty_ugraph | Some _ -> assert false (* only univ_maker ca use this *) with Not_found -> CacheOfCookedObjects.find uri ;; let find_or_add_unchecked uri ~get_object_to_add = try let o,g = List.assq uri !unchecked_list in match g with None -> o,CicUniv.empty_ugraph | Some g' -> o,g' with Not_found -> if List.mem_assq uri !frozen_list then 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 CacheOfCookedObjects.mem uri then raise (AlreadyCooked (UriManager.string_of_uri uri)) else (* OK, it is not already frozen nor cooked *) let obj,ugraph = get_object_to_add () in let ugraph_real = match ugraph with 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 *************************************************************) 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 ; CacheOfCookedObjects.add 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 match ugraph with None -> false | Some _ -> true with Not_found -> false ;; 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"^ " jet 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 = CacheOfCookedObjects.find uri;; let add_cooked ~key:uri (obj,ugraph) = CacheOfCookedObjects.add uri (obj,ugraph);; let remove uri = if (!unchecked_list <> []) || (!frozen_list <> []) then failwith "CicEnvironment.remove while type checking" else CacheOfCookedObjects.remove uri ;; let dump_to_channel = CacheOfCookedObjects.dump_to_channel;; let restore_from_channel = CacheOfCookedObjects.restore_from_channel;; let empty () = CacheOfCookedObjects.empty (); unchecked_list := [] ; frozen_list := [] ;; end ;; let dump_to_channel = Cache.dump_to_channel;; let restore_from_channel = Cache.restore_from_channel;; let empty = Cache.empty;; let find_or_add_unchecked_to_cache uri = Cache.find_or_add_unchecked uri ~get_object_to_add: (function () -> 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 (* maybe this is not the right place to do this.. but I think obj_of_xml is called only here *) (* this brakes something : let _ = CicUniv.restart_numbering () in *) let obj = CicParser.obj_of_xml filename bodyfilename in let ugraph,filename_univ = (* 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)); None,None *) (********************************************** TASSI: should fail when universes will be ON ***********************************************) (Some CicUniv.empty_ugraph,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 cleanup(); obj,ugraph) ;; (* set_type_checking_info uri *) (* must be called once the type-checking of uri is finished *) (* The object whose uri is uri is unfreezed *) 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 an no 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 ;; (* is_type_checked uri *) (* CSC: commento falso ed obsoleto *) (* returns a CheckedObj if the term has been type-checked *) (* otherwise it freezes the term for type-checking and returns it *) (* set_type_checking_info must be called to unfreeze the term *) let is_type_checked ?(trust=true) uri base_univ = try let o,u = Cache.find_cooked uri in CheckedObj (o,CicUniv.merge_ugraphs u base_univ) with Not_found -> let obj,ugraph = find_or_add_unchecked_to_cache uri in Cache.unchecked_to_frozen uri ; if trust && trust_obj uri then begin CicLogger.log (`Trusting uri) ; set_type_checking_info uri ; let o,u = Cache.find_cooked uri in let u' = CicUniv.merge_ugraphs base_univ ugraph in CheckedObj (o,u') end else begin UncheckedObj obj end ;; (* get_cooked_obj ~trust uri *) (* returns the object if it is already type-checked or if it can be *) (* trusted (if [trust] = true and the trusting function accepts it) *) (* Otherwise it raises Not_found *) let get_cooked_obj ?(trust=true) uri base_univ = try let o,u = Cache.find_cooked uri in o,(CicUniv.merge_ugraphs base_univ u) with Not_found -> if trust && trust_obj uri then begin match is_type_checked uri base_univ with CheckedObj (obj,ugraph) -> obj,(CicUniv.merge_ugraphs ugraph base_univ) | _ -> assert false end else begin prerr_endline ( "@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^ ") raises Not_found since the object is not type-checked"^ " nor trusted."); raise Not_found end ;; (* get_obj uri *) (* returns the cic object whose uri is uri. If the term is not just in cache,*) (* then it is parsed via CicParser.term_of_xml from the file whose name is *) (* the result of Getter.getxml uri *) let get_obj ?(not_jet_cooked=false) uri base_univ = if not_jet_cooked then let o,u = Cache.not_jet_cooked uri in o,(CicUniv.merge_ugraphs base_univ u) else try get_cooked_obj uri base_univ with Not_found -> let s = ( UriManager.string_of_uri uri) in let o,u = find_or_add_unchecked_to_cache uri in o,(CicUniv.merge_ugraphs base_univ u) ;; 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 = try ignore (Cache.find_cooked uri); prerr_endline "TROVATO NELLA CHECKED";true with Not_found -> 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