From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Oct 2004 12:34:30 +0000 (+0000)
Subject: - ported to new getter API
X-Git-Tag: V_0_0_10~37
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f945768c2bdd355b394f1c4606727283504fbb54;p=helm.git

- ported to new getter API
- implemented remove_term
---

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) *)