diff options
Diffstat (limited to 'stlc-pred.rkt')
| -rw-r--r-- | stlc-pred.rkt | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/stlc-pred.rkt b/stlc-pred.rkt index d13e60d..c9c77b6 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -25,9 +25,9 @@ (require (only-in "stlc-ref.rkt" interpret)) ;; (check Expr Type Table[Sym, Type]): Bool -(define (check expr with [Γ #hash()]) - (check- (desugar expr) with Γ)) -(define (check- expr with Γ) +(define (check expr with) + (check-core (desugar expr) with #hash())) +(define (check-core expr with Γ) ; (print (format "check: ~a" (fmt expr))) (match* (expr with) [('sole 'Unit) #t] @@ -35,30 +35,30 @@ [(x _) #:when (dict-has-key? Γ x) (equal? (dict-ref Γ x) with)] - [(`(new ,e) `(Ref ,t)) (check- e t Γ)] - [(`(! ,e) t) (check- e `(Ref ,t) Γ)] + [(`(new ,e) `(Ref ,t)) (check-core e t Γ)] + [(`(! ,e) t) (check-core e `(Ref ,t) Γ)] [(`(set ,e1 ,e2) 'Unit) - (match (infer- e1 Γ) - [`(Ref ,t) (check- e2 t Γ)] + (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- e t2 (dict-set Γ x t1)))] + (check-core e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) - (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] + (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))] [t #f])] [(e t) #f])) ;; (infer Expr Table[Sym, Type]): Type -(define (infer expr [Γ #hash()]) - (infer- (desugar expr) Γ)) -(define (infer- expr Γ) +(define (infer expr) + (infer-core (desugar expr) #hash())) +(define (infer-core expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr ['sole 'Unit] @@ -66,28 +66,28 @@ [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] - [`(new ,e) `(Ref ,(infer- e Γ))] + [`(new ,e) `(Ref ,(infer-core e Γ))] [`(! ,e) - (match (infer- e Γ) + (match (infer-core e Γ) [`(Ref ,t) t] [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(Ref ,t) - (if (check- e2 t Γ) 'Unit + (if (check-core e2 t Γ) 'Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 t e2 (infer- e2 Γ))))] + e1 t e2 (infer-core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t1) ,e) - (let ([t2 (infer- e (dict-set Γ x t1))]) + (let ([t2 (infer-core e (dict-set Γ x t1))]) (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; (KNOB) `(,t1 → ,k ,t2)))] [`(,e1 ,e2) - (match (infer- e1 Γ) + (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) - (if (check- e2 t1 Γ) t2 - (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))] + (if (check-core e2 t1 Γ) t2 + (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))] [t (err (format "expected → type on application body, got ~a" t))])] [e (err (format "attempting to infer an unknown expression ~a" e))])) |