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