repos / machines.hs.git

commit

d487e9f

parent

fd04588

author

Evgenii Akentev

date

2024-09-07 14:54:54 +0400 +04

Add Virtual CEK and Krivine machines

 1@@ -17,7 +17,10 @@ library
 2                       Abstract.SECD,
 3                       Abstract.SEC,
 4                       Abstract.SE,
 5-                      Abstract.EC
 6+                      Abstract.EC,
 7+
 8+                      Virtual.CEK,
 9+                      Virtual.Krivine
10     build-depends:    base ^>=4.18.2.1
11     hs-source-dirs:   src
12     default-language: Haskell2010

 1@@ -0,0 +1,59 @@
 2+{-# LANGUAGE LambdaCase #-}
 3+
 4+-- From Interpreter to Compiler and
 5+-- Virtual Machine: A Functional Derivation
 6+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
 7+
 8+module Virtual.CEK where
 9+
10+data Term = Var String | Lam String Term | App Term Term
11+  deriving (Show)
12+
13+data Inst = Access String | Close String [Inst] | Push [Inst]
14+  deriving (Show)
15+
16+compile :: Term -> [Inst]
17+compile = \case
18+  (Var x) -> [Access x]
19+  (Lam x t) -> [Close x (compile t)]
20+  (App t0 t1) -> [Push (compile t1)] ++ compile t0
21+
22+type Env = [(String, Val)]
23+data Val = Closure String [Inst] Env
24+  deriving (Show)
25+
26+data Context = C0 | C1 [Inst] Env Context | C2 Val Context
27+  deriving (Show)
28+
29+transition1 :: [Inst] -> Env -> Context -> (Context, Val)
30+transition1 (Access x : _) e k = case lookup x e of
31+  Just v -> transition2 k v
32+  Nothing -> error "var not in scope"
33+transition1 (Close x c' : _) e k = transition2 k (Closure x c' e)
34+transition1 (Push c' : c) e k = transition1 c e (C1 c' e k)
35+
36+transition2 :: Context -> Val -> (Context, Val)
37+transition2 (C1 c e k) v = transition1 c e (C2 v k)
38+transition2 (C2 (Closure x c e) k) v = transition1 c ((x, v):e) k
39+transition2 C0 v = (C0, v)
40+
41+run :: [Inst] -> Val
42+run c =
43+  let (C0, v) = transition1 c [] C0
44+  in v
45+
46+eval :: Term -> Val
47+eval t = run $ compile t
48+
49+t1 :: Term
50+t1 = App (Lam "x" (App (Var "x") (Var "x"))) (Lam "x" (Var "x"))
51+
52+ex1 :: Val
53+ex1 = eval t1
54+
55+--((λ 0) (λ 0)) (λ 0)
56+t2 :: Term
57+t2 = App (App (Lam "x" $ Var "x") (Lam "x" $ Var "x")) (Lam "x" $ Var "x")
58+
59+ex2 :: Val
60+ex2 = eval t2

 1@@ -0,0 +1,51 @@
 2+{-# language LambdaCase #-}
 3+
 4+-- From Interpreter to Compiler and
 5+-- Virtual Machine: A Functional Derivation
 6+-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
 7+
 8+module Virtual.Krivine where
 9+
10+data Term = Var Int | Lam String Term | App Term Term
11+  deriving (Show)
12+
13+data Inst = Access Int | Grab String | Push [Inst]
14+  deriving (Show)
15+
16+compile :: Term -> [Inst]
17+compile = \case
18+  (Var n) -> [Access n]
19+  (Lam x t) -> Grab x : compile t
20+  (App t0 t1) -> Push (compile t1) : compile t0
21+
22+type Env = [Val]
23+data Val = Closure [Inst] Env
24+  deriving (Show)
25+data Res = Result String Env
26+  deriving (Show)
27+type Stack = [Val]
28+
29+step :: [Inst] -> Env -> Stack -> Res
30+step (Access n : _) e s = let (Closure c' e') = e!!n in step c' e' s
31+step (Grab _ : c) e (Closure c' e' :s) = step c (Closure c' e' :e) s
32+step (Push c' : c) e s = step c e (Closure c' e : s)
33+step (Grab l : c) e [] = Result l e
34+
35+run :: [Inst] -> Res
36+run c = step c [] []
37+
38+eval :: Term -> Res
39+eval t = run $ compile t
40+
41+t1 :: Term
42+t1 = App (Lam "x" (App (Var 0) (Var 0))) (Lam "x" (Var 0))
43+
44+ex1 :: Res 
45+ex1 = eval t1
46+
47+--((λ 0) (λ 0)) (λ 0)
48+t2 :: Term
49+t2 = App (App (Lam "x" $ Var 0) (Lam "x" $ Var 0)) (Lam "x" $ Var 0)
50+
51+ex2 :: Res 
52+ex2 = eval t2