stlc-dll: rename interpret-, remove optional parameters

2 files changed, 40 insertions, 32 deletions

diff --git a/lib.rkt b/lib.rkt
index 29d3b83..e44eb6a 100644
--- a/lib.rkt
+++ b/lib.rkt
@@ -95,7 +95,7 @@
     [`(let (,id : (,a → ,b)) (λ ,x ,e) ,in)
       (desugar `((λ (,id : (,a → ,b)) ,in) (λ (,x : ,a) ,e)))]
     [`(let ,x (,e : ,t) ,in)
-      (desugar `((λ (,x : ,t) ,in) ,e))]
+      (desugar `((λ (,x : ,t) ,in) (,e : ,t)))]
     [`(let ,x ,e ,in)
       (desugar `((λ ,x ,in) ,e))]
     [`(let ,x ,e)
diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 98b6f85..5579a7a 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -11,9 +11,9 @@
 ;; Σ: a Table[Symbol, Expr] representing the heap:
 ;;   the current references on the heap generated by (gensym). mutable
 ;;      (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value ⊕ Err
-(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]
@@ -23,59 +23,59 @@
     [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))])]
 
     [`(new ,e)
       (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]
 
-    [`(fold ,e) `(fold ,(interpret- e Γ Σ))]
+    [`(fold ,e) `(fold ,(interpret-core e Γ Σ))]
     [`(unfold ,e)
-      (match (interpret- e Γ Σ)
+      (match (interpret-core e Γ Σ)
         [`(fold ,e) e]
         [e (err (format "attempting to unfold unknown expression ~a" e))])]
 
     [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
     [`(,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))]))
@@ -85,8 +85,8 @@
 ;; Γ: a Table[Symbol, Expr ⊕ Type] representing the context:
 ;;   the current bindings in scope introduced by λx.[] and μx.[] and τx.[]
 ;;      (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with [Γ #hash()])
-  (check-core (desugar expr) with Γ))
+(define (check expr with)
+  (check-core (desugar expr) with #hash()))
 (define (check-core expr with Γ)
   ; (print (format "check: ~a with ~a" (fmt expr) with))
   (match expr
@@ -205,8 +205,8 @@
 
 ;; Infers a type from a given expression, if possible, or errors out.
 ;;      (infer Expr Table[Sym, Type]): Type
-(define (infer expr [Γ #hash()])
-  (infer-core (desugar expr) Γ))
+(define (infer expr)
+  (infer-core (desugar expr) #hash()))
 (define (infer-core expr Γ)
   ; (print (format "infer: ~a" (fmt expr)))
   (match expr
@@ -304,7 +304,7 @@
 
     [e (err (format "attempting to infer an unknown expression ~a" e))]))
 
-;; Expands a type alias to a matchable outside structure, for literal matching.
+;; Expands a type alias into weak-head normal form, for literal matching.
 ;;      (expand Type Table[Id, Expr ⊕ Type]): Type
 (define (expand t Γ)
   (if (dict-has-key? Γ t) (expand (dict-ref Γ t) Γ) t))
@@ -568,9 +568,6 @@
    (next my_list))))
   '(inr sole))
 
-; issue: we only need annotations on the first case here because stlc-dll will try and return (μ Self (Nat × (Ref Self) × (Ref Self))) instead. this is perhaps bad, there should be some way to recover the original bindings... maybe??
-; todo: check should be able to place annotations on the right place idk
-; ok that is done. still original issue tho
 (check-equal?
   (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
     (λ (self : DoublyLinkedList)
@@ -580,6 +577,17 @@
   '(DoublyLinkedList → 1 DoublyLinkedList))
 
 (check-true
+  (equiv?
+    (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
+      (λ (self : DoublyLinkedList)
+         (case (unfold self)
+          (some ⇒ (! (cdr (cdr some))))
+          (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
+  '(DoublyLinkedList → 1 DoublyLinkedList)
+    #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
+    #hash((DoublyLinkedList . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
+
+(check-true
   (check '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
     (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit)))
       (λ self