From e86a94763db29f61f951329d62e785845a1b48e9 Mon Sep 17 00:00:00 2001
From: Iavor Diatchki <iavor.diatchki@gmail.com>
Date: Mon, 27 Sep 2021 11:15:43 -0700
Subject: [PATCH] Add rewrite rules to simplify constraints due to `generate`.

max 1 (a ^ n) ~> a ^ n    (for a >= 1)
width (2 ^ n - 1) ~> n

Fixes #1291
---
 src/Cryptol/TypeCheck/SimpType.hs | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/Cryptol/TypeCheck/SimpType.hs b/src/Cryptol/TypeCheck/SimpType.hs
index 0d42e200..c88bebf7 100644
--- a/src/Cryptol/TypeCheck/SimpType.hs
+++ b/src/Cryptol/TypeCheck/SimpType.hs
@@ -262,6 +262,12 @@ tMax x y
   maxK (Nat 0) t = t
   maxK (Nat k) t
 
+    -- max 1 t ~> t,   if t = a ^ b && a >= 1
+    | k == 1
+    , TCon (TF TCExp) [a,_] <- t'
+    , Just base <- tIsNat' a
+    , base >= Nat 1 = t
+
     | TCon (TF TCAdd) [a,b] <- t'
     , Just n <- tIsNum a = if k <= n
                              then t
@@ -283,6 +289,13 @@ tMax x y
 tWidth :: Type -> Type
 tWidth x
   | Just t <- tOp TCWidth (total (op1 nWidth)) [x] = t
+
+  -- width (2^n - 1) = n
+  | TCon (TF TCSub) [a,b] <- tNoUser x
+  , Just 1 <- tIsNum b
+  , TCon (TF TCExp) [p,q] <- tNoUser a
+  , Just 2 <- tIsNum p = q
+
   | otherwise = tf1 TCWidth x
 
 tLenFromThenTo :: Type -> Type -> Type -> Type