{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}

-- | This module provides the 'Nominal' type class. A type is
-- 'Nominal' if the group of finitely supported permutations of atoms
-- acts on it. We can abstract over an atom in such a type.
--
-- We also provide some generic programming so that instances of
-- 'Nominal' can be automatically derived in most 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.Nominal where

import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics

import Nominal.ConcreteNames
import Nominal.Atom
import Nominal.Permutation

-- ----------------------------------------------------------------------
-- * The Nominal class

-- | A type is nominal if the group of finitely supported permutations
-- of atoms acts on it.
--
-- 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 t where
  -- | Apply a permutation of atoms to a term.
  (•) :: NominalPermutation -> t -> t

  default (•) :: (Generic t, GNominal (Rep t)) => NominalPermutation -> t -> t
  NominalPermutation
π • t
x = Rep t Any -> t
forall a x. Generic a => Rep a x -> a
forall x. Rep t x -> t
to (NominalPermutation -> Rep t Any -> Rep t Any
forall a. NominalPermutation -> Rep t a -> Rep t a
forall (f :: * -> *) a.
GNominal f =>
NominalPermutation -> f a -> f a
gbullet NominalPermutation
π (t -> Rep t Any
forall x. t -> Rep t x
forall a x. Generic a => a -> Rep a x
from t
x))

-- ----------------------------------------------------------------------
-- * Deferred permutation

-- | 'Defer' /t/ is the type /t/, but equipped with an explicit substitution.
-- This is used to cache substitutions so that they can be optimized
-- and applied all at once.
data Defer t = Defer NominalPermutation t

-- | Apply a deferred permutation.
force :: (Nominal t) => Defer t -> t
force :: forall t. Nominal t => Defer t -> t
force (Defer NominalPermutation
sigma t
t) = NominalPermutation
sigma NominalPermutation -> t -> t
forall t. Nominal t => NominalPermutation -> t -> t
• t
t

instance Nominal (Defer t) where
  -- This is where 'Defer' pays off. Rather than using 'force',
  -- we compile the permutations for later efficient use.
  NominalPermutation
π • :: NominalPermutation -> Defer t -> Defer t
• (Defer NominalPermutation
sigma t
t) = NominalPermutation -> t -> Defer t
forall t. NominalPermutation -> t -> Defer t
Defer (NominalPermutation -> NominalPermutation -> NominalPermutation
perm_composeR NominalPermutation
π NominalPermutation
sigma) t
t
  
-- ----------------------------------------------------------------------
-- * Atom abstraction

-- | 'BindAtom' /t/ is the type of atom abstractions, denoted [a]t in
-- the nominal logic literature. Its elements are of the form (/a/:./v/)
-- modulo alpha-equivalence. For full technical details on what this
-- means, see Definition 4 of [Pitts 2002].
--
-- Implementation note: we currently use an HOAS encoding, as this
-- turns out to be far more efficient (both in time and memory usage)
-- than the alternatives. An important invariant of the HOAS encoding
-- is that the underlying function must only be applied to /fresh/
-- atoms.
data BindAtom t = BindAtom NameGen (Atom -> Defer t)

-- | Atom abstraction: 'atom_abst' /a/ /t/ represents the equivalence
-- class of pairs (/a/,/t/) modulo alpha-equivalence. We first define
-- this for 'Atom' and later generalize to other 'Atomic' types.
atom_abst :: Atom -> t -> BindAtom t
atom_abst :: forall t. Atom -> t -> BindAtom t
atom_abst Atom
a t
t = NameGen -> (Atom -> Defer t) -> BindAtom t
forall t. NameGen -> (Atom -> Defer t) -> BindAtom t
BindAtom (Atom -> NameGen
atom_names Atom
a) (\Atom
x -> NominalPermutation -> t -> Defer t
forall t. NominalPermutation -> t -> Defer t
Defer (Atom -> Atom -> NominalPermutation
perm_swap Atom
a Atom
x) t
t)

-- | Destructor for atom abstractions. If /m/ = /y/:./s/, the term
-- 
-- > open m (\x t -> body)
--
-- binds /x/ to a fresh name and /t/ to a term such that /x/:./t/ = /y/:./s/.
-- 
-- The correct use of this function is subject to Pitts's freshness
-- condition.
atom_open :: (Nominal t) => BindAtom t -> (Atom -> t -> s) -> s
atom_open :: forall t s. Nominal t => BindAtom t -> (Atom -> t -> s) -> s
atom_open (BindAtom NameGen
ng Atom -> Defer t
f) Atom -> t -> s
k =
  NameGen -> (Atom -> s) -> s
forall a. NameGen -> (Atom -> a) -> a
with_fresh_atom NameGen
ng (\Atom
a -> Atom -> t -> s
k Atom
a (Defer t -> t
forall t. Nominal t => Defer t -> t
force (Atom -> Defer t
f Atom
a)))

instance (Nominal t, Eq t) => Eq (BindAtom t) where
  BindAtom t
b1 == :: BindAtom t -> BindAtom t -> Bool
== BindAtom t
b2 = BindAtom (t, t) -> (Atom -> (t, t) -> Bool) -> Bool
forall t s. Nominal t => BindAtom t -> (Atom -> t -> s) -> s
atom_open (BindAtom t -> BindAtom t -> BindAtom (t, t)
forall t s.
(Nominal t, Nominal s) =>
BindAtom t -> BindAtom s -> BindAtom (t, s)
atom_merge BindAtom t
b1 BindAtom t
b2) ((Atom -> (t, t) -> Bool) -> Bool)
-> (Atom -> (t, t) -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \Atom
a (t
t1,t
t2) -> t
t1 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
t2

instance (Nominal t) => Nominal (BindAtom t) where
  NominalPermutation
π • :: NominalPermutation -> BindAtom t -> BindAtom t
• (BindAtom NameGen
n Atom -> Defer t
f) = NameGen -> (Atom -> Defer t) -> BindAtom t
forall t. NameGen -> (Atom -> Defer t) -> BindAtom t
BindAtom NameGen
n (\Atom
x -> NominalPermutation
π NominalPermutation -> Defer t -> Defer t
forall t. Nominal t => NominalPermutation -> t -> t
• (Atom -> Defer t
f Atom
x))

-- | Merge two abstractions. The defining property is
--
-- > merge (x :. t) (x :. s) = (x :. (t,s))
atom_merge :: (Nominal t, Nominal s) => BindAtom t -> BindAtom s -> BindAtom (t,s)
atom_merge :: forall t s.
(Nominal t, Nominal s) =>
BindAtom t -> BindAtom s -> BindAtom (t, s)
atom_merge (BindAtom NameGen
ng Atom -> Defer t
f) (BindAtom NameGen
ng' Atom -> Defer s
g) = NameGen -> (Atom -> Defer (t, s)) -> BindAtom (t, s)
forall t. NameGen -> (Atom -> Defer t) -> BindAtom t
BindAtom NameGen
ng'' Atom -> Defer (t, s)
h where
  ng'' :: NameGen
ng'' = NameGen -> NameGen -> NameGen
combine_names NameGen
ng NameGen
ng'
  h :: Atom -> Defer (t, s)
h Atom
x = NominalPermutation -> (t, s) -> Defer (t, s)
forall t. NominalPermutation -> t -> Defer t
Defer NominalPermutation
perm_identity (Defer t -> t
forall t. Nominal t => Defer t -> t
force (Atom -> Defer t
f Atom
x), Defer s -> s
forall t. Nominal t => Defer t -> t
force (Atom -> Defer s
g Atom
x))

-- ----------------------------------------------------------------------
-- * Basic types

-- | A /basic/ or /non-nominal/ type is a type whose elements cannot
-- contain any atoms. Typical examples are base types, such as 'Integer'
-- or 'Bool', and other types constructed exclusively from them,
-- such as @['Integer']@ or @'Bool' -> 'Bool'@. On such types, the
-- nominal structure is trivial, i.e., @π • /x/ = /x/@ for all /x/.
--
-- For convenience, we define 'Basic' as a wrapper around such types,
-- which will automatically generate appropriate instances of
-- 'Nominal', 'NominalSupport', 'NominalShow', and 'Bindable'. You can
-- use it, for example, like this:
--
-- > type Term = Var Atom | Const (Basic Int) | App Term Term
--
-- Some common base types, including 'Bool', 'Char', 'Int', 'Integer',
-- 'Double', 'Float', and 'Ordering' are already instances of the
-- relevant type classes, and do not need to be wrapped in 'Basic'.
--
-- The use of 'Basic' can sometimes have a performance advantage. For
-- example, @'Basic' 'String'@ is a more efficient 'Nominal' instance
-- than 'String'. Although they are semantically equivalent, the use
-- of 'Basic' prevents having to traverse the string to check each
-- character for atoms that are clearly not there.
newtype Basic t = Basic t
  deriving (Int -> Basic t -> ShowS
[Basic t] -> ShowS
Basic t -> String
(Int -> Basic t -> ShowS)
-> (Basic t -> String) -> ([Basic t] -> ShowS) -> Show (Basic t)
forall t. Show t => Int -> Basic t -> ShowS
forall t. Show t => [Basic t] -> ShowS
forall t. Show t => Basic t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Basic t -> ShowS
showsPrec :: Int -> Basic t -> ShowS
$cshow :: forall t. Show t => Basic t -> String
show :: Basic t -> String
$cshowList :: forall t. Show t => [Basic t] -> ShowS
showList :: [Basic t] -> ShowS
Show, Basic t -> Basic t -> Bool
(Basic t -> Basic t -> Bool)
-> (Basic t -> Basic t -> Bool) -> Eq (Basic t)
forall t. Eq t => Basic t -> Basic t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => Basic t -> Basic t -> Bool
== :: Basic t -> Basic t -> Bool
$c/= :: forall t. Eq t => Basic t -> Basic t -> Bool
/= :: Basic t -> Basic t -> Bool
Eq, Eq (Basic t)
Eq (Basic t) =>
(Basic t -> Basic t -> Ordering)
-> (Basic t -> Basic t -> Bool)
-> (Basic t -> Basic t -> Bool)
-> (Basic t -> Basic t -> Bool)
-> (Basic t -> Basic t -> Bool)
-> (Basic t -> Basic t -> Basic t)
-> (Basic t -> Basic t -> Basic t)
-> Ord (Basic t)
Basic t -> Basic t -> Bool
Basic t -> Basic t -> Ordering
Basic t -> Basic t -> Basic 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 (Basic t)
forall t. Ord t => Basic t -> Basic t -> Bool
forall t. Ord t => Basic t -> Basic t -> Ordering
forall t. Ord t => Basic t -> Basic t -> Basic t
$ccompare :: forall t. Ord t => Basic t -> Basic t -> Ordering
compare :: Basic t -> Basic t -> Ordering
$c< :: forall t. Ord t => Basic t -> Basic t -> Bool
< :: Basic t -> Basic t -> Bool
$c<= :: forall t. Ord t => Basic t -> Basic t -> Bool
<= :: Basic t -> Basic t -> Bool
$c> :: forall t. Ord t => Basic t -> Basic t -> Bool
> :: Basic t -> Basic t -> Bool
$c>= :: forall t. Ord t => Basic t -> Basic t -> Bool
>= :: Basic t -> Basic t -> Bool
$cmax :: forall t. Ord t => Basic t -> Basic t -> Basic t
max :: Basic t -> Basic t -> Basic t
$cmin :: forall t. Ord t => Basic t -> Basic t -> Basic t
min :: Basic t -> Basic t -> Basic t
Ord)

-- ----------------------------------------------------------------------
-- * Nominal instances

-- $ Most of the time, instances of 'Nominal' should be derived using
-- @deriving (Generic, Nominal)@, as in this example:
--
-- > {-# LANGUAGE DeriveGeneric #-}
-- > {-# LANGUAGE DeriveAnyClass #-}
-- >
-- > data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
-- >   deriving (Generic, Nominal)
--
-- In the case of non-nominal types (typically base types such as
-- 'Double'), a 'Nominal' instance can be defined using
-- 'basic_action':
--
-- > instance Nominal MyType where
-- >   (•) = basic_action

-- | A helper function for defining 'Nominal' instances
-- for non-nominal types.
basic_action :: NominalPermutation -> t -> t
basic_action :: forall t. NominalPermutation -> t -> t
basic_action NominalPermutation
π t
t = t
t

-- Base cases

instance Nominal Atom where
  • :: NominalPermutation -> Atom -> Atom
(•) = NominalPermutation -> Atom -> Atom
perm_apply_atom

instance Nominal Bool where
  • :: NominalPermutation -> Bool -> Bool
(•) = NominalPermutation -> Bool -> Bool
forall t. NominalPermutation -> t -> t
basic_action

instance Nominal Integer where
  • :: NominalPermutation -> Integer -> Integer
(•) = NominalPermutation -> Integer -> Integer
forall t. NominalPermutation -> t -> t
basic_action

instance Nominal Int where
  • :: NominalPermutation -> Int -> Int
(•) = NominalPermutation -> Int -> Int
forall t. NominalPermutation -> t -> t
basic_action

instance Nominal Char where
  • :: NominalPermutation -> Char -> Char
(•) = NominalPermutation -> Char -> Char
forall t. NominalPermutation -> t -> t
basic_action

instance Nominal Double where
  • :: NominalPermutation -> Double -> Double
(•) = NominalPermutation -> Double -> Double
forall t. NominalPermutation -> t -> t
basic_action

instance Nominal Float where
  • :: NominalPermutation -> Float -> Float
(•) = NominalPermutation -> Float -> Float
forall t. NominalPermutation -> t -> t
basic_action

instance Nominal Ordering where
  • :: NominalPermutation -> Ordering -> Ordering
(•) = NominalPermutation -> Ordering -> Ordering
forall t. NominalPermutation -> t -> t
basic_action

instance Nominal (Basic t) where
  • :: NominalPermutation -> Basic t -> Basic t
(•) = NominalPermutation -> Basic t -> Basic t
forall t. NominalPermutation -> t -> t
basic_action

-- Generic instances

instance (Nominal t) => Nominal [t]
instance Nominal ()
instance (Nominal t, Nominal s) => Nominal (t,s)
instance (Nominal t, Nominal s, Nominal r) => Nominal (t,s,r)
instance (Nominal t, Nominal s, Nominal r, Nominal q) => Nominal (t,s,r,q)
instance (Nominal t, Nominal s, Nominal r, Nominal q, Nominal p) => Nominal (t,s,r,q,p)
instance (Nominal t, Nominal s, Nominal r, Nominal q, Nominal p, Nominal o) => Nominal (t,s,r,q,p,o)
instance (Nominal t, Nominal s, Nominal r, Nominal q, Nominal p, Nominal o, Nominal n) => Nominal (t,s,r,q,p,o,n)
instance (Nominal a) => Nominal (Maybe a)
instance (Nominal a, Nominal b) => Nominal (Either a b)


-- Special instances

instance (Nominal t, Nominal s) => Nominal (t -> s) where
  NominalPermutation
π • :: NominalPermutation -> (t -> s) -> t -> s
• t -> s
f = \t
x -> NominalPermutation
π NominalPermutation -> s -> s
forall t. Nominal t => NominalPermutation -> t -> t
• (t -> s
f (NominalPermutation
π' NominalPermutation -> t -> t
forall t. Nominal t => NominalPermutation -> t -> t
• t
x))
    where
      π' :: NominalPermutation
π' = NominalPermutation -> NominalPermutation
perm_invert NominalPermutation
π

instance (Ord k, Nominal k, Nominal v) => Nominal (Map k v) where
  NominalPermutation
π • :: NominalPermutation -> Map k v -> Map k v
• Map k v
map = [(k, v)] -> Map k v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (NominalPermutation
π NominalPermutation -> k -> k
forall t. Nominal t => NominalPermutation -> t -> t
• k
k, NominalPermutation
π NominalPermutation -> v -> v
forall t. Nominal t => NominalPermutation -> t -> t
• v
v) | (k
k, v
v) <- Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
map ]

instance (Ord k, Nominal k) => Nominal (Set k) where
  NominalPermutation
π • :: NominalPermutation -> Set k -> Set k
• Set k
set = [k] -> Set k
forall a. Ord a => [a] -> Set a
Set.fromList [ NominalPermutation
π NominalPermutation -> k -> k
forall t. Nominal t => NominalPermutation -> t -> t
• k
k | k
k <- Set k -> [k]
forall a. Set a -> [a]
Set.toList Set k
set ]

-- ----------------------------------------------------------------------
-- * Generic programming for Nominal

-- | A version of the 'Nominal' class suitable for generic programming.
class GNominal f where
  gbullet :: NominalPermutation -> f a -> f a

instance GNominal V1 where
  gbullet :: forall a. NominalPermutation -> V1 a -> V1 a
gbullet NominalPermutation
π V1 a
x = V1 a
forall a. HasCallStack => a
undefined -- Does not occur, because V1 is an empty type.

instance GNominal U1 where
  gbullet :: forall a. NominalPermutation -> U1 a -> U1 a
gbullet NominalPermutation
π U1 a
U1 = U1 a
forall k (p :: k). U1 p
U1

instance (GNominal a, GNominal b) => GNominal (a :*: b) where
  gbullet :: forall a. NominalPermutation -> (:*:) a b a -> (:*:) a b a
gbullet NominalPermutation
π (a a
a :*: b a
b) = NominalPermutation -> a a -> a a
forall a. NominalPermutation -> a a -> a a
forall (f :: * -> *) a.
GNominal f =>
NominalPermutation -> f a -> f a
gbullet NominalPermutation
π a a
a a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: NominalPermutation -> b a -> b a
forall a. NominalPermutation -> b a -> b a
forall (f :: * -> *) a.
GNominal f =>
NominalPermutation -> f a -> f a
gbullet NominalPermutation
π b a
b

instance (GNominal a, GNominal b) => GNominal (a :+: b) where
  gbullet :: forall a. NominalPermutation -> (:+:) a b a -> (:+:) a b a
gbullet NominalPermutation
π (L1 a a
x) = a a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (NominalPermutation -> a a -> a a
forall a. NominalPermutation -> a a -> a a
forall (f :: * -> *) a.
GNominal f =>
NominalPermutation -> f a -> f a
gbullet NominalPermutation
π a a
x)
  gbullet NominalPermutation
π (R1 b a
x) = b a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (NominalPermutation -> b a -> b a
forall a. NominalPermutation -> b a -> b a
forall (f :: * -> *) a.
GNominal f =>
NominalPermutation -> f a -> f a
gbullet NominalPermutation
π b a
x)

instance (GNominal a) => GNominal (M1 i c a) where
  gbullet :: forall a. NominalPermutation -> M1 i c a a -> M1 i c a a
gbullet NominalPermutation
π (M1 a a
x) = a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (NominalPermutation -> a a -> a a
forall a. NominalPermutation -> a a -> a a
forall (f :: * -> *) a.
GNominal f =>
NominalPermutation -> f a -> f a
gbullet NominalPermutation
π a a
x)

instance (Nominal a) => GNominal (K1 i a) where
  gbullet :: forall a. NominalPermutation -> K1 i a a -> K1 i a a
gbullet NominalPermutation
π (K1 a
x) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (NominalPermutation
π NominalPermutation -> a -> a
forall t. Nominal t => NominalPermutation -> t -> t
• a
x)