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

1 files changed, 22 insertions, 23 deletions

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))]))