diff options
| author | Matthieu Sozeau | 2013-11-04 18:19:28 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:55 +0200 |
| commit | ede4fa2f51bee0a425f68cd159178835a3af3ca6 (patch) | |
| tree | 0cbd06a11bdc25ef4b1d8e81af23f5b5f4cfe9cc /pretyping | |
| parent | 7dfb0fb915fa095f8af57e8bb5e4727ebb61304a (diff) | |
Restore reasonable performance by not allocating during universe checks,
using a fast_compare_neq.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 6 | ||||
| -rw-r--r-- | pretyping/evd.ml | 3 | ||||
| -rw-r--r-- | pretyping/evd.mli | 3 |
3 files changed, 11 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 908e592270..bca599305a 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -126,6 +126,10 @@ let nf_evar_map_undefined evm = (* Auxiliary functions for the conversion algorithms modulo evars *) +let has_flexible_level evd l = + let a = Univ.Instance.to_array l in + Array.exists (fun l -> Evd.is_flexible_level evd l) a + let has_undefined_evars or_sorts evd t = let rec has_ev t = match kind_of_term t with @@ -138,7 +142,7 @@ let has_undefined_evars or_sorts evd t = | Sort (Type _) (*FIXME could be finer, excluding Prop and Set universes *) when or_sorts -> raise Not_found | Ind (_,l) | Const (_,l) | Construct (_,l) - when l <> Univ.Instance.empty && or_sorts -> raise Not_found + when or_sorts && not (Univ.Instance.is_empty l) (* has_flexible_level evd l *) -> raise Not_found | _ -> iter_constr has_ev t in try let _ = has_ev t in false with (Not_found | NotInstantiatedEvar) -> true diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ef93a827a6..21a0603c3f 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1021,6 +1021,9 @@ let is_sort_variable evd s = | None -> None) | _ -> None +let is_flexible_level evd l = + let uctx = evd.universes in + Univ.LMap.mem l uctx.uctx_univ_variables let is_eq_sort s1 s2 = if Sorts.equal s1 s2 then None diff --git a/pretyping/evd.mli b/pretyping/evd.mli index e44e8e9069..020f0a7b44 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -439,6 +439,9 @@ val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> (Univ.universe_level * bool) option (** [is_sort_variable evm s] returns [Some (u, is_rigid)] or [None] if [s] is not a sort variable declared in [evm] *) +val is_flexible_level : evar_map -> Univ.Level.t -> bool + + val whd_sort_variable : evar_map -> constr -> constr (* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) val normalize_universe : evar_map -> Univ.universe -> Univ.universe |