From: Stefano Zacchiroli Date: Tue, 16 Dec 2003 15:58:38 +0000 (+0000) Subject: renamed module "logger" to "cicLogger" to avoid confusion with user X-Git-Tag: V_0_2_2~10 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d70688ca1e1bcefc463d3397c6da77b40d055c85;p=helm.git renamed module "logger" to "cicLogger" to avoid confusion with user interface logger --- diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index c1319a692..2698db04e 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -1,7 +1,7 @@ -logger.cmo: logger.cmi -logger.cmx: logger.cmi -cicEnvironment.cmo: logger.cmi cicEnvironment.cmi -cicEnvironment.cmx: logger.cmx cicEnvironment.cmi +cicLogger.cmo: cicLogger.cmi +cicLogger.cmx: cicLogger.cmi +cicEnvironment.cmo: cicEnvironment.cmi +cicEnvironment.cmx: cicEnvironment.cmi cicPp.cmo: cicEnvironment.cmi cicPp.cmi cicPp.cmx: cicEnvironment.cmx cicPp.cmi cicSubstitution.cmo: cicEnvironment.cmi cicSubstitution.cmi @@ -17,6 +17,6 @@ cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ cicReduction.cmi cicTypeChecker.cmo: cicEnvironment.cmi cicPp.cmi cicReduction.cmi \ - cicSubstitution.cmi logger.cmi cicTypeChecker.cmi + cicSubstitution.cmi cicTypeChecker.cmi cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \ - cicSubstitution.cmx logger.cmx cicTypeChecker.cmi + cicSubstitution.cmx cicTypeChecker.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 0de0fcda0..96ac166b5 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -4,9 +4,10 @@ PREDICATES = REDUCTION_IMPLEMENTATION = cicReductionMachine.ml -INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ - cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ - cicTypeChecker.mli +INTERFACE_FILES = \ + cicLogger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \ + cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \ + cicTypeChecker.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) # Metadata tools only need zeta-reduction diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index f63b1618c..3a201ad69 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -351,7 +351,7 @@ let is_type_checked ?(trust=true) uri = Cache.unchecked_to_frozen uri ; if trust && trust_obj uri then begin - Logger.log (`Trusting uri) ; + CicLogger.log (`Trusting uri) ; set_type_checking_info uri ; CheckedObj (Cache.find_cooked uri) end diff --git a/helm/ocaml/cic_proof_checking/cicLogger.ml b/helm/ocaml/cic_proof_checking/cicLogger.ml new file mode 100644 index 000000000..9fc983fc7 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicLogger.ml @@ -0,0 +1,66 @@ +(* 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 + | `Trusting 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" + ) + | `Trusting uri -> + print_and_flush ( + mkindent () ^ + "
" ^ + (U.string_of_uri uri) ^ " is trusted.
\n" + ) +;; + +let log_callback = ref (function (_:msg) -> ()) +let log msg = !log_callback msg;; diff --git a/helm/ocaml/cic_proof_checking/cicLogger.mli b/helm/ocaml/cic_proof_checking/cicLogger.mli new file mode 100644 index 000000000..781abdef6 --- /dev/null +++ b/helm/ocaml/cic_proof_checking/cicLogger.mli @@ -0,0 +1,40 @@ +(* 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 + | `Trusting 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 diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 7521f0f90..0d171604d 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -136,7 +136,7 @@ let rec type_of_constant uri = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> - Logger.log (`Start_type_checking uri) ; + CicLogger.log (`Start_type_checking uri) ; (* let's typecheck the uncooked obj *) (match uobj with C.Constant (_,Some te,ty,_) -> @@ -166,7 +166,7 @@ let rec type_of_constant uri = raise (TypeCheckerFailure (WrongUriToConstant (U.string_of_uri uri))) ) ; CicEnvironment.set_type_checking_info uri ; - Logger.log (`Type_checking_completed uri) ; + CicLogger.log (`Type_checking_completed uri) ; match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError @@ -184,7 +184,7 @@ and type_of_variable uri = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> - Logger.log (`Start_type_checking uri) ; + CicLogger.log (`Start_type_checking uri) ; (* only to check that ty is well-typed *) let _ = type_of ty in (match bo with @@ -196,7 +196,7 @@ and type_of_variable uri = (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))) ) ; CicEnvironment.set_type_checking_info uri ; - Logger.log (`Type_checking_completed uri) ; + CicLogger.log (`Type_checking_completed uri) ; ty | _ -> raise @@ -529,10 +529,10 @@ and type_of_mutual_inductive_defs uri i = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> - Logger.log (`Start_type_checking uri) ; + CicLogger.log (`Start_type_checking uri) ; check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; - Logger.log (`Type_checking_completed uri) ; + CicLogger.log (`Type_checking_completed uri) ; (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError @@ -555,10 +555,10 @@ and type_of_mutual_inductive_constr uri i j = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> - Logger.log (`Start_type_checking uri) ; + CicLogger.log (`Start_type_checking uri) ; check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; - Logger.log (`Type_checking_completed uri) ; + CicLogger.log (`Type_checking_completed uri) ; (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError @@ -1762,7 +1762,7 @@ let typecheck uri = CicEnvironment.CheckedObj _ -> () | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) - Logger.log (`Start_type_checking uri) ; + CicLogger.log (`Start_type_checking uri) ; (match uobj with C.Constant (_,Some te,ty,_) -> let _ = type_of ty in @@ -1802,5 +1802,5 @@ let typecheck uri = check_mutual_inductive_defs uri uobj ) ; CicEnvironment.set_type_checking_info uri ; - Logger.log (`Type_checking_completed uri) + CicLogger.log (`Type_checking_completed uri) ;; diff --git a/helm/ocaml/cic_proof_checking/logger.ml b/helm/ocaml/cic_proof_checking/logger.ml deleted file mode 100644 index 2fe8ac0a1..000000000 --- a/helm/ocaml/cic_proof_checking/logger.ml +++ /dev/null @@ -1,66 +0,0 @@ -(* 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 - | `Trusting 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" - ) - | `Trusting uri -> - print_and_flush ( - mkindent () ^ - "
" ^ - (U.string_of_uri uri) ^ " is trusted.
\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 deleted file mode 100644 index 781abdef6..000000000 --- a/helm/ocaml/cic_proof_checking/logger.mli +++ /dev/null @@ -1,40 +0,0 @@ -(* 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 - | `Trusting 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