diff options
Diffstat (limited to 'stlc-ext.rkt')
| -rw-r--r-- | stlc-ext.rkt | 57 |
1 files changed, 29 insertions, 28 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt index eb65c87..45cd5bc 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -82,7 +82,7 @@ [(s 'Str) #:when (string? s) #t] [(n 'Nat) #:when (natural? n) #t] [(b 'Bool) #:when (boolean? b) #t] - [(e `(+ ,t1 ,t2)) + [(e `(,t1 ⊕ ,t2)) (or (check- e t1 Γ) (check- e t2 Γ))] [(x _) #:when (dict-has-key? Γ x) (equiv? (dict-ref Γ x) with Γ Γ)] @@ -96,32 +96,32 @@ (and (check- c 'Bool Γ) (check- e1 with Γ) (check e2 with Γ))] - [(`(pair ,e1 ,e2) `(× ,t1 ,t2)) + [(`(pair ,e1 ,e2) `(,t1 × ,t2)) (and (check- e1 t1 Γ) (check- e2 t2 Γ))] [(`(car ,e) with) (match (infer- e Γ) - [`(× ,t1 ,t2) (equiv? t1 with Γ Γ)] + [`(,t1 × ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(cdr ,e) with) (match (infer- e Γ) - [`(× ,t1 ,t2) (equiv? t2 with Γ Γ)] + [`(,t1 × ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(inl ,e) with) (match (infer- e Γ) - [`(+ ,t1 ,t2) (equiv? t1 with Γ Γ)] + [`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)] [t #f])] [(`(inr ,e) with) (match (infer- e Γ) - [`(+ ,t1 ,t2) (equiv? t2 with Γ Γ)] + [`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)] [t #f])] [(`(case ,e ,f1 ,f2) with) (match* ((infer- f1 Γ) (infer- f2 Γ)) - [(`(→ ,a1 ,t1) `(→ ,a2 ,t2)) - (and (check- e `(+ ,a1 ,a2)) - (check- f1 `(→ ,a1 ,with) Γ) (check- f2 `(→ ,a2 ,with) Γ))] + [(`(,a1 → ,t1) `(,a2 → ,t2)) + (and (check- e `(,a1 ⊕ ,a2)) + (check- f1 `(,a1 → ,with) Γ) (check- f2 `(,a2 → ,with) Γ))] [(t1 t2) #f])] - [(`(,e (: ,t)) with) + [(`(,e : ,t) with) (and (equiv? t with Γ Γ) (check- e t Γ))] [('nil `(List ,t)) #t] @@ -134,11 +134,11 @@ [(`(tail ,e) with) (equiv? (infer- e Γ) with Γ Γ)] - [(`(λ ,x (: ,t) ,e) `(→ ,t1 ,t2)) + [(`(λ (,x : ,t) ,e) `(,t1 → ,t2)) (and (equiv? t t1 Γ Γ) (check- e t2 (dict-set Γ x t1)))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,t1 → ,t2) (and (equiv? t2 t Γ Γ) (equiv? t1 (infer- e2 Γ) Γ Γ))] [t #f])] @@ -171,31 +171,31 @@ (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))] [`(pair ,e1 ,e2) - `(× ,(infer- e1 Γ) ,(infer- e2 Γ))] + `(,(infer- e1 Γ) × ,(infer- e2 Γ))] [`(car ,e) (match (infer- e Γ) - [`(× ,t1 ,t2) t1] + [`(,t1 × ,t2) t1] [t (err (format "calling car on incorrect type ~a" t))])] [`(cdr ,e) (match (infer- e Γ) - [`(× ,t1 ,t2) t2] + [`(,t1 × ,t2) t2] [t (err (format "calling cdr on incorrect type ~a" t))])] [`(inl ,e) (match (infer- e Γ) - [`(+ ,t1 ,t2) t1] + [`(,t1 ⊕ ,t2) t1] [t (err (format "calling inl on incorrect type ~a" t))])] [`(inr ,e) (match (infer- e Γ) - [`(+ ,t1 ,t2) t2] + [`(,t1 ⊕ ,t2) t2] [t (err (format "calling inr on incorrect type ~a" t))])] [`(case ,e ,f1 ,f2) (match* ((infer- f1 Γ) (infer- f2 Γ)) - [(`(→ ,a1 ,t1) `(→ ,a2 ,t2)) - (if (and (check- e `(+ ,a1 ,a2)) (equiv? t1 t2 Γ Γ)) t1 + [(`(,a1 → ,t1) `(,a2 → ,t2)) + (if (and (check- e `(,a1 ⊕ ,a2)) (equiv? t1 t2 Γ Γ)) t1 (err (format "case ~a is not of consistent type!" `(case ,e ,f1 ,f2))))] [(t1 t2) (err (format "case ~a is malformed!" `(case ,e ,f1 ,f2)))])] - [`(,e (: ,t)) + [`(,e : ,t) (if (check- e t Γ) t (err (format "annotated expression ~a is not of annotated type ~a" e t)))] @@ -213,11 +213,11 @@ [`(List ,t) `(List ,t)] [t (err (format "calling tail on incorrect type ~a" t))])] - [`(λ ,x (: ,t) ,e) - `(→ ,t ,(infer- e (dict-set Γ x t)))] + [`(λ (,x : ,t) ,e) + `(,t → ,(infer- e (dict-set Γ x t)))] [`(,e1 ,e2) (match (infer- e1 Γ) - [`(→ ,t1 ,t2) + [`(,t1 → ,t2) (if (check- e2 t1 Γ) t2 (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))] [t (err (format "expected → type on application body, got ~a" t))])] @@ -234,9 +234,10 @@ (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 x2) (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)] - [(`(λ ,x1 (: _) ,e1) `(λ ,x2 (: _) ,e2)) ; todo: merge these into one + [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) ; todo: merge these into one (let ([name gensym]) - (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + (and (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) + (equiv? t1 t2 Γ1 Γ2)))] [(`(λ ,x1 ,e1) `(λ ,x2 ,e2)) (let ([name gensym]) (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] @@ -248,6 +249,6 @@ (check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))))) (check-eq? (interpret '(if #t 1 0)) 1) -(check-eq? (interpret '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 2) -(check-eq? (infer '(type Natural Nat ((λ x (: Natural) (inc x)) 1))) 'Nat) -(check-true (check '(type Natural Nat ((λ x (: Natural) (inc x)) 1)) 'Nat)) +(check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2) +(check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat) +(check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat)) |