From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 3 Mar 2019 21:03:37 +0100 Subject: Change the representation of kernel case. We store bound variable names instead of functions for both branches and predicate, and we furthermore add the parameters in the node. Let bindings are not taken into account and require an environment lookup for retrieval. --- tactics/cbn.ml | 60 ++++++++++++++++++++++++++++++++++++---------------- tactics/eqschemes.ml | 40 +++++++++++++++++------------------ tactics/hints.ml | 4 ++-- tactics/tactics.ml | 2 +- tactics/term_dnet.ml | 5 +++-- 5 files changed, 68 insertions(+), 43 deletions(-) (limited to 'tactics') 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)) -> -- cgit v1.2.3