Map Lean's Option to Java's Optional in getIonSerializer%

[keyboardDrummer-bot]

Summary

Fixes the getIonSerializer% Java code generator to map Lean's Option α to java.util.Optional<T> instead of nullable T.

Problem

The IfThenElse record was generated as:

public record IfThenElse(
  AstNode<StmtExpr> cond, 
  AstNode<StmtExpr> thenBranch, 
  AstNode<StmtExpr> elseBranch)

The elseBranch field should be Optional<AstNode<StmtExpr>> since the Lean type has Option (AstNode StmtExpr) for that field.

Root Cause

In javaTypeForInfo, the .option elem case was mapped to just javaBoxedTypeForInfo elem (the inner type), which completely drops the optionality from the Java type signature. The serializer correctly handled null checks, but the type system provided no safety.

Fix

• Type mapping: .option elem now maps to java.util.Optional<{boxedType}> instead of just the raw inner type
• Serialization: Uses .isPresent() / .get() instead of null checks
• Ion wire format: Unchanged — still serializes None as Ion null

After

public record IfThenElse(
  AstNode<StmtExpr> cond,
  AstNode<StmtExpr> thenBranch,
  java.util.Optional<AstNode<StmtExpr>> elseBranch)

Testing

• lake build Strata.DDM.Integration.Java.Gen ✓
• lake build StrataTest ✓ (583 jobs)

Addresses strata-org/jverify#405 comment."
true