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.

• groupDatatypesByScc — groups mutually recursive datatypes into SCC groups 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.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.

inductive Strata.Laurel.OrderedDecl : Type

A single declaration in an ordered Laurel program. Declarations are in dependency order (dependencies before dependents).

• procs (procs : List Procedure) (isRecursive : Bool) : OrderedDecl

  A group of functions (single non-recursive, or mutually recursive).

• datatypes (dts : List DatatypeDefinition) : OrderedDecl

  A group of (possibly mutually recursive) datatypes.

• constant (c : Constant) : OrderedDecl

  A named constant.

structure Strata.Laurel.OrderedLaurel : Type

A Laurel program whose declarations have been grouped and topologically ordered. Produced by orderProgram from a Program.

• decls : List OrderedDecl

def Strata.Laurel.groupDatatypesByScc (program : Program) : List (List DatatypeDefinition)

Group mutually recursive datatypes into SCC groups using Tarjan's SCC algorithm. Returns groups in topological order (dependencies before dependents).

Equations

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

def Strata.Laurel.groupProcsByScc (program : Program) : List OrderedDecl

Group procedures into SCC groups and wrap them as OrderedDecl.procs.

Equations

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

def Strata.Laurel.orderProgram (program : Program) : OrderedLaurel

Produce an OrderedLaurel from a Program by grouping and ordering procedures via SCC, collecting datatypes, and constants.

Equations

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