aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-06-15 03:51:32 +0000
committerJJ2024-06-15 03:51:32 +0000
commitcdaf46285227528e336418144ed9faae58e5422a (patch)
tree7de5890975b9275a6d10a27eac79e07e6d8d0af9
parent0947a5ba0ffa38397b4d5e760c5e0ed4c8288e6d (diff)
stlc-*: do not throw errors within check
-rw-r--r--stlc-let.rkt4
-rw-r--r--stlc-pred.rkt7
-rw-r--r--stlc-ref.rkt6
-rw-r--r--stlc.rkt4
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()])