Add unextend_op

2 files changed, 73 insertions, 0 deletions

diff --git a/src/Compilers/ZExtended/Syntax.v b/src/Compilers/ZExtended/Syntax.v
index 5f6d5b3eb..0a40abb8b 100644
--- a/src/Compilers/ZExtended/Syntax.v
+++ b/src/Compilers/ZExtended/Syntax.v
@@ -26,6 +26,8 @@ Definition interp_base_type (v : base_type) : Set :=
 Inductive op : flat_type base_type -> flat_type base_type -> Set :=
 | AddGetCarry : op (tuple tZ 3) (tuple tZ 2)
 | MulSplitAtBitwidth : op (tuple tZ 3) (tuple tZ 2)
+| AddGetCarryZ (bitwidth : Z) : op (tuple tZ 2) (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)
 | Zadd    : op (tuple tZ 2) (tuple tZ 1)
@@ -54,6 +56,8 @@ Definition interp_op {s d} (opv : op s d) : interp_flat_type interp_base_type s
   := match opv with
      | AddGetCarry => curry3 Z.add_get_carry
      | MulSplitAtBitwidth => curry3 Z.mul_split_at_bitwidth
+     | AddGetCarryZ bitwidth => curry2 (Z.add_get_carry bitwidth)
+     | MulSplitAtBitwidthZ bitwidth => curry2 (Z.mul_split_at_bitwidth bitwidth)
      | 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
new file mode 100644
index 000000000..ffbf2e64d
--- /dev/null
+++ b/src/Compilers/ZExtended/Syntax/Util.v
@@ -0,0 +1,69 @@
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.ZExtended.Syntax.
+
+Definition unextend_base_type (t : ZExtended.Syntax.base_type) : Z.Syntax.base_type
+  := match t with
+     | TZ => Z.Syntax.TZ
+     | TBool => Z.Syntax.TZ
+     end.
+
+Definition invert_Const s d (opc : op s d) : option (interp_flat_type interp_base_type d)
+  := match opc with
+     | ConstZ v => Some v
+     | ConstBool v => Some v
+     | AddGetCarry
+     | MulSplitAtBitwidth
+     | AddGetCarryZ _
+     | MulSplitAtBitwidthZ _
+     | Zselect
+     | Zmul
+     | Zadd
+     | Zopp
+     | Zshiftr
+     | Zshiftl
+     | Zland
+     | Zlor
+     | Zmodulo
+     | Zdiv
+     | Zlog2
+     | Zpow
+     | Zones
+     | Zeqb
+     | BoolCase _
+       => None
+     end.
+
+Definition unextend_op {s d} (opc : ZExtended.Syntax.op s d)
+  : option (Z.Syntax.op (lift_flat_type unextend_base_type s)
+                        (lift_flat_type unextend_base_type d))
+  := match opc in 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 _ _ _ _ _) *)
+     | MulSplitAtBitwidth => None
+     | MulSplitAtBitwidthZ bitwidth
+       => Some (Z.Syntax.MulSplit bitwidth _ _ _ _)
+     | Zselect => Some (Z.Syntax.Zselect _ _ _ _)
+     | Zmul => Some (Z.Syntax.Mul _ _ _)
+     | Zadd => Some (Z.Syntax.Add _ _ _)
+     | Zopp => Some (Z.Syntax.Opp _ _)
+     | Zshiftr => Some (Z.Syntax.Shr _ _ _)
+     | Zshiftl => Some (Z.Syntax.Shl _ _ _)
+     | Zland => Some (Z.Syntax.Land _ _ _)
+     | Zlor => Some (Z.Syntax.Lor _ _ _)
+     | Zmodulo => None
+     | Zdiv => None
+     | Zlog2 => None
+     | Zpow => None
+     | Zones => None
+     | Zeqb => None
+     | ConstZ v => Some (OpConst v)
+     | ConstBool v => None
+     | BoolCase T => None
+     end.