diff options
| author | JJ | 2024-06-20 20:45:11 +0000 |
|---|---|---|
| committer | JJ | 2024-06-20 20:47:53 +0000 |
| commit | cb9799b57a0afe78e6019875075bf0d3a4b34c01 (patch) | |
| tree | 2334ac41fd2fb5e6351a42eb7694c778b174a15e | |
| parent | 95b269dbd4337d35b38a53a6c3e87c8b97aa6d14 (diff) | |
stlc-ext: conditional fixes and tests
| -rw-r--r-- | stlc-ext.rkt | 15 |
1 files 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)) |