diff options
| author |  Jade Philipoom <jadep@google.com> | 2018-02-19 11:38:52 +0100 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-02-23 13:06:33 -0500 |
| commit | 0c62a62f81f349dcafa37b38fabb5beac5432a89 (patch) | |
| tree | 84083d64b5347bc6a7e49cd7a931f47635953ef9 /src | |
| parent | 91a366c5572e53e5f51603d7604a015fb58a4284 (diff) | |
fixed inlining of opaque pairs as per Jason's recommendation
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 46 |
1 files changed, 11 insertions, 35 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 07e76bfcc..0761b653c 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -3124,7 +3124,7 @@ Module Compilers. => @interp_let_in _ B b (fun b => f (inr (a, b)))) - | inl e => f (inl e) + | inl e => partial.expr.reflect (expr_let y := e in partial.expr.reify (f (inl (Var y))))%expr end | type.type_primitive _ as t => fun (x : expr t + type.interp t) (f : expr t + type.interp t -> value var tC) @@ -5251,42 +5251,18 @@ Print Montgomery256.montred256. (Z.mul_split @@ (115792089237316195423570985008687907853269984665640564039457584007913129639936, fst @@ v, 115792089210356248768974548684794254293921932838497980611635986753331132366849)) in - expr_let v1 := Z.zselect @@ - (snd @@ - (Z.add_with_get_carry @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, - snd @@ - (Z.add_get_carry @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, fst @@ v, - fst @@ - (Z.mul_split @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, v0, - 115792089210356248762697446949407573530086143415290314195533631308867097853951)))), snd @@ v, - snd @@ - (Z.mul_split @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, v0, - 115792089210356248762697446949407573530086143415290314195533631308867097853951)))), 0, + expr_let v1 := Z.mul_split @@ + (115792089237316195423570985008687907853269984665640564039457584007913129639936, v0, 115792089210356248762697446949407573530086143415290314195533631308867097853951) in - expr_let v2 := fst @@ - (Z.sub_get_borrow @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, - fst @@ - (Z.add_with_get_carry @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, - snd @@ - (Z.add_get_carry @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, fst @@ v, - fst @@ - (Z.mul_split @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, v0, - 115792089210356248762697446949407573530086143415290314195533631308867097853951)))), snd @@ v, - snd @@ - (Z.mul_split @@ - (115792089237316195423570985008687907853269984665640564039457584007913129639936, v0, - 115792089210356248762697446949407573530086143415290314195533631308867097853951)))), v1)) in - Z.add_modulo @@ (v2, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951))%expr) + expr_let v2 := Z.add_get_carry @@ + (115792089237316195423570985008687907853269984665640564039457584007913129639936, fst @@ v, fst @@ v1) in + expr_let v3 := Z.add_with_get_carry @@ + (115792089237316195423570985008687907853269984665640564039457584007913129639936, snd @@ v2, snd @@ v, snd @@ v1) in + expr_let v4 := Z.zselect @@ (snd @@ v3, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951) in + expr_let v5 := fst @@ + (Z.sub_get_borrow @@ (115792089237316195423570985008687907853269984665640564039457584007913129639936, fst @@ v3, v4)) in + Z.add_modulo @@ (v5, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951))%expr) : Z * Z -> Z - *) (* with named constants *) |