From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 12 Dec 2008 12:08:16 +0000 (+0000)
Subject: better error message, functions to clear various caches used during translation of... 
X-Git-Tag: make_still_working~4416
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f551aa5900d5c756eb48cea751c032b3bcbcf37;p=helm.git

better error message, functions to clear various caches used during translation of old2new cic, logger functions implemented inside the typechecker so that
uncommenting one line makes the type checker more verbose when recursively typing stuff
---

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index fa2816773..ae721526b 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -27,3 +27,5 @@ let get_obj u =
       NUri.UriHash.add cache u o) l;
     HExtlib.list_last l
 ;;
+
+let clear_cache () = NUri.UriHash.clear cache;;
diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli
index a6b3a6909..1893e9659 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.mli
+++ b/helm/software/components/ng_kernel/nCicLibrary.mli
@@ -15,4 +15,6 @@ exception ObjectNotFound of string Lazy.t
 
 val get_obj: NUri.uri -> NCic.obj
 
+val clear_cache : unit -> unit
+
 (* EOF *)
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index db449c16a..a4ff68d9f 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -678,7 +678,7 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                  ("Appl: wrong application of %s: the argument %s has type"^^
                    "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
                   (PP.ppterm ~subst ~metasenv ~context he)
                   (PP.ppterm ~subst ~metasenv ~context arg)
@@ -1303,4 +1303,31 @@ E.set_typecheck_obj
 
 let _ = NCicReduction.set_get_relevance get_relevance;;
 
+
+let indent = ref 0;;
+let debug = true;;
+let logger =
+    let do_indent () = String.make !indent ' ' in  
+    (function 
+      | `Start_type_checking s ->
+          if debug then
+           prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); 
+          incr indent
+      | `Type_checking_completed s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
+      | `Type_checking_interrupted s ->
+          decr indent;
+          if debug then
+           prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s)
+      | `Type_checking_failed s ->
+          decr indent;
+          if debug then
+           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 _ = set_logger logger ;; *)
 (* EOF *)
diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml
index 88bdf4f00..2738b1c90 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.ml
+++ b/helm/software/components/ng_kernel/oCic2NCic.ml
@@ -458,11 +458,11 @@ prerr_endline ("CACHE SAME NAME: " ^ NReference.string_of_reference ref ^ " <==>
  with Found ref -> Some ref
 ;;
 
+let cache1 = UriManager.UriHashtbl.create 313;;
 let rec get_height =
- let cache = UriManager.UriHashtbl.create 313 in
    function u ->
      try
-       UriManager.UriHashtbl.find cache u
+       UriManager.UriHashtbl.find cache1 u
      with
       Not_found ->
         let h = ref 0 in
@@ -476,7 +476,7 @@ let rec get_height =
                1 + !h
            | _ -> 0
          in
-           UriManager.UriHashtbl.add cache u res;
+           UriManager.UriHashtbl.add cache1 u res;
            res
 and height_of_term ?(h=ref 0) t =
  let rec aux =
@@ -845,6 +845,11 @@ let convert_obj uri obj =
   fixpoints @ [obj]
 ;;
 
+let clear () =
+  Hashtbl.clear cache;
+  UriManager.UriHashtbl.clear cache1
+;;
+
 (*
 let convert_context uri =
   let name_of = function Cic.Name s -> s | _ -> "_" in
diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli
index 02ee706ef..ddb1baa3d 100644
--- a/helm/software/components/ng_kernel/oCic2NCic.mli
+++ b/helm/software/components/ng_kernel/oCic2NCic.mli
@@ -17,3 +17,5 @@ val reference_of_ouri: UriManager.uri -> NReference.spec -> NReference.reference
 
 val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list
 val convert_term: UriManager.uri -> Cic.term -> NCic.term * NCic.obj list
+
+val clear: unit -> unit