repos / machines.hs.git

VEC.hs

 1{-# language LambdaCase #-}
 2
 3module Virtual.VEC where
 4
 5-- From Interpreter to Compiler and
 6-- Virtual Machine: A Functional Derivation
 7-- https://pdfs.semanticscholar.org/08f9/c12239dd720cb28a1039db9ce706cc7ee3b2.pdf
 8
 9data Term = App Term Term | CBNLam String Term | CBVLam String Term | Var String | Lit Literal | Succ Term | IfThenElse Term Term Term 
10data Literal = BoolLit Bool | NumLit Int
11  deriving (Show)
12data Inst = Pushclosure [Inst] | Pushconst Literal | Call | Return | Push String | Bind String | Incr | Test [Inst] [Inst]
13  deriving (Show)
14type Env = [(String, Val)]
15data Val = Closure [Inst] Env | Primitive Literal
16  deriving (Show)
17
18compile :: Term -> [Inst]
19compile = \case
20  (App t0 t1) -> Pushclosure (compile t1 ++ [Return]) : compile t0 ++ [Call] 
21  (CBNLam x t) -> [Pushclosure (Bind x : compile t ++ [Return])]
22  (CBVLam x t) -> [Pushclosure (Call : Bind x : compile t ++ [Return])]
23  (Var x) -> [Push x]
24  (Lit l) -> [Pushconst l]
25  (Succ t) -> compile t ++ [Incr]
26  (IfThenElse t0 t1 t2) -> compile t0 ++ [Test (compile t1) (compile t2)]
27
28run :: [Val] -> [Env] -> [Inst] -> Val
29run vs (e : es) (Pushclosure c':cs) = run (Closure c' e : vs) (e : es) cs
30run vs es (Pushconst l : cs) = run (Primitive l:vs) es cs
31run (Closure c' e : vs) es (Call : cs) = run vs (e : es) (c' ++ cs)
32run vs (_:es) (Return : cs) = run vs es cs
33run vs (e:es) (Push x : cs) = case lookup x e of
34  Just v@(Primitive _) -> run (v : vs) (e : es) cs
35  Just (Closure c' e') -> run vs (e' : e : es) (c' ++ cs) 
36  Nothing -> error "var not in scope"
37run (v : vs) (e : es) (Bind x : cs) = run vs (((x, v):e) : es) cs
38run (Primitive (NumLit n) : vs) es (Incr : cs) = run (Primitive (NumLit $ n + 1) : vs) es cs
39run (Primitive (BoolLit True) : vs) es (Test c1 _ : cs) = run vs es (c1 ++ cs)
40run (Primitive (BoolLit False) : vs) es (Test _ c2 : cs) = run vs es (c2 ++ cs)
41run (v:_) _ [] = v 
42run _ _ _ = error "Impossible"
43
44eval :: Term -> Val
45eval t = run [] [[]] $ compile t
46
47t1 :: Term
48t1 = Succ $ (Lit $ NumLit 2)
49
50ex1 :: Val 
51ex1 = eval t1
52
53--((λ 0) (λ 0)) (λ 0)
54t2 :: Term
55t2 = App (App (CBNLam "x" $ Var "x") (CBNLam "x" $ Var "x")) (CBNLam "x" $ Var "x")
56
57ex2 :: Val 
58ex2 = eval t2
59
60t3 :: Term
61t3 = App (App (App (CBNLam "x" $ CBNLam "y" $ CBNLam "z" $ IfThenElse (Var "x") (Succ $ Var "y") (Var "z")) (Lit $ BoolLit True)) (Lit $ NumLit 2)) (Lit $ NumLit 7)
62
63ex3 :: Val
64ex3 = eval t3