{-# OPTIONS_GHC -Wno-orphans #-}

module Data.OpenApi.Compare.Subtree
  ( Steppable (..),
    Step (..),
    TraceRoot,
    Trace,
    Traced,
    Traced',
    pattern Traced,
    traced,
    retraced,
    stepTraced,
    Subtree (..),
    checkCompatibility,
    checkSubstructure,
    CompatM (..),
    CompatFormula',
    SemanticCompatFormula,
    ProdCons (..),
    orientProdCons,
    swapProdCons,
    runCompatFormula,
    issueAt,
    anItem,
    anIssue,
    invertIssueOrientation,
    invertIssueOrientationP,
    embedFormula,
    anyOfAt,
    clarifyIssue,
    structuralIssue,

    -- * Structural helpers
    structuralMaybe,
    structuralMaybeWith,
    structuralEq,
    iohmStructural,
    iohmStructuralWith,
    structuralList,

    -- * Reexports
    (>>>),
    (<<<),
    extract,
    ask,
    local,
    step,
    Typeable,
  )
where

import Control.Comonad.Env
import Control.Monad.Identity
import Control.Monad.State
import Data.Foldable
import Data.Functor.Compose
import Data.HList
import qualified Data.HashMap.Strict.InsOrd as IOHM
import Data.Hashable
import Data.Kind
import Data.OpenApi
import Data.OpenApi.Compare.Behavior
import Data.OpenApi.Compare.Formula
import Data.OpenApi.Compare.Memo
import Data.OpenApi.Compare.Paths
import qualified Data.OpenApi.Compare.PathsPrefixTree as P
import qualified Data.Set as S
import Data.Typeable

class
  (Typeable Step, Typeable a, Typeable b, Ord (Step a b), Show (Step a b)) =>
  Steppable (a :: Type) (b :: Type)
  where
  -- | How to get from an @a@ node to a @b@ node
  data Step a b :: Type

data TraceRoot

instance Steppable TraceRoot OpenApi where
  data Step TraceRoot OpenApi
    = ClientSchema
    | ServerSchema
    deriving stock (Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
(Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool)
-> (Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool)
-> Eq (Step TraceRoot OpenApi)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
$c/= :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
== :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
$c== :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
Eq, Eq (Step TraceRoot OpenApi)
Eq (Step TraceRoot OpenApi)
-> (Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Ordering)
-> (Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool)
-> (Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool)
-> (Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool)
-> (Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool)
-> (Step TraceRoot OpenApi
    -> Step TraceRoot OpenApi -> Step TraceRoot OpenApi)
-> (Step TraceRoot OpenApi
    -> Step TraceRoot OpenApi -> Step TraceRoot OpenApi)
-> Ord (Step TraceRoot OpenApi)
Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Ordering
Step TraceRoot OpenApi
-> Step TraceRoot OpenApi -> Step TraceRoot OpenApi
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
min :: Step TraceRoot OpenApi
-> Step TraceRoot OpenApi -> Step TraceRoot OpenApi
$cmin :: Step TraceRoot OpenApi
-> Step TraceRoot OpenApi -> Step TraceRoot OpenApi
max :: Step TraceRoot OpenApi
-> Step TraceRoot OpenApi -> Step TraceRoot OpenApi
$cmax :: Step TraceRoot OpenApi
-> Step TraceRoot OpenApi -> Step TraceRoot OpenApi
>= :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
$c>= :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
> :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
$c> :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
<= :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
$c<= :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
< :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
$c< :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Bool
compare :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Ordering
$ccompare :: Step TraceRoot OpenApi -> Step TraceRoot OpenApi -> Ordering
$cp1Ord :: Eq (Step TraceRoot OpenApi)
Ord, Int -> Step TraceRoot OpenApi -> ShowS
[Step TraceRoot OpenApi] -> ShowS
Step TraceRoot OpenApi -> String
(Int -> Step TraceRoot OpenApi -> ShowS)
-> (Step TraceRoot OpenApi -> String)
-> ([Step TraceRoot OpenApi] -> ShowS)
-> Show (Step TraceRoot OpenApi)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Step TraceRoot OpenApi] -> ShowS
$cshowList :: [Step TraceRoot OpenApi] -> ShowS
show :: Step TraceRoot OpenApi -> String
$cshow :: Step TraceRoot OpenApi -> String
showsPrec :: Int -> Step TraceRoot OpenApi -> ShowS
$cshowsPrec :: Int -> Step TraceRoot OpenApi -> ShowS
Show)

type Trace = Paths Step TraceRoot

type instance AdditionalQuiverConstraints Step _ _ = ()

type Traced' a b = Env (Trace a) b

type Traced a = Traced' a a

pattern Traced :: Trace a -> b -> Traced' a b
pattern $bTraced :: Trace a -> b -> Traced' a b
$mTraced :: forall r a b.
Traced' a b -> (Trace a -> b -> r) -> (Void# -> r) -> r
Traced t x = EnvT t (Identity x)

{-# COMPLETE Traced #-}

traced :: Trace a -> a -> Traced a
traced :: Trace a -> a -> Traced a
traced = Trace a -> a -> Traced a
forall e a. e -> a -> Env e a
env

retraced :: (Trace a -> Trace a') -> Traced' a b -> Traced' a' b
retraced :: (Trace a -> Trace a') -> Traced' a b -> Traced' a' b
retraced Trace a -> Trace a'
f (Traced Trace a
a b
b) = Trace a' -> b -> Traced' a' b
forall a b. Trace a -> b -> Traced' a b
Traced (Trace a -> Trace a'
f Trace a
a) b
b

stepTraced :: Steppable a a' => Step a a' -> Traced' a b -> Traced' a' b
stepTraced :: Step a a' -> Traced' a b -> Traced' a' b
stepTraced Step a a'
s = (Trace a -> Trace a') -> Traced' a b -> Traced' a' b
forall a a' b. (Trace a -> Trace a') -> Traced' a b -> Traced' a' b
retraced (Trace a -> Paths Step a a' -> Trace a'
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Step a a' -> Paths Step a a'
forall k (q :: k -> k -> *) (a :: k) (b :: k).
NiceQuiver q a b =>
q a b -> Paths q a b
step Step a a'
s)

data ProdCons a = ProdCons
  { ProdCons a -> a
producer :: a
  , ProdCons a -> a
consumer :: a
  }
  deriving stock (ProdCons a -> ProdCons a -> Bool
(ProdCons a -> ProdCons a -> Bool)
-> (ProdCons a -> ProdCons a -> Bool) -> Eq (ProdCons a)
forall a. Eq a => ProdCons a -> ProdCons a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProdCons a -> ProdCons a -> Bool
$c/= :: forall a. Eq a => ProdCons a -> ProdCons a -> Bool
== :: ProdCons a -> ProdCons a -> Bool
$c== :: forall a. Eq a => ProdCons a -> ProdCons a -> Bool
Eq, Eq (ProdCons a)
Eq (ProdCons a)
-> (ProdCons a -> ProdCons a -> Ordering)
-> (ProdCons a -> ProdCons a -> Bool)
-> (ProdCons a -> ProdCons a -> Bool)
-> (ProdCons a -> ProdCons a -> Bool)
-> (ProdCons a -> ProdCons a -> Bool)
-> (ProdCons a -> ProdCons a -> ProdCons a)
-> (ProdCons a -> ProdCons a -> ProdCons a)
-> Ord (ProdCons a)
ProdCons a -> ProdCons a -> Bool
ProdCons a -> ProdCons a -> Ordering
ProdCons a -> ProdCons a -> ProdCons a
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 a. Ord a => Eq (ProdCons a)
forall a. Ord a => ProdCons a -> ProdCons a -> Bool
forall a. Ord a => ProdCons a -> ProdCons a -> Ordering
forall a. Ord a => ProdCons a -> ProdCons a -> ProdCons a
min :: ProdCons a -> ProdCons a -> ProdCons a
$cmin :: forall a. Ord a => ProdCons a -> ProdCons a -> ProdCons a
max :: ProdCons a -> ProdCons a -> ProdCons a
$cmax :: forall a. Ord a => ProdCons a -> ProdCons a -> ProdCons a
>= :: ProdCons a -> ProdCons a -> Bool
$c>= :: forall a. Ord a => ProdCons a -> ProdCons a -> Bool
> :: ProdCons a -> ProdCons a -> Bool
$c> :: forall a. Ord a => ProdCons a -> ProdCons a -> Bool
<= :: ProdCons a -> ProdCons a -> Bool
$c<= :: forall a. Ord a => ProdCons a -> ProdCons a -> Bool
< :: ProdCons a -> ProdCons a -> Bool
$c< :: forall a. Ord a => ProdCons a -> ProdCons a -> Bool
compare :: ProdCons a -> ProdCons a -> Ordering
$ccompare :: forall a. Ord a => ProdCons a -> ProdCons a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (ProdCons a)
Ord, Int -> ProdCons a -> ShowS
[ProdCons a] -> ShowS
ProdCons a -> String
(Int -> ProdCons a -> ShowS)
-> (ProdCons a -> String)
-> ([ProdCons a] -> ShowS)
-> Show (ProdCons a)
forall a. Show a => Int -> ProdCons a -> ShowS
forall a. Show a => [ProdCons a] -> ShowS
forall a. Show a => ProdCons a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProdCons a] -> ShowS
$cshowList :: forall a. Show a => [ProdCons a] -> ShowS
show :: ProdCons a -> String
$cshow :: forall a. Show a => ProdCons a -> String
showsPrec :: Int -> ProdCons a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> ProdCons a -> ShowS
Show, a -> ProdCons b -> ProdCons a
(a -> b) -> ProdCons a -> ProdCons b
(forall a b. (a -> b) -> ProdCons a -> ProdCons b)
-> (forall a b. a -> ProdCons b -> ProdCons a) -> Functor ProdCons
forall a b. a -> ProdCons b -> ProdCons a
forall a b. (a -> b) -> ProdCons a -> ProdCons b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> ProdCons b -> ProdCons a
$c<$ :: forall a b. a -> ProdCons b -> ProdCons a
fmap :: (a -> b) -> ProdCons a -> ProdCons b
$cfmap :: forall a b. (a -> b) -> ProdCons a -> ProdCons b
Functor, ProdCons a -> Bool
(a -> m) -> ProdCons a -> m
(a -> b -> b) -> b -> ProdCons a -> b
(forall m. Monoid m => ProdCons m -> m)
-> (forall m a. Monoid m => (a -> m) -> ProdCons a -> m)
-> (forall m a. Monoid m => (a -> m) -> ProdCons a -> m)
-> (forall a b. (a -> b -> b) -> b -> ProdCons a -> b)
-> (forall a b. (a -> b -> b) -> b -> ProdCons a -> b)
-> (forall b a. (b -> a -> b) -> b -> ProdCons a -> b)
-> (forall b a. (b -> a -> b) -> b -> ProdCons a -> b)
-> (forall a. (a -> a -> a) -> ProdCons a -> a)
-> (forall a. (a -> a -> a) -> ProdCons a -> a)
-> (forall a. ProdCons a -> [a])
-> (forall a. ProdCons a -> Bool)
-> (forall a. ProdCons a -> Int)
-> (forall a. Eq a => a -> ProdCons a -> Bool)
-> (forall a. Ord a => ProdCons a -> a)
-> (forall a. Ord a => ProdCons a -> a)
-> (forall a. Num a => ProdCons a -> a)
-> (forall a. Num a => ProdCons a -> a)
-> Foldable ProdCons
forall a. Eq a => a -> ProdCons a -> Bool
forall a. Num a => ProdCons a -> a
forall a. Ord a => ProdCons a -> a
forall m. Monoid m => ProdCons m -> m
forall a. ProdCons a -> Bool
forall a. ProdCons a -> Int
forall a. ProdCons a -> [a]
forall a. (a -> a -> a) -> ProdCons a -> a
forall m a. Monoid m => (a -> m) -> ProdCons a -> m
forall b a. (b -> a -> b) -> b -> ProdCons a -> b
forall a b. (a -> b -> b) -> b -> ProdCons a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: ProdCons a -> a
$cproduct :: forall a. Num a => ProdCons a -> a
sum :: ProdCons a -> a
$csum :: forall a. Num a => ProdCons a -> a
minimum :: ProdCons a -> a
$cminimum :: forall a. Ord a => ProdCons a -> a
maximum :: ProdCons a -> a
$cmaximum :: forall a. Ord a => ProdCons a -> a
elem :: a -> ProdCons a -> Bool
$celem :: forall a. Eq a => a -> ProdCons a -> Bool
length :: ProdCons a -> Int
$clength :: forall a. ProdCons a -> Int
null :: ProdCons a -> Bool
$cnull :: forall a. ProdCons a -> Bool
toList :: ProdCons a -> [a]
$ctoList :: forall a. ProdCons a -> [a]
foldl1 :: (a -> a -> a) -> ProdCons a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> ProdCons a -> a
foldr1 :: (a -> a -> a) -> ProdCons a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> ProdCons a -> a
foldl' :: (b -> a -> b) -> b -> ProdCons a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> ProdCons a -> b
foldl :: (b -> a -> b) -> b -> ProdCons a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> ProdCons a -> b
foldr' :: (a -> b -> b) -> b -> ProdCons a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> ProdCons a -> b
foldr :: (a -> b -> b) -> b -> ProdCons a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> ProdCons a -> b
foldMap' :: (a -> m) -> ProdCons a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> ProdCons a -> m
foldMap :: (a -> m) -> ProdCons a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> ProdCons a -> m
fold :: ProdCons m -> m
$cfold :: forall m. Monoid m => ProdCons m -> m
Foldable, Functor ProdCons
Foldable ProdCons
Functor ProdCons
-> Foldable ProdCons
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> ProdCons a -> f (ProdCons b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    ProdCons (f a) -> f (ProdCons a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> ProdCons a -> m (ProdCons b))
-> (forall (m :: * -> *) a.
    Monad m =>
    ProdCons (m a) -> m (ProdCons a))
-> Traversable ProdCons
(a -> f b) -> ProdCons a -> f (ProdCons b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => ProdCons (m a) -> m (ProdCons a)
forall (f :: * -> *) a.
Applicative f =>
ProdCons (f a) -> f (ProdCons a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ProdCons a -> m (ProdCons b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ProdCons a -> f (ProdCons b)
sequence :: ProdCons (m a) -> m (ProdCons a)
$csequence :: forall (m :: * -> *) a. Monad m => ProdCons (m a) -> m (ProdCons a)
mapM :: (a -> m b) -> ProdCons a -> m (ProdCons b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> ProdCons a -> m (ProdCons b)
sequenceA :: ProdCons (f a) -> f (ProdCons a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
ProdCons (f a) -> f (ProdCons a)
traverse :: (a -> f b) -> ProdCons a -> f (ProdCons b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> ProdCons a -> f (ProdCons b)
$cp2Traversable :: Foldable ProdCons
$cp1Traversable :: Functor ProdCons
Traversable)

orientProdCons :: Orientation -> ProdCons x -> ProdCons x
orientProdCons :: Orientation -> ProdCons x -> ProdCons x
orientProdCons Orientation
Forward ProdCons x
x = ProdCons x
x
orientProdCons Orientation
Backward (ProdCons x
p x
c) = x -> x -> ProdCons x
forall a. a -> a -> ProdCons a
ProdCons x
c x
p

swapProdCons ::
  SwapEnvRoles xs =>
  (HList xs -> ProdCons x -> CompatFormula' q AnIssue r a) ->
  (HList xs -> ProdCons x -> CompatFormula' q AnIssue r a)
swapProdCons :: (HList xs -> ProdCons x -> CompatFormula' q AnIssue r a)
-> HList xs -> ProdCons x -> CompatFormula' q AnIssue r a
swapProdCons HList xs -> ProdCons x -> CompatFormula' q AnIssue r a
f HList xs
e (ProdCons x
p x
c) =
  CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a
forall (q :: BehaviorLevel -> BehaviorLevel -> *)
       (r :: BehaviorLevel) a.
CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a
invertIssueOrientation (CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a)
-> CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a
forall a b. (a -> b) -> a -> b
$
    HList xs -> ProdCons x -> CompatFormula' q AnIssue r a
f (HList xs -> HList xs
forall (xs :: [*]). SwapEnvRoles xs => HList xs -> HList xs
swapEnvRoles HList xs
e) (x -> x -> ProdCons x
forall a. a -> a -> ProdCons a
ProdCons x
c x
p)
{-# INLINE swapProdCons #-}

type family IsProdCons (x :: Type) :: Bool where
  IsProdCons (ProdCons _) = 'True
  IsProdCons _ = 'False

type SwapEnvElementRoles x = SwapEnvElementRoles' x (IsProdCons x)

class IsProdCons x ~ f => SwapEnvElementRoles' (x :: Type) f where
  swapEnvElementRoles :: x -> x

instance SwapEnvElementRoles' (ProdCons x) 'True where
  swapEnvElementRoles :: ProdCons x -> ProdCons x
swapEnvElementRoles (ProdCons x
p x
c) = x -> x -> ProdCons x
forall a. a -> a -> ProdCons a
ProdCons x
c x
p

instance IsProdCons x ~ 'False => SwapEnvElementRoles' x 'False where
  swapEnvElementRoles :: x -> x
swapEnvElementRoles = x -> x
forall a. a -> a
id

class SwapEnvRoles xs where
  swapEnvRoles :: HList xs -> HList xs

instance SwapEnvRoles '[] where
  swapEnvRoles :: HList '[] -> HList '[]
swapEnvRoles = HList '[] -> HList '[]
forall a. a -> a
id

instance (SwapEnvElementRoles x, SwapEnvRoles xs) => SwapEnvRoles (x ': xs) where
  swapEnvRoles :: HList (x : xs) -> HList (x : xs)
swapEnvRoles (HCons x
x HList xs
xs) = x -> HList xs -> HList (x : xs)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons (x -> x
forall x (f :: Bool). SwapEnvElementRoles' x f => x -> x
swapEnvElementRoles x
x) (HList xs -> HList xs
forall (xs :: [*]). SwapEnvRoles xs => HList xs -> HList xs
swapEnvRoles HList xs
xs)

instance Applicative ProdCons where
  pure :: a -> ProdCons a
pure a
x = a -> a -> ProdCons a
forall a. a -> a -> ProdCons a
ProdCons a
x a
x
  ProdCons a -> b
fp a -> b
fc <*> :: ProdCons (a -> b) -> ProdCons a -> ProdCons b
<*> ProdCons a
xp a
xc = b -> b -> ProdCons b
forall a. a -> a -> ProdCons a
ProdCons (a -> b
fp a
xp) (a -> b
fc a
xc)

newtype CompatM a = CompatM
  { CompatM a -> StateT (MemoState Int) Identity a
unCompatM ::
      StateT (MemoState VarRef) Identity a
  }
  deriving newtype
    ( a -> CompatM b -> CompatM a
(a -> b) -> CompatM a -> CompatM b
(forall a b. (a -> b) -> CompatM a -> CompatM b)
-> (forall a b. a -> CompatM b -> CompatM a) -> Functor CompatM
forall a b. a -> CompatM b -> CompatM a
forall a b. (a -> b) -> CompatM a -> CompatM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> CompatM b -> CompatM a
$c<$ :: forall a b. a -> CompatM b -> CompatM a
fmap :: (a -> b) -> CompatM a -> CompatM b
$cfmap :: forall a b. (a -> b) -> CompatM a -> CompatM b
Functor
    , Functor CompatM
a -> CompatM a
Functor CompatM
-> (forall a. a -> CompatM a)
-> (forall a b. CompatM (a -> b) -> CompatM a -> CompatM b)
-> (forall a b c.
    (a -> b -> c) -> CompatM a -> CompatM b -> CompatM c)
-> (forall a b. CompatM a -> CompatM b -> CompatM b)
-> (forall a b. CompatM a -> CompatM b -> CompatM a)
-> Applicative CompatM
CompatM a -> CompatM b -> CompatM b
CompatM a -> CompatM b -> CompatM a
CompatM (a -> b) -> CompatM a -> CompatM b
(a -> b -> c) -> CompatM a -> CompatM b -> CompatM c
forall a. a -> CompatM a
forall a b. CompatM a -> CompatM b -> CompatM a
forall a b. CompatM a -> CompatM b -> CompatM b
forall a b. CompatM (a -> b) -> CompatM a -> CompatM b
forall a b c. (a -> b -> c) -> CompatM a -> CompatM b -> CompatM 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
<* :: CompatM a -> CompatM b -> CompatM a
$c<* :: forall a b. CompatM a -> CompatM b -> CompatM a
*> :: CompatM a -> CompatM b -> CompatM b
$c*> :: forall a b. CompatM a -> CompatM b -> CompatM b
liftA2 :: (a -> b -> c) -> CompatM a -> CompatM b -> CompatM c
$cliftA2 :: forall a b c. (a -> b -> c) -> CompatM a -> CompatM b -> CompatM c
<*> :: CompatM (a -> b) -> CompatM a -> CompatM b
$c<*> :: forall a b. CompatM (a -> b) -> CompatM a -> CompatM b
pure :: a -> CompatM a
$cpure :: forall a. a -> CompatM a
$cp1Applicative :: Functor CompatM
Applicative
    , Applicative CompatM
a -> CompatM a
Applicative CompatM
-> (forall a b. CompatM a -> (a -> CompatM b) -> CompatM b)
-> (forall a b. CompatM a -> CompatM b -> CompatM b)
-> (forall a. a -> CompatM a)
-> Monad CompatM
CompatM a -> (a -> CompatM b) -> CompatM b
CompatM a -> CompatM b -> CompatM b
forall a. a -> CompatM a
forall a b. CompatM a -> CompatM b -> CompatM b
forall a b. CompatM a -> (a -> CompatM b) -> CompatM 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 :: a -> CompatM a
$creturn :: forall a. a -> CompatM a
>> :: CompatM a -> CompatM b -> CompatM b
$c>> :: forall a b. CompatM a -> CompatM b -> CompatM b
>>= :: CompatM a -> (a -> CompatM b) -> CompatM b
$c>>= :: forall a b. CompatM a -> (a -> CompatM b) -> CompatM b
$cp1Monad :: Applicative CompatM
Monad
    , MonadState (MemoState VarRef)
    )

type CompatFormula' q f r = Compose CompatM (FormulaF q f r)

type SemanticCompatFormula = CompatFormula' Behave AnIssue 'APILevel

type StructuralCompatFormula = CompatFormula' VoidQuiver Proxy ()

data VoidQuiver a b

deriving stock instance Eq (VoidQuiver a b)

type instance AdditionalQuiverConstraints VoidQuiver _ _ = ()

deriving stock instance Ord (VoidQuiver a b)

deriving stock instance Show (VoidQuiver a b)

class (Typeable t, Issuable (SubtreeLevel t)) => Subtree (t :: Type) where
  type CheckEnv t :: [Type]
  type SubtreeLevel t :: BehaviorLevel

  checkStructuralCompatibility ::
    HList (CheckEnv t) ->
    ProdCons (Traced t) ->
    StructuralCompatFormula ()

  checkSemanticCompatibility ::
    HList (CheckEnv t) ->
    Behavior (SubtreeLevel t) ->
    ProdCons (Traced t) ->
    SemanticCompatFormula ()

{-# WARNING checkStructuralCompatibility "You should not be calling this directly. Use 'checkSubstructure'" #-}

{-# WARNING checkSemanticCompatibility "You should not be calling this directly. Use 'checkCompatibility'" #-}

checkCompatibility ::
  forall t xs.
  (ReassembleHList xs (CheckEnv t), Subtree t) =>
  Behavior (SubtreeLevel t) ->
  HList xs ->
  ProdCons (Traced t) ->
  SemanticCompatFormula ()
checkCompatibility :: Behavior (SubtreeLevel t)
-> HList xs -> ProdCons (Traced t) -> SemanticCompatFormula ()
checkCompatibility Behavior (SubtreeLevel t)
bhv HList xs
e = Behavior (SubtreeLevel t)
-> MemoKey
-> (ProdCons (Traced t) -> SemanticCompatFormula ())
-> ProdCons (Traced t)
-> SemanticCompatFormula ()
forall k (l :: k) (q :: k -> k -> *) (f :: k -> *) a (r :: k).
(Typeable l, Typeable q, Typeable f, Typeable k, Typeable a) =>
Paths q r l
-> MemoKey
-> (ProdCons (Traced a) -> CompatFormula' q f r ())
-> ProdCons (Traced a)
-> CompatFormula' q f r ()
memo Behavior (SubtreeLevel t)
bhv MemoKey
SemanticMemoKey ((ProdCons (Traced t) -> SemanticCompatFormula ())
 -> ProdCons (Traced t) -> SemanticCompatFormula ())
-> (ProdCons (Traced t) -> SemanticCompatFormula ())
-> ProdCons (Traced t)
-> SemanticCompatFormula ()
forall a b. (a -> b) -> a -> b
$ \ProdCons (Traced t)
pc ->
  case CompatFormula' VoidQuiver Proxy () ()
-> Either (PathsPrefixTree VoidQuiver Proxy ()) ()
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
CompatFormula' q f r a -> Either (PathsPrefixTree q f r) a
runCompatFormula (CompatFormula' VoidQuiver Proxy () ()
 -> Either (PathsPrefixTree VoidQuiver Proxy ()) ())
-> CompatFormula' VoidQuiver Proxy () ()
-> Either (PathsPrefixTree VoidQuiver Proxy ()) ()
forall a b. (a -> b) -> a -> b
$ HList xs
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
forall (xs :: [*]) t.
(ReassembleHList xs (CheckEnv t), Subtree t) =>
HList xs
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
checkSubstructure HList xs
e ProdCons (Traced t)
pc of
    Left PathsPrefixTree VoidQuiver Proxy ()
_ -> HList (CheckEnv t)
-> Behavior (SubtreeLevel t)
-> ProdCons (Traced t)
-> SemanticCompatFormula ()
forall t.
Subtree t =>
HList (CheckEnv t)
-> Behavior (SubtreeLevel t)
-> ProdCons (Traced t)
-> SemanticCompatFormula ()
checkSemanticCompatibility (HList xs -> HList (CheckEnv t)
forall (xs :: [*]) (ys :: [*]) (f :: Bool).
ReassembleHList' xs ys f =>
HList xs -> HList ys
reassemble HList xs
e) Behavior (SubtreeLevel t)
bhv ProdCons (Traced t)
pc
    Right () -> () -> SemanticCompatFormula ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
{-# INLINE checkCompatibility #-}

checkSubstructure ::
  (ReassembleHList xs (CheckEnv t), Subtree t) =>
  HList xs ->
  ProdCons (Traced t) ->
  StructuralCompatFormula ()
checkSubstructure :: HList xs
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
checkSubstructure HList xs
e = Paths VoidQuiver () ()
-> MemoKey
-> (ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Traced t)
-> CompatFormula' VoidQuiver Proxy () ()
forall k (l :: k) (q :: k -> k -> *) (f :: k -> *) a (r :: k).
(Typeable l, Typeable q, Typeable f, Typeable k, Typeable a) =>
Paths q r l
-> MemoKey
-> (ProdCons (Traced a) -> CompatFormula' q f r ())
-> ProdCons (Traced a)
-> CompatFormula' q f r ()
memo Paths VoidQuiver () ()
forall k (q :: k -> k -> *) (a :: k). Paths q a a
Root MemoKey
StructuralMemoKey ((ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ())
 -> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ())
-> (ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Traced t)
-> CompatFormula' VoidQuiver Proxy () ()
forall a b. (a -> b) -> a -> b
$ HList (CheckEnv t)
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
forall t.
Subtree t =>
HList (CheckEnv t)
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
checkStructuralCompatibility (HList xs -> HList (CheckEnv t)
forall (xs :: [*]) (ys :: [*]) (f :: Bool).
ReassembleHList' xs ys f =>
HList xs -> HList ys
reassemble HList xs
e)
{-# INLINE checkSubstructure #-}

structuralMaybe ::
  (Subtree a, ReassembleHList xs (CheckEnv a)) =>
  HList xs ->
  ProdCons (Maybe (Traced a)) ->
  StructuralCompatFormula ()
structuralMaybe :: HList xs
-> ProdCons (Maybe (Traced a))
-> CompatFormula' VoidQuiver Proxy () ()
structuralMaybe HList xs
e = (ProdCons (Traced a) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Maybe (Traced a))
-> CompatFormula' VoidQuiver Proxy () ()
forall a.
(ProdCons a -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Maybe a) -> CompatFormula' VoidQuiver Proxy () ()
structuralMaybeWith (HList xs
-> ProdCons (Traced a) -> CompatFormula' VoidQuiver Proxy () ()
forall (xs :: [*]) t.
(ReassembleHList xs (CheckEnv t), Subtree t) =>
HList xs
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
checkSubstructure HList xs
e)
{-# INLINE structuralMaybe #-}

structuralMaybeWith ::
  (ProdCons a -> StructuralCompatFormula ()) ->
  ProdCons (Maybe a) ->
  StructuralCompatFormula ()
structuralMaybeWith :: (ProdCons a -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Maybe a) -> CompatFormula' VoidQuiver Proxy () ()
structuralMaybeWith ProdCons a -> CompatFormula' VoidQuiver Proxy () ()
f (ProdCons (Just a
a) (Just a
b)) = ProdCons a -> CompatFormula' VoidQuiver Proxy () ()
f (ProdCons a -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons a -> CompatFormula' VoidQuiver Proxy () ()
forall a b. (a -> b) -> a -> b
$ a -> a -> ProdCons a
forall a. a -> a -> ProdCons a
ProdCons a
a a
b
structuralMaybeWith ProdCons a -> CompatFormula' VoidQuiver Proxy () ()
_ (ProdCons Maybe a
Nothing Maybe a
Nothing) = () -> CompatFormula' VoidQuiver Proxy () ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
structuralMaybeWith ProdCons a -> CompatFormula' VoidQuiver Proxy () ()
_ ProdCons (Maybe a)
_ = CompatFormula' VoidQuiver Proxy () ()
forall a. StructuralCompatFormula a
structuralIssue
{-# INLINE structuralMaybeWith #-}

structuralList ::
  (Subtree a, ReassembleHList xs (CheckEnv a)) =>
  HList xs ->
  ProdCons [Traced a] ->
  StructuralCompatFormula ()
structuralList :: HList xs
-> ProdCons [Traced a] -> CompatFormula' VoidQuiver Proxy () ()
structuralList HList xs
_ (ProdCons [] []) = () -> CompatFormula' VoidQuiver Proxy () ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
structuralList HList xs
e (ProdCons (Traced a
a : [Traced a]
aa) (Traced a
b : [Traced a]
bb)) = do
  HList xs
-> ProdCons (Traced a) -> CompatFormula' VoidQuiver Proxy () ()
forall (xs :: [*]) t.
(ReassembleHList xs (CheckEnv t), Subtree t) =>
HList xs
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
checkSubstructure HList xs
e (ProdCons (Traced a) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Traced a) -> CompatFormula' VoidQuiver Proxy () ()
forall a b. (a -> b) -> a -> b
$ Traced a -> Traced a -> ProdCons (Traced a)
forall a. a -> a -> ProdCons a
ProdCons Traced a
a Traced a
b
  HList xs
-> ProdCons [Traced a] -> CompatFormula' VoidQuiver Proxy () ()
forall a (xs :: [*]).
(Subtree a, ReassembleHList xs (CheckEnv a)) =>
HList xs
-> ProdCons [Traced a] -> CompatFormula' VoidQuiver Proxy () ()
structuralList HList xs
e (ProdCons [Traced a] -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons [Traced a] -> CompatFormula' VoidQuiver Proxy () ()
forall a b. (a -> b) -> a -> b
$ [Traced a] -> [Traced a] -> ProdCons [Traced a]
forall a. a -> a -> ProdCons a
ProdCons [Traced a]
aa [Traced a]
bb
  pure ()
structuralList HList xs
_ ProdCons [Traced a]
_ = CompatFormula' VoidQuiver Proxy () ()
forall a. StructuralCompatFormula a
structuralIssue
{-# INLINE structuralList #-}

structuralEq :: (Eq a, Comonad w) => ProdCons (w a) -> StructuralCompatFormula ()
structuralEq :: ProdCons (w a) -> CompatFormula' VoidQuiver Proxy () ()
structuralEq (ProdCons w a
a w a
b) = if w a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract w a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== w a -> a
forall (w :: * -> *) a. Comonad w => w a -> a
extract w a
b then () -> CompatFormula' VoidQuiver Proxy () ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure () else CompatFormula' VoidQuiver Proxy () ()
forall a. StructuralCompatFormula a
structuralIssue
{-# INLINE structuralEq #-}

iohmStructural ::
  (ReassembleHList (k ': xs) (CheckEnv v), Ord k, Subtree v, Hashable k, Typeable k, Show k) =>
  HList xs ->
  ProdCons (Traced (IOHM.InsOrdHashMap k v)) ->
  StructuralCompatFormula ()
iohmStructural :: HList xs
-> ProdCons (Traced (InsOrdHashMap k v))
-> CompatFormula' VoidQuiver Proxy () ()
iohmStructural HList xs
e =
  (k -> ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Traced (InsOrdHashMap k v))
-> CompatFormula' VoidQuiver Proxy () ()
forall k v.
(Ord k, Hashable k, Typeable k, Typeable v, Show k) =>
(k -> ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Traced (InsOrdHashMap k v))
-> CompatFormula' VoidQuiver Proxy () ()
iohmStructuralWith (\k
k -> HList (k : xs)
-> ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ()
forall (xs :: [*]) t.
(ReassembleHList xs (CheckEnv t), Subtree t) =>
HList xs
-> ProdCons (Traced t) -> CompatFormula' VoidQuiver Proxy () ()
checkSubstructure (k
k k -> HList xs -> HList (k : xs)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xs
e))
{-# INLINE iohmStructural #-}

instance (Typeable k, Typeable v, Ord k, Show k) => Steppable (IOHM.InsOrdHashMap k v) v where
  data Step (IOHM.InsOrdHashMap k v) v = InsOrdHashMapKeyStep k
    deriving stock (Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
(Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Bool)
-> Eq (Step (InsOrdHashMap k v) v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k v.
Eq k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
/= :: Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
$c/= :: forall k v.
Eq k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
== :: Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
$c== :: forall k v.
Eq k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
Eq, Eq (Step (InsOrdHashMap k v) v)
Eq (Step (InsOrdHashMap k v) v)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Ordering)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Bool)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Bool)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Bool)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Bool)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v)
-> (Step (InsOrdHashMap k v) v
    -> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v)
-> Ord (Step (InsOrdHashMap k v) v)
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Ordering
Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v
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 k v. Ord k => Eq (Step (InsOrdHashMap k v) v)
forall k v.
Ord k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
forall k v.
Ord k =>
Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Ordering
forall k v.
Ord k =>
Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v
min :: Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v
$cmin :: forall k v.
Ord k =>
Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v
max :: Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v
$cmax :: forall k v.
Ord k =>
Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v
>= :: Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
$c>= :: forall k v.
Ord k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
> :: Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
$c> :: forall k v.
Ord k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
<= :: Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
$c<= :: forall k v.
Ord k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
< :: Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
$c< :: forall k v.
Ord k =>
Step (InsOrdHashMap k v) v -> Step (InsOrdHashMap k v) v -> Bool
compare :: Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Ordering
$ccompare :: forall k v.
Ord k =>
Step (InsOrdHashMap k v) v
-> Step (InsOrdHashMap k v) v -> Ordering
$cp1Ord :: forall k v. Ord k => Eq (Step (InsOrdHashMap k v) v)
Ord, Int -> Step (InsOrdHashMap k v) v -> ShowS
[Step (InsOrdHashMap k v) v] -> ShowS
Step (InsOrdHashMap k v) v -> String
(Int -> Step (InsOrdHashMap k v) v -> ShowS)
-> (Step (InsOrdHashMap k v) v -> String)
-> ([Step (InsOrdHashMap k v) v] -> ShowS)
-> Show (Step (InsOrdHashMap k v) v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k v. Show k => Int -> Step (InsOrdHashMap k v) v -> ShowS
forall k v. Show k => [Step (InsOrdHashMap k v) v] -> ShowS
forall k v. Show k => Step (InsOrdHashMap k v) v -> String
showList :: [Step (InsOrdHashMap k v) v] -> ShowS
$cshowList :: forall k v. Show k => [Step (InsOrdHashMap k v) v] -> ShowS
show :: Step (InsOrdHashMap k v) v -> String
$cshow :: forall k v. Show k => Step (InsOrdHashMap k v) v -> String
showsPrec :: Int -> Step (InsOrdHashMap k v) v -> ShowS
$cshowsPrec :: forall k v. Show k => Int -> Step (InsOrdHashMap k v) v -> ShowS
Show)

iohmStructuralWith ::
  (Ord k, Hashable k, Typeable k, Typeable v, Show k) =>
  (k -> ProdCons (Traced v) -> StructuralCompatFormula ()) ->
  ProdCons (Traced (IOHM.InsOrdHashMap k v)) ->
  StructuralCompatFormula ()
iohmStructuralWith :: (k -> ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Traced (InsOrdHashMap k v))
-> CompatFormula' VoidQuiver Proxy () ()
iohmStructuralWith k -> ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ()
f ProdCons (Traced (InsOrdHashMap k v))
pc = do
  let ProdCons Set k
pEKeys Set k
cEKeys = [k] -> Set k
forall a. Ord a => [a] -> Set a
S.fromList ([k] -> Set k)
-> (Traced (InsOrdHashMap k v) -> [k])
-> Traced (InsOrdHashMap k v)
-> Set k
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InsOrdHashMap k v -> [k]
forall k v. InsOrdHashMap k v -> [k]
IOHM.keys (InsOrdHashMap k v -> [k])
-> (Traced (InsOrdHashMap k v) -> InsOrdHashMap k v)
-> Traced (InsOrdHashMap k v)
-> [k]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Traced (InsOrdHashMap k v) -> InsOrdHashMap k v
forall (w :: * -> *) a. Comonad w => w a -> a
extract (Traced (InsOrdHashMap k v) -> Set k)
-> ProdCons (Traced (InsOrdHashMap k v)) -> ProdCons (Set k)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProdCons (Traced (InsOrdHashMap k v))
pc
  if Set k
pEKeys Set k -> Set k -> Bool
forall a. Eq a => a -> a -> Bool
== Set k
cEKeys
    then
      Set k
-> (k -> CompatFormula' VoidQuiver Proxy () ())
-> CompatFormula' VoidQuiver Proxy () ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_
        Set k
pEKeys
        ( \k
eKey ->
            k -> ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ()
f k
eKey (ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ())
-> ProdCons (Traced v) -> CompatFormula' VoidQuiver Proxy () ()
forall a b. (a -> b) -> a -> b
$ Step (InsOrdHashMap k v) v
-> Traced' (InsOrdHashMap k v) v -> Traced v
forall a a' b.
Steppable a a' =>
Step a a' -> Traced' a b -> Traced' a' b
stepTraced (k -> Step (InsOrdHashMap k v) v
forall k v. k -> Step (InsOrdHashMap k v) v
InsOrdHashMapKeyStep k
eKey) (Traced' (InsOrdHashMap k v) v -> Traced v)
-> (Traced (InsOrdHashMap k v) -> Traced' (InsOrdHashMap k v) v)
-> Traced (InsOrdHashMap k v)
-> Traced v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InsOrdHashMap k v -> v)
-> Traced (InsOrdHashMap k v) -> Traced' (InsOrdHashMap k v) v
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (v -> k -> InsOrdHashMap k v -> v
forall k v. (Eq k, Hashable k) => v -> k -> InsOrdHashMap k v -> v
IOHM.lookupDefault (String -> v
forall a. HasCallStack => String -> a
error String
"impossible") k
eKey) (Traced (InsOrdHashMap k v) -> Traced v)
-> ProdCons (Traced (InsOrdHashMap k v)) -> ProdCons (Traced v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProdCons (Traced (InsOrdHashMap k v))
pc
        )
    else CompatFormula' VoidQuiver Proxy () ()
forall a. StructuralCompatFormula a
structuralIssue
{-# INLINE iohmStructuralWith #-}

runCompatFormula ::
  CompatFormula' q f r a ->
  Either (P.PathsPrefixTree q f r) a
runCompatFormula :: CompatFormula' q f r a -> Either (PathsPrefixTree q f r) a
runCompatFormula (Compose CompatM (FormulaF q f r a)
f) =
  FormulaF q f r a -> Either (PathsPrefixTree q f r) a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
FormulaF q f r a -> Either (PathsPrefixTree q f r) a
calculate (FormulaF q f r a -> Either (PathsPrefixTree q f r) a)
-> (CompatM (FormulaF q f r a) -> FormulaF q f r a)
-> CompatM (FormulaF q f r a)
-> Either (PathsPrefixTree q f r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (FormulaF q f r a) -> FormulaF q f r a
forall a. Identity a -> a
runIdentity (Identity (FormulaF q f r a) -> FormulaF q f r a)
-> (CompatM (FormulaF q f r a) -> Identity (FormulaF q f r a))
-> CompatM (FormulaF q f r a)
-> FormulaF q f r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> StateT (MemoState Int) Identity (FormulaF q f r a)
-> Identity (FormulaF q f r a)
forall (m :: * -> *) s a.
Monad m =>
s -> StateT (MemoState s) m a -> m a
runMemo Int
0 (StateT (MemoState Int) Identity (FormulaF q f r a)
 -> Identity (FormulaF q f r a))
-> (CompatM (FormulaF q f r a)
    -> StateT (MemoState Int) Identity (FormulaF q f r a))
-> CompatM (FormulaF q f r a)
-> Identity (FormulaF q f r a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompatM (FormulaF q f r a)
-> StateT (MemoState Int) Identity (FormulaF q f r a)
forall a. CompatM a -> StateT (MemoState Int) Identity a
unCompatM (CompatM (FormulaF q f r a) -> Either (PathsPrefixTree q f r) a)
-> CompatM (FormulaF q f r a) -> Either (PathsPrefixTree q f r) a
forall a b. (a -> b) -> a -> b
$ CompatM (FormulaF q f r a)
f
{-# INLINE runCompatFormula #-}

embedFormula :: Paths q r l -> CompatFormula' q f l a -> CompatFormula' q f r a
embedFormula :: Paths q r l -> CompatFormula' q f l a -> CompatFormula' q f r a
embedFormula Paths q r l
bhv (Compose CompatM (FormulaF q f l a)
x) = CompatM (FormulaF q f r a) -> CompatFormula' q f r a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (CompatM (FormulaF q f r a) -> CompatFormula' q f r a)
-> CompatM (FormulaF q f r a) -> CompatFormula' q f r a
forall a b. (a -> b) -> a -> b
$ (PathsPrefixTree q f l -> PathsPrefixTree q f r)
-> FormulaF q f l a -> FormulaF q f r a
forall k1 k2 (q :: k1 -> k1 -> *) (f :: k1 -> *) (r :: k1)
       (q' :: k2 -> k2 -> *) (f' :: k2 -> *) (r' :: k2) a.
(PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors (Paths q r l -> PathsPrefixTree q f l -> PathsPrefixTree q f r
forall k (q :: k -> k -> *) (r :: k) (a :: k) (f :: k -> *).
Paths q r a -> PathsPrefixTree q f a -> PathsPrefixTree q f r
P.embed Paths q r l
bhv) (FormulaF q f l a -> FormulaF q f r a)
-> CompatM (FormulaF q f l a) -> CompatM (FormulaF q f r a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CompatM (FormulaF q f l a)
x

issueAt :: Issuable l => Paths q r l -> Issue l -> CompatFormula' q AnIssue r a
issueAt :: Paths q r l -> Issue l -> CompatFormula' q AnIssue r a
issueAt Paths q r l
xs Issue l
issue = CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a)
-> CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall a b. (a -> b) -> a -> b
$ FormulaF q AnIssue r a -> CompatM (FormulaF q AnIssue r a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FormulaF q AnIssue r a -> CompatM (FormulaF q AnIssue r a))
-> FormulaF q AnIssue r a -> CompatM (FormulaF q AnIssue r a)
forall a b. (a -> b) -> a -> b
$ AnItem q AnIssue r -> FormulaF q AnIssue r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
AnItem q f r -> FormulaF q f r a
anError (AnItem q AnIssue r -> FormulaF q AnIssue r a)
-> AnItem q AnIssue r -> FormulaF q AnIssue r a
forall a b. (a -> b) -> a -> b
$ Paths q r l -> AnIssue l -> AnItem q AnIssue r
forall k (f :: k -> *) (a :: k) (q :: k -> k -> *) (r :: k).
Ord (f a) =>
Paths q r a -> f a -> AnItem q f r
AnItem Paths q r l
xs (AnIssue l -> AnItem q AnIssue r)
-> AnIssue l -> AnItem q AnIssue r
forall a b. (a -> b) -> a -> b
$ Issue l -> AnIssue l
forall (l :: BehaviorLevel). Issuable l => Issue l -> AnIssue l
anIssue Issue l
issue
{-# INLINE issueAt #-}

anIssue :: Issuable l => Issue l -> AnIssue l
anIssue :: Issue l -> AnIssue l
anIssue = Orientation -> Issue l -> AnIssue l
forall (l :: BehaviorLevel).
Issuable l =>
Orientation -> Issue l -> AnIssue l
AnIssue Orientation
Forward
{-# INLINE anIssue #-}

anItem :: AnItem q AnIssue r -> CompatFormula' q AnIssue r a
anItem :: AnItem q AnIssue r -> CompatFormula' q AnIssue r a
anItem = CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a)
-> (AnItem q AnIssue r -> CompatM (FormulaF q AnIssue r a))
-> AnItem q AnIssue r
-> CompatFormula' q AnIssue r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FormulaF q AnIssue r a -> CompatM (FormulaF q AnIssue r a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FormulaF q AnIssue r a -> CompatM (FormulaF q AnIssue r a))
-> (AnItem q AnIssue r -> FormulaF q AnIssue r a)
-> AnItem q AnIssue r
-> CompatM (FormulaF q AnIssue r a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AnItem q AnIssue r -> FormulaF q AnIssue r a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
AnItem q f r -> FormulaF q f r a
anError
{-# INLINE anItem #-}

invertIssueOrientation :: CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a
invertIssueOrientation :: CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a
invertIssueOrientation (Compose CompatM (FormulaF q AnIssue r a)
x) =
  CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a)
-> CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall a b. (a -> b) -> a -> b
$ (PathsPrefixTree q AnIssue r -> PathsPrefixTree q AnIssue r)
-> FormulaF q AnIssue r a -> FormulaF q AnIssue r a
forall k1 k2 (q :: k1 -> k1 -> *) (f :: k1 -> *) (r :: k1)
       (q' :: k2 -> k2 -> *) (f' :: k2 -> *) (r' :: k2) a.
(PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors PathsPrefixTree q AnIssue r -> PathsPrefixTree q AnIssue r
forall (q :: BehaviorLevel -> BehaviorLevel -> *)
       (r :: BehaviorLevel).
PathsPrefixTree q AnIssue r -> PathsPrefixTree q AnIssue r
invertIssueOrientationP (FormulaF q AnIssue r a -> FormulaF q AnIssue r a)
-> CompatM (FormulaF q AnIssue r a)
-> CompatM (FormulaF q AnIssue r a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CompatM (FormulaF q AnIssue r a)
x

invertIssueOrientationP :: P.PathsPrefixTree q AnIssue r -> P.PathsPrefixTree q AnIssue r
invertIssueOrientationP :: PathsPrefixTree q AnIssue r -> PathsPrefixTree q AnIssue r
invertIssueOrientationP = (forall (x :: BehaviorLevel). AnIssue x -> AnIssue x)
-> PathsPrefixTree q AnIssue r -> PathsPrefixTree q AnIssue r
forall k (f :: k -> *) (q :: k -> k -> *) (r :: k).
(forall (x :: k). f x -> f x)
-> PathsPrefixTree q f r -> PathsPrefixTree q f r
P.map (\(AnIssue ori i) -> Orientation -> Issue x -> AnIssue x
forall (l :: BehaviorLevel).
Issuable l =>
Orientation -> Issue l -> AnIssue l
AnIssue (Orientation -> Orientation
toggleOrientation Orientation
ori) Issue x
i)

structuralIssue :: StructuralCompatFormula a
structuralIssue :: StructuralCompatFormula a
structuralIssue = CompatM (FormulaF VoidQuiver Proxy () a)
-> StructuralCompatFormula a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (CompatM (FormulaF VoidQuiver Proxy () a)
 -> StructuralCompatFormula a)
-> CompatM (FormulaF VoidQuiver Proxy () a)
-> StructuralCompatFormula a
forall a b. (a -> b) -> a -> b
$ FormulaF VoidQuiver Proxy () a
-> CompatM (FormulaF VoidQuiver Proxy () a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FormulaF VoidQuiver Proxy () a
 -> CompatM (FormulaF VoidQuiver Proxy () a))
-> FormulaF VoidQuiver Proxy () a
-> CompatM (FormulaF VoidQuiver Proxy () a)
forall a b. (a -> b) -> a -> b
$ AnItem VoidQuiver Proxy () -> FormulaF VoidQuiver Proxy () a
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) a.
AnItem q f r -> FormulaF q f r a
anError (AnItem VoidQuiver Proxy () -> FormulaF VoidQuiver Proxy () a)
-> AnItem VoidQuiver Proxy () -> FormulaF VoidQuiver Proxy () a
forall a b. (a -> b) -> a -> b
$ Paths VoidQuiver () () -> Proxy () -> AnItem VoidQuiver Proxy ()
forall k (f :: k -> *) (a :: k) (q :: k -> k -> *) (r :: k).
Ord (f a) =>
Paths q r a -> f a -> AnItem q f r
AnItem Paths VoidQuiver () ()
forall k (q :: k -> k -> *) (a :: k). Paths q a a
Root Proxy ()
forall k (t :: k). Proxy t
Proxy

anyOfAt ::
  Issuable l =>
  Paths q r l ->
  Issue l ->
  [CompatFormula' q AnIssue r a] ->
  CompatFormula' q AnIssue r a
anyOfAt :: Paths q r l
-> Issue l
-> [CompatFormula' q AnIssue r a]
-> CompatFormula' q AnIssue r a
anyOfAt Paths q r l
_ Issue l
_ [CompatFormula' q AnIssue r a
x] = CompatFormula' q AnIssue r a
x
anyOfAt Paths q r l
xs Issue l
issue [CompatFormula' q AnIssue r a]
fs =
  CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a)
-> CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall a b. (a -> b) -> a -> b
$ ([FormulaF q AnIssue r a]
-> AnItem q AnIssue r -> FormulaF q AnIssue r a
forall k1 k2 (q' :: k1 -> k1 -> *) (f' :: k1 -> *) (r' :: k1) a
       (q :: k2 -> k2 -> *) (f :: k2 -> *) (r :: k2).
[FormulaF q' f' r' a] -> AnItem q f r -> FormulaF q f r a
`eitherOf` Paths q r l -> AnIssue l -> AnItem q AnIssue r
forall k (f :: k -> *) (a :: k) (q :: k -> k -> *) (r :: k).
Ord (f a) =>
Paths q r a -> f a -> AnItem q f r
AnItem Paths q r l
xs (Issue l -> AnIssue l
forall (l :: BehaviorLevel). Issuable l => Issue l -> AnIssue l
anIssue Issue l
issue)) ([FormulaF q AnIssue r a] -> FormulaF q AnIssue r a)
-> CompatM [FormulaF q AnIssue r a]
-> CompatM (FormulaF q AnIssue r a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CompatFormula' q AnIssue r a -> CompatM (FormulaF q AnIssue r a))
-> [CompatFormula' q AnIssue r a]
-> CompatM [FormulaF q AnIssue r a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CompatFormula' q AnIssue r a -> CompatM (FormulaF q AnIssue r a)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose [CompatFormula' q AnIssue r a]
fs

-- | If the given formula contains any issues, add another issue on top. Otherwise succeed.
clarifyIssue ::
  AnItem q AnIssue r ->
  CompatFormula' q AnIssue r a ->
  CompatFormula' q AnIssue r a
clarifyIssue :: AnItem q AnIssue r
-> CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a
clarifyIssue AnItem q AnIssue r
item CompatFormula' q AnIssue r a
f =
  CompatM (FormulaF q AnIssue r a) -> CompatFormula' q AnIssue r a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (([FormulaF q AnIssue r a]
-> AnItem q AnIssue r -> FormulaF q AnIssue r a
forall k1 k2 (q' :: k1 -> k1 -> *) (f' :: k1 -> *) (r' :: k1) a
       (q :: k2 -> k2 -> *) (f :: k2 -> *) (r :: k2).
[FormulaF q' f' r' a] -> AnItem q f r -> FormulaF q f r a
`eitherOf` AnItem q AnIssue r
item) ([FormulaF q AnIssue r a] -> FormulaF q AnIssue r a)
-> (FormulaF q AnIssue r a -> [FormulaF q AnIssue r a])
-> FormulaF q AnIssue r a
-> FormulaF q AnIssue r a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FormulaF q AnIssue r a -> [FormulaF q AnIssue r a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FormulaF q AnIssue r a -> FormulaF q AnIssue r a)
-> CompatM (FormulaF q AnIssue r a)
-> CompatM (FormulaF q AnIssue r a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CompatFormula' q AnIssue r a -> CompatM (FormulaF q AnIssue r a)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose CompatFormula' q AnIssue r a
f) CompatFormula' q AnIssue r a
-> CompatFormula' q AnIssue r a -> CompatFormula' q AnIssue r a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> CompatFormula' q AnIssue r a
f

fixpointKnot ::
  MonadState (MemoState VarRef) m =>
  KnotTier (FormulaF q f r ()) VarRef m
fixpointKnot :: KnotTier (FormulaF q f r ()) Int m
fixpointKnot =
  KnotTier :: forall v d (m :: * -> *).
m d -> (d -> m v) -> (d -> v -> m v) -> KnotTier v d m
KnotTier
    { $sel:onKnotFound:KnotTier :: m Int
onKnotFound = (Int -> Int) -> m Int
forall s (m :: * -> *). MonadMemo s m => (s -> s) -> m s
modifyMemoNonce Int -> Int
forall a. Enum a => a -> a
succ
    , $sel:onKnotUsed:KnotTier :: Int -> m (FormulaF q f r ())
onKnotUsed = \Int
i -> FormulaF q f r () -> m (FormulaF q f r ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FormulaF q f r () -> m (FormulaF q f r ()))
-> FormulaF q f r () -> m (FormulaF q f r ())
forall a b. (a -> b) -> a -> b
$ Int -> FormulaF q f r ()
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k).
Int -> FormulaF q f r ()
variable Int
i
    , $sel:tieKnot:KnotTier :: Int -> FormulaF q f r () -> m (FormulaF q f r ())
tieKnot = \Int
i FormulaF q f r ()
x -> FormulaF q f r () -> m (FormulaF q f r ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FormulaF q f r () -> m (FormulaF q f r ()))
-> FormulaF q f r () -> m (FormulaF q f r ())
forall a b. (a -> b) -> a -> b
$ Int -> FormulaF q f r () -> FormulaF q f r ()
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k).
Int -> FormulaF q f r () -> FormulaF q f r ()
maxFixpoint Int
i FormulaF q f r ()
x
    }

memo ::
  (Typeable (l :: k), Typeable q, Typeable f, Typeable k, Typeable a) =>
  Paths q r l ->
  MemoKey ->
  (ProdCons (Traced a) -> CompatFormula' q f r ()) ->
  (ProdCons (Traced a) -> CompatFormula' q f r ())
memo :: Paths q r l
-> MemoKey
-> (ProdCons (Traced a) -> CompatFormula' q f r ())
-> ProdCons (Traced a)
-> CompatFormula' q f r ()
memo Paths q r l
bhv MemoKey
k ProdCons (Traced a) -> CompatFormula' q f r ()
f ProdCons (Traced a)
pc = CompatM (FormulaF q f r ()) -> CompatFormula' q f r ()
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (CompatM (FormulaF q f r ()) -> CompatFormula' q f r ())
-> CompatM (FormulaF q f r ()) -> CompatFormula' q f r ()
forall a b. (a -> b) -> a -> b
$ do
  FormulaF q f l ()
formula' <-
    KnotTier (FormulaF q f l ()) Int CompatM
-> CompatM (FormulaF q f l ())
-> (MemoKey, ProdCons (Paths Step TraceRoot a))
-> CompatM (FormulaF q f l ())
forall k v d (m :: * -> *) s.
(Typeable k, Typeable v, Typeable d, Ord k, MonadMemo s m) =>
KnotTier v d m -> m v -> k -> m v
memoWithKnot
      KnotTier (FormulaF q f l ()) Int CompatM
forall k (m :: * -> *) (q :: k -> k -> *) (f :: k -> *) (r :: k).
MonadState (MemoState Int) m =>
KnotTier (FormulaF q f r ()) Int m
fixpointKnot
      ( do
          FormulaF q f r ()
formula <- CompatFormula' q f r () -> CompatM (FormulaF q f r ())
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (CompatFormula' q f r () -> CompatM (FormulaF q f r ()))
-> CompatFormula' q f r () -> CompatM (FormulaF q f r ())
forall a b. (a -> b) -> a -> b
$ ProdCons (Traced a) -> CompatFormula' q f r ()
f ProdCons (Traced a)
pc
          pure $ (PathsPrefixTree q f r -> PathsPrefixTree q f l)
-> FormulaF q f r () -> FormulaF q f l ()
forall k1 k2 (q :: k1 -> k1 -> *) (f :: k1 -> *) (r :: k1)
       (q' :: k2 -> k2 -> *) (f' :: k2 -> *) (r' :: k2) a.
(PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors (Paths q r l -> PathsPrefixTree q f r -> PathsPrefixTree q f l
forall k (q :: k -> k -> *) (f :: k -> *) (r :: k) (a :: k).
Paths q r a -> PathsPrefixTree q f r -> PathsPrefixTree q f a
P.takeSubtree Paths q r l
bhv) FormulaF q f r ()
formula
      )
      (MemoKey
k, Traced a -> Paths Step TraceRoot a
forall e (w :: * -> *) a. ComonadEnv e w => w a -> e
ask (Traced a -> Paths Step TraceRoot a)
-> ProdCons (Traced a) -> ProdCons (Paths Step TraceRoot a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProdCons (Traced a)
pc)
  pure $ (PathsPrefixTree q f l -> PathsPrefixTree q f r)
-> FormulaF q f l () -> FormulaF q f r ()
forall k1 k2 (q :: k1 -> k1 -> *) (f :: k1 -> *) (r :: k1)
       (q' :: k2 -> k2 -> *) (f' :: k2 -> *) (r' :: k2) a.
(PathsPrefixTree q f r -> PathsPrefixTree q' f' r')
-> FormulaF q f r a -> FormulaF q' f' r' a
mapErrors (Paths q r l -> PathsPrefixTree q f l -> PathsPrefixTree q f r
forall k (q :: k -> k -> *) (r :: k) (a :: k) (f :: k -> *).
Paths q r a -> PathsPrefixTree q f a -> PathsPrefixTree q f r
P.embed Paths q r l
bhv) FormulaF q f l ()
formula'

data MemoKey = SemanticMemoKey | StructuralMemoKey
  deriving stock (MemoKey -> MemoKey -> Bool
(MemoKey -> MemoKey -> Bool)
-> (MemoKey -> MemoKey -> Bool) -> Eq MemoKey
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MemoKey -> MemoKey -> Bool
$c/= :: MemoKey -> MemoKey -> Bool
== :: MemoKey -> MemoKey -> Bool
$c== :: MemoKey -> MemoKey -> Bool
Eq, Eq MemoKey
Eq MemoKey
-> (MemoKey -> MemoKey -> Ordering)
-> (MemoKey -> MemoKey -> Bool)
-> (MemoKey -> MemoKey -> Bool)
-> (MemoKey -> MemoKey -> Bool)
-> (MemoKey -> MemoKey -> Bool)
-> (MemoKey -> MemoKey -> MemoKey)
-> (MemoKey -> MemoKey -> MemoKey)
-> Ord MemoKey
MemoKey -> MemoKey -> Bool
MemoKey -> MemoKey -> Ordering
MemoKey -> MemoKey -> MemoKey
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
min :: MemoKey -> MemoKey -> MemoKey
$cmin :: MemoKey -> MemoKey -> MemoKey
max :: MemoKey -> MemoKey -> MemoKey
$cmax :: MemoKey -> MemoKey -> MemoKey
>= :: MemoKey -> MemoKey -> Bool
$c>= :: MemoKey -> MemoKey -> Bool
> :: MemoKey -> MemoKey -> Bool
$c> :: MemoKey -> MemoKey -> Bool
<= :: MemoKey -> MemoKey -> Bool
$c<= :: MemoKey -> MemoKey -> Bool
< :: MemoKey -> MemoKey -> Bool
$c< :: MemoKey -> MemoKey -> Bool
compare :: MemoKey -> MemoKey -> Ordering
$ccompare :: MemoKey -> MemoKey -> Ordering
$cp1Ord :: Eq MemoKey
Ord)