From 5d17c1e7254e1359484b4dfd7a1236cf6f3b8adb Mon Sep 17 00:00:00 2001
From: JJ
Date: Thu, 20 Jun 2024 13:19:52 -0700
Subject: stlc-ext: typecheck boolean and natural operations

---
 stlc-ext.rkt | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'stlc-ext.rkt')

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)
-- 
cgit v1.2.3-70-g09d2