{-# LANGUAGE PatternSignatures   #-}

import IO
import Control.Concurrent
import Control.Concurrent.STM

import MultiSetRewrite.Base
import MultiSetRewrite.RuleSyntax
import MultiSetRewrite.RuleCompiler
import MultiSetRewrite.StoreRepresentation

import CHRSolver


{-

Gossiping girls problem (found somewhere on the internet):

A number of girls initially know one distinct secret each. Each girl has access to a phone 
which can be used to call another girl to share their secrets. Each time two girls talk to each other 
they always exchange all secrets with each other (thus after the phone call they both 
know all secrets they knew together before the phone call). The girls can communicate 
only in pairs (no conference calls) but it is possible that different pairs of girls talk concurrently. 


-}


{-


Here's a solution using CHR (Constraint Handling Rules):

  Girl(name1,secrets1), Girl(name2,secrets2) <==> 
                        newSecrets(secrets1,secrets1) | let s=shareSecrets(secrets1,secrets2)
                                                        Girl(name1,s)
                                                        Girl(name2,s)

  Girl(name,s) | allSecrets(s) ==> Done(name)


  --termination condition for M girls

  Girl(n1,s1), Done(n1), ..., Girl(nM,sM), Done(nM) <==> True


  Primitive functions used:
 
   newSecrets(s1,s2) =   not ( (s1 union s2) == s2 /\ (s1 union s2) == s1)

         new secret in either s1 or s2

   shareSecrets(s1,s2) = s1 union s2

   allSecrets(s)  checks if all secrets are in s
 
              

-}


-- Here's an encoding of the gossiping girl problem using 
-- the CHRSolver implemented on top of multisetrewrite


-----------------------------------
-- secrets primitives

-- We assume that each secret is represent as a lower-case letter.
-- Hence, we can simply use strings to represent secrets

type Secret = String

-- four secrets
secretDB = ['a'..'d']

newSecrets :: Secret -> Secret -> Bool
newSecrets s1 s2 =   not $ and $ [ elem x s1 | x <- s2] ++
                                 [ elem x s2 | x <- s1]


shareSecrets :: Secret -> Secret -> Secret
shareSecrets s1 s2 = s1 ++ s2

allSecrets :: String -> Bool
allSecrets s = and $ [elem x s | x <- secretDB]


newSecretsLifted s1 s2 = do
    v1 <- readVar s1
    v2 <- readVar s2
    return (newSecrets v1 v2)

allSecretsLifted s = do
    v <- readVar s
    return (allSecrets v)

---------------------------
-- chr rules

girl n s = cons "Girl" (n,s)

ruleGossipGirls :: CHR -> ActiveConstraint -> IO ()
ruleGossipGirls (chr@(chrD,chrR)) activeCons = do
  [n1,s1,n2,s2] <- mapM (\ _ -> newVar :: IO (VAR String)) [1..4]

  let prog = compileRulePattern
               [ 
                 -- two girls gossiping
                 [girl n1 s1, girl n2 s2]
                 `when` (newSecretsLifted s1 s2) 
                    .->. do [v_n1,v_s1,v_n2,v_s2] <- mapM (\x -> readVar x) [n1,s1,n2,s2]
                            let s = shareSecrets v_s1 v_s2
                            stackGoal chr (girl v_n1 s)
                            stackGoal chr (girl v_n2 s)
                            if allSecrets s
                             then do queueGoal chr (cons "Done" ())
                                     queueGoal chr (cons "Done" ())
                             else return ()


                  -- termination check for 5 girls
                , [ cons "Done" (),cons "Done" (), cons "Done" (), cons "Done" (), cons "Done" ()]
                  .->. stackGoal chr (cons "Stop" ())

{-
                , [girl n1 s1, cons "Stop" ()] .->. return ()
-}
                ]

        -- Our CHR solver doesn't support 'pure' propagation rules.
        -- Therefore, we check for the 'all secrets' condition in the body of the first rule.
        -- Second rule checks if all five girls are done. 
        -- Third rule removes the girls from the store

  res <- executeRules (store chrD) activeCons prog
  case res of
         Just action -> action
         Nothing -> return ()



main :: IO ()
main = do
  let threads = 4
  initStore <- newStore valHashOpMsg
  let initG  = [ girl "Helga" "a"
               , girl "Gertrud" "b"
               , girl "Emmy" "c"
               , girl "Ludmila" "d"
               , girl "Karin" "a"
               ]
  initGoals <- atomically $ newTVar initG
  inActive <- atomically $ newTVar 0

  let chr = (Data {store = initStore,
                   goals = initGoals,
                   numberOfSolverThreads = threads,
                   inActiveThreads = inActive},
             Rules { rules = ruleGossipGirls } )

  mapM_ (\x -> forkIO (solverThread chr)) [1..threads]

  suspendUntilRulesHaveExhaustivelyFired chr

  putStr "Done"