diff options
Diffstat (limited to 'engine/universes.ml')
-rw-r--r-- | engine/universes.ml | 178 |
1 files changed, 99 insertions, 79 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index f20108186..bd4d75930 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -283,11 +283,11 @@ let new_Type_sort dp = Type (new_univ dp) let fresh_universe_instance ctx = Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) - (UContext.instance ctx) + (AUContext.instance ctx) let fresh_instance_from_context ctx = let inst = fresh_universe_instance ctx in - let constraints = instantiate_univ_constraints inst ctx in + let constraints = UContext.constraints (subst_instance_context inst ctx) in inst, constraints let fresh_instance ctx = @@ -296,13 +296,13 @@ let fresh_instance ctx = Instance.subst_fn (fun v -> let u = new_univ_level (Global.current_dirpath ()) in ctx' := LSet.add u !ctx'; u) - (UContext.instance ctx) + (AUContext.instance ctx) in !ctx', inst let existing_instance ctx inst = let () = let a1 = Instance.to_array inst - and a2 = Instance.to_array (UContext.instance ctx) in + and a2 = Instance.to_array (AUContext.instance ctx) in let len1 = Array.length a1 and len2 = Array.length a2 in if not (len1 == len2) then CErrors.user_err ~hdr:"Universes" @@ -317,59 +317,75 @@ let fresh_instance_from ctx inst = | Some inst -> existing_instance ctx inst | None -> fresh_instance ctx in - let constraints = instantiate_univ_constraints inst ctx in + let constraints = UContext.constraints (subst_instance_context inst ctx) in inst, (ctx', constraints) let unsafe_instance_from ctx = - (Univ.UContext.instance ctx, ctx) + (Univ.AUContext.instance ctx, Univ.instantiate_univ_context ctx) (** Fresh universe polymorphic construction *) let fresh_constant_instance env c inst = let cb = lookup_constant c env in - if cb.Declarations.const_polymorphic then - let inst, ctx = - fresh_instance_from - (Declareops.universes_of_constant (Environ.opaque_tables env) cb) inst - in - ((c, inst), ctx) - else ((c,Instance.empty), ContextSet.empty) + match cb.Declarations.const_universes with + | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_const auctx -> + let inst, ctx = + fresh_instance_from auctx inst + in + ((c, inst), ctx) let fresh_inductive_instance env ind inst = let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in - ((ind,inst), ctx) - else ((ind,Instance.empty), ContextSet.empty) + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + ((ind,Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind uactx -> + let inst, ctx = (fresh_instance_from uactx) inst in + ((ind,inst), ctx) + | Declarations.Cumulative_ind acumi -> + let inst, ctx = + fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst + in ((ind,inst), ctx) let fresh_constructor_instance env (ind,i) inst = let mib, mip = Inductive.lookup_mind_specif env ind in - if mib.Declarations.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.Declarations.mind_universes inst in + match mib.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty) + | Declarations.Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx inst in (((ind,i),inst), ctx) - else (((ind,i),Instance.empty), ContextSet.empty) + | Declarations.Cumulative_ind acumi -> + 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 - if cb.Declarations.const_polymorphic then - let inst, ctx = unsafe_instance_from - (Declareops.universes_of_constant (Environ.opaque_tables env) cb) in - ((c, inst), ctx) - else ((c,Instance.empty), UContext.empty) + 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 - if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in - ((ind,inst), ctx) - else ((ind,Instance.empty), UContext.empty) + 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 - if mib.Declarations.mind_polymorphic then - let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in - (((ind,i),inst), ctx) - else (((ind,i),Instance.empty), UContext.empty) + 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 @@ -452,26 +468,49 @@ let type_of_reference env r = | ConstRef c -> let cb = Environ.lookup_constant c env in let ty = Typeops.type_of_constant_type env cb.const_type in - if cb.const_polymorphic then - let inst, ctx = fresh_instance_from (Declareops.universes_of_constant (Environ.opaque_tables env) cb) None in - Vars.subst_instance_constr inst ty, ctx - else ty, ContextSet.empty - + begin + match cb.const_universes with + | Monomorphic_const _ -> ty, ContextSet.empty + | Polymorphic_const auctx -> + let inst, ctx = fresh_instance_from auctx None in + Vars.subst_instance_constr inst ty, ctx + end | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in + ty, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - else - let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in - ty, ContextSet.empty + ty, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + end + | ConstructRef cstr -> - let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - if mib.mind_polymorphic then - let inst, ctx = fresh_instance_from mib.mind_universes None in - Inductive.type_of_constructor (cstr,inst) specif, ctx - else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + let (mib,oib as specif) = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) + in + begin + match mib.mind_universes with + | Monomorphic_ind _ -> + Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + | Polymorphic_ind auctx -> + let inst, ctx = fresh_instance_from auctx None in + Inductive.type_of_constructor (cstr,inst) specif, ctx + | Cumulative_ind cumi -> + let inst, ctx = + fresh_instance_from (ACumulativityInfo.univ_context cumi) None + in + Inductive.type_of_constructor (cstr,inst) specif, ctx + end let type_of_global t = type_of_reference (Global.env ()) t @@ -976,36 +1015,6 @@ let normalize_context_set ctx us algs = (* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) (* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) -let universes_of_constr c = - let rec aux s c = - match kind_of_term c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> fold_constr aux s c - in aux LSet.empty c - -let restrict_universe_context (univs,csts) s = - (* Universes that are not necessary to typecheck the term. - E.g. univs introduced by tactics and not used in the proof term. *) - let diff = LSet.diff univs s in - let rec aux diff candid univs ness = - let (diff', candid', univs', ness') = - Constraint.fold - (fun (l, d, r as c) (diff, candid, univs, csts) -> - if not (LSet.mem l diff) then - (LSet.remove r diff, candid, univs, Constraint.add c csts) - else if not (LSet.mem r diff) then - (LSet.remove l diff, candid, univs, Constraint.add c csts) - else (diff, Constraint.add c candid, univs, csts)) - candid (diff, Constraint.empty, univs, ness) - in - if ness' == ness then (LSet.diff univs diff', ness) - else aux diff' candid' univs' ness' - in aux diff csts univs Constraint.empty - let simplify_universe_context (univs,csts) = let uf = UF.create () in let noneqs = @@ -1118,3 +1127,14 @@ let solve_constraints_system levels level_bounds level_min = done; done; v + + +(** Operations for universe_info_ind *) + +(** Given a universe context representing constraints of an inductive + this function produces a UInfoInd.t that with the trivial subtyping relation. *) +let univ_inf_ind_from_universe_context univcst = + let freshunivs = Instance.of_array + (Array.map (fun _ -> new_univ_level ()) + (Instance.to_array (UContext.instance univcst))) + in CumulativityInfo.from_universe_context univcst freshunivs |