-- | This file contains a semantic interpreter designed in continuation passing style 
-- | and implemented in Haskell. It implements the denotational semantics of 
-- | the concurrent language Lsyn^omega presented in section 3.2 of the paper:
-- |
-- | "Abstractness of Metric Semantics for Concurrency in Continuation-Passing Style"
-- | Authors: Eneia Nicolae Todoran and Gabriel Ciobanu
-- | Submitted to ACM Computing Surveys (2025)
-- | 
-- | The language Lsyn^omega is essentially based on well-known Milner's CCS [1]. 
-- | The language Lsyn^omega extends the (uniform) language with synchronization 
-- | described in [2] (section 11.2) with the joint input construct of 
-- | process calculus CCS^n presented in [3].
-- |
-- | [1] R. Milner, Communication and Concurrency, Prentice Hall, 1989.
-- | [2] J.W. de Bakker and E.P. de Vink, Control Flow Semantics, MIT Press, 1996.
-- | [3] C. Laneve and A. Vitale, "The expressive power of synchronizations", Proc. of LICS 2010, pp. 382-–391, 2010.
-- |
-- | In CCS^n calculus the joint input construct is a list of names of length at most n. 
-- | Unlike CCS^n, in the language Lsyn^omega a joint input is a non-empty multiset 
-- | (implemented as a Haskell list) that can contain a (finite, but) arbitrarily large number of names. 
-- | The language  Lsyn^omega provides support for synchronous multiparty interactions 
-- | between an arbitrarily large (finite) number of concurrent processes.
-- |
-- | The function 'sem' implements the denotational (compositional) semantics of the concurrent language Lsyn^omega.   
-- | The semantic function 'dsem' evaluates the denotational semantics w.r.t. the initial continuation. 
-- |
-- | In the experiments given below, s1, s2, s3 and s4 implement the Lsyn^omega statements 
-- | presented in Example 3 (and Example 2) in our paper submitted to ACM Computing Surveys.  
-- | 
-- | The semantic interpreter can be tested as in the following examples:
-- | 
-- | Main> run s1
-- | ...
-- | Main> run s2
-- | ...
-- | Main> run s3
-- | ...
-- | Main> run s4
-- | ...
-- | (Main> is the GHC prompt)
-- |
-- | The same experiments can be performed using function 'main':
-- |
-- | -- | Main> main 
-- | ...
-- | 
-- | Further Lsyn^omega example programs (which are not presented in the paper) 
-- | can be tested using function 'main2'    
-- |
-- | -- | Main> main2  
-- | ...
-- | 
-- | Remark: In this implementation we avoided using various specific Haskell 
-- | library functions. Had we have done this, the implementation would have been shorter
-- | but the connection with our ACM Computing Surveys submission would have been 
-- | less obvious to a non Haskell-expert reader


-- | Syntax of Lsyn^omega

type Name   = String                       -- ^ Names
type CoName = String                       -- ^ Co-names
type J      = [Name]                       -- ^ Joint inputs 
type B      = String       
data IAct   = Tau | B B deriving Eq        -- ^ Internal actions  
  
data Act  = I IAct | S CoName | J J | Stop -- ^ Actions 
            deriving Eq 
		  
type Yvar = String                         -- ^ Recursion variables (procedure variables)
  
-- | Statements and declarations
data Stat = Act Act                        -- ^ Actions
          | Y Yvar                         -- ^ Recursion variable
          | New Stat Name                  -- ^ Restriction
          | Seq Stat Stat                  -- ^ Sequential composition		  
          | Ned Stat Stat                  -- ^ Nondeterministic choice
          | Par Stat Stat                  -- ^ Parallel composition (merge)
          | Lpar Stat Stat                 -- ^ Left merge 		  
          | Syn Stat Stat                  -- ^ Synchronization merge		  		  
          | Lsyn Stat Stat                 -- ^ Left synchronization merge		  		  
            deriving Eq 		  
type Decl = Yvar -> Stat                   -- ^ Declarations

-- | Interaction multisets
type U = [M]
data M = ActM Act | NewM Name U 

-- | Interaction function  
iu :: U -> [Act]
iu ([ActM act])   = [act]
iu ([NewM c u])   = 
   case iu u of
        [I b]       -> [I b] 	
        [J j]       -> if not (c `elem` j) then [J j] else [Stop]
        w           -> if (out w) && (not (c `elem` (compl w))) then w else [Stop] 				
iu u              = chi (bigsumms [ iu [m] | m <- u ])

out :: [Act] -> Bool
out w = and [ pout act | act <- w ] 
   where pout :: Act -> Bool 
         pout (S c) = True
         pout _     = False  		 
		
compl :: [Act] -> J
compl w = [ c | S c <- w ]

chi :: [Act] -> [Act]
chi w = let wia   = [ I b | I b <- w ]    
            win   = [ J j | J j <- w ]		   
            wout  = [ S c | S c <- w ]
            wstop = [ Stop | Stop <- w ]  		   		   
   in case (wia,wstop,win) of	   
           ([],[],[J j]) -> if j `eqms` (compl wout) then [I Tau] else 	
                            if wout == [] then [J j] else 
                            if (compl wout) `subms` j then [J (j `diffms` (compl wout))] else [Stop]		   
           ([],[],[])    -> if wout /= [] then wout else [Stop] 										 
           _             -> [Stop]		   

-- | Final semantic domain (R is a type synonym for P)
type R = P               
type P = [Q]
data Q = Epsilon | Delta | Q IAct Q
  deriving Eq

prefix :: IAct -> P -> P
prefix b p = [ Q b q | q <- p ]

-- | Nondeterministic choice operator 
ned :: P -> P -> P
ned p1 p2 = [q | q <- p1 `union` p2, q /= Delta] `union`
            [Delta | Delta <- p1 `intersect` p2]

-- | Semantic domain
type D = C -> R       -- ^ Computations (denotations) 
type C = (U, K) -> R  -- ^ Synchronous continuations
data K = Ke | K D     -- ^ Asynchronous continuations

-- | Denotational semantics
bigpsi :: (Stat -> D) -> Stat -> D
bigpsi psi (Act a)      gamma = gamma ([ActM a], Ke)
bigpsi psi (Y y)        gamma = psi (decl y) gamma
bigpsi psi (New s c)    gamma = new c (bigpsi psi s) gamma 
bigpsi psi (Ned s1 s2)  gamma = bigpsi psi s1 gamma `ned` bigpsi psi s2 gamma
bigpsi psi (Seq s1 s2)  gamma = (bigpsi psi s1 `seqd` psi s2) gamma
bigpsi psi (Par s1 s2)  gamma = (bigpsi psi s1 `lpard` psi s2) gamma `ned`
                                (bigpsi psi s2 `lpard` psi s1) gamma `ned`
                                (bigpsi psi s1 `synd` bigpsi psi s2) gamma
bigpsi psi (Syn s1 s2)  gamma = (bigpsi psi s1 `synd` bigpsi psi s2) gamma
bigpsi psi (Lpar s1 s2) gamma = (bigpsi psi s1 `lpard` psi s2) gamma
bigpsi psi (Lsyn s1 s2) gamma = (bigpsi psi s1 `lsynd` bigpsi psi s2) gamma

sem :: Stat -> D
sem = fix bigpsi

bigpsiC :: C -> C
bigpsiC gamma (u, Ke) =
  case iu u of
    [I b]  -> [Q b Epsilon]  
    _      -> [Delta]
bigpsiC gamma (u, K d) =
  case iu u of
    [I b] -> prefix b (d gamma)   
    _     -> [Delta]

-- Initial synchronous continuation	
gammae :: C
gammae = fix bigpsiC

dsem :: Stat -> R
dsem t = sem t gammae

-- | Semantic operators
omeganew :: (Name -> D -> D) -> Name -> D -> D 
omeganew omega c d = \gamma -> d (\(u,k) -> gamma ([NewM c u],liftn omega c k))

liftn :: (Name -> D -> D) -> (Name -> K -> K)
liftn omega c Ke     = Ke
liftn omega c (K d)  = K (omega c d) 

omegaseq :: (D -> D -> D) -> (D -> D -> D)
omegaseq omega d1 d2 =
  \gamma -> d1 (\(u1, k1) -> gamma (u1, lift omega k1 (K d2)))

omegalsyn :: (D -> D -> D) -> (D -> D -> D)
omegalsyn omega d1 d2 =
  \gamma -> d1 (\(u1, k1) -> d2 (\(u2, k2) -> gamma (u1 `summs` u2, lift omega k1 k2)))

omegasyn :: (D -> D -> D) -> (D -> D -> D)
omegasyn omega d1 d2 =
  \gamma -> (omegalsyn omega d1 d2 gamma) `ned` (omegalsyn omega d2 d1 gamma)

omegapar :: (D -> D -> D) -> (D -> D -> D)
omegapar omega d1 d2 =
   \gamma -> (lpard d1 d2 gamma) `ned` (lpard d2 d1 gamma) `ned` (lsynd d1 d2 gamma) `ned` (lsynd d2 d1 gamma)

new :: Name -> D -> D
new = fix omeganew

seqd :: D -> D -> D
seqd = fix omegaseq

pard :: D -> D -> D
pard = fix omegapar

lpard :: D -> D -> D
lpard = omegaseq pard

lsynd :: D -> D -> D
lsynd = omegalsyn pard

synd :: D -> D -> D
synd = omegasyn pard

lift :: (D -> D -> D) -> (K -> K -> K)
lift omega Ke     Ke     = Ke
lift omega Ke     (K d)  = K d
lift omega (K d)  Ke     = K d
lift omega (K d1) (K d2) = K (omega d1 d2)

-- | Fixed point operator
fix :: (a -> a) -> a
fix f = f (fix f)

-- | Multiset operations
summs :: [a] -> [a] -> [a]
summs u1 u2 = u1 ++ u2

bigsumms :: [[a]] -> [a]
bigsumms [] = []
bigsumms (u:us) = u `summs` (bigsumms us)

subms :: Eq a => [a] -> [a] -> Bool
subms [] [] = True
subms [] _  = True
subms _  [] = False
subms (x:xs) xs' =
   if (x `elem` xs') then subms xs (remove x xs') else False    

eqms :: Eq a => [a] -> [a] -> Bool
eqms [] []      = True
eqms [] _       = False
eqms _  []      = False
eqms (x:xs) xs' = 
   if (x `elem` xs') then eqms xs (remove x xs') else False   
   
diffms :: Eq a => [a] -> [a] -> [a]
diffms xs []       = xs
diffms xs (x':xs') =
   if (elem x' xs) then diffms (remove x' xs) xs' else diffms xs xs'    

remove :: Eq a => a -> [a] -> [a]
remove x []      = []
remove x (x':xs) = if (x == x') then xs else x' : remove x xs

-- | Set operations
union :: Eq a => [a] -> [a] -> [a]
union []       ys = ys
union (x : xs) ys = if x `elem` ys then union xs ys else x : union xs ys

intersect :: Eq a => [a] -> [a] -> [a]
intersect []       ys = []
intersect (x : xs) ys = if x `elem` ys then x : intersect xs ys else intersect xs ys

-- | Show instances
instance Show IAct where
  show Tau     = "tau" 
  show (B b)   = b  

instance Show Q where
  show Epsilon    = "\n[]" 
  show Delta      = "\n[deadlock]" 
  show (Q b q)    = "\n[" ++ (aux (Q b q)) ++ "]" 
    where aux (Q b Epsilon) = show b
          aux (Q b Delta)   = show b ++ ",deadlock"
          aux (Q b q)       = show b ++ "," ++ aux q

-- | Test support function
run :: Stat -> P
run s = dsem s 

-------------------------------------------------------------------------------------------
------------------------------------ Test examples ----------------------------------------
-------------------------------------------------------------------------------------------

-- | Function 'main' runs the Lsyn^omega programs introduced in the paper in Example 2.
main = do { print (run s1); print (run s2); print (run s3); print (run s4) }

s1, s2, s3, s4 :: Stat
s1 = Par (Act (I (B "b1"))) (Act (I (B "b2")))
s2 = Par (Act (J ["c0"])) (Act (S "c0"))
s3 = Lsyn (New (Lsyn (Act (J ["c1","c2"])) (Act (S "c1"))) "c1") (Act (S "c2")) 						
s4 = Syn  (New (Syn  (Act (J ["c1","c2"])) (Act (S "c1"))) "c1") (Act (S "c2")) 						

-- | Function 'main2' can be used to run Lsyn^omega programs which are not presented in the paper.  
-- | Statement s5 is similar to statement s4, but uses the operator for parallel composition (merge)
-- | instead of the synchronization merge operator. Statement s6 is a sequential composition 
-- | between statement s1 and the internal action b3. Statements s7, s8 and s9 are more complex. 
-- | Statement s7 specifies a multiparty synchronous interaction between 4 (=3+1) concurrent processes.  
-- | Statements s8 and s9 extend statement s7 with operations for sequential composition 
-- | and procedure calls.
   
main2 = do { print (run s5); print (run s6); print (run s7); print (run s8); print (run s9) }

s5, s6, s7, s8 :: Stat
s5 = Par (New (Par  (Act (J ["c1","c2"])) (Act (S "c1"))) "c1") (Act (S "c2")) 						
s6 = Seq (Par (Act (I (B "b1"))) (Act (I (B "b2")))) (Act (I (B "b3")))
s7 = Par (New (Par (New (Par  (Act (J ["c1","c2","c3"])) (Act (S "c1"))) "c1") 
               (Act (S "c2"))) "c2") 
         (Act (S "c3")) 					
s8 = Seq (Par (New (Par (New (Par  (Act (J ["c1","c2","c3"])) (Act (S "c1"))) "c1") 
                        (Act (S "c2"))) "c2") 
              (Seq (Act (I (B "b1"))) (Act (S "c3"))))
         (Y "y8") 			  
s9 = Seq (Y "y9")
         (Par (New (Par (New (Par  (Act (J ["c1","c2","c3"])) (Act (S "c1"))) "c1") 
                        (Act (S "c2"))) "c2") 
              (Seq (Act (S "c3")) (Act (I (B "b3"))))) 

decl :: Decl
decl "y8" = Ned (Act (I (B "b2"))) (Act (I (B "b3")))
decl "y9" = Ned (Act (I (B "b1"))) (Act (I (B "b2")))