aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-06-17 00:16:51 +0000
committerJJ2024-06-17 00:20:15 +0000
commit3a4704b8fce33f3d86897ff857d59462b93a6755 (patch)
treedc22e23e7d542a2891f6f7b92976896b2af44e74
parent4906ecb9802c7e9889a8399b3cf2553d0daa5d6c (diff)
stlc-ext: add primitive operations on booleans and naturals
-rw-r--r--stlc-ext.rkt11
1 files changed, 10 insertions, 1 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 0bc69b5..80ff6d9 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -15,6 +15,16 @@
[b #:when (boolean? b) b]
[x #:when (dict-has-key? ctx x) (dict-ref ctx x)]
+ [`(inc ,e)
+ (match (interpret- e ctx heap)
+ [n #:when (natural? n) (+ n 1)]
+ [e (format "incrementing an unknown value ~a" e)])]
+ [`(if ,c ,e1 ,e2)
+ (match (interpret- c ctx heap)
+ ['#t (interpret- e1 ctx heap)]
+ ['#f (interpret- e2 ctx heap)]
+ [e (err (format "calling if on unknown expression ~a" e))])]
+
[`(pair ,e1 ,e2)
`(pair ,(interpret- e1 ctx) ,(interpret- e2 ctx))]
[`(car ,e)
@@ -64,7 +74,6 @@
(define (check expr with [Γ #hash()])
(check- (desugar expr) with Γ))
(define (check- expr with Γ)
- ; (print (format "check: ~a" (fmt expr)))
(let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)])
(match* (expr with)
[('sole 'Unit) #t]