repos / machines.hs.git

commit

2b5df21

parent

2b5df21

author

Evgenii Akentev

date

2024-09-04 16:22:00 +0400 +04

Add Krivine, CEK & stubs

 1@@ -0,0 +1,23 @@
 2+dist
 3+dist-*
 4+cabal-dev
 5+*.o
 6+*.hi
 7+*.hie
 8+*.chi
 9+*.chs.h
10+*.dyn_o
11+*.dyn_hi
12+.hpc
13+.hsenv
14+.cabal-sandbox/
15+cabal.sandbox.config
16+*.prof
17+*.aux
18+*.hp
19+*.eventlog
20+.stack-work/
21+cabal.project.local
22+cabal.project.local~
23+.HTF/
24+.ghc.environment.*

 1@@ -0,0 +1,20 @@
 2+Copyright (c) 2024 Evgenii Akentev
 3+
 4+Permission is hereby granted, free of charge, to any person obtaining
 5+a copy of this software and associated documentation files (the
 6+"Software"), to deal in the Software without restriction, including
 7+without limitation the rights to use, copy, modify, merge, publish,
 8+distribute, sublicense, and/or sell copies of the Software, and to
 9+permit persons to whom the Software is furnished to do so, subject to
10+the following conditions:
11+
12+The above copyright notice and this permission notice shall be included
13+in all copies or substantial portions of the Software.
14+
15+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
16+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
17+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
18+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
19+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
20+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
21+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

 1@@ -0,0 +1,18 @@
 2+cabal-version:      3.0
 3+name:               machines
 4+version:            0.1.0.0
 5+license:            MIT
 6+license-file:       LICENSE
 7+author:             Evgenii Akentev
 8+maintainer:         hi@ak3n.com
 9+build-type:         Simple
10+
11+common warnings
12+    ghc-options: -Wall
13+
14+library
15+    import:           warnings
16+    exposed-modules:  Krivine, CEK
17+    build-depends:    base ^>=4.18.2.1
18+    hs-source-dirs:   src
19+    default-language: Haskell2010

 1@@ -0,0 +1,55 @@
 2+module CEK where
 3+
 4+-- https://en.wikipedia.org/wiki/CEK_Machine
 5+-- https://legacy.cs.indiana.edu/ftp/techreports/TR202.pdf
 6+
 7+-- i'm fine with the defunctionalized version
 8+
 9+data V = Bound Int
10+  deriving (Show, Eq)
11+
12+data Term = Appl Term Term | Var V | Abst Term
13+  deriving (Show)
14+
15+data Val = Closure Term [Val]
16+  deriving (Show)
17+
18+data Cont
19+  = C2 Term [Val] Cont
20+  | C1 Val Cont
21+  | C0
22+
23+continue :: Cont -> Val -> Val 
24+continue c v = case (c, v) of
25+  (C2 t1 e k, v0) -> eval t1 e (C1 v0 k)
26+  (C1 v0 k, v1) -> apply v0 v1 k
27+  (C0, v') -> v'
28+
29+apply :: Val -> Val -> Cont -> Val
30+apply v0 v1 k =
31+  let (Closure t e) = v0
32+  in eval t (v1 : e) k
33+
34+eval :: Term -> [Val] -> Cont -> Val
35+eval t e k = case t of
36+  Var (Bound n) -> continue k (e!!n)
37+  Abst t' -> continue k (Closure t' e)
38+  Appl t0 t1 -> eval t0 e (C2 t1 e k)
39+
40+run :: Term -> Val
41+run t = eval t [] C0
42+
43+
44+-- (\ 0 0) (\ 0)
45+t1 :: Term
46+t1 = Appl (Abst (Appl (Var $ Bound 0) (Var $ Bound 0))) (Abst (Var $ Bound 0))
47+
48+ex1 :: Val
49+ex1 = run t1
50+
51+--((λ 0) (λ 0)) (λ 0)
52+t2 :: Term
53+t2 = Appl (Appl (Abst $ Var $ Bound 0) (Abst $ Var $ Bound 0)) (Abst $ Var $ Bound 0)
54+
55+ex2 :: Val
56+ex2 = run t2

1@@ -0,0 +1,5 @@
2+module CESK where
3+
4+-- https://cstheory.stackexchange.com/a/41257
5+
6+-- TODO: implement

1@@ -0,0 +1,3 @@
2+module CK where
3+
4+-- TODO: implement

1@@ -0,0 +1,3 @@
2+module CS where
3+
4+-- TODO: implement

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

 1@@ -0,0 +1,21 @@
 2+module SECD where
 3+
 4+-- https://en.wikipedia.org/wiki/SECD_machine
 5+
 6+data Inst
 7+  = Nil
 8+  | Ldc
 9+  | Ld
10+  | Sel
11+  | Join
12+  | Ldf
13+  | Ap
14+  | Ret
15+  | Dum
16+  | Rap
17+
18+data State = State
19+  -- Control
20+  -- Environment
21+  -- Stack
22+  -- Dump