1 files changed, 58 insertions, 0 deletions
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.