From 57ddc251461ed5806e6f2fd2c98a6555f18f58fe Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 17 May 2017 01:21:09 -0400 Subject: 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. --- src/Compilers/Z/Bounds/Pipeline.v | 16 ++++++++++------ src/Compilers/Z/Bounds/Pipeline/Definition.v | 19 +++++++++++++------ src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 13 ++++++++----- 3 files changed, 31 insertions(+), 17 deletions(-) (limited to 'src') 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. -- cgit v1.2.3