Skip to content

Commit

Permalink
Fix incorrect overridding of bool notations
Browse files Browse the repository at this point in the history 
This notation system is fragile and kludgy.

This discovered from @davidben's
ff0fb38#r159793723
  • Loading branch information
@JasonGross
JasonGross committed Jan 5, 2018
1 parent 86a04b5 commit 72528f5
Showing 1 changed file with 13 additions and 13 deletions.
26 changes: 13 additions & 13 deletions src/Compilers/Z/CNotations.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,7 +265,7 @@ for opn, op, lvl in (('*', 'Mul', 40), ('+', 'Add', 50), ('-', 'Sub', 50)):
y = ('y' if not v2 else '(Var y)')
print('''Notation "%s'1&(' %s %s %s ')'%s" := (Op (%s %s) (Pair %s %s)) (at level %d, format "%s'1&(' %s %s %s ')'%s").''' %
(OPEN, 'x', opn, 'y', CLOSE,
op, ' '.join((TWord(0), TWord(_), TWord(_))), x, y, lvl,
op, ' '.join((TWord(_), TWord(_), TWord(0))), x, y, lvl,
OPEN, 'x', opn, 'y', CLOSE))
for opn, op, lvl in (('&', 'Land', 40), ('|', 'Lor', 45)):
for v1 in (False, True):
Expand Down Expand Up @@ -1312,18 +1312,18 @@ Notation "( x - y )" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x y)) (for
Notation "( x - y )" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair x (Var y))) (format "( x - y )") : expr_scope.
Notation "( x - y )" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) y)) (format "( x - y )") : expr_scope.
Notation "( x - y )" := (Op (Sub (TWord 8) (TWord 8) (TWord 8)) (Pair (Var x) (Var y))) (format "( x - y )") : expr_scope.
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord 0) (TWord _) (TWord _)) (Pair x y)) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord 0) (TWord _) (TWord _)) (Pair x (Var y))) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord 0) (TWord _) (TWord _)) (Pair (Var x) y)) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord 0) (TWord _) (TWord _)) (Pair (Var x) (Var y))) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord 0) (TWord _) (TWord _)) (Pair x y)) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord 0) (TWord _) (TWord _)) (Pair x (Var y))) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord 0) (TWord _) (TWord _)) (Pair (Var x) y)) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord 0) (TWord _) (TWord _)) (Pair (Var x) (Var y))) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord 0) (TWord _) (TWord _)) (Pair x y)) (at level 50, format "( '1&(' x - y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord 0) (TWord _) (TWord _)) (Pair x (Var y))) (at level 50, format "( '1&(' x - y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord 0) (TWord _) (TWord _)) (Pair (Var x) y)) (at level 50, format "( '1&(' x - y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord 0) (TWord _) (TWord _)) (Pair (Var x) (Var y))) (at level 50, format "( '1&(' x - y ')' )").
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x * y ')' )" := (Op (Mul (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 40, format "( '1&(' x * y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x + y ')' )" := (Op (Add (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50, format "( '1&(' x + y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x y)) (at level 50, format "( '1&(' x - y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair x (Var y))) (at level 50, format "( '1&(' x - y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) y)) (at level 50, format "( '1&(' x - y ')' )").
Notation "( '1&(' x - y ')' )" := (Op (Sub (TWord _) (TWord _) (TWord 0)) (Pair (Var x) (Var y))) (at level 50, format "( '1&(' x - y ')' )").
Notation "( x & y )" := (Op (Land _ _ _) (Pair x y)) (format "( x & y )") : expr_scope.
Notation "( x &ℤ y )" := (Op (Land _ _ TZ) (Pair x y)) (at level 40, format "( x &ℤ y )") : expr_scope.
Notation "( x & y )" := (Op (Land _ _ _) (Pair x (Var y))) (format "( x & y )") : expr_scope.
Expand Down

0 comments on commit 72528f5

Please sign in to comment.