aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inductiveops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/inductiveops.ml')
-rw-r--r--pretyping/inductiveops.ml146
1 files changed, 28 insertions, 118 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 78e6bc6f1..275a079d5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -84,7 +84,7 @@ let mis_is_recursive_subset listind rarg =
List.exists
(fun ra ->
match dest_recarg ra with
- | Mrec (_,i) -> Int.List.mem i listind
+ | Mrec (_,i) -> Int.List.mem i listind
| _ -> false) rvec
in
Array.exists one_is_rec (dest_subterms rarg)
@@ -361,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches =
if (* dependent *) not (Vars.noccurn sigma 1 t) &&
not (has_dependent_elim mib) then
user_err ~hdr:"make_case_or_project"
- Pp.(str"Dependent case analysis not allowed" ++
- str" on inductive type " ++ Names.MutInd.print (fst ind))
+ Pp.(str"Dependent case analysis not allowed" ++
+ str" on inductive type " ++ Names.MutInd.print (fst ind))
in
let branch = branches.(0) in
let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
let n, subst =
List.fold_right
(fun decl (i, subst) ->
- match decl with
- | LocalAssum (na, t) ->
- let t = mkProj (Projection.make ps.(i) true, c) in
- (i + 1, t :: subst)
- | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
- ctx (0, [])
+ match decl with
+ | LocalAssum (na, t) ->
+ let t = mkProj (Projection.make ps.(i) true, c) in
+ (i + 1, t :: subst)
+ | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
+ ctx (0, [])
in Vars.substl subst br
(* substitution in a signature *)
@@ -511,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign =
let pv' = whd_all env sigma pval in
match EConstr.kind sigma pv', arsign with
| Lambda (na,t,b), (LocalAssum _)::arsign ->
- srec (push_rel_assum (na, t) env) b arsign
+ srec (push_rel_assum (na, t) env) b arsign
| Lambda (na,_,t), _ ->
(* The following code has an impact on the introduction names
- given by the tactics "case" and "inversion": when the
- elimination is not dependent, "case" uses Anonymous for
- inductive types in Prop and names created by mkProd_name for
- inductive types in Set/Type while "inversion" uses anonymous
- for inductive types both in Prop and Set/Type !!
-
- Previously, whether names were created or not relied on
- whether the predicate created in Indrec.make_case_com had a
- dependent arity or not. To avoid different predicates
- printed the same in v8, all predicates built in indrec.ml
- got a dependent arity (Aug 2004). The new way to decide
- whether names have to be created or not is to use an
- Anonymous or Named variable to enforce the expected
- dependency status (of course, Anonymous implies non
- dependent, but not conversely).
+ given by the tactics "case" and "inversion": when the
+ elimination is not dependent, "case" uses Anonymous for
+ inductive types in Prop and names created by mkProd_name for
+ inductive types in Set/Type while "inversion" uses anonymous
+ for inductive types both in Prop and Set/Type !!
+
+ Previously, whether names were created or not relied on
+ whether the predicate created in Indrec.make_case_com had a
+ dependent arity or not. To avoid different predicates
+ printed the same in v8, all predicates built in indrec.ml
+ got a dependent arity (Aug 2004). The new way to decide
+ whether names have to be created or not is to use an
+ Anonymous or Named variable to enforce the expected
+ dependency status (of course, Anonymous implies non
+ dependent, but not conversely).
From Coq > 8.2, using or not the the effective dependency of
the predicate is parametrable! *)
@@ -600,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function
let ctx,_ = Reduction.dest_arity env ty in
let u = Univ.Universe.make l in
let s =
- (* Does the sort of parameter [u] appear in (or equal)
+ (* Does the sort of parameter [u] appear in (or equal)
the sort of inductive [is] ? *)
if univ_level_mem l is then
scl (* constrained sort: replace by scl *)
else
(* unconstrained sort: replace by fresh universe *)
let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
- let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
- evdref := evm; s
+ let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
+ evdref := evm; s
in
(LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp)
| sign, [] -> sign (* Uniform parameters are exhausted *)
@@ -656,93 +656,3 @@ let control_only_guard env c =
iter_constr_with_full_binders push_rel iter env c
in
iter env c
-
-(* inference of subtyping condition for inductive types *)
-
-let infer_inductive_subtyping_arity_constructor
- (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) =
- let numchecked = ref 0 in
- let numparams = Context.Rel.nhyps params in
- let update_contexts (env, evd, csts) csts' =
- (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
- in
- let basic_check (env, evd, csts) tp =
- let result =
- if !numchecked >= numparams then
- let csts' =
- Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
- in update_contexts (env, evd, csts) csts'
- else
- (env, evd, csts)
- in
- numchecked := !numchecked + 1; result
- in
- let infer_typ typ ctxs =
- match typ with
- | LocalAssum (_, typ') ->
- begin
- try
- let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
- with Reduction.NotConvertible ->
- anomaly ~label:"inference of record/inductive subtyping relation failed"
- (Pp.str "Can't infer subtyping for record/inductive type")
- end
- | _ -> anomaly (Pp.str "")
- in
- let arcn' = Term.it_mkProd_or_LetIn arcn params in
- let typs, codom = Reduction.dest_prod env arcn' in
- let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
- if not is_arity then basic_check last_contexts codom else last_contexts
-
-let infer_inductive_subtyping env evd mind_ent =
- let { Entries.mind_entry_params = params;
- Entries.mind_entry_inds = entries;
- Entries.mind_entry_universes = ground_univs;
- } = mind_ent
- in
- let uinfind =
- match ground_univs with
- | Entries.Monomorphic_ind_entry _
- | Entries.Polymorphic_ind_entry _ -> ground_univs
- | Entries.Cumulative_ind_entry cumi ->
- begin
- let uctx = Univ.CumulativityInfo.univ_context cumi in
- let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
- let dosubst = subst_univs_level_constr sbsubst in
- let instance_other =
- Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx)
- in
- let constraints_other =
- Univ.subst_univs_level_constraints
- sbsubst (Univ.UContext.constraints uctx)
- in
- let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
- let env = Environ.push_context uctx env in
- let env = Environ.push_context uctx_other env in
- let evd =
- Evd.merge_universe_context
- evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other))
- in
- let (_, _, subtyp_constraints) =
- List.fold_left
- (fun ctxs indentry ->
- let _, params = Typeops.infer_local_decls env params in
- let ctxs' = infer_inductive_subtyping_arity_constructor
- ctxs dosubst indentry.Entries.mind_entry_arity true params
- in
- List.fold_left
- (fun ctxs cons ->
- infer_inductive_subtyping_arity_constructor
- ctxs dosubst cons false params
- )
- ctxs' indentry.Entries.mind_entry_lc
- ) (env, evd, Univ.Constraint.empty) entries
- in
- Entries.Cumulative_ind_entry
- (Univ.CumulativityInfo.make
- (Univ.CumulativityInfo.univ_context cumi,
- Univ.UContext.make
- (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi),
- subtyp_constraints)))
- end
- in {mind_ent with Entries.mind_entry_universes = uinfind;}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 04:39:24 +0000