Add syntactic tuples

3 files changed, 52 insertions, 6 deletions

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 4c56ada4c..9282e703f 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -1,6 +1,7 @@
 (** * PHOAS Representation of Gallina *)
 Require Import Coq.Strings.String Coq.Classes.RelationClasses Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
@@ -27,6 +28,17 @@ Section language.
   Notation "A -> B" := (Arrow A B) : ctype_scope.
   Local Coercion Tbase : base_type_code >-> flat_type.
 
+  Fixpoint tuple' T n :=
+    match n with
+    | O => T
+    | S n' => (tuple' T n' * T)%ctype
+    end.
+  Definition tuple T n :=
+    match n with
+    | O => T (* default value; no empty tuple *)
+    | S n' => tuple' T n'
+    end.
+
   Section interp.
     Section type.
       Section hetero.
@@ -69,6 +81,21 @@ Section language.
         | Prod x y => prod (interp_flat_type x) (interp_flat_type y)
         end.
       Definition interp_type := interp_type_gen interp_flat_type.
+      Fixpoint flat_interp_tuple' {T n} : interp_flat_type (tuple' T n) -> Tuple.tuple' (interp_flat_type T) n
+        := match n return interp_flat_type (tuple' T n) -> Tuple.tuple' (interp_flat_type T) n with
+           | O => fun x => x
+           | S n' => fun xy => (@flat_interp_tuple' _ n' (fst xy), snd xy)
+           end.
+      Definition flat_interp_tuple {T n} : interp_flat_type (tuple T n) -> Tuple.tuple (interp_flat_type T) n
+        := match n return interp_flat_type (tuple T n) -> Tuple.tuple (interp_flat_type T) n with
+           | O => fun _ => tt
+           | S n' => @flat_interp_tuple' T n'
+           end.
+      Fixpoint flat_interp_untuple' {T n} : Tuple.tuple' (interp_flat_type T) n -> interp_flat_type (tuple' T n)
+        := match n return Tuple.tuple' (interp_flat_type T) n -> interp_flat_type (tuple' T n) with
+           | O => fun x => x
+           | S n' => fun xy => (@flat_interp_untuple' _ n' (fst xy), snd xy)
+           end.
       Section rel.
         Context (R : forall t, interp_base_type t -> interp_base_type t -> Prop).
         Fixpoint interp_flat_type_rel_pointwise (t : flat_type)
@@ -317,12 +344,28 @@ Section language.
     Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E.
   End expr_param.
 End language.
+Global Arguments tuple' {_}%type_scope _%ctype_scope _%nat_scope.
+Global Arguments tuple {_}%type_scope _%ctype_scope _%nat_scope.
 Global Arguments Prod {_}%type_scope (_ _)%ctype_scope.
 Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope.
 Global Arguments Tbase {_}%type_scope _%ctype_scope.
 
 Ltac admit_Wf := apply Wf_admitted.
 
+Scheme Equality for flat_type.
+Scheme Equality for type.
+
+Global Instance dec_eq_flat_type {base_type_code} `{DecidableRel (@eq base_type_code)}
+  : DecidableRel (@eq (flat_type base_type_code)).
+Proof.
+  repeat intro; hnf; decide equality; apply dec; auto.
+Defined.
+Global Instance dec_eq_type {base_type_code} `{DecidableRel (@eq base_type_code)}
+  : DecidableRel (@eq (type base_type_code)).
+Proof.
+  repeat intro; hnf; decide equality; apply dec; typeclasses eauto.
+Defined.
+
 Global Arguments Const {_ _ _ _ _} _.
 Global Arguments Var {_ _ _ _ _} _.
 Global Arguments SmartVarf {_ _ _ _ _} _.
@@ -337,6 +380,9 @@ Global Arguments LetIn {_ _ _ _ _} _ {_} _.
 Global Arguments Pair {_ _ _ _ _} _ {_} _.
 Global Arguments Return {_ _ _ _ _} _.
 Global Arguments Abs {_ _ _ _ _ _} _.
+Global Arguments flat_interp_tuple' {_ _ _ _} _.
+Global Arguments flat_interp_tuple {_ _ _ _} _.
+Global Arguments flat_interp_untuple' {_ _ _ _} _.
 Global Arguments interp_type_rel_pointwise2 {_ _ _} R {t} _ _.
 Global Arguments interp_type_gen_rel_pointwise2_hetero {_ _ _ _ _} Rsrc R {t} _ _.
 Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _.
diff --git a/src/Specific/FancyMachine256/Barrett.v b/src/Specific/FancyMachine256/Barrett.v
index fd880b440..f3258fe60 100644
--- a/src/Specific/FancyMachine256/Barrett.v
+++ b/src/Specific/FancyMachine256/Barrett.v
@@ -85,8 +85,8 @@ Section reflected.
   Context (m μ : Z)
           (props : fancy_machine.arithmetic ops).
 
-  Let result (v : tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple m μ (fst v) (snd v).
-  Let assembled_result (v : tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax m μ (fst v) (snd v).
+  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple m μ (fst v) (snd v).
+  Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax m μ (fst v) (snd v).
 
   Theorem sanity : result = expression ops m μ.
   Proof.
@@ -108,7 +108,7 @@ Section reflected.
             (H3 : b^(k - offset) <= m + 1)
             (H4 : 0 <= m < 2^(k + offset))
             (H5 : 0 <= b^(2 * k) / m < b^(k + offset))
-            (v : tuple fancy_machine.W 2)
+            (v : Tuple.tuple fancy_machine.W 2)
             (H6 : 0 <= decode v < b^(2 * k)).
     Theorem correctness : fancy_machine.decode (result v) = decode v mod m.
     Proof.
diff --git a/src/Specific/FancyMachine256/Montgomery.v b/src/Specific/FancyMachine256/Montgomery.v
index fcf14afe2..b6f2da64a 100644
--- a/src/Specific/FancyMachine256/Montgomery.v
+++ b/src/Specific/FancyMachine256/Montgomery.v
@@ -76,9 +76,9 @@ Section reflected.
   Context (modulus m' : Z)
           (props : fancy_machine.arithmetic ops).
 
-  Let result (v : tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple modulus m' (fst v) (snd v).
+  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple modulus m' (fst v) (snd v).
 
-  Let assembled_result (v : tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax modulus m' (fst v) (snd v).
+  Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax modulus m' (fst v) (snd v).
 
   Theorem sanity : result = expression ops modulus m'.
   Proof.
@@ -100,7 +100,7 @@ Section reflected.
             (H2 : 0 <= m' < 2^256)
             (H3 : 2^256 * R' ≡ 1)
             (H4 : modulus * m' ≡₂₅₆ -1)
-            (v : tuple fancy_machine.W 2)
+            (v : Tuple.tuple fancy_machine.W 2)
             (H5 : 0 <= decode v <= 2^256 * modulus).
     Theorem correctness
       : fancy_machine.decode (result v) = (decode v * R') mod modulus.