-- Theory exploration which accepts one term at a time.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards #-}
module QuickSpec.Internal.Explore.Terms where

import qualified Data.Map.Strict as Map
import Data.Map(Map)
import QuickSpec.Internal.Term
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Type
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Testing
import QuickSpec.Internal.Testing.DecisionTree hiding (Result, Singleton)
import Control.Monad.Trans.State.Strict hiding (State)
import Data.Lens.Light
import QuickSpec.Internal.Utils
import QuickSpec.Internal.Terminal

data Terms testcase result term norm =
  Terms {
    -- Empty decision tree.
    forall testcase result term norm.
Terms testcase result term norm
-> DecisionTree testcase result term
tm_empty :: DecisionTree testcase result term,
    -- Terms already explored. These are stored in the *values* of the map.
    -- The keys are those terms but normalised.
    -- We do it like this so that explore can guarantee to always return
    -- the same representative for each equivalence class (see below).
    forall testcase result term norm.
Terms testcase result term norm -> Map norm term
tm_terms  :: Map norm term,
    -- Decision tree mapping test case results to terms.
    -- Terms are not stored normalised.
    -- Terms of different types must not be equal, because that results in
    -- ill-typed equations and bad things happening in the pruner.
    forall testcase result term norm.
Terms testcase result term norm
-> Map Type (DecisionTree testcase result term)
tm_tree   :: Map Type (DecisionTree testcase result term) }

tree :: Lens
  (Terms testcase result term norm)
  (Map Type (DecisionTree testcase result term))
tree = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens forall testcase result term norm.
Terms testcase result term norm
-> Map Type (DecisionTree testcase result term)
tm_tree (\Map Type (DecisionTree testcase result term)
x Terms testcase result term norm
y -> Terms testcase result term norm
y { tm_tree :: Map Type (DecisionTree testcase result term)
tm_tree = Map Type (DecisionTree testcase result term)
x })

treeForType :: Type -> Lens (Terms testcase result term norm) (DecisionTree testcase result term)
treeForType :: forall testcase result term norm.
Type
-> Lens
     (Terms testcase result term norm)
     (DecisionTree testcase result term)
treeForType Type
ty = forall a b. (a -> Lens a b) -> Lens a b
reading (\Terms{Map norm term
Map Type (DecisionTree testcase result term)
DecisionTree testcase result term
tm_tree :: Map Type (DecisionTree testcase result term)
tm_terms :: Map norm term
tm_empty :: DecisionTree testcase result term
tm_tree :: forall testcase result term norm.
Terms testcase result term norm
-> Map Type (DecisionTree testcase result term)
tm_terms :: forall testcase result term norm.
Terms testcase result term norm -> Map norm term
tm_empty :: forall testcase result term norm.
Terms testcase result term norm
-> DecisionTree testcase result term
..} -> forall a b. Ord a => a -> b -> Lens (Map a b) b
keyDefault Type
ty DecisionTree testcase result term
tm_empty forall (cat :: * -> * -> *) b c a.
Category cat =>
cat b c -> cat a b -> cat a c
# forall {testcase} {result} {term} {norm}.
Lens
  (Terms testcase result term norm)
  (Map Type (DecisionTree testcase result term))
tree)

initialState ::
  (term -> testcase -> Maybe result) ->
  Terms testcase result term norm
initialState :: forall term testcase result norm.
(term -> testcase -> Maybe result)
-> Terms testcase result term norm
initialState term -> testcase -> Maybe result
eval =
  Terms {
    tm_empty :: DecisionTree testcase result term
tm_empty = forall term testcase result.
(term -> testcase -> Maybe result)
-> DecisionTree testcase result term
empty term -> testcase -> Maybe result
eval,
    tm_terms :: Map norm term
tm_terms = forall k a. Map k a
Map.empty,
    tm_tree :: Map Type (DecisionTree testcase result term)
tm_tree = forall k a. Map k a
Map.empty }

data Result term =
    -- Discovered a new law.
    Discovered (Prop term)
    -- Term is equal to an existing term so redundant.
  | Knew (Prop term)
  | Singleton

-- The Prop returned is always t :=: u, where t is the term passed to explore
-- and u is the representative of t's equivalence class, not normalised.
-- The representatives of the equivalence classes are guaranteed not to change.
--
-- Discovered properties are not added to the pruner.
explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m, MonadTerminal m) =>
  term -> StateT (Terms testcase result term norm) m (Result term)
explore :: forall term norm result testcase (m :: * -> *).
(Pretty term, Typed term, Ord norm, Ord result,
 MonadTester testcase term m, MonadPruner term norm m,
 MonadTerminal m) =>
term -> StateT (Terms testcase result term norm) m (Result term)
explore term
t = do
  Result term
res <- forall term norm result testcase (m :: * -> *).
(Pretty term, Typed term, Ord norm, Ord result,
 MonadTester testcase term m, MonadPruner term norm m) =>
term -> StateT (Terms testcase result term norm) m (Result term)
explore' term
t
  --case res of
  --  Discovered prop -> putLine ("discovered " ++ prettyShow prop)
  --  Knew prop -> putLine ("knew " ++ prettyShow prop)
  --  Singleton -> putLine ("singleton " ++ prettyShow t)
  forall (m :: * -> *) a. Monad m => a -> m a
return Result term
res
explore' :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>
  term -> StateT (Terms testcase result term norm) m (Result term)
explore' :: forall term norm result testcase (m :: * -> *).
(Pretty term, Typed term, Ord norm, Ord result,
 MonadTester testcase term m, MonadPruner term norm m) =>
term -> StateT (Terms testcase result term norm) m (Result term)
explore' term
t = do
  term -> norm
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
  forall {m :: * -> *} {norm} {result} {testcase}.
(Monad m, Ord norm, Ord result) =>
(term -> norm)
-> (Prop term
    -> StateT (Terms testcase result term norm) m (Result term))
-> StateT (Terms testcase result term norm) m (Result term)
exp term -> norm
norm forall a b. (a -> b) -> a -> b
$ \Prop term
prop -> do
    TestResult testcase
res <- forall testcase term (m :: * -> *).
MonadTester testcase term m =>
Prop term -> m (TestResult testcase)
test Prop term
prop
    case TestResult testcase
res of
      TestResult testcase
Untestable ->
        forall (m :: * -> *) a. Monad m => a -> m a
return forall term. Result term
Singleton
      TestResult testcase
TestPassed -> do
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall term. Prop term -> Result term
Discovered Prop term
prop)
      TestFailed testcase
tc -> do
        forall testcase result term norm.
Type
-> Lens
     (Terms testcase result term norm)
     (DecisionTree testcase result term)
treeForType Type
ty forall a (m :: * -> *) b.
MonadState a m =>
Lens a b -> (b -> b) -> m ()
%= forall testcase result term.
testcase
-> DecisionTree testcase result term
-> DecisionTree testcase result term
addTestCase testcase
tc
        forall {m :: * -> *} {norm} {result} {testcase}.
(Monad m, Ord norm, Ord result) =>
(term -> norm)
-> (Prop term
    -> StateT (Terms testcase result term norm) m (Result term))
-> StateT (Terms testcase result term norm) m (Result term)
exp term -> norm
norm forall a b. (a -> b) -> a -> b
$
          forall a. HasCallStack => [Char] -> a
error [Char]
"returned counterexample failed to falsify property"

  where
    ty :: Type
ty = forall a. Typed a => a -> Type
typ term
t
    exp :: (term -> norm)
-> (Prop term
    -> StateT (Terms testcase result term norm) m (Result term))
-> StateT (Terms testcase result term norm) m (Result term)
exp term -> norm
norm Prop term
-> StateT (Terms testcase result term norm) m (Result term)
found = do
      tm :: Terms testcase result term norm
tm@Terms{Map norm term
Map Type (DecisionTree testcase result term)
DecisionTree testcase result term
tm_tree :: Map Type (DecisionTree testcase result term)
tm_terms :: Map norm term
tm_empty :: DecisionTree testcase result term
tm_tree :: forall testcase result term norm.
Terms testcase result term norm
-> Map Type (DecisionTree testcase result term)
tm_terms :: forall testcase result term norm.
Terms testcase result term norm -> Map norm term
tm_empty :: forall testcase result term norm.
Terms testcase result term norm
-> DecisionTree testcase result term
..} <- forall (m :: * -> *) s. Monad m => StateT s m s
get
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup norm
t' Map norm term
tm_terms of
        Just term
u -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall term. Prop term -> Result term
Knew (term
t forall a. a -> a -> Prop a
=== term
u))
        Maybe term
Nothing ->
          case forall result term testcase.
Ord result =>
term
-> DecisionTree testcase result term -> Result testcase result term
insert term
t (Terms testcase result term norm
tm forall b c. b -> Lens b c -> c
^. forall testcase result term norm.
Type
-> Lens
     (Terms testcase result term norm)
     (DecisionTree testcase result term)
treeForType Type
ty) of
            Distinct DecisionTree testcase result term
tree -> do
              forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (forall a b. Lens a b -> b -> a -> a
setL (forall testcase result term norm.
Type
-> Lens
     (Terms testcase result term norm)
     (DecisionTree testcase result term)
treeForType Type
ty) DecisionTree testcase result term
tree Terms testcase result term norm
tm { tm_terms :: Map norm term
tm_terms = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert norm
t' term
t Map norm term
tm_terms })
              forall (m :: * -> *) a. Monad m => a -> m a
return forall term. Result term
Singleton
            EqualTo term
u
              -- tm_terms is not kept normalised wrt the discovered laws;
              -- instead, we normalise it lazily like so.
              | norm
t' forall a. Eq a => a -> a -> Bool
== norm
u' -> do
                forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put Terms testcase result term norm
tm { tm_terms :: Map norm term
tm_terms = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert norm
u' term
u Map norm term
tm_terms }
                forall (m :: * -> *) a. Monad m => a -> m a
return (forall term. Prop term -> Result term
Knew Prop term
prop)
              -- Ask QuickCheck for a counterexample to the property.
              | Bool
otherwise -> Prop term
-> StateT (Terms testcase result term norm) m (Result term)
found Prop term
prop
              where
                u' :: norm
u' = term -> norm
norm term
u
                prop :: Prop term
prop = term
t forall a. a -> a -> Prop a
=== term
u
      where
        t' :: norm
t' = term -> norm
norm term
t