From f945768c2bdd355b394f1c4606727283504fbb54 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Oct 2004 12:34:30 +0000 Subject: [PATCH] - ported to new getter API - implemented remove_term --- .../cic_proof_checking/cicEnvironment.ml | 21 +++++++++++++++++-- .../cic_proof_checking/cicEnvironment.mli | 6 ++++++ 2 files changed, 25 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index d214d89b5..77d2252eb 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -50,6 +50,7 @@ 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 *) @@ -63,6 +64,7 @@ module Cache : uri:UriManager.uri -> unit val find_cooked : key:UriManager.uri -> Cic.obj val add_cooked : key:UriManager.uri -> Cic.obj -> 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 @@ -75,6 +77,7 @@ module Cache : val mem : UriManager.uri -> bool val find : UriManager.uri -> Cic.obj val add : UriManager.uri -> Cic.obj -> unit + val remove : UriManager.uri -> unit (** (de)serialization of type checker cache *) val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit @@ -103,6 +106,12 @@ module Cache : let add uri obj = HT.add hashtable uri obj ;; + 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 = @@ -289,7 +298,12 @@ module Cache : ;; let find_cooked ~key:uri = CacheOfCookedObjects.find uri;; let add_cooked ~key:uri obj = CacheOfCookedObjects.add uri obj;; - + 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;; @@ -314,7 +328,7 @@ let find_or_add_unchecked_to_cache uri = (* The body exists ==> it is not an axiom *) Some (Http_getter.getxml' bodyuri) with - Http_getter_types.Unresolvable_URI _ -> + Http_getter_types.Key_not_found _ -> (* The body does not exist ==> we consider it an axiom *) None in @@ -425,3 +439,6 @@ let add_type_checked_term uri obj = | _ -> assert false Cache.add_cooked ;; + +let remove_term = Cache.remove + diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index e3def568e..3e5c2bf77 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -36,6 +36,7 @@ (******************************************************************************) exception CircularDependency of string;; +exception Term_not_found of UriManager.uri;; (* get_obj uri *) (* returns the cic object whose uri is uri. If the term is not just in cache, *) @@ -64,6 +65,11 @@ val set_type_checking_info : UriManager.uri -> unit (* We need this in the Qed. *) val add_type_checked_term : UriManager.uri -> Cic.obj -> unit + (** remove a type checked term + * @raise Term_not_found when given term is not in the environment + * @raise Failure when remove_term is invoked while type checking *) +val remove_term: UriManager.uri -> unit + (* 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) *) -- 2.39.2