diff options
| author |  jadep <jadep@mit.edu> | 2019-03-07 15:18:42 -0500 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-03-25 06:13:45 -0400 |
| commit | 3e4edb9a9b8cc15bdc02b9005e0b94561645b77b (patch) | |
| tree | 765489dd5ce02b3baf141190b1f52e3eb2ffb1fb /src/Rewriter.v | |
| parent | bbabd295594448f12161075c5d19dd369ed04a53 (diff) | |
Get new Barrett proofs to generate Fancy code as before
Diffstat (limited to 'src/Rewriter.v')
| -rw-r--r-- | src/Rewriter.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 1aefc35e8..01d7614e3 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -2437,6 +2437,26 @@ Module Compilers. ; (forall c x, Z.abs c <= Z.abs max_const_val -> 'c * x = x * 'c) + + (* transform +- to + *) + ; (forall s y x, + Z.add_get_carry_full s x (- y) + = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) + ; (forall s y x, + Z.add_get_carry_full s (- y) x + = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) + ; (forall s y x, + Z.add_with_get_carry_full s 0 x (- y) + = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) + ; (forall s y x, + Z.add_with_get_carry_full s 0 (- y) x + = dlet vb := Z.sub_get_borrow_full s x y in (fst vb, - snd vb)) + ; (forall s c y x, + Z.add_with_get_carry_full s (- c) (- y) x + = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb)) + ; (forall s c y x, + Z.add_with_get_carry_full s (- c) x (- y) + = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb)) ] ; reify [ (* [do_again], so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *) |