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

-- | This module provides the 'NominalSupport' type class. It consists
-- of those types for which the support can be calculated. With the
-- exception of function types, most 'Nominal' types are also
-- in 'NominalSupport'.
--
-- We also provide some generic programming so that instances of
-- 'NominalSupport' 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.NominalSupport 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.Nominal

-- ----------------------------------------------------------------------
-- * Literal strings

-- | A wrapper around strings. This is used to denote any literal
-- strings whose values should not clash with the names of bound
-- variables. For example, if a term contains a constant symbol /c/,
-- the name /c/ should not also be used as the name of a bound
-- variable. This can be achieved by marking the string with
-- 'Literal', like this
-- 
-- > data Term = Var Atom | Const (Literal String) | ...
--
-- Another way to use 'Literal' is in the definition of custom
-- 'NominalSupport' instances. See
-- <#CUSTOM "Defining custom instances"> for an example.

newtype Literal = Literal String
                deriving (Int -> Literal -> ShowS
[Literal] -> ShowS
Literal -> String
(Int -> Literal -> ShowS)
-> (Literal -> String) -> ([Literal] -> ShowS) -> Show Literal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Literal -> ShowS
showsPrec :: Int -> Literal -> ShowS
$cshow :: Literal -> String
show :: Literal -> String
$cshowList :: [Literal] -> ShowS
showList :: [Literal] -> ShowS
Show)

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

-- ----------------------------------------------------------------------
-- * Support

-- | Something to be avoided can be an atom or a string.
data Avoidee = A Atom | S String
             deriving (Avoidee -> Avoidee -> Bool
(Avoidee -> Avoidee -> Bool)
-> (Avoidee -> Avoidee -> Bool) -> Eq Avoidee
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Avoidee -> Avoidee -> Bool
== :: Avoidee -> Avoidee -> Bool
$c/= :: Avoidee -> Avoidee -> Bool
/= :: Avoidee -> Avoidee -> Bool
Eq, Eq Avoidee
Eq Avoidee =>
(Avoidee -> Avoidee -> Ordering)
-> (Avoidee -> Avoidee -> Bool)
-> (Avoidee -> Avoidee -> Bool)
-> (Avoidee -> Avoidee -> Bool)
-> (Avoidee -> Avoidee -> Bool)
-> (Avoidee -> Avoidee -> Avoidee)
-> (Avoidee -> Avoidee -> Avoidee)
-> Ord Avoidee
Avoidee -> Avoidee -> Bool
Avoidee -> Avoidee -> Ordering
Avoidee -> Avoidee -> Avoidee
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
$ccompare :: Avoidee -> Avoidee -> Ordering
compare :: Avoidee -> Avoidee -> Ordering
$c< :: Avoidee -> Avoidee -> Bool
< :: Avoidee -> Avoidee -> Bool
$c<= :: Avoidee -> Avoidee -> Bool
<= :: Avoidee -> Avoidee -> Bool
$c> :: Avoidee -> Avoidee -> Bool
> :: Avoidee -> Avoidee -> Bool
$c>= :: Avoidee -> Avoidee -> Bool
>= :: Avoidee -> Avoidee -> Bool
$cmax :: Avoidee -> Avoidee -> Avoidee
max :: Avoidee -> Avoidee -> Avoidee
$cmin :: Avoidee -> Avoidee -> Avoidee
min :: Avoidee -> Avoidee -> Avoidee
Ord, Int -> Avoidee -> ShowS
[Avoidee] -> ShowS
Avoidee -> String
(Int -> Avoidee -> ShowS)
-> (Avoidee -> String) -> ([Avoidee] -> ShowS) -> Show Avoidee
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Avoidee -> ShowS
showsPrec :: Int -> Avoidee -> ShowS
$cshow :: Avoidee -> String
show :: Avoidee -> String
$cshowList :: [Avoidee] -> ShowS
showList :: [Avoidee] -> ShowS
Show)

-- | This type provides an internal representation for the support of
-- a nominal term, i.e., the set of atoms (and constants) occurring in
-- it. This is an abstract type with no exposed structure. The only way
-- to construct a value of type 'Support' is to use the function
-- 'support'.
newtype Support = Support (Set Avoidee)

-- | The empty support.
support_empty :: Support
support_empty :: Support
support_empty = Set Avoidee -> Support
Support Set Avoidee
forall a. Set a
Set.empty

-- | The union of a list of supports.
support_unions :: [Support] -> Support
support_unions :: [Support] -> Support
support_unions [Support]
xs = Set Avoidee -> Support
Support ([Set Avoidee] -> Set Avoidee
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ Set Avoidee
x | Support Set Avoidee
x <- [Support]
xs ])

-- | The union of two supports.
support_union :: Support -> Support -> Support
support_union :: Support -> Support -> Support
support_union (Support Set Avoidee
x) (Support Set Avoidee
y) = Set Avoidee -> Support
Support (Set Avoidee -> Set Avoidee -> Set Avoidee
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Avoidee
x Set Avoidee
y)

-- | Add an atom to the support.
support_insert :: Atom -> Support -> Support
support_insert :: Atom -> Support -> Support
support_insert Atom
a (Support Set Avoidee
x) = Set Avoidee -> Support
Support (Avoidee -> Set Avoidee -> Set Avoidee
forall a. Ord a => a -> Set a -> Set a
Set.insert (Atom -> Avoidee
A Atom
a) Set Avoidee
x)

-- | A singleton support.
support_atom :: Atom -> Support
support_atom :: Atom -> Support
support_atom Atom
a = Set Avoidee -> Support
Support (Avoidee -> Set Avoidee
forall a. a -> Set a
Set.singleton (Atom -> Avoidee
A Atom
a))

-- | Delete an atom from the support.
support_delete :: Atom -> Support -> Support
support_delete :: Atom -> Support -> Support
support_delete Atom
a (Support Set Avoidee
s) = Set Avoidee -> Support
Support (Avoidee -> Set Avoidee -> Set Avoidee
forall a. Ord a => a -> Set a -> Set a
Set.delete (Atom -> Avoidee
A Atom
a) Set Avoidee
s)

-- | Delete a list of atoms from the support.
support_deletes :: [Atom] -> Support -> Support
support_deletes :: [Atom] -> Support -> Support
support_deletes [] Support
s = Support
s
support_deletes (Atom
a:[Atom]
as) Support
s = [Atom] -> Support -> Support
support_deletes [Atom]
as (Atom -> Support -> Support
support_delete Atom
a Support
s)

-- | Add a literal string to the support.
support_string :: String -> Support
support_string :: String -> Support
support_string String
s = Set Avoidee -> Support
Support (Avoidee -> Set Avoidee
forall a. a -> Set a
Set.singleton (String -> Avoidee
S String
s))

-- | Convert the support to a list of strings.
strings_of_support :: Support -> Set String
strings_of_support :: Support -> Set String
strings_of_support (Support Set Avoidee
s) = (Avoidee -> String) -> Set Avoidee -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Avoidee -> String
name Set Avoidee
s where
  name :: Avoidee -> String
name (A Atom
a) = Atom -> String
forall a. Show a => a -> String
show Atom
a
  name (S String
s) = String
s
                 
-- ----------------------------------------------------------------------
-- * The NominalSupport class

-- | 'NominalSupport' is a subclass of 'Nominal' consisting of those
-- types for which the support can be calculated. With the notable
-- exception of function types, most 'Nominal' types are also
-- instances of 'NominalSupport'.
--
-- In most cases, instances of 'NominalSupport' 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) => NominalSupport t where
  -- | Compute a set of atoms and strings that should not be used as
  -- the names of bound variables.
  support :: t -> Support

  default support :: (Generic t, GNominalSupport (Rep t)) => t -> Support
  support t
x = Rep t Any -> Support
forall a. Rep t a -> Support
forall (f :: * -> *) a. GNominalSupport f => f a -> Support
gsupport (t -> Rep t Any
forall x. t -> Rep t x
forall a x. Generic a => a -> Rep a x
from t
x)

-- ----------------------------------------------------------------------
-- * Open for printing

-- | 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/. 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>.
atom_open_for_printing :: (Nominal t) => Support -> BindAtom t -> (Atom -> t -> Support -> s) -> s
atom_open_for_printing :: forall t s.
Nominal t =>
Support -> BindAtom t -> (Atom -> t -> Support -> s) -> s
atom_open_for_printing Support
sup t :: BindAtom t
t@(BindAtom NameGen
ng Atom -> Defer t
f) Atom -> t -> Support -> s
k =
  String -> NameGen -> (Atom -> s) -> s
forall a. String -> NameGen -> (Atom -> a) -> a
with_fresh_atom_named String
n NameGen
ng (\Atom
a -> Atom -> t -> Support -> s
k Atom
a (Defer t -> t
forall t. Nominal t => Defer t -> t
force (Atom -> Defer t
f Atom
a)) (Atom -> Support
sup' Atom
a))
  where
    n :: String
n = Set String -> NameGen -> String
rename_fresh (Support -> Set String
strings_of_support Support
sup) NameGen
ng
    sup' :: Atom -> Support
sup' Atom
a = Atom -> Support -> Support
support_insert Atom
a Support
sup

-- ----------------------------------------------------------------------
-- * NominalSupport instances

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

-- | A helper function for defining 'NominalSupport' instances
-- for non-nominal types.
basic_support :: t -> Support
basic_support :: forall t. t -> Support
basic_support t
t = () -> Support
forall t. NominalSupport t => t -> Support
support ()

-- Base cases

instance NominalSupport Atom where
  support :: Atom -> Support
support = Atom -> Support
support_atom

instance NominalSupport Bool where
  support :: Bool -> Support
support = Bool -> Support
forall t. t -> Support
basic_support

instance NominalSupport Integer where
  support :: Integer -> Support
support = Integer -> Support
forall t. t -> Support
basic_support

instance NominalSupport Int where
  support :: Int -> Support
support = Int -> Support
forall t. t -> Support
basic_support

instance NominalSupport Char where
  support :: Char -> Support
support = Char -> Support
forall t. t -> Support
basic_support

instance NominalSupport Double where
  support :: Double -> Support
support = Double -> Support
forall t. t -> Support
basic_support

instance NominalSupport Float where
  support :: Float -> Support
support = Float -> Support
forall t. t -> Support
basic_support

instance NominalSupport Ordering where
  support :: Ordering -> Support
support = Ordering -> Support
forall t. t -> Support
basic_support

instance NominalSupport (Basic t) where
  support :: Basic t -> Support
support = Basic t -> Support
forall t. t -> Support
basic_support

instance NominalSupport Literal where
  support :: Literal -> Support
support (Literal String
s) = String -> Support
support_string String
s

-- Generic instances

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


-- Special instances

instance (NominalSupport t) => NominalSupport (BindAtom t) where
  support :: BindAtom t -> Support
support (BindAtom NameGen
ng Atom -> Defer t
f) =
    NameGen -> (Atom -> Support) -> Support
forall a. NameGen -> (Atom -> a) -> a
with_fresh_atom NameGen
ng (\Atom
a -> Atom -> Support -> Support
support_delete Atom
a (Defer t -> Support
forall t. NominalSupport t => t -> Support
support (Atom -> Defer t
f Atom
a)))

instance (NominalSupport t) => NominalSupport (Defer t) where
  support :: Defer t -> Support
support Defer t
t = t -> Support
forall t. NominalSupport t => t -> Support
support (Defer t -> t
forall t. Nominal t => Defer t -> t
force Defer t
t)

instance (Ord k, NominalSupport k, NominalSupport v) => NominalSupport (Map k v) where
  support :: Map k v -> Support
support Map k v
map = [(k, v)] -> Support
forall t. NominalSupport t => t -> Support
support (Map k v -> [(k, v)]
forall k a. Map k a -> [(k, a)]
Map.toList Map k v
map)

instance (Ord k, NominalSupport k) => NominalSupport (Set k) where
  support :: Set k -> Support
support Set k
set = [k] -> Support
forall t. NominalSupport t => t -> Support
support (Set k -> [k]
forall a. Set a -> [a]
Set.toList Set k
set)

-- ----------------------------------------------------------------------
-- * Generic programming for NominalSupport

-- | A version of the 'NominalSupport' class suitable for generic programming.
class GNominalSupport f where
  gsupport :: f a -> Support

instance GNominalSupport V1 where
  gsupport :: forall a. V1 a -> Support
gsupport V1 a
x = Support
forall a. HasCallStack => a
undefined -- Does not occur, because V1 is an empty type.

instance GNominalSupport U1 where
  gsupport :: forall a. U1 a -> Support
gsupport U1 a
U1 = Support
support_empty

instance (GNominalSupport a, GNominalSupport b) => GNominalSupport (a :*: b) where
  gsupport :: forall a. (:*:) a b a -> Support
gsupport (a a
a :*: b a
b) = Support -> Support -> Support
support_union (a a -> Support
forall a. a a -> Support
forall (f :: * -> *) a. GNominalSupport f => f a -> Support
gsupport a a
a) (b a -> Support
forall a. b a -> Support
forall (f :: * -> *) a. GNominalSupport f => f a -> Support
gsupport b a
b)

instance (GNominalSupport a, GNominalSupport b) => GNominalSupport (a :+: b) where
  gsupport :: forall a. (:+:) a b a -> Support
gsupport (L1 a a
x) = a a -> Support
forall a. a a -> Support
forall (f :: * -> *) a. GNominalSupport f => f a -> Support
gsupport a a
x
  gsupport (R1 b a
x) = b a -> Support
forall a. b a -> Support
forall (f :: * -> *) a. GNominalSupport f => f a -> Support
gsupport b a
x

instance (GNominalSupport a) => GNominalSupport (M1 i c a) where
  gsupport :: forall a. M1 i c a a -> Support
gsupport (M1 a a
x) = a a -> Support
forall a. a a -> Support
forall (f :: * -> *) a. GNominalSupport f => f a -> Support
gsupport a a
x

instance (NominalSupport a) => GNominalSupport (K1 i a) where
  gsupport :: forall a. K1 i a a -> Support
gsupport (K1 a
x) = a -> Support
forall t. NominalSupport t => t -> Support
support a
x