diff options
Diffstat (limited to 'src/Compilers/Z/Syntax.v')
| -rw-r--r-- | src/Compilers/Z/Syntax.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v index 7d0c84421..5bfa1168c 100644 --- a/src/Compilers/Z/Syntax.v +++ b/src/Compilers/Z/Syntax.v @@ -30,6 +30,8 @@ Inductive op : flat_type base_type -> flat_type base_type -> Type := | Zselect T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout) | AddWithCarry T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout) | AddWithGetCarry (bitwidth : Z) T1 T2 T3 Tout1 Tout2 : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout1 * Tbase Tout2) +| SubWithBorrow T1 T2 T3 Tout : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout) +| SubWithGetBorrow (bitwidth : Z) T1 T2 T3 Tout1 Tout2 : op (Tbase T1 * Tbase T2 * Tbase T3) (Tbase Tout1 * Tbase Tout2) . Definition interp_base_type (v : base_type) : Type := @@ -85,6 +87,8 @@ Definition Zinterp_op src dst (f : op src dst) | Zselect _ _ _ _ => fun ctf => let '(c, t, f) := eta3 ctf in Z.zselect c t f | AddWithCarry _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_carry c x y | AddWithGetCarry bitwidth _ _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.add_with_get_carry bitwidth c x y + | SubWithBorrow _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.sub_with_borrow c x y + | SubWithGetBorrow bitwidth _ _ _ _ _ => fun cxy => let '(c, x, y) := eta3 cxy in Z.sub_with_get_borrow bitwidth c x y end%Z. Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst |