Skip to content

Commit

Permalink
Merge pull request #1293 from GaloisInc/T1291
Browse files Browse the repository at this point in the history
Add rewrite rules to simplify constraints due to `generate`.
  • Loading branch information
yav authored Sep 27, 2021
2 parents 15b3b98 + e86a947 commit 66e054f
Showing 1 changed file with 13 additions and 0 deletions.
13 changes: 13 additions & 0 deletions src/Cryptol/TypeCheck/SimpType.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit 66e054f

Please sign in to comment.