From b8ef115e278fdafb25e16b0f65fccbc42dcbedbf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 27 Apr 2023 16:21:14 +0200 Subject: [PATCH] Add head reduction flags (`lazy head beta` etc) --- doc/sphinx/proofs/writing-proofs/equality.rst | 12 ++++++-- doc/tools/docgram/common.edit_mlg | 8 +++--- doc/tools/docgram/fullGrammar | 7 +++-- doc/tools/docgram/orderedGrammar | 7 +++-- plugins/funind/recdef.ml | 3 +- plugins/ltac/g_tactic.mlg | 19 ++++++++----- plugins/ltac2/tac2quote.ml | 2 +- plugins/ltac2/tac2stdlib.ml | 1 + plugins/ssr/ssrcommon.ml | 2 +- tactics/genredexpr.mli | 5 ++++ tactics/redexpr.ml | 28 +++++++++++++------ tactics/redops.ml | 15 ++++++---- test-suite/output/reduction.out | 27 ++++++++++++++++++ test-suite/output/reduction.v | 14 ++++++++++ 14 files changed, 113 insertions(+), 37 deletions(-) diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst index ee57c0ebb06d..735f897bf5bc 100644 --- a/doc/sphinx/proofs/writing-proofs/equality.rst +++ b/doc/sphinx/proofs/writing-proofs/equality.rst @@ -492,9 +492,10 @@ which reduction engine to use. See :ref:`type-cast`.) For example: .. prodn:: reductions ::= {+ @reduction } - | @delta_reductions + | {? head } @delta_reductions reduction ::= beta | delta {? @delta_reductions } + | head | match | fix | cofix @@ -506,6 +507,11 @@ which reduction engine to use. See :ref:`type-cast`.) For example: specified by name, all reductions are applied. If any reductions are specified by name, then only the named reductions are applied. The reductions include: + `head` + Do only head reduction, without going under binders. Only + supported by :tacn:`simpl`, :tacn:`cbn` and :tacn:`lazy`. + If this is the only specified reduction, all other reductions are applied. + `beta` :term:`beta-reduction` of functional application @@ -577,7 +583,7 @@ which reduction engine to use. See :ref:`type-cast`.) For example: information about the constants it encounters and the unfolding decisions it makes. -.. tacn:: simpl {? @delta_reductions } {? {| @reference_occs | @pattern_occs } } @simple_occurrences +.. tacn:: simpl {? head } {? @delta_reductions } {? {| @reference_occs | @pattern_occs } } @simple_occurrences .. insertprodn reference_occs pattern_occs @@ -891,7 +897,7 @@ Evaluation of a term can be performed with: | native_compute {? {| @reference_occs | @pattern_occs } } | red | hnf - | simpl {? @delta_reductions } {? {| @reference_occs | @pattern_occs } } + | simpl {? head } {? @delta_reductions } {? {| @reference_occs | @pattern_occs } } | cbn {? @reductions } | unfold {+, @reference_occs } | fold {+ @one_term } diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 9eee6fc463fd..355f3288d7fa 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -673,8 +673,8 @@ ltac2_branches: [ ] strategy_flag: [ -| REPLACE OPT delta_flag -| WITH delta_flag +| REPLACE OPT "head" OPT delta_flag +| WITH OPT "head" delta_flag (*| REPLACE LIST1 red_flags | WITH LIST1 red_flag*) | (* empty *) @@ -980,8 +980,8 @@ simple_tactic: [ | WITH "autounfold" hintbases OPT simple_occurrences | REPLACE "red" clause_dft_concl | WITH "red" simple_occurrences -| REPLACE "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl -| WITH "simpl" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences +| REPLACE "simpl" OPT "head" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl +| WITH "simpl" OPT "head" OPT delta_flag OPT ref_or_pattern_occ simple_occurrences | REPLACE "hnf" clause_dft_concl | WITH "hnf" simple_occurrences | REPLACE "cbv" strategy_flag clause_dft_concl diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 970d9a3af689..1c4a48f46145 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1778,7 +1778,7 @@ simple_tactic: [ | "inversion" quantified_hypothesis "using" constr in_hyp_list | "red" clause_dft_concl | "hnf" clause_dft_concl -| "simpl" delta_flag OPT ref_or_pattern_occ clause_dft_concl +| "simpl" OPT "head" delta_flag OPT ref_or_pattern_occ clause_dft_concl | "cbv" strategy_flag clause_dft_concl | "cbn" strategy_flag clause_dft_concl | "lazy" strategy_flag clause_dft_concl @@ -2431,6 +2431,7 @@ red_flag: [ | "cofix" | "zeta" | "delta" delta_flag +| "head" ] delta_flag: [ @@ -2441,13 +2442,13 @@ delta_flag: [ strategy_flag: [ | LIST1 red_flag -| delta_flag +| OPT "head" delta_flag ] red_expr: [ | "red" | "hnf" -| "simpl" delta_flag OPT ref_or_pattern_occ +| "simpl" OPT "head" delta_flag OPT ref_or_pattern_occ | "cbv" strategy_flag | "cbn" strategy_flag | "lazy" strategy_flag diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index c9a1897b4f4e..6ce77e5a245e 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -485,7 +485,7 @@ red_expr: [ | "native_compute" OPT [ reference_occs | pattern_occs ] | "red" | "hnf" -| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ] +| "simpl" OPT "head" OPT delta_reductions OPT [ reference_occs | pattern_occs ] | "cbn" OPT reductions | "unfold" LIST1 reference_occs SEP "," | "fold" LIST1 one_term @@ -495,12 +495,13 @@ red_expr: [ reductions: [ | LIST1 reduction -| delta_reductions +| OPT "head" delta_reductions ] reduction: [ | "beta" | "delta" OPT delta_reductions +| "head" | "match" | "fix" | "cofix" @@ -1526,7 +1527,7 @@ simple_tactic: [ | "inversion" [ ident | natural ] "using" one_term OPT ( "in" LIST1 ident ) | "red" simple_occurrences | "hnf" simple_occurrences -| "simpl" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences +| "simpl" OPT "head" OPT delta_reductions OPT [ reference_occs | pattern_occs ] simple_occurrences | "cbv" OPT reductions simple_occurrences | "cbn" OPT reductions simple_occurrences | "lazy" OPT reductions simple_occurrences diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e83c71302049..7c0093bd5dfc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -161,7 +161,8 @@ let simpl_iter clause = ; rCofix = true ; rZeta = true ; rDelta = false - ; rConst = [EvalConstRef (const_of_ref (delayed_force iter_ref))] }) + ; rConst = [EvalConstRef (const_of_ref (delayed_force iter_ref))] + ; rStrength = Norm }) clause (* Others ugly things ... *) diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 73bfffb2d6d3..4e639f993d59 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -30,7 +30,9 @@ open Locus open Pcoq -let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] +let all_with ~head delta = + let all = [FBeta;FMatch;FFix;FCofix;FZeta;delta] in + Redops.make_red_flag (if head then FHead :: all else all) let err () = raise Gramlib.Stream.Failure @@ -348,6 +350,7 @@ GRAMMAR EXTEND Gram | IDENT "cofix" -> { [FCofix] } | IDENT "zeta" -> { [FZeta] } | IDENT "delta"; d = delta_flag -> { [d] } + | IDENT "head" -> { [FHead] } ] ] ; delta_flag: @@ -358,17 +361,18 @@ GRAMMAR EXTEND Gram ; strategy_flag: [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) } - | d = delta_flag -> { all_with d } + | h = OPT [ IDENT "head" -> { () } ]; d = delta_flag -> { all_with ~head:(Option.has_some h) d } ] ] ; red_expr: [ [ IDENT "red" -> { Red false } | IDENT "hnf" -> { Hnf } - | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with d,po) } + | IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ]; + d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with ~head:(Option.has_some h) d,po) } | IDENT "cbv"; s = strategy_flag -> { Cbv s } | IDENT "cbn"; s = strategy_flag -> { Cbn s } | IDENT "lazy"; s = strategy_flag -> { Lazy s } - | IDENT "compute"; delta = delta_flag -> { Cbv (all_with delta) } + | IDENT "compute"; delta = delta_flag -> { Cbv (all_with ~head:false delta) } | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po } | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po } | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul } @@ -677,8 +681,9 @@ GRAMMAR EXTEND Gram { CAst.make ~loc @@ TacAtom (TacReduce (Red false, cl)) } | IDENT "hnf"; cl = clause_dft_concl -> { CAst.make ~loc @@ TacAtom (TacReduce (Hnf, cl)) } - | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - { CAst.make ~loc @@ TacAtom (TacReduce (Simpl (all_with d, po), cl)) } + | IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ]; d = delta_flag; + po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> + { CAst.make ~loc @@ TacAtom (TacReduce (Simpl (all_with ~head:(Option.has_some h) d, po), cl)) } | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl -> { CAst.make ~loc @@ TacAtom (TacReduce (Cbv s, cl)) } | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl -> @@ -686,7 +691,7 @@ GRAMMAR EXTEND Gram | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl -> { CAst.make ~loc @@ TacAtom (TacReduce (Lazy s, cl)) } | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl -> - { CAst.make ~loc @@ TacAtom (TacReduce (Cbv (all_with delta), cl)) } + { CAst.make ~loc @@ TacAtom (TacReduce (Cbv (all_with ~head:false delta), cl)) } | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> { CAst.make ~loc @@ TacAtom (TacReduce (CbvVm po, cl)) } | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml index a9c510787e38..841da5099a08 100644 --- a/plugins/ltac2/tac2quote.ml +++ b/plugins/ltac2/tac2quote.ml @@ -379,7 +379,7 @@ let make_red_flag l = in add_flag {rBeta = false; rMatch = false; rFix = false; rCofix = false; - rZeta = false; rDelta = false; rConst = []} + rZeta = false; rDelta = false; rConst = []; rStrength = Norm; } l let of_reference r = diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml index e0f65739cf3b..5ed3c3a7a23c 100644 --- a/plugins/ltac2/tac2stdlib.ml +++ b/plugins/ltac2/tac2stdlib.ml @@ -64,6 +64,7 @@ let clause = make_to_repr to_clause let to_red_flag v = match Value.to_tuple v with | [| beta; iota; fix; cofix; zeta; delta; const |] -> { + rStrength = Norm; (* specifying rStrength is not yet supported *) rBeta = Value.to_bool beta; rMatch = Value.to_bool iota; rFix = Value.to_bool fix; diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index fbec5e3e5cf4..9807cd0856c2 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1194,7 +1194,7 @@ let tclFULL_BETAIOTA = Goal.enter begin fun gl -> let r, _ = Redexpr.reduction_of_red_expr (Goal.env gl) Genredexpr.(Lazy { rBeta=true; rMatch=true; rFix=true; rCofix=true; - rZeta=false; rDelta=false; rConst=[]}) in + rZeta=false; rDelta=false; rConst=[]; rStrength=Norm}) in Tactics.e_reduct_in_concl ~cast:false ~check:false (r,Constr.DEFAULTcast) end diff --git a/tactics/genredexpr.mli b/tactics/genredexpr.mli index f506c11e62be..f7563c533a66 100644 --- a/tactics/genredexpr.mli +++ b/tactics/genredexpr.mli @@ -20,10 +20,15 @@ type 'a red_atom = | FZeta | FConst of 'a list | FDeltaBut of 'a list + | FHead (** This list of atoms is immediately converted to a [glob_red_flag] *) +type strength = Norm | Head +(* someday we may add NotUnderBinders *) + type 'a glob_red_flag = { + rStrength : strength; rBeta : bool; rMatch : bool; rFix : bool; diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 2b9f4883a061..1b4928fb5300 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -132,7 +132,7 @@ type red_expr = (constr, evaluable_global_reference, constr_pattern) red_expr_gen type red_expr_val = - (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0 + (constr, evaluable_global_reference, constr_pattern, strength * CClosure.RedFlags.reds) red_expr_gen0 let make_flag_constant = function | EvalVarRef id -> fVAR id @@ -158,7 +158,8 @@ let make_flag env f = List.fold_right (fun v red -> red_add red (make_flag_constant v)) f.rConst red - in red + in + f.rStrength, red (* table of custom reductino fonctions, not synchronized, filled via ML calls to [declare_reduction] *) @@ -227,7 +228,7 @@ let rec eval_red_expr env = function let () = if not (simplIsCbn () || List.is_empty f.rConst) then warn_simpl_unfolding_modifiers () in - let f = if simplIsCbn () then make_flag env f else CClosure.all (* dummy *) in + let f = if simplIsCbn () then make_flag env f else f.rStrength, CClosure.all (* dummy *) in Simpl (f, o) | Cbv f -> Cbv (make_flag env f) | Cbn f -> Cbn (make_flag env f) @@ -244,13 +245,22 @@ let reduction_of_red_expr_val = function if internal then (e_red try_red_product,DEFAULTcast) else (e_red red_product,DEFAULTcast) | Hnf -> (e_red hnf_constr,DEFAULTcast) - | Simpl (f,o) -> - let am = if simplIsCbn () then Cbn.norm_cbn f else simpl in + | Simpl ((w,f),o) -> + let am = match w, simplIsCbn () with + | Norm, true -> Cbn.norm_cbn f + | Norm, false -> simpl + | Head, true -> Cbn.whd_cbn f + | Head, false -> whd_simpl + in (contextuallize am o,DEFAULTcast) - | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast) - | Cbn f -> - (e_red (Cbn.norm_cbn f), DEFAULTcast) - | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast) + | Cbv (Norm, f) -> (e_red (cbv_norm_flags f),DEFAULTcast) + | Cbv (Head, _) -> CErrors.user_err Pp.(str "cbv does not support head-only reduction.") + | Cbn (w,f) -> + let cbn = match w with Norm -> Cbn.norm_cbn | Head -> Cbn.whd_cbn in + (e_red (cbn f), DEFAULTcast) + | Lazy (w,f) -> + let redf = match w with Norm -> clos_norm_flags | Head -> clos_whd_flags in + (e_red (redf f),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) diff --git a/tactics/redops.ml b/tactics/redops.ml index bc846681c90e..828f36ff3f24 100644 --- a/tactics/redops.ml +++ b/tactics/redops.ml @@ -12,9 +12,15 @@ open Genredexpr let union_consts l1 l2 = Util.List.union (=) l1 l2 (* FIXME *) + +let all_flags = + {rBeta = true; rMatch = true; rFix = true; rCofix = true; + rZeta = true; rDelta = true; rConst = []; rStrength = Norm; } + let make_red_flag l = let rec add_flag red = function | [] -> red + | FHead :: lf -> add_flag { red with rStrength = Head } lf | FBeta :: lf -> add_flag { red with rBeta = true } lf | FMatch :: lf -> add_flag { red with rMatch = true } lf | FFix :: lf -> add_flag { red with rFix = true } lf @@ -35,13 +41,12 @@ let make_red_flag l = in add_flag {rBeta = false; rMatch = false; rFix = false; rCofix = false; - rZeta = false; rDelta = false; rConst = []} + rZeta = false; rDelta = false; rConst = []; rStrength = Norm; } l - -let all_flags = - {rBeta = true; rMatch = true; rFix = true; rCofix = true; - rZeta = true; rDelta = true; rConst = []} +let make_red_flag = function + | [FHead] -> { all_flags with rStrength = Head } + | l -> make_red_flag l (** Mapping [red_expr_gen] *) diff --git a/test-suite/output/reduction.out b/test-suite/output/reduction.out index ff327aa5f13a..19f7dcaaffc5 100644 --- a/test-suite/output/reduction.out +++ b/test-suite/output/reduction.out @@ -2,3 +2,30 @@ : nat = n + 0 : nat + = S (1 + 2) + : nat + = S (1 + 2) + : nat + = S + ((fix add (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (add p m) + end) 1 2) + : nat + = (fix add (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (add p m) + end) 2 2 + : nat + = S (1 + (2 + 2)) + : nat + = S (1 + 2 + 2) + : nat + = ignore (fun x : nat => 1 + x) + : unit + = ignore (fun x : nat => 1 + x) + : unit + = ignore (fun x : nat => 1 + x) + : unit diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v index ab6262823c21..5263ed40d493 100644 --- a/test-suite/output/reduction.v +++ b/test-suite/output/reduction.v @@ -11,3 +11,17 @@ Eval simpl in (fix plus (n m : nat) {struct n} : nat := Eval hnf in match (plus (S n) O) with S n => n | _ => O end. +Eval simpl head in 2 + 2. +Eval cbn head in 2 + 2. +Eval lazy head in 2 + 2. + +Eval lazy head delta in 2 + 2. + +Eval simpl head in 2 + (2 + 2). + +Eval simpl head in (2 + 2) + 2. + +Axiom ignore : forall {T}, T -> unit. +Eval simpl head in ignore (fun x => 1 + x). +Eval cbn head in ignore (fun x => 1 + x). +Eval lazy head in ignore (fun x => 1 + x).