diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 12 | ||||
| -rw-r--r-- | kernel/constr.mli | 5 | ||||
| -rw-r--r-- | kernel/environ.ml | 48 | ||||
| -rw-r--r-- | kernel/environ.mli | 5 | ||||
| -rw-r--r-- | kernel/typeops.ml | 15 | ||||
| -rw-r--r-- | kernel/univ.ml | 3 | ||||
| -rw-r--r-- | kernel/univ.mli | 3 | ||||
| -rw-r--r-- | kernel/vars.ml | 14 | ||||
| -rw-r--r-- | kernel/vars.mli | 2 |
9 files changed, 69 insertions, 38 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index c97969c0e0..b490aa5092 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -227,6 +227,12 @@ let mkMeta n = Meta n (* Constructs a Variable named id *) let mkVar id = Var id +let mkRef (gr,u) = let open GlobRef in match gr with + | ConstRef c -> mkConstU (c,u) + | IndRef ind -> mkIndU (ind,u) + | ConstructRef c -> mkConstructU (c,u) + | VarRef x -> mkVar x + (************************************************************************) (* kind_of_term = constructions as seen by the user *) (************************************************************************) @@ -401,6 +407,12 @@ let destCoFix c = match kind c with | CoFix cofix -> cofix | _ -> raise DestKO +let destRef c = let open GlobRef in match kind c with + | Var x -> VarRef x, Univ.Instance.empty + | Const (c,u) -> ConstRef c, u + | Ind (ind,u) -> IndRef ind, u + | Construct (c,u) -> ConstructRef c, u + | _ -> raise DestKO (******************************************************************) (* Flattening and unflattening of embedded applications and casts *) diff --git a/kernel/constr.mli b/kernel/constr.mli index 3c9cc96a0d..c012f04260 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -128,6 +128,9 @@ val mkConstruct : constructor -> constr val mkConstructU : pconstructor -> constr val mkConstructUi : pinductive * int -> constr +(** Make a constant, inductive, constructor or variable. *) +val mkRef : GlobRef.t Univ.puniverses -> constr + (** Constructs a destructor of inductive type. [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] @@ -340,6 +343,8 @@ val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint +val destRef : constr -> GlobRef.t Univ.puniverses + (** {6 Equality} *) (** [equal a b] is true if [a] equals [b] modulo alpha, casts, diff --git a/kernel/environ.ml b/kernel/environ.ml index 2fa33eb1cd..3b7e3ae544 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -419,12 +419,6 @@ let constant_type env (kn,u) = let csts = constraints_of cb u in (subst_instance_constr u cb.const_type, csts) -let constant_context env kn = - let cb = lookup_constant kn env in - match cb.const_universes with - | Monomorphic_const _ -> Univ.AUContext.empty - | Polymorphic_const ctx -> ctx - type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result @@ -550,28 +544,38 @@ let lookup_inductive_variables (kn,_i) env = let lookup_constructor_variables (ind,_) env = lookup_inductive_variables ind env +(* Universes *) +let constant_context env c = + let cb = lookup_constant c env in + Declareops.constant_polymorphic_context cb + +let universes_of_global env r = + let open GlobRef in + match r with + | VarRef _ -> Univ.AUContext.empty + | ConstRef c -> constant_context env c + | IndRef (mind,_) | ConstructRef ((mind,_),_) -> + let mib = lookup_mind mind env in + Declareops.inductive_polymorphic_context mib + (* Returns the list of global variables in a term *) -let vars_of_global env constr = - match kind constr with - Var id -> Id.Set.singleton id - | Const (kn, _) -> lookup_constant_variables kn env - | Ind (ind, _) -> lookup_inductive_variables ind env - | Construct (cstr, _) -> lookup_constructor_variables cstr env - (** FIXME: is Proj missing? *) - | _ -> raise Not_found +let vars_of_global env gr = + let open GlobRef in + match gr with + | VarRef id -> Id.Set.singleton id + | ConstRef kn -> lookup_constant_variables kn env + | IndRef ind -> lookup_inductive_variables ind env + | ConstructRef cstr -> lookup_constructor_variables cstr env let global_vars_set env constr = let rec filtrec acc c = - let acc = - match kind c with - | Var _ | Const _ | Ind _ | Construct _ -> - Id.Set.union (vars_of_global env c) acc - | _ -> - acc in - Constr.fold filtrec acc c + match destRef c with + | gr, _ -> + Id.Set.union (vars_of_global env gr) acc + | exception DestKO -> Constr.fold filtrec acc c in - filtrec Id.Set.empty constr + filtrec Id.Set.empty constr (* [keep_hyps env ids] keeps the part of the section context of [env] which diff --git a/kernel/environ.mli b/kernel/environ.mli index 031e7968d7..3d653bcfe0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -267,6 +267,8 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env val set_typing_flags : typing_flags -> env -> env +val universes_of_global : env -> GlobRef.t -> AUContext.t + (** {6 Sets of referred section variables } [global_vars_set env c] returns the list of [id]'s occurring either directly as [Var id] in [c] or indirectly as a section variable @@ -274,8 +276,7 @@ val set_typing_flags : typing_flags -> env -> env val global_vars_set : env -> constr -> Id.Set.t -(** the constr must be a global reference *) -val vars_of_global : env -> constr -> Id.Set.t +val vars_of_global : env -> GlobRef.t -> Id.Set.t (** closure of the input id set w.r.t. dependency *) val really_needed : env -> Id.Set.t -> Id.Set.t 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/univ.ml b/kernel/univ.ml index fa37834a23..d09b54e7ec 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1065,6 +1065,9 @@ type universe_context_set = ContextSet.t type 'a in_universe_context = 'a * universe_context type 'a in_universe_context_set = 'a * universe_context_set +let extend_in_context_set (a, ctx) ctx' = + (a, ContextSet.union ctx ctx') + (** Substitutions. *) let empty_subst = LMap.empty diff --git a/kernel/univ.mli b/kernel/univ.mli index 1aa53b8aa8..7ac8247ca4 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -433,6 +433,9 @@ end type 'a in_universe_context = 'a * UContext.t type 'a in_universe_context_set = 'a * ContextSet.t +val extend_in_context_set : 'a in_universe_context_set -> ContextSet.t -> + 'a in_universe_context_set + val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool 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 |