diff options
| -rw-r--r-- | src/Compilers/ZExtended/Syntax.v | 8 | ||||
| -rw-r--r-- | src/Compilers/ZExtended/Syntax/Util.v | 10 |
2 files changed, 9 insertions, 9 deletions
diff --git a/src/Compilers/ZExtended/Syntax.v b/src/Compilers/ZExtended/Syntax.v index 0a40abb8b..38141c7c2 100644 --- a/src/Compilers/ZExtended/Syntax.v +++ b/src/Compilers/ZExtended/Syntax.v @@ -24,9 +24,9 @@ Definition interp_base_type (v : base_type) : Set := end. Inductive op : flat_type base_type -> flat_type base_type -> Set := -| AddGetCarry : op (tuple tZ 3) (tuple tZ 2) +| AddWithGetCarry : op (tuple tZ 4) (tuple tZ 2) | MulSplitAtBitwidth : op (tuple tZ 3) (tuple tZ 2) -| AddGetCarryZ (bitwidth : Z) : op (tuple tZ 2) (tuple tZ 2) +| AddWithGetCarryZ (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) @@ -54,9 +54,9 @@ 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 - | AddGetCarry => curry3 Z.add_get_carry + | AddWithGetCarry => curry4 Z.add_with_get_carry | MulSplitAtBitwidth => curry3 Z.mul_split_at_bitwidth - | AddGetCarryZ bitwidth => curry2 (Z.add_get_carry bitwidth) + | AddWithGetCarryZ bitwidth => curry3 (Z.add_with_get_carry bitwidth) | MulSplitAtBitwidthZ bitwidth => curry2 (Z.mul_split_at_bitwidth bitwidth) | Zselect => curry3 Z.zselect | Zmul => curry2 Z.mul diff --git a/src/Compilers/ZExtended/Syntax/Util.v b/src/Compilers/ZExtended/Syntax/Util.v index ffbf2e64d..24b53ad75 100644 --- a/src/Compilers/ZExtended/Syntax/Util.v +++ b/src/Compilers/ZExtended/Syntax/Util.v @@ -14,9 +14,9 @@ Definition invert_Const s d (opc : op s d) : option (interp_flat_type interp_bas := match opc with | ConstZ v => Some v | ConstBool v => Some v - | AddGetCarry + | AddWithGetCarry | MulSplitAtBitwidth - | AddGetCarryZ _ + | AddWithGetCarryZ _ | MulSplitAtBitwidthZ _ | Zselect | Zmul @@ -43,9 +43,9 @@ Definition unextend_op {s d} (opc : ZExtended.Syntax.op s d) return option (Z.Syntax.op (lift_flat_type unextend_base_type s) (lift_flat_type unextend_base_type d)) with - | AddGetCarry => None - | AddGetCarryZ bitwidth - => None (* XXX FIXME Some (Z.Syntax.AddGetCarry bitwidth _ _ _ _ _) *) + | AddWithGetCarry => None + | AddWithGetCarryZ bitwidth + => Some (Z.Syntax.AddWithGetCarry bitwidth _ _ _ _ _) | MulSplitAtBitwidth => None | MulSplitAtBitwidthZ bitwidth => Some (Z.Syntax.MulSplit bitwidth _ _ _ _) |