{-# OPTIONS_HADDOCK show-extensions #-}
-- |
-- Module     : Unbound.Generics.LocallyNameless.Bind
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- The fundamental binding form.  The type @'Bind' p t@ allows you to
-- place a pattern @p@ in a term @t@ such that the names in the
-- pattern scope over the term.  Use 'Unbound.Generics.LocallyNameless.Operations.bind'
-- and 'Unbound.Generics.LocallyNameless.Operations.unbind' and 'Unbound.Generics.LocallyNameless.Operations.lunbind'
-- to work with @'Bind' p t@
{-# LANGUAGE DeriveGeneric #-}
module Unbound.Generics.LocallyNameless.Bind (
  -- * Name binding
  Bind(..)
  ) where

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

import GHC.Generics (Generic)

import Unbound.Generics.LocallyNameless.Alpha

-- | A term of type @'Bind' p t@ is a term that binds the free
-- variable occurrences of the variables in pattern @p@ in the term
-- @t@.  In the overall term, those variables are now bound. See also
-- 'Unbound.Generics.LocallyNameless.Operations.bind' and
-- 'Unbound.Generics.LocallyNameless.Operations.unbind' and
-- 'Unbound.Generics.LocallyNameless.Operations.lunbind'
data Bind p t = B p t
              deriving ((forall x. Bind p t -> Rep (Bind p t) x)
-> (forall x. Rep (Bind p t) x -> Bind p t) -> Generic (Bind p t)
forall x. Rep (Bind p t) x -> Bind p t
forall x. Bind p t -> Rep (Bind p t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall p t x. Rep (Bind p t) x -> Bind p t
forall p t x. Bind p t -> Rep (Bind p t) x
$cfrom :: forall p t x. Bind p t -> Rep (Bind p t) x
from :: forall x. Bind p t -> Rep (Bind p t) x
$cto :: forall p t x. Rep (Bind p t) x -> Bind p t
to :: forall x. Rep (Bind p t) x -> Bind p t
Generic)

instance (NFData p, NFData t) => NFData (Bind p t) where
  rnf :: Bind p t -> ()
rnf (B p
p t
t) = p -> ()
forall a. NFData a => a -> ()
rnf p
p () -> () -> ()
forall a b. a -> b -> b
`seq` t -> ()
forall a. NFData a => a -> ()
rnf t
t () -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance (Show p, Show t) => Show (Bind p t) where
  showsPrec :: Int -> Bind p t -> ShowS
showsPrec Int
prec (B p
p t
t) =
    Bool -> ShowS -> ShowS
showParen (Int
prec 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 -> p -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
prec p
p
                          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 -> t -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 t
t)

instance (Alpha p, Alpha t) => Alpha (Bind p t) where

  aeq' :: AlphaCtx -> Bind p t -> Bind p t -> Bool
aeq' AlphaCtx
ctx (B p
p1 t
t1) (B p
p2 t
t2) =
    AlphaCtx -> p -> p -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) p
p1 p
p2
    Bool -> Bool -> Bool
&& AlphaCtx -> t -> t -> Bool
forall a. Alpha a => AlphaCtx -> a -> a -> Bool
aeq' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) t
t1 t
t2

  fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Bind p t -> f (Bind p t)
fvAny' AlphaCtx
ctx AnyName -> f AnyName
nfn (B p
p t
t) = p -> t -> Bind p t
forall p t. p -> t -> Bind p t
B (p -> t -> Bind p t) -> f p -> f (t -> Bind p t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AlphaCtx -> (AnyName -> f AnyName) -> p -> f p
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) -> p -> f p
fvAny' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) AnyName -> f AnyName
nfn p
p
                             f (t -> Bind p t) -> f t -> f (Bind p t)
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) -> t -> f t
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) -> t -> f t
fvAny' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) AnyName -> f AnyName
nfn t
t

  isPat :: Bind p t -> DisjointSet AnyName
isPat Bind p t
_ = DisjointSet AnyName
forall a. DisjointSet a
inconsistentDisjointSet

  isTerm :: Bind p t -> All
isTerm (B p
p t
t) = (Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ DisjointSet AnyName -> Bool
forall a. DisjointSet a -> Bool
isConsistentDisjointSet (DisjointSet AnyName -> Bool) -> DisjointSet AnyName -> Bool
forall a b. (a -> b) -> a -> b
$ p -> DisjointSet AnyName
forall a. Alpha a => a -> DisjointSet AnyName
isPat p
p) All -> All -> All
forall a. Semigroup a => a -> a -> a
<> t -> All
forall a. Alpha a => a -> All
isTerm t
t

  close :: AlphaCtx -> NamePatFind -> Bind p t -> Bind p t
close AlphaCtx
ctx NamePatFind
b (B p
p t
t) =
    p -> t -> Bind p t
forall p t. p -> t -> Bind p t
B (AlphaCtx -> NamePatFind -> p -> p
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) NamePatFind
b p
p) (AlphaCtx -> NamePatFind -> t -> t
forall a. Alpha a => AlphaCtx -> NamePatFind -> a -> a
close (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) NamePatFind
b t
t)

  open :: AlphaCtx -> NthPatFind -> Bind p t -> Bind p t
open AlphaCtx
ctx NthPatFind
b (B p
p t
t) =
    p -> t -> Bind p t
forall p t. p -> t -> Bind p t
B (AlphaCtx -> NthPatFind -> p -> p
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) NthPatFind
b p
p) (AlphaCtx -> NthPatFind -> t -> t
forall a. Alpha a => AlphaCtx -> NthPatFind -> a -> a
open (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) NthPatFind
b t
t)

  nthPatFind :: Bind p t -> NthPatFind
nthPatFind Bind p t
b = String -> NthPatFind
forall a. HasCallStack => String -> a
error (String -> NthPatFind) -> String -> NthPatFind
forall a b. (a -> b) -> a -> b
$ String
"Binding " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bind p t -> String
forall a. Show a => a -> String
show Bind p t
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" used as a pattern"
  namePatFind :: Bind p t -> NamePatFind
namePatFind Bind p t
b = String -> NamePatFind
forall a. HasCallStack => String -> a
error (String -> NamePatFind) -> String -> NamePatFind
forall a b. (a -> b) -> a -> b
$ String
"Binding " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bind p t -> String
forall a. Show a => a -> String
show Bind p t
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" used as a pattern"

  swaps' :: AlphaCtx -> Perm AnyName -> Bind p t -> Bind p t
swaps' AlphaCtx
ctx Perm AnyName
perm (B p
p t
t) =
    p -> t -> Bind p t
forall p t. p -> t -> Bind p t
B (AlphaCtx -> Perm AnyName -> p -> p
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) Perm AnyName
perm p
p)
      (AlphaCtx -> Perm AnyName -> t -> t
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) Perm AnyName
perm t
t)

  freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Bind p t -> m (Bind p t, Perm AnyName)
freshen' AlphaCtx
ctx (B p
p t
t) = do
    (p
p', Perm AnyName
perm1) <- AlphaCtx -> p -> m (p, Perm AnyName)
forall a (m :: * -> *).
(Alpha a, Fresh m) =>
AlphaCtx -> a -> m (a, Perm AnyName)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> p -> m (p, Perm AnyName)
freshen' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) p
p
    (t
t', Perm AnyName
perm2) <- AlphaCtx -> t -> m (t, Perm AnyName)
forall a (m :: * -> *).
(Alpha a, Fresh m) =>
AlphaCtx -> a -> m (a, Perm AnyName)
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> t -> m (t, Perm AnyName)
freshen' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) (AlphaCtx -> Perm AnyName -> t -> t
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) Perm AnyName
perm1 t
t)
    (Bind p t, Perm AnyName) -> m (Bind p t, Perm AnyName)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (p -> t -> Bind p t
forall p t. p -> t -> Bind p t
B p
p' t
t', Perm AnyName
perm1 Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
perm2)
  {-# INLINE freshen' #-}

  lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Bind p t -> (Bind p t -> Perm AnyName -> m b) -> m b
lfreshen' AlphaCtx
ctx (B p
p t
t) Bind p t -> Perm AnyName -> m b
cont =
    AlphaCtx -> p -> (p -> 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 -> p -> (p -> Perm AnyName -> m b) -> m b
lfreshen' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) p
p ((p -> Perm AnyName -> m b) -> m b)
-> (p -> Perm AnyName -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \p
p' Perm AnyName
pm1 ->
    AlphaCtx -> t -> (t -> 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 -> t -> (t -> Perm AnyName -> m b) -> m b
lfreshen' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) (AlphaCtx -> Perm AnyName -> t -> t
forall a. Alpha a => AlphaCtx -> Perm AnyName -> a -> a
swaps' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) Perm AnyName
pm1 t
t) ((t -> Perm AnyName -> m b) -> m b)
-> (t -> Perm AnyName -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \t
t' Perm AnyName
pm2 ->
    Bind p t -> Perm AnyName -> m b
cont (p -> t -> Bind p t
forall p t. p -> t -> Bind p t
B p
p' t
t') (Perm AnyName
pm1 Perm AnyName -> Perm AnyName -> Perm AnyName
forall a. Semigroup a => a -> a -> a
<> Perm AnyName
pm2)

  acompare' :: AlphaCtx -> Bind p t -> Bind p t -> Ordering
acompare' AlphaCtx
ctx (B p
p1 t
t1) (B p
p2 t
t2) =
    AlphaCtx -> p -> p -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' (AlphaCtx -> AlphaCtx
patternCtx AlphaCtx
ctx) p
p1 p
p2 Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> AlphaCtx -> t -> t -> Ordering
forall a. Alpha a => AlphaCtx -> a -> a -> Ordering
acompare' (AlphaCtx -> AlphaCtx
incrLevelCtx AlphaCtx
ctx) t
t1 t
t2