{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}

-- | This module provides the class 'Atomic', which generalizes the
-- type 'Atom'. The purpose of this is to allow users to define more
-- than one type of atoms.
--
-- 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.Atomic where

import GHC.Generics

import Nominal.ConcreteNames
import Nominal.Atom
import Nominal.Nominal
import Nominal.NominalSupport
import Nominal.NominalShow
import Nominal.Bindable
import Nominal.Unsafe

-- ----------------------------------------------------------------------
-- * The 'Atomic' class

-- | A type class for atom types.
--
-- The suggested way to define a type of atoms is to define a new
-- empty type /t/ that is an instance of 'AtomKind'.  Optionally, a
-- list of suggested names for the new atoms can be provided.  (These
-- will be used as the names of bound variables unless otherwise
-- specified). Then 'AtomOfKind' /t/ is a new type of atoms.
-- 
-- > data VarName
-- > instance AtomKind VarName where
-- >   suggested_names = ["x", "y", "z"]
-- > type Variable = AtomOfKind VarName
class (Nominal a, NominalSupport a, Eq a, Ord a, Show a, Bindable a) => Atomic a where
  to_atom :: a -> Atom
  from_atom :: Atom -> a

  -- | The default variable names for the atom type.
  names :: a -> NameGen

instance Atomic Atom where
  to_atom :: Atom -> Atom
to_atom = Atom -> Atom
forall a. a -> a
id
  from_atom :: Atom -> Atom
from_atom = Atom -> Atom
forall a. a -> a
id
  names :: Atom -> NameGen
names Atom
a = NameGen
default_namegen

-- ----------------------------------------------------------------------
-- ** Basic operations

-- | Return the name of an atom.
atomic_show :: (Atomic a) => a -> String
atomic_show :: forall a. Atomic a => a -> String
atomic_show a
a = Atom -> String
atom_show (a -> Atom
forall a. Atomic a => a -> Atom
to_atom a
a)

-- ----------------------------------------------------------------------
-- ** Creation of fresh atoms in a scope

-- | Perform a computation in the presence of a fresh atom.
--
-- The correct use of this function is subject to
-- <#CONDITION Pitts's freshness condition>.
-- Thus, for example, the following uses are permitted:
--   
-- > with_fresh (\a -> a :. f a b c)
-- > with_fresh (\a -> f a == g a)
--
-- Here is an example of what is /not/ permitted:
--
-- > with_fresh (\a -> a)
--
-- See <#CONDITION "Pitts's freshness condition"> for more details.
with_fresh :: (Atomic a) => (a -> t) -> t
with_fresh :: forall a t. Atomic a => (a -> t) -> t
with_fresh a -> t
k = NameSuggestion -> (a -> t) -> t
forall a t. Atomic a => NameSuggestion -> (a -> t) -> t
with_fresh_namelist [] a -> t
k

-- | A version of 'with_fresh' that permits a suggested name to be
-- given to the atom. The name is only a suggestion, and will be
-- changed, if necessary, to avoid clashes.
--
-- The correct use of this function is subject to
-- <#CONDITION Pitts's freshness condition>.
with_fresh_named :: (Atomic a) => String -> (a -> t) -> t
with_fresh_named :: forall a t. Atomic a => String -> (a -> t) -> t
with_fresh_named String
n = IO a -> (a -> t) -> t
forall a b. IO a -> (a -> b) -> b
unsafe_with (String -> IO a
forall a. Atomic a => String -> IO a
fresh_named String
n)

-- | A version of 'with_fresh' that permits a list of suggested names
-- to be specified. The first suitable name in the list will be used
-- if possible.
--
-- The correct use of this function is subject to
-- <#CONDITION Pitts's freshness condition>.
with_fresh_namelist :: (Atomic a) => NameSuggestion -> (a -> t) -> t
with_fresh_namelist :: forall a t. Atomic a => NameSuggestion -> (a -> t) -> t
with_fresh_namelist NameSuggestion
ns a -> t
k =
  NameGen -> (Atom -> t) -> t
forall a. NameGen -> (Atom -> a) -> a
with_fresh_atom NameGen
ng (\Atom
a -> a -> t
k (Atom -> a
forall a. Atomic a => Atom -> a
from_atom Atom
a))
  where
    NameGen NameSuggestion
ns1 NameSuggestion -> NameSuggestion
ex = a -> NameGen
forall a. Atomic a => a -> NameGen
names ((a -> t) -> a
forall a t. (a -> t) -> a
un a -> t
k)
    ns2 :: NameSuggestion
ns2 = if NameSuggestion -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null NameSuggestion
ns then NameSuggestion
ns1 else NameSuggestion
ns
    ng :: NameGen
ng = NameSuggestion -> (NameSuggestion -> NameSuggestion) -> NameGen
NameGen NameSuggestion
ns2 NameSuggestion -> NameSuggestion
ex
    un :: (a -> t) -> a
    un :: forall a t. (a -> t) -> a
un = (a -> t) -> a
forall a. HasCallStack => a
undefined

-- ----------------------------------------------------------------------
-- ** Creation of fresh atoms globally

-- | Generate a globally fresh atom of the given atomic type.
fresh :: (Atomic a) => IO a
fresh :: forall a. Atomic a => IO a
fresh = NameSuggestion -> IO a
forall a. Atomic a => NameSuggestion -> IO a
fresh_namelist []

-- | A version of 'fresh' that that permits a suggested name to be
-- given to the atom. The name is only a suggestion, and will be
-- changed, if necessary, when the atom is bound.
fresh_named :: (Atomic a) => String -> IO a
fresh_named :: forall a. Atomic a => String -> IO a
fresh_named String
n = IO a
result
  where
    result :: IO a
result = do
      Atom
a <- String -> NameGen -> IO Atom
fresh_atom_named String
n NameGen
ng
      a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> a
forall a. Atomic a => Atom -> a
from_atom Atom
a)

    NameGen NameSuggestion
ns NameSuggestion -> NameSuggestion
ex = a -> NameGen
forall a. Atomic a => a -> NameGen
names (IO a -> a
forall a. IO a -> a
un IO a
result)
    ng :: NameGen
ng = NameSuggestion -> (NameSuggestion -> NameSuggestion) -> NameGen
NameGen [String
n] NameSuggestion -> NameSuggestion
ex
    un :: IO a -> a
    un :: forall a. IO a -> a
un = IO a -> a
forall a. HasCallStack => a
undefined

-- | A version of 'with_fresh' that permits a list of suggested names
-- to be specified. The first suitable name in the list will be used
-- if possible.
fresh_namelist :: (Atomic a) => NameSuggestion -> IO a
fresh_namelist :: forall a. Atomic a => NameSuggestion -> IO a
fresh_namelist NameSuggestion
ns = IO a
result
  where
    result :: IO a
result = do
      Atom
a <- NameGen -> IO Atom
fresh_atom NameGen
ng
      a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Atom -> a
forall a. Atomic a => Atom -> a
from_atom Atom
a)

    NameGen NameSuggestion
ns1 NameSuggestion -> NameSuggestion
ex = a -> NameGen
forall a. Atomic a => a -> NameGen
names (IO a -> a
forall a. IO a -> a
un IO a
result)
    ns2 :: NameSuggestion
ns2 = if NameSuggestion -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null NameSuggestion
ns then NameSuggestion
ns1 else NameSuggestion
ns
    ng :: NameGen
ng = NameSuggestion -> (NameSuggestion -> NameSuggestion) -> NameGen
NameGen NameSuggestion
ns2 NameSuggestion -> NameSuggestion
ex
    un :: IO a -> a
    un :: forall a. IO a -> a
un = IO a -> a
forall a. HasCallStack => a
undefined

-- $ Implementation note: the implementation of 'fresh_namelist'
-- differs slightly from that of 'with_fresh_namelist'. The function
-- 'fresh_namelist' generates a concrete name for the atom
-- immediately, whereas 'with_fresh_namelist' only does so on demand.
-- The idea is that most atoms generated by 'with_fresh_namelist' will
-- be bound immediately and their concrete name never displayed.

-- ----------------------------------------------------------------------
-- ** Convenience functions for abstraction

-- | A convenience function for constructing binders. We can write
--
-- > bind (\x -> t)
--
-- to denote the abstraction @(@/x/ ':.' /t/@)@, where /x/ is a fresh atom.
bind :: (Atomic a, Nominal t) => (a -> t) -> Bind a t
bind :: forall a t. (Atomic a, Nominal t) => (a -> t) -> Bind a t
bind a -> t
f = (a -> Bind a t) -> Bind a t
forall a t. Atomic a => (a -> t) -> t
with_fresh (\a
x -> a
x a -> t -> Bind a t
forall b a. (Nominal b, Bindable a) => a -> b -> Bind a b
:. a -> t
f a
x)

-- | A version of 'bind' that also takes a suggested name for the bound atom.
bind_named :: (Atomic a, Nominal t) => String -> (a -> t) -> Bind a t
bind_named :: forall a t. (Atomic a, Nominal t) => String -> (a -> t) -> Bind a t
bind_named String
n a -> t
f = String -> (a -> Bind a t) -> Bind a t
forall a t. Atomic a => String -> (a -> t) -> t
with_fresh_named String
n (\a
x -> a
x a -> t -> Bind a t
forall b a. (Nominal b, Bindable a) => a -> b -> Bind a b
:. a -> t
f a
x)

-- | A version of 'bind' that also take a list of suggested names for
-- the bound atom.
bind_namelist :: (Atomic a, Nominal t) => NameSuggestion -> (a -> t) -> Bind a t
bind_namelist :: forall a t.
(Atomic a, Nominal t) =>
NameSuggestion -> (a -> t) -> Bind a t
bind_namelist NameSuggestion
ns a -> t
f = NameSuggestion -> (a -> Bind a t) -> Bind a t
forall a t. Atomic a => NameSuggestion -> (a -> t) -> t
with_fresh_namelist NameSuggestion
ns (\a
x -> a
x a -> t -> Bind a t
forall b a. (Nominal b, Bindable a) => a -> b -> Bind a b
:. a -> t
f a
x)

-- ----------------------------------------------------------------------
-- ** Merging

-- | Convert an atomic binding to an atom binding.
to_bindatom :: (Atomic a, Nominal t) => Bind a t -> BindAtom t
to_bindatom :: forall a t. (Atomic a, Nominal t) => Bind a t -> BindAtom t
to_bindatom (a
a :. t
t) = Atom -> t -> BindAtom t
forall t. Atom -> t -> BindAtom t
atom_abst (a -> Atom
forall a. Atomic a => a -> Atom
to_atom a
a) t
t

-- | Convert an atom binding to an atomic binding.
from_bindatom :: (Atomic a, Nominal t) => BindAtom t -> Bind a t
from_bindatom :: forall a t. (Atomic a, Nominal t) => BindAtom t -> Bind a t
from_bindatom BindAtom t
body = BindAtom t -> (Atom -> t -> Bind a t) -> Bind a t
forall t s. Nominal t => BindAtom t -> (Atom -> t -> s) -> s
atom_open BindAtom t
body ((Atom -> t -> Bind a t) -> Bind a t)
-> (Atom -> t -> Bind a t) -> Bind a t
forall a b. (a -> b) -> a -> b
$ \Atom
a t
t -> (Atom -> a
forall a. Atomic a => Atom -> a
from_atom Atom
a a -> t -> Bind a t
forall b a. (Nominal b, Bindable a) => a -> b -> Bind a b
:. t
t)

-- | Sometimes, it is necessary to open two abstractions, using the
-- /same/ fresh name for both of them. An example of this is the
-- typing rule for lambda abstraction in dependent type theory:
--
-- >           Gamma, x:t  |-  e : s
-- >      ------------------------------------
-- >        Gamma |-  Lam (x:.e) : Pi t (x:.s)
--
-- In the bottom-up reading of this rule, we are given the terms @Lam@
-- /body/ and @Pi@ /t/ /body'/, and we require a fresh name /x/ and
-- terms /e/, /s/ such that /body/ = (/x/ ':.' /e/) and
-- /body'/ = (/x/ ':.' /s/).  Crucially, the same atom /x/ should be used
-- in both /e/ and /s/, because we subsequently need to check that /e/
-- has type /s/ in some scope that is common to /e/ and /s/.
--
-- The 'merge' primitive permits us to deal with such situations.  Its
-- defining property is
--
-- > merge (x :. e) (x :. s) = (x :. (e,s)).
--
-- We can therefore solve the above problem:
--
-- > let (x :. (e,s)) = merge body body' in ....
--
-- Moreover, the 'merge' primitive can be used to define other
-- merge-like functionality. For example, it is easy to define a
-- function
--
-- > merge_list :: (Atomic a, Nominal t) => [Bind a t] -> Bind a [t]
--
-- in terms of it.
--
-- Semantically, the 'merge' operation implements the isomorphism of
-- nominal sets [/A/]/T/ × [/A/]/S/ = [/A/](/T/ × /S/).
--
-- If /x/ and /y/ are atoms with user-suggested concrete names and
--
-- > (z :. (t',s')) = merge (x :. t) (y :. s),
--
-- then /z/ will be preferably given the concrete name of /x/, but the
-- concrete name of /y/ will be used if the name of /x/ would cause a
-- clash.
merge :: (Atomic a, Nominal t, Nominal s) => Bind a t -> Bind a s -> Bind a (t,s)
merge :: forall a t s.
(Atomic a, Nominal t, Nominal s) =>
Bind a t -> Bind a s -> Bind a (t, s)
merge Bind a t
at Bind a s
as = BindAtom (t, s) -> Bind a (t, s)
forall a t. (Atomic a, Nominal t) => BindAtom t -> Bind a t
from_bindatom (BindAtom t -> BindAtom s -> BindAtom (t, s)
forall t s.
(Nominal t, Nominal s) =>
BindAtom t -> BindAtom s -> BindAtom (t, s)
atom_merge (Bind a t -> BindAtom t
forall a t. (Atomic a, Nominal t) => Bind a t -> BindAtom t
to_bindatom Bind a t
at) (Bind a s -> BindAtom s
forall a t. (Atomic a, Nominal t) => Bind a t -> BindAtom t
to_bindatom Bind a s
as))

-- ----------------------------------------------------------------------
-- * Multiple atom types

-- | An atom kind is a type-level constant (typically an empty type)
-- that is an instance of the 'AtomKind' class. An atom kind is
-- optionally equipped with a list of suggested names for this kind of
-- atom.  For example:
--
-- > data VarName
-- > instance AtomKind VarName where
-- >   suggested_names _ = ["x", "y", "z"]
--
-- > data TypeName
-- > instance AtomKind TypeName where
-- >   suggested_names _ = ["a", "b", "c"]
--
-- It is possible to have infinitely many atom kinds, for example:
--
-- > data Zero
-- > data Succ a
-- > instance AtomKind Zero
-- > instance AtomKind (Succ a)
--
-- Then Zero, Succ Zero, Succ (Succ Zero), etc., will all be atom kinds.
class AtomKind a where
  -- | An optional list of default names for this kind of atom.
  suggested_names :: a -> NameSuggestion
  suggested_names a
a = NameSuggestion
default_names

  -- | An optional function for generating infinitely many distinct
  -- names from a finite list of suggestions. The default behavior is
  -- to append numerical subscripts. For example, the names
  -- @[x, y, z]@ are by default expanded to @[x, y, z, x₁, y₁, z₁,
  -- x₂, y₂, …]@, using Unicode for the subscripts.  To use a a
  -- different naming convention, redefine 'expand_names'.
  -- 
  -- It is not strictly necessary for all of the returned names to be
  -- distinct; it is sufficient that there are infinitely many
  -- distinct ones.
  --
  -- Example: the following generates new variable names by appending
  -- primes instead of subscripts:
  --
  -- > expand_names _ xs = ys
  -- >   where ys = xs ++ map (++ "'") ys
  expand_names :: a -> NameSuggestion -> [String]
  expand_names a
a = NameSuggestion -> NameSuggestion
expand_default

-- | The type of atoms of a given kind. For example:
--
-- > type Variable = AtomOfKind VarName
-- > type Type = AtomOfKind TypeName
newtype AtomOfKind a = AtomOfKind Atom
  deriving (AtomOfKind a -> AtomOfKind a -> Bool
(AtomOfKind a -> AtomOfKind a -> Bool)
-> (AtomOfKind a -> AtomOfKind a -> Bool) -> Eq (AtomOfKind a)
forall a. AtomOfKind a -> AtomOfKind a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. AtomOfKind a -> AtomOfKind a -> Bool
== :: AtomOfKind a -> AtomOfKind a -> Bool
$c/= :: forall a. AtomOfKind a -> AtomOfKind a -> Bool
/= :: AtomOfKind a -> AtomOfKind a -> Bool
Eq, Eq (AtomOfKind a)
Eq (AtomOfKind a) =>
(AtomOfKind a -> AtomOfKind a -> Ordering)
-> (AtomOfKind a -> AtomOfKind a -> Bool)
-> (AtomOfKind a -> AtomOfKind a -> Bool)
-> (AtomOfKind a -> AtomOfKind a -> Bool)
-> (AtomOfKind a -> AtomOfKind a -> Bool)
-> (AtomOfKind a -> AtomOfKind a -> AtomOfKind a)
-> (AtomOfKind a -> AtomOfKind a -> AtomOfKind a)
-> Ord (AtomOfKind a)
AtomOfKind a -> AtomOfKind a -> Bool
AtomOfKind a -> AtomOfKind a -> Ordering
AtomOfKind a -> AtomOfKind a -> AtomOfKind a
forall a. Eq (AtomOfKind a)
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 a. AtomOfKind a -> AtomOfKind a -> Bool
forall a. AtomOfKind a -> AtomOfKind a -> Ordering
forall a. AtomOfKind a -> AtomOfKind a -> AtomOfKind a
$ccompare :: forall a. AtomOfKind a -> AtomOfKind a -> Ordering
compare :: AtomOfKind a -> AtomOfKind a -> Ordering
$c< :: forall a. AtomOfKind a -> AtomOfKind a -> Bool
< :: AtomOfKind a -> AtomOfKind a -> Bool
$c<= :: forall a. AtomOfKind a -> AtomOfKind a -> Bool
<= :: AtomOfKind a -> AtomOfKind a -> Bool
$c> :: forall a. AtomOfKind a -> AtomOfKind a -> Bool
> :: AtomOfKind a -> AtomOfKind a -> Bool
$c>= :: forall a. AtomOfKind a -> AtomOfKind a -> Bool
>= :: AtomOfKind a -> AtomOfKind a -> Bool
$cmax :: forall a. AtomOfKind a -> AtomOfKind a -> AtomOfKind a
max :: AtomOfKind a -> AtomOfKind a -> AtomOfKind a
$cmin :: forall a. AtomOfKind a -> AtomOfKind a -> AtomOfKind a
min :: AtomOfKind a -> AtomOfKind a -> AtomOfKind a
Ord, (forall x. AtomOfKind a -> Rep (AtomOfKind a) x)
-> (forall x. Rep (AtomOfKind a) x -> AtomOfKind a)
-> Generic (AtomOfKind a)
forall x. Rep (AtomOfKind a) x -> AtomOfKind a
forall x. AtomOfKind a -> Rep (AtomOfKind a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (AtomOfKind a) x -> AtomOfKind a
forall a x. AtomOfKind a -> Rep (AtomOfKind a) x
$cfrom :: forall a x. AtomOfKind a -> Rep (AtomOfKind a) x
from :: forall x. AtomOfKind a -> Rep (AtomOfKind a) x
$cto :: forall a x. Rep (AtomOfKind a) x -> AtomOfKind a
to :: forall x. Rep (AtomOfKind a) x -> AtomOfKind a
Generic, Nominal (AtomOfKind a)
Nominal (AtomOfKind a) =>
(AtomOfKind a -> NominalBinder (AtomOfKind a))
-> Bindable (AtomOfKind a)
AtomOfKind a -> NominalBinder (AtomOfKind a)
forall a. Nominal a => (a -> NominalBinder a) -> Bindable a
forall a. AtomKind a => Nominal (AtomOfKind a)
forall a.
AtomKind a =>
AtomOfKind a -> NominalBinder (AtomOfKind a)
$cbinding :: forall a.
AtomKind a =>
AtomOfKind a -> NominalBinder (AtomOfKind a)
binding :: AtomOfKind a -> NominalBinder (AtomOfKind a)
Bindable)

instance (AtomKind a) => Nominal (AtomOfKind a) where
  NominalPermutation
π • :: NominalPermutation -> AtomOfKind a -> AtomOfKind a
• (AtomOfKind Atom
a) = Atom -> AtomOfKind a
forall a. Atom -> AtomOfKind a
AtomOfKind (NominalPermutation
π NominalPermutation -> Atom -> Atom
forall t. Nominal t => NominalPermutation -> t -> t
• Atom
a)

instance (AtomKind a) => NominalSupport (AtomOfKind a) where
  support :: AtomOfKind a -> Support
support (AtomOfKind Atom
a) = Atom -> Support
forall t. NominalSupport t => t -> Support
support Atom
a

instance (AtomKind a) => NominalShow (AtomOfKind a) where
  showsPrecSup :: Support -> Int -> AtomOfKind a -> ShowS
showsPrecSup Support
sup Int
d AtomOfKind a
t = String -> ShowS
showString (AtomOfKind a -> String
forall a. Atomic a => a -> String
atomic_show AtomOfKind a
t)

instance (AtomKind a) => Show (AtomOfKind a) where
  show :: AtomOfKind a -> String
show = AtomOfKind a -> String
forall a. Atomic a => a -> String
atomic_show

instance (AtomKind a) => Atomic (AtomOfKind a) where
  to_atom :: AtomOfKind a -> Atom
to_atom (AtomOfKind Atom
a) = Atom
a
  from_atom :: Atom -> AtomOfKind a
from_atom Atom
a = Atom -> AtomOfKind a
forall a. Atom -> AtomOfKind a
AtomOfKind Atom
a
  names :: AtomOfKind a -> NameGen
names AtomOfKind a
f = AtomOfKind a -> NameGen
forall a. AtomKind a => AtomOfKind a -> NameGen
atomofkind_names AtomOfKind a
f

-- | Return the list of default names associated with the /kind/ of
-- the given atom (not the name(s) of the atom itself).
atomofkind_names :: (AtomKind a) => AtomOfKind a -> NameGen
atomofkind_names :: forall a. AtomKind a => AtomOfKind a -> NameGen
atomofkind_names AtomOfKind a
f = NameSuggestion -> (NameSuggestion -> NameSuggestion) -> NameGen
NameGen NameSuggestion
ns NameSuggestion -> NameSuggestion
ex
  where
    ns :: NameSuggestion
ns = a -> NameSuggestion
forall a. AtomKind a => a -> NameSuggestion
suggested_names (AtomOfKind a -> a
forall a. AtomOfKind a -> a
un AtomOfKind a
f)
    ex :: NameSuggestion -> NameSuggestion
ex = a -> NameSuggestion -> NameSuggestion
forall a. AtomKind a => a -> NameSuggestion -> NameSuggestion
expand_names (AtomOfKind a -> a
forall a. AtomOfKind a -> a
un AtomOfKind a
f)
    un :: AtomOfKind a -> a
    un :: forall a. AtomOfKind a -> a
un = AtomOfKind a -> a
forall a. HasCallStack => a
undefined