diff options
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 39 |
1 files changed, 35 insertions, 4 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index a54c082979..d303038c5d 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -9,7 +9,7 @@ open CErrors open Util open Names -open Term +open Constr open Context open Evd @@ -34,7 +34,7 @@ end type t val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term -val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type +val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type val whd_evar : Evd.evar_map -> t -> t val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t val of_constr : Constr.t -> t @@ -54,7 +54,7 @@ struct type t = Sorts.t let make s = s let kind sigma = function - | Type u -> sort_of_univ (Evd.normalize_universe sigma u) + | Sorts.Type u -> Sorts.sort_of_univ (Evd.normalize_universe sigma u) | s -> s let unsafe_to_sorts s = s end @@ -114,7 +114,7 @@ let rec to_constr sigma c = match Constr.kind c with | Some c -> to_constr sigma c | None -> Constr.map (fun c -> to_constr sigma c) c end -| Sort (Type u) -> +| Sort (Sorts.Type u) -> let u' = Evd.normalize_universe sigma u in if u' == u then c else mkSort (Sorts.sort_of_univ u') | Const (c', u) when not (Univ.Instance.is_empty u) -> @@ -645,6 +645,37 @@ let eq_constr_universes_proj env sigma m n = let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in if res then Some !cstrs else None +let universes_of_constr env sigma c = + let open Univ in + let open Declarations in + let rec aux s c = + match kind sigma c with + | Const (c, u) -> + begin match (Environ.lookup_constant c env).const_universes with + | Polymorphic_const _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_const (univs, _) -> + LSet.union s univs + end + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + begin match (Environ.lookup_mind mind env).mind_universes with + | Cumulative_ind _ | Polymorphic_ind _ -> + LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s + | Monomorphic_ind (univs,_) -> + LSet.union s univs + end + | Sort u -> + let sort = ESorts.kind sigma u in + if Sorts.is_small sort then s + else + let u = Sorts.univ_of_sort sort in + LSet.fold LSet.add (Universe.levels u) s + | Evar (k, args) -> + let concl = Evd.evar_concl (Evd.find sigma k) in + fold sigma aux (aux s (of_constr concl)) c + | _ -> fold sigma aux s c + in aux LSet.empty c + open Context open Environ |