diff options
Diffstat (limited to 'stlc-imp.rkt')
| -rw-r--r-- | stlc-imp.rkt | 45 |
1 files changed, 25 insertions, 20 deletions
diff --git a/stlc-imp.rkt b/stlc-imp.rkt index 541de2c..fc34115 100644 --- a/stlc-imp.rkt +++ b/stlc-imp.rkt @@ -31,38 +31,43 @@ (define (check expr with) (check-core (desugar expr) with #hash())) (define (check-core expr with Γ) - (match* (expr with) - [('sole 'Unit) #t] - [(n 'Nat) #:when (natural? n) #t] - [(x _) #:when (dict-has-key? Γ x) + (match with + ['sole (equal? 'Unit with)] + [n #:when (natural? n) (equal? 'Nat with)] + [x #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(new ,e) `(Ref ,t)) (check-core e t Γ)] - [(`(! ,e) t) (check-core e `(Ref ,t) Γ)] - [(`(set ,e1 ,e2) 'Unit) + [`(new ,e) + (match with + [`(Ref ,t) (check-core e t Γ)] + [_ #f])] + [`(! ,e) (check-core e `(Ref ,with) Γ)] + [`(set ,e1 ,e2) (match (infer-core e1 Γ) - [`(Ref ,t) (check-core e2 t Γ)] - [t #f])] - - [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2)) - (and - (equal? t t1) - (> k (max-level e (dict-set Γ x t1) t1 t2)) ; KNOB - (check-core e t2 (dict-set Γ x t1)))] - [(`(,e1 ,e2) t) + [`(Ref ,t) + (and (equal? 'Unit with) + (check-core e2 t Γ))] + [_ #f])] + + [`(λ (,x : ,t) ,e) + (match with + [`(,t1 → ,k ,t2) + (and (equal? t t1) (check-core e t2 (dict-set Γ x t)) + (> k (max-level e t1 t2 (dict-set Γ x t1))))] ; KNOB + [_ #f])] + [`(,e1 ,e2) (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) - (and (equal? t2 t) + (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] - [t #f])] + [_ #f])] - [(e t) #f])) + [_ #f])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) (infer-core (desugar expr) #hash())) (define (infer-core expr Γ) - ; (print (format "infer: ~a" (fmt expr))) (match expr ['sole 'Unit] [n #:when (natural? n) 'Nat] |