From 906073e9c4d051e6bdc738d0fd18efccce147b8b Mon Sep 17 00:00:00 2001 From: JJ Date: Fri, 7 Jun 2024 18:16:27 -0700 Subject: lib: provide fmt and strip functions --- lib.rkt | 39 ++++++++++++++++++++++++++++++++++++++- stlc-let.rkt | 10 ---------- stlc-pred.rkt | 33 --------------------------------- stlc-ref.rkt | 38 +++----------------------------------- 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 ' -- cgit v1.2.3-70-g09d2