Template FUNCTION_BLOCKs — Concept¶

The right question is not "how do I avoid writing Vec3, Vec4, Vec5?" It is "what does the compiler need to stay confident that every concrete instance is safe?" Templates answer that question: they push parameterization into the type itself, so the compiler monomorphizes once and verifies each instance independently — without any runtime generics and without any sacrifice to the Bounded-Cycle Theorem.

The problem: monomorphism without templates¶

LoLa arrays have static, compile-time sizes. That constraint is non-negotiable: it is what lets the SMT encoder stay quantifier-free, what lets the code generator know WCET, and what makes the Bounded-Cycle Theorem hold.

Without templates you would write a separate file for every array size you needed:

(* Vec3.lola *)
FUNCTION_BLOCK Vec3 …   (* ARRAY[0..2] OF LREAL, SUM(k IN 0..2 : …) *)
(* Vec4.lola *)
FUNCTION_BLOCK Vec4 …   (* ARRAY[0..3] OF LREAL, SUM(k IN 0..3 : …) *)

Every change to the algorithm must be made in every copy. A five-line block becomes dozens of near-identical files. This is the monomorphism trap.

Template parameters solve it without introducing runtime generics. The template Vec<N: UINT> is not a run-time abstraction; it is a compile-time recipe that the compiler expands into an ordinary concrete FB at every use site:

Vec<3>  →  concrete FB with ARRAY[0..2], SUM(k IN 0..2 : …)
Vec<4>  →  concrete FB with ARRAY[0..3], SUM(k IN 0..3 : …)

Both results are as static and verifiable as hand-written blocks.

Monomorphization¶

Monomorphization is the process of substituting concrete UINT values for all type-parameter references in a template block. It happens at the materialize_closure phase, before composition flattening, semantic analysis, and SMT encoding. The compiler:

Detects that a VAR type name carries angle-bracket arguments (Vec<3>).
Loads the template source file (Vec.lola) via the normal file resolver.
Substitutes N = 3 everywhere in the AST: array bounds, aggregate bounds, index expressions.
Names the result Vec<3> and stores it in the closure snapshot.
Compiles and inlines Vec<3> exactly like any ordinary concrete FB.

The template file itself is never independently compiled — only its monomorphized instances are. If Vec.lola is on the search path but never instantiated, no verification of it occurs.

Why only UINT?¶

Array bounds must be non-negative integers. UINT is the natural type: it excludes negative values at the type level (no "ARRAY[0..(-3)]") and maps directly to the kind of structural size that the Bounded-Cycle Theorem reasons about.

Future versions may support other integral kinds (for offsets, strides, etc.), but extending beyond integer-valued parameters would require a more general expression evaluator and is deferred.

Template parameters vs. CONST¶

Both let you write a block whose behaviour depends on a named number. The difference is scope and what the compiler does with them.

	`CONST`	Type template parameter
Scope	One concrete FB, all instances share it	One parameter tuple per concrete type
Verification unit	One FB with fixed constants	Separate proof per concrete type
Visible in generated code?	No (inlined by substitution)	No (inlined by monomorphization)
Allowed in array bounds?	No (only literals in bounds)	Yes
Allowed in aggregate bounds?	No (only literals in bounds)	Yes
Types	Any scalar primitive	`UINT` only
Instantiation site	`VAR inst : MyFB(Kp := 2.0)`	`VAR v : Vec<3>`

Use CONST when the numeric value is an internal constant of the algorithm that every instance of the same FB shares (a physical constant, a fixed gain). Use a type template parameter when the size of the data structure itself varies per use site — array lengths, matrix dimensions, pipeline depths.

Template parameters vs. PARAMETER¶

PARAMETER values are fixed at instantiation time but remain as Z3 free constants in the proof. They let the verifier reason about a family of configurations without committing to a specific value.

Type template parameters are erased entirely before verification: after monomorphization there is no N symbol — only concrete integer literals. The trade-off is that N = 3 and N = 4 are verified separately (complete, per-instance), whereas a PARAMETER proof is generic over all valid configurations at once.

Bounded-Cycle Theorem interaction¶

The Bounded-Cycle Theorem states that every LoLa program has a statically proven finite per-scan execution. Template parameters preserve this:

Array bounds are evaluated to concrete integers before any structural check runs. A Vec<N> with N = 1 000 000 would exceed the element cap just like a hand-written ARRAY[0..999999] — no exemption.
Aggregate bounds SUM(k IN 0..N-1 : …) are unrolled or encoded with the concrete N value. Static finiteness holds.
The monomorphized FB is checked by the same structure_bounds pass as any other FB. Template instantiation cannot bypass any structural limit.

What is not yet implemented¶

Non-UINT template parameter kinds. Parameters of type INT, DINT, or BOOL are not yet supported.