aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-08-31 21:37:40 +0000
committerJJ2024-08-31 21:37:40 +0000
commit89104040aff982da74ad08412ec2322587eb656a (patch)
treebb6ce9006bcf37c7df43edd52378ca28d6b1d50b
parent62717b52649129131ae69381e22b2bc09ff93dc7 (diff)
stlc-full: fix bugs
-rw-r--r--stlc-full.rkt14
1 files changed, 7 insertions, 7 deletions
diff --git a/stlc-full.rkt b/stlc-full.rkt
index b355292..28629ae 100644
--- a/stlc-full.rkt
+++ b/stlc-full.rkt
@@ -373,11 +373,11 @@
[`(if ,c ,e1 ,e2)
(level-max (level-expr c Γ)
- (level-expr e1 Γ) (level-expr e2 Γ))]
+ (level-max (level-expr e1 Γ) (level-expr e2 Γ)))]
[`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
(level-max (level-expr c Γ) ; support shadowing
- (level-expr e1 (dict-remove Γ x1))
- (level-expr e2 (dict-remove Γ x2)))]
+ (level-max (level-expr e1 (dict-remove Γ x1))
+ (level-expr e2 (dict-remove Γ x2))))]
[`(λ (,x : ,_) ,e) ; support shadowing
(level-expr e (dict-remove Γ x))]
@@ -526,8 +526,8 @@
;; Expands a type alias into weak-head normal form, for literal matching.
(define/contract (expand-whnf t Γ) (-> type? dict? type?)
- (if (dict-has-key? Γ `(type t))
- (expand-whnf (dict-ref Γ t) Γ) t))
+ (if (dict-has-key? Γ `(type ,t))
+ (expand-whnf (dict-ref Γ `(type ,t)) Γ) t))
;; Replaces all references to a type alias with another alias.
(define/contract (replace-type type key value) (-> type? type? type? type?)
@@ -563,7 +563,7 @@
(cbv-core e Γ Σ)]
[`(new ,e)
- (let ([p (alloc! Σ (level-expr e))])
+ (let ([p (alloc! Σ (level-expr e Γ))])
(write! Σ p (cbv-core e Γ Σ)))]
[`(! ,e)
(match (cbv-core e Γ Σ)
@@ -771,7 +771,7 @@
[t (err (format "case has incorrect type ~a on condition, expected a sum" t))])]
[`(unfold ,e)
- (match (expand-whnf (infer-core e Γ) Γ)
+ (match (infer-core e Γ)
[`(μ ,x ,t) (replace-type t x `(μ ,x ,t))]
[t (err (format "expected ~a to be of recursive type, got ~a" e t))])]