backport interpret-/infer-/check- renaming and remove implicit params

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