From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 12 May 2008 21:41:02 +0000 (+0000)
Subject: trust implemented, but in the nCicTypeChecker!
X-Git-Tag: make_still_working~5231
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=32522cf70b6bc38f0c3cc5d25b9bd1a93f05862f;p=helm.git

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 28aeb16c8..350d2e6f2 100644
--- 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 041cf4615..33d3e86cf 100644
--- 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 021d321a1..b13edc540 100644
--- 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