The argument-swapping front end

A swappable operation (Swap) has two arguments of one sort and a semi-inverse that solves the first; in the flow signature, add. A program that adds a + b where b is to be consumed is not typed as written; swapArgs rewrites it to add(b, a).

The choice is made by forward inference. Every line contributes its forward form, its solved form if it has a semi-inverse, and, for a swappable o(a, b), the swapped solved form b ← (c, a). Starting from the weights and the returned variables, an equation fires when its reads are known and its results unknown, until nothing fires (fwdKnown). The pass swaps exactly the lines whose swapped form fired. The swap preserves the meaning for a model where the swappable operations commute (FrontSem), and if any swap of the program is typed, the one chosen here is (FrontComplete).

class RoleFlow.Swap {S : Type} (Sg : Sig S) : Type

The swappable operations of a signature: two arguments of one sort, and a semi-inverse that solves the first.

• swappable {as bs : List S} : Sg.Op as bs → Bool
• sorts {as bs : List S} (o : Sg.Op as bs) : swappable o = true → ∃ (a : S), as = [a, a]
• k_one {as bs : List S} (o : Sg.Op as bs) : swappable o = true → ∃ (si : SemiInv Sg.Op as bs), Sg.inv o = some si ∧ si.k = 1

def RoleFlow.kOf {S : Type} {Sg : Sig S} (l : Line Sg) : Option ℕ

How many leading arguments the semi-inverse of l solves, if there is one.

Equations

• RoleFlow.kOf l = Option.map (fun (x : RoleFlow.SemiInv Sg.Op l.as l.bs) => x.k) (Sg.inv l.op)

def RoleFlow.solvedEqns {S : Type} {Sg : Sig S} (i n : ℕ) (l : Line Sg) : List Search.Eqn

The solved form of the line l, numbered i, at scope n.

Equations

• RoleFlow.solvedEqns i n l = match RoleFlow.kOf l with | some k => [{ binds := List.take k l.args, reads := l.ys n ++ List.drop k l.args, line := i, swap := false }] | none => []

def RoleFlow.swappedEqns {S : Type} {Sg : Sig S} [Swap Sg] (i n : ℕ) (l : Line Sg) : List Search.Eqn

The swapped solved form: a swappable o(a, b) solved for b.

Equations

• RoleFlow.swappedEqns i n l = match RoleFlow.Swap.swappable l.op, l.args with | true, [a, b] => [{ binds := [b], reads := l.ys n ++ [a], line := i, swap := true }] | x, x_1 => []

def RoleFlow.lineEqns {S : Type} {Sg : Sig S} [Swap Sg] (i n : ℕ) (l : Line Sg) : List Search.Eqn

The equations of the line l: forward, solved, and swapped solved.

Equations

• RoleFlow.lineEqns i n l = { binds := l.ys n, reads := l.args, line := i, swap := false } :: RoleFlow.solvedEqns i n l ++ RoleFlow.swappedEqns i n l

def RoleFlow.eqns {S : Type} {Sg : Sig S} [Swap Sg] : ℕ → ℕ → List (Line Sg) → List Search.Eqn

The equations of the lines at scope n, numbered from i.

Equations

• RoleFlow.eqns x✝¹ x✝ [] = []
• RoleFlow.eqns x✝¹ x✝ (l :: ls) = RoleFlow.lineEqns x✝¹ x✝ l ++ RoleFlow.eqns (x✝¹ + 1) (x✝ + l.bs.length) ls

def RoleFlow.swapIf {S : Type} {Sg : Sig S} [Swap Sg] (s : Bool) (l : Line Sg) : Line Sg

Swap the arguments of l if it is swappable and s holds.

Equations

• RoleFlow.swapIf s l = if (s && RoleFlow.Swap.swappable l.op && l.args.length == 2) = true then { as := l.as, bs := l.bs, op := l.op, args := l.args.reverse } else l

def RoleFlow.swapLines {S : Type} {Sg : Sig S} [Swap Sg] (sw : ℕ → Bool) : ℕ → List (Line Sg) → List (Line Sg)

Swap the lines whose number (from i) satisfies sw.

Equations

• RoleFlow.swapLines sw x✝ [] = []
• RoleFlow.swapLines sw x✝ (l :: ls) = RoleFlow.swapIf (sw x✝) l :: RoleFlow.swapLines sw (x✝ + 1) ls

def RoleFlow.swapSet {S : Type} {Sg : Sig S} [Swap Sg] (P : Prog Sg) : Std.HashSet ℕ

The lines whose swapped form fired.

Equations

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

def RoleFlow.swapArgs {S : Type} {Sg : Sig S} [Swap Sg] (P : Prog Sg) : Prog Sg

The front end: swap the arguments of the lines whose swapped solved form fired.

Equations

• RoleFlow.swapArgs P = { wts := P.wts, ins := P.ins, outs := P.outs, lines := RoleFlow.swapLines (RoleFlow.swapSet P).contains 0 P.lines, ret := P.ret }