From 51c7e2682851dede7caab38c897e0499892e1451 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 10 Jun 2020 07:04:52 -0700 Subject: [PATCH] [sledge] Test: Move tests for (un)signed ints from Exp_test to Term_test Summary: The functionality being tested is in Term. Reviewed By: jvillard Differential Revision: D21720990 fbshipit-source-id: 24f5a06b4 --- sledge/src/exp_test.ml | 52 ----------------------------------------- sledge/src/exp_test.mli | 6 ----- sledge/src/term_test.ml | 41 ++++++++++++++++++++++++++++++++ 3 files changed, 41 insertions(+), 58 deletions(-) delete mode 100644 sledge/src/exp_test.ml delete mode 100644 sledge/src/exp_test.mli diff --git a/sledge/src/exp_test.ml b/sledge/src/exp_test.ml deleted file mode 100644 index 7a4958e0c..000000000 --- a/sledge/src/exp_test.ml +++ /dev/null @@ -1,52 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) - -let%test_module _ = - ( module struct - let () = Trace.init ~margin:68 () - - (* let () = Trace.init ~margin:68 ~config:Trace.all () *) - - open Exp - - let pp e = - Format.printf "@\n{desc= %a; term= %a}@." pp e Term.pp (Term.of_exp e) - - let ( ! ) i = integer Typ.siz (Z.of_int i) - - let%expect_test _ = - pp (signed 1 !1 ~to_:Typ.bool) ; - [%expect {| {desc= ((i1)(s1) 1); term= -1} |}] - - let%expect_test _ = - pp (unsigned 1 !(-1) ~to_:Typ.byt) ; - [%expect {| {desc= ((i8)(u1) -1); term= 1} |}] - - let%expect_test _ = - pp (signed 8 !(-1) ~to_:Typ.int) ; - [%expect {| {desc= ((i32)(s8) -1); term= -1} |}] - - let%expect_test _ = - pp (unsigned 8 !(-1) ~to_:Typ.int) ; - [%expect {| {desc= ((i32)(u8) -1); term= 255} |}] - - let%expect_test _ = - pp (signed 8 !255 ~to_:Typ.byt) ; - [%expect {| {desc= ((i8)(s8) 255); term= -1} |}] - - let%expect_test _ = - pp (signed 7 !255 ~to_:Typ.byt) ; - [%expect {| {desc= ((i8)(s7) 255); term= -1} |}] - - let%expect_test _ = - pp (unsigned 7 !255 ~to_:Typ.byt) ; - [%expect {| {desc= ((i8)(u7) 255); term= 127} |}] - - let%expect_test _ = - pp (uge (integer Typ.bool Z.minus_one) (signed 1 !1 ~to_:Typ.bool)) ; - [%expect {| {desc= (-1 u≥ ((i1)(s1) 1)); term= -1} |}] - end ) diff --git a/sledge/src/exp_test.mli b/sledge/src/exp_test.mli deleted file mode 100644 index 81857a06f..000000000 --- a/sledge/src/exp_test.mli +++ /dev/null @@ -1,6 +0,0 @@ -(* - * Copyright (c) Facebook, Inc. and its affiliates. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - *) diff --git a/sledge/src/term_test.ml b/sledge/src/term_test.ml index e7fb5ebcc..039f29a4b 100644 --- a/sledge/src/term_test.ml +++ b/sledge/src/term_test.ml @@ -45,6 +45,47 @@ let%test_module _ = (Exp.integer Typ.bool Z.minus_one) (Exp.signed 1 (Exp.integer Typ.siz Z.one) ~to_:Typ.bool))) + let pp_exp e = + Format.printf "@\nexp= %a; term= %a@." Exp.pp e Term.pp + (Term.of_exp e) + + let ( !! ) i = Exp.integer Typ.siz (Z.of_int i) + + let%expect_test _ = + pp_exp (Exp.signed 1 !!1 ~to_:Typ.bool) ; + [%expect {| exp= ((i1)(s1) 1); term= -1 |}] + + let%expect_test _ = + pp_exp (Exp.unsigned 1 !!(-1) ~to_:Typ.byt) ; + [%expect {| exp= ((i8)(u1) -1); term= 1 |}] + + let%expect_test _ = + pp_exp (Exp.signed 8 !!(-1) ~to_:Typ.int) ; + [%expect {| exp= ((i32)(s8) -1); term= -1 |}] + + let%expect_test _ = + pp_exp (Exp.unsigned 8 !!(-1) ~to_:Typ.int) ; + [%expect {| exp= ((i32)(u8) -1); term= 255 |}] + + let%expect_test _ = + pp_exp (Exp.signed 8 !!255 ~to_:Typ.byt) ; + [%expect {| exp= ((i8)(s8) 255); term= -1 |}] + + let%expect_test _ = + pp_exp (Exp.signed 7 !!255 ~to_:Typ.byt) ; + [%expect {| exp= ((i8)(s7) 255); term= -1 |}] + + let%expect_test _ = + pp_exp (Exp.unsigned 7 !!255 ~to_:Typ.byt) ; + [%expect {| exp= ((i8)(u7) 255); term= 127 |}] + + let%expect_test _ = + pp_exp + (Exp.uge + (Exp.integer Typ.bool Z.minus_one) + (Exp.signed 1 !!1 ~to_:Typ.bool)) ; + [%expect {| exp= (-1 u≥ ((i1)(s1) 1)); term= -1 |}] + let%expect_test _ = pp (!42 + !13) ; [%expect {| 55 |}]