aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--stlc-dll.rkt90
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 '