diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-28 16:02:00 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-07-03 19:28:55 -0400 |
| commit | 243fab24ba4f48d742ac6cb5998a0df0ef8c188d (patch) | |
| tree | 5e3585f11bc904d1d59e75f5c0e612e27b00f607 /src | |
| parent | 811bd8821d8e79b429353da5e4b5dfda337509c8 (diff) | |
Don't subst01 in square
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 26 |
1 files changed, 24 insertions, 2 deletions
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index c79c27b44..a0ecc885b 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -943,6 +943,28 @@ Module Import UnsaturatedSolinas. Hrop rv) (only parsing). + Notation BoundsPipelineToStrings_no_subst01 prefix name rop in_bounds out_bounds + := ((prefix ++ name)%string, + Pipeline.BoundsPipelineToStrings + true (* static *) prefix (prefix ++ name)%string + (*false*) false None + relax_zrange + rop%Expr in_bounds out_bounds). + + Notation BoundsPipeline_no_subst01_correct in_bounds out_bounds op + := (fun rv (rop : Expr (reify_type_of op)) Hrop + => @Pipeline.BoundsPipeline_correct_trans + (*false*) false None + relax_zrange + (relax_zrange_gen_good _) + _ + rop + in_bounds + out_bounds + op + Hrop rv) + (only parsing). + Notation BoundsPipelineToStrings_with_bytes_no_subst01 prefix name rop in_bounds out_bounds := ((prefix ++ name)%string, Pipeline.BoundsPipelineToStrings @@ -981,7 +1003,7 @@ Module Import UnsaturatedSolinas. (carry_mulmod (Qnum limbwidth) (Z.pos (Qden limbwidth)) s c n idxs). Definition srcarry_square prefix - := BoundsPipelineToStrings + := BoundsPipelineToStrings_no_subst01 prefix "carry_square" (carry_square_gen @ GallinaReify.Reify (Qnum limbwidth) @ GallinaReify.Reify (Z.pos (Qden limbwidth)) @ GallinaReify.Reify s @ GallinaReify.Reify c @ GallinaReify.Reify n @ GallinaReify.Reify idxs) @@ -989,7 +1011,7 @@ Module Import UnsaturatedSolinas. (Some tight_bounds). Definition rcarry_square_correct - := BoundsPipeline_correct + := BoundsPipeline_no_subst01_correct (Some loose_bounds, tt) (Some tight_bounds) (carry_squaremod (Qnum limbwidth) (Z.pos (Qden limbwidth)) s c n idxs). |