{-# 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 {
tm_empty :: DecisionTree testcase result term,
tm_terms :: Map norm term,
tm_tree :: Map Type (DecisionTree testcase result term) }
tree = lens tm_tree (\x y -> y { tm_tree = x })
treeForType :: Type -> Lens (Terms testcase result term norm) (DecisionTree testcase result term)
treeForType ty = reading (\Terms{..} -> keyDefault ty tm_empty # tree)
initialState ::
(term -> testcase -> result) ->
Terms testcase result term norm
initialState eval =
Terms {
tm_empty = empty eval,
tm_terms = Map.empty,
tm_tree = 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 t = do
res <- explore' t
return 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' t = do
norm <- normaliser
exp norm $ \prop -> do
res <- test prop
case res of
Nothing -> do
return (Discovered prop)
Just tc -> do
treeForType ty %= addTestCase tc
exp norm $
error "returned counterexample failed to falsify property"
where
ty = typ t
exp norm found = do
tm@Terms{..} <- get
case Map.lookup t' tm_terms of
Just u -> return (Knew (t === u))
Nothing ->
case insert t (tm ^. treeForType ty) of
Distinct tree -> do
put (setL (treeForType ty) tree tm { tm_terms = Map.insert t' t tm_terms })
return Singleton
EqualTo u
| t' == u' -> do
put tm { tm_terms = Map.insert u' u tm_terms }
return (Knew prop)
| otherwise -> found prop
where
u' = norm u
prop = t === u
where
t' = norm t