Use pushed typed Kotlin backend
ober
c2b12090bf658f476fbf1202ed49d4fed9d76b93
--- a/.build.yml +++ b/.build.yml @@ -5,7 +5,7 @@ packages: - make=4.4.1-r4 sources: # Build dependency: full immutable commit, mirrored in dependencies.lock.json. - - "https://git.sr.ht/~lisp/jerboa#23ad83d28ac65cf6f0d2d702fd32934f207c26bf" + - "https://git.sr.ht/~lisp/jerboa#610d17bceac32fd4f42d7e394c5264ee3d761d1a" # The second source is the build subject selected by the SourceHut submitter. - https://git.sr.ht/~lisp/jerboa-android tasks: @@ -14,6 +14,6 @@ tasks: test "$(apk info -v chez-scheme)" = chez-scheme-10.3.0-r2 test "$(apk info -v git)" = git-2.54.0-r0 test "$(apk info -v make)" = make-4.4.1-r4 - test "$(git -C ../jerboa rev-parse HEAD)" = 23ad83d28ac65cf6f0d2d702fd32934f207c26bf - test "$(git -C ../jerboa rev-parse 'HEAD^{tree}')" = 6cbc7dd433a88801de82540e74433fc04d2474cd + test "$(git -C ../jerboa rev-parse HEAD)" = 610d17bceac32fd4f42d7e394c5264ee3d761d1a + test "$(git -C ../jerboa rev-parse 'HEAD^{tree}')" = fb3934d1ac782a04daacfe7fca0966f60e22407c JERBOA="chez --libdirs .:../jerboa/lib --script" make test --- a/Makefile +++ b/Makefile @@ -49,6 +49,9 @@ test: clean generate $(JERBOA) jandroid.ss generate $(CLIENT_EXAMPLE) $(CLIENT_BUILD_DIR) test -f $(CLIENT_BUILD_DIR)/app/src/main/java/org/jerboa/sampleclient/SampleClient.kt grep -q 'generated named client' $(CLIENT_BUILD_DIR)/app/src/main/java/org/jerboa/sampleclient/SampleClient.kt + $(JERBOA) jandroid.ss generate tests/fixtures/typed-kotlin-app.ss build/typed-kotlin + test -f build/typed-kotlin/app/src/main/java/org/jerboa/typedfixture/CounterModel.kt # gitsafe:ignore + grep -q 'fun add_one(x: ULong): ULong' build/typed-kotlin/app/src/main/java/org/jerboa/typedfixture/CounterModel.kt # gitsafe:ignore $(MAKE) security $(MAKE) supply-chain --- a/README.md +++ b/README.md @@ -87,6 +87,7 @@ Android project metadata supported by the generator: - `(kotlin-source-dir "relative/path")` - `(fragment "relative/path.ss")` - `(client original-tactics)` +- `(typed-kotlin-file "relative/File.kt" (typed-library ...))` `asset-dir` and `jni-lib-dir` copy directory contents into the generated Android project. This lets app repos keep only Jerboa specs and binary assets @@ -118,6 +119,10 @@ Fragments are expanded into the app spec before generation. They are useful for large generated source sets that should stay in `.ss` files instead of the main app spec. +`typed-kotlin-file` emits a normal Typed Jerboa `typed-library` through the +upstream `(jerboa typed kotlin)` backend. Use it for new generated Kotlin +instead of `kotlin-file`, `kotlin-file-lines`, or `kotlin-source-dir`. + `client` expands a named generator-owned template from `templates/<name>.ss`. This is the preferred bridge for larger apps while the higher-level Android DSL is growing, because application repositories can keep concise Jerboa app specs @@ -142,6 +147,8 @@ configuration and limits are documented in [SECURITY.md](SECURITY.md). ## Direction -The next useful step is a typed backend beside Jerboa's existing Rust and LLVM -emitters, so pure typed Jerboa functions can be emitted to Kotlin and called -from generated Android screens. +The upstream typed backend now provides the first structured Kotlin emitter. +The next Android-specific step is to lower screen/state declarations through +that same AST instead of the legacy `MainActivity.kt` string emitter, then +remove raw Kotlin fragments after the two migrated clients are represented as +typed Jerboa and Android/JVM DSL forms. --- a/dependencies.lock.json +++ b/dependencies.lock.json @@ -11,8 +11,8 @@ "generator_runtime": { "name": "jerboa", "repository": "https://git.sr.ht/~lisp/jerboa", - "commit": "23ad83d28ac65cf6f0d2d702fd32934f207c26bf", - "tree": "6cbc7dd433a88801de82540e74433fc04d2474cd" + "commit": "610d17bceac32fd4f42d7e394c5264ee3d761d1a", + "tree": "fb3934d1ac782a04daacfe7fca0966f60e22407c" }, "assurance_tools": { "osv_scanner": { new file mode 100644 --- /dev/null +++ b/full-kotlin.md @@ -0,0 +1,911 @@ +# Full Jerboa to Kotlin/Android Compiler Plan + +Status: implementation plan +Audience: implementers working in Jerboa and `jerboa-android` +Primary goal: generate a complete Android application from Jerboa source without storing Kotlin or Java source as strings in Scheme + +## 1. Executive decision + +The current repository is an Android project generator with a tiny expression and view emitter. It is not a Jerboa-to-Kotlin compiler. The two large templates are Kotlin source archives encoded as Scheme string lists. That representation must be removed, not extended. + +Build the replacement as four cooperating pieces: + +1. **A target-neutral Jerboa front end and typed high-level IR (HIR).** Reuse and extend Jerboa's existing typed parser, checker, source locations, and typed core instead of adding more cases to `jandroid.ss`. +2. **A structured Kotlin/JVM backend.** Lower HIR into a Kotlin AST (KAST), then render it with a deterministic printer. No compiler stage accepts arbitrary Kotlin text. +3. **A typed JVM/Android interop layer and Android DSL.** Jerboa code must be able to declare classes, override lifecycle methods, call Java/Android APIs, implement callbacks, draw on a `Canvas`, and use files/networking without spelling those operations as Kotlin strings. High-level Android forms lower to the same HIR and JVM interop nodes. +4. **A compatibility compiler for ordinary Jerboa.** Existing `~/sfb/sfb/*.ss` is mostly untyped, list/alist-oriented Jerboa. Compile that code through a small JVM Jerboa runtime so it can be used before it is converted to Typed Jerboa. New code should use the typed lane; existing code must not require a flag-day rewrite. + +Kotlin is the primary output language. Java source generation is a separate backend over the same JVM IR and should be added only for a verified Java-only need. Calling Java libraries does not require generating Java source; normal Kotlin/JVM interop is sufficient. + +## 2. What the repository review found + +### 2.1 Current `jerboa-android` + +- `jandroid.ss` is an 884-line monolithic script that parses a quoted `(android-app ...)` datum and directly concatenates Gradle, XML, and Kotlin strings. +- Its real Kotlin expression language supports literals, symbols, binary `+ - * /`, and `(set ...)`. +- Its UI language supports one screen and `column`, `row`, `text`, `small-text`, `button`, and `spacer`. +- `fragment`, `client`, `kotlin-file`, `kotlin-file-lines`, `kotlin-source-dir`, and raw `(file ...)` are text/copy escape hatches, not compilation. +- `templates/original-tactics.ss` contains 17 Kotlin files and about 10,800 quoted Kotlin lines. +- `templates/ssd-review.ss` contains 9 Kotlin files and about 4,660 quoted Kotlin lines. +- The two real app specs in `~/sfb/android` select those templates with `(client ...)`; their visible `(screen ...)` bodies are placeholders and do not describe the installed applications. +- Existing output confinement in `jandroid/secure-output.ss` is useful and should be retained. It provides descriptor-relative, no-follow, exclusive output and bounded source copying. +- Existing dependency locking, Gradle verification metadata, SDK/JDK checks, SBOM production, and security tests are also useful. Compiler work must preserve these controls. + +### 2.2 Existing Jerboa compiler work + +The vendored Jerboa tree already has the right starting point: + +- `(jerboa typed parser)` parses `typed-library`, records, variants, resources, typed functions, effects, and source annotations. +- `(jerboa typed checker)` validates types/effects and elaborates expressions. +- `(jerboa typed core)` defines typed IR nodes with types and source locations. +- Rust and LLVM backends already consume that IR. +- The existing typed subset includes literals, `begin`, `let`, `if`, `match`, arithmetic/comparison/boolean/bitwise operations, a restricted `for/fold`, bytes operations, records, variants, `Option`, `Result`, and same-module calls. + +Do not fork that model inside `jandroid.ss`. General Kotlin backend work belongs in Jerboa. Android project and Android DSL work belongs in `jerboa-android`. + +Version caveat: this review inspected the clean, shallow `~/sfb/vendor/jerboa` checkout at commit `896d553d84f23e1a92728a3a078c69ff8aad694f`. This repository currently pins Jerboa commit `23ad83d28ac65cf6f0d2d702fd32934f207c26bf`, which is not present in that shallow checkout. Before editing compiler APIs, check out the exact pinned commit (or the intended replacement commit), rerun the typed parser/checker/core inventory, and record any differences. Do not assume the two snapshots expose identical IR. + +### 2.3 `~/sfb` source requirements + +After excluding vendored dependencies and duplicate build/output trees, the authored workspace has 48 `.ss` inputs: + +- 2 Android app specifications. +- 38 rules engine, generated data, and test modules under `sfb/`. +- 1 root test runner. +- 7 operational/reproduction/web tools. + +The non-generated SFB modules are roughly 204,000 lines, with especially large generated API/test expansions. The code relies heavily on: + +- proper and improper lists, alists, pairs, symbols, quoted and quasiquoted data; +- `def`, library imports/exports, local functions, lambdas, named `let`, recursion, `cond`, `case`, and mutation in test infrastructure; +- numeric and boolean primitives, string operations, sorting, maps/folds, vectors and bytevectors; +- structural `equal?` and symbol identity; +- JSON serialization, ports/files, HTTP service boundaries, threads, exceptions, and test-suite macros. + +The Android templates additionally require: + +- classes, data classes, singleton objects, enums, fields, properties, constructors, inheritance, interfaces, annotations, visibility, and method overrides; +- nullable/platform types, generics, overload resolution, varargs, casts, type tests, static members, getters/setters, and callbacks; +- `when`, loops, early return, exceptions, `try/catch/finally`, resource cleanup, and mutable collections; +- Android activity lifecycle, custom `View`/`ViewGroup`, `Canvas`, gestures, animation, dialogs, permissions, storage, assets, PDF rendering, audio, and UI controls; +- Java file/network/TLS/ZIP/crypto/time APIs, JSON, ML Kit, native libraries, and threads. + +A useful compiler has to cover these categories through language semantics or typed interop. A larger catalog of hard-coded widgets will not solve the problem. + +## 3. Product definition + +### 3.1 Required user experience + +The normal source tree should look like this: + +```text +app.ss structured Android project declaration +src/app/main.ss typed Jerboa Android component code +src/app/model.ss typed portable Jerboa +src/legacy/sfb/*.ss ordinary Jerboa compatibility modules +resources/ images, XML data, fonts, and other assets +native/ reviewed .so inputs, when needed +``` + +Normal commands: + +```sh +jerboa android check app.ss +jerboa android generate app.ss --out build/generated +jerboa android build app.ss +jerboa kotlin emit src/app/model.ss --out build/kotlin +``` + +`check` must parse, expand, type-check, resolve JVM calls, validate Android metadata, and report all useful diagnostics without writing a project. `generate` must produce deterministic, readable source. `build` must run generation and the pinned, verified Android build. + +### 3.2 Definition of "full Kotlin" + +For this project, full support means all of the following: + +1. Typed Jerboa declarations and expressions needed by the two applications lower to structured, readable Kotlin. +2. Ordinary Jerboa production modules used by SFB compile with compatible observable behavior through the JVM compatibility runtime. +3. Android components and JVM calls are written as checked Jerboa forms, not target-language strings. +4. Android project metadata, resources, manifests, and Gradle configuration are structured data with validation. +5. Generated Kotlin compiles with the pinned Kotlin/AGP/JDK/SDK toolchain. +6. The counter example and both real Android apps contain no generated source hidden in `.ss` strings. +7. Public compiler APIs have no `raw-kotlin`, `kotlin-file`, `kotlin-file-lines`, `emit-verbatim`, or equivalent facility. + +This does not require compiling every possible Chez Scheme feature. Runtime `eval`, arbitrary macro generation after compilation, first-class continuations, arbitrary Chez FFI declarations, and dynamic loading need explicit profiles or a clear compile-time rejection. They must never silently produce incorrect Kotlin. + +## 4. Design principles + +1. **Scheme is source, Kotlin is output.** Kotlin text is an artifact, never the semantic input. +2. **One semantic pipeline.** The Android DSL, typed functions, and JVM interop all lower into shared checked IR before rendering. +3. **Macros produce syntax, not text.** Jerboa macros/templates may construct app, declaration, expression, and resource AST nodes with source locations. They may not return Kotlin fragments. +4. **Portable core, explicit boundary.** Domain logic should not know Android types. JVM and Android effects appear only in modules that import those capabilities. +5. **Preserve semantics before optimizing style.** Existing ordinary Jerboa initially compiles to a compatibility representation. Typed modules compile to idiomatic Kotlin. +6. **No ambiguous magic.** Overloaded JVM calls, numeric narrowing, null conversion, ownership, blocking work, and UI-thread transitions must be explicit when inference cannot prove them. +7. **Determinism and reviewability.** Stable ordering, stable names, canonical formatting, source maps, and no timestamps in generated files. +8. **Fail closed.** Unknown forms, unresolved methods, unsafe paths, unsupported effects, API-level violations, and output collisions are errors. +9. **Models get a small grammar.** Prefer a small set of orthogonal declarations and expressions over one special form per Android class. + +## 5. Source language model + +Use three source layers. They are distinct for checking, but can coexist in a project. + +### 5.1 Typed Jerboa: portable application logic + +Keep `typed-library` as the source form and extend it rather than inventing another typed language. + +```scheme +(typed-library (app counter model) + (export make-State State? State-count increment display-count) + + (record State + ((count : Int))) + + (def (increment (state : State)) : State + (make-State (+ (State-count state) 1))) + + (def (display-count (state : State)) : String + (string-append "Count: " (int->string (State-count state))))) +``` + +Typed Jerboa should remain backend-neutral. Kotlin-specific concepts enter through imported JVM declarations, not through raw syntax. + +### 5.2 Typed JVM declarations and expressions + +Add a `jvm-library` declaration form that uses ordinary typed Jerboa expressions plus a small number of JVM-specific operations. + +Illustrative surface syntax: + +```scheme +(jvm-library (app counter main) + (package "org.jerboa.counter") + (export MainActivity) + (import (app counter model)) + (jvm-import android.app.Activity + android.os.Bundle + android.widget.Button + android.widget.LinearLayout + android.widget.TextView) + + (class MainActivity + (extends Activity) + + (field (mut state : State) (make-State 0) #:private) + + (override (onCreate (saved : (Nullable Bundle))) : Unit + (super-call onCreate saved) + (let ((root (new LinearLayout this)) + (label (new TextView this)) + (button (new Button this))) + (.setOrientation root LinearLayout/VERTICAL) + (.setText label (display-count state)) + (.setText button "Increment") + (.setOnClickListener button + (callback ((view : View)) + (set! state (increment state)) + (.setText label (display-count state)))) + (.addView root label) + (.addView root button) + (.setContentView this root))))) +``` + +The exact spelling can be adjusted during implementation, but the semantic set must remain small: + +- `class`, `interface`, `object`, `enum`, annotation, visibility, constructor, field/property, method, and override declarations; +- `new`, instance call, static call/member, `super-call`, property get/set, cast, type test, callback/lambda, null, and non-null assertion/check; +- structured `try`, `throw`, loops, `return`, `break`, and `continue` where typed Jerboa expression semantics are insufficient; +- explicit overload signature only when the binding index cannot select one uniquely. + +These forms create typed AST nodes. They must not concatenate strings. + +### 5.3 Android project and UI DSL + +The project form owns metadata and source modules. It is not quoted Kotlin. + +```scheme +(android-project counter + (application-id "org.jerboa.counter") + (display-name "Jerboa Counter") + (version 1 "0.1.0") + (sdk #:min 26 #:target 35 #:compile 35) + (toolchain #:jdk 17 #:kotlin "2.0.21" #:agp "8.13.2") + (dependency "androidx.activity" "activity" "1.10.1") + (resource-dir "resources") + (module (app counter model)) + (module (app counter main)) + (launcher MainActivity)) +``` + +Provide an optional high-level View DSL for common screens: + +```scheme +(activity MainActivity #:launcher + (state (model : State) (make-State 0)) + (content + (column #:padding (dp 24) #:gravity center + (text (display-count model) #:size (sp 28)) + (space (dp 12)) + (button "Increment" + (set! model (increment model)))))) +``` + +This DSL expands into normal checked Android/JVM AST. Custom views, drawing, touch handling, storage, and networking use typed JVM forms rather than waiting for a bespoke DSL form. Compose can be an additional lowering plugin later; the initial backend should target Android Views because that matches both existing applications and avoids adding a large runtime dependency. + +### 5.4 Structured build and resource forms + +Keep structured declarations for: + +- manifest application/activity/service/provider/receiver declarations; +- permissions with API constraints; +- string, color, dimension, style, drawable, raw, XML, and asset resources; +- build types, product flavors, ABI filters, native libraries, ProGuard/R8 rules, packaging, and test dependencies; +- Maven dependencies as exact coordinates plus locked checksums; +- generated `BuildConfig` constants with non-secret values. + +Do not expose raw Gradle or XML insertion. When an unsupported Gradle feature appears, add a typed build-model node and validation for it. A user-owned conventional source/resource directory can remain as a temporary migration input, clearly reported by `check`, but it is not compiler success. + +## 6. Compiler architecture + +### 6.1 Ownership and repository boundaries + +Changes to the general compiler belong in the upstream Jerboa repository: + +```text +lib/jerboa/typed/core.ss target-neutral typed HIR +lib/jerboa/typed/parser.ss typed surface parsing +lib/jerboa/typed/checker.ss types, effects, ownership, elaboration +lib/jerboa/typed/kotlin/ast.ss structured Kotlin AST +lib/jerboa/typed/kotlin/lower.ss HIR to KAST +lib/jerboa/typed/kotlin/print.ss canonical renderer +lib/jerboa/typed/kotlin.ss public backend API +lib/jerboa/jvm/signature.ss JVM type/signature model +lib/jerboa/jvm/index.ss classpath/API binding index +lib/jerboa/jvm/checker.ss JVM overload/null/effect checks +lib/jerboa/jvm/runtime/ compatibility runtime source/resources +support/typed-kotlin.ss command-line backend driver +tests/test-typed-kotlin.ss backend unit/golden tests +tests/fixtures/typed/kotlin/ compiler fixtures +``` + +Android-specific work belongs here: + +```text +lib/jandroid/project.ss project AST/parser/validation +lib/jandroid/android-ast.ss Android declarations and UI nodes +lib/jandroid/lower.ss Android DSL to typed JVM HIR +lib/jandroid/gradle-ast.ss structured Gradle model +lib/jandroid/gradle-print.ss Gradle Kotlin DSL renderer +lib/jandroid/resource.ss manifest/resource AST and writers +lib/jandroid/generate.ss orchestration and output plan +lib/jandroid/secure-output.ss retained hardened output capability +support/jandroid.ss thin CLI +tests/compiler/ parser/checker/lowering tests +tests/e2e/ generated Android projects +``` + +Do not implement a second typed parser/checker in `jerboa-android`. During development, point `JERBOA_HOME` or `--libdirs` at a sibling Jerboa checkout. Once compiler changes land upstream, update the pinned Jerboa commit and tree in `dependencies.lock.json` and `.build.yml` together. + +### 6.2 Pipeline + +The generation pipeline must be visible and independently testable: + +```text +source files + -> source-aware reader + -> hygienic macro expansion + -> module/import resolution + -> surface AST + -> type/effect/JVM signature checking + -> target-neutral typed HIR + -> optional ordinary-Jerboa compatibility lowering + -> JVM IR (classes, members, calls, control flow) + -> Kotlin AST + -> canonical Kotlin documents + -> output plan + -> confined filesystem writer + -> Kotlin compiler / Android build +``` + +Every boundary should have a data predicate, constructor API, validator, and debug printer. The renderer should only accept a validated KAST. The filesystem writer should only accept a validated output plan with normalized relative paths and byte content. + +### 6.3 Extend the typed HIR before writing emitters + +The current typed core is too small for Android code. Add target-neutral nodes in coherent groups: + +1. Collection construction/access/update for lists, vectors, maps, sets, and byte arrays. +2. General lambdas and typed calls, including closures. +3. Local recursion and tail-position information. +4. Mutation, assignment, and scoped mutable bindings. +5. General iteration (`for`, `while`, sequence iteration, folds with multiple accumulators). +6. Early return/break/continue represented as checked control flow. +7. Exceptions, `try/catch/finally`, and resource scopes. +8. Nullable values only in the JVM layer; portable code continues to use `Option`. +9. Module-qualified references and cross-module call signatures. +10. Constants and top-level initialization with dependency ordering. + +Do not encode these as emitter-specific alists. Use records like the existing `typed-ir-*` records and retain inferred type, effects, and source on each node. + +### 6.4 JVM IR + +Introduce an IR between typed HIR and Kotlin syntax. It should describe JVM meaning, not Kotlin spelling: + +- package/import aliases; +- class/interface/enum/object kind; +- generic parameters and bounds; +- annotations and modifiers; +- primary/secondary constructors; +- fields, properties, accessors, methods, static/companion members; +- inheritance and implemented interfaces; +- typed method/constructor/field references with resolved JVM descriptors; +- expression/statement control flow; +- nullability and platform type facts; +- source origin and requested Android API level. + +This makes a later Java printer possible and prevents Android logic from depending on Kotlin formatting details. + +### 6.5 Kotlin AST and printer + +KAST must have explicit nodes for files, imports, declarations, types, expressions, statements, string/char/numeric literals, annotations, and comments. Use a small document algebra (`text`, `line`, `nest`, `group`, `concat`) for formatting instead of indentation embedded in arbitrary strings. + +Printer requirements: + +- syntactically valid Kotlin for every valid KAST; +- stable formatting and declaration/import order; +- correct precedence and parentheses; +- complete string/char escaping, including `$`, Unicode controls, and triple-quote decisions; +- Kotlin keyword escaping and deterministic Jerboa-name mangling; +- no unstructured source payload node; +- source comments only when requested, plus a machine-readable source map from generated spans to `.ss` locations; +- round-trip syntax validation with the pinned Kotlin compiler in tests. + +Identifier mapping must handle hyphens, `?`, `!`, operators, leading digits, case collisions, Kotlin keywords, JVM signature collisions, and generated temporary names. Store the mapping in compiler state; never reconstruct names ad hoc in printers. + +## 7. Type and semantic mapping + +### 7.1 Typed lane + +Define mappings once in a backend contract and test edge cases: + +| Jerboa type | Kotlin representation | Notes | +| --- | --- | --- | +| `Unit` | `Unit` | No accidental `null`/`void` mixing | +| `Bool` | `Boolean` | Scheme truth rules apply only in compatibility lane | +| `Char` | `Char` | Validate Unicode scalar/code-unit policy | +| `Int` | `Long` | Match existing typed backend's signed 64-bit contract | +| `Nat` | `ULong` | Checked conversion at Java/Android boundaries | +| `Fixnum` | `Long` | Document target-independent fixed range | +| `Float` | `Double` | Preserve current typed meaning | +| `String` | `String` | Non-null in portable typed code | +| `Bytes` | `ByteArray` | Equality must be content equality in Jerboa operations | +| `Symbol` | `JerboaSymbol` | Interned value, not a Kotlin string | +| `(List T)` | `List<T>` | Persistent-by-contract; copy on mutation operations | +| `(Vector T)` | `List<T>` initially | Add mutable vector representation only when required | +| `(Pair A B)` | `JerboaPair<A,B>` | Must support improper pairs | +| `(Option T)` | `JOption<T>` | Do not use nullable `T?`; nested options must be representable | +| `(Result T E)` | `JResult<T,E>` | Sealed success/error representation | +| record | `data class` or class | Mutable field forces class/`var` as needed | +| variant | sealed interface + cases | Exhaustive `when` lowering | +| resource | closeable wrapper | Ownership/effect checker controls use | + +Add explicit fixed-width JVM types (`I8`, `I16`, `I32`, `I64`, `U8`, and so on) or checked conversion primitives. Android APIs overwhelmingly use 32-bit `int`; implicit narrowing from Jerboa `Int` must not be allowed. + +### 7.2 Equality and arithmetic + +Generate helper calls when Kotlin operators have different semantics: + +- structural `equal?` must compare arrays and Jerboa data by content; +- `eq?` on interned symbols is identity/value identity as specified; +- byte arrays need content equality and content hash; +- division, remainder, overflow, unsigned operations, shifts, NaN, and negative zero need differential tests against the Jerboa typed contract; +- typed integer overflow policy must be explicit: checked, wrapping, or fixed-width. Do not inherit Kotlin overflow accidentally. + +### 7.3 Options, results, and nullability + +Portable code never sees a platform type. JVM signatures classify values as non-null, nullable, or unknown-platform. Boundary adapters perform: + +- `JOption<T>` to/from nullable references; +- checked primitive boxing/unboxing; +- `Result` to an explicit value or declared exception mapping; +- platform-null checks with source-aware error messages. + +Nested `Option`, `Option<Unit>`, and nullable Java generics are mandatory tests. + +### 7.4 Tail calls and recursion + +Kotlin/JVM cannot rely on general tail-call optimization. + +- Self-tail recursion lowers to a `while` loop with parameter reassignment. +- Mutually recursive tail calls lower to a generated state machine when the strongly connected component is eligible. +- Other deep recursion in the compatibility lane uses a trampoline. +- Non-tail recursion remains normal JVM recursion and should produce a warning when static analysis identifies an obviously unbounded path. + +Named `let`, which is common in SFB, must lower through this mechanism rather than recursively consuming the JVM stack. + +### 7.5 Effects and threads + +Extend effects with JVM/Android facts rather than hiding them: + +- `ui` for main-thread Android UI operations; +- `io`, `network`, `block`, `mut`, `throw`, `native`, and `unsafe` as applicable; +- callback interfaces record the thread/effect context they invoke; +- UI calls from a background effect require an explicit dispatcher operation; +- blocking work in `onCreate`, draw, touch, or UI callbacks is a checker error or high-severity diagnostic. + +## 8. JVM and Android binding system + +### 8.1 Signature index + +The checker needs more than class names. Build a deterministic binding index from: + +- the pinned JDK runtime API; +- `android.jar` for the selected compile SDK; +- exact resolved dependency jars/aars; +- small checked override files for nullability/effect/API facts not recoverable from bytecode. + +Each entry contains owner, JVM name, descriptor, generic signature, static/instance kind, visibility, nullability, thrown exceptions, Android API introduction/deprecation level, and known effects. + +Cache the index by toolchain/dependency digests. Record its digest in provenance. Do not scan arbitrary ambient classpaths. + +### 8.2 Resolution rules + +For each constructor/method/property call: + +1. Resolve the receiver and imported owner. +2. Filter by name, visibility, static kind, and API level. +3. Check arity, varargs, generics, nullability, and allowed numeric conversions. +4. Rank only conversions that Kotlin/Java actually supports. +5. Require an explicit descriptor/signature when more than one best candidate remains. +6. Store the selected JVM member in IR; the Kotlin printer does no overload resolution. + +Diagnostics should list the attempted signature and the closest candidates with source locations. + +### 8.3 Callbacks and inheritance + +Support SAM interfaces, anonymous objects, and named class implementations. A `callback` is checked against the expected interface method and lowers to a Kotlin lambda only when SAM conversion is legal. Otherwise generate an object expression or named class. + +Override checking must validate: + +- exact JVM override target; +- parameter and return variance; +- visibility and final/abstract constraints; +- checked nullability; +- required `super` calls where Android lifecycle policy demands them. + +### 8.4 Android API-level checking + +Compare every resolved API entry with `min-sdk` and guards in control-flow facts. Calls above `min-sdk` require one of: + +- a statically proven `SDK_INT` guard; +- an annotated wrapper with a fallback; +- a project-level minimum SDK increase. + +Emit the same information in a report so reviewers can audit platform reachability. + +## 9. Ordinary Jerboa compatibility lane + +Typed Jerboa alone cannot compile the current SFB libraries. Add a compatibility profile that compiles expanded ordinary Jerboa into Kotlin using a small runtime. + +### 9.1 Compile-time expansion + +Run Jerboa macros on the build host, preserve source locations through expansion, and compile the expanded core. Do not ship a macro expander in the APK. Record both original source digests and deterministic expanded-form digests. + +The first implementation task is an expansion audit: feed every authored SFB production module through the normal Jerboa expander and inventory the residual core forms. That inventory defines the compatibility compiler backlog; source-text regexes do not. + +### 9.2 Runtime representation + +Use a deliberately small runtime, for example: + +- `JNil` distinct from false; +- `JPair` for proper/improper lists and alists; +- interned `JSymbol` and `JKeyword`; +- booleans, chars, strings, byte arrays, vectors, and numeric values; +- `JProcedure`/closure with arity metadata; +- multiple-values carrier; +- Jerboa condition/exception wrapper; +- ports and capabilities only for explicitly supported Android/JVM services. + +`JValue` may be represented as `Any?` internally for practical JVM interop, but all operations must go through tested semantic helpers. Never use Kotlin truthiness, reference equality, list equality, number coercion, or `null` as an accidental Scheme semantic. + +Exact ordinary-Jerboa integers should use `Long` fast paths with `BigInteger` promotion so arithmetic does not silently overflow. Generated static data should use compact initialization tables or serialized resources where Kotlin method/class limits would otherwise be exceeded. + +### 9.3 Core forms to support + +Prioritize the expanded forms used by SFB: + +- literals, quote, quasiquote after expansion, variables, definition, assignment; +- lambda, fixed/rest arity, calls, closures; +- `if`, `begin`, `let`, `let*`, named `let`, `letrec`, `cond`, `case`, `and`, `or` after expansion; +- pairs/lists/alists, symbols, vectors, bytevectors, strings, numbers; +- values/multiple values where present; +- exceptions/guards and `dynamic-wind` where present; +- module import/export and top-level initialization; +- host service bindings for JSON, files, HTTP/thread tools only when the Android target actually includes them. + +Unsupported expanded primitives are compilation errors collected into a feature report. Add runtime primitives by category and test each against host Jerboa before migrating application code. + +### 9.4 Typed/compatibility bridge + +Generate adapters only at explicit exported boundaries: + +- typed record/variant to a documented legacy alist/list schema; +- typed scalar/collection to compatible values; +- compatibility result to typed `Option`/`Result` with validation; +- JSON strings/bytes as a preferred coarse boundary for the existing SFB service API. + +For the SFB application, the lowest-risk initial integration is to compile the existing request/response service boundary and call it from typed Android UI. That keeps the rules engine unchanged while new UI code remains typed. + +## 10. Android generator redesign + +### 10.1 Split the current monolith + +Break `jandroid.ss` into libraries before adding language features. The CLI should do only argument parsing and orchestration. Parsing, validation, lowering, rendering, copying, security, and build execution must be separate modules with unit tests. + +### 10.2 Output plan + +All renderers return an immutable output plan: + +```scheme +(output-plan + (file "settings.gradle.kts" gradle-settings-bytes generated) + (file "app/src/main/AndroidManifest.xml" manifest-bytes generated) + (file "app/src/main/java/org/example/MainActivity.kt" kotlin-bytes generated) + (copy "resources/icon.png" "app/src/main/res/drawable/icon.png" asset)) +``` + +Validate the complete plan before opening the output root: + +- normalized, allowed paths; +- no duplicate/case-folding collisions; +- file count/size/total budgets; +- source kind and extension rules; +- no generated file overwritten by copied input; +- no missing launcher/resource/dependency references. + +Then execute it through the existing secure output capability. + +### 10.3 Gradle and manifest generation + +Replace `string-append` Gradle/XML construction with structured AST plus escaping printers. Keep all existing supply-chain behavior. Move hard-coded dependency constraints into versioned, validated toolchain policy data rather than interpolated source lines. + +The project validator must check package names, versions, SDK relationships, immutable dependencies, component exports, permission/API compatibility, native ABI availability, resource names, and dependency-lock coverage before output. + +### 10.4 Generated source layout + +Use one Kotlin file per source module or top-level public class unless JVM initialization constraints require a companion file. Put runtime code in a stable `org.jerboa.runtime` package. Generated app code uses the application's package. + +Add a header containing generator version, input digest, and a do-not-edit notice, but no wall-clock timestamp. Generate `jerboa-source-map.json` and `jerboa-build-manifest.json` alongside the project. + +## 11. Human and model ergonomics + +### 11.1 Small, documented grammar + +Publish a concise reference containing: + +- every declaration and expression form; +- expected type and effect rules; +- 1-3 canonical examples per form; +- common compiler errors and fixes; +- an Android cookbook for activities, custom views, dialogs, storage, networking, and native calls; +- a machine-readable grammar/schema version. + +Avoid aliases until the core grammar is stable. One canonical spelling is easier for humans, formatters, and models. + +### 11.2 Formatter and inspector + +Provide: + +```sh +jerboa fmt app.ss src/**/*.ss +jerboa android check app.ss --explain +jerboa android dump-ir app.ss --stage hir +jerboa android dump-ir app.ss --stage jvm +jerboa android api android.widget.TextView.setText +``` + +`api` shows available overloads and the corresponding Jerboa call signature. `dump-ir` must use readable S-expressions, making implementation and model debugging possible without reading generated Kotlin. + +### 11.3 Diagnostics + +Every diagnostic needs: + +- source path, line, and column; +- stable diagnostic code; +- form/type/effect that was expected and received; +- related declaration/candidate locations; +- one actionable hint when possible; +- no generated-Kotlin stack trace as the primary error. + +When `kotlinc` or Gradle still rejects generated output, map its generated span back to the Jerboa source map and include both locations. + +### 11.4 Templates done correctly + +Templates remain useful only as Jerboa macros or functions that return validated AST values. For example, a standard toolbar template can accept typed actions and return a `view-node`. The constructor must attach call-site source information. It cannot accept or return Kotlin strings. + +## 12. Implementation sequence and gates + +Implement in small, testable increments. Do not begin by translating the 15,500 string lines into token-shaped S-expressions. + +### Phase 0: freeze behavior and remove the false claim + +Deliverables: + +- Add this plan to the repository and update roadmap terminology: current templates are migration snapshots, not generated clients. +- Check out the exact pinned Jerboa dependency, compare its typed parser/checker/core/backend APIs with the reviewed `~/sfb/vendor/jerboa` snapshot, and write the compatibility delta into the first compiler change. +- Add a census tool that reports raw-source forms, copied Kotlin, generated file count, and DSL coverage. +- Extract the quoted Kotlin templates into conventional `.kt` fixture/source trees as a temporary migration step. Preserve exact compiled behavior and history; stop editing Kotlin through escaped Scheme strings. +- Keep `client` only as a deprecated pointer to those temporary trees and print a warning. +- Capture clean generated-project and APK baselines for counter, SSD review, and Original Tactics. + +Gate: + +- No behavior change; all current tests and both real app compiles pass. +- No new `kotlin-file*` content is accepted in reviews. + +### Phase 1: KAST and canonical printer + +Deliverables: + +- KAST records, validators, identifier mapper, literal escaping, document formatter, and source map builder. +- Property-based/generative tests for identifiers, literals, precedence, nesting, and deterministic output. +- Golden files for representative Kotlin constructs already present in the clients. + +Gate: + +- Every KAST fixture parses/compiles with pinned `kotlinc`. +- No KAST node contains arbitrary source text. + +### Phase 2: existing Typed Jerboa to Kotlin + +Deliverables: + +- Kotlin lowering for the complete currently accepted typed IR. +- Records, variants, options/results, matches, functions, imports, numeric/bytes/string primitives, loops already represented in IR. +- `support/typed-kotlin.ss` and public backend API parallel to Rust. +- Cross-backend semantic tests: evaluate host Jerboa, compile/run Kotlin, compare output. + +Gate: + +- Every existing typed fixture supported by Rust has either matching Kotlin behavior or an explicit backend capability diagnostic. +- Counter model logic compiles from Typed Jerboa without Android dependencies. + +### Phase 3: project model and output planner + +Deliverables: + +- Parsed/validated `android-project` form. +- Structured Gradle, manifest, resource, dependency, and output-plan modules. +- Existing secure writer adapted to execute output plans. +- CLI `check`, `generate`, and `build` commands. + +Gate: + +- Counter project skeleton is byte-for-byte deterministic and passes existing security/supply-chain tests. + +### Phase 4: JVM signature index and typed interop + +Deliverables: + +- Reproducible JDK/Android/dependency signature index. +- JVM types, nullability, overload resolution, constructors, methods, fields/properties, callbacks, exceptions, and API-level checking. +- JVM class/interface/object declarations and inheritance/override checking. +- Query command for bindings. + +Gate: + +- Focused fixtures cover overloaded Android calls, SAM callbacks, anonymous interfaces, nullable platform APIs, generics, varargs, exceptions, inheritance, and lifecycle override. +- No fixture relies on raw Kotlin. + +### Phase 5: Android Views DSL and counter migration + +Deliverables: + +- Activity/content/state/event forms lowering to JVM HIR. +- Common View widgets and layout/style/resource values. +- Lifecycle/state restoration and UI-thread effect rules. +- Counter app rewritten entirely in the new source language. + +Gate: + +- `rg 'kotlin-file|kotlin-source-dir|raw-kotlin' examples/counter` finds nothing. +- Generated counter APK builds and an instrumentation/screenshot test can increment and restore the count. + +### Phase 6: ordinary Jerboa compatibility compiler + +Deliverables: + +- Expansion inventory over all authored SFB production `.ss` files. +- Compatibility core AST/lowering, runtime values/primitives, module initialization, closure conversion, trampoline, and errors. +- Differential runner comparing exported function calls in host Jerboa and JVM output. +- Explicit unsupported-feature report. + +Gate: + +- Geometry, movement, RNG, timing, combat, seeking, energy, ships, rules engine, API, and service production libraries compile in dependency order. +- Their production test suites pass through a JVM test adapter or differential corpus. Large generated data stays below JVM method/class limits. + +### Phase 7: SFB service bridge + +Deliverables: + +- Typed adapter around the compiled `handle-service-json` boundary. +- Android-side background execution, timeout/cancellation, and error mapping. +- Eliminate any need for a remote Mac rules service for local rules operations that are compiled into the APK. + +Gate: + +- A recorded request corpus produces semantically identical JSON in host Jerboa and Android/JVM. +- No rules call blocks the UI thread. + +### Phase 8: SSD Review migration + +Migrate by coherent vertical slices, not file-by-file transliteration: + +1. models and box-type data; +2. pure guessing/feature logic; +3. local truth storage and bounded I/O helpers; +4. drawing and gesture custom view; +5. PDF/image/OCR/ML Kit adapters; +6. activity UI and lifecycle; +7. remote sync/TLS/ZIP security path. + +At each slice, preserve the existing security assertions and add source-level tests. + +Gate: + +- SSD Review builds with no quoted/copied Kotlin application code. +- Existing TLS pinning, redirect rejection, path containment, ZIP budgets, storage budgets, and bounded read/write tests still pass. + +### Phase 9: Original Tactics migration + +Migrate by subsystem: + +1. hex math and pure UI models; +2. rules client replaced by the local compiled SFB bridge; +3. individual status/timeline/command panels; +4. tactical map drawing and gestures; +5. assets/audio/custom layout; +6. main activity orchestration and lifecycle. + +Gate: + +- Original Tactics builds and runs without Kotlin source inputs. +- Golden rendering/interaction tests cover the tactical map and main panels. + +### Phase 10: deletion and enforcement + +Deliverables: + +- Delete `templates/original-tactics.ss`, `templates/ssd-review.ss`, `kotlin-file`, `kotlin-file-lines`, and generator-owned `kotlin-source-dir` support. +- Remove the placeholder screen fallback and old direct Kotlin emitter from `jandroid.ss`. +- Add CI checks rejecting suspicious raw target-source payloads in `.ss` files and application-owned generated `.kt` inputs. +- Update documentation and security model to the compiler architecture. + +Gate: + +- All three applications build from Jerboa plus declared binary/assets/resources. +- A clean checkout can reproduce outputs and release evidence. + +### Phase 11: Java backend only if justified + +Add Java AST/lowering/printing over JVM IR if an annotation processor, framework, or external consumer demonstrably requires Java source. It must meet the same no-verbatim, deterministic, source-map, and compile-test requirements. Do not block the Android/Kotlin compiler on this phase. + +## 13. Testing strategy + +### 13.1 Compiler unit tests + +- parser success/failure for every form; +- type, effect, nullability, ownership, API-level, import, and overload errors; +- HIR/JVM IR/KAST invariants; +- identifier/literal escaping and precedence; +- deterministic ordering and source locations; +- malformed and adversarial source depth/size limits. + +### 13.2 Differential semantic tests + +For pure and compatibility code: + +1. Run a function/corpus in host Jerboa. +2. Compile the same module to Kotlin/JVM. +3. Run it in an isolated JVM process. +4. Compare canonical serialized values or typed results. + +Cover numeric boundaries, improper lists, nested alists, symbols, equality, recursion depth, exceptions, byte arrays, records, variants, options/results, and randomized rules-engine states. + +### 13.3 Backend syntax tests + +- Compile every generated Kotlin fixture with the pinned compiler. +- Run JVM unit tests without Android where possible. +- Compile Android fixtures against min and compile SDK contracts. +- Test generated code with warnings-as-errors after the backend stabilizes. + +### 13.4 Android end-to-end tests + +- Gradle compile for debug and release configurations. +- Instrumented lifecycle, state restoration, permission, storage, and callback tests. +- Screenshot/golden tests for fixed custom-view states. +- Gesture tests for pan/zoom/tap and layout tests across representative viewport/density/font-scale combinations. +- Network/TLS tests use controlled local endpoints and retain all current negative security cases. + +### 13.5 Reproducibility and security tests + +- Generate twice in separate directories and compare all bytes except explicitly documented build-tool artifacts. +- Fuzz paths, package/resource names, class/member names, literals, deep forms, huge forms, cyclic imports, and dependency metadata. +- Preserve descriptor-relative output, exclusive creation, no-follow traversal, budgets, exact dependency versions, artifact verification, SBOMs, and advisory scans. +- Treat compiler plugins, binding indexes, formatter binaries, and runtime libraries as pinned build dependencies in provenance. + +## 14. Performance and scale + +The SFB source/data size makes scale a design constraint, not a later optimization. + +- Cache reader/expanded AST/typechecked module/JVM index/rendered output by content digest and compiler version. +- Compile modules independently after an import graph/type-signature pass. +- Keep generated Kotlin functions and class initializers below JVM bytecode limits; shard large constants and prefer compact binary/JSON resources when data is not executable code. +- Avoid a Kotlin expression per generated datum in the 13,700-line rules dataset. +- Add benchmark gates for clean check, incremental one-module check, Kotlin compilation, APK size, startup, service request latency, custom-view frame time, and compatibility-runtime allocation. +- Profile before replacing compatibility values with specialized representations. Typed boundaries are the long-term performance path. + +## 15. Migration rules + +1. Do not mechanically wrap each Kotlin token in an S-expression. That is the current problem with more punctuation. +2. Do not add raw target-language escape hatches, even temporarily, to the new AST. Keep transitional `.kt` sources visibly conventional and outside compiler success metrics. +3. Migrate pure logic before Android orchestration. +4. Keep JVM/Android calls at narrow adapter boundaries. +5. Use differential tests before refactoring existing SFB data shapes into records/variants. +6. Convert legacy alists to typed records only when a subsystem is stable and its serialized/service schema is covered. +7. Every migrated slice deletes its old Kotlin input in the same change after parity tests pass. +8. Generated Kotlin is never hand-edited. A failure is fixed in source, lowering, bindings, or the printer. + +## 16. Risks and mitigations + +| Risk | Mitigation | +| --- | --- | +| Typed Jerboa subset grows without architectural control | Extend source AST and HIR by semantic groups; require checker and differential tests before emitter support | +| JVM interop becomes a second Kotlin syntax | Keep only typed semantic operations and resolve to JVM descriptors before KAST | +| Existing SFB rewrite dominates the project | Compatibility lane plus JSON service boundary; typed migration is incremental | +| Dynamic semantics differ subtly | Central runtime helpers and host/JVM differential corpus | +| Kotlin/JVM method or initializer limits | Shard declarations, tail-loop lowering, compact resource encoding, bytecode-size tests | +| Android API/nullability metadata is incomplete | Pinned signature index plus reviewed override facts and explicit ambiguity errors | +| Generated code is unreadable | Canonical KAST printer, source mapping, idiomatic typed lowering, golden review | +| Build security regresses during rewrite | Preserve output capability and supply-chain tests as phase gates, not cleanup work | +| Macros hide target code | Macros can construct only validated AST; expanded-form dump and digest in evidence | +| A lesser implementation model takes shortcuts | Phase gates reject raw strings, require compiler parsing, and specify deletion criteria | + +## 17. Definition of done + +The project is complete only when all of these are true: + +- `jandroid.ss` is a thin compatibility CLI or has been replaced by modular libraries and a thin CLI. +- The general Typed Jerboa Kotlin backend lives with Jerboa's other typed backends and passes cross-backend tests. +- JVM signatures, overloads, generics, callbacks, inheritance, nullability, exceptions, and Android API levels are checked before rendering. +- The Android project/UI DSL lowers through checked IR and can express ordinary screens plus custom Android classes. +- Required ordinary SFB production modules compile and match host Jerboa behavior at the service boundary. +- Counter, SSD Review, and Original Tactics build from Jerboa sources without application Kotlin/Java source strings or copied source directories. +- `templates/original-tactics.ss` and `templates/ssd-review.ss` are deleted. +- The public AST/compiler API cannot represent verbatim Kotlin or Java. +- Generated projects are deterministic, confined, dependency-verified, source-mapped, testable, and release-evidenced. + +## 18. First implementation backlog + +The first implementer should execute these tasks in order and stop at each failing gate: + +1. Add a test that counts and rejects new `kotlin-file*` forms. +2. Add a script that extracts current template strings to temporary conventional `.kt` trees and proves byte equality with current generated output. +3. Split `jandroid.ss` parsing, model, rendering, output planning, and CLI without changing output. +4. Implement KAST data records and validators with no renderer. +5. Implement identifier and literal rendering tests. +6. Implement the document printer and compile its fixtures with pinned Kotlin. +7. Add `(jerboa typed kotlin)` using existing elaborated typed IR. +8. Port the smallest typed Rust fixtures and establish host/Kotlin differential execution. +9. Complete coverage of the existing typed core. +10. Add the structured Android project model while retaining the current secure writer. +11. Generate the counter project skeleton through the new project path. +12. Build the JVM signature index for JDK plus `android.jar`. +13. Add constructor/method/field/static-call resolution and diagnostics. +14. Add JVM class declarations, overrides, callbacks, and nullability. +15. Rewrite counter fully in Typed Jerboa and Android DSL. +16. Run the ordinary-Jerboa expansion audit over `~/sfb/sfb` and commit the generated feature inventory as a test fixture. +17. Implement compatibility runtime/compiler primitives by inventory frequency, always with differential tests. +18. Compile the SFB JSON service boundary. +19. Migrate SSD Review by the phase-8 slices. +20. Migrate Original Tactics by the phase-9 slices. +21. Delete all raw/copy escape hatches and enforce the final repository invariant. + +The critical path is KAST -> current Typed Jerboa backend -> JVM bindings -> counter -> compatibility service bridge -> the two real apps. Work outside that path should not delay removal of the raw Kotlin templates. --- a/jandroid.ss +++ b/jandroid.ss @@ -1,5 +1,6 @@ (import (jerboa prelude) (only (chezscheme) file-directory?) + (jerboa typed kotlin) (jandroid secure-output)) (def *max-copy-files* 10000) @@ -220,6 +221,12 @@ (def (kotlin-files spec) (filter kotlin-file-entry? (entries spec)))