aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.mllib1
-rw-r--r--kernel/fast_typeops.ml7
-rw-r--r--kernel/reduction.ml32
-rw-r--r--kernel/univ.ml117
-rw-r--r--kernel/vars.ml7
-rw-r--r--library/universes.ml5
-rw-r--r--pretyping/evarconv.ml7
-rw-r--r--pretyping/evd.ml17
-rw-r--r--pretyping/unification.ml15
-rw-r--r--proofs/refiner.ml7
10 files changed, 123 insertions, 92 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index 12cfe4a48..7488a2c57 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -30,6 +30,7 @@ Ephemeron
Future
CUnix
System
+Profile
RemoteCounter
Envars
Predicate
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index e03720997..bb5695885 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -478,8 +478,11 @@ let infer env constr =
let t = execute env constr in
make_judge constr t
-(* let infer_key = Profile.declare_profile "Fast_infer" *)
-(* let infer = Profile.profile2 infer_key infer *)
+let infer =
+ if Flags.profile then
+ let infer_key = Profile.declare_profile "Fast_infer" in
+ Profile.profile2 infer_key infer
+ else infer
let infer_type env constr =
execute_type env constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 396175c9e..5f0684d37 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -264,7 +264,6 @@ let check_leq (univs, cstrs as cuniv) u u' =
(* with UniverseInconsistency _ -> raise NotConvertible *)
let sort_cmp_universes pb s0 s1 univs =
- let dir = if is_cumul pb then check_leq univs else check_eq univs in
match (s0,s1) with
| (Prop c1, Prop c2) when is_cumul pb ->
begin match c1, c2 with
@@ -272,9 +271,20 @@ let sort_cmp_universes pb s0 s1 univs =
| _ -> raise NotConvertible
end
| (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible
- | (Prop c1, Type u) -> dir (univ_of_sort s0) u
- | (Type u, Prop c) -> dir u (univ_of_sort s1)
- | (Type u1, Type u2) -> dir u1 u2
+ | (Prop c1, Type u) ->
+ let u0 = univ_of_sort s0 in
+ (match pb with
+ | CUMUL -> check_leq univs u0 u
+ | CONV -> check_eq univs u0 u)
+ | (Type u, Prop c) ->
+ let u1 = univ_of_sort s1 in
+ (match pb with
+ | CUMUL -> check_leq univs u u1
+ | CONV -> check_eq univs u u1)
+ | (Type u1, Type u2) ->
+ (match pb with
+ | CUMUL -> check_leq univs u1 u2
+ | CONV -> check_eq univs u1 u2)
(* let sort_cmp _ _ _ cuniv = cuniv *)
@@ -617,8 +627,11 @@ let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 =
()
(* Profiling *)
-(* let trans_fconv_universes_key = Profile.declare_profile "trans_fconv_universes" *)
-(* let trans_fconv_universes = Profile.profile8 trans_fconv_universes_key trans_fconv_universes *)
+let trans_fconv_universes =
+ if Flags.profile then
+ let trans_fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in
+ Profile.profile8 trans_fconv_universes_key trans_fconv_universes
+ else trans_fconv_universes
let trans_fconv reds cv_pb l2r evars env =
trans_fconv_universes reds cv_pb l2r evars env (universes env)
@@ -659,8 +672,11 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
in Option.get cstrs
(* Profiling *)
-(* let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" *)
-(* let infer_conv_universes = Profile.profile8 infer_conv_universes_key infer_conv_universes *)
+let infer_conv_universes =
+ if Flags.profile then
+ let infer_conv_universes_key = Profile.declare_profile "infer_conv_universes" in
+ Profile.profile8 infer_conv_universes_key infer_conv_universes
+ else infer_conv_universes
let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_state)
env univs t1 t2 =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d3dfd47cb..13e186720 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -814,20 +814,9 @@ struct
hence the definition of [type1_univ], the type of [Prop] *)
let type1 = tip (Expr.successor Expr.set)
- let is_type0m u =
- match level u with
- | Some l -> Level.is_prop l
- | _ -> false
-
- let is_type0 u =
- match level u with
- | Some l -> Level.is_set l
- | _ -> false
-
- let is_type1 u =
- match node u with
- | Cons (l, n) when is_nil n -> Expr.is_type1 (Hunivelt.node l)
- | _ -> false
+ let is_type0m x = equal type0m x
+ let is_type0 x = equal type0 x
+ let is_type1 x = equal type1 x
(* Returns the formal universe that lies juste above the universe variable u.
Used to type the sort u. *)
@@ -960,7 +949,7 @@ let repr g u =
in
repr_rec u
-let can g = List.map (repr g)
+let can g l = List.map (repr g) l
(* [safe_repr] also search for the canonical representative, but
if the graph doesn't contain the searched universe, we add it. *)
@@ -1225,76 +1214,71 @@ let check_smaller g strict u v =
if strict then
is_lt g arcu arcv
else
- arcu == snd (safe_repr g Level.prop) || is_leq g arcu arcv
+ let proparc = snd (safe_repr g Level.prop) in
+ arcu == proparc ||
+ (let setarc = snd (safe_repr g Level.set) in
+ (arcu == setarc && arcv != proparc) ||
+ is_leq g arcu arcv)
(** Then, checks on universes *)
type 'a check_function = universes -> 'a -> 'a -> bool
-(* let equiv_list cmp l1 l2 = *)
-(* let rec aux l1 l2 = *)
-(* match l1 with *)
-(* | [] -> l2 = [] *)
-(* | hd :: tl1 -> *)
-(* let rec aux' acc = function *)
-(* | hd' :: tl2 -> *)
-(* if cmp hd hd' then aux tl1 (acc @ tl2) *)
-(* else aux' (hd' :: acc) tl2 *)
-(* | [] -> false *)
-(* in aux' [] l2 *)
-(* in aux l1 l2 *)
-
-let incl_list cmp l1 l2 =
- Huniv.for_all (fun x1 -> Huniv.exists (fun x2 -> cmp x1 x2) l2) l1
-
-let compare_list cmp l1 l2 =
- (l1 == l2) || (* (equiv_list cmp l1 l2) *)
- (incl_list cmp l1 l2 && incl_list cmp l2 l1)
-
let check_equal_expr g x y =
x == y || (let (u, n) = Hunivelt.node x and (v, m) = Hunivelt.node y in
n = m && check_equal g u v)
+let check_eq_univs g l1 l2 =
+ let f x1 x2 = check_equal_expr g x1 x2 in
+ let exists x1 l = Huniv.exists (fun x2 -> f x1 x2) l in
+ Huniv.for_all (fun x1 -> exists x1 l2) l1
+ && Huniv.for_all (fun x2 -> exists x2 l1) l2
+
(** [check_eq] is also used in [Evd.set_eq_sort],
hence [Evarconv] and [Unification]. In this case,
it seems that the Atom/Max case may occur,
hence a relaxed version. *)
-(* let gen_check_eq strict g u v = *)
-(* match u,v with *)
-(* | Atom ul, Atom vl -> check_equal g ul vl *)
-(* | Max(ule,ult), Max(vle,vlt) -> *)
-(* (\* TODO: remove elements of lt in le! *\) *)
-(* compare_list (check_equal g) ule vle && *)
-(* compare_list (check_equal g) ult vlt *)
-(* | _ -> *)
-(* (\* not complete! (Atom(u) = Max([u],[]) *\) *)
-(* if strict then anomaly (str "check_eq") *)
-(* else false (\* in non-strict mode, under-approximation *\) *)
-
-(* let check_eq = gen_check_eq true *)
-(* let lax_check_eq = gen_check_eq false *)
let check_eq g u v =
- compare_list (check_equal_expr g) u v
+ Universe.equal u v || check_eq_univs g u v
+
let check_eq_level g u v = u == v || check_equal g u v
+
+let check_eq =
+ if Flags.profile then
+ let check_eq_key = Profile.declare_profile "check_eq" in
+ Profile.profile3 check_eq_key check_eq
+ else check_eq
+
let lax_check_eq = check_eq
let check_smaller_expr g (u,n) (v,m) =
- if n <= m then
- check_smaller g false u v
- else if n - m = 1 then
- check_smaller g true u v
- else false
+ let diff = n - m in
+ match diff with
+ | 0 -> check_smaller g false u v
+ | 1 -> check_smaller g true u v
+ | x when x < 0 -> check_smaller g false u v
+ | _ -> false
let exists_bigger g ul l =
Huniv.exists (fun ul' ->
check_smaller_expr g (Hunivelt.node ul) (Hunivelt.node ul')) l
+let real_check_leq g u v =
+ (* prerr_endline ("Real check leq" ^ (string_of_ppcmds *)
+ (* (Universe.pr u ++ str" " ++ Universe.pr v))); *)
+ Huniv.for_all (fun ul -> exists_bigger g ul v) u
+
let check_leq g u v =
- u == v ||
- match Universe.level u with
- | Some l when Level.is_prop l -> true
- | _ -> Huniv.for_all (fun ul -> exists_bigger g ul v) u
+ Universe.equal u v ||
+ Universe.is_type0m u ||
+ check_eq g u v || real_check_leq g u v
+
+let check_leq =
+ if Flags.profile then
+ let check_leq_key = Profile.declare_profile "check_leq" in
+ Profile.profile3 check_leq_key check_leq
+ else check_leq
(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
@@ -2050,8 +2034,11 @@ let enforce_eq_instances_univs strict x y c =
let merge_constraints c g =
Constraint.fold enforce_constraint c g
-let merge_constraints_key = Profile.declare_profile "merge_constraints";;
-let merge_constraints = Profile.profile2 merge_constraints_key merge_constraints
+let merge_constraints =
+ if Flags.profile then
+ let key = Profile.declare_profile "merge_constraints" in
+ Profile.profile2 key merge_constraints
+ else merge_constraints
let check_constraint g (l,d,r) =
match d with
@@ -2062,9 +2049,11 @@ let check_constraint g (l,d,r) =
let check_constraints c g =
Constraint.for_all (check_constraint g) c
-let check_constraints_key = Profile.declare_profile "check_constraints";;
let check_constraints =
- Profile.profile2 check_constraints_key check_constraints
+ if Flags.profile then
+ let key = Profile.declare_profile "check_constraints" in
+ Profile.profile2 key check_constraints
+ else check_constraints
let enforce_univ_constraint (u,d,v) =
match d with
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 3cff51ba6..a9f4644ab 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -259,8 +259,11 @@ let subst_univs_constr subst c =
let f = Univ.make_subst subst in
subst_univs_fn_constr f c
-(* let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" *)
-(* let subst_univs_constr = Profile.profile2 subst_univs_constr_key subst_univs_constr *)
+let subst_univs_constr =
+ if Flags.profile then
+ let subst_univs_constr_key = Profile.declare_profile "subst_univs_constr" in
+ Profile.profile2 subst_univs_constr_key subst_univs_constr
+ else subst_univs_constr
let subst_univs_level_constr subst c =
if Univ.is_empty_level_subst subst then c
diff --git a/library/universes.ml b/library/universes.ml
index b31aab198..99c8b39f9 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -638,6 +638,9 @@ let restrict_universe_context (univs,csts) s =
csts Constraint.empty
in (univs', csts')
+let is_small_leq (l,d,r) =
+ Level.is_small l && d == Univ.Le
+
let is_prop_leq (l,d,r) =
Level.equal Level.prop l && d == Univ.Le
@@ -651,7 +654,7 @@ let refresh_constraints univs (ctx, cstrs) =
let cstrs', univs' =
Univ.Constraint.fold (fun c (cstrs', univs as acc) ->
let c = translate_cstr c in
- if Univ.check_constraint univs c && not (is_prop_leq c) then acc
+ if Univ.check_constraint univs c && not (is_small_leq c) then acc
else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
cstrs (Univ.Constraint.empty, univs)
in ((ctx, cstrs'), univs')
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 594481af3..098f5ada5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -695,8 +695,11 @@ and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
| _ -> UnifFailure (evd,NotSameHead)
(* Profiling *)
-(* let evar_conv_xkey = Profile.declare_profile "evar_conv_x";; *)
-(* let evar_conv_x = Profile.profile6 evar_conv_xkey evar_conv_x *)
+let evar_conv_x =
+ if Flags.profile then
+ let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in
+ Profile.profile6 evar_conv_xkey evar_conv_x
+ else evar_conv_x
(* We assume here |l1| <= |l2| *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 21a0603c3..52e37e611 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -328,7 +328,7 @@ let diff_evar_universe_context ctx' ctx =
uctx_universes = Univ.empty_universes }
(* let diff_evar_universe_context_key = Profile.declare_profile "diff_evar_universe_context";; *)
-(* let diff_evar_universe_context = *)
+(* let diff_evar_universe_context = *)
(* Profile.profile2 diff_evar_universe_context_key diff_evar_universe_context;; *)
type 'a in_evar_universe_context = 'a * evar_universe_context
@@ -360,8 +360,9 @@ let process_universe_constraints univs postponed vars alg local cstrs =
in
if d == Univ.ULe then
if Univ.check_leq univs l r then
- (** Keep Prop <= var around if var might be instantiated by prop later. *)
- if Univ.is_type0m_univ l && not (Univ.is_small_univ r) then
+ (** Keep Prop/Set <= var around if var might be instantiated by prop or set
+ later. *)
+ if Univ.is_small_univ l && not (Univ.is_small_univ r) then
match Univ.Universe.level l, Univ.Universe.level r with
| Some l, Some r -> Univ.Constraint.add (l,Univ.Le,r) local, postponed
| _, _ -> local, postponed
@@ -899,6 +900,9 @@ let merge orig ext =
universes;
metas = merge_metas orig.metas ext.metas }
+(* let merge_key = Profile.declare_profile "merge" *)
+(* let merge = Profile.profile2 merge_key merge *)
+
(**********************************************************)
(* Sort variables *)
@@ -1243,8 +1247,11 @@ let nf_constraints evd =
let uctx' = normalize_evar_universe_context uctx' in
{evd with universes = uctx'}
-(* let nfconstrkey = Profile.declare_profile "nf_constraints";; *)
-(* let nf_constraints = Profile.profile1 nfconstrkey nf_constraints;; *)
+let nf_constraints =
+ if Flags.profile then
+ let nfconstrkey = Profile.declare_profile "nf_constraints" in
+ Profile.profile1 nfconstrkey nf_constraints
+ else nf_constraints
let universes evd = evd.universes.uctx_universes
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index dbd83bb42..3bb3aa9ba 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1370,12 +1370,15 @@ let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
| _ -> w_typed_unify env evd cv_pb flags ty1 ty2
(* Profiling *)
-(* let wunifkey = Profile.declare_profile "w_unify";; *)
-(* let w_unify env evd cv_pb flags ty1 ty2 = *)
-(* w_unify env evd cv_pb ~flags:flags ty1 ty2 *)
+let w_unify env evd cv_pb flags ty1 ty2 =
+ w_unify env evd cv_pb ~flags:flags ty1 ty2
-(* let w_unify = Profile.profile6 wunifkey w_unify *)
+let w_unify =
+ if Flags.profile then
+ let wunifkey = Profile.declare_profile "w_unify" in
+ Profile.profile6 wunifkey w_unify
+ else w_unify
-(* let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 = *)
-(* w_unify env evd cv_pb flags ty1 ty2 *)
+let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
+ w_unify env evd cv_pb flags ty1 ty2
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 663e24f9f..da9e8c68d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -28,8 +28,11 @@ let refiner pr goal_sigma =
{ it = sgl; sigma = sigma'; }
(* Profiling refiner *)
-(* let refiner_key = Profile.declare_profile "refiner" *)
-(* let refiner = Profile.profile2 refiner_key refiner *)
+let refiner =
+ if Flags.profile then
+ let refiner_key = Profile.declare_profile "refiner" in
+ Profile.profile2 refiner_key refiner
+ else refiner
(*********************)
(* Tacticals *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:56:10 +0000