diff options
| -rw-r--r-- | stlc-pred.rkt | 132 |
1 files changed, 64 insertions, 68 deletions
diff --git a/stlc-pred.rkt b/stlc-pred.rkt index 7865f44..0a4f61f 100644 --- a/stlc-pred.rkt +++ b/stlc-pred.rkt @@ -11,42 +11,39 @@ (define (check- expr with Γ) ; (print (format "check: ~a" (fmt expr))) (match* (expr with) + [('sole 'Unit) #t] ; ↝ Γ ⊢ ⟨⟩: Unit [(n 'Nat) #:when (natural? n) #t] ; ↝ Γ ⊢ n: Nat - [('⟨⟩ 'Unit) #t] ; ↝ Γ ⊢ ⟨⟩: Unit - [(x _) #:when (dict-has-key? Γ x) ; x: τ ∈ Γ → Γ ⊢ x: τ + [(x _) #:when (dict-has-key? Γ x) ; x: τ ∈ Γ → Γ ⊢ x: τ (equal? (dict-ref Γ x) with)] - [(`(new ,e) `(Ref ,τ)) (check- e τ Γ)] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ - [(`(! ,e) τ) (check- e `(Ref ,τ) Γ)] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ + [(`(new ,e) `(Ref ,t)) (check- e t Γ)] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ + [(`(! ,e) t) (check- e `(Ref ,t) Γ)] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ [(`(set ,e1 ,e2) 'Unit) ; ↝ Γ ⊢ e1 := e2: Unit (match (infer- e1 Γ) - [`(Ref ,τ) (check- e2 τ Γ)] ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ - [type (err (format "attempting to update non-reference ~a: ~a" e1 type))])] + [`(Ref ,t) (check- e2 t Γ)] ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ + [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - [(`(λ ,x (: ,τ) ,e) `(→ ,k ,τ1 ,τ2)) ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 + [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2)) ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 (and - (equal? τ τ1) - (>= k (max-level e (dict-set Γ x τ1) τ1 τ2)) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) - (check- e τ2 (dict-set Γ x τ1)))] ; Γ, x: τ1 ⊢ e: τ2 - - [(`(,e1 ,e2) τ) ; ↝ Γ ⊢ (e1 e2): τ2 + (equal? t t1) + (>= k (max-level e (dict-set Γ x t1) t1 t2)) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) + (check- e t2 (dict-set Γ x t1)))] ; Γ, x: τ1 ⊢ e: τ2 + [(`(,e1 ,e2) t) ; ↝ Γ ⊢ (e1 e2): τ2 (match (infer- e1 Γ) - [`(→ ,k ,τ1 ,τ2) ; Γ ⊢ e1: τ1 →k τ2 - (and (equal? τ2 τ) ; Γ ⊢ e2: τ1 - (equal? τ1 (infer- e2 Γ)))] - [type (err (format "expected → type on application body, got ~a" type))])] + [`(→ ,k ,t1 ,t2) ; Γ ⊢ e1: τ1 →k τ2 + (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))] ; Γ ⊢ e2: τ1 + [t (err (format "expected → type on application body, got ~a" t))])] - [(`(λ ,id (: ,type) ,body) `(→ ,a ,b)) ; error handling - (err "you forgot to add a level annotation dummy")] - [(expr _) (err (format "checking an unknown expression ~a with type ~a" expr with))])) + [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) (err "you forgot to add a level annotation dummy")] + [(e t) (err (format "checking an unknown expression ~a with type ~a" e with))])) -;; (infer Expr Table[Sym, Type]) → Type +;; (infer Expr Table[Sym, Type]): Type (define (infer expr [Γ #hash()]) (infer- (desugar expr) Γ)) (define (infer- expr Γ) ; (print (format "infer: ~a" (fmt expr))) (match expr - ['⟨⟩ 'Unit] ; ↝ Γ ⊢ ⟨⟩: Unit + ['sole 'Unit] ; ↝ Γ ⊢ ⟨⟩: Unit [n #:when (natural? n) 'Nat] ; ↝ Γ ⊢ n: Nat [x #:when (dict-has-key? Γ x) ; x: τ ∈ Γ (dict-ref Γ x)] ; ↝ Γ ⊢ x: τ @@ -54,80 +51,79 @@ [`(new ,e) `(Ref ,(infer- e Γ))] ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ [`(! ,e) (match (infer- e Γ) - [`(Ref ,type) type] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ - [_ (err "attempting to deref term not of Ref type!")])] + [`(Ref ,t) t] ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ + [t (err "attempting to deref term not of Ref type!")])] [`(set ,e1 ,e2) (match (infer- e1 Γ) - [`(Ref ,τ) ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ - (if (check- e2 τ Γ) 'Unit ; ↝ Γ ⊢ e1 := e2: Unit + [`(Ref ,t) ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ + (if (check- e2 t Γ) 'Unit ; ↝ Γ ⊢ e1 := e2: Unit (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type" - e1 τ e2 (infer- e2 Γ))))] - [type (err (format "attempting to update non-reference ~a: ~a" e1 type))])] - - [`(λ ,x (: ,τ1) ,e) - (let ([τ2 (infer- e (dict-set Γ x τ1))]) ; Γ, x: τ1 ⊢ e: τ2 - (let ([k (max-level e (dict-set Γ x τ1) τ1 τ2)]) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) - `(→ ,k ,τ1 ,τ2)))] ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 + e1 t e2 (infer- e2 Γ))))] + [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] + [`(λ ,x (: ,t1) ,e) + (let ([t2 (infer- e (dict-set Γ x t1))]) ; Γ, x: τ1 ⊢ e: τ2 + (let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; k ≥ max-level(Γ, τ1, τ2) (KNOB) + `(→ ,k ,t1 ,t2)))] ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2 [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,k ,τ1 ,τ2) ; Γ ⊢ e1: τ1 →k τ2 - (if (check- e2 τ1 Γ) ; Γ ⊢ e2: τ1 - τ2 ; ↝ Γ ⊢ (e1 e2): τ2 - (err (format "inferred argument type ~a does not match arg ~a" τ1 e2)))] - [type (err (format "expected → type on application body, got ~a" type))])] - - [`(λ ,x ,e) ; error handling - (err "unable to infer type from λ lacking parameter annotation")] - [expr (err (format "inferring an unknown expression ~a" expr))])) - -;; (max-level Table[Sym, Type] Expr Type Type) → Natural -(define (max-level e Γ τ1 τ2) + [`(→ ,k ,t1 ,t2) ; Γ ⊢ e1: τ1 →k τ2 + (if (check- e2 t1 Γ) t2 ; Γ ⊢ e2: τ1 ↝ Γ ⊢ (e1 e2): τ2 + (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] + [t (err (format "expected → type on application body, got ~a" t))])] + + [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 τ1) - (level-type τ2) + (level-type t1) + (level-type t2) (level-body e Γ))) -;; (level-type Type) → Natural -(define (level-type τ) - (match τ +;; (level-type Type): Natural +(define (level-type t) + (match t ['Unit 0] ['Nat 0] - [`(→ ,k ,τ1 ,τ2) - (if (or (< k (level-type τ1)) (< k (level-type τ2))) + [`(→ ,k ,t1 ,t2) + (if (or (< k (level-type t1)) (< k (level-type t2))) (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" - k τ1 τ2)) + k t1 t2)) k)] - [`(Ref ,τ) (+ 1 (level-type τ))] ; (KNOB) - [τ (err (format "inferring the level of unknown type ~a" τ))])) + [`(Ref ,t) (+ 1 (level-type t))] ; (KNOB) + [t (err (format "attempting to infer the level of unknown type ~a" t))])) -;; (level-body Expr Table[Sym, Type]) → Natural +;; (level-body Expr Table[Sym, Type]): Natural (define (level-body e Γ) (match e - ['⟨⟩ 0] + ['sole 0] [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 (: ,τ) ,e) (level-body e (dict-set Γ x τ))] ; todo: should be 0? - [`(,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))])) ; simple diverging program in STLC-ref ; https://www.youtube.com/watch?v=XNgE8kBfSz8 #; (interpret ' (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (ref id) - (let f (: (→ 1 Nat Nat)) (λ x ((deref r) x)) + (let r (: (Ref (→ 0 Nat Nat))) (new id) + (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) (set r f (f 0)))))) #; (print (fmt ' (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (ref id) - (let f (: (→ 1 Nat Nat)) (λ x ((deref r) x)) + (let r (: (Ref (→ 0 Nat Nat))) (new id) + (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) (set r f (f 0))))))) @@ -136,24 +132,24 @@ exn:fail? (λ () (infer ' (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (ref id) - (let f (: (→ 1 Nat Nat)) (λ x ((deref r) x)) + (let r (: (Ref (→ 0 Nat Nat))) (new id) + (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) (set r f (f 0)))))))) (check-eq? (infer ' (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (ref id) - (let f (: (→ 1 Nat Nat)) (λ x ((deref r) x)) + (let r (: (Ref (→ 0 Nat Nat))) (new id) + (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) (f 0))))) 'Nat) (check-eq? (check ' (let id (: (→ 0 Nat Nat)) (λ x x) - (let r (: (Ref (→ 0 Nat Nat))) (ref id) - (let f (: (→ 1 Nat Nat)) (λ x ((deref r) x)) + (let r (: (Ref (→ 0 Nat Nat))) (new id) + (let f (: (→ 1 Nat Nat)) (λ x ((! r) x)) (f 0)))) 'Nat) #t) |