diff options
| -rw-r--r-- | lib.rkt | 5 | ||||
| -rw-r--r-- | stlc-dll.rkt | 130 |
2 files changed, 110 insertions, 25 deletions
@@ -154,8 +154,3 @@ (check-equal? '(λ a (λ b (λ c (a (b c))))) (α-convert '(λ c (λ a (λ b (c (a b))))))) -(define (replace expr key value) - (match expr - [x #:when (equal? x key) value] - [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))] - [v v])) diff --git a/stlc-dll.rkt b/stlc-dll.rkt index bdd439b..927161a 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -5,7 +5,12 @@ ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references, ;; plus sums products booleans ascryption etc, to implement doubly-linked lists -;; (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value +;; Interprets a desugared, stripped expression. +;; Γ: a Table[Symbol, Expr] representing the context: +;; the current bindings in scope introduced by λx.[] +;; Σ: 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 Γ Σ) @@ -75,38 +80,96 @@ [e (err (format "attempting to interpret unknown expression ~a" e))])) +;; Checks that an expression is of a type, and returns #t or #f (or a bubbled-up error) +;; with: a *normalized* type +;; Γ: 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-core expr with Γ) ; (print (format "check: ~a with ~a" (fmt expr) with)) - (let ([with (expand with Γ)]) (match expr + [`(type ,t1 ,t2 ,in) + (check-core in with (dict-set Γ t1 t2))] + + [`(inc ,e) + (and (equiv? with 'Nat) + (check-core e 'Nat Γ))] + [`(if ,c ,e1 ,e2) + (and (check-core c 'Bool Γ) + (check-core e1 with Γ) (check-core e2 with Γ))] + + [`(pair ,e1 ,e2) + (match (expand with Γ) + [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))] + [t #f])] + [`(car ,e) + (match (expand (infer-core e Γ) Γ) + [`(,t1 × ,t2) (equiv? t1 with Γ Γ)] + [t #f])] + [`(cdr ,e) + (match (expand (infer-core e Γ) Γ) + [`(,t1 × ,t2) (equiv? t2 with Γ Γ)] + [t #f])] + [`(inl ,e) - (match with - [`(,t1 ⊕ ,t2) (equiv? t1 (infer-core e Γ) Γ Γ)] + (match (expand with Γ) + [`(,t1 ⊕ ,t2) (check-core e t1 Γ)] [t #f])] [`(inr ,e) - (match with - [`(,t1 ⊕ ,t2) (equiv? t2 (infer-core e Γ) Γ Γ)] + (match (expand with Γ) + [`(,t1 ⊕ ,t2) (check-core e t2 Γ)] + [t #f])] + [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) + (match (expand (infer-core e Γ) Γ) + [`(,a1 ⊕ ,a2) + (and (check-core e1 with (dict-set Γ x1 a1)) + (check-core e2 with (dict-set Γ x2 a2)))] + [t #f])] + + [`(new ,e) + (match (expand with Γ) + [`(Ref ,t) (check-core e t Γ)] + [t #f])] + [`(! ,e) (check-core e `(Ref ,with) Γ)] + [`(set ,e1 ,e2) + (match (expand (infer-core e1 Γ) Γ) + [`(Ref ,t) + (and (equiv? with 'Unit Γ Γ) + (check-core e2 t Γ))] [t #f])] [`(fold (μ ,x ,t) ,e) - (match with + (match (expand with Γ) [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))])] [`(unfold (μ ,x ,t) ,e) (and (check-core e `(μ ,x ,t) Γ) - (equiv? with t #hash() #hash((x . `(μ ,x ,t)))))] + (equiv? with t Γ (dict-set Γ x `(μ ,x ,t))))] [`(fold ,e) - (match with + (match (expand with Γ) [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))])] [`(unfold ,e) ; FIXME: GROSS (match* ((infer-core e Γ) with) [(`(μ ,_ ,t) `(μ ,_ ,t)) #T] [(t u) #f])] - [_ (equiv? with (infer-core expr Γ) Γ Γ)]))) + [`(λ (,x : ,t) ,e) + (match (expand with Γ) + [`(,t1 → ,k ,t2) + (and (equiv? t t1 Γ Γ) (check-core e t2 (dict-set Γ x t)) + (> k (max-level e t1 t2 (dict-set Γ x t1))))] ; KNOB + [t #f])] + [`(,e1 ,e2) + (match (infer-core e1 Γ) + [`(,t1 → ,_ ,t2) + (and (equiv? with t2 Γ Γ) + (check-core e2 t1 Γ))] + [t #f])] + + + [_ (equiv? with (infer-core expr Γ) Γ Γ)])) ;; Checks if two expressions or types are equivalent, up to α-conversion, ;; given their respective contexts @@ -140,6 +203,7 @@ (foldl (λ (x1 x2 acc) (if (equiv? 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. ;; (infer Expr Table[Sym, Type]): Type (define (infer expr [Γ #hash()]) (infer-core (desugar expr) Γ)) @@ -153,7 +217,7 @@ (dict-ref Γ x)] [`(type ,t1 ,t2 ,in) - (infer-core in (dict-set Γ t1 (expand t2 Γ)))] + (infer-core in (dict-set Γ t1 t2))] [`(,e : ,t) (if (check-core e t Γ) t (err (format "annotated expression ~a is not of annotated type ~a" e t)))] @@ -187,10 +251,11 @@ [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2)) (match (infer-core e Γ) [`(,a1 ⊕ ,a2) - (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))] - [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))]) + (let ([b1 (infer-core e1 (dict-set Γ x1 a1))] + [b2 (infer-core e2 (dict-set Γ x2 a2))]) (if (equiv? b1 b2 Γ Γ) b1 - (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))] + (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))])] [`(new ,e) @@ -217,17 +282,17 @@ e `(μ ,x ,t) (infer-core e Γ))))] [`(fold ,e) - (match (infer-core e Γ) + (match (expand (infer-core e Γ) Γ) [`(μ ,x ,t) `(μ ,x ,t)] [t (err (format "expected ~a to be recursive, got ~a" e t))])] [`(unfold ,e) - (match (infer-core e Γ) + (match (expand (infer-core e Γ) Γ) [`(μ ,x ,t) (replace t x `(μ ,x ,t))] ; AAAA [t (err (format "expected ~a to be recursive, got ~a" e t))])] [`(λ (,x : ,t1) ,e) - (let ([t2 (infer-core e (dict-set Γ x (expand t1 Γ)))]) - (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x (expand t1 Γ))))]) ; KNOB + (let ([t2 (infer-core e (dict-set Γ x t1))]) + (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))]) ; KNOB `(,t1 → ,k ,t2)))] [`(,e1 ,e2) (match (infer-core e1 Γ) @@ -239,9 +304,34 @@ [e (err (format "attempting to infer an unknown expression ~a" e))])) +;; Expands a type alias to a matchable outside structure, for literal matching. ;; (expand Type Table[Id, Expr ⊕ Type]): Type (define (expand t Γ) - (if (dict-has-key? Γ t) (dict-ref Γ t) t)) + (if (dict-has-key? Γ t) (expand (dict-ref Γ t) Γ) t)) + +(define (replace expr key value) + (match expr + ; do not accidentally replace shadowed bindings + [(or `(λ (,x : ,_) ,_) `(λ ,x ,_) `(μ ,x ,_) + `(type ,x ,_ ,_)) #:when (equal? x key) expr] + [x #:when (equal? x key) value] + [`(,e ...) `(,@(map (λ (x) (replace x key value)) e))] + [v v])) + +;; Checks if a type is well-formed in the current context. +;; (well-formed Type Context): Bool +(define (well-formed t Γ) + (if (well-formed-friend t Γ) #t + (err (format "type ~a is not well-formed!" t)))) +(define (well-formed-friend t Γ) + (match t + [x #:when (dict-has-key? Γ x) (dict-ref Γ x)] + [(or 'Unit 'Nat 'Bool) #t] + [`(Ref ,t) (well-formed-friend t Γ)] + [`(μ ,x ,t) (well-formed-friend t (dict-set Γ x 'Unit))] ; HACK + [(or `(,t1 → ,t2) `(,t1 → ,_ ,t2) `(,t1 × ,t2) `(,t1 ⊕ ,t2)) + (and (well-formed-friend t1 Γ) (well-formed-friend t2 Γ))] + [_ #f])) ;; (max-level Table[Sym, Type] Expr Type Type): Natural (define (max-level e t1 t2 Γ) @@ -296,7 +386,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 (expand t Γ)))] ; todo: should be 0? + [`(λ (,x : ,t) ,e) (level-body e (dict-set Γ x t))] ; todo: should be 0? [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))])) |