aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml8
-rw-r--r--pretyping/cases.ml6
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/constr_matching.ml10
-rw-r--r--pretyping/detyping.ml14
-rw-r--r--pretyping/evarconv.ml19
-rw-r--r--pretyping/evardefine.ml4
-rw-r--r--pretyping/glob_ops.ml10
-rw-r--r--pretyping/inductiveops.ml146
-rw-r--r--pretyping/inductiveops.mli9
-rw-r--r--pretyping/inferCumulativity.ml224
-rw-r--r--pretyping/inferCumulativity.mli10
-rw-r--r--pretyping/nativenorm.ml28
-rw-r--r--pretyping/patternops.ml6
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/recordops.ml27
-rw-r--r--pretyping/reductionops.ml92
-rw-r--r--pretyping/reductionops.mli6
-rw-r--r--pretyping/tacred.ml16
-rw-r--r--pretyping/typeclasses.ml3
-rw-r--r--pretyping/typing.ml5
-rw-r--r--pretyping/typing.mli1
-rw-r--r--pretyping/unification.ml10
-rw-r--r--pretyping/vnorm.ml18
25 files changed, 387 insertions, 300 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index d59102b6c7..8ac471404a 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -40,16 +40,10 @@ let subst_rename_args (subst, (_, (r, names as orig))) =
let r' = fst (subst_global subst r) in
if r==r' then orig else (r', names)
-let section_segment_of_reference = function
- | ConstRef con -> Lib.section_segment_of_constant con
- | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- Lib.section_segment_of_mutual_inductive kn
- | _ -> [], Univ.LMap.empty, Univ.AUContext.empty
-
let discharge_rename_args = function
| _, (ReqGlobal (c, names), _ as req) ->
(try
- let vars,_,_ = section_segment_of_reference c in
+ let vars = Lib.variable_section_segment_of_reference c in
let c' = pop_global_reference c in
let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
let names' = var_names @ names in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1207c967b5..311c1c09ec 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1276,7 +1276,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
(* This is a bit too strong I think, in the sense that what we would *)
(* really like is to have beta-iota reduction only at the positions where *)
(* parameters are substituted *)
- let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in
+ let typs = List.map (map_type (nf_betaiota pb.env !(pb.evdref))) typs in
(* We build the matrix obtained by expanding the matching on *)
(* "C x1..xn as x" followed by a residual matching on eqn into *)
@@ -1426,7 +1426,7 @@ and match_current pb (initial,tomatch) =
find_predicate pb.caseloc pb.env pb.evdref
pred current indt (names,dep) tomatch in
let ci = make_case_info pb.env (fst mind) pb.casestyle in
- let pred = nf_betaiota !(pb.evdref) pred in
+ let pred = nf_betaiota pb.env !(pb.evdref) pred in
let case =
make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
in
@@ -1663,7 +1663,7 @@ let rec list_assoc_in_triple x = function
*)
let abstract_tycon ?loc env evdref subst tycon extenv t =
- let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*)
+ let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*)
let src = match EConstr.kind !evdref t with
| Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk)
| _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 192eca63bb..e42576d95b 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -171,7 +171,7 @@ let fixp_reducible flgs ((reci,i),_) stk =
let cofixp_reducible flgs _ stk =
if red_set flgs fCOFIX then
match stk with
- | (CASE _ | APP(_,CASE _)) -> true
+ | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true
| _ -> false
else
false
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index ec7c3077fb..c3a221944d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -462,19 +462,21 @@ let sub_match ?(closed=true) env sigma pat c =
in
let sub = (env, c1) :: (env, hd) :: subargs env lc in
try_aux sub next_mk_ctx next
- | Fix (indx,(names,types,bodies)) ->
+ | Fix (indx,(names,types,bodies as recdefs)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
let (ntypes,nbodies) = CList.chop nb_fix le in
mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in
- let sub = subargs env types @ subargs env bodies in
+ let env' = push_rec_types recdefs env in
+ let sub = subargs env types @ subargs env' bodies in
try_aux sub next_mk_ctx next
- | CoFix (i,(names,types,bodies)) ->
+ | CoFix (i,(names,types,bodies as recdefs)) ->
let nb_fix = Array.length types in
let next_mk_ctx le =
let (ntypes,nbodies) = CList.chop nb_fix le in
mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in
- let sub = subargs env types @ subargs env bodies in
+ let env' = push_rec_types recdefs env in
+ let sub = subargs env types @ subargs env' bodies in
try_aux sub next_mk_ctx next
| Proj (p,c') ->
begin try
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 23993243f4..754e881398 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -581,12 +581,7 @@ and detype_r d flags avoid env sigma t =
| Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
| Proj (p,c) ->
let noparams () =
- let pb = Environ.lookup_projection p (snd env) in
- let pars = pb.Declarations.proj_npars in
- let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
- let args = List.make pars hole in
- GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
- (args @ [detype d flags avoid env sigma c]))
+ GProj (p, detype d flags avoid env sigma c)
in
if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
try noparams ()
@@ -1002,6 +997,13 @@ let rec subst_glob_constr subst = DAst.map (function
let r1' = subst_glob_constr subst r1 in
let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
if r1' == r1 && k' == k then raw else GCast (r1',k')
+
+ | GProj (p,c) as raw ->
+ let kn = Projection.constant p in
+ let b = Projection.unfolded p in
+ let kn' = subst_constant subst kn in
+ let c' = subst_glob_constr subst c in
+ if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c')
)
(* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 788e4d268a..dc3acbc3e2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -276,11 +276,6 @@ let rec ise_app_stack2 env f evd sk1 sk2 =
end
| _, _ -> (sk1,sk2), Success evd
-let push_rec_types pfix env =
- let (i, c, t) = pfix in
- let inj c = EConstr.Unsafe.to_constr c in
- push_rec_types (i, Array.map inj c, Array.map inj t) env
-
(* This function tries to unify 2 stacks element by element. It works
from the end to the beginning. If it unifies a non empty suffix of
stacks but not the entire stacks, the first part of the answer is
@@ -358,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
let check_leq_inductives evd cumi u u' =
let u = EConstr.EInstance.kind evd u in
let u' = EConstr.EInstance.kind evd u' in
- let length_ind_instance =
- Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
- in
- let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in
- if not ((length_ind_instance = Univ.Instance.length u) &&
- (length_ind_instance = Univ.Instance.length u')) then
- anomaly (Pp.str "Invalid inductive subtyping encountered!")
- else
- begin
- let comp_subst = (Univ.Instance.append u u') in
- let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in
- Evd.add_constraints evd comp_cst
- end
+ Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u')
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index b646a37f8a..fd83795f55 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -28,8 +28,8 @@ let env_nf_evar sigma env =
let env_nf_betaiotaevar sigma env =
process_rel_context
- (fun d e ->
- push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env
+ (fun d env ->
+ push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota env sigma c) d) env) env
(****************************************)
(* Operations on value/type constraints *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 093f1f0b68..a21137a05c 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -133,8 +133,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
Miscops.intro_pattern_naming_eq nam1 nam2
| GCast (c1, t1), GCast (c2, t2) ->
f c1 c2 && cast_type_eq f t1 t2
+ | GProj (p1, t1), GProj (p2, t2) ->
+ Projection.equal p1 p2 && f t1 t2
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
- GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false
+ GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false
let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
@@ -180,6 +182,8 @@ let map_glob_constr_left_to_right f = DAst.map (function
let comp1 = f c in
let comp2 = Miscops.map_cast_type f k in
GCast (comp1,comp2)
+ | GProj (p,c) ->
+ GProj (p, f c)
| (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
)
@@ -212,6 +216,8 @@ let fold_glob_constr f acc = DAst.with_val (function
let acc = match k with
| CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
f acc c
+ | GProj(_,c) ->
+ f acc c
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
)
@@ -253,6 +259,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
let acc = match k with
| CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
f v acc c
+ | GProj(_,c) ->
+ f v acc c
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc))
let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 78e6bc6f14..275a079d5d 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;}
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 58b1ce6c3f..55149552aa 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -199,12 +199,3 @@ val type_of_inductive_knowing_conclusion :
(********************)
val control_only_guard : env -> types -> unit
-
-(* inference of subtyping condition for inductive types *)
-(* for debugging purposes only to be removed *)
-val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
-(constr -> constr) ->
-types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
-
-val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
- Entries.mutual_inductive_entry
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
new file mode 100644
index 0000000000..a0a8276c5c
--- /dev/null
+++ b/pretyping/inferCumulativity.ml
@@ -0,0 +1,224 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Reduction
+open Declarations
+open Constr
+open Univ
+open Util
+
+(** Throughout this module we modify a map [variances] from local
+ universes to [Variance.t]. It starts as a trivial mapping to
+ [Irrelevant] and every time we encounter a local universe we
+ restrict it accordingly. *)
+
+let infer_level_eq u variances =
+ if LMap.mem u variances
+ then LMap.set u Variance.Invariant variances
+ else variances
+
+let infer_level_leq u variances =
+ match LMap.find u variances with
+ | exception Not_found -> variances
+ | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances
+
+let infer_generic_instance_eq variances u =
+ Array.fold_left (fun variances u -> infer_level_eq u variances)
+ variances (Instance.to_array u)
+
+let variance_pb cv_pb var =
+ let open Variance in
+ match cv_pb, var with
+ | _, Irrelevant -> Irrelevant
+ | _, Invariant -> Invariant
+ | CONV, Covariant -> Invariant
+ | CUMUL, Covariant -> Covariant
+
+let infer_cumulative_ind_instance cv_pb cumi variances u =
+ Array.fold_left2 (fun variances varu u ->
+ match LMap.find u variances with
+ | exception Not_found -> variances
+ | varu' ->
+ LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
+ variances (ACumulativityInfo.variance cumi) (Instance.to_array u)
+
+let infer_inductive_instance cv_pb env variances ind nargs u =
+ let mind = Environ.lookup_mind (fst ind) env in
+ match mind.mind_universes with
+ | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
+ | Polymorphic_ind _ -> infer_generic_instance_eq variances u
+ | Cumulative_ind cumi ->
+ if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
+ then infer_generic_instance_eq variances u
+ else infer_cumulative_ind_instance cv_pb cumi variances u
+
+let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
+ let mind = Environ.lookup_mind mi env in
+ match mind.mind_universes with
+ | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
+ | Polymorphic_ind _ -> infer_generic_instance_eq variances u
+ | Cumulative_ind cumi ->
+ if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
+ then infer_generic_instance_eq variances u
+ else infer_cumulative_ind_instance CONV cumi variances u
+
+let infer_sort cv_pb variances s =
+ match cv_pb with
+ | CONV ->
+ LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances
+ | CUMUL ->
+ LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
+
+let infer_table_key infos variances c =
+ let open Names in
+ match c with
+ | ConstKey (_, u) ->
+ infer_generic_instance_eq variances u
+ | VarKey _ | RelKey _ -> variances
+
+let rec infer_fterm cv_pb infos variances hd stk =
+ Control.check_for_interrupt ();
+ let open CClosure in
+ let hd,stk = whd_stack infos hd stk in
+ match fterm_of hd with
+ | FAtom a ->
+ begin match kind a with
+ | Sort s -> infer_sort cv_pb variances s
+ | Meta _ -> infer_stack infos variances stk
+ | _ -> assert false
+ end
+ | FEvar ((_,args),e) ->
+ let variances = infer_stack infos variances stk in
+ infer_vect infos variances (Array.map (mk_clos e) args)
+ | FRel _ -> variances
+ | FFlex fl ->
+ let variances = infer_table_key infos variances fl in
+ infer_stack infos variances stk
+ | FProj (_,c) ->
+ let variances = infer_fterm CONV infos variances c [] in
+ infer_stack infos variances stk
+ | FLambda _ ->
+ let (_,ty,bd) = destFLambda mk_clos hd in
+ let variances = infer_fterm CONV infos variances ty [] in
+ infer_fterm CONV infos variances bd []
+ | FProd (_,dom,codom) ->
+ let variances = infer_fterm CONV infos variances dom [] in
+ infer_fterm cv_pb infos variances codom []
+ | FInd (ind, u) ->
+ let variances =
+ if Instance.is_empty u then variances
+ else
+ let nargs = stack_args_size stk in
+ infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
+ in
+ infer_stack infos variances stk
+ | FConstruct (ctor,u) ->
+ let variances =
+ if Instance.is_empty u then variances
+ else
+ let nargs = stack_args_size stk in
+ infer_constructor_instance_eq (info_env infos) variances ctor nargs u
+ in
+ infer_stack infos variances stk
+ | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
+ let n = Array.length cl in
+ let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in
+ let le = Esubst.subs_liftn n e in
+ let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
+ infer_stack infos variances stk
+
+ (* Removed by whnf *)
+ | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
+
+and infer_stack infos variances (stk:CClosure.stack) =
+ match stk with
+ | [] -> variances
+ | z :: stk ->
+ let open CClosure in
+ let variances = match z with
+ | Zapp v -> infer_vect infos variances v
+ | Zproj _ -> variances
+ | Zfix (fx,a) ->
+ let variances = infer_fterm CONV infos variances fx [] in
+ infer_stack infos variances a
+ | ZcaseT (ci,p,br,e) ->
+ let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
+ infer_vect infos variances (Array.map (mk_clos e) br)
+ | Zshift _ -> variances
+ | Zupdate _ -> variances
+ in
+ infer_stack infos variances stk
+
+and infer_vect infos variances v =
+ Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+
+let infer_term cv_pb env variances c =
+ let open CClosure in
+ let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in
+ let infos = create_clos_infos reds env in
+ infer_fterm cv_pb infos variances (CClosure.inject c) []
+
+let infer_arity_constructor env variances arcn is_arity params =
+ let numchecked = ref 0 in
+ let numparams = Context.Rel.nhyps params in
+ let basic_check env variances tp =
+ let variances =
+ if !numchecked >= numparams then
+ infer_term CUMUL env variances tp
+ else
+ variances
+ in
+ numchecked := !numchecked + 1; variances
+ in
+ let infer_typ typ (env,variances) =
+ match typ with
+ | Context.Rel.Declaration.LocalAssum (_, typ') ->
+ (Environ.push_rel typ env, basic_check env variances typ')
+ | Context.Rel.Declaration.LocalDef _ -> assert false
+ in
+ let arcn' = Term.it_mkProd_or_LetIn arcn params in
+ let typs, codom = Reduction.dest_prod env arcn' in
+ let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in
+ (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j}
+ i is irrelevant, j is invariant. *)
+ if not is_arity then basic_check env variances codom else variances
+
+let infer_inductive env mie =
+ let open Entries in
+ let { mind_entry_params = params;
+ mind_entry_inds = entries; } = mie
+ in
+ let univs =
+ match mie.mind_entry_universes with
+ | Monomorphic_ind_entry _
+ | Polymorphic_ind_entry _ as univs -> univs
+ | Cumulative_ind_entry cumi ->
+ let uctx = CumulativityInfo.univ_context cumi in
+ let uarray = Instance.to_array @@ UContext.instance uctx in
+ let env = Environ.push_context uctx env in
+ let variances =
+ Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
+ LMap.empty uarray
+ in
+ let variances = List.fold_left (fun variances entry ->
+ let _, params = Typeops.infer_local_decls env params in
+ let variances = infer_arity_constructor
+ env variances entry.mind_entry_arity true params
+ in
+ List.fold_left
+ (fun variances cons ->
+ infer_arity_constructor
+ env variances cons false params)
+ variances entry.mind_entry_lc)
+ variances
+ entries
+ in
+ let variances = Array.map (fun u -> LMap.find u variances) uarray in
+ Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
+ in
+ { mie with mind_entry_universes = univs }
diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli
new file mode 100644
index 0000000000..a5037ea475
--- /dev/null
+++ b/pretyping/inferCumulativity.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
+ Entries.mutual_inductive_entry
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 79e0afa72b..b41e15f5a6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -224,7 +224,7 @@ and nf_accu env sigma accu =
if Int.equal (accu_nargs accu) 0 then nf_atom env sigma atom
else
let a,typ = nf_atom_type env sigma atom in
- let _, args = nf_args env sigma accu typ in
+ let _, args = nf_args env sigma (args_of_accu accu) typ in
mkApp(a,Array.of_list args)
and nf_accu_type env sigma accu =
@@ -232,10 +232,10 @@ and nf_accu_type env sigma accu =
if Int.equal (accu_nargs accu) 0 then nf_atom_type env sigma atom
else
let a,typ = nf_atom_type env sigma atom in
- let t, args = nf_args env sigma accu typ in
+ let t, args = nf_args env sigma (args_of_accu accu) typ in
mkApp(a,Array.of_list args), t
-and nf_args env sigma accu t =
+and nf_args env sigma args t =
let aux arg (t,l) =
let _,dom,codom =
try decompose_prod env t with
@@ -246,7 +246,7 @@ and nf_args env sigma accu t =
let c = nf_val env sigma arg dom in
(subst1 c codom, c::l)
in
- let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in
+ let t,l = Array.fold_right aux args (t,[]) in
t, List.rev l
and nf_bargs env sigma b t =
@@ -277,7 +277,6 @@ and nf_atom env sigma atom =
let codom = nf_type env sigma (codom vn) in
mkProd(n,dom,codom)
| Ameta (mv,_) -> mkMeta mv
- | Aevar (ev,_) -> mkEvar ev
| Aproj(p,c) ->
let c = nf_accu env sigma c in
mkProj(Projection.make p true,c)
@@ -347,9 +346,9 @@ and nf_atom_type env sigma atom =
let env = push_rel (LocalAssum (n,dom)) env in
let codom,s2 = nf_type_sort env sigma (codom vn) in
mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
- | Aevar(ev,ty) ->
- let ty = nf_type env sigma ty in
- mkEvar ev, ty
+ | Aevar(evk,ty,args) ->
+ let ty = nf_type env sigma ty in
+ nf_evar env sigma evk ty args
| Ameta(mv,ty) ->
let ty = nf_type env sigma ty in
mkMeta mv, ty
@@ -386,6 +385,19 @@ and nf_predicate env sigma ind mip params v pT =
true, mkLambda(name,dom,body)
| _, _ -> false, nf_type env sigma v
+and nf_evar env sigma evk ty args =
+ let evi = try Evd.find sigma evk with Not_found -> assert false in
+ let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
+ if List.is_empty hyps then begin
+ assert (Int.equal (Array.length args) 0);
+ mkEvar (evk, [||]), ty
+ end
+ else
+ let fold accu d = Term.mkNamedProd_or_LetIn d accu in
+ let t = List.fold_left fold ty hyps in
+ let ty, args = nf_args env sigma args t in
+ mkEvar (evk, Array.of_list args), ty
+
let evars_of_evar_map sigma =
{ Nativelambda.evars_val = Evd.existential_opt_value sigma;
Nativelambda.evars_typ = Evd.existential_type sigma;
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 41e09004c6..1bec4a6f15 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -137,8 +137,7 @@ let rec head_pattern_bound t =
| PCase (_,p,c,br) -> head_pattern_bound c
| PRef r -> r
| PVar id -> VarRef id
- | PProj (p,c) -> ConstRef (Projection.constant p)
- | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _
+ | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _
-> raise BoundPattern
(* Perhaps they were arguments, but we don't beta-reduce *)
| PLambda _ -> raise BoundPattern
@@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
one non-trivial branch. These facts are used in [Constrextern]. *)
PCase (info, pred, pat_of_raw metas vars c, brs)
+ | GProj(p,c) ->
+ PProj(p, pat_of_raw metas vars c)
+
| GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
err ?loc (Pp.str "Non supported pattern."))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b930c5db83..8809558ff7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -70,7 +70,7 @@ let get_extra env sigma =
let ids = List.map get_id (named_context env) in
let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
- (rel_context env) ~init:(empty_csubst, [], avoid, named_context env)
+ (rel_context env) ~init:(empty_csubst, avoid, named_context env)
let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) }
let rel_context env = rel_context env.env
@@ -90,12 +90,11 @@ let push_rel_context sigma ctx env = {
let lookup_named id env = lookup_named id env.env
let e_new_evar env evdref ?src ?naming typ =
- let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in
let open Context.Named.Declaration in
let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in
let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
- let (subst, vsubst, _, nc) = Lazy.force env.extra in
- let typ' = subst2 subst vsubst typ in
+ let (subst, _, nc) = Lazy.force env.extra in
+ let typ' = csubst_subst subst typ in
let instance = inst_rels @ inst_vars in
let sign = val_of_named_context nc in
let sigma = !evdref in
@@ -738,6 +737,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = pretype_sort ?loc evdref s in
inh_conv_coerce_to_tycon ?loc env evdref j tycon
+ | GProj (p, c) ->
+ (* TODO: once GProj is used as an input syntax, use bidirectional typing here *)
+ let cj = pretype empty_tycon env evdref lvar c in
+ judge_of_projection env.ExtraEnv.env !evdref p cj
+
| GApp (f,args) ->
let fj = pretype empty_tycon env evdref lvar f in
let floc = loc_of_glob_constr f in
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 1da5b4567f..ae4ad0be7d 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -4,6 +4,7 @@ Locusops
Pretype_errors
Reductionops
Inductiveops
+InferCumulativity
Vnorm
Arguments_renaming
Nativenorm
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 9ff9a75b3e..ab1f3cd320 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -298,29 +298,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
(*s High-level declaration of a canonical structure *)
-let error_not_structure ref =
+let error_not_structure ref description =
user_err ~hdr:"object_declare"
- (Id.print (basename_of_global ref) ++ str" is not a structure object.")
+ (str"Could not declare a canonical structure " ++
+ (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
+ str(description)))
let check_and_decompose_canonical_structure ref =
- let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
+ let sp =
+ match ref with
+ ConstRef sp -> sp
+ | _ -> error_not_structure ref "Expected an instance of a record or structure."
+ in
let env = Global.env () in
let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
let vc = match Environ.constant_opt_value_in env (sp, u) with
| Some vc -> vc
- | None -> error_not_structure ref in
+ | None -> error_not_structure ref "Could not find its value in the global environment." in
let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
let body = EConstr.Unsafe.to_constr body in
let f,args = match kind body with
| App (f,args) -> f,args
- | _ -> error_not_structure ref in
+ | _ ->
+ error_not_structure ref "Expected a record or structure constructor applied to arguments." in
let indsp = match kind f with
| Construct ((indsp,1),u) -> indsp
- | _ -> error_not_structure ref in
- let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
+ | _ -> error_not_structure ref "Expected an instance of a record or structure." in
+ let s =
+ try lookup_structure indsp
+ with Not_found ->
+ error_not_structure ref
+ ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in
let ntrue_projs = List.count snd s.s_PROJKIND in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
- error_not_structure ref;
+ error_not_structure ref "Got too few arguments to the record or structure constructor.";
(sp,indsp)
let declare_canonical_structure ref =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ac88468545..418ea271cd 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -121,10 +121,10 @@ module ReductionBehaviour = struct
let r' = fst (subst_global subst r) in if r==r' then orig else (r',o)
let discharge = function
- | _,(ReqGlobal (ConstRef c, req), (_, b)) ->
+ | _,(ReqGlobal (ConstRef c as gr, req), (_, b)) ->
let b =
- if Lib.is_in_section (ConstRef c) then
- let vars, _, _ = Lib.section_segment_of_constant c in
+ if Lib.is_in_section gr then
+ let vars = Lib.variable_section_segment_of_reference gr in
let extra = List.length vars in
let nargs' =
if b.b_nargs = max_int then max_int
@@ -1241,9 +1241,9 @@ let clos_whd_flags flgs env sigma t =
(CClosure.inject (EConstr.Unsafe.to_constr t)))
with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
-let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
-let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
-let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ())
+let nf_beta = clos_norm_flags CClosure.beta
+let nf_betaiota = clos_norm_flags CClosure.betaiota
+let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta
let nf_all env sigma =
clos_norm_flags CClosure.all env sigma
@@ -1324,79 +1324,17 @@ let sigma_compare_instances ~flex i0 i1 sigma =
| Univ.UniverseInconsistency _ ->
raise Reduction.NotConvertible
-let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
- let len_instance =
- Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind)
- in
- let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in
- if not ((len_instance = Univ.Instance.length u) &&
- (len_instance = Univ.Instance.length u')) then
- anomaly (Pp.str "Invalid inductive subtyping encountered!")
- else
- let comp_cst =
- let comp_subst = (Univ.Instance.append u u') in
- Univ.AUContext.instantiate comp_subst ind_sbctx
- in
- let comp_cst =
- match cv_pb with
- Reduction.CONV ->
- let comp_subst = (Univ.Instance.append u' u) in
- let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in
- Univ.Constraint.union comp_cst comp_cst'
- | Reduction.CUMUL -> comp_cst
- in
- try Evd.add_constraints sigma comp_cst
- with Evd.UniversesDiffer
- | Univ.UniverseInconsistency _ ->
- raise Reduction.NotConvertible
-
-let sigma_conv_inductives
- cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
- try sigma_compare_instances ~flex:false u1 u2 sigma with
- Reduction.NotConvertible ->
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Polymorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Cumulative_ind cumi ->
- let num_param_arity =
- mind.Declarations.mind_nparams +
- mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
- in
- if not (num_param_arity = sv1 && num_param_arity = sv2) then
- raise Reduction.NotConvertible
- else
- sigma_check_inductive_instances cv_pb cumi u1 u2 sigma
-
-let sigma_conv_constructors
- (mind, ind, cns) u1 sv1 u2 sv2 sigma =
- try sigma_compare_instances ~flex:false u1 u2 sigma with
- Reduction.NotConvertible ->
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Polymorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Cumulative_ind cumi ->
- let num_cnstr_args =
- let nparamsctxt =
- mind.Declarations.mind_nparams +
- mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
- in
- nparamsctxt +
- mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
- in
- if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
- raise Reduction.NotConvertible
- else
- sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
+let sigma_check_inductive_instances csts sigma =
+ try Evd.add_constraints sigma csts
+ with Evd.UniversesDiffer
+ | Univ.UniverseInconsistency _ ->
+ raise Reduction.NotConvertible
let sigma_univ_state =
- { Reduction.compare = sigma_compare_sorts;
- Reduction.compare_instances = sigma_compare_instances;
- Reduction.conv_inductives = sigma_conv_inductives;
- Reduction.conv_constructors = sigma_conv_constructors}
+ let open Reduction in
+ { compare_sorts = sigma_compare_sorts;
+ compare_instances = sigma_compare_instances;
+ compare_cumul_instances = sigma_check_inductive_instances; }
let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
?(ts=full_transparent_state) env sigma x y =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index a277864c92..0565baf45f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -168,9 +168,9 @@ val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
(** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *)
-val nf_beta : local_reduction_function
-val nf_betaiota : local_reduction_function
-val nf_betaiotazeta : local_reduction_function
+val nf_beta : reduction_function
+val nf_betaiota : reduction_function
+val nf_betaiotazeta : reduction_function
val nf_all : reduction_function
val nf_evar : evar_map -> constr -> constr
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 5a522e06a5..9b9408698d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -60,9 +60,7 @@ let value_of_evaluable_ref env evref u =
match evref with
| EvalConstRef con ->
let u = Unsafe.to_instance u in
- EConstr.of_constr (try constant_value_in env (con,u)
- with NotEvaluableConst IsProj ->
- raise (Invalid_argument "value_of_evaluable_ref"))
+ EConstr.of_constr (constant_value_in env (con, u))
| EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get
let evaluable_of_global_reference env = function
@@ -476,7 +474,7 @@ let contract_fix_use_function env sigma f
let nbodies = Array.length recindices in
let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
let lbodies = List.init nbodies make_Fi in
- substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum))
+ substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum))
let reduce_fix_use_function env sigma f whfun fix stack =
match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
@@ -500,7 +498,7 @@ let contract_cofix_use_function env sigma f
let make_Fi j = (mkCoFix(j,typedbodies), f j) in
let subbodies = List.init nbodies make_Fi in
substl_checking_arity env (List.rev subbodies)
- sigma (nf_beta sigma bodies.(bodynum))
+ sigma (nf_beta env sigma bodies.(bodynum))
let reduce_mind_case_use_function func env sigma mia =
match EConstr.kind sigma mia.mconstr with
@@ -697,7 +695,7 @@ let rec red_elim_const env sigma ref u largs =
let whfun = whd_construct_stack env sigma in
(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
| NotReducible -> raise Redelimination
- | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
+ | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
| EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
let rec descend (ref,u) args =
let c = reference_value env sigma ref u in
@@ -712,7 +710,7 @@ let rec red_elim_const env sigma ref u largs =
let whfun = whd_construct_stack env sigma in
(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
| NotReducible -> raise Redelimination
- | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
+ | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
| NotAnElimination when unfold_nonelim ->
let c = reference_value env sigma ref u in
(whd_betaiotazeta sigma (applist (c, largs)), []), nocase
@@ -1103,7 +1101,7 @@ let unfoldoccs env sigma (occs,name) c =
| [] -> ()
| _ -> error_invalid_occurrence rest
in
- nf_betaiotazeta sigma uc
+ nf_betaiotazeta env sigma uc
in
match occs with
| NoOccurrences -> c
@@ -1284,7 +1282,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else raise Not_found
with Not_found ->
try
- let t' = nf_betaiota sigma (one_step_reduce env sigma t) in
+ let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in
elimrec env t' l
with NotStepReducible -> error_cannot_recognize ref
in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index f153b63410..3f947fd23f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -219,7 +219,8 @@ let discharge_class (_,cl) =
in grs', discharge_rel_context subst 1 ctx @ ctx' in
let cl_impl' = Lib.discharge_global cl.cl_impl in
if cl_impl' == cl.cl_impl then cl else
- let ctx, _, _ as info = abs_context cl in
+ let info = abs_context cl in
+ let ctx = info.Lib.abstr_ctx in
let ctx, subst = rel_of_variable_context ctx in
let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
let context = discharge_context ctx (subst, usubst) cl.cl_context in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 43066c8099..3132d2ad53 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -23,11 +23,6 @@ open Arguments_renaming
open Pretype_errors
open Context.Rel.Declaration
-let push_rec_types pfix env =
- let (i, c, t) = pfix in
- let inj c = EConstr.Unsafe.to_constr c in
- push_rec_types (i, Array.map inj c, Array.map inj t) env
-
let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 9f084ae8df..153a48a710 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
val judge_of_product : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
+val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b41fb4e4dd..e1720ec955 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-module CVars = Vars
-
open CErrors
open Pp
open Util
@@ -196,7 +194,7 @@ let pose_all_metas_as_evars env evd t =
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
let ty =
if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
- then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
+ then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
let src = Evd.evar_source_of_meta mv !evdref in
let ev = Evarutil.e_new_evar env evdref ~src ty in
@@ -1279,7 +1277,7 @@ let w_coerce env evd mv c =
let unify_to_type env sigma flags c status u =
let sigma, c = refresh_universes (Some false) env sigma c in
let t = get_type_of env sigma (nf_meta sigma c) in
- let t = nf_betaiota sigma (nf_meta sigma t) in
+ let t = nf_betaiota env sigma (nf_meta sigma t) in
unify_0 env sigma CUMUL flags t u
let unify_type env sigma flags mv status c =
@@ -1527,7 +1525,7 @@ let indirectly_dependent sigma c d decls =
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in
let sigma, subst = nf_univ_variables sigma in
- (sigma, EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
+ (sigma, EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr (nf_evar sigma c))))
let default_matching_core_flags sigma =
let ts = Names.full_transparent_state in {
@@ -1617,7 +1615,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
| Some (sigma,_,l) ->
let c = applist (nf_evar sigma (local_strong whd_meta sigma c), l) in
let univs, subst = nf_univ_variables sigma in
- Some (sigma,EConstr.of_constr (CVars.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
+ Some (sigma,EConstr.of_constr (Universes.subst_univs_constr subst (EConstr.Unsafe.to_constr c))))
let make_eq_test env evd c =
let out cstr =
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index e395bdbc63..c93b41786b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -15,6 +15,7 @@ open Vars
open Environ
open Inductive
open Reduction
+open Vmvalues
open Vm
open Context.Rel.Declaration
@@ -134,7 +135,7 @@ let build_case_type dep p realargs c =
(* La fonction de normalisation *)
-let rec nf_val env sigma v t = nf_whd env sigma (whd_val v) t
+let rec nf_val env sigma v t = nf_whd env sigma (Vmvalues.whd_val v) t
and nf_vtype env sigma v = nf_val env sigma v crazy_type
@@ -144,7 +145,7 @@ and nf_whd env sigma whd typ =
| Vprod p ->
let dom = nf_vtype env sigma (dom p) in
let name = Name (Id.of_string "x") in
- let vc = body_of_vfun (nb_rel env) (codom p) in
+ let vc = reduce_fun (nb_rel env) (codom p) in
let codom = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vc in
mkProd(name,dom,codom)
| Vfun f -> nf_fun env sigma f typ
@@ -191,7 +192,7 @@ and nf_univ_args ~nb_univs mk env sigma stk =
else match stk with
| Zapp args :: _ ->
let inst =
- Array.init nb_univs (fun i -> Vm.uni_lvl_val (arg args i))
+ Array.init nb_univs (fun i -> uni_lvl_val (arg args i))
in
Univ.Instance.of_array inst
| _ -> assert false
@@ -239,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nparams = mib.mind_nparams in
let params,realargs = Util.Array.chop nparams allargs in
+ let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
- hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
+ hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
let pT = whd_all env pT in
let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
@@ -254,7 +256,7 @@ and nf_stk ?from:(from=0) env sigma c t stk =
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type dep p realargs c in
- let ci = case_info sw in
+ let ci = sw.sw_annot.Cbytecodes.ci in
nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk
| Zproj p :: stk ->
assert (from = 0) ;
@@ -266,14 +268,14 @@ and nf_predicate env sigma ind mip params v pT =
match whd_val v, kind pT with
| Vfun f, Prod _ ->
let k = nb_rel env in
- let vb = body_of_vfun k f in
+ let vb = reduce_fun k f in
let name,dom,codom = decompose_prod env pT in
let dep,body =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
dep, mkLambda(name,dom,body)
| Vfun f, _ ->
let k = nb_rel env in
- let vb = body_of_vfun k f in
+ let vb = reduce_fun k f in
let name = Name (Id.of_string "c") in
let n = mip.mind_nrealargs in
let rargs = Array.init n (fun i -> mkRel (n-i)) in
@@ -307,7 +309,7 @@ and nf_bargs env sigma b ofs t =
and nf_fun env sigma f typ =
let k = nb_rel env in
- let vb = body_of_vfun k f in
+ let vb = reduce_fun k f in
let name,dom,codom =
try decompose_prod env typ
with DestKO ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 19:35:39 +0000