lib: provide fmt and strip functions

4 files changed, 41 insertions, 79 deletions

diff --git a/lib.rkt b/lib.rkt
index 85ea0ce..c0e1e3e 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -19,6 +19,9 @@
       msg)))
 
 (define-syntax-rule (note msg)
+  (eprintf "note: ~a~%" msg))
+
+(define-syntax-rule (print msg)
   (eprintf "~a~%" msg))
 
 (define-syntax (todo stx)
@@ -29,5 +32,39 @@
 ; todo: write a fmt alias to format
 ; todo: write a namer
 
-(provide dbg err note todo)
+;; removes typing annotations
+(define (strip expr)
+  (match expr
+    [`(λ ,id (: ,type) ,body (: ,type)) `(λ ,(strip id) ,(strip body))]
+    [`(λ ,id ,body (: ,type)) `(λ ,(strip id) ,(strip body))]
+    [`(λ ,id (: ,type) ,body) `(λ ,(strip id) ,(strip body))]
+    [`(,a ,b) `(,(strip a) ,(strip b))]
+    [expr expr]))
+
+;;      (fmt Expr) → String
+(define (fmt expr)
+  (match expr
+    ['sole "⟨⟩"]
+    [`(λ ,id ,body) (format "λ~a.[~a]" id (fmt body))]
+    [`((λ ,id ,body) ,arg) (format "~a = ~a; ~a" id (fmt arg) (fmt body))]
+    [`(λ ,id (: ,type) ,body) (format "~a: ~a; ~a" id (fmt type) (fmt body))]
+    [`((λ ,id (: ,type) ,body) ,arg) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt arg) (fmt body))]
+    [`(λ ,id ,body ,env) (format "λ~a.[~a]" id (fmt body))]
+    [`(let ,id ,expr ,body) (format "~a = ~a; ~a" id (fmt expr) (fmt body))]
+    [`(let ,id (: ,type) ,expr ,body) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt expr) (fmt body))]
+    [`(set ,id ,expr ,body) (format "~a := ~a; ~a" id (fmt expr) (fmt body))]
+    [`(→ ,a ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
+    [`(→ ,k ,a ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))]
+    [`(Ref ,a) (format "Ref ~a" (fmt a))]
+    [`(new ,a) (format "new ~a" (fmt a))]
+    [`(! ,a) (format "!~a" (fmt a))]
+    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
+    [(hash-table) "{}"] ; fixme lmao
+    [(hash-table (k v)) (format "{~a: ~a}" (fmt k) (fmt v))]
+    [(hash-table (k1 v1) (k2 v2)) (format "{~a: ~a; ~a: ~a}" (fmt k1) (fmt v1) (fmt k2) (fmt v2))]
+    [(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)]))
+
+
+(provide dbg err note print todo strip fmt)
 ; todo: how to provide everything??
diff --git a/stlc-let.rkt b/stlc-let.rkt
index b2de7c8..23f697c 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -29,16 +29,6 @@
     [`(let ,id ,expr ,body) (interpret- `((λ ,id ,body) ,expr) ctx)]
     [expr (err (format "interpreting an unknown expression ~a" expr))]))
 
-;; removes typing annotations. this is helpful for interpretation.
-(define (strip expr)
-  (match expr
-    [`(,a ,b) `(,(strip a) ,(strip b))]
-    [`(λ ,id ,body) `(λ ,id ,(strip body))]
-    [`(let ,id ,expr ,body) `(let ,id ,(strip expr) ,(strip body))]
-    [`(λ ,id (: ,type) ,body) (strip `(λ ,id ,body))]
-    [`(let ,id (: ,type) ,expr ,body) (strip `(let ,id ,expr ,body))]
-    [expr expr]))
-
 ;;      (check Expr Type Table[Sym, Type]): Bool
 (define (check expr with [ctx #hash()])
   (match expr
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index 902d75d..a8ab219 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -66,15 +66,6 @@
 
     [expr (err (format "desugaring unknown expression ~a" expr))]))
 
-;; removes typing annotations
-(define (strip expr)
-  (match expr
-    [`(λ ,id (: ,type) ,body (: ,type)) `(λ ,(strip id) ,(strip body))]
-    [`(λ ,id ,body (: ,type)) `(λ ,(strip id) ,(strip body))]
-    [`(λ ,id (: ,type) ,body) `(λ ,(strip id) ,(strip body))]
-    [`(,a ,b) `(,(strip a) ,(strip b))]
-    [expr expr]))
-
 ;;      (check Expr Type Table[Sym, Type]): Bool
 (define (check expr with [Γ #hash()])
   (check- (desugar expr) with Γ))
@@ -184,30 +175,6 @@
     [`(λ ,x (: ,τ) ,e) (level-body e (dict-set Γ x τ))] ; todo: should be 0?
     [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]))
 
-;;      (fmt Expr) → String
-(define (fmt expr)
-  (match expr
-    ['⟨⟩ "⟨⟩"]
-    [`(λ ,id ,body) (format "λ~a.[~a]" id (fmt body))]
-    [`((λ ,id ,body) ,arg) (format "~a = ~a; ~a" id (fmt arg) (fmt body))]
-    [`(λ ,id (: ,type) ,body) (format "~a: ~a; ~a" id (fmt type) (fmt body))]
-    [`((λ ,id (: ,type) ,body) ,arg) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt arg) (fmt body))]
-    [`(λ ,id ,body ,env) (format "λ~a.[~a]" id (fmt body))]
-    [`(let ,id ,expr ,body) (format "~a = ~a; ~a" id (fmt expr) (fmt body))]
-    [`(let ,id (: ,type) ,expr ,body) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt expr) (fmt body))]
-    [`(set ,id ,expr ,body) (format "~a := ~a; ~a" id (fmt expr) (fmt body))]
-    [`(→ ,a ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
-    [`(→ ,k ,a ,b) (format "(~a →~a ~a)" (fmt a) k (fmt b))]
-    [`(Ref ,a) (format "Ref ~a" (fmt a))]
-    [`(new ,a) (format "new ~a" (fmt a))]
-    [`(! ,a) (format "!~a" (fmt a))]
-    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
-    [(hash-table) "{}"] ; fixme lmao
-    [(hash-table (k v)) (format "{~a: ~a}" (fmt k) (fmt v))]
-    [(hash-table (k1 v1) (k2 v2)) (format "{~a: ~a; ~a: ~a}" (fmt k1) (fmt v1) (fmt k2) (fmt v2))]
-    [(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)]))
-
 ; simple diverging program in STLC-ref
 ; https://www.youtube.com/watch?v=XNgE8kBfSz8
 #;
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index a3b6a90..29f4527 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -22,7 +22,8 @@
     ; references
     [`(ref ,id) `(ref ,id)]                 ; refs. pointer to immutable bound value
     [`(deref ,id)                           ; deref. accesses a stored reference from the heap
-      (interpret- (dict-get heap id) ctx heap)]
+      #:when (dict-has-key? heap id)
+      (interpret- (dict-ref heap id) ctx heap)]
     [`(set ,id ,expr ,body)                 ; set. arbitrarily updates a reference to point elsewhere
       ; note: MUST resolve the binding before applying!! !!
       (interpret- body ctx (dict-set heap id (interpret- expr ctx heap)))]
@@ -38,42 +39,9 @@
 
     ; desugaring and error handling
     [`(let ,id ,expr ,body) (interpret- `((λ ,id ,body) ,expr) ctx heap)]
+    [`(deref ,id) (err (format "attempting to deref unknown reference ~a" id))]
     [expr (err (format "interpreting an unknown expression ~a" expr))]))
 
-;; removes typing annotations.
-(define (strip expr)
-  (match expr
-    [`(,a ,b) `(,(strip a) ,(strip b))]
-    [`(λ ,id ,body) `(λ ,id ,(strip body))]
-    [`(let ,id ,expr ,body) `(let ,id ,(strip expr) ,(strip body))]
-    [`(λ ,id (: ,type) ,body) (strip `(λ ,id ,body))]
-    [`(let ,id (: ,type) ,expr ,body) (strip `(let ,id ,expr ,body))]
-    [expr expr]))
-
-(define (dict-get dict key)
-  (dict-ref dict key (λ () (err (format "identifier ~a not found" key)))))
-
-(define (fmt expr)
-  (match expr
-    [`(λ ,id ,body) (format "λ~a.[~a]" id (fmt body))]
-    [`((λ ,id ,body) ,arg) (format "~a = ~a; ~a" id (fmt arg) (fmt body))]
-    [`(λ ,id (: ,type) ,body) (format "~a: ~a; ~a" id (fmt type) (fmt body))]
-    [`((λ ,id (: ,type) ,body) ,arg) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt arg) (fmt body))]
-    [`(λ ,id ,body ,ctx) (format "λ~a.[~a]" id (fmt body))]
-    [`(let ,id ,expr ,body) (format "~a = ~a; ~a" id (fmt expr) (fmt body))]
-    [`(let ,id (: ,type) ,expr ,body) (format "~a: ~a; ~a = ~a; ~a" id (fmt type) id (fmt expr) (fmt body))]
-    [`(set ,id ,expr ,body) (format "~a := ~a; ~a" id (fmt expr) (fmt body))]
-    [`(→ ,a ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
-    [`(Ref ,a) (format "Ref ~a" (fmt a))]
-    [`(ref ,a) (format "&~a" (fmt a))]
-    [`(deref ,a) (format "*~a" (fmt a))]
-    [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
-    [(hash-table) "{}"]
-    [(hash-table (k v)) (format "{~a: ~a}" (fmt k) (fmt v))]
-    [(hash-table (k1 v1) (k2 v2)) (format "{~a: ~a; ~a: ~a}" (fmt k1) (fmt v1) (fmt k2) (fmt v2))]
-    [(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)]))
-
 ; simple diverging program in STLC-ref
 ; https://www.youtube.com/watch?v=XNgE8kBfSz8
 (interpret '