From 502eecdd0e3d63c7e1a647c633b588e738f0afcf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 24 Jan 2005 16:17:33 +0000 Subject: [PATCH] - renamed Term_not_found exception (useless) with Object_not_found (now used) - added getter exception handling. Now, hopefully, we will no longer see Pxp_types.At exception, but more meaningful ones (like Object_not_found) - added in_libary which checks if an object exists (either in cache or via getter) - in_cache: removed old debugging messages --- .../cic_proof_checking/cicEnvironment.ml | 28 +++++++++---------- .../cic_proof_checking/cicEnvironment.mli | 9 ++++-- 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 7845818b7..461c3edc6 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -59,7 +59,7 @@ exception AlreadyCooked of string;; exception CircularDependency of string;; exception CouldNotFreeze of string;; exception CouldNotUnfreeze of string;; -exception Term_not_found of UriManager.uri;; +exception Object_not_found of UriManager.uri;; (* ************************************************************************** * @@ -508,7 +508,10 @@ let get_object_to_add uri = CicParser.obj_of_xml filename bodyfilename with exn -> cleanup (); - raise 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,filename_univ = (* FIXME: decomment this when the universes will be part of the library @@ -653,18 +656,8 @@ let put_inductive_definition 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 in_cache uri = + Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri let add_type_checked_term uri (obj,ugraph) = match obj with @@ -674,5 +667,12 @@ let add_type_checked_term uri (obj,ugraph) = assert false ;; +let in_library uri = + in_cache uri || + (try + ignore (Http_getter.resolve' uri); + true + with Http_getter_types.Key_not_found _ -> false) + let remove_term = Cache.remove diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 9875f52ac..77f97ed96 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -37,10 +37,11 @@ (****************************************************************************) exception CircularDependency of string;; -exception Term_not_found of UriManager.uri;; +exception Object_not_found of UriManager.uri;; (* as the get cooked, but if not present the object is only fetched, * not unfreezed and committed + * @raise Object_not_found *) val get_obj : CicUniv.universe_graph -> UriManager.uri -> @@ -115,7 +116,11 @@ val empty : unit -> unit (** Set trust function. Per default this function is set to (fun _ -> true) *) val set_trust: (UriManager.uri -> bool) -> unit -(* for filtering in tacticChaser *) + (** @return true for objects currently cooked/frozend/unchecked, false + * otherwise (i.e. objects already parsed from XML) *) val in_cache : UriManager.uri -> bool + (** @return true for objects available in the library *) +val in_library: UriManager.uri -> bool + (* EOF *) -- 2.39.2