Evgenii Akentev
·
2024-09-06
SECD.hs
1module Abstract.SECD where
2
3-- https://en.wikipedia.org/wiki/SECD_machine
4-- https://www.brics.dk/RS/03/33/BRICS-RS-03-33.pdf
5
6data Term = Appl Term Term | Var String | Abst String Term | Lit Int
7 deriving (Show)
8
9data Val = Num Int | Succ | Closure Term String Env
10 deriving (Show)
11
12data Directive = DTerm Term | DApply
13
14type Stack = [Val]
15type Env = [(String, Val)]
16type Control = [Directive]
17type Dump = [(Stack, Env, Control)]
18
19initEnv :: Env
20initEnv = [("succ", Succ)]
21
22-- S, E, C, D -> val
23run :: Stack -> Env -> Control -> Dump -> Val
24run (v:[]) _ [] [] = v
25-- ret
26run (v:[]) _ [] ((s, e, c):d) = run (v:s) e c d
27-- ldc
28run s e ((DTerm (Lit n)):c) d = run ((Num n):s) e c d
29
30run s e ((DTerm (Var x)):c) d = case lookup x e of
31 Just v' -> run (v':s) e c d
32 Nothing -> error "Var is undefined"
33
34run s e ((DTerm (Abst x t)):c) d = run ((Closure t x e):s) e c d
35
36run s e ((DTerm (Appl t0 t1)):c) d =
37 run s e ((DTerm t1):(DTerm t0):DApply:c) d
38
39run (Succ:(Num n):s) e (DApply:c) d = run ((Num $ n + 1):s) e c d
40
41-- ap
42run ((Closure t x e'):v':s) e (DApply:c) d =
43 run [] ((x, v'):e') [DTerm t] ((s, e, c):d)
44
45run _ _ _ _ = error "impossible"
46
47eval :: Term -> Val
48eval t = run [] initEnv [DTerm t] []
49
50-- (\ 0 0) (\ 0)
51t1 :: Term
52t1 = Appl (Abst "x" (Appl (Var "x") (Var "x"))) (Abst "x" (Appl (Var "succ") (Lit 1)))
53
54ex1 :: Val
55ex1 = eval t1
56
57--((λ 0) (λ 0)) (λ 0)
58t2 :: Term
59t2 = Appl (Appl (Abst "x" $ Var "x") (Abst "x" $ Var "x")) (Abst "x" $ Var "x")
60
61ex2 :: Val
62ex2 = eval t2