{-# LANGUAGE GADTs #-}

module Lab5 where

--         ∞
-- fix f = ⊔ fⁱ ⊥
--        i=0
fix :: (a -> a) -> a
fix f = f (fix f)

type Iden = String
type Σ = Iden -> Int

data Ω = Normal Σ | Abort Σ | Out (Int, Ω) | In (Int -> Ω)

update :: Σ -> Iden -> Int -> Σ
update σ v n v' = if v == v' then n else σ v'

data Expr a where
    -- Expresiones enteras
    Const :: Int -> Expr Int  -- n
    Var :: String -> Expr Int  -- v
    Plus :: Expr Int -> Expr Int -> Expr Int  -- e + e'
    -- Expresiones booleanas
    Eq :: Expr Int -> Expr Int -> Expr Bool  -- e = e'
    Lt :: Expr Int -> Expr Int -> Expr Bool  -- e < e'
    -- Comandos
    Skip :: Expr Ω  -- skip
    NewVar :: Iden -> Expr Int -> Expr Ω -> Expr Ω  -- newvar v := e in e'
    Assign :: Iden -> Expr Int -> Expr Ω  -- v := e
    Fail :: Expr Ω  -- fail
    Catch :: Expr Ω -> Expr Ω -> Expr Ω  -- catch c with c'
    While :: Expr Bool -> Expr Ω -> Expr Ω  -- while b do c
    If :: Expr Bool -> Expr Ω -> Expr Ω -> Expr Ω  -- if b then c else c'
    Seq :: Expr Ω -> Expr Ω -> Expr Ω  -- c ; c'
    EMark :: Expr Int -> Expr Ω  -- !e
    QMark :: String -> Expr Ω  -- ?v

class DomSem dom where
    sem :: Expr dom -> Σ -> dom

instance DomSem Int where
    sem (Const a) = \_ -> a
    sem (Var v) = \σ -> σ v
    sem (Plus e1 e2) = \σ -> sem e1 σ + sem e2 σ

instance DomSem Bool where
    sem (Eq e1 e2) = \σ -> sem e1 σ == sem e2 σ
    sem (Lt e1 e2) = \σ -> sem e1 σ < sem e2 σ

(*.) :: (Σ -> Ω) -> Ω -> Ω
(*.) f (Normal σ) = f σ
(*.) _ (Abort σ) = Abort σ
(*.) f (Out (n, ω)) = Out (n, f *. ω)
(*.) f (In g) = In ((f *.) . g)

(†.) :: (Σ -> Σ) -> Ω -> Ω
(†.) f (Normal σ) = Normal $ f σ
(†.) f (Abort σ) = Abort $ f σ
(†.) f (Out (n, ω)) = Out (n, f †. ω)
(†.) f (In g) = In ((f †.) . g)

(+.) :: (Σ -> Ω) -> Ω -> Ω
(+.) _ (Normal σ) = Normal σ
(+.) f (Abort σ) = f σ
(+.) f (Out (n, ω)) = Out (n, f +. ω)
(+.) f (In g) = In ((f +.) . g)

instance DomSem Ω where
    sem Skip = \σ -> Normal σ
    sem (NewVar v e c) = \σ ->
        (\σ' -> update σ' v (σ v))
            †. (sem c (update σ v (sem e σ)))
    sem (Assign v n) = \σ -> Normal (update σ v (sem n σ))
    sem Fail = \σ -> Abort σ
    sem (Catch c c') = \σ -> sem c' +. (sem c σ)
    sem (While b p) = fix f
      where
        f :: (Σ -> Ω) -> (Σ -> Ω)
        f ω σ
            | sem b σ = ω *. (sem p σ)
            | otherwise = Normal σ
    sem (If b p p') = \σ ->
        if sem b σ
            then sem p σ
            else sem p' σ
    sem (Seq c c') = \σ -> sem c' *. (sem c σ)
    sem (EMark e) = \σ -> Out (sem e σ, Normal σ)
    sem (QMark v) = \σ -> In (\n -> Normal (update σ v n))

-- | Funciones de evaluación de dom
class Eval dom where
    eval :: Expr dom -> Σ -> IO ()

instance Eval Int where
    eval e = putStrLn . show . sem e

instance Eval Bool where
    eval e = putStrLn . show . sem e

instance Eval Ω where
    eval e = unrollOmega . sem e
      where
        unrollOmega :: Ω -> IO ()
        unrollOmega (Normal σ) = return ()
        unrollOmega (Abort σ) = putStrLn "Abort"
        unrollOmega (Out (n, ω)) = putStrLn (show n) >> unrollOmega ω
        unrollOmega (In f) = getLine >>= unrollOmega . f . read