From 08f5ede8d8466ad9bbf695a8c069d08d4dfc734a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Nov 2017 13:05:10 -0500 Subject: Make pipeline options more easily extensible Also add a dummy option about renaming binders, to be used in an upcoming commit. --- src/Compilers/Z/Bounds/Pipeline.v | 5 +++-- src/Compilers/Z/Bounds/Pipeline/Definition.v | 13 +++++++++---- 2 files changed, 12 insertions(+), 6 deletions(-) (limited to 'src/Compilers/Z') 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 -- cgit v1.2.3