Lower typed Kotlin try finally

ober

1c1b45bea323c0d4fa2881ef66d884cb4ff6b284

diff --git a/lib/jerboa/typed/checker.ss b/lib/jerboa/typed/checker.ss
index 6c48241..e746841 100644
--- a/lib/jerboa/typed/checker.ss
+++ b/lib/jerboa/typed/checker.ss
@@ -3245,6 +3245,21 @@
                               (append body-errors catch-errors)))
                     (values moved '())))
                 (values moved '()))]
+             [(try-finally)
+              (if (< (length args) 2)
+                (values moved '())
+                (let-values ([(after-body body-errors)
+                              (check-ownership-expression
+                                (car args)
+                                env
+                                moved)]
+                             [(_after-finally finally-errors)
+                              (check-ownership-body
+                                (cdr args)
+                                env
+                                moved)])
+                  (values after-body
+                          (append body-errors finally-errors))))]
              [(lambda)
               (if (< (length args) 2)
                 (values moved '())
@@ -3535,6 +3550,46 @@
                    (append body-errors catch-errors
                            catch-type-errors branch-errors)))))))]))
 
+  (def (infer-try-finally args env type-names expr)
+    (cond
+      [(< (length args) 2)
+       (values #f
+         (list (error-at expr 'bad-try-finally
+                 "try-finally expects a body expression and finalizer body"
+                 expr)))]
+      [else
+       (let-values ([(body-ir body-errors)
+                     (infer-expression (car args) env type-names)]
+                    [(finally-ir finally-errors)
+                     (infer-body
+                       (cdr args)
+                       env
+                       type-names
+                       (expr-source expr))])
+         (let* ([body-type (ir-type body-ir)]
+                [finally-type (ir-type finally-ir)]
+                [finally-type-errors
+                 (if (and finally-type (not (eq? finally-type 'Unit)))
+                   (list (error-at expr 'try-finally-body-type-mismatch
+                           "try-finally finalizer must return Unit"
+                           finally-type))
+                   '())]
+                [ok? (and body-ir
+                          finally-ir
+                          body-type
+                          (null? body-errors)
+                          (null? finally-errors)
+                          (null? finally-type-errors))])
+           (values
+             (and ok?
+                  (make-typed-ir-try-finally
+                    body-type
+                    (expr-source expr)
+                    body-ir
+                    finally-ir))
+             (append body-errors finally-errors
+                     finally-type-errors))))]))
+
   (def (infer-expression expr env type-names)
     (let ([value (expr-value expr)]
           [src (expr-source expr)])
@@ -3609,6 +3664,8 @@
               (infer-throw args env type-names expr)]
              [(try)
               (infer-try args env type-names expr)]
+             [(try-finally)
+              (infer-try-finally args env type-names expr)]
              [(lambda)
               (infer-lambda args env type-names expr)]
              [(object)
diff --git a/lib/jerboa/typed/core.ss b/lib/jerboa/typed/core.ss
index 8efa569..0751ba5 100644
--- a/lib/jerboa/typed/core.ss
+++ b/lib/jerboa/typed/core.ss
@@ -77,6 +77,11 @@
     typed-ir-try-body typed-ir-try-catch-name
     typed-ir-try-catch-type typed-ir-try-catch-body
 
+    typed-ir-try-finally?
+    make-typed-ir-try-finally
+    typed-ir-try-finally-type typed-ir-try-finally-source
+    typed-ir-try-finally-body typed-ir-try-finally-finally-body
+
     typed-ir-lambda?
     make-typed-ir-lambda
     typed-ir-lambda-type typed-ir-lambda-source
@@ -159,6 +164,7 @@
   (defstruct typed-ir-return (type source expr))
   (defstruct typed-ir-throw (type source exception))
   (defstruct typed-ir-try (type source body catch-name catch-type catch-body))
+  (defstruct typed-ir-try-finally (type source body finally-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
@@ -291,6 +297,7 @@
         (typed-ir-return? x)
         (typed-ir-throw? x)
         (typed-ir-try? x)
+        (typed-ir-try-finally? x)
         (typed-ir-lambda? x)
         (typed-ir-object? x)
         (typed-ir-new? x)
@@ -314,6 +321,7 @@
       [(typed-ir-return? node) (typed-ir-return-type node)]
       [(typed-ir-throw? node) (typed-ir-throw-type node)]
       [(typed-ir-try? node) (typed-ir-try-type node)]
+      [(typed-ir-try-finally? node) (typed-ir-try-finally-type node)]
       [(typed-ir-lambda? node) (typed-ir-lambda-type node)]
       [(typed-ir-object? node) (typed-ir-object-type node)]
       [(typed-ir-new? node) (typed-ir-new-type node)]
@@ -338,6 +346,7 @@
       [(typed-ir-return? node) (typed-ir-return-source node)]
       [(typed-ir-throw? node) (typed-ir-throw-source node)]
       [(typed-ir-try? node) (typed-ir-try-source node)]
+      [(typed-ir-try-finally? node) (typed-ir-try-finally-source node)]
       [(typed-ir-lambda? node) (typed-ir-lambda-source node)]
       [(typed-ir-object? node) (typed-ir-object-source node)]
       [(typed-ir-new? node) (typed-ir-new-source node)]
diff --git a/lib/jerboa/typed/kotlin/ast.ss b/lib/jerboa/typed/kotlin/ast.ss
index 629bd14..e92c3c1 100644
--- a/lib/jerboa/typed/kotlin/ast.ss
+++ b/lib/jerboa/typed/kotlin/ast.ss
@@ -105,6 +105,9 @@
     kt-try? make-kt-try
     kt-try-body kt-try-catch
 
+    kt-try-finally? make-kt-try-finally
+    kt-try-finally-body kt-try-finally-finally-body
+
     kt-block? make-kt-block
     kt-block-statements kt-block-result
 
@@ -166,6 +169,7 @@
   (defstruct kt-throw (exception))
   (defstruct kt-catch (name type body))
   (defstruct kt-try (body catch))
+  (defstruct kt-try-finally (body finally-body))
   (defstruct kt-block (statements result))
   (defstruct kt-new (type args))
   (defstruct kt-when (subject branches))
diff --git a/lib/jerboa/typed/kotlin/lower.ss b/lib/jerboa/typed/kotlin/lower.ss
index d036c17..dbb4c80 100644
--- a/lib/jerboa/typed/kotlin/lower.ss
+++ b/lib/jerboa/typed/kotlin/lower.ss
@@ -867,6 +867,10 @@
            (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-try-finally? ir)
+       (make-kt-try-finally
+         (lower-expr (typed-ir-try-finally-body ir))
+         (lower-expr (typed-ir-try-finally-finally-body ir)))]
       [(typed-ir-lambda? ir)
        (lower-lambda ir)]
       [(typed-ir-object? ir)
diff --git a/lib/jerboa/typed/kotlin/print.ss b/lib/jerboa/typed/kotlin/print.ss
index f1a843f..fd4a132 100644
--- a/lib/jerboa/typed/kotlin/print.ss
+++ b/lib/jerboa/typed/kotlin/print.ss
@@ -258,6 +258,7 @@
         (kt-unary? expr)
         (kt-if? expr)
         (kt-try? expr)
+        (kt-try-finally? expr)
         (kt-block? expr)
         (kt-when? expr)
         (kt-object-expr? expr)
@@ -380,6 +381,14 @@
              (display (kotlin-type->string (kt-catch-type catch)) port)
              (display ") " port)
              (write-expression-block port 0 (kt-catch-body catch)))))]
+      [(kt-try-finally? expr)
+       (emit-to-string
+         (lambda (port)
+           (display "try " port)
+           (write-expression-block port 0 (kt-try-finally-body expr))
+           (display " finally " port)
+           (write-expression-block port 0
+             (kt-try-finally-finally-body expr))))]
       [(kt-block? expr)
        (emit-to-string
          (lambda (port)
diff --git a/tests/test-typed-kotlin.ss b/tests/test-typed-kotlin.ss
index 5806c7b..b265105 100644
--- a/tests/test-typed-kotlin.ss
+++ b/tests/test-typed-kotlin.ss
@@ -557,6 +557,26 @@
   try-kotlin
   "return try {\n    Risky.name()\n} catch (error: Exception) {\n    (\"fallback: \" + error.message())\n}")
 
+(define try-finally-form
+  '(typed-library (sample typed tryfinally)
+     (export readThenClose)
+     (type Resource)
+     (extern (readResource (resource : Resource)) : String
+       (kotlin-call readResource))
+     (extern (closeResource (resource : Resource)) : Unit
+       (kotlin-call closeResource))
+     (def (readThenClose (resource : Resource)) : String
+       (try-finally
+         (readResource resource)
+         (closeResource resource)))))
+
+(define try-finally-kotlin
+  (typed-library-form->kotlin-string try-finally-form))
+
+(test-contains "typed try-finally lowers to Kotlin finally"
+  try-finally-kotlin
+  "return try {\n    readResource(resource)\n} finally {\n    closeResource(resource)\n}")
+
 (define geometry-form
   '(typed-library (sample typed geometry)
      (export make-SsdCell SsdCell? SsdCell-x SsdCell-y SsdCell-w SsdCell-h