From 5d3c0a0326af68e85f1f1cfc6bfa2214b0052de8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 10 Mar 2020 01:06:34 -0400
Subject: [flags] [profile] Remove bit-rotten CProfile code.

As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.

It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.

We thus remove all bitrotten dead code.
---
 kernel/cooking.ml   |  3 ---
 kernel/inductive.ml |  5 -----
 kernel/reduction.ml | 41 ++++++-----------------------------------
 kernel/typeops.ml   |  6 ------
 kernel/uGraph.ml    | 25 -------------------------
 kernel/vars.ml      |  8 --------
 6 files changed, 6 insertions(+), 82 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f82b754c59..87b1a71c9d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -252,9 +252,6 @@ let cook_constant { from = cb; info } =
     cook_context = Some const_hyps;
   }
 
-(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
-(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
-
 (********************************)
 (* Discharging mutual inductive *)
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index eb18d4b90e..6cb61174d3 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1334,11 +1334,6 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
   else
     ()
 
-(*
-let cfkey = CProfile.declare_profile "check_fix";;
-let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
-*)
-
 (************************************************************************)
 (* Co-fixpoints. *)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1e39756d47..18c3a3ec9c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -964,7 +964,8 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
     compare_instances = infer_convert_instances;
     compare_cumul_instances = infer_inductive_instances; }
 
-let gen_conv cv_pb l2r reds env evars univs t1 t2 =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _ -> None)) t1 t2 =
+  let univs = Environ.universes env in
   let b =
     if cv_pb = CUMUL then leq_constr_univs univs t1 t2
     else eq_constr_univs univs t1 t2
@@ -974,16 +975,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
       let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
         ()
 
-(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
-  let univs = Environ.universes env in
-  if Flags.profile then
-    let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
-      CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
-  else gen_conv cv_pb l2r reds env evars univs
-
 let conv = gen_conv CONV
-
 let conv_leq = gen_conv CUMUL
 
 let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
@@ -992,7 +984,7 @@ let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
     clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
   in s
 
-let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
+let infer_conv_universes cv_pb ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env t1 t2 =
   let univs = Environ.universes env in
   let b, cstrs =
     if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
@@ -1001,37 +993,16 @@ let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
     if b then cstrs
     else
       let state = ((univs, Univ.Constraint.empty), inferred_universes) in
-      let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
+      let ((_,cstrs), _) = clos_gen_conv ts cv_pb l2r evars env univs state t1 t2 in
         cstrs
 
-(* Profiling *)
-let infer_conv_universes =
-  if Flags.profile then
-    let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
-      CProfile.profile7 infer_conv_universes_key infer_conv_universes
-  else infer_conv_universes
-
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env t1 t2 =
-  infer_conv_universes CONV l2r evars ts env t1 t2
-
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env t1 t2 =
-  infer_conv_universes CUMUL l2r evars ts env t1 t2
+let infer_conv = infer_conv_universes CONV
+let infer_conv_leq = infer_conv_universes CUMUL
 
 let default_conv cv_pb ?l2r:_ env t1 t2 =
     gen_conv cv_pb env t1 t2
 
 let default_conv_leq = default_conv CUMUL
-(*
-let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";;
-let conv_leq env t1 t2 =
-  CProfile.profile4 convleqkey conv_leq env t1 t2;;
-
-let convkey = CProfile.declare_profile "Kernel_reduction.conv";;
-let conv env t1 t2 =
-  CProfile.profile4 convleqkey conv env t1 t2;;
-*)
 
 (* Application with on-the-fly reduction *)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1b1aa84e6b..3a946fc03a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -644,12 +644,6 @@ let infer env constr =
   let constr, t = execute env constr in
   make_judge constr t
 
-let infer =
-  if Flags.profile then
-    let infer_key = CProfile.declare_profile "Fast_infer" in
-      CProfile.profile2 infer_key (fun b c -> infer b c)
-  else (fun b c -> infer b c)
-
 let assumption_of_judgment env {uj_val=c; uj_type=t} =
   infer_assumption env c t
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index b988ec40a7..6db54a3bb6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -251,28 +251,3 @@ type node = G.node =
 let repr g = G.repr g.graph
 
 let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g
-
-(** Profiling *)
-
-let merge_constraints =
-  if Flags.profile then
-    let key = CProfile.declare_profile "merge_constraints" in
-      CProfile.profile2 key merge_constraints
-  else merge_constraints
-let check_constraints =
-  if Flags.profile then
-    let key = CProfile.declare_profile "check_constraints" in
-      CProfile.profile2 key check_constraints
-  else check_constraints
-
-let check_eq =
-  if Flags.profile then
-    let check_eq_key = CProfile.declare_profile "check_eq" in
-      CProfile.profile3 check_eq_key check_eq
-  else check_eq
-
-let check_leq =
-  if Flags.profile then
-    let check_leq_key = CProfile.declare_profile "check_leq" in
-      CProfile.profile3 check_leq_key check_leq
-  else check_leq
diff --git a/kernel/vars.ml b/kernel/vars.ml
index b09577d4db..b9991391c2 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -123,11 +123,6 @@ let substn_many lamv n c =
       | _ -> Constr.map_with_binders succ substrec depth c in
     substrec n c
 
-(*
-let substkey = CProfile.declare_profile "substn_many";;
-let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;;
-*)
-
 let make_subst = function
 | [] -> [||]
 | hd :: tl ->
@@ -343,9 +338,6 @@ let univ_instantiate_constr u c =
   assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder));
   subst_instance_constr u c.univ_abstracted_value
 
-(* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
-(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
-
 let subst_instance_context s ctx =
   if Univ.Instance.is_empty s then ctx
   else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
-- 
cgit v1.2.3