diff options
| author | Gaëtan Gilbert | 2018-10-10 14:20:51 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:53 +0200 |
| commit | 44ecd58e9ab5fb0f2c45e9eec76440f84995825c (patch) | |
| tree | 5ce39ab09db09194d5a28ee48cd4a7ee7643b4fc /kernel | |
| parent | e99b4c66cf38bb5b6ccb76b69ebd7e7a44ed295d (diff) | |
{Univops -> Vars}.universes_of_constr
It's basically an occur check so it makes sense to put it in vars
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/typeops.ml | 15 | ||||
| -rw-r--r-- | kernel/vars.ml | 14 | ||||
| -rw-r--r-- | kernel/vars.mli | 2 |
3 files changed, 17 insertions, 14 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7456ecea56..164a47dd9a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -432,21 +432,8 @@ and execute_array env = Array.map (execute env) (* Derived functions *) -let universe_levels_of_constr _env c = - let rec aux s c = - match kind c with - | Const (_c, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = Sorts.univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> Constr.fold aux s c - in aux LSet.empty c - let check_wellformed_universes env c = - let univs = universe_levels_of_constr env c in + let univs = universes_of_constr c in try UGraph.check_declared_universes (universes env) univs with UGraph.UndeclaredLevel u -> error_undeclared_universe env u diff --git a/kernel/vars.ml b/kernel/vars.ml index 9d5d79124b..7380a860dd 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -312,3 +312,17 @@ let subst_instance_constr subst 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 + +let universes_of_constr c = + let open Univ in + let rec aux s c = + match kind c with + | Const (_c, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = Sorts.univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> Constr.fold aux s c + in aux LSet.empty c diff --git a/kernel/vars.mli b/kernel/vars.mli index fdddbdb342..7c928e2694 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -139,3 +139,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context + +val universes_of_constr : constr -> Univ.LSet.t |