--  This file contains a semantic interpreter implemented in Haskell.
--  It implements the denotational semantics of a language Lsnpmr described in the paper:
-- 
--  "A Semantic Investigation of Spiking Neural P Systems with Mute Rules"
--  Authors: Eneia Nicolae Todoran and Gabriel Ciobanu  
--  Submitted to 28th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2026 (SYNASC 2026)
-- 
--  The function 'dsem' implements the denotational semantics of Lsnpmr programs.
-- 
--  The variable 'pi1' implements the Lsnpmr program presented in the paper in Example 1 and Example 2.
--  The variable 'pi2' implements the Lsnpmr program presented in the paper in the Appendix (Section C).
-- 
--  The semantic interpreter contained in this file is a direct implementation 
--  of the denotational semantics presented in the paper. It is engineered 
--  to generate all execution traces (irrespective of their number or size),
--  hence it can only be used to test (toy) Lsnpmr programs like pi1. 
-- 
--  (The Lsnpmr program pi2 also included below is both nondeterministic and nonterminating.
--  The Lsnpmr program pi2 can only be tested using the semantic interpreters 
--  contained in the files Lsnpmr-osem-cps-fin.hs and Lsnpmr-dsem-cps-fin.hs 
--  which are based on finite execution traces) 
-- 
--  The Lsnpmr program 'pi1'  can be tested as in the following examples (function 'main' calls 'dsem pi1'):
-- 
--  Main> main 
--  ...
--  Main> dsem pi1 
--  ...
--  (Main> is the GHC prompt)
-- 
--  Remark: In this implementation we avoided using various specific Haskell 
--  tools and library functions. Had we have done this, the implementation 
--  would have been shorter, but the connection with our submission 
--  would have been less obvious to a non Haskell-expert reader

--- Syntax of Lsnpmr
type Oset  = String                                             -- Spikes (objects)
type W     = [Oset]                                             -- Multisets of spikes  

type Nn = String                                                -- Neuron names
type Xi = [Nn]                                                  -- Sets of neuron names  		   
data XiInit = XiInit Xi deriving Eq 

data ES    = Spike Oset | SelectiveSpike Xi Oset | InitSpike Xi -- Elementary statements
data Stat  = ES ES | Par Stat Stat                              -- Statements 

data Rule  = Rfire (RE Oset) W Stat                             -- Spiking rule
           | Rminus (RE Oset) W                                 -- Mute rule
           | Rplus (RE Oset) W                                  -- Mute rule
type Rs    = [Rule]                                             -- Lists of rules 
type ND    = (Nn,Rs,Xi)                                         -- Neuron declarations                     
type Ndecl = [ND]                                               -- Declarations 
type Prg   = (Ndecl,Stat)                                       -- Lsnpmr programs

-- Regular expressions 
data RE a = LambdaRE | ARE a | Concat (RE a) (RE a) | Union (RE a) (RE a) | Plus (RE a)  

nns :: Ndecl -> Xi  
nns ndecl = [ nu | (nu,_,_) <- ndecl ]

nbs :: Ndecl -> Nn -> Xi
nbs []                   nu = [] 
nbs ((nu',rho,alpha):ndecl) nu = if nu'==nu then alpha else nbs ndecl nu

rs :: Ndecl -> Nn -> Rs
rs []                   nu = [] 
rs ((nu',rho,alpha):ndecl) nu = if nu'==nu then rho else rs ndecl nu 

data Sigma  = Sigma [(Nn,W)]                                         -- Neural states 

halt :: Ndecl -> Sigma -> Bool
halt ndecl (Sigma sigma) = and [ hltN ndecl nu s | (nu,s) <- sigma ]

hltN :: Ndecl -> Nn -> W -> Bool
hltN ndecl nu w                 = 
   case rs ndecl nu of
        []  -> True 
        rho -> and [ not (ar varrho w)  | varrho <- rho ]		
		
ar :: Rule -> W -> Bool
ar (Rfire re wr x) w = and [elemRE w re,wr `subms` w]
ar (Rplus re wr)   w = elemRE w re
ar (Rminus re wr)  w = and [elemRE w re,wr `subms` w]

type U      = [Act]                            -- Multiset of actions 
data Act   = At Oset Xi                        -- Actions
           | AtI Oset XiInit 
           | AtInit XiInit deriving Eq 

opa :: ES -> Xi -> Act
opa (Spike a)                 alpha = At a alpha
opa (SelectiveSpike alpha1 a) alpha = AtI a (XiInit (alpha1 `intersect` alpha))
opa (InitSpike alpha1)        alpha = AtInit (XiInit (alpha1 `intersect` alpha))
		   
--- Final semantic domain and operators 
type P    = [Q]
data Q    = Epsilon | Q Sigma Q   deriving Eq

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

nedP :: P -> P -> P
nedP p1 p2 = 
   let povr = [q | q <- p1 `union` p2, q /= Epsilon] 
   in  case povr of
            [] -> [Epsilon]
            _  -> povr			

bignedP :: [P] -> P
bignedP []     = [Epsilon]
bignedP (p:ps) = p `nedP` (bignedP ps)
			 					
--- Computations and continuations
type D  = C -> R
type C  = U -> R                          
data F  = Fe | F D
type R  = Sigma -> P

-- Denotational semantics of Lsnpmr statements
sem :: Stat -> Xi -> D
sem (ES e)      xi = \gamma -> gamma [opa e xi] 
sem (Par s1 s2) xi = (sem s1 xi) `syn` (sem s2 xi)   

type Op = D -> D -> D

lsyn :: Op
lsyn d1 d2 = \gamma -> d1 (\u1 -> d2 (\u2 -> gamma (u1 `summs` u2)))

syn :: Op  
syn d1 d2 = \gamma sigma -> 
   (lsyn d1 d2 gamma sigma) `nedP` (lsyn d2 d1 gamma sigma)

synf :: F -> F -> F
synf Fe  Fe        = Fe
synf Fe  (F d)     = F d
synf (F d)  Fe     = F d
synf (F d1) (F d2) = F (d1 `syn` d2)

bigsynf :: [F] -> F
bigsynf [] = Fe
bigsynf (k:ks) = k `synf` (bigsynf ks)

--- Initial continuation gammaN is defined as fixed point of phiN
phiN :: Ndecl -> C -> C 
phiN ndecl gamma u sigma =
   let sigma1 = initsigma u sigma
       sigma2 = sndu u sigma1      
       sigmaobs = sigmaObs ndecl sigma2	   
   in  prefix sigmaobs (sigmasched ndecl gamma sigma2)  	   

sigmasched :: Ndecl -> C -> Sigma -> P
sigmasched ndecl gamma sigma = 
   if halt ndecl sigma then [Epsilon]
   else let varpi = schedd ndecl sigma 
        in  bignedP [ d' gamma sigma' | (d',sigma') <- varpi ]

-- The mapping '(sigmaObs ndecl sigma)' yields a list (an observable) of type 'Sigma' where 
-- neuron names occur in the same order as in the neural net definition 'ndecl'   

sigmaObs :: Ndecl -> Sigma -> Sigma  
sigmaObs ndecl (Sigma sigma) = Sigma [ (nu,w) | nu <- nns ndecl, (nu',w) <- sigma, nu'==nu ] 

initsigma :: U -> Sigma -> Sigma
initsigma u (Sigma sigma) = Sigma (sigma ++ [ (nu,[]) | nu <- alphainit `diffs` alphasigma ]) 
   where alphasigma = [ nu | (nu,w) <- sigma ]
         alphainit = bigunion [ alpha | (AtI a (XiInit alpha))  <- u ] `union`
                     bigunion [ alpha | (AtInit (XiInit alpha)) <- u ] 

sndu :: U -> Sigma -> Sigma
sndu []                          sigma = sigma
sndu ((At a alpha):u)            sigma = sndf (a,alpha) (sndu u sigma)
sndu ((AtI a (XiInit alpha)):u)  sigma = sndf (a,alpha) (sndu u sigma)
sndu ((AtInit (XiInit alpha)):u) sigma = sndu u sigma
   
sndf :: (Oset,Xi) -> Sigma -> Sigma
sndf (a,alpha) (Sigma sigma) =
   Sigma [ addn (a,alpha) nstate | nstate <- sigma ]

addn :: (Oset,Xi) -> (Nn,W) -> (Nn,W)
addn (a,alpha) (nu1,w)                 = 
   if nu1 `elem` alpha then (nu1,[a] `summs` w) else (nu1,w)

schedd :: Ndecl -> Sigma -> [(D,Sigma)]
schedd ndecl (Sigma sigma) = 
   if   halt ndecl (Sigma sigma) then [] 
   else [ (fd (bigsynf [ F d | (F d,_) <- scheds ]),Sigma [ (nu,w) | (_,(nu,w)) <- scheds ])
        | scheds <- prod [ scheddn ndecl nu w | (nu,w) <- sigma ]]
   where prod :: [[a]] -> [[a]]
         prod []       = [[]]
         prod [xs]     = [[x] | x <- xs ]
         prod (xs:xss) = [ x : tup | x <- xs, tup <- prod xss ]

scheddn :: Ndecl -> Nn -> W -> [(F,(Nn,W))]
scheddn ndecl nu w = 
   if hltN ndecl nu w then [(Fe,(nu,w))]
   else let rho = rs ndecl nu
            xi  = nbs ndecl nu   
   in  [ (F (sem x xi),(nu,w `diffms` wconsumed)) 
       | Rfire re wconsumed x <- rho, elemRE w re, wconsumed `subms` w ] ++ 
       [ (Fe,(nu,w `summs` wadd)) | Rplus re wadd <- rho, elemRE w re ] ++
       [ (Fe,(nu,w `diffms` wconsumed)) | Rminus re wconsumed <- rho, elemRE w re, wconsumed `subms` w ] 	   	   

fd :: F -> D
fd Fe    = sem (ES (InitSpike [])) []
fd (F d) = d

--- Denotational semantics of Lsnpmr programs

dsem :: Prg -> P 	 
dsem (ndecl,x) =
   sem x xi0 gammaN sigma0
   where gammaN             = fix (phiN ndecl)
         sigma0             = Sigma [("nu0",[])]   
         xi0                = xizero ndecl		 
         xizero :: Ndecl -> Xi
         xizero ((nu0,rho0,xi0):_) = xi0		 		 		 

--- Mathematical operators 
--- General fixed point operator
fix :: (a -> a) -> a
fix f = f (fix f)

--- Operations on sets 
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
   
bigunion :: Eq a => [[a]] -> [a]
bigunion []       = []
bigunion (x : xs) = x `union` (bigunion xs)
   
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

diffs :: Eq a => [a] -> [a] -> [a]
diffs []     ys = []
diffs (x:xs) ys = if (x `elem` ys) then diffs xs ys else x : diffs xs ys 
   
subseteq :: Eq a => [a] -> [a] -> Bool
subseteq []     ys = True
subseteq (x:xs) ys = (x `elem` ys) && (subseteq xs ys)

eqset :: Eq a => [a] -> [a] -> Bool
eqset xs ys = and [subseteq xs ys,subseteq ys xs]   
   
--- Operators on multisets  
summs :: Eq a => [a] -> [a] -> [a]
summs xs ys = xs ++ ys

subms :: Eq a => [a] -> [a] -> Bool
subms []       ys = True
subms (x : xs) ys =
   if (elem x ys) then subms xs (remems x ys) else False    

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

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

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

--- Operations with regular expressions
--- 'elemRE' verifies if (any permutation of) a multiset is an element 
--- of a language associated with a regular expression

elemRE :: Eq a => [a] -> (RE a) -> Bool
elemRE w re = or [ elemre w' re | w' <- perm w ]
   where elemre :: Eq a => [a] -> (RE a) -> Bool
         elemre z  LambdaRE         = case z of { [] -> True; _ -> False } 
         elemre z  (ARE a)          = case z of { [a'] -> (a' == a); _ -> False }
         elemre z  (Union re1 re2)  = or [ elemre z re1, elemre z re2 ]
         elemre z  (Concat re1 re2) = or [ and [elemre z1 re1,elemre z2 re2] | (z1,z2) <- decompose z ]  
         elemre z  (Plus re)        = or [ elemre z (ncopies re n) | n <- [1 .. length z] ] 
		 
decompose :: [a] -> [([a],[a])]
decompose []     = [([],[])] 
decompose (x:xs) = ([],x:xs):([x],xs):[ (x:x':z1',z2) | (x':z1',z2) <- decompose xs ] 
 
ncopies :: (RE a) -> Int -> (RE a)
ncopies LambdaRE n = LambdaRE
ncopies re       n = if n<=1 then re else Concat re (ncopies re (n-1))
		 
--- Permutations generator   		 

perm :: [a] -> [[a]]
perm [] = [[]]
perm xs = [ y:zs | (y,ys) <- sel xs, zs <- perm ys ]
		 
sel :: [a] -> [(a,[a])]
sel []     = []
sel (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- sel xs ]

--- Eq instances
   
instance Eq Sigma where
   (Sigma sigma1) == (Sigma sigma2) = sigma1 `eqset` sigma2      
 
--- Show instances 
instance Show Sigma where 
   show (Sigma sigma) = show sigma  
   
instance Show Q where 
   show Epsilon = "\n[]"
   show q       = "\n[" ++ (showQ q) ++ "]"
   
showQ :: Q -> String
showQ (Q ns Epsilon) = show ns 
showQ (Q obs q)      = (show obs) ++ " .\n " ++ (showQ q)

-- | Test Examples and Main Program 

pi1 :: Prg
pi1 =       
   ([("nu0",[],["nu1","nu2"]),
     ("nu1",[Rplus (ARE "a") ["a"],
             Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (Par (ES (Spike "a")) (ES (Spike "a")))],["nu2"]),   
     ("nu2",[Rminus (ARE "a") ["a"],Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (ES (Spike "a"))],["nu0"])],
    Par (ES (SelectiveSpike ["nu1"] "a"))  
        (Par (ES (SelectiveSpike ["nu2"] "a"))(ES (SelectiveSpike ["nu2"] "a"))))   	 		

pi2 :: Prg
pi2 =       
   ([("nu0",[],["nu1","nu2"]),
     ("nu1",[Rplus (ARE "a") ["a"],Rfire (Concat (ARE "a") (ARE "a")) ["a"] (ES (Spike "a")),
             Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (Par (ES (Spike "a")) (ES (Spike "a")))],["nu2"]),   
     ("nu2",[Rminus (ARE "a") ["a"],Rfire (Concat (ARE "a") (ARE "a")) ["a","a"] (ES (Spike "a"))],["nu0"])],
    Par (ES (SelectiveSpike ["nu1"] "a"))  
        (Par (ES (SelectiveSpike ["nu2"] "a"))(ES (SelectiveSpike ["nu2"] "a"))))   	 		

main = do
  print (dsem pi1)