X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=0c5c9c01e9030259fff0591ca2a43260e347a84a;hb=a785a3526d4dcbb6c5810ed4fb943132c9ff2d45;hp=22138dde8d1eee672f46385db7bc68f9428c29d7;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 22138dde8..0c5c9c01e 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -37,7 +37,9 @@
 
 let cleanup_tmp = true;;
 
-let trust_obj = function uri -> 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     (* cooked obj *)
@@ -49,6 +51,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 *)
@@ -62,6 +65,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
@@ -74,6 +78,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
@@ -102,6 +107,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 =
@@ -288,7 +299,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;;
@@ -303,28 +319,39 @@ let find_or_add_unchecked_to_cache uri =
  Cache.find_or_add_unchecked uri
   ~get_object_to_add:
    (function () ->
-     let filename = Getter.getxml uri in
+     let filename = Http_getter.getxml' uri in
      let bodyfilename =
       match UriManager.bodyuri_of_uri uri with
          None -> None
        | Some bodyuri ->
           try
-           ignore (Getter.resolve bodyuri) ;
+           ignore (Http_getter.resolve' bodyuri) ;
            (* The body exists ==> it is not an axiom *)
-           Some (Getter.getxml bodyuri)
+           Some (Http_getter.getxml' bodyuri)
           with
-           Getter.Unresolved ->
+           Http_getter_types.Key_not_found _ ->
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
-      let obj = CicParser.obj_of_xml filename bodyfilename in
+     let cleanup () =
        if cleanup_tmp then
         begin
-         Unix.unlink filename ;
+         if Sys.file_exists filename then Unix.unlink filename ;
          match bodyfilename with
-            Some f -> Unix.unlink f
+            Some f -> if Sys.file_exists f then Unix.unlink f
           | None -> ()
         end ;
+      in
+      CicUniv.directly_to_env_begin ();
+      let obj =
+        try
+          CicParser.obj_of_xml filename bodyfilename
+        with exn ->
+          cleanup ();
+          raise exn
+      in
+      CicUniv.directly_to_env_end ();
+      cleanup ();
        obj
    )
 ;;
@@ -399,3 +426,20 @@ let put_inductive_definition uri obj =
     Cic.InductiveDefinition _ -> Cache.add_cooked uri obj
   | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
 ;;
+
+let in_cache uri = 
+ try
+  ignore (Cache.find_cooked uri);true
+ with Not_found -> false
+;;
+
+let add_type_checked_term uri obj =
+  match obj with 
+  Cic.Constant (s,(Some bo),ty,ul) ->
+    Cache.add_cooked ~key:uri obj
+  | _ -> assert false 
+  Cache.add_cooked 
+;;
+
+let remove_term = Cache.remove
+