aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-06-05 18:30:49 +0000
committerJJ2024-06-05 18:30:49 +0000
commitee8159945ceddc74058a3c26070e0470a19cfa7e (patch)
tree764181aa17697df2b1756dbe424d0be355e5a002
parent3d1fe69221ec3f4779ba080e91b2ab66e74462af (diff)
stld-pred: bugfixes
-rw-r--r--stlc-pred.rkt8
1 files changed, 3 insertions, 5 deletions
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index 10dc4a5..902d75d 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -8,14 +8,12 @@
(interpret- (strip (desugar expr)) ctx heap))
(define (interpret- expr ctx heap)
(match expr
- [x #:when (dict-has-key? ctx x) ; x
- (interpret- (dict-ref ctx x) ctx heap)]
+ [x #:when (dict-has-key? ctx x) (dict-ref ctx x)] ; x
[x #:when (dict-has-key? heap x) x] ; todo
[n #:when (natural? n) n] ; n
['⟨⟩ '⟨⟩] ; ⟨⟩
[`(λ ,id ,body) `(λ ,id ,body ,ctx)] ; λx:τ.e
- [`(λ ,id ,body ,env) `(λ ,id ,body ,env)]
[`(new ,expr) ; new e
(let ([address (gensym)])
@@ -85,8 +83,8 @@
(match* (expr with)
[(n 'Nat) #:when (natural? n) #t] ; ↝ Γ ⊢ n: Nat
[('⟨⟩ 'Unit) #t] ; ↝ Γ ⊢ ⟨⟩: Unit
- [(val _) #:when (dict-has-key? Γ val) ; x: τ ∈ Γ → Γ ⊢ x: τ
- (equal? (dict-ref Γ val) with)]
+ [(x _) #:when (dict-has-key? Γ x) ; x: τ ∈ Γ → Γ ⊢ x: τ
+ (equal? (dict-ref Γ x) with)]
[(`(new ,e) `(Ref ,τ)) (check- e τ Γ)] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ
[(`(! ,e) τ) (check- e `(Ref ,τ) Γ)] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ