dvanhorn

#lang racket

;; Mogensen-Scott encoding
(define-syntax encode
  (syntax-rules (λ)
    [(encode (λ (x) e))
     (λ (VAR) (λ (APP) (λ (LAM) (LAM (λ (x) (encode e))))))]
    [(encode (e0 e1))
     (λ (VAR) (λ (APP) (λ (LAM) ((APP (encode e0)) (encode e1)))))]
    [(encode x) 

dvanhorn

#lang typed/racket
(define-type Term (U VAR LAM APP))
(struct: VAR ([x : String]) #:transparent)
(struct: LAM ([x : String] [m0 : Term]) #:transparent)
(struct: APP ([m1 : Term] [m2 : Term]) #:transparent)

(define-type Sem (U TM FUN))
(struct: TM ([l : (Integer -> Term)]))
(struct: FUN ([f : ((-> Sem) -> Sem)]))

dvanhorn

#lang typed/racket
(define-type Term (U VAR LAM APP))
(struct: VAR ([x : String]) #:transparent)
(struct: LAM ([x : String] [m0 : Term]) #:transparent)
(struct: APP ([m1 : Term] [m2 : Term]) #:transparent)

(define-type Sem (U Ind Fun))

(define-type Env (U R1 R2))
(struct: R1 ())

dvanhorn

diff popl12-reviews.txt popl12-reviews-final.txt 
333c333
<                  Updated Tuesday 6 Sep 2011 6:28:00pm EDT
---
>                  Updated Monday 19 Sep 2011 1:03:02pm EDT
339c339
<                       Overall merit: 4. Accept
---
>                       Overall merit: 3. Weak accept
525d524

dvanhorn

#lang racket
(require redex/reduction-semantics)

(define-language pre-C
  (CON X
       nat?
       (or/c CON CON)
       (rec/c X CON)
       (cons/c CON CON)
       (CON -> CON))

dvanhorn

#lang racket
(require redex/reduction-semantics)

(define-language C
  (CON X
       nat?
       (or/c CON CON)
       (rec/c X CON)
       (cons/c CON CON)
       (CON -> CON))

dvanhorn

doom:shan dvanhorn$ java Eval
Exception in thread "main" java.lang.StackOverflowError
	at Evaluate.visit(Eval.java:142)
	at Evaluate.visit(Eval.java:119)
	at App.accept(Eval.java:56)
	at Evaluate.visit(Eval.java:142)
	at Evaluate.visit(Eval.java:119)
	at App.accept(Eval.java:56)
	at Evaluate$1.apply(Eval.java:136)
	at Evaluate.visit(Eval.java:142)

dvanhorn

// Compositional evaluator as visitor

import java.math.BigInteger;

// Syntax

interface Exp {
    <X> X accept(Visitor<X> v);
}

dvanhorn

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

;; SYNTAX
;; ======
;;
;; E = (vbl X)
;;   | (app E E)
;;   | (if E E E)
;;   | (lam X E)

dvanhorn

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

;; SYNTAX
;; ======
;;
;; E = (vbl X)
;;   | (app E E)
;;   | (if E E E)
;;   | (lam X E)