diff options
| -rw-r--r-- | stlc-dll.rkt | 90 |
1 files changed, 24 insertions, 66 deletions
diff --git a/stlc-dll.rkt b/stlc-dll.rkt index 8829ead..8b447c1 100644 --- a/stlc-dll.rkt +++ b/stlc-dll.rkt @@ -1,19 +1,18 @@ #lang racket (require "lib.rkt") (require (only-in "stlc-rec.rkt" replace)) -(require rackunit) ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references, ;; plus sums products booleans ascryption etc, to implement doubly-linked lists -;; Interprets a desugared, stripped expression. +;; (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value ⊕ Err +(define (interpret expr) + (interpret-core (strip (desugar expr)) #hash() (make-hash))) ;; Γ: 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) - (interpret-core (strip (desugar expr)) #hash() (make-hash))) +;; Interprets a *desugared* expression *stripped* of type annotations. (define (interpret-core expr Γ Σ) (match expr ['sole 'sole] @@ -92,9 +91,6 @@ [`(type ,t1 ,t2 ,in) (check-core in with (dict-set Γ t1 t2))] - [`(inc ,e) - (and (equiv? 'Nat with) - (check-core e 'Nat Γ))] [`(if ,c ,e1 ,e2) (and (check-core c 'Bool Γ) (check-core e1 with Γ) (check-core e2 with Γ))] @@ -103,14 +99,6 @@ (match with [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))] [_ #f])] - [`(car ,e) - (match (infer-core e Γ) - [`(,t1 × ,t2) (equiv? t1 with Γ Γ)] - [_ #f])] - [`(cdr ,e) - (match (infer-core e Γ) - [`(,t1 × ,t2) (equiv? t2 with Γ Γ)] - [_ #f])] [`(inl ,e) (match with @@ -131,17 +119,8 @@ (match with [`(Ref ,t) (check-core e t Γ)] [_ #f])] - [`(! ,e) (check-core e `(Ref ,with) Γ)] - [`(set ,e1 ,e2) - (match (infer-core e1 Γ) - [`(Ref ,t) - (and (equiv? 'Unit with Γ Γ) - (check-core e2 t Γ))] - [_ #f])] - - ; [`(fold (μ ,x ,t) ,e) - ; (match with - ; [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))])] + [`(! ,e) + (check-core e `(Ref ,with) Γ)] [`(fold ,e) (match with @@ -152,16 +131,10 @@ (match 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 - [_ #f])] - [`(,e1 ,e2) - (match (infer-core e1 Γ) - [`(,t1 → ,_ ,t2) - (and (equiv? t2 with Γ Γ) - (check-core e2 t1 Γ))] + (> 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 Γ Γ)])) ;; Checks if two expressions or types are equivalent, up to α-conversion, @@ -182,22 +155,23 @@ [(`(μ ,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? e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)) - (equiv? t1 t2 Γ1 Γ2)))] + (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)))] - ; check for syntactic equivalence on lists and values + ; check for syntactic equivalence on remaining forms [(`(,l1 ...) `(,l2 ...)) (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. -;; Should always return a type in weak-head normal form for structural matching. +;; Returns a type in weak-head normal form for structural matching. ;; (infer Expr Table[Sym, Type]): Type (define (infer expr) (infer-core (desugar expr) #hash())) @@ -265,29 +239,16 @@ e1 t e2 (infer-core e2 Γ))))] [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])] - [`(fold (μ ,x ,t) ,e) - (if (check-core e (expand t Γ) (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t) - (err (format "expected ~a to be of type ~a, got ~a" - e t (infer e (dict-set Γ x `(μ ,x ,t))))))] - [`(unfold (μ ,x ,t) ,e) - (if (check-core e `(μ ,x ,t)) (replace t x `(μ ,x ,t)) - (err (format "expected ~a to be of type ~a, got ~a" - e `(μ ,x ,t) (infer-core e Γ))))] - - [`(fold ,e) - (match (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 Γ) [`(μ ,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-core e (dict-set Γ x t1))]) - (let ([t1 (expand t1 Γ)]) ; type annotation, must expand to weak-head normal form - (let ([k (+ 1 (max-level e t1 t2 (dict-set Γ x t1)))]) ; KNOB - `(,t1 → ,k ,t2))))] + (let* ([t2 (infer-core e (dict-set Γ x t1))] + [t1 (expand t1 Γ)] ; type annotation, must expand + [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB + `(,t1 → ,k ,t2))] [`(,e1 ,e2) (match (infer-core e1 Γ) [`(,t1 → ,k ,t2) @@ -301,7 +262,8 @@ ;; 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)) + (if (dict-has-key? Γ t) + (expand (dict-ref Γ t) Γ) t)) ;; Checks if a type is well-formed in the current context. ;; (well-formed Type Context): Bool @@ -315,12 +277,6 @@ (and (well-formed t1 Γ) (well-formed t2 Γ))] [_ #f])) -;; (max-level Table[Sym, Type] Expr Type Type): Natural -(define (max-level e t1 t2 Γ) - (max - (level-body e Γ) - (level-type t1 Γ) - (level-type t2 Γ))) ;; Checks if a type is well-kinded with respect to a level in the current context ;; (well-kinded Type Level Context): Bool (define (well-kinded t l Γ) @@ -349,14 +305,14 @@ [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (max (level-type t1 Γ) (level-type t2 Γ))] [`(μ ,x ,t) ; fixme: correct, ish, but VERY WEIRD - (level-type t (dict-set Γ x 'Unit))] + (level-type t Γ)] [`(,t1 → ,k ,t2) - (if (and (> k (level-type t1 Γ)) (> k (level-type t2 Γ))) k ; KNOB + (if (and (>= k (level-type t1 Γ)) (>= k (level-type t2 Γ))) k ; KNOB (err (format "annotated level ~a is less than inferred levels of ~a and ~a!" k t1 t2)))] [`(Ref ,t) (let ([k (level-type t Γ)]) (if (zero? k) 0 (+ 1 k)))] ; KNOB - [t (err (format "attempting to infer the level of unknown type ~a" t))])) + [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ ;; Infers the level of a (well-formed) expression. ;; (level-body Expr Table[Sym, Type]): Natural @@ -376,6 +332,8 @@ (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))] [x #:when (symbol? x) 0])) ; local variables, not in Γ +(require rackunit) + (check-exn exn:fail? (λ () (infer ' |