rename-everything

1 files changed, 35 insertions, 0 deletions

diff --git a/src/Compilers/TypeUtil.v b/src/Compilers/TypeUtil.v
new file mode 100644
index 000000000..050374562
--- /dev/null
+++ b/src/Compilers/TypeUtil.v
@@ -0,0 +1,35 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope expr_scope.
+
+Section language.
+  Context {base_type_code : Type}
+          (base_type_beq : base_type_code -> base_type_code -> bool)
+          (base_type_leb : base_type_code -> base_type_code -> bool).
+  Local Infix "<=?" := base_type_leb : expr_scope.
+  Local Infix "=?" := base_type_beq : expr_scope.
+
+  Definition base_type_min (a b : base_type_code) : base_type_code
+    := if a <=? b then a else b.
+  Definition base_type_max (a b : base_type_code) : base_type_code
+    := if a <=? b then b else a.
+  Section gen.
+    Context (join : base_type_code -> base_type_code -> base_type_code).
+    Fixpoint flat_type_join {t : flat_type base_type_code}
+      : interp_flat_type (fun _ => base_type_code) t -> option base_type_code
+      := match t with
+         | Tbase _ => fun v => Some v
+         | Unit => fun _ => None
+         | Prod A B
+           => fun v => match @flat_type_join A (fst v), @flat_type_join B (snd v) with
+                       | Some a, Some b => Some (join a b)
+                       | Some a, None => Some a
+                       | None, Some b => Some b
+                       | None, None => None
+                       end
+         end.
+  End gen.
+  Definition flat_type_min {t} := @flat_type_join base_type_min t.
+  Definition flat_type_max {t} := @flat_type_join base_type_max t.
+End language.