aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/ZExtended
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-03 01:33:24 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-11-03 01:33:24 -0400
commit3b3903b4eb063eac4f6277a4e87d93d1fb9b0c81 (patch)
tree85f5a5899cec8515701adbf84c6ade896f55e352 /src/Compilers/ZExtended
parentf3934d9e5e30947a07f39f5d93a3935d1c870b2a (diff)
Fix missing cases in previous commit
Diffstat (limited to 'src/Compilers/ZExtended')
-rw-r--r--src/Compilers/ZExtended/Syntax/Util.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Compilers/ZExtended/Syntax/Util.v b/src/Compilers/ZExtended/Syntax/Util.v
index 24b53ad75..d0c7b42db 100644
--- a/src/Compilers/ZExtended/Syntax/Util.v
+++ b/src/Compilers/ZExtended/Syntax/Util.v
@@ -15,8 +15,10 @@ Definition invert_Const s d (opc : op s d) : option (interp_flat_type interp_bas
| ConstZ v => Some v
| ConstBool v => Some v
| AddWithGetCarry
+ | SubWithGetBorrow
| MulSplitAtBitwidth
| AddWithGetCarryZ _
+ | SubWithGetBorrowZ _
| MulSplitAtBitwidthZ _
| Zselect
| Zmul
@@ -46,6 +48,9 @@ Definition unextend_op {s d} (opc : ZExtended.Syntax.op s d)
| AddWithGetCarry => None
| AddWithGetCarryZ bitwidth
=> Some (Z.Syntax.AddWithGetCarry bitwidth _ _ _ _ _)
+ | SubWithGetBorrow => None
+ | SubWithGetBorrowZ bitwidth
+ => Some (Z.Syntax.SubWithGetBorrow bitwidth _ _ _ _ _)
| MulSplitAtBitwidth => None
| MulSplitAtBitwidthZ bitwidth
=> Some (Z.Syntax.MulSplit bitwidth _ _ _ _)