Make pipeline options more easily extensible

Also add a dummy option about renaming binders, to be used in an
upcoming commit.

4 files changed, 15 insertions, 6 deletions

diff --git a/_CoqProject b/_CoqProject
index 75635f2b8..e8d3b792d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5818,6 +5818,7 @@ src/Util/CPSUtil.v
 src/Util/ChangeInAll.v
 src/Util/Curry.v
 src/Util/Decidable.v
+src/Util/DefaultedTypes.v
 src/Util/Equality.v
 src/Util/Factorize.v
 src/Util/FixCoqMistakes.v
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v
index 54dc00871..c7060ea44 100644
--- a/src/Compilers/Z/Bounds/Pipeline.v
+++ b/src/Compilers/Z/Bounds/Pipeline.v
@@ -17,6 +17,7 @@ while instantiating [?x] and [?bounds] with nicely-reduced constants.
 Module Export Exports.
   Export Glue.Exports.
   Export ReflectiveTactics.Exports.
+  Existing Instance DefaultedTypes.by_default.
 End Exports.
 
 Ltac refine_reflectively_gen allowable_bit_widths opts :=
@@ -43,9 +44,9 @@ Ltac refine_reflectively64_with_uint8 := refine_reflectively64_with_uint8_with d
 Ltac refine_reflectively32_with_uint8 := refine_reflectively32_with_uint8_with default_PipelineOptions.
 
 (** Convenience notations for options *)
-Definition anf := {| Pipeline.Definition.anf := true ; Pipeline.Definition.adc_fusion := true |}.
+Definition anf := {| Pipeline.Definition.anf := true |}.
 Definition anf_without_adc_fusion := {| Pipeline.Definition.anf := true ; Pipeline.Definition.adc_fusion := false |}.
-Definition adc_fusion := {| Pipeline.Definition.anf := true ; Pipeline.Definition.adc_fusion := false |}.
+Definition adc_fusion := {| Pipeline.Definition.adc_fusion := true |}.
 Definition default := default_PipelineOptions.
 
 (** The default *)
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index b8bc3d163..e5503511d 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -72,14 +72,19 @@ Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
 Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnInterp.
 Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnWf.
 Require Import Crypto.Util.Sigma.MapProjections.
+Require Import Crypto.Util.DefaultedTypes.
 
 (** *** Definition of the Post-Wf Pipeline *)
 (** We define the record that holds various options to customize the
     pipeline. *)
-Record PipelineOptions := { anf : bool ; adc_fusion : bool }.
-Definition default_PipelineOptions :=
-  {| anf := false ;
-     adc_fusion := true |}.
+Record PipelineOptions :=
+  {
+    anf            : with_default bool false;
+    adc_fusion     : with_default bool true;
+    rename_binders : with_default bool false;
+  }.
+Definition default_PipelineOptions := {| anf := _ |}.
+
 (** Do not change the name or the type of these two definitions *)
 (** The definition [PostWfPreBoundsPipeline] is for the part of the
     pipeline that comes before [MapCast]; it must preserve the type of
diff --git a/src/Util/DefaultedTypes.v b/src/Util/DefaultedTypes.v
new file mode 100644
index 000000000..37d9c25ef
--- /dev/null
+++ b/src/Util/DefaultedTypes.v
@@ -0,0 +1,2 @@
+Class with_default (T : Type) (default : T) := defaulted : T.
+Global Instance by_default {T} {d} : with_default T d := d.