aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh6
-rwxr-xr-xdev/tools/make-changelog.sh2
-rw-r--r--doc/sphinx/proof-engine/tactics.rst2
-rw-r--r--pretyping/nativenorm.ml11
-rw-r--r--pretyping/recordops.ml29
-rw-r--r--pretyping/recordops.mli11
-rw-r--r--pretyping/reductionops.ml14
-rw-r--r--pretyping/reductionops.mli26
-rw-r--r--pretyping/tacred.ml282
-rw-r--r--pretyping/vnorm.ml11
-rw-r--r--test-suite/bugs/closed/bug_12649.v11
-rw-r--r--test-suite/success/bug_10890.v8
-rw-r--r--test-suite/success/sprop_uip.v26
-rw-r--r--toplevel/coqtop.ml2
-rw-r--r--vernac/record.ml21
-rw-r--r--vernac/record.mli5
16 files changed, 254 insertions, 213 deletions
diff --git a/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh b/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh
new file mode 100644
index 0000000000..d4c67b03b5
--- /dev/null
+++ b/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12650" ] || [ "$CI_BRANCH" = "rebuild-record" ]; then
+
+ elpi_CI_REF=rebuild-record
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index de58527cca..413433ef41 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -28,7 +28,7 @@ esac
printf "Fixes? (space separated list of bug numbers)\n"
read -r fixes_list
-fixes_string="$(echo $fixes_list | sed 's/ /~ and /g; s,\([0-9]\+\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
+fixes_string="$(echo $fixes_list | sed 's/ /~ and /g; s,\([0-9][0-9]*\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
if [ ! -z "$fixes_string" ]; then fixes_string="$(printf '\n fixes %s,' "$fixes_string")"; fi
# shellcheck disable=SC2016
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4af3ebc47b..25c4de7389 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4162,7 +4162,7 @@ Hint locality
Hints provided by the ``Hint`` commands are erased when closing a section.
Conversely, all hints of a module ``A`` that are not defined inside a
section (and not defined with option ``Local``) become available when the
-module ``A`` is imported (using e.g. ``Require Import A.``).
+module ``A`` is required (using e.g. ``Require A.``).
As of today, hints only have a binary behavior regarding locality, as
described above: either they disappear at the end of a section scope,
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 30e1dc0611..3f68e3c78f 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -318,13 +318,12 @@ and nf_atom_type env sigma atom =
| Avar id ->
mkVar id, Typeops.type_of_variable env id
| Acase(ans,accu,p,bs) ->
- let () = if Typeops.should_invert_case env ans.asw_ci then
- (* TODO implement case inversion readback (properly reducing
- it is a problem for the kernel) *)
- CErrors.user_err Pp.(str "Native compute readback of case inversion not implemented.")
- in
let a,ta = nf_accu_type env sigma accu in
let ((mind,_),u as ind),allargs = find_rectype_a env ta in
+ let iv = if Typeops.should_invert_case env ans.asw_ci then
+ CaseInvert {univs=u; args=allargs}
+ else NoInvert
+ in
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
let params,realargs = Array.chop nparams allargs in
@@ -344,7 +343,7 @@ and nf_atom_type env sigma atom =
in
let branchs = Array.mapi mkbranch bsw in
let tcase = build_case_type p realargs a in
- mkCase(ans.asw_ci, p, NoInvert, a, branchs), tcase
+ mkCase(ans.asw_ci, p, iv, a, branchs), tcase
| Afix(tt,ft,rp,s) ->
let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
let tt = Array.map fst tt and rt = Array.map snd tt in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c26da8ccc7..e6e5ad8dd4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -54,34 +54,29 @@ let structure_table =
let projection_table =
Summary.ref (Cmap.empty : struc_typ Cmap.t) ~name:"record-projs"
-(* TODO: could be unify struc_typ and struc_tuple ? *)
-
-type struc_tuple =
- constructor * proj_kind list * Constant.t option list
-
-let register_structure env (id,kl,projs) =
- let open Declarations in
- let ind = fst id in
- let mib, mip = Inductive.lookup_mind_specif env ind in
- let n = mib.mind_nparams in
- let struc =
- { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
+let register_structure ({ s_CONST = (ind,_); s_PROJ = projs; } as struc) =
structure_table := Indmap.add ind struc !structure_table;
projection_table :=
List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
projs !projection_table
-let subst_structure subst (id, kl, projs as obj) =
+let subst_structure subst struc =
let projs' =
(* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
List.Smart.map
(Option.Smart.map (subst_constant subst))
- projs
+ struc.s_PROJ
in
- let id' = Globnames.subst_constructor subst id in
- if projs' == projs && id' == id then obj else
- (id',kl,projs')
+ let id' = Globnames.subst_constructor subst struc.s_CONST in
+ if projs' == struc.s_PROJ && id' == struc.s_CONST
+ then struc
+ else { struc with s_CONST = id'; s_PROJ = projs' }
+
+let rebuild_structure env struc =
+ let mib = Environ.lookup_mind (fst (fst struc.s_CONST)) env in
+ let npars = mib.Declarations.mind_nparams in
+ { struc with s_EXPECTEDPARAM = npars }
let lookup_structure indsp = Indmap.find indsp !structure_table
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 955a4e7aae..3be60d5e62 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -27,13 +27,12 @@ type struc_typ = {
s_CONST : constructor;
s_EXPECTEDPARAM : int;
s_PROJKIND : proj_kind list;
- s_PROJ : Constant.t option list }
-
-type struc_tuple =
- constructor * proj_kind list * Constant.t option list
+ s_PROJ : Constant.t option list;
+}
-val register_structure : Environ.env -> struc_tuple -> unit
-val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
+val register_structure : struc_typ -> unit
+val subst_structure : Mod_subst.substitution -> struc_typ -> struc_typ
+val rebuild_structure : Environ.env -> struc_typ -> struc_typ
(** [lookup_structure isp] returns the struc_typ associated to the
inductive path [isp] if it corresponds to a structure, otherwise
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6f02d76f3a..594b8ab54c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -436,15 +436,11 @@ type state = constr * constr Stack.t
type reduction_function = env -> evar_map -> constr -> constr
type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
-type contextual_stack_reduction_function =
+type stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
-type stack_reduction_function = contextual_stack_reduction_function
-type local_stack_reduction_function =
- evar_map -> constr -> constr * constr list
type state_reduction_function =
env -> evar_map -> state -> state
-type local_state_reduction_function = evar_map -> state -> state
let pr_state env sigma (tm,sk) =
let open Pp in
@@ -572,14 +568,6 @@ let reduce_and_refold_fix recfun env sigma fix sk =
(fun _ (t,sk') -> recfun (t,sk'))
[] sigma raw_answer sk
-let fix_recarg ((recindices,bodynum),_) stack =
- assert (0 <= bodynum && bodynum < Array.length recindices);
- let recargnum = Array.get recindices bodynum in
- try
- Some (recargnum, Stack.nth stack recargnum)
- with Not_found ->
- None
-
open Primred
module CNativeEntries =
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b316b3c213..218936edfb 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -112,15 +112,11 @@ type reduction_function = env -> evar_map -> constr -> constr
type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
-type contextual_stack_reduction_function =
+type stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
-type stack_reduction_function = contextual_stack_reduction_function
-type local_stack_reduction_function =
- evar_map -> constr -> constr * constr list
type state_reduction_function =
env -> evar_map -> state -> state
-type local_state_reduction_function = evar_map -> state -> state
val pr_state : env -> evar_map -> state -> Pp.t
@@ -130,11 +126,6 @@ val strong_with_flags :
(CClosure.RedFlags.reds -> reduction_function) ->
(CClosure.RedFlags.reds -> reduction_function)
val strong : reduction_function -> reduction_function
-(*i
-val stack_reduction_of_reduction :
- 'a reduction_function -> 'a state_reduction_function
-i*)
-val stacklam : (state -> 'a) -> constr list -> evar_map -> constr -> constr Stack.t -> 'a
val whd_state_gen :
CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state
@@ -167,13 +158,13 @@ val whd_allnolet : reduction_function
val whd_betalet : reduction_function
(** Removes cast and put into applicative form *)
-val whd_nored_stack : contextual_stack_reduction_function
-val whd_beta_stack : contextual_stack_reduction_function
-val whd_betaiota_stack : contextual_stack_reduction_function
-val whd_betaiotazeta_stack : contextual_stack_reduction_function
-val whd_all_stack : contextual_stack_reduction_function
-val whd_allnolet_stack : contextual_stack_reduction_function
-val whd_betalet_stack : contextual_stack_reduction_function
+val whd_nored_stack : stack_reduction_function
+val whd_beta_stack : stack_reduction_function
+val whd_betaiota_stack : stack_reduction_function
+val whd_betaiotazeta_stack : stack_reduction_function
+val whd_all_stack : stack_reduction_function
+val whd_allnolet_stack : stack_reduction_function
+val whd_betalet_stack : stack_reduction_function
val whd_nored_state : state_reduction_function
val whd_beta_state : state_reduction_function
@@ -242,7 +233,6 @@ val is_arity : env -> evar_map -> constr -> bool
val is_sort : env -> evar_map -> types -> bool
val contract_fix : evar_map -> fixpoint -> constr
-val fix_recarg : ('a, 'a) pfixpoint -> 'b Stack.t -> (int * 'b) option
(** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
val is_transparent : Environ.env -> Constant.t tableKey -> bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index baa32565f6..e4b5dc1edf 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -358,30 +358,6 @@ let reference_eval env sigma = function
let x = Name default_dependent_ident
-let make_elim_fun (names,(nbfix,lv,n)) u largs =
- let lu = List.firstn n largs in
- let p = List.length lv in
- let lyi = List.map fst lv in
- let la =
- List.map_i (fun q aq ->
- (* k from the comment is q+1 *)
- try mkRel (p+1-(List.index Int.equal (n-q) lyi))
- with Not_found -> aq)
- 0 (List.map (Vars.lift p) lu)
- in
- fun i ->
- match names.(i) with
- | None -> None
- | Some (minargs,ref) ->
- let body = applist (mkEvalRef ref u, la) in
- let g =
- List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
- let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in
- let tij' = Vars.substl (List.rev subst) tij in
- let x = make_annot x Sorts.Relevant in (* TODO relevance *)
- mkLambda (x,tij',c)) 1 body (List.rev lv)
- in Some (minargs,g)
-
(* [f] is convertible to [Fix(recindices,bodynum),bodyvect)]:
do so that the reduction uses this extra information *)
@@ -467,16 +443,6 @@ let substl_checking_arity env subst sigma c =
type fix_reduction_result = NotReducible | Reduced of (constr * constr list)
-let reduce_fix whdfun sigma fix stack =
- match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
- | None -> NotReducible
- | Some (recargnum,recarg) ->
- let (recarg'hd,_ as recarg') = whdfun sigma recarg in
- let stack' = List.assign stack recargnum (applist recarg') in
- (match EConstr.kind sigma recarg'hd with
- | Construct _ -> Reduced (contract_fix sigma fix, stack')
- | _ -> NotReducible)
-
let contract_fix_use_function env sigma f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
let nbodies = Array.length recindices in
@@ -484,22 +450,6 @@ let contract_fix_use_function env sigma f
let lbodies = List.init nbodies make_Fi in
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
- | None -> NotReducible
- | Some (recargnum,recarg) ->
- let (recarg'hd,_ as recarg') =
- if EConstr.isRel sigma recarg then
- (* The recarg cannot be a local def, no worry about the right env *)
- (recarg, [])
- else
- whfun recarg in
- let stack' = List.assign stack recargnum (applist recarg') in
- (match EConstr.kind sigma recarg'hd with
- | Construct _ ->
- Reduced (contract_fix_use_function env sigma f fix,stack')
- | _ -> NotReducible)
-
let contract_cofix_use_function env sigma f
(bodynum,(_names,_,bodies as typedbodies)) =
let nbodies = Array.length bodies in
@@ -574,34 +524,23 @@ let match_eval_ref_value env sigma constr stack =
env |> lookup_rel n |> RelDecl.get_value |> Option.map (lift n)
| _ -> None
-let special_red_case env sigma whfun (ci, p, iv, c, lf) =
- let rec redrec s =
- let (constr, cargs) = whfun s in
- match match_eval_ref env sigma constr cargs with
- | Some (ref, u) ->
- (match reference_opt_value env sigma ref u with
- | None -> raise Redelimination
- | Some gvalue ->
- if reducible_mind_case sigma gvalue then
- reduce_mind_case_use_function constr env sigma
- {mP=p; mconstr=gvalue; mcargs=cargs;
- mci=ci; mlf=lf}
- else
- redrec (applist(gvalue, cargs)))
- | None ->
- if reducible_mind_case sigma constr then
- reduce_mind_case sigma
- {mP=p; mconstr=constr; mcargs=cargs;
- mci=ci; mlf=lf}
- else
- raise Redelimination
- in
- redrec c
+let push_app sigma (hd, stk as p) = match EConstr.kind sigma hd with
+| App (hd, args) ->
+ (hd, Array.fold_right (fun x accu -> x :: accu) args stk)
+| _ -> p
let recargs = function
| EvalVar _ | EvalRel _ | EvalEvar _ -> None
| EvalConst c -> ReductionBehaviour.get (GlobRef.ConstRef c)
+let fix_recarg ((recindices,bodynum),_) stack =
+ assert (0 <= bodynum && bodynum < Array.length recindices);
+ let recargnum = Array.get recindices bodynum in
+ try
+ Some (recargnum, List.nth stack recargnum)
+ with Failure _ ->
+ None
+
let reduce_projection env sigma p ~npars (recarg'hd,stack') stack =
(match EConstr.kind sigma recarg'hd with
| Construct _ ->
@@ -609,24 +548,9 @@ let reduce_projection env sigma p ~npars (recarg'hd,stack') stack =
Reduced (List.nth stack' proj_narg, stack)
| _ -> NotReducible)
-let reduce_proj env sigma whfun whfun' c =
- let rec redrec s =
- match EConstr.kind sigma s with
- | Proj (proj, c) ->
- let c' = try redrec c with Redelimination -> c in
- let constr, cargs = whfun c' in
- (match EConstr.kind sigma constr with
- | Construct _ ->
- let proj_narg = Projection.npars proj + Projection.arg proj in
- List.nth cargs proj_narg
- | _ -> raise Redelimination)
- | Case (n,p,iv,c,brs) ->
- let c' = redrec c in
- let p = (n,p,iv,c',brs) in
- (try special_red_case env sigma whfun' p
- with Redelimination -> mkCase p)
- | _ -> raise Redelimination
- in redrec c
+let rec beta_applist sigma accu c stk = match EConstr.kind sigma c, stk with
+| Lambda (_, _, c), arg :: stk -> beta_applist sigma (arg :: accu) c stk
+| _ -> substl accu c, stk
let whd_nothing_for_iota env sigma s =
let rec whrec (x, stack as s) =
@@ -650,17 +574,17 @@ let whd_nothing_for_iota env sigma s =
(match constant_opt_value_in env (const, u) with
| Some body -> whrec (EConstr.of_constr body, stack)
| None -> s)
- | LetIn (_,b,_,c) -> stacklam whrec [b] sigma c stack
+ | LetIn (_,b,_,c) -> whrec (beta_applist sigma [b] c stack)
| Cast (c,_,_) -> whrec (c, stack)
- | App (f,cl) -> whrec (f, Stack.append_app cl stack)
+ | App (f,cl) -> whrec (f, Array.fold_right (fun c accu -> c :: accu) cl stack)
| Lambda (na,t,c) ->
- (match Stack.decomp stack with
- | Some (a,m) -> stacklam whrec [a] sigma c m
+ (match stack with
+ | a :: stack -> whrec (beta_applist sigma [a] c stack)
| _ -> s)
| x -> s
in
- EConstr.decompose_app sigma (Stack.zip sigma (whrec (s,Stack.empty)))
+ whrec s
(* [red_elim_const] contracts iota/fix/cofix redexes hidden behind
constants by keeping the name of the constants in the recursive calls;
@@ -703,21 +627,17 @@ let rec red_elim_const env sigma ref u largs =
try match reference_eval env sigma ref with
| EliminationCases n when nargs >= n ->
let c = reference_value env sigma ref u in
- let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
- let whfun = whd_simpl_stack env sigma in
- (special_red_case env sigma whfun (EConstr.destCase sigma c'), lrest), nocase
+ let c', lrest = whd_nothing_for_iota env sigma (c, largs) in
+ (special_red_case env sigma (EConstr.destCase sigma c'), lrest), nocase
| EliminationProj n when nargs >= n ->
let c = reference_value env sigma ref u in
- let c', lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
- let whfun = whd_construct_stack env sigma in
- let whfun' = whd_simpl_stack env sigma in
- (reduce_proj env sigma whfun whfun' c', lrest), nocase
+ let c', lrest = whd_nothing_for_iota env sigma (c, largs) in
+ (reduce_proj env sigma c', lrest), nocase
| EliminationFix (min,minfxargs,infos) when nargs >= min ->
let c = reference_value env sigma ref u in
- let d, lrest = whd_nothing_for_iota env sigma (applist(c,largs)) in
- let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) u largs in
- let whfun = whd_construct_stack env sigma in
- (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
+ let d, lrest = whd_nothing_for_iota env sigma (c, largs) in
+ let f = ([|Some (minfxargs,ref)|],infos), u, largs in
+ (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
| EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
@@ -729,10 +649,9 @@ let rec red_elim_const env sigma ref u largs =
let c', lrest = whd_betalet_stack env sigma (applist(c,args)) in
descend (destEvalRefU sigma c') lrest in
let (_, midargs as s) = descend (ref,u) largs in
- let d, lrest = whd_nothing_for_iota env sigma (applist s) in
- let f = make_elim_fun refinfos u midargs in
- let whfun = whd_construct_stack env sigma in
- (match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
+ let d, lrest = whd_nothing_for_iota env sigma s in
+ let f = refinfos, u, midargs in
+ (match reduce_fix_use_function env sigma f (destFix sigma d) lrest with
| NotReducible -> raise Redelimination
| Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
| NotAnElimination when unfold_nonelim ->
@@ -755,32 +674,30 @@ and reduce_params env sigma stack l =
| _ -> raise Redelimination)
stack l
-
(* reduce to whd normal form or to an applied constant that does not hide
a reducible iota/fix/cofix redex (the "simpl" tactic) *)
and whd_simpl_stack env sigma =
let open ReductionBehaviour in
let rec redrec s =
- let (x, stack) = decompose_app_vect sigma s in
- let stack = Array.to_list stack in
- let s' = (x, stack) in
+ let s' = push_app sigma s in
+ let (x, stack) = s' in
match EConstr.kind sigma x with
| Lambda (na,t,c) ->
(match stack with
| [] -> s'
- | a :: rest -> redrec (beta_applist sigma (x, stack)))
- | LetIn (n,b,t,c) -> redrec (applist (Vars.substl [b] c, stack))
- | App (f,cl) -> redrec (applist(f, (Array.to_list cl)@stack))
- | Cast (c,_,_) -> redrec (applist(c, stack))
+ | a :: rest -> redrec (beta_applist sigma [a] c rest))
+ | LetIn (n,b,t,c) -> redrec (Vars.substl [b] c, stack)
+ | App (f,cl) -> assert false (* see push_app above *)
+ | Cast (c,_,_) -> redrec (c, stack)
| Case (ci,p,iv,c,lf) ->
(try
- redrec (applist(special_red_case env sigma redrec (ci,p,iv,c,lf), stack))
+ redrec (special_red_case env sigma (ci,p,iv,c,lf), stack)
with
Redelimination -> s')
| Fix fix ->
- (try match reduce_fix (whd_construct_stack env) sigma fix stack with
- | Reduced s' -> redrec (applist s')
+ (try match reduce_fix env sigma fix stack with
+ | Reduced s' -> redrec s'
| NotReducible -> s'
with Redelimination -> s')
@@ -800,11 +717,11 @@ and whd_simpl_stack env sigma =
(match reduce_projection env sigma p ~npars
(whd_construct_stack env sigma c) stack
with
- | Reduced s' -> redrec (applist s')
+ | Reduced s' -> redrec s'
| NotReducible -> s')
| _ ->
match reduce_projection env sigma p ~npars (whd_construct_stack env sigma c) stack with
- | Reduced s' -> redrec (applist s')
+ | Reduced s' -> redrec s'
| NotReducible -> s')
else s'
with Redelimination -> s')
@@ -814,7 +731,7 @@ and whd_simpl_stack env sigma =
| Some (ref, u) ->
(try
let sapp, nocase = red_elim_const env sigma ref u stack in
- let hd, _ as s'' = redrec (applist(sapp)) in
+ let hd, _ as s'' = redrec sapp in
let rec is_case x = match EConstr.kind sigma x with
| Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x
| App (hd, _) -> is_case hd
@@ -827,10 +744,102 @@ and whd_simpl_stack env sigma =
in
redrec
+and reduce_fix env sigma fix stack =
+ match fix_recarg fix stack with
+ | None -> NotReducible
+ | Some (recargnum,recarg) ->
+ let (recarg'hd,_ as recarg') = whd_construct_stack env sigma recarg in
+ let stack' = List.assign stack recargnum (applist recarg') in
+ (match EConstr.kind sigma recarg'hd with
+ | Construct _ -> Reduced (contract_fix sigma fix, stack')
+ | _ -> NotReducible)
+
+and reduce_fix_use_function env sigma f fix stack =
+ match fix_recarg fix stack with
+ | None -> NotReducible
+ | Some (recargnum,recarg) ->
+ let (recarg'hd,_ as recarg') =
+ if EConstr.isRel sigma recarg then
+ (* The recarg cannot be a local def, no worry about the right env *)
+ (recarg, [])
+ else
+ whd_construct_stack env sigma recarg in
+ let stack' = List.assign stack recargnum (applist recarg') in
+ (match EConstr.kind sigma recarg'hd with
+ | Construct _ ->
+ let (names, (nbfix, lv, n)), u, largs = f in
+ let lu = List.firstn n largs in
+ let p = List.length lv in
+ let lyi = List.map fst lv in
+ let la =
+ List.map_i (fun q aq ->
+ (* k from the comment is q+1 *)
+ try mkRel (p+1-(List.index Int.equal (n-q) lyi))
+ with Not_found -> Vars.lift p aq)
+ 0 lu
+ in
+ let f i = match names.(i) with
+ | None -> None
+ | Some (minargs,ref) ->
+ let body = applist (mkEvalRef ref u, la) in
+ let g =
+ List.fold_left_i (fun q (* j = n+1-q *) c (ij,tij) ->
+ let subst = List.map (Vars.lift (-q)) (List.firstn (n-ij) la) in
+ let tij' = Vars.substl (List.rev subst) tij in
+ let x = make_annot x Sorts.Relevant in (* TODO relevance *)
+ mkLambda (x,tij',c)) 1 body (List.rev lv)
+ in Some (minargs,g)
+ in
+ Reduced (contract_fix_use_function env sigma f fix,stack')
+ | _ -> NotReducible)
+
+and reduce_proj env sigma c =
+ let rec redrec s =
+ match EConstr.kind sigma s with
+ | Proj (proj, c) ->
+ let c' = try redrec c with Redelimination -> c in
+ let constr, cargs = whd_construct_stack env sigma c' in
+ (match EConstr.kind sigma constr with
+ | Construct _ ->
+ let proj_narg = Projection.npars proj + Projection.arg proj in
+ List.nth cargs proj_narg
+ | _ -> raise Redelimination)
+ | Case (n,p,iv,c,brs) ->
+ let c' = redrec c in
+ let p = (n,p,iv,c',brs) in
+ (try special_red_case env sigma p
+ with Redelimination -> mkCase p)
+ | _ -> raise Redelimination
+ in redrec c
+
+and special_red_case env sigma (ci, p, iv, c, lf) =
+ let rec redrec s =
+ let (constr, cargs) = whd_simpl_stack env sigma s in
+ match match_eval_ref env sigma constr cargs with
+ | Some (ref, u) ->
+ (match reference_opt_value env sigma ref u with
+ | None -> raise Redelimination
+ | Some gvalue ->
+ if reducible_mind_case sigma gvalue then
+ reduce_mind_case_use_function constr env sigma
+ {mP=p; mconstr=gvalue; mcargs=cargs;
+ mci=ci; mlf=lf}
+ else
+ redrec (gvalue, cargs))
+ | None ->
+ if reducible_mind_case sigma constr then
+ reduce_mind_case sigma
+ {mP=p; mconstr=constr; mcargs=cargs;
+ mci=ci; mlf=lf}
+ else
+ raise Redelimination
+ in
+ redrec (push_app sigma (c, []))
+
(* reduce until finding an applied constructor or fail *)
and whd_construct_stack env sigma s =
- let (constr, cargs as s') = whd_simpl_stack env sigma s in
+ let (constr, cargs as s') = whd_simpl_stack env sigma (s, []) in
if reducible_mind_case sigma constr then s'
else match match_eval_ref env sigma constr cargs with
| Some (ref, u) ->
@@ -855,13 +864,13 @@ let try_red_product env sigma c =
| App (f,l) ->
(match EConstr.kind sigma f with
| Fix fix ->
- let stack = Stack.append_app l Stack.empty in
- (match fix_recarg fix stack with
+ (match fix_recarg fix (Array.to_list l) with
| None -> raise Redelimination
| Some (recargnum,recarg) ->
let recarg' = redrec env recarg in
- let stack' = Stack.assign stack recargnum recarg' in
- simpfun (Stack.zip sigma (f,stack')))
+ let l = Array.copy l in
+ let () = Array.set l recargnum recarg' in
+ simpfun (mkApp (f, l)))
| _ -> simpfun (mkApp (redrec env f, l)))
| Cast (c,_,_) -> redrec env c
| Prod (x,a,b) ->
@@ -973,19 +982,19 @@ let whd_simpl_orelse_delta_but_fix env sigma c =
if List.length stack <= npars then
(* Do not show the eta-expanded form *)
s'
- else redrec (applist (c, stack))
- | _ -> redrec (applist(c, stack)))
+ else redrec (c, stack)
+ | _ -> redrec (c, stack))
| None -> s'
in
let simpfun = clos_norm_flags betaiota env sigma in
simpfun (applist (redrec c))
-let hnf_constr = whd_simpl_orelse_delta_but_fix
+let hnf_constr env sigma c = whd_simpl_orelse_delta_but_fix env sigma (c, [])
(* The "simpl" reduction tactic *)
let whd_simpl env sigma c =
- applist (whd_simpl_stack env sigma c)
+ applist (whd_simpl_stack env sigma (c, []))
let simpl env sigma c = strong whd_simpl env sigma c
@@ -1267,11 +1276,10 @@ let one_step_reduce env sigma c =
| Cast (c,_,_) -> redrec (c,stack)
| Case (ci,p,iv,c,lf) ->
(try
- (special_red_case env sigma (whd_simpl_stack env sigma)
- (ci,p,iv,c,lf), stack)
+ (special_red_case env sigma (ci,p,iv,c,lf), stack)
with Redelimination -> raise NotStepReducible)
| Fix fix ->
- (try match reduce_fix (whd_construct_stack env) sigma fix stack with
+ (try match reduce_fix env sigma fix stack with
| Reduced s' -> s'
| NotReducible -> raise NotStepReducible
with Redelimination -> raise NotStepReducible)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b3f577b684..854a5ff63d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -263,12 +263,11 @@ and nf_stk ?from:(from=0) env sigma c t stk =
| Zswitch sw :: stk ->
assert (from = 0) ;
let ci = sw.sw_annot.Vmvalues.ci in
- let () = if Typeops.should_invert_case env ci then
- (* TODO implement case inversion readback (properly reducing
- it is a problem for the kernel) *)
- CErrors.user_err Pp.(str "VM compute readback of case inversion not implemented.")
- in
let ((mind,_ as ind), u), allargs = find_rectype_a env t in
+ let iv = if Typeops.should_invert_case env ci then
+ CaseInvert {univs=u; args=allargs}
+ else NoInvert
+ in
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
@@ -287,7 +286,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 p realargs c in
- nf_stk env sigma (mkCase(ci, p, NoInvert, c, branchs)) tcase stk
+ nf_stk env sigma (mkCase(ci, p, iv, c, branchs)) tcase stk
| Zproj p :: stk ->
assert (from = 0) ;
let p' = Projection.make p true in
diff --git a/test-suite/bugs/closed/bug_12649.v b/test-suite/bugs/closed/bug_12649.v
new file mode 100644
index 0000000000..5547de84ff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12649.v
@@ -0,0 +1,11 @@
+
+
+Module Type A.
+
+ Record baz : Prop := B { }. (* any sort would do *)
+
+End A.
+
+Print A.
+Module Type UseA (c: A). End UseA.
+Print UseA. (* ANOMALY! Int.Map.get's assert false *)
diff --git a/test-suite/success/bug_10890.v b/test-suite/success/bug_10890.v
new file mode 100644
index 0000000000..37b6c816cc
--- /dev/null
+++ b/test-suite/success/bug_10890.v
@@ -0,0 +1,8 @@
+Require Import Derive.
+
+Derive foo SuchThat (foo = foo :> nat) As bar.
+Proof.
+ Unshelve.
+ 2:abstract exact 0.
+ exact eq_refl.
+Defined. (* or Qed: anomaly kernel doesn't support existential variables *)
diff --git a/test-suite/success/sprop_uip.v b/test-suite/success/sprop_uip.v
index 508cc2be7d..eae1b75689 100644
--- a/test-suite/success/sprop_uip.v
+++ b/test-suite/success/sprop_uip.v
@@ -95,6 +95,32 @@ Section funext.
:= eq_refl.
End funext.
+(* test reductions on inverted cases *)
+
+(* first check production of correct blocked cases *)
+Definition lazy_seq_rect := Eval lazy in seq_rect.
+Definition vseq_rect := Eval vm_compute in seq_rect.
+Definition native_seq_rect := Eval native_compute in seq_rect.
+Definition cbv_seq_rect := Eval cbv in seq_rect.
+
+(* check it reduces according to indices *)
+Ltac reset := match goal with H : _ |- _ => change (match H with srefl _ => False end) end.
+Ltac check := match goal with |- False => idtac end.
+Lemma foo (H:seq 0 0) : False.
+Proof.
+ reset.
+ Fail check. (* check that "reset" and "check" actually do something *)
+
+ lazy; check; reset.
+
+ (* TODO *)
+ vm_compute. Fail check.
+ native_compute. Fail check.
+ cbv. Fail check.
+ cbn. Fail check.
+ simpl. Fail check.
+Abort.
+
(* check that extraction doesn't fall apart on matches with special reduction *)
Require Extraction.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 4231915be1..bbcfcc4826 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -161,7 +161,7 @@ let init_gc () =
* In this case, we put in place our preferred configuration.
*)
Gc.set { (Gc.get ()) with
- Gc.minor_heap_size = 33554432; (* 4M *)
+ Gc.minor_heap_size = 32*1024*1024; (* 32Mwords x 8 bytes/word = 256Mb *)
Gc.space_overhead = 120}
let init_process () =
diff --git a/vernac/record.ml b/vernac/record.ml
index 820bcba0b6..d0036e40f9 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -388,23 +388,26 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
open Typeclasses
let load_structure i (_, structure) =
- Recordops.register_structure (Global.env()) structure
+ Recordops.register_structure structure
let cache_structure o =
load_structure 1 o
-let subst_structure (subst, (id, kl, projs as obj)) =
+let subst_structure (subst, obj) =
Recordops.subst_structure subst obj
let discharge_structure (_, x) = Some x
-let inStruc : Recordops.struc_tuple -> obj =
+let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s
+
+let inStruc : Recordops.struc_typ -> obj =
declare_object {(default_object "STRUCTURE") with
cache_function = cache_structure;
load_function = load_structure;
subst_function = subst_structure;
classify_function = (fun x -> Substitute x);
- discharge_function = discharge_structure }
+ discharge_function = discharge_structure;
+ rebuild_function = rebuild_structure; }
let declare_structure_entry o =
Lib.add_anonymous_leaf (inStruc o)
@@ -497,7 +500,15 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
let build = GlobRef.ConstructRef cstr in
let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
- let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
+ let npars = Inductiveops.inductive_nparams (Global.env()) rsp in
+ let struc = {
+ Recordops.s_CONST = cstr;
+ s_PROJ = List.rev sp_projs;
+ s_PROJKIND = List.rev kinds;
+ s_EXPECTEDPARAM = npars;
+ }
+ in
+ let () = declare_structure_entry struc in
rsp
in
List.mapi map record_data
diff --git a/vernac/record.mli b/vernac/record.mli
index e890f80150..38a622977a 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -29,8 +29,6 @@ val declare_projections :
Constr.rel_context ->
Recordops.proj_kind list * Constant.t option list
-val declare_structure_entry : Recordops.struc_tuple -> unit
-
val definition_structure
: universe_decl_expr option
-> inductive_kind
@@ -46,3 +44,6 @@ val definition_structure
-> GlobRef.t list
val declare_existing_class : GlobRef.t -> unit
+
+(** Used by elpi *)
+val declare_structure_entry : Recordops.struc_typ -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 19:23:34 +0000