Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
2.1 kB · 49 lines
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950# eukhe: the proof of LAW command_enter_without_row## PROOF of LAW command_enter_without_row: with no row, every walk state# answers Enter through key.bare (the root and a walk find no row to# pick), which is key.enter on the line's resolution; key.enter and# cmd_enter_bare agree on each answer, the menu of a bare path because# the model's join of a path is the spec's cmd_render of it (B.cb_join).
import Baseimport ../../bend/command.bend as Cmdimport ../../laws/command/paths.bend as Commandimport ./base.bend as LA
# key.enter is cmd_enter_bare on every resolutiondef kewr_enter(r: Cmd.Res, line: List<&2, Nat>) -> {Cmd.key.enter(r, line) == Command.cmd_enter_bare(r, line) : Cmd.Out}: match r: case Cmd.Runs{q, a}: {==} case Cmd.Opens{+q}: %LA.cb_join(q) : {Cmd.Out{List.append(&2, Nat, Cmd.join(q), [32n]), True{}, False{}} == Cmd.Out{List.append(&2, Nat, _, [32n]), True{}, False{}} : Cmd.Out} {==} case Cmd.Unknown{q, w}: {==} case Cmd.NoCmd{}: {==}
# at any walk state, Enter with no row is key.enter on the resolutiondef kewr_at(s: Cmd.St, +t: List<&2, Cmd.Ent>, +line: List<&2, Nat>, p: List<&2, Nat>) -> {Cmd.key.at(s, t, line, p, Cmd.NoRow{}, Cmd.Enter{}) == Cmd.key.enter(Cmd.resolve(t, line), line) : Cmd.Out}: match s: case Cmd.Top{}: {==} case Cmd.Walk{q, e}: {==} case Cmd.Rest{q, ws}: {==} case Cmd.Lost{q, w}: {==} case Cmd.Stray{}: {==}
# whatever the line cuts intodef kewr_cut(c: List<&2, List<&2, Nat>> & List<&2, Nat>, +t: List<&2, Cmd.Ent>, +line: List<&2, Nat>) -> {Cmd.key.cut(c, t, line, Cmd.NoRow{}, Cmd.Enter{}) == Cmd.key.enter(Cmd.resolve(t, line), line) : Cmd.Out}: match c: case (d, p): kewr_at(Cmd.walk(d, t, Cmd.Top{}), t, line, p)
def Command.command_enter_without_row(t, line): %Equal.sym(Cmd.Out, Cmd.key.cut(Cmd.cut(Cmd.words(line)), t, line, Cmd.NoRow{}, Cmd.Enter{}), Cmd.key.enter(Cmd.resolve(t, line), line), kewr_cut(Cmd.cut(Cmd.words(line)), t, line)) : {_ == Command.cmd_enter_bare(Cmd.resolve(t, line), line) : Cmd.Out} kewr_enter(Cmd.resolve(t, line), line)