From d70688ca1e1bcefc463d3397c6da77b40d055c85 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 16 Dec 2003 15:58:38 +0000 Subject: [PATCH] renamed module "logger" to "cicLogger" to avoid confusion with user interface logger --- helm/ocaml/cic_proof_checking/.depend | 12 +++++------ helm/ocaml/cic_proof_checking/Makefile | 7 ++++--- .../cic_proof_checking/cicEnvironment.ml | 2 +- .../{logger.ml => cicLogger.ml} | 2 +- .../{logger.mli => cicLogger.mli} | 0 .../cic_proof_checking/cicTypeChecker.ml | 20 +++++++++---------- 6 files changed, 22 insertions(+), 21 deletions(-) rename helm/ocaml/cic_proof_checking/{logger.ml => cicLogger.ml} (98%) rename helm/ocaml/cic_proof_checking/{logger.mli => cicLogger.mli} (100%) 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/logger.ml b/helm/ocaml/cic_proof_checking/cicLogger.ml similarity index 98% rename from helm/ocaml/cic_proof_checking/logger.ml rename to helm/ocaml/cic_proof_checking/cicLogger.ml index 2fe8ac0a1..9fc983fc7 100644 --- a/helm/ocaml/cic_proof_checking/logger.ml +++ b/helm/ocaml/cic_proof_checking/cicLogger.ml @@ -37,7 +37,7 @@ let log_to_html ~print_and_flush = String.make !indent ' ' in function - `Start_type_checking uri -> + | `Start_type_checking uri -> print_and_flush ( mkindent () ^ "
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) ;; -- 2.39.2