program-analysis-examples/cesk.rkt at master · kmicinski/program-analysis-examples · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
;; CESK interpreter for the direct-style lambda calculus
#lang racket

(define lit? number?)

(define (expr? e)
  (match e
    [`(,(? expr? e0) ,(? expr? e1)) #t]
    [(? symbol? x) #t]
    [(? lit? l) #t]
    [`(lambda (,x) ,(? expr? e-body)) #t]
    [else #f]))

(define (addr? x) (or (number? x) (equal? x '•)))

(define (env? ρ)
  (and (andmap symbol? (hash-keys ρ))
       (andmap addr? (hash-values ρ))))

(define (clo? clo)
  (match clo
    [`(clo (lambda (,x) ,e) ,(? env? ρ)) #t]
    [else #f]))

(define (continuation? k)
  (match k
    [`halt #t]
    [`(ar ,(? expr? e) ,(? env? ρ) ,(? addr? k)) #t]
    [`(fn ,(? clo? clo) ,(? addr? k)) #t]
    [else #f]))

(define (store? σ)
  (and (andmap addr? (hash-keys σ))
       (andmap (lambda (x) (or (continuation? x) (clo? x))) (hash-values σ))))

(define (state? ς)
  (match ς
    [`(,(? expr? c) ,(? env? ρ) ,(? store? σ) ,(? addr? α)) #t]
    [else #f]))

(define (inj e)
  `(,e ,(hash) ,(hash '• 'halt) •))


(define num-allocs 0)
(define (alloc σ)
  (set! num-allocs (add1 num-allocs))
  num-allocs)

(define (aexpr? ae)
  (match ae
    [`(lambda (,x) ,(? expr? e)) #t]
    [(? symbol? x) #t]
    [else #f]))

(define (aeval ae ρ σ)
  (match ae
    [(? symbol? x) (hash-ref σ (hash-ref ρ x))]
    [`(lambda (,x) ,e) `(clo ,ae ,ρ)]))

(define (step ς)
  (match ς
    [`((,e₀ ,e₁) ,ρ ,σ ,kα)
     (let* ([kα₁ (alloc σ)]
            [σ₁ (hash-set σ kα₁ `(ar ,e₁ ,ρ ,kα))])
       `(,e₀ ,ρ ,σ₁ ,kα₁))]
    [`(,(? aexpr? ae) ,ρ ,σ ,kα)
     (match (hash-ref σ kα)
       [`(ar ,e ,ρ₁ ,kα₁)
        (let* ([kα₂ (alloc σ)]
               [σ₁ (hash-set σ kα₂ `(fn ,(aeval ae ρ σ) ,kα₁))])
          `(,e ,ρ₁ ,σ₁ ,kα₂))]
       [`(fn (clo (lambda (,x) ,e) ,ρ₁) ,kα)
        (let* ([α (alloc σ)]
               [σ₁ (hash-set σ α (aeval ae ρ σ))]
               [ρ₂ (hash-set ρ₁ x α)])
          `(,e ,ρ₂ ,σ₁ ,kα))])]))

(define (halting ς)
  (match ς
    [`(,(? aexpr? ae) ,ρ ,σ ,kα)
     (equal? (hash-ref σ kα) 'halt)]
    [else #f]))

(define (step-n e n)
  (define (iter n ς)
    (if (or (halting ς) (= n 0))
        (begin
           (pretty-print ς)
           (displayln "Done!"))
        (begin
          (pretty-print ς)
          (display "→")
          (iter (sub1 n) (step ς)))))
  (iter n (inj e)))

(define (repl)
  (display "> ")
  (let ([e (read)])
    ;; Evaluate...
    (step-n e 100)
    (repl)))

(repl)