Module reorder_decls

Compute an ordering on declarations that:

• Detects mutually-recursive groups;
• Always orders an item before any of its uses (except for recursive cases);
• Otherwise keeps a stable order.

Aeneas needs this because proof assistant languages are sensitive to declaration order and need to be explicit about mutual recursion. This should come useful for translation to any other language with these properties.

Structs

Deps

Transform

Functions

compute_declarations_graph 🔒

compute_reordered_decls 🔒

group_declarations_from_scc 🔒