repos / machines.hs.git

CAM.hs

 1{-# language LambdaCase #-}
 2
 3module Virtual.CAM 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 = Var Int | Lam Term | App Term Term | Nil | MkPair Term Term | Car Term | Cdr Term | Lit Int
10
11data Inst = Fst | Snd | Push | Swap | Cons | Call | Cur [Inst] | Quote Val
12  deriving (Show)
13
14data Val = Null | Pair Val Val | Closure Val [Inst] | Num Int
15  deriving (Show)
16
17type Stack = [Val]
18
19compile :: Term -> [Inst]
20compile = \case
21  (Var 0) -> [Snd]
22  (Var n) -> Fst : compile (Var $ n - 1)
23  (Lam t) -> [Cur $ compile t]
24  (App t0 t1) -> Push : compile t0 ++ (Swap : compile t1) ++ [Cons, Call]
25  Nil -> [Quote Null]
26  (MkPair t0 t1) -> Push : compile t0 ++ (Swap : compile t1) ++ [Cons]
27  (Car t) -> compile t ++ [Fst]
28  (Cdr t) -> compile t ++ [Snd]
29  (Lit n) -> [Quote $ Num n]
30
31run :: [Inst] -> Val -> Stack -> Val
32run (Fst : c) (Pair v1 _) s = run c v1 s
33run (Snd : c) (Pair _ v2) s = run c v2 s
34run (Quote v': c) _ s = run c v' s
35run (Cur c' : c) v s = run c (Closure v c') s
36run (Push : c) v s = run c v (v : s)
37run (Swap : c) v (v' : s) = run c v' (v : s)
38run (Cons : c) v (v' : s) = run c (Pair v' v) s 
39run (Call : c) (Pair (Closure v c') v') s = run (c' ++ c) (Pair v v') s
40run [] v [] = v
41
42eval :: Term -> Val
43eval t = run (compile t) Null []
44
45t1 :: Term
46t1 = Car $ MkPair (Lit 1) (Lit 2)
47
48ex1 :: Val 
49ex1 = eval t1
50
51--((λ 0) (λ 0)) (λ 0)
52t2 :: Term
53t2 = App (App (Lam $ Var 0) (Lam $ Var 0)) (Lam $ Var 0)
54
55ex2 :: Val 
56ex2 = eval t2