GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-29 19:14:24 +03:00
Code Issues Projects Releases Wiki Activity

Add rewrite rules to simplify constraints due to generate.

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

Fixes #1291
This commit is contained in:
Iavor Diatchki 2021-09-27 11:15:43 -07:00
parent 15b3b98482
commit e86a94763d
1 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/Cryptol/TypeCheck/SimpType.hs
View File

@ -262,6 +262,12 @@ tMax x y
maxK (Nat 0) t = t maxK (Nat 0) t = t
maxK (Nat k) 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' | TCon (TF TCAdd) [a,b] <- t'
, Just n <- tIsNum a = if k <= n , Just n <- tIsNum a = if k <= n
then t then t
@ -283,6 +289,13 @@ tMax x y
tWidth :: Type -> Type tWidth :: Type -> Type
tWidth x tWidth x
| Just t <- tOp TCWidth (total (op1 nWidth)) [x] = t | 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 | otherwise = tf1 TCWidth x
tLenFromThenTo :: Type -> Type -> Type -> Type tLenFromThenTo :: Type -> Type -> Type -> Type