Allow specifying pipeline options at call-time

For now, the only option is anormal-form.  This will be needed for
freeze, because the adc optimization doesn't work when not in anf.

3 files changed, 31 insertions, 17 deletions

diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v
index 0db061ec4..4e3696854 100644
--- a/src/Compilers/Z/Bounds/Pipeline.v
+++ b/src/Compilers/Z/Bounds/Pipeline.v
@@ -15,13 +15,17 @@ Module Export Exports.
   Export ReflectiveTactics.Exports.
 End Exports.
 
-Ltac refine_reflectively_gen allowable_bit_widths :=
+Ltac refine_reflectively_gen allowable_bit_widths opts :=
   refine_to_reflective_glue allowable_bit_widths;
-  do_reflective_pipeline.
+  do_reflective_pipeline opts.
 
-Ltac refine_reflectively128 := refine_reflectively_gen (128::256::nil)%nat%list.
-Ltac refine_reflectively64 := refine_reflectively_gen (64::128::nil)%nat%list.
-Ltac refine_reflectively32 := refine_reflectively_gen (32::64::nil)%nat%list.
+Ltac refine_reflectively128_with opts := refine_reflectively_gen (128::256::nil)%nat%list opts.
+Ltac refine_reflectively64_with opts := refine_reflectively_gen (64::128::nil)%nat%list opts.
+Ltac refine_reflectively32_with opts := refine_reflectively_gen (32::64::nil)%nat%list opts.
+Ltac refine_reflectively128 := refine_reflectively128_with default_PipelineOptions.
+Ltac refine_reflectively64 := refine_reflectively64_with default_PipelineOptions.
+Ltac refine_reflectively32 := refine_reflectively32_with default_PipelineOptions.
 
 (** The default *)
-Ltac refine_reflectively := refine_reflectively64.
+Ltac refine_reflectively_with opts := refine_reflectively64_with opts.
+Ltac refine_reflectively := refine_reflectively_with default_PipelineOptions.
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index 8ab15943d..675c4d2d0 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -71,9 +71,15 @@ Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnWf.
 Require Import Crypto.Util.Sigma.MapProjections.
 
 (** *** Definition of the Post-Wf Pipeline *)
+(** We define the record that holds various options to customize the
+    pipeline. *)
+Record PipelineOptions := { anf : bool }.
+Definition default_PipelineOptions :=
+  {| anf := false |}.
 (** Do not change the name or the type of this definition *)
 Definition PostWfPipeline
            round_up
+           (opts : PipelineOptions)
            {t} (e : Expr base_type op t)
            (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
   : option (@ProcessedReflectivePackage round_up)
@@ -83,7 +89,7 @@ Definition PostWfPipeline
         let e := SimplifyArith e in
         let e := InlineConst e in
         let e := SimplifyArith e in
-        (*let e := ANormal e in*)
+        let e := if opts.(anormal) then ANormal e else e in
         let e := InlineConst e in
         (*let e := CSE false e in*)
         let e := MapCast _ e input_bounds in
@@ -115,11 +121,12 @@ Section with_round_up_list.
   Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
 
   Definition PostWfPipelineCorrect
+             opts
              {t}
              (e : Expr base_type op t)
              (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
              (Hwf : Wf e)
-             {b e'} (He : PostWfPipeline _ e input_bounds
+             {b e'} (He : PostWfPipeline _ opts e input_bounds
                           = Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |})
              (v : interp_flat_type Syntax.interp_base_type (domain t))
              (v' : interp_flat_type Syntax.interp_base_type (pick_type input_bounds))
@@ -133,12 +140,12 @@ Section with_round_up_list.
             || inversion_sigma || eliminate_hprop_eq || inversion_prod
             || simpl in * || subst).
     (** Now handle all the transformations that come after the word-size selection *)
-    autorewrite with reflective_interp.
+    all:autorewrite with reflective_interp.
     (** Now handle word-size selection *)
-    eapply MapCastCorrect_eq; [ | eassumption | eassumption | .. ];
-      [ solve [ auto 60 with wf ] | reflexivity | ].
+    all:(eapply MapCastCorrect_eq; [ | eassumption | eassumption | .. ];
+         [ solve [ auto 60 with wf ] | reflexivity | ]).
     (** Now handle all the transformations that come before the word-size selection *)
-    repeat autorewrite with reflective_interp; reflexivity.
+    all:repeat autorewrite with reflective_interp; reflexivity.
   Qed.
 End with_round_up_list.
 
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 9876c568c..1f82cb9f8 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -155,6 +155,7 @@ Section with_round_up_list.
   Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
 
   Definition PipelineCorrect
+             opts
              {t}
              {input_bounds : interp_flat_type Bounds.interp_base_type (domain t)}
              {given_output_bounds : interp_flat_type Bounds.interp_base_type (codomain t)}
@@ -174,7 +175,7 @@ Section with_round_up_list.
                  let P := (@reflect_wfT base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil _ _ (ExprEta' e _) (ExprEta' e _)) in
                  trueify P = P)
              (** ** post-wf-pipeline *)
-             (Hpost : e_pkg = PostWfPipeline _ e input_bounds)
+             (Hpost : e_pkg = PostWfPipeline _ opts e input_bounds)
              (Hpost_correct : Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg)
              (** ** renaming *)
              (Hrenaming : e_final = e')
@@ -218,10 +219,11 @@ End with_round_up_list.
     [PipelineCorrect] lemma to create side-conditions.  It assumes the
     goal is in exactly the form given in the conclusion of the
     [PipelineCorrect] lemma. *)
-Ltac refine_with_pipeline_correct :=
+
+Ltac refine_with_pipeline_correct opts :=
   lazymatch goal with
   | [ |- _ /\ ?castback ?fW = ?fZ ?arg ]
-    => let lem := open_constr:(@PipelineCorrect _ _ _ _ _ _ _ _ _ _ _ _ _) in
+    => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ _ _ _ _ _ _) in
        simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _);
        subst fW fZ
   end;
@@ -288,5 +290,6 @@ Ltac solve_side_conditions :=
 (** The [do_reflective_pipeline] tactic solves a goal of the form that
     is described at the top of this file, and is the public interface
     of this file. *)
-Ltac do_reflective_pipeline :=
-  refine_with_pipeline_correct; solve_side_conditions.
+Ltac do_reflective_pipeline opts :=
+  refine_with_pipeline_correct opts; solve_side_conditions.
+Notation default_PipelineOptions := default_PipelineOptions.