{-# 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 {
forall testcase result term norm.
Terms testcase result term norm
-> DecisionTree testcase result term
tm_empty :: DecisionTree testcase result term,
forall testcase result term norm.
Terms testcase result term norm -> Map norm term
tm_terms :: Map norm term,
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 (Prop term)
| Knew (Prop term)
| Singleton
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
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
| 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)
| 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