diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 3 | ||||
| -rw-r--r-- | engine/namegen.ml | 5 | ||||
| -rw-r--r-- | engine/termops.ml | 3 | ||||
| -rw-r--r-- | engine/uState.ml | 2 | ||||
| -rw-r--r-- | engine/universes.ml | 178 | ||||
| -rw-r--r-- | engine/universes.mli | 14 |
6 files changed, 114 insertions, 91 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 08d26f40d4..bf1e052b63 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -659,8 +659,7 @@ let restrict evk filter ?candidates ?src evd = let evar_info' = { evar_info with evar_filter = filter; evar_candidates = candidates; - evar_source = (match src with None -> evar_info.evar_source | Some src -> src); - evar_extra = Store.empty } in + evar_source = (match src with None -> evar_info.evar_source | Some src -> src) } in let last_mods = match evd.conv_pbs with | [] -> evd.last_mods | _ -> Evar.Set.add evk evd.last_mods in diff --git a/engine/namegen.ml b/engine/namegen.ml index 5bd62273c8..783085654e 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -412,13 +412,12 @@ let rename_bound_vars_as_displayed sigma avoid env c = let h_based_elimination_names = ref false -let use_h_based_elimination_names () = - !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4 +let use_h_based_elimination_names () = !h_based_elimination_names open Goptions let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "use of \"H\"-based proposition names in elimination tactics"; optkey = ["Standard";"Proposition";"Elimination";"Names"]; optread = (fun () -> !h_based_elimination_names); diff --git a/engine/termops.ml b/engine/termops.ml index 92016d4af4..3eef71b2d0 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1173,6 +1173,9 @@ let compare_constr_univ sigma f cv_pb t1 t2 = Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2) | Prod (_,t1,c1), Prod (_,t2,c2) -> f Reduction.CONV t1 t2 && f cv_pb c1 c2 + | Const (c, u), Const (c', u') -> Constant.equal c c' + | Ind (i, _), Ind (i', _) -> eq_ind i i' + | Construct (i, _), Construct (i', _) -> eq_constructor i i' | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 let constr_cmp sigma cv_pb t1 t2 = diff --git a/engine/uState.ml b/engine/uState.ml index acef901432..0973ca457f 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -284,7 +284,7 @@ let universe_context ?names ctx = in map, ctx let restrict ctx vars = - let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in + let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } type rigid = diff --git a/engine/universes.ml b/engine/universes.ml index f201081862..bd4d75930c 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 diff --git a/engine/universes.mli b/engine/universes.mli index 83ca1ea606..5ce5e4a42a 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -101,10 +101,10 @@ val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrai (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) -val fresh_instance_from_context : universe_context -> +val fresh_instance_from_context : abstract_universe_context -> universe_instance constrained -val fresh_instance_from : universe_context -> universe_instance option -> +val fresh_instance_from : abstract_universe_context -> universe_instance option -> universe_instance in_universe_context_set val fresh_sort_in_family : env -> sorts_family -> @@ -210,10 +210,6 @@ val unsafe_type_of_global : Globnames.global_reference -> types val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr -(** Shrink a universe context to a restricted set of variables *) - -val universes_of_constr : constr -> universe_set -val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst @@ -227,3 +223,9 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds val solve_constraints_system : universe option array -> universe array -> universe array -> universe array + +(** 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. *) +val univ_inf_ind_from_universe_context : universe_context -> cumulativity_info |