{-# LANGUAGE PatternSynonyms #-} -- For Comb
{-# LANGUAGE TemplateHaskell #-} -- For branch
{-# LANGUAGE ViewPatterns #-} -- For unSimplComb
{-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name
-- | Bottom-up optimization of 'Comb'inators,
-- reexamining downward as needed after each optimization.
module Symantic.Parser.Grammar.Optimize where

import Data.Bool (Bool(..), (&&), not)
import Data.Either (Either(..), either)
import Data.Eq (Eq(..))
import Data.Function (($), (.))
import Data.Kind (Constraint)
import Data.Maybe (Maybe(..))
import Data.Set (Set)
import Data.Functor.Identity (Identity(..))
import Data.Functor.Product (Product(..))
import Unsafe.Coerce (unsafeCoerce)
import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
import Data.Semigroup (Semigroup(..))
import qualified Data.Foldable as Foldable
import qualified Data.Functor as F
import qualified Data.HashMap.Strict as HM
import qualified Data.HashSet as HS
import Data.Hashable (Hashable)
import qualified Language.Haskell.TH as TH

import Symantic.Parser.Grammar.Combinators
import Symantic.Parser.Grammar.Production
import Symantic.Parser.Grammar.ObserveSharing hiding (def)
import Symantic.Derive
import qualified Symantic.Data as Prod
import qualified Symantic.Lang as Prod

{-
import Data.Function (($), flip)
import Debug.Trace (trace)

(&) = flip ($)
infix 0 &
-}
type OptimizeGrammar = KnotComb TH.Name

-- | TODO: remove useless wrapping?
newtype TiedComb repr a = TiedComb
  {  combSimpl :: SimplComb repr a
  --,  combRefs :: HS.HashSet letName
  }

-- * Type 'KnotComb'
data KnotComb letName repr a = KnotComb
  { knotCombOpens :: OpenRecs letName (SomeLet (TiedComb repr))
    -- ^ 'TiedComb' for all 'letName' in 'lets'.
  , knotCombOpen ::
      LetRecs letName (SomeLet (TiedComb repr)) ->
      TiedComb repr a
    -- ^ 'TiedComb' of the current combinator,
    -- with access to the final 'knotCombOpens'.
  }

optimizeGrammar ::
  Derivable (SimplComb repr) =>
  KnotComb TH.Name repr a -> repr a
optimizeGrammar = derive . derive

type instance Derived (KnotComb letName repr) = SimplComb repr
instance Derivable (KnotComb letName repr) where
  derive opt = combSimpl $
    knotCombOpen opt (mutualFix (knotCombOpens opt))
instance LiftDerived (KnotComb letName repr) where
  liftDerived x = KnotComb
    { knotCombOpens = HM.empty
    , knotCombOpen = \finals -> TiedComb
        { combSimpl = x
        }
    }
instance LiftDerived1 (KnotComb letName repr) where
  liftDerived1 f a = a
    { knotCombOpen = \finals -> TiedComb
      { combSimpl = f (combSimpl (knotCombOpen a finals))
      }
    }
instance (Eq letName, Hashable letName) => LiftDerived2 (KnotComb letName repr) where
  liftDerived2 f a b = KnotComb
    { knotCombOpens = knotCombOpens a <> knotCombOpens b
    , knotCombOpen = \finals -> TiedComb
      { combSimpl = f
         (combSimpl (knotCombOpen a finals))
         (combSimpl (knotCombOpen b finals))
      }
    }
instance (Eq letName, Hashable letName) => LiftDerived3 (KnotComb letName repr) where
  liftDerived3 f a b c = KnotComb
    { knotCombOpens = HM.unions
      [ knotCombOpens a
      , knotCombOpens b
      , knotCombOpens c
      ]
    , knotCombOpen = \finals -> TiedComb
      { combSimpl = f
         (combSimpl (knotCombOpen a finals))
         (combSimpl (knotCombOpen b finals))
         (combSimpl (knotCombOpen c finals))
      }
    }
instance (Eq letName, Hashable letName) => LiftDerived4 (KnotComb letName repr) where
  liftDerived4 f a b c d = KnotComb
    { knotCombOpens = HM.unions
      [ knotCombOpens a
      , knotCombOpens b
      , knotCombOpens c
      , knotCombOpens d
      ]
    , knotCombOpen = \finals -> TiedComb
      { combSimpl = f
         (combSimpl (knotCombOpen a finals))
         (combSimpl (knotCombOpen b finals))
         (combSimpl (knotCombOpen c finals))
         (combSimpl (knotCombOpen d finals))
      }
    }

-- * Data family 'Comb'
-- | 'Comb'inators of the 'Grammar'.
-- This is an extensible data-type.
data family Comb
  (comb :: ReprComb -> Constraint)
  :: ReprComb -> ReprComb
type instance Derived (Comb comb repr) = repr

-- | 'unsafeCoerce' restrained to 'SimplComb'.
-- Useful to avoid dependant-map when inlining.
unsafeSimplComb :: SimplComb repr a -> SimplComb repr b
unsafeSimplComb = unsafeCoerce

-- | Convenient utility to pattern-match a 'SimplComb'.
pattern Comb :: Typeable comb => Comb comb repr a -> SimplComb repr a
pattern Comb x <- (unSimplComb -> Just x)

-- ** Type 'SimplComb'
-- | Interpreter simplifying combinators.
-- Useful to handle a list of 'Comb'inators
-- without requiring impredicative quantification.
-- Must be used by pattern-matching
-- on the 'SimplComb' data-constructor,
-- to bring the constraints in scope.
--
-- The optimizations are directly applied within it,
-- to avoid introducing an extra newtype,
-- this also give a more understandable code.
data SimplComb repr a =
  forall comb.
  (Derivable (Comb comb repr), Typeable comb) =>
  SimplComb
    { combData :: Comb comb repr a
      -- ^ Some 'Comb'inator existentialized
      -- over the actual combinator symantic class.
    , combInline :: Bool
      -- ^ Whether this combinator must be inlined
      -- in place of a 'ref'erence pointing to it
      -- (instead of generating a 'call').
    , combRefs :: HS.HashSet TH.Name
      -- ^ 'ref''s names reacheable from combinator
      -- (including those behind 'ref's).
    }

type instance Derived (SimplComb repr) = repr
instance Derivable (SimplComb repr) where
  derive SimplComb{..} = derive combData

-- | @(unSimplComb c :: 'Maybe' ('Comb' comb repr a))@
-- extract the data-constructor from the given 'SimplComb'
-- iif. it belongs to the @('Comb' comb repr a)@ data-instance.
unSimplComb ::
  forall comb repr a.
  Typeable comb =>
  SimplComb repr a -> Maybe (Comb comb repr a)
unSimplComb SimplComb{ combData = c :: Comb c repr a } =
  case typeRep @comb `eqTypeRep` typeRep @c of
    Just HRefl -> Just c
    Nothing -> Nothing

-- CombAlternable
data instance Comb CombAlternable repr a where
  Alt :: Exception -> SimplComb repr a -> SimplComb repr a -> Comb CombAlternable repr a
  Empty :: Comb CombAlternable repr a
  Failure :: SomeFailure -> Comb CombAlternable repr a
  Throw :: ExceptionLabel -> Comb CombAlternable repr a
  Try :: SimplComb repr a -> Comb CombAlternable repr a
instance CombAlternable repr => Derivable (Comb CombAlternable repr) where
  derive = \case
    Alt exn x y -> alt exn (derive x) (derive y)
    Empty -> empty
    Failure sf -> failure sf
    Throw exn -> throw exn
    Try x -> try (derive x)
instance
  ( CombAlternable repr
  , CombApplicable repr
  , CombLookable repr
  , CombMatchable repr
  , CombSelectable repr
  ) => CombAlternable (SimplComb repr) where
  empty = SimplComb
    { combData = Empty
    , combInline = True
    , combRefs = HS.empty
    }
  failure sf = SimplComb
    { combData = Failure sf
    , combInline = True
    , combRefs = HS.empty
    }

  alt _exn p@(Comb Pure{}) _ = p
    -- & trace "Left Catch Law"
  alt _exn (Comb Empty) u = u
    -- & trace "Left Neutral Law"
  alt _exn u (Comb Empty) = u
    -- & trace "Right Neutral Law"
  alt exn (Comb (Alt exn' u v)) w | exn' == exn = u <|> (v <|> w)
    -- See Lemma 1 (Associativity of choice for labeled PEGs)
    -- in https://doi.org/10.1145/2851613.2851750
    -- & trace "Associativity Law"
  alt exn (Comb (Look p)) (Comb (Look q)) = look (alt exn (try p) q)
    -- & trace "Distributivity Law"
  alt exn x y = SimplComb
    { combData = Alt exn x y
    , combInline = False
    , combRefs = combRefs x <> combRefs y
    }

  throw exn = SimplComb
    { combData = Throw exn
    , combInline = True
    , combRefs = HS.empty
    }

  try (Comb (p :$>: x)) = try p $> x
    -- & trace "Try Interchange Law"
  try (Comb (f :<$>: p)) = f <$> try p
    -- & trace "Try Interchange Law"
  try x = SimplComb
    { combData = Try x
    , combInline = False
    , combRefs = combRefs x
    }
instance
  ( CombApplicable repr
  , CombAlternable repr
  , CombLookable repr
  , CombMatchable repr
  , CombSelectable repr
  , Eq letName
  , Hashable letName
  ) => CombAlternable (KnotComb letName repr)

-- CombApplicable
data instance Comb CombApplicable repr a where
  Pure :: Production a -> Comb CombApplicable repr a
  (:<*>:) :: SimplComb repr (a -> b) -> SimplComb repr a -> Comb CombApplicable repr b
  (:<*:) :: SimplComb repr a -> SimplComb repr b -> Comb CombApplicable repr a
  (:*>:) :: SimplComb repr a -> SimplComb repr b -> Comb CombApplicable repr b
infixl 4 :<*>:, :<*:, :*>:
pattern (:<$>:) :: Production (a -> b) -> SimplComb repr a -> Comb CombApplicable repr b
pattern t :<$>: x <- Comb (Pure t) :<*>: x
pattern (:$>:) :: SimplComb repr a -> Production b -> Comb CombApplicable repr b
pattern x :$>: t <- x :*>: Comb (Pure t)
instance CombApplicable repr => Derivable (Comb CombApplicable repr) where
  derive = \case
    Pure x -> pure x
    f :<*>: x -> derive f <*> derive x
    x :<*: y -> derive x <* derive y
    x :*>: y -> derive x *> derive y
instance
  ( CombApplicable repr
  , CombAlternable repr
  , CombLookable repr
  , CombMatchable repr
  , CombSelectable repr
  ) => CombApplicable (SimplComb repr) where
  pure a = SimplComb
    { combData = Pure a
    , combInline = False -- TODO: maybe True?
    , combRefs = HS.empty
    }
  f <$> Comb (Branch b l r) =
    branch b
      ((Prod..) Prod..@ f <$> l)
      ((Prod..) Prod..@ f <$> r)
    -- & trace "Branch Distributivity Law"
  f <$> Comb (Conditional a bs def) =
    conditional a
      ((\(p, b) -> (p, f <$> b)) F.<$> bs)
      (f <$> def)
    -- & trace "Conditional Distributivity Law"
  -- Being careful here to use (<*>),
  -- instead of SimplComb { combData = f <$> combData x },
  -- in order to apply the optimizations of (<*>).
  f <$> x = pure f <*> x

  x <$ u = u $> x
    -- & trace "Commutativity Law"

  Comb Empty <*> _ = empty
    -- & trace "App Right Absorption Law"
  u <*> Comb Empty = u *> empty
    -- & trace "App Failure Weakening Law"
  Comb (Pure f) <*> Comb (Pure x) = pure (f Prod..@ x)
    -- & trace "Homomorphism Law"
  {-
  Comb (Pure f) <*> Comb (g :<$>: p) =
    -- This is basically a shortcut,
    -- it can be caught by one Composition Law
    -- and two Homomorphism Law.
    (Prod..) Prod..@ f Prod..@ g <$> p
    -- & trace "Functor Composition Law"
  -}
  u <*> Comb (Pure x) = Prod.flip Prod..@ (Prod.$) Prod..@ x <$> u
    -- & trace "Interchange Law"
  u <*> Comb (v :<*>: w) = (((Prod..) <$> u) <*> v) <*> w
    -- & trace "Composition Law"
  Comb (u :*>: v) <*> w = u *> (v <*> w)
    -- & trace "Reassociation Law 1"
  u <*> Comb (v :<*: w) = (u <*> v) <* w
    -- & trace "Reassociation Law 2"
  u <*> Comb (v :$>: x) = (u <*> pure x) <* v
    -- & trace "Reassociation Law 3"
  p <*> Comb (NegLook q) =
    (p <*> pure Prod.unit) <* negLook q
    -- & trace "Absorption Law"
  x <*> y = SimplComb
    { combData = x :<*>: y
    , combInline = False
    , combRefs = combRefs x <> combRefs y
    }

  Comb Empty *> _ = empty
    -- & trace "App Right Absorption Law"
  Comb (_ :<$>: p) *> q = p *> q
    -- & trace "Right Absorption Law"
  Comb Pure{} *> u = u
    -- & trace "Identity Law"
  Comb (u :$>: _) *> v = u *> v
    -- & trace "Identity Law"
  u *> Comb (v :*>: w) = (u *> v) *> w
    -- & trace "Associativity Law"
  x *> y = SimplComb
    { combData = x :*>: y
    , combInline = False
    , combRefs = combRefs x <> combRefs y
    }

  Comb Empty <* _ = empty
    -- & trace "App Right Absorption Law"
  u <* Comb Empty = u *> empty
    -- & trace "App Failure Weakening Law"
  p <* Comb (_ :<$>: q) = p <* q
    -- & trace "Left Absorption Law"
  u <* Comb Pure{} = u
    -- & trace "Identity Law"
  u <* Comb (v :$>: _) = u <* v
    -- & trace "Identity Law"
  Comb (u :<*: v) <* w = u <* (v <* w)
    -- & trace "Associativity Law"
  x <* y = SimplComb
    { combData = x :<*: y
    , combInline = False
    , combRefs = combRefs x <> combRefs y
    }
instance
  ( CombApplicable repr
  , CombAlternable repr
  , CombLookable repr
  , CombMatchable repr
  , CombSelectable repr
  , Eq letName
  , Hashable letName
  ) => CombApplicable (KnotComb letName repr)

-- CombFoldable
data instance Comb CombFoldable repr a where
  ChainPre :: SimplComb repr (a -> a) -> SimplComb repr a -> Comb CombFoldable repr a
  ChainPost :: SimplComb repr a -> SimplComb repr (a -> a) -> Comb CombFoldable repr a
instance CombFoldable repr => Derivable (Comb CombFoldable repr) where
  derive = \case
    ChainPre op p -> chainPre (derive op) (derive p)
    ChainPost p op -> chainPost (derive p) (derive op)
instance CombFoldable repr => CombFoldable (SimplComb repr) where
  chainPre op p = SimplComb
    { combData = ChainPre op p
    , combInline = False
    , combRefs = combRefs op <> combRefs p
    }
  chainPost p op = SimplComb
    { combData = ChainPost p op
    , combInline = False
    , combRefs = combRefs p <> combRefs op
    }
instance
  ( CombFoldable repr
  , Eq letName
  , Hashable letName
  ) => CombFoldable (KnotComb letName repr)

-- CombLookable
data instance Comb CombLookable repr a where
  Look :: SimplComb repr a -> Comb CombLookable repr a
  NegLook :: SimplComb repr a -> Comb CombLookable repr ()
  Eof :: Comb CombLookable repr ()
instance CombLookable repr => Derivable (Comb CombLookable repr) where
  derive = \case
    Look x -> look (derive x)
    NegLook x -> negLook (derive x)
    Eof -> eof
instance
  ( CombAlternable repr
  , CombApplicable repr
  , CombLookable repr
  , CombSelectable repr
  , CombMatchable repr
  ) => CombLookable (SimplComb repr) where
  look p@(Comb Pure{}) = p
    -- & trace "Pure Look Law"
  look p@(Comb Empty) = p
    -- & trace "Dead Look Law"
  look (Comb (Look x)) = look x
    -- & trace "Idempotence Law"
  look (Comb (NegLook x)) = negLook x
    -- & trace "Left Identity Law"
  look (Comb (p :$>: x)) = look p $> x
    -- & trace "Interchange Law"
  look (Comb (f :<$>: p)) = f <$> look p
    -- & trace "Interchange Law"
  look x = SimplComb
    { combData = Look x
    , combInline = False
    , combRefs = combRefs x
    }

  negLook (Comb Pure{}) = empty
    -- & trace "Pure Negative-Look"
  negLook (Comb Empty) = pure Prod.unit
    -- & trace "Dead Negative-Look"
  negLook (Comb (NegLook x)) = look (try x *> pure Prod.unit)
    -- & trace "Double Negation Law"
  negLook (Comb (Try x)) = negLook x
    -- & trace "Zero Consumption Law"
  negLook (Comb (Look x)) = negLook x
    -- & trace "Right Identity Law"
  negLook (Comb (Alt _exn (Comb (Try p)) q)) = negLook p *> negLook q
    -- FIXME: see if this really holds for all exceptions.
    -- & trace "Transparency Law"
  negLook (Comb (p :$>: _)) = negLook p
    -- & trace "NegLook Idempotence Law"
  negLook x = SimplComb
    { combData = NegLook x
    , combInline = False
    , combRefs = combRefs x
    }

  eof = SimplComb
    { combData = Eof
    , combInline = True
    , combRefs = HS.empty
    }
instance
  ( CombLookable repr
  , CombAlternable repr
  , CombApplicable repr
  , CombSelectable repr
  , CombMatchable repr
  , Eq letName
  , Hashable letName
  ) => CombLookable (KnotComb letName repr)

-- CombMatchable
data instance Comb CombMatchable repr a where
  Conditional ::
    SimplComb repr a ->
    [(Production (a -> Bool), SimplComb repr b)] ->
    SimplComb repr b ->
    Comb CombMatchable repr b
instance CombMatchable repr => Derivable (Comb CombMatchable repr) where
  derive = \case
    Conditional a bs def ->
      conditional (derive a)
        ((\(p, b) -> (p, derive b)) F.<$> bs)
        (derive def)
instance
  ( CombApplicable repr
  , CombAlternable repr
  , CombLookable repr
  , CombSelectable repr
  , CombMatchable repr
  ) => CombMatchable (SimplComb repr) where
  conditional (Comb Empty) _ def = def
    -- & trace "Conditional Absorption Law"
  conditional a bs (Comb Empty)
    | Foldable.all (\case { (_, Comb Empty) -> True; _ -> False }) bs = a *> empty
      -- & trace "Conditional Weakening Law"
  conditional (Comb (Pure a)) bs def =
    Foldable.foldr (\(p, b) acc ->
      if runValue (p Prod..@ a) then b else acc
    ) def bs
    -- & trace "Conditional Pure Law"
  conditional a bs d = SimplComb
    { combData = Conditional a bs d
    , combInline = False
    , combRefs = HS.unions
        $ combRefs a
        : combRefs d
        : ((\(_p, b) -> combRefs b) F.<$> bs)
    }
instance
  ( CombMatchable repr
  , CombAlternable repr
  , CombApplicable repr
  , CombLookable repr
  , CombSelectable repr
  , Eq letName
  , Hashable letName
  ) => CombMatchable (KnotComb letName repr) where
  conditional a bs d = KnotComb
    { knotCombOpens = HM.unions
        $ knotCombOpens a
        : knotCombOpens d
        : ((\(_p, b) -> knotCombOpens b) F.<$> bs)
    , knotCombOpen = \finals -> TiedComb
        { combSimpl = conditional
            (combSimpl (knotCombOpen a finals))
            ((\(p, b) -> (p, combSimpl (knotCombOpen b finals))) F.<$> bs)
            (combSimpl (knotCombOpen d finals))
        }
    }

-- CombSatisfiable
data instance Comb (CombSatisfiable tok) repr a where
  -- | To include the @('Set' 'SomeFailure')@ is a little kludge
  -- it would be cleaner to be able to pattern-match
  -- on @(alt exn (Comb 'Satisfy'{}) (Failure{}))@
  -- when generating 'Program', but this is not easily possible then
  -- because data types have already been converted back to class methods,
  -- hence pattern-matching is no longer possible
  -- (at least not without reintroducing data types).
  SatisfyOrFail ::
    CombSatisfiable tok repr =>
    Set SomeFailure ->
    Production (tok -> Bool) ->
    Comb (CombSatisfiable tok) repr tok
instance
  CombSatisfiable tok repr =>
  Derivable (Comb (CombSatisfiable tok) repr) where
  derive = \case
    SatisfyOrFail fs p -> satisfyOrFail fs p
instance
  (CombSatisfiable tok repr, Typeable tok) =>
  CombSatisfiable tok (SimplComb repr) where
  satisfyOrFail fs p = SimplComb
    { combData = SatisfyOrFail fs p
    , combInline = False -- TODO: True? depending on p?
    , combRefs = HS.empty
    }
instance
  ( CombSatisfiable tok repr
  , Typeable tok
  , Eq letName
  , Hashable letName
  ) => CombSatisfiable tok (KnotComb letName repr)

-- CombSelectable
data instance Comb CombSelectable repr a where
  Branch ::
    SimplComb repr (Either a b) ->
    SimplComb repr (a -> c) ->
    SimplComb repr (b -> c) ->
    Comb CombSelectable repr c
instance CombSelectable repr => Derivable (Comb CombSelectable repr) where
  derive = \case
    Branch lr l r -> branch (derive lr) (derive l) (derive r)
instance
  ( CombApplicable repr
  , CombAlternable repr
  , CombLookable repr
  , CombSelectable repr
  , CombMatchable repr
  ) => CombSelectable (SimplComb repr) where
  branch (Comb Empty) _ _ = empty
    -- & trace "Branch Absorption Law"
  branch b (Comb Empty) (Comb Empty) = b *> empty
    -- & trace "Branch Weakening Law"
  branch (Comb (Pure lr)) l r =
    case runValue lr of
      Left value -> l <*> pure (Pair v c)
        where
        v = Prod.SomeData $ Prod.Var $ Identity value
        c = Prod.SomeData $ Prod.Var
          [|| case $$(runCode lr) of Left x -> x ||]
      Right value -> r <*> pure (Pair v c)
        where
        v = Prod.SomeData $ Prod.Var $ Identity value
        c = Prod.SomeData $ Prod.Var
          [|| case $$(runCode lr) of Right x -> x ||]
    -- & trace "Branch Pure Either Law"
  branch b (Comb (Pure l)) (Comb (Pure r)) =
    Pair v c <$> b
    -- & trace "Branch Generalised Identity Law"
    where
    v = Prod.SomeData $ Prod.Var $ Identity $ either (runValue l) (runValue r)
    c = Prod.SomeData $ Prod.Var [|| either $$(runCode l) $$(runCode r) ||]
  branch (Comb (x :*>: y)) p q = x *> branch y p q
    -- & trace "Interchange Law"
  branch b l (Comb Empty) =
    branch (pure (Pair v c) <*> b) empty l
    -- & trace "Negated Branch Law"
    where
    v = Prod.SomeData $ Prod.Var $ Identity $ either Right Left
    c = Prod.SomeData $ Prod.Var $ [||either Right Left||]
  branch (Comb (Branch b (Comb Empty) (Comb (Pure lr)))) (Comb Empty) br =
    branch (pure (Pair v c) <*> b) empty br
    -- & trace "Branch Fusion Law"
    where
    v = Prod.SomeData $ Prod.Var $ Identity $ \case
      Left{} -> Left ()
      Right r ->
        case runValue lr r of
          Left{} -> Left ()
          Right rr -> Right rr
    c = Prod.SomeData $ Prod.Var
      [|| \case Left{} -> Left ()
                Right r -> case $$(runCode lr) r of
                             Left{} -> Left ()
                             Right rr -> Right rr ||]
  branch b l r = SimplComb
    { combData = Branch b l r
    , combInline = False
    , combRefs = HS.unions [ combRefs b, combRefs l, combRefs r ]
    }
instance
  ( CombSelectable repr
  , CombAlternable repr
  , CombApplicable repr
  , CombLookable repr
  , CombMatchable repr
  , Eq letName
  , Hashable letName
  ) => CombSelectable (KnotComb letName repr)

-- CombRegisterableUnscoped
data instance Comb CombRegisterableUnscoped repr a where
  NewUnscoped :: UnscopedRegister a -> SimplComb repr a -> SimplComb repr b -> Comb CombRegisterableUnscoped repr b
  GetUnscoped :: UnscopedRegister a -> Comb CombRegisterableUnscoped repr a
  PutUnscoped :: UnscopedRegister a -> SimplComb repr a -> Comb CombRegisterableUnscoped repr ()
instance CombRegisterableUnscoped repr => Derivable (Comb CombRegisterableUnscoped repr) where
  derive = \case
    NewUnscoped r ini x -> newUnscoped r (derive ini) (derive x)
    GetUnscoped r -> getUnscoped r
    PutUnscoped r x -> putUnscoped r (derive x)
instance -- TODO: optimizations
  ( CombRegisterableUnscoped repr
  ) => CombRegisterableUnscoped (SimplComb repr) where
  newUnscoped r ini x = SimplComb
    { combData = NewUnscoped r ini x
    , combInline = combInline ini && combInline x
    , combRefs = combRefs ini <> combRefs x
    }
  getUnscoped r = SimplComb
    { combData = GetUnscoped r
    , combInline = True
    , combRefs = HS.empty
    }
  putUnscoped r x = SimplComb
    { combData = PutUnscoped r x
    , combInline = combInline x
    , combRefs = combRefs x
    }
instance
  ( CombRegisterableUnscoped repr
  , Eq letName
  , Hashable letName
  ) => CombRegisterableUnscoped (KnotComb letName repr) where

-- Letsable
data instance Comb (Letsable letName) repr a where
  Lets ::
    LetBindings letName (SimplComb repr) ->
    SimplComb repr a ->
    Comb (Letsable letName) repr a
instance
  Letsable letName repr =>
  Derivable (Comb (Letsable letName) repr) where
  derive = \case
    Lets defs x -> lets
      ((\(SomeLet sub) -> SomeLet (derive sub)) F.<$> defs)
      (derive x)
instance
  (Letsable letName repr, Typeable letName) =>
  Letsable letName (SimplComb repr) where
  lets defs body = SimplComb
    { combData = Lets defs body
    , combInline = False
    , combRefs = HS.unions
        $ combRefs body
        : ((\(SomeLet sub) -> combRefs sub) F.<$> HM.elems defs)
    }
instance
  Letsable TH.Name repr =>
  Letsable TH.Name (KnotComb TH.Name repr) where
  lets defs body = KnotComb
    { knotCombOpens =
        HM.unions
          $ knotCombOpens body
          : ((\(SomeLet sub) -> SomeLet . knotCombOpen sub) F.<$> defs)
          -- Not really necessary to include 'knotCombOpens' of 'defs' here
          -- since there is only a single 'lets' at the top of the AST,
          -- but well.
          : ((\(SomeLet sub) -> knotCombOpens sub) F.<$> HM.elems defs)
    , knotCombOpen = \finals -> TiedComb
        { combSimpl =
          let bodySimpl = combSimpl $ knotCombOpen body finals in
          let defsSimpl = (\(SomeLet sub) -> SomeLet $ combSimpl $ knotCombOpen sub finals) F.<$> defs in
          let defsUsed = HS.unions
                $ combRefs bodySimpl
                : ((\(SomeLet sub) -> combRefs sub) F.<$> HM.elems defsSimpl) in
          lets (HM.intersection defsSimpl (HS.toMap defsUsed)) bodySimpl
        }
    }

-- Referenceable
data instance Comb (Referenceable letName) repr a where
  Ref :: Bool -> letName -> Comb (Referenceable letName) repr a
instance
  Referenceable letName repr =>
  Derivable (Comb (Referenceable letName) repr) where
  derive = \case
    Ref isRec name -> ref isRec name
instance
  Referenceable TH.Name repr =>
  Referenceable TH.Name (SimplComb repr) where
  ref isRec name = SimplComb
    { combData = Ref isRec name
    , combInline = not isRec
    , combRefs = HS.singleton name
    }
instance
  Referenceable TH.Name repr =>
  Referenceable TH.Name (KnotComb TH.Name repr) where
  ref isRec name = KnotComb
    { knotCombOpens = HM.empty
    , knotCombOpen = \finals ->
      if isRec
      then TiedComb
        { combSimpl = ref isRec name
        }
      else case finals HM.! name of
        SomeLet a@TiedComb
          { combSimpl = p@SimplComb{ combInline = True }
          } -> a{combSimpl = unsafeSimplComb p}
        SomeLet TiedComb
          { combSimpl = SimplComb{ combRefs = refs }
          } -> TiedComb
            { combSimpl = (ref isRec name)
              { combRefs = HS.insert name refs }
            }
    }