diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-04 19:55:29 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-04 19:55:29 -0400 |
| commit | 7048d5892bd6bf705900488a62975b72a5f6bd8f (patch) | |
| tree | fc758beac0b946dd371d209cb951853daf376e7c /src/Compilers | |
| parent | 34fe7947da904853bafd5328d0377c7fc23ed2ac (diff) | |
Add IdWithAlt to ZExtended
Diffstat (limited to 'src/Compilers')
| -rw-r--r-- | src/Compilers/ZExtended/Syntax.v | 2 | ||||
| -rw-r--r-- | src/Compilers/ZExtended/Syntax/Util.v | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/Compilers/ZExtended/Syntax.v b/src/Compilers/ZExtended/Syntax.v index 04f16c1fa..901de599f 100644 --- a/src/Compilers/ZExtended/Syntax.v +++ b/src/Compilers/ZExtended/Syntax.v @@ -30,6 +30,7 @@ Inductive op : flat_type base_type -> flat_type base_type -> Set := | 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) +| IdWithAlt {T} : op (tuple (Tbase T) 2) (tuple (Tbase T) 1) | Zselect : op (tuple tZ 3) (tuple tZ 1) | Zmul : op (tuple tZ 2) (tuple tZ 1) | Zadd : op (tuple tZ 2) (tuple tZ 1) @@ -63,6 +64,7 @@ Definition interp_op {s d} (opv : op s d) : interp_flat_type interp_base_type s | 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) + | IdWithAlt T => curry2 id_with_alt | Zselect => curry3 Z.zselect | Zmul => curry2 Z.mul | Zadd => curry2 Z.add diff --git a/src/Compilers/ZExtended/Syntax/Util.v b/src/Compilers/ZExtended/Syntax/Util.v index e62915107..6a552e129 100644 --- a/src/Compilers/ZExtended/Syntax/Util.v +++ b/src/Compilers/ZExtended/Syntax/Util.v @@ -20,6 +20,7 @@ Definition invert_Const s d (opc : op s d) : option (interp_flat_type interp_bas | AddWithGetCarryZ _ | SubWithGetBorrowZ _ | MulSplitAtBitwidthZ _ + | IdWithAlt _ | Zselect | Zmul | Zadd @@ -55,6 +56,8 @@ Definition unextend_op {s d} (opc : ZExtended.Syntax.op s d) | MulSplitAtBitwidth => None | MulSplitAtBitwidthZ bitwidth => Some (Z.Syntax.MulSplit bitwidth _ _ _ _) + | IdWithAlt _ + => Some (Z.Syntax.IdWithAlt _ _ _) | Zselect => Some (Z.Syntax.Zselect _ _ _ _) | Zmul => Some (Z.Syntax.Mul _ _ _) | Zadd => Some (Z.Syntax.Add _ _ _) |