{-# 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,
structuralMaybe,
structuralMaybeWith,
structuralEq,
iohmStructural,
iohmStructuralWith,
structuralList,
(>>>),
(<<<),
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
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
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)