-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
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
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
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
--- /dev/null
+(* 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 () ^
+ "<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"
+ )
+ | `Trusting uri ->
+ print_and_flush (
+ mkindent () ^
+ "<div style=\"color: blue ; margin-left: " ^
+ string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
+ (U.string_of_uri uri) ^ " is trusted.</div>\n"
+ )
+;;
+
+let log_callback = ref (function (_:msg) -> ())
+let log msg = !log_callback msg;;
--- /dev/null
+(* 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
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,_) ->
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
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
(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
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
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
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
check_mutual_inductive_defs uri uobj
) ;
CicEnvironment.set_type_checking_info uri ;
- Logger.log (`Type_checking_completed uri)
+ CicLogger.log (`Type_checking_completed uri)
;;
+++ /dev/null
-(* 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 () ^
- "<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"
- )
- | `Trusting uri ->
- print_and_flush (
- mkindent () ^
- "<div style=\"color: blue ; margin-left: " ^
- string_of_float (float_of_int !indent *. 0.5) ^ "cm\">" ^
- (U.string_of_uri uri) ^ " is trusted.</div>\n"
- )
-;;
-
-let log_callback = ref (function (_:msg) -> ())
-let log msg = !log_callback msg;;
+++ /dev/null
-(* 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
projects / helm.git / commitdiff