aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--lib.rkt2
-rw-r--r--stlc-dll.rkt70
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