aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-07-15 19:28:30 +0000
committerJJ2024-07-15 20:48:34 +0000
commita5a6418813900441e846e6853711dff94d1f9406 (patch)
tree30230e3015d3c0339c8d9d83c786150696617265
parent060acee3310597b5ddbd9bf42635d8ebbdef8f34 (diff)
backport interpret-/infer-/check- renaming and remove implicit params
-rw-r--r--stlc-ext.rkt138
-rw-r--r--stlc-fix.rkt42
-rw-r--r--stlc-imp.rkt45
-rw-r--r--stlc-let.rkt36
-rw-r--r--stlc-pred.rkt44
-rw-r--r--stlc-rec.rkt48
-rw-r--r--stlc-ref.rkt60
-rw-r--r--stlc.rkt12
8 files changed, 212 insertions, 213 deletions
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 93e2dd8..72490a2 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -7,9 +7,9 @@
;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption
;; (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [Γ #hash()])
- (interpret- (strip (desugar expr)) Γ))
-(define (interpret- expr Γ)
+(define (interpret expr)
+ (interpret-core (strip (desugar expr)) #hash()))
+(define (interpret-core expr Γ)
(match expr
['sole 'sole]
[s #:when (string? s) s]
@@ -18,64 +18,64 @@
[x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
[`(inc ,e)
- (match (interpret- e Γ)
+ (match (interpret-core 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-core c Γ)
+ ['#t (interpret-core e1 Γ)]
+ ['#f (interpret-core e2 Γ)]
[e (err (format "calling if on unknown expression ~a" e))])]
[`(pair ,e1 ,e2)
- `(pair ,(interpret- e1 Γ) ,(interpret- e2 Γ))]
+ `(pair ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))]
[`(car ,e)
- (match (interpret- e Γ)
+ (match (interpret-core e Γ)
[`(pair ,e1 ,e2) e1]
[e (err (format "calling car on unknown expression ~a" e))])]
[`(cdr ,e)
- (match (interpret- e Γ)
+ (match (interpret-core e Γ)
[`(pair ,e1 ,e2) e2]
[e (err (format "calling cdr on unknown expression ~a" e))])]
- [`(inl ,e) `(inl ,(interpret- e Γ))]
- [`(inr ,e) `(inr ,(interpret- e Γ))]
+ [`(inl ,e) `(inl ,(interpret-core e Γ))]
+ [`(inr ,e) `(inr ,(interpret-core e Γ))]
[`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
- (match (interpret- e Γ)
- [`(inl ,e) (interpret- e1 (dict-set Γ x1 e))]
- [`(inr ,e) (interpret- e2 (dict-set Γ x2 e))]
+ (match (interpret-core e Γ)
+ [`(inl ,e) (interpret-core e1 (dict-set Γ x1 e))]
+ [`(inr ,e) (interpret-core e2 (dict-set Γ x2 e))]
[e (err (format "calling case on unknown expression ~a" e))])]
['nil 'nil]
[`(nil? ,e)
- (match (interpret- e Γ)
+ (match (interpret-core e Γ)
['nil '#t]
[`(cons ,e1 ,e2) '#f]
[e (err (format "calling isnil on unknown expression ~a" e))])]
[`(cons ,e1 ,e2)
- `(cons ,(interpret- e1 Γ) ,(interpret- e2 Γ))]
+ `(cons ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))]
[`(head ,e)
- (match (interpret- e Γ)
- [`(cons ,e1 ,e2) (interpret- e1 Γ)]
+ (match (interpret-core e Γ)
+ [`(cons ,e1 ,e2) (interpret-core e1 Γ)]
[e (err (format "calling head on unknown expression ~a" e))])]
[`(tail ,e)
- (match (interpret- e Γ)
- [`(cons ,e1 ,e2) (interpret- e2 Γ)]
+ (match (interpret-core e Γ)
+ [`(cons ,e1 ,e2) (interpret-core e2 Γ)]
[e (err (format "calling tail on unknown expression ~a" e))])]
[`(λ ,x ,e) `(λ ,x ,e ,Γ)]
[`(,e1 ,e2)
- (match (interpret- e1 Γ)
+ (match (interpret-core e1 Γ)
[`(λ ,x ,e ,env)
- (interpret- e (dict-set env x (interpret- e2 Γ)))]
+ (interpret-core e (dict-set env x (interpret-core e2 Γ)))]
[e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
[e (err (format "interpreting an unknown expression ~a" e))]))
;; (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
- (check- (desugar expr) with Γ))
-(define (check- expr with Γ)
+(define (check expr with)
+ (check-core (desugar expr) with #hash()))
+(define (check-core expr with Γ)
(let ([with (expand with Γ)])
(match* (expr with)
[('sole 'Unit) #t]
@@ -83,67 +83,67 @@
[(n 'Nat) #:when (natural? n) #t]
[(b 'Bool) #:when (boolean? b) #t]
[(e `(,t1 ⊕ ,t2))
- (or (equiv? (infer- e Γ) with) (check- e t1 Γ) (check- e t2 Γ))]
+ (or (equiv? (infer-core e Γ) with) (check-core e t1 Γ) (check-core e t2 Γ))]
[(x _) #:when (dict-has-key? Γ x)
(equiv? (dict-ref Γ x) with Γ Γ)]
[(`(type ,t1 ,t2 ,in) with)
- (check- in with (dict-set Γ t1 t2))]
+ (check-core in with (dict-set Γ t1 t2))]
[(`(inc ,e) 'Nat)
- (check- e 'Nat Γ)]
+ (check-core e 'Nat Γ)]
[(`(if ,c ,e1 ,e2) with)
- (and (check- c 'Bool Γ)
- (check- e1 with Γ) (check e2 with Γ))]
+ (and (check-core c 'Bool Γ)
+ (check-core e1 with Γ) (check e2 with Γ))]
[(`(pair ,e1 ,e2) `(,t1 × ,t2))
- (and (check- e1 t1 Γ) (check- e2 t2 Γ))]
+ (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
[(`(car ,e) with)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 × ,t2) (equiv? t1 with Γ Γ)]
[t #f])]
[(`(cdr ,e) with)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 × ,t2) (equiv? t2 with Γ Γ)]
[t #f])]
[(`(inl ,e) with)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 ⊕ ,t2) (equiv? t1 with Γ Γ)]
[t #f])]
[(`(inr ,e) with)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 ⊕ ,t2) (equiv? t2 with Γ Γ)]
[t #f])]
[(`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) with)
- (equiv? with (infer- `(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) Γ) Γ Γ)]
+ (equiv? with (infer-core `(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) Γ) Γ Γ)]
[(`(,e : ,t) with)
- (and (equiv? t with Γ Γ) (check- e t Γ))]
+ (and (equiv? t with Γ Γ) (check-core e t Γ))]
[('nil `(List ,t)) #t]
[(`(cons ,f1 ,f2) `(List ,t))
- (and (check- f1 t Γ) (check- f2 `(List ,t) Γ))]
+ (and (check-core f1 t Γ) (check-core f2 `(List ,t) Γ))]
[(`(head ,e) with)
- (match (infer- e)
+ (match (infer-core e)
[`(List ,t) (equiv? t with Γ Γ)]
[t #f])]
[(`(tail ,e) with)
- (equiv? (infer- e Γ) with Γ Γ)]
+ (equiv? (infer-core e Γ) with Γ Γ)]
[(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
- (and (equiv? t t1 Γ Γ) (check- e t2 (dict-set Γ x t1)))]
+ (and (equiv? t t1 Γ Γ) (check-core e t2 (dict-set Γ x t1)))]
[(`(,e1 ,e2) t)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (and (equiv? t2 t Γ Γ) (equiv? t1 (infer- e2 Γ) Γ Γ))]
+ (and (equiv? t2 t Γ Γ) (equiv? t1 (infer-core e2 Γ) Γ Γ))]
[t #f])]
[(e t) #f])))
;; (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
- (infer- (desugar expr) Γ))
-(define (infer- expr Γ)
+(define (infer expr)
+ (infer-core (desugar expr) #hash()))
+(define (infer-core expr Γ)
(match expr
['sole 'Unit]
[s #:when (string? s) 'Str]
@@ -156,66 +156,66 @@
(infer in (dict-set Γ t1 t2))]
[`(inc ,e)
- (if (check- e 'Nat Γ) 'Nat
- (err (format "calling inc on incorrect type ~a" (infer- e Γ))))]
+ (if (check-core e 'Nat Γ) 'Nat
+ (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))]
[`(if ,c ,e1 ,e2)
- (if (check- c 'Bool Γ)
- (let ([t (infer- e1 Γ)])
- (if (check- e2 t Γ) t
+ (if (check-core c 'Bool Γ)
+ (let ([t (infer-core e1 Γ)])
+ (if (check-core 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 Γ))))]
+ t (infer-core e2 Γ)))))
+ (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))]
[`(pair ,e1 ,e2)
- `(,(infer- e1 Γ) × ,(infer- e2 Γ))]
+ `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))]
[`(car ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 × ,t2) t1]
[t (err (format "calling car on incorrect type ~a" t))])]
[`(cdr ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 × ,t2) t2]
[t (err (format "calling cdr on incorrect type ~a" t))])]
[`(inl ,e) ; annotations necessary
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)]
[t (err (format "calling inl on incorrect type ~a" t))])]
[`(inr ,e) ; annotations necessary
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t1 ⊕ ,t2) `(,t1 ⊕ ,t2)]
[t (err (format "calling inr on incorrect type ~a" t))])]
[`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,a1 ⊕ ,a2)
- (let ([b1 (infer- e1 (dict-set Γ x1 (expand a1 Γ)))] [b2 (infer- e2 (dict-set Γ x2 (expand a2 Γ)))])
+ (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))] [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))])
(if (equiv? b1 b2 Γ Γ) b1
(err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))]
[t (err (format "calling case on incorrect type ~a" t))])]
[`(,e : ,t)
- (if (check- e t Γ) t
+ (if (check-core e t Γ) t
(err (format "annotated expression ~a is not of annotated type ~a" e t)))]
['nil (err (format "unable to infer type of empty list!"))]
[`(cons ,e1 ,e2)
- (let ([t (infer- e1 Γ)])
- (if (check- e2 `(List ,t) Γ) `(List ,t)
+ (let ([t (infer-core e1 Γ)])
+ (if (check-core e2 `(List ,t) Γ) `(List ,t)
(err (format "list ~a is not of consistent type!" `(cons ,e1 ,e2)))))]
[`(head ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(List ,t) t]
[t (err (format "calling head on incorrect type ~a" t))])]
[`(tail ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(List ,t) `(List ,t)]
[t (err (format "calling tail on incorrect type ~a" t))])]
[`(λ (,x : ,t) ,e)
- `(,t → ,(infer- e (dict-set Γ x t)))]
+ `(,t → ,(infer-core e (dict-set Γ x t)))]
[`(,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (if (check- e2 t1 Γ) t2
+ (if (check-core e2 t1 Γ) t2
(err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
[t (err (format "expected → type on application body, got ~a" t))])]
diff --git a/stlc-fix.rkt b/stlc-fix.rkt
index cb6a592..e8f15e6 100644
--- a/stlc-fix.rkt
+++ b/stlc-fix.rkt
@@ -4,35 +4,35 @@
;; The Simply-Typed Lambda Calculus, with general recursion
;; (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [Γ #hash()])
- (interpret- (strip (desugar expr)) Γ))
-(define (interpret- expr Γ)
+(define (interpret expr)
+ (interpret-core (strip (desugar expr)) #hash()))
+(define (interpret-core expr Γ)
(match expr
['sole 'sole]
[n #:when (natural? n) n]
[x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
[`(fix ,e)
- (match (interpret- e Γ)
+ (match (interpret-core e Γ)
[`(λ ,x ,e ,env)
; FIXME: unsure what should be Γ and what should be env
- (interpret- e (dict-set Γ x `(fix (λ ,x ,e ,Γ))))]
+ (interpret-core e (dict-set Γ x `(fix (λ ,x ,e ,Γ))))]
[e (err (format "applying fix to unknown expression ~a" e))])]
[`(λ ,id ,body) `(λ ,id ,body ,Γ)]
[`(λ ,id ,body ,env) `(λ ,id ,body ,env)]
[`(,body ,arg)
- (match (interpret- body Γ)
+ (match (interpret-core body Γ)
[`(λ ,id ,body ,env)
- (interpret- body (dict-set env id (interpret- arg Γ)))]
+ (interpret-core body (dict-set env id (interpret-core arg Γ)))]
[e (err (format "applying arg ~a to unknown expression ~a" arg e))])]
[e (err (format "interpreting an unknown expression ~a" e))]))
;; (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
- (check- (desugar expr) with Γ))
-(define (check- expr with Γ)
+(define (check expr with)
+ (check-core (desugar expr) with #hash()))
+(define (check-core expr with Γ)
(let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)])
(match* (expr with)
[('sole 'Unit) #t]
@@ -41,22 +41,22 @@
(equal? (dict-ref Γ x) with)]
[(`(fix ,e) with)
- (check- (infer- e) `(,with → ,with) Γ)]
+ (check-core (infer-core e) `(,with → ,with) Γ)]
[(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
- (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
+ (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
[(`(,e1 ,e2) t)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
+ (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
[t #f])]
[(e t) #f])))
;; (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
- (infer- (desugar expr) Γ))
-(define (infer- expr Γ)
+(define (infer expr)
+ (infer-core (desugar expr) #hash()))
+(define (infer-core expr Γ)
(match expr
['sole 'Unit]
[n #:when (natural? n) 'Nat]
@@ -64,16 +64,16 @@
(dict-ref Γ x)]
[`(fix ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(,t → ,t) t]
[t (err (format "fix expects a term of type t → t, got ~a" t))])]
[`(λ (,x : ,t) ,e)
- `(,t → ,(infer- e (dict-set Γ x t)))]
+ `(,t → ,(infer-core e (dict-set Γ x t)))]
[`(,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (if (check- e2 t1 Γ) t2
+ (if (check-core e2 t1 Γ) t2
(err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
[t (err (format "expected → type on application body, got ~a" t))])]
diff --git a/stlc-imp.rkt b/stlc-imp.rkt
index e10b09c..541de2c 100644
--- a/stlc-imp.rkt
+++ b/stlc-imp.rkt
@@ -28,41 +28,40 @@
(require (only-in "stlc-ref.rkt" interpret))
;; (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
- (check- (desugar expr) with Γ))
-(define (check- expr with Γ)
- ; (check- expr (dict-ref Γ with) Γ)
+(define (check expr with)
+ (check-core (desugar expr) with #hash()))
+(define (check-core expr with Γ)
(match* (expr with)
[('sole 'Unit) #t]
[(n 'Nat) #:when (natural? n) #t]
[(x _) #:when (dict-has-key? Γ x)
(equal? (dict-ref Γ x) with)]
- [(`(new ,e) `(Ref ,t)) (check- e t Γ)]
- [(`(! ,e) t) (check- e `(Ref ,t) Γ)]
+ [(`(new ,e) `(Ref ,t)) (check-core e t Γ)]
+ [(`(! ,e) t) (check-core e `(Ref ,t) Γ)]
[(`(set ,e1 ,e2) 'Unit)
- (match (infer- e1 Γ)
- [`(Ref ,t) (check- e2 t Γ)]
+ (match (infer-core e1 Γ)
+ [`(Ref ,t) (check-core e2 t Γ)]
[t #f])]
[(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2))
(and
(equal? t t1)
(> k (max-level e (dict-set Γ x t1) t1 t2)) ; KNOB
- (check- e t2 (dict-set Γ x t1)))]
+ (check-core e t2 (dict-set Γ x t1)))]
[(`(,e1 ,e2) t)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,k ,t2)
(and (equal? t2 t)
- (equal? t1 (infer- e2 Γ)))]
+ (equal? t1 (infer-core e2 Γ)))]
[t #f])]
[(e t) #f]))
;; (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
- (infer- (desugar expr) Γ))
-(define (infer- expr Γ)
+(define (infer expr)
+ (infer-core (desugar expr) #hash()))
+(define (infer-core expr Γ)
; (print (format "infer: ~a" (fmt expr)))
(match expr
['sole 'Unit]
@@ -70,28 +69,28 @@
[x #:when (dict-has-key? Γ x)
(dict-ref Γ x)]
- [`(new ,e) `(Ref ,(infer- e Γ))]
+ [`(new ,e) `(Ref ,(infer-core e Γ))]
[`(! ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(Ref ,t) t]
[t (err "attempting to deref term not of Ref type!")])]
[`(set ,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(Ref ,t)
- (if (check- e2 t Γ) 'Unit
+ (if (check-core e2 t Γ) 'Unit
(err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
- e1 t e2 (infer- e2 Γ))))]
+ e1 t e2 (infer-core e2 Γ))))]
[t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
[`(λ (,x : ,t1) ,e)
- (let ([t2 (infer- e (dict-set Γ x t1))])
+ (let ([t2 (infer-core e (dict-set Γ x t1))])
(let ([k (+ 1 (max-level e (dict-set Γ x t1) t1 t2))]) ; KNOB
`(,t1 → ,k ,t2)))]
[`(,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,k ,t2)
- (if (check- e2 t1 Γ) t2
- (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))]
+ (if (check-core e2 t1 Γ) t2
+ (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))]
[t (err (format "expected → type on application body, got ~a" t))])]
[e (err (format "attempting to infer an unknown expression ~a" e))]))
diff --git a/stlc-let.rkt b/stlc-let.rkt
index edf39a7..3c4fef0 100644
--- a/stlc-let.rkt
+++ b/stlc-let.rkt
@@ -4,50 +4,50 @@
;; The Simply-Typed Lambda Calculus, with let sugar and some base types
;; (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [Γ #hash()])
- (interpret- (strip (desugar expr)) Γ))
-(define (interpret- expr Γ)
+(define (interpret expr)
+ (interpret-core (strip (desugar expr)) #hash()))
+(define (interpret-core expr Γ)
(match expr
['sole 'sole]
[n #:when (natural? n) n]
[x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
[`(λ ,x ,e) `(λ ,x ,e ,Γ)]
[`(,e1 ,e2)
- (match (interpret- e1 Γ)
- [`(λ ,x ,e1 ,env) (interpret- e1 (dict-set env x (interpret- e2 Γ)))]
- [e1 `(,e1 ,(interpret- e2 Γ))])]
+ (match (interpret-core e1 Γ)
+ [`(λ ,x ,e1 ,env) (interpret-core e1 (dict-set env x (interpret-core e2 Γ)))]
+ [e1 `(,e1 ,(interpret-core e2 Γ))])]
[e e]))
;; (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
- (check- (desugar expr) with Γ))
-(define (check- expr with Γ)
+(define (check expr with)
+ (check-core (desugar expr) with #hash()))
+(define (check-core expr with Γ)
(match* (expr with)
[('sole 'Unit) #t]
[(n 'Nat) #:when (natural? n) #t]
[(x _) #:when (dict-has-key? Γ x)
(equal? (dict-ref Γ x) with)]
[(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
- (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
+ (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
[(`(,e1 ,e2) t)
- (match (infer- e1 Γ)
- [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
+ (match (infer-core e1 Γ)
+ [`(,t1 → ,t2) (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
[t #f])]
[(e t) #f]))
;; (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
- (infer- (desugar expr) Γ))
-(define (infer- expr Γ)
+(define (infer expr)
+ (infer-core (desugar expr) #hash()))
+(define (infer-core expr Γ)
(match expr
['sole 'Unit]
[n #:when (natural? n) 'Nat]
[`(λ (,x : ,t) ,e)
- `(,t → ,(infer- e (dict-set Γ x t)))]
+ `(,t → ,(infer-core e (dict-set Γ x t)))]
[`(,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (if (check- e2 t1 Γ) t2
+ (if (check-core e2 t1 Γ) t2
(err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
[t (err (format "expected → type on application body, got ~a" t))])]
[e (err (format "attempting to infer an unknown expression ~a" e))]))
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
index d13e60d..c9c77b6 100644
--- a/stlc-pred.rkt
+++ b/stlc-pred.rkt
@@ -25,9 +25,9 @@
(require (only-in "stlc-ref.rkt" interpret))
;; (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
- (check- (desugar expr) with Γ))
-(define (check- expr with Γ)
+(define (check expr with)
+ (check-core (desugar expr) with #hash()))
+(define (check-core expr with Γ)
; (print (format "check: ~a" (fmt expr)))
(match* (expr with)
[('sole 'Unit) #t]
@@ -35,30 +35,30 @@
[(x _) #:when (dict-has-key? Γ x)
(equal? (dict-ref Γ x) with)]
- [(`(new ,e) `(Ref ,t)) (check- e t Γ)]
- [(`(! ,e) t) (check- e `(Ref ,t) Γ)]
+ [(`(new ,e) `(Ref ,t)) (check-core e t Γ)]
+ [(`(! ,e) t) (check-core e `(Ref ,t) Γ)]
[(`(set ,e1 ,e2) 'Unit)
- (match (infer- e1 Γ)
- [`(Ref ,t) (check- e2 t Γ)]
+ (match (infer-core e1 Γ)
+ [`(Ref ,t) (check-core e2 t Γ)]
[t #f])]
[(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2))
(and
(equal? t t1)
(>= k (max-level e (dict-set Γ x t1) t1 t2)) ; (KNOB)
- (check- e t2 (dict-set Γ x t1)))]
+ (check-core e t2 (dict-set Γ x t1)))]
[(`(,e1 ,e2) t)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,k ,t2)
- (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
+ (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
[t #f])]
[(e t) #f]))
;; (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
- (infer- (desugar expr) Γ))
-(define (infer- expr Γ)
+(define (infer expr)
+ (infer-core (desugar expr) #hash()))
+(define (infer-core expr Γ)
; (print (format "infer: ~a" (fmt expr)))
(match expr
['sole 'Unit]
@@ -66,28 +66,28 @@
[x #:when (dict-has-key? Γ x)
(dict-ref Γ x)]
- [`(new ,e) `(Ref ,(infer- e Γ))]
+ [`(new ,e) `(Ref ,(infer-core e Γ))]
[`(! ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(Ref ,t) t]
[t (err "attempting to deref term not of Ref type!")])]
[`(set ,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(Ref ,t)
- (if (check- e2 t Γ) 'Unit
+ (if (check-core e2 t Γ) 'Unit
(err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
- e1 t e2 (infer- e2 Γ))))]
+ e1 t e2 (infer-core e2 Γ))))]
[t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
[`(λ (,x : ,t1) ,e)
- (let ([t2 (infer- e (dict-set Γ x t1))])
+ (let ([t2 (infer-core e (dict-set Γ x t1))])
(let ([k (max-level e (dict-set Γ x t1) t1 t2)]) ; (KNOB)
`(,t1 → ,k ,t2)))]
[`(,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,k ,t2)
- (if (check- e2 t1 Γ) t2
- (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer- e2 Γ))))]
+ (if (check-core e2 t1 Γ) t2
+ (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))]
[t (err (format "expected → type on application body, got ~a" t))])]
[e (err (format "attempting to infer an unknown expression ~a" e))]))
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index 3d099c2..8819116 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -13,33 +13,33 @@
; Γ ⊢ unfold [μx.t] e: [x ↦ μx.t] t
;; (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [Γ #hash()])
- (interpret- (strip (desugar expr)) Γ))
-(define (interpret- expr Γ)
+(define (interpret expr)
+ (interpret-core (strip (desugar expr)) #hash()))
+(define (interpret-core expr Γ)
(match expr
['sole 'sole]
[n #:when (natural? n) n]
[x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
- [`(fold ,e) `(fold ,(interpret- e Γ))]
+ [`(fold ,e) `(fold ,(interpret-core e Γ))]
[`(unfold ,e)
- (match (interpret- e Γ)
+ (match (interpret-core e Γ)
[`(fold ,e) e]
[e `(unfold e)])]
[`(λ ,x ,e) `(λ ,x ,e ,Γ)]
[`(,e1 ,e2)
- (match (interpret- e1 Γ)
+ (match (interpret-core e1 Γ)
[`(λ ,x ,e ,env)
- (interpret- e (dict-set env x (interpret- e2 Γ)))]
+ (interpret-core e (dict-set env x (interpret-core e2 Γ)))]
[e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
[e (err (format "interpreting an unknown expression ~a" e))]))
;; (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
- (check- (desugar expr) with Γ))
-(define (check- expr with Γ)
+(define (check expr with)
+ (check-core (desugar expr) with #hash()))
+(define (check-core expr with Γ)
; (print (format "check: ~a" (fmt expr)))
(match* (expr with)
[('sole 'Unit) #t]
@@ -48,26 +48,26 @@
(equal? (dict-ref Γ x) with)]
[(`(fold (μ ,x ,t) ,e) `(μ ,x ,t))
- (check- e t (dict-set Γ x `(μ ,x ,t)))]
+ (check-core e t (dict-set Γ x `(μ ,x ,t)))]
[(`(unfold (μ ,x ,t) ,e) with)
- (and (check- e `(μ ,x ,t) Γ)
+ (and (check-core e `(μ ,x ,t) Γ)
(equiv? with t #hash() #hash((x . `(μ ,x ,t)))))]
[(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
- (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
+ (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
[(`(,e1 ,e2) t)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
+ (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
[t #f])]
[(e t) #f]))
;; (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
- (infer- (desugar expr) Γ))
-(define (infer- expr Γ)
+(define (infer expr)
+ (infer-core (desugar expr) #hash()))
+(define (infer-core expr Γ)
; (print (format "infer: ~a" (fmt expr)))
(match expr
['sole 'Unit]
@@ -77,21 +77,21 @@
(dict-ref Γ x)]
[`(fold (μ ,x ,t) ,e)
- (if (check- e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t)
+ (if (check-core e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t)
(err (format "expected ~a to be of type ~a, got ~a"
e t (infer e (dict-set Γ x `(μ ,x ,t))))))]
[`(unfold (μ ,x ,t) ,e)
- (if (check- e `(μ ,x ,t)) (replace t x `(μ ,x ,t))
+ (if (check-core e `(μ ,x ,t)) (replace t x `(μ ,x ,t))
(err (format "expected ~a to be of type ~a, got ~a"
- e `(μ ,x ,t) (infer- e Γ))))]
+ e `(μ ,x ,t) (infer-core e Γ))))]
[`(λ (,x : ,t) ,e)
- `(,t → ,(infer- e (dict-set Γ x t)))]
+ `(,t → ,(infer-core e (dict-set Γ x t)))]
[`(,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (if (check- e2 t1 Γ) t2
+ (if (check-core e2 t1 Γ) t2
(err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
[t (err (format "expected → type on application body, got ~a" t))])]
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index b025309..f054d4e 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -4,9 +4,9 @@
;; The Simply-Typed Lambda Calculus with references
;; (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value
-(define (interpret expr [Γ #hash()] [Σ (make-hash)])
- (interpret- (strip (desugar expr)) Γ Σ))
-(define (interpret- expr Γ Σ)
+(define (interpret expr)
+ (interpret-core (strip (desugar expr)) #hash() (make-hash)))
+(define (interpret-core expr Γ Σ)
; (print (format "interpret: ~a" (fmt expr)))
(match expr
['sole 'sole]
@@ -18,30 +18,30 @@
(let ([r (gensym)])
(dict-set! Σ r e) r)]
[`(! ,e)
- (let ([r (interpret- e Γ Σ)])
+ (let ([r (interpret-core e Γ Σ)])
(if (dict-has-key? Σ r)
- (interpret- (dict-ref Σ r) Γ Σ)
+ (interpret-core (dict-ref Σ r) Γ Σ)
(err (format "attempting to deref unknown reference ~a" r))))]
[`(set ,e1 ,e2)
- (let ([r (interpret- e1 Γ Σ)])
- (if (dict-has-key? Σ r) (dict-set! Σ r (interpret- e2 Γ Σ))
+ (let ([r (interpret-core e1 Γ Σ)])
+ (if (dict-has-key? Σ r) (dict-set! Σ r (interpret-core e2 Γ Σ))
(err (format "attempting to update unknown reference ~a" r))))
'sole]
[`(λ ,x ,e) `(λ ,x ,e ,Γ)]
[`(λ ,x ,e ,env) `(λ ,x ,e ,env)] ; ???
[`(,e1 ,e2)
- (match (interpret- e1 Γ Σ)
+ (match (interpret-core e1 Γ Σ)
[`(λ ,x ,e1 ,env)
- (interpret- e1 (dict-set env x (interpret- e2 Γ Σ)) Σ)]
+ (interpret-core e1 (dict-set env x (interpret-core e2 Γ Σ)) Σ)]
[e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]
[e (err (format "attempting to interpret unknown expression ~a" e))]))
;; (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
- (check- (desugar expr) with Γ))
-(define (check- expr with Γ)
+(define (check expr with)
+ (check-core (desugar expr) with #hash()))
+(define (check-core expr with Γ)
; (print (format "check: ~a" (fmt expr)))
(match* (expr with)
[('sole 'Unit) #t]
@@ -49,27 +49,27 @@
[(x _) #:when (dict-has-key? Γ x)
(equal? (dict-ref Γ x) with)]
- [(`(new ,e) `(Ref ,t)) (check- e t Γ)]
- [(`(! ,e) t) (check- e `(Ref ,t) Γ)]
+ [(`(new ,e) `(Ref ,t)) (check-core e t Γ)]
+ [(`(! ,e) t) (check-core e `(Ref ,t) Γ)]
[(`(set ,e1 ,e2) 'Unit)
- (match (infer- e1 Γ)
- [`(Ref ,t) (check- e2 t Γ)]
+ (match (infer-core e1 Γ)
+ [`(Ref ,t) (check-core e2 t Γ)]
[t #f])]
[(`(λ (,x : ,t) ,e) `(,t1 → ,t2))
- (and (equal? t t1) (check- e t2 (dict-set Γ x t1)))]
+ (and (equal? t t1) (check-core e t2 (dict-set Γ x t1)))]
[(`(,e1 ,e2) t)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (and (equal? t2 t) (equal? t1 (infer- e2 Γ)))]
+ (and (equal? t2 t) (equal? t1 (infer-core e2 Γ)))]
[t #f])]
[(e t) #f]))
;; (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
- (infer- (desugar expr) Γ))
-(define (infer- expr Γ)
+(define (infer expr)
+ (infer-core (desugar expr) #hash()))
+(define (infer-core expr Γ)
; (print (format "infer: ~a" (fmt expr)))
(match expr
['sole 'Unit]
@@ -77,25 +77,25 @@
[x #:when (dict-has-key? Γ x)
(dict-ref Γ x)]
- [`(new ,e) `(Ref ,(infer- e Γ))]
+ [`(new ,e) `(Ref ,(infer-core e Γ))]
[`(! ,e)
- (match (infer- e Γ)
+ (match (infer-core e Γ)
[`(Ref ,t) t]
[t (err "attempting to deref term not of Ref type!")])]
[`(set ,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(Ref ,t)
- (if (check- e2 t Γ) 'Unit
+ (if (check-core e2 t Γ) 'Unit
(err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
- e1 t e2 (infer- e2 Γ))))]
+ e1 t e2 (infer-core e2 Γ))))]
[t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
[`(λ (,x : ,t) ,e)
- `(,t → ,(infer- e (dict-set Γ x t)))]
+ `(,t → ,(infer-core e (dict-set Γ x t)))]
[`(,e1 ,e2)
- (match (infer- e1 Γ)
+ (match (infer-core e1 Γ)
[`(,t1 → ,t2)
- (if (check- e2 t1 Γ) t2
+ (if (check-core e2 t1 Γ) t2
(err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
[t (err (format "expected → type on application body, got ~a" t))])]
diff --git a/stlc.rkt b/stlc.rkt
index 584f150..803cc8c 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -4,16 +4,16 @@
;; The Simply-Typed Lambda Calculus
;; (interpret Expr Table[Sym, Expr]): Value
-(define (interpret expr [Γ #hash()])
- (interpret- (strip expr) Γ))
-(define (interpret- expr Γ)
+(define (interpret expr)
+ (interpret-core (strip expr) #hash()))
+(define (interpret-core expr Γ)
(match expr
[x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
[`(λ ,x ,e) `(λ ,x ,e ,Γ)]
[`(,e1 ,e2)
- (match (interpret- e1 Γ)
- [`(λ ,x ,e ,env) (interpret- e (dict-set env x (interpret- e2 Γ)))]
- [e `(,e ,(interpret- e2 Γ))])]
+ (match (interpret-core e1 Γ)
+ [`(λ ,x ,e ,env) (interpret-core e (dict-set env x (interpret-core e2 Γ)))]
+ [e `(,e ,(interpret-core e2 Γ))])]
[e e]))
;; (check Expr Type Table[Sym, Type]): Bool