diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 17:48:41 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-17 17:16:47 -0400 |
| commit | b9b47568c04dd1c1e06e3922faae82d83461fe32 (patch) | |
| tree | 72fd50274931097ae59ad36f13168b8772ec89f9 /src | |
| parent | be5f86b5483d2e00ec9002b8db00a1ff8ecb9cfe (diff) | |
Zselect notation
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Z/CNotations.v | 168 |
1 files changed, 168 insertions, 0 deletions
diff --git a/src/Compilers/Z/CNotations.v b/src/Compilers/Z/CNotations.v index 80d1e17c9..8769fcf97 100644 --- a/src/Compilers/Z/CNotations.v +++ b/src/Compilers/Z/CNotations.v @@ -136,6 +136,22 @@ for opn, op, lvl in (('>>', 'Shr', 30),): % (types[lgwordsz], opn, op, lgwordsz, lhs, rhs, lvl)) print('Notation "x %s y" := (Op (%s (TWord %d) (TWord _) (TWord %d)) (Pair %s %s)).' % (opn, op, lgwordsz, lgwordsz, lhs, rhs)) +for v0 in (False, True): + for v1 in (False, True): + for v2 in (False, True): + tes = ('v' if not v0 else '(Var v)') + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair %s %s) %s)).' % (tes, lhs, rhs)) +for lgwordsz in range(0, len(types)): + for v0 in (False, True): + for v1 in (False, True): + for v2 in (False, True): + tes = ('v' if not v0 else '(Var v)') + lhs = ('x' if not v1 else '(Var x)') + rhs = ('y' if not v2 else '(Var y)') + print('Notation "\'(%s)\' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord %d)) (Pair (Pair %s %s) %s)) (at level 40, x at level 10, y at level 10).' % (types[lgwordsz], lgwordsz, tes, lhs, rhs)) + print('Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord %d) (TWord %d) (TWord %d)) (Pair (Pair %s %s) %s)).' % (lgwordsz, lgwordsz, lgwordsz, tes, lhs, rhs)) print('Notation Return x := (Var x).') print('Notation C_like := (Expr base_type op _).') >> *) @@ -1326,5 +1342,157 @@ Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) ( Notation "x >> y" := (Op (Shr (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) y)). Notation "'(uint256_t)' ( x >> y )" := (Op (Shr (TWord _) (TWord _) (TWord 8)) (Pair (Var x) (Var y))) (at level 30). Notation "x >> y" := (Op (Shr (TWord 8) (TWord _) (TWord 8)) (Pair (Var x) (Var y))). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v x) y)). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v x) (Var y))). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) y)). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair v (Var x)) (Var y))). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) y)). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) x) (Var y))). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) y)). +Notation "v == 0 ? x : y" := (Op (Zselect _ _ _ _) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) y)). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v x) (Var y))). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) y)). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) y)). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(bool)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 0) (TWord 0) (TWord 0)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v x) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 1) (TWord 1) (TWord 1)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v x) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 2) (TWord 2) (TWord 2)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v x) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint8_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 3) (TWord 3) (TWord 3)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) y)). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v x) (Var y))). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) y)). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) y)). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint16_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 4) (TWord 4) (TWord 4)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) y)). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v x) (Var y))). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) y)). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) y)). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint32_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 5) (TWord 5) (TWord 5)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) y)). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v x) (Var y))). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) y)). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) y)). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint64_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 6) (TWord 6) (TWord 6)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) y)). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v x) (Var y))). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) y)). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) y)). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint128_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 7) (TWord 7) (TWord 7)) (Pair (Pair (Var v) (Var x)) (Var y))). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) y)). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v x) (Var y))). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) y)). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair v (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair v (Var x)) (Var y))). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) y)). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) x) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) x) (Var y))). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) y)). +Notation "'(uint256_t)' ( v == 0 ? x : y )" := (Op (Zselect _ (TWord _) (TWord _) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))) (at level 40, x at level 10, y at level 10). +Notation "v == 0 ? x : y" := (Op (Zselect _ (TWord 8) (TWord 8) (TWord 8)) (Pair (Pair (Var v) (Var x)) (Var y))). Notation Return x := (Var x). Notation C_like := (Expr base_type op _). |