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.after_compile?/0.
Callback implementation for Spark.Dsl.Transformer.before?/1.
Auto-generates a TypeOK invariant from variable usage.
Functions
Callback implementation for Spark.Dsl.Transformer.after?/1.
Callback implementation for Spark.Dsl.Transformer.after_compile?/0.
Callback implementation for Spark.Dsl.Transformer.before?/1.
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.