diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-03 18:30:27 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-03 18:30:27 -0400 |
| commit | a6cd4891cd8c73aff596f13a6762abf154ec7d4d (patch) | |
| tree | cf8ac236dbe9db0414c52216a07eb02b0e0fe4c2 /src/Compilers/ZExtended | |
| parent | 3cd7034675be89d1c42bc681d3144fe4cff6aac0 (diff) | |
Add Zsub to extended syntax
Diffstat (limited to 'src/Compilers/ZExtended')
| -rw-r--r-- | src/Compilers/ZExtended/Syntax.v | 2 | ||||
| -rw-r--r-- | src/Compilers/ZExtended/Syntax/Util.v | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/src/Compilers/ZExtended/Syntax.v b/src/Compilers/ZExtended/Syntax.v index 8b62af2c3..04f16c1fa 100644 --- a/src/Compilers/ZExtended/Syntax.v +++ b/src/Compilers/ZExtended/Syntax.v @@ -33,6 +33,7 @@ Inductive op : flat_type base_type -> flat_type base_type -> Set := | Zselect : op (tuple tZ 3) (tuple tZ 1) | Zmul : op (tuple tZ 2) (tuple tZ 1) | Zadd : op (tuple tZ 2) (tuple tZ 1) +| Zsub : op (tuple tZ 2) (tuple tZ 1) | Zopp : op (tuple tZ 1) (tuple tZ 1) | Zshiftr : op (tuple tZ 2) (tuple tZ 1) | Zshiftl : op (tuple tZ 2) (tuple tZ 1) @@ -65,6 +66,7 @@ Definition interp_op {s d} (opv : op s d) : interp_flat_type interp_base_type s | Zselect => curry3 Z.zselect | Zmul => curry2 Z.mul | Zadd => curry2 Z.add + | Zsub => curry2 Z.sub | Zopp => Z.opp | Zshiftr => curry2 Z.shiftr | Zshiftl => curry2 Z.shiftl diff --git a/src/Compilers/ZExtended/Syntax/Util.v b/src/Compilers/ZExtended/Syntax/Util.v index d0c7b42db..e62915107 100644 --- a/src/Compilers/ZExtended/Syntax/Util.v +++ b/src/Compilers/ZExtended/Syntax/Util.v @@ -23,6 +23,7 @@ Definition invert_Const s d (opc : op s d) : option (interp_flat_type interp_bas | Zselect | Zmul | Zadd + | Zsub | Zopp | Zshiftr | Zshiftl @@ -57,6 +58,7 @@ Definition unextend_op {s d} (opc : ZExtended.Syntax.op s d) | Zselect => Some (Z.Syntax.Zselect _ _ _ _) | Zmul => Some (Z.Syntax.Mul _ _ _) | Zadd => Some (Z.Syntax.Add _ _ _) + | Zsub => Some (Z.Syntax.Sub _ _ _) | Zopp => Some (Z.Syntax.Opp _ _) | Zshiftr => Some (Z.Syntax.Shr _ _ _) | Zshiftl => Some (Z.Syntax.Shl _ _ _) |