Machine semantics for Contract PCF

cpcf-machine.rkt

#lang typed/racket
;; Machine semantics for Contract PCF

;; SYNTAX
;; ======
;;
;; E = (vbl X)
;;   | (app E E)
;;   | (if E E E)
;;   | (lam X E)
;;   | (num N)
;;   | (mon C E L L L)
;;   | (prim O)
;;   | (bool B)
;;
;; C = (pred E)
;;   | (~> C C)
;;
;; X = Symbol
;; L = Symbol

;; SEMANTICS
;; =========
;;
;; V = N | O | B
;;   | (clo E R)
;;   | (arr D D V)
;; 
;; O = '+ | '-
;;   | (plus N) 
;;   | (minus N)
;;
;; D = (--> D D)
;;   | (flat V L L)

;; Ans = (ret V Σ)
;;     | (blame L L)

;; Dns = (dret D Σ)
;;     | (blame L L)

(define-type C (U pred ~>))
(define-type D (U flat -->))
(define-type E (U app lam vbl num mon prim bool ife))
(define-type R (Listof (Pair X A)))
(define-type Σ (Listof (Pair A V)))
(define-type V (U N B O clo arr prim))
(define-type N Integer)
(define-type O (U '+ '- plus minus
                  'even? 'odd?))
(define-type A Symbol) ;; Addresses
(define-type X Symbol) ;; Variables
(define-type L Symbol) ;; Labels
(define-type B Boolean)
(define-type Ans (U ret blame))
(define-type Dns (U dret blame))

(struct: app   ([e0 : E]  [e1 : E])         #:transparent)
(struct: lam   ([x  : X]  [e  : E])         #:transparent)
(struct: vbl   ([x  : X])                   #:transparent)
(struct: num   ([n  : N])                   #:transparent)
(struct: mon   ([c  : C]  
                [e  : E] 
                [p  : L]
                [n  : L]
                [s  : L])                   #:transparent)
(struct: prim  ([o  : O])                   #:transparent)
(struct: ~>    ([c1 : C] [c2 : C])          #:transparent)
(struct: pred  ([e  : E])                   #:transparent)
(struct: bool  ([b  : B])                   #:transparent)
(struct: ife   ([e0 : E] [e1 : E] [e2 : E]) #:transparent)

(struct: -->   ([d1 : D] [d2 : D])          #:transparent)
(struct: flat  ([v  : V] [p  : L] [s : L])  #:transparent)

(struct: blame ([l1 : L] [l2 : L])          #:transparent)
(struct: clo   ([e  : E] [ρ  : R])          #:transparent)
(struct: ret   ([v  : V] [σ  : Σ])          #:transparent)
(struct: dret  ([d  : D] [σ  : Σ])          #:transparent)
(struct: arr   ([d0 : D] [d1 : D] [v : V])  #:transparent)
(struct: plus  ([n  : N])                   #:transparent)
(struct: minus ([n  : N])                   #:transparent)

(define-type J (U D1 D2 D3))
(struct: D1 ([v : V] [κ : K]))
(struct: D2 ([c : C] [ρ : R] [n : L] [p : L] [s : L] [κ : J]))
(struct: D3 ([d : D] [κ : J]))

(define-type K (U C0 C1 C2 C3 C4 C5 C6 C7 C8))
(struct: C0 ())
(struct: C1 ([e  : E] [ρ  : R] [κ : K]))
(struct: C2 ([v  : V] [κ  : K]))
(struct: C3 ([e1 : E] [e2 : E] [ρ : R] [κ : K]))
(struct: C4 ([c  : C] [ρ  : R] [p : L] [n : L] [s : L] [κ : K]))
(struct: C5 ([v  : V] [p  : L] [s : L] [κ : K]))
(struct: C6 ([p  : L] [s  : L] [κ : J]))
(struct: C7 ([v  : V] [d  : D] [κ : K]))
(struct: C8 ([d  : D] [κ  : K]))

(: parse (Any -> E))
(define (parse sexp)
  (match sexp    
    ['+ (prim '+)]
    ['- (prim '-)]
    ['even? (prim 'even?)]
    ['odd? (prim 'odd?)]
    [(? symbol? x) (vbl x)]
    [(? exact-integer? n) (num n)]
    [(? boolean? b) (bool b)]
    [(list 'if e1 e2 e3)
     (ife (parse e1)
          (parse e2)
          (parse e3))]
    [(list '=> c e)
     (define l (gensym))
     (define pos (symbol+ '+: l))
     (define neg (symbol+ '-: l))
     (mon (parse-con c) (parse e) pos neg pos)]
    [(list 'λ (list (? symbol? x)) e)
     (lam x (parse e))]
    [(list e1 e2)
     (app (parse e1) (parse e2))]
    [_ (error "Unkown sexp")]))

(: parse-con (Any -> C))
(define (parse-con sexp)
  (match sexp
    [(list '-> c1 c2)
     (~> (parse-con c1) (parse-con c2))]
    [e (pred (parse e))]))

(: ev/k (E R Σ K -> Ans))
(define (ev/k e ρ σ κ)
  (match e
    [(lam x e) (kvapply κ (ret (clo (lam x e) ρ) σ))]
    [(vbl x)   (kvapply κ (ret (lookup σ ρ x) σ))]
    [(num n)   (kvapply κ (ret n σ))]
    [(prim o)  (kvapply κ (ret o σ))]
    [(bool b)  (kvapply κ (ret b σ))]
    [(app e0 e1)
     (ev/k e0 ρ σ (C1 e1 ρ κ))]  
    [(ife e0 e1 e2)
     (ev/k e0 ρ σ (C3 e1 e2 ρ κ))]
    [(mon c e p n s)
     (ev/k e ρ σ (C4 c ρ p n s κ))]))

(: monitor/k (D V Σ K -> Ans))
(define (monitor/k d v σ κ)
  (match d
    [(--> d1 d2)
     (kvapply κ (ret (arr d1 d2 v) σ))]
    [(flat f p s)
     (apply/k f v σ (C5 v p s κ))]))

(: cv/k (C R Σ L L L J -> Ans))
(define (cv/k c ρ σ p n s κ)
  (match c
    [(~> c1 c2)
     (cv/k c1 ρ σ p n s (D2 c2 ρ n p s κ))]
    [(pred e)
     (ev/k e ρ σ (C6 p s κ))]))

(: apply/k (V V Σ K -> Ans))
(define (apply/k f v σ κ)
  (match f
    [(arr d1 d2 f)
     (monitor/k d1 v σ (C7 f d2 κ))]
    ['+
     (match v
       [(? number? n) (kvapply κ (ret (plus n) σ))])]
    ['-
     (match v
       [(? number? n) (kvapply κ (ret (minus n) σ))])]
    [(plus n)
     (match v
       [(? number? m)
        (kvapply κ (ret (+ m n) σ))])]
    [(minus n)
     (match v
       [(? number? m)
        (kvapply κ (ret (- m n) σ))])]
    ['even?
     (match v
       [(? number? n)
        (kvapply κ (ret (even? n) σ))])]
    ['odd?
     (match v
       [(? number? n)
        (kvapply κ (ret (odd? n) σ))])]
    [(clo (lam x e) ρ)
     (define a (alloc))
     (ev/k e 
           (extend-env ρ x a)
           (extend-sto σ a v)
           κ)]))

(: kvapply (K Ans -> Ans))
(define (kvapply κ a)
  (match κ
    [(C0) a]
    [(C1 e1 ρ κ)
     (match a
       [(? blame? b) (kvapply κ b)]
       [(ret v1 σ1) 
        (ev/k e1 ρ σ1 (C2 v1 κ))])]
    [(C2 v1 κ)
     (match a
       [(? blame? b) (kvapply κ b)]
       [(ret v2 σ2)
        (apply/k v1 v2 σ2 κ)])]
    [(C3 e1 e2 ρ κ)
     (match a
       [(? blame? b) (kvapply κ b)]
       [(ret #f σ1)  
        (ev/k e2 ρ σ1 κ)]
       [(ret v σ1)
        (ev/k e1 ρ σ1 κ)])]
    [(C4 c ρ p n s κ)
     (match a
       [(ret v1 σ)
        (cv/k c ρ σ p n s (D1 v1 κ))])]
    [(C5 v p s κ)
     (match a
       [(? blame? b) (kvapply κ b)]
       [(ret #t σ)   (kvapply κ (ret v σ))]
       [(ret #f σ)   (kvapply κ (blame p s))])]
    [(C6 p s κ)
     (match a
       [(? blame? b) (kdapply κ b)]
       [(ret v σ) 
        (kdapply κ (dret (flat v p s) σ))])]
    [(C7 f d2 κ)
     (match a
       [(? blame? b) (kvapply κ b)]
       [(ret v1 σ1)
        (apply/k f v1 σ1 (C8 d2 κ))])]
    [(C8 d2 κ)
     (match a
       [(ret v2 σ2)
        (monitor/k d2 v2 σ2 κ)])]))

(: kdapply (J Dns -> Ans))
(define (kdapply j a)
  (match j 
    [(D1 v1 κ)
     (match a
       [(dret d σ) 
        (monitor/k d v1 σ κ)])]
    [(D2 c2 ρ n p s κ)
     (match a
       [(dret d1 σ1)
        (cv/k c2 ρ σ1 n p s (D3 d1 κ))])]
    [(D3 d1 κ)
     (match a
       [(dret d2 σ2)
        (kdapply κ (dret (--> d1 d2) σ2))])]))

(: lookup (Σ R X -> V))
(define (lookup σ ρ x)
  (define xa ((inst assoc X A) x ρ))
  (if xa
      (let ()
        (define av ((inst assoc A V) (cdr xa) σ))
        (if av 
            (cdr av)
            (error "Unbound address")))
      (error "Unbound variable")))

(: extend-env (R X A -> R))
(define (extend-env ρ x a)
  ((inst cons (Pair X A) R) 
   ((inst cons X A) x a) ρ))

(: extend-sto (Σ A V -> Σ))
(define (extend-sto σ a v)
  ((inst cons (Pair A V) Σ) 
   ((inst cons A V) a v) σ))
  

(define (alloc) (gensym))

(: symbol+ (Symbol Symbol -> Symbol))
(define (symbol+ s1 s2) 
  (string->symbol (string-append (symbol->string s1)
                                 (symbol->string s2))))

(: run (Any -> Ans))
(define (run sexp)
  (ev/k (parse sexp) empty empty (C0)))


(run '5)
(run '+)
(run '(λ (x) 4))
(run '((λ (x) 4) 5))
(run '((λ (x) x) 5))
(run '(if 0 1 2))
(run '(if #f 1 2))
(run '(+ 5))
(run '((+ 5) 6))
(run '((- 5) 6))
(run '(even? 5))
(run '(odd? 5))
(run '(=> odd? 5))
(run '(=> even? 5))
(run '(=> (-> even? even?) (λ (x) x)))
(run '(=> (λ (_) #t) 7))
(run '(=> (-> (λ (_) #t) (λ (_) #t)) (λ (x) x)))
(run '((=> (-> (λ (y) #t) (λ (z) #t)) (λ (x) x)) 6))
(run '((=> (-> (λ (y) #f) (λ (z) #t)) (λ (x) x)) 6))
(run '((=> (-> (λ (y) #t) (λ (z) #f)) (λ (x) x)) 6))