Add a version of exprf that lives in Set

3 files changed, 256 insertions, 0 deletions

diff --git a/src/Compilers/InSet/Syntax.v b/src/Compilers/InSet/Syntax.v
new file mode 100644
index 000000000..4a3bb7a46
--- /dev/null
+++ b/src/Compilers/InSet/Syntax.v
@@ -0,0 +1,84 @@
+(** * PHOAS Representation of Gallina, in [Set] *)
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Compilers.Syntax.
+
+(** Universes are annoying.  See, e.g.,
+    [bug#5996](https://github.com/coq/coq/issues/5996), where using
+    [pattern] and [constr:(...)] to replace [Set] with [Type] breaks
+    things.  Because we need to get reflective syntax by patterning [Z
+    : Set], we make a version of [exprf] in [Set].  We build the
+    minimial infrastructure needed to get this sort of expression into
+    the [Type]-based one. *)
+
+Delimit Scope set_expr_scope with set_expr.
+Local Open Scope set_expr_scope.
+Section language.
+  Context (base_type_code : Set).
+
+  Local Notation flat_type := (flat_type base_type_code).
+
+  Let Tbase' := @Tbase base_type_code.
+  Local Coercion Tbase' : base_type_code >-> flat_type.
+
+  Section interp.
+    Context (interp_base_type : base_type_code -> Set).
+    Fixpoint interp_flat_type (t : flat_type) :=
+      match t with
+      | Tbase t => interp_base_type t
+      | Unit => unit
+      | Prod x y => prod (interp_flat_type x) (interp_flat_type y)
+      end.
+  End interp.
+
+  Section expr_param.
+    Context (interp_base_type : base_type_code -> Set).
+    Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Set).
+    Local Notation interp_flat_type_gen := interp_flat_type.
+    Local Notation interp_flat_type := (interp_flat_type interp_base_type).
+    Section expr.
+      Context {var : base_type_code -> Set}.
+
+      Inductive exprf : flat_type -> Set :=
+      | TT : exprf Unit
+      | Var {t} (v : var t) : exprf t
+      | Op {t1 tR} (opc : op t1 tR) (args : exprf t1) : exprf tR
+      | LetIn {tx} (ex : exprf tx) {tC} (eC : interp_flat_type_gen var tx -> exprf tC) : exprf tC
+      | Pair {tx} (ex : exprf tx) {ty} (ey : exprf ty) : exprf (Prod tx ty).
+      Bind Scope set_expr_scope with exprf.
+    End expr.
+
+    Section interp.
+      Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
+
+      Definition interpf_step
+                 (interpf : forall {t} (e : @exprf interp_flat_type t), interp_flat_type t)
+                 {t} (e : @exprf interp_flat_type t) : interp_flat_type t
+        := match e in exprf t return interp_flat_type t with
+           | TT => tt
+           | Var _ x => x
+           | Op _ _ op args => @interp_op _ _ op (@interpf _ args)
+           | LetIn _ ex _ eC => dlet x := @interpf _ ex in @interpf _ (eC x)
+           | Pair _ ex _ ey => (@interpf _ ex, @interpf _ ey)
+           end.
+
+      Fixpoint interpf {t} e
+        := @interpf_step (@interpf) t e.
+    End interp.
+  End expr_param.
+End language.
+Global Arguments Var {_ _ _ _} _.
+Global Arguments TT {_ _ _}.
+Global Arguments Op {_ _ _ _ _} _ _.
+Global Arguments LetIn {_ _ _ _} _ {_} _.
+Global Arguments Pair {_ _ _ _} _ {_} _.
+Global Arguments Abs {_ _ _ _ _} _.
+Global Arguments interp_flat_type {_} _ _.
+Global Arguments interpf {_ _ _} interp_op {t} _.
+
+Module Export Notations.
+  Notation "'slet' x .. y := A 'in' b" := (LetIn A%set_expr (fun x => .. (fun y => b%set_expr) .. )) : set_expr_scope.
+  Notation "( x , y , .. , z )" := (Pair .. (Pair x%set_expr y%set_expr) .. z%set_expr) : set_expr_scope.
+  Notation "( )" := TT : set_expr_scope.
+  Notation "()" := TT : set_expr_scope.
+End Notations.
diff --git a/src/Compilers/InSet/Typeify.v b/src/Compilers/InSet/Typeify.v
new file mode 100644
index 000000000..d2fbad987
--- /dev/null
+++ b/src/Compilers/InSet/Typeify.v
@@ -0,0 +1,58 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InSet.Syntax.
+
+Section language.
+  Context {base_type_code : Set}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Set}
+          {var : base_type_code -> Set}.
+
+  Fixpoint typeify_interp_flat_type {t}
+    : InSet.Syntax.interp_flat_type var t -> Compilers.Syntax.interp_flat_type var t
+    := match t with
+       | Tbase T => fun v => v
+       | Unit => fun v => v
+       | Prod A B => fun ab : InSet.Syntax.interp_flat_type _ A * InSet.Syntax.interp_flat_type _ B
+                     => (@typeify_interp_flat_type _ (fst ab),
+                         @typeify_interp_flat_type _ (snd ab))
+       end.
+  Fixpoint untypeify_interp_flat_type {t}
+    : Compilers.Syntax.interp_flat_type var t -> InSet.Syntax.interp_flat_type var t
+    := match t with
+       | Tbase T => fun v => v
+       | Unit => fun v => v
+       | Prod A B => fun ab : Compilers.Syntax.interp_flat_type _ A * Compilers.Syntax.interp_flat_type _ B
+                     => (@untypeify_interp_flat_type _ (fst ab),
+                         @untypeify_interp_flat_type _ (snd ab))
+       end.
+
+  Fixpoint typeify {t} (e : @InSet.Syntax.exprf base_type_code op var t)
+    : @Compilers.Syntax.exprf base_type_code op var t
+    := match e with
+       | TT => Compilers.Syntax.TT
+       | Var t v => Compilers.Syntax.Var v
+       | Op t1 tR opc args => Compilers.Syntax.Op opc (@typeify _ args)
+       | LetIn tx ex tC eC
+         => Compilers.Syntax.LetIn
+              (@typeify _ ex)
+              (fun x => @typeify _ (eC (untypeify_interp_flat_type x)))
+       | Pair tx ex ty ey => Compilers.Syntax.Pair
+                               (@typeify _ ex)
+                               (@typeify _ ey)
+       end.
+
+  Fixpoint untypeify {t} (e : @Compilers.Syntax.exprf base_type_code op var t)
+    : @InSet.Syntax.exprf base_type_code op var t
+    := match e with
+       | Compilers.Syntax.TT => TT
+       | Compilers.Syntax.Var t v => Var v
+       | Compilers.Syntax.Op t1 tR opc args => Op opc (@untypeify _ args)
+       | Compilers.Syntax.LetIn tx ex tC eC
+         => LetIn
+              (@untypeify _ ex)
+              (fun x => @untypeify _ (eC (typeify_interp_flat_type x)))
+       | Compilers.Syntax.Pair tx ex ty ey
+         => Pair
+              (@untypeify _ ex)
+              (@untypeify _ ey)
+       end.
+End language.
diff --git a/src/Compilers/InSet/TypeifyInterp.v b/src/Compilers/InSet/TypeifyInterp.v
new file mode 100644
index 000000000..77790eec8
--- /dev/null
+++ b/src/Compilers/InSet/TypeifyInterp.v
@@ -0,0 +1,114 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InSet.Syntax.
+Require Import Crypto.Compilers.InSet.Typeify.
+
+
+Local Ltac t :=
+  repeat first [ reflexivity
+               | progress simpl in *
+               | apply (f_equal2 (@pair _ _))
+               | solve [ auto ]
+               | progress cbv [LetIn.Let_In]
+               | progress autorewrite with core
+               | progress intros
+               | match goal with
+                 | [ v : _ * _ |- _ ] => destruct v
+                 | [ H : _ |- _ ] => rewrite H
+                 end ].
+
+Section language.
+  Context {base_type_code : Set}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Set}
+          {interp_base_type : base_type_code -> Set}.
+
+  Lemma typeify_untypeify_interp_flat_type {t} v
+    : @typeify_interp_flat_type base_type_code interp_base_type t (untypeify_interp_flat_type v) = v.
+  Proof using Type. induction t; t. Qed.
+  Lemma untypeify_typeify_interp_flat_type {t} v
+    : @untypeify_interp_flat_type base_type_code interp_base_type t (typeify_interp_flat_type v) = v.
+  Proof using Type. induction t; t. Qed.
+  Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type.
+
+  Section gen.
+    Context {interp_op : forall s d, op s d -> Compilers.Syntax.interp_flat_type interp_base_type s -> Compilers.Syntax.interp_flat_type interp_base_type d}
+            {interp_op' : forall s d, op s d -> InSet.Syntax.interp_flat_type interp_base_type s -> InSet.Syntax.interp_flat_type interp_base_type d}
+            (untypeify_interp_op
+             : forall s d opc args,
+                untypeify_interp_flat_type (interp_op s d opc args)
+                = interp_op' s d opc (untypeify_interp_flat_type args))
+            (typeify_interp_op
+             : forall s d opc args,
+                typeify_interp_flat_type (interp_op' s d opc args)
+                = interp_op s d opc (typeify_interp_flat_type args)).
+
+    Local Notation interpf := (Compilers.Syntax.interpf interp_op).
+    Local Notation interpf' := (InSet.Syntax.interpf interp_op').
+    Local Notation typeify := (typeify (var:=interp_base_type)).
+
+    Lemma interpf_typeify {t} e
+      : interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e).
+    Proof using typeify_interp_op. induction e; t. Qed.
+    Lemma interpf_untypeify {t} e
+      : interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e).
+    Proof using untypeify_interp_op. induction e; t. Qed.
+
+    Lemma interpf_typeify_untypeify {t} e
+      : interpf (typeify (untypeify (t:=t) e)) = interpf e.
+    Proof using Type. induction e; t. Qed.
+    Lemma interpf_untypeify_typeify {t} e
+      : interpf' (untypeify (t:=t) (typeify e)) = interpf' e.
+    Proof using Type. induction e; t. Qed.
+  End gen.
+End language.
+
+Module Compilers.
+  Import Compilers.Syntax.
+  Section language.
+    Context {base_type_code : Set}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Set}
+            {interp_base_type : base_type_code -> Set}
+            {interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}.
+
+    Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type.
+
+    Local Notation interp_op' :=
+      (fun s d opc args => untypeify_interp_flat_type (interp_op s d opc (typeify_interp_flat_type args))).
+
+    Local Notation interpf := (Compilers.Syntax.interpf interp_op).
+    Local Notation interpf' := (InSet.Syntax.interpf interp_op').
+    Local Notation typeify := (typeify (var:=interp_base_type)).
+
+    Lemma interpf_typeify {t} e
+      : interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e).
+    Proof using Type. apply interpf_typeify; t. Qed.
+    Lemma interpf_untypeify {t} e
+      : interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e).
+    Proof using Type. apply interpf_untypeify; t. Qed.
+  End language.
+End Compilers.
+
+Module InSet.
+  Import InSet.Syntax.
+  Section language.
+    Context {base_type_code : Set}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Set}
+            {interp_base_type : base_type_code -> Set}
+            {interp_op' : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}.
+
+    Hint Rewrite @typeify_untypeify_interp_flat_type @untypeify_typeify_interp_flat_type.
+
+    Local Notation interp_op :=
+      (fun s d opc args => typeify_interp_flat_type (interp_op' s d opc (untypeify_interp_flat_type args))).
+
+    Local Notation interpf := (Compilers.Syntax.interpf interp_op).
+    Local Notation interpf' := (InSet.Syntax.interpf interp_op').
+    Local Notation typeify := (typeify (var:=interp_base_type)).
+
+    Lemma interpf_typeify {t} e
+      : interpf (typeify e) = typeify_interp_flat_type (t:=t) (interpf' e).
+    Proof using Type. apply interpf_typeify; t. Qed.
+    Lemma interpf_untypeify {t} e
+      : interpf' (untypeify e) = untypeify_interp_flat_type (t:=t) (interpf e).
+    Proof using Type. apply interpf_untypeify; t. Qed.
+  End language.
+End InSet.