Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
9.8 kB · 390 lines
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391# doc_commit: the models of how the documents tools put files on disk# (crates/eukhe-docs/src/write.rs, hashline/mod.rs, documents.rs).## Edit: an edit of many files first locks every path and checks every# file (phase 1): when one file changed since it was staged, the edit# writes nothing. Then it publishes the files in order and stops at the# first publish that fails (phase 2). A publish lands; or lands with a# warning (the rename is done but the directory sync fails, or a move put# its destination in place but could not remove its source); or fails# (nothing of that file lands). The reply calls a file applied only when# it landed.## Write: the write tool replaces a file only when the bytes on disk are a# version the session saw (it read them, grep showed them, or it wrote# them); a missing file is created. The session keeps the last 8 versions# it saw.## Move: an MV never replaces a file: when its destination exists it is# refused and nothing changes.## Sweep: a replace of a file removes the temporary files of that file# that no live writer holds; it keeps every other entry.## The bridge (bridge/bridge_doc_commit.bend,# crates/eukhe-docs/src/write/bridge.rs) runs the real code on generated# scenarios and compares.
import Base
# Edit# ----
type Op is Data: Update{} # the file gets new content Moving{} # the file moves to a free name
type Fault is Data: Clean{} # no fault Sync{} # the rename is done; the directory sync fails Publish{} # the publish fails: nothing of the file lands Remove{} # a move: the destination lands; the source removal fails
# one file of an edit: changed says that its bytes changed since the edit# staged ittype Doc is Data: Doc{op: Op, changed: Bool, fault: Fault}
# what one publish didtype Out is Data: Landed{warn: Bool} Failed{}
def publish.go(x: Fault, k: Op) -> Out: match x: case Clean{}: Landed{False{}} case Sync{}: Landed{True{}} case Publish{}: Failed{} case Remove{}: match k: case Update{}: Landed{False{}} case Moving{}: Landed{True{}}
def publish(f: Doc) -> Out: match f: case Doc{k, c, x}: publish.go(x, k)
def Fault.fails(x: Fault) -> Bool: match x: case Clean{}: False{} case Sync{}: False{} case Publish{}: True{} case Remove{}: False{}
# phase 1: whether a file changed since the edit staged itdef conflict(fs: List<&2, Doc>) -> Bool: match fs: case Nil{}: False{} case f <> rest: match f: case Doc{k, c, x}: Bool.or(c, conflict(rest))
# whether a publish failsdef failing(fs: List<&2, Doc>) -> Bool: match fs: case Nil{}: False{} case f <> rest: match f: case Doc{k, c, x}: Bool.or(Fault.fails(x), failing(rest))
def landed.put(+n: Nat, rest: List<&2, Nat>, o: Out) -> List<&2, Nat>: match o: case Landed{w}: n <> rest case Failed{}: Nil{}
# the disk: the files (by index, from n) whose new content lands, in orderdef landed.go(fs: List<&2, Doc>, +n: Nat) -> List<&2, Nat>: match fs: case Nil{}: Nil{} case f <> rest: landed.put(n, landed.go(rest, 1n+n), publish(f))
def landed.pick(c: Bool, fs: List<&2, Doc>) -> List<&2, Nat>: match c: case True{}: Nil{} case False{}: landed.go(fs, 0n)
# the files whose new content is on disk after the editdef landed(+fs: List<&2, Doc>) -> List<&2, Nat>: landed.pick(conflict(fs), fs)
def run.put(o: Out, rest: List<&2, Out>) -> List<&2, Out>: match o: case Landed{w}: Landed{w} <> rest case Failed{}: [Failed{}]
# phase 2: the publishes, in order, up to the first that failsdef run(fs: List<&2, Doc>) -> List<&2, Out>: match fs: case Nil{}: Nil{} case f <> rest: run.put(publish(f), run(rest))
# what the reply says of one filetype Report is Data: Applied{warn: Bool} NotWritten{}
def report.put(o: Out, rest: List<&2, Report>) -> List<&2, Report>: match o: case Landed{w}: Applied{w} <> rest case Failed{}: NotWritten{} <> rest
# one report a file, from the publishes: a file with no publish was not# writtendef report(fs: List<&2, Doc>, os: List<&2, Out>) -> List<&2, Report>: match fs: case Nil{}: Nil{} case f <> rest: match os: case Nil{}: NotWritten{} <> report(rest, Nil{}) case o <> more: report.put(o, report(rest, more))
type Reply is Data: Rejected{} # an error: nothing was written Answered{files: List<&2, Report>} # applied, or applied in part
def reply.go(os: List<&2, Out>, fs: List<&2, Doc>) -> Reply: match os: case Nil{}: Answered{report(fs, Nil{})} case o <> more: match o: case Landed{w}: Answered{report(fs, Landed{w} <> more)} case Failed{}: Rejected{}
def reply.pick(c: Bool, +fs: List<&2, Doc>) -> Reply: match c: case True{}: Rejected{} case False{}: reply.go(run(fs), fs)
# the reply of the editdef reply(+fs: List<&2, Doc>) -> Reply: reply.pick(conflict(fs), fs)
def applied(rs: List<&2, Report>, +n: Nat) -> List<&2, Nat>: match rs: case Nil{}: Nil{} case r <> rest: match r: case Applied{w}: n <> applied(rest, 1n+n) case NotWritten{}: applied(rest, 1n+n)
# the files (by index) the reply reports applieddef reported(r: Reply) -> List<&2, Nat>: match r: case Rejected{}: Nil{} case Answered{rs}: applied(rs, 0n)
# the indices of the files, from ndef ids(fs: List<&2, Doc>, +n: Nat) -> List<&2, Nat>: match fs: case Nil{}: Nil{} case f <> rest: n <> ids(rest, 1n+n)
# Write# -----
def mem(+v: Nat, xs: List<&2, Nat>) -> Bool: match xs: case Nil{}: False{} case x <> rest: Bool.or(Nat.is_eq(x, v), mem(v, rest))
def drop.put(+x: Nat, rest: List<&2, Nat>, b: Bool) -> List<&2, Nat>: match b: case True{}: rest case False{}: x <> rest
def drop(+v: Nat, xs: List<&2, Nat>) -> List<&2, Nat>: match xs: case Nil{}: Nil{} case +x <> rest: drop.put(x, drop(v, rest), Nat.is_eq(x, v))
# the versions seen after the session sees v: newest first, once each,# the last 8def saw(+v: Nat, s: List<&2, Nat>) -> List<&2, Nat>: List.take(&2, Nat, v <> drop(v, s), 8n)
# whether the disk holds a version the session did not seedef unseen(d: Maybe<&2, Nat>, +s: List<&2, Nat>) -> Bool: match d: case None{}: False{} case Some{v}: Bool.not(mem(v, s))
# what a write did: whether it wrote, the disk and the seen versions aftertype Wt is Data: Wt{ok: Bool, disk: Maybe<&2, Nat>, seen: List<&2, Nat>}
def write.go(b: Bool, d: Maybe<&2, Nat>, +s: List<&2, Nat>, +c: Nat) -> Wt: match b: case True{}: Wt{False{}, d, s} case False{}: Wt{True{}, Some{c}, saw(c, s)}
# the session writes c over the disk d, having seen the versions sdef write(+d: Maybe<&2, Nat>, +s: List<&2, Nat>, +c: Nat) -> Wt: write.go(unseen(d, s), d, s, c)
# Move# ----
# a file: its name and its contenttype Entry is Data: Entry{name: Nat, body: Nat}
def has(+n: Nat, es: List<&2, Entry>) -> Bool: match es: case Nil{}: False{} case e <> rest: match e: case Entry{m, g}: Bool.or(Nat.is_eq(m, n), has(n, rest))
def get.put(b: Bool, g: Nat, rest: Maybe<&2, Nat>) -> Maybe<&2, Nat>: match b: case True{}: Some{g} case False{}: rest
# the content of the file named ndef get(+n: Nat, es: List<&2, Entry>) -> Maybe<&2, Nat>: match es: case Nil{}: None{} case e <> rest: match e: case Entry{m, g}: get.put(Nat.is_eq(m, n), g, get(n, rest))
def rename.put(+t: Nat, +m: Nat, g: Nat, rest: List<&2, Entry>, b: Bool) -> List<&2, Entry>: match b: case True{}: Entry{t, g} <> rest case False{}: Entry{m, g} <> rest
# the files after the file s takes the name tdef rename(+s: Nat, +t: Nat, es: List<&2, Entry>) -> List<&2, Entry>: match es: case Nil{}: Nil{} case e <> rest: match e: case Entry{+m, g}: rename.put(t, m, g, rename(s, t, rest), Nat.is_eq(m, s))
# what a move did: whether it moved, and the files after ittype Mv is Data: Mv{ok: Bool, es: List<&2, Entry>}
def Mv.ok(m: Mv) -> Bool: match m: case Mv{ok, es}: ok
def Mv.es(m: Mv) -> List<&2, Entry>: match m: case Mv{ok, es}: es
def move.go(+s: Nat, +t: Nat, taken: Bool, es: List<&2, Entry>) -> Mv: match taken: case True{}: Mv{False{}, es} case False{}: Mv{True{}, rename(s, t, es)}
# MV s t over the files esdef move(+s: Nat, +t: Nat, +es: List<&2, Entry>) -> Mv: move.go(s, t, has(t, es), es)
# Sweep# -----
type Sort is Data: Own{} # a temporary file of the target Foreign{} # a temporary file of another target Plain{} # another file
def Sort.own(k: Sort) -> Bool: match k: case Own{}: True{} case Foreign{}: False{} case Plain{}: False{}
# an entry of the target's directory; held: a live writer holds its locktype Temp is Data: Temp{id: Nat, sort: Sort, held: Bool}
# whether the sweep removes the entrydef removes(n: Temp) -> Bool: match n: case Temp{i, k, h}: Bool.and(Sort.own(k), Bool.not(h))
def sweep.put(+n: Temp, rest: List<&2, Temp>, b: Bool) -> List<&2, Temp>: match b: case True{}: n <> rest case False{}: rest
# the entries the sweep removes, in orderdef sweep(ns: List<&2, Temp>) -> List<&2, Temp>: match ns: case Nil{}: Nil{} case +n <> rest: sweep.put(n, sweep(rest), removes(n))