-- A pruning layer which automatically adds axioms about functions as they appear.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, TypeOperators #-}
module QuickSpec.Internal.Pruning.Background where

import QuickSpec.Internal.Term
import QuickSpec.Internal.Testing
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Terminal
import qualified Data.Set as Set
import Data.Set(Set)
import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Strict hiding (State)

newtype Pruner fun m a =
  Pruner (StateT (Set fun) m a)
  deriving (forall a b. a -> Pruner fun m b -> Pruner fun m a
forall a b. (a -> b) -> Pruner fun m a -> Pruner fun m b
forall fun (m :: * -> *) a b.
Functor m =>
a -> Pruner fun m b -> Pruner fun m a
forall fun (m :: * -> *) a b.
Functor m =>
(a -> b) -> Pruner fun m a -> Pruner fun m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Pruner fun m b -> Pruner fun m a
$c<$ :: forall fun (m :: * -> *) a b.
Functor m =>
a -> Pruner fun m b -> Pruner fun m a
fmap :: forall a b. (a -> b) -> Pruner fun m a -> Pruner fun m b
$cfmap :: forall fun (m :: * -> *) a b.
Functor m =>
(a -> b) -> Pruner fun m a -> Pruner fun m b
Functor, forall a. a -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall a b.
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
forall a b c.
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
forall {fun} {m :: * -> *}. Monad m => Functor (Pruner fun m)
forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
forall fun (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m a
$c<* :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m a
*> :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
$c*> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
liftA2 :: forall a b c.
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
$cliftA2 :: forall fun (m :: * -> *) a b c.
Monad m =>
(a -> b -> c) -> Pruner fun m a -> Pruner fun m b -> Pruner fun m c
<*> :: forall a b.
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
$c<*> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m (a -> b) -> Pruner fun m a -> Pruner fun m b
pure :: forall a. a -> Pruner fun m a
$cpure :: forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
Applicative, forall a. a -> Pruner fun m a
forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall a b.
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
forall fun (m :: * -> *). Monad m => Applicative (Pruner fun m)
forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Pruner fun m a
$creturn :: forall fun (m :: * -> *) a. Monad m => a -> Pruner fun m a
>> :: forall a b. Pruner fun m a -> Pruner fun m b -> Pruner fun m b
$c>> :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> Pruner fun m b -> Pruner fun m b
>>= :: forall a b.
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
$c>>= :: forall fun (m :: * -> *) a b.
Monad m =>
Pruner fun m a -> (a -> Pruner fun m b) -> Pruner fun m b
Monad, forall a. IO a -> Pruner fun m a
forall {fun} {m :: * -> *}. MonadIO m => Monad (Pruner fun m)
forall fun (m :: * -> *) a. MonadIO m => IO a -> Pruner fun m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Pruner fun m a
$cliftIO :: forall fun (m :: * -> *) a. MonadIO m => IO a -> Pruner fun m a
MonadIO, forall fun (m :: * -> *) a. Monad m => m a -> Pruner fun m a
forall (m :: * -> *) a. Monad m => m a -> Pruner fun m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: forall (m :: * -> *) a. Monad m => m a -> Pruner fun m a
$clift :: forall fun (m :: * -> *) a. Monad m => m a -> Pruner fun m a
MonadTrans, MonadTester testcase term, String -> Pruner fun m ()
forall {fun} {m :: * -> *}. MonadTerminal m => Monad (Pruner fun m)
forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
forall (m :: * -> *).
Monad m
-> (String -> m ())
-> (String -> m ())
-> (String -> m ())
-> MonadTerminal m
putTemp :: String -> Pruner fun m ()
$cputTemp :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
putLine :: String -> Pruner fun m ()
$cputLine :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
putText :: String -> Pruner fun m ()
$cputText :: forall fun (m :: * -> *).
MonadTerminal m =>
String -> Pruner fun m ()
MonadTerminal)

class Background f where
  background :: f -> [Prop (Term f)]
  background f
_ = []

run :: Monad m => Pruner fun m a -> m a
run :: forall (m :: * -> *) fun a. Monad m => Pruner fun m a -> m a
run (Pruner StateT (Set fun) m a
x) =
  forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (Set fun) m a
x forall a. Set a
Set.empty

instance (Ord fun, Background fun, MonadPruner (Term fun) norm m) =>
  MonadPruner (Term fun) norm (Pruner fun m) where
  normaliser :: Pruner fun m (Term fun -> norm)
normaliser = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
  add :: Prop (Term fun) -> Pruner fun m Bool
add Prop (Term fun)
prop = do
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall fun norm (m :: * -> *).
(Ord fun, Background fun, MonadPruner (Term fun) norm m) =>
fun -> Pruner fun m ()
addFunction (forall f a. Symbolic f a => a -> [f]
funs Prop (Term fun)
prop)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add Prop (Term fun)
prop)

addFunction :: (Ord fun, Background fun, MonadPruner (Term fun) norm m) => fun -> Pruner fun m ()
addFunction :: forall fun norm (m :: * -> *).
(Ord fun, Background fun, MonadPruner (Term fun) norm m) =>
fun -> Pruner fun m ()
addFunction fun
f = do
  Set fun
funcs <- forall fun (m :: * -> *) a. StateT (Set fun) m a -> Pruner fun m a
Pruner forall (m :: * -> *) s. Monad m => StateT s m s
get
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (fun
f forall a. Ord a => a -> Set a -> Bool
`Set.member` Set fun
funcs) forall a b. (a -> b) -> a -> b
$ do
    forall fun (m :: * -> *) a. StateT (Set fun) m a -> Pruner fun m a
Pruner (forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (forall a. Ord a => a -> Set a -> Set a
Set.insert fun
f Set fun
funcs))
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add (forall f. Background f => f -> [Prop (Term f)]
background fun
f)

instance (Background fun1, Background fun2) => Background (fun1 :+: fun2) where
  background :: (fun1 :+: fun2) -> [Prop (Term (fun1 :+: fun2))]
background (Inl fun1
x) = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> a :+: b
Inl)) (forall f. Background f => f -> [Prop (Term f)]
background fun1
x)
  background (Inr fun2
x) = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. b -> a :+: b
Inr)) (forall f. Background f => f -> [Prop (Term f)]
background fun2
x)