Add Z.FoldTypes.{Min,Max}TypeUsed

2 files changed, 20 insertions, 0 deletions

diff --git a/src/Reflection/Z/FoldTypes.v b/src/Reflection/Z/FoldTypes.v
new file mode 100644
index 000000000..776f000f5
--- /dev/null
+++ b/src/Reflection/Z/FoldTypes.v
@@ -0,0 +1,17 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Reflection.Z.Syntax.Util.
+Require Import Crypto.Reflection.FoldTypes.
+
+Section min_or_max.
+  Context (f : base_type -> base_type -> base_type)
+          (init : base_type).
+
+  Definition TypeFold {t} (e : Expr base_type op t) : base_type
+    := TypeFold (fun t => t) f init e.
+End min_or_max.
+
+Definition MaxTypeUsed {t} (e : Expr base_type op t) : base_type
+  := TypeFold base_type_max (TWord 0) e.
+Definition MinTypeUsed {t} (e : Expr base_type op t) : base_type
+  := TypeFold base_type_min TZ e.
diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Reflection/Z/Syntax/Util.v
index 8e9102101..24fe5b331 100644
--- a/src/Reflection/Z/Syntax/Util.v
+++ b/src/Reflection/Z/Syntax/Util.v
@@ -35,8 +35,11 @@ Definition base_type_leb (v1 v2 : base_type) : bool
      end.
 
 Definition base_type_min := base_type_min base_type_leb.
+Definition base_type_max := base_type_max base_type_leb.
 Global Arguments base_type_min !_ !_ / .
+Global Arguments base_type_max !_ !_ / .
 Global Arguments TypeUtil.base_type_min _ _ _ /  _.
+Global Arguments TypeUtil.base_type_max _ _ _ /  _.
 
 Definition Castb {var} A A' (v : exprf base_type op (var:=var) (Tbase A))
   : exprf base_type op (var:=var) (Tbase A')