-- syntax of While

type Var = String

--type Num = Integer

data Aexp = Var Var | Num Integer
          | Aexp :+ Aexp | Aexp :- Aexp | Aexp :* Aexp

data Bexp = T | F | Aexp :== Aexp | Aexp :<= Aexp 
          | Not Bexp | Bexp :&& Bexp | Bexp :|| Bexp 

data Stm  = Var := Aexp | Skip | Stm :\ Stm
          | If Bexp Stm Stm | While Bexp Stm



data AbsInt  = NoInt | Zero | Neg | Pos | NonZero | NonNeg | NonPos | AnyInt
         deriving (Eq, Show) 

absint :: Integer -> AbsInt
absint x | x == 0 = Zero
         | x <  0 = Neg
         | x >  0 = Pos 

instance Num AbsInt where
  NoInt + i = NoInt
  AnyInt + i = AnyInt
  Zero + i = i 
  Neg + Neg = Neg 
  i + Zero = i
  Neg + Pos = AnyInt
  i + AnyInt = AnyInt
  Pos + Neg = AnyInt 
  Pos + Pos = Pos
  --
  NoInt - i = NoInt
  Neg - Pos = Neg
  AnyInt - i = AnyInt
  Pos - Pos = AnyInt
 

data AbsBool = NoBool | TT | FF | AnyBool 
         deriving (Eq, Show)  

absbool :: Bool -> AbsBool
absbool True  = TT
absbool False = FF

--

class Lattice a where
  join :: a -> a -> a
  bottom :: a

instance Lattice AbsInt where
  NoInt `join` x = x
  x `join` NoInt = x
  AnyInt `join` x = AnyInt
  Pos `join` Pos = Pos
  Neg `join` Neg = Neg
  bottom = NoInt

instance Lattice AbsBool where
  NoBool `join` x = x
  x `join` NoBool = x
  TT `join` FF = AnyBool
  bottom = NoBool

instance Lattice b => Lattice (a -> b) where
  (f `join` g) x = f x `join` g x
  bottom x = bottom



-- semantic categories for direct style denotational semantics

type State = Var -> Integer

allzeros :: State
allzeros x = 0

type AbsState = Var -> AbsInt

allanys :: AbsState
allanys x = AnyInt

allnones :: AbsState
allnones x = NoInt

update :: Eq a => (a -> b)  -> a -> b -> (a -> b)
update st y z x = if x == y then z else st x

cond :: (State -> Bool, State -> State, State -> State) -> (State -> State)
cond (pred, g1, g2) st = if pred st then g1 st else g2 st

abscond :: (AbsState -> AbsBool, AbsState -> AbsState, AbsState -> AbsState) -> 
        (AbsState -> AbsState)

abscond (pred, g1, g2) st = case pred st of 
       NoBool  -> allnones
       TT      -> g1 st
       FF      -> g2 st
       AnyBool -> g1 st `join` g2 st

fix :: (a -> a) -> a
fix f = f (fix f)

fixappr :: (Lattice a, Eq a) => (a -> a) -> a
--fix  :: ((State -> State) -> (State -> State)) -> (State -> State)
fixappr f = fixappr' f bottom

fixappr' :: (Lattice a, Eq a) => (a -> a) -> a -> a
fixappr' f a = let a' = f a
           in if a' == a then a else fixappr' f a'

instance Eq a => Eq (Var -> a) where
   f == g = f "x" == g "x" && f "y" == g "y" && f "z" == g "z" 


-- direct style denotational semantics 

-- -- arithmetical expressions

semA :: Aexp -> State -> Integer
semA (Var x) st    = st x
semA (Num n) st    = n
semA (a1 :+ a2) st = semA a1 st + semA a2 st 
semA (a1 :- a2) st = semA a1 st - semA a2 st 
semA (a1 :* a2) st = semA a1 st * semA a2 st 

abssemA :: Aexp -> AbsState -> AbsInt
abssemA (Var x) st    = st x
abssemA (Num n) st    = absint n
abssemA (a1 :+ a2) st = abssemA a1 st + abssemA a2 st 
abssemA (a1 :- a2) st = abssemA a1 st - abssemA a2 st 
abssemA (a1 :* a2) st = abssemA a1 st * abssemA a2 st 


-- -- boolean expressions

semB :: Bexp -> State -> Bool
semB T st   = True
semB F st   = False
semB (a1 :== a2) st = semA a1 st == semA a2 st
semB (a1 :<= a2) st = semA a1 st <= semA a2 st
semB (Not b) st     = not (semB b st)
semB (b1 :&& b2) st = semB b1 st && semB b2 st
semB (b1 :|| b2) st = semB b1 st || semB b2 st


abssemB :: Bexp -> AbsState -> AbsBool
abssemB T st   = TT
abssemB F st   = FF

abssemB (a1 :== a2) st = case (abssemA a1 st, abssemA a2 st) of
                             (NoInt, _) -> NoBool
                             (Pos, Neg) -> FF
                             (Pos, Zero) -> FF
                             (Pos, Pos) -> AnyBool
                             (AnyInt, _) -> AnyBool
                             (_, AnyInt) -> AnyBool
                             (Zero, Zero) -> TT
                             (Neg, Zero) -> FF


--abssemB (a1 :<= a2) st = abssemA a1 st <= abssemA a2 st
abssemB (Not b) st     = case abssemB b st of  
                              NoBool -> NoBool 
                              TT -> FF
                              FF -> TT
                              AnyBool -> AnyBool


--abssemB (b1 :&& b2) st = abssemB b1 st && abssemB b2 st
--abssemB (b1 :|| b2) st = abssemB b1 st || abssemB b2 st


-- -- statements

dssemS :: Stm -> State -> State
dssemS (x := a) st     = update st x (semA a st)
dssemS Skip st         = st 
dssemS (s1 :\ s2) st   = (dssemS s2 . dssemS s1) st
dssemS (If b s1 s2) st = cond (semB b, dssemS s1, dssemS s2) st
dssemS (While b s) st  = fix f st where
                           f g = cond (semB b, g . dssemS s, id)

dsabssemS :: Stm -> AbsState -> AbsState
dsabssemS (x := a) st     = update st x (abssemA a st)
dsabssemS Skip st         = st 
dsabssemS (s1 :\ s2) st   = (dsabssemS s2 . dsabssemS s1) st
dsabssemS (If b s1 s2) st = abscond (abssemB b, dsabssemS s1, dsabssemS s2) st
{-
dsabssemS (While b s) st  = fixappr f st where
                           f g = abscond (abssemB b, g . dsabssemS s, id)
-}
dsabssemS (While b s) st  = fixappr f where
                           f st' = (case abssemB b st' of 
                                      NoBool -> allnones
                                      TT -> dsabssemS s st'
                                      FF -> allnones
                                      AnyBool -> dsabssemS s st') `join` st

-- example

{-

   fact is abstract syntax for 

   y := 1 ; while not (x = 1) do (y := y + x ; x := x - 1) 

-}

--fact :: Stm
fact = ("y" := Num 1) :\
       (While (Not (Var "x" :== Num 0))
                  (("y" := (Var "y" :+ Var "x")) :\ ("x" := (Var "x" :- Num 1))
                  )
       )

 
               

testfact :: AbsInt -> (AbsInt, AbsInt)
testfact z = (st' "x", st' "y") where 
               st' = dsabssemS fact st where
                 st  = update allanys "x" z