From 3e4edb9a9b8cc15bdc02b9005e0b94561645b77b Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 7 Mar 2019 15:18:42 -0500 Subject: Get new Barrett proofs to generate Fancy code as before --- src/Rewriter.v | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'src/Rewriter.v') 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 *) -- cgit v1.2.3