diff options
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 91 |
1 files changed, 12 insertions, 79 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index dd6a69d9f..08461a218 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -282,28 +282,27 @@ let new_Type dp = mkType (new_univ dp) let new_Type_sort dp = Type (new_univ dp) let fresh_universe_instance ctx = - Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) - (AUContext.instance ctx) + let init _ = new_univ_level (Global.current_dirpath ()) in + Instance.of_array (Array.init (AUContext.size ctx) init) let fresh_instance_from_context ctx = let inst = fresh_universe_instance ctx in - let constraints = UContext.constraints (subst_instance_context inst ctx) in + let constraints = AUContext.instantiate inst ctx in inst, constraints let fresh_instance ctx = let ctx' = ref LSet.empty in - let inst = - Instance.subst_fn (fun v -> - let u = new_univ_level (Global.current_dirpath ()) in - ctx' := LSet.add u !ctx'; u) - (AUContext.instance ctx) + let init _ = + let u = new_univ_level (Global.current_dirpath ()) in + ctx' := LSet.add u !ctx'; u + in + let inst = Instance.of_array (Array.init (AUContext.size ctx) init) in !ctx', inst let existing_instance ctx inst = let () = - let a1 = Instance.to_array inst - and a2 = Instance.to_array (AUContext.instance ctx) in - let len1 = Array.length a1 and len2 = Array.length a2 in + let len1 = Array.length (Instance.to_array inst) + and len2 = AUContext.size ctx in if not (len1 == len2) then CErrors.user_err ~hdr:"Universes" (str "Polymorphic constant expected " ++ int len2 ++ @@ -317,12 +316,9 @@ let fresh_instance_from ctx inst = | Some inst -> existing_instance ctx inst | None -> fresh_instance ctx in - let constraints = UContext.constraints (subst_instance_context inst ctx) in + let constraints = AUContext.instantiate inst ctx in inst, (ctx', constraints) -let unsafe_instance_from ctx = - (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx) - (** Fresh universe polymorphic construction *) let fresh_constant_instance env c inst = @@ -359,34 +355,6 @@ let fresh_constructor_instance env (ind,i) inst = let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in (((ind,i),inst), ctx) -let unsafe_constant_instance env c = - let cb = lookup_constant c env in - match cb.Declarations.const_universes with - | Declarations.Monomorphic_const _ -> - ((c,Instance.empty), UContext.empty) - | Declarations.Polymorphic_const auctx -> - let inst, ctx = unsafe_instance_from auctx in ((c, inst), ctx) - -let unsafe_inductive_instance env ind = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> ((ind,Instance.empty), UContext.empty) - | Declarations.Polymorphic_ind auctx -> - let inst, ctx = unsafe_instance_from auctx in ((ind,inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in - ((ind,inst), ctx) - -let unsafe_constructor_instance env (ind,i) = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> (((ind, i),Instance.empty), UContext.empty) - | Declarations.Polymorphic_ind auctx -> - let inst, ctx = unsafe_instance_from auctx in (((ind, i),inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = unsafe_instance_from (ACumulativityInfo.univ_context acumi) in - (((ind, i),inst), ctx) - open Globnames let fresh_global_instance ?names env gr = @@ -411,19 +379,6 @@ let fresh_inductive_instance env sp = let fresh_constructor_instance env sp = fresh_constructor_instance env sp None -let unsafe_global_instance env gr = - match gr with - | VarRef id -> mkVar id, UContext.empty - | ConstRef sp -> - let c, ctx = unsafe_constant_instance env sp in - mkConstU c, ctx - | ConstructRef sp -> - let c, ctx = unsafe_constructor_instance env sp in - mkConstructU c, ctx - | IndRef sp -> - let c, ctx = unsafe_inductive_instance env sp in - mkIndU c, ctx - let constr_of_global gr = let c, ctx = fresh_global_instance (Global.env ()) gr in if not (Univ.ContextSet.is_empty ctx) then @@ -438,9 +393,6 @@ let constr_of_global gr = let constr_of_reference = constr_of_global -let unsafe_constr_of_global gr = - unsafe_global_instance (Global.env ()) gr - let constr_of_global_univ (gr,u) = match gr with | VarRef id -> mkVar id @@ -514,25 +466,6 @@ let type_of_reference env r = let type_of_global t = type_of_reference (Global.env ()) t -let unsafe_type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env - | ConstRef c -> - let cb = Environ.lookup_constant c env in - Typeops.type_of_constant_type env cb.const_type - - | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - let (_, inst), _ = unsafe_inductive_instance env ind in - Inductive.type_of_inductive env (specif, inst) - - | ConstructRef (ind, _ as cstr) -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - let (_, inst), _ = unsafe_inductive_instance env ind in - Inductive.type_of_constructor (cstr,inst) specif - -let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t - let fresh_sort_in_family env = function | InProp -> prop_sort, ContextSet.empty | InSet -> set_sort, ContextSet.empty |