Test binop simplifications

test/unit/test_binop.ml

@@ -5,90 +5,124 @@ open Value
 
 let ( = ) = Expr.equal
 
+let true_ = value True
+
+let false_ = value False
+
+let int x = value (Int x)
+
+let real x = value (Real x)
+
+let string x = value (Str x)
+
+let int32 x = value (Num (I32 x))
+
+let int64 x = value (Num (I64 x))
+
+let list x = value (List x)
+
 (* int *)
 let () =
-  let v i = value (Int i) in
-  assert (binop Ty_int Add (v 0) (v 42) = v 42);
-  assert (binop Ty_int Sub (v 0) (v 1) = v (-1));
-  assert (binop Ty_int Mul (v 2) (v 21) = v 42);
-  assert (binop Ty_int Div (v 84) (v 2) = v 42);
-  assert (binop Ty_int Rem (v 0) (v 1) = v 0);
-  assert (binop Ty_int Pow (v 2) (v 2) = v 4);
-  assert (binop Ty_int Min (v 2) (v 4) = v 2);
-  assert (binop Ty_int Max (v 2) (v 4) = v 4);
-  assert (binop Ty_int And (v 1) (v 0) = v 0);
-  assert (binop Ty_int Or (v 0) (v 1) = v 1);
-  assert (binop Ty_int Xor (v 1) (v 1) = v 0);
-  assert (binop Ty_int Shl (v 1) (v 2) = v 4);
-  assert (binop Ty_int ShrA (v 4) (v 2) = v 1);
-  assert (binop Ty_int ShrA (v (-4)) (v 2) = v (-1));
-  assert (binop Ty_int ShrL (v (-4)) (v 2) <> v (-1))
+  assert (binop Ty_int Add (int 0) (int 42) = int 42);
+  assert (binop Ty_int Sub (int 0) (int 1) = int (-1));
+  assert (binop Ty_int Mul (int 2) (int 21) = int 42);
+  assert (binop Ty_int Div (int 84) (int 2) = int 42);
+  assert (binop Ty_int Rem (int 0) (int 1) = int 0);
+  assert (binop Ty_int Pow (int 2) (int 2) = int 4);
+  assert (binop Ty_int Min (int 2) (int 4) = int 2);
+  assert (binop Ty_int Max (int 2) (int 4) = int 4);
+  assert (binop Ty_int And (int 1) (int 0) = int 0);
+  assert (binop Ty_int Or (int 0) (int 1) = int 1);
+  assert (binop Ty_int Xor (int 1) (int 1) = int 0);
+  assert (binop Ty_int Shl (int 1) (int 2) = int 4);
+  assert (binop Ty_int ShrA (int 4) (int 2) = int 1);
+  assert (binop Ty_int ShrA (int (-4)) (int 2) = int (-1));
+  assert (binop Ty_int ShrL (int (-4)) (int 2) <> int (-1))
 
 (* real *)
 let () =
-  let v i = value (Real i) in
-  assert (binop Ty_real Add (v 0.0) (v 42.0) = v 42.0);
-  assert (binop Ty_real Sub (v 0.0) (v 1.0) = v (-1.0));
-  assert (binop Ty_real Mul (v 2.0) (v 21.0) = v 42.0);
-  assert (binop Ty_real Div (v 84.0) (v 2.0) = v 42.0);
-  assert (binop Ty_real Rem (v 0.0) (v 1.0) = v 0.0);
-  assert (binop Ty_real Min (v 2.0) (v 4.0) = v 2.0);
-  assert (binop Ty_real Max (v 2.0) (v 4.0) = v 4.0)
+  assert (binop Ty_real Add (real 0.0) (real 42.0) = real 42.0);
+  assert (binop Ty_real Sub (real 0.0) (real 1.0) = real (-1.0));
+  assert (binop Ty_real Mul (real 2.0) (real 21.0) = real 42.0);
+  assert (binop Ty_real Div (real 84.0) (real 2.0) = real 42.0);
+  assert (binop Ty_real Rem (real 0.0) (real 1.0) = real 0.0);
+  assert (binop Ty_real Min (real 2.0) (real 4.0) = real 2.0);
+  assert (binop Ty_real Max (real 2.0) (real 4.0) = real 4.0)
 
 (* str *)
 let () =
-  let i i = value (Int i) in
-  let v s = value (Str s) in
-  assert (binop Ty_str At (v "abc") (i 0) = v "a");
-  assert (binop Ty_str String_prefix (v "ab") (v "abcd") = value True);
-  assert (binop Ty_str String_suffix (v "ab") (v "abcd") = value False);
-  assert (binop Ty_str String_contains (v "abcd") (v "bc") = value True)
+  assert (binop Ty_str At (string "abc") (int 0) = string "a");
+  assert (binop Ty_str String_prefix (string "ab") (string "abcd") = true_);
+  assert (binop Ty_str String_suffix (string "ab") (string "abcd") = false_);
+  assert (binop Ty_str String_contains (string "abcd") (string "bc") = true_)
 
 (* list *)
 let () =
-  let i i = value (Int i) in
-  let v l = value (List l) in
-  assert (binop Ty_list At (v [ Int 0; Int 1; Int 2 ]) (i 0) = i 0);
+  let clist = list [ Int 0; Int 1; Int 2 ] in
+  assert (binop Ty_list At clist (int 0) = int 0);
+  assert (binop Ty_list List_append_last (list [ Int 0; Int 1 ]) (int 2) = clist);
+  assert (binop Ty_list List_append (list [ Int 1; Int 2 ]) (int 0) = clist);
+  let slist2 = make (List [ int 0; int 1 ]) in
+  let slist3 = make (List [ int 0; int 1; int 2 ]) in
+  assert (binop Ty_list At slist3 (int 0) = int 0);
+  assert (binop Ty_list List_append_last slist2 (int 2) = slist3);
   assert (
-    binop Ty_list List_append_last (v [ Int 0; Int 1 ]) (i 2)
-    = v [ Int 0; Int 1; Int 2 ] );
-  assert (
-    binop Ty_list List_append (v [ Int 1; Int 2 ]) (i 0)
-    = v [ Int 0; Int 1; Int 2 ] )
+    binop Ty_list List_append (make (List [ int 1; int 2 ])) (int 0) = slist3 )
 
 (* i32 *)
 let () =
-  let v i = value (Num (I32 i)) in
   assert (
-    let ptr = ptr 8390670l (v 2l) in
-    binop (Ty_bitv 32) Rem ptr (v 1l) = v 0l );
-  assert (binop (Ty_bitv 32) Add (v 0l) (v 1l) = v 1l);
-  assert (binop (Ty_bitv 32) Sub (v 1l) (v 0l) = v 1l);
+    let ptr = ptr 8390670l (int32 2l) in
+    binop (Ty_bitv 32) Rem ptr (int32 1l) = int32 0l );
+  assert (binop (Ty_bitv 32) Add (int32 0l) (int32 1l) = int32 1l);
+  assert (binop (Ty_bitv 32) Sub (int32 1l) (int32 0l) = int32 1l);
   assert (
-    let x = binop (Ty_bitv 32) Mul (v 2l) (v 2l) in
-    binop (Ty_bitv 32) Div x (v 2l) = v 2l );
-  assert (binop (Ty_bitv 32) Rem (v 10l) (v 7l) = v 3l);
-  assert (binop (Ty_bitv 32) And (v 1l) (v 0l) = v 0l);
-  assert (binop (Ty_bitv 32) Or (v 0l) (v 1l) = v 1l);
-  assert (binop (Ty_bitv 32) Xor (v 1l) (v 1l) = v 0l);
-  assert (binop (Ty_bitv 32) Shl (v 1l) (v 2l) = v 4l);
-  assert (binop (Ty_bitv 32) ShrA (v 4l) (v 2l) = v 1l);
-  assert (binop (Ty_bitv 32) Rotl (v Int32.min_int) (v 2l) = v 2l);
-  assert (binop (Ty_bitv 32) Rotr (v 2l) (v 2l) = v Int32.min_int)
+    let x = binop (Ty_bitv 32) Mul (int32 2l) (int32 2l) in
+    binop (Ty_bitv 32) Div x (int32 2l) = int32 2l );
+  assert (binop (Ty_bitv 32) Rem (int32 10l) (int32 7l) = int32 3l);
+  assert (binop (Ty_bitv 32) And (int32 1l) (int32 0l) = int32 0l);
+  assert (binop (Ty_bitv 32) Or (int32 0l) (int32 1l) = int32 1l);
+  assert (binop (Ty_bitv 32) Xor (int32 1l) (int32 1l) = int32 0l);
+  assert (binop (Ty_bitv 32) Shl (int32 1l) (int32 2l) = int32 4l);
+  assert (binop (Ty_bitv 32) ShrA (int32 4l) (int32 2l) = int32 1l);
+  assert (binop (Ty_bitv 32) Rotl (int32 Int32.min_int) (int32 2l) = int32 2l);
+  assert (binop (Ty_bitv 32) Rotr (int32 2l) (int32 2l) = int32 Int32.min_int)
 
 (* i64 *)
 let () =
-  let v i = value (Num (I64 i)) in
-  assert (binop (Ty_bitv 64) Add (v 0L) (v 1L) = v 1L);
-  assert (binop (Ty_bitv 64) Sub (v 1L) (v 0L) = v 1L);
+  assert (binop (Ty_bitv 64) Add (int64 0L) (int64 1L) = int64 1L);
+  assert (binop (Ty_bitv 64) Sub (int64 1L) (int64 0L) = int64 1L);
+  assert (
+    let x = binop (Ty_bitv 64) Mul (int64 2L) (int64 2L) in
+    binop (Ty_bitv 64) Div x (int64 2L) = int64 2L );
+  assert (binop (Ty_bitv 64) Rem (int64 10L) (int64 7L) = int64 3L);
+  assert (binop (Ty_bitv 64) And (int64 1L) (int64 0L) = int64 0L);
+  assert (binop (Ty_bitv 64) Or (int64 0L) (int64 1L) = int64 1L);
+  assert (binop (Ty_bitv 64) Xor (int64 1L) (int64 1L) = int64 0L);
+  assert (binop (Ty_bitv 64) Shl (int64 1L) (int64 2L) = int64 4L);
+  assert (binop (Ty_bitv 64) ShrA (int64 4L) (int64 2L) = int64 1L);
+  assert (binop (Ty_bitv 64) Rotl (int64 Int64.min_int) (int64 2L) = int64 2L);
+  assert (binop (Ty_bitv 64) Rotr (int64 2L) (int64 2L) = int64 Int64.min_int)
+
+(* ptr *)
+let () =
+  let p0 = ptr 0l (int32 0l) in
+  let p1 = binop (Ty_bitv 32) Add p0 (int32 4l) in
+  assert (p1 = ptr 0l (int32 4l));
+  assert (binop (Ty_bitv 32) Sub p1 p0 = int32 4l);
+  assert (binop (Ty_bitv 32) Sub p1 (int32 4l) = p0);
+  assert (binop (Ty_bitv 32) Add (int32 4l) p0 = p1)
+
+(* Simplification *)
+let () =
+  let x = symbol @@ Symbol.make (Ty_bitv 32) "x" in
+  let zero = int32 0l in
+  let binop32 = binop (Ty_bitv 32) in
+  assert (binop32 And x zero = zero && binop32 And zero x = zero);
+  assert (binop32 Or zero x = x && binop32 Or x zero = x);
+  assert (
+    binop32 Sub (binop32 Sub x (int32 1l)) (int32 1l) = binop32 Sub x (int32 2l) );
+  assert (
+    binop32 Mul (binop32 Mul x (int32 2l)) (int32 2l) = binop32 Mul x (int32 4l) );
   assert (
-    let x = binop (Ty_bitv 64) Mul (v 2L) (v 2L) in
-    binop (Ty_bitv 64) Div x (v 2L) = v 2L );
-  assert (binop (Ty_bitv 64) Rem (v 10L) (v 7L) = v 3L);
-  assert (binop (Ty_bitv 64) And (v 1L) (v 0L) = v 0L);
-  assert (binop (Ty_bitv 64) Or (v 0L) (v 1L) = v 1L);
-  assert (binop (Ty_bitv 64) Xor (v 1L) (v 1L) = v 0L);
-  assert (binop (Ty_bitv 64) Shl (v 1L) (v 2L) = v 4L);
-  assert (binop (Ty_bitv 64) ShrA (v 4L) (v 2L) = v 1L);
-  assert (binop (Ty_bitv 64) Rotl (v Int64.min_int) (v 2L) = v 2L);
-  assert (binop (Ty_bitv 64) Rotr (v 2L) (v 2L) = v Int64.min_int)
+    binop32 Mul (int32 2l) (binop32 Mul x (int32 2l)) = binop32 Mul (int32 4l) x )