From 8ca41a9639a7278095f464088513881a1b61414e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 4 Sep 2020 13:37:17 -0700 Subject: [PATCH] [sledge] Test: Move test modules into test directory Reviewed By: ngorogiannis Differential Revision: D23459511 fbshipit-source-id: 29570a0ad --- sledge/dune | 11 +++++++++++ sledge/src/{ses => test}/equality_test.ml | 2 ++ sledge/src/{ses => test}/equality_test.mli | 0 sledge/src/{ => test}/fol_test.ml | 3 +++ sledge/src/{ => test}/fol_test.mli | 0 sledge/src/{ => test}/sh_test.ml | 11 ++++++----- sledge/src/{ => test}/sh_test.mli | 0 sledge/src/{ => test}/solver_test.ml | 1 + sledge/src/{ => test}/solver_test.mli | 0 sledge/src/{ses => test}/term_test.ml | 2 ++ sledge/src/{ses => test}/term_test.mli | 0 11 files changed, 25 insertions(+), 5 deletions(-) rename sledge/src/{ses => test}/equality_test.ml (99%) rename sledge/src/{ses => test}/equality_test.mli (100%) rename sledge/src/{ => test}/fol_test.ml (99%) rename sledge/src/{ => test}/fol_test.mli (100%) rename sledge/src/{ => test}/sh_test.ml (97%) rename sledge/src/{ => test}/sh_test.mli (100%) rename sledge/src/{ => test}/solver_test.ml (99%) rename sledge/src/{ => test}/solver_test.mli (100%) rename sledge/src/{ses => test}/term_test.ml (99%) rename sledge/src/{ses => test}/term_test.mli (100%) diff --git a/sledge/dune b/sledge/dune index 9ab830dc8..3ff4ba061 100644 --- a/sledge/dune +++ b/sledge/dune @@ -69,6 +69,17 @@ (pps ppx_sledge ppx_trace)) (inline_tests))) +(subdir + src/test + (library + (name test) + (libraries sledge) + (flags + (:standard -open NS)) + (preprocess + (pps ppx_sledge ppx_trace)) + (inline_tests))) + (subdir model (rule diff --git a/sledge/src/ses/equality_test.ml b/sledge/src/test/equality_test.ml similarity index 99% rename from sledge/src/ses/equality_test.ml rename to sledge/src/test/equality_test.ml index cbddcd342..7b803b2e1 100644 --- a/sledge/src/ses/equality_test.ml +++ b/sledge/src/test/equality_test.ml @@ -5,6 +5,8 @@ * LICENSE file in the root directory of this source tree. *) +open Ses + let%test_module _ = ( module struct open Equality diff --git a/sledge/src/ses/equality_test.mli b/sledge/src/test/equality_test.mli similarity index 100% rename from sledge/src/ses/equality_test.mli rename to sledge/src/test/equality_test.mli diff --git a/sledge/src/fol_test.ml b/sledge/src/test/fol_test.ml similarity index 99% rename from sledge/src/fol_test.ml rename to sledge/src/test/fol_test.ml index be9f579b6..01ba4e153 100644 --- a/sledge/src/fol_test.ml +++ b/sledge/src/test/fol_test.ml @@ -5,6 +5,8 @@ * LICENSE file in the root directory of this source tree. *) +open Sledge + let%test_module _ = ( module struct open Fol @@ -123,6 +125,7 @@ let%test_module _ = pp_raw r1 ; [%expect {| + %x_5 = %y_6 {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [-1 ↦ ]; [0 ↦ ]]} |}] diff --git a/sledge/src/fol_test.mli b/sledge/src/test/fol_test.mli similarity index 100% rename from sledge/src/fol_test.mli rename to sledge/src/test/fol_test.mli diff --git a/sledge/src/sh_test.ml b/sledge/src/test/sh_test.ml similarity index 97% rename from sledge/src/sh_test.ml rename to sledge/src/test/sh_test.ml index e1e5d7a04..ddfc1f29b 100644 --- a/sledge/src/sh_test.ml +++ b/sledge/src/test/sh_test.ml @@ -5,6 +5,7 @@ * LICENSE file in the root directory of this source tree. *) +open Sledge open Fol let%test_module _ = @@ -60,11 +61,11 @@ let%test_module _ = pp (star p q) ; [%expect {| - ∃ %x_6 . emp - - 0 = %x_6 ∧ emp - - 0 = %x_6 ∧ emp |}] + ∃ %x_6 . emp + + 0 = %x_6 ∧ emp + + 0 = %x_6 ∧ emp |}] let%expect_test _ = let q = diff --git a/sledge/src/sh_test.mli b/sledge/src/test/sh_test.mli similarity index 100% rename from sledge/src/sh_test.mli rename to sledge/src/test/sh_test.mli diff --git a/sledge/src/solver_test.ml b/sledge/src/test/solver_test.ml similarity index 99% rename from sledge/src/solver_test.ml rename to sledge/src/test/solver_test.ml index c9042516f..26663f1ba 100644 --- a/sledge/src/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -5,6 +5,7 @@ * LICENSE file in the root directory of this source tree. *) +open Sledge open Fol let%test_module _ = diff --git a/sledge/src/solver_test.mli b/sledge/src/test/solver_test.mli similarity index 100% rename from sledge/src/solver_test.mli rename to sledge/src/test/solver_test.mli diff --git a/sledge/src/ses/term_test.ml b/sledge/src/test/term_test.ml similarity index 99% rename from sledge/src/ses/term_test.ml rename to sledge/src/test/term_test.ml index 9b8987b05..97a1cd3e0 100644 --- a/sledge/src/ses/term_test.ml +++ b/sledge/src/test/term_test.ml @@ -5,6 +5,8 @@ * LICENSE file in the root directory of this source tree. *) +open Ses + (* [@@@warning "-32"] *) let%test_module _ = diff --git a/sledge/src/ses/term_test.mli b/sledge/src/test/term_test.mli similarity index 100% rename from sledge/src/ses/term_test.mli rename to sledge/src/test/term_test.mli