aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-07-26 19:32:14 +0000
committerJJ2024-07-26 19:32:22 +0000
commit06b890f26a7b308af135b3ba156c1203cdfcb36d (patch)
treed7b57798591c8ca40cebc8f7403d468abadc75bd
parenta8fa6eeb42fd0d119d3ce55f53c332da3df46db7 (diff)
stlc-dll: rewrite level-body and implement well-formed
-rw-r--r--stlc-dll.rkt82
1 files changed, 43 insertions, 39 deletions
diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 1bd82e9..8829ead 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -318,59 +318,63 @@
;; (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 Γ)
- (level-body e Γ)))
+ (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 Γ)
+ (match t
+ [x #:when (dict-has-key? Γ x)
+ (well-kinded (dict-ref Γ x) l Γ)]
+ [(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 Γ))]
+ [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
+ (and (well-kinded t1 l Γ) (well-kinded t2 l Γ))]
+ [_ #f]))
;; (level-type Type): Natural
(define (level-type t Γ)
- (match (expand t Γ)
- ['Unit 0]
- ['Nat 0]
- [`(,t1 × ,t2) (max (level-type t1 Γ) (level-type t2 Γ))]
- [`(,t1 ⊕ ,t2) (max (level-type t1 Γ) (level-type t2 Γ))]
- [`(μ ,x ,t) (level-type t (dict-set Γ x 'Unit))] ; VERY WEIRD
+ (match t
+ [x #:when (dict-has-key? Γ x)
+ (level-type (dict-ref Γ x) Γ)]
+ [(or 'Unit 'Nat) 0]
+ [(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))]
[`(,t1 → ,k ,t2)
- (if (or (< k (level-type t1 Γ)) (< k (level-type t2 Γ)))
- (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
- k t1 t2))
- k)]
+ (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))]))
+;; Infers the level of a (well-formed) expression.
;; (level-body Expr Table[Sym, Type]): Natural
-(define (level-body e Γ) ; FIXME: this part is mostly wrong
+(define (level-body e Γ)
(match e
- [`(,e : ,t) (level-type t Γ)] ; hrm
['sole 0]
[n #:when (natural? n) 0]
- [x #:when (dict-has-key? Γ x)
- (level-type (dict-ref Γ x) Γ)]
- [`(inc ,e) (level-body e Γ)]
- [`(new ,e) (level-body e Γ)]
-
- [`(pair ,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]
- [`(car ,e) (level-body e Γ)]
- [`(cdr ,e) (level-body e Γ)]
- [`(inl ,e) (level-body e Γ)]
- [`(inr ,e) (level-body e Γ)]
- [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
- (max (level-body e Γ)
- (level-body e1 (dict-set Γ x1 'Unit)) ; FIXME: totally incorrect
- (level-body e2 (dict-set Γ x2 'Unit)))]
- [`(fold (μ ,x ,t) ,e) (level-body e Γ)]
- [`(unfold (μ ,x ,t) ,e) (level-body e Γ)]
- [`(fold ,e) (level-body e Γ)]
- [`(unfold ,e) (level-body e Γ)]
-
- [`(! ,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 t))] ; todo: should be 0?
- [`(,e1 ,e2) (max (level-body e1 Γ) (level-body e2 Γ))]))
-
+ [x #:when (dict-has-key? Γ x) ; free variables
+ (level-type (expand (dict-ref Γ x) Γ) Γ)]
+ [(or `(,e : ,_) `(λ (,_ : ,_) ,e)
+ `(inc ,e) `(new ,e) `(! ,e) `(car ,e) `(cdr ,e) `(inl ,e) `(inr ,e)
+ `(fold ,e) `(unfold ,e) `(fold (μ ,_ ,_) ,e) `(unfold (μ ,_ ,_) ,e))
+ (level-body e Γ)]
+ [(or `(set ,e1 ,e2) `(pair ,e1 ,e2) `(,e1 ,e2))
+ (max (level-body e1 Γ) (level-body e2 Γ))]
+ [(or `(if ,c ,e1 ,e2) `(case ,c (,_ ⇒ ,e1) (,_ ⇒ ,e2)))
+ (max (level-body c Γ) (level-body e1 Γ) (level-body e2 Γ))]
+ [x #:when (symbol? x) 0])) ; local variables, not in Γ
(check-exn
exn:fail?