diff --git a/code/elim-complex-values.rkt b/code/elim-complex-values.rkt new file mode 100644 index 0000000000000000000000000000000000000000..0b57b2ac66231654499311a17722e3d10bbe3d55 --- /dev/null +++ b/code/elim-complex-values.rkt @@ -0,0 +1,70 @@ +#lang racket + +(require racket/control) + +;; Eliminating complex values using delimited control +(define (celim-val v) + (match v + [(? symbol? x) x] + [(list 'cons car cdr) (list 'cons (celim-val car) (celim-val cdr))] + [(list 'split discrim (list 'cons x1 x2) kv) + (control k + (list 'split (celim-val discrim) + (list 'cons x1 x2) + (% (k (celim-val kv)))))] + [(list 'nil) (list 'nil)] + [(list 'split discrim (list 'nil) kv) + (control k + (list 'split (celim-val discrim) + (list 'nil) + (% (k (celim-val kv)))))] + [(list (? injection? in) v) (list in (celim-val v))] + [`(case ,discrim + [(inl ,xl) ,kvl] + [(inr ,xr) ,kvr]) + (control k + `(case ,(celim-val discrim) + [(inl ,xl) ,(% (k (celim-val kvl)))] + [(inr ,xr) ,(% (k (celim-val kvr)))]))] + [`(case ,discrim) (control k `(case ,(celim-val discrim)))] + [(list 'thunk t) (list 'thunk (celim-term))] + [(list 'let (? symbol? x) v1 v2) + (control k + (list 'let + x + (list 'ret (celim-val v1)) + (% (k (celim-val v2)))))])) + +(define (celim-term t) + (match t + [(list 'ret v) + (list 'ret (celim-val v))] + [(list 'let x t1 t2) + (list 'let + x + (celim-term t1) + (% (celim-term t2)))] + [(list 'split discrim (list 'cons x1 x2) kt) + (list 'split (celim-val discrim) + (list 'cons x1 x2) + (% (celim-term kt)))] + [(list 'split discrim (list 'nil) kt) + (list 'split (celim-val discrim) + (list 'nil) + (% (celim-term kt)))] + [`(case ,discrim + [(inl ,xl) ,ktl] + [(inr ,xr) ,ktr]) + `(case ,(celim-val discrim) + [(inl ,xl) ,(% (celim-term ktl))] + [(inr ,xr) ,(% (celim-term ktr))])] + [`(case ,discrim) `(case ,(celim-val discrim))] + [`(force ,v) `(force ,(celim-val v))] + [`(λ ,x ,t) `(λ ,x ,(% (celim-term t)))] + [`(app ,t ,v) `(app ,(celim-term t) ,(celim-val v))] + [`(copat [fst ,t1] [snd ,t2]) `(copat [fst ,(celim-term t1)] [snd ,(celim-term t2)])] + [(list (? projection? p) t) (list p (celim-term t))] + [`(copat) `(copat)])) + +(define (injection? x) (or (symbol=? x 'inl) (symbol=? x 'inr))) +(define (projection? x) (or (symbol=? x 'fst) (symbol=? x 'snd))) \ No newline at end of file