{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE UndecidableInstances #-} module Blanks.Split ( BinderId (..) , SplitFunctor (..) , SplitBinder (..) , SplitResult (..) , splitLocScope ) where import Blanks.Core (BinderScope (..)) import Blanks.LocScope (LocScope, pattern LocScopeBinder, pattern LocScopeBound, pattern LocScopeEmbed, pattern LocScopeFree) import Blanks.Tracked (Tracked (..), WithTracked (..), mkTrackedBound, mkTrackedFree) import Control.DeepSeq (NFData (..)) import Control.Monad.State (State, gets, modify', runState) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Sequence (Seq) import qualified Data.Sequence as Seq import Data.Set (Set) import qualified Data.Set as Set import GHC.Generics (Generic) data Stream x = Stream !x (Stream x) enumStreamFrom :: Enum e => e -> Stream e enumStreamFrom :: e -> Stream e enumStreamFrom e :: e e = e -> Stream e -> Stream e forall x. x -> Stream x -> Stream x Stream e e (e -> Stream e forall e. Enum e => e -> Stream e enumStreamFrom (e -> e forall a. Enum a => a -> a succ e e)) enumStream :: Enum e => Stream e enumStream :: Stream e enumStream = e -> Stream e forall e. Enum e => e -> Stream e enumStreamFrom (Int -> e forall a. Enum a => Int -> a toEnum 0) newtype BinderId = BinderId { BinderId -> Int unBinderId :: Int } deriving stock (BinderId -> BinderId -> Bool (BinderId -> BinderId -> Bool) -> (BinderId -> BinderId -> Bool) -> Eq BinderId forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: BinderId -> BinderId -> Bool $c/= :: BinderId -> BinderId -> Bool == :: BinderId -> BinderId -> Bool $c== :: BinderId -> BinderId -> Bool Eq, Int -> BinderId -> ShowS [BinderId] -> ShowS BinderId -> String (Int -> BinderId -> ShowS) -> (BinderId -> String) -> ([BinderId] -> ShowS) -> Show BinderId forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [BinderId] -> ShowS $cshowList :: [BinderId] -> ShowS show :: BinderId -> String $cshow :: BinderId -> String showsPrec :: Int -> BinderId -> ShowS $cshowsPrec :: Int -> BinderId -> ShowS Show, Eq BinderId Eq BinderId => (BinderId -> BinderId -> Ordering) -> (BinderId -> BinderId -> Bool) -> (BinderId -> BinderId -> Bool) -> (BinderId -> BinderId -> Bool) -> (BinderId -> BinderId -> Bool) -> (BinderId -> BinderId -> BinderId) -> (BinderId -> BinderId -> BinderId) -> Ord BinderId BinderId -> BinderId -> Bool BinderId -> BinderId -> Ordering BinderId -> BinderId -> BinderId 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 :: BinderId -> BinderId -> BinderId $cmin :: BinderId -> BinderId -> BinderId max :: BinderId -> BinderId -> BinderId $cmax :: BinderId -> BinderId -> BinderId >= :: BinderId -> BinderId -> Bool $c>= :: BinderId -> BinderId -> Bool > :: BinderId -> BinderId -> Bool $c> :: BinderId -> BinderId -> Bool <= :: BinderId -> BinderId -> Bool $c<= :: BinderId -> BinderId -> Bool < :: BinderId -> BinderId -> Bool $c< :: BinderId -> BinderId -> Bool compare :: BinderId -> BinderId -> Ordering $ccompare :: BinderId -> BinderId -> Ordering $cp1Ord :: Eq BinderId Ord) deriving newtype (Int -> BinderId BinderId -> Int BinderId -> [BinderId] BinderId -> BinderId BinderId -> BinderId -> [BinderId] BinderId -> BinderId -> BinderId -> [BinderId] (BinderId -> BinderId) -> (BinderId -> BinderId) -> (Int -> BinderId) -> (BinderId -> Int) -> (BinderId -> [BinderId]) -> (BinderId -> BinderId -> [BinderId]) -> (BinderId -> BinderId -> [BinderId]) -> (BinderId -> BinderId -> BinderId -> [BinderId]) -> Enum BinderId forall a. (a -> a) -> (a -> a) -> (Int -> a) -> (a -> Int) -> (a -> [a]) -> (a -> a -> [a]) -> (a -> a -> [a]) -> (a -> a -> a -> [a]) -> Enum a enumFromThenTo :: BinderId -> BinderId -> BinderId -> [BinderId] $cenumFromThenTo :: BinderId -> BinderId -> BinderId -> [BinderId] enumFromTo :: BinderId -> BinderId -> [BinderId] $cenumFromTo :: BinderId -> BinderId -> [BinderId] enumFromThen :: BinderId -> BinderId -> [BinderId] $cenumFromThen :: BinderId -> BinderId -> [BinderId] enumFrom :: BinderId -> [BinderId] $cenumFrom :: BinderId -> [BinderId] fromEnum :: BinderId -> Int $cfromEnum :: BinderId -> Int toEnum :: Int -> BinderId $ctoEnum :: Int -> BinderId pred :: BinderId -> BinderId $cpred :: BinderId -> BinderId succ :: BinderId -> BinderId $csucc :: BinderId -> BinderId Enum, BinderId -> () (BinderId -> ()) -> NFData BinderId forall a. (a -> ()) -> NFData a rnf :: BinderId -> () $crnf :: BinderId -> () NFData, Integer -> BinderId BinderId -> BinderId BinderId -> BinderId -> BinderId (BinderId -> BinderId -> BinderId) -> (BinderId -> BinderId -> BinderId) -> (BinderId -> BinderId -> BinderId) -> (BinderId -> BinderId) -> (BinderId -> BinderId) -> (BinderId -> BinderId) -> (Integer -> BinderId) -> Num BinderId forall a. (a -> a -> a) -> (a -> a -> a) -> (a -> a -> a) -> (a -> a) -> (a -> a) -> (a -> a) -> (Integer -> a) -> Num a fromInteger :: Integer -> BinderId $cfromInteger :: Integer -> BinderId signum :: BinderId -> BinderId $csignum :: BinderId -> BinderId abs :: BinderId -> BinderId $cabs :: BinderId -> BinderId negate :: BinderId -> BinderId $cnegate :: BinderId -> BinderId * :: BinderId -> BinderId -> BinderId $c* :: BinderId -> BinderId -> BinderId - :: BinderId -> BinderId -> BinderId $c- :: BinderId -> BinderId -> BinderId + :: BinderId -> BinderId -> BinderId $c+ :: BinderId -> BinderId -> BinderId Num) data SplitFunctor f a = SplitFunctorBase !(f a) | SplitFunctorClosure !BinderId !(Seq Int) deriving stock (SplitFunctor f a -> SplitFunctor f a -> Bool (SplitFunctor f a -> SplitFunctor f a -> Bool) -> (SplitFunctor f a -> SplitFunctor f a -> Bool) -> Eq (SplitFunctor f a) forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a forall (f :: * -> *) a. Eq (f a) => SplitFunctor f a -> SplitFunctor f a -> Bool /= :: SplitFunctor f a -> SplitFunctor f a -> Bool $c/= :: forall (f :: * -> *) a. Eq (f a) => SplitFunctor f a -> SplitFunctor f a -> Bool == :: SplitFunctor f a -> SplitFunctor f a -> Bool $c== :: forall (f :: * -> *) a. Eq (f a) => SplitFunctor f a -> SplitFunctor f a -> Bool Eq, Int -> SplitFunctor f a -> ShowS [SplitFunctor f a] -> ShowS SplitFunctor f a -> String (Int -> SplitFunctor f a -> ShowS) -> (SplitFunctor f a -> String) -> ([SplitFunctor f a] -> ShowS) -> Show (SplitFunctor f a) forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a forall (f :: * -> *) a. Show (f a) => Int -> SplitFunctor f a -> ShowS forall (f :: * -> *) a. Show (f a) => [SplitFunctor f a] -> ShowS forall (f :: * -> *) a. Show (f a) => SplitFunctor f a -> String showList :: [SplitFunctor f a] -> ShowS $cshowList :: forall (f :: * -> *) a. Show (f a) => [SplitFunctor f a] -> ShowS show :: SplitFunctor f a -> String $cshow :: forall (f :: * -> *) a. Show (f a) => SplitFunctor f a -> String showsPrec :: Int -> SplitFunctor f a -> ShowS $cshowsPrec :: forall (f :: * -> *) a. Show (f a) => Int -> SplitFunctor f a -> ShowS Show, (forall x. SplitFunctor f a -> Rep (SplitFunctor f a) x) -> (forall x. Rep (SplitFunctor f a) x -> SplitFunctor f a) -> Generic (SplitFunctor f a) forall x. Rep (SplitFunctor f a) x -> SplitFunctor f a forall x. SplitFunctor f a -> Rep (SplitFunctor f a) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (f :: * -> *) a x. Rep (SplitFunctor f a) x -> SplitFunctor f a forall (f :: * -> *) a x. SplitFunctor f a -> Rep (SplitFunctor f a) x $cto :: forall (f :: * -> *) a x. Rep (SplitFunctor f a) x -> SplitFunctor f a $cfrom :: forall (f :: * -> *) a x. SplitFunctor f a -> Rep (SplitFunctor f a) x Generic, a -> SplitFunctor f b -> SplitFunctor f a (a -> b) -> SplitFunctor f a -> SplitFunctor f b (forall a b. (a -> b) -> SplitFunctor f a -> SplitFunctor f b) -> (forall a b. a -> SplitFunctor f b -> SplitFunctor f a) -> Functor (SplitFunctor f) forall a b. a -> SplitFunctor f b -> SplitFunctor f a forall a b. (a -> b) -> SplitFunctor f a -> SplitFunctor f b forall (f :: * -> *) a b. Functor f => a -> SplitFunctor f b -> SplitFunctor f a forall (f :: * -> *) a b. Functor f => (a -> b) -> SplitFunctor f a -> SplitFunctor f b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> SplitFunctor f b -> SplitFunctor f a $c<$ :: forall (f :: * -> *) a b. Functor f => a -> SplitFunctor f b -> SplitFunctor f a fmap :: (a -> b) -> SplitFunctor f a -> SplitFunctor f b $cfmap :: forall (f :: * -> *) a b. Functor f => (a -> b) -> SplitFunctor f a -> SplitFunctor f b Functor, SplitFunctor f a -> Bool (a -> m) -> SplitFunctor f a -> m (a -> b -> b) -> b -> SplitFunctor f a -> b (forall m. Monoid m => SplitFunctor f m -> m) -> (forall m a. Monoid m => (a -> m) -> SplitFunctor f a -> m) -> (forall m a. Monoid m => (a -> m) -> SplitFunctor f a -> m) -> (forall a b. (a -> b -> b) -> b -> SplitFunctor f a -> b) -> (forall a b. (a -> b -> b) -> b -> SplitFunctor f a -> b) -> (forall b a. (b -> a -> b) -> b -> SplitFunctor f a -> b) -> (forall b a. (b -> a -> b) -> b -> SplitFunctor f a -> b) -> (forall a. (a -> a -> a) -> SplitFunctor f a -> a) -> (forall a. (a -> a -> a) -> SplitFunctor f a -> a) -> (forall a. SplitFunctor f a -> [a]) -> (forall a. SplitFunctor f a -> Bool) -> (forall a. SplitFunctor f a -> Int) -> (forall a. Eq a => a -> SplitFunctor f a -> Bool) -> (forall a. Ord a => SplitFunctor f a -> a) -> (forall a. Ord a => SplitFunctor f a -> a) -> (forall a. Num a => SplitFunctor f a -> a) -> (forall a. Num a => SplitFunctor f a -> a) -> Foldable (SplitFunctor f) forall a. Eq a => a -> SplitFunctor f a -> Bool forall a. Num a => SplitFunctor f a -> a forall a. Ord a => SplitFunctor f a -> a forall m. Monoid m => SplitFunctor f m -> m forall a. SplitFunctor f a -> Bool forall a. SplitFunctor f a -> Int forall a. SplitFunctor f a -> [a] forall a. (a -> a -> a) -> SplitFunctor f a -> a forall m a. Monoid m => (a -> m) -> SplitFunctor f a -> m forall b a. (b -> a -> b) -> b -> SplitFunctor f a -> b forall a b. (a -> b -> b) -> b -> SplitFunctor f a -> b forall (f :: * -> *) a. (Foldable f, Eq a) => a -> SplitFunctor f a -> Bool forall (f :: * -> *) a. (Foldable f, Num a) => SplitFunctor f a -> a forall (f :: * -> *) a. (Foldable f, Ord a) => SplitFunctor f a -> a forall (f :: * -> *) m. (Foldable f, Monoid m) => SplitFunctor f m -> m forall (f :: * -> *) a. Foldable f => SplitFunctor f a -> Bool forall (f :: * -> *) a. Foldable f => SplitFunctor f a -> Int forall (f :: * -> *) a. Foldable f => SplitFunctor f a -> [a] forall (f :: * -> *) a. Foldable f => (a -> a -> a) -> SplitFunctor f a -> a forall (f :: * -> *) m a. (Foldable f, Monoid m) => (a -> m) -> SplitFunctor f a -> m forall (f :: * -> *) b a. Foldable f => (b -> a -> b) -> b -> SplitFunctor f a -> b forall (f :: * -> *) a b. Foldable f => (a -> b -> b) -> b -> SplitFunctor f 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 :: SplitFunctor f a -> a $cproduct :: forall (f :: * -> *) a. (Foldable f, Num a) => SplitFunctor f a -> a sum :: SplitFunctor f a -> a $csum :: forall (f :: * -> *) a. (Foldable f, Num a) => SplitFunctor f a -> a minimum :: SplitFunctor f a -> a $cminimum :: forall (f :: * -> *) a. (Foldable f, Ord a) => SplitFunctor f a -> a maximum :: SplitFunctor f a -> a $cmaximum :: forall (f :: * -> *) a. (Foldable f, Ord a) => SplitFunctor f a -> a elem :: a -> SplitFunctor f a -> Bool $celem :: forall (f :: * -> *) a. (Foldable f, Eq a) => a -> SplitFunctor f a -> Bool length :: SplitFunctor f a -> Int $clength :: forall (f :: * -> *) a. Foldable f => SplitFunctor f a -> Int null :: SplitFunctor f a -> Bool $cnull :: forall (f :: * -> *) a. Foldable f => SplitFunctor f a -> Bool toList :: SplitFunctor f a -> [a] $ctoList :: forall (f :: * -> *) a. Foldable f => SplitFunctor f a -> [a] foldl1 :: (a -> a -> a) -> SplitFunctor f a -> a $cfoldl1 :: forall (f :: * -> *) a. Foldable f => (a -> a -> a) -> SplitFunctor f a -> a foldr1 :: (a -> a -> a) -> SplitFunctor f a -> a $cfoldr1 :: forall (f :: * -> *) a. Foldable f => (a -> a -> a) -> SplitFunctor f a -> a foldl' :: (b -> a -> b) -> b -> SplitFunctor f a -> b $cfoldl' :: forall (f :: * -> *) b a. Foldable f => (b -> a -> b) -> b -> SplitFunctor f a -> b foldl :: (b -> a -> b) -> b -> SplitFunctor f a -> b $cfoldl :: forall (f :: * -> *) b a. Foldable f => (b -> a -> b) -> b -> SplitFunctor f a -> b foldr' :: (a -> b -> b) -> b -> SplitFunctor f a -> b $cfoldr' :: forall (f :: * -> *) a b. Foldable f => (a -> b -> b) -> b -> SplitFunctor f a -> b foldr :: (a -> b -> b) -> b -> SplitFunctor f a -> b $cfoldr :: forall (f :: * -> *) a b. Foldable f => (a -> b -> b) -> b -> SplitFunctor f a -> b foldMap' :: (a -> m) -> SplitFunctor f a -> m $cfoldMap' :: forall (f :: * -> *) m a. (Foldable f, Monoid m) => (a -> m) -> SplitFunctor f a -> m foldMap :: (a -> m) -> SplitFunctor f a -> m $cfoldMap :: forall (f :: * -> *) m a. (Foldable f, Monoid m) => (a -> m) -> SplitFunctor f a -> m fold :: SplitFunctor f m -> m $cfold :: forall (f :: * -> *) m. (Foldable f, Monoid m) => SplitFunctor f m -> m Foldable, Functor (SplitFunctor f) Foldable (SplitFunctor f) (Functor (SplitFunctor f), Foldable (SplitFunctor f)) => (forall (f :: * -> *) a b. Applicative f => (a -> f b) -> SplitFunctor f a -> f (SplitFunctor f b)) -> (forall (f :: * -> *) a. Applicative f => SplitFunctor f (f a) -> f (SplitFunctor f a)) -> (forall (m :: * -> *) a b. Monad m => (a -> m b) -> SplitFunctor f a -> m (SplitFunctor f b)) -> (forall (m :: * -> *) a. Monad m => SplitFunctor f (m a) -> m (SplitFunctor f a)) -> Traversable (SplitFunctor f) (a -> f b) -> SplitFunctor f a -> f (SplitFunctor f 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 (f :: * -> *). Traversable f => Functor (SplitFunctor f) forall (f :: * -> *). Traversable f => Foldable (SplitFunctor f) forall (f :: * -> *) (m :: * -> *) a. (Traversable f, Monad m) => SplitFunctor f (m a) -> m (SplitFunctor f a) forall (f :: * -> *) (f :: * -> *) a. (Traversable f, Applicative f) => SplitFunctor f (f a) -> f (SplitFunctor f a) forall (f :: * -> *) (m :: * -> *) a b. (Traversable f, Monad m) => (a -> m b) -> SplitFunctor f a -> m (SplitFunctor f b) forall (f :: * -> *) (f :: * -> *) a b. (Traversable f, Applicative f) => (a -> f b) -> SplitFunctor f a -> f (SplitFunctor f b) forall (m :: * -> *) a. Monad m => SplitFunctor f (m a) -> m (SplitFunctor f a) forall (f :: * -> *) a. Applicative f => SplitFunctor f (f a) -> f (SplitFunctor f a) forall (m :: * -> *) a b. Monad m => (a -> m b) -> SplitFunctor f a -> m (SplitFunctor f b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> SplitFunctor f a -> f (SplitFunctor f b) sequence :: SplitFunctor f (m a) -> m (SplitFunctor f a) $csequence :: forall (f :: * -> *) (m :: * -> *) a. (Traversable f, Monad m) => SplitFunctor f (m a) -> m (SplitFunctor f a) mapM :: (a -> m b) -> SplitFunctor f a -> m (SplitFunctor f b) $cmapM :: forall (f :: * -> *) (m :: * -> *) a b. (Traversable f, Monad m) => (a -> m b) -> SplitFunctor f a -> m (SplitFunctor f b) sequenceA :: SplitFunctor f (f a) -> f (SplitFunctor f a) $csequenceA :: forall (f :: * -> *) (f :: * -> *) a. (Traversable f, Applicative f) => SplitFunctor f (f a) -> f (SplitFunctor f a) traverse :: (a -> f b) -> SplitFunctor f a -> f (SplitFunctor f b) $ctraverse :: forall (f :: * -> *) (f :: * -> *) a b. (Traversable f, Applicative f) => (a -> f b) -> SplitFunctor f a -> f (SplitFunctor f b) $cp2Traversable :: forall (f :: * -> *). Traversable f => Foldable (SplitFunctor f) $cp1Traversable :: forall (f :: * -> *). Traversable f => Functor (SplitFunctor f) Traversable) deriving anyclass (SplitFunctor f a -> () (SplitFunctor f a -> ()) -> NFData (SplitFunctor f a) forall a. (a -> ()) -> NFData a forall (f :: * -> *) a. NFData (f a) => SplitFunctor f a -> () rnf :: SplitFunctor f a -> () $crnf :: forall (f :: * -> *) a. NFData (f a) => SplitFunctor f a -> () NFData) data SplitBinder l n f a = SplitBinder { SplitBinder l n f a -> Int splitBinderClosureArity :: !Int , SplitBinder l n f a -> Set a splitBinderFree :: !(Set a) , SplitBinder l n f a -> BinderScope n (LocScope l n (SplitFunctor f) a) splitBinderScope :: !(BinderScope n (LocScope l n (SplitFunctor f) a)) } deriving stock ((forall x. SplitBinder l n f a -> Rep (SplitBinder l n f a) x) -> (forall x. Rep (SplitBinder l n f a) x -> SplitBinder l n f a) -> Generic (SplitBinder l n f a) forall x. Rep (SplitBinder l n f a) x -> SplitBinder l n f a forall x. SplitBinder l n f a -> Rep (SplitBinder l n f a) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall l n (f :: * -> *) a x. Rep (SplitBinder l n f a) x -> SplitBinder l n f a forall l n (f :: * -> *) a x. SplitBinder l n f a -> Rep (SplitBinder l n f a) x $cto :: forall l n (f :: * -> *) a x. Rep (SplitBinder l n f a) x -> SplitBinder l n f a $cfrom :: forall l n (f :: * -> *) a x. SplitBinder l n f a -> Rep (SplitBinder l n f a) x Generic) instance (Eq l, Eq n, Eq a, Eq (f (LocScope l n (SplitFunctor f) a))) => Eq (SplitBinder l n f a) where SplitBinder a1 :: Int a1 f1 :: Set a f1 s1 :: BinderScope n (LocScope l n (SplitFunctor f) a) s1 == :: SplitBinder l n f a -> SplitBinder l n f a -> Bool == SplitBinder a2 :: Int a2 f2 :: Set a f2 s2 :: BinderScope n (LocScope l n (SplitFunctor f) a) s2 = Int a1 Int -> Int -> Bool forall a. Eq a => a -> a -> Bool == Int a2 Bool -> Bool -> Bool && Set a f1 Set a -> Set a -> Bool forall a. Eq a => a -> a -> Bool == Set a f2 Bool -> Bool -> Bool && BinderScope n (LocScope l n (SplitFunctor f) a) s1 BinderScope n (LocScope l n (SplitFunctor f) a) -> BinderScope n (LocScope l n (SplitFunctor f) a) -> Bool forall a. Eq a => a -> a -> Bool == BinderScope n (LocScope l n (SplitFunctor f) a) s2 instance (Show l, Show n, Show a, Show (f (LocScope l n (SplitFunctor f) a))) => Show (SplitBinder l n f a) where showsPrec :: Int -> SplitBinder l n f a -> ShowS showsPrec d :: Int d (SplitBinder a :: Int a f :: Set a f s :: BinderScope n (LocScope l n (SplitFunctor f) a) s) = String -> ShowS showString "SplitBinder " ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> Int -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec (Int dInt -> Int -> Int forall a. Num a => a -> a -> a +1) Int a ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Char -> ShowS showChar ' ' ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> Set a -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec (Int dInt -> Int -> Int forall a. Num a => a -> a -> a +1) Set a f ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Char -> ShowS showChar ' ' ShowS -> ShowS -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> BinderScope n (LocScope l n (SplitFunctor f) a) -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec (Int dInt -> Int -> Int forall a. Num a => a -> a -> a +1) BinderScope n (LocScope l n (SplitFunctor f) a) s instance (NFData l, NFData n, NFData a, NFData (f (LocScope l n (SplitFunctor f) a))) => NFData (SplitBinder l n f a) where rnf :: SplitBinder l n f a -> () rnf (SplitBinder a :: Int a f :: Set a f s :: BinderScope n (LocScope l n (SplitFunctor f) a) s) = () -> () -> () forall a b. a -> b -> b seq (Int -> () forall a. NFData a => a -> () rnf Int a) (() -> () -> () forall a b. a -> b -> b seq (Set a -> () forall a. NFData a => a -> () rnf Set a f) (BinderScope n (LocScope l n (SplitFunctor f) a) -> () forall a. NFData a => a -> () rnf BinderScope n (LocScope l n (SplitFunctor f) a) s)) data SplitState l n f a = SplitState { SplitState l n f a -> Stream BinderId splitStateStream :: !(Stream BinderId) , SplitState l n f a -> Map BinderId (SplitBinder l n f a) splitStateBinders :: !(Map BinderId (SplitBinder l n f a)) } initSplitState :: SplitState l n f a initSplitState :: SplitState l n f a initSplitState = Stream BinderId -> Map BinderId (SplitBinder l n f a) -> SplitState l n f a forall l n (f :: * -> *) a. Stream BinderId -> Map BinderId (SplitBinder l n f a) -> SplitState l n f a SplitState Stream BinderId forall e. Enum e => Stream e enumStream Map BinderId (SplitBinder l n f a) forall k a. Map k a Map.empty getNextBinderId :: State (SplitState l n f a) BinderId getNextBinderId :: State (SplitState l n f a) BinderId getNextBinderId = do Stream BinderId st <- (SplitState l n f a -> Stream BinderId) -> StateT (SplitState l n f a) Identity (Stream BinderId) forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a gets SplitState l n f a -> Stream BinderId forall l n (f :: * -> *) a. SplitState l n f a -> Stream BinderId splitStateStream let Stream hd :: BinderId hd tl :: Stream BinderId tl = Stream BinderId st (SplitState l n f a -> SplitState l n f a) -> StateT (SplitState l n f a) Identity () forall s (m :: * -> *). MonadState s m => (s -> s) -> m () modify' (\ss :: SplitState l n f a ss -> SplitState l n f a ss { splitStateStream :: Stream BinderId splitStateStream = Stream BinderId tl }) BinderId -> State (SplitState l n f a) BinderId forall (f :: * -> *) a. Applicative f => a -> f a pure BinderId hd insertBinder :: BinderId -> SplitBinder l n f a -> State (SplitState l n f a) () insertBinder :: BinderId -> SplitBinder l n f a -> State (SplitState l n f a) () insertBinder bid :: BinderId bid lb :: SplitBinder l n f a lb = (SplitState l n f a -> SplitState l n f a) -> State (SplitState l n f a) () forall s (m :: * -> *). MonadState s m => (s -> s) -> m () modify' (\ss :: SplitState l n f a ss -> SplitState l n f a ss { splitStateBinders :: Map BinderId (SplitBinder l n f a) splitStateBinders = BinderId -> SplitBinder l n f a -> Map BinderId (SplitBinder l n f a) -> Map BinderId (SplitBinder l n f a) forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert BinderId bid SplitBinder l n f a lb (SplitState l n f a -> Map BinderId (SplitBinder l n f a) forall l n (f :: * -> *) a. SplitState l n f a -> Map BinderId (SplitBinder l n f a) splitStateBinders SplitState l n f a ss) }) remapBound :: Int -> Set Int -> Int -> Int remapBound :: Int -> Set Int -> Int -> Int remapBound r :: Int r bs :: Set Int bs b :: Int b = Int -> (Int -> Int) -> Maybe Int -> Int forall b a. b -> (a -> b) -> Maybe a -> b maybe Int b (Int -> Int -> Int forall a. Num a => a -> a -> a + Int r) (Int -> Set Int -> Maybe Int forall a. Ord a => a -> Set a -> Maybe Int Set.lookupIndex Int b Set Int bs) splitLocScopeInner :: (Traversable f, Ord a) => Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) splitLocScopeInner :: Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) splitLocScopeInner r :: Int r bs :: Set Int bs ls :: LocScope (WithTracked a l) n f a ls = case LocScope (WithTracked a l) n f a ls of LocScopeBound (WithTracked _ l :: l l) b :: Int b -> let !b' :: Int b' = Int -> Set Int -> Int -> Int remapBound Int r Set Int bs Int b in (Tracked a, LocScope l n (SplitFunctor f) a) -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a. Applicative f => a -> f a pure (Int -> Tracked a forall a. Int -> Tracked a mkTrackedBound Int b', l -> Int -> LocScope l n (SplitFunctor f) a forall l n (f :: * -> *) a. l -> Int -> LocScope l n f a LocScopeBound l l Int b') LocScopeFree (WithTracked _ l :: l l) a :: a a -> (Tracked a, LocScope l n (SplitFunctor f) a) -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a. Applicative f => a -> f a pure (a -> Tracked a forall a. a -> Tracked a mkTrackedFree a a, l -> a -> LocScope l n (SplitFunctor f) a forall l a n (f :: * -> *). l -> a -> LocScope l n f a LocScopeFree l l a a) LocScopeEmbed (WithTracked _ l :: l l) fe :: f (LocScope (WithTracked a l) n f a) fe -> (f (Tracked a, LocScope l n (SplitFunctor f) a) -> (Tracked a, LocScope l n (SplitFunctor f) a)) -> StateT (SplitState l n f a) Identity (f (Tracked a, LocScope l n (SplitFunctor f) a)) -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap (\fx :: f (Tracked a, LocScope l n (SplitFunctor f) a) fx -> let (!Tracked a t, !f (LocScope l n (SplitFunctor f) a) fe') = f (Tracked a, LocScope l n (SplitFunctor f) a) -> (Tracked a, f (LocScope l n (SplitFunctor f) a)) forall (t :: * -> *) (m :: * -> *) a. (Traversable t, Monad m) => t (m a) -> m (t a) sequence f (Tracked a, LocScope l n (SplitFunctor f) a) fx in (Tracked a t, l -> SplitFunctor f (LocScope l n (SplitFunctor f) a) -> LocScope l n (SplitFunctor f) a forall l (f :: * -> *) n a. l -> f (LocScope l n f a) -> LocScope l n f a LocScopeEmbed l l (f (LocScope l n (SplitFunctor f) a) -> SplitFunctor f (LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a. f a -> SplitFunctor f a SplitFunctorBase f (LocScope l n (SplitFunctor f) a) fe'))) ((LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a)) -> f (LocScope (WithTracked a l) n f a) -> StateT (SplitState l n f a) Identity (f (Tracked a, LocScope l n (SplitFunctor f) a)) forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse (Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a l n. (Traversable f, Ord a) => Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) splitLocScopeInner Int r Set Int bs) f (LocScope (WithTracked a l) n f a) fe) LocScopeBinder (WithTracked (Tracked fv :: Set a fv bv :: Set Int bv) l :: l l) x :: Int x n :: n n e :: LocScope (WithTracked a l) n f a e -> do BinderId bid <- State (SplitState l n f a) BinderId forall l n (f :: * -> *) a. State (SplitState l n f a) BinderId getNextBinderId let bs' :: Set Int bs' = (Int -> Int) -> Set Int -> Set Int forall a b. (a -> b) -> Set a -> Set b Set.mapMonotonic (Int -> Int -> Int forall a. Num a => a -> a -> a + Int r) Set Int bv (_, e' :: LocScope l n (SplitFunctor f) a e') <- Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a l n. (Traversable f, Ord a) => Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) splitLocScopeInner Int x Set Int bs' LocScope (WithTracked a l) n f a e let lb :: SplitBinder l n f a lb = Int -> Set a -> BinderScope n (LocScope l n (SplitFunctor f) a) -> SplitBinder l n f a forall l n (f :: * -> *) a. Int -> Set a -> BinderScope n (LocScope l n (SplitFunctor f) a) -> SplitBinder l n f a SplitBinder (Set Int -> Int forall a. Set a -> Int Set.size Set Int bs') Set a fv (Int -> n -> LocScope l n (SplitFunctor f) a -> BinderScope n (LocScope l n (SplitFunctor f) a) forall n e. Int -> n -> e -> BinderScope n e BinderScope Int x n n LocScope l n (SplitFunctor f) a e') BinderId -> SplitBinder l n f a -> State (SplitState l n f a) () forall l n (f :: * -> *) a. BinderId -> SplitBinder l n f a -> State (SplitState l n f a) () insertBinder BinderId bid SplitBinder l n f a lb let ss :: Seq Int ss = [Int] -> Seq Int forall a. [a] -> Seq a Seq.fromList (Set Int -> [Int] forall a. Set a -> [a] Set.toList Set Int bv) (Tracked a, LocScope l n (SplitFunctor f) a) -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a. Applicative f => a -> f a pure (Set a -> Set Int -> Tracked a forall a. Set a -> Set Int -> Tracked a Tracked Set a forall a. Set a Set.empty Set Int bv, l -> SplitFunctor f (LocScope l n (SplitFunctor f) a) -> LocScope l n (SplitFunctor f) a forall l (f :: * -> *) n a. l -> f (LocScope l n f a) -> LocScope l n f a LocScopeEmbed l l (BinderId -> Seq Int -> SplitFunctor f (LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a. BinderId -> Seq Int -> SplitFunctor f a SplitFunctorClosure BinderId bid Seq Int ss)) data SplitResult l n f a = SplitResult { SplitResult l n f a -> Tracked a splitResultTracked :: !(Tracked a) , SplitResult l n f a -> LocScope l n (SplitFunctor f) a splitResultScope :: !(LocScope l n (SplitFunctor f) a) , SplitResult l n f a -> Map BinderId (SplitBinder l n f a) splitResultBinders :: !(Map BinderId (SplitBinder l n f a)) } splitLocScope :: (Traversable f, Ord a) => LocScope (WithTracked a l) n f a -> SplitResult l n f a splitLocScope :: LocScope (WithTracked a l) n f a -> SplitResult l n f a splitLocScope s :: LocScope (WithTracked a l) n f a s = let ((!Tracked a t, !LocScope l n (SplitFunctor f) a s'), !SplitState l n f a ss) = State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) -> SplitState l n f a -> ((Tracked a, LocScope l n (SplitFunctor f) a), SplitState l n f a) forall s a. State s a -> s -> (a, s) runState (Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) forall (f :: * -> *) a l n. (Traversable f, Ord a) => Int -> Set Int -> LocScope (WithTracked a l) n f a -> State (SplitState l n f a) (Tracked a, LocScope l n (SplitFunctor f) a) splitLocScopeInner 0 Set Int forall a. Set a Set.empty LocScope (WithTracked a l) n f a s) SplitState l n f a forall l n (f :: * -> *) a. SplitState l n f a initSplitState in Tracked a -> LocScope l n (SplitFunctor f) a -> Map BinderId (SplitBinder l n f a) -> SplitResult l n f a forall l n (f :: * -> *) a. Tracked a -> LocScope l n (SplitFunctor f) a -> Map BinderId (SplitBinder l n f a) -> SplitResult l n f a SplitResult Tracked a t LocScope l n (SplitFunctor f) a s' (SplitState l n f a -> Map BinderId (SplitBinder l n f a) forall l n (f :: * -> *) a. SplitState l n f a -> Map BinderId (SplitBinder l n f a) splitStateBinders SplitState l n f a ss)