{-# 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 Prelude hiding ((.))
import GHC.Generics

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

-- ----------------------------------------------------------------------
-- * 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 (Generic, Nominal)

-- | Abstract a list of atoms in a term.
atomlist_abst :: [Atom] -> t -> BindAtomList t
atomlist_abst [] t = BindNil t
atomlist_abst (a:as) t = BindCons (atom_abst a (atomlist_abst as 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 (BindNil t) k = k [] t
atomlist_open (BindCons body) k =
  atom_open body $ \a body2 ->
  atomlist_open body2 $ \as t ->
  k (a:as) 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 sup (BindNil t) k = k [] t sup
atomlist_open_for_printing sup (BindCons body) k =
  atom_open_for_printing sup body $ \a body2 sup' ->
  atomlist_open_for_printing sup' body2 $ \as t sup'' ->
  k (a:as) t 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 (BindNil t) (BindNil s) = Just (BindNil (t,s))
atomlist_merge (BindCons body1) (BindCons body2) =
  atom_open (atom_merge body1 body2) $ \x (t,s) -> do
    ts <- atomlist_merge t s
    return (BindCons (atom_abst x ts))
atomlist_merge _ _ = 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 a = NominalBinder [] (\xs -> (a, xs))

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

-- | Map a function over a 'NominalBinder'.
binder_map :: (a -> b) -> NominalBinder a -> NominalBinder b
binder_map f (NominalBinder xs g) = NominalBinder xs h where
  h xs = (f a, ys) where
    (a, ys) = g 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 (NominalBinder xs f) (NominalBinder ys g) = NominalBinder (xs ++ ys) h where
  h zs = (a b, zs'') where
    (a, zs') = f zs
    (b, zs'') = g zs'

instance Functor NominalBinder where
  fmap = binder_map

instance Applicative NominalBinder where
  pure = nobinding
  f <*> b = binder_app f 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. For full technical details on what this
-- means, see Definition 4 of
-- <#PITTS2003 [Pitts 2003]>.

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

-- | 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 'Nominal' 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 x = gbinding (from x) to

-- | Constructor for abstractions. The term /a/'.'/t/ represents the
-- equivalence class of pairs (/a/,/t/) modulo alpha-equivalence.
--
-- We use the infix operator @(@'.'@)@, which is normally bound to
-- function composition in the standard Haskell library. Thus, nominal
-- programs should import the standard library like this:
-- 
-- > import Prelude hiding ((.))
--
-- Note that @(@'.'@)@ is a 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'.
(.) :: (Bindable a, Nominal t) => a -> t -> Bind a t
a . t = Bind (fst ∘ f) (atomlist_abst xs t)
  where
    NominalBinder xs f = binding a
infixr 5 .

-- | A pattern matching syntax for abstractions. The pattern
-- @(x :. t)@ is called an /abstraction pattern/. It matches any term
-- of type @('Bind' /a/ /b/)@. The result of matching the pattern
-- @(x :. t)@ against a value /y/'.'/s/ is to bind /x/ to a fresh name
-- and /t/ to a value such that /x/'.'/t/ = /y/'.'/s/.
-- 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 :. t <- ((\body -> open body (\a t -> (a,t))) -> (a, t))
 where
   a :. t = a . t
infixr 5 :.

-- | An alternative non-infix notation for @(@'.'@)@. This can be
-- useful when using qualified module names, because \"̈@Nominal..@\" is not
-- valid syntax.
abst :: (Bindable a, Nominal t) => a -> t -> Bind a t
abst = (.)

-- | 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 (Bind f body) k =
  atomlist_open body (\ys t -> k (f ys) 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 sup (Bind f body) k =
  atomlist_open_for_printing sup body (\ys t sup' -> k (f ys) t sup')

instance (Nominal a, Nominal t, Eq a, Eq t) => Eq (Bind a t) where
  Bind f1 body1 == Bind f2 body2 =
    case atomlist_merge body1 body2 of
      Nothing -> False
      Just bodies ->
        atomlist_open bodies $ \xs (t1, t2) ->
          t1 == t2 && f1 xs == f2 xs

instance (Bindable a, Nominal t) => Nominal (Bind a t) where
  π • (Bind f body) = Bind (π • f) (π • body)

instance (Bindable a, NominalSupport a, NominalSupport t) => NominalSupport (Bind a t) where
  support (Bind f body) = atomlist_open body $ \xs t ->
    support_deletes xs (support (f xs, 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 (Show, Eq, Ord, Generic, Nominal, 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 = nobinding

-- Base cases

instance Bindable Atom where
  binding = atom_binding

instance Bindable Bool where
  binding = basic_binding
  
instance Bindable Integer where
  binding = basic_binding
  
instance Bindable Int where
  binding = basic_binding
  
instance Bindable Char where
  binding = basic_binding
  
instance Bindable Double where
  binding = basic_binding
  
instance Bindable Float where
  binding = basic_binding
  
instance Bindable Ordering where
  binding = basic_binding
  
instance Bindable (Basic t) where
  binding = basic_binding

instance Bindable Literal where
  binding = basic_binding

instance (Nominal t) => Bindable (NoBind t) where
  binding = 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 (NominalBinder xs f) (NominalBinder ys g) k = NominalBinder (xs ++ ys) h where
  h zs = (k (a :*: b), zs'') where
    (a, zs') = f zs
    (b, zs'') = g 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 = undefined -- never occurs, because V1 is empty

instance GBindable U1 where
  gbinding a k = NominalBinder [] (\xs -> (k a, xs))

instance (GBindable a, GBindable b) => GBindable (a :*: b) where
  gbinding (a :*: b) k =
    binder_gpair (gbinding a id) (gbinding b id) k

instance (GBindable a, GBindable b) => GBindable (a :+: b) where
  gbinding (L1 a) k = gbinding a (\a -> k (L1 a))
  gbinding (R1 a) k = gbinding a (\a -> k (R1 a))

instance (GBindable a) => GBindable (M1 i c a) where
  gbinding (M1 a) k = gbinding a (\a -> k (M1 a))
  
instance (Bindable a) => GBindable (K1 i a) where
  gbinding (K1 a) k = binder_map k (K1 <$> binding a)

-- ----------------------------------------------------------------------
-- * Miscellaneous

-- | Function composition.
-- 
-- Since we hide (.) from the standard library, and the fully
-- qualified name of the "Prelude"'s dot operator, \"̈@Prelude..@\", is
-- not legal syntax, we provide '∘' as an alternate notation for
-- composition.
(∘) :: (b -> c) -> (a -> b) -> (a -> c)
(g ∘ f) x = g (f x)