From 0cee03aaa12eca0d90e32baa9ba2985128633230 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 16 Apr 2020 03:38:30 -0700 Subject: [PATCH] [sledge] Simplify identity type conversions only at initial construction Summary: The types are constants and need not be re-checked for equality during normalization, etc. Reviewed By: jvillard Differential Revision: D20863526 fbshipit-source-id: 1adde5ee0 --- sledge/lib/term.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/sledge/lib/term.ml b/sledge/lib/term.ml index 51948c2f6..00f41fe6a 100644 --- a/sledge/lib/term.ml +++ b/sledge/lib/term.ml @@ -435,8 +435,7 @@ let simp_unsigned bits arg = | Integer {data} -> integer (Z.extract data 0 bits) | _ -> Ap1 (Unsigned {bits}, arg) -let simp_convert src dst arg = - if Typ.equivalent src dst then arg else Ap1 (Convert {src; dst}, arg) +let simp_convert src dst arg = Ap1 (Convert {src; dst}, arg) (* arithmetic *) @@ -999,7 +998,10 @@ let normN op xs = let signed bits term = norm1 (Signed {bits}) term let unsigned bits term = norm1 (Unsigned {bits}) term -let convert src ~to_:dst term = norm1 (Convert {src; dst}) term + +let convert src ~to_:dst arg = + if Typ.equivalent src dst then arg else norm1 (Convert {src; dst}) arg + let eq = norm2 Eq let dq = norm2 Dq let lt = norm2 Lt