module Core(
            Nominal
           ,Name
           ,Locality
           ,Location
           ,CoreProcessSyntax
           ,CoreAgentSyntax
           ,MinimalProcessSyntax
           ,MinimalAgentSyntax
           )
  where

-- What's in a name?

class Nominal a where
    nominate :: i -> a i

data Name i = Nominate i

instance Nominal Name where
    nominate i = Nominate i

instance (Eq i) => Eq (Name i) where
    (==) (Nominate id1) (Nominate id2) = (id1 == id2)

-- Where are we?

class Locality a where
    locate :: (Eq s, Nominal n) => s -> (n i) -> a s (n i)
    name :: (Eq s, Nominal n) => a s (n i) -> (n i)

data Location s n = Locate s n

instance Locality Location where
   locate s n = (Locate s n)
   name (Locate s n) = n

instance (Eq s, Eq n) => Eq (Location s n) where
    (==) (Locate s1 name1) (Locate s2 name2) = ((s1 == s2) && (name1 == name2))

-- Constraints

class CoreProcessSyntax p where
    zero :: (Locality a, CoreAgentSyntax x) =>
            (p (a s (n i)) x)
    sequence :: (Locality a, CoreAgentSyntax x) =>
                (a s (n i)) -> x -> (p (a s (n i)) x)
    compose :: (Locality a, CoreAgentSyntax x) =>
               [(p (a s (n i)) x)] -> (p (a s (n i)) x)

class CoreAgentSyntax x where
--    bind :: (Nominal n, Locality a, CoreProcessSyntax p) =>
--            [(n i)] -> (p (a s (n i)) x) -> x
    bind :: (CoreProcessSyntax p) => [n] -> (p a x) -> x
--    offer :: (Nominal n, Locality a, CoreProcessSyntax p) =>
--             [(n i)] -> (p (a s (n i)) x) -> x
    offer :: (CoreProcessSyntax p) => [n] -> (p a x) -> x 

-- Freedom (as in freely generated)

data MinimalProcessSyntax l x =
     Null
     | Sequence l x
     | Composition [(MinimalProcessSyntax l x)]

data MinimalAgentSyntax n p =
     Thunk (() -> p)
     | Abstraction ([n] -> p)
     | Concretion [n] p

-- Constraining freedom

instance CoreProcessSyntax MinimalProcessSyntax where
     zero = Null
     sequence l a = Sequence l a
     compose [] = zero
     compose ps = Composition ps

-- instance (Eq n, Eq p) =>
--     CoreAgentSyntax (MinimalAgentSyntax n p) where
--      bind [] proc = Thunk (\() -> proc)

--      -- TODO : lgm : need to substitute m for n in proc 
--      bind [name:names] proc = Abstraction (\m -> (bind names proc)) 
--      offer names proc = Concretion names proc