-- This file contains a Hugs implementation of the programs described in:
--
-- Mark P. Jones, Computing with lattices: An application of type classes,
-- Journal of Functional Programming, Volume 2, Number 4, Oct 1992.
--

module Lattice where

class Eq a => Lattice a where           -- A type class representing lattices
    bottom, top :: a
    meet, join  :: a -> a -> a
    lt          :: a -> a -> Bool
    x `lt` y     = (x `join` y) == y

instance Lattice Bool where             -- Simple instances of Lattice
    bottom = False
    top    = True
    meet   = (&&)
    join   = (||)

instance (Lattice a, Lattice b) => Lattice (a,b) where
    bottom             = (bottom,bottom)
    top                = (top,top)
    (x,y) `meet` (u,v) = (x `meet` u, y `meet` v)
    (x,y) `join` (u,v) = (x `join` u, y `join` v)


-- Defining the least fixed point operator:

fix f          = firstRepeat (iterate f bottom)
firstRepeat xs = head [ x | (x,y) <- zip xs (tail xs), x==y ]


-- Maximum and minimum frontiers:

data Minf a = Minf [a]
data Maxf a = Maxf [a]

instance Eq a => Eq (Minf a) where                -- Equality on Frontiers
    (Minf xs) == (Minf ys)  = setEquals xs ys

instance Eq a => Eq (Maxf a) where
    (Maxf xs) == (Maxf ys)  = setEquals xs ys

xs `subset` ys  = all (`elem` ys) xs
setEquals xs ys =  xs `subset` ys  &&  ys `subset` xs

instance Lattice a => Lattice (Minf a) where      -- Lattice structure
    bottom                     = Minf []
    top                        = Minf [bottom]
    (Minf xs) `meet` (Minf ys) = minimal [ x`join`y | x<-xs, y<-ys ]
    (Minf xs) `join` (Minf ys) = minimal (xs++ys)

instance Lattice a => Lattice (Maxf a) where
    bottom                     = Maxf []
    top                        = Maxf [top]
    (Maxf xs) `meet` (Maxf ys) = maximal [ x`meet`y | x<-xs, y<-ys ]
    (Maxf xs) `join` (Maxf ys) = maximal (xs++ys)

-- Find maximal elements of a list xs with respect to partial order po:

maximalWrt po = loop []
 where loop xs []                 = xs
       loop xs (y:ys)
            | any (po y) (xs++ys) = loop xs ys
            | otherwise           = loop (y:xs) ys

minimal :: Lattice a => [a] -> Minf a       -- list to minimum frontier
minimal  = Minf . maximalWrt (flip lt)
maximal :: Lattice a => [a] -> Maxf a       -- list to maximum frontier
maximal  = Maxf . maximalWrt lt

-- A representation for functions of type Lattice a => a -> Bool:

data Fn a = Fn (Minf a) (Maxf a)

instance Eq a => Eq (Fn a) where
    Fn f1 f0 == Fn g1 g0  =  f1==g1 -- && f0==g0

instance Lattice a => Lattice (Fn a) where
    bottom               = Fn bottom top
    top                  = Fn top bottom
    Fn u l `meet` Fn v m = Fn (u `meet` v) (l `join` m)
    Fn u l `join` Fn v m = Fn (u `join` v) (l `meet` m)

-- Navigable lattices:

class Lattice a => Navigable a where
    succs :: a -> Minf a
    preds :: a -> Maxf a

maxComp :: Navigable a => [a] -> Maxf a   -- implementation of complement
maxComp  = foldr meet top . map preds
minComp :: Navigable a => [a] -> Minf a
minComp  = foldr meet top . map succs

instance Navigable Bool where             -- instances of Navigable
    succs False = Minf [True]
    succs True  = Minf []
    preds False = Maxf []
    preds True  = Maxf [False]

minfOf (Minf xs) = xs
maxfOf (Maxf xs) = xs

instance (Navigable a, Navigable b) => Navigable (a,b) where
    succs (x,y) = Minf ([(sx,bottom) | sx <- minfOf (succs x)] ++
                        [(bottom,sy) | sy <- minfOf (succs y)])
    preds (x,y) = Maxf ([(px,top)    | px <- maxfOf (preds x)] ++
                        [(top,py)    | py <- maxfOf (preds y)])

instance Navigable a => Navigable (Fn a) where
    succs (Fn f1 f0) = Minf [Fn (Minf [y]) (preds y) | y <- maxfOf f0]
    preds (Fn f1 f0) = Maxf [Fn (succs x) (Maxf [x]) | x <- minfOf f1]

-- Upwards and downwards closure operators:

upwards (Minf [])         = []
upwards ts@(Minf (t:_))   = t : upwards (ts `meet` succs t)

downwards (Maxf [])       = []
downwards ts@(Maxf (t:_)) = t : downwards (ts `meet` preds t)

elements :: Navigable a => [a]    -- enumerate all elements in lattice
elements  = upwards top