Module Logger added.

[helm.git] / helm / ocaml / cic_proof_checking / cicTypeChecker.ml

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index c818431376ca9d4972972bbf1740ffd4a8b32986..ba72a37a2a6edbfe8300007f140358765a46e7cc 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -23,7 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented;;
 exception Impossible of int;;
 exception NotWellTyped of string;;
 exception WrongUriToConstant of string;;
@@ -34,30 +33,6 @@ exception NotPositiveOccurrences of string;;
 exception NotWellFormedTypeOfInductiveConstructor of string;;
 exception WrongRequiredArgument of string;;
 
-let log =
- let module U = UriManager in
-  let indent = ref 0 in
-   function
-      `Start_type_checking uri ->
-        print_string (
-         (String.make !indent ' ') ^
-         "<div style=\"margin-left: " ^
-         string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
-         "Type-Checking of " ^ (U.string_of_uri uri) ^ " started</div>\n"
-        ) ;
-        flush stdout ;
-        incr indent
-    | `Type_checking_completed uri ->
-        decr indent ;
-        print_string (
-         (String.make !indent ' ') ^
-         "<div style=\"color: green ; margin-left: " ^
-         string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
-         "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.</div>\n"
-        ) ;
-        flush stdout
-;;
-
 let fdebug = ref 0;;
 let debug t env =
  let rec debug_aux t i =
@@ -87,7 +62,7 @@ let rec cooked_type_of_constant uri cookingsno =
    match CicEnvironment.is_type_checked uri cookingsno with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       log (`Start_type_checking uri) ;
+       Logger.log (`Start_type_checking uri) ;
        (* let's typecheck the uncooked obj *)
        (match uobj with
            C.Definition (_,te,ty,_) ->
@@ -104,7 +79,7 @@ let rec cooked_type_of_constant uri cookingsno =
          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        match CicEnvironment.is_type_checked uri cookingsno with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -123,7 +98,7 @@ and type_of_variable uri =
   match CicEnvironment.is_type_checked uri 0 with
      CicEnvironment.CheckedObj (C.Variable (_,_,ty)) -> ty
    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty)) ->
-       log (`Start_type_checking uri) ;
+      Logger.log (`Start_type_checking uri) ;
       (* only to check that ty is well-typed *)
       let _ = type_of ty in
        (match bo with
@@ -133,7 +108,7 @@ and type_of_variable uri =
              raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
        ) ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        ty
    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 
@@ -377,10 +352,10 @@ and cooked_type_of_mutual_inductive_defs uri cookingsno i =
    match CicEnvironment.is_type_checked uri cookingsno with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       log (`Start_type_checking uri) ;
+       Logger.log (`Start_type_checking uri) ;
        cooked_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked uri cookingsno with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -400,10 +375,10 @@ and cooked_type_of_mutual_inductive_constr uri cookingsno i j =
    match CicEnvironment.is_type_checked uri cookingsno with
       CicEnvironment.CheckedObj cobj -> cobj
     | CicEnvironment.UncheckedObj uobj ->
-       log (`Start_type_checking uri) ;
+       Logger.log (`Start_type_checking uri) ;
        cooked_mutual_inductive_defs uri uobj ;
        CicEnvironment.set_type_checking_info uri ;
-       log (`Type_checking_completed uri) ;
+       Logger.log (`Type_checking_completed uri) ;
        (match CicEnvironment.is_type_checked uri cookingsno with
           CicEnvironment.CheckedObj cobj -> cobj
         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
@@ -1341,7 +1316,7 @@ let typecheck uri =
      CicEnvironment.CheckedObj _ -> ()
    | CicEnvironment.UncheckedObj uobj ->
       (* let's typecheck the uncooked object *)
-      log (`Start_type_checking uri) ;
+      Logger.log (`Start_type_checking uri) ;
       (match uobj with
           C.Definition (_,te,ty,_) ->
            let _ = type_of ty in
@@ -1369,6 +1344,6 @@ let typecheck uri =
            cooked_mutual_inductive_defs uri uobj
       ) ;
       CicEnvironment.set_type_checking_info uri ;
-      log (`Type_checking_completed uri)
+      Logger.log (`Type_checking_completed uri)
 ;;