diff options
Diffstat (limited to 'stlc-pred.rkt')
-rw-r--r-- | stlc-pred.rkt | 56 |
1 files changed, 12 insertions, 44 deletions
diff --git a/stlc-pred.rkt b/stlc-pred.rkt index ee64fcb..9f3fc9c 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -29,37 +29,19 @@ (check-core (desugar expr) with #hash())) (define (check-core expr 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)] - [`(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) - (and (equal? 'Unit with) - (check-core e2 t Γ))] - [_ #f])] [`(λ (,x : ,t) ,e) (match with [`(,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) - (match (infer-core e1 Γ) - [`(,t1 → ,k ,t2) - (and (equal? t2 with) (equal? t1 (infer-core e2 Γ)))] + (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)) + (>= k (level-body e (dict-set Γ x t1))))] ; KNOB [_ #f])] - [_ #f])) + [_ (equal? (infer-core expr Γ) with)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -85,9 +67,9 @@ [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] [`(λ (,x : ,t1) ,e) - (let ([t2 (infer-core e (dict-set Γ x t1))]) - (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; (KNOB) - `(,t1 → ,k ,t2)))] + (let* ([t2 (infer-core e (dict-set Γ x t1))] + [k (level-body e (dict-set Γ x t1))]) ; KNOB + `(,t1 → ,k ,t2))] [`(,e1 ,e2) (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) @@ -97,23 +79,14 @@ [e (err (format "attempting to infer an unknown expression ~a" e))])) -;; (max-level Table[Sym, Type] Expr Type Type): Natural -(define (max-level e Γ t1 t2) - (max - (level-type t1) - (level-type t2) - (level-body e Γ))) - ;; (level-type Type): Natural (define (level-type t) (match t - ['Unit 0] - ['Nat 0] + [(or 'Unit 'Nat) 0] [`(,t1 → ,k ,t2) - (if (or (< k (level-type t1)) (< k (level-type t2))) + (if (and (>= k (level-type t1)) (>= k (level-type t2))) k (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" - k t1 t2)) - k)] + k t1 t2)))] [`(Ref ,t) (+ 1 (level-type t))] ; (KNOB) [t (err (format "attempting to infer the level of unknown type ~a" t))])) @@ -124,14 +97,9 @@ [n #:when (natural? n) 0] [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))] - - [`(new ,e) (level-body e Γ)] - [`(! ,e) (level-body e Γ)] - [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))] - - [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? - [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))] - [e (err (format "attempting to infer the level of unknown expression ~a" e))])) + [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)] + [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))] + [x #:when (symbol? x) 0])) ; simple diverging program in STLC-ref ; https://www.youtube.com/watch?v=XNgE8kBfSz8 |