{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RecordWildCards #-}
module QuickSpec.Internal.Explore.Polymorphic(
module QuickSpec.Internal.Explore.Polymorphic,
Result(..),
Universe(..),
VariableUse(..)) where
import qualified QuickSpec.Internal.Explore.Schemas as Schemas
import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..), VariableUse(..))
import QuickSpec.Internal.Term hiding (mapFun)
import QuickSpec.Internal.Type
import QuickSpec.Internal.Testing
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Utils
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Terminal
import qualified Data.Map.Strict as Map
import Data.Map(Map)
import qualified Data.Set as Set
import Data.Set(Set)
import Data.Lens.Light
import Control.Monad.Trans.State.Strict
import Control.Monad.Trans.Class
import qualified Twee.Base as Twee
import Control.Monad
import qualified Data.DList as DList
import Data.Maybe
data Polymorphic testcase result fun norm =
Polymorphic {
forall testcase result fun norm.
Polymorphic testcase result fun norm
-> Schemas testcase result (PolyFun fun) norm
pm_schemas :: Schemas testcase result (PolyFun fun) norm,
forall testcase result fun norm.
Polymorphic testcase result fun norm -> Universe
pm_universe :: Universe }
data PolyFun fun =
PolyFun { forall fun. PolyFun fun -> fun
fun_original :: fun, forall fun. PolyFun fun -> fun
fun_specialised :: fun }
deriving (PolyFun fun -> PolyFun fun -> Bool
forall fun. Eq fun => PolyFun fun -> PolyFun fun -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PolyFun fun -> PolyFun fun -> Bool
$c/= :: forall fun. Eq fun => PolyFun fun -> PolyFun fun -> Bool
== :: PolyFun fun -> PolyFun fun -> Bool
$c== :: forall fun. Eq fun => PolyFun fun -> PolyFun fun -> Bool
Eq, PolyFun fun -> PolyFun fun -> Bool
PolyFun fun -> PolyFun 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 (PolyFun fun)
forall fun. Ord fun => PolyFun fun -> PolyFun fun -> Bool
forall fun. Ord fun => PolyFun fun -> PolyFun fun -> Ordering
forall fun. Ord fun => PolyFun fun -> PolyFun fun -> PolyFun fun
min :: PolyFun fun -> PolyFun fun -> PolyFun fun
$cmin :: forall fun. Ord fun => PolyFun fun -> PolyFun fun -> PolyFun fun
max :: PolyFun fun -> PolyFun fun -> PolyFun fun
$cmax :: forall fun. Ord fun => PolyFun fun -> PolyFun fun -> PolyFun fun
>= :: PolyFun fun -> PolyFun fun -> Bool
$c>= :: forall fun. Ord fun => PolyFun fun -> PolyFun fun -> Bool
> :: PolyFun fun -> PolyFun fun -> Bool
$c> :: forall fun. Ord fun => PolyFun fun -> PolyFun fun -> Bool
<= :: PolyFun fun -> PolyFun fun -> Bool
$c<= :: forall fun. Ord fun => PolyFun fun -> PolyFun fun -> Bool
< :: PolyFun fun -> PolyFun fun -> Bool
$c< :: forall fun. Ord fun => PolyFun fun -> PolyFun fun -> Bool
compare :: PolyFun fun -> PolyFun fun -> Ordering
$ccompare :: forall fun. Ord fun => PolyFun fun -> PolyFun fun -> Ordering
Ord)
instance Pretty fun => Pretty (PolyFun fun) where
pPrint :: PolyFun fun -> Doc
pPrint = forall a. Pretty a => a -> Doc
pPrint forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun. PolyFun fun -> fun
fun_specialised
instance PrettyTerm fun => PrettyTerm (PolyFun fun) where
termStyle :: PolyFun fun -> TermStyle
termStyle = forall f. PrettyTerm f => f -> TermStyle
termStyle forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun. PolyFun fun -> fun
fun_specialised
data Universe = Universe { Universe -> Set Type
univ_types :: Set Type }
schemas :: Lens
(Polymorphic testcase result fun norm)
(Schemas testcase result (PolyFun fun) norm)
schemas = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens forall testcase result fun norm.
Polymorphic testcase result fun norm
-> Schemas testcase result (PolyFun fun) norm
pm_schemas (\Schemas testcase result (PolyFun fun) norm
x Polymorphic testcase result fun norm
y -> Polymorphic testcase result fun norm
y { pm_schemas :: Schemas testcase result (PolyFun fun) norm
pm_schemas = Schemas testcase result (PolyFun fun) norm
x })
univ :: Lens (Polymorphic testcase result fun norm) Universe
univ = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens forall testcase result fun norm.
Polymorphic testcase result fun norm -> Universe
pm_universe (\Universe
x Polymorphic testcase result fun norm
y -> Polymorphic testcase result fun norm
y { pm_universe :: Universe
pm_universe = Universe
x })
initialState ::
(Type -> VariableUse) ->
Universe ->
(Term fun -> Bool) ->
(Term fun -> testcase -> Maybe result) ->
Polymorphic testcase result fun norm
initialState :: 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 -> Bool
inst Term fun -> testcase -> Maybe result
eval =
Polymorphic {
pm_schemas :: Schemas testcase result (PolyFun fun) norm
pm_schemas = forall fun testcase result norm.
(Type -> VariableUse)
-> (Term fun -> Bool)
-> (Term fun -> testcase -> Maybe result)
-> Schemas testcase result fun norm
Schemas.initialState Type -> VariableUse
use (Term fun -> Bool
inst 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. PolyFun fun -> fun
fun_specialised) (Term fun -> testcase -> Maybe result
eval 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. PolyFun fun -> fun
fun_specialised),
pm_universe :: Universe
pm_universe = Universe
univ }
polyFun :: Typed fun => fun -> PolyFun fun
polyFun :: forall fun. Typed fun => fun -> PolyFun fun
polyFun fun
x = forall fun. fun -> fun -> PolyFun fun
PolyFun fun
x (forall a. Typed a => a -> a
oneTypeVar fun
x)
polyTerm :: Typed fun => Term fun -> Term (PolyFun fun)
polyTerm :: forall fun. Typed fun => Term fun -> Term (PolyFun fun)
polyTerm = forall a. Typed a => a -> a
oneTypeVar 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. Typed fun => fun -> PolyFun fun
polyFun
instance Typed fun => Typed (PolyFun fun) where
typ :: PolyFun fun -> Type
typ = forall a. Typed a => a -> Type
typ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun. PolyFun fun -> fun
fun_specialised
otherTypesDL :: PolyFun fun -> DList Type
otherTypesDL = forall a. Typed a => a -> DList Type
otherTypesDL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun. PolyFun fun -> fun
fun_specialised
typeSubst_ :: (Var -> Builder TyCon) -> PolyFun fun -> PolyFun fun
typeSubst_ Var -> Builder TyCon
_ PolyFun fun
x = PolyFun fun
x
newtype PolyM testcase result fun norm m a = PolyM { forall testcase result fun norm (m :: * -> *) a.
PolyM testcase result fun norm m a
-> StateT (Polymorphic testcase result fun norm) m a
unPolyM :: StateT (Polymorphic testcase result fun norm) m a }
deriving (forall a b.
a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
forall a b.
(a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
forall testcase result fun norm (m :: * -> *) a b.
Functor m =>
a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
forall testcase result fun norm (m :: * -> *) a b.
Functor m =>
(a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm 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
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
$c<$ :: forall testcase result fun norm (m :: * -> *) a b.
Functor m =>
a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
fmap :: forall a b.
(a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
$cfmap :: forall testcase result fun norm (m :: * -> *) a b.
Functor m =>
(a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
Functor, forall a. a -> PolyM testcase result fun norm m a
forall a b.
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
forall a b.
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
forall a b.
PolyM testcase result fun norm m (a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
forall a b c.
(a -> b -> c)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m c
forall {testcase} {result} {fun} {norm} {m :: * -> *}.
Monad m =>
Functor (PolyM testcase result fun norm m)
forall testcase result fun norm (m :: * -> *) a.
Monad m =>
a -> PolyM testcase result fun norm m a
forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m (a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
forall testcase result fun norm (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm 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.
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
$c<* :: forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m a
*> :: forall a b.
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
$c*> :: forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
liftA2 :: forall a b c.
(a -> b -> c)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m c
$cliftA2 :: forall testcase result fun norm (m :: * -> *) a b c.
Monad m =>
(a -> b -> c)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m c
<*> :: forall a b.
PolyM testcase result fun norm m (a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
$c<*> :: forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m (a -> b)
-> PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
pure :: forall a. a -> PolyM testcase result fun norm m a
$cpure :: forall testcase result fun norm (m :: * -> *) a.
Monad m =>
a -> PolyM testcase result fun norm m a
Applicative, forall a. a -> PolyM testcase result fun norm m a
forall a b.
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
forall a b.
PolyM testcase result fun norm m a
-> (a -> PolyM testcase result fun norm m b)
-> PolyM testcase result fun norm m b
forall testcase result fun norm (m :: * -> *).
Monad m =>
Applicative (PolyM testcase result fun norm m)
forall testcase result fun norm (m :: * -> *) a.
Monad m =>
a -> PolyM testcase result fun norm m a
forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> (a -> PolyM testcase result fun norm m b)
-> PolyM testcase result fun norm 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 -> PolyM testcase result fun norm m a
$creturn :: forall testcase result fun norm (m :: * -> *) a.
Monad m =>
a -> PolyM testcase result fun norm m a
>> :: forall a b.
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
$c>> :: forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> PolyM testcase result fun norm m b
-> PolyM testcase result fun norm m b
>>= :: forall a b.
PolyM testcase result fun norm m a
-> (a -> PolyM testcase result fun norm m b)
-> PolyM testcase result fun norm m b
$c>>= :: forall testcase result fun norm (m :: * -> *) a b.
Monad m =>
PolyM testcase result fun norm m a
-> (a -> PolyM testcase result fun norm m b)
-> PolyM testcase result fun norm m b
Monad, String -> PolyM testcase result fun norm m ()
forall {testcase} {result} {fun} {norm} {m :: * -> *}.
MonadTerminal m =>
Monad (PolyM testcase result fun norm m)
forall testcase result fun norm (m :: * -> *).
MonadTerminal m =>
String -> PolyM testcase result fun norm m ()
forall (m :: * -> *).
Monad m
-> (String -> m ())
-> (String -> m ())
-> (String -> m ())
-> MonadTerminal m
putTemp :: String -> PolyM testcase result fun norm m ()
$cputTemp :: forall testcase result fun norm (m :: * -> *).
MonadTerminal m =>
String -> PolyM testcase result fun norm m ()
putLine :: String -> PolyM testcase result fun norm m ()
$cputLine :: forall testcase result fun norm (m :: * -> *).
MonadTerminal m =>
String -> PolyM testcase result fun norm m ()
putText :: String -> PolyM testcase result fun norm m ()
$cputText :: forall testcase result fun norm (m :: * -> *).
MonadTerminal m =>
String -> PolyM testcase result fun norm m ()
MonadTerminal)
explore ::
(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 :: 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 = do
Universe
univ <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens (Polymorphic testcase result fun norm) Universe
univ
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term fun
t forall fun. Typed fun => Term fun -> Universe -> Bool
`usefulForUniverse` Universe
univ) forall a b. (a -> b) -> a -> b
$
forall a. HasCallStack => String -> a
error (String
"Type " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (forall a. Typed a => a -> Type
typ Term fun
t) forall a. [a] -> [a] -> [a]
++ String
" not in universe for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow Term fun
t)
if Bool -> Bool
not (Term fun
t forall fun.
(PrettyTerm fun, Typed fun) =>
Term fun -> Universe -> Bool
`inUniverse` Universe
univ) then
forall (m :: * -> *) a. Monad m => a -> m a
return (forall fun. [Prop (Term fun)] -> Result fun
Accepted [])
else do
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)
exploreNoMGU Term fun
t
case Result fun
res of
Rejected{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Result fun
res
Accepted{} -> do
[Result fun]
ress <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a fun.
(Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun,
Typed a) =>
Universe -> a -> [a]
typeInstances Universe
univ Term fun
t) forall a b. (a -> b) -> a -> b
$ \Term fun
u ->
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)
exploreNoMGU Term fun
u
forall (m :: * -> *) a. Monad m => a -> m a
return Result fun
res { result_props :: [Prop (Term fun)]
result_props = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall fun. Result fun -> [Prop (Term fun)]
result_props (Result fun
resforall a. a -> [a] -> [a]
:[Result fun]
ress) }
exploreNoMGU ::
(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)
exploreNoMGU :: 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)
exploreNoMGU Term fun
t = do
Universe
univ <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens (Polymorphic testcase result fun norm) Universe
univ
if Bool -> Bool
not (Term fun
t forall fun.
(PrettyTerm fun, Typed fun) =>
Term fun -> Universe -> Bool
`inUniverse` Universe
univ) then forall (m :: * -> *) a. Monad m => a -> m a
return (forall fun. [Prop (Term fun)] -> Result fun
Rejected []) else do
Schemas testcase result (PolyFun fun) norm
schemas1 <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens
(Polymorphic testcase result fun norm)
(Schemas testcase result (PolyFun fun) norm)
schemas
(Result (PolyFun fun)
res, Schemas testcase result (PolyFun fun) norm
schemas2) <- forall testcase result fun norm (m :: * -> *) a.
PolyM testcase result fun norm m a
-> StateT (Polymorphic testcase result fun norm) m a
unPolyM (forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall fun result norm testcase (m :: * -> *).
(PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,
MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m,
MonadTerminal m) =>
Term fun
-> StateT (Schemas testcase result fun norm) m (Result fun)
Schemas.explore (forall fun. Typed fun => Term fun -> Term (PolyFun fun)
polyTerm Term fun
t)) Schemas testcase result (PolyFun fun) norm
schemas1)
forall {testcase} {result} {fun} {norm}.
Lens
(Polymorphic testcase result fun norm)
(Schemas testcase result (PolyFun fun) norm)
schemas forall a (m :: * -> *) b. MonadState a m => Lens a b -> b -> m ()
~= Schemas testcase result (PolyFun fun) norm
schemas2
forall (m :: * -> *) a. Monad m => a -> m a
return (forall {fun} {fun}.
(Prop (Term fun) -> Prop (Term fun)) -> Result fun -> Result fun
mapProps (forall fun.
(PrettyTerm fun, Typed fun, Apply (Term fun)) =>
Prop (Term fun) -> Prop (Term fun)
regeneralise forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapFun forall fun. PolyFun fun -> fun
fun_original) Result (PolyFun fun)
res)
where
mapProps :: (Prop (Term fun) -> Prop (Term fun)) -> Result fun -> Result fun
mapProps Prop (Term fun) -> Prop (Term fun)
f (Accepted [Prop (Term fun)]
props) = forall fun. [Prop (Term fun)] -> Result fun
Accepted (forall a b. (a -> b) -> [a] -> [b]
map Prop (Term fun) -> Prop (Term fun)
f [Prop (Term fun)]
props)
mapProps Prop (Term fun) -> Prop (Term fun)
f (Rejected [Prop (Term fun)]
props) = forall fun. [Prop (Term fun)] -> Result fun
Rejected (forall a b. (a -> b) -> [a] -> [b]
map Prop (Term fun) -> Prop (Term fun)
f [Prop (Term fun)]
props)
instance (PrettyTerm fun, Ord fun, Typed fun, Apply (Term fun), MonadPruner (Term fun) norm m, MonadTerminal m) =>
MonadPruner (Term (PolyFun fun)) norm (PolyM testcase result fun norm m) where
normaliser :: PolyM testcase result fun norm m (Term (PolyFun fun) -> norm)
normaliser = forall testcase result fun norm (m :: * -> *) a.
StateT (Polymorphic testcase result fun norm) m a
-> PolyM testcase result fun norm m a
PolyM forall a b. (a -> b) -> a -> b
$ do
Term 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 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. PolyFun fun -> fun
fun_specialised)
add :: Prop (Term (PolyFun fun)) -> PolyM testcase result fun norm m Bool
add Prop (Term (PolyFun fun))
prop = forall testcase result fun norm (m :: * -> *) a.
StateT (Polymorphic testcase result fun norm) m a
-> PolyM testcase result fun norm m a
PolyM forall a b. (a -> b) -> a -> b
$ do
Universe
univ <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens (Polymorphic testcase result fun norm) Universe
univ
let insts :: [Prop (Term fun)]
insts = forall a fun.
(Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun,
Typed a) =>
Universe -> a -> [a]
typeInstances Universe
univ (forall fun a. Symbolic fun a => a -> a
canonicalise (forall fun.
(PrettyTerm fun, Typed fun, Apply (Term fun)) =>
Prop (Term fun) -> Prop (Term fun)
regeneralise (forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapFun forall fun. PolyFun fun -> fun
fun_original Prop (Term (PolyFun fun))
prop)))
forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add [Prop (Term fun)]
insts
normTheorems :: PolyM testcase result fun norm m [Theorem norm]
normTheorems = forall testcase result fun norm (m :: * -> *) a.
StateT (Polymorphic testcase result fun norm) m a
-> PolyM testcase result fun norm m a
PolyM forall term norm (m :: * -> *).
MonadPruner term norm m =>
m [Theorem norm]
normTheorems
decodeNormalForm :: (Type -> Maybe (Term (PolyFun fun)))
-> norm
-> PolyM testcase result fun norm m (Maybe (Term (PolyFun fun)))
decodeNormalForm Type -> Maybe (Term (PolyFun fun))
hole norm
t =
forall testcase result fun norm (m :: * -> *) a.
StateT (Polymorphic testcase result fun norm) m a
-> PolyM testcase result fun norm m a
PolyM forall a b. (a -> b) -> a -> b
$ do
Maybe (Term 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. PolyFun fun -> fun
fun_specialised) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Term (PolyFun fun))
hole) norm
t
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 (\fun
f -> forall fun. fun -> fun -> PolyFun fun
PolyFun fun
f fun
f)) Maybe (Term fun)
t
instance MonadTester testcase (Term fun) m =>
MonadTester testcase (Term (PolyFun fun)) (PolyM testcase result fun norm m) where
test :: Prop (Term (PolyFun fun))
-> PolyM testcase result fun norm m (TestResult testcase)
test Prop (Term (PolyFun fun))
prop = forall testcase result fun norm (m :: * -> *) a.
StateT (Polymorphic testcase result fun norm) m a
-> PolyM testcase result fun norm m a
PolyM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall testcase term (m :: * -> *).
MonadTester testcase term m =>
Prop term -> m (TestResult testcase)
test (forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapFun forall fun. PolyFun fun -> fun
fun_original Prop (Term (PolyFun fun))
prop))
retest :: testcase
-> Prop (Term (PolyFun fun))
-> PolyM testcase result fun norm m (TestResult testcase)
retest testcase
testcase Prop (Term (PolyFun fun))
prop = forall testcase result fun norm (m :: * -> *) a.
StateT (Polymorphic testcase result fun norm) m a
-> PolyM testcase result fun norm m a
PolyM forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall testcase term (m :: * -> *).
MonadTester testcase term m =>
testcase -> Prop term -> m (TestResult testcase)
retest testcase
testcase (forall fun1 fun2.
(fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)
mapFun forall fun. PolyFun fun -> fun
fun_original Prop (Term (PolyFun fun))
prop))
regeneralise :: (PrettyTerm fun, Typed fun, Apply (Term fun)) => Prop (Term fun) -> Prop (Term fun)
regeneralise :: forall fun.
(PrettyTerm fun, Typed fun, Apply (Term fun)) =>
Prop (Term fun) -> Prop (Term fun)
regeneralise =
forall {f} {a}. (Symbolic f a, Typed a) => Prop a -> Prop a
restrict forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Poly a -> a
unPoly forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {f}. Typed f => Prop (Term f) -> Poly (Prop (Term f))
generalise
where
generalise :: Prop (Term f) -> Poly (Prop (Term f))
generalise ([Equation (Term f)]
lhs :=>: Equation (Term f)
rhs) =
forall a b c.
(Typed a, Typed b, Typed c) =>
(a -> b -> c) -> Poly a -> Poly b -> Poly c
polyApply forall a. [Equation a] -> Equation a -> Prop a
(:=>:) (forall a. Typed a => [Poly a] -> Poly [a]
polyList (forall a b. (a -> b) -> [a] -> [b]
map forall {f}.
Typed f =>
Equation (Term f) -> Poly (Equation (Term f))
genLit [Equation (Term f)]
lhs)) (forall {f}.
Typed f =>
Equation (Term f) -> Poly (Equation (Term f))
genLit Equation (Term f)
rhs)
genLit :: Equation (Term f) -> Poly (Equation (Term f))
genLit (Term f
t :=: Term f
u) = forall a b c.
(Typed a, Typed b, Typed c) =>
(a -> b -> c) -> Poly a -> Poly b -> Poly c
polyApply forall a. a -> a -> Equation a
(:=:) (forall {f}. Typed f => Term f -> Poly (Term f)
genTerm Term f
t) (forall {f}. Typed f => Term f -> Poly (Term f)
genTerm Term f
u)
genTerm :: Term f -> Poly (Term f)
genTerm (Var (V Type
ty Int
x)) =
forall a. Typed a => a -> Poly a
poly (forall f. Var -> Term f
Var (Type -> Int -> Var
V (forall {f}. Term f -> Term f
genType Type
ty) Int
x))
genTerm (Fun f
f) = forall a. Typed a => a -> Poly a
poly (forall f. f -> Term f
Fun f
f)
genTerm (Term f
t :$: Term f
u) =
let
(Term f
t', Term f
u') = forall a. Poly a -> a
unPoly (forall a b. (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)
polyPair (Term f -> Poly (Term f)
genTerm Term f
t) (Term f -> Poly (Term f)
genTerm Term f
u))
Just Type
ty = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Poly a -> a
unPoly (Poly Type -> Poly Type -> Maybe (Poly Type)
polyMgu (forall a. Typed a => Poly a -> Poly Type
polyTyp (forall a. Typed a => a -> Poly a
poly Term f
t')) (forall a b c.
(Typed a, Typed b, Typed c) =>
(a -> b -> c) -> Poly a -> Poly b -> Poly c
polyApply (\Type
arg Type
res -> [Type] -> Type -> Type
arrowType [Type
arg] Type
res) (forall a. Typed a => Poly a -> Poly Type
polyTyp (forall a. Typed a => a -> Poly a
poly Term f
u')) (forall a. Typed a => a -> Poly a
poly Type
typeVar)))
Just (Type
arg, Type
_) = Type -> Maybe (Type, Type)
unpackArrow Type
ty
Just Term f
t'' = forall a. Typed a => Type -> a -> Maybe a
cast Type
ty Term f
t'
Just Term f
u'' = forall a. Typed a => Type -> a -> Maybe a
cast Type
arg Term f
u'
in
forall a. Typed a => a -> Poly a
poly (Term f
t'' forall f. Term f -> Term f -> Term f
:$: Term f
u'')
genType :: Term f -> Term f
genType = forall a. Build a => a -> Term (BuildFun a)
Twee.build forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {f}. Int -> TermList f -> Builder f
aux Int
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
Twee.singleton
where
aux :: Int -> TermList f -> Builder f
aux !Int
_ TermList f
Twee.Empty = forall a. Monoid a => a
mempty
aux Int
n (Twee.Cons (Twee.Var Var
_) TermList f
ts) =
forall f. Var -> Builder f
Twee.var (Int -> Var
Twee.V Int
n) forall a. Monoid a => a -> a -> a
`mappend` Int -> TermList f -> Builder f
aux (Int
nforall a. Num a => a -> a -> a
+Int
1) TermList f
ts
aux Int
n (Twee.Cons (Twee.App Fun f
f TermList f
ts) TermList f
us) =
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
Twee.app Fun f
f (Int -> TermList f -> Builder f
aux Int
n TermList f
ts) forall a. Monoid a => a -> a -> a
`mappend`
Int -> TermList f -> Builder f
aux (Int
nforall a. Num a => a -> a -> a
+forall f. TermList f -> Int
Twee.lenList TermList f
ts) TermList f
us
restrict :: Prop a -> Prop a
restrict Prop a
prop = forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Subst TyCon
sub Prop a
prop
where
Just Subst TyCon
sub = forall f. TermList f -> TermList f -> Maybe (Subst f)
Twee.unifyList (forall a. Build a => a -> TermList (BuildFun a)
Twee.buildList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Type, Type)]
cs)) (forall a. Build a => a -> TermList (BuildFun a)
Twee.buildList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Type, Type)]
cs))
cs :: [(Type, Type)]
cs = [(Var -> Type
var_ty Var
x, Var -> Type
var_ty Var
y) | Var
x:[Var]
xs <- [[Var]]
vs, Var
y <- [Var]
xs] forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. Typed a => Equation a -> [(Type, Type)]
litCs (forall a. Prop a -> [Equation a]
lhs Prop a
prop) forall a. [a] -> [a] -> [a]
++ forall {a}. Typed a => Equation a -> [(Type, Type)]
litCs (forall a. Prop a -> Equation a
rhs Prop a
prop)
vs :: [[Var]]
vs = forall b a. Ord b => (a -> b) -> [a] -> [[a]]
partitionBy Var -> Var
skel (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall f a. Symbolic f a => a -> [Var]
vars (forall f a. Symbolic f a => a -> [Term f]
terms Prop a
prop))
skel :: Var -> Var
skel (V Type
ty Int
x) = Type -> Int -> Var
V (forall a. Typed a => a -> a
oneTypeVar Type
ty) Int
x
litCs :: Equation a -> [(Type, Type)]
litCs (a
t :=: a
u) = [(forall a. Typed a => a -> Type
typ a
t, forall a. Typed a => a -> Type
typ a
u)]
typeInstancesList :: [Type] -> [Type] -> [Twee.Var -> Type]
typeInstancesList :: [Type] -> [Type] -> [Var -> Type]
typeInstancesList [Type]
types [Type]
prop =
forall a b. (a -> b) -> [a] -> [b]
map forall {k} {a}. (Ord k, Pretty k) => Map k a -> k -> a
eval
(forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [Map Var Type] -> [Map Var Type] -> [Map Var Type]
intersection [forall k a. Map k a
Map.empty]
(forall a b. (a -> b) -> [a] -> [b]
map Type -> [Map Var Type]
constrain
(forall a. Ord a => [a] -> [a]
usort [Type]
prop)))
where
constrain :: Type -> [Map Var Type]
constrain Type
t =
forall a. Ord a => [a] -> [a]
usort [ forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall f. Subst f -> [(Var, Term f)]
Twee.substToList Subst TyCon
sub) | Type
u <- [Type]
types, Just Subst TyCon
sub <- [forall f. Term f -> Term f -> Maybe (Subst f)
Twee.match Type
t Type
u] ]
eval :: Map k a -> k -> a
eval Map k a
sub k
x =
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (forall a. HasCallStack => String -> a
error (String
"not found: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow k
x)) k
x Map k a
sub
typeInstances :: (Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun, Typed a) => Universe -> a -> [a]
typeInstances :: forall a fun.
(Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun,
Typed a) =>
Universe -> a -> [a]
typeInstances Universe{Set Type
univ_types :: Set Type
univ_types :: Universe -> Set Type
..} a
prop =
[ forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Var -> Type
sub a
prop
| Var -> Type
sub <- [Type] -> [Type] -> [Var -> Type]
typeInstancesList (forall a. Set a -> [a]
Set.toList Set Type
univ_types) (forall a b. (a -> b) -> [a] -> [b]
map forall a. Typed a => a -> Type
typ (forall a. DList a -> [a]
DList.toList (forall f a. Symbolic f a => a -> DList (Term f)
termsDL a
prop) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall f. Term f -> [Term f]
subtermsFO)) ]
intersection :: [Map Twee.Var Type] -> [Map Twee.Var Type] -> [Map Twee.Var Type]
[Map Var Type]
ms1 intersection :: [Map Var Type] -> [Map Var Type] -> [Map Var Type]
`intersection` [Map Var Type]
ms2 = forall a. Ord a => [a] -> [a]
usort [ forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Var Type
m1 Map Var Type
m2 | Map Var Type
m1 <- [Map Var Type]
ms1, Map Var Type
m2 <- [Map Var Type]
ms2, forall {k} {a}. (Ord k, Eq a) => Map k a -> Map k a -> Bool
ok Map Var Type
m1 Map Var Type
m2 ]
where
ok :: Map k a -> Map k a -> Bool
ok Map k a
m1 Map k a
m2 = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
x Map k a
m1 forall a. Eq a => a -> a -> Bool
== forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
x Map k a
m2 | k
x <- forall k a. Map k a -> [k]
Map.keys (forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection Map k a
m1 Map k a
m2) ]
universe :: Typed a => [a] -> Universe
universe :: forall a. Typed a => [a] -> Universe
universe [a]
xs = Set Type -> Universe
Universe (forall a. Ord a => [a] -> Set a
Set.fromList [Type]
univ)
where
types :: [Type]
types = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ Type
typeVarforall a. a -> [a] -> [a]
:forall a b. (a -> b) -> [a] -> [b]
map forall a. Typed a => a -> Type
typ [a]
xs
univBase :: [Type]
univBase = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
components [Type]
types
univHo :: [Type]
univHo = forall a. Ord a => [a] -> [a]
usort forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
addHo [Type]
univBase
where
addHo :: Type -> [Type]
addHo Type
ty =
Type
tyforall a. a -> [a] -> [a]
:
[ forall a s.
(Typed a, Substitution s, SubstFun s ~ TyCon) =>
s -> a -> a
typeSubst Var -> Type
sub Type
ho
| Type
fun <- [Type]
types,
Type
ho <- Type -> [Type]
arrows Type
fun,
Var -> Type
sub <- [Type] -> [Type] -> [Var -> Type]
typeInstancesList [Type]
univBase (Type -> [Type]
components Type
fun) ]
univ :: [Type]
univ = forall a. Typed a => a -> a
oneTypeVar (forall a. Eq a => (a -> a) -> a -> a
fixpoint (forall a. Ord a => [a] -> [a]
usort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Typed a => a -> a
canonicaliseType forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> [Type]
mgus forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type] -> [Type]
prune) [Type]
univHo)
where
prune :: [Type] -> [Type]
prune [Type]
tys = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Bool
subsumed) [Type]
tys
where
subsumed :: Type -> Bool
subsumed Type
ty =
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [forall a. Typed a => a -> a
oneTypeVar Type
pat forall a. Eq a => a -> a -> Bool
== forall a. Typed a => a -> a
oneTypeVar Type
ty Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isJust (Type -> Type -> Maybe (Subst TyCon)
matchType Type
pat Type
ty) Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (Type -> Type -> Maybe (Subst TyCon)
matchType Type
ty Type
pat) | Type
pat <- [Type]
tys]
mgus :: [Type] -> [Type]
mgus [Type]
tys =
[Type]
tys forall a. [a] -> [a] -> [a]
++
[ Type
ty
| Type
ty1 <- [Type]
tys, Type
ty2 <- [Type]
tys,
Type
ty <- forall a. Poly a -> a
unPoly forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Poly Type -> Poly Type -> [Poly Type]
combine (forall a. Typed a => a -> Poly a
poly Type
ty1) (forall a. Typed a => a -> Poly a
poly Type
ty2),
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [forall a. Maybe a -> Bool
isJust (Type -> Type -> Maybe (Subst TyCon)
matchType Type
ty Type
bound) | Type
bound <- [Type]
tys] ]
combine :: Poly Type -> Poly Type -> [Poly Type]
combine Poly Type
ty1 Poly Type
ty2 =
forall a. [Maybe a] -> [a]
catMaybes [Poly Type -> Poly Type -> Maybe (Poly Type)
polyMgu Poly Type
ty1 Poly Type
ty2 | Poly Type
ty1 forall a. Ord a => a -> a -> Bool
< Poly Type
ty2] forall a. [a] -> [a] -> [a]
++
forall a. Maybe a -> [a]
maybeToList (forall a. Apply a => a -> a -> Maybe a
tryApply Poly Type
ty1 Poly Type
ty2) forall a. [a] -> [a] -> [a]
++
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[forall a. Typed a => a -> Poly a
poly Type
x, forall a. Typed a => a -> Poly a
poly Type
y] | (Type
x, Type
y) <- forall a. Maybe a -> [a]
maybeToList (forall a. Poly a -> a
unPoly forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))
polyFunctionMgu Poly Type
ty1 Poly Type
ty2)]
components :: Type -> [Type]
components Type
ty =
case Type -> Maybe (Type, Type)
unpackArrow Type
ty of
Maybe (Type, Type)
Nothing -> [Type
ty]
Just (Type
ty1, Type
ty2) -> Type -> [Type]
components Type
ty1 forall a. [a] -> [a] -> [a]
++ Type -> [Type]
components Type
ty2
arrows :: Type -> [Type]
arrows Type
ty =
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
arrows1 (Type -> [Type]
typeArgs Type
ty)
where
arrows1 :: Type -> [Type]
arrows1 Type
ty =
case Type -> Maybe (Type, Type)
unpackArrow Type
ty of
Just (Type
arg, Type
res) ->
[Type
ty] forall a. [a] -> [a] -> [a]
++ Type -> [Type]
arrows1 Type
arg forall a. [a] -> [a] -> [a]
++ Type -> [Type]
arrows1 Type
res
Maybe (Type, Type)
_ -> []
inUniverse :: (PrettyTerm fun, Typed fun) => Term fun -> Universe -> Bool
Term fun
t inUniverse :: forall fun.
(PrettyTerm fun, Typed fun) =>
Term fun -> Universe -> Bool
`inUniverse` Universe{Set Type
univ_types :: Set Type
univ_types :: Universe -> Set Type
..} =
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall a. Typed a => a -> a
oneTypeVar (forall a. Typed a => a -> Type
typ Term fun
u) forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Type
univ_types | Term fun
u <- forall f. Term f -> [Term f]
subtermsFO Term fun
t forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall f. Var -> Term f
Var (forall f a. Symbolic f a => a -> [Var]
vars Term fun
t)]
usefulForUniverse :: Typed fun => Term fun -> Universe -> Bool
Term fun
t usefulForUniverse :: forall fun. Typed fun => Term fun -> Universe -> Bool
`usefulForUniverse` Universe{Set Type
univ_types :: Set Type
univ_types :: Universe -> Set Type
..} =
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [forall a. Typed a => a -> a
oneTypeVar (forall a. Typed a => a -> Type
typ Term fun
u) forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Type
univ_types | Term fun
u <- forall f. Term f -> [Term f]
properSubtermsFO Term fun
t forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall f. Var -> Term f
Var (forall f a. Symbolic f a => a -> [Var]
vars Term fun
t)] Bool -> Bool -> Bool
&&
forall a. Typed a => a -> a
oneTypeVar (Type -> Type
typeRes (forall a. Typed a => a -> Type
typ Term fun
t)) forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Type
univ_types