add some typing rules, minor fixes

5 files changed, 85 insertions, 35 deletions

diff --git a/lib.rkt b/lib.rkt
index eb0c201..edb8623 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -34,6 +34,15 @@
 ; todo: write a fmt alias to format
 ; todo: write a namer
 
+(define (any? proc lst)
+  (foldl (λ (x acc) (if (proc x) #t acc)) #f lst))
+
+(define (all? proc lst)
+  (foldl (λ (x acc) (if (proc x) acc #f)) #t lst))
+
+(define (inc i) (+ i 1))
+(define (dec i) (- i 1))
+
 ;; removes typing annotations
 (define (strip expr)
   (match expr
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 80ff6d9..04c84bd 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -61,12 +61,12 @@
         [`(cons ,e1 ,e2) (interpret- e2 ctx)]
         [e (err (format "calling tail on unknown expression ~a" e))])]
 
-    [`(λ ,id ,body) `(λ ,id ,body ,ctx)]
-    [`(,body ,arg)
-      (match (interpret- body ctx)
-        [`(λ ,id ,body ,env)
-          (interpret- body (dict-set env id (interpret- arg ctx)))]
-        [e (err (format "applying arg ~a to unknown expression ~a" arg e))])]
+    [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
+    [`(,e1 ,e2)
+      (match (interpret- e1 ctx)
+        [`(λ ,x ,e ,env)
+          (interpret- e (dict-set env x (interpret- e2 ctx)))]
+        [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
 
     [e (err (format "interpreting an unknown expression ~a" e))]))
 
diff --git a/stlc-imp.rkt b/stlc-imp.rkt
index 4d16188..cd392d9 100644
--- a/stlc-imp.rkt
+++ b/stlc-imp.rkt
@@ -3,6 +3,28 @@
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references
 
+; Γ, x: τ₁ ⊢ e: τ₂    k > max-level(Γ, τ₁, τ₂)
+; ---------------------------------------------
+; Γ ⊢ λx:τ₁.e : τ₁ →ᵏ τ₂
+
+; Γ ⊢ e₁: τ₁ →ᵏ τ₂    Γ ⊢ e₂: τ₁
+; --------------------------------
+; Γ ⊢ (e₁ e₂): τ₂
+
+; --------------------------
+; Nat::Type₀, Unit::Type₀
+
+; τ::Type₀
+; ---------------
+; Ref τ :: Type₀
+
+; τ::Typeᵢ, i ≥ 0
+; ---------------
+; Ref τ :: Typeᵢ₊₁
+
+; τ₁::Typeᵢ, τ₂::Typeⱼ, k > max-level(τ₁, τ₂)
+; -----------------------------------------
+; τ₁ →ᵏ τ₂ :: Typeₖ
 (require (only-in "stlc-ref.rkt" interpret))
 
 ;;      (check Expr Type Table[Sym, Type]): Bool
@@ -93,7 +115,7 @@
         k)]
     [`(Ref ,t)
       (let ([k (level-type t)])
-      (if (zero? k) 0 ((+ 1 k))))] ; KNOB
+      (if (zero? k) 0 (+ 1 k)))] ; KNOB
     [t (err (format "attempting to infer the level of unknown type ~a" t))]))
 
 ;;      (level-body Expr Table[Sym, Type]): Natural
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index cc81a8f..415ecc9 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -3,6 +3,25 @@
 
 ;; The Simply-Typed Lambda Calculus with higher-order *predicative* references
 
+; Γ, x: τ₁ ⊢ e: τ₂    k ≥ max-level(Γ, τ₁, τ₂)
+; ---------------------------------------------
+; Γ ⊢ λx:τ₁.e : τ₁ →ᵏ τ₂
+
+; Γ ⊢ e₁: τ₁ →ᵏ τ₂    Γ ⊢ e₂: τ₁
+; --------------------------------
+; Γ ⊢ (e₁ e₂): τ₂
+
+; --------------------------
+; Nat::Type₀, Unit::Type₀
+
+; τ::Typeᵢ
+; -------------
+; Ref τ :: Typeᵢ₊₁
+
+; τ₁::Typeᵢ, τ₂::Typeⱼ, k ≥ max-level(τ₁, τ₂)
+; -----------------------------------------
+; τ₁ →ᵏ τ₂ :: Typeₖ
+
 (require (only-in "stlc-ref.rkt" interpret))
 
 ;;      (check Expr Type Table[Sym, Type]): Bool
@@ -11,27 +30,27 @@
 (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
-    [(x _) #:when (dict-has-key? Γ x)       ; x: τ ∈ Γ → Γ ⊢ x: τ
+    [('sole 'Unit) #t]
+    [(n 'Nat) #:when (natural? n) #t]
+    [(x _) #:when (dict-has-key? Γ x)
       (equal? (dict-ref Γ x) with)]
 
-    [(`(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
+    [(`(new ,e) `(Ref ,t)) (check- e t Γ)]
+    [(`(! ,e) t) (check- e `(Ref ,t) Γ)]
+    [(`(set ,e1 ,e2) 'Unit)
       (match (infer- e1 Γ)
-        [`(Ref ,t) (check- e2 t Γ)]         ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ
+        [`(Ref ,t) (check- e2 t Γ)]
         [t #f])]
 
-    [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))    ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2
+    [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))
       (and
         (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
+        (>= k (max-level e (dict-set Γ x t1) t1 t2))  ; (KNOB)
+        (check- e t2 (dict-set Γ x t1)))]
+    [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
-        [`(→ ,k ,t1 ,t2)                                  ; Γ ⊢ e1: τ1 →k τ2
-          (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]  ; Γ ⊢ e2: τ1
+        [`(→ ,k ,t1 ,t2)
+          (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
         [t #f])]
 
     [(e t) #f]))
@@ -42,33 +61,33 @@
 (define (infer- expr Γ)
   ; (print (format "infer: ~a" (fmt expr)))
   (match expr
-    ['sole 'Unit]                       ; ↝ Γ ⊢ ⟨⟩: Unit
-    [n #:when (natural? n) 'Nat]        ; ↝ Γ ⊢ n: Nat
-    [x #:when (dict-has-key? Γ x)       ; x: τ ∈ Γ
-      (dict-ref Γ x)]                   ; ↝ Γ ⊢ x: τ
+    ['sole 'Unit]
+    [n #:when (natural? n) 'Nat]
+    [x #:when (dict-has-key? Γ x)
+      (dict-ref Γ x)]
 
-    [`(new ,e) `(Ref ,(infer- e Γ))]    ; Γ ⊢ e: τ → Γ ⊢ new e: Ref τ
+    [`(new ,e) `(Ref ,(infer- e Γ))]
     [`(! ,e)
       (match (infer- e Γ)
-        [`(Ref ,t) t]                   ; Γ ⊢ e: Ref τ → Γ ⊢ !e: τ
+        [`(Ref ,t) t]                   ; Γ ⊢ e: Ref t → Γ ⊢ !e: t
         [t (err "attempting to deref term not of Ref type!")])]
     [`(set ,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(Ref ,t)                      ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ
+        [`(Ref ,t)                      ; Γ ⊢ e1: Ref t, Γ ⊢ e2: t
           (if (check- e2 t Γ) 'Unit     ; ↝ Γ ⊢ e1 := e2: Unit
             (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
               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
+      (let ([t2 (infer- e (dict-set Γ x t1))])            ; Γ, x: t1 ⊢ e: t2
+        (let ([k (max-level e (dict-set Γ x t1) t1 t2)])  ; k ≥ max-level(Γ, t1, t2) (KNOB)
+          `(→ ,k ,t1 ,t2)))]                             ; ↝ Γ ⊢ λx: t1.e: t1 →k t2
     [`(,e1 ,e2)
       (match (infer- e1 Γ)
-        [`(→ ,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)))]
+        [`(→ ,k ,t1 ,t2)                ; Γ ⊢ e1: t1 →k t2
+          (if (check- e2 t1 Γ) t2       ; Γ ⊢ e2: t1 ↝ Γ ⊢ (e1 e2): t2
+            (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))]
         [t (err (format "expected → type on application body, got ~a" t))])]
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
diff --git a/stlc.rkt b/stlc.rkt
index 7979239..f9167ed 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -12,8 +12,8 @@
     [`(λ ,x ,e) `(λ ,x ,e ,ctx)]
     [`(,e1 ,e2)
       (match (interpret- e1 ctx)
-        [`(λ ,x ,e1 ,env) (interpret- e1 (dict-set env x (interpret- e2 ctx)))]
-        [e1 `(,e1 ,(interpret- e2 ctx))])]
+        [`(λ ,x ,e ,env) (interpret- e (dict-set env x (interpret- e2 ctx)))]
+        [e `(,e ,(interpret- e2 ctx))])]
     [e e]))
 
 ;;      (check Expr Type Table[Sym, Type]): Bool