diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /checker/inductive.ml | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 33 |
1 files changed, 27 insertions, 6 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 30c5f878a..e1860a23f 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -54,10 +54,31 @@ let inductive_params (mib,_) = mib.mind_nparams (** Polymorphic inductives *) -let inductive_instance mib = - if mib.mind_polymorphic then - UContext.instance (UInfoInd.univ_context mib.mind_universes) - else Instance.empty +let inductive_is_polymorphic mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> true + | Cumulative_ind cumi -> true + +let inductive_is_cumulative mib = + match mib.mind_universes with + | Monomorphic_ind _ -> false + | Polymorphic_ind ctx -> false + | Cumulative_ind cumi -> true + +let inductive_polymorphic_instance mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Instance.empty + | Polymorphic_ind ctx -> Univ.AUContext.instance ctx + | Cumulative_ind cumi -> + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + +let inductive_polymorphic_context mib = + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.UContext.empty + | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx + | Cumulative_ind cumi -> + Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi) (************************************************************************) @@ -93,7 +114,7 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (subst_instance_context u sign,dummy) in + let t = mkArity (Term.subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = @@ -199,7 +220,7 @@ let instantiate_universes env ctx ar argsorts = let type_of_inductive_gen env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> - if not mib.mind_polymorphic then a.mind_user_arity + if not (inductive_is_polymorphic mib) then a.mind_user_arity else subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in |