diff options
| -rw-r--r-- | stlc-let.rkt | 4 | ||||
| -rw-r--r-- | stlc-pred.rkt | 7 | ||||
| -rw-r--r-- | stlc-ref.rkt | 6 | ||||
| -rw-r--r-- | 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()]) @@ -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()]) |