repos / machines.hs.git

Krivine.hs

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