diff options
| -rw-r--r-- | lib.rkt | 24 | ||||
| -rw-r--r-- | stlc-pred.rkt | 28 |
2 files changed, 23 insertions, 29 deletions
@@ -65,6 +65,28 @@ [(hash-table (k1 v1) (k2 v2) (k3 v3)) (format "{~a: ~a; ~a: ~a; ~a: ~a}" (fmt k1) (fmt v1) (fmt k2) (fmt v2) (fmt k3) (fmt v3))] [expr (format "~a" expr)])) +;; transforms higher-level constructs into the core calculus +(define (desugar expr) + (match expr + ['⟨⟩ 'sole] + [`(ref ,e) (desugar `(new ,e))] + [`(deref ,e) (desugar `(! ,e))] + [`(set ,e1 ,e2 ,in) + (desugar `(let _ (set ,e1 ,e2) ,in))] + + [`(let ,x (: (→ ,k ,a ,b)) (λ ,x ,e) ,in) + (desugar `((λ ,x (: (→ ,k ,a ,b)) ,in) (λ ,x (: ,a) ,e)))] + [`(let ,x (: (→ ,a ,b)) (λ ,x ,e) ,in) + (desugar `((λ ,x (: (→ ,a ,b)) ,in) (λ ,x (: ,a) ,e)))] + [`(let ,x (: ,t) ,e ,in) + (desugar `((λ ,x (: ,t) ,in) ,e))] + [`(let ,x (: ,t) ,e) + (desugar `(let ,x (: ,t) ,e 'sole))] + + [`(λ ,x (: ,t) ,e) `(λ ,x (: ,t) ,(desugar e))] + [`(,e1 ,e2 ,e3) `(,(desugar e1) ,(desugar e2) ,(desugar e3))] + [`(,e1 ,e2) `(,(desugar e1) ,(desugar e2))] + [e e])) -(provide dbg err note print todo strip fmt) +(provide dbg err note print todo strip fmt desugar) ; todo: how to provide everything?? diff --git a/stlc-pred.rkt b/stlc-pred.rkt index a8ab219..eac2d00 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -38,34 +38,6 @@ [expr (err (format "interpreting an unknown expression ~a" expr))])) -;; transforms higher-level constructs into the core calculus -(define (desugar expr) - (match expr - ['sole '⟨⟩] - [`(ref ,expr) (desugar `(new ,expr))] - [`(deref ,expr) (desugar `(! ,expr))] - [`(set ,id ,expr ,body) - (desugar `(let _ (set ,id ,expr) ,body))] - - [`(let ,id (: (→ ,k ,a ,b)) (λ ,x ,e) ,body) - (desugar `((λ ,id (: (→ ,k ,a ,b)) ,body) (λ ,x (: ,a) ,e)))] - [`(let ,id (: (→ ,a ,b)) ,expr ,body) - (err "you forgot to add a level annotation dummy")] - [`(let ,id (: ,type) ,e ,body) - (desugar `((λ ,id (: ,type) ,body) ,e))] - [`(let ,id (: ,type) ,expr) - (desugar `(let ,id (: ,type) ,expr '⟨⟩))] - - [`(new ,expr) `(new ,(desugar expr))] - [`(! ,expr) `(! ,(desugar expr))] - [`(set ,id ,expr) `(set ,(desugar id) ,(desugar expr))] - [`(λ ,id (: ,type) ,expr) `(λ ,id (: ,type) ,(desugar expr))] - [`(,body ,arg) `(,(desugar body) ,(desugar arg))] - [id #:when (number? id) id] - [id #:when (symbol? id) id] - - [expr (err (format "desugaring unknown expression ~a" expr))])) - ;; (check Expr Type Table[Sym, Type]): Bool (define (check expr with [Γ #hash()]) (check- (desugar expr) with Γ)) |