diff options
Diffstat (limited to 'stlc-let.rkt')
| -rw-r--r-- | stlc-let.rkt | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/stlc-let.rkt b/stlc-let.rkt index f906e48..089f9d0 100644 --- a/stlc-let.rkt +++ b/stlc-let.rkt @@ -23,21 +23,12 @@ (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) (match with - ['sole (equal? 'Unit with)] - [n #:when (natural? n) (equal? 'Nat with)] - [x #:when (dict-has-key? Γ x) - (equal? (dict-ref Γ x) 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 Γ)))] - [_ #f])] - [_ #f])) + [_ (equal? (infer-core expr Γ) with)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -46,6 +37,7 @@ (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] [`(λ (,x : ,t) ,e) `(,t → ,(infer-core e (dict-set Γ x t)))] [`(,e1 ,e2) |