Language-Neutral Type Shape Analysis

Shared front end for the Ion serializer generators (getIonSerializer% for Java in Strata.Java.Gen, getIonGoSerializer% for Go in Strata.Go.Gen).

Every such generator needs the same answer to the same question: what shape does this Lean type have, and what is in each of its fields? That answer depends only on the Lean environment, not on the target language, so it lives here and each backend consumes it. Only the naming, type mapping and code emission are language-specific and stay in the backends.

What a shape is

analyzeType reduces a Lean declaration to one of three TypeShapes, matching the three Ion encodings the deserializer understands:

TypeShape	Lean declaration	Ion encoding
.struct	a structure	Ion struct, keys = field names
.singleCtor	an inductive with one constructor	Ion struct, keys _0, _1, …
.multiCtor	an inductive with zero or 2+ constructors	Ion sexp (ctorName arg …)

Deliberately, a TypeShape carries no target-language name: the Lean Name is the only identity it records, and each backend derives its own identifier from it (Strata.Java.javaClassName, Strata.Go.goTypeName). A single shared name would have to pick one language's escaping rules, and the two disagree — Java reserves String and record, Go reserves string and range.

Supported field types

Leaves are Nat, Int, Float, String, Bool and StrataDDM.Decimal; containers are List α and Option α, nestable to any depth; anything else that is a structure or an inductive is a .compound reference that pulls that type into the generated closure (see collectNestedTypes).

Name utilities

def Strata.CodeGen.toPascalCase (s : String) : String

Convert a Lean identifier to PascalCase: split on _, drop empty segments, upcase the first character of each remaining segment, and concatenate.

Used for both type and member names, so my_ctor and myCtor both land on MyCtor — see disambiguate for why that is safe.

Equations

• One or more equations did not get rendered due to their size.

def Strata.CodeGen.disambiguate (base : String) (usedNames : Std.HashSet String) : String × Std.HashSet String

Return a variant of base that is not already in usedNames, adding a _ (then _2, _3, …) suffix on collision, along with the extended set.

Escaping is not injective: a backend's escape function strips characters the target language does not allow in identifiers and toPascalCase upcases segment heads, so distinct Lean names can fold to one target identifier (foo and Foo both become Foo; so do myCtor and my_ctor). Emitting the folded name twice would declare the same type or the same field twice, which does not compile.

Comparison is case-insensitive because members that differ only in case are still confusable, and because each generated type becomes a file on a possibly case-insensitive filesystem.

Equations

• Strata.CodeGen.disambiguate base usedNames = (Strata.CodeGen.disambiguate.findUnused✝ base usedNames 0, usedNames.insert (Strata.CodeGen.disambiguate.findUnused✝ base usedNames 0).toLower)

def Strata.CodeGen.disambiguateAll (names : List String) : List String

Disambiguate a whole list of names left to right, so earlier names keep their unsuffixed form and only later collisions are renamed.

Equations

• One or more equations did not get rendered due to their size.

Leaf and compound type detection

def Strata.CodeGen.isLeafTypeName (name : Lean.Name) : Bool

The Lean types that serialize directly to an Ion scalar. Everything else is either a container (List/Option) or a .compound reference.

Equations

• Strata.CodeGen.isLeafTypeName name = (name == `Nat || name == `Int || name == `String || name == `Bool || name == `Float || name == `StrataDDM.Decimal)

Shape description

inductive Strata.CodeGen.FieldTypeInfo : Type

What a single field's Lean type maps to, stripped of everything a code generator does not need to know.

• leaf (name : Lean.Name) : FieldTypeInfo

  One of the scalar leaf types (see isLeafTypeName). An unrecognised type also lands here, with a name the backends map to their "unknown" type.

• compound (name : Lean.Name) (typeArgs : Array FieldTypeInfo) : FieldTypeInfo

  A reference to another structure or inductive, with its type arguments.

• typeParam (paramName : String) : FieldTypeInfo

  A type parameter of the enclosing type; generates a target-language generic.

• list (elem : FieldTypeInfo) : FieldTypeInfo

  List α.

• option (elem : FieldTypeInfo) : FieldTypeInfo

  Option α; none serializes to an Ion null.

structure Strata.CodeGen.FieldShape : Type

One field of a structure, or one argument of a constructor. name is the Lean name and stays the Ion key; the backend derives its own identifier.

• name : String
• typeInfo : FieldTypeInfo

  The field's analyzed type.

structure Strata.CodeGen.CtorShape : Type

One constructor of an inductive.

• name : Lean.Name

  The fully qualified constructor name.

• shortName : String

  The last component of name, which is the Ion sexp tag for .multiCtor.

• fields : Array FieldShape

  The constructor's arguments, in declaration order.

inductive Strata.CodeGen.TypeShape : Type

The analyzed shape of a Lean type: which of the three Ion encodings it uses and what it contains. Carries no target-language name by design — see the module docstring.

• struct (name : Lean.Name) (fields : Array FieldShape) (typeParams : Array String := #[]) : TypeShape

  A structure: Ion struct keyed by field name.

• singleCtor (name : Lean.Name) (ctor : CtorShape) (typeParams : Array String := #[]) : TypeShape

  An inductive with exactly one constructor: Ion struct keyed _0, _1, ….

• multiCtor (name : Lean.Name) (ctors : Array CtorShape) (typeParams : Array String := #[]) : TypeShape

  An inductive with zero or 2+ constructors: Ion sexp tagged by ctor name.

def Strata.CodeGen.isCompoundType (env : Lean.Environment) (name : Lean.Name) : Bool

Whether name names a type the generator should emit a declaration for, as opposed to a leaf it maps to a built-in.

Equations

• One or more equations did not get rendered due to their size.

Type parameter tagging

Lean constructor types are forallE telescopes whose leading binders are the type's parameters. To see which fields mention which parameter, the parameters have to be instantiated with something recognisable before the field types are inspected. extractCtorFields substitutes a Sort whose universe is a Level parameter tagged with typeParamPlaceholderPrefix, and extractTypeParamName recovers the parameter name from it.

This is a marker, not a real universe parameter: nothing ever elaborates these levels, they only survive long enough for classifyFieldType to read them back.

Analysis

def Strata.CodeGen.analyzeType (env : Lean.Environment) (typeName : Lean.Name) : Lean.MetaM TypeShape

Reduce a Lean type declaration to its TypeShape. Throws if typeName is neither a structure nor an inductive.

Equations

• One or more equations did not get rendered due to their size.

def Strata.CodeGen.collectNestedTypes (env : Lean.Environment) (rootName : Lean.Name) : Lean.MetaM (Array Lean.Name)

Breadth-first closure of the compound types reachable from rootName, starting with rootName itself. This is the set of types a generator must emit.

Equations

• One or more equations did not get rendered due to their size.