diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v new file mode 100644 index 000000000..6c9cda840 --- /dev/null +++ b/src/Compilers/Z/Bounds/Pipeline.v @@ -0,0 +1,20 @@ +(** * Reflective Pipeline *) +Require Import Crypto.Compilers.Z.Bounds.Pipeline.Glue. +Require Import Crypto.Compilers.Z.Bounds.Pipeline.ReflectiveTactics. +(** This file combines the various PHOAS modules in tactics, + culminating in a tactic [refine_reflectively], which solves a goal of the form +<< +cast_back_flat_const (?x args) = f (cast_back_flat_const args) + /\ Bounds.is_bounded_by ?bounds (?x args) +>> +while instantiating [?x] and [?bounds] with nicely-reduced constants. + *) + +Module Export Exports. + Export Glue.Exports. + Export ReflectiveTactics.Exports. +End Exports. + +Ltac refine_reflectively := + refine_to_reflective_glue; + do_reflective_pipeline. |