trust is always false by default

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index ec70116a211d6594149d2abe0b7ca36fb9e5a25f..25042b4cdf8b1d6aee7f82145cee50ac4d29a9ca 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -19,14 +19,6 @@ module U = NCicUtils
 module E = NCicEnvironment
 module PP = NCicPp
 
-(* web interface stuff *)
-
-let logger = 
-  ref (function (`Start_type_checking _|`Type_checking_completed _) -> ())
-;;
-
-let set_logger f = logger := f;;
-
 exception TypeCheckerFailure of string Lazy.t
 exception AssertFailure of string Lazy.t
 
@@ -731,7 +723,6 @@ and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args
 and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t = 
  let recursor f k t = U.fold shift_k k (fun k () -> f k) () t in
  let rec aux (context, recfuns, x as k) t = 
-  let t = R.whd ~delta:max_int ~subst context t in
 (*
    prerr_endline ("GB:\n" ^ 
      PP.ppcontext ~subst ~metasenv context^
@@ -971,17 +962,7 @@ and returns_a_coinductive ~subst context ty =
   | _ -> None
 
 and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = 
-  let cobj =
-    match E.get_obj uri with
-    | true, cobj -> cobj
-    | false, uobj ->
-       !logger (`Start_type_checking uri);
-       check_obj_well_typed uobj;
-       E.add_obj uobj;
-       !logger (`Type_checking_completed uri);
-       uobj
-  in
-  match cobj, ref with
+  match E.get_checked_obj uri, ref with
   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i)  ->
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
@@ -993,8 +974,9 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
       arity
   | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty
   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
+;;
 
-and check_obj_well_typed (uri,height,metasenv,subst,kind) =
+let typecheck_obj (uri,height,metasenv,subst,kind) =
  (* CSC: here we should typecheck the metasenv and the subst *)
  assert (metasenv = [] && subst = []);
  match kind with
@@ -1063,7 +1045,45 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
                raise (TypeCheckerFailure
                 (lazy "CoFix: not guarded by constructors"))
         ) fl dfl
+;;
+
+(* trust *)
+
+let trust = ref  (fun _ -> false);;
+let set_trust f = trust := f
+let trust_obj obj = !trust obj
 
-let typecheck_obj = check_obj_well_typed;;
+
+(* web interface stuff *)
+
+let logger = 
+ ref (function (`Start_type_checking _|`Type_checking_completed _|`Type_checking_interrupted _|`Type_checking_failed _|`Trust_obj _) -> ())
+;;
+
+let set_logger f = logger := f;;
+
+let typecheck_obj obj =
+ let u,_,_,_,_ = obj in
+ try
+  !logger (`Start_type_checking u);
+  typecheck_obj obj;
+  !logger (`Type_checking_completed u)
+ with
+    Sys.Break as e ->
+     !logger (`Type_checking_interrupted u);
+     raise e
+  | e ->
+     !logger (`Type_checking_failed u);
+     raise e
+;;
+
+E.set_typecheck_obj
+ (fun obj ->
+   if trust_obj obj then
+    let u,_,_,_,_ = obj in
+     !logger (`Trust_obj u)
+   else
+    typecheck_obj obj)
+;;
 
 (* EOF *)