From 284e079d593483cadeeac3b222a91fa98fda9786 Mon Sep 17 00:00:00 2001 From: "Iavor S. Diatchki" Date: Wed, 17 Dec 2014 17:39:06 -0800 Subject: [PATCH] Don't rewrite `Width` to `Lg2`. Since we don't rewrite assumptions in the same way, we end up with silly goals like: x >= width y => x >= lg2 (y + 1) --- src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs index 40b8538b..3b9b3d70 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs @@ -654,7 +654,12 @@ crySimpExprStep expr = K (Nat 2) :^^ e -> Just e _ -> Nothing - Width x -> Just (Lg2 (x :+ one)) + -- Width x -> Just (Lg2 (x :+ one)) + Width x -> + case x of + K a -> Just (K (IN.nWidth a)) + K (Nat 2) :^^ e -> Just (one :+ e) + _ -> Nothing LenFromThen x y w -> case (x,y,w) of