--This program implements Sum & Product problem in DEMO
--(Hans Freudenthal Version)
module SNP
where 
import DEMO
--Dynamic Epistemic MOdelling Tools, developed by Jan van Eijck

--possible pairs 1<x<y, x+y<=100
pairs  = [(x,y)|x<-[2..100], y<-[2..100], x<y, x+y<=100]
--number of the possible worlds(pairs)
numpairs =llength(pairs)

--function computing the number of elements in a list
llength [] =0
llength (x:xs) = 1+ llength xs

--used for creating valuation and accessibility relations
ipairs = zip [0..numpairs-1] pairs

--initial pointed epistemic model
msnp :: EpistM
msnp = (Pmod [0..numpairs-1] val acc [0..numpairs-1])
  where 
  val   = [(w,[P x, Q y]) | (w,(x,y))<- ipairs]
  acc   = [(a,w,v)| (w,(x1,y1))<-ipairs, (v,(x2,y2))<-ipairs, x1+y1==x2+y2 ]++
          [(b,w,v)| (w,(x1,y1))<-ipairs, (v,(x2,y2))<-ipairs, x1*y1==x2*y2 ]
  	          
--Sum says: I knew that you didn't know the two numbers.
fmrs1e = K a (Conj [Disj[Neg (Conj [Prop (P x),Prop (Q y)]), 
		         Neg (K b (Conj [Prop (P x),Prop (Q y)]))]| (x,y)<-pairs])
amrs1e = public (fmrs1e)

--Product says: Now I know the two numbers
fmrp2e = Conj [(Disj[Neg (Conj [Prop (P x),Prop (Q y)]), 
		     K b (Conj [Prop (P x),Prop (Q y)]) ] )|(x,y)<-pairs] 
amrp2e = public (fmrp2e)

--Sum says: Now I know the two numbers too
fmrs3e = Conj [(Disj[Neg (Conj [Prop (P x),Prop (Q y)]), 
		     K a (Conj [Prop (P x),Prop (Q y)]) ] )|(x,y)<-pairs]
amrs3e = public (fmrs3e)

solution = showM (upds msnp [amrs1e, amrp2e, amrs3e])