From cb9799b57a0afe78e6019875075bf0d3a4b34c01 Mon Sep 17 00:00:00 2001
From: JJ
Date: Thu, 20 Jun 2024 13:45:11 -0700
Subject: stlc-ext: conditional fixes and tests

---
 stlc-ext.rkt | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 5f9af56..eb65c87 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -9,7 +9,7 @@
 ;;      (interpret Expr Table[Sym, Expr]): Value
 (define (interpret expr [Γ #hash()])
   (interpret- (strip (desugar expr)) Γ))
-(define (interpret- expr Γ Σ)
+(define (interpret- expr Γ)
   (match expr
     ['sole 'sole]
     [s #:when (string? s) s]
@@ -18,13 +18,13 @@
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
 
     [`(inc ,e)
-      (match (interpret- e Γ Σ)
+      (match (interpret- e Γ)
         [n #:when (natural? n) (+ n 1)]
         [e (format "incrementing an unknown value ~a" e)])]
     [`(if ,c ,e1 ,e2)
-      (match (interpret- c Γ Σ)
-        ['#t (interpret- e1 Γ Σ)]
-        ['#f (interpret- e2 Γ Σ)]
+      (match (interpret- c Γ)
+        ['#t (interpret- e1 Γ)]
+        ['#f (interpret- e2 Γ)]
         [e (err (format "calling if on unknown expression ~a" e))])]
 
     [`(pair ,e1 ,e2)
@@ -246,3 +246,8 @@
 (check-true (equiv? '(λ a a) '(λ b b)))
 (check-true (equiv? '(λ a (λ b a)) '(λ b (λ a b))))
 (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))
-- 
cgit v1.2.3-70-g09d2