diff options
| -rw-r--r-- | stlc-dll.rkt | 462 | ||||
| -rw-r--r-- | stlc-ext.rkt | 66 |
2 files changed, 268 insertions, 260 deletions
diff --git a/stlc-dll.rkt b/stlc-dll.rkt index 81bab7b..42ed82e 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -131,44 +131,33 @@ [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,k ,t2) - (and (equiv? t t1 Γ Γ) (check-core e t2 (dict-set Γ x t)) + (and (equiv-type t t1 Γ) (check-core e t2 (dict-set Γ x t)) (> k (level-body e (dict-set Γ x t1))))] ; KNOB [`(,t1 → ,t2) (err (format "missing level annotation on function type"))] [_ #f])] - [_ (equiv? (infer-core expr Γ) with Γ Γ)])) + [_ (equiv-type (infer-core expr Γ) with Γ)])) -;; Checks if two expressions or types are equivalent, up to α-conversion, -;; given their respective contexts -;; (equiv? -;; e1, e2: Expr ⊕ Type -;; Γ1, Γ2: Table[Sym (Expr ⊕ Type)] -;; ): Bool -(define (equiv? e1 e2 Γ1 Γ2) +;; Checks if two types are equivalent up to α-conversion in context +;; (equiv-type Type Type Table[Sym Type]): Bool +(define (equiv-type e1 e2 Γ) + (equiv-type-core e1 e2 Γ Γ)) +(define (equiv-type-core e1 e2 Γ1 Γ2) (match* (e1 e2) ; bound identifiers: if a key exists in the context, look it up [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)] + (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)] + (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)] ; recursive types: self-referential names can be arbitrary [(`(μ ,x1 ,t1) `(μ ,x2 ,t2)) (let ([name gensym]) - (equiv? t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] - - ; function expressions: parameter names can be arbitrary - [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) - (let ([name gensym]) - (and (equiv? t1 t2 Γ1 Γ2) - (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))))] - [(`(λ ,x1 ,e1) `(λ ,x2 ,e2)) - (let ([name gensym]) - (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + (equiv-type-core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] ; check for syntactic equivalence on remaining forms [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv? x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] [(v1 v2) (equal? v1 v2)])) ;; Infers a type from a given expression, if possible, or errors out. @@ -221,7 +210,7 @@ [`(,a1 ⊕ ,a2) (let ([b1 (infer-core e1 (dict-set Γ x1 a1))] [b2 (infer-core e2 (dict-set Γ x2 a2))]) - (if (equiv? b1 b2 Γ Γ) b1 + (if (equiv-type b1 b2 Γ) b1 (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] [t (err (format "calling case on incorrect type ~a" t))])] @@ -260,43 +249,40 @@ [e (err (format "attempting to infer an unknown expression ~a" e))])) -;; 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)) - ;; Checks if a type is well-formed in the current context. +;; BIG ASSUMPTION: types in the current context are well-formed ;; (well-formed Type Context): Bool (define (well-formed t Γ) (match t - [x #:when (dict-has-key? Γ x) (well-formed (dict-ref Γ x) Γ)] + [x #:when (dict-has-key? Γ x) #t] [(or 'Unit 'Nat 'Bool) #t] [`(Ref ,t) (well-formed t Γ)] - [`(μ ,x ,t) (well-formed t (dict-set Γ x 'Unit))] ; todo: HACK + [`(μ ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))] + [`(type ,x ,t) (well-formed t (dict-set Γ x `(μ ,x ,t)))] [(or `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (well-formed t1 Γ) (well-formed t2 Γ))] [_ #f])) ;; Checks if a type is well-kinded with respect to a level in the current context +;; BIG ASSUMPTION: types in the current context are well-formed ;; (well-kinded Type Level Context): Bool (define (well-kinded t l Γ) (match t - [x #:when (dict-has-key? Γ x) - (well-kinded (dict-ref Γ x) l Γ)] + [x #:when (dict-has-key? Γ x) #t] [(or 'Unit 'Nat 'Bool) (>= l 0)] [`(Ref ,t) (if (zero? l) (well-kinded t l Γ) (well-kinded t (- l 1) Γ))] [`(μ ,x ,t) - (well-kinded t l (dict-set Γ x 'Unit))] ; FIXME - [`(,t1 → ,k ,t2) - (and (>= l k) (well-kinded t1 k Γ) (well-kinded t2 k Γ))] + (well-kinded t l (dict-set Γ x `(μ ,x ,t)))] [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (well-kinded t1 l Γ) (well-kinded t2 l Γ))] + [`(,t1 → ,k ,t2) + (and (>= l k) (well-kinded t1 k Γ) (well-kinded t2 k Γ))] [_ #f])) +;; Infers the level of a (well-formed) type. ;; (level-type Type): Natural (define (level-type t Γ) (match t @@ -305,7 +291,7 @@ [(or 'Unit 'Nat) 0] [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (max (level-type t1 Γ) (level-type t2 Γ))] - [`(μ ,x ,t) ; fixme: correct, ish, but VERY WEIRD + [`(μ ,x ,t) ; note: correct but VERY WEIRD (level-type t Γ)] [`(,t1 → ,k ,t2) (if (and (>= k (level-type t1 Γ)) (>= k (level-type t2 Γ))) k ; KNOB @@ -316,7 +302,7 @@ [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ ;; Infers the level of a (well-formed) expression. -;; (level-body Expr Table[Sym, Type]): Natural +;; (level-body Expr Context): Natural (define (level-body e Γ) (match e ['sole 0] @@ -334,228 +320,224 @@ [x #:when (symbol? x) 0])) ; local variables, not in Γ (require rackunit) - -(check-exn - exn:fail? - (λ () (infer ' - (let (id : (Nat → 1 Nat)) (λ x x) +(define-test-suite let-set-inc-case + (check-exn + exn:fail? + (λ () (infer ' + (let (id : (Nat → 1 Nat)) (λ x x) (let (r : (Ref (Nat → 1 Nat))) (new id) - (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) - (set r f - (f 0)))))))) + (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) + (set r f + (f 0)))))))) -(check-eq? - (infer ' - (let (id : (Nat → 1 Nat)) (λ x x) + (check-eq? + (infer ' + (let (id : (Nat → 1 Nat)) (λ x x) (let (r : (Ref (Nat → 1 Nat))) (new id) - (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) - (f 0))))) - 'Nat) - -(check-eq? - (check ' - (let (id : (Nat → 1 Nat)) (λ x x) - (let (r : (Ref (Nat → 1 Nat))) (new id) - (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) - (f 0)))) + (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) + (f 0))))) 'Nat) - #t) - -(check-eq? (interpret '(if #t 1 0)) 1) -(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 (car (unfold p1))) - (fold - (pair 413 - (pair (inl sole) - (inl sole)))))) - 413) + (check-eq? + (check ' + (let (id : (Nat → 1 Nat)) (λ x x) + (let (r : (Ref (Nat → 1 Nat))) (new id) + (let (f : (Nat → 3 Nat)) (λ x ((! r) x)) + (f 0)))) + 'Nat) + #t) + + (check-eq? (interpret '(if #t 1 0)) 1) + (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 (car (unfold p1))) + (fold + (pair 413 + (pair (inl sole) + (inl sole)))))) + 413)) ;; initial implementation of doubly linked lists: ;; (type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit))))) - -(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 - (equiv? - (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) - (λ (self : DoublyLinkedList) - (case (cdr (cdr (unfold self))) - (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit))) - (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit))))))) - '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)) - #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))))) - #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))))))) - -(check-true - (check - '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) - (λ (self : DoublyLinkedList) - (case (cdr (cdr (unfold self))) - (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)) - (λ self (car (unfold self))) - (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) - (λ self - (case (car (cdr (unfold self))) - (x ⇒ (inl (! x))) - (x ⇒ (inr sole)))) - (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) - (λ self - (case (cdr (cdr (unfold self))) - (x ⇒ (inl (! x))) - (x ⇒ (inr sole)))) - (let (my_list : DoublyLinkedList) +(define-test-suite dll-no-empty-lists + (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 ((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)) - (λ self (car (unfold self))) - (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) - (λ self - (case (car (cdr (unfold self))) + (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 (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) - (λ self - (case (cdr (cdr (unfold self))) + (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 : DoublyLinkedList) + (let my_list (fold (pair 413 - (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)) - ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))))) - (prev my_list)))))) - '(DoublyLinkedList ⊕ Unit))) - + (pair (inr (new sole)) + (inr (new sole))))) + (next my_list))))) + '(inr sole)) + + (check-true + (equiv-type + (infer '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (λ (self : DoublyLinkedList) + (case (cdr (cdr (unfold self))) + (x ⇒ ((inl (! x)) : (DoublyLinkedList ⊕ Unit))) + (x ⇒ ((inr sole) : (DoublyLinkedList ⊕ Unit))))))) + '(DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit)) + #hash((DoublyLinkedList . (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))))))) + + (check-true + (check + '(type DoublyLinkedList (μ Self (Nat × (((Ref Self) ⊕ Unit) × ((Ref Self) ⊕ Unit)))) + (λ (self : DoublyLinkedList) + (case (cdr (cdr (unfold self))) + (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)) + (λ self (car (unfold self))) + (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ self + (case (car (cdr (unfold self))) + (x ⇒ (inl (! x))) + (x ⇒ (inr sole)))) + (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ self + (case (cdr (cdr (unfold self))) + (x ⇒ (inl (! x))) + (x ⇒ (inr sole)))) + (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)) + (λ self (car (unfold self))) + (let (prev : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ self + (case (car (cdr (unfold self))) + (x ⇒ (inl (! x))) + (x ⇒ (inr sole)))) + (let (next : (DoublyLinkedList → 1 (DoublyLinkedList ⊕ Unit))) + (λ self + (case (cdr (cdr (unfold self))) + (x ⇒ (inl (! x))) + (x ⇒ (inr sole)))) + (let (my_list : DoublyLinkedList) + (fold + (pair 413 + (pair ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit)) + ((inr sole) : ((Ref DoublyLinkedList) ⊕ Unit))))) + (prev my_list)))))) + '(DoublyLinkedList ⊕ Unit)))) ;; new implementation of doubly linked lists: ;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))) - -(check-equal? - (interpret - '(let next - (λ self - (case (unfold self) - (some ⇒ (! (cdr (cdr some)))) - (none ⇒ (fold (inr sole))))) - (let my_list - (fold - (inl - (pair 413 - (pair (new (inr sole)) - (new (inr sole)))))) - (next my_list)))) - '(inr sole)) - -(check-equal? - (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) - (λ (self : DoublyLinkedList) - (case (unfold self) - (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList)) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))) - '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) - -(check-true - (equiv? +(define-test-suite dll-with-empty-lists + (check-equal? + (interpret + '(let next + (λ self + (case (unfold self) + (some ⇒ (! (cdr (cdr some)))) + (none ⇒ (fold (inr sole))))) + (let my_list + (fold + (inl + (pair 413 + (pair (new (inr sole)) + (new (inr sole)))))) + (next my_list)))) + '(inr sole)) + + (check-equal? (infer '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) (λ (self : DoublyLinkedList) (case (unfold self) - (some ⇒ (! (cdr (cdr some)))) + (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList)) (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 - (case (unfold self) - (some ⇒ (inl (car some))) - (none ⇒ (inr sole)))) - (let (prev : (DoublyLinkedList → 1 DoublyLinkedList)) - (λ self - (case (unfold self) - (some ⇒ (! (car (cdr some)))) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) - (let (next : (DoublyLinkedList → 1 DoublyLinkedList)) - (λ self - (case (unfold self) - (some ⇒ (! (cdr (cdr some)))) - (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) - (let (my_list : DoublyLinkedList) - (fold (inl - (pair 413 - (pair (new ((fold (inr sole)) : DoublyLinkedList)) - (new ((fold (inr sole)) : DoublyLinkedList)))))) - (prev my_list)))))) - 'DoublyLinkedList)) + '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))) + + (check-true + (equiv-type + (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)))))) + + (check-true + (check '(type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) + (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit))) + (λ self + (case (unfold self) + (some ⇒ (inl (car some))) + (none ⇒ (inr sole)))) + (let (prev : (DoublyLinkedList → 1 DoublyLinkedList)) + (λ self + (case (unfold self) + (some ⇒ (! (car (cdr some)))) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) + (let (next : (DoublyLinkedList → 1 DoublyLinkedList)) + (λ self + (case (unfold self) + (some ⇒ (! (cdr (cdr some)))) + (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))) + (let (my_list : DoublyLinkedList) + (fold (inl + (pair 413 + (pair (new ((fold (inr sole)) : DoublyLinkedList)) + (new ((fold (inr sole)) : DoublyLinkedList)))))) + (prev my_list)))))) + 'DoublyLinkedList))) diff --git a/stlc-ext.rkt b/stlc-ext.rkt index 9727068..300a473 100644 --- a/stlc-ext.rkt +++ b/stlc-ext.rkt @@ -1,7 +1,6 @@ #lang racket (require "lib.rkt") -(require rackunit) -(provide (all-defined-out)) +(provide interpret check infer expand equiv-type equiv-term) ;; The Simply-Typed Lambda Calculus, with simple extensions ;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption @@ -118,10 +117,10 @@ [`(λ (,x : ,t) ,e) (match with [`(,t1 → ,t2) - (and (equiv? t1 t Γ Γ) (check-core e t2 (dict-set Γ x t1)))] + (and (equiv-type t1 t Γ) (check-core e t2 (dict-set Γ x t1)))] [_ #f])] - [_ (equiv? (infer-core expr Γ) with Γ Γ)])) + [_ (equiv-type (infer-core expr Γ) with Γ)])) ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) @@ -176,7 +175,7 @@ [`(,a1 ⊕ ,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 + (if (equiv-type 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))])] @@ -211,28 +210,55 @@ (if (dict-has-key? Γ t) (expand (dict-ref Γ t) Γ) t)) -;; checks if two expressions are equivalent up to α-renaming and ascryption -(define (equiv? e1 e2 Γ1 Γ2) +;; Checks if two types are equivalent up to α-conversion in context +;; (equiv-type Expr Expr Table[Sym Expr]): Bool +(define (equiv-type e1 e2 Γ) + (equiv-type-core e1 e2 Γ Γ)) +(define (equiv-type-core e1 e2 Γ1 Γ2) (match* (e1 e2) + ; bound identifiers: if a key exists in the context, look it up [(x1 x2) #:when (dict-has-key? Γ1 x1) - (equiv? (dict-ref Γ1 x1) x2 Γ1 Γ2)] + (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)] [(x1 x2) #:when (dict-has-key? Γ2 x2) - (equiv? x1 (dict-ref Γ2 x2) Γ1 Γ2)] + (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + + ; check for syntactic equivalence on remaining forms + [(`(,l1 ...) `(,l2 ...)) + (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + [(v1 v2) (equal? v1 v2)])) + +;; Checks if two terms are equivalent up to α-conversion in context +;; (equiv-term Expr Expr Table[Sym Expr]): Bool +(define (equiv-term e1 e2 Γ) + (equiv-term-core e1 e2 Γ Γ)) +(define (equiv-term-core e1 e2 Γ1 Γ2) + (match* (e1 e2) + ; bound identifiers: if a key exists in the context, look it up + [(x1 x2) #:when (dict-has-key? Γ1 x1) + (equiv-term-core (dict-ref Γ1 x1) x2 Γ1 Γ2)] + [(x1 x2) #:when (dict-has-key? Γ2 x2) + (equiv-term-core x1 (dict-ref Γ2 x2) Γ1 Γ2)] + + ; function expressions: parameter names can be arbitrary [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2)) (let ([name gensym]) - (and (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) - (equiv? t1 t2 Γ1 Γ2)))] + (and (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) + (equiv-term-core t1 t2 Γ1 Γ2)))] [(`(λ ,x1 ,e1) `(λ ,x2 ,e2)) (let ([name gensym]) - (equiv? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))] + + ; check for syntactic equivalence on remaining forms [(`(,l1 ...) `(,l2 ...)) - (foldl (λ (x1 x2 acc) (if (equiv? x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] + (foldl (λ (x1 x2 acc) (if (equiv-term-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)] [(v1 v2) (equal? v1 v2)])) -(check-true (equiv? '(λ a a) '(λ b b) #hash() #hash())) -(check-true (equiv? '(λ a (λ b a)) '(λ b (λ a b)) #hash() #hash())) -(check-true (equiv? '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash() #hash())) -(check-eq? (interpret '(if #t 1 0)) 1) -(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)) +(require rackunit) +(define-test-suite ext + (check-true (equiv-term '(λ a a) '(λ b b) #hash())) + (check-true (equiv-term '(λ a (λ b a)) '(λ b (λ a b)) #hash())) + (check-true (equiv-term '(λ a (λ b (λ c (a (b c))))) '(λ c (λ a (λ b (c (a b))))) #hash())) + (check-eq? (interpret '(if #t 1 0)) 1) + (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))) |