{-# language DataKinds             #-}
{-# language DerivingVia           #-}
{-# language FlexibleInstances     #-}
{-# language GADTs                 #-}
{-# language MultiParamTypeClasses #-}
{-# language QuantifiedConstraints #-}
{-# language ScopedTypeVariables   #-}
{-# language StandaloneDeriving    #-}
{-# language TemplateHaskell       #-}
{-# language TypeApplications      #-}
{-# language TypeFamilies          #-}
{-# language TypeOperators         #-}
-- | Example of how to use `unbound-kind-generics`
module Unbound.Generics.LocallyNameless.Kind.Example where

import           Data.Typeable                                (Typeable)
import           Generics.Kind.TH
import           Unbound.Generics.LocallyNameless
import           Unbound.Generics.LocallyNameless.Kind.Derive

-- | Variables stand for expressions
type Var t = Name (Expr t)

-- | Well-typed lambda expressions
data Expr t where
  V   :: Var t -> Expr t
  Lam :: (Typeable a, Typeable b) => Bind (Var a) (Expr b) -> Expr (a -> b)
  App :: (Typeable a) => Expr (a -> b) -> Expr a -> Expr b

$(deriveGenericK ''Expr)

eval :: Typeable t => Expr t -> FreshM (Expr t)
eval :: forall t. Typeable t => Expr t -> FreshM (Expr t)
eval (V Var t
x) = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"unbound variable " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Var t
x
eval e :: Expr t
e@Lam {} = forall (m :: * -> *) a. Monad m => a -> m a
return Expr t
e
eval (App Expr (a -> t)
e1 Expr a
e2) = do
  Expr (a -> t)
v1 <- forall t. Typeable t => Expr t -> FreshM (Expr t)
eval Expr (a -> t)
e1
  Expr a
v2 <- forall t. Typeable t => Expr t -> FreshM (Expr t)
eval Expr a
e2
  case Expr (a -> t)
v1 of
   (Lam Bind (Var a) (Expr b)
bnd) -> do
     -- open the lambda by picking a fresh name for the bound variable x in body
     (Var a
x, Expr b
body) <- forall p t (m :: * -> *).
(Alpha p, Alpha t, Fresh m) =>
Bind p t -> m (p, t)
unbind Bind (Var a) (Expr b)
bnd
     let body' :: Expr b
body' = forall b a. Subst b a => Name b -> b -> a -> a
subst Var a
x Expr a
v2 Expr b
body
     forall t. Typeable t => Expr t -> FreshM (Expr t)
eval Expr b
body'
   Expr (a -> t)
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"application of non-lambda"

example :: forall a. Typeable a => Expr (a -> a)
example :: forall a. Typeable a => Expr (a -> a)
example =
  let x :: Name a
x = forall a. [Char] -> Name a
s2n [Char]
"x"
      y :: Name a
y = forall a. [Char] -> Name a
s2n [Char]
"y"
      e1 :: Expr ((a -> a) -> (a -> a) -> a -> a)
e1 = forall a b.
(Typeable a, Typeable b) =>
Bind (Var a) (Expr b) -> Expr (a -> b)
Lam @(a -> a) forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind forall {a}. Name a
x (forall a b.
(Typeable a, Typeable b) =>
Bind (Var a) (Expr b) -> Expr (a -> b)
Lam @(a -> a) forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind forall {a}. Name a
y (forall t. Var t -> Expr t
V forall {a}. Name a
x)) -- \x y -> x
      z :: Name a
z = forall a. [Char] -> Name a
s2n [Char]
"z"
      e2 :: Expr (a -> a)
e2 = forall a b.
(Typeable a, Typeable b) =>
Bind (Var a) (Expr b) -> Expr (a -> b)
Lam @a forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind forall {a}. Name a
z (forall t. Var t -> Expr t
V forall {a}. Name a
z) -- \z -> z
  in forall a. FreshM a -> a
runFreshM forall a b. (a -> b) -> a -> b
$ forall t. Typeable t => Expr t -> FreshM (Expr t)
eval (forall a b. Typeable a => Expr (a -> b) -> Expr a -> Expr b
App (forall a b. Typeable a => Expr (a -> b) -> Expr a -> Expr b
App Expr ((a -> a) -> (a -> a) -> a -> a)
e1 Expr (a -> a)
e2) Expr (a -> a)
e2)

deriving instance Show (Expr t)

{-
instance GenericK (Expr t) LoT0 where
  type RepK (Expr t) =
    ((Field (Kon (Name (Expr t)))))
    :+:
    (Exists Type {- Var1 = a -} ((Typeable :$: Var0) :=>:
      (Exists Type {- Var0 = b -} ((Typeable :$: Var0) :=>:
        (((Kon t) :~: ((->) :$: Var1 :@: Var0))
         :=>:
         (Field (Bind :$: (Name :$: (Expr :$: Var1)) :@: (Expr :$: Var0)))) ))))
    :+:
    (Exists Type {- Var0 = a -} (
      (Typeable :$: Var0)
      :=>:
      ((Field (Expr :$: ((->) :$: Var0 :@: (Kon t)))) :*: Field (Expr :$: Var0)) ))

  fromK (V   v)   = L1 (Field v)
  fromK (Lam b)   = R1 (L1 (Exists (SuchThat (Exists (SuchThat (SuchThat (Field b)))))))
  fromK (App x y) = R1 (R1 (Exists (SuchThat (Field x :*: Field y))))

  toK (L1 (Field v)) = V v
  toK (R1 (L1 (Exists (SuchThat (Exists (SuchThat (SuchThat (Field b)))))))) = Lam b
  toK (R1 (R1 (Exists (SuchThat (Field x :*: Field y))))) = App x y
-}

instance Typeable t => Alpha (Expr t) where
  aeq' :: AlphaCtx -> Expr t -> Expr t -> Bool
aeq'        = forall a. GenericAlpha a => AlphaCtx -> a -> a -> Bool
aeqDefK
  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Expr t -> f (Expr t)
fvAny'      = forall (g :: * -> *) a.
(GenericAlpha a, Contravariant g, Applicative g) =>
AlphaCtx -> (AnyName -> g AnyName) -> a -> g a
fvAnyDefK
  close :: AlphaCtx -> NamePatFind -> Expr t -> Expr t
close       = forall a. GenericAlpha a => AlphaCtx -> NamePatFind -> a -> a
closeDefK
  open :: AlphaCtx -> NthPatFind -> Expr t -> Expr t
open        = forall a. GenericAlpha a => AlphaCtx -> NthPatFind -> a -> a
openDefK
  isPat :: Expr t -> DisjointSet AnyName
isPat       = forall a. GenericAlpha a => a -> DisjointSet AnyName
isPatDefK
  isTerm :: Expr t -> All
isTerm      = forall a. GenericAlpha a => a -> All
isTermDefK
  isEmbed :: Expr t -> Bool
isEmbed     = forall a. a -> Bool
isEmbedDefK
  nthPatFind :: Expr t -> NthPatFind
nthPatFind  = forall a. GenericAlpha a => a -> NthPatFind
nthPatFindDefK
  namePatFind :: Expr t -> NamePatFind
namePatFind = forall a. GenericAlpha a => a -> NamePatFind
namePatFindDefK
  swaps' :: AlphaCtx -> Perm AnyName -> Expr t -> Expr t
swaps'      = forall a. GenericAlpha a => AlphaCtx -> Perm AnyName -> a -> a
swapsDefK
  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Expr t -> (Expr t -> Perm AnyName -> m b) -> m b
lfreshen'   = forall (m :: * -> *) a b.
(LFresh m, GenericAlpha a) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
lfreshenDefK
  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Expr t -> m (Expr t, Perm AnyName)
freshen'    = forall (m :: * -> *) a.
(Fresh m, GenericAlpha a) =>
AlphaCtx -> a -> m (a, Perm AnyName)
freshenDefK
  acompare' :: AlphaCtx -> Expr t -> Expr t -> Ordering
acompare'   = forall a. GenericAlpha a => AlphaCtx -> a -> a -> Ordering
acompareDefK
-- deriving via (AutoAlpha (Expr t)) instance Typeable t => Alpha (Expr t)

instance (Typeable small, Typeable big)
         => Subst (Expr small) (Expr big) where
  isvar :: Expr big -> Maybe (SubstName (Expr big) (Expr small))
isvar (V Var big
x) = forall a b.
(Typeable a, Typeable b) =>
Name a -> Maybe (SubstName a b)
buildSubstName Var big
x
  isvar Expr big
_     = forall a. Maybe a
Nothing
  subst :: Name (Expr small) -> Expr small -> Expr big -> Expr big
subst  = forall a b.
(GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) =>
Name b -> b -> a -> a
gsubstDefK
  substs :: [(Name (Expr small), Expr small)] -> Expr big -> Expr big
substs = forall a b.
(GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) =>
[(Name b, b)] -> a -> a
gsubstsDefK
  substBvs :: AlphaCtx -> [Expr small] -> Expr big -> Expr big
substBvs = forall a b.
(GenericK a, GSubstK b (RepK a) 'LoT0, Subst b a) =>
AlphaCtx -> [b] -> a -> a
gsubstBvsDefK