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.

• 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 : UnorderedCoreWithLaurelTypes) : 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 axioms are placed as early as possible — before unrelated procedures without them — by stably partitioning them first before building the graph. Tarjan then naturally assigns them lower indices, causing them to appear earlier in the output.

Equations

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

inductive Strata.Laurel.OrderedDecl : Type

A single declaration in a CoreWithLaurelTypes program. Declarations are in dependency order (dependencies before dependents).

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

  A group of functions (single non-recursive, or mutually recursive). Invariant: funcs.length > 1 → isRecursive = true.

• procedure (procedure : Procedure) : OrderedDecl

  A single (non-functional) procedure.

• datatypes (dts : List DatatypeDefinition) : OrderedDecl

  A group of (possibly mutually recursive) datatypes.

• constant (c : Constant) : OrderedDecl

  A named constant.

structure Strata.Laurel.CoreWithLaurelTypes : Type

A program whose declarations have been grouped and topologically ordered, using Laurel types. Produced by orderFunctionsAndProcedures from a UnorderedCoreWithLaurelTypes.

• decls : List OrderedDecl

def Strata.Laurel.formatOrderedDecl : OrderedDecl → Std.Format

Equations

• Strata.Laurel.formatOrderedDecl (Strata.Laurel.OrderedDecl.funcs funcs isRecursive) = Std.Format.joinSep (List.map Strata.Laurel.formatAsFunction✝ funcs) (Std.Format.text "\n\n")
• Strata.Laurel.formatOrderedDecl (Strata.Laurel.OrderedDecl.procedure proc) = Std.format proc
• Strata.Laurel.formatOrderedDecl (Strata.Laurel.OrderedDecl.datatypes dts) = Std.Format.joinSep (List.map Std.format dts) (Std.Format.text "\n\n")
• Strata.Laurel.formatOrderedDecl (Strata.Laurel.OrderedDecl.constant c) = Std.format c

@[implicit_reducible]

instance Strata.Laurel.instToFormatOrderedDecl : Std.ToFormat OrderedDecl

Equations

• Strata.Laurel.instToFormatOrderedDecl = { format := Strata.Laurel.formatOrderedDecl }

def Strata.Laurel.formatCoreWithLaurelTypes (p : CoreWithLaurelTypes) : Std.Format

Equations

• Strata.Laurel.formatCoreWithLaurelTypes p = Std.Format.joinSep (List.map Strata.Laurel.formatOrderedDecl p.decls) (Std.Format.text "\n\n")

@[implicit_reducible]

instance Strata.Laurel.instToFormatCoreWithLaurelTypes : Std.ToFormat CoreWithLaurelTypes

Equations

• Strata.Laurel.instToFormatCoreWithLaurelTypes = { format := Strata.Laurel.formatCoreWithLaurelTypes }

def Strata.Laurel.orderingPass : LaurelPass UnorderedCoreWithLaurelTypes CoreWithLaurelTypes

Equations

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