From 7048d5892bd6bf705900488a62975b72a5f6bd8f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 4 Nov 2017 19:55:29 -0400 Subject: Add IdWithAlt to ZExtended --- src/Compilers/ZExtended/Syntax.v | 2 ++ src/Compilers/ZExtended/Syntax/Util.v | 3 +++ 2 files changed, 5 insertions(+) (limited to 'src/Compilers') 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 _ _ _) -- cgit v1.2.3