-- Pruning support for partial application and the like.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-}
module QuickSpec.Internal.Pruning.PartialApplication where

import QuickSpec.Internal.Term as Term
import QuickSpec.Internal.Type
import QuickSpec.Internal.Pruning.Background hiding (Pruner)
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Prop as Prop
import QuickSpec.Internal.Terminal
import QuickSpec.Internal.Testing
import Control.Monad.IO.Class
import Control.Monad.Trans.Class

data PartiallyApplied f =
    -- A partially-applied function symbol.
    -- The Int describes how many arguments the function expects.
    Partial f Int
    -- The ($) operator, for oversaturated applications.
    -- The type argument is the type of the first argument to ($).
  | Apply Type
  deriving (PartiallyApplied f -> PartiallyApplied f -> Bool
forall f. Eq f => PartiallyApplied f -> PartiallyApplied f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PartiallyApplied f -> PartiallyApplied f -> Bool
$c/= :: forall f. Eq f => PartiallyApplied f -> PartiallyApplied f -> Bool
== :: PartiallyApplied f -> PartiallyApplied f -> Bool
$c== :: forall f. Eq f => PartiallyApplied f -> PartiallyApplied f -> Bool
Eq, PartiallyApplied f -> PartiallyApplied f -> Bool
PartiallyApplied f -> PartiallyApplied f -> 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 {f}. Ord f => Eq (PartiallyApplied f)
forall f. Ord f => PartiallyApplied f -> PartiallyApplied f -> Bool
forall f.
Ord f =>
PartiallyApplied f -> PartiallyApplied f -> Ordering
forall f.
Ord f =>
PartiallyApplied f -> PartiallyApplied f -> PartiallyApplied f
min :: PartiallyApplied f -> PartiallyApplied f -> PartiallyApplied f
$cmin :: forall f.
Ord f =>
PartiallyApplied f -> PartiallyApplied f -> PartiallyApplied f
max :: PartiallyApplied f -> PartiallyApplied f -> PartiallyApplied f
$cmax :: forall f.
Ord f =>
PartiallyApplied f -> PartiallyApplied f -> PartiallyApplied f
>= :: PartiallyApplied f -> PartiallyApplied f -> Bool
$c>= :: forall f. Ord f => PartiallyApplied f -> PartiallyApplied f -> Bool
> :: PartiallyApplied f -> PartiallyApplied f -> Bool
$c> :: forall f. Ord f => PartiallyApplied f -> PartiallyApplied f -> Bool
<= :: PartiallyApplied f -> PartiallyApplied f -> Bool
$c<= :: forall f. Ord f => PartiallyApplied f -> PartiallyApplied f -> Bool
< :: PartiallyApplied f -> PartiallyApplied f -> Bool
$c< :: forall f. Ord f => PartiallyApplied f -> PartiallyApplied f -> Bool
compare :: PartiallyApplied f -> PartiallyApplied f -> Ordering
$ccompare :: forall f.
Ord f =>
PartiallyApplied f -> PartiallyApplied f -> Ordering
Ord, forall a b. a -> PartiallyApplied b -> PartiallyApplied a
forall a b. (a -> b) -> PartiallyApplied a -> PartiallyApplied 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 -> PartiallyApplied b -> PartiallyApplied a
$c<$ :: forall a b. a -> PartiallyApplied b -> PartiallyApplied a
fmap :: forall a b. (a -> b) -> PartiallyApplied a -> PartiallyApplied b
$cfmap :: forall a b. (a -> b) -> PartiallyApplied a -> PartiallyApplied b
Functor)

instance Sized f => Sized (PartiallyApplied f) where
  size :: PartiallyApplied f -> Int
size (Partial f
f Int
_) = forall a. Sized a => a -> Int
size f
f
  size (Apply Type
_) = Int
1

instance Arity (PartiallyApplied f) where
  arity :: PartiallyApplied f -> Int
arity (Partial f
_ Int
n) = Int
n
  arity (Apply Type
_) = Int
2

instance Pretty f => Pretty (PartiallyApplied f) where
  pPrint :: PartiallyApplied f -> Doc
pPrint (Partial f
f Int
n) = forall a. Pretty a => a -> Doc
pPrint f
f Doc -> Doc -> Doc
<#> String -> Doc
text String
"@" Doc -> Doc -> Doc
<#> forall a. Pretty a => a -> Doc
pPrint Int
n
  pPrint (Apply Type
_) = String -> Doc
text String
"$"

instance PrettyTerm f => PrettyTerm (PartiallyApplied f) where
  termStyle :: PartiallyApplied f -> TermStyle
termStyle (Partial f
f Int
_) = forall f. PrettyTerm f => f -> TermStyle
termStyle f
f
  termStyle (Apply Type
_) = Int -> TermStyle
infixStyle Int
2

instance Typed f => Typed (PartiallyApplied f) where
  typ :: PartiallyApplied f -> Type
typ (Apply Type
ty) = [Type] -> Type -> Type
arrowType [Type
ty] Type
ty
  typ (Partial f
f Int
_) = forall a. Typed a => a -> Type
typ f
f
  otherTypesDL :: PartiallyApplied f -> DList Type
otherTypesDL (Apply Type
_) = forall a. Monoid a => a
mempty
  otherTypesDL (Partial f
f Int
_) = forall a. Typed a => a -> DList Type
otherTypesDL f
f
  typeSubst_ :: (Var -> Builder TyCon) -> PartiallyApplied f -> PartiallyApplied f
typeSubst_ Var -> Builder TyCon
sub (Apply Type
ty) = forall f. Type -> PartiallyApplied f
Apply (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Type
ty)
  typeSubst_ Var -> Builder TyCon
sub (Partial f
f Int
n) = forall f. f -> Int -> PartiallyApplied f
Partial (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub f
f) Int
n

partial :: f -> Term (PartiallyApplied f)
partial :: forall f. f -> Term (PartiallyApplied f)
partial f
f = forall f. f -> Term f
Fun (forall f. f -> Int -> PartiallyApplied f
Partial f
f Int
0)

total :: Arity f => f -> PartiallyApplied f
total :: forall f. Arity f => f -> PartiallyApplied f
total f
f = forall f. f -> Int -> PartiallyApplied f
Partial f
f (forall f. Arity f => f -> Int
arity f
f)

smartApply ::
  Typed f => Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
smartApply :: forall f.
Typed f =>
Term (PartiallyApplied f)
-> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
smartApply (Fun (Partial f
f Int
n) :@: [Term (PartiallyApplied f)]
ts) Term (PartiallyApplied f)
u =
  forall f. f -> Term f
Fun (forall f. f -> Int -> PartiallyApplied f
Partial f
f (Int
nforall a. Num a => a -> a -> a
+Int
1)) forall {f}. Term f -> [Term f] -> Term f
:@: ([Term (PartiallyApplied f)]
ts forall a. [a] -> [a] -> [a]
++ [Term (PartiallyApplied f)
u])
smartApply Term (PartiallyApplied f)
t Term (PartiallyApplied f)
u = forall f.
Typed f =>
Term (PartiallyApplied f)
-> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
simpleApply Term (PartiallyApplied f)
t Term (PartiallyApplied f)
u

simpleApply ::
  Typed f =>
  Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
simpleApply :: forall f.
Typed f =>
Term (PartiallyApplied f)
-> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
simpleApply Term (PartiallyApplied f)
t Term (PartiallyApplied f)
u =
  forall f. f -> Term f
Fun (forall f. Type -> PartiallyApplied f
Apply (forall a. Typed a => a -> Type
typ Term (PartiallyApplied f)
t)) forall {f}. Term f -> [Term f] -> Term f
:@: [Term (PartiallyApplied f)
t, Term (PartiallyApplied f)
u]

instance (Typed f, Background f) => Background (PartiallyApplied f) where
  background :: PartiallyApplied f -> [Prop (Term (PartiallyApplied f))]
background (Partial f
f Int
_) =
    forall a b. (a -> b) -> [a] -> [b]
map (forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
Prop.mapFun (\f
f -> forall f. f -> Int -> PartiallyApplied f
Partial f
f Int
arity)) (forall f. Background f => f -> [Prop (Term f)]
background f
f) forall a. [a] -> [a] -> [a]
++
    [ forall f.
Typed f =>
Term (PartiallyApplied f)
-> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
simpleApply (Int -> Term (PartiallyApplied f)
partial Int
n) (forall {f}. [Term f]
vs forall a. [a] -> Int -> a
!! Int
n) forall a. a -> a -> Prop a
=== Int -> Term (PartiallyApplied f)
partial (Int
nforall a. Num a => a -> a -> a
+Int
1)
    | Int
n <- [Int
0..Int
arityforall a. Num a => a -> a -> a
-Int
1] ]
    where
      arity :: Int
arity = Type -> Int
typeArity (forall a. Typed a => a -> Type
typ f
f)
      partial :: Int -> Term (PartiallyApplied f)
partial Int
i =
        forall f. f -> Term f
Fun (forall f. f -> Int -> PartiallyApplied f
Partial f
f Int
i) forall {f}. Term f -> [Term f] -> Term f
:@: forall a. Int -> [a] -> [a]
take Int
i forall {f}. [Term f]
vs
      vs :: [Term f]
vs = 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 -> [Type]
typeArgs (forall a. Typed a => a -> Type
typ f
f)) [Int
0..])
  background PartiallyApplied f
_ = []

newtype Pruner fun pruner a =
  Pruner { forall fun (pruner :: * -> *) a. Pruner fun pruner a -> pruner a
run :: pruner a }
  deriving (forall a b. a -> Pruner fun pruner b -> Pruner fun pruner a
forall a b. (a -> b) -> Pruner fun pruner a -> Pruner fun pruner b
forall fun (pruner :: * -> *) a b.
Functor pruner =>
a -> Pruner fun pruner b -> Pruner fun pruner a
forall fun (pruner :: * -> *) a b.
Functor pruner =>
(a -> b) -> Pruner fun pruner a -> Pruner fun pruner 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 pruner b -> Pruner fun pruner a
$c<$ :: forall fun (pruner :: * -> *) a b.
Functor pruner =>
a -> Pruner fun pruner b -> Pruner fun pruner a
fmap :: forall a b. (a -> b) -> Pruner fun pruner a -> Pruner fun pruner b
$cfmap :: forall fun (pruner :: * -> *) a b.
Functor pruner =>
(a -> b) -> Pruner fun pruner a -> Pruner fun pruner b
Functor, forall a. a -> Pruner fun pruner a
forall a b.
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner a
forall a b.
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
forall a b.
Pruner fun pruner (a -> b)
-> Pruner fun pruner a -> Pruner fun pruner b
forall a b c.
(a -> b -> c)
-> Pruner fun pruner a
-> Pruner fun pruner b
-> Pruner fun pruner c
forall {fun} {pruner :: * -> *}.
Applicative pruner =>
Functor (Pruner fun pruner)
forall fun (pruner :: * -> *) a.
Applicative pruner =>
a -> Pruner fun pruner a
forall fun (pruner :: * -> *) a b.
Applicative pruner =>
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner a
forall fun (pruner :: * -> *) a b.
Applicative pruner =>
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
forall fun (pruner :: * -> *) a b.
Applicative pruner =>
Pruner fun pruner (a -> b)
-> Pruner fun pruner a -> Pruner fun pruner b
forall fun (pruner :: * -> *) a b c.
Applicative pruner =>
(a -> b -> c)
-> Pruner fun pruner a
-> Pruner fun pruner b
-> Pruner fun pruner 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 pruner a -> Pruner fun pruner b -> Pruner fun pruner a
$c<* :: forall fun (pruner :: * -> *) a b.
Applicative pruner =>
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner a
*> :: forall a b.
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
$c*> :: forall fun (pruner :: * -> *) a b.
Applicative pruner =>
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
liftA2 :: forall a b c.
(a -> b -> c)
-> Pruner fun pruner a
-> Pruner fun pruner b
-> Pruner fun pruner c
$cliftA2 :: forall fun (pruner :: * -> *) a b c.
Applicative pruner =>
(a -> b -> c)
-> Pruner fun pruner a
-> Pruner fun pruner b
-> Pruner fun pruner c
<*> :: forall a b.
Pruner fun pruner (a -> b)
-> Pruner fun pruner a -> Pruner fun pruner b
$c<*> :: forall fun (pruner :: * -> *) a b.
Applicative pruner =>
Pruner fun pruner (a -> b)
-> Pruner fun pruner a -> Pruner fun pruner b
pure :: forall a. a -> Pruner fun pruner a
$cpure :: forall fun (pruner :: * -> *) a.
Applicative pruner =>
a -> Pruner fun pruner a
Applicative, forall a. a -> Pruner fun pruner a
forall a b.
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
forall a b.
Pruner fun pruner a
-> (a -> Pruner fun pruner b) -> Pruner fun pruner b
forall {fun} {pruner :: * -> *}.
Monad pruner =>
Applicative (Pruner fun pruner)
forall fun (pruner :: * -> *) a.
Monad pruner =>
a -> Pruner fun pruner a
forall fun (pruner :: * -> *) a b.
Monad pruner =>
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
forall fun (pruner :: * -> *) a b.
Monad pruner =>
Pruner fun pruner a
-> (a -> Pruner fun pruner b) -> Pruner fun pruner 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 pruner a
$creturn :: forall fun (pruner :: * -> *) a.
Monad pruner =>
a -> Pruner fun pruner a
>> :: forall a b.
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
$c>> :: forall fun (pruner :: * -> *) a b.
Monad pruner =>
Pruner fun pruner a -> Pruner fun pruner b -> Pruner fun pruner b
>>= :: forall a b.
Pruner fun pruner a
-> (a -> Pruner fun pruner b) -> Pruner fun pruner b
$c>>= :: forall fun (pruner :: * -> *) a b.
Monad pruner =>
Pruner fun pruner a
-> (a -> Pruner fun pruner b) -> Pruner fun pruner b
Monad, forall a. IO a -> Pruner fun pruner a
forall {fun} {pruner :: * -> *}.
MonadIO pruner =>
Monad (Pruner fun pruner)
forall fun (pruner :: * -> *) a.
MonadIO pruner =>
IO a -> Pruner fun pruner a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Pruner fun pruner a
$cliftIO :: forall fun (pruner :: * -> *) a.
MonadIO pruner =>
IO a -> Pruner fun pruner a
MonadIO, MonadTester testcase term, String -> Pruner fun pruner ()
forall {fun} {pruner :: * -> *}.
MonadTerminal pruner =>
Monad (Pruner fun pruner)
forall fun (pruner :: * -> *).
MonadTerminal pruner =>
String -> Pruner fun pruner ()
forall (m :: * -> *).
Monad m
-> (String -> m ())
-> (String -> m ())
-> (String -> m ())
-> MonadTerminal m
putTemp :: String -> Pruner fun pruner ()
$cputTemp :: forall fun (pruner :: * -> *).
MonadTerminal pruner =>
String -> Pruner fun pruner ()
putLine :: String -> Pruner fun pruner ()
$cputLine :: forall fun (pruner :: * -> *).
MonadTerminal pruner =>
String -> Pruner fun pruner ()
putText :: String -> Pruner fun pruner ()
$cputText :: forall fun (pruner :: * -> *).
MonadTerminal pruner =>
String -> Pruner fun pruner ()
MonadTerminal)

instance MonadTrans (Pruner fun) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> Pruner fun m a
lift = forall fun (pruner :: * -> *) a. pruner a -> Pruner fun pruner a
Pruner

instance (PrettyTerm fun, Typed fun, MonadPruner (Term (PartiallyApplied fun)) norm pruner) => MonadPruner (Term fun) norm (Pruner fun pruner) where
  normaliser :: Pruner fun pruner (Term fun -> norm)
normaliser =
    forall fun (pruner :: * -> *) a. pruner a -> Pruner fun pruner a
Pruner forall a b. (a -> b) -> a -> b
$ do
      Term (PartiallyApplied fun) -> norm
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \Term fun
t ->
        Term (PartiallyApplied fun) -> norm
norm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun. Typed fun => Term fun -> Term (PartiallyApplied fun)
encode forall a b. (a -> b) -> a -> b
$ Term fun
t

  add :: Prop (Term fun) -> Pruner fun pruner Bool
add Prop (Term fun)
prop =
    forall fun (pruner :: * -> *) a. pruner a -> Pruner fun pruner a
Pruner forall a b. (a -> b) -> a -> b
$ do
      forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add (forall fun. Typed fun => Term fun -> Term (PartiallyApplied fun)
encode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall fun a. Symbolic fun a => a -> a
canonicalise Prop (Term fun)
prop)

  decodeNormalForm :: (Type -> Maybe (Term fun))
-> norm -> Pruner fun pruner (Maybe (Term fun))
decodeNormalForm Type -> Maybe (Term fun)
hole norm
t =
    forall fun (pruner :: * -> *) a. pruner a -> Pruner fun pruner a
Pruner forall a b. (a -> b) -> a -> b
$ do
      Maybe (Term (PartiallyApplied 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 a b c. (a -> b -> c) -> b -> a -> c
flip forall f. f -> Int -> PartiallyApplied f
Partial Int
0)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Term fun)
hole) norm
t
      let f :: PartiallyApplied f -> OrId f
f (Partial f
x Int
_) = forall f. f -> OrId f
NotId f
x
          f (Apply Type
_) = forall f. OrId f
Id
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe (Term (PartiallyApplied fun))
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall f. Term (OrId f) -> Maybe (Term f)
eliminateId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f g. (f -> g) -> Term f -> Term g
Term.mapFun forall {f}. PartiallyApplied f -> OrId f
f

encode :: Typed fun => Term fun -> Term (PartiallyApplied fun)
encode :: forall fun. Typed fun => Term fun -> Term (PartiallyApplied fun)
encode (Var Var
x) = forall f. Var -> Term f
Var Var
x
encode (Fun fun
f) = forall f. f -> Term (PartiallyApplied f)
partial fun
f
encode (Term fun
t :$: Term fun
u) = forall f.
Typed f =>
Term (PartiallyApplied f)
-> Term (PartiallyApplied f) -> Term (PartiallyApplied f)
smartApply (forall fun. Typed fun => Term fun -> Term (PartiallyApplied fun)
encode Term fun
t) (forall fun. Typed fun => Term fun -> Term (PartiallyApplied fun)
encode Term fun
u)