diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-03 01:31:52 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-03 01:31:52 -0400 |
| commit | f3934d9e5e30947a07f39f5d93a3935d1c870b2a (patch) | |
| tree | 0ee92bb55d590cde0b9cad0dcc4c6c334e66dd91 /src/Compilers | |
| parent | 5abe840c27713771665edd0a3beb040fccfbf041 (diff) | |
Add SubWithGetBorrow with ZExtended
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/ZExtended/Syntax.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Compilers/ZExtended/Syntax.v b/src/Compilers/ZExtended/Syntax.v index 38141c7c2..8b62af2c3 100644 --- a/src/Compilers/ZExtended/Syntax.v +++ b/src/Compilers/ZExtended/Syntax.v @@ -25,8 +25,10 @@ Definition interp_base_type (v : base_type) : Set := Inductive op : flat_type base_type -> flat_type base_type -> Set := | AddWithGetCarry : op (tuple tZ 4) (tuple tZ 2) +| SubWithGetBorrow : op (tuple tZ 4) (tuple tZ 2) | MulSplitAtBitwidth : op (tuple tZ 3) (tuple tZ 2) | AddWithGetCarryZ (bitwidth : Z) : op (tuple tZ 3) (tuple tZ 2) +| SubWithGetBorrowZ (bitwidth : Z) : op (tuple tZ 3) (tuple tZ 2) | MulSplitAtBitwidthZ (bitwidth : Z) : op (tuple tZ 2) (tuple tZ 2) | Zselect : op (tuple tZ 3) (tuple tZ 1) | Zmul : op (tuple tZ 2) (tuple tZ 1) @@ -55,8 +57,10 @@ Definition Const {t} : interp_base_type t -> op Unit (Tbase t) Definition interp_op {s d} (opv : op s d) : interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d := match opv with | AddWithGetCarry => curry4 Z.add_with_get_carry + | SubWithGetBorrow => curry4 Z.sub_with_get_borrow | MulSplitAtBitwidth => curry3 Z.mul_split_at_bitwidth | AddWithGetCarryZ bitwidth => curry3 (Z.add_with_get_carry bitwidth) + | SubWithGetBorrowZ bitwidth => curry3 (Z.sub_with_get_borrow bitwidth) | MulSplitAtBitwidthZ bitwidth => curry2 (Z.mul_split_at_bitwidth bitwidth) | Zselect => curry3 Z.zselect | Zmul => curry2 Z.mul |