Interface improvement (???): the Check button has been moved to a brand new

[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 d48ff09bdaa5af533b192c1d304db212d948fc45..e9050cd8c1867ac6f0686abc2094facedfabcd9f 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -37,9 +37,7 @@
 
 let cleanup_tmp = true;;
 
-let never_trust = function uri -> false;;
-let always_trust = function uri -> true;;
-let trust_obj = ref never_trust;;
+let trust_obj = function uri -> true;;
 
 type type_checked_obj =
    CheckedObj of Cic.obj     (* cooked obj *)
@@ -153,7 +151,7 @@ let find_or_add_unchecked_to_cache uri =
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
-      let obj = CicParser.obj_of_xml filename bodyfilename uri in
+      let obj = CicParser.obj_of_xml filename bodyfilename in
        if cleanup_tmp then
         begin
          Unix.unlink filename ;
@@ -169,7 +167,6 @@ let find_or_add_unchecked_to_cache uri =
 (* must be called once the type-checking of uri is finished *)
 (* The object whose uri is uri is unfreezed                 *)
 let set_type_checking_info uri =
- trust_obj := never_trust ;
  Cache.frozen_to_cooked uri
 ;;
 
@@ -179,39 +176,42 @@ let set_type_checking_info uri =
 (* otherwise it freezes the term for type-checking and returns
  it *)
 (* set_type_checking_info must be called to unfreeze the term         *)
-let is_type_checked uri =
+let is_type_checked ?(trust=true) uri =
  try
   CheckedObj (Cache.find_cooked uri)
  with
   Not_found ->
    let obj = find_or_add_unchecked_to_cache uri in
     Cache.unchecked_to_frozen uri ;
-    if !trust_obj uri then
+    if trust && trust_obj uri then
      begin
       Logger.log (`Trusting uri) ;
       set_type_checking_info uri ;
-      trust_obj := always_trust ;
       CheckedObj (Cache.find_cooked uri)
      end
     else
-     begin
-      trust_obj := always_trust ;
-      UncheckedObj obj
-     end
+     UncheckedObj obj
 ;;
 
-(* get_cooked_obj uri                                                        *)
-(* returns the cooked cic object whose uri is uri. The term must be present  *)
-(* and cooked in cache                                                       *)
-let get_cooked_obj uri =
+(* 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) *)
+(* Otherwise it raises Not_found                                    *)
+let get_cooked_obj ?(trust=true) uri =
  try
   Cache.find_cooked uri
  with Not_found ->
-  if not (!trust_obj uri) then
-   prerr_endline ("@@@ OOOOOOOPS: WE TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE SHOULD NOT DO THAT! THAT MEANS LOOKING FOR TROUBLES ;-(") ;
-  match is_type_checked uri with
-     CheckedObj obj -> obj
-   | _ -> assert false
+  if trust && trust_obj uri then
+   begin
+    match is_type_checked uri with
+       CheckedObj obj -> obj
+     | _ -> assert false
+   end
+  else
+   begin
+    prerr_endline ("@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^ ") raises Not_found since the object is not type-checked nor trusted.") ;
+    raise Not_found
+   end
 ;;
 
 (* get_obj uri                                                                *)