Check Typed Jerboa function calls
ober
cd2dc7701b3234616cf3f49dd88b47717cde84a2
--- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -148,9 +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, and boolean primitives. General 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, 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. ## Surface Syntax @@ -741,7 +742,8 @@ Minimum excluded features: - Build module environment. - Check primitive expressions. Initial literal/variable/`begin`/`let`/`if`, arithmetic, comparison, and boolean primitive return checking landed. -- Check function applications. +- Check function applications. Same-module typed function calls now check + arity, argument types, and return type flow. - Check records and variants. - Check match exhaustiveness. - Produce useful errors. --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -17,6 +17,9 @@ (jerboa typed parser)) (defstruct typed-check-error (kind message detail)) + (defstruct typed-function-sig (param-types return-type)) + + (def *function-env* (make-parameter '())) (def builtin-type-names '(Unit Bool Char Int Nat Fixnum Float String Bytes Symbol Keyword)) @@ -128,6 +131,21 @@ (typed-param-type param))) params)) + (def (function-signature decl) + (and (typed-def? decl) + (cons (typed-def-name decl) + (make-typed-function-sig + (map typed-param-type (typed-def-params decl)) + (typed-def-return-type decl))))) + + (def (function-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)))]))) + (def (check-compound-type type type-names) (let* ([head (car type)] [args (cdr type)] @@ -379,6 +397,44 @@ (if (and (null? errors) (null? operand-errors)) 'Bool #f) (append errors operand-errors))))])) + (def (argument-type-errors name expected-types actual-types) + (let loop ([expected expected-types] [actual actual-types] [out '()]) + (cond + [(or (null? expected) (null? actual)) (reverse out)] + [(or (not (car actual)) + (type-assignable? (car actual) (car expected))) + (loop (cdr expected) (cdr actual) out)] + [else + (loop (cdr expected) + (cdr actual) + (cons (make-check-error 'argument-type-mismatch + "function argument type does not match parameter type" + (list name (car expected) (car actual))) + out))]))) + + (def (infer-function-call name args env type-names expr) + (let ([sig (lookup-name name (*function-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)]) + (if (not (= (length args) (length expected-types))) + (values #f + (list (make-check-error 'bad-call-arity + "function call arity does not match definition" + (list name (length expected-types) (length args))))) + (let-values ([(actual-types arg-errors) + (infer-args args env type-names)]) + (let ([type-errors + (argument-type-errors name expected-types actual-types)]) + (values + (if (and (null? arg-errors) (null? type-errors)) + (typed-function-sig-return-type sig) + #f) + (append arg-errors type-errors))))))))) + (def (infer-expression expr env type-names) (cond [(boolean? expr) (values 'Bool '())] @@ -415,10 +471,12 @@ [(not and or) (infer-boolean (car expr) (cdr expr) env type-names expr)] [else - (values #f - (list (make-check-error 'unsupported-expression - "expression form is not in the typed checker subset yet" - expr)))])] + (if (symbol? (car expr)) + (infer-function-call (car expr) (cdr expr) env type-names expr) + (values #f + (list (make-check-error 'unsupported-expression + "expression form is not in the typed checker subset yet" + expr))))])] [else (values #f (list (make-check-error 'unsupported-expression @@ -471,18 +529,20 @@ (def (check-typed-module module) (let* ([declarations (typed-module-declarations module)] [type-names (declared-type-names declarations)] - [value-names (declared-value-names declarations)]) - (append - (duplicate-errors 'duplicate-type - "duplicate type declaration" - type-names) - (duplicate-errors 'duplicate-value - "duplicate value declaration" - value-names) - (check-exports (typed-module-exports module) value-names) - (append-map - (lambda (decl) (check-declaration decl type-names)) - declarations)))) + [value-names (declared-value-names declarations)] + [functions (function-env declarations)]) + (parameterize ([*function-env* functions]) + (append + (duplicate-errors 'duplicate-type + "duplicate type declaration" + type-names) + (duplicate-errors 'duplicate-value + "duplicate value declaration" + value-names) + (check-exports (typed-module-exports module) value-names) + (append-map + (lambda (decl) (check-declaration decl type-names)) + declarations))))) (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 @@ -201,6 +201,50 @@ (foo x)))) '(unsupported-expression)) +(test "typed function call" + (error-kinds + '(typed-library (body call-ok) + (export f g) + (def (g (x : Nat)) : Nat x) + (def (f (x : Nat)) : Nat + (g x)))) + '()) + +(test "typed recursive function call" + (error-kinds + '(typed-library (body recursive-call) + (export f) + (def (f (x : Nat)) : Nat + (f x)))) + '()) + +(test "typed function call arity mismatch" + (error-kinds + '(typed-library (body call-arity) + (export f g) + (def (g (x : Nat)) : Nat x) + (def (f (x : Nat)) : Nat + (g x x)))) + '(bad-call-arity)) + +(test "typed function call argument mismatch" + (error-kinds + '(typed-library (body call-arg) + (export f g) + (def (g (x : String)) : String x) + (def (f (x : Nat)) : String + (g x)))) + '(argument-type-mismatch)) + +(test "typed function call return mismatch" + (error-kinds + '(typed-library (body call-return) + (export f g) + (def (g (x : String)) : String x) + (def (f (x : String)) : Nat + (g x)))) + '(return-type-mismatch)) + (test "arithmetic primitive returns numeric type" (error-kinds '(typed-library (body arithmetic)