(module core-language mzscheme
(require (planet "reduction-semantics.ss" ("robby" "redex.plt" 3 9))
(planet "subst.ss" ("robby" "redex.plt" 3 9))
(lib "match.ss"))
(define (operator? x)
(and (memq x '(+ - =)) #t))
(define (ground-type? t)
(and (symbol? t)
(not (eq? t 'dynamic))))
(define (function-type? t)
(match t
[`(,_ -> ,_) #t]
[_ #f]))
(define (function-type-domain t)
(match t
[`(,dom -> ,_) dom]))
(define (function-type-range t)
(match t
[`(,_ -> ,rng) rng]))
(define (binding? x)
(match x
[`(,_ : ,_ = ,_) #t]
[`(,_ = ,_) #t]
[_ #f]))
(define (binding-variable x)
(match x
[`(,var : ,_ = ,_) var]
[`(,var = ,_) var]))
(define (binding-type x)
(match x
[`(,_ : ,t = ,_) t]
[`(,_ = ,_) 'dynamic]))
(define (binding-init x)
(match x
[`(,_ : ,_ = ,init) init]
[`(,_ = ,init) init]))
(define (occurs-free? x e)
(match e
[(? symbol?) (eq? x e)]
[(? number?) #f]
[(? boolean?) #f]
[`(lambda (,y : ,t) ,b)
(and (not (eq? x y))
(occurs-free? x b))]
[`(let (,y : ,t = ,e1) ,e2)
(or (occurs-free? x e1)
(and (not (eq? x y))
(occurs-free? x e2)))]
[`(letrec ([,ys : ,ts = ,vs] ...) ,b)
(and (not (memq x ys))
(ormap (lambda (e)
(occurs-free? x e))
(cons b vs)))]
[`(,(and op (? operator?)) ,e1 ,e2)
(or (occurs-free? x e1)
(occurs-free? x e2))]
[`(if ,e1 ,e2 ,e3)
(or (occurs-free? x e1)
(occurs-free? x e2)
(occurs-free? x e3))]
[`(cast ,_ ,e)
(occurs-free? x e)]
[`(,e1 ,e2)
(or (occurs-free? x e1)
(occurs-free? x e2))]))
(define (live-letrec? x)
(match x
[`(letrec ([,xs : ,_ = ,_] ...) ,body)
(ormap (lambda (x)
(occurs-free? x body))
xs)]))
(define core-language
(language [x (variable-except lambda + - = if error cast int bool dynamic -> : let succ fail function ∘ ! ? <=)]
[e (e e)
(+ e e)
(- e e)
(= e e)
(if e e e)
(let (x : t = e) e)
(letrec ([x : t = v] ...) e)
x
s]
[F (v hole)
((hole #f) e)
(+ hole e)
(+ v hole)
(- hole e)
(- v hole)
(= hole e)
(= v hole)
(if hole e e)
(let (x : t = hole) e)
(letrec ([x : t = v] ...) hole)]
[C hole (in-hole F E)]
[E C]
[s number
#t #f
(lambda (x : t) e)]
[v s
(side-condition (name form (letrec ([x : t = v] ...) v))
(live-letrec? (term form)))]
[t dynamic
int
bool
(t -> t)]
))
(define language/st
(extend-language core-language
[e .... (cast t e)]
[C .... (cast t E)] [v .... (cast dynamic s)]))
(define language/htf
(extend-language core-language
[D int
bool
function]
[c succ
fail
(! D)
(? D)
(function c c)
(∘ c c)]
[e .... (cast (t <= c) e)]
[E .... (cast (t <= c) C)]
[v .... (side-condition (cast (t <= c_0) s) (not (test-match language/htf succ (term c_0))))]))
(define (substitute* vars vals expr)
(cond
[(and (null? vars) (null? vals))
expr]
[(or (null? vars) (null? vals))
(error 'eval "formal and actual parameter lists of different length: " vars vals)]
[else
(substitute* (cdr vars) (cdr vals) (substitute (car vars) (car vals) expr))]))
(define substitute
(plt-subst
[(? symbol?) (variable)]
[(? number?) (constant)]
[(? boolean?) (constant)]
[`(lambda (,x : ,t) ,b)
(all-vars (list x))
(build (lambda (vars body) `(lambda (,(car vars) : ,t) ,body)))
(subterm (list x) b)]
[`(let (,x : ,t = ,e1) ,e2)
(all-vars (list x))
(build (lambda (vars binding body) `(let (,(car vars) : ,t = ,binding) ,body)))
(subterm '() e1)
(subterm (list x) e2)]
[`(letrec ([,xs : ,ts = ,vs] ...) ,b)
(all-vars xs)
(build (lambda (vars vs body)
`(letrec ,(map (lambda (x t v)
`[,x : ,t = ,v])
vars ts vs)
,body)))
(subterm xs vs)
(subterm xs b)]
[`(,(and op (? operator?)) ,e1 ,e2)
(all-vars '())
(build (lambda (vars e1 e2) `(,op ,e1 ,e2)))
(subterm '() e1)
(subterm '() e2)]
[`(if ,e1 ,e2 ,e3)
(all-vars '())
(build (lambda (vars e1 e2 e3) `(if ,e1 ,e2 ,e3)))
(subterm '() e1)
(subterm '() e2)
(subterm '() e3)]
[`(cast ,x ,e)
(all-vars '())
(build (lambda (vars e) `(cast ,x ,e)))
(subterm '() e)]
[`(,f ,x)
(all-vars '())
(build (lambda (vars f x) `(,f ,x)))
(subterm '() f)
(subterm '() x)]
))
(define (core-reductions lang)
(define-metafunction lookup-letrec
lang
[((in-hole E_0 (letrec ([x_0 : t_0 = v_0] ... [x_1 : t_1 = v_1] [x_2 : t_2 = v_2] ...) hole)) x_1)
v_1]
[((in-hole E_0 F_0) x_0)
(lookup-letrec (E_0 x_0))]
[((in-hole E_0 (cast any hole)) x_0)
(lookup-letrec (E_0 x_0))]
[((hole #f) x_0)
"error: free variable"])
(reduction-relation lang
[==> ((lambda (x_0 : t_0) e_0) v_0)
,(substitute (term x_0)
(term v_0)
(term e_0))
"βv"]
[==> (let (variable_x : t_xt = v_binding) e_body)
,(substitute (term variable_x)
(term v_binding)
(term e_body))
"ELet"]
[--> (in-hole E_0 variable_x)
(in-hole E_0 (lookup-letrec (E_0 variable_x)))
"ERec"]
[==> (+ number_m number_n)
,(+ (term number_m) (term number_n))
"EAdd"]
[==> (- number_m number_n)
,(- (term number_m) (term number_n))
"ESub"]
[==> (= number_m number_n)
,(= (term number_m) (term number_n))
"EEq"]
[==> (if #t e_consequent e_alternate)
e_consequent
"EIfT"]
[==> (if #f e_consequent e_alternate)
e_alternate
"EIfF"]
[==> (letrec ([variable_xs : t_ts = v_bindings] ...) v_result)
v_result
"EGC"]
where
[(==> a b) (--> (in-hole E_1 a) (in-hole E_1 b))]))
(provide (all-defined)))