diff options
Diffstat (limited to 'stlc-fix.rkt')
| -rw-r--r-- | stlc-fix.rkt | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/stlc-fix.rkt b/stlc-fix.rkt index 8fa96f9..ad45b90 100644 --- a/stlc-fix.rkt +++ b/stlc-fix.rkt @@ -35,26 +35,17 @@ (define (check-core expr with Γ) (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)]) (match expr - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) with)] - [`(fix ,e) (check-core (infer-core e) `(,with → ,with) Γ)] [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) - (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))] - [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] + (and (equal? t1 t) + (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [_ #f]))) + [_ (equal? (infer-core expr Γ) with)]))) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -63,8 +54,7 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] - [x #:when (dict-has-key? Γ x) - (dict-ref Γ x)] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(fix ,e) (match (infer-core e Γ) |