-- Decision trees for testing terms for equality.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE RecordWildCards #-}
module QuickSpec.Internal.Testing.DecisionTree where

import qualified Data.Map as Map
import Data.Map(Map)

data DecisionTree testcase result term =
  DecisionTree {
    -- A function for evaluating terms on test cases.
    forall testcase result term.
DecisionTree testcase result term
-> term -> testcase -> Maybe result
dt_evaluate :: term -> testcase -> Maybe result,
    -- The set of test cases gathered so far.
    forall testcase result term.
DecisionTree testcase result term -> [testcase]
dt_test_cases :: [testcase],
    -- The tree itself.
    forall testcase result term.
DecisionTree testcase result term -> Maybe (InnerTree result term)
dt_tree :: !(Maybe (InnerTree result term)) }

data InnerTree result term =
    TestCase !(Map result (InnerTree result term))
  | Singleton !term

data Result testcase result term =
    Distinct (DecisionTree testcase result term)
  | EqualTo term

-- Make a new decision tree.
empty :: (term -> testcase -> Maybe result) -> DecisionTree testcase result term
empty :: forall term testcase result.
(term -> testcase -> Maybe result)
-> DecisionTree testcase result term
empty term -> testcase -> Maybe result
eval =
  DecisionTree {
    dt_evaluate :: term -> testcase -> Maybe result
dt_evaluate = term -> testcase -> Maybe result
eval,
    dt_test_cases :: [testcase]
dt_test_cases = [],
    dt_tree :: Maybe (InnerTree result term)
dt_tree = forall a. Maybe a
Nothing }

-- Add a new test case to a decision tree.
addTestCase ::
  testcase -> DecisionTree testcase result term ->
  DecisionTree testcase result term
addTestCase :: forall testcase result term.
testcase
-> DecisionTree testcase result term
-> DecisionTree testcase result term
addTestCase testcase
tc dt :: DecisionTree testcase result term
dt@DecisionTree{[testcase]
Maybe (InnerTree result term)
term -> testcase -> Maybe result
dt_tree :: Maybe (InnerTree result term)
dt_test_cases :: [testcase]
dt_evaluate :: term -> testcase -> Maybe result
dt_tree :: forall testcase result term.
DecisionTree testcase result term -> Maybe (InnerTree result term)
dt_test_cases :: forall testcase result term.
DecisionTree testcase result term -> [testcase]
dt_evaluate :: forall testcase result term.
DecisionTree testcase result term
-> term -> testcase -> Maybe result
..} =
  DecisionTree testcase result term
dt{dt_test_cases :: [testcase]
dt_test_cases = [testcase]
dt_test_cases forall a. [a] -> [a] -> [a]
++ [testcase
tc]}

-- Insert a value into a decision tree.
insert :: Ord result =>
  term -> DecisionTree testcase result term ->
  Result testcase result term
insert :: forall result term testcase.
Ord result =>
term
-> DecisionTree testcase result term -> Result testcase result term
insert term
x dt :: DecisionTree testcase result term
dt@DecisionTree{dt_tree :: forall testcase result term.
DecisionTree testcase result term -> Maybe (InnerTree result term)
dt_tree = Maybe (InnerTree result term)
Nothing, [testcase]
term -> testcase -> Maybe result
dt_test_cases :: [testcase]
dt_evaluate :: term -> testcase -> Maybe result
dt_test_cases :: forall testcase result term.
DecisionTree testcase result term -> [testcase]
dt_evaluate :: forall testcase result term.
DecisionTree testcase result term
-> term -> testcase -> Maybe result
..} =
  forall testcase result term.
DecisionTree testcase result term -> Result testcase result term
Distinct DecisionTree testcase result term
dt{dt_tree :: Maybe (InnerTree result term)
dt_tree = forall a. a -> Maybe a
Just (forall result term. term -> InnerTree result term
Singleton term
x)}
insert term
x dt :: DecisionTree testcase result term
dt@DecisionTree{dt_tree :: forall testcase result term.
DecisionTree testcase result term -> Maybe (InnerTree result term)
dt_tree = Just InnerTree result term
dt_tree, [testcase]
term -> testcase -> Maybe result
dt_test_cases :: [testcase]
dt_evaluate :: term -> testcase -> Maybe result
dt_test_cases :: forall testcase result term.
DecisionTree testcase result term -> [testcase]
dt_evaluate :: forall testcase result term.
DecisionTree testcase result term
-> term -> testcase -> Maybe result
..} =
  forall {testcase} {result}.
(InnerTree result term -> DecisionTree testcase result term)
-> [testcase]
-> InnerTree result term
-> Result testcase result term
aux InnerTree result term -> DecisionTree testcase result term
k [testcase]
dt_test_cases InnerTree result term
dt_tree
  where
    k :: InnerTree result term -> DecisionTree testcase result term
k InnerTree result term
tree = DecisionTree testcase result term
dt{dt_tree :: Maybe (InnerTree result term)
dt_tree = forall a. a -> Maybe a
Just InnerTree result term
tree}
    aux :: (InnerTree result term -> DecisionTree testcase result term)
-> [testcase]
-> InnerTree result term
-> Result testcase result term
aux InnerTree result term -> DecisionTree testcase result term
_ [] (Singleton term
y) = forall testcase result term. term -> Result testcase result term
EqualTo term
y
    aux InnerTree result term -> DecisionTree testcase result term
k (testcase
t:[testcase]
ts) (Singleton term
y) =
      case term -> testcase -> Maybe result
dt_evaluate term
y testcase
t of
        Maybe result
Nothing ->
          -- y is untestable, so we can evict it from the tree
          forall testcase result term.
DecisionTree testcase result term -> Result testcase result term
Distinct (InnerTree result term -> DecisionTree testcase result term
k (forall result term. term -> InnerTree result term
Singleton term
x))
        Just result
val ->
          (InnerTree result term -> DecisionTree testcase result term)
-> [testcase]
-> InnerTree result term
-> Result testcase result term
aux InnerTree result term -> DecisionTree testcase result term
k (testcase
tforall a. a -> [a] -> [a]
:[testcase]
ts) forall a b. (a -> b) -> a -> b
$
            forall result term.
Map result (InnerTree result term) -> InnerTree result term
TestCase (forall k a. k -> a -> Map k a
Map.singleton result
val (forall result term. term -> InnerTree result term
Singleton term
y)) 
    aux InnerTree result term -> DecisionTree testcase result term
k (testcase
t:[testcase]
ts) (TestCase Map result (InnerTree result term)
res) =
      case term -> testcase -> Maybe result
dt_evaluate term
x testcase
t of
        Maybe result
Nothing ->
          forall testcase result term.
DecisionTree testcase result term -> Result testcase result term
Distinct (InnerTree result term -> DecisionTree testcase result term
k (forall result term.
Map result (InnerTree result term) -> InnerTree result term
TestCase Map result (InnerTree result term)
res))
        Just result
val ->
          let
            k' :: InnerTree result term -> DecisionTree testcase result term
k' InnerTree result term
tree = InnerTree result term -> DecisionTree testcase result term
k (forall result term.
Map result (InnerTree result term) -> InnerTree result term
TestCase (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert result
val InnerTree result term
tree Map result (InnerTree result term)
res))
          in case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup result
val Map result (InnerTree result term)
res of
            Maybe (InnerTree result term)
Nothing ->
              forall testcase result term.
DecisionTree testcase result term -> Result testcase result term
Distinct (InnerTree result term -> DecisionTree testcase result term
k' (forall result term. term -> InnerTree result term
Singleton term
x))
            Just InnerTree result term
tree ->
              (InnerTree result term -> DecisionTree testcase result term)
-> [testcase]
-> InnerTree result term
-> Result testcase result term
aux InnerTree result term -> DecisionTree testcase result term
k' [testcase]
ts InnerTree result term
tree
    aux InnerTree result term -> DecisionTree testcase result term
_ [] (TestCase Map result (InnerTree result term)
_) =
      forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected node in decision tree"

data Statistics =
  Statistics {
    -- Total number of terms in the decision tree
    Statistics -> Int
stat_num_terms :: !Int,
    -- Total number of tests executed
    Statistics -> Int
stat_num_tests :: !Int,
    -- Number of distinct test cases used
    Statistics -> Int
stat_num_test_cases :: !Int }
  deriving (Statistics -> Statistics -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Statistics -> Statistics -> Bool
$c/= :: Statistics -> Statistics -> Bool
== :: Statistics -> Statistics -> Bool
$c== :: Statistics -> Statistics -> Bool
Eq, Int -> Statistics -> ShowS
[Statistics] -> ShowS
Statistics -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Statistics] -> ShowS
$cshowList :: [Statistics] -> ShowS
show :: Statistics -> [Char]
$cshow :: Statistics -> [Char]
showsPrec :: Int -> Statistics -> ShowS
$cshowsPrec :: Int -> Statistics -> ShowS
Show)

statistics :: DecisionTree testcase result term -> Statistics
statistics :: forall testcase result term.
DecisionTree testcase result term -> Statistics
statistics DecisionTree{dt_tree :: forall testcase result term.
DecisionTree testcase result term -> Maybe (InnerTree result term)
dt_tree = Maybe (InnerTree result term)
Nothing} =
  Int -> Int -> Int -> Statistics
Statistics Int
0 Int
0 Int
0
statistics DecisionTree{dt_tree :: forall testcase result term.
DecisionTree testcase result term -> Maybe (InnerTree result term)
dt_tree = Just InnerTree result term
dt_tree, [testcase]
term -> testcase -> Maybe result
dt_test_cases :: [testcase]
dt_evaluate :: term -> testcase -> Maybe result
dt_test_cases :: forall testcase result term.
DecisionTree testcase result term -> [testcase]
dt_evaluate :: forall testcase result term.
DecisionTree testcase result term
-> term -> testcase -> Maybe result
..} =
  Statistics {
    stat_num_terms :: Int
stat_num_terms = Int
x,
    stat_num_tests :: Int
stat_num_tests = Int
y,
    stat_num_test_cases :: Int
stat_num_test_cases = forall (t :: * -> *) a. Foldable t => t a -> Int
length [testcase]
dt_test_cases }
  where
    (Int
x, Int
y) = forall {b} {result} {term}.
Num b =>
InnerTree result term -> (b, b)
stat InnerTree result term
dt_tree

    -- Returns (number of terms, number of tests)
    stat :: InnerTree result term -> (b, b)
stat Singleton{} = (b
1, b
0)
    -- To calculate the number of test cases, note that each term
    -- under res executed one test case on the way through this node.
    stat (TestCase Map result (InnerTree result term)
res) =
      (forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(b, b)]
ss), forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ b
x forall a. Num a => a -> a -> a
+ b
y | (b
x, b
y) <- [(b, b)]
ss ])
      where
        ss :: [(b, b)]
ss = forall a b. (a -> b) -> [a] -> [b]
map InnerTree result term -> (b, b)
stat (forall k a. Map k a -> [a]
Map.elems Map result (InnerTree result term)
res)