repos / machines.hs.git

commit

d12d51c

parent

2b5df21

author

Evgenii Akentev

date

2024-09-05 09:26:26 +0400 +04

Add SECD

1@@ -12,7 +12,7 @@ common warnings
2 
3 library
4     import:           warnings
5-    exposed-modules:  Krivine, CEK
6+    exposed-modules:  Krivine, CEK, SECD
7     build-depends:    base ^>=4.18.2.1
8     hs-source-dirs:   src
9     default-language: Haskell2010

 1@@ -1,21 +1,62 @@
 2 module SECD where
 3 
 4 -- https://en.wikipedia.org/wiki/SECD_machine
 5+-- https://www.brics.dk/RS/03/33/BRICS-RS-03-33.pdf
 6 
 7-data Inst
 8-  = Nil
 9-  | Ldc
10-  | Ld
11-  | Sel
12-  | Join
13-  | Ldf
14-  | Ap
15-  | Ret
16-  | Dum
17-  | Rap
18-
19-data State = State
20-  -- Control
21-  -- Environment
22-  -- Stack
23-  -- Dump
24+data Term = Appl Term Term | Var String | Abst String Term | Lit Int
25+  deriving (Show)
26+
27+data Val = Num Int | Succ | Closure Term String Env
28+  deriving (Show)
29+
30+data Directive = DTerm Term | DApply
31+
32+type Stack = [Val]
33+type Env = [(String, Val)]
34+type Control = [Directive]
35+type Dump = [(Stack, Env, Control)]
36+
37+initEnv :: Env
38+initEnv = [("succ", Succ)]
39+
40+-- S, E, C, D -> val
41+run :: Stack -> Env -> Control -> Dump -> Val
42+run (v:[]) _ [] [] = v
43+-- ret
44+run (v:[]) _ [] ((s, e, c):d) = run (v:s) e c d
45+-- ldc 
46+run s e ((DTerm (Lit n)):c) d = run ((Num n):s) e c d
47+
48+run s e ((DTerm (Var x)):c) d = case lookup x e of
49+  Just v' -> run (v':s) e c d 
50+  Nothing -> error "Var is undefined"
51+
52+run s e ((DTerm (Abst x t)):c) d = run ((Closure t x e):s) e c d
53+
54+run s e ((DTerm (Appl t0 t1)):c) d =
55+  run s e ((DTerm t1):(DTerm t0):DApply:c) d
56+
57+run (Succ:(Num n):s) e (DApply:c) d = run ((Num $ n + 1):s) e c d
58+
59+-- ap
60+run ((Closure t x e'):v':s) e (DApply:c) d =
61+  run [] ((x, v'):e') [DTerm t] ((s, e, c):d)
62+
63+run _ _ _ _ = error "impossible"
64+
65+eval :: Term -> Val
66+eval t = run [] initEnv [DTerm t] []
67+
68+-- (\ 0 0) (\ 0)
69+t1 :: Term
70+t1 = Appl (Abst "x" (Appl (Var "x") (Var "x"))) (Abst "x" (Appl (Var "succ") (Lit 1)))
71+
72+ex1 :: Val
73+ex1 = eval t1
74+
75+--((λ 0) (λ 0)) (λ 0)
76+t2 :: Term
77+t2 = Appl (Appl (Abst "x" $ Var "x") (Abst "x" $ Var "x")) (Abst "x" $ Var "x")
78+
79+ex2 :: Val
80+ex2 = eval t2