From: Stefano Zacchiroli Date: Mon, 5 Jul 2004 07:05:24 +0000 (+0000) Subject: commeted out some debugging instructions X-Git-Tag: pre_subst_in_kernel~7 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57b385b0d728a06d50d3011473e9afeaf51b674f;p=helm.git commeted out some debugging instructions --- diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index f5daaf3d7..387c747f6 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -25,6 +25,7 @@ open Printf +(* (* PROFILING *) let apply_subst_counter = ref 0 let apply_subst_context_counter = ref 0 let apply_subst_metasenv_counter = ref 0 @@ -34,7 +35,6 @@ let whd_counter = ref 0 let are_convertible_counter = ref 0 let metasenv_length = ref 0 let context_length = ref 0 - let reset_counters () = apply_subst_counter := 0; apply_subst_context_counter := 0; @@ -45,7 +45,6 @@ let reset_counters () = are_convertible_counter := 0; metasenv_length := 0; context_length := 0 - let print_counters () = prerr_endline (Printf.sprintf "apply_subst: %d @@ -65,6 +64,7 @@ context length: %d (avg = %.2f) !context_length ((float !context_length) /. (float !apply_subst_context_counter)) ) +*) exception MetaSubstFailure of string exception Uncertain of string @@ -179,13 +179,15 @@ let apply_subst = end in fun s t -> - incr apply_subst_counter; +(* incr apply_subst_counter; *) apply_subst_gen ~appl_fun s t ;; let rec apply_subst_context subst context = +(* incr apply_subst_context_counter; context_length := !context_length + List.length context; +*) List.fold_right (fun item context -> match item with @@ -204,8 +206,10 @@ let rec apply_subst_context subst context = context [] let apply_subst_metasenv subst metasenv = +(* incr apply_subst_metasenv_counter; metasenv_length := !metasenv_length + List.length metasenv; +*) List.map (fun (n, context, ty) -> (n, apply_subst_context subst context, apply_subst subst ty)) @@ -263,7 +267,7 @@ let ppmetasenv ?(sep = "\n") metasenv subst = * the calculus *) let lift subst n term = - incr subst_counter; +(* incr subst_counter; *) let term = apply_subst subst term in try CicSubstitution.lift n term @@ -271,7 +275,7 @@ let lift subst n term = raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e)) let subst subst t1 t2 = - incr subst_counter; +(* incr subst_counter; *) let t1 = apply_subst subst t1 in let t2 = apply_subst subst t2 in try @@ -280,7 +284,7 @@ let subst subst t1 t2 = raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e)) let whd subst context term = - incr whd_counter; +(* incr whd_counter; *) let term = apply_subst subst term in let context = apply_subst_context subst context in try @@ -290,7 +294,7 @@ let whd subst context term = Printexc.to_string e)) let are_convertible subst context t1 t2 = - incr are_convertible_counter; +(* incr are_convertible_counter; *) let context = apply_subst_context subst context in let t1 = apply_subst subst t1 in let t2 = apply_subst subst t2 in diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 46a50a63a..14d6da3f6 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -86,7 +86,9 @@ val fppsubst: Format.formatter -> substitution -> unit val fppterm: Format.formatter -> Cic.term -> unit val fppmetasenv: Format.formatter -> Cic.metasenv -> unit +(* (* DEBUG *) val print_counters: unit -> unit val reset_counters: unit -> unit +*)