repos / machines.hs.git


machines.hs.git / src / Abstract
Evgenii Akentev  ·  2024-09-06

EC.hs

 1module Abstract.EC where
 2
 3-- https://www.brics.dk/RS/03/33/BRICS-RS-03-33.pdf
 4
 5data Term = Appl Term Term | Var String | Abst String Term | Lit Int
 6  deriving (Show)
 7
 8data Val = Num Int | Succ | Closure Term String Env
 9  deriving (Show)
10
11type Env = [(String, Val)]
12
13data Stackable = SEnv Env 
14               | STerm Term
15               | SVal Val
16
17type C = [Stackable]
18
19initEnv :: Env
20initEnv = [("succ", Succ)]
21
22runC :: (Val, Env, C) -> Val
23runC (v, e, []) = v
24runC (v, e, (SEnv e'):c) = runC (v, e', c)
25runC (v1, e, (STerm t0):c) = runT (t0, e, (SVal v1):c)
26runC (v0, e, (SVal v1):c) = runA (v0, v1, e, c)
27
28runT :: (Term, Env, C) -> Val
29runT (Lit n, e, c) = runC (Num n, e, c)
30runT (Var x, e, c) = case lookup x e of
31  Just v -> runC (v, e, c)
32  Nothing -> error "var is not in scope"
33runT (Abst x t, e, c) = runC (Closure t x e, e, c)
34runT (Appl t0 t1, e, c) = runT (t1, e, (STerm t0):c)
35
36runA :: (Val, Val, Env, C) -> Val 
37runA (Succ, Num n, e, c) = runC (Num $ n + 1, e, c)
38runA (Closure t x e', v, e, c) = runT (t, (x, v):e', (SEnv e):c)
39
40-- (\ 0 0) (\ 0)
41t1 :: Term
42t1 = Appl (Abst "x" (Appl (Var "x") (Var "x"))) (Abst "x" (Appl (Var "succ") (Lit 1)))
43
44ex1 :: Val
45ex1 = runT (t1, initEnv, [])
46
47--((λ 0) (λ 0)) (λ 0)
48t2 :: Term
49t2 = Appl (Appl (Abst "x" $ Var "x") (Abst "x" $ Var "x")) (Abst "x" $ Var "x")
50
51ex2 :: Val
52ex2 = runT (t2, initEnv, [])