From: Claudio Sacerdoti Coen Date: Tue, 16 Apr 2002 16:24:03 +0000 (+0000) Subject: Module Logger added. X-Git-Tag: V_0_3_0_debian_8~144 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5b2c666a48028daeba3fe6692e6ad3e14cad0a42;p=helm.git Module Logger added. --- diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index 64a4fb254..e03d3e436 100644 --- 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 591446ccd..b4e5b8ae6 100644 --- 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 c81843137..ba72a37a2 100644 --- 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 ' ') ^ - "
" ^ - "Type-Checking of " ^ (U.string_of_uri uri) ^ " started
\n" - ) ; - flush stdout ; - incr indent - | `Type_checking_completed uri -> - decr indent ; - print_string ( - (String.make !indent ' ') ^ - "
" ^ - "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.
\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 index 000000000..efae1b195 --- /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 () ^ + "
" ^ + "Type-Checking of " ^ (U.string_of_uri uri) ^ " started
\n" + ) ; + incr indent + | `Type_checking_completed uri -> + decr indent ; + print_and_flush ( + mkindent () ^ + "
" ^ + "Type-Checking of " ^ (U.string_of_uri uri) ^ " completed.
\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 index 000000000..c5e74ec90 --- /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