Check Typed Jerboa option results
ober
dc3897fc786caa3686a5b151255ac331a4f27d92
--- a/docs/jerboa-to-rust.md +++ b/docs/jerboa-to-rust.md @@ -154,6 +154,11 @@ Initial type mapping: | Record | `struct` | | Variant | `enum` | +Current landing: the checker types explicit Option/Result constructors: +`option-some`, `option-none`, `result-ok`, and `result-err`. The Rust backend +already maps Option/Result types, but constructor expression lowering is still +future work. + Boundary-facing values should use ABI-safe wrappers instead of raw Rust layout. ## Records --- a/docs/typed-jerboa.md +++ b/docs/typed-jerboa.md @@ -209,6 +209,10 @@ Current landing: as `(Bytes -> Nat)` and lowers the same way. Imported calls and richer forms are reported as unsupported. It does not yet resolve imports, lower to typed core IR, or emit LLVM. +- `Option` and `Result` type expressions now have explicit checked + constructors in the front end: `(option-some expr)`, `(option-none Type)`, + `(result-ok expr ErrorType)`, and `(result-err ValueType expr)`. Rust + lowering for these constructors is still future work. - The current Rust lowering uses a conservative Clone-only ownership model: generated constructors, ordinary calls, and recursive match rebinding clone owned values so recursive branch code can pass the same child value to more --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -867,6 +867,50 @@ (if (and (null? errors) (null? operand-errors)) 'Bool #f) (append errors operand-errors))))])) + (def (bad-constructor-arity name expected args) + (list (make-check-error 'bad-call-arity + "typed constructor arity does not match" + (list name expected (length args))))) + + (def (infer-option-some args env type-names expr) + (if (not (= (length args) 1)) + (values #f (bad-constructor-arity 'option-some 1 args)) + (let-values ([(value-type errors) + (infer-expression (car args) env type-names)]) + (values (and value-type (list 'Option value-type)) + errors)))) + + (def (infer-option-none args env type-names expr) + (if (not (= (length args) 1)) + (values #f (bad-constructor-arity 'option-none 1 args)) + (let ([errors (check-type (car args) type-names)]) + (values (and (null? errors) (list 'Option (car args))) + errors)))) + + (def (infer-result-ok args env type-names expr) + (if (not (= (length args) 2)) + (values #f (bad-constructor-arity 'result-ok 2 args)) + (let-values ([(value-type value-errors) + (infer-expression (car args) env type-names)]) + (let ([error-type-errors (check-type (cadr args) type-names)]) + (values + (and value-type + (null? error-type-errors) + (list 'Result value-type (cadr args))) + (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 'result-err 2 args)) + (let-values ([(error-type error-errors) + (infer-expression (cadr args) env type-names)]) + (let ([value-type-errors (check-type (car args) type-names)]) + (values + (and error-type + (null? value-type-errors) + (list 'Result (car args) error-type)) + (append value-type-errors error-errors)))))) + (def (argument-type-errors name expected-types actual-types) (let loop ([expected expected-types] [actual actual-types] [out '()]) (cond @@ -1089,6 +1133,14 @@ (infer-comparison (car expr) (cdr expr) env type-names expr)] [(not and or) (infer-boolean (car expr) (cdr expr) env type-names expr)] + [(option-some) + (infer-option-some (cdr expr) env type-names expr)] + [(option-none) + (infer-option-none (cdr expr) env type-names expr)] + [(result-ok) + (infer-result-ok (cdr expr) env type-names expr)] + [(result-err) + (infer-result-err (cdr expr) env type-names expr)] [else (if (symbol? (car expr)) (infer-function-call (car expr) (cdr expr) env type-names expr) --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -189,6 +189,70 @@ 0))) '(bad-type-arity)) +(test "option-some returns Option" + (error-kinds + '(typed-library (option some) + (export f) + (def (f (x : Nat)) : (Option Nat) + (option-some x)))) + '()) + +(test "option-none returns typed Option" + (error-kinds + '(typed-library (option none) + (export f) + (def (f) : (Option String) + (option-none String)))) + '()) + +(test "option constructor return mismatch" + (error-kinds + '(typed-library (option mismatch) + (export f) + (def (f (x : Nat)) : (Option String) + (option-some x)))) + '(return-type-mismatch)) + +(test "option-none rejects unknown type" + (error-kinds + '(typed-library (option unknown) + (export f) + (def (f) : Nat + (option-none Missing)))) + '(unknown-type)) + +(test "option constructor arity mismatch" + (error-kinds + '(typed-library (option arity) + (export f) + (def (f) : (Option Nat) + (option-some)))) + '(bad-call-arity)) + +(test "result-ok returns Result" + (error-kinds + '(typed-library (result ok) + (export f) + (def (f (x : Nat)) : (Result Nat String) + (result-ok x String)))) + '()) + +(test "result-err returns Result" + (error-kinds + '(typed-library (result err) + (export f) + (def (f (message : String)) : (Result Nat String) + (result-err Nat message)))) + '()) + +(test "result constructor return mismatch" + (error-kinds + '(typed-library (result mismatch) + (export f) + (def (f (x : Nat)) : (Result String String) + (result-ok x String)))) + '(return-type-mismatch)) + (test "owned resource can move once" (error-kinds '(typed-library (resource move-once)