Add typed Kotlin try catch expressions
ober
f2951420acb559c6b2e44f712e02a74a5a474eed
--- a/data/changelog.sexp +++ b/data/changelog.sexp @@ -2,7 +2,19 @@ . "Machine-readable changelog of Jerboa API drift. Consumers (LLM tooling, lints, jerboa_verify) use this to invalidate stale recommendations and to suggest migrations when a symbol is renamed or relocated.") ("entries" - (("added" "make-ring" "ring?" "ring-capacity" "ring-size" + (("added" "typed Kotlin try/catch expression form") + ("date" . "2026-07-17") + ("modules_added") + ("moved") + ("notes" + . + "Typed Jerboa Kotlin now accepts `(try body (catch (name : Type) handler ...))`, checks that the body and handler produce the same type, carries it through typed IR, and lowers it via structured Kotlin AST/printer nodes. This is intended for Android and JVM generation paths that need exception handling without raw Kotlin listener or background-task strings.") + ("removed") + ("renamed") + ("tier_changes") + ("tools_added") + ("version" . "v0.2.4")) + (("added" "make-ring" "ring?" "ring-capacity" "ring-size" "ring-append!" "ring-oldest-offset" "ring-newest-offset" "ring-slice-from") ("date" . "2026-07-16") --- a/data/cookbooks.sexp +++ b/data/cookbooks.sexp @@ -6786,4 +6786,14 @@ "ansible") ("title" . - "Deploy jerboa-site to dns2 as a Jerboa-built binary only"))) + "Deploy jerboa-site to dns2 as a Jerboa-built binary only")) + (("code" + . + "(import (jerboa typed kotlin))\n\n(define source\n '(typed-library (sample typed tryexpr)\n (export name-or-fallback)\n (type Exception)\n (extern (risky-name) : String\n (kotlin-call Risky name))\n (def (name-or-fallback) : String\n (try\n (risky-name)\n (catch (error : Exception)\n \"fallback\")))))\n\n(display (typed-library-form->kotlin-string source))") + ("id" . "typed-kotlin-try-catch-expression") + ("imports" "(jerboa typed kotlin)") + ("notes" + . + "Typed Kotlin supports `(try body (catch (name : Type) handler ...))`. The body and catch handler must produce the same result type. The catch binding is available only in the handler. The Kotlin backend lowers this through structured KAST nodes; do not use raw Kotlin strings for try/catch bodies.") + ("tags" "typed" "kotlin" "try" "catch" "exception" "compiler") + ("title" . "Use typed Kotlin try/catch expressions"))) --- a/lib/jerboa/typed/checker.ss +++ b/lib/jerboa/typed/checker.ss @@ -2805,6 +2805,26 @@ (values after-cond (append cond-errors then-errors else-errors))) (values moved '()))] + [(try) + (if (= (length args) 2) + (let ([catch-form (expr-value (cadr args))]) + (if (and (list? catch-form) + (>= (length catch-form) 3) + (eq? (expr-value (car catch-form)) 'catch)) + (let-values ([(after-body body-errors) + (check-ownership-expression + (car args) + env + moved)] + [(_after-catch catch-errors) + (check-ownership-body + (cddr catch-form) + env + moved)]) + (values after-body + (append body-errors catch-errors))) + (values moved '()))) + (values moved '()))] [(lambda) (if (< (length args) 2) (values moved '()) @@ -2975,6 +2995,71 @@ exception-ir)) (append exception-errors result-type-errors)))))])) + (def (infer-try args env type-names expr) + (cond + [(not (= (length args) 2)) + (values #f + (list (error-at expr 'bad-try + "try expects a body expression and one catch clause" + expr)))] + [else + (let* ([catch-expr (cadr args)] + [catch-value (expr-value catch-expr)] + [catch-raw (strip-source-annotations catch-expr)]) + (if (not (and (list? catch-raw) + (>= (length catch-raw) 3) + (eq? (car catch-raw) 'catch) + (list? (cadr catch-raw)) + (= (length (cadr catch-raw)) 3) + (symbol? (car (cadr catch-raw))) + (eq? (cadr (cadr catch-raw)) ':))) + (values #f + (list (error-at catch-expr 'bad-try + "catch clause must be shaped (catch (name : Type) handler ...)" + catch-expr))) + (let* ([catch-binding (cadr catch-raw)] + [catch-name (car catch-binding)] + [catch-type (parse-typed-type (caddr catch-binding))] + [catch-type-errors (check-type catch-type type-names)] + [catch-body (cddr catch-value)] + [catch-env (extend-env catch-name catch-type env)]) + (let-values ([(body-ir body-errors) + (infer-expression (car args) env type-names)] + [(catch-ir catch-errors) + (infer-body + catch-body + catch-env + type-names + (expr-source catch-expr))]) + (let* ([body-type (ir-type body-ir)] + [catch-result-type (ir-type catch-ir)] + [branch-errors + (if (and body-type catch-result-type + (not (equal? body-type catch-result-type))) + (list (error-at expr 'branch-type-mismatch + "try body and catch handler must have the same type" + (list body-type catch-result-type))) + '())] + [ok? (and body-ir + catch-ir + body-type + (valid-type? catch-type type-names) + (null? body-errors) + (null? catch-errors) + (null? catch-type-errors) + (null? branch-errors))]) + (values + (and ok? + (make-typed-ir-try + body-type + (expr-source expr) + body-ir + catch-name + catch-type + catch-ir)) + (append body-errors catch-errors + catch-type-errors branch-errors)))))))])) + (def (infer-expression expr env type-names) (let ([value (expr-value expr)] [src (expr-source expr)]) @@ -3020,6 +3105,8 @@ (infer-if args env type-names expr)] [(throw) (infer-throw args env type-names expr)] + [(try) + (infer-try args env type-names expr)] [(lambda) (infer-lambda args env type-names expr)] [(object) --- a/lib/jerboa/typed/core.ss +++ b/lib/jerboa/typed/core.ss @@ -44,6 +44,12 @@ typed-ir-throw-type typed-ir-throw-source typed-ir-throw-exception + typed-ir-try? + make-typed-ir-try + typed-ir-try-type typed-ir-try-source + typed-ir-try-body typed-ir-try-catch-name + typed-ir-try-catch-type typed-ir-try-catch-body + typed-ir-lambda? make-typed-ir-lambda typed-ir-lambda-type typed-ir-lambda-source @@ -114,6 +120,7 @@ (defstruct typed-ir-binding (name expr)) (defstruct typed-ir-if (type source test then else)) (defstruct typed-ir-throw (type source exception)) + (defstruct typed-ir-try (type source body catch-name catch-type catch-body)) (defstruct typed-ir-lambda (type source params body)) (defstruct typed-ir-object (type source super-type super-args methods)) (defstruct typed-ir-object-method @@ -237,6 +244,7 @@ (typed-ir-let? x) (typed-ir-if? x) (typed-ir-throw? x) + (typed-ir-try? x) (typed-ir-lambda? x) (typed-ir-object? x) (typed-ir-for-fold? x) @@ -252,6 +260,7 @@ [(typed-ir-let? node) (typed-ir-let-type node)] [(typed-ir-if? node) (typed-ir-if-type node)] [(typed-ir-throw? node) (typed-ir-throw-type node)] + [(typed-ir-try? node) (typed-ir-try-type node)] [(typed-ir-lambda? node) (typed-ir-lambda-type node)] [(typed-ir-object? node) (typed-ir-object-type node)] [(typed-ir-for-fold? node) (typed-ir-for-fold-type node)] @@ -268,6 +277,7 @@ [(typed-ir-let? node) (typed-ir-let-source node)] [(typed-ir-if? node) (typed-ir-if-source node)] [(typed-ir-throw? node) (typed-ir-throw-source node)] + [(typed-ir-try? node) (typed-ir-try-source node)] [(typed-ir-lambda? node) (typed-ir-lambda-source node)] [(typed-ir-object? node) (typed-ir-object-source node)] [(typed-ir-for-fold? node) (typed-ir-for-fold-source node)] --- a/lib/jerboa/typed/kotlin/ast.ss +++ b/lib/jerboa/typed/kotlin/ast.ss @@ -88,6 +88,12 @@ kt-throw? make-kt-throw kt-throw-exception + kt-catch? make-kt-catch + kt-catch-name kt-catch-type kt-catch-body + + kt-try? make-kt-try + kt-try-body kt-try-catch + kt-block? make-kt-block kt-block-statements kt-block-result @@ -143,6 +149,8 @@ (defstruct kt-unary (op expr)) (defstruct kt-if (test then else)) (defstruct kt-throw (exception)) + (defstruct kt-catch (name type body)) + (defstruct kt-try (body catch)) (defstruct kt-block (statements result)) (defstruct kt-new (type args)) (defstruct kt-when (subject branches)) --- a/lib/jerboa/typed/kotlin/lower.ss +++ b/lib/jerboa/typed/kotlin/lower.ss @@ -799,6 +799,13 @@ (lower-expr (typed-ir-if-else ir)))] [(typed-ir-throw? ir) (make-kt-throw (lower-expr (typed-ir-throw-exception ir)))] + [(typed-ir-try? ir) + (make-kt-try + (lower-expr (typed-ir-try-body ir)) + (make-kt-catch + (typed-ir-try-catch-name ir) + (typed-type->kotlin-type (typed-ir-try-catch-type ir)) + (lower-expr (typed-ir-try-catch-body ir))))] [(typed-ir-lambda? ir) (lower-lambda ir)] [(typed-ir-object? ir) --- a/lib/jerboa/typed/kotlin/print.ss +++ b/lib/jerboa/typed/kotlin/print.ss @@ -239,6 +239,7 @@ (or (kt-binary? expr) (kt-unary? expr) (kt-if? expr) + (kt-try? expr) (kt-block? expr) (kt-when? expr) (kt-object-expr? expr) @@ -334,6 +335,18 @@ (kotlin-expr->string (kt-if-else expr)))] [(kt-throw? expr) (string-append "throw " (kotlin-expr->string (kt-throw-exception expr)))] + [(kt-try? expr) + (emit-to-string + (lambda (port) + (let ([catch (kt-try-catch expr)]) + (display "try " port) + (display (kotlin-expr->string (kt-try-body expr)) port) + (display " catch (" port) + (display (kotlin-symbol-name (kt-catch-name catch)) port) + (display ": " port) + (display (kotlin-type->string (kt-catch-type catch)) port) + (display ") " port) + (display (kotlin-expr->string (kt-catch-body catch)) port))))] [(kt-block? expr) (emit-to-string (lambda (port) --- a/tests/test-typed-checker.ss +++ b/tests/test-typed-checker.ss @@ -417,6 +417,41 @@ (if x 1 "bad")))) '(branch-type-mismatch)) +(test "try catch success" + (error-kinds + '(typed-library (body try-ok) + (export f) + (type Exception) + (def (f (x : Nat)) : Nat + (try + x + (catch (error : Exception) + 0))))) + '()) + +(test "try catch branch mismatch" + (error-kinds + '(typed-library (body try-mismatch) + (export f) + (type Exception) + (def (f (x : Nat)) : Nat + (try + x + (catch (error : Exception) + "bad"))))) + '(branch-type-mismatch return-type-mismatch)) + +(test "try catch bad shape" + (error-kinds + '(typed-library (body try-bad-shape) + (export f) + (type Exception) + (def (f (x : Nat)) : Nat + (try + x + (catch error x))))) + '(bad-try)) + (test "unsupported call expression" (error-kinds '(typed-library (body unsupported) --- a/tests/test-typed-kotlin.ss +++ b/tests/test-typed-kotlin.ss @@ -143,6 +143,16 @@ (list (make-kt-lit 'String "bad"))))) "throw CertificateException(\"bad\")") +(test "try catch expression printer" + (kotlin-expr->string + (make-kt-try + (make-kt-block '() (make-kt-lit 'String "ok")) + (make-kt-catch + 'error + (make-kt-type 'Exception #f '()) + (make-kt-block '() (make-kt-lit 'String "fallback"))))) + "try run {\n \"ok\"\n} catch (error: Exception) run {\n \"fallback\"\n}") + (define ast-file-text (string-append "// Generated by Jerboa's typed Kotlin backend. Do not edit.\n\n" @@ -510,6 +520,27 @@ throw-kotlin "throw CertificateException(\"bad\")") +(define try-form + '(typed-library (sample typed tryexpr) + (export nameOrFallback) + (type Exception) + (extern (riskyName) : String + (kotlin-call Risky name)) + (extern (exceptionMessage (error : Exception)) : String + (kotlin-member-call message)) + (def (nameOrFallback) : String + (try + (riskyName) + (catch (error : Exception) + (string-append "fallback: " (exceptionMessage error))))))) + +(define try-kotlin + (typed-library-form->kotlin-string try-form)) + +(test-contains "typed try catch lowers to Kotlin try" + try-kotlin + "return try Risky.name() catch (error: Exception) (\"fallback: \" + error.message())") + (define geometry-form '(typed-library (sample typed geometry) (export make-SsdCell SsdCell? SsdCell-x SsdCell-y SsdCell-w SsdCell-h