Towards nominal renaming sets

Renaming.hs

{-# language DeriveGeneric #-}
{-# language LambdaCase #-}
{-# language DeriveAnyClass #-}
{-# language StrictData #-}
{-# language TypeOperators #-}
{-# language MultiParamTypeClasses #-}
{-# language FlexibleInstances #-}
{-# language UndecidableInstances #-}

---------------------------------------------------------------------------------
-- |
-- Copyright :  (c) Edward Kmett 2018
-- License   :  BSD-2-Clause OR Apache-2.0
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
---------------------------------------------------------------------------------

module Pat1 where

import Control.Lens (prism)
import Data.Rename
import GHC.Generics
import GHC.Show
import Data.Text.Short
import Type.Reflection

-- type Show_ f = forall a. Show (f a)
class Show_ f where showsPrec_ :: Int -> f a -> ShowS
instance Show_ Proxy where showsPrec_ = showsPrec
instance Show a => Show_ (Const a) where showsPrec_ = showsPrec
instance Show_ V1 where showsPrec_ = \case
instance Show_ U1 where showsPrec _ U1 = showString "U1"
instance Show_ f => Show_ (M1 i c f) where showsPrec d (M1 c) = showParen (d > 10) $ showString "K1 " . showsPrec_ 11 c
instance Show c => Show_ (K1 i c) where showsPrec d (K1 c) = showParen (d > 10) $ showString "K1 " . showsPrec 11 c
instance (Show_ f, Show_ g) => Show_ (f :*: g) where showsPrec_ d (s :*: t) = showParen (d > 6) $ showsPrec_ 7 s . showString " :*: " . showsPrec_ 6 s
instance (Show_ f, Show_ g) => Show_ (f :+: g) where
  showsPrec_ d (L1 s) = showParen (d > 10) $ showString "L1 " . showsPrec 11 s
  showsPrec_ d (R1 s) = showParen (d > 10) $ showString "R1 " . showsPrec 11 s
instance (Show1 f, Show_ g) => Show_ (f :.: g) where
  showsPrec_ d (Comp1 s) = showParen (d > 10) $ showString "Comp1 " . showsPrec1_ 11 s

showsPrec1_ :: (Show1 f, Show_ g) => Int -> f (g a) -> ShowS
showsPrec1_ = liftShowsPrec showsPrec_ (showList_ (showsPrec_ 0))

-- type Eq_ f = forall a. Eq (f a)
class Eq_ f where eq_ :: f a -> f a -> Bool
eq1_ :: (Eq1 f, Eq_ g) => f (g a) -> f (g a) -> Bool
eq1_ = liftEq eq_
instance Eq_ Proxy where showsPrec_ = showsPrec
instance Eq a => Eq_ (Const a) where eq_ = (==)
instance Eq_ V1 where eq_ = absurd
instance Eq_ U1 where eq_ _ _ = True
instance Eq_ c => Eq_ (K1 i c) where eq_ (M1 a) (M1 b) = a == b
instance Eq_ f => Eq_ (M1 i c f) where eq_ (M1 a) (M1 b) = eq_ a b
instance (Eq1 f, Eq_ g) => Eq_ (f :.: g) where eq_ (Comp1 s) (Comp1 t) = eq1_ s t 
instance (Eq_ f, Eq_ g) => Eq_ (f :*: g) where (a :*: b) == (c :*: d) = eq_ a c && eq_ b d
instance (Eq_ f, Eq_ g) => Eq_ (f :+: g) where
  L1 a == L1 b = eq_ a b
  R1 a == R1 b = eq_ a b
  _ == _ = False

-- type Semigroup_ f = forall a. Semigroup (f a)
class Semigroup_ f where mappend_ :: f a -> f a -> f a
instance Semigroup_ Proxy where mappend_ _ _ = Proxy
instance Semigroup a => Semigroup_ (Const a) where mappend_ = (<>)
instance Semigroup_ [] where mappend_ = (++)
instance Semigroup_ NonEmpty where mappend_ = (<>)
instance (Applicative f, Semigroup_ g) => Semigroup (f :.: g) where mappend_ (Comp1 s) (Comp1 t) = Comp1 (liftA2 mappend_ s t)
instance (Semigroup_ a, Semigroup_ b) => Semigroup_ (f :*: g) where mappend_ (a :*: b) (c :*: d) = mappend_ a c :*: mappend_ b d
instance Semigroup a => Semigroup_ (K1 i c) where K1 a `mappend_` K1 b = K1 (a <> b)
instance Semigroup_ f => Semigroup_ (M1 i c f) where M1 a `mappend_` M1 b = M1 (mappend_ a b)

-- type Monoid_ f = forall a. Monoid (f a)
class Semigroup_ f => Monoid_ f where mempty_ :: f a
instance Monoid_ Proxy where mempty_ = Proxy
instance Monoid a => Monoid_ (Const a) where mempty_ = mempty
instance Monoid_ [] where mempty_ = mempty
instance (Applicative f, Monoid_ g) => Monoid (f :.: g) where mempty = Comp1 (pure mempty_)
instance (Monoid_ a, Monoid_ b) => Monoid_ (f :*: g) where mempty_ = mempty_ :*: mempty_
instance Monoid a => Monoid_ (K1 i c) where mempty_ = K1 mempty
instance Monoid_ f => Monoid_ (M1 i c f) where mempty_ = M1 mempty_

type f ~> g = forall x. f x -> g x

-- let's make up a ton of vocabulary
data Tag a = Tag (TypeRep a) ShortText deriving (Eq, Show)
mistag :: Typeable b => Tag a -> Tag b
mistag (Tag _ t) = Tag typeRep t
instance TestEquality Tag where testEquality (Tag s a) (Tag t b) = guard (a == b) >> testEquality s t
instance TestCoercion Tag where testCoercion (Tag s a) (Tag t b) = guard (a == b) >> testCoercion s t 
instance Eq_ Tag where eq_ (Tag _ a) (Tag _ b) = a == b
instance Eq (Tag a) where Tag _ a == Tag _ b = a == b
instance Show_ Tag where showsPrec d (Tag t s) = showParen (d > 10) $ showString "Tag " . showsPrec 11 t . showChar ' ' . showsPrec 11 s
instance Show (Tag a) where showsPrec = showsPrec_

data Name a = Name (Tag a) (Maybe Natural) deriving (Eq, Show)
misname :: Typeable b => Name a -> Name b
misname (Name t n) = Name (mistag t) n
instance TestEquality Name where testEquality (Name s i) (Name t j) = guard (i == j) >> testEquality s t
instance TestCoercion Name where testCoercion (Name s i) (Name t j) = guard (i == j) >> testCoercion s t 
instance Eq_ Name where eq_ (Name a b) (Name c d) = eq_ a c && b == d
instance Eq (Name a) where (==) = eq_
instance Show_ Name where showsPrec_ d (Name t i) = showParen (d > 10) $ showString "Name " . showsPrec 11 t . showChar ' ' . showsPrec 11 i
instance Show (Name a) where showsPrec = showsPrec_

data K where K :: Tag a -> K
instance Eq K where K s == K t = isJust (testEquality s t)
instance Show K where showsPrec d (K t) = showParen (d > 10) $ showString "K " . showsPrec 11 t

class FFunctor t where ffmap :: (f ~> g) -> t f -> t g
instance FFunctor (Const a) where ffmap _ (Const a) = Const a
instance FFunctor Proxy where ffmap _ Proxy = Proxy

class FFunctor t => FTraversable t where ftraverse :: (forall x. f x -> m (g x)) -> t f -> m (t g)
instance FTraversable (Const a) where ftraverse _ (Const a) = pure $ Const a
instance FTraversable Proxy where ftraverse _ Proxy = Proxy
ffmapDefault :: FTraversable t => (f ~> g) -> t f -> t g
ffmapDefault f = runIdentity #. ftraverse (Identity #. f)

data V f where V :: TypeRep a -> f a -> V
instance FFunctor V where ffmap f (V t a) = V t (f a)
instance FTraversable V where ftraverse f (V t a) = V t (f a)
unV :: forall a. Typeable a => V f -> Maybe (f a)
unV (V t b) = eqTypeRep t (typeRep @a) <&> \Refl -> b
instance Show_ f => Show (V f) where showsPrec_ d (V t a) = showParen (d > 10) $ showString "V " . showsPrec 11 t . showChar ' ' . showsPrec 11 a
instance Eq_ f => Eq (V f) where
  V s a == V t b = case testEquality s t of
    Just Refl -> eq_ a b
    Nothing -> False
instance Semigroup_ f => Semigroup (V f) where
  l@(V s a) <> V t b = case testEquality s t of
    Just Refl -> V s (mappend_ a b)
    Nothing -> l -- bad sketch

newtype Sketch f = Sketch { getSketch :: Map K (V f) } deriving (Eq, Show)
makePrisms ''Sketch
instance FFunctor Sketch where ffmap f (Sketch m) = Sketch $ fmap (ffmap f) m
instance FTraversable Sketch where ftraverse f (Sketch m) = Sketch <$> traverse (ftraverse f) m
instance Semigroup_ f => Semigroup (Sketch f) where Sketch m <> Sketch n = Sketch (unionWith (<>) m n)
instance Semigroup_ f => Monoid (Sketch f) where mempty = Sketch mempty

sketch :: Tag a -> Lens (Sketch f) (Maybe (f a))
sketch t f (Sketch m) = Sketch <$> at (K t) f' m where
  f' Nothing = fmap (V t) <$> f Nothing
  f' (Just (V t' a)) = case testEquality t t' of
    Just Refl -> fmap (V t) <$> f (Just a)
    Nothing -> error "bad sketch"

class FTraversable t => FTraversableWithIndex s t | t -> s where iftraverse :: (forall a. s a -> f a -> m (g a)) -> t f -> t g
instance FTraversableWithIndex Tag Sketch where
  iftraverse f = _Sketch.itraverse $ \(K t@(Tag tr _)) (V tr' b) -> case testEquality tr tr' of
    Just Refl -> V tr' <$> f t b
    Nothing -> error "bad sketch"

class HFunctor t where hfmap :: (f ~> g) -> t f a -> t g a
instance HFunctor (WriterT e) where hfmap f = WriterT #. f .# runWriterT
instance HFunctor (ExceptT e) where hfmap f = ExceptT #. f .# runExceptT
instance HFunctor MaybeT where hfmap f = MaybeT #. f .# runMaybeT
instance HFunctor (StateT s) where hfmap f = StateT #. fmap f .# runStateT
instance HFunctor (M1 i c) where hfmap f = M1 #. f .# unM1
instance HFunctor Rec1 where hfmap f = Rec1 #. f .# unRec1
instance HFunctor ((:*:) f) where hfmap f (s :*: a) = s :*: f a
instance HFunctor ((:+:) f) where
  hfmap f (L1 s) = L1 s
  hfmap f (R1 a) = R1 (f a)
instance Functor f => HFunctor ((:.:) f) where hfmap f = Comp1 #. fmap f .# unComp1
instance Functor f => HFunctor (Compose f) where hfmap f = Compose #. fmap f .# getCompose

class HFunctor t => HTraversable t where htraverse :: (forall x. f x -> m (g x)) -> t f a -> m (t g a)
instance HTraversable (EitherT e) where htraverse f = fmap ExceptT . f .# runExceptT
instance HTraversable MaybeT where htraverse f = fmap MaybeT . traverse f .# runMaybeT
instance HTraversable (WriterT e) where htraverse f = fmap WriterT . f .# runWriterT
instance HTraversable (M1 i c) where htraverse f = fmap M1 . f .# unM1
instance HTraversable Rec1 where htraverse f = fmap Rec1 . f .# unRec1
instance HTraversable ((:*:) f) where htraverse f (s :*: a) = (:*:) s <$> f a
instance HTraversable ((:+:) f) where
  htraverse f (L1 s) = pure $ L1 s
  htraverse f (R1 a) = R1 <$> f a
instance Traversable f => HTraversable (Compose f) where htraverse f = fmap Compose . traverse f .# getCompose
instance Traversable f => HTraversable ((:.:) f) where htraverse f = fmap Comp1 . traverse f .# unComp1

hfmapDefault :: FTraversable t => (f ~> g) -> t f a -> t g a
hfmapDefault f = runIdentity #. htraverse (Identity #. f)

data I f a = I (Maybe (f a)) (Map Natural (f a))
instance HFunctor I where hfmap f (I ma as) = I (fmap f ma) (fmap f as)
instance HTraversable I where htraverse f (I ma as) = I <$> f ma <*> fmap f as
instance Eq_ f => Eq_ (I f) where eq_ (I ma as) (I mb bs) = eq1_ ma mb && eq1_ as bs
instance Eq_ f => Eq (I f a) where (==) = eq_
instance Show_ f => Show_ (I f) where showsPrec_ d (I m b) = showParen (d > 10) $ showString "I " . showsPrec1_ 11 m . showChar ' ' . showsPrec1_ 11 b
instance Show_ f => Show (I f a) where showsPrec = showsPrec_
instance Semigroup_ f => Semigroup_ (I f) where
  I ma as `mappend_` I mb bs = I mc (Map.unionWith mappend_ as bs) where
    mc = case ma of
      Nothing -> mb
      Just a -> maybe (mappend_ a) ma mb

newtype St f = St (Sketch K (I f)) deriving (Eq, Show, Semigroup, Monoid)
makePrisms ''St
instance FFunctor St where ffmap f (St m) = St $ ffmap (hfmap f) m
instance FTraversable St where ftraverse f = _St $ ftraverse (htraverse f)
st :: Name a -> Lens (St f) (Maybe (f a))
st (Name t mn) f (St m) = St <$> sketch t f' m where
  f' Nothing = f Nothing <&> \mb -> mb <&> \_ -> case mn of
    Nothing -> I mb mempty
    Just i ->  I Nothing $ Map.singleton i mb
  f' (Just (I mb bs)) = case mn of 
    Nothing -> f mb <&> \case 
      Nothing | null bs -> Nothing
      mb' -> I mb' bs 
    Just i -> at i f bs <&> \bs' -> I mb bs' <$ guard (isJust mb || not (null bs'))
instance FTraversableWithIndex Name St where
  iftraverse f = _St.iftraverse $ \t (I ma as) -> I <$> traverse (f (Name t Nothing)) ma <$> itraverse (f . Name t . Just) as

newtype N a = N Natural deriving (Eq,Ord,Show,Read,Num)
makePrisms ''N
instance Semigroup_ N where N a `mappend_` N b = N (max a b)
instance Semigroup (N a) where N a <> N b = N (max a b)
instance Monoid_ N where mempty_ = N 0
instance Monoid (N a) where mempty = N 0
sup :: I f a -> N
sup (I _ as) = N . (1+) . fst <$> maxView as <|> Just 0

data Counted f a = Counted Natural (f a) -- 0 references means this is the only one?
instance Semigroup_ f => Semigroup_ (Counted f) where mappend_ (Counted n a) (Counted m b) = Counted (n + m) (mappend_ a b)
instance Monoid_ f => Monoid_ (Counted f) where mempty_ = Counted 0 mempty
-- add :: St f -> St (Counted g) -> St (Counted g)
-- sub :: St f -> St (Counted g) -> St (Counted g)

newtype Store f = Store (St (Counted f)) -- counts let me track exact usage figures
makePrisms ''Store

-- | this can be used to produce an endless supply of fresh names
newtype Supply = Supply (Sketch N) deriving (Eq,Ord,Show,Semigroup,Monoid)
makePrisms ''Supply

newtype Renaming = Renaming (Store Name) deriving (Eq, Show)
makePrisms ''Renaming

data Support where Support :: Store f -> Support

instance Semigroup Supply where Supply m <> Supply n = Supply (m <> n)
instance Monoid Supply where mempty = Supply mempty

insertSupply :: Name a -> Supply -> Supply
insertSupply (Name t mn) = _Supply . sketch t <>~ fmap (N #. (1+)) mn <|> Just 0

fresh :: Tag a -> State Supply (Name a)
fresh t = _Supply.sketch t %%= \mn -> (Name t mn, fmap (1+) mn <|> Just 0)

refresh :: Name a -> State Supply (Name a)
refresh (Name t _) = fresh t

-- this is more set-like again, later, check to see if we can recover the finer support i like in names
instance Semigroup Support where Support m <> Support n = Support $ error "TODO"
instance Monoid Support where mempty = Support (mempty :: Store (Const Void))
-- compute something for each member of the support
walk :: Applicative m => Support -> (Name a -> m (f a)) -> m (Store f)
walk (Support m) f = iftraverse (\n _ -> f n) m

single :: Name a -> Support
single n = Support $ mempty & store t ?~ Proxy

renaming :: Name a -> Lens Renaming (Name a)
renaming n = _Renaming.store n.non n

infix 9 ↦
-- @
-- rename (a ↦ b) a = b
-- rename (a ↦ b) b = b
-- rename (a ↦ b) c = b
-- @
(↦) :: Name a -> Name a -> Renaming
a ↦ b = mempty & renaming a .~ b

instance Monoid Renaming where mempty = Renaming mempty
-- | @a ↦ b <> b ↦ a = a ↦ b@
instance Semigroup Renaming where
  l <> Renaming (Store (Sketch r)) = Map.foldrWithKey step l r where
    step (K t@(Tag tr _)) (V tr' (I ma as)) l' = case testEquality tr tr' of
      Just Refl -> maybe id (renaming (Name t Nothing) .~) ma $ Map.foldrWithKey (\i -> renaming (Name t (Just i)) .~) l' as
      Nothing -> error "bad renaming"

-- an even better version would be to store actual counts in the nodes, then we can give exact updates
store :: Supported (f a) => Name a -> Lens (Store f) (Maybe (f a))
store a0 f0 (Store t0) = tweak <$> getCompose (st a0 (Compose . fmap diag . f0) t0) where
  diag a = (a,a)
  tweak (_, n) | null n = 
  tweak (Just a, t)  = -- grab the support of a then insert it into St as "nothings"
  tweak (Nothing, t) = t
  
  f' (

  at a0 f0 (Map s0 t0) = tweak <$> getCompose (at a0 (Compose . fmap diag . f0) t0) where
    diag a = (a,a)
    tweak (_, Empty)  = Map mempty Empty
    tweak (Just a,t)  = Map (supp a0 <> supp a <> s0) t
    tweak (Nothing,t) = Map s0 t
  -- we should make the tweak then merge the support of the result

class Supported a where
  rename :: Renaming -> a -> a
  default rename :: (Generic a, GSupported (Rep a)) => Renaming -> a -> a
  rename m = from . rename m . to
  -- |
  -- @supp (rename s a)) ⊆ rename s (supp a)@
  --
  -- if @s@ is injective, @supp (rename s a) = rename s (supp a)@
  supp :: a -> Support
  default supp :: Deciding Supported a => a -> Support
  supp = getOp $ deciding (Proxy :: Proxy Support) (Op supp) 

  -- | @supply = supply.supp@
  supply :: a -> Supply
  default supply :: Deciding Supported a => a -> Support
  supply = getOp $ deciding (Proxy :: Proxy Support) (Op supp) 

-- instance Supported1 f => Supported (Store f) where 
instance Supported Name where
  rename n (Renaming s) = fromMaybe n $ s^?store n
instance Supported () where rename _ = id; supp = mempty; supply = mempty
instance Supported Char where rename _ = id; supp = mempty; supply = mempty
instance Supported Int where rename _ = id; supp = mempty; supply = mempty
instance Supported Void where rename _ = absurd; supp = absurd; supply = absurd
instance Supported a => Supported [a]
instance Supported a => Supported (Maybe a)
instance (Supported a, Supported b) => Supported (a, b)
instance (Supported a, Supported b, Supported c) => Supported (a, b, c)
instance (Supported a, Supported b) => Supported (Either a b)

class Supported1 f where
  rename1 :: (Renaming a -> a -> a) -> Renaming -> f a -> f a
  default rename1 :: (Generic1 f, Supported1 (Rep1 f)) => (Renaming a -> a -> a) -> Renaming -> f a -> f a
  rename1 f m = from1 . rename1 f m . to1

  supp1 :: (a -> Support) -> f a -> Support
  default supp1 :: (Generic1 f, Supported1 (Rep1 f)) => (a -> Support) -> f a -> Support
  supp1 f = supp1 f . to1

  supply1 :: (a -> Supply) -> f a -> Supply
  default supply1 :: (Generic1 f, Supported1 (Rep1 f)) => (a -> Supply) -> f a -> Supply
  supply1 f = supply1 f . to1

instance Supported1 U1 where
  rename1 _ _ U1 = U1
  supp1 = mempty
  supply1 = mempty

instance Supported1 V1 where
  rename1 _ _ = \case
  supp1 _ = \case
  supply1 _ = \case

instance Supported c => Supported1 (K1 i c) where
  rename1 _ n (K1 m) = K1 (rename n m)
  supp1 _ (K1 m) = supp m
  supply1 _ (K1 m) = supply m

instance Supported1 f => Supported1 (M1 i c f) where
  rename1 f n (M1 s) = M1 (rename1 f n s)
  supp1 f (M1 s) = supp1 f s
  supply1 f (M1 s) = supply1 f s

instance Supported1 Par1 where
  rename1 f n (Par1 a) = Par1 (f n a)
  supp1 f (Par1 a) = f a
  supply1 f (Par1 a) = f a

instance Supported1 f => Supported1 (Rec1 f) where
  rename1 f n (Rec1 a) = Rec1 (rename1 f n a)
  supp1 f (Rec1 a) = supp1 f a
  supply1 f (Rec1 a) = supply1 f a

instance (Supported1 f, Supported1 g) => Supported1 (f :*: g) where
  rename1 f n (s :*: t) = rename1 f n s :*: rename1 f n t
  supp1 f (s :*: t) = supp1 f s <> supp1 f t
  supply1 f (s :*: t) = supply1 f s <> supply1 f t

instance (Supported1 f, Supported1 g) => Supported1 (f :.: g) where
  rename1 f n (Comp1 s) = Comp1 (rename1 (rename1 f) s)
  supp1 f (Comp1 s) = supp1 (supp1 f) s
  supply1 f (Comp1 s) = supply1 (supply1 f) s

instance (Supported1 f, Supported1 g) => Supported1 (f :+: g) where
  rename1 f n (L1 s) = L1 (rename1 f n s)
  rename1 f n (R1 t) = R1 (rename1 f n t)
  supp1 f (L1 s) = supp1 f s
  supp1 f (R1 s) = supp1 f s
  supply1 f (L1 s) = supply1 f s
  supply1 f (R1 s) = supply1 f s

instance Supported1 []
instance Supported1 Maybe
instance Supported a => Supported1 ((,) a)
instance Supported a => Supported1 (Either a)

class GSupported f where
  grename :: Renaming -> f a -> f a
  gsupp :: f a -> Support
  gsupply :: f a -> Supply

instance GSupported U1 where
  grename _ U1 = U1
  gsupp = mempty
  gsupply = mempty

instance GSupported V1 where
  grename _ = \case
  gsupp = \case
  gsupply = \case

instance Supported c => GSupported (K1 i c) where
  grename n (K1 m) = K1 (rename n m)
  gsupp (K1 m) = supp m
  gsupply (K1 m) = supply m

instance GSupported f => GSupported (M1 i c f) where
  grename n (M1 m) = M1 (grename n m)
  gsupp (M1 m) = gsupp m
  gsupply (M1 m) = gsupply m

instance (GSupported f, GSupported g) => GSupported (f :*: g) where
  grename n (s :*: t) = grename n s :*: grename n t
  gsupp (s :*: t) = gsupp s <> gsupp t
  gsupply (s :*: t) = gsupply s <> gsupply t

instance (Supported1 f, GSupported g) => GSupported (f :.: g) where
  grename n (Comp1 s) = Comp1 (rename1 grename s)
  gsupp (Comp1 s) = supp1 gsupp s
  gsupply (Comp1 s) = supply1 gsupply s

instance (GSupported f, GSupported g) => GSupported (f :+: g) where
  grename n (L1 s) = L1 (grename n s)
  grename n (R1 t) = L1 (grename n t)
  gsupp (L1 s) = gsupp s
  gsupp (R1 t) = gsupp t
  gsupply (L1 s) = gsupply s
  gsupply (R1 t) = gsupply t

($$) :: Ren a b -> a -> b
($$) (Ren _ f) = f

-- unsafely construct an arrow in ren from an arrow in Hask with empty support
ren_ :: (a -> b) -> Ren a b
ren_ = Ren mempty

-- | @
-- f $$ rename s a = rename s (f $$ a)

data Ren a b = Ren Support (a -> b)
instance Category Ren where
  id = Ren mempty id
  Ren s f . Ren t g = Ren (s <> t) (f . g)

-- TODO: fuse rename and Supported together, there is no benefit of separation here unlike in nominal sets
class Rename a => Supported a where

instance Supported Renaming where
  supp (Renaming n) = supp n -- TODO: this needs both sets of keys
  supply (Renaming n) = supply n

instance Supported (Store f) where
  supp = Supp
  supply (Sketch m) = Supply $ ffmap sup m

instance Supported Support where supp = id; supply (Support m) = supply m
instance Supported Char
instance Supported Int
instance Supported a => Supported [a]
instance Supported a => Supported (Maybe a)

instance (Rename a, Supported b) => Rename (Ren a b) where -- we use Gabbay's partial definition extension method
  rename r (Ren s f) = Ren (rename r s) $ \a -> 
    let (h, (_, y)) = runState (walk (supp a) $ \n -> do n' <- zoom _1 (refresh n); n' <$ (_2.store n' .= n)) (supply (r,s,a),mempty)
    in rename (Renaming y) $ f $ rename (Renaming h) a
  -- is it worth mangling 'r' into a field of Ren, rather than doing this repeatedly? this complicates the category, but may be worth it
  
-- TODO: the support of a substitution needs to include the stuff in the terms it binds to
newtype Substitution = Substitution { getSubstitition :: Store Identity }
-- TODO: Semigroup Substitution, Monoid Substitution
instance Monoid Substitution where mempty = Substitution mempty
substgen :: (Generic a, GSubst (Rep a)) => Substitution -> a -> a
substgen m = to . gsubst m . from

class Subst a where
  subst :: Substitution -> a -> a
  default :: (Generic a, GSubst (Rep a)) => Substitution -> a -> a
  subst = substgen
instance Subst () where subst _ = id
instance Subst Char where subst _ = id
instance Subst Int where subst _ = id
instance Subst Void where subst _ = absurd
instance Subst a => Subst [a]
instance Subst a => Subst (Maybe a)
instance (Subst a, Subst b) => Subst (a, b)
instance (Subst a, Subst b) => Subst (Either a b)
  
class Subst1 f where subst1 :: (Substitution -> a -> a) -> Substitution -> f a -> f a
instance Subst1 U1 where subst1 _ _ U1 = U1
instance Subst1 V1 where subst1 _ _ = \case
instance Subst c => Subst1 (K1 i c) where subst1 _ n (K1 m) = K1 (subst n m)
instance Subst1 f => Subst1 (M1 i c f) where subst1 f n (M1 s) = M1 (subst1 f n s)
instance Subst1 Par1 where subst1 f n (Par1 a) = Par1 (f n a)
instance Subst1 f => Subst1 (Rec1 f) where subst1 f n (Rec1 a) = Rec1 (subst1 f n a)
instance (Subst1 f, Subst1 g) => Subst1 (f :*: g) where subst1 f n (s :*: t) = subst1 f n s :*: subst1 f n t
instance (Subst1 f, Subst1 g) => Subst1 (f :.: g) where subst1 f n (Comp1 s) = Comp1 (subst1 (subst1 f) s)
instance (Subst1 f, Subst1 g) => Subst1 (f :+: g) where
  subst1 f n (L1 s) = L1 (subst1 f n s)
  subst1 f n (R1 t) = R1 (subst1 f n t)
instance Subst1 []
instance Subst1 Maybe
instance Subst a => Subst1 ((,) a)
instance Subst a => Subst1 (Either a)

class GSubst f where gsubst :: Substitution -> f a -> f a
instance GSubst U1 where gsubst _ U1 = U1
instance GSubst V1 where gsubst _ = \case
instance Subst c => GSubst (K1 i c) where gsubst n (K1 m) = K1 (subst n m)
instance GSubst f => GSubst (M1 i c f) where gsubst n (M1 m) = M1 (gsubst n m)
instance (GSubst f, GSubst g) => GSubst (f :*: g) where gsubst n (s :*: t) = gsubst n s :*: gsubst n t
instance (Subst1 f, GSubst g) => GSubst (f :.: g) where gsubst n (Comp1 s) = Comp1 (subst1 gsubst s)
instance (GSubst f, GSubst g) => GSubst (f :+: g) where
  gsubst n (L1 s) = L1 (gsubst n s)
  gsubst n (R1 t) = L1 (gsubst n t)

class AsName t where
  _Name :: Prism' t (Name t)

-- use for type, term, kind, etc.
substExp :: AsName a => Subst a
substExp s@(Substitution m) t = case t^?_Name of
  Just v -> maybe t (review _Name) $ m^?store v
  Nothing -> substgen s t

newtype Ap f a = Ap { getAp :: f a }
instance (Applicative f, Semigroup a) => Semigroup (Ap f a) where (<>) = liftA2 (<>)
instance (Applicative f, Monoid a) => Monoid (Ap f a) where mempty = pure mempty

newtype Binder a = Binder { getBinder :: a -> a -> Maybe Renaming }
instance Contravariant Binder where contramap f (Binder g) = Binder $ \a b -> g (f a) (g b)

instance Divisible Binder where
  conquer = Binder $ \ _ _ -> Just mempty
  divide f (Binder g) (Binder h) = Binder $ \a a' -> case f a of
    (b, c) -> case f a' of
      (b', c') -> liftA2 (g b b') (h c c')

instance Decidable Binder where
  lose f = Binder $ absurd . f
  choose f (Binder g) (Binder h) = Binder $ \a a' -> case f a of
    Left b  -> g b ||| const Nothing $ f a'
    Right c -> const Nothing ||| h c $ f a'
  
-- TODO: define directly rather than through divisible/decidable? This gives a better supply of Binding_'s and GBinding1s
class Supported a => Binding a where
  binding :: a -> a -> Maybe Renaming -- this is _directional_ and turns b into a, if it succeeds, for biimplication, simply use this twice.
  default binding :: Deriving Binding a => a -> a -> Maybe Renaming
  binding = getBinder $ deciding (Proxy :: Proxy Binding) (Binder binding)

  bv :: a -> Support
  default bv :: Deriving Binding a => a -> Support
  bv = getOp $ deciding (Proxy :: Proxy Binding) (Op bv)

instance Binding (Proxy a) where binding = binding_; bv = bv_
instance Binding (Name a) where binding = binding_; bv = bv_
instance Binding Char where binding a b = mempty <$ guard (a == b); bv = mempty
instance Binding Int where binding a b = mempty <$ guard (a == b) bv = mempty
instance Binding () where binding a b = Just mempty; bv = mempty
instance Binding Void where binding = absurd; bv = absurd

-- GBinding?
class Supported_ f => Binding_ f where
  binding_ :: f a -> f a -> Maybe Renaming -- this is _directional_ and turns b into a, if it succeeds, for biimplication, simply use this twice.
  bv_ :: f a -> Support

instance Binding_ Proxy where binding_ _ _ = Just mempty; bv_ = mempty
instance Binding_ Name where binding_ a b = Just $ a ↦ b; bv_ = single

-- GBinding1
class Supported1 f => Binding1 f where
  binding1 :: (a -> a -> Maybe Renaming) -> f a -> f a -> Maybe Renaming
  default binding1 :: Deriving1 Binding f => (a -> a -> Maybe Renaming) -> f a -> f a -> Maybe Renaming
  binding1 f = getBinder $ deciding1 (Proxy :: Proxy Binding) (Binder f) (Binder binding)
  bv1 :: (a -> Support) -> f a -> Support
  default bv1 :: Deriving Binding a => (a -> Support) -> f a -> Support
  bv1 f = getOp $ deciding1 (Proxy :: Proxy Binding) (Op f) (Op bv)

instance Binding1 Proxy where binding1 _ = binding_; bv1 _ = bv_
instance Binding1 Name where binding1 _ = binding_ bv1 _ = bv_
instance Binding1 []
instance Binding1 Maybe
instance Binding a => Binding1 (Either a)
instance Binding a => Binding1 ((,) a)

data Tie a b = Tie a b deriving Show

instance (Binding a, Supported b) => Eq (Tie a b) where 
  Tie a as == Tie b bs
    | a == b = as == bs
    | otherwise = case binding a b *> binding b a of
      Nothing -> False
      Just p -> disjoint (supp bs) (bv a \\ bv b) && as == rename p bs

(\\) :: Support -> Support -> Support
(\\) = error "TODO"
disjoint :: Support -> Support -> Bool
disjoint = error "TODO"

instance (Binding a, Supported b) => Rename (Tie a b) where
  rename r (Tie a b) = Tie (rename r' a) (rename r' b) where
    r' = r <> evalState (walk (bv a) refresh) (supply (r,a,b))

instance (Binding a, Supported b) => Supported (Tie a b) where
  supp (Tie a b) = supp (a, b) \\ bv a
  supply (Tie a b) = supply (a, b)

instance (Binding a, Subst b) => Subst (Tie a b) where
  subst s (Tie a b) = Tie (subst s (rename r a)) (subst s (rename r b)) where
    r = evalState (walk (bv a) refresh) (supply (s,a,b))

type Con = String

data Pat
  = PWild
  | PVar (Name Term)
  | PCon Con [Pat]
  | PLit Int
  deriving (Show, Eq, Generic, Rename, Supported, Binding)

data Sig a b = a ::: b deriving (Show, Eq, Generic, Generic1, Rename, Rename1, Supported, Supported1, Subst)

instance (Binding a, Nominal b, Eq b) => Binding (Sig a b) where
  binding (a ::: b) (c ::: d) | b == d = binding a c
  binding _ _ = Nothing
  bv (a ::: b) = bv a

data Kind
  = KVar (Name Kind)
  | KType
  | KHole
  | KArr Kind Kind
  deriving (Show, Eq, Generic, Rename, Supported)

instance Subst Kind where subst = substExp
instance AsName Kind where
  _Name = prism KVar $ \case
    KVar v -> Right v
    x -> Left x

data Type
  = TVar (Name Type)
  | TInt
  | TArr Type Type
  | TCon Con [Type]
  | THole
  | TForall (Sig (Name Type) Kind ⊸ Type)
  deriving (Show, Eq, Generic, Rename, Supported)

instance Subst Type where subst = substExp
instance AsName Type where
  _Name = prism TVar $ \case
    TVar v -> Right v
    x -> Left x

data Term
  = Var (Name Term)
  | App Term Term
  | Lam (Pat ⊸ Term)
  | Let (Sig (Name Term) Type ⊸ Term) Term
  | Case Term [Pat ⊸ Term]
  deriving (Show, Eq, Generic, Rename, Supported)


instance Subst Term where subst = substExp
instance AsName Term where
  _Name = prism Var $ \case
    Var v -> Right v
    x -> Left x