diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 3 | ||||
| -rw-r--r-- | kernel/inductive.ml | 5 | ||||
| -rw-r--r-- | kernel/reduction.ml | 41 | ||||
| -rw-r--r-- | kernel/typeops.ml | 6 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 25 | ||||
| -rw-r--r-- | kernel/vars.ml | 8 |
6 files changed, 6 insertions, 82 deletions
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 |