diff options
Diffstat (limited to 'stlc-dll.rkt')
| -rw-r--r-- | stlc-dll.rkt | 70 |
1 files changed, 39 insertions, 31 deletions
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 |