-- Theory exploration which handles polymorphism.
{-# 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

-- The set of all types being explored
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 -- because it's supposed to be monomorphic

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))

-- Given a property which only contains one type variable,
-- add as much polymorphism to the property as possible.
-- e.g.    map (f :: a -> a) (xs++ys) = map f xs++map f ys
-- becomes map (f :: a -> b) (xs++ys) = map f xs++map f ys.
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 =
  -- First replace each type variable occurrence with a fresh
  -- type variable (generalise), then unify type variables
  -- where necessary to preserve well-typedness (restrict).
  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)) =
      -- It's tempting to return Var (V typeVar x) here.
      -- But this is wrong!
      -- In the case of the type (), we get the law x == y :: (),
      -- which we must not generalise to x == y :: a.
      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)
        -- Two variables that were equal before generalisation must have the
        -- same type afterwards
        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 of all functions
    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

    -- Take the argument and result type of every function.
    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

    -- Add partially-applied functions, if they can be used to
    -- fill in a higher-order argument.
    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) ]
  
    -- Finally, close the universe under the following operations:
    -- * Unifying two types
    -- * Unifying a function's argument with another type
    --   (the closure includes the function type, the argument type
    --   and the result type)
    -- but only if some type in the universe is an instance of the
    -- resulting type. The idea is that, if some term can be built
    -- whose type is a generalisation of the type in the universe,
    -- that generalised type should also be in the universe.
    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]
++
          -- Get the function and argument types used by tryApply
          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