diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 7 | ||||
| -rw-r--r-- | engine/evd.mli | 15 |
2 files changed, 20 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index aa91fc5222..a6b6f742b7 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -854,6 +854,13 @@ let is_eq_sort s1 s2 = if Univ.Universe.equal u1 u2 then None else Some (u1, u2) +(* Precondition: l is not defined in the substitution *) +let universe_rigidity evd l = + let uctx = evd.universes in + if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then + UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx)) + else UnivRigid + let normalize_universe evd = let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in diff --git a/engine/evd.mli b/engine/evd.mli index b47b389d1b..86887f3dcc 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (********************************************************* Sort/universe variables *) -(** Rigid or flexible universe variables *) +(** Rigid or flexible universe variables. + + [UnivRigid] variables are user-provided or come from an explicit + [Type] in the source, we do not minimize them or unify them eagerly. + + [UnivFlexible alg] variables are fresh universe variables of + polymorphic constants or generated during refinement, sometimes in + algebraic position (i.e. not appearing in the term at the moment of + creation). They are the candidates for minimization (if alg, to an + algebraic universe) and unified eagerly in the first-order + unification heurstic. *) type rigid = UState.rigid = | UnivRigid @@ -514,7 +524,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map - + +val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is |