aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/cbn.ml60
-rw-r--r--tactics/eqschemes.ml40
-rw-r--r--tactics/hints.ml4
-rw-r--r--tactics/tactics.ml2
-rw-r--r--tactics/term_dnet.ml5
5 files changed, 68 insertions, 43 deletions
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 31873ea6b0..56bf2b056d 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -104,9 +104,11 @@ sig
| Cst_const of pconstant
| Cst_proj of Projection.t
+ type 'a case_stk =
+ case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
+ | Case of 'a case_stk * Cst_stack.t
| Proj of Projection.t * Cst_stack.t
| Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -121,7 +123,7 @@ sig
val append_app : 'a array -> 'a t -> 'a t
val decomp : 'a t -> ('a * 'a t) option
val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool)
- -> 'a t -> 'a t -> bool
+ -> ('a case_stk -> 'a case_stk -> bool) -> 'a t -> 'a t -> bool
val strip_app : 'a t -> 'a t * 'a t
val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
val will_expose_iota : 'a t -> bool
@@ -156,9 +158,11 @@ struct
| Cst_const of pconstant
| Cst_proj of Projection.t
+ type 'a case_stk =
+ case_info * EInstance.t * 'a array * 'a pcase_return * ('a, EInstance.t) pcase_invert * 'a pcase_branch array
type 'a member =
| App of 'a app_node
- | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
+ | Case of 'a case_stk * Cst_stack.t
| Proj of Projection.t * Cst_stack.t
| Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -172,9 +176,9 @@ struct
let pr_c x = hov 1 (pr_c x) in
match member with
| App app -> str "ZApp" ++ pr_app_node pr_c app
- | Case (_,_,_,br,cst) ->
+ | Case ((_,_,_,_,_,br),cst) ->
str "ZCase(" ++
- prvect_with_sep (pr_bar) pr_c br
+ prvect_with_sep (pr_bar) (fun (_, b) -> pr_c b) br
++ str ")"
| Proj (p,cst) ->
str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
@@ -221,7 +225,7 @@ struct
if i < j then (l.(j), App (i,l,pred j) :: sk)
else (l.(j), sk)
- let equal f f_fix sk1 sk2 =
+ let equal f f_fix f_case sk1 sk2 =
let equal_cst_member x y =
match x, y with
| Cst_const (c1,u1), Cst_const (c2, u2) ->
@@ -236,8 +240,8 @@ struct
let t1,s1' = decomp_node_last a1 s1 in
let t2,s2' = decomp_node_last a2 s2 in
(f t1 t2) && (equal_rec s1' s2')
- | Case (_,t1,_,a1,_) :: s1, Case (_,t2,_,a2,_) :: s2 ->
- f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
+ | Case ((ci1,pms1,p1,t1,iv1,a1),_) :: s1, Case ((ci2,pms2,p2,iv2,t2,a2),_) :: s2 ->
+ f_case (ci1,pms1,p1,t1,iv1,a1) (ci2,pms2,p2,iv2,t2,a2) && equal_rec s1 s2
| (Proj (p,_)::s1, Proj(p2,_)::s2) ->
Projection.Repr.CanOrd.equal (Projection.repr p) (Projection.repr p2)
&& equal_rec s1 s2
@@ -284,7 +288,7 @@ struct
let will_expose_iota args =
List.exists
- (function (Fix (_,_,l) | Case (_,_,_,_,l) |
+ (function (Fix (_,_,l) | Case (_,l) |
Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
args
@@ -346,9 +350,9 @@ struct
then a
else Array.sub a i (j - i + 1) in
zip (mkApp (f, a'), s)
- | f, (Case (ci,rt,iv,br,cst_l)::s) when refold ->
- zip (best_state sigma (mkCase (ci,rt,iv,f,br), s) cst_l)
- | f, (Case (ci,rt,iv,br,_)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
+ | f, (Case ((ci,u,pms,rt,iv,br),cst_l)::s) when refold ->
+ zip (best_state sigma (mkCase (ci,u,pms,rt,iv,f,br), s) cst_l)
+ | f, (Case ((ci,u,pms,rt,iv,br),_)::s) -> zip (mkCase (ci,u,pms,rt,iv,f,br), s)
| f, (Fix (fix,st,cst_l)::s) when refold ->
zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
| f, (Fix (fix,st,_)::s) -> zip
@@ -533,7 +537,26 @@ let debug_RAKAM = Reductionops.debug_RAKAM
let equal_stacks sigma (x, l) (y, l') =
let f_equal x y = eq_constr sigma x y in
let eq_fix a b = f_equal (mkFix a) (mkFix b) in
- Stack.equal f_equal eq_fix l l' && f_equal x y
+ let eq_case (ci1, u1, pms1, p1, _, br1) (ci2, u2, pms2, p2, _, br2) =
+ Array.equal f_equal pms1 pms2 &&
+ f_equal (snd p1) (snd p2) &&
+ Array.equal (fun (_, c1) (_, c2) -> f_equal c1 c2) br1 br2
+ in
+ Stack.equal f_equal eq_fix eq_case l l' && f_equal x y
+
+let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
+ let args = Stack.tail ci.ci_npar args in
+ let args = Option.get (Stack.list_of_app_stack args) in
+ let br = lf.(i - 1) in
+ let subst =
+ if Int.equal ci.ci_cstr_nargs.(i - 1) ci.ci_cstr_ndecls.(i - 1) then
+ (* No let-bindings *)
+ List.rev args
+ else
+ let ctx = expand_branch env sigma u pms (ind, i) br in
+ subst_of_rel_context_instance ctx args
+ in
+ Vars.substl subst (snd br)
let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let open Context.Named.Declaration in
@@ -699,8 +722,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| _ -> fold ())
| _ -> fold ())
- | Case (ci,p,iv,d,lf) ->
- whrec Cst_stack.empty (d, Stack.Case (ci,p,iv,lf,cst_l) :: stack)
+ | Case (ci,u,pms,p,iv,d,lf) ->
+ whrec Cst_stack.empty (d, Stack.Case ((ci,u,pms,p,iv,lf),cst_l) :: stack)
| Fix ((ri,n),_ as f) ->
(match Stack.strip_n_app ri.(n) stack with
@@ -708,13 +731,14 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
|Some (bef,arg,s') ->
whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s'))
- | Construct ((ind,c),u) ->
+ | Construct (cstr ,u) ->
let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
if use_match || use_fix then
match Stack.strip_app stack with
- |args, (Stack.Case(ci, _, _, lf,_)::s') when use_match ->
- whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
+ |args, (Stack.Case(case,_)::s') when use_match ->
+ let r = apply_branch env sigma cstr args case in
+ whrec Cst_stack.empty (r, s')
|args, (Stack.Proj (p,_)::s') when use_match ->
whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f90c143a1a..54e9a87c96 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -216,7 +216,7 @@ let build_sym_scheme env ind =
let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+1) realsign_ind)
(mkApp (mkIndU indu,Array.concat
@@ -225,7 +225,7 @@ let build_sym_scheme env ind =
rel_vect (2*nrealargs+2) nrealargs])),
NoInvert,
mkRel 1 (* varH *),
- [|cstr (nrealargs+1)|]))))
+ [|cstr (nrealargs+1)|])))))
in c, UState.of_context_set ctx
let sym_scheme_kind =
@@ -279,13 +279,13 @@ let build_sym_involutive_scheme env ind =
let c =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign_ind
- (mkCase (ci,
- my_it_mkLambda_or_LetIn_name
- (lift_rel_context (nrealargs+1) realsign_ind)
- (mkApp (eq,[|
- mkApp
- (mkIndU indu, Array.concat
- [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
+ (mkCase (Inductive.contract_case env (ci,
+ my_it_mkLambda_or_LetIn_name
+ (lift_rel_context (nrealargs+1) realsign_ind)
+ (mkApp (eq,[|
+ mkApp
+ (mkIndU indu, Array.concat
+ [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
rel_vect (2*nrealargs+2) nrealargs;
rel_vect 1 nrealargs]);
mkApp (sym,Array.concat
@@ -300,7 +300,7 @@ let build_sym_involutive_scheme env ind =
mkRel 1|])),
NoInvert,
mkRel 1 (* varH *),
- [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+ [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))))
in (c, UState.of_context_set ctx)
let sym_involutive_scheme_kind =
@@ -437,11 +437,11 @@ let build_l2r_rew_scheme dep env ind kind =
rel_vect 4 nrealargs;
[|mkRel 2|]])|]]) in
let main_body =
- mkCase (ci,
+ mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
NoInvert,
applied_sym_C 3,
- [|mkVar varHC|])
+ [|mkVar varHC|]))
in
let c =
(my_it_mkLambda_or_LetIn paramsctxt
@@ -451,7 +451,7 @@ let build_l2r_rew_scheme dep env ind kind =
(mkNamedLambda (make_annot varHC indr) applied_PC
(mkNamedLambda (make_annot varH indr) (lift 2 applied_ind)
(if dep then (* we need a coercion *)
- mkCase (cieq,
+ mkCase (Inductive.contract_case env (cieq,
mkLambda (make_annot (Name varH) indr,lift 3 applied_ind,
mkLambda (make_annot Anonymous indr,
mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
@@ -459,7 +459,7 @@ let build_l2r_rew_scheme dep env ind kind =
NoInvert,
mkApp (sym_involutive,
Array.append (Context.Rel.to_extended_vect mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]),
- [|main_body|])
+ [|main_body|]))
else
main_body))))))
in (c, UState.of_context_set ctx)
@@ -540,7 +540,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(my_it_mkLambda_or_LetIn paramsctxt
(my_it_mkLambda_or_LetIn_name realsign
(mkNamedLambda (make_annot varH indr) applied_ind
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+1) realsign_ind)
(mkNamedProd (make_annot varP indr)
@@ -553,7 +553,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
(my_it_mkProd_or_LetIn
(if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
(mkNamedLambda (make_annot varHC indr) applied_PC'
- (mkVar varHC))|])))))
+ (mkVar varHC))|]))))))
in c, UState.of_context_set ctx
(**********************************************************************)
@@ -620,7 +620,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
(if dep then realsign_ind else realsign)) s)
(mkNamedLambda (make_annot varHC indr) (lift 1 applied_PG)
(mkApp
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (nrealargs+3) realsign_ind)
(mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)),
@@ -629,7 +629,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
[|mkLambda
(make_annot (Name varHC) indr,
lift (nrealargs+3) applied_PC,
- mkRel 1)|]),
+ mkRel 1)|])),
[|mkVar varHC|]))))))
in c, UState.of_context_set ctx
@@ -825,7 +825,7 @@ let build_congr env (eq,refl,ctx) ind =
(mkIndU indu,
Context.Rel.to_extended_list mkRel (mip.mind_nrealargs+2) paramsctxt @
Context.Rel.to_extended_list mkRel 0 realsign))
- (mkCase (ci,
+ (mkCase (Inductive.contract_case env (ci,
my_it_mkLambda_or_LetIn_name
(lift_rel_context (mip.mind_nrealargs+3) realsign)
(mkLambda
@@ -843,7 +843,7 @@ let build_congr env (eq,refl,ctx) ind =
mkVar varH,
[|mkApp (refl,
[|mkVar varB;
- mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
+ mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))))
in c, UState.of_context_set ctx
let congr_scheme_kind = declare_individual_scheme_object "_congr"
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ace51c40d4..0cc8becd8f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -46,7 +46,7 @@ let rec head_bound sigma t = match EConstr.kind sigma t with
| Prod (_, _, b) -> head_bound sigma b
| LetIn (_, _, _, b) -> head_bound sigma b
| App (c, _) -> head_bound sigma c
-| Case (_, _, _, c, _) -> head_bound sigma c
+| Case (_, _, _, _, _, c, _) -> head_bound sigma c
| Ind (ind, _) -> GlobRef.IndRef ind
| Const (c, _) -> GlobRef.ConstRef c
| Construct (c, _) -> GlobRef.ConstructRef c
@@ -591,7 +591,7 @@ struct
let head_evar sigma c =
let rec hrec c = match EConstr.kind sigma c with
| Evar (evk,_) -> evk
- | Case (_,_,_,c,_) -> hrec c
+ | Case (_,_,_,_,_,c,_) -> hrec c
| App (c,_) -> hrec c
| Cast (c,_,_) -> hrec c
| Proj (p, c) -> hrec c
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 39c5c9562f..b40bdbc25e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3293,7 +3293,7 @@ let expand_projections env sigma c =
let rec aux env c =
match EConstr.kind sigma c with
| Proj (p, c) -> Retyping.expand_projection env sigma p (aux env c) []
- | _ -> map_constr_with_full_binders sigma push_rel aux env c
+ | _ -> map_constr_with_full_binders env sigma push_rel aux env c
in
aux env c
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index df07dcbca7..f12d4e5de5 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -335,8 +335,9 @@ struct
meta
in
Meta meta
- | Case (ci,c1,_iv,c2,ca) ->
- Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca))
+ | Case (ci,u1,pms1,c1,_iv,c2,ca) ->
+ let f_ctx (_, p) = pat_of_constr p in
+ Term(DCase(ci,f_ctx c1,pat_of_constr c2,Array.map f_ctx ca))
| Fix ((ia,i),(_,ta,ca)) ->
Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca))
| CoFix (i,(_,ta,ca)) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:17:22 +0000