From cdaf46285227528e336418144ed9faae58e5422a Mon Sep 17 00:00:00 2001
From: JJ
Date: Fri, 14 Jun 2024 20:51:32 -0700
Subject: stlc-*: do not throw errors within check

---
 stlc-let.rkt  | 4 ++--
 stlc-pred.rkt | 7 +++----
 stlc-ref.rkt  | 6 +++---
 stlc.rkt      | 4 ++--
 4 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/stlc-let.rkt b/stlc-let.rkt
index ab42711..3d6afc6 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -32,8 +32,8 @@
     [(`(,e1 ,e2) t)
       (match (infer- e1 Γ)
         [`(→ ,t1 ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-    [(e t) (err (format "checking an unknown expression ~a with type ~a" e t))]))
+        [t #f])]
+    [(e t) #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index 0a4f61f..cc81a8f 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -21,7 +21,7 @@
     [(`(set ,e1 ,e2) 'Unit)                 ; ↝ Γ ⊢ e1 := e2: Unit
       (match (infer- e1 Γ)
         [`(Ref ,t) (check- e2 t Γ)]         ; Γ ⊢ e1: Ref τ, Γ ⊢ e2: τ
-        [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
+        [t #f])]
 
     [(`(λ ,x (: ,t) ,e) `(→ ,k ,t1 ,t2))    ; ↝ Γ ⊢ λx: τ1.e: τ1 →k τ2
       (and
@@ -32,10 +32,9 @@
       (match (infer- e1 Γ)
         [`(→ ,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))])]
+        [t #f])]
 
-    [(`(λ ,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))]))
+    [(e t) #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index 6194728..73365f2 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -54,7 +54,7 @@
     [(`(set ,e1 ,e2) 'Unit)
       (match (infer- e1 Γ)
         [`(Ref ,t) (check- e2 t Γ)]
-        [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
+        [t #f])]
 
     [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2))
       (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
@@ -62,9 +62,9 @@
       (match (infer- e1 Γ)
         [`(→ ,t1 ,t2)
           (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
+        [t #f])]
 
-    [(e t) (err (format "checking an unknown expression ~a with type ~a" e t))]))
+    [(e t) #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
diff --git a/stlc.rkt b/stlc.rkt
index bf65b73..7979239 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -26,8 +26,8 @@
     [(`(,e1 ,e2) t)
       (match (infer e1 Γ)
         [`(→ ,t1 ,t2) (and (equal? t2 t) (equal? t1 (infer e2 Γ)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-    [(e t) (err (format "checking an unknown expression ~a with type ~a" e t))]))
+        [t #f])]
+    [(e t) #f]))
 
 ;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr [Γ #hash()])
-- 
cgit v1.2.3-70-g09d2