Emit typed Kotlin properties and external declarations

ober

832b6cba585bb6bd81b9b7ca0da726d853d6b114

diff --git a/lib/jerboa/typed/checker.ss b/lib/jerboa/typed/checker.ss
index a842b95..426cbb5 100644
--- a/lib/jerboa/typed/checker.ss
+++ b/lib/jerboa/typed/checker.ss
@@ -42,6 +42,7 @@
   (def *call-env* (make-parameter '()))
   (def *variant-env* (make-parameter '()))
   (def *current-effects* (make-parameter '()))
+  (def *global-value-env* (make-parameter '()))
 
   (def builtin-type-names
     '(Unit Bool Char Int Nat Fixnum Float String Bytes Symbol Keyword))
@@ -302,6 +303,7 @@
   (def (declaration-value-names decl)
     (cond
       [(typed-def? decl) (list (typed-def-name decl))]
+      [(typed-property? decl) (list (typed-property-name decl))]
       [(typed-extern? decl) (list (typed-extern-name decl))]
       [(typed-record? decl) (record-value-names decl)]
       [(typed-variant? decl) (variant-value-names decl)]
@@ -388,19 +390,25 @@
     (and (typed-extern? decl)
          (let* ([target (typed-extern-kotlin-path decl)]
                 [kind-entry (assq 'kind target)]
-                [kind (and kind-entry (cdr kind-entry))])
+                [kind (and kind-entry (cdr kind-entry))]
+                [call-target
+                 (if (eq? kind 'external)
+                   (list (cons 'kind 'call)
+                         (cons 'path (list (typed-extern-name decl))))
+                   target)])
            (cons (typed-extern-name decl)
                  (make-typed-call-sig
                    (map typed-param-type (typed-extern-params decl))
                    (typed-extern-return-type decl)
                    '()
                    (case kind
+                     [(external) 'kotlin-call]
                      [(call) 'kotlin-call]
                      [(member-call) 'kotlin-member-call]
                      [(member-get) 'kotlin-member-get]
                      [(member-set) 'kotlin-member-set]
                      [else 'kotlin-call])
-                   target)))))
+                   call-target)))))
 
   (def builtin-call-signatures
     (list
@@ -849,6 +857,53 @@
         (typed-extern-params decl))
       (check-type (typed-extern-return-type decl) type-names)))
 
+  (def (global-property-env declarations)
+    (let loop ([rest declarations] [out '()])
+      (cond
+        [(null? rest) (reverse out)]
+        [(typed-property? (car rest))
+         (let ([prop (car rest)])
+           (loop (cdr rest)
+                 (cons
+                   (cons (typed-property-name prop)
+                         (if (typed-property-mutable? prop)
+                           (mutable-local-value (typed-property-type prop))
+                           (typed-property-type prop)))
+                   out)))]
+        [else (loop (cdr rest) out)])))
+
+  (def (record-elaboration-by-name! name body-ir)
+    (let ([acc (*elaboration-acc*)])
+      (when (and acc body-ir)
+        (set-box! acc
+          (cons (cons name body-ir) (unbox acc))))))
+
+  (def (check-property prop type-names)
+    (let-values ([(init-ir init-errors)
+                  (infer-expression
+                    (typed-property-init prop)
+                    (*global-value-env*)
+                    type-names)])
+      (let* ([actual-type (ir-type init-ir)]
+             [declared-type (typed-property-type prop)]
+             [type-errors
+              (append
+                (check-type declared-type type-names)
+                (if (and actual-type
+                         (valid-type? declared-type type-names)
+                         (not (type-assignable? actual-type declared-type)))
+                  (list (make-check-error 'property-type-mismatch
+                          "property initializer type does not match declared type"
+                          (list (typed-property-name prop)
+                                declared-type
+                                actual-type)
+                          (typed-property-source prop)))
+                  '()))]
+             [all-errors (append init-errors type-errors)])
+        (when (null? all-errors)
+          (record-elaboration-by-name! (typed-property-name prop) init-ir))
+        all-errors)))
+
   (def (infer-body exprs env type-names . src*)
     (let ([src (if (pair? src*) (car src*) #f)])
       (cond
@@ -3423,13 +3478,11 @@
   (def *elaboration-acc* (make-parameter #f))
 
   (def (record-elaboration! def body-ir)
-    (let ([acc (*elaboration-acc*)])
-      (when (and acc body-ir)
-        (set-box! acc
-          (cons (cons (typed-def-name def) body-ir) (unbox acc))))))
+    (record-elaboration-by-name! (typed-def-name def) body-ir))
 
   (def (check-def-body def type-names)
-    (let* ([env (param-env (typed-def-params def))]
+    (let* ([env (append (param-env (typed-def-params def))
+                        (*global-value-env*))]
            [body (typed-def-body def)]
            [last-expr (and (pair? body)
                            (let loop ([rest body])
@@ -3465,6 +3518,7 @@
     (cond
       [(typed-record? decl) (check-record decl type-names)]
       [(typed-variant? decl) (check-variant decl type-names)]
+      [(typed-property? decl) (check-property decl type-names)]
       [(typed-extern? decl) (check-extern decl type-names)]
       [(typed-def? decl) (check-def decl type-names)]
       [else '()]))
@@ -3497,6 +3551,8 @@
                   [exported?
                    (cond
                      [(typed-def? decl) (memq (typed-def-name decl) exports)]
+                     [(typed-property? decl)
+                      (memq (typed-property-name decl) exports)]
                      [(typed-record? decl)
                       (or (memq (typed-record-name decl) exports)
                           (let any-loop ([rs values])
@@ -3615,13 +3671,15 @@
            [type-names (declared-type-names declarations)]
            [value-names (declared-value-names declarations)]
            [calls (call-env declarations)]
-           [variants (declared-variant-env declarations)])
+           [variants (declared-variant-env declarations)]
+           [global-values (global-property-env declarations)])
       (let-values ([(import-types import-calls import-variants import-errors)
                     (build-import-context module registry)]
                    [(same-types same-calls same-variants)
                     (same-module-context module registry)])
         (parameterize ([*call-env* (append import-calls same-calls calls)]
-                       [*variant-env* (append import-variants same-variants variants)])
+                       [*variant-env* (append import-variants same-variants variants)]
+                       [*global-value-env* global-values])
           (append
             import-errors
             (duplicate-errors 'duplicate-type
@@ -3677,6 +3735,16 @@
                                        name def (cdr entry))
                                      out)
                                out)))]
+                    [(typed-property? (car rest))
+                     (let* ([prop (car rest)]
+                            [name (typed-property-name prop)]
+                            [entry (assq name entries)])
+                       (loop (cdr rest)
+                             (if entry
+                               (cons (make-elaborated-def
+                                       name prop (cdr entry))
+                                     out)
+                               out)))]
                     [else (loop (cdr rest) out)]))])
           (values errors defs)))))
 
diff --git a/lib/jerboa/typed/kotlin/lower.ss b/lib/jerboa/typed/kotlin/lower.ss
index ba292ed..418e695 100644
--- a/lib/jerboa/typed/kotlin/lower.ss
+++ b/lib/jerboa/typed/kotlin/lower.ss
@@ -991,10 +991,40 @@
           (list (make-kt-return (lower-expr (cdr ir-entry)))))
         '())))
 
+  (def (lower-property prop)
+    (let ([ir-entry (assq (typed-property-name prop) (*kotlin-ir-env*))])
+      (unless ir-entry
+        (error 'lower-property
+          "missing elaborated IR for typed property"
+          (typed-property-name prop)))
+      (make-kt-property
+        #f
+        (typed-property-mutable? prop)
+        (typed-property-name prop)
+        (typed-type->kotlin-type (typed-property-type prop))
+        (lower-expr (cdr ir-entry))
+        '())))
+
+  (def (lower-extern decl)
+    (let* ([target (typed-extern-kotlin-path decl)]
+           [kind-entry (assq 'kind target)]
+           [kind (and kind-entry (cdr kind-entry))])
+      (and (eq? kind 'external)
+           (make-kt-function
+             #f
+             '(external)
+             (typed-extern-name decl)
+             (map lower-param (typed-extern-params decl))
+             (typed-type->kotlin-type (typed-extern-return-type decl))
+             #f
+             '()))))
+
   (def (lower-declaration decl)
     (cond
       [(typed-record? decl) (lower-record decl)]
       [(typed-variant? decl) (lower-variant decl)]
+      [(typed-property? decl) (lower-property decl)]
+      [(typed-extern? decl) (lower-extern decl)]
       [(typed-def? decl) (lower-def decl)]
       [else #f]))
 
diff --git a/lib/jerboa/typed/kotlin/print.ss b/lib/jerboa/typed/kotlin/print.ss
index 9947380..ad5a7ca 100644
--- a/lib/jerboa/typed/kotlin/print.ss
+++ b/lib/jerboa/typed/kotlin/print.ss
@@ -519,10 +519,11 @@
         (if (kt-function-return-type fn)
           (string-append ": " (kotlin-type->string (kt-function-return-type fn)))
           "")
-        " {"))
-    (for-each (lambda (stmt) (write-statement port (+ indent 1) stmt))
-              (kt-function-body fn))
-    (write-line port indent "}"))
+        (if (kt-function-body fn) " {" "")))
+    (when (kt-function-body fn)
+      (for-each (lambda (stmt) (write-statement port (+ indent 1) stmt))
+                (kt-function-body fn))
+      (write-line port indent "}")))
 
   (def (write-property port indent prop)
     (for-each (lambda (line) (write-line port indent line))
diff --git a/lib/jerboa/typed/parser.ss b/lib/jerboa/typed/parser.ss
index 67dd57e..a469d81 100644
--- a/lib/jerboa/typed/parser.ss
+++ b/lib/jerboa/typed/parser.ss
@@ -34,6 +34,10 @@
     typed-resource? make-typed-resource
     typed-resource-name typed-resource-close typed-resource-source
 
+    typed-property? make-typed-property
+    typed-property-mutable? typed-property-name
+    typed-property-type typed-property-init typed-property-source
+
     typed-extern? make-typed-extern
     typed-extern-name typed-extern-params typed-extern-return-type
     typed-extern-kotlin-path typed-extern-source
@@ -61,6 +65,7 @@
   (defstruct typed-field (name type mutable? source))
   (defstruct typed-record (name fields source))
   (defstruct typed-resource (name close source))
+  (defstruct typed-property (mutable? name type init source))
   (defstruct typed-extern (name params return-type kotlin-path source))
   (defstruct typed-variant (name cases source))
   (defstruct typed-variant-case (name fields source))
@@ -448,9 +453,12 @@
               (symbol? (cadr form)))
          (list (cons 'kind 'member-set)
                (cons 'member (cadr form)))]
+        [(and (= (length form) 1)
+              (eq? (car form) 'kotlin-external))
+         (list (cons 'kind 'external))]
         [else
          (error 'parse-typed-extern
-          "expected (kotlin-call PackageOrObject function), (kotlin-member-call method), (kotlin-member-get property), or (kotlin-member-set property)"
+          "expected (kotlin-call PackageOrObject function), (kotlin-member-call method), (kotlin-member-get property), (kotlin-member-set property), or (kotlin-external)"
           form)])))
 
   (def (parse-extern form)
@@ -474,6 +482,31 @@
             (parse-kotlin-call-target target)
             source)))))
 
+  (def (parse-property form)
+    (let* ([source (datum-source form)]
+           [raw-form (datum-value form)]
+           [form (strip-source-annotations form)])
+      (expect-length 'parse-typed-property form 5)
+      (let ([kind (car form)]
+            [name (cadr form)]
+            [type-marker (caddr form)]
+            [type (cadddr form)]
+            [init (list-ref raw-form 4)])
+        (unless (memq kind '(val var))
+          (error 'parse-typed-property
+            "expected val or var declaration"
+            form))
+        (unless (eq? type-marker ':)
+          (error 'parse-typed-property
+            "expected (val name : Type init) or (var name : Type init)"
+            form))
+        (make-typed-property
+          (eq? kind 'var)
+          (expect-symbol 'parse-typed-property name form)
+          (parse-typed-type type)
+          init
+          source))))
+
   (def (parse-type-decl form)
     (let ([source (datum-source form)]
           [form (strip-source-annotations form)])
@@ -491,6 +524,7 @@
         [(type) (parse-type-decl form)]
         [(record) (parse-record form)]
         [(resource) (parse-resource form)]
+        [(val var) (parse-property form)]
         [(variant) (parse-variant form)]
         [(extern) (parse-extern form)]
         [(def) (parse-def form)]
diff --git a/tests/test-typed-kotlin.ss b/tests/test-typed-kotlin.ss
index e511b14..a40b99e 100644
--- a/tests/test-typed-kotlin.ss
+++ b/tests/test-typed-kotlin.ss
@@ -1385,5 +1385,43 @@
   control-flow-kotlin
   "if ((read < 0)) continue else Unit")
 
+(define top-level-property-form
+  '(typed-library (sample typed globals)
+     (export available nativeThing)
+     (type Throwable)
+     (type Int32)
+     (extern (systemLoadLibrary (name : String)) : Unit
+       (kotlin-call System loadLibrary))
+     (extern (nativeThing (x : Int32)) : String
+       (kotlin-external))
+     (var loadError : (Nullable Throwable)
+       (nullable-none Throwable))
+     (val loaded : Bool
+       (try
+         (begin
+           (systemLoadLibrary "jerboa_vision")
+           #t)
+         (catch (error : Throwable)
+           (begin
+             (set! loadError (nullable-some error))
+             #f))))
+     (def (available) : Bool loaded)))
+
+(define top-level-property-kotlin
+  (typed-library-form->kotlin-string top-level-property-form))
+
+(test-contains "top-level var lowers to Kotlin property"
+  top-level-property-kotlin
+  "var loadError: Throwable? = null")
+(test-contains "top-level val lowers checked try initializer"
+  top-level-property-kotlin
+  "val loaded: Boolean = try {\n    System.loadLibrary(\"jerboa_vision\")\n    true")
+(test-contains "set! can assign top-level mutable property"
+  top-level-property-kotlin
+  "loadError = error")
+(test-contains "external Kotlin extern declaration is emitted without body"
+  top-level-property-kotlin
+  "external fun nativeThing(x: Int): String")
+
 (printf "typed-kotlin tests: ~a passed, ~a failed~%" pass fail)
 (when (> fail 0) (exit 1))