{-# OPTIONS_HADDOCK show-extensions #-}
-- |
-- Module     : Unbound.Generics.LocallyNameless.Rebind
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- The pattern @'Rebind' p1 p2@ binds the names in @p1@ and @p2@ just as @(p1, p2)@ would,
-- however it additionally also brings the names of @p1@ into scope in @p2@.
--
{-# LANGUAGE DeriveGeneric #-}
module Unbound.Generics.LocallyNameless.Rebind where

import Control.Applicative ((<*>), (<$>))
import Control.DeepSeq (NFData(..))
import Data.Monoid ((<>), All(..))
import GHC.Generics

import Unbound.Generics.LocallyNameless.Alpha


-- | @'Rebind' p1 p2@ is a pattern that binds the names of @p1@ and @p2@, and additionally
-- brings the names of @p1@ into scope over @p2@.
--
-- This may be used, for example, to faithfully represent Scheme's @let*@ binding form, defined by:
-- 
-- >  (let* () body) ≙ body
-- >  (let* ([v1, e1] binds ...) body) ≙ (let ([v1, e1]) (let* (binds ...) body))
-- 
-- using the following AST:
--
-- @
-- type Var = Name Expr
-- data Lets = EmptyLs
--           | ConsLs (Rebind (Var, Embed Expr) Lets)
-- data Expr = ...
--           | LetStar (Bind Lets Expr)
--           | ...
-- @
data Rebind p1 p2 = Rebnd p1 p2
                  deriving ((forall x. Rebind p1 p2 -> Rep (Rebind p1 p2) x)
-> (forall x. Rep (Rebind p1 p2) x -> Rebind p1 p2)
-> Generic (Rebind p1 p2)
forall x. Rep (Rebind p1 p2) x -> Rebind p1 p2
forall x. Rebind p1 p2 -> Rep (Rebind p1 p2) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p1 p2 x. Rep (Rebind p1 p2) x -> Rebind p1 p2
forall p1 p2 x. Rebind p1 p2 -> Rep (Rebind p1 p2) x
$cfrom :: forall p1 p2 x. Rebind p1 p2 -> Rep (Rebind p1 p2) x
from :: forall x. Rebind p1 p2 -> Rep (Rebind p1 p2) x
$cto :: forall p1 p2 x. Rep (Rebind p1 p2) x -> Rebind p1 p2
to :: forall x. Rep (Rebind p1 p2) x -> Rebind p1 p2
Generic, Rebind p1 p2 -> Rebind p1 p2 -> Bool
(Rebind p1 p2 -> Rebind p1 p2 -> Bool)
-> (Rebind p1 p2 -> Rebind p1 p2 -> Bool) -> Eq (Rebind p1 p2)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall p1 p2.
(Eq p1, Eq p2) =>
Rebind p1 p2 -> Rebind p1 p2 -> Bool
$c== :: forall p1 p2.
(Eq p1, Eq p2) =>
Rebind p1 p2 -> Rebind p1 p2 -> Bool
== :: Rebind p1 p2 -> Rebind p1 p2 -> Bool
$c/= :: forall p1 p2.
(Eq p1, Eq p2) =>
Rebind p1 p2 -> Rebind p1 p2 -> Bool
/= :: Rebind p1 p2 -> Rebind p1 p2 -> Bool
Eq)

instance (NFData p1, NFData p2) => NFData (Rebind p1 p2) where
  rnf :: Rebind p1 p2 -> ()
rnf (Rebnd p1
p1 p2
p2) = p1 -> ()
forall a. NFData a => a -> ()
rnf p1
p1 () -> () -> ()
forall a b. a -> b -> b
`seq` p2 -> ()
forall a. NFData a => a -> ()
rnf p2
p2 () -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance (Show p1, Show p2) => Show (Rebind p1 p2) where
  showsPrec :: Int -> Rebind p1 p2 -> ShowS
showsPrec Int
paren (Rebnd p1
p1 p2
p2) =
    Bool -> ShowS -> ShowS
showParen (Int
paren Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (String -> ShowS
showString String
"<<"
                           ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> p1 -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
paren p1
p1
                           ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
">> "
                           ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> p2 -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 p2
p2)

instance (Alpha p1, Alpha p2) => Alpha (Rebind p1 p2) where
  isTerm :: Rebind p1 p2 -> All
isTerm Rebind p1 p2
_ = Bool -> All
All Bool
False

  isPat :: Rebind p1 p2 -> DisjointSet AnyName
isPat (Rebnd p1
p1 p2
p2) = p1 -> DisjointSet AnyName
forall a. Alpha a => a -> DisjointSet AnyName
isPat p1
p1 DisjointSet AnyName -> DisjointSet AnyName -> DisjointSet AnyName
forall a. Semigroup a => a -> a -> a
<> p2 -> DisjointSet AnyName
forall a. Alpha a => a -> DisjointSet AnyName
isPat p2
p2

  swaps' :: AlphaCtx -> Perm AnyName -> Rebind p1 p2 -> Rebind p1 p2
swaps' AlphaCtx
ctx Perm AnyName
perm (Rebnd p1
p1 p2
p2) =
    p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd (AlphaCtx -> Perm AnyName -> p1 -> p1
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' AlphaCtx
ctx Perm AnyName
perm p1
p1) (AlphaCtx -> Perm AnyName -> p2 -> p2
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) Perm AnyName
perm p2
p2)

  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Rebind p1 p2 -> m (Rebind p1 p2, Perm AnyName)
freshen' AlphaCtx
ctx (Rebnd p1
p1 p2
p2) =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> m (Rebind p1 p2, Perm AnyName)
forall a. HasCallStack => String -> a
error String
"freshen' on Rebind in Term mode"
    else do
      (p1
p1', Perm AnyName
perm1) <- AlphaCtx -> p1 -> m (p1, Perm AnyName)
forall a (m :: * -> *).
(Alpha a, Fresh m) =>
AlphaCtx -> a -> m (a, Perm AnyName)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> p1 -> m (p1, Perm AnyName)
freshen' AlphaCtx
ctx p1
p1
      (p2
p2', Perm AnyName
perm2) <- AlphaCtx -> p2 -> m (p2, Perm AnyName)
forall a (m :: * -> *).
(Alpha a, Fresh m) =>
AlphaCtx -> a -> m (a, Perm AnyName)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> p2 -> m (p2, Perm AnyName)
freshen' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) (AlphaCtx -> Perm AnyName -> p2 -> p2
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) Perm AnyName
perm1 p2
p2)
      (Rebind p1 p2, Perm AnyName) -> m (Rebind p1 p2, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd p1
p1' p2
p2', Perm AnyName
perm1 Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
perm2)

  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx
-> Rebind p1 p2 -> (Rebind p1 p2 -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx (Rebnd p1
p p2
q) Rebind p1 p2 -> Perm AnyName -> m b
cont =
    if AlphaCtx -> Bool
isTermCtx AlphaCtx
ctx
    then String -> m b
forall a. HasCallStack => String -> a
error String
"lfreshen' on Rebind in Term mode"
    else
      AlphaCtx -> p1 -> (p1 -> Perm AnyName -> m b) -> m b
forall a (m :: * -> *) b.
(Alpha a, LFresh m) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> p1 -> (p1 -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx p1
p ((p1 -> Perm AnyName -> m b) -> m b)
-> (p1 -> Perm AnyName -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \ p1
p' Perm AnyName
pm1 ->
      AlphaCtx -> p2 -> (p2 -> Perm AnyName -> m b) -> m b
forall a (m :: * -> *) b.
(Alpha a, LFresh m) =>
AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> p2 -> (p2 -> Perm AnyName -> m b) -> m b
lfreshen' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) (AlphaCtx -> Perm AnyName -> p2 -> p2
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) Perm AnyName
pm1 p2
q) ((p2 -> Perm AnyName -> m b) -> m b)
-> (p2 -> Perm AnyName -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \ p2
q' Perm AnyName
pm2 ->
      Rebind p1 p2 -> Perm AnyName -> m b
cont (p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd p1
p' p2
q') (Perm AnyName
pm1 Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
pm2)


  aeq' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Bool
aeq' AlphaCtx
ctx (Rebnd p1
p1 p2
p2) (Rebnd p1
q1 p2
q2) =
    -- XXX TODO: Unbound had (aeq' ctx p2 q2) here.  But that doesn't seem right.
    AlphaCtx -> p1 -> p1 -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' AlphaCtx
ctx p1
p1 p1
q1 Bool -> Bool -> Bool
&& AlphaCtx -> p2 -> p2 -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) p2
p2 p2
q2

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx
-> (AnyName -> f AnyName) -> Rebind p1 p2 -> f (Rebind p1 p2)
fvAny' AlphaCtx
ctx AnyName -> f AnyName
afa (Rebnd p1
p1 p2
p2) = p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd (p1 -> p2 -> Rebind p1 p2) -> f p1 -> f (p2 -> Rebind p1 p2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AlphaCtx -> (AnyName -> f AnyName) -> p1 -> f p1
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> p1 -> f p1
fvAny' AlphaCtx
ctx AnyName -> f AnyName
afa p1
p1
                                       f (p2 -> Rebind p1 p2) -> f p2 -> f (Rebind p1 p2)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> AlphaCtx -> (AnyName -> f AnyName) -> p2 -> f p2
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> a -> f a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> p2 -> f p2
fvAny' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) AnyName -> f AnyName
afa p2
p2

  open :: AlphaCtx -> NthPatFind -> Rebind p1 p2 -> Rebind p1 p2
open AlphaCtx
ctx NthPatFind
b (Rebnd p1
p1 p2
p2) = p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd (AlphaCtx -> NthPatFind -> p1 -> p1
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open AlphaCtx
ctx NthPatFind
b p1
p1) (AlphaCtx -> NthPatFind -> p2 -> p2
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) NthPatFind
b p2
p2)
  close :: AlphaCtx -> NamePatFind -> Rebind p1 p2 -> Rebind p1 p2
close AlphaCtx
ctx NamePatFind
b (Rebnd p1
p1 p2
p2) = p1 -> p2 -> Rebind p1 p2
forall p1 p2. p1 -> p2 -> Rebind p1 p2
Rebnd (AlphaCtx -> NamePatFind -> p1 -> p1
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close AlphaCtx
ctx NamePatFind
b p1
p1) (AlphaCtx -> NamePatFind -> p2 -> p2
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) NamePatFind
b p2
p2)

  acompare' :: AlphaCtx -> Rebind p1 p2 -> Rebind p1 p2 -> Ordering
acompare' AlphaCtx
ctx (Rebnd p1
p1 p2
p2) (Rebnd p1
q1 p2
q2) =
    AlphaCtx -> p1 -> p1 -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' AlphaCtx
ctx p1
p1 p1
q1 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> AlphaCtx -> p2 -> p2 -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) p2
p2 p2
q2