diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-21 12:12:40 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-21 15:24:46 -0400 |
| commit | 5dd87014371a731db764ddd1ae599a3ce776c9c1 (patch) | |
| tree | 5e71169754cf6c8766b7248a2c37562f6515977b /src/Compilers | |
| parent | f883825abc2f6eea856ba88f0764795b4ed9b3e8 (diff) | |
Only use bool in freeze
This closes #186
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v index fd61fefb4..c2ce603f5 100644 --- a/src/Compilers/Z/Bounds/Pipeline.v +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -1,6 +1,10 @@ (** * Reflective Pipeline *) +Require Import Coq.Lists.List. Require Import Crypto.Compilers.Z.Bounds.Pipeline.Glue. Require Import Crypto.Compilers.Z.Bounds.Pipeline.ReflectiveTactics. +Import ListNotations. +Local Open Scope nat_scope. +Local Open Scope list_scope. (** This file combines the various PHOAS modules in tactics, culminating in a tactic [refine_reflectively], which solves a goal of the form << @@ -19,16 +23,23 @@ Ltac refine_reflectively_gen allowable_bit_widths opts := refine_to_reflective_glue allowable_bit_widths; do_reflective_pipeline opts. -Ltac refine_reflectively128_with opts := refine_reflectively_gen (1::128::256::nil)%nat%list opts. -Ltac refine_reflectively64_with opts := refine_reflectively_gen (1::64::128::nil)%nat%list opts. -Ltac refine_reflectively32_with opts := refine_reflectively_gen (1::32::64::nil)%nat%list opts. +Ltac refine_reflectively128_with opts := refine_reflectively_gen [128; 256] opts. +Ltac refine_reflectively64_with opts := refine_reflectively_gen [64; 128] opts. +Ltac refine_reflectively32_with opts := refine_reflectively_gen [32; 64] opts. +Ltac refine_reflectively128_with_bool_with opts := refine_reflectively_gen [1; 128; 256] opts. +Ltac refine_reflectively64_with_bool_with opts := refine_reflectively_gen [1; 64; 128] opts. +Ltac refine_reflectively32_with_bool_with opts := refine_reflectively_gen [1; 32; 64] 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. +Ltac refine_reflectively128_with_bool := refine_reflectively128_with_bool_with default_PipelineOptions. +Ltac refine_reflectively64_with_bool := refine_reflectively64_with_bool_with default_PipelineOptions. +Ltac refine_reflectively32_with_bool := refine_reflectively32_with_bool_with default_PipelineOptions. (** Convenience notations for options *) Definition anf := {| Pipeline.Definition.anf := true |}. (** The default *) +Ltac refine_reflectively_with_bool_with opts := refine_reflectively64_with_bool_with opts. Ltac refine_reflectively_with opts := refine_reflectively64_with opts. Ltac refine_reflectively := refine_reflectively_with default_PipelineOptions. |