----------------------------------------------------------------------------------
----------------------------------------------------------------------------------

-- ***   Web Service Algebra: basic Haskell module ***

-- ***   (c) December 2007 by Peter Höfner and Florian Lautenbacher ***

----------------------------------------------------------------------------------
----------------------------------------------------------------------------------

module WebService where



-- homogen relations in Haskell

infixl 4  ??              -- subset-relation
infixl 5  \/ , /\ , !-    -- union, meet, set-difference
infixl 6  # , #! , !#, ## -- composition
infixl 7  ^^^, ^<=        -- power, limited iteration

--------------------------------------

type Rel a = [(a,a)]

--------------------------------------
empty = []

--------------------------------------

set s = deleteMultipleOccurences (qsort s)

-- Quicksort -------------------------

qsort [] = []

qsort (x:xs) = qsort begin ++ [x] ++ qsort end
  where begin = [ y | y <- xs, y <= x ]
        end = [ y | y <- xs, y >  x ]

-- sorted liste  (delete multiple occurences)---

deleteMultipleOccurences []  = []
deleteMultipleOccurences [x]  =  [x]
deleteMultipleOccurences (x:(y:s))  =
  if x == y then deleteMultipleOccurences (y:s)
            else x : deleteMultipleOccurences (y:s)

--------------------------------------

r \/ s  =  set (r ++ s)

--------------------------------------

s !- []  =  s
s !- (y:t)  =
  [x | x <- s, x /= y ] !- t
--------------------------------------


--------------------------------------

union :: [[a]] -> [a]
union  =  concat

--------------------------------------

(??) :: Eq a => a -> [a] -> Bool

x ?? s  =  any (==x) s

--------------------------------------

s /\ t  =  [ x | x <- s, x ?? t ]

-- euivalence (same elements) -----

equiv s t  =  (sub s t) && (sub t s)

-- inclusion -------------------------

sub s t    =  (s /\ t == s)

-- (co)domain -----------------------
dom r = set[fst u | u <- r]
cod r = set[snd u | u <- r]


-- diamonds (no check if p is a test, ks = knowledge set)
fd r p = dom (r#!p)
-- bd r p = cod (p#r)
fb r p = neg (fd r (neg p))
-- bb r p ks = neg (bd r (neg p ks)) ks
-- fb r p = neg (fd r (neg p powk)) powk
-- bb r p = neg (bd r (neg p powk)) powk
--------------------------------------

-- calculate knowledge set ------------------------

knowledge r = set (defset r ++ valset r)

-- definition- and value set -----

defset  r  =  set (map fst r)

valset r  =  set (map snd r)

-- Converse ----------------------------------

conv r = set [ (y,x) | (x,y) <- r ]

-- identity relation -------------------------

idRel r = set [ (x,x) | x <- knowledge r ]

-- composition -------------------------------

r # s =
  set [(x,y) | (x,z1)<-r, (z2,y)<-s, z1==z2] 
r #! p = 
  set [(x,y)| (x,y)<-r, y`elem`p]
p !# r = 
  set [(x,y)| (x,y)<-r, x`elem`p]
p##q = p/\q


--powers --------------------------------------

r^^^1      =  r
r^^^(n+1)  =  r # (r^^^n)

-----------------------------------------------

-- Iteration ----------------------------------

r^<=n  =  union [ r^^^i | i <- [1..n] ]

-----------------------------------------------

plus r  =  union [ r^^^i | i <- [1..] ]

-----------------------------------------------

------------Plus-------------------------------

pplus r = r \/ r # pplus r

--------------------------------------
--                                  --
--   Iteration with termination 	--
--                                  --
--------------------------------------

ttplus r  =  it4 r (r # r) r empty

it4 r s t u =
  if sub t u then u
             else it4 r (s # r) (t \/ s) t

ttstar r = idRel r \/ ttplus r

-- generating the powerset --------------------
powerset [] = [[]]
powerset (x:xs) = let p = powerset xs in p ++ map (x:) p

-- blow ---------------------------------------
blow ws = set[(i\/e,o\/e) | (i,o)<- ws, e<-powerset (k!-o)]
blowt p = set[p\/e | e<-powerset(k!-p)]

buildplan :: [[String]] -> Rel [String]
buildplan p = set[(set [], x) | x <- p]


-------------------------------------------------------------

star r = skip \/ ttplus r 

-------------------------------------------------------------
--define knowledge set (empty for the module)
k = []

powk = powerset k
-- assertions / tests ---------------------------
skip = [(x,x) | x <- powerset k]

-- negation of a test w.r.t. a knowledge power (skip) set
-- neg p ks = set [(x,x) | x<- ks,  not(x `elem` (defset p))]
neg p = powk !- p


----------------------------------------------------------------------------------
--PRINTING
----------------------------------------------------------------------------------

sep1 = "---------------------------------------------------------------------\n"
sep2 = "=====================================================================\n"

----------------------------------------------------------------------------------
-- print list

printTest1 wst = putStr (foldl (++) "" (map (++"\n") (map show wst)))
printTest2 wst = putStr (sep1 ++ foldl (++) "" (map (++"\n"++sep1) (map show wst)))
printTest3 wst = putStr (sep1 ++ foldl (++) "" (map (++sep1) (map unlines wst)))

printWS_hlp xs = putStr(sep1++foldl (++) "" (map (++"\n"++sep1) xs))

printWS1 ws = printWS_hlp [show x | x<- ws]
printWS2 ws = printWS_hlp [(show a)++"\n"++(show b) | (a,b)<- ws]
printWS3 ws = printWS_hlp [(show a)++"\n   ->\n"++(show (b!-a)) | (a,b)<- ws]
printWS4 ws = printWS_hlp ["INPUT:\n  "++(show a)++"\nOUTPUT:\n  "++(show b) | (a,b)<- ws]
printWS5 ws = printWS_hlp ["INPUT:\n  "++(show a)++"\nADDITIONAL OUTPUT:\n  "++(show (b!-a)) | (a,b)<- ws]
printWS6 ws = printWS_hlp ["INPUT:\n"++(unlines (map ("  "++) a))++"\nOUTPUT:\n"++(unlines (map ("  "++) b)) | (a,b)<- ws]
printWS7 ws = printWS_hlp ["INPUT:\n"++(unlines (map ("  "++) a))++"\nADDITIONAL OUTPUT:\n"++(unlines (map ("  "++)(b!-a))) | (a,b)<- ws]



out ws = printWS3 ws
outt ws = printTest2 ws