{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternSynonyms #-}

-- | This module provides a type class 'Bindable'. It contains things
-- (such as atoms, tuples of atoms, etc.) that can be abstracted by
-- binders.  Moreover, for each bindable type /a/ and nominal type
-- /t/, it defines a type 'Bind' /a/ /t/ of abstractions.
--
-- We also provide some generic programming so that instances of
-- 'Bindable' can be automatically derived in many cases.
--
-- For example, @(/x/,/y/) :. /t/@ binds a pair of atoms in /t/. It is
-- roughly equivalent to @/x/ :. /y/ :. /t/@, except that it is of type
-- 'Bind' ('Atom', 'Atom') /t/ instead of 'Bind' 'Atom' ('Bind' 'Atom'
-- /t/).
--
-- If a binder contains repeated atoms, they are regarded as
-- distinct. The binder is treated as if one atom occurrence was bound
-- at a time, in some fixed but unspecified order. For example,
-- @(/x/,/x/) :. (/x/,/x/)@ is equivalent to either @(/x/,/y/) :. (/x/,/x/)@
-- or @(/x/,/y/) :. (/y/,/y/)@. Which of the two alternatives is chosen
-- is implementation specific and user code should not rely on the
-- order of abstractions in such cases.
--
-- This module exposes implementation details of the Nominal library,
-- and should not normally be imported. Users of the library should
-- only import the top-level module "Nominal".

module Nominal.Bindable where

import GHC.Generics

import Nominal.Atom
import Nominal.Nominal
import Nominal.NominalSupport
import Nominal.NominalShow

-- ----------------------------------------------------------------------
-- * Binding lists of atoms

-- | The type of abstractions of a list of atoms. It is equivalent to
-- @'Bind' ['Atom'] /t/@, but has a more low-level implementation.
data BindAtomList t =
  BindNil t
  | BindCons (BindAtom (BindAtomList t))
  deriving ((forall x. BindAtomList t -> Rep (BindAtomList t) x)
-> (forall x. Rep (BindAtomList t) x -> BindAtomList t)
-> Generic (BindAtomList t)
forall x. Rep (BindAtomList t) x -> BindAtomList t
forall x. BindAtomList t -> Rep (BindAtomList t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (BindAtomList t) x -> BindAtomList t
forall t x. BindAtomList t -> Rep (BindAtomList t) x
$cfrom :: forall t x. BindAtomList t -> Rep (BindAtomList t) x
from :: forall x. BindAtomList t -> Rep (BindAtomList t) x
$cto :: forall t x. Rep (BindAtomList t) x -> BindAtomList t
to :: forall x. Rep (BindAtomList t) x -> BindAtomList t
Generic, NominalPermutation -> BindAtomList t -> BindAtomList t
(NominalPermutation -> BindAtomList t -> BindAtomList t)
-> Nominal (BindAtomList t)
forall t.
Nominal t =>
NominalPermutation -> BindAtomList t -> BindAtomList t
forall t. (NominalPermutation -> t -> t) -> Nominal t
$c• :: forall t.
Nominal t =>
NominalPermutation -> BindAtomList t -> BindAtomList t
• :: NominalPermutation -> BindAtomList t -> BindAtomList t
Nominal)

-- | Abstract a list of atoms in a term.
atomlist_abst :: [Atom] -> t -> BindAtomList t
atomlist_abst :: forall t. [Atom] -> t -> BindAtomList t
atomlist_abst [] t
t = t -> BindAtomList t
forall t. t -> BindAtomList t
BindNil t
t
atomlist_abst (Atom
a:[Atom]
as) t
t = BindAtom (BindAtomList t) -> BindAtomList t
forall t. BindAtom (BindAtomList t) -> BindAtomList t
BindCons (Atom -> BindAtomList t -> BindAtom (BindAtomList t)
forall t. Atom -> t -> BindAtom t
atom_abst Atom
a ([Atom] -> t -> BindAtomList t
forall t. [Atom] -> t -> BindAtomList t
atomlist_abst [Atom]
as t
t))

-- | Open a list abstraction.
--
-- The correct use of this function is subject to Pitts's freshness
-- condition.
atomlist_open :: (Nominal t) => BindAtomList t -> ([Atom] -> t -> s) -> s
atomlist_open :: forall t s. Nominal t => BindAtomList t -> ([Atom] -> t -> s) -> s
atomlist_open (BindNil t
t) [Atom] -> t -> s
k = [Atom] -> t -> s
k [] t
t
atomlist_open (BindCons BindAtom (BindAtomList t)
body) [Atom] -> t -> s
k =
  BindAtom (BindAtomList t) -> (Atom -> BindAtomList t -> s) -> s
forall t s. Nominal t => BindAtom t -> (Atom -> t -> s) -> s
atom_open BindAtom (BindAtomList t)
body ((Atom -> BindAtomList t -> s) -> s)
-> (Atom -> BindAtomList t -> s) -> s
forall a b. (a -> b) -> a -> b
$ \Atom
a BindAtomList t
body2 ->
  BindAtomList t -> ([Atom] -> t -> s) -> s
forall t s. Nominal t => BindAtomList t -> ([Atom] -> t -> s) -> s
atomlist_open BindAtomList t
body2 (([Atom] -> t -> s) -> s) -> ([Atom] -> t -> s) -> s
forall a b. (a -> b) -> a -> b
$ \[Atom]
as t
t ->
  [Atom] -> t -> s
k (Atom
aAtom -> [Atom] -> [Atom]
forall a. a -> [a] -> [a]
:[Atom]
as) t
t

-- | Open a list abstraction for printing.
--
-- The correct use of this function is subject to Pitts's freshness
-- condition.
atomlist_open_for_printing :: (Nominal t) => Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s
atomlist_open_for_printing :: forall t s.
Nominal t =>
Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s
atomlist_open_for_printing Support
sup (BindNil t
t) [Atom] -> t -> Support -> s
k = [Atom] -> t -> Support -> s
k [] t
t Support
sup
atomlist_open_for_printing Support
sup (BindCons BindAtom (BindAtomList t)
body) [Atom] -> t -> Support -> s
k =
  Support
-> BindAtom (BindAtomList t)
-> (Atom -> BindAtomList t -> Support -> s)
-> s
forall t s.
Nominal t =>
Support -> BindAtom t -> (Atom -> t -> Support -> s) -> s
atom_open_for_printing Support
sup BindAtom (BindAtomList t)
body ((Atom -> BindAtomList t -> Support -> s) -> s)
-> (Atom -> BindAtomList t -> Support -> s) -> s
forall a b. (a -> b) -> a -> b
$ \Atom
a BindAtomList t
body2 Support
sup' ->
  Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s
forall t s.
Nominal t =>
Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s
atomlist_open_for_printing Support
sup' BindAtomList t
body2 (([Atom] -> t -> Support -> s) -> s)
-> ([Atom] -> t -> Support -> s) -> s
forall a b. (a -> b) -> a -> b
$ \[Atom]
as t
t Support
sup'' ->
  [Atom] -> t -> Support -> s
k (Atom
aAtom -> [Atom] -> [Atom]
forall a. a -> [a] -> [a]
:[Atom]
as) t
t Support
sup''

-- | Merge a pair of list abstractions. If the lists are of different
-- lengths, return 'Nothing'.
atomlist_merge :: (Nominal t, Nominal s) => BindAtomList t -> BindAtomList s -> Maybe (BindAtomList (t,s))
atomlist_merge :: forall t s.
(Nominal t, Nominal s) =>
BindAtomList t -> BindAtomList s -> Maybe (BindAtomList (t, s))
atomlist_merge (BindNil t
t) (BindNil s
s) = BindAtomList (t, s) -> Maybe (BindAtomList (t, s))
forall a. a -> Maybe a
Just ((t, s) -> BindAtomList (t, s)
forall t. t -> BindAtomList t
BindNil (t
t,s
s))
atomlist_merge (BindCons BindAtom (BindAtomList t)
body1) (BindCons BindAtom (BindAtomList s)
body2) =
  BindAtom (BindAtomList t, BindAtomList s)
-> (Atom
    -> (BindAtomList t, BindAtomList s) -> Maybe (BindAtomList (t, s)))
-> Maybe (BindAtomList (t, s))
forall t s. Nominal t => BindAtom t -> (Atom -> t -> s) -> s
atom_open (BindAtom (BindAtomList t)
-> BindAtom (BindAtomList s)
-> BindAtom (BindAtomList t, BindAtomList s)
forall t s.
(Nominal t, Nominal s) =>
BindAtom t -> BindAtom s -> BindAtom (t, s)
atom_merge BindAtom (BindAtomList t)
body1 BindAtom (BindAtomList s)
body2) ((Atom
  -> (BindAtomList t, BindAtomList s) -> Maybe (BindAtomList (t, s)))
 -> Maybe (BindAtomList (t, s)))
-> (Atom
    -> (BindAtomList t, BindAtomList s) -> Maybe (BindAtomList (t, s)))
-> Maybe (BindAtomList (t, s))
forall a b. (a -> b) -> a -> b
$ \Atom
x (BindAtomList t
t,BindAtomList s
s) -> do
    BindAtomList (t, s)
ts <- BindAtomList t -> BindAtomList s -> Maybe (BindAtomList (t, s))
forall t s.
(Nominal t, Nominal s) =>
BindAtomList t -> BindAtomList s -> Maybe (BindAtomList (t, s))
atomlist_merge BindAtomList t
t BindAtomList s
s
    return (BindAtom (BindAtomList (t, s)) -> BindAtomList (t, s)
forall t. BindAtom (BindAtomList t) -> BindAtomList t
BindCons (Atom -> BindAtomList (t, s) -> BindAtom (BindAtomList (t, s))
forall t. Atom -> t -> BindAtom t
atom_abst Atom
x BindAtomList (t, s)
ts))
atomlist_merge BindAtomList t
_ BindAtomList s
_ = Maybe (BindAtomList (t, s))
forall a. Maybe a
Nothing

-- ----------------------------------------------------------------------
-- * Binder combinators

-- | A representation of binders of type /a/. This is an abstract
-- type with no exposed structure. The only way to construct a value
-- of type 'NominalBinder' /a/ is through the 'Applicative' interface and by
-- using the functions 'binding' and 'nobinding'.

data NominalBinder a =
  NominalBinder [Atom] ([Atom] -> (a, [Atom]))

-- $ Implementation note: The behavior of a binders is determined by two
-- things: the list of bound atom occurrences (binding sites), and a
-- renaming function that takes such a list of atoms and returns a
-- term. For efficiency, the renaming function is stateful: it also
-- returns a list of atoms not yet used.
--
-- The binding sites must be serialized in some deterministic order,
-- and must be accepted in the same corresponding order by the
-- renaming function.
--
-- If an atom occurs at multiple binding sites, it must be serialized
-- multiple times. The corresponding renaming function must accept
-- fresh atoms and put them into the respective binding sites.
--
-- ==== Examples:
--
-- > binding x = NominalBinder [x] (\(x:zs) -> (x, zs))
-- >
-- > binding (x, y) = NominalBinder [x, y] (\(x:y:zs) -> ((x, y), zs))
-- >
-- > binding (x, NoBind y) = NominalBinder [x] (\(x:zs) -> ((x, NoBind y), zs))
-- >
-- > binding (x, x, y) = NominalBinder [x, x, y] (\(x:x':y:zs) -> ((x, x', y), zs))

-- | Constructor for non-binding binders. This can be used to mark
-- non-binding subterms when defining a 'Bindable' instance. See
-- <#CUSTOM "Defining custom instances"> for examples.
nobinding :: a -> NominalBinder a
nobinding :: forall a. a -> NominalBinder a
nobinding a
a = [Atom] -> ([Atom] -> (a, [Atom])) -> NominalBinder a
forall a. [Atom] -> ([Atom] -> (a, [Atom])) -> NominalBinder a
NominalBinder [] (\[Atom]
xs -> (a
a, [Atom]
xs))

-- | Constructor for a binder binding a single atom.
atom_binding :: Atom -> NominalBinder Atom
atom_binding :: Atom -> NominalBinder Atom
atom_binding Atom
a = [Atom] -> ([Atom] -> (Atom, [Atom])) -> NominalBinder Atom
forall a. [Atom] -> ([Atom] -> (a, [Atom])) -> NominalBinder a
NominalBinder [Atom
a] (\(Atom
a:[Atom]
xs) -> (Atom
a, [Atom]
xs))

-- | Map a function over a 'NominalBinder'.
binder_map :: (a -> b) -> NominalBinder a -> NominalBinder b
binder_map :: forall a b. (a -> b) -> NominalBinder a -> NominalBinder b
binder_map a -> b
f (NominalBinder [Atom]
xs [Atom] -> (a, [Atom])
g) = [Atom] -> ([Atom] -> (b, [Atom])) -> NominalBinder b
forall a. [Atom] -> ([Atom] -> (a, [Atom])) -> NominalBinder a
NominalBinder [Atom]
xs [Atom] -> (b, [Atom])
h where
  h :: [Atom] -> (b, [Atom])
h [Atom]
xs = (a -> b
f a
a, [Atom]
ys) where
    (a
a, [Atom]
ys) = [Atom] -> (a, [Atom])
g [Atom]
xs

-- | Combinator giving 'NominalBinder' an applicative structure. This
-- is used for constructing tuple binders.
binder_app :: NominalBinder (a -> b) -> NominalBinder a -> NominalBinder b
binder_app :: forall a b.
NominalBinder (a -> b) -> NominalBinder a -> NominalBinder b
binder_app (NominalBinder [Atom]
xs [Atom] -> (a -> b, [Atom])
f) (NominalBinder [Atom]
ys [Atom] -> (a, [Atom])
g) = [Atom] -> ([Atom] -> (b, [Atom])) -> NominalBinder b
forall a. [Atom] -> ([Atom] -> (a, [Atom])) -> NominalBinder a
NominalBinder ([Atom]
xs [Atom] -> [Atom] -> [Atom]
forall a. [a] -> [a] -> [a]
++ [Atom]
ys) [Atom] -> (b, [Atom])
h where
  h :: [Atom] -> (b, [Atom])
h [Atom]
zs = (a -> b
a a
b, [Atom]
zs'') where
    (a -> b
a, [Atom]
zs') = [Atom] -> (a -> b, [Atom])
f [Atom]
zs
    (a
b, [Atom]
zs'') = [Atom] -> (a, [Atom])
g [Atom]
zs'

instance Functor NominalBinder where
  fmap :: forall a b. (a -> b) -> NominalBinder a -> NominalBinder b
fmap = (a -> b) -> NominalBinder a -> NominalBinder b
forall a b. (a -> b) -> NominalBinder a -> NominalBinder b
binder_map

instance Applicative NominalBinder where
  pure :: forall a. a -> NominalBinder a
pure = a -> NominalBinder a
forall a. a -> NominalBinder a
nobinding
  NominalBinder (a -> b)
f <*> :: forall a b.
NominalBinder (a -> b) -> NominalBinder a -> NominalBinder b
<*> NominalBinder a
b = NominalBinder (a -> b) -> NominalBinder a -> NominalBinder b
forall a b.
NominalBinder (a -> b) -> NominalBinder a -> NominalBinder b
binder_app NominalBinder (a -> b)
f NominalBinder a
b
  
-- ----------------------------------------------------------------------
-- * The Bindable class

-- | 'Bind' /a/ /t/ is the type of /abstractions/, denoted [/A/]/T/ in
-- the nominal logic literature. Its elements are pairs (/a/,/t/)
-- modulo alpha-equivalence. We also write /a/ ':.' /t/ for such an
-- equivalence class of pairs, which is denoted /a/./t/ in the nominal
-- logic literature. For full technical details on what this means,
-- see Definition 4 of <#PITTS2003 [Pitts 2003]>.

data Bind a t =
  Bind ([Atom] -> a) (BindAtomList t)

instance (Bindable a, NominalShow a, NominalShow t) => NominalShow (Bind a t) where
  showsPrecSup :: Support -> Int -> Bind a t -> ShowS
showsPrecSup Support
sup Int
d Bind a t
t =
    Support -> Bind a t -> (a -> t -> Support -> ShowS) -> ShowS
forall a t s.
(Bindable a, Nominal t) =>
Support -> Bind a t -> (a -> t -> Support -> s) -> s
open_for_printing Support
sup Bind a t
t ((a -> t -> Support -> ShowS) -> ShowS)
-> (a -> t -> Support -> ShowS) -> ShowS
forall a b. (a -> b) -> a -> b
$ \a
a t
s Support
sup' ->
      Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString (a -> String
forall t. NominalShow t => t -> String
nominal_show a
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :. " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Support -> Int -> t -> ShowS
forall t. NominalShow t => Support -> Int -> t -> ShowS
showsPrecSup Support
sup' Int
5 t
s String
"")

instance (Bindable a, NominalShow a, NominalShow t) => Show (Bind a t) where
  showsPrec :: Int -> Bind a t -> ShowS
showsPrec = Int -> Bind a t -> ShowS
forall t. NominalShow t => Int -> t -> ShowS
nominal_showsPrec

-- | A type is 'Bindable' if its elements can be abstracted. Such
-- elements are also called /binders/, or sometimes /patterns/.
-- Examples include atoms, tuples of atoms, list of atoms, etc.
--
-- In most cases, instances of 'Bindable' can be automatically
-- derived. See <#DERIVING "Deriving generic instances"> for
-- information on how to do so, and
-- <#CUSTOM "Defining custom instances"> for how to write custom
-- instances.
class (Nominal a) => Bindable a where
  -- | A function that maps a term to a binder. New binders can be
  -- constructed using the 'Applicative' structure of 'NominalBinder'.
  -- See <#CUSTOM "Defining custom instances"> for examples.
  binding :: a -> NominalBinder a
  
  default binding :: (Generic a, GBindable (Rep a)) => a -> NominalBinder a
  binding a
x = Rep a Any -> (Rep a Any -> a) -> NominalBinder a
forall a b. Rep a a -> (Rep a a -> b) -> NominalBinder b
forall (f :: * -> *) a b.
GBindable f =>
f a -> (f a -> b) -> NominalBinder b
gbinding (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x) Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to

-- |
-- ==== Usage as a constructor
--
-- The term /a/ ':.' /t/ is a constructor for abstractions. It
-- represents the equivalence class of pairs (/a/,/t/) modulo
-- alpha-equivalence. This is the same concept that is written as
-- /a/./t/ in the nominal logic literature. We use the notation
-- @(@':.'@)@ because the standard Haskell library reserves @(@'.'@)@
-- for function composition.
--
-- Note that @(@':.'@)@ is an abstraction operator of the
-- /object language/ (i.e., whatever datatype you are defining), not
-- of the /metalanguage/ (i.e., Haskell). A term such as /a/ ':.' /t/
-- only makes sense if the variable /a/ is already defined to be a
-- particular atom.  Thus, abstractions are often used in the context
-- of a scoped operation such as 'Nominal.with_fresh' or on the
-- right-hand side of an abstraction pattern match, as in the
-- following examples:
--
-- > with_fresh (\a -> a :. a)
-- >
-- > subst m z (Abs (x :. t)) = Abs (x :. subst m z t)
--
-- For building an abstraction by using a binder of the metalanguage,
-- see also the function 'Nominal.bind'.
--
-- ==== Usage as a pattern
-- 
-- We can also use @(@/x/ ':.' /t/@)@ as a pattern for pattern
-- matching. It is called an /abstraction pattern/. Its behavior is
-- very different from ordinary patterns. An abstraction pattern
-- @(@/x/ ':.' /t/@)@ matches any term of type @('Bind' /a/
-- /b/)@. When matching the pattern @(@/x/ ':.' /t/@)@ with a value
-- /y/':.'/s/, the effect is that a /fresh/ name /x/ and a value /t/
-- will be generated such that /x/ ':.' /t/ = /y/ ':.' /s/. Is it
-- important to note that a /different/ fresh /x/ is chosen each time
-- an abstraction patterns is used.  Here are some examples:
--
-- > foo (x :. t) = body
-- > 
-- > let (x :. t) = s in body
-- > 
-- > case t of
-- >   Var v -> body1
-- >   App m n -> body2
-- >   Abs (x :. t) -> body3
--   
-- Like all patterns, abstraction patterns can be nested. For example:
--
-- > foo1 (a :. b :. t) = ...
-- >
-- > foo2 (x :. (s,t)) = (x :. s, x :. t)
-- >
-- > foo3 (Abs (x :. Var y))
-- >   | x == y    = ...
-- >   | otherwise = ...
-- >
--
-- The correct use of abstraction patterns is subject to
-- <#CONDITION Pitts's freshness condition>.
-- Thus, for example, the following are permitted
--
-- > let (x :. t) = s in x :. t,
-- > let (x :. t) = s in f x t == g x t,
--
-- whereas the following is not permitted:
--
-- > let (x :. t) = s in (x,t).
--
-- See <#CONDITION "Pitts's freshness condition"> for more details.
pattern (:.) :: (Nominal b, Bindable a) => a -> b -> Bind a b 
pattern a $m:. :: forall {r} {b} {a}.
(Nominal b, Bindable a) =>
Bind a b -> (a -> b -> r) -> ((# #) -> r) -> r
$b:. :: forall b a. (Nominal b, Bindable a) => a -> b -> Bind a b
:. t <- ((\Bind a b
body -> Bind a b -> (a -> b -> (a, b)) -> (a, b)
forall a t s.
(Bindable a, Nominal t) =>
Bind a t -> (a -> t -> s) -> s
open Bind a b
body (\a
a b
t -> (a
a,b
t))) -> (a, t))
 where
   a
a :. b
t = a -> b -> Bind a b
forall a t. (Bindable a, Nominal t) => a -> t -> Bind a t
abst a
a b
t
infixr 5 :.
{-# COMPLETE (:.) #-}
  
-- | An alternative non-infix notation for @(@':.'@)@.
abst :: (Bindable a, Nominal t) => a -> t -> Bind a t
abst :: forall a t. (Bindable a, Nominal t) => a -> t -> Bind a t
abst a
a t
t = ([Atom] -> a) -> BindAtomList t -> Bind a t
forall a t. ([Atom] -> a) -> BindAtomList t -> Bind a t
Bind ((a, [Atom]) -> a
forall a b. (a, b) -> a
fst ((a, [Atom]) -> a) -> ([Atom] -> (a, [Atom])) -> [Atom] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Atom] -> (a, [Atom])
f) ([Atom] -> t -> BindAtomList t
forall t. [Atom] -> t -> BindAtomList t
atomlist_abst [Atom]
xs t
t)
  where
    NominalBinder [Atom]
xs [Atom] -> (a, [Atom])
f = a -> NominalBinder a
forall a. Bindable a => a -> NominalBinder a
binding a
a

-- | An alternative notation for abstraction patterns.
--
-- > f t = open t (\x s -> body)
--
-- is precisely equivalent to
--
-- > f (x :. s) = body.
--
-- The correct use of this function is subject to
-- <#CONDITION Pitts's freshness condition>.
open :: (Bindable a, Nominal t) => Bind a t -> (a -> t -> s) -> s
open :: forall a t s.
(Bindable a, Nominal t) =>
Bind a t -> (a -> t -> s) -> s
open (Bind [Atom] -> a
f BindAtomList t
body) a -> t -> s
k =
  BindAtomList t -> ([Atom] -> t -> s) -> s
forall t s. Nominal t => BindAtomList t -> ([Atom] -> t -> s) -> s
atomlist_open BindAtomList t
body (\[Atom]
ys t
t -> a -> t -> s
k ([Atom] -> a
f [Atom]
ys) t
t)
  
-- | A variant of 'open' which moreover chooses a name for the
-- bound atom that does not clash with any free name in its
-- scope. This function is mostly useful for building custom
-- pretty-printers for nominal terms. Except in pretty-printers, it is
-- equivalent to 'open'.
--
-- Usage:
--
-- > open_for_printing sup t (\x s sup' -> body)
--
-- Here, /sup/ = 'support' /t/ (this requires a 'NominalSupport'
-- instance). For printing to be efficient (roughly O(/n/)), the
-- support must be pre-computed in a bottom-up fashion, and then
-- passed into each subterm in a top-down fashion (rather than
-- re-computing it at each level, which would be O(/n/²)).  For this
-- reason, 'open_for_printing' takes the support of /t/ as an
-- additional argument, and provides /sup'/, the support of /s/, as an
-- additional parameter to the body.
--
-- The correct use of this function is subject to
-- <#CONDITION Pitts's freshness condition>.
open_for_printing :: (Bindable a, Nominal t) => Support -> Bind a t -> (a -> t -> Support -> s) -> s
open_for_printing :: forall a t s.
(Bindable a, Nominal t) =>
Support -> Bind a t -> (a -> t -> Support -> s) -> s
open_for_printing Support
sup (Bind [Atom] -> a
f BindAtomList t
body) a -> t -> Support -> s
k =
  Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s
forall t s.
Nominal t =>
Support -> BindAtomList t -> ([Atom] -> t -> Support -> s) -> s
atomlist_open_for_printing Support
sup BindAtomList t
body (\[Atom]
ys t
t Support
sup' -> a -> t -> Support -> s
k ([Atom] -> a
f [Atom]
ys) t
t Support
sup')

instance (Nominal a, Nominal t, Eq a, Eq t) => Eq (Bind a t) where
  Bind [Atom] -> a
f1 BindAtomList t
body1 == :: Bind a t -> Bind a t -> Bool
== Bind [Atom] -> a
f2 BindAtomList t
body2 =
    case BindAtomList t -> BindAtomList t -> Maybe (BindAtomList (t, t))
forall t s.
(Nominal t, Nominal s) =>
BindAtomList t -> BindAtomList s -> Maybe (BindAtomList (t, s))
atomlist_merge BindAtomList t
body1 BindAtomList t
body2 of
      Maybe (BindAtomList (t, t))
Nothing -> Bool
False
      Just BindAtomList (t, t)
bodies ->
        BindAtomList (t, t) -> ([Atom] -> (t, t) -> Bool) -> Bool
forall t s. Nominal t => BindAtomList t -> ([Atom] -> t -> s) -> s
atomlist_open BindAtomList (t, t)
bodies (([Atom] -> (t, t) -> Bool) -> Bool)
-> ([Atom] -> (t, t) -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \[Atom]
xs (t
t1, t
t2) ->
          t
t1 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
t2 Bool -> Bool -> Bool
&& [Atom] -> a
f1 [Atom]
xs a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== [Atom] -> a
f2 [Atom]
xs

instance (Bindable a, Nominal t) => Nominal (Bind a t) where
  NominalPermutation
π • :: NominalPermutation -> Bind a t -> Bind a t
• (Bind [Atom] -> a
f BindAtomList t
body) = ([Atom] -> a) -> BindAtomList t -> Bind a t
forall a t. ([Atom] -> a) -> BindAtomList t -> Bind a t
Bind (NominalPermutation
π NominalPermutation -> ([Atom] -> a) -> [Atom] -> a
forall t. Nominal t => NominalPermutation -> t -> t
• [Atom] -> a
f) (NominalPermutation
π NominalPermutation -> BindAtomList t -> BindAtomList t
forall t. Nominal t => NominalPermutation -> t -> t
• BindAtomList t
body)

instance (Bindable a, NominalSupport a, NominalSupport t) => NominalSupport (Bind a t) where
  support :: Bind a t -> Support
support (Bind [Atom] -> a
f BindAtomList t
body) = BindAtomList t -> ([Atom] -> t -> Support) -> Support
forall t s. Nominal t => BindAtomList t -> ([Atom] -> t -> s) -> s
atomlist_open BindAtomList t
body (([Atom] -> t -> Support) -> Support)
-> ([Atom] -> t -> Support) -> Support
forall a b. (a -> b) -> a -> b
$ \[Atom]
xs t
t ->
    [Atom] -> Support -> Support
support_deletes [Atom]
xs ((a, t) -> Support
forall t. NominalSupport t => t -> Support
support ([Atom] -> a
f [Atom]
xs, t
t))

-- ----------------------------------------------------------------------
-- * Non-binding binders

-- | The type constructor 'NoBind' permits data of arbitrary types
-- (including nominal types) to be embedded in binders without
-- becoming bound. For example, in the term
--
-- > m = (a, NoBind b) :. (a,b),
--
-- the atom /a/ is bound, but the atom /b/ remains free. Thus, /m/ is
-- alpha-equivalent to @(x, NoBind b) :. (x,b)@, but not to
-- @(x, NoBind c) :. (x,c)@.
--
-- A typical use case is using contexts as binders. A /context/ is a
-- map from atoms to some data (for example, a /typing context/ is a
-- map from atoms to types, and an /evaluation context/ is a map from
-- atoms to values). If we define contexts like this:
--
-- > type Context t = [(Atom, NoBind t)]
--
-- then we can use contexts as binders. Specifically, if
-- Γ = {/x/₁ ↦ /A/₁, …, /x/ₙ ↦ /A/ₙ} is a context, then (Γ :. /t/)
-- binds the context to a term /t/. This means, /x/₁,…,/x/ₙ are bound
-- in /t/, but not any atoms that occur in /A/₁,…,/A/ₙ. Without the
-- use of 'NoBind', any atoms occurring on /A/₁,…,/A/ₙ would have been
-- bound as well.
--
-- Even though atoms under 'NoBind' are not /binding/, they can still
-- be /bound/ by other binders. For example, the term
-- @/x/:.(/x/, 'NoBind' /x/)@ is alpha-equivalent to
-- @/y/:.(/y/, 'NoBind' /y/)@. Another way to say this is that 'NoBind'
-- has a special behavior on the left, but not on the right of a dot.

newtype NoBind t = NoBind t
  deriving (Int -> NoBind t -> ShowS
[NoBind t] -> ShowS
NoBind t -> String
(Int -> NoBind t -> ShowS)
-> (NoBind t -> String) -> ([NoBind t] -> ShowS) -> Show (NoBind t)
forall t. Show t => Int -> NoBind t -> ShowS
forall t. Show t => [NoBind t] -> ShowS
forall t. Show t => NoBind t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> NoBind t -> ShowS
showsPrec :: Int -> NoBind t -> ShowS
$cshow :: forall t. Show t => NoBind t -> String
show :: NoBind t -> String
$cshowList :: forall t. Show t => [NoBind t] -> ShowS
showList :: [NoBind t] -> ShowS
Show, NoBind t -> NoBind t -> Bool
(NoBind t -> NoBind t -> Bool)
-> (NoBind t -> NoBind t -> Bool) -> Eq (NoBind t)
forall t. Eq t => NoBind t -> NoBind t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => NoBind t -> NoBind t -> Bool
== :: NoBind t -> NoBind t -> Bool
$c/= :: forall t. Eq t => NoBind t -> NoBind t -> Bool
/= :: NoBind t -> NoBind t -> Bool
Eq, Eq (NoBind t)
Eq (NoBind t) =>
(NoBind t -> NoBind t -> Ordering)
-> (NoBind t -> NoBind t -> Bool)
-> (NoBind t -> NoBind t -> Bool)
-> (NoBind t -> NoBind t -> Bool)
-> (NoBind t -> NoBind t -> Bool)
-> (NoBind t -> NoBind t -> NoBind t)
-> (NoBind t -> NoBind t -> NoBind t)
-> Ord (NoBind t)
NoBind t -> NoBind t -> Bool
NoBind t -> NoBind t -> Ordering
NoBind t -> NoBind t -> NoBind t
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall t. Ord t => Eq (NoBind t)
forall t. Ord t => NoBind t -> NoBind t -> Bool
forall t. Ord t => NoBind t -> NoBind t -> Ordering
forall t. Ord t => NoBind t -> NoBind t -> NoBind t
$ccompare :: forall t. Ord t => NoBind t -> NoBind t -> Ordering
compare :: NoBind t -> NoBind t -> Ordering
$c< :: forall t. Ord t => NoBind t -> NoBind t -> Bool
< :: NoBind t -> NoBind t -> Bool
$c<= :: forall t. Ord t => NoBind t -> NoBind t -> Bool
<= :: NoBind t -> NoBind t -> Bool
$c> :: forall t. Ord t => NoBind t -> NoBind t -> Bool
> :: NoBind t -> NoBind t -> Bool
$c>= :: forall t. Ord t => NoBind t -> NoBind t -> Bool
>= :: NoBind t -> NoBind t -> Bool
$cmax :: forall t. Ord t => NoBind t -> NoBind t -> NoBind t
max :: NoBind t -> NoBind t -> NoBind t
$cmin :: forall t. Ord t => NoBind t -> NoBind t -> NoBind t
min :: NoBind t -> NoBind t -> NoBind t
Ord, (forall x. NoBind t -> Rep (NoBind t) x)
-> (forall x. Rep (NoBind t) x -> NoBind t) -> Generic (NoBind t)
forall x. Rep (NoBind t) x -> NoBind t
forall x. NoBind t -> Rep (NoBind t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (NoBind t) x -> NoBind t
forall t x. NoBind t -> Rep (NoBind t) x
$cfrom :: forall t x. NoBind t -> Rep (NoBind t) x
from :: forall x. NoBind t -> Rep (NoBind t) x
$cto :: forall t x. Rep (NoBind t) x -> NoBind t
to :: forall x. Rep (NoBind t) x -> NoBind t
Generic, NominalPermutation -> NoBind t -> NoBind t
(NominalPermutation -> NoBind t -> NoBind t) -> Nominal (NoBind t)
forall t. Nominal t => NominalPermutation -> NoBind t -> NoBind t
forall t. (NominalPermutation -> t -> t) -> Nominal t
$c• :: forall t. Nominal t => NominalPermutation -> NoBind t -> NoBind t
• :: NominalPermutation -> NoBind t -> NoBind t
Nominal, Nominal (NoBind t)
Nominal (NoBind t) =>
(NoBind t -> Support) -> NominalSupport (NoBind t)
NoBind t -> Support
forall t. Nominal t => (t -> Support) -> NominalSupport t
forall t. NominalSupport t => Nominal (NoBind t)
forall t. NominalSupport t => NoBind t -> Support
$csupport :: forall t. NominalSupport t => NoBind t -> Support
support :: NoBind t -> Support
NominalSupport)

-- ----------------------------------------------------------------------
-- * Bindable instances

-- $ Most of the time, instances of 'Bindable' should be derived using
-- @deriving (Generic, Nominal, Bindable)@, as in this example:
--
-- > {-# LANGUAGE DeriveGeneric #-}
-- > {-# LANGUAGE DeriveAnyClass #-}
-- >
-- > data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
-- >   deriving (Generic, Nominal, Bindable)
--
-- In the case of non-nominal types (typically base types such as
-- 'Double'), a 'Bindable' instance can be defined using
-- 'basic_binding':
--
-- > instance Bindable MyType where
-- >   binding = basic_binding
--
-- In this case, an abstraction (/x/ ':.' /t/) is equivalent to an ordinary
-- pair (/x/, /t/), since there is no bound atom that could be renamed.

-- | A helper function for defining 'Bindable' instances
-- for non-nominal types.
basic_binding :: a -> NominalBinder a
basic_binding :: forall a. a -> NominalBinder a
basic_binding = a -> NominalBinder a
forall a. a -> NominalBinder a
nobinding

-- Base cases

instance Bindable Atom where
  binding :: Atom -> NominalBinder Atom
binding = Atom -> NominalBinder Atom
atom_binding

instance Bindable Bool where
  binding :: Bool -> NominalBinder Bool
binding = Bool -> NominalBinder Bool
forall a. a -> NominalBinder a
basic_binding
  
instance Bindable Integer where
  binding :: Integer -> NominalBinder Integer
binding = Integer -> NominalBinder Integer
forall a. a -> NominalBinder a
basic_binding
  
instance Bindable Int where
  binding :: Int -> NominalBinder Int
binding = Int -> NominalBinder Int
forall a. a -> NominalBinder a
basic_binding
  
instance Bindable Char where
  binding :: Char -> NominalBinder Char
binding = Char -> NominalBinder Char
forall a. a -> NominalBinder a
basic_binding
  
instance Bindable Double where
  binding :: Double -> NominalBinder Double
binding = Double -> NominalBinder Double
forall a. a -> NominalBinder a
basic_binding
  
instance Bindable Float where
  binding :: Float -> NominalBinder Float
binding = Float -> NominalBinder Float
forall a. a -> NominalBinder a
basic_binding
  
instance Bindable Ordering where
  binding :: Ordering -> NominalBinder Ordering
binding = Ordering -> NominalBinder Ordering
forall a. a -> NominalBinder a
basic_binding
  
instance Bindable (Basic t) where
  binding :: Basic t -> NominalBinder (Basic t)
binding = Basic t -> NominalBinder (Basic t)
forall a. a -> NominalBinder a
basic_binding

instance Bindable Literal where
  binding :: Literal -> NominalBinder Literal
binding = Literal -> NominalBinder Literal
forall a. a -> NominalBinder a
basic_binding

instance (Nominal t) => Bindable (NoBind t) where
  binding :: NoBind t -> NominalBinder (NoBind t)
binding = NoBind t -> NominalBinder (NoBind t)
forall a. a -> NominalBinder a
nobinding
  
-- Generic instances
  
instance (Bindable a) => Bindable [a]
instance Bindable ()
instance (Bindable a, Bindable b) => Bindable (a, b)
instance (Bindable a, Bindable b, Bindable c) => Bindable (a, b, c)
instance (Bindable a, Bindable b, Bindable c, Bindable d) => Bindable (a, b, c, d)
instance (Bindable a, Bindable b, Bindable c, Bindable d, Bindable e) => Bindable (a, b, c, d, e)
instance (Bindable a, Bindable b, Bindable c, Bindable d, Bindable e, Bindable f) => Bindable (a, b, c, d, e, f)
instance (Bindable a, Bindable b, Bindable c, Bindable d, Bindable e, Bindable f, Bindable g) => Bindable (a, b, c, d, e, f, g)
instance (Bindable a) => Bindable (Maybe a)
instance (Bindable a, Bindable b) => Bindable (Either a b)

-- ----------------------------------------------------------------------
-- * Generic programming for Bindable

-- | A specialized combinator. Although this functionality is
-- expressible in terms of the applicative structure, we give a custom
-- CPS-based implementation for performance reasons. It improves the
-- overall performance by 14% (time) and 16% (space) in a typical
-- benchmark.
binder_gpair :: NominalBinder (a x) -> NominalBinder (b x) -> ((a :*: b) x -> c) -> NominalBinder c
binder_gpair :: forall (a :: * -> *) x (b :: * -> *) c.
NominalBinder (a x)
-> NominalBinder (b x) -> ((:*:) a b x -> c) -> NominalBinder c
binder_gpair (NominalBinder [Atom]
xs [Atom] -> (a x, [Atom])
f) (NominalBinder [Atom]
ys [Atom] -> (b x, [Atom])
g) (:*:) a b x -> c
k = [Atom] -> ([Atom] -> (c, [Atom])) -> NominalBinder c
forall a. [Atom] -> ([Atom] -> (a, [Atom])) -> NominalBinder a
NominalBinder ([Atom]
xs [Atom] -> [Atom] -> [Atom]
forall a. [a] -> [a] -> [a]
++ [Atom]
ys) [Atom] -> (c, [Atom])
h where
  h :: [Atom] -> (c, [Atom])
h [Atom]
zs = ((:*:) a b x -> c
k (a x
a a x -> b x -> (:*:) a b x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b x
b), [Atom]
zs'') where
    (a x
a, [Atom]
zs') = [Atom] -> (a x, [Atom])
f [Atom]
zs
    (b x
b, [Atom]
zs'') = [Atom] -> (b x, [Atom])
g [Atom]
zs'

-- | A version of the 'Bindable' class suitable for generic programming.
class GBindable f where
  gbinding :: f a -> (f a -> b) -> NominalBinder b

instance GBindable V1 where
  gbinding :: forall a b. V1 a -> (V1 a -> b) -> NominalBinder b
gbinding = V1 a -> (V1 a -> b) -> NominalBinder b
forall a. HasCallStack => a
undefined -- never occurs, because V1 is empty

instance GBindable U1 where
  gbinding :: forall a b. U1 a -> (U1 a -> b) -> NominalBinder b
gbinding U1 a
a U1 a -> b
k = [Atom] -> ([Atom] -> (b, [Atom])) -> NominalBinder b
forall a. [Atom] -> ([Atom] -> (a, [Atom])) -> NominalBinder a
NominalBinder [] (\[Atom]
xs -> (U1 a -> b
k U1 a
a, [Atom]
xs))

instance (GBindable a, GBindable b) => GBindable (a :*: b) where
  gbinding :: forall a b. (:*:) a b a -> ((:*:) a b a -> b) -> NominalBinder b
gbinding (a a
a :*: b a
b) (:*:) a b a -> b
k =
    NominalBinder (a a)
-> NominalBinder (b a) -> ((:*:) a b a -> b) -> NominalBinder b
forall (a :: * -> *) x (b :: * -> *) c.
NominalBinder (a x)
-> NominalBinder (b x) -> ((:*:) a b x -> c) -> NominalBinder c
binder_gpair (a a -> (a a -> a a) -> NominalBinder (a a)
forall a b. a a -> (a a -> b) -> NominalBinder b
forall (f :: * -> *) a b.
GBindable f =>
f a -> (f a -> b) -> NominalBinder b
gbinding a a
a a a -> a a
forall a. a -> a
id) (b a -> (b a -> b a) -> NominalBinder (b a)
forall a b. b a -> (b a -> b) -> NominalBinder b
forall (f :: * -> *) a b.
GBindable f =>
f a -> (f a -> b) -> NominalBinder b
gbinding b a
b b a -> b a
forall a. a -> a
id) (:*:) a b a -> b
k

instance (GBindable a, GBindable b) => GBindable (a :+: b) where
  gbinding :: forall a b. (:+:) a b a -> ((:+:) a b a -> b) -> NominalBinder b
gbinding (L1 a a
a) (:+:) a b a -> b
k = a a -> (a a -> b) -> NominalBinder b
forall a b. a a -> (a a -> b) -> NominalBinder b
forall (f :: * -> *) a b.
GBindable f =>
f a -> (f a -> b) -> NominalBinder b
gbinding a a
a (\a a
a -> (:+:) a b a -> b
k (a a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 a a
a))
  gbinding (R1 b a
a) (:+:) a b a -> b
k = b a -> (b a -> b) -> NominalBinder b
forall a b. b a -> (b a -> b) -> NominalBinder b
forall (f :: * -> *) a b.
GBindable f =>
f a -> (f a -> b) -> NominalBinder b
gbinding b a
a (\b a
a -> (:+:) a b a -> b
k (b a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 b a
a))

instance (GBindable a) => GBindable (M1 i c a) where
  gbinding :: forall a b. M1 i c a a -> (M1 i c a a -> b) -> NominalBinder b
gbinding (M1 a a
a) M1 i c a a -> b
k = a a -> (a a -> b) -> NominalBinder b
forall a b. a a -> (a a -> b) -> NominalBinder b
forall (f :: * -> *) a b.
GBindable f =>
f a -> (f a -> b) -> NominalBinder b
gbinding a a
a (\a a
a -> M1 i c a a -> b
k (a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 a a
a))
  
instance (Bindable a) => GBindable (K1 i a) where
  gbinding :: forall a b. K1 i a a -> (K1 i a a -> b) -> NominalBinder b
gbinding (K1 a
a) K1 i a a -> b
k = (K1 i a a -> b) -> NominalBinder (K1 i a a) -> NominalBinder b
forall a b. (a -> b) -> NominalBinder a -> NominalBinder b
binder_map K1 i a a -> b
k (a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> NominalBinder a -> NominalBinder (K1 i a a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> NominalBinder a
forall a. Bindable a => a -> NominalBinder a
binding a
a)