----------------------------------------------------------------------

-- |

-- Module      :  Unbound.LocallyNameless

-- License     :  BSD-like (see LICENSE)

-- Maintainer  :  Brent Yorgey <byorgey@cis.upenn.edu>

-- Stability   :  experimental

-- Portability :  GHC only (-XKitchenSink)

--

-- A generic implementation of standard functions dealing with names

-- and binding structure (alpha equivalence, free variable

-- calculation, capture-avoiding substitution, name permutation, ...)

-- using a locally nameless representation.

--

-- Normal users of this library should only need to import this

-- module.  In particular, this module is careful to export only an

-- abstract interface with various safety guarantees.  Power users who

-- wish to have access to the internals of the library (at the risk of

-- shooting oneself in the foot) can directly import the various

-- implementation modules such as "Unbound.LocallyNameless.Name" and

-- so on.

--

-- /Ten-second tutorial/: use the type combinators 'Bind', 'Embed',

-- 'Rebind', 'Rec', 'TRec', and 'Shift' to specify the binding

-- structure of your data types.  Then use Template Haskell to derive

-- generic representations for your types:

--

-- > $(derive [''Your, ''Types, ''Here])

--

-- Finally, declare 'Alpha' and 'Subst' instances for your types.

-- Then you can go to town using all the generically-derived

-- operations like 'aeq', 'fv', 'subst', and so on.

--

-- For more information, see the more in-depth literate Haskell

-- tutorial in the @tutorial@ directory (which can be obtained as part

-- of the library source package: @cabal unpack unbound@) and the

-- examples in the @example@ directory.

--

-- See also: Stephanie Weirich, Brent A. Yorgey, and Tim Sheard.

-- /Binders Unbound/. ICFP'11, September 2011, Tokyo, Japan. <http://www.cis.upenn.edu/~byorgey/papers/binders-unbound.pdf>.

----------------------------------------------------------------------


module Unbound.LocallyNameless
  ( -- * Names

    Name, AnyName(..),

    -- ** Constructing and destructing free names

    integer2Name, string2Name, s2n, makeName,
    name2Integer, name2String, anyName2Integer, anyName2String,
    -- ** Dealing with name sorts

    translate, toSortedName,

    -- * Type combinators for specifying binding structure

    --

    -- | 'Bind', 'Embed', 'Rebind', 'Rec', 'TRec', and 'Shift' are

    --   special types provided by Unbound for use in specifying the

    --   binding structure of your data types.

    --

    --   An important distinction to keep in mind is the difference

    --   between /term types/ and /pattern types/.

    --

    --   * /Term types/ are normal types whose values represent data in

    --     your program.  Any 'Name's occurring in term types are

    --     either free variables, or /references/ to binders.

    --

    --   * /Pattern types/ are types which may be used on the left

    --     hand side of a 'Bind'.  They /bind/ names, that is, any

    --     'Name's occurring in pattern types are /binding sites/ to

    --     which other names may refer.

    --

    --   'Name' may be used as both a term type (where it represents a

    --   free variable/reference) and a pattern type (where it

    --   represents a binding site).

    --

    --   Any first-order algebraic data type (/i.e./ one containing no

    --   functions) which contains only term types may be used as a

    --   term type, and likewise for algebraic data types containing

    --   only pattern types. For example,

    --

    --   > (Name, [Name])

    --

    --   may be used as either a term type or a pattern type. On the

    --   other hand,

    --

    --   > (Bind Name Name, Name)

    --

    --   may only be used as a term type, since @Bind Name Name@ is a

    --   term type and not a pattern type.

    --

    --   We adopt the convention that the type variable @t@ stands for

    --   term types, and the type variable @p@ stands for pattern

    --   types.  It would be nicer if we could actually use Haskell's

    --   type system to enforce the distinction, but for various

    --   technical reasons (involving the RepLib generic programming

    --   framework which is used in the implementation), we cannot.

    --   Or at least, we are not sufficiently clever to see how.


    -- ** Bind


    Bind,

    -- *** Bind constructors

    bind,
    permbind,
    setbind,
    setbindAny,


    -- *** Bind destructors


    -- | Directly pattern-matching on 'Bind' values is not allowed,

    --   but there are quite a few different ways to safely \"open\" a

    --   binding.  (If you want direct, unsafe access to the

    --   components of a binding --- e.g. to write a function to

    --   compute the size of terms that ignores all names --- you can

    --   directly import "Unbound.LocallyNameless.Ops" and use the

    --   'unsafeUnbind' function.)

    unbind,
    lunbind,

    -- *** Simultaneous unbinding


    -- | Sometimes one may wish to open several bindings using /same/

    --   names for their binding variables --- for example, when

    --   checking equality of terms involving binders, so that the

    --   free variables in the bodies will match appropriately during

    --   recursive calls.  Opening two bindings simultaneously is

    --   accomplished with 'unbind2' (which picks globally fresh

    --   names) and 'lunbind2' (which picks /locally/ fresh names, see

    --   the 'LFresh' documentation for more information).  'unbind3'

    --   and 'lunbind3' open three bindings simultaneously.  In

    --   principle, of course, @unbindN@ and @lunbindN@ can be easily

    --   implemented for any @N@; please let the maintainers know if

    --   for some reason you would like an N > 3.

    unbind2, unbind3,
    lunbind2, lunbind3,

    unbind2Plus, unbind3Plus,
    lunbind2Plus, lunbind3Plus,

    -- ** Embed


    Embed(..),

    embed, unembed,

    -- ** Rebind


    Rebind,

    rebind, unrebind,

    -- ** Rec

    Rec,
    rec, unrec,

    -- ** TRec

    TRec,
    trec, untrec, luntrec,

    -- ** Shift

    Shift(..),

    -- * Generically derived operations


    -- | This section lists a number of operations which are derived

    --   generically for any types whose binding structure is

    --   specified via the type combinators described in the previous

    --   section.


    -- ** Alpha-equivalence

    aeq, aeqBinders,
    acompare,

    -- ** Variable calculations


    -- | Functions for computing the free variables or binding

    --   variables of a term or pattern.  Note that all these

    --   functions may return an arbitrary /collection/, which

    --   includes lists, sets, and multisets.

    fv, fvAny, patfv, patfvAny, binders, bindersAny,

    -- *** Collections

    Collection(..), Multiset(..),

    -- ** Substitution


    -- | Capture-avoiding substitution.

    Subst(..), SubstName(..),substBind,

    -- ** Permutations


    Perm,

    -- *** Working with permutations

    single, compose, apply, support, isid, join, empty, restrict, mkPerm,

    -- *** Permuting terms

    swaps, swapsEmbeds, swapsBinders,

    -- * Freshness


    -- | When opening a term-level binding ('Bind' or 'TRec'), fresh

    --   names must be generated for the binders of its pattern.

    --   Fresh names can be generated according to one of two

    --   strategies: names can be /globally/ fresh (not conflicting

    --   with any other generated names, ever; see 'Fresh') or

    --   /locally/ fresh (not conflicting only with a specific set of

    --   \"currently in-scope\" names; see 'LFresh').  Generating

    --   globally fresh names is simpler and suffices for many

    --   applications.  Generating locally fresh names tends to be

    --   useful when the names are for human consumption, e.g. when

    --   implementing a pretty-printer.


    -- ** Global freshness

    freshen,

    -- *** The @Fresh@ class

    Fresh(..),

    -- *** The @FreshM@ monad


    -- | The @FreshM@ monad provides a concrete implementation of the

    --   'Fresh' type class.  The @FreshMT@ monad transformer variant

    --   can be freely combined with other standard monads and monad

    --   transformers from the @transformers@ library.


    FreshM, runFreshM,
    FreshMT, runFreshMT,

    -- ** Local freshness

    lfreshen,

    -- *** The @LFresh@ class

    LFresh(..),

    -- *** The @LFreshM@ monad


    -- | The @LFreshM@ monad provides a concrete implementation of the

    --   'LFresh' type class.  The @LFreshMT@ monad transformer variant

    --   can be freely combined with other standard monads and monad

    --   transformers from the @transformers@ library.


    LFreshM, runLFreshM,
    LFreshMT, runLFreshMT,

    -- * The @Alpha@ class

    Alpha(..),

    -- * Re-exported RepLib API for convenience


    module Generics.RepLib,

    -- * Pay no attention to the man behind the curtain


    -- | These type representation objects are exported so they can be

    --   referenced by auto-generated code.  Please pretend they do not

    --   exist.

    rName, rGenBind, rRebind, rEmbed, rRec, rShift
) where

import Unbound.LocallyNameless.Name
import Unbound.LocallyNameless.Fresh
import Unbound.LocallyNameless.Types
import Unbound.LocallyNameless.Alpha
import Unbound.LocallyNameless.Subst
import Unbound.LocallyNameless.Ops
import Unbound.Util
import Unbound.PermM

import Generics.RepLib