mirror of https://gitlab.com/baco/l-c2019.git
109 lines
3.2 KiB
Haskell
109 lines
3.2 KiB
Haskell
{-# 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
|