Module Logger added.

diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend
index 64a4fb25444f7db187c85c5c39dbafd44da77e72..e03d3e43620559b44f62461a4987603f5c893ec4 100644 (file)
--- a/helm/ocaml/cic_proof_checking/.depend
+++ b/helm/ocaml/cic_proof_checking/.depend
@@ -1,23 +1,17 @@
 cicSubstitution.cmo: cicSubstitution.cmi 
 cicSubstitution.cmx: cicSubstitution.cmi 
+logger.cmo: logger.cmi 
+logger.cmx: logger.cmi 
 cicEnvironment.cmo: cicSubstitution.cmi cicEnvironment.cmi 
 cicEnvironment.cmx: cicSubstitution.cmx cicEnvironment.cmi 
 cicPp.cmo: cicEnvironment.cmi cicPp.cmi 
 cicPp.cmx: cicEnvironment.cmx cicPp.cmi 
 cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi 
 cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi 
-cicReductionNaif.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \
-    cicReductionNaif.cmi 
-cicReductionNaif.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \
-    cicReductionNaif.cmi 
 cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \
     cicReduction.cmi 
 cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \
     cicReduction.cmi 
-cicReductionMachine.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \
-    cicReductionMachine.cmi 
-cicReductionMachine.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \
-    cicReductionMachine.cmi 
 cicTypeChecker.cmo: cicEnvironment.cmi cicPp.cmi cicReduction.cmi \
     cicSubstitution.cmi cicTypeChecker.cmi 
 cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \

diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile
index 591446ccd548b33a098d9a3dba2c7034c856571f..b4e5b8ae618876ef9259fc9903b3b211adcefaeb 100644 (file)
--- a/helm/ocaml/cic_proof_checking/Makefile
+++ b/helm/ocaml/cic_proof_checking/Makefile
@@ -2,8 +2,8 @@ PACKAGE = cic_proof_checking
 REQUIRES = helm-cic
 PREDICATES =
 
-INTERFACE_FILES = cicSubstitution.mli cicEnvironment.mli cicPp.mli \
-                  cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli cicReductionMachine.mli cicTypeChecker.mli \
+INTERFACE_FILES = cicSubstitution.mli logger.mli cicEnvironment.mli cicPp.mli \
+                  cicMiniReduction.mli cicReduction.mli cicTypeChecker.mli \
                   cicCooking.mli
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
@@ -11,6 +11,7 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL = \
             cicSubstitution.cmo cicSubstitution.cmx cicSubstitution.o \
             cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o
+EXTRA_OBJECTS_TO_CLEAN =
 
 
 include ../Makefile.common

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)
 ;;
 

diff --git a/helm/ocaml/cic_proof_checking/logger.ml b/helm/ocaml/cic_proof_checking/logger.ml
new file mode 100644 (file)
index 0000000..efae1b1
--- /dev/null
+++ b/helm/ocaml/cic_proof_checking/logger.ml
@@ -0,0 +1,58 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+type msg =
+ [ `Start_type_checking of UriManager.uri
+ | `Type_checking_completed of UriManager.uri
+ ]
+;;
+
+let log_to_html ~print_and_flush =
+ let module U = UriManager in
+  let indent = ref 0 in
+   let mkindent () = 
+    String.make !indent ' '
+   in
+    function
+       `Start_type_checking uri ->
+         print_and_flush (
+          mkindent () ^
+          "<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"
+         ) ;
+         incr indent
+     | `Type_checking_completed uri ->
+         decr indent ;
+         print_and_flush (
+           mkindent () ^
+          "<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"
+         )
+;;
+
+let log_callback = ref (function (_:msg) -> ())
+let log msg = !log_callback msg;;

diff --git a/helm/ocaml/cic_proof_checking/logger.mli b/helm/ocaml/cic_proof_checking/logger.mli
new file mode 100644 (file)
index 0000000..c5e74ec
--- /dev/null
+++ b/helm/ocaml/cic_proof_checking/logger.mli
@@ -0,0 +1,39 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+type msg =
+ [ `Start_type_checking of UriManager.uri
+ | `Type_checking_completed of UriManager.uri
+ ]
+;;
+
+(* A callback that can be used to log to html *)
+val log_to_html : print_and_flush:(string -> unit) -> msg -> unit
+
+(* The log function used. The default does nothing. *)
+val log_callback : (msg -> unit) ref
+
+(* Log something via log_callback *)
+val log : msg -> unit