Grouping and Ordering for Core Translation

Utilities for computing the grouping and topological ordering of Laurel declarations before they are emitted as Strata Core declarations.

• groupDatatypes — groups mutually recursive datatypes into a single .data declaration using Tarjan's SCC algorithm.
• computeSccDecls — builds the procedure call graph, runs Tarjan's SCC algorithm, and returns each SCC as a list of procedures paired with a flag indicating whether the SCC is recursive. The result is in reverse topological order (dependencies before dependents), which is the order required by Core.

def Strata.Laurel.groupDatatypes (dts : List DatatypeDefinition) (ldts : List (Lambda.LDatatype Unit)) : List (List (Lambda.LDatatype Unit))

Group LDatatype Unit values by strongly connected components of their direct type references. Datatypes in the same SCC (mutually recursive) share a single .data declaration. Non-recursive datatypes each get their own singleton .data declaration. The returned groups are in topological order: leaves (no dependencies) first, roots last.

Equations

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

def Strata.Laurel.computeSccDecls (program : Program) : List (List Procedure × Bool)

Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC as a list of procedures paired with a flag indicating whether the SCC is recursive. Results are in reverse topological order: dependencies before dependents.

Procedures with an invokeOn trigger are placed as early as possible — before unrelated procedures without one — by stably partitioning them first before building the graph. Tarjan then naturally assigns them lower indices, causing them to appear earlier in the output.

External procedures are excluded.

Equations

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