better error message, functions to clear various caches used during translation of...

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 fa2816773cbc9d3107f62a789e2fcf9b07ee44e4..ae721526b948e6ff1bf723fd133c79ff852bef1e 100644 (file)
--- 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 a6b3a69096a68bd68afc5cd3f56bc7b1dddabb15..1893e9659eb8394533728a397514d7a7c2715f34 100644 (file)
--- 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 db449c16aaa2cabbd0427003f137d5f05c2059b2..a4ff68d9fc4ae745488b63c220cd2718a167f1d9 100644 (file)
--- 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 88bdf4f00e620fc7194d7cfd2083a90106abefd3..2738b1c901835183078c7a24b0f3470475f13f02 100644 (file)
--- 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 02ee706efa1fa597da0df7b5b58a3b3c024d129c..ddb1baa3d964b4d1a29d9aeb3e015ee36eaf1aea 100644 (file)
--- 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