Merge branch 'develop-test-libraries'. Close #475.

**Description**

As part of the requirements for Class D (NPR7150.2C), we need unit tests
for all of copilot.

A natural next step is to introduce the testing infrastructure for
`copilot-libraries`.

**Type**

- Management: conformance with new requirement.

**Additional context**

None.

**Requester**

- Ivan Perez

**Method to check presence of bug**

The following Dockerfile checks that copilot-libraries's tests can be
executed, in which case it prints the message Success:

```
FROM ubuntu:focal

RUN apt-get update

RUN apt-get install --yes libz-dev
RUN apt-get install --yes git

RUN apt-get install --yes wget
RUN mkdir -p $HOME/.ghcup/bin
RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup

RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/
RUN apt-get install --yes curl
RUN apt-get install --yes gcc make libgmp3-dev g++

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.4.7
RUN ghcup install cabal 3.8
RUN ghcup set ghc 9.4.7
RUN cabal update

RUN apt-get install --yes z3

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd copilot-libraries && \
    cabal test copilot-libraries:unit-tests && \
    echo Success
```

Command (substitute variables based on new path after merge):
```
$ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-475
```

**Expected result**

The library `copilot-libraries` includes tests for some of the existing
modules. Introducing (some classes of) errors in the implementation of
`copilot-libraries` makes the tests detect those errors.

Running the docker file above prints the message success, indicating
that copilot-libraries now declares a unit-tests component.

**Solution implemented**

Add tests for `copilot-libraries` that test a basic property in the
module Copilot.Libraries.PTLTL. The property is tested using both
copilot-theorem and copilot-interpreter, showing how both interfaces can
be used.

**Further notes**

Due to the magnitude of this change, we decide to simplify the issue by
merely introducing the infrastructure. We leave it to a future issue to
include a more comprehensive list of properties that covers all modules.

Author: ivanperez-keera

.travis.yml

@@ -33,6 +33,7 @@ script:
   #
   # Only libraries with tests are listed below or the v2-test command fails.
   #
-  # Testing copilot-theorem requires z3. See above conditional installation,
-  # and keep GHC version numbers in both places in sync.
-  - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99 copilot-theorem; fi
+  # Testing copilot-theorem and copilot-libraries requires z3. See above
+  # conditional installation, and keep GHC version numbers in both places in
+  # sync.
+  - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99 copilot-theorem copilot-libraries; fi

copilot-libraries/CHANGELOG

@@ -1,3 +1,6 @@
+2023-12-24
+        * Introduce testing infrastructure for Copilot.Library. (#475)
+
 2023-11-07
         * Version bump (3.17). (#466)
 

copilot-libraries/copilot-libraries.cabal

@@ -57,3 +57,34 @@ library
 
   ghc-options:
     -Wall
+
+test-suite unit-tests
+  type:
+    exitcode-stdio-1.0
+
+  main-is:
+    Main.hs
+
+  other-modules:
+    Test.Copilot.Library.PTLTL
+    Test.Extra
+
+  build-depends:
+      base
+    , QuickCheck
+    , test-framework
+    , test-framework-quickcheck2
+
+    , copilot-interpreter
+    , copilot-language
+    , copilot-libraries
+    , copilot-theorem
+
+  hs-source-dirs:
+    tests
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall

copilot-libraries/tests/Main.hs

@@ -0,0 +1,18 @@
+-- | Test copilot-libraries.
+module Main where
+
+-- External imports
+import Test.Framework (Test, defaultMain)
+
+-- Internal imports
+import qualified Test.Copilot.Library.PTLTL
+
+-- | Run all unit tests on copilot-libraries.
+main :: IO ()
+main = defaultMain tests
+
+-- | All unit tests in copilot-libraries.
+tests :: [Test.Framework.Test]
+tests =
+  [ Test.Copilot.Library.PTLTL.tests
+  ]

copilot-libraries/tests/Test/Copilot/Library/PTLTL.hs

@@ -0,0 +1,72 @@
+-- | Test copilot-libraries:Copilot.Library.PTLTL
+module Test.Copilot.Library.PTLTL
+    (tests)
+  where
+
+-- External imports
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Gen, Property)
+
+-- External imports: Copilot
+import           Copilot.Language                   (extern)
+import qualified Copilot.Language.Operators.Boolean as Copilot
+import           Copilot.Language.Stream            (Stream)
+import           Copilot.Theorem.What4              (SatResult (..))
+
+-- Internal imports: auxiliary functions
+import Test.Extra (arbitraryBoolExpr, testWithInterpreter, testWithTheorem)
+
+-- Internal imports: Modules being tested
+import Copilot.Library.PTLTL (eventuallyPrev, previous)
+
+-- * Constants
+
+-- | Unit tests for copilot-libraries:Copilot.Library.PTLTL.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Library.PTLTL"
+    [ testProperty "previous x ==> eventuallyPrev x (theorem)"
+        testProvePreviousEventually
+    , testProperty "previous x ==> eventuallyPrev x (interpreter)"
+        testCheckPreviousEventually
+    ]
+
+-- * Individual tests
+
+-- | Test that Z3 is able to prove the following expression valid:
+-- @
+--    previous x ==> eventuallyPrev x
+-- @
+testProvePreviousEventually :: Property
+testProvePreviousEventually = testWithTheorem pair
+  where
+    pair :: Gen (Stream Bool, SatResult)
+    pair = pure (stream, expectation)
+
+    stream :: Stream Bool
+    stream =
+        previous boolStream Copilot.==> eventuallyPrev boolStream
+      where
+        boolStream = extern "x" Nothing
+
+    expectation :: SatResult
+    expectation = Valid
+
+-- | Test that the following stream is always true:
+-- @
+--    previous x ==> eventuallyPrev x
+-- @
+testCheckPreviousEventually :: Property
+testCheckPreviousEventually = testWithInterpreter pair
+  where
+    pair :: Gen (Stream Bool, [Bool])
+    pair = do
+      -- We discard the expectation from the expression; the temporal formula
+      -- holds at all times regardless.
+      boolStream <- fst <$> arbitraryBoolExpr
+      let prop = previous boolStream Copilot.==> eventuallyPrev boolStream
+      return (prop, expectation)
+
+    expectation :: [Bool]
+    expectation = repeat True