trust implemented, but in the nCicTypeChecker!

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 28aeb16c8da1b338fd93bcd3e5b66dc80c227eff..350d2e6f20ffff098f2d4c2e2a68f4e7d7422a03 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -31,7 +31,10 @@ let logger =
       | `Type_checking_failed s ->
           decr indent;
           if debug then
-           prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s))
+           prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s)
+      | `Trust_obj s ->
+          if debug then
+           prerr_endline (do_indent () ^ "Trust: " ^ NUri.string_of_uri s))
 ;;
 
 let _ =

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 041cf4615e433e915fd371030359a61af6f39e27..33d3e86cfad7d693d8b372b990d0fc243b8f1cc3 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1047,10 +1047,17 @@ let typecheck_obj (uri,height,metasenv,subst,kind) =
         ) fl dfl
 ;;
 
+(* trust *)
+
+let trust = ref  (fun _ -> true);;
+let set_trust f = trust := f
+let trust_obj obj = !trust obj
+
+
 (* web interface stuff *)
 
 let logger = 
- ref (function (`Start_type_checking _|`Type_checking_completed _|`Type_checking_interrupted _|`Type_checking_failed _) -> ())
+ ref (function (`Start_type_checking _|`Type_checking_completed _|`Type_checking_interrupted _|`Type_checking_failed _|`Trust_obj _) -> ())
 ;;
 
 let set_logger f = logger := f;;
@@ -1070,6 +1077,13 @@ let typecheck_obj obj =
      raise e
 ;;
 
-E.set_typecheck_obj typecheck_obj;;
+E.set_typecheck_obj
+ (fun obj ->
+   if trust_obj obj then
+    let u,_,_,_,_ = obj in
+     !logger (`Trust_obj u)
+   else
+    typecheck_obj obj)
+;;
 
 (* EOF *)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli
index 021d321a1fa686aa7ba2fb7146682f3216498b89..b13edc5408e5518e615ba8ddd80d9e15bf542c38 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.mli
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli
@@ -18,8 +18,11 @@ val set_logger:
    | `Type_checking_completed of NUri.uri
    | `Type_checking_interrupted of NUri.uri
    | `Type_checking_failed of NUri.uri
+   | `Trust_obj of NUri.uri
    ] -> unit) -> unit
 
+val set_trust : (NCic.obj -> bool) -> unit
+
 (* typechecks the object, raising an exception if illtyped *)
 val typecheck_obj : NCic.obj -> unit