diff options
| -rw-r--r-- | stlc-dll.rkt | 8 | ||||
| -rw-r--r-- | stlc-ext.rkt | 4 | ||||
| -rw-r--r-- | stlc-fix.rkt | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/stlc-dll.rkt b/stlc-dll.rkt index 296648e..31c5bcc 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -91,7 +91,7 @@ (define (check-core expr with Γ) (match expr [`(type ,t1 ,t2 ,in) - (check-core in with (dict-set Γ t1 t2))] + (check-core in with (dict-set Γ `(type ,t1) t2))] [`(if ,c ,e1 ,e2) (and (check-core c 'Bool Γ) @@ -111,7 +111,7 @@ [`(,t1 ⊕ ,t2) (check-core e t2 Γ)] [_ #f])] [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) - (match (infer-core e Γ) + (match (infer-core e Γ) ; avoid needing type annotation on e [`(,a1 ⊕ ,a2) (and (check-core e1 with (dict-set Γ x1 a1)) (check-core e2 with (dict-set Γ x2 a2)))] @@ -126,7 +126,7 @@ [`(fold ,e) (match with - [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))] + [`(μ ,x ,t) (check-core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))] [_ #f])] [`(λ (,x : ,t) ,e) @@ -175,7 +175,7 @@ (expand (dict-ref Γ x) Γ)] [`(type ,t1 ,t2 ,in) - (infer-core in (dict-set Γ t1 t2))] + (infer-core in (dict-set Γ `(type ,t1) t2))] [`(,e : ,t) ; we have a manual type annotation, so we must expand to weak-head normal form (if (check-core e (expand t Γ) Γ) (expand t Γ) (err (format "annotated expression ~a is not of annotated type ~a" e t)))] diff --git a/stlc-ext.rkt b/stlc-ext.rkt index 84c476c..2662135 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -208,8 +208,8 @@ ;; Expands a type alias into weak-head normal form, for literal matching. ;; (expand Type Table[Id, Expr ⊕ Type]): Type (define (expand t Γ) - (if (dict-has-key? Γ t) - (expand (dict-ref Γ t) Γ) t)) + (if (dict-has-key? Γ `(type ,t)) + (expand (dict-ref Γ `(type ,t)) Γ) t)) ;; Checks if two types are equivalent up to α-conversion in context ;; (equiv-type Expr Expr Table[Sym Expr]): Bool diff --git a/stlc-fix.rkt b/stlc-fix.rkt index 2c68696..420aa15 100644 --- a/stlc-fix.rkt +++ b/stlc-fix.rkt @@ -17,7 +17,7 @@ (match (interpret-core e Γ) [`(λ ,x ,e ,env) ; FIXME: unsure what should be Γ and what should be env - (interpret-core e (dict-set Γ x `(fix (λ ,x ,e ,Γ))))] + (interpret-core e (dict-set env x `(fix (λ ,x ,e ,Γ))))] [e (err (format "applying fix to unknown expression ~a" e))])] [`(λ ,id ,body) `(λ ,id ,body ,Γ)] |