aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-06-20 20:19:52 +0000
committerJJ2024-06-20 20:47:53 +0000
commit5d17c1e7254e1359484b4dfd7a1236cf6f3b8adb (patch)
treebf010ad3493e7c27c2cd82c93438623bf063b62b
parent011219189f4d6525ee844bcf9ff03fcf3555ee2c (diff)
stlc-ext: typecheck boolean and natural operations
-rw-r--r--stlc-ext.rkt17
1 files changed, 17 insertions, 0 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 04c84bd..1ab83ba 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -88,6 +88,12 @@
[(`(type ,t1 ,t2 ,in) with)
(check- in with (dict-set Γ t1 t2))]
+ [(`(inc ,e) 'Nat)
+ (check- e 'Nat Γ)]
+ [(`(if ,c ,e1 ,e2) with)
+ (and (check- c 'Bool Γ)
+ (check- e1 with Γ) (check e2 with Γ))]
+
[(`(pair ,e1 ,e2) `(× ,t1 ,t2))
(and (check- e1 t1 Γ) (check- e2 t2 Γ))]
[(`(car ,e) with)
@@ -151,6 +157,17 @@
[`(type ,t1 ,t2 ,in)
(infer in (dict-set Γ t1 t2))]
+ [`(inc ,e)
+ (if (check- e 'Nat Γ) 'Nat
+ (err (format "calling inc on incorrect type ~a" (infer- e Γ))))]
+ [`(if ,c ,e1 ,e2)
+ (if (check- c 'Bool Γ)
+ (let ([t (infer- e1 Γ)])
+ (if (check- e2 t Γ) t
+ (err (format "condition has branches of differing types ~a and ~a"
+ t (infer- e2 Γ)))))
+ (err (format "condition ~a has incorrect type ~a" c (infer- c Γ))))]
+
[`(pair ,e1 ,e2)
`(× ,(infer- e1 Γ) ,(infer- e2 Γ))]
[`(car ,e)