From 356833e01ea8c211873262c73f2aabd64bfd5791 Mon Sep 17 00:00:00 2001
From: JJ
Date: Fri, 7 Jun 2024 18:40:55 -0700
Subject: lib: provide desugaring function

---
 lib.rkt       | 24 +++++++++++++++++++++++-
 stlc-pred.rkt | 28 ----------------------------
 2 files changed, 23 insertions(+), 29 deletions(-)

diff --git a/lib.rkt b/lib.rkt
index c0e1e3e..6fc3204 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -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 Γ))
-- 
cgit v1.2.3-70-g09d2