ported debian stuff to ocaml 3.08

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 3a201ad696b387222cde6a466f62004425e0cc17..e15186fdecdb489f437d50c91bbad63b3e54e00c 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -38,6 +38,7 @@
 let cleanup_tmp = true;;
 
 let trust_obj = function uri -> true;;
+(*let trust_obj = function uri -> false;;*)
 
 type type_checked_obj =
    CheckedObj of Cic.obj     (* cooked obj *)
@@ -129,7 +130,7 @@ module Cache :
              in
               C.Meta(i,l')
           | C.Sort _ as t -> t
-          | C.Implicit 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)
@@ -303,21 +304,23 @@ 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.Unresolvable_URI _ ->
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
+      CicUniv.directly_to_env_begin ();
       let obj = CicParser.obj_of_xml filename bodyfilename in
+      CicUniv.directly_to_env_end ();
        if cleanup_tmp then
         begin
          Unix.unlink filename ;
@@ -399,3 +402,17 @@ 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 
+;;