TLX.Transformers.TypeOK (TLX v0.5.2)

Copy Markdown

Spark transformer that auto-generates a TypeOK invariant from variable usage when the user hasn't declared one.

Summary

Functions

Callback implementation for Spark.Dsl.Transformer.after?/1.

Callback implementation for Spark.Dsl.Transformer.before?/1.

Auto-generates a TypeOK invariant from variable usage.

Functions

after?(arg1)

Callback implementation for Spark.Dsl.Transformer.after?/1.

after_compile?()

Callback implementation for Spark.Dsl.Transformer.after_compile?/0.

before?(_)

Callback implementation for Spark.Dsl.Transformer.before?/1.

transform(dsl_state)

Auto-generates a TypeOK invariant from variable usage.

Collects all literal values assigned to each variable via next transitions. Variables whose transitions only use literals (atoms, booleans) get a TypeOK invariant: var \in {val1, val2, ...}.

Variables with arithmetic expressions or no literal assignments are skipped. Variables with type_ok: false are excluded.