-- Encode monomorphic types during pruning.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}
module QuickSpec.Internal.Pruning.Types where

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

data Tagged fun =
    Func fun
  | Tag Type
  deriving (Tagged fun -> Tagged fun -> Bool
forall fun. Eq fun => Tagged fun -> Tagged fun -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Tagged fun -> Tagged fun -> Bool
$c/= :: forall fun. Eq fun => Tagged fun -> Tagged fun -> Bool
== :: Tagged fun -> Tagged fun -> Bool
$c== :: forall fun. Eq fun => Tagged fun -> Tagged fun -> Bool
Eq, Tagged fun -> Tagged fun -> Bool
Tagged fun -> Tagged 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 (Tagged fun)
forall fun. Ord fun => Tagged fun -> Tagged fun -> Bool
forall fun. Ord fun => Tagged fun -> Tagged fun -> Ordering
forall fun. Ord fun => Tagged fun -> Tagged fun -> Tagged fun
min :: Tagged fun -> Tagged fun -> Tagged fun
$cmin :: forall fun. Ord fun => Tagged fun -> Tagged fun -> Tagged fun
max :: Tagged fun -> Tagged fun -> Tagged fun
$cmax :: forall fun. Ord fun => Tagged fun -> Tagged fun -> Tagged fun
>= :: Tagged fun -> Tagged fun -> Bool
$c>= :: forall fun. Ord fun => Tagged fun -> Tagged fun -> Bool
> :: Tagged fun -> Tagged fun -> Bool
$c> :: forall fun. Ord fun => Tagged fun -> Tagged fun -> Bool
<= :: Tagged fun -> Tagged fun -> Bool
$c<= :: forall fun. Ord fun => Tagged fun -> Tagged fun -> Bool
< :: Tagged fun -> Tagged fun -> Bool
$c< :: forall fun. Ord fun => Tagged fun -> Tagged fun -> Bool
compare :: Tagged fun -> Tagged fun -> Ordering
$ccompare :: forall fun. Ord fun => Tagged fun -> Tagged fun -> Ordering
Ord, Int -> Tagged fun -> ShowS
forall fun. Show fun => Int -> Tagged fun -> ShowS
forall fun. Show fun => [Tagged fun] -> ShowS
forall fun. Show fun => Tagged fun -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Tagged fun] -> ShowS
$cshowList :: forall fun. Show fun => [Tagged fun] -> ShowS
show :: Tagged fun -> String
$cshow :: forall fun. Show fun => Tagged fun -> String
showsPrec :: Int -> Tagged fun -> ShowS
$cshowsPrec :: forall fun. Show fun => Int -> Tagged fun -> ShowS
Show, Typeable)

instance Arity fun => Arity (Tagged fun) where
  arity :: Tagged fun -> Int
arity (Func fun
f) = forall f. Arity f => f -> Int
arity fun
f
  arity (Tag Type
_) = Int
1

instance Sized fun => Sized (Tagged fun) where
  size :: Tagged fun -> Int
size (Func fun
f) = forall a. Sized a => a -> Int
size fun
f
  size (Tag Type
_) = Int
0

instance Pretty fun => Pretty (Tagged fun) where
  pPrint :: Tagged fun -> Doc
pPrint (Func fun
f) = forall a. Pretty a => a -> Doc
pPrint fun
f
  pPrint (Tag Type
ty) = String -> Doc
text String
"tag[" Doc -> Doc -> Doc
<#> forall a. Pretty a => a -> Doc
pPrint Type
ty Doc -> Doc -> Doc
<#> String -> Doc
text String
"]"

instance PrettyTerm fun => PrettyTerm (Tagged fun) where
  termStyle :: Tagged fun -> TermStyle
termStyle (Func fun
f) = forall f. PrettyTerm f => f -> TermStyle
termStyle fun
f
  termStyle (Tag Type
_) = TermStyle
uncurried

instance Typed fun => Typed (Tagged fun) where
  typ :: Tagged fun -> Type
typ (Func fun
f) = forall a. Typed a => a -> Type
typ fun
f
  typ (Tag Type
ty) = [Type] -> Type -> Type
arrowType [Type
ty] Type
ty

  typeSubst_ :: (Var -> Builder TyCon) -> Tagged fun -> Tagged fun
typeSubst_ Var -> Builder TyCon
sub (Func fun
f) = forall fun. fun -> Tagged fun
Func (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub fun
f)
  typeSubst_ Var -> Builder TyCon
sub (Tag Type
ty) = forall fun. Type -> Tagged fun
Tag (forall a. Typed a => (Var -> Builder TyCon) -> a -> a
typeSubst_ Var -> Builder TyCon
sub Type
ty)

instance EqualsBonus (Tagged fun) where

type TypedTerm fun = Term fun
type UntypedTerm fun = Term (Tagged fun)

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 (UntypedTerm fun) norm pruner) => MonadPruner (TypedTerm fun) norm (Pruner fun pruner) where
  normaliser :: Pruner fun pruner (TypedTerm fun -> norm)
normaliser =
    forall fun (pruner :: * -> *) a. pruner a -> Pruner fun pruner a
Pruner forall a b. (a -> b) -> a -> b
$ do
      UntypedTerm fun -> norm
norm <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
m (term -> norm)
normaliser :: pruner (UntypedTerm fun -> norm)

      -- Note that we don't call addFunction on the functions in the term.
      -- This is because doing so might be expensive, as adding typing
      -- axioms starts the completion algorithm.
      -- This is OK because in encode, we tag all functions and variables
      -- with their types (i.e. we can fall back to the naive type encoding).
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \TypedTerm fun
t ->
        UntypedTerm fun -> norm
norm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun. Typed fun => TypedTerm fun -> UntypedTerm fun
encode forall a b. (a -> b) -> a -> b
$ TypedTerm fun
t

  add :: Prop (TypedTerm fun) -> Pruner fun pruner Bool
add Prop (TypedTerm 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 (forall fun. Typed fun => TypedTerm fun -> UntypedTerm fun
encode forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall fun a. Symbolic fun a => a -> a
canonicalise Prop (TypedTerm fun)
prop))

  decodeNormalForm :: (Type -> Maybe (TypedTerm fun))
-> norm -> Pruner fun pruner (Maybe (TypedTerm fun))
decodeNormalForm Type -> Maybe (TypedTerm fun)
hole norm
t =
    forall fun (pruner :: * -> *) a. pruner a -> Pruner fun pruner a
Pruner forall a b. (a -> b) -> a -> b
$ do
      Maybe (UntypedTerm 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 -> Tagged fun
Func) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (TypedTerm fun)
hole) norm
t
      let f :: Tagged f -> OrId f
f (Func f
x) = forall f. f -> OrId f
NotId f
x
          f (Tag Type
_) = forall f. OrId f
Id
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Maybe (UntypedTerm 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
mapFun forall {f}. Tagged f -> OrId f
f

instance (Typed fun, Arity fun, Background fun) => Background (Tagged fun) where
  background :: Tagged fun -> [Prop (Term (Tagged fun))]
background = forall fun.
(Typed fun, Arity fun, Background fun) =>
Tagged fun -> [Prop (Term (Tagged fun))]
typingAxioms

-- Compute the typing axioms for a function or type tag.
typingAxioms :: (Typed fun, Arity fun, Background fun) =>
  Tagged fun -> [Prop (UntypedTerm fun)]
typingAxioms :: forall fun.
(Typed fun, Arity fun, Background fun) =>
Tagged fun -> [Prop (Term (Tagged fun))]
typingAxioms (Tag Type
ty) =
  [forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag Type
ty (forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag Type
ty forall {f}. Term f
x) forall a. a -> a -> Prop a
=== forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag Type
ty forall {f}. Term f
x]
  where
    x :: Term f
x = forall f. Var -> Term f
Var (Type -> Int -> Var
V Type
ty Int
0)
typingAxioms (Func fun
func) =
  [forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag Type
res UntypedTerm fun
t forall a. a -> a -> Prop a
=== UntypedTerm fun
t] forall a. [a] -> [a] -> [a]
++
  [Int -> Type -> UntypedTerm fun
tagArg Int
i Type
ty forall a. a -> a -> Prop a
=== UntypedTerm fun
t | (Int
i, Type
ty) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Type]
args] forall a. [a] -> [a] -> [a]
++
  forall a b. (a -> b) -> [a] -> [b]
map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall fun. Typed fun => TypedTerm fun -> UntypedTerm fun
encode) (forall f. Background f => f -> [Prop (Term f)]
background fun
func)
  where
    f :: UntypedTerm fun
f = forall f. f -> Term f
Fun (forall fun. fun -> Tagged fun
Func fun
func)
    xs :: [Term f]
xs = forall a. Int -> [a] -> [a]
take Int
n (forall a b. (a -> b) -> [a] -> [b]
map (forall f. Var -> Term f
Var forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Int -> Var
V Type
typeVar) [Int
0..])

    ty :: Type
ty = forall a. Typed a => a -> Type
typ fun
func
    -- Use arity rather than typeArity, so that we can support
    -- partially-applied functions
    n :: Int
n = forall f. Arity f => f -> Int
arity fun
func
    args :: [Type]
args = forall a. Int -> [a] -> [a]
take Int
n (Type -> [Type]
typeArgs Type
ty)
    res :: Type
res = Int -> Type -> Type
typeDrop Int
n Type
ty

    t :: UntypedTerm fun
t = UntypedTerm fun
f forall {f}. Term f -> [Term f] -> Term f
:@: forall {f}. [Term f]
xs

    tagArg :: Int -> Type -> UntypedTerm fun
tagArg Int
i Type
ty =
      UntypedTerm fun
f forall {f}. Term f -> [Term f] -> Term f
:@:
        (forall a. Int -> [a] -> [a]
take Int
i forall {f}. [Term f]
xs forall a. [a] -> [a] -> [a]
++
         [forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag Type
ty (forall {f}. [Term f]
xs forall a. [a] -> Int -> a
!! Int
i)] forall a. [a] -> [a] -> [a]
++
         forall a. Int -> [a] -> [a]
drop (Int
iforall a. Num a => a -> a -> a
+Int
1) forall {f}. [Term f]
xs)

tag :: Type -> UntypedTerm fun -> UntypedTerm fun
tag :: forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag Type
ty UntypedTerm fun
t = forall f. f -> Term f
Fun (forall fun. Type -> Tagged fun
Tag Type
ty) forall f. Term f -> Term f -> Term f
:$: UntypedTerm fun
t

encode :: Typed fun => TypedTerm fun -> UntypedTerm fun
-- We always add type tags; see comment in normaliseMono.
-- In the common case, twee will immediately remove these surplus type tags
-- by rewriting using the typing axioms.
encode :: forall fun. Typed fun => TypedTerm fun -> UntypedTerm fun
encode (Var Var
x) = forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag (forall a. Typed a => a -> Type
typ Var
x) (forall f. Var -> Term f
Var Var
x)
encode (Fun fun
f :@: [Term fun]
ts) =
  forall fun. Type -> UntypedTerm fun -> UntypedTerm fun
tag (Int -> Type -> Type
typeDrop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term fun]
ts) (forall a. Typed a => a -> Type
typ fun
f)) (forall f. f -> Term f
Fun (forall fun. fun -> Tagged fun
Func fun
f) forall {f}. Term f -> [Term f] -> Term f
:@: forall a b. (a -> b) -> [a] -> [b]
map forall fun. Typed fun => TypedTerm fun -> UntypedTerm fun
encode [Term fun]
ts)
encode Term fun
_ = forall a. HasCallStack => String -> a
error String
"partial application"