Skip to content

Instantly share code, notes, and snippets.

@dvanhorn

dvanhorn/cpcf-den.rkt

Created July 3, 2012 18:32
Show Gist options
  • Save dvanhorn/3041667 to your computer and use it in GitHub Desktop.
Save dvanhorn/3041667 to your computer and use it in GitHub Desktop.
Download ZIP
Denotational semantics for Contract PCF
Raw
cpcf-den.rkt
#lang typed/racket
;; Denotational 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)
(: 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 (E R Σ -> Ans))
(define (ev e ρ σ)
(match e
[(lam x e) (ret (clo (lam x e) ρ) σ)]
[(vbl x) (ret (lookup σ ρ x) σ)]
[(num n) (ret n σ)]
[(prim o) (ret o σ)]
[(bool b) (ret b σ)]
[(app e0 e1)
(match (ev e0 ρ σ)
[(? blame? b) b]
[(ret v1 σ1)
(match (ev e1 ρ σ1)
[(? blame? b) b]
[(ret v2 σ2)
(apply v1 v2 σ2)])])]
[(ife e0 e1 e2)
(match (ev e0 ρ σ)
[(? blame? b) b]
[(ret #f σ1) (ev e2 ρ σ1)]
[(ret v σ1) (ev e1 ρ σ1)])]
[(mon c e p n s)
(match (ev e ρ σ)
[(ret v1 σ)
(match (cv c ρ σ p n s)
[(dret d σ)
(monitor d v1 σ)])])]))
(: cv (C R Σ L L L -> Dns))
(define (cv c ρ σ p n s)
(match c
[(~> c1 c2)
(match (cv c1 ρ σ p n s)
[(dret d1 σ1)
(match (cv c2 ρ σ1 n p s)
[(dret d2 σ2)
(dret (--> d1 d2) σ2)])])]
[(pred e)
(match (ev e ρ σ)
[(? blame? b) b]
[(ret v σ) (dret (flat v p s) σ)])]))
(: apply (V V Σ -> Ans))
(define (apply f v σ)
(match f
[(arr d1 d2 f)
(match (monitor d1 v σ)
[(? blame? b) b]
[(ret v1 σ1)
(match (apply f v1 σ1)
[(ret v2 σ2)
(monitor d2 v2 σ2)])])]
['+
(match v
[(? number? n) (ret (plus n) σ)])]
['-
(match v
[(? number? n) (ret (minus n) σ)])]
[(plus n)
(match v
[(? number? m)
(ret (+ m n) σ)])]
[(minus n)
(match v
[(? number? m)
(ret (- m n) σ)])]
['even?
(match v
[(? number? n)
(ret (even? n) σ)])]
['odd?
(match v
[(? number? n)
(ret (odd? n) σ)])]
[(clo (lam x e) ρ)
(define a (alloc))
(ev e
(extend-env ρ x a)
(extend-sto σ a v))]))
(: monitor (D V Σ -> Ans))
(define (monitor d v σ)
(match d
[(--> d1 d2)
(ret (arr d1 d2 v) σ)]
[(flat f p s)
(match (apply f v σ)
[(? blame? b) b]
[(ret #t σ) (ret v σ)]
[(ret #f σ) (blame p s)])]))
(: 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 (parse sexp) empty empty))
(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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment