Elaborate Typed Jerboa def bodies into core IR
ober
b8e1b616a4acfb109e6789db46f3207c7f6ff489
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -81,9 +81,13 @@ Landed: Still open: -- Typed core IR adoption. The IR record types now live in - `(jerboa typed core)`; the checker and Rust emitter still walk surface - datums and need to be switched over. +- Typed core IR adoption. The IR record types live in `(jerboa typed core)` + and the checker now elaborates def bodies into IR via + `check-and-elaborate-typed-module` (each def's body is a `typed-ir-begin` + wrapping inferred `typed-ir-lit`/`typed-ir-var`/`typed-ir-let`/`typed-ir-if`/ + `typed-ir-match`/`typed-ir-call` nodes with pre-resolved call kinds). The + Rust emitter still walks surface datums and needs to be switched over to + consume the IR. - Import resolution between typed modules. - Structured Rust-to-Scheme error returns instead of conservative panic defaults. --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -146,8 +146,13 @@ Current landing: `typed-ir-if`, `typed-ir-match`, and a unified `typed-ir-call` covering primitives, typed function calls, record/variant operations, Option/Result constructors, and string builtins. Every node carries its inferred type and - optional source location. The checker and Rust emitter do not yet consume - the IR; that wiring is the next step. + optional source location. The checker now elaborates each def body into a + `typed-ir-begin` wrapping these IR nodes — exposed through + `check-and-elaborate-typed-module` (returns errors + ordered + `elaborated-def` records) and the per-def + `elaborate-typed-def-ir` helper. Pre-resolved call kinds and info travel on + `typed-ir-call` so the Rust emitter (next step) can lower without repeating + name lookups. - `(jerboa typed checker)` performs the first backend-neutral validation pass: duplicate names, export resolution, type-reference resolution, compound type arities, duplicate fields, duplicate params, duplicate variant cases, and a @@ -275,10 +280,10 @@ Code that has landed: The next model should continue in small commits with tests and docs per step. Highest-value next steps: -1. Continue the typed core IR rollout. The IR record types now live in - `(jerboa typed core)`; the next steps are to have the checker emit IR - alongside its existing type/effect output and then to switch the Rust - emitter to consume IR rather than re-walking surface datums. +1. Continue the typed core IR rollout. The IR record types live in + `(jerboa typed core)` and the checker now elaborates def bodies into IR via + `check-and-elaborate-typed-module`. The remaining step is to switch the + Rust emitter to consume IR rather than re-walking surface datums. 2. Resolve imports between typed modules. The checker currently handles calls within one typed module only; imported calls are intentionally unsupported. 3. Improve boundary semantics for Option/Result. They currently cross the FFI --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -12,6 +12,13 @@ typed-check-error-hint typed-check-error->string check-typed-module + check-and-elaborate-typed-module + elaborate-typed-def-ir + elaborated-def? + make-elaborated-def + elaborated-def-name + elaborated-def-decl + elaborated-def-body-ir typecheck-typed-library-form typed-module-valid?) @@ -19,10 +26,16 @@ (only (jerboa core) def defstruct) (only (jerboa reader) source-location? source-location-path source-location-line source-location-column) - (jerboa typed parser)) + (jerboa typed parser) + (jerboa typed core)) (defstruct typed-check-error (kind message detail source)) - (defstruct typed-call-sig (param-types return-type effects)) + (defstruct typed-call-sig (param-types return-type effects kind info)) + (defstruct elaborated-def (name decl body-ir)) + + ;; Pull-out helpers for extracting type/source from optional IR nodes. + (def (ir-type ir) (and ir (typed-ir-node-type ir))) + (def (ir-source ir) (and ir (typed-ir-node-source ir))) (def *call-env* (make-parameter '())) (def *variant-env* (make-parameter '())) @@ -328,16 +341,21 @@ (make-typed-call-sig (map typed-param-type (typed-def-params decl)) (typed-def-return-type decl) - (typed-def-effects decl))))) + (typed-def-effects decl) + 'function + '())))) (def builtin-call-signatures (list (cons 'string-length - (make-typed-call-sig (list 'String) 'Nat '())) + (make-typed-call-sig (list 'String) 'Nat '() + 'string-length '())) (cons 'string-append - (make-typed-call-sig (list 'String 'String) 'String '())) + (make-typed-call-sig (list 'String 'String) 'String '() + 'string-append '())) (cons 'bytevector-length - (make-typed-call-sig (list 'Bytes) 'Nat '())))) + (make-typed-call-sig (list 'Bytes) 'Nat '() + 'bytevector-length '())))) (def (field-types fields) (map typed-field-type fields)) @@ -355,14 +373,20 @@ (make-typed-call-sig (list record-name) field-type - '()))]) + '() + 'record-accessor + (list (cons 'record record-name) + (cons 'field field-name))))]) (if (typed-field-mutable? field) (list accessor (cons (symbol-append accessor-name "-set!") (make-typed-call-sig (list record-name field-type) 'Unit - '()))) + '() + 'record-setter + (list (cons 'record record-name) + (cons 'field field-name))))) (list accessor)))) (typed-record-fields record)))) @@ -372,9 +396,13 @@ (append (list (cons (symbol-append "make-" record-name) - (make-typed-call-sig (field-types fields) record-name '())) + (make-typed-call-sig (field-types fields) record-name '() + 'record-ctor + (list (cons 'record record-name)))) (cons (symbol-append record-name "?") - (make-typed-call-sig (list any-value-type) 'Bool '()))) + (make-typed-call-sig (list any-value-type) 'Bool '() + 'record-pred + (list (cons 'record record-name))))) (record-field-call-signatures record)))) (def (variant-case-call-signature variant-name case) @@ -382,13 +410,18 @@ (make-typed-call-sig (field-types (typed-variant-case-fields case)) variant-name - '()))) + '() + 'variant-ctor + (list (cons 'variant variant-name) + (cons 'case (typed-variant-case-name case)))))) (def (variant-call-signatures variant) (let ([variant-name (typed-variant-name variant)]) (cons (cons (symbol-append variant-name "?") - (make-typed-call-sig (list any-value-type) 'Bool '())) + (make-typed-call-sig (list any-value-type) 'Bool '() + 'variant-pred + (list (cons 'variant variant-name)))) (map (lambda (case) (variant-case-call-signature variant-name case)) (typed-variant-cases variant))))) @@ -495,18 +528,30 @@ (check-type (typed-def-return-type def) type-names) (check-def-body def type-names))) - (def (infer-body exprs env type-names) - (cond - [(null? exprs) (values 'Unit '())] - [else - (let loop ([rest exprs] [errors '()] [last-type 'Unit]) - (if (null? rest) - (values last-type (reverse errors)) - (let-values ([(expr-type expr-errors) - (infer-expression (car rest) env type-names)]) - (loop (cdr rest) - (append (reverse expr-errors) errors) - expr-type))))])) + (def (infer-body exprs env type-names . src*) + (let ([src (if (pair? src*) (car src*) #f)]) + (cond + [(null? exprs) + (values (make-typed-ir-begin 'Unit src '()) '())] + [else + (let loop ([rest exprs] [irs '()] [errors '()]) + (if (null? rest) + (let* ([ir-list (reverse irs)] + [last-ir (and (pair? ir-list) + (let lp ([xs ir-list]) + (if (null? (cdr xs)) + (car xs) + (lp (cdr xs)))))] + [last-type (ir-type last-ir)]) + (values + (and last-type + (make-typed-ir-begin last-type src ir-list)) + (reverse errors))) + (let-values ([(ir expr-errors) + (infer-expression (car rest) env type-names)]) + (loop (cdr rest) + (cons ir irs) + (append (reverse expr-errors) errors)))))]))) (def (extend-env name type env) (cons (cons name type) env)) @@ -571,22 +616,37 @@ (if (or (not (null? shape-errors)) (not (null? duplicate-name-errors))) (values #f (append duplicate-name-errors shape-errors)) - (let loop ([rest binding-list] [local-env env] [errors '()]) + (let loop ([rest binding-list] + [local-env env] + [ir-bindings '()] + [errors '()]) (if (null? rest) - (let-values ([(body-type body-errors) - (infer-body body local-env type-names)]) - (values body-type (append (reverse errors) body-errors))) + (let-values ([(body-ir body-errors) + (infer-body body local-env type-names + (expr-source expr))]) + (let ([body-type (ir-type body-ir)]) + (values + (and body-type + (make-typed-ir-let body-type (expr-source expr) + (reverse ir-bindings) + (if body-ir + (typed-ir-begin-exprs body-ir) + '()))) + (append (reverse errors) body-errors)))) (let* ([binding (car rest)] [binding-value (expr-value binding)] [name (expr-value (car binding-value))] [value-expr (cadr binding-value)]) - (let-values ([(value-type value-errors) + (let-values ([(value-ir value-errors) (infer-expression value-expr env type-names)]) - (loop (cdr rest) - (if value-type - (extend-env name value-type local-env) - local-env) - (append (reverse value-errors) errors))))))))])) + (let ([value-type (ir-type value-ir)]) + (loop (cdr rest) + (if value-type + (extend-env name value-type local-env) + local-env) + (cons (make-typed-ir-binding name value-ir) + ir-bindings) + (append (reverse value-errors) errors)))))))))])) (def (infer-if args env type-names expr) (if (not (= (length args) 3)) @@ -594,26 +654,33 @@ (list (error-at expr 'bad-if "if expects condition, then branch, and else branch" expr))) - (let-values ([(cond-type cond-errors) + (let-values ([(cond-ir cond-errors) (infer-expression (car args) env type-names)] - [(then-type then-errors) + [(then-ir then-errors) (infer-expression (cadr args) env type-names)] - [(else-type else-errors) + [(else-ir else-errors) (infer-expression (caddr args) env type-names)]) - (let ([condition-errors - (if (and cond-type (not (eq? cond-type 'Bool))) - (list (error-at (car args) 'condition-type-mismatch - "if condition must be Bool" - cond-type)) - '())] - [branch-errors - (if (and then-type else-type (not (equal? then-type else-type))) - (list (error-at expr 'branch-type-mismatch - "if branches must have the same type" - (list then-type else-type))) - '())]) + (let* ([cond-type (ir-type cond-ir)] + [then-type (ir-type then-ir)] + [else-type (ir-type else-ir)] + [condition-errors + (if (and cond-type (not (eq? cond-type 'Bool))) + (list (error-at (car args) 'condition-type-mismatch + "if condition must be Bool" + cond-type)) + '())] + [branch-errors + (if (and then-type else-type (not (equal? then-type else-type))) + (list (error-at expr 'branch-type-mismatch + "if branches must have the same type" + (list then-type else-type))) + '())] + [ok? (and (null? branch-errors) + (null? condition-errors) + cond-ir then-ir else-ir then-type)]) (values - (if (null? branch-errors) then-type #f) + (and ok? (make-typed-ir-if then-type (expr-source expr) + cond-ir then-ir else-ir)) (append cond-errors then-errors else-errors condition-errors branch-errors)))))) @@ -687,21 +754,21 @@ [case-decl (lookup-variant-case variant case-name)]) (cond [(not case-decl) - (values #f + (values #f #f (list (error-at (car pattern-list) 'unknown-match-case "match pattern is not a case of the variant" case-name)) #f #f)] [(not (and (for-all expr-symbol? vars))) - (values #f + (values #f #f (list (error-at pattern 'bad-match-pattern "match case fields must be symbols" clause)) case-name #f)] [(memq case-name seen) - (values #f + (values #f #f (list (error-at (car pattern-list) 'duplicate-match-case "duplicate variant case in match" case-name)) @@ -724,29 +791,43 @@ (pattern-binding-names var-values))]) (if (or (not (null? arity-errors)) (not (null? duplicate-binding-errors))) - (values #f + (values #f #f (append duplicate-binding-errors arity-errors) case-name #f) - (let-values ([(body-type body-errors) + (let-values ([(body-ir body-errors) (infer-body body (extend-env* var-values case-field-types env) - type-names)]) - (values body-type body-errors case-name #f))))]))) + type-names + (expr-source clause))]) + (let ([body-type (ir-type body-ir)]) + (values + (and body-type + (make-typed-ir-match-clause + case-name + var-values + case-field-types + (if body-ir + (typed-ir-begin-exprs body-ir) + '()))) + body-type + body-errors + case-name + #f)))))]))) (def (infer-match-clause clause variant env type-names seen) (let ([cv (expr-value clause)]) (cond [(or (not (pair? cv)) (not (list? cv))) - (values #f + (values #f #f (list (error-at clause 'bad-match-clause "match clause must be a proper list" clause)) #f #f)] [(null? (cdr cv)) - (values #f + (values #f #f (list (error-at clause 'bad-match-clause "match clause needs a body" clause)) @@ -757,27 +838,36 @@ [body (cdr cv)]) (cond [(fallback-match-pattern? pattern) - (let-values ([(body-type body-errors) - (infer-body body env type-names)]) - (values body-type body-errors #f #t))] + (let-values ([(body-ir body-errors) + (infer-body body env type-names + (expr-source clause))]) + (let ([body-type (ir-type body-ir)]) + (values + (and body-ir (typed-ir-begin-exprs body-ir)) + body-type + body-errors + #f + #t)))] [(and (expr-pair? pattern) (expr-list? pattern) (expr-symbol? (car (expr-value pattern)))) (infer-match-case-clause clause pattern body variant env type-names seen)] [else - (values #f + (values #f #f (list (error-at pattern 'bad-match-pattern "match pattern must be a variant case, _, or else" pattern)) #f #f)]))]))) - (def (infer-match-clauses clauses variant env type-names expr) + (def (infer-match-clauses target-ir target-type clauses variant env type-names expr) (let loop ([rest clauses] [seen '()] [fallback? #f] [branch-types '()] + [case-clauses '()] + [default-ir #f] [errors '()]) (if (null? rest) (let* ([ordered-types (reverse branch-types)] @@ -795,17 +885,33 @@ (list (error-at expr 'non-exhaustive-match "match does not cover all variant cases" missing)))] - [result-type (consistent-branch-type ordered-types)]) + [result-type (consistent-branch-type ordered-types)] + [all-errors + (append errors exhaustiveness-errors branch-errors)] + [ok? (and (null? all-errors) result-type)]) (values - (if (null? branch-errors) result-type #f) - (append errors exhaustiveness-errors branch-errors))) - (let-values ([(branch-type clause-errors case-name fallback-clause?) + (and ok? + (make-typed-ir-match + result-type + (expr-source expr) + target-ir + target-type + (reverse case-clauses) + default-ir)) + all-errors)) + (let-values ([(clause-ir branch-type clause-errors case-name fallback-clause?) (infer-match-clause (car rest) variant env type-names seen)]) (loop (cdr rest) (if case-name (add-unique case-name seen) seen) (or fallback? fallback-clause?) (cons branch-type branch-types) + (if (and clause-ir (not fallback-clause?)) + (cons clause-ir case-clauses) + case-clauses) + (if (and clause-ir fallback-clause?) + clause-ir + default-ir) (append errors clause-errors)))))) (def (infer-match args env type-names expr) @@ -814,9 +920,10 @@ (list (error-at expr 'bad-match "match expects a target expression and at least one clause" expr))) - (let-values ([(target-type target-errors) + (let-values ([(target-ir target-errors) (infer-expression (car args) env type-names)]) - (let ([variant (and target-type (lookup-variant target-type))]) + (let* ([target-type (ir-type target-ir)] + [variant (and target-type (lookup-variant target-type))]) (if (not variant) (values #f (append @@ -826,10 +933,11 @@ "match target must have a declared variant type" target-type)) '()))) - (let-values ([(result-type clause-errors) + (let-values ([(result-ir clause-errors) (infer-match-clauses + target-ir target-type (cdr args) variant env type-names expr)]) - (values result-type + (values result-ir (append target-errors clause-errors)))))))) (def (numeric-type? type) @@ -843,15 +951,26 @@ [else 'Nat])) (def (infer-args args env type-names) - (let loop ([rest args] [types '()] [errors '()]) + ;; Returns (values <list of IR or #f per arg> errors). + (let loop ([rest args] [irs '()] [errors '()]) (if (null? rest) - (values (reverse types) (reverse errors)) - (let-values ([(type arg-errors) + (values (reverse irs) (reverse errors)) + (let-values ([(ir arg-errors) (infer-expression (car rest) env type-names)]) (loop (cdr rest) - (cons type types) + (cons ir irs) (append (reverse arg-errors) errors)))))) + (def (ir-list-types irs) + (map ir-type irs)) + + (def (all-irs-valid? irs) + (let loop ([rest irs]) + (cond + [(null? rest) #t] + [(not (car rest)) #f] + [else (loop (cdr rest))]))) + (def (operand-type-errors expected-kind types arg-exprs detail) (let loop ([rest types] [rest-exprs arg-exprs] [out '()]) (cond @@ -889,12 +1008,15 @@ (list (error-at expr 'bad-primitive-arity "arithmetic primitive needs at least one operand" expr))) - (let-values ([(types errors) (infer-args args env type-names)]) - (let ([operand-errors (operand-type-errors 'numeric types args expr)]) + (let-values ([(arg-irs errors) (infer-args args env type-names)]) + (let* ([types (ir-list-types arg-irs)] + [operand-errors (operand-type-errors 'numeric types args expr)] + [ok? (and (null? errors) (null? operand-errors) + (all-irs-valid? arg-irs))]) (values - (if (and (null? errors) (null? operand-errors)) - (merge-numeric-types types) - #f) + (and ok? + (make-typed-ir-call (merge-numeric-types types) + (expr-source expr) 'prim-arith op arg-irs '())) (append errors operand-errors)))))) (def (infer-comparison op args env type-names expr) @@ -903,10 +1025,15 @@ (list (error-at expr 'bad-primitive-arity "comparison primitive needs exactly two operands" expr))) - (let-values ([(types errors) (infer-args args env type-names)]) - (let ([operand-errors (operand-type-errors 'numeric types args expr)]) + (let-values ([(arg-irs errors) (infer-args args env type-names)]) + (let* ([types (ir-list-types arg-irs)] + [operand-errors (operand-type-errors 'numeric types args expr)] + [ok? (and (null? errors) (null? operand-errors) + (all-irs-valid? arg-irs))]) (values - (if (and (null? errors) (null? operand-errors)) 'Bool #f) + (and ok? + (make-typed-ir-call 'Bool (expr-source expr) + 'prim-cmp op arg-irs '())) (append errors operand-errors)))))) (def (infer-equality args env type-names expr) @@ -915,13 +1042,19 @@ (list (error-at expr 'bad-primitive-arity "equal? needs exactly two operands" expr))) - (let-values ([(types errors) (infer-args args env type-names)]) - (let ([same-type? - (and (car types) - (cadr types) - (equal? (car types) (cadr types)))]) + (let-values ([(arg-irs errors) (infer-args args env type-names)]) + (let* ([types (ir-list-types arg-irs)] + [same-type? + (and (car types) + (cadr types) + (equal? (car types) (cadr types)))] + [ok? (and (null? errors) same-type? + (all-irs-valid? arg-irs))]) (values - (if (and (null? errors) same-type?) 'Bool #f) + (and ok? + (make-typed-ir-call 'Bool (expr-source expr) + 'prim-eq 'equal? arg-irs + (list (cons 'operand-type (car types))))) (append errors (if (or (not (null? errors)) same-type?) @@ -936,9 +1069,13 @@ (list (error-at expr 'bad-primitive-arity "debug-string needs exactly one operand" expr))) - (let-values ([(type errors) (infer-expression (car args) env type-names)]) - (values (and type (null? errors) 'String) - errors)))) + (let-values ([(arg-ir errors) (infer-expression (car args) env type-names)]) + (let ([arg-type (ir-type arg-ir)]) + (values (and arg-type (null? errors) + (make-typed-ir-call 'String (expr-source expr) + 'debug-string 'debug-string (list arg-ir) + (list (cons 'operand-type arg-type)))) + errors))))) (def (infer-boolean op args env type-names expr) (cond @@ -948,10 +1085,15 @@ "not needs exactly one operand" expr)))] [else - (let-values ([(types errors) (infer-args args env type-names)]) - (let ([operand-errors (operand-type-errors 'Bool types args expr)]) + (let-values ([(arg-irs errors) (infer-args args env type-names)]) + (let* ([types (ir-list-types arg-irs)] + [operand-errors (operand-type-errors 'Bool types args expr)] + [ok? (and (null? errors) (null? operand-errors) + (all-irs-valid? arg-irs))]) (values - (if (and (null? errors) (null? operand-errors)) 'Bool #f) + (and ok? + (make-typed-ir-call 'Bool (expr-source expr) + 'prim-bool op arg-irs '())) (append errors operand-errors))))])) (def (bad-constructor-arity expr name expected args) @@ -962,43 +1104,64 @@ (def (infer-option-some args env type-names expr) (if (not (= (length args) 1)) (values #f (bad-constructor-arity expr 'option-some 1 args)) - (let-values ([(value-type errors) + (let-values ([(value-ir errors) (infer-expression (car args) env type-names)]) - (values (and value-type (list 'Option value-type)) - errors)))) + (let ([value-type (ir-type value-ir)]) + (values + (and value-type + (make-typed-ir-call (list 'Option value-type) + (expr-source expr) 'option-some 'option-some + (list value-ir) + (list (cons 'inner-type value-type)))) + errors))))) (def (infer-option-none args env type-names expr) (if (not (= (length args) 1)) (values #f (bad-constructor-arity expr 'option-none 1 args)) (let* ([type-arg (strip-source-annotations (car args))] [errors (check-type type-arg type-names)]) - (values (and (null? errors) (list 'Option type-arg)) - errors)))) + (values + (and (null? errors) + (make-typed-ir-call (list 'Option type-arg) + (expr-source expr) 'option-none 'option-none + '() + (list (cons 'inner-type type-arg)))) + errors)))) (def (infer-result-ok args env type-names expr) (if (not (= (length args) 2)) (values #f (bad-constructor-arity expr 'result-ok 2 args)) - (let-values ([(value-type value-errors) + (let-values ([(value-ir value-errors) (infer-expression (car args) env type-names)]) - (let* ([err-type (strip-source-annotations (cadr args))] + (let* ([value-type (ir-type value-ir)] + [err-type (strip-source-annotations (cadr args))] [error-type-errors (check-type err-type type-names)]) (values (and value-type (null? error-type-errors) - (list 'Result value-type err-type)) + (make-typed-ir-call (list 'Result value-type err-type) + (expr-source expr) 'result-ok 'result-ok + (list value-ir) + (list (cons 'value-type value-type) + (cons 'error-type err-type)))) (append value-errors error-type-errors)))))) (def (infer-result-err args env type-names expr) (if (not (= (length args) 2)) (values #f (bad-constructor-arity expr 'result-err 2 args)) - (let-values ([(error-type error-errors) + (let-values ([(error-ir error-errors) (infer-expression (cadr args) env type-names)]) - (let* ([val-type (strip-source-annotations (car args))] + (let* ([error-type (ir-type error-ir)] + [val-type (strip-source-annotations (car args))] [value-type-errors (check-type val-type type-names)]) (values (and error-type (null? value-type-errors) - (list 'Result val-type error-type)) + (make-typed-ir-call (list 'Result val-type error-type) + (expr-source expr) 'result-err 'result-err + (list error-ir) + (list (cons 'value-type val-type) + (cons 'error-type error-type)))) (append value-type-errors error-errors)))))) (def (argument-type-errors name expected-types actual-types arg-exprs) @@ -1179,38 +1342,53 @@ (list (error-at expr 'bad-call-arity "function call arity does not match definition" (list name (length expected-types) (length args))))) - (let-values ([(actual-types arg-errors) + (let-values ([(arg-irs arg-errors) (infer-args args env type-names)]) - (let ([type-errors - (argument-type-errors - name expected-types actual-types args)] - [effect-errors - (call-effect-errors - expr - name - (typed-call-sig-effects sig) - (*current-effects*))]) + (let* ([actual-types (ir-list-types arg-irs)] + [type-errors + (argument-type-errors + name expected-types actual-types args)] + [effect-errors + (call-effect-errors + expr + name + (typed-call-sig-effects sig) + (*current-effects*))] + [ok? (and (null? arg-errors) + (null? type-errors) + (null? effect-errors) + (all-irs-valid? arg-irs))]) (values - (if (and (null? arg-errors) - (null? type-errors) - (null? effect-errors)) - (typed-call-sig-return-type sig) - #f) + (and ok? + (make-typed-ir-call + (typed-call-sig-return-type sig) + (expr-source expr) + (typed-call-sig-kind sig) + name + arg-irs + (typed-call-sig-info sig))) (append arg-errors type-errors effect-errors))))))))) (def (infer-expression expr env type-names) - (let ([value (expr-value expr)]) + (let ([value (expr-value expr)] + [src (expr-source expr)]) (cond - [(boolean? value) (values 'Bool '())] - [(char? value) (values 'Char '())] - [(string? value) (values 'String '())] - [(bytevector? value) (values 'Bytes '())] + [(boolean? value) + (values (make-typed-ir-lit 'Bool src value) '())] + [(char? value) + (values (make-typed-ir-lit 'Char src value) '())] + [(string? value) + (values (make-typed-ir-lit 'String src value) '())] + [(bytevector? value) + (values (make-typed-ir-lit 'Bytes src value) '())] [(integer? value) - (values (if (>= value 0) 'Nat 'Int) '())] + (values + (make-typed-ir-lit (if (>= value 0) 'Nat 'Int) src value) + '())] [(symbol? value) (let ([type (lookup-name value env)]) (if type - (values type '()) + (values (make-typed-ir-var type src value) '()) (values #f (list (error-at expr 'unknown-value "unknown value in expression" @@ -1220,7 +1398,7 @@ [args (expr-args expr)]) (case head [(begin) - (infer-body args env type-names)] + (infer-body args env type-names src)] [(let) (if (< (length args) 2) (values #f @@ -1263,34 +1441,51 @@ "expression is not in the typed checker subset yet" expr)))]))) + ;; Accumulator parameter for elaborated def IRs collected during checking. + ;; The value is a box containing an alist of (def-name . body-ir) entries + ;; in declaration order (entries are consed during checking and reversed + ;; at the end). When #f, no elaboration is collected (the existing + ;; check-only path). + (def *elaboration-acc* (make-parameter #f)) + + (def (record-elaboration! def body-ir) + (let ([acc (*elaboration-acc*)]) + (when (and acc body-ir) + (set-box! acc + (cons (cons (typed-def-name def) body-ir) (unbox acc)))))) + (def (check-def-body def type-names) (let* ([env (param-env (typed-def-params def))] [body (typed-def-body def)] [last-expr (and (pair? body) (let loop ([rest body]) (if (null? (cdr rest)) (car rest) (loop (cdr rest)))))]) - (let-values ([(actual-type body-errors) + (let-values ([(body-ir body-errors) (parameterize ([*current-effects* (normalize-effects (typed-def-effects def))]) - (infer-body body env type-names))] + (infer-body body env type-names (typed-def-source def)))] [(_moved ownership-errors) (check-ownership-body body env '())]) - (append - body-errors - ownership-errors - (if (and actual-type - (valid-type? (typed-def-return-type def) type-names) - (not (type-assignable? actual-type - (typed-def-return-type def)))) - (list (make-check-error 'return-type-mismatch - "function body type does not match declared return type" - (list (typed-def-name def) - (typed-def-return-type def) - actual-type) - (or (and last-expr (expr-source last-expr)) - (typed-def-source def)))) - '()))))) + (let* ([actual-type (ir-type body-ir)] + [return-type-errors + (if (and actual-type + (valid-type? (typed-def-return-type def) type-names) + (not (type-assignable? actual-type + (typed-def-return-type def)))) + (list (make-check-error 'return-type-mismatch + "function body type does not match declared return type" + (list (typed-def-name def) + (typed-def-return-type def) + actual-type) + (or (and last-expr (expr-source last-expr)) + (typed-def-source def)))) + '())] + [all-errors + (append body-errors ownership-errors return-type-errors)]) + (when (null? all-errors) + (record-elaboration! def body-ir)) + all-errors)))) (def (check-declaration decl type-names) (cond @@ -1336,6 +1531,46 @@ (lambda (decl) (check-declaration decl type-names)) declarations))))) + (def (check-and-elaborate-typed-module module) + ;; Returns (values errors elaborated-defs), where elaborated-defs is a + ;; list of elaborated-def records in declaration order. Only defs whose + ;; bodies passed all checks appear in the list; their body-ir field is a + ;; typed-ir-begin node carrying the inferred types. + (let ([acc (box '())]) + (let ([errors + (parameterize ([*elaboration-acc* acc]) + (check-typed-module module))]) + (let* ([entries (reverse (unbox acc))] + [defs + (let loop ([rest (typed-module-declarations module)] [out '()]) + (cond + [(null? rest) (reverse out)] + [(typed-def? (car rest)) + (let* ([def (car rest)] + [name (typed-def-name def)] + [entry (assq name entries)]) + (loop (cdr rest) + (if entry + (cons (make-elaborated-def + name def (cdr entry)) + out) + out)))] + [else (loop (cdr rest) out)]))]) + (values errors defs))))) + + (def (elaborate-typed-def-ir def module) + ;; Convenience for callers that want a single def's body IR. + (let-values ([(errors defs) + (check-and-elaborate-typed-module module)]) + (cond + [(not (null? errors)) #f] + [else + (let ([entry (find (lambda (ed) + (eq? (elaborated-def-name ed) + (typed-def-name def))) + defs)]) + (and entry (elaborated-def-body-ir entry)))]))) + (def (typecheck-typed-library-form form) (check-typed-module (parse-typed-library form))) --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -4,7 +4,8 @@ (import (chezscheme) (jerboa reader) (jerboa typed parser) - (jerboa typed checker)) + (jerboa typed checker) + (jerboa typed core)) (define pass 0) (define fail 0) @@ -1037,6 +1038,134 @@ (string=? (substring text 0 prefix-len) "diag.ss:"))))) #t) +;; --- IR elaboration ------------------------------------------------------ + +(define (elab-defs form) + (let-values ([(errors defs) + (check-and-elaborate-typed-module (parse-typed-library form))]) + (and (null? errors) defs))) + +(define (find-elab defs name) + (let loop ([rest defs]) + (cond + [(null? rest) #f] + [(eq? (elaborated-def-name (car rest)) name) (car rest)] + [else (loop (cdr rest))]))) + +(define (body-expr defs name) + ;; A def body's IR is wrapped in a typed-ir-begin; pull the (single) inner expr. + (let* ([ed (find-elab defs name)] + [ir (and ed (elaborated-def-body-ir ed))]) + (cond + [(and ir (typed-ir-begin? ir)) + (let ([exprs (typed-ir-begin-exprs ir)]) + (and (pair? exprs) (car (reverse exprs))))] + [else ir]))) + +(define ir-form + '(typed-library (ir test sample) + (export id-nat add-nats pick branch describe ok-num) + + (record Pair-N + ((a : Nat) (b : Nat))) + + (variant Tag + (TA (n : Nat)) + (TB)) + + (def (id-nat (x : Nat)) : Nat x) + + (def (add-nats (a : Nat) (b : Nat)) : Nat (+ a b)) + + (def (pick (cond? : Bool) (a : Nat) (b : Nat)) : Nat + (if cond? a b)) + + (def (branch (t : Tag)) : Nat + (match t + [(TA n) n] + [(TB) 0])) + + (def (describe (n : Nat)) : String + (debug-string n)) + + (def (ok-num (n : Nat)) : (Result Nat String) + (result-ok n String)))) + +(test "elab returns defs in declaration order" + (map elaborated-def-name (elab-defs ir-form)) + '(id-nat add-nats pick branch describe ok-num)) + +(test "elab id-nat body is a typed-ir-var" + (typed-ir-var? (body-expr (elab-defs ir-form) 'id-nat)) + #t) + +(test "elab id-nat body type is Nat" + (typed-ir-node-type (body-expr (elab-defs ir-form) 'id-nat)) + 'Nat) + +(test "elab add-nats body is a call with kind prim-arith" + (let ([ir (body-expr (elab-defs ir-form) 'add-nats)]) + (and (typed-ir-call? ir) + (typed-ir-call-kind ir))) + 'prim-arith) + +(test "elab add-nats call operator is +" + (typed-ir-call-operator (body-expr (elab-defs ir-form) 'add-nats)) + '+) + +(test "elab pick body is a typed-ir-if" + (typed-ir-if? (body-expr (elab-defs ir-form) 'pick)) + #t) + +(test "elab pick if type is Nat" + (typed-ir-node-type (body-expr (elab-defs ir-form) 'pick))