-- | Possibly doubly pointed lattices

module Compiler.Hoopl.Pointed
, liftJoinTop, extendJoinDomain
, WithTop, WithBot, WithTopAndBot
)
where

import Compiler.Hoopl.Graph
import Compiler.Hoopl.Label
import Compiler.Hoopl.Dataflow

-- | Adds top, bottom, or both to help form a lattice
data Pointed t b a where
Bot   ::      Pointed t C a
PElem :: a -> Pointed t b a
Top   ::      Pointed C b a

-- ^ The type parameters 't' and 'b' are used to say whether top
-- and bottom elements have been added.  The analogy with 'Block'
-- is nearly exact:
--
--  * A 'Block' is closed at the entry if and only if it has a first node;
--    a 'Pointed' is closed at the top if and only if it has a top element.
--
--  * A 'Block' is closed at the exit if and only if it has a last node;
--    a 'Pointed' is closed at the bottom if and only if it has a bottom element.
--
-- We thus have four possible types, of which three are interesting:
--
--  [@Pointed C C a@] Type @a@ extended with both top and bottom elements.
--
--  [@Pointed C O a@] Type @a@ extended with a top element
--  only. (Presumably @a@ comes equipped with a bottom element of its own.)
--
--  [@Pointed O C a@] Type @a@ extended with a bottom element only.
--
--  [@Pointed O O a@] Isomorphic to @a@, and therefore not interesting.
--
-- 'Bot', 'Top', and 'PElem' can all be used polymorphically.
--
-- A 'Pointed t b' type is an instance of 'Functor' and 'Show'.

type WithBot a = Pointed O C a
-- ^ Type 'a' with a bottom element adjoined

type WithTop a = Pointed C O a
-- ^ Type 'a' with a top element adjoined

type WithTopAndBot a = Pointed C C a
-- ^ Type 'a' with top and bottom elements adjoined

-- | Given a join function and a name, creates a semi lattice by
-- adding a bottom element, and possibly a top element also.
-- A specialized version of 'addPoints''.
addPoints  :: String -> JoinFun a -> DataflowLattice (Pointed t C a)
-- | A more general case for creating a new lattice
addPoints' :: forall a t .
String
-> (Label -> OldFact a -> NewFact a -> (ChangeFlag, Pointed t C a))
-> DataflowLattice (Pointed t C a)

where join' l o n = (change, PElem f)
where (change, f) = join l o n

addPoints' name joinx = DataflowLattice name Bot join
where -- careful: order of cases matters for ChangeFlag
join :: JoinFun (Pointed t C a)
join _ (OldFact f)            (NewFact Bot) = (NoChange, f)
join _ (OldFact Top)          (NewFact _)   = (NoChange, Top)
join _ (OldFact Bot)          (NewFact f)   = (SomeChange, f)
join _ (OldFact _)            (NewFact Top) = (SomeChange, Top)
join l (OldFact (PElem old)) (NewFact (PElem new))
= joinx l (OldFact old) (NewFact new)

liftJoinTop :: JoinFun a -> JoinFun (WithTop a)
extendJoinDomain :: forall a
. (Label -> OldFact a -> NewFact a -> (ChangeFlag, WithTop a))
-> JoinFun (WithTop a)

extendJoinDomain joinx = join
where join :: JoinFun (WithTop a)
join _ (OldFact Top)          (NewFact _)   = (NoChange, Top)
join _ (OldFact _)            (NewFact Top) = (SomeChange, Top)
join l (OldFact (PElem old)) (NewFact (PElem new))
= joinx l (OldFact old) (NewFact new)

liftJoinTop joinx = extendJoinDomain (\l old new -> liftPair \$ joinx l old new)
where liftPair (c, a) = (c, PElem a)

-- | Given a join function and a name, creates a semi lattice by
-- adding a top element but no bottom element.  Caller must supply the bottom
-- element.
addTop  :: DataflowLattice a -> DataflowLattice (WithTop a)
-- | A more general case for creating a new lattice
String
-> a
-> (Label -> OldFact a -> NewFact a -> (ChangeFlag, WithTop a))
-> DataflowLattice (WithTop a)

where name' = fact_name lattice ++ " + T"
join' l o n = (change, PElem f)
where (change, f) = fact_join lattice l o n

addTop' name bot joinx = DataflowLattice name (PElem bot) join
where -- careful: order of cases matters for ChangeFlag
join :: JoinFun (WithTop a)
join _ (OldFact Top)          (NewFact _)   = (NoChange, Top)
join _ (OldFact _)            (NewFact Top) = (SomeChange, Top)
join l (OldFact (PElem old)) (NewFact (PElem new))
= joinx l (OldFact old) (NewFact new)

instance Show a => Show (Pointed t b a) where
show Bot = "_|_"
show Top = "T"
show (PElem a) = show a

instance Functor (Pointed t b) where
fmap _ Bot = Bot
fmap _ Top = Top
fmap f (PElem a) = PElem (f a)

instance Eq a => Eq (Pointed t b a) where
Bot == Bot = True
Top == Top = True
(PElem a) == (PElem a') = a == a'
_ == _ = False

instance Ord a => Ord (Pointed t b a) where
Bot     `compare` Bot      = EQ
Bot     `compare` _        = LT
_       `compare` Bot      = GT
PElem a `compare` PElem a' = a `compare` a'
Top     `compare` Top      = EQ
Top     `compare` _        = GT
_       `compare` Top      = LT