Check Typed Jerboa records and variants
ober
6ed02595a027751de7792a10d6b78f4b0ea1e2fd
--- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -148,10 +148,10 @@ Current landing: `def` forms with typed parameters and `:` or `->` return markers. - This is still a front-end milestone. Function-body checking currently covers literals, variables, `begin`, simple `let`, `if`, arithmetic primitives, - numeric comparisons, boolean primitives, and calls to typed functions defined - in the same module. Imported calls and richer forms are reported as - unsupported. It does not yet resolve imports, lower to typed core IR, or emit - Rust/LLVM. + numeric comparisons, boolean primitives, calls to typed functions defined in + the same module, and generated record/variant operations. Imported calls and + richer forms are reported as unsupported. It does not yet resolve imports, + lower to typed core IR, or emit Rust/LLVM. ## Surface Syntax @@ -257,6 +257,10 @@ Generated operations: - Equality where all fields support equality - Debug formatting +The current checker recognizes constructor, predicate, accessor, and mutable +field setter calls for records declared in the same typed module. It checks +their arity, argument types, and return type flow before any backend exists. + ## Variants Variants should cover algebraic data types: @@ -280,6 +284,10 @@ Pattern matching should be exhaustive for typed variants: Non-exhaustive matches should be compile errors unless there is an explicit fallback branch. +The current checker recognizes variant constructors and the variant predicate +for variants declared in the same typed module. Exhaustive `match` checking is +still a later milestone. + ## Functions Function signatures should be explicit at exported boundaries: @@ -744,7 +752,9 @@ Minimum excluded features: arithmetic, comparison, and boolean primitive return checking landed. - Check function applications. Same-module typed function calls now check arity, argument types, and return type flow. -- Check records and variants. +- Check records and variants. Same-module record constructors, predicates, + accessors, mutable setters, variant constructors, and variant predicates now + check arity, argument types, and return type flow. - Check match exhaustiveness. - Produce useful errors. --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -17,9 +17,9 @@ (jerboa typed parser)) (defstruct typed-check-error (kind message detail)) - (defstruct typed-function-sig (param-types return-type)) + (defstruct typed-call-sig (param-types return-type)) - (def *function-env* (make-parameter '())) + (def *call-env* (make-parameter '())) (def builtin-type-names '(Unit Bool Char Int Nat Fixnum Float String Bytes Symbol Keyword)) @@ -31,6 +31,8 @@ (Result . 2) (Pair . 2))) + (def any-value-type (gensym "typed-any")) + (def (make-check-error kind message detail) (make-typed-check-error kind message detail)) @@ -123,6 +125,7 @@ (def (type-assignable? actual expected) (or (equal? actual expected) + (eq? expected any-value-type) (and (eq? actual 'Nat) (eq? expected 'Int)))) (def (param-env params) @@ -134,17 +137,74 @@ (def (function-signature decl) (and (typed-def? decl) (cons (typed-def-name decl) - (make-typed-function-sig + (make-typed-call-sig (map typed-param-type (typed-def-params decl)) (typed-def-return-type decl))))) - (def (function-env declarations) + (def (field-types fields) + (map typed-field-type fields)) + + (def (record-field-call-signatures record) + (let ([record-name (typed-record-name record)] + [prefix (symbol->string (typed-record-name record))]) + (append-map + (lambda (field) + (let* ([field-name (typed-field-name field)] + [field-type (typed-field-type field)] + [accessor-name (symbol-append prefix "-" field-name)] + [accessor + (cons accessor-name + (make-typed-call-sig (list record-name) field-type))]) + (if (typed-field-mutable? field) + (list accessor + (cons (symbol-append accessor-name "-set!") + (make-typed-call-sig + (list record-name field-type) + 'Unit))) + (list accessor)))) + (typed-record-fields record)))) + + (def (record-call-signatures record) + (let* ([record-name (typed-record-name record)] + [fields (typed-record-fields record)]) + (append + (list + (cons (symbol-append "make-" record-name) + (make-typed-call-sig (field-types fields) record-name)) + (cons (symbol-append record-name "?") + (make-typed-call-sig (list any-value-type) 'Bool))) + (record-field-call-signatures record)))) + + (def (variant-case-call-signature variant-name case) + (cons (typed-variant-case-name case) + (make-typed-call-sig + (field-types (typed-variant-case-fields case)) + variant-name))) + + (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)) + (map (lambda (case) + (variant-case-call-signature variant-name case)) + (typed-variant-cases variant))))) + + (def (declaration-call-signatures decl) + (cond + [(typed-def? decl) (list (function-signature decl))] + [(typed-record? decl) (record-call-signatures decl)] + [(typed-variant? decl) (variant-call-signatures decl)] + [else '()])) + + (def (call-env declarations) (let loop ([rest declarations] [out '()]) (cond [(null? rest) (reverse out)] [else - (let ([sig (function-signature (car rest))]) - (loop (cdr rest) (if sig (cons sig out) out)))]))) + (loop (cdr rest) + (append (reverse (declaration-call-signatures (car rest))) + out))]))) (def (check-compound-type type type-names) (let* ([head (car type)] @@ -413,13 +473,13 @@ out))]))) (def (infer-function-call name args env type-names expr) - (let ([sig (lookup-name name (*function-env*))]) + (let ([sig (lookup-name name (*call-env*))]) (if (not sig) (values #f (list (make-check-error 'unsupported-expression "expression form is not in the typed checker subset yet" expr))) - (let ([expected-types (typed-function-sig-param-types sig)]) + (let ([expected-types (typed-call-sig-param-types sig)]) (if (not (= (length args) (length expected-types))) (values #f (list (make-check-error 'bad-call-arity @@ -431,7 +491,7 @@ (argument-type-errors name expected-types actual-types)]) (values (if (and (null? arg-errors) (null? type-errors)) - (typed-function-sig-return-type sig) + (typed-call-sig-return-type sig) #f) (append arg-errors type-errors))))))))) @@ -530,8 +590,8 @@ (let* ([declarations (typed-module-declarations module)] [type-names (declared-type-names declarations)] [value-names (declared-value-names declarations)] - [functions (function-env declarations)]) - (parameterize ([*function-env* functions]) + [calls (call-env declarations)]) + (parameterize ([*call-env* calls]) (append (duplicate-errors 'duplicate-type "duplicate type declaration" --- a/tests/fixtures/typed/valid-split-tree.ss +++ b/tests/fixtures/typed/valid-split-tree.ss @@ -1,6 +1,6 @@ (typed-library (sample typed split-tree) (export make-Pane Pane? Pane-id Pane-focused? Pane-focused?-set! - split-size EditOp? Insert Noop) + split-size make-insert make-noop edit-op? EditOp? Insert Noop) (record Pane ((id : Nat) @@ -11,4 +11,13 @@ (Noop)) (def (split-size (pane : Pane)) : Nat - (+ 0 0))) + (Pane-id pane)) + + (def (make-insert (at : Nat) (text : String)) : EditOp + (Insert at text)) + + (def (make-noop) : EditOp + (Noop)) + + (def (edit-op? (op : EditOp)) : Bool + (EditOp? op))) --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -245,6 +245,105 @@ (g x)))) '(return-type-mismatch)) +(test "record constructor and accessor calls" + (error-kinds + '(typed-library (body record-ok) + (export pane-id) + (record Pane + ((id : Nat) + (mut focused? : Bool))) + (def (pane-id (x : Nat)) : Nat + (Pane-id (make-Pane x #f))))) + '()) + +(test "record predicate accepts typed values" + (error-kinds + '(typed-library (body record-predicate) + (export is-pane?) + (record Pane + ((id : Nat))) + (def (is-pane? (x : Pane)) : Bool + (Pane? x)))) + '()) + +(test "record mutable field setter call" + (error-kinds + '(typed-library (body record-setter) + (export focus!) + (record Pane + ((id : Nat) + (mut focused? : Bool))) + (def (focus! (pane : Pane)) : Unit + (Pane-focused?-set! pane #t)))) + '()) + +(test "record constructor arity mismatch" + (error-kinds + '(typed-library (body record-arity) + (export f) + (record Pane + ((id : Nat) + (focused? : Bool))) + (def (f (x : Nat)) : Pane + (make-Pane x)))) + '(bad-call-arity)) + +(test "record constructor argument mismatch" + (error-kinds + '(typed-library (body record-arg) + (export f) + (record Pane + ((id : Nat) + (focused? : Bool))) + (def (f (x : String)) : Pane + (make-Pane x #f)))) + '(argument-type-mismatch)) + +(test "record accessor argument mismatch" + (error-kinds + '(typed-library (body record-accessor-arg) + (export f) + (record Pane + ((id : Nat))) + (def (f (x : String)) : Nat + (Pane-id x)))) + '(argument-type-mismatch)) + +(test "variant constructor and predicate calls" + (error-kinds + '(typed-library (body variant-ok) + (export make-insert make-noop edit-op?) + (variant EditOp + (Insert (at : Nat) (text : String)) + (Noop)) + (def (make-insert (at : Nat) (text : String)) : EditOp + (Insert at text)) + (def (make-noop) : EditOp + (Noop)) + (def (edit-op? (op : EditOp)) : Bool + (EditOp? op)))) + '()) + +(test "variant constructor arity mismatch" + (error-kinds + '(typed-library (body variant-arity) + (export f) + (variant EditOp + (Insert (at : Nat) (text : String))) + (def (f (at : Nat)) : EditOp + (Insert at)))) + '(bad-call-arity)) + +(test "variant constructor argument mismatch" + (error-kinds + '(typed-library (body variant-arg) + (export f) + (variant EditOp + (Insert (at : Nat) (text : String))) + (def (f (at : Nat)) : EditOp + (Insert at at)))) + '(argument-type-mismatch)) + (test "arithmetic primitive returns numeric type" (error-kinds '(typed-library (body arithmetic)