-- Theory exploration which works on a schema at a time.
{-# OPTIONS_HADDOCK hide #-}
{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, MultiParamTypeClasses, FlexibleInstances #-}
module QuickSpec.Internal.Explore.Schemas where

import qualified Data.Map.Strict as Map
import Data.Map(Map)
import QuickSpec.Internal.Prop
import QuickSpec.Internal.Pruning
import QuickSpec.Internal.Term
import QuickSpec.Internal.Type
import QuickSpec.Internal.Testing
import QuickSpec.Internal.Utils
import QuickSpec.Internal.Terminal
import qualified QuickSpec.Internal.Explore.Terms as Terms
import QuickSpec.Internal.Explore.Terms(Terms)
import Control.Monad.Trans.State.Strict hiding (State)
import Data.List
import Data.Ord
import Data.Lens.Light
import qualified Data.Set as Set
import Data.Set(Set)
import Data.Maybe
import Control.Monad
import Data.Label

-- | Constrains how variables of a particular type may occur in a term.
data VariableUse =
    UpTo Int -- ^ @UpTo n@: terms may contain up to @n@ distinct variables of this type
             -- (in some cases, laws with more variables may still be found)
  | Linear   -- ^ Each variable in the term must be distinct
  deriving (VariableUse -> VariableUse -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VariableUse -> VariableUse -> Bool
$c/= :: VariableUse -> VariableUse -> Bool
== :: VariableUse -> VariableUse -> Bool
$c== :: VariableUse -> VariableUse -> Bool
Eq, Int -> VariableUse -> ShowS
[VariableUse] -> ShowS
VariableUse -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VariableUse] -> ShowS
$cshowList :: [VariableUse] -> ShowS
show :: VariableUse -> String
$cshow :: VariableUse -> String
showsPrec :: Int -> VariableUse -> ShowS
$cshowsPrec :: Int -> VariableUse -> ShowS
Show)

data Schemas testcase result fun norm =
  Schemas {
    forall testcase result fun norm.
Schemas testcase result fun norm -> Type -> VariableUse
sc_use :: Type -> VariableUse,
    forall testcase result fun norm.
Schemas testcase result fun norm -> Term fun -> Bool
sc_instantiate_singleton :: Term fun -> Bool,
    forall testcase result fun norm.
Schemas testcase result fun norm
-> Terms testcase result (Term fun) norm
sc_empty :: Terms testcase result (Term fun) norm,
    forall testcase result fun norm.
Schemas testcase result fun norm
-> Terms testcase result (Term fun) norm
sc_classes :: Terms testcase result (Term fun) norm,
    forall testcase result fun norm.
Schemas testcase result fun norm -> Set (Term fun)
sc_instantiated :: Set (Term fun),
    forall testcase result fun norm.
Schemas testcase result fun norm
-> Map (Term fun) (Terms testcase result (Term fun) norm)
sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm) }

classes :: Lens
  (Schemas testcase result fun norm)
  (Terms testcase result (Term fun) norm)
classes = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens forall testcase result fun norm.
Schemas testcase result fun norm
-> Terms testcase result (Term fun) norm
sc_classes (\Terms testcase result (Term fun) norm
x Schemas testcase result fun norm
y -> Schemas testcase result fun norm
y { sc_classes :: Terms testcase result (Term fun) norm
sc_classes = Terms testcase result (Term fun) norm
x })
use :: Lens (Schemas testcase result fun norm) (Type -> VariableUse)
use = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens forall testcase result fun norm.
Schemas testcase result fun norm -> Type -> VariableUse
sc_use (\Type -> VariableUse
x Schemas testcase result fun norm
y -> Schemas testcase result fun norm
y { sc_use :: Type -> VariableUse
sc_use = Type -> VariableUse
x })
instances :: Lens
  (Schemas testcase result fun norm)
  (Map (Term fun) (Terms testcase result (Term fun) norm))
instances = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens forall testcase result fun norm.
Schemas testcase result fun norm
-> Map (Term fun) (Terms testcase result (Term fun) norm)
sc_instances (\Map (Term fun) (Terms testcase result (Term fun) norm)
x Schemas testcase result fun norm
y -> Schemas testcase result fun norm
y { sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm)
sc_instances = Map (Term fun) (Terms testcase result (Term fun) norm)
x })
instantiated :: Lens (Schemas testcase result fun norm) (Set (Term fun))
instantiated = forall a b. (a -> b) -> (b -> a -> a) -> Lens a b
lens forall testcase result fun norm.
Schemas testcase result fun norm -> Set (Term fun)
sc_instantiated (\Set (Term fun)
x Schemas testcase result fun norm
y -> Schemas testcase result fun norm
y { sc_instantiated :: Set (Term fun)
sc_instantiated = Set (Term fun)
x })

instance_ :: Ord fun => Term fun -> Lens (Schemas testcase result fun norm) (Terms testcase result (Term fun) norm)
instance_ :: forall fun testcase result norm.
Ord fun =>
Term fun
-> Lens
     (Schemas testcase result fun norm)
     (Terms testcase result (Term fun) norm)
instance_ Term fun
t = forall a b. (a -> Lens a b) -> Lens a b
reading (\Schemas{Map (Term fun) (Terms testcase result (Term fun) norm)
Set (Term fun)
Terms testcase result (Term fun) norm
Type -> VariableUse
Term fun -> Bool
sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm)
sc_instantiated :: Set (Term fun)
sc_classes :: Terms testcase result (Term fun) norm
sc_empty :: Terms testcase result (Term fun) norm
sc_instantiate_singleton :: Term fun -> Bool
sc_use :: Type -> VariableUse
sc_instances :: forall testcase result fun norm.
Schemas testcase result fun norm
-> Map (Term fun) (Terms testcase result (Term fun) norm)
sc_instantiated :: forall testcase result fun norm.
Schemas testcase result fun norm -> Set (Term fun)
sc_classes :: forall testcase result fun norm.
Schemas testcase result fun norm
-> Terms testcase result (Term fun) norm
sc_empty :: forall testcase result fun norm.
Schemas testcase result fun norm
-> Terms testcase result (Term fun) norm
sc_instantiate_singleton :: forall testcase result fun norm.
Schemas testcase result fun norm -> Term fun -> Bool
sc_use :: forall testcase result fun norm.
Schemas testcase result fun norm -> Type -> VariableUse
..} -> forall a b. Ord a => a -> b -> Lens (Map a b) b
keyDefault Term fun
t Terms testcase result (Term fun) norm
sc_empty forall (cat :: * -> * -> *) b c a.
Category cat =>
cat b c -> cat a b -> cat a c
# forall {testcase} {result} {fun} {norm}.
Lens
  (Schemas testcase result fun norm)
  (Map (Term fun) (Terms testcase result (Term fun) norm))
instances)

initialState ::
  (Type -> VariableUse) ->
  (Term fun -> Bool) ->
  (Term fun -> testcase -> Maybe result) ->
  Schemas testcase result fun norm
initialState :: forall fun testcase result norm.
(Type -> VariableUse)
-> (Term fun -> Bool)
-> (Term fun -> testcase -> Maybe result)
-> Schemas testcase result fun norm
initialState Type -> VariableUse
use Term fun -> Bool
inst Term fun -> testcase -> Maybe result
eval =
  Schemas {
    sc_use :: Type -> VariableUse
sc_use = Type -> VariableUse
use,
    sc_instantiate_singleton :: Term fun -> Bool
sc_instantiate_singleton = Term fun -> Bool
inst,
    sc_empty :: Terms testcase result (Term fun) norm
sc_empty = forall term testcase result norm.
(term -> testcase -> Maybe result)
-> Terms testcase result term norm
Terms.initialState Term fun -> testcase -> Maybe result
eval,
    sc_classes :: Terms testcase result (Term fun) norm
sc_classes = forall term testcase result norm.
(term -> testcase -> Maybe result)
-> Terms testcase result term norm
Terms.initialState Term fun -> testcase -> Maybe result
eval,
    sc_instantiated :: Set (Term fun)
sc_instantiated = forall a. Set a
Set.empty,
    sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm)
sc_instances = forall k a. Map k a
Map.empty }

data Result fun =
    Accepted { forall fun. Result fun -> [Prop (Term fun)]
result_props :: [Prop (Term fun)] }
  | Rejected { result_props :: [Prop (Term fun)] }

-- The schema is represented as a term where there is only one distinct variable of each type
explore ::
  (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)
explore :: 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)
explore Term fun
t0 = do
  Type -> VariableUse
use <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens (Schemas testcase result fun norm) (Type -> VariableUse)
use
  if forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Type -> VariableUse
use Type
ty forall a. Eq a => a -> a -> Bool
== Int -> VariableUse
UpTo Int
0 | Type
ty <- forall a. Ord a => [a] -> [a]
usort (forall a b. (a -> b) -> [a] -> [b]
map forall a. Typed a => a -> Type
typ (forall f a. Symbolic f a => a -> [Var]
vars Term fun
t0))] then forall (m :: * -> *) a. Monad m => a -> m a
return (forall fun. [Prop (Term fun)] -> Result fun
Rejected []) else do
    let t :: Term fun
t = forall f. Term f -> Term f
mostSpecific Term fun
t0
    Result (Term fun)
res <- forall (stateT :: * -> (* -> *) -> * -> *) s (m :: * -> *) s' a.
(MonadStateT stateT, MonadState s (stateT s m),
 MonadTrans (stateT s), Monad m) =>
Lens s s' -> stateT s' m a -> stateT s m a
zoom forall {testcase} {result} {fun} {norm}.
Lens
  (Schemas testcase result fun norm)
  (Terms testcase result (Term fun) norm)
classes (forall term norm result testcase (m :: * -> *).
(Pretty term, Typed term, Ord norm, Ord result,
 MonadTester testcase term m, MonadPruner term norm m,
 MonadTerminal m) =>
term -> StateT (Terms testcase result term norm) m (Result term)
Terms.explore Term fun
t)
    case Result (Term fun)
res of
      Result (Term fun)
Terms.Singleton -> do
        Term fun -> Bool
inst <- forall (m :: * -> *) s a. Monad m => (s -> a) -> StateT s m a
gets forall testcase result fun norm.
Schemas testcase result fun norm -> Term fun -> Bool
sc_instantiate_singleton
        if Term fun -> Bool
inst Term fun
t then
          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)
instantiateRep Term fun
t
         else do
          -- Add the most general instance of the schema
          forall (stateT :: * -> (* -> *) -> * -> *) s (m :: * -> *) s' a.
(MonadStateT stateT, MonadState s (stateT s m),
 MonadTrans (stateT s), Monad m) =>
Lens s s' -> stateT s' m a -> stateT s m a
zoom (forall fun testcase result norm.
Ord fun =>
Term fun
-> Lens
     (Schemas testcase result fun norm)
     (Terms testcase result (Term fun) norm)
instance_ Term fun
t) (forall term norm result testcase (m :: * -> *).
(Pretty term, Typed term, Ord norm, Ord result,
 MonadTester testcase term m, MonadPruner term norm m,
 MonadTerminal m) =>
term -> StateT (Terms testcase result term norm) m (Result term)
Terms.explore (forall f. (Type -> VariableUse) -> Term f -> Term f
mostGeneral Type -> VariableUse
use Term fun
t0))
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall fun. [Prop (Term fun)] -> Result fun
Accepted [])
      Terms.Discovered ([] :=>: Term fun
_ :=: Term fun
u) ->
        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
-> Term fun
-> StateT (Schemas testcase result fun norm) m (Result fun)
exploreIn Term fun
u Term fun
t
      Terms.Knew ([] :=>: Term fun
_ :=: Term fun
u) ->
        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
-> Term fun
-> StateT (Schemas testcase result fun norm) m (Result fun)
exploreIn Term fun
u Term fun
t
      Result (Term fun)
_ -> forall a. HasCallStack => String -> a
error String
"term layer returned non-equational property"

{-# INLINEABLE exploreIn #-}
exploreIn ::
  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,
  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>
  Term fun -> Term fun ->
  StateT (Schemas testcase result fun norm) m (Result fun)
exploreIn :: 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
-> Term fun
-> StateT (Schemas testcase result fun norm) m (Result fun)
exploreIn Term fun
rep Term fun
t = do
  -- First check if schema is redundant
  Type -> VariableUse
use <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens (Schemas testcase result fun norm) (Type -> VariableUse)
use
  Result (Term fun)
res <- forall (stateT :: * -> (* -> *) -> * -> *) s (m :: * -> *) s' a.
(MonadStateT stateT, MonadState s (stateT s m),
 MonadTrans (stateT s), Monad m) =>
Lens s s' -> stateT s' m a -> stateT s m a
zoom (forall fun testcase result norm.
Ord fun =>
Term fun
-> Lens
     (Schemas testcase result fun norm)
     (Terms testcase result (Term fun) norm)
instance_ Term fun
rep) (forall term norm result testcase (m :: * -> *).
(Pretty term, Typed term, Ord norm, Ord result,
 MonadTester testcase term m, MonadPruner term norm m,
 MonadTerminal m) =>
term -> StateT (Terms testcase result term norm) m (Result term)
Terms.explore (forall f. (Type -> VariableUse) -> Term f -> Term f
mostGeneral Type -> VariableUse
use Term fun
t))
  case Result (Term fun)
res of
    Terms.Discovered Prop (Term fun)
prop -> do
      forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add Prop (Term fun)
prop
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall fun. [Prop (Term fun)] -> Result fun
Rejected [Prop (Term fun)
prop])
    Terms.Knew Prop (Term fun)
_ ->
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall fun. [Prop (Term fun)] -> Result fun
Rejected [])
    Result (Term fun)
Terms.Singleton -> do
      -- Instantiate rep too if not already done
      Set (Term fun)
inst <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens (Schemas testcase result fun norm) (Set (Term fun))
instantiated
      [Prop (Term fun)]
props <-
        if forall a. Ord a => a -> Set a -> Bool
Set.notMember Term fun
rep Set (Term fun)
inst
        then forall fun. Result fun -> [Prop (Term fun)]
result_props forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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)
instantiateRep Term fun
rep
        else forall (m :: * -> *) a. Monad m => a -> m a
return []
      Result fun
res <- 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
-> Term fun
-> StateT (Schemas testcase result fun norm) m (Result fun)
instantiate Term fun
rep Term fun
t
      forall (m :: * -> *) a. Monad m => a -> m a
return Result fun
res { result_props :: [Prop (Term fun)]
result_props = [Prop (Term fun)]
props forall a. [a] -> [a] -> [a]
++ forall fun. Result fun -> [Prop (Term fun)]
result_props Result fun
res }

{-# INLINEABLE instantiateRep #-}
instantiateRep ::
  (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)
instantiateRep :: 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)
instantiateRep Term fun
t = do
  forall {testcase} {result} {fun} {norm}.
Lens (Schemas testcase result fun norm) (Set (Term fun))
instantiated forall a (m :: * -> *) b.
MonadState a m =>
Lens a b -> (b -> b) -> m ()
%= forall a. Ord a => a -> Set a -> Set a
Set.insert Term fun
t
  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
-> Term fun
-> StateT (Schemas testcase result fun norm) m (Result fun)
instantiate Term fun
t Term fun
t

{-# INLINEABLE instantiate #-}
instantiate ::
  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,
  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>
  Term fun -> Term fun ->
  StateT (Schemas testcase result fun norm) m (Result fun)
instantiate :: 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
-> Term fun
-> StateT (Schemas testcase result fun norm) m (Result fun)
instantiate Term fun
rep Term fun
t = do
  Type -> VariableUse
use <- forall a (m :: * -> *) b. MonadState a m => Lens a b -> m b
access forall {testcase} {result} {fun} {norm}.
Lens (Schemas testcase result fun norm) (Type -> VariableUse)
use
  forall (stateT :: * -> (* -> *) -> * -> *) s (m :: * -> *) s' a.
(MonadStateT stateT, MonadState s (stateT s m),
 MonadTrans (stateT s), Monad m) =>
Lens s s' -> stateT s' m a -> stateT s m a
zoom (forall fun testcase result norm.
Ord fun =>
Term fun
-> Lens
     (Schemas testcase result fun norm)
     (Terms testcase result (Term fun) norm)
instance_ Term fun
rep) forall a b. (a -> b) -> a -> b
$ do
    let instances :: [Term fun]
instances = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall f. Term f -> (Int, [Var])
generality) (forall fun. (Type -> VariableUse) -> Term fun -> [Term fun]
allUnifications Type -> VariableUse
use (forall f. (Type -> VariableUse) -> Term f -> Term f
mostGeneral Type -> VariableUse
use Term fun
t))
    forall fun. [Prop (Term fun)] -> Result fun
Accepted forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Term fun]
instances (\Term fun
t -> do
      Result (Term fun)
res <- forall term norm result testcase (m :: * -> *).
(Pretty term, Typed term, Ord norm, Ord result,
 MonadTester testcase term m, MonadPruner term norm m,
 MonadTerminal m) =>
term -> StateT (Terms testcase result term norm) m (Result term)
Terms.explore Term fun
t
      case Result (Term fun)
res of
        Terms.Discovered Prop (Term fun)
prop -> do
          Bool
res <- forall term norm (m :: * -> *).
MonadPruner term norm m =>
Prop term -> m Bool
add Prop (Term fun)
prop
          if Bool
res then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Prop (Term fun)
prop) else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Result (Term fun)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)

-- sortBy (comparing generality) should give most general instances first.
generality :: Term f -> (Int, [Var])
generality :: forall f. Term f -> (Int, [Var])
generality Term f
t = (-forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Ord a => [a] -> [a]
usort (forall f a. Symbolic f a => a -> [Var]
vars Term f
t)), forall f a. Symbolic f a => a -> [Var]
vars Term f
t)

mkVar :: Type -> Int -> Var
mkVar :: Type -> Int -> Var
mkVar Type
ty Int
n = Type -> Int -> Var
V Type
ty Int
m
  -- Try to make sure that variables of different types don't end up with the
  -- same number. It would be better to deal with this in QuickSpec.Term.
  -- (Note: the problem we are trying to avoid is that, if two variables have
  -- the same number and different but unifiable types, then a type substitution
  -- can turn them into the same variable.)
  where
    m :: Int
m = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Label a -> Int32
labelNum (forall a. (Typeable a, Ord a) => a -> Label a
label (Type
ty, Int
n)))

-- | Instantiate a schema by making all the variables different.
mostGeneral :: (Type -> VariableUse) -> Term f -> Term f
mostGeneral :: forall f. (Type -> VariableUse) -> Term f -> Term f
mostGeneral Type -> VariableUse
use Term f
s = forall s a. State s a -> s -> a
evalState (forall {m :: * -> *} {f}.
Monad m =>
Term f -> StateT (Map Type Int) m (Term f)
aux Term f
s) forall k a. Map k a
Map.empty
  where
    aux :: Term f -> StateT (Map Type Int) m (Term f)
aux (Var (V Type
ty Int
_)) = do
      Map Type Int
m <- forall (m :: * -> *) s. Monad m => StateT s m s
get
      let n :: Int
          n :: Int
n = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Int
0 Type
ty Map Type Int
m
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type -> VariableUse
use Type
ty forall a. Eq a => a -> a -> Bool
== Int -> VariableUse
UpTo Int
1) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put forall a b. (a -> b) -> a -> b
$! forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Type
ty (Int
nforall a. Num a => a -> a -> a
+Int
1) Map Type Int
m
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall f. Var -> Term f
Var (Type -> Int -> Var
mkVar Type
ty Int
n))
    aux (Fun f
f) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall f. f -> Term f
Fun f
f)
    aux (Term f
t :$: Term f
u) = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall f. Term f -> Term f -> Term f
(:$:) (Term f -> StateT (Map Type Int) m (Term f)
aux Term f
t) (Term f -> StateT (Map Type Int) m (Term f)
aux Term f
u)

mostSpecific :: Term f -> Term f
mostSpecific :: forall f. Term f -> Term f
mostSpecific = forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst (\(V Type
ty Int
_) -> forall f. Var -> Term f
Var (Type -> Int -> Var
mkVar Type
ty Int
0))

allUnifications :: (Type -> VariableUse) -> Term fun -> [Term fun]
allUnifications :: forall fun. (Type -> VariableUse) -> Term fun -> [Term fun]
allUnifications Type -> VariableUse
use Term fun
t =
  [ forall f a. Symbolic f a => (Var -> Term f) -> a -> a
subst (\Var
x -> forall f. Var -> Term f
Var (forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. HasCallStack => a
undefined Var
x Map Var Var
s)) Term fun
t | Map Var Var
s <- [Map Var Var]
ss ]
  where
    ss :: [Map Var Var]
ss =
      forall a b. (a -> b) -> [a] -> [b]
map forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
        [forall {a}. [a] -> Type -> [[(a, Var)]]
substsFor [Var]
xs (forall a. Typed a => a -> Type
typ Var
y) | xs :: [Var]
xs@(Var
y:[Var]
_) <- forall b a. Ord b => (a -> b) -> [a] -> [[a]]
partitionBy forall a. Typed a => a -> Type
typ (forall a. Ord a => [a] -> [a]
usort (forall f a. Symbolic f a => a -> [Var]
vars Term fun
t))]

    substsFor :: [a] -> Type -> [[(a, Var)]]
substsFor [a]
xs Type
ty =
      case Type -> VariableUse
use Type
ty of
        UpTo Int
k ->
          forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[(a
x, Var
v) | Var
v <- forall a. Int -> [a] -> [a]
take Int
k [Var]
vs] | a
x <- [a]
xs]
        VariableUse
Linear ->
          forall a b. (a -> b) -> [a] -> [b]
map (forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs) (forall a. [a] -> [[a]]
permutations (forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs) [Var]
vs))
      where
        vs :: [Var]
vs = forall a b. (a -> b) -> [a] -> [b]
map (Type -> Int -> Var
mkVar Type
ty) [Int
0..]