% Testing CallTime Choice of FunctionalLogic Operations
% Sebastian Fischer (sebf@informatik.unikiel.de)
This module defines tests that specify the intended behaviour of
functionallogic programs w.r.t. laziness and sharing. Although
nondeterministic computations must be executed on demand, their
results have to be as if they were executed eagerly.
> module CFLP.Tests.CallTimeChoice where
>
> import CFLP
> import CFLP.Tests
>
> import Test.HUnit
>
> import Prelude hiding ( not, null, head )
> import CFLP.Types.Bool
> import CFLP.Types.List
Every module under `CFLP.Tests` defines a constant `tests` that
collects all defined tests.
> tests :: Test
> tests = "call-time choice" ~: test
> [ "ignore first, narrow second" ~: ignoreFirstNarrowSecond
> , "shared vars are equal" ~: sharedVarsAreEqual
> , "no demand on shared var" ~: noDemandOnSharedVar
> , "shared compound terms" ~: sharedCompoundTerms
> ]
The following test checks a function with two arguments, where the
first must be ignored. Any changes in the translation scheme must not
lead to demand on the first argument of `ignot`. I have no better idea
to check demand than with using `error`. So an *error* is considered a
*failure* in this test case.
> ignoreFirstNarrowSecond :: Assertion
> ignoreFirstNarrowSecond = assertResults comp [True,False]
> where
> comp cs u = ignot (error "illegal demand") (unknown u) cs
>
> ignot :: CFLP s
> => Data s a -> Data s Bool -> Context (Ctx s) -> Data s Bool
> ignot _ = not
The following test checks calltime choice semantics: variables
represent identical ground values. The elements of the constructed
list must be equal although they are computed from a free variable.
> sharedVarsAreEqual :: Assertion
> sharedVarsAreEqual = assertResults comp [[False,False],[True,True]]
> where
> comp _ = two . unknown
>
> two :: (Monad m, Generic a) => Nondet cs m a -> Nondet cs m [a]
> two x = x ^: x ^: nil
In the current translation scheme sharing is implicit (we have no
special combinator to express sharing but use Haskell's sharing
directly). In case we introduce such a combinator, the following tests
are interesting.
Even with an explicit combinator for sharing (to be used, e.g., in the
definition of the function `two`) there must not be demand on
something that is shared.
> noDemandOnSharedVar :: Assertion
> noDemandOnSharedVar = assertResults comp [False]
> where
> comp cs _ = null (two (error "illegal demand" :: Nondet cs m Bool)) cs
The following test checks whether sharing is ensured on aruments of
compound terms even if they are consumed. In this example, the
variable `l` is shared, so the heads that are computed twice must be
equal and the negated head must be different from the head.
> sharedCompoundTerms :: Assertion
> sharedCompoundTerms = assertResults comp [[True,False],[False,True]]
> where
> comp cs u = negHeads (unknown u) cs
>
> negHeads :: CFLP s
> => Data s [Bool] -> Context (Ctx s) -> Data s [Bool]
> negHeads l cs = not (head l cs) cs ^: head l cs ^: nil