diff options
Diffstat (limited to 'checker/inductive.ml')
| -rw-r--r-- | checker/inductive.ml | 87 |
1 files changed, 27 insertions, 60 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index adb9e0347d..c23b2578b1 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -54,29 +54,20 @@ let inductive_params (mib,_) = mib.mind_nparams (** Polymorphic inductives *) -let make_inductive_subst mib u = - if mib.mind_polymorphic then - Univ.make_universe_subst u mib.mind_universes - else Univ.empty_level_subst - -let inductive_paramdecls (mib,u) = - let subst = make_inductive_subst mib u in - subst_univs_level_context subst mib.mind_params_ctxt - let inductive_instance mib = - if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty + if mib.mind_polymorphic then + UContext.instance mib.mind_universes + else Instance.empty let inductive_context mib = if mib.mind_polymorphic then - mib.mind_universes - else Univ.UContext.empty + instantiate_univ_context mib.mind_universes + else UContext.empty -let instantiate_inductive_constraints mib subst = +let instantiate_inductive_constraints mib u = if mib.mind_polymorphic then - Univ.instantiate_univ_context subst mib.mind_universes - else Univ.Constraint.empty + subst_instance_constraints u (UContext.constraints mib.mind_universes) + else Constraint.empty (************************************************************************) @@ -88,9 +79,9 @@ let ind_subst mind mib u = List.init ntypes make_Ik (* Instantiate inductives in constructor type *) -let constructor_instantiate mind u subst mib c = +let constructor_instantiate mind u mib c = let s = ind_subst mind mib u in - substl s (subst_univs_level_constr subst c) + substl s (subst_instance_constr u c) let instantiate_params full t args sign = let fail () = @@ -112,13 +103,11 @@ let instantiate_params full t args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in let t = mkArity (sign,dummy) in - let subst = make_inductive_subst mib u in let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in - subst_univs_level_context subst ar + subst_instance_context u ar let full_constructor_instantiate ((mind,_),u,(mib,_),params) = - let subst = make_inductive_subst mib u in - let inst_ind = constructor_instantiate mind u subst mib in + let inst_ind = constructor_instantiate mind u mib in (fun t -> instantiate_params true (inst_ind t) params mib.mind_params_ctxt) @@ -155,8 +144,8 @@ let sort_as_univ = function let cons_subst u su subst = try - (u, Univ.sup su (List.assoc_f Univ.Universe.equal u subst)) :: - List.remove_assoc_f Univ.Universe.equal u subst + (u, Univ.sup su (List.assoc_f Univ.Level.equal u subst)) :: + List.remove_assoc_f Univ.Level.equal u subst with Not_found -> (u, su) :: subst let actualize_decl_level env lev t = @@ -225,30 +214,11 @@ let is_prop_sort = function | Prop Null -> true | _ -> false -let type_of_inductive_subst ?(polyprop=true) env ((mib,mip),u) paramtyps = - match mip.mind_arity with - | RegularArity a -> - if not mib.mind_polymorphic then (a.mind_user_arity, Univ.LMap.empty) - else - let subst = make_inductive_subst mib u in - (subst_univs_level_constr subst a.mind_user_arity, subst) - | TemplateArity ar -> - let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes env ctx ar paramtyps in - (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. - the situation where a non-Prop singleton inductive becomes Prop - when applied to Prop params *) - if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s - then raise (SingletonInductiveBecomesProp mip.mind_typename); - mkArity (List.rev ctx,s), Univ.LMap.empty - let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> if not mib.mind_polymorphic then a.mind_user_arity - else - let subst = make_inductive_subst mib u in - (subst_univs_level_constr subst a.mind_user_arity) + else subst_instance_constr u a.mind_user_arity | TemplateArity ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in @@ -263,13 +233,13 @@ let type_of_inductive env pind = type_of_inductive_gen env pind [||] let constrained_type_of_inductive env ((mib,mip),u as pind) = - let ty, subst = type_of_inductive_subst env pind [||] in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_inductive_gen env pind [||] in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = - let ty, subst = type_of_inductive_subst env pind args in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_inductive_gen env pind args in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let type_of_inductive_knowing_parameters env mip args = @@ -293,36 +263,33 @@ let max_inductive_sort = (************************************************************************) (* Type of a constructor *) -let type_of_constructor_subst cstr u subst (mib,mip) = +let type_of_constructor_subst cstr u (mib,mip) = let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in if i > nconstr then error "Not enough constructors in the type."; - let c = constructor_instantiate (fst ind) u subst mib specif.(i-1) in - c + constructor_instantiate (fst ind) u mib specif.(i-1) let type_of_constructor_gen (cstr,u) (mib,mip as mspec) = - let subst = make_inductive_subst mib u in - type_of_constructor_subst cstr u subst mspec, subst + type_of_constructor_subst cstr u mspec let type_of_constructor cstru mspec = - fst (type_of_constructor_gen cstru mspec) + type_of_constructor_gen cstru mspec let type_of_constructor_in_ctx cstr (mib,mip as mspec) = let u = Univ.UContext.instance mib.mind_universes in let c = type_of_constructor_gen (cstr, u) mspec in - (fst c, mib.mind_universes) + (c, mib.mind_universes) let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = - let ty, subst = type_of_constructor_gen cstru ind in - let cst = instantiate_inductive_constraints mib subst in + let ty = type_of_constructor_gen cstru ind in + let cst = instantiate_inductive_constraints mib u in (ty, cst) let arities_of_specif (kn,u) (mib,mip) = let specif = mip.mind_nf_lc in - let subst = make_inductive_subst mib u in - Array.map (constructor_instantiate kn u subst mib) specif + Array.map (constructor_instantiate kn u mib) specif |