{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleContexts, PatternGuards, CPP #-}
module QuickSpec.Internal.Explore where

import QuickSpec.Internal.Explore.Polymorphic
import QuickSpec.Internal.Testing
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Term
import QuickSpec.Internal.Type
import QuickSpec.Internal.Utils
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Terminal
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.State.Strict
import Text.Printf
#if! MIN_VERSION_base(4,9,0)
import Data.Semigroup(Semigroup(..))
#endif
import Data.List

newtype Enumerator a = Enumerator { forall a. Enumerator a -> Int -> [[a]] -> [a]
enumerate :: Int -> [[a]] -> [a] }

-- N.B. order matters!
-- Later enumerators get to see terms which were generated by earlier ones.
instance Semigroup (Enumerator a) where
  Enumerator a
e1 <> :: Enumerator a -> Enumerator a -> Enumerator a
<> Enumerator a
e2 = forall a. (Int -> [[a]] -> [a]) -> Enumerator a
Enumerator forall a b. (a -> b) -> a -> b
$ \Int
n [[a]]
tss ->
    let us :: [a]
us = forall a. Enumerator a -> Int -> [[a]] -> [a]
enumerate Enumerator a
e1 Int
n [[a]]
tss
        vs :: [a]
vs = forall a. Enumerator a -> Int -> [[a]] -> [a]
enumerate Enumerator a
e2 Int
n (forall a. Int -> [a] -> [[a]] -> [[a]]
appendAt Int
n [a]
us [[a]]
tss)
    in [a]
us forall a. [a] -> [a] -> [a]
++ [a]
vs
instance Monoid (Enumerator a) where
  mempty :: Enumerator a
mempty = forall a. (Int -> [[a]] -> [a]) -> Enumerator a
Enumerator (\Int
_ [[a]]
_ -> [])
  mappend :: Enumerator a -> Enumerator a -> Enumerator a
mappend = forall a. Semigroup a => a -> a -> a
(<>)

mapEnumerator :: ([a] -> [a]) -> Enumerator a -> Enumerator a
mapEnumerator :: forall a. ([a] -> [a]) -> Enumerator a -> Enumerator a
mapEnumerator [a] -> [a]
f Enumerator a
e =
  forall a. (Int -> [[a]] -> [a]) -> Enumerator a
Enumerator forall a b. (a -> b) -> a -> b
$ \Int
n [[a]]
tss ->
    [a] -> [a]
f (forall a. Enumerator a -> Int -> [[a]] -> [a]
enumerate Enumerator a
e Int
n [[a]]
tss)

filterEnumerator :: (a -> Bool) -> Enumerator a -> Enumerator a
filterEnumerator :: forall a. (a -> Bool) -> Enumerator a -> Enumerator a
filterEnumerator a -> Bool
p Enumerator a
e =
  forall a. ([a] -> [a]) -> Enumerator a -> Enumerator a
mapEnumerator (forall a. (a -> Bool) -> [a] -> [a]
filter a -> Bool
p) Enumerator a
e

enumerateConstants :: Sized a => [a] -> Enumerator a
enumerateConstants :: forall a. Sized a => [a] -> Enumerator a
enumerateConstants [a]
ts = forall a. (Int -> [[a]] -> [a]) -> Enumerator a
Enumerator (\Int
n [[a]]
_ -> [a
t | a
t <- [a]
ts, forall a. Sized a => a -> Int
size a
t forall a. Eq a => a -> a -> Bool
== Int
n])

enumerateApplications :: Apply a => Enumerator a
enumerateApplications :: forall a. Apply a => Enumerator a
enumerateApplications = forall a. (Int -> [[a]] -> [a]) -> Enumerator a
Enumerator forall a b. (a -> b) -> a -> b
$ \Int
n [[a]]
tss ->
    [ forall a. Poly a -> a
unPoly Poly a
v
    | Int
i <- [Int
0..Int
n],
      a
t <- [[a]]
tss forall a. [a] -> Int -> a
!! Int
i,
      a
u <- [[a]]
tss forall a. [a] -> Int -> a
!! (Int
nforall a. Num a => a -> a -> a
-Int
i),
      Just Poly a
v <- [forall a. Apply a => a -> a -> Maybe a
tryApply (forall a. Typed a => a -> Poly a
poly a
t) (forall a. Typed a => a -> Poly a
poly a
u)] ]

filterUniverse :: Typed f => Universe -> Enumerator (Term f) -> Enumerator (Term f)
filterUniverse :: forall f.
Typed f =>
Universe -> Enumerator (Term f) -> Enumerator (Term f)
filterUniverse Universe
univ Enumerator (Term f)
e =
  forall a. (a -> Bool) -> Enumerator a -> Enumerator a
filterEnumerator (forall fun. Typed fun => Term fun -> Universe -> Bool
`usefulForUniverse` Universe
univ) Enumerator (Term f)
e

sortTerms :: Ord b => (a -> b) -> Enumerator a -> Enumerator a
sortTerms :: forall b a. Ord b => (a -> b) -> Enumerator a -> Enumerator a
sortTerms a -> b
measure Enumerator a
e =
  forall a. ([a] -> [a]) -> Enumerator a -> Enumerator a
mapEnumerator (forall b a. Ord b => (a -> b) -> [a] -> [a]
sortBy' a -> b
measure) Enumerator a
e

quickSpec ::
  (Ord fun, Ord norm, Sized fun, Typed fun, Ord result, PrettyTerm fun,
  MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>
  (Prop (Term fun) -> m ()) ->
  (Term fun -> testcase -> Maybe result) ->
  Int -> Int -> (Type -> VariableUse) -> Universe -> Enumerator (Term fun) -> m ()
quickSpec :: forall fun norm result (m :: * -> *) testcase.
(Ord fun, Ord norm, Sized fun, Typed fun, Ord result,
 PrettyTerm fun, MonadPruner (Term fun) norm m,
 MonadTester testcase (Term fun) m, MonadTerminal m) =>
(Prop (Term fun) -> m ())
-> (Term fun -> testcase -> Maybe result)
-> Int
-> Int
-> (Type -> VariableUse)
-> Universe
-> Enumerator (Term fun)
-> m ()
quickSpec Prop (Term fun) -> m ()
present Term fun -> testcase -> Maybe result
eval Int
maxSize Int
maxCommutativeSize Type -> VariableUse
use Universe
univ Enumerator (Term fun)
enum = do
  let
    state0 :: Polymorphic testcase result fun norm
state0 = forall fun testcase result norm.
(Type -> VariableUse)
-> Universe
-> (Term fun -> Bool)
-> (Term fun -> testcase -> Maybe result)
-> Polymorphic testcase result fun norm
initialState Type -> VariableUse
use Universe
univ (\Term fun
t -> forall a. Sized a => a -> Int
size Term fun
t forall a. Ord a => a -> a -> Bool
<= Int
maxCommutativeSize) Term fun -> testcase -> Maybe result
eval

    loop :: Int
-> Int
-> [[Term fun]]
-> StateT (Polymorphic testcase result fun norm) m ()
loop Int
m Int
n [[Term fun]]
_ | Int
m forall a. Ord a => a -> a -> Bool
> Int
n = forall (m :: * -> *) a. Monad m => a -> m a
return ()
    loop Int
m Int
n [[Term fun]]
tss = do
      forall (m :: * -> *). MonadTerminal m => String -> m ()
putStatus (forall r. PrintfType r => String -> r
printf String
"enumerating terms of size %d" Int
m)
      let
        ts :: [Term fun]
ts = forall a. Enumerator a -> Int -> [[a]] -> [a]
enumerate (forall f.
Typed f =>
Universe -> Enumerator (Term f) -> Enumerator (Term f)
filterUniverse Universe
univ Enumerator (Term fun)
enum) Int
m [[Term fun]]
tss
        total :: Int
total = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term fun]
ts
        consider :: (t, Term fun)
-> StateT (Polymorphic testcase result fun norm) m Bool
consider (t
i, Term fun
t) = do
          forall (m :: * -> *). MonadTerminal m => String -> m ()
putStatus (forall r. PrintfType r => String -> r
printf String
"testing terms of size %d: %d/%d" Int
m t
i Int
total)
          Result fun
res <- forall fun result norm testcase (m :: * -> *).
(PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun,
 Apply (Term fun), MonadTester testcase (Term fun) m,
 MonadPruner (Term fun) norm m, MonadTerminal m) =>
Term fun
-> StateT (Polymorphic testcase result fun norm) m (Result fun)
explore Term fun
t
          forall (m :: * -> *). MonadTerminal m => String -> m ()
putStatus (forall r. PrintfType r => String -> r
printf String
"testing terms of size %d: %d/%d" Int
m t
i Int
total)
          forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prop (Term fun) -> m ()
present (forall fun. Result fun -> [Prop (Term fun)]
result_props Result fun
res)
          case Result fun
res of
            Accepted [Prop (Term fun)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            Rejected [Prop (Term fun)]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      [Term fun]
us <- forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM forall {result} {norm} {testcase} {t}.
(Ord result, Ord norm, MonadTester testcase (Term fun) m,
 MonadPruner (Term fun) norm m, PrintfArg t) =>
(t, Term fun)
-> StateT (Polymorphic testcase result fun norm) m Bool
consider (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1 :: Int ..] [Term fun]
ts)
      forall (m :: * -> *). MonadTerminal m => m ()
clearStatus
      Int
-> Int
-> [[Term fun]]
-> StateT (Polymorphic testcase result fun norm) m ()
loop (Int
mforall a. Num a => a -> a -> a
+Int
1) Int
n (forall a. Int -> [a] -> [[a]] -> [[a]]
appendAt Int
m [Term fun]
us [[Term fun]]
tss)

  forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall {testcase} {norm} {result}.
(MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m,
 Ord result, Ord norm) =>
Int
-> Int
-> [[Term fun]]
-> StateT (Polymorphic testcase result fun norm) m ()
loop Int
0 Int
maxSize (forall a. a -> [a]
repeat [])) forall {norm}. Polymorphic testcase result fun norm
state0

----------------------------------------------------------------------
-- Functions that are not really to do with theory exploration,
-- but are useful for printing the output nicely.
----------------------------------------------------------------------

pPrintSignature :: (Pretty a, Typed a) => [a] -> Doc
pPrintSignature :: forall a. (Pretty a, Typed a) => [a] -> Doc
pPrintSignature [a]
funs =
  String -> Doc
text String
"== Functions ==" Doc -> Doc -> Doc
$$
  [Doc] -> Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map (String, Doc) -> Doc
pPrintDecl [(String, Doc)]
decls)
  where
    decls :: [(String, Doc)]
decls = [ (forall a. Pretty a => a -> String
prettyShow a
f, Type -> Doc
pPrintType (forall a. Typed a => a -> Type
typ a
f)) | a
f <- [a]
funs ]
    maxWidth :: Int
maxWidth = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0forall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(String, Doc)]
decls)
    pad :: String -> Doc
pad String
xs = Int -> Doc -> Doc
nest (Int
maxWidth forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
xs) (String -> Doc
text String
xs)
    pPrintDecl :: (String, Doc) -> Doc
pPrintDecl (String
name, Doc
ty) =
      String -> Doc
pad String
name Doc -> Doc -> Doc
<+> String -> Doc
text String
"::" Doc -> Doc -> Doc
<+> Doc
ty

-- Put an equation that defines the function f into the form f lhs = rhs.
-- An equation defines f if:
--   * it is of the form f lhs = rhs (or vice versa).
--   * f is not a background function.
--   * lhs only contains background functions.
--   * rhs does not contain f.
--   * all vars in rhs appear in lhs
prettyDefinition :: Eq fun => [fun] -> Prop (Term fun) -> Prop (Term fun)
prettyDefinition :: forall fun. Eq fun => [fun] -> Prop (Term fun) -> Prop (Term fun)
prettyDefinition [fun]
cons ([Equation (Term fun)]
lhs :=>: Term fun
t :=: Term fun
u)
  | Just (fun
f, [Term fun]
ts) <- Term fun -> Maybe (fun, [Term fun])
defines Term fun
u,
    fun
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` forall f a. Symbolic f a => a -> [f]
funs Term fun
t,
    forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. Ord a => [a] -> [a]
usort (forall f a. Symbolic f a => a -> [Var]
vars Term fun
t) forall a. Eq a => [a] -> [a] -> [a]
\\ forall f a. Symbolic f a => a -> [Var]
vars [Term fun]
ts) =
    [Equation (Term fun)]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: Term fun
u forall a. a -> a -> Equation a
:=: Term fun
t
    -- In the case where t defines f, the equation is already oriented correctly
  | Bool
otherwise = [Equation (Term fun)]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: Term fun
t forall a. a -> a -> Equation a
:=: Term fun
u
  where
    defines :: Term fun -> Maybe (fun, [Term fun])
defines (Fun fun
f :@: [Term fun]
ts)
      | fun
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [fun]
cons,
        forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [fun]
cons) (forall f a. Symbolic f a => a -> [f]
funs [Term fun]
ts) = forall a. a -> Maybe a
Just (fun
f, [Term fun]
ts)
    defines Term fun
_ = forall a. Maybe a
Nothing

-- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative
prettyAC :: (Eq f, Eq norm) => (Term f -> norm) -> Prop (Term f) -> Prop (Term f)
prettyAC :: forall f norm.
(Eq f, Eq norm) =>
(Term f -> norm) -> Prop (Term f) -> Prop (Term f)
prettyAC Term f -> norm
norm ([Equation (Term f)]
lhs :=>: Fun f
f :@: [Var Var
x, Fun f
f1 :@: [Var Var
y, Var Var
z]] :=: Fun f
f2 :@: [Var Var
y1, Fun f
f3 :@: [Var Var
x1, Var Var
z1]])
  | f
f forall a. Eq a => a -> a -> Bool
== f
f1, f
f1 forall a. Eq a => a -> a -> Bool
== f
f2, f
f2 forall a. Eq a => a -> a -> Bool
== f
f3,
    Var
x forall a. Eq a => a -> a -> Bool
== Var
x1, Var
y forall a. Eq a => a -> a -> Bool
== Var
y1, Var
z forall a. Eq a => a -> a -> Bool
== Var
z1,
    Var
x forall a. Eq a => a -> a -> Bool
/= Var
y, Var
y forall a. Eq a => a -> a -> Bool
/= Var
z, Var
x forall a. Eq a => a -> a -> Bool
/= Var
z,
    Term f -> norm
norm (forall f. f -> Term f
Fun f
f forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. Var -> Term f
Var Var
x, forall f. Var -> Term f
Var Var
y]) forall a. Eq a => a -> a -> Bool
== Term f -> norm
norm (forall f. f -> Term f
Fun f
f forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. Var -> Term f
Var Var
y, forall f. Var -> Term f
Var Var
x]) =
      [Equation (Term f)]
lhs forall a. [Equation a] -> Equation a -> Prop a
:=>: forall f. f -> Term f
Fun f
f forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. f -> Term f
Fun f
f forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. Var -> Term f
Var Var
x, forall f. Var -> Term f
Var Var
y], forall f. Var -> Term f
Var Var
z] forall a. a -> a -> Equation a
:=: forall f. f -> Term f
Fun f
f forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. Var -> Term f
Var Var
x, forall f. f -> Term f
Fun f
f forall {f}. Term f -> [Term f] -> Term f
:@: [forall f. Var -> Term f
Var Var
y, forall f. Var -> Term f
Var Var
z]]
prettyAC Term f -> norm
_ Prop (Term f)
prop = Prop (Term f)
prop

-- Add a type signature when printing the equation x = y.
disambiguatePropType :: Prop (Term fun) -> Doc
disambiguatePropType :: forall fun. Prop (Term fun) -> Doc
disambiguatePropType ([Equation (Term fun)]
_ :=>: (Var Var
x) :=: Var Var
_) =
  String -> Doc
text String
"::" Doc -> Doc -> Doc
<+> Type -> Doc
pPrintType (forall a. Typed a => a -> Type
typ Var
x)
disambiguatePropType Prop (Term fun)
_ = Doc
pPrintEmpty