repos / machines.hs.git

Krivine.hs

 1module Abstract.Krivine where
 2
 3
 4-- https://www.pls-lab.org/en/Krivine_machine
 5-- https://en.wikipedia.org/wiki/Krivine_machine
 6
 7data V = Bound Int | Free String
 8  deriving (Show, Eq)
 9
10data Term = Appl Term Term | Var V | Abst Term
11  deriving (Show)
12
13newtype Closure = Closure (Term, [(V, Closure)])
14  deriving (Show)
15
16data State = State Term [Closure] [(V, Closure)]
17  deriving (Show)
18
19
20step :: State -> State
21step (State (Abst m) (c:s) e) = State m s ((Bound 0, c):e)
22step (State (Appl m n) s e) = State m (Closure (n,e):s) e
23step (State (Var x) s e) =
24  case lookup x e of
25    Just (Closure (m, e')) ->
26      State m s e'
27    Nothing -> error "variable is not found"
28step _ = error "bad state"
29
30eval :: State -> State
31eval s@(State (Abst _) [] _) = s
32eval s = let s' = step s in eval s'
33
34-- (\ 0 0) (\ 0)
35t1 :: Term
36t1 = Appl (Abst (Appl (Var $ Bound 0) (Var $ Bound 0))) (Abst (Var $ Bound 0))
37
38ex1 :: State
39ex1 =
40  let initState = State t1 [] []
41  in eval initState
42
43--((λ 0) (λ 0)) (λ 0)
44t2 :: Term
45t2 = Appl (Appl (Abst $ Var $ Bound 0) (Abst $ Var $ Bound 0)) (Abst $ Var $ Bound 0)
46
47ex2 :: State
48ex2 =
49  eval $ State t2 [] []