diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-13 13:05:10 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-13 13:56:29 -0500 |
commit | 08f5ede8d8466ad9bbf695a8c069d08d4dfc734a (patch) | |
tree | 14feb03e26dee7f0058a953d96fdedf7d3ba138e /src | |
parent | 011e29790182b3c85889ce402f7fc9fad0ac0817 (diff) |
Make pipeline options more easily extensible
Also add a dummy option about renaming binders, to be used in an
upcoming commit.
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 5 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 13 | ||||
-rw-r--r-- | src/Util/DefaultedTypes.v | 2 |
3 files changed, 14 insertions, 6 deletions
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. |