aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJJ2024-08-31 00:27:21 +0000
committerJJ2024-08-31 00:27:21 +0000
commitb6c33b87b64bcbbd7555849031d1597966716634 (patch)
tree4d81788e2a53552733d409e5507499d7e8263018
parent83a1400957da57bf6930bab4b81af87f1851be5b (diff)
add self-contained implementation as stlc-full
-rw-r--r--stlc-full.rkt739
1 files changed, 739 insertions, 0 deletions
diff --git a/stlc-full.rkt b/stlc-full.rkt
new file mode 100644
index 0000000..3df2fa8
--- /dev/null
+++ b/stlc-full.rkt
@@ -0,0 +1,739 @@
+#lang racket
+(require syntax/location)
+(require (for-syntax syntax/location))
+
+;; The simply-typed lambda calculus, with:
+;; - sums, products, recursive types, ascryption
+;; - bidirectional typechecking
+;; - impredicative references built on a levels system
+;; - explicit level stratification syntax
+;; - automatic level collection
+;;
+;; This system is impredicative. It can be made predicative by tweaking
+;; the sections of the code labeled with "KNOB".
+
+(define-syntax-rule (print msg)
+ (eprintf "~a~%" msg))
+
+(define-syntax-rule (dbg body)
+ (let ([res body])
+ (eprintf "[~a:~a] ~v = ~a~%"
+ (syntax-source-file-name #'body)
+ (syntax-line #'body)
+ 'body
+ res)
+ res))
+
+(define-syntax-rule (err msg)
+ (error 'error
+ (format "[~a:~a] ~a"
+ (syntax-source-file-name #'msg)
+ (syntax-line #'msg)
+ msg)))
+
+(define-syntax (todo stx)
+ (with-syntax ([src (syntax-source-file-name stx)] [line (syntax-line stx)])
+ #'(error 'todo (format "[~a:~a] unimplemented" src line))))
+
+(define (any? proc lst)
+ (foldl (λ (x acc) (if (proc x) #t acc)) #f lst))
+
+(define (all? proc lst)
+ (foldl (λ (x acc) (if (proc x) acc #f)) #t lst))
+
+;; Whether a given level is a syntactically valid level.
+;; This does not account for context, and so all symbols are valid levels.
+(define (level? level)
+ (match level
+ [n #:when (natural? n) #t]
+ ; Symbols are only valid if previously bound (by `level`).
+ ; We can't check that here, however.
+ [s #:when (symbol? s) #t]
+ ; Levels may be a list of symbols, or a list of symbols followed by a natural.
+ [`(+ ,l ... ,n) #:when (natural? n)
+ (all? (λ (s) (symbol? s)) l)]
+ [`(+ ,l ...)
+ (all? (λ (s) (symbol? s)) l)]
+ [_ #f]))
+
+;; Whether a given type is a syntactically valid type.
+;; This does not account for context, and so all symbols are valid types.
+(define (type? type)
+ (match type
+ [(or 'Unit 'Bool 'Nat) #t]
+ ; Symbols are only valid if previously bound (by `type` or `μ`).
+ ; We can't check that here, however.
+ [s #:when (symbol? s) #t]
+ [`(Ref ,t) (type? t)]
+ [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (type? t1) (type? t2))]
+ [`(,t1 → ,l ,t2) (and (type? t1) (level? l) (type? t2))]
+ [`(μ ,x ,t) (and (symbol? x) (type? t))]
+ [_ #f]))
+
+;; Whether a given expression is a syntactically valid expression.
+;; This does not account for context, and so all symbols are valid exprs.
+(define (expr? expr)
+ (match expr
+ ['sole #t]
+ [n #:when (natural? n) #t]
+ [b #:when (boolean? b) #t]
+ ; Symbols are only valid if previously bound by `λ` or `case`.
+ ; We can't check that here, however.
+ [s #:when (symbol? s) #t]
+
+ [`(,e : ,t) (and (expr? e) (type? t))]
+ [`(type ,t1 ,t2 ,e)
+ (and (type? t1) (type? t2) (expr? e))]
+
+ ; Note that level must only introduce new variables as levels.
+ [`(level ,l ,e)
+ (and (symbol? l) (expr? e))]
+ ; Kind of want to call ⇑ :: on analogy with :
+ [`(,e ⇑ ,l)
+ (and (expr? e) (level? l))]
+
+ [(or `(new ,e) `(! ,e)) (expr? e)]
+ ; [`(ptr ,a) (symbol? a)]
+ [`(set ,e1 ,e2) (and (expr? e1) (expr? e2))]
+
+ [`(inc ,e) (expr? e)]
+ [`(if ,c ,e1 ,e2)
+ (and (expr? c) (expr? e1) (expr? e2))]
+
+ [`(pair ,e1 ,e2)
+ (and (expr? e1) (expr? e2))]
+ [(or `(car ,e) `(cdr ,e)) (expr? e)]
+
+ [(or `(inl ,e) `(inr ,e)) (expr? e)]
+ [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+ (and (symbol? x1) (symbol? x2)
+ (expr? c) (expr? e1) (expr? e2))]
+
+ [(or `(fold ,e) `(unfold ,e)) (expr? e)]
+
+ [`(λ (,x : ,t) ,e)
+ (and (symbol? x) (type? t) (expr? e))]
+ [`(,e1 ,e2) (and (expr? e1) (expr? e2))]
+ [_ #f]))
+
+;; Whether a term is a value or a computation. What's that little rhyme about this again?
+;; A value is, a computation/expr/term does?
+(define (value? expr)
+ (match expr
+ ['sole #t]
+ [n #:when (natural? n) #t]
+ [b #:when (boolean? b) #t]
+
+ ; [`(,v : ,t) (and (expr? v) (type? t))]
+ ; [`(type ,t1 ,t2 ,b)
+ ; (and (type? t1) (type? t2) (value? v))]
+
+ ; [(or `(level ,l ,v) `(,v ⇑ ,l))
+ ; (and (level? l) (value? v))]
+
+ [`(ptr ,l ,a) (and (level? l) (symbol? a))]
+
+ [`(pair ,v1 ,v2)
+ (and (value? v1) (value? v2))]
+
+ [(or `(inl ,v) `(inr ,v)) (value? v)]
+
+ ; [(or `(fold ,v) `(unfold ,v)) (value? v)]
+
+ [`(λ (,x : ,t) ,e ,env)
+ (and (symbol? x) (type? t) (expr? e) (dict? env))]
+ [_ #f]))
+
+(define (ptr? expr)
+ (match expr
+ [`(ptr ,l ,a) (and (level? l) (symbol? a))]
+ [_ #f]))
+
+;; Checks if a level is at its "base" form.
+(define/contract (level-base? l) (-> level? boolean?)
+ (match l
+ [n #:when (natural? n) (zero? n)]
+ [s #:when (symbol? s) #t]
+ [`(+ ,s ... ,n) #:when (natural? n) (zero? n)] ; should be avoided
+ [`(+ ,s ...) #t]))
+
+;; Syntactic equality between levels is not trivial.
+;; This helper function defines it.
+(define/contract (level-eq? l1 l2) (-> level? level? boolean?)
+ (match* (l1 l2)
+ [(n1 n2) #:when (and (natural? n1) (natural? n2))
+ (equal? n1 n2)]
+ [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2))
+ (and (equal? n1 n2) (level-eq? `(+ ,@s1) `(+ ,@s2)))]
+ [(`(+ ,s1 ...) `(+ ,s2 ...))
+ todo] ; need to check for equality as multisets
+ [(_ _) #f]))
+
+;; Levels can carry natural numbers, and so we define a stratification between them.
+;; Note: this returns FALSE if the levels are incomparable (i.e. (level-geq 'a 'b))
+(define/contract (level-geq? l1 l2) (-> level? level? boolean?)
+ (match* (l1 l2)
+ [(n1 n2) #:when (and (natural? n1) (natural? n2))
+ (>= n1 n2)]
+ [(s1 s2) #:when (and (symbol? s1) (symbol? s2))
+ (equal? s1 s2)]
+ [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2))
+ (and (level-eq? `(+ ,@s1) `(+ ,@s2)) (level-geq? n1 n2))]
+ [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n)
+ (level-eq? `(+ ,@s1) `(+ ,@s2))]
+ [(`(+ ,s1 ...) `(+ ,s2 ...))
+ todo] ; this needs to inspect the levels... ugh
+ [(_ _) #f]))
+
+;; We define a maximum of two levels.
+;; This can return one of the two levels or an entirely new level.
+(define/contract (level-max l1 l2) (-> level? level? level?)
+ (match* (l1 l2)
+ [(n1 n2) #:when (and (natural? n1) (natural? n2))
+ (max n1 n2)]
+ [(s1 s2) #:when (and (symbol? s1) (symbol? s2))
+ (if (equal? s1 s2) s1 `(+ ,s1 ,s2))]
+ [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2))
+ (if (equal? s1 s2)
+ `(+ ,@s1 ,(max n1 n2))
+ (level-intersect `(+ ,@s1) `(+ ,@s2)))]
+ [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n)
+ (if (level-geq? s1 s2)
+ `(+ ,@s1 ,n)
+ (level-intersect `(+ ,@s1) `(+ ,@s2)))]
+ [(`(+ ,s1 ...) `(+ ,s2 ... ,n)) #:when (natural? n)
+ (if (level-geq? s2 s1)
+ `(+ ,@s2 ,n)
+ (level-intersect `(+ ,@s1) `(+ ,@s2)))]
+ [(`(+ ,s ... ,n1) n2) #:when (and (natural? n1) (natural? n2))
+ `(+ ,s ... ,n1)]
+ [(n1 `(+ ,s ... ,n2)) #:when (and (natural? n1) (natural? n2))
+ `(+ ,s ... ,n2)]
+ [(`(+ ,s ...) n) #:when (natural? n)
+ `(+ ,@s ,n)]
+ [(n `(+ ,s ...)) #:when (natural? n)
+ `(+ ,@s ,n)]
+ [(`(+ ,s1 ...) `(+ ,s2 ...))
+ (level-intersect `(+ ,@s1) `(+ ,@s2))]))
+
+;; A helper function to perform intersection of levels.
+(define/contract (level-intersect l1 l2) (-> level-base? level-base? level-base?)
+ (match* (l1 l2)
+ [(0 l) l]
+ [(l 0) l]
+ [(`(+ ,s1 ...) `(+ ,s2 ...)) todo])) ; we need multisets. this is gross.
+
+;; We define addition in terms of our syntactic constructs.
+(define/contract (level-add l1 l2) (-> level? level? level?)
+ (match* (l1 l2)
+ [(n1 n2) #:when (and (natural? n1) (natural? n2))
+ (+ n1 n2)]
+ [(s1 s2) #:when (and (symbol? s1) (symbol? s2))
+ `(+ ,s1 ,s2)]
+ [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2))
+ (level-add (level-add `(+ ,@s1) `(+ ,@s2)) (+ n1 n2))]
+ [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n)
+ (level-add (level-add `(+ ,@s1) `(+ ,@s2)) n)]
+ [(`(+ ,s1 ...) `(+ ,s2 ... ,n)) #:when (natural? n)
+ (level-add (level-add `(+ ,@s1) `(+ ,@s2)) n)]
+ [(`(+ ,s ... ,n1) n2) #:when (and (natural? n1) (natural? n2))
+ `(+ ,@s ,(+ n1 n2))]
+ [(n1 `(+ ,s ... ,n2)) #:when (and (natural? n1) (natural? n2))
+ `(+ ,@s ,(+ n1 n2))]
+ [(`(+ ,s ...) n) #:when (natural? n)
+ `(+ ,@s ,n)]
+ [(n `(+ ,s ...)) #:when (natural? n)
+ `(+ ,@s ,n)]
+ [(`(+ ,s1 ...) `(+ ,s2 ...))
+ `(+ ,@s1 ,@s2)]))
+
+;; Decrements a level by 1.
+;; ASSUMPTION: the level is not a base level (i.e. there is some n to dec)
+(define/contract (level-dec l) (-> level? level?)
+ (match l
+ [n #:when (and (natural? n) (not (zero? n))) (- n 1)]
+ [`(+ ,s ... 1) `(+ ,@s)]
+ [`(+ ,s ... ,n) #:when (and (natural? n) (not (zero? n))) `(+ ,@s ,(- n 1))]
+ [_ (err (format "attempting to decrement base level ~a" l))]))
+
+;; Returns the "base" form of a level.
+(define/contract (level-base l) (-> level? level?)
+ (match l
+ [n #:when (natural? n) 0]
+ [s #:when (symbol? s) s]
+ [`(+ ,s ... ,n) #:when (natural? n) `(+ ,@s)]
+ [`(+ ,s ...) `(+ ,@s)]))
+
+;; Returns the "offset" portion of a level.
+(define/contract (level-offset l) (-> level? level?)
+ (match l
+ [n #:when (natural? n) n]
+ [s #:when (symbol? s) 0]
+ [`(+ ,s ... ,n) #:when (natural? n) n]
+ [`(+ ,s ...) 0]))
+
+;; Infers the level of a (well-formed) type in a context.
+;; We need the context for type ascryption, and μ-types.
+;; Otherwise, levels are syntactically inferred.
+;; ASSUMPTION: the type is well-formed in the given context (i.e. all symbols bound).
+;; This is not checked via contracts due to (presumably) massive performance overhead.
+(define/contract (level-type t Γ) (-> type? dict? level?)
+ (match t
+ [(or 'Unit 'Bool 'Nat) 0]
+ [s #:when (symbol? s) 0] ; HACK: μ-type variables, not in Γ
+ [`(Ref ,t) ; KNOB
+ (let ([l (level-type t Γ)])
+ (if (level-base? l) l
+ (level-add l 1)))]
+ [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
+ (level-max (level-type t1 Γ) (level-type t2 Γ))]
+ [`(,t1 → ,l ,t2) ; KNOB
+ (if (and (level-geq? l (level-type t1 Γ)) (level-geq? l (level-type t2 Γ))) l
+ (err (format "annotated level ~a is less than inferred levels ~a and ~a!")))]
+ [`(μ ,x ,t)
+ (level-type t (dict-set Γ x `(μ ,x ,t)))]))
+
+;; Infers the level of a (well-formed) expression.
+(define/contract (level-expr e Γ) (-> expr? dict? level?)
+ (match e
+ ['sole 0]
+ [n #:when (natural? n) 0]
+ [b #:when (boolean? b) 0]
+ [x #:when (dict-has-key? Γ x) ; free variables
+ (level-type (expand-whnf (dict-ref Γ x) Γ) Γ)]
+ [s #:when (symbol? s) 0] ; local variables
+
+ [`(,e : ,t)
+ (let ([l1 (level-expr e Γ)] [l2 (level-type t Γ)])
+ (if (level-geq? l1 l2) l1
+ (err (format "annotated level ~a is less than inferred level ~a!" l1 l2))))]
+ [`(type ,t1 ,t2 ,e)
+ (level-expr e (dict-set Γ `(type ,t1) t2))]
+
+ [`(level ,l ,e) ; NOTE: is this correct?
+ (level-expr e Γ)]
+ [`(,e ⇑ ,l)
+ (level-add l (level-expr e Γ))]
+
+ [`(new ,e) ; KNOB
+ (let ([l (level-expr e Γ)])
+ (if (level-base? l) l (level-add l 1)))]
+
+ [`(if ,c ,e1 ,e2)
+ (level-max (level-expr c Γ)
+ (level-expr e1 Γ) (level-expr e2 Γ))]
+ [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+ (level-max (level-expr c Γ) ; support shadowing
+ (level-expr e1 (dict-remove Γ x1))
+ (level-expr e2 (dict-remove Γ x2)))]
+ [`(λ (,x : ,_) ,e) ; support shadowing
+ (level-expr e (dict-remove Γ x))]
+
+ [(or `(! ,e)`(inc ,e)
+ `(car ,e) `(cdr ,e)
+ `(inl ,e) `(inr ,e)
+ `(fold ,e) `(unfold ,e))
+ (level-expr e Γ)]
+ [(or `(set ,e1 ,e2) `(pair ,e1 ,e2) `(,e1 ,e2))
+ (level-max (level-expr e1 Γ) (level-expr e2 Γ))]))
+
+;; Whether a given type is a semantically valid type.
+;; We assume any type in Γ is semantically valid.
+;; Otherwise, we would infinitely recurse re: μ.
+(define/contract (well-formed? t Γ) (-> type? dict? boolean?)
+ (match t
+ [(or 'Unit 'Bool 'Nat) #t]
+ [s #:when (symbol? s) (dict-has-key? Γ `(type s))]
+ [`(Ref ,t) (well-formed? t Γ)]
+ [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (well-formed? t1 Γ) (well-formed? t2 Γ))]
+ [`(,t1 → ,l ,t2)
+ (and (dict-has-key? Γ `(level ,l))
+ (well-formed? t1 Γ) (well-formed? t2 Γ))]
+ [`(μ ,x ,t) ; check: this might infinitely recurse??
+ (well-formed? t (dict-set Γ `(type ,x) `(μ ,x ,t)))]))
+
+;; Whether a given type at a given level is semantically valid.
+(define/contract (well-kinded? t l Γ) (-> type? level? dict? boolean?)
+ (match t
+ [(or 'Unit 'Bool 'Nat) (level-geq? l 0)]
+ [s #:when (symbol? s)
+ (if (dict-has-key? `(type ,s))
+ (well-kinded? (dict-ref Γ `(type ,t))) #f)]
+ [`(Ref ,t) ; FIXME: this is not entirely correct. hrm.
+ (if (level-base? l)
+ (well-kinded? t l Γ)
+ (well-kinded? t (level-dec l) Γ))]
+ [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
+ (and (well-kinded? t1 l Γ) (well-kinded? t1 l Γ))]
+ [`(,t1 → ,k ,t2)
+ (and (level-geq? l k) (well-kinded? t1 k Γ) (well-kinded? t2 k Γ))]
+ [`(μ ,x ,t) ; HACK
+ (well-kinded? t l (dict-set Γ `(type ,x) 'Unit))]))
+
+;; Whether a given structure is the heap, in our model.
+;; This is a quite useless function and is just here to note the model of the heap.
+;; Our heap is a Dict[Level, List[Dict[Addr, Expr]]]. In other words:
+;; - the heap is first stratified by algebraic levels, i.e. α, β, α+β, etc
+;; - those heaps are then stratified by n: the level as a natural number.
+;; - this is
+(define (heap? heap)
+ (match heap
+ [`((,level-var . (,subheap ...)) ...)
+ (and (all? (λ (l) (level? l)) level-var)
+ (all? (λ (n) (dict? n)) subheap))]
+ [_ #f]))
+
+;; Extends a list to have at least n+1 elements. Takes a default-generating procedure.
+(define/contract (list-extend l n default) (-> list? natural? procedure? list?)
+ (if (>= n (length l))
+ (build-list (+ n 1)
+ (λ (k)
+ (if (< k (length l))
+ (list-ref l k)
+ (default))))
+ l))
+
+;; Models the allocation of an (unsized) memory pointer at an arbitrary heap level.
+(define/contract (alloc! Σ l) (-> dict? level? ptr?)
+ (let ([addr (gensym)] [base (level-base l)] [offset (level-offset l)])
+ (if (dict-has-key? Σ base)
+ (let ([base-heap (dict-ref Σ base)])
+ (if (>= offset (length base-heap))
+ (dict-set! Σ base ; FIXME: we probably should error if location is occupied
+ (let ([offset-heap (make-hash)])
+ (dict-set! offset-heap addr 'null) ; FIXME: probably should not be null
+ (list-set (list-extend base-heap offset make-hash) offset offset-heap)))
+ (let ([offset-heap (list-ref base-heap offset)])
+ (dict-set! offset-heap addr 'null))))
+ (dict-set! Σ base
+ (let ([offset-heap (make-hash)])
+ (dict-set! offset-heap addr 'null)
+ (list-set (build-list (+ offset 1) (λ (_) (make-hash))) offset offset-heap))))
+ `(ptr ,l ,addr)))
+
+;; Updates the heap given a pointer to a memory location and a value.
+(define/contract (write! Σ p v) (-> dict? ptr? value? ptr?)
+ (match p
+ [`(ptr ,l ,a)
+ (let ([base (level-base l)] [offset (level-offset l)])
+ (if (dict-has-key? Σ base)
+ (let ([base-heap (dict-ref Σ base)])
+ (if (< offset (length base-heap))
+ (dict-set! (list-ref base-heap offset) a v)
+ (err (format "writing to invalid memory location ~a!" p))))
+ (err (format "writing to invalid memory location ~a!" p))))])
+ p)
+
+;; Returns the corresponding value of a pointer to a memory location on the heap.
+(define/contract (read! Σ p) (-> dict? ptr? value?)
+ (match p
+ [`(ptr ,l ,a)
+ (let ([base (level-base l)] [offset (level-offset l)])
+ (if (dict-has-key? Σ base)
+ (let ([base-heap (dict-ref Σ base)])
+ (if (< offset (length base-heap))
+ (dict-ref (list-ref base-heap offset) a)
+ (err (format "reading from invalid memory location ~a!" p))))
+ (err (format "reading from invalid memory location ~a!" p))))]))
+
+;; Models the deallocation of all memory locations of level `l` or higher.
+;; For complexity and performance purposes, we only support deallocating base levels.
+(define/contract (dealloc! Σ l) (-> dict? level-base? void?)
+ (for-each
+ (λ (key) (if (level-geq? key l) (dict-remove! Σ key) (void)))
+ (dict-keys Σ)))
+
+;; Whether two types are equivalent in a context.
+;; We define equivalence as equivalence up to α-renaming.
+(define/contract (equiv-type t1 t2 Γ) (-> type? type? dict? boolean?)
+ (equiv-type-core t1 t2 Γ Γ))
+(define (equiv-type-core t1 t2 Γ1 Γ2)
+ (match* (t1 t2)
+ ; bound identifiers: if a key exists in the context, look it up
+ [(x1 x2) #:when (dict-has-key? Γ1 x1)
+ (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
+ [(x1 x2) #:when (dict-has-key? Γ2 x2)
+ (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+
+ ; recursive types: self-referential names can be arbitrary
+ [(`(μ ,x1 ,t1) `(μ ,x2 ,t2))
+ (let ([name gensym])
+ (equiv-type-core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+
+ ; check for syntactic equivalence on remaining forms
+ [(`(,l1 ...) `(,l2 ...))
+ (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+ [(v1 v2) (equal? v1 v2)]))
+
+;; Whether two expressions are equivalent in a context.
+;; We define equivalence as equivalence up to α-renaming.
+; (define/contract (equiv-expr e1 e2 Γ) (-> expr? expr? dict? boolean?)
+; (equiv-expr-core e1 e2 Γ Γ))
+; (define (equiv-expr-core e1 e2 Γ1 Γ2)
+; (match* (e1 e2)))
+
+;; Expands a type alias into weak-head normal form, for literal matching.
+(define/contract (expand-whnf t Γ) (-> type? dict? type?)
+ (if (dict-has-key? Γ `(type t))
+ (expand-whnf (dict-ref Γ t) Γ) t))
+
+;; Replaces all references to a type alias with another alias.
+(define/contract (replace-type type key value) (-> type? type? type? type?)
+ (match type
+ ; Do not accidentally replace shadowed bindings
+ [`(μ ,x _) #:when (equal? x key) type]
+ [`(,e ...) `(,@(map (λ (x) (replace-type x key value)) e))]
+ [x #:when (equal? x key) value]
+ [v v]))
+
+;; Evaluates an expression to a value.
+;; Follows the call-by-value evaluation strategy.
+(define/contract (call-by-value expr) (-> expr? value?)
+ (cbv-core expr #hash() (make-hash)))
+(define (cbv-core expr Γ Σ) ; ℓ
+ (match expr
+ ['sole 'sole]
+ [n #:when (natural? n) n]
+ [b #:when (boolean? b) b]
+ [p #:when (dict-has-key? Σ p) p]
+ [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+
+ [`(,e : ,t)
+ (cbv-core e Γ Σ)]
+ [`(type ,t1 ,t2 ,e)
+ (cbv-core e (dict-set Γ `(type ,t1) t2) Σ)]
+
+ ; The (level ...) syntax introduces new level *variables*.
+ [`(level ,l ,e)
+ (let ([v (cbv-core e (dict-set Γ `(level ,l) 'level) Σ)])
+ (dealloc! Σ l) v)] ; they are then freed at the end of scope
+ [`(,e ⇑ ,l)
+ (cbv-core e Γ Σ)]
+
+ [`(new ,e)
+ (let ([p (alloc! Σ (level-expr e))])
+ (write! Σ p (cbv-core e Γ Σ)))]
+ [`(! ,e)
+ (match (cbv-core e Γ Σ)
+ [`(ptr ,l ,a) (read! Σ `(ptr ,l ,a))]
+ [e (err (format "attempting to deref unknown expression ~a, expected ptr" e))])]
+ [`(set ,e1 ,e2) ; FIXME: we do NOT check levels before writing here
+ (match (cbv-core e1 Γ Σ)
+ [`(ptr ,l ,a) (write! Σ `(ptr ,l ,a) (cbv-core e2 Γ Σ))]
+ [e (err (format "attempting to write to unknown expression ~a, expected ptr" e))])]
+
+ [`(inc ,e)
+ (match (cbv-core e Γ Σ)
+ [n #:when (natural? n) (+ n 1)]
+ [e (err (format "incrementing an unknown value ~a" e))])]
+ [`(if ,c ,e1 ,e2)
+ (match (cbv-core c Γ Σ)
+ ['#t (cbv-core e1 Γ Σ)]
+ ['#f (cbv-core e2 Γ Σ)]
+ [e (err (format "calling if on unknown expression ~a" e))])]
+
+ [`(pair ,e1 ,e2)
+ `(pair ,(cbv-core e1 Γ Σ) ,(cbv-core e2 Γ Σ))]
+ [`(car ,e)
+ (match (cbv-core e Γ Σ)
+ [`(pair ,e1 ,e2) e1]
+ [e (err (format "calling car on unknown expression ~a" e))])]
+ [`(cdr ,e)
+ (match (cbv-core e Γ Σ)
+ [`(pair ,e1 ,e2) e2]
+ [e (err (format "calling cdr on unknown expression ~a" e))])]
+
+ [`(inl ,e)
+ `(inl ,(cbv-core e Γ Σ))]
+ [`(inr ,e)
+ `(inr ,(cbv-core e Γ Σ))]
+ [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+ (match (cbv-core e Γ Σ)
+ [`(inl ,e) (cbv-core e1 (dict-set Γ x1 e) Σ)]
+ [`(inr ,e) (cbv-core e2 (dict-set Γ x2 e) Σ)]
+ [e (err (format "calling case on unknown expression ~a" e))])]
+
+ [`(fold ,e) `(fold ,(cbv-core e Γ Σ))]
+ [`(unfold ,e)
+ (match (cbv-core e Γ Σ)
+ [`(fold ,e) e]
+ [e (err (format "attempting to unfold unknown expression ~a" e))])]
+
+ [`(λ (,x : ,t) ,e)
+ `(λ (,x : ,t) ,e ,Γ)]
+ [`(,e1 ,e2)
+ (match (cbv-core e1 Γ Σ)
+ [`(λ (,x : ,t) ,e1 ,env)
+ (cbv-core e1 (dict-set env x (cbv-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))]))
+
+;; Checks that an expression is of a type, and returns #t or #f, or a bubbled-up error.
+;; `with` must be a type in weak-head normal form for structural matching.
+(define/contract (check expr with) (-> expr? type? boolean?)
+ (check-core expr with #hash()))
+(define (check-core expr with Γ)
+ (match expr
+ ['sole 'Unit]
+ [n #:when (natural? n) 'Nat]
+ [b #:when (boolean? b) 'Bool]
+ ; We expand into weak-head normal form as the binding may be whatever.
+ [x #:when (dict-has-key? Γ x)
+ (expand-whnf (dict-ref Γ x) Γ)]
+
+ [`(type ,t1 ,t2 ,e)
+ (check-core e with (dict-set Γ `(type ,t1) t2))]
+
+ [`(level ,l ,e) ; We add the level to the context just to note it is valid.
+ (check-core e with (dict-set Γ `(level ,l) 'level))]
+
+ [`(new ,e)
+ (match with
+ [`(Ref ,t) (check-core e t Γ)]
+ [_ #f])]
+ [`(! ,e)
+ (check-core e `(Ref ,with) Γ)]
+
+ [`(if ,c ,e1 ,e2)
+ (and (check-core c 'Bool Γ)
+ (check-core e1 with Γ) (check-core e2 with Γ))]
+
+ [`(pair ,e1 ,e2)
+ (match with
+ [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
+ [_ #f])]
+
+ [`(inl ,e)
+ (match with
+ [`(,t1 ⊕ ,t2) (check-core e t1 Γ)]
+ [_ #f])]
+ [`(inr ,e)
+ (match with
+ [`(,t1 ⊕ ,t2) (check-core e t2 Γ)]
+ [_ #f])]
+ ; We do not technically need case in check form.
+ ; We keep it here to avoid needing type annotations on `c`.
+ [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+ (match (infer-core c Γ)
+ [`(,a1 ⊕ ,a2)
+ (and (check-core e1 with (dict-set Γ x1 a1))
+ (check-core e2 with (dict-set Γ x2 a2)))]
+ [_ #f])]
+
+ [`(fold ,e)
+ (match with
+ [`(μ ,x ,t) (check-core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))]
+ [_ #f])]
+
+ [`(λ (,x : ,t) ,e)
+ (match with
+ [`(,t1 → ,l ,t2) ; KNOB
+ (and (equiv-type t t1 Γ) (check-core e t2 (dict-set Γ x t))
+ (> l (level-expr e (dict-set Γ x t1))))]
+ [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
+ [_ #f])]
+
+ [_ (equiv-type (infer-core expr Γ) with Γ)]))
+
+;; Infers a type from a given expression, if possible. Errors out otherwise.
+;; Returns a type in weak-head normal form for structural matching.
+(define/contract (infer expr) (-> expr? type?)
+ (infer-core expr #hash()))
+;; Γ is our context: a dictionary from symbols to types??? i forget actually
+;; note: our context plays many roles.
+(define (infer-core expr Γ)
+ (match expr
+ ['sole 'Unit]
+ [n #:when (natural? n) 'Nat]
+ [b #:when (boolean? b) 'Bool]
+ ; We expand into weak-head normal form as the binding may be to another binding.
+ [x #:when (dict-has-key? Γ x)
+ (expand-whnf (dict-ref Γ x) Γ)]
+
+ [`(type ,t1 ,t2 ,e)
+ (infer-core e (dict-set Γ `(type ,t1) t2))]
+ [`(,e : ,t)
+ (if (check-core e (expand-whnf t Γ) Γ) (expand-whnf t Γ)
+ (err (format "expression ~a is not of annotated type ~a" e t)))]
+
+ [`(level ,l ,e) ; We add the level to the context just to note it is valid.
+ (infer-core e (dict-set Γ `(level ,l) 'level))]
+ [`(,e ⇑ ,l) ; We retrieve the level from the context to check it is valid.
+ (if (dict-has-key? Γ `(level ,(level-base l)))
+ (infer-core e Γ)
+ (err (format "level ~a not found in context, was it introduced?")))]
+
+ [`(new ,e)
+ `(Ref ,(infer-core e Γ))]
+ [`(ptr ,a)
+ (err (format "cannot infer type from raw pointer ~a" `(ptr ,a)))]
+ [`(! ,e)
+ (match (infer-core e Γ)
+ [`(Ref ,t) t]
+ [t (err (format "attempting to deref term ~a of type ~a" e t))])]
+ [`(set ,e1 ,e2) ; FIXME: this does not account for explicit allocation syntax!
+ (match (infer-core e1 Γ) ; should we check levels?
+ [`(Ref ,t)
+ (if (check-core e2 t Γ) 'Unit
+ (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
+ e1 t e2 (infer-core e2 Γ))))]
+ [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
+
+ [`(inc ,e)
+ (if (check-core e 'Nat Γ) 'Nat
+ (err (format "calling inc on incorrect type ~a, expected Nat" (infer-core e Γ))))]
+ [`(if ,c ,e1 ,e2)
+ (if (check-core c 'Bool Γ)
+ (let ([t (infer-core e1 Γ)])
+ (if (check-core e2 t Γ) t
+ (err (format "if ~a is not of consistent type!"
+ `(if Bool ,t ,(infer-core e2 Γ))))))
+ (err (format "if ~a has incorrect type ~a on condition, expected Bool"
+ c (infer-core c Γ))))]
+
+ [`(pair ,e1 ,e2)
+ `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))]
+ [`(car ,e)
+ (match (infer-core e Γ)
+ [`(,t1 × ,t2) t1]
+ [t (err (format "calling car on incorrect type ~a, expected a product" t))])]
+ [`(cdr ,e)
+ (match (infer-core e Γ)
+ [`(,t1 × ,t2) t2]
+ [t (err (format "calling cdr on incorrect type ~a, expected a product" t))])]
+
+ [`(inl ,e)
+ (err (format "unable to infer the type of a raw inl"))]
+ [`(inr ,e)
+ (err (format "unable to infer the type of a raw inr"))]
+ [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+ (match (infer-core c Γ)
+ [`(,a1 ⊕ ,a2)
+ (let ([b1 (infer-core e1 (dict-set Γ x1 a1))]
+ [b2 (infer-core e2 (dict-set Γ x2 a2))])
+ (if (equiv-type b1 b2 Γ) b1
+ (err (format "case ~a is not of consistent type!"
+ `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))]
+ [t (err (format "case has incorrect type ~a on condition, expected a sum" t))])]
+
+ [`(unfold ,e)
+ (match (expand-whnf (infer-core e Γ) Γ)
+ [`(μ ,x ,t) (replace-type t x `(μ ,x ,t))]
+ [t (err (format "expected ~a to be of recursive type, got ~a" e t))])]
+
+ [`(λ (,x : ,t1) ,e) ; KNOB
+ (let* ([t2 (infer-core e (dict-set Γ x t1))]
+ [t1 (expand-whnf t1 Γ)] [l (+ 1 (level-expr e (dict-set Γ x t1)))])
+ `(,t1 → ,l ,t2))]
+ [`(,e1 ,e2)
+ (match (infer-core e1 Γ)
+ [`(,t1 → ,l ,t2) ; should we check levels here? probably redundant
+ (if (check-core e2 t1 Γ) t2
+ (err (format "inferred argument type ~a does not match arg ~a of type ~a"
+ t1 e2 (infer-core e2 Γ))))]
+ [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
+ [t (err (format "expected → type on application body, got ~a" t))])]
+
+ [_ (err (format "attempting to infer an unknown expression ~a" expr))]))