{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DeriveFunctor #-}
module QuickSpec.Internal.Explore.Conditionals where

import QuickSpec.Internal.Prop as Prop
import QuickSpec.Internal.Term as Term
import QuickSpec.Internal.Type
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Pruning.Background(Background(..))
import QuickSpec.Internal.Testing
import QuickSpec.Internal.Terminal
import QuickSpec.Internal.Utils
import QuickSpec.Internal.Explore.Polymorphic
import qualified Twee.Base as Twee
import Data.List
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.IO.Class

newtype Conditionals m a = Conditionals (m a)
  deriving (forall a b. a -> Conditionals m b -> Conditionals m a
forall a b. (a -> b) -> Conditionals m a -> Conditionals m b
forall (m :: * -> *) a b.
Functor m =>
a -> Conditionals m b -> Conditionals m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> Conditionals m a -> Conditionals 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 -> Conditionals m b -> Conditionals m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> Conditionals m b -> Conditionals m a
fmap :: forall a b. (a -> b) -> Conditionals m a -> Conditionals m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> Conditionals m a -> Conditionals m b
Functor, forall a. a -> Conditionals m a
forall a b.
Conditionals m a -> Conditionals m b -> Conditionals m a
forall a b.
Conditionals m a -> Conditionals m b -> Conditionals m b
forall a b.
Conditionals m (a -> b) -> Conditionals m a -> Conditionals m b
forall a b c.
(a -> b -> c)
-> Conditionals m a -> Conditionals m b -> Conditionals 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 {m :: * -> *}. Applicative m => Functor (Conditionals m)
forall (m :: * -> *) a. Applicative m => a -> Conditionals m a
forall (m :: * -> *) a b.
Applicative m =>
Conditionals m a -> Conditionals m b -> Conditionals m a
forall (m :: * -> *) a b.
Applicative m =>
Conditionals m a -> Conditionals m b -> Conditionals m b
forall (m :: * -> *) a b.
Applicative m =>
Conditionals m (a -> b) -> Conditionals m a -> Conditionals m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> Conditionals m a -> Conditionals m b -> Conditionals m c
<* :: forall a b.
Conditionals m a -> Conditionals m b -> Conditionals m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
Conditionals m a -> Conditionals m b -> Conditionals m a
*> :: forall a b.
Conditionals m a -> Conditionals m b -> Conditionals m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
Conditionals m a -> Conditionals m b -> Conditionals m b
liftA2 :: forall a b c.
(a -> b -> c)
-> Conditionals m a -> Conditionals m b -> Conditionals m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c)
-> Conditionals m a -> Conditionals m b -> Conditionals m c
<*> :: forall a b.
Conditionals m (a -> b) -> Conditionals m a -> Conditionals m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
Conditionals m (a -> b) -> Conditionals m a -> Conditionals m b
pure :: forall a. a -> Conditionals m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> Conditionals m a
Applicative, forall a. a -> Conditionals m a
forall a b.
Conditionals m a -> Conditionals m b -> Conditionals m b
forall a b.
Conditionals m a -> (a -> Conditionals m b) -> Conditionals m b
forall {m :: * -> *}. Monad m => Applicative (Conditionals m)
forall (m :: * -> *) a. Monad m => a -> Conditionals m a
forall (m :: * -> *) a b.
Monad m =>
Conditionals m a -> Conditionals m b -> Conditionals m b
forall (m :: * -> *) a b.
Monad m =>
Conditionals m a -> (a -> Conditionals m b) -> Conditionals 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 -> Conditionals m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> Conditionals m a
>> :: forall a b.
Conditionals m a -> Conditionals m b -> Conditionals m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
Conditionals m a -> Conditionals m b -> Conditionals m b
>>= :: forall a b.
Conditionals m a -> (a -> Conditionals m b) -> Conditionals m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
Conditionals m a -> (a -> Conditionals m b) -> Conditionals m b
Monad, forall a. IO a -> Conditionals m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall {m :: * -> *}. MonadIO m => Monad (Conditionals m)
forall (m :: * -> *) a. MonadIO m => IO a -> Conditionals m a
liftIO :: forall a. IO a -> Conditionals m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> Conditionals m a
MonadIO, MonadTester testcase term, String -> Conditionals m ()
forall (m :: * -> *).
Monad m
-> (String -> m ())
-> (String -> m ())
-> (String -> m ())
-> MonadTerminal m
forall {m :: * -> *}. MonadTerminal m => Monad (Conditionals m)
forall (m :: * -> *).
MonadTerminal m =>
String -> Conditionals m ()
putTemp :: String -> Conditionals m ()
$cputTemp :: forall (m :: * -> *).
MonadTerminal m =>
String -> Conditionals m ()
putLine :: String -> Conditionals m ()
$cputLine :: forall (m :: * -> *).
MonadTerminal m =>
String -> Conditionals m ()
putText :: String -> Conditionals m ()
$cputText :: forall (m :: * -> *).
MonadTerminal m =>
String -> Conditionals m ()
MonadTerminal)
instance MonadTrans Conditionals where
  lift :: forall (m :: * -> *) a. Monad m => m a -> Conditionals m a
lift = forall (m :: * -> *) a. m a -> Conditionals m a
Conditionals
instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
  MonadPruner (Term fun) norm (Conditionals m) where
  normaliser :: Conditionals m (Term fun -> norm)
normaliser = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
    Term (WithConstructor fun) -> norm
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
    forall (m :: * -> *) a. Monad m => a -> m a
return (Term (WithConstructor fun) -> norm
norm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall fun. fun -> WithConstructor fun
Normal)
  add :: Prop (Term fun) -> Conditionals m Bool
add Prop (Term fun)
prop = do
    Bool
redundant <- forall fun norm (m :: * -> *).
(Typed fun, Ord fun, PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
Prop (Term fun) -> Conditionals m Bool
conditionallyRedundant Prop (Term fun)
prop
    if Bool
redundant then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False else do
      Bool
res <- 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 (forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
Prop.mapFun forall fun. fun -> WithConstructor fun
Normal Prop (Term fun)
prop))
      forall fun norm (m :: * -> *).
(Typed fun, Ord fun, PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
Prop (Term fun) -> Conditionals m ()
considerConditionalising Prop (Term fun)
prop
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
res

  decodeNormalForm :: (Type -> Maybe (Term fun))
-> norm -> Conditionals m (Maybe (Term fun))
decodeNormalForm Type -> Maybe (Term fun)
hole norm
t = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
    Maybe (Term (WithConstructor fun))
t <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
(Type -> Maybe term) -> norm -> m (Maybe term)
decodeNormalForm (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 fun. fun -> WithConstructor fun
Normal) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Term fun)
hole) norm
t
    let f :: WithConstructor a -> Maybe a
f (Normal a
x) = forall a. a -> Maybe a
Just a
x
        f WithConstructor a
_ = forall a. Maybe a
Nothing
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe (Term (WithConstructor fun))
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f g. (f -> g) -> Term f -> Term g
Term.mapFun forall {a}. WithConstructor a -> Maybe a
f

conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe
conditionalsUniverse :: forall fun.
(Typed fun, Predicate fun) =>
[Type] -> [fun] -> Universe
conditionalsUniverse [Type]
tys [fun]
funs =
  forall a. Typed a => [a] -> Universe
universe forall a b. (a -> b) -> a -> b
$
    [Type]
tys forall a. [a] -> [a] -> [a]
++
    (forall a b. (a -> b) -> [a] -> [b]
map forall a. Typed a => a -> Type
typ forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map forall fun. fun -> WithConstructor fun
Normal [fun]
funs forall a. [a] -> [a] -> [a]
++
      [ forall fun. fun -> Type -> WithConstructor fun
Constructor fun
pred Type
clas_test_case | fun
pred <- [fun]
funs, Predicate{[fun]
Type
Term fun
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Type
clas_selectors :: forall fun. Classification fun -> [fun]
clas_true :: Term fun
clas_selectors :: [fun]
clas_test_case :: Type
..} <- [forall fun. Predicate fun => fun -> Classification fun
classify fun
pred] ])

runConditionals ::
  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
  [fun] -> Conditionals m a -> m a
runConditionals :: forall fun norm (m :: * -> *) a.
(PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[fun] -> Conditionals m a -> m a
runConditionals [fun]
preds Conditionals m a
mx =
  forall {m :: * -> *} {a}. Conditionals m a -> m a
run (forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall fun norm (m :: * -> *).
(PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
fun -> Conditionals m ()
considerPredicate [fun]
preds forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Conditionals m a
mx)
  where
    run :: Conditionals m a -> m a
run (Conditionals m a
mx) = m a
mx

class Predicate fun where
  classify :: fun -> Classification fun

data Classification fun =
    Predicate { forall fun. Classification fun -> [fun]
clas_selectors :: [fun], forall fun. Classification fun -> Type
clas_test_case :: Type, forall fun. Classification fun -> Term fun
clas_true :: Term fun }
  | Selector { forall fun. Classification fun -> Int
clas_index :: Int, forall fun. Classification fun -> fun
clas_pred :: fun, clas_test_case :: Type }
  | Function
  deriving (Classification fun -> Classification fun -> Bool
forall fun.
Eq fun =>
Classification fun -> Classification fun -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Classification fun -> Classification fun -> Bool
$c/= :: forall fun.
Eq fun =>
Classification fun -> Classification fun -> Bool
== :: Classification fun -> Classification fun -> Bool
$c== :: forall fun.
Eq fun =>
Classification fun -> Classification fun -> Bool
Eq, Classification fun -> Classification fun -> Bool
Classification fun -> Classification fun -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {fun}. Ord fun => Eq (Classification fun)
forall fun.
Ord fun =>
Classification fun -> Classification fun -> Bool
forall fun.
Ord fun =>
Classification fun -> Classification fun -> Ordering
forall fun.
Ord fun =>
Classification fun -> Classification fun -> Classification fun
min :: Classification fun -> Classification fun -> Classification fun
$cmin :: forall fun.
Ord fun =>
Classification fun -> Classification fun -> Classification fun
max :: Classification fun -> Classification fun -> Classification fun
$cmax :: forall fun.
Ord fun =>
Classification fun -> Classification fun -> Classification fun
>= :: Classification fun -> Classification fun -> Bool
$c>= :: forall fun.
Ord fun =>
Classification fun -> Classification fun -> Bool
> :: Classification fun -> Classification fun -> Bool
$c> :: forall fun.
Ord fun =>
Classification fun -> Classification fun -> Bool
<= :: Classification fun -> Classification fun -> Bool
$c<= :: forall fun.
Ord fun =>
Classification fun -> Classification fun -> Bool
< :: Classification fun -> Classification fun -> Bool
$c< :: forall fun.
Ord fun =>
Classification fun -> Classification fun -> Bool
compare :: Classification fun -> Classification fun -> Ordering
$ccompare :: forall fun.
Ord fun =>
Classification fun -> Classification fun -> Ordering
Ord, forall a b. a -> Classification b -> Classification a
forall a b. (a -> b) -> Classification a -> Classification 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 -> Classification b -> Classification a
$c<$ :: forall a b. a -> Classification b -> Classification a
fmap :: forall a b. (a -> b) -> Classification a -> Classification b
$cfmap :: forall a b. (a -> b) -> Classification a -> Classification b
Functor)

data WithConstructor fun =
    Constructor fun Type
  | Normal fun
  deriving (WithConstructor fun -> WithConstructor fun -> Bool
forall fun.
Eq fun =>
WithConstructor fun -> WithConstructor fun -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WithConstructor fun -> WithConstructor fun -> Bool
$c/= :: forall fun.
Eq fun =>
WithConstructor fun -> WithConstructor fun -> Bool
== :: WithConstructor fun -> WithConstructor fun -> Bool
$c== :: forall fun.
Eq fun =>
WithConstructor fun -> WithConstructor fun -> Bool
Eq, WithConstructor fun -> WithConstructor fun -> Bool
WithConstructor fun -> WithConstructor fun -> Ordering
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {fun}. Ord fun => Eq (WithConstructor fun)
forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> Bool
forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> Ordering
forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> WithConstructor fun
min :: WithConstructor fun -> WithConstructor fun -> WithConstructor fun
$cmin :: forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> WithConstructor fun
max :: WithConstructor fun -> WithConstructor fun -> WithConstructor fun
$cmax :: forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> WithConstructor fun
>= :: WithConstructor fun -> WithConstructor fun -> Bool
$c>= :: forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> Bool
> :: WithConstructor fun -> WithConstructor fun -> Bool
$c> :: forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> Bool
<= :: WithConstructor fun -> WithConstructor fun -> Bool
$c<= :: forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> Bool
< :: WithConstructor fun -> WithConstructor fun -> Bool
$c< :: forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> Bool
compare :: WithConstructor fun -> WithConstructor fun -> Ordering
$ccompare :: forall fun.
Ord fun =>
WithConstructor fun -> WithConstructor fun -> Ordering
Ord)

instance Sized fun => Sized (WithConstructor fun) where
  size :: WithConstructor fun -> Int
size Constructor{} = Int
0
  size (Normal fun
f) = forall a. Sized a => a -> Int
size fun
f

instance Pretty fun => Pretty (WithConstructor fun) where
  pPrintPrec :: PrettyLevel -> Rational -> WithConstructor fun -> Doc
pPrintPrec PrettyLevel
l Rational
p (Constructor fun
f Type
_) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun
f Doc -> Doc -> Doc
<#> String -> Doc
text String
"_con"
  pPrintPrec PrettyLevel
l Rational
p (Normal fun
f) = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
l Rational
p fun
f

instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where
  termStyle :: WithConstructor fun -> TermStyle
termStyle (Constructor fun
_ Type
_) = TermStyle
curried
  termStyle (Normal fun
f) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun
f

instance (Predicate fun, Background fun) => Background (WithConstructor fun) where
  background :: WithConstructor fun -> [Prop (Term (WithConstructor fun))]
background (Normal fun
f) = forall a b. (a -> b) -> [a] -> [b]
map (forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
Prop.mapFun forall fun. fun -> WithConstructor fun
Normal) (forall f. Background f => f -> [Prop (Term f)]
background fun
f)
  background WithConstructor fun
_ = []

instance Typed fun => Typed (WithConstructor fun) where
  typ :: WithConstructor fun -> Type
typ (Constructor fun
pred Type
ty) =
    [Type] -> Type -> Type
arrowType (Type -> [Type]
typeArgs (forall a. Typed a => a -> Type
typ fun
pred)) Type
ty
  typ (Normal fun
f) = forall a. Typed a => a -> Type
typ fun
f
  otherTypesDL :: WithConstructor fun -> DList Type
otherTypesDL (Constructor fun
pred Type
_) = forall a. Typed a => a -> DList Type
typesDL fun
pred
  otherTypesDL (Normal fun
f) = forall a. Typed a => a -> DList Type
otherTypesDL fun
f
  typeSubst_ :: (Var -> Builder TyCon)
-> WithConstructor fun -> WithConstructor fun
typeSubst_ Var -> Builder TyCon
sub (Constructor fun
pred Type
ty) = forall fun. fun -> Type -> WithConstructor fun
Constructor (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub fun
pred) (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Type
ty)
  typeSubst_ Var -> Builder TyCon
sub (Normal fun
f) = forall fun. fun -> WithConstructor fun
Normal (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub fun
f)

predType :: TyCon -> [Type] -> Type
predType :: TyCon -> [Type] -> Type
predType TyCon
name [Type]
tys =
  forall a. Build a => a -> Term (BuildFun a)
Twee.build (forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
Twee.app (forall f. Labelled f => f -> Fun f
Twee.fun TyCon
name) [Type]
tys)

considerPredicate ::
  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
  fun -> Conditionals m ()
considerPredicate :: forall fun norm (m :: * -> *).
(PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
fun -> Conditionals m ()
considerPredicate fun
f =
  case forall fun. Predicate fun => fun -> Classification fun
classify fun
f of
    Predicate [fun]
sels Type
ty Term fun
true -> do
      let
        x :: Term f
x = forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
0)
        eqns :: [Prop (Term (WithConstructor fun))]
eqns =
          [forall f. f -> Term f
Fun (forall fun. fun -> Type -> WithConstructor fun
Constructor fun
f Type
ty) forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. f -> Term f
Fun (forall fun. fun -> WithConstructor fun
Normal fun
sel) forall f. Term f -> Term f -> Term f
:$: forall {f}. Term f
x | fun
sel <- [fun]
sels] forall a. a -> a -> Prop a
=== forall {f}. Term f
x,
           forall f. f -> Term f
Fun (forall fun. fun -> WithConstructor fun
Normal fun
f) forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. f -> Term f
Fun (forall fun. fun -> WithConstructor fun
Normal fun
sel) forall f. Term f -> Term f -> Term f
:$: forall {f}. Term f
x | fun
sel <- [fun]
sels] forall a. a -> a -> Prop a
=== forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall fun. fun -> WithConstructor fun
Normal Term fun
true]
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add) [Prop (Term (WithConstructor fun))]
eqns
    Classification fun
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

considerConditionalising ::
  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
  Prop (Term fun) -> Conditionals m ()
considerConditionalising :: forall fun norm (m :: * -> *).
(Typed fun, Ord fun, PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
Prop (Term fun) -> Conditionals m ()
considerConditionalising ([Equation (Term fun)]
lhs :=>: Term fun
t :=: Term fun
u) = do
  Term fun -> norm
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
  -- If we have discovered that "somePredicate x_1 x_2 ... x_n = True"
  -- we should add the axiom "get_x_n (toSomePredicate x_1 x_2 ... x_n) = x_n"
  -- to the set of known equations
  case Term fun
t of
    Fun fun
f :@: [Term fun]
ts | Predicate{[fun]
Type
Term fun
clas_true :: Term fun
clas_test_case :: Type
clas_selectors :: [fun]
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Type
clas_selectors :: forall fun. Classification fun -> [fun]
..} <- forall fun. Predicate fun => fun -> Classification fun
classify fun
f -> -- It is an interesting predicate, i.e. it was added by the user
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Term fun -> norm
norm Term fun
u forall a. Eq a => a -> a -> Bool
== Term fun -> norm
norm Term fun
clas_true) forall a b. (a -> b) -> a -> b
$
        forall fun norm (m :: * -> *).
(PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()
addPredicate [Equation (Term fun)]
lhs fun
f [Term fun]
ts
    Term fun
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

conditionallyRedundant ::
  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
  Prop (Term fun) -> Conditionals m Bool
conditionallyRedundant :: forall fun norm (m :: * -> *).
(Typed fun, Ord fun, PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
Prop (Term fun) -> Conditionals m Bool
conditionallyRedundant ([Equation (Term fun)]
lhs :=>: Term fun
t :=: Term fun
u) = do
  norm
t' <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
term -> m norm
normalise Term fun
t
  norm
u' <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
term -> m norm
normalise Term fun
u
  forall fun norm (m :: * -> *).
(Typed fun, Ord fun, PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[Equation (Term fun)]
-> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool
conditionallyRedundant' [Equation (Term fun)]
lhs Term fun
t Term fun
u norm
t' norm
u'

conditionallyRedundant' ::
  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
  [Equation (Term fun)] -> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool
conditionallyRedundant' :: forall fun norm (m :: * -> *).
(Typed fun, Ord fun, PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[Equation (Term fun)]
-> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool
conditionallyRedundant' [Equation (Term fun)]
lhs Term fun
t Term fun
u norm
t' norm
u' = do
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Ord a => [a] -> [a]
usort (forall f a. Symbolic f a => a -> [f]
funs [Term fun
t, Term fun
u])) forall a b. (a -> b) -> a -> b
$ \fun
f ->
    case forall fun. Predicate fun => fun -> Classification fun
classify fun
f of
      Selector{fun
Int
Type
clas_test_case :: Type
clas_pred :: fun
clas_index :: Int
clas_pred :: forall fun. Classification fun -> fun
clas_index :: forall fun. Classification fun -> Int
clas_test_case :: forall fun. Classification fun -> Type
..} -> do
        let
          Predicate{[fun]
Type
Term fun
clas_true :: Term fun
clas_test_case :: Type
clas_selectors :: [fun]
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Type
clas_selectors :: forall fun. Classification fun -> [fun]
..} = forall fun. Predicate fun => fun -> Classification fun
classify fun
clas_pred
          tys :: [Type]
tys = Type -> [Type]
typeArgs (forall a. Typed a => a -> Type
typ fun
clas_pred)
          argss :: [[Term fun]]
argss = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ [ Term fun
arg | Term fun
arg <- forall f a. Symbolic f a => a -> [Term f]
terms [Term fun
t, Term fun
u] forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall f. Term f -> [Term f]
subterms, forall a. Typed a => a -> Type
typ Term fun
arg forall a. Eq a => a -> a -> Bool
== Type
ty ] | Type
ty <- [Type]
tys ]
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [[Term fun]]
argss forall a b. (a -> b) -> a -> b
$ \[Term fun]
args -> do
          Term fun -> norm
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
          let p :: Term fun
p = forall f. f -> Term f
Fun fun
clas_pred forall {f}. Term f -> [Term f] -> Term f
:@: [Term fun]
args
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Term fun -> norm
norm Term fun
p forall a. Eq a => a -> a -> Bool
== Term fun -> norm
norm Term fun
clas_true) forall a b. (a -> b) -> a -> b
$ do
            forall fun norm (m :: * -> *).
(PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()
addPredicate [Equation (Term fun)]
lhs fun
clas_pred [Term fun]
args
      Classification fun
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

  norm
t'' <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
term -> m norm
normalise Term fun
t
  norm
u'' <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
term -> m norm
normalise Term fun
u
  if norm
t'' forall a. Eq a => a -> a -> Bool
== norm
u'' then
    forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
   else if norm
t'' forall a. Eq a => a -> a -> Bool
== norm
t' Bool -> Bool -> Bool
&& norm
u'' forall a. Eq a => a -> a -> Bool
== norm
u' then
     forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    else
     forall fun norm (m :: * -> *).
(Typed fun, Ord fun, PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[Equation (Term fun)]
-> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool
conditionallyRedundant' [Equation (Term fun)]
lhs Term fun
t Term fun
u norm
t'' norm
u''

addPredicate ::
  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>
  [Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()
addPredicate :: forall fun norm (m :: * -> *).
(PrettyTerm fun, Ord norm,
 MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun,
 MonadTerminal m) =>
[Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()
addPredicate [Equation (Term fun)]
lhs fun
f [Term fun]
ts = do
  let Predicate{[fun]
Type
Term fun
clas_true :: Term fun
clas_test_case :: Type
clas_selectors :: [fun]
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Type
clas_selectors :: forall fun. Classification fun -> [fun]
..} = forall fun. Predicate fun => fun -> Classification fun
classify fun
f
      ts' :: [Term (WithConstructor fun)]
ts' = forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall fun. fun -> WithConstructor fun
Normal) [Term fun]
ts
      lhs' :: [Equation (Term (WithConstructor fun))]
lhs' = 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 fun. fun -> WithConstructor fun
Normal)) [Equation (Term fun)]
lhs
      -- The "to_p x1 x2 ... xm" term
      construction :: Term (WithConstructor fun)
construction = forall f. f -> Term f
Fun (forall fun. fun -> Type -> WithConstructor fun
Constructor fun
f Type
clas_test_case) forall {f}. Term f -> [Term f] -> Term f
:@: [Term (WithConstructor fun)]
ts'
      -- The "p_n (to_p x1 x2 ... xn ... xm) = xn"
      -- equations
      equations :: [Prop (Term (WithConstructor fun))]
equations = [ [Equation (Term (WithConstructor fun))]
lhs' forall a. [Equation a] -> Equation a -> Prop a
:=>: forall f. f -> Term f
Fun (forall fun. fun -> WithConstructor fun
Normal ([fun]
clas_selectors forall a. [a] -> Int -> a
!! Int
i)) forall f. Term f -> Term f -> Term f
:$: Term (WithConstructor fun)
construction forall a. a -> a -> Equation a
:=: Term (WithConstructor fun)
x | (Term (WithConstructor fun)
x, Int
i) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Term (WithConstructor fun)]
ts' [Int
0..]]

  -- Declare the relevant equations as axioms
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add) [Prop (Term (WithConstructor fun))]
equations

conditionalise :: (PrettyTerm fun, Typed fun, Ord fun, Predicate fun) => Prop (Term fun) -> Prop (Term fun)
conditionalise :: forall fun.
(PrettyTerm fun, Typed fun, Ord fun, Predicate fun) =>
Prop (Term fun) -> Prop (Term fun)
conditionalise ([Equation (Term fun)]
lhs :=>: Term fun
t :=: Term fun
u) =
  forall {f}.
(Predicate f, Ord f, Typed f) =>
[Equation (Term f)] -> Term f -> Term f -> Prop (Term f)
go [Equation (Term fun)]
lhs Term fun
t Term fun
u
  where
    -- Replace one predicate with a conditional
    go :: [Equation (Term f)] -> Term f -> Term f -> Prop (Term f)
go [Equation (Term f)]
lhs Term f
t Term f
u =
      case [ (f
p, Var
x, [f]
clas_selectors, Term f
clas_true) | Fun f
f :$: Var Var
x <- forall f. Term f -> [Term f]
subterms Term f
t forall a. [a] -> [a] -> [a]
++ forall f. Term f -> [Term f]
subterms Term f
u, Selector Int
_ f
p Type
_ <- [forall fun. Predicate fun => fun -> Classification fun
classify f
f], Predicate{[f]
Type
Term f
clas_test_case :: Type
clas_true :: Term f
clas_selectors :: [f]
clas_true :: forall fun. Classification fun -> Term fun
clas_test_case :: forall fun. Classification fun -> Type
clas_selectors :: forall fun. Classification fun -> [fun]
..} <- [forall fun. Predicate fun => fun -> Classification fun
classify f
p] ] of
        [] -> forall a. Ord a => [a] -> [a]
sort [Equation (Term f)]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: Term f
t forall a. a -> a -> Equation a
:=: Term f
u
        ((f
p, Var
x, [f]
sels, Term f
true):[(f, Var, [f], Term f)]
_) ->
          let
            n :: Int
n = forall f a. Symbolic f a => a -> Int
freeVar [Term f
t, Term f
u]
            tys :: [Type]
tys = Type -> [Type]
typeArgs (forall a. Typed a => a -> Type
typ f
p)
            xs :: [Term f]
xs = forall a b. (a -> b) -> [a] -> [b]
map forall f. Var -> Term f
Var (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Int -> Var
V [Type]
tys [Int
n..])
            subs :: [(Term f, Term f)]
subs = [(forall f. f -> Term f
Fun ([f]
sels forall a. [a] -> Int -> a
!! Int
i) forall f. Term f -> Term f -> Term f
:$: forall f. Var -> Term f
Var Var
x, forall {f}. [Term f]
xs forall a. [a] -> Int -> a
!! Int
i) | Int
i <- [Int
0..forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tysforall a. Num a => a -> a -> a
-Int
1]]
          in
            [Equation (Term f)] -> Term f -> Term f -> Prop (Term f)
go ((forall f. f -> Term f
Fun f
p forall {f}. Term f -> [Term f] -> Term f
:@: forall {f}. [Term f]
xs forall a. a -> a -> Equation a
:=: Term f
true)forall a. a -> [a] -> [a]
:[Equation (Term f)]
lhs) (forall {t :: * -> *} {f}.
(Foldable t, Eq f) =>
t (Term f, Term f) -> Term f -> Term f
replaceMany forall {f}. [(Term f, Term f)]
subs Term f
t) (forall {t :: * -> *} {f}.
(Foldable t, Eq f) =>
t (Term f, Term f) -> Term f -> Term f
replaceMany forall {f}. [(Term f, Term f)]
subs Term f
u)

    replace :: Term f -> Term f -> Term f -> Term f
replace Term f
from Term f
to Term f
t
      | Term f
t forall a. Eq a => a -> a -> Bool
== Term f
from = Term f
to
    replace Term f
from Term f
to (Term f
t :$: Term f
u) =
      Term f -> Term f -> Term f -> Term f
replace Term f
from Term f
to Term f
t forall f. Term f -> Term f -> Term f
:$: Term f -> Term f -> Term f -> Term f
replace Term f
from Term f
to Term f
u
    replace Term f
_ Term f
_ (Var Var
x) = forall f. Var -> Term f
Var Var
x
    replace Term f
_ Term f
_ (Fun f
f) = forall f. f -> Term f
Fun f
f

    replaceMany :: t (Term f, Term f) -> Term f -> Term f
replaceMany t (Term f, Term f)
subs Term f
t =
      forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall {f}. Eq f => Term f -> Term f -> Term f -> Term f
replace) Term f
t t (Term f, Term f)
subs