From 422e17fbe2193cd0708903cd3e2182a2059e973f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 9 Feb 2024 14:46:01 +0100 Subject: [PATCH] CEP on unifying the syntax and expressiveness of reduction strategies. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Gaëtan Gilbert --- text/unified-reduction-strategies.md | 83 ++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 text/unified-reduction-strategies.md diff --git a/text/unified-reduction-strategies.md b/text/unified-reduction-strategies.md new file mode 100644 index 00000000..2bfaab2c --- /dev/null +++ b/text/unified-reduction-strategies.md @@ -0,0 +1,83 @@ +- Title: A unified view at reduction strategies with extended unfolding control + +- Drivers: Hugo Herbelin + +---- + +# Summary and motivation + +Each user-level, compilation-free, reduction strategy of Coq, `simpl`, +`cbn`, `cbv`, `lazy`, come, in addition to a reduction order +(call-by-name, call-by-value, call-by-need), with its own +specificities, such as: + +- refolding (co)fixpoints (in `simpl` and `cbn`) +- local specification of the kind of reduction to consider (`cbn`, `cbv`, `lazy`) +- specification of a subterm to reduce (`simpl pattern`) +- some static parameterization of the unfolding (argument flags `simpl never`, `simpl nonmeta`, `!`, `/`) + +The proposal is to go in the direction of one unified entry point to +reduction strategies eventually supporting all combinations of the +features currently provided only by one or the other entry point, thus +gaining both in expressiveness and easiness to document. At the +current time, the focus is however only on a unified syntax. + +Additionally, the proposal is intended to complement CEP coq/ceps#35 +(more fine-tuning of reduction) and CEP coq/ceps#84 (support for +symbol sets, hereafter called unfol bases). + +# Detailed design + +We propose to elaborate a unified syntax for all four mentioned user-level reduction strategies on top of the following: + +```text +red_expr ::= red_name pattern_opt flags_opt +red_name ::= "cbv" | "cbn" | "lazy" | "simpl" +pattern ::= CONSTR +flags ::= "with" head_flag_opt flag_list unfold_bases +head_flag ::= "head" +flag ::= "beta" | "iota" | "zeta" | "match" | "fix" | "cofix" | "delta" +unfold_bases ::= "+" unfold_base signed_unfold_base_list | signed_unfold_base_list +signed_unfold_base ::= unfold_base | "-" unfold_base +unfold_base ::= "[" QUALID_list "]" | IDENT constraint_opt | "module" "(" QUALID ")" +constraint ::= "(" op INT ")" +op ::= "<" | ">" | "<=" | ">=" +``` +where: +- `pattern` would work as it does currently in `simpl pattern` +- the use of `with` is reminiscent of the `with hintbase` of `auto`, `autorewrite`, `autounfold`, `firstorder`, ... +- `red_name with ...` can be abbreviated into `red_name ...` for consistency with the current syntax of `cbn`, `cbv`, `lazy` +- `- unfold_base` would mean subtracting the given unfold_base to what has been computed so far +- `unfold_base` in `signed_unfold_base` would mean adding to what has been computed so far +- `+ unfold_base signed_unfold_base_list` would mean starting from the current transparency state, adding `unfold_base`, and continuing with `signed_unfold_base_list` +- `[ QUALID_list ]` would refers to a list of names controlling the reduction, be as it is now +- `IDENT` would refer to an unfolding database (see CEP coq/ceps#84 about how to build such databases) +- `module(QUALID)` would mean to include constants from module `QUALID` +- one could add a variant of `module(QUALID)` for recursive inclusion +- `constraint` would select a subset of the bases depending on the level of the hint +- the list of names in `QUALID_list` could include constructors, e.g. `None` to reduce `match` only on constructor `None` +- then, current flag `match` could be seen as an alias for declaring all constructors "unfoldable" +- `iota` would remain an alias for `match` + `fix` + `cofix` +- if both `delta` and bases are given, `delta` should be last in the list of flags + +Note: in a world where all fixpoint and cofixpoints are globally +named, the trigerring of `iota` could thus be mostly controlled by +giving or not the names of the relevant fixpoint, cofixpoints, +projections, constructors. + +Note: we could also try to unify the syntax `[ QUALID_list ]` with the +`using QUALID_list` clause of `auto` and `firstorder`. + +# Implementation issues + +The implementation work at this stage would be mostly at the parsing level or database management level: +- a generic `pattern` combinator is already implemented (`contextually`), it is just a matter of encapsulating all reduction strategies with it +- for database management, see CEP coq/ceps#84 + +# Unresolved questions + +We would probably expect all reduction strategies to eventually do **refolding**? This refolding could be `simpl`-style (maximal refolding) or to just the surrounding name of the global (co)fixpoints. + +We would probably expect all reduction strategies to eventually support different **unfolding policies** (exposing `match`, supporting reduction of nested `match`/`fix`, supporting reduction of match-free constant which "simplify" the term in some sense). + +Would a **level**, like in `with_strategy level [...]` be useful?