diff options
| -rw-r--r-- | stlc-dll.rkt | 157 |
1 files changed, 149 insertions, 8 deletions
diff --git a/stlc-dll.rkt b/stlc-dll.rkt index 92fd520..2c981e1 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -90,10 +90,10 @@ [(e `(,t1 ⊕ ,t2)) (or (equiv? (infer- e Γ) with) (check- e t1 Γ) (check- e t2 Γ))] [(x _) #:when (dict-has-key? Γ x) - (equiv? (dict-ref Γ x) with Γ Γ)] + (equiv? (expand (dict-ref Γ x) Γ) with Γ Γ)] [(`(type ,t1 ,t2 ,in) with) - (check- in with (dict-set Γ t1 t2))] + (check- in with (dict-set Γ t1 (expand t2 Γ)))] [(`(inc ,e) 'Nat) (check- e 'Nat Γ)] @@ -138,11 +138,18 @@ (and (check- e `(μ ,x ,t) Γ) (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))] + [(`(fold ,e) `(μ ,x ,t)) + (check- e t (dict-set Γ x `(μ ,x ,t)))] + [(`(unfold ,e) with) ; FIXME: GROSS + (match* ((infer- e Γ) with) + [(`(μ ,_ ,t) `(μ ,_ ,t)) #T] + [(t u) #f])] + [(`(λ (,x : ,t) ,e) `(,t1 → ,k ,t2)) (and (equiv? t t1 Γ Γ) - (> k (max-level e t1 t2 (dict-set Γ x t1))) ; KNOB - (check- e t2 (dict-set Γ x t1)))] + (> k (max-level e t1 t2 (dict-set Γ x (expand t1 Γ)))) ; KNOB + (check- e t2 (dict-set Γ x (expand t1 Γ))))] [(`(,e1 ,e2) t) (match (infer- e1 Γ) [`(,t1 → ,k ,t2) @@ -165,7 +172,7 @@ (dict-ref Γ x)] [`(type ,t1 ,t2 ,in) - (infer in (dict-set Γ t1 t2))] + (infer in (dict-set Γ t1 (expand t2 Γ)))] [`(inc ,e) (if (check- e 'Nat Γ) 'Nat @@ -230,9 +237,18 @@ (err (format "expected ~a to be of type ~a, got ~a" e `(μ ,x ,t) (infer- e Γ))))] + [`(fold ,e) + (match (infer- e Γ) + [`(μ ,x ,t) `(μ ,x ,t)] + [t (err (format "expected ~a to be recursive, got ~a" e t))])] + [`(unfold ,e) + (match (infer- e Γ) + [`(μ ,x ,t) (replace t x `(μ ,x ,t))] + [t (err (format "expected ~a to be recursive, got ~a" e t))])] + [`(λ (,x : ,t1) ,e) - (let ([t2 (infer- e (dict-set Γ x t1))]) - (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))]) ; KNOB + (let ([t2 (infer- e (dict-set Γ x (expand t1 Γ)))]) + (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x (expand t1 Γ))))]) ; KNOB `(,t1 → ,k ,t2)))] [`(,e1 ,e2) (match (infer- e1 Γ) @@ -301,7 +317,7 @@ [`(! ,e) (level-body e Γ)] [`(set ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))] [`(if ,c ,e1 ,e2) (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))] - [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? + [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x (expand t Γ)))] ; todo: should be 0? [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))])) @@ -335,3 +351,128 @@ (check-eq? (interpret '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 2) (check-eq? (infer '(type Natural Nat ((λ (x : Natural) (inc x)) 1))) 'Nat) (check-true (check '(type Natural Nat ((λ (x : Natural) (inc x)) 1)) 'Nat)) + +(check-equal? + (infer + '(case (inr (sole : (Nat ⊕ Unit))) + (x ⇒ 0) (x ⇒ 1))) 'Nat) + +(check-true + (check + '(case (inr (sole : (Nat ⊕ Unit))) + (x ⇒ x) + (x ⇒ 1)) 'Nat)) + +(check-equal? + (interpret + '((λ (p1 : DoublyLinkedList) (car (unfold p1))) + (fold + (pair 413 + (pair (inl (sole : (Unit ⊕ DoublyLinkedList))) + (inl (sole : (Unit ⊕ DoublyLinkedList)))))))) + 413) + +(check-equal? + (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (let get + (λ x (car (unfold x))) + (let my_list + (fold + (pair 413 + (pair (inl sole) + (inl sole)))) + (get my_list))))) + 413) + + +(check-equal? + (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (let prev + (λ x + (case (car (cdr (unfold x))) + (x ⇒ (inl (! x))) + (x ⇒ (inr sole)))) + (let my_list + (fold + (pair 413 + (pair (inl (new sole)) + (inl (new sole))))) + (prev my_list))))) + '(inl sole)) + + +(check-equal? + (interpret '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (let next + (λ x + (case (cdr (cdr (unfold x))) + (x ⇒ (inl (! x))) + (x ⇒ (inr sole)))) + (let my_list + (fold + (pair 413 + (pair (inr (new sole)) + (inr (new sole))))) + (next my_list))))) + '(inr sole)) + +(check-true + (check + '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + sole) + '(DoublyLinkedList ⊕ Unit))) + +(check-equal? + (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (λ (p3 : DoublyLinkedList) (case (cdr (cdr (unfold p3))) (x ⇒ (inl ((! x) : (DoublyLinkedList ⊕ Unit)))) (x ⇒ (inr (sole : (DoublyLinkedList ⊕ Unit)))))))) + '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + +(check-true + (check + '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (λ (p3 : DoublyLinkedList) (case (cdr (cdr (unfold p3))) (x ⇒ (inl ((! x) : (DoublyLinkedList ⊕ Unit)))) (x ⇒ (inr (sole : (DoublyLinkedList ⊕ Unit))))))) + '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)))) + +(check-equal? + (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (let (get : (DoublyLinkedList → 1 Nat)) + (λ (p1 : DoublyLinkedList) (car (unfold p1))) + (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ (p2 : DoublyLinkedList) + (case (car (cdr (unfold p2))) + (x ⇒ (inl ((! x) : (DoublyLinkedList ⊕ Unit)))) + (x ⇒ (inr (sole : (DoublyLinkedList ⊕ Unit)))))) + (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ (p3 : DoublyLinkedList) + (case (cdr (cdr (unfold p3))) + (x ⇒ (inl ((! x) : (DoublyLinkedList ⊕ Unit)))) + (x ⇒ (inr (sole : (DoublyLinkedList ⊕ Unit)))))) + (let (my_list : DoublyLinkedList) + (fold + (pair 413 + (pair (inr (sole : ((Ref DoublyLinkedList) ⊕ Unit))) + (inr (sole : ((Ref DoublyLinkedList) ⊕ Unit)))))) + (prev my_list))))))) + '(DoublyLinkedList ⊕ Unit)) + +(check-true + (check '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (let (get : (DoublyLinkedList → 1 Nat)) + (λ (p1 : DoublyLinkedList) (car (unfold p1))) + (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ (p2 : DoublyLinkedList) + (case (car (cdr (unfold p2))) + (x ⇒ (inl ((! x) : (DoublyLinkedList ⊕ Unit)))) + (x ⇒ (inr (sole : (DoublyLinkedList ⊕ Unit)))))) + (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ (p3 : DoublyLinkedList) + (case (cdr (cdr (unfold p3))) + (x ⇒ (inl ((! x) : (DoublyLinkedList ⊕ Unit)))) + (x ⇒ (inr (sole : (DoublyLinkedList ⊕ Unit)))))) + (let (my_list : DoublyLinkedList) + (fold + (pair 413 + (pair (inr (sole : ((Ref DoublyLinkedList) ⊕ Unit))) + (inr (sole : ((Ref DoublyLinkedList) ⊕ Unit)))))) + (prev my_list)))))) + '(DoublyLinkedList ⊕ Unit))) |