snap Releases (4): 1.4.0.0 0x8e26a6f8c31689519e618374376ee3dd indexed https://jend.leeeet.dev/files.txt?path=snap@1.4.0.0 1.3.0.0 0xead4c7939c9eaca8d47da53b4496b731 unindexed https://jend.leeeet.dev/files.txt?path=snap@1.3.0.0 1.2.0.0 0xa3b6f2e4e2b12fe8d8466a9a7bb176a3 unindexed https://jend.leeeet.dev/files.txt?path=snap@1.2.0.0 1.1.0.0 0xabe575924687afad4cee1a2c1194d639 unindexed https://jend.leeeet.dev/files.txt?path=snap@1.1.0.0 Definitions (50): Snap.run (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=run) # a program run with its arguments: the exit status on its own first line, # then stdout and stderr together. A refused argv answers 127 and runs nothing. def run(argv: List<&2, String>) -> IO(String): # noqa: L001 IO entry point Snap.exec (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=exec) # a program run with its arguments; the same as `run` def exec(argv: List<&2, String>) -> IO(String): # noqa: L001 IO entry point Snap.start (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=start) # a program started with its arguments and left running; the answer is its # pid, or 0 when it could not be started or its argv was refused def start(argv: List<&2, String>) -> IO(String): # noqa: L001 IO entry point Snap.par (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=par) # several programs run at once, each answered exactly as `run` answers one, in # the order the jobs were given; a job `run` would refuse answers 127 in its # place. `at` is a directory the caller owns and this fills: job n writes to # `at/n`. A width of "" leaves the count to the effect, which reads the cores # and divides them by `gb`, the memory cap each job runs under. `by` is the # second every job must be finished by, or "0" for none. def par( # noqa: L001 IO entry point js: List<&2, List<&2, String>>, +width: String, +gb: String, +at: String, … Snap.code (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=code) # the exit status an answer holds: everything before its first newline def code(out: String) -> String: # noqa: L001 src/answer.bend's law holds it (SNAP-TRUST-5) Snap.text (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=text) # what the program printed, stdout and stderr together: everything after the # answer's first newline def text(out: String) -> String: # noqa: L001 src/answer.bend's law holds it (SNAP-TRUST-5) Snap.ok (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=ok) # whether an answer's status is 0 def ok(+out: String) -> Bool: # noqa: L001 src/answer.bend's law holds it (SNAP-TRUST-5) Snap.cmd (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=cmd) # the arguments joined on newlines, the wire ez's `pass` effect reads def cmd(argv: List<&2, String>) -> String: # noqa: L001 src/argv.bend's law holds it (SNAP-TRUST-5) Snap.line (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/main.bend&name=line) # the arguments joined on newlines; the same as `cmd` def line(argv: List<&2, String>) -> String: # noqa: L001 src/argv.bend's law holds it (SNAP-TRUST-5) Answer.code.at (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/answer.bend&name=code.at) # one char of the status: a newline ends it, and any other char is part of it, # with the rest of the status read only then def code.at(nl: Bool, +ch: Char, rest: Unit -> String) -> String: Answer.code (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/answer.bend&name=code) # the exit status a run answered with: the answer up to its first newline. # It reads no further, so a long body costs nothing. def code(out: String) -> String: Answer.text.at (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/answer.bend&name=text.at) # one char before the body: a newline starts the body, which is the rest as # it stands, and any other char is still the status def text.at(nl: Bool, +tail: String, rest: Unit -> String) -> String: Answer.text (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/answer.bend&name=text) # what the program printed, stdout and stderr together: the answer after its # first newline, or nothing when it has none. The body is returned as it # stands, never walked. def text(out: String) -> String: Answer.ok (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/answer.bend&name=ok) # a run that finished with status 0 def ok(+out: String) -> Bool: Argv.cmd (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=cmd) # the arguments joined on newlines, which is the wire ez's `pass` effect # reads. snap's own effects are handed `wire` and `par.plan`, since an # argument may hold a newline. def cmd(argv: List<&2, String>) -> String: Argv.line (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=line) # the arguments joined on newlines; the same as `cmd` def line(argv: List<&2, String>) -> String: Argv.free_of (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=free_of) # whether a string holds no copy of a char def free_of(text: String, +sep: Char) -> Bool: Argv.free_of.all (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=free_of.all) # whether no string of a list holds a copy of a char def free_of.all(ps: List<&2, String>, +sep: Char) -> Bool: Argv.accepts (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=accepts) # whether an argv can reach its program whole: it names a program, and no # argument holds NUL, which separates them on the wire and which no program # could be handed inside an argument anyway def accepts(argv: List<&2, String>) -> Bool: Argv.wire (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=wire) # the arguments as the effects want them: joined on NUL, the one char no # argument can hold, so each is split back out whole def wire(argv: List<&2, String>) -> String: Argv.Step (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=Step) # what a call does with its argv: refuse it, or hand the effect this wire type Step is Data: Refused{} Run{wire: String} Argv.run.plan.of (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=run.plan.of) # an argv accepted is run; any other is refused def run.plan.of(ok: Bool, argv: List<&2, String>) -> Step: Argv.run.plan (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=run.plan) # what `run`, `exec` and `start` do with an argv. It decides everything: the # effect is called only with the wire of an argv this accepts. def run.plan(+argv: List<&2, String>) -> Step: Argv.run.with (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=run.with) # a step performed by an effect that waits: a refused argv answers as a # program that could not be started, and the effect is never called def run.with(eff: String -> IO(String), step: Step) -> IO(String): Argv.start.with (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/argv.bend&name=start.with) # a step performed by an effect that does not wait: a refused argv answers # as a program that could not be started, and the effect is never called def start.with(eff: String -> IO(String), step: Step) -> IO(String): Effect.snaprun.exec (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/effect.bend&name=snaprun.exec) # the program and its arguments, NUL separated (`wire`), run with no shell # between. The answer is the exit status on its own first line, then stdout # and stderr. def snaprun.exec(cmd: String) -> IO(String): Effect.snaprun.start (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/effect.bend&name=snaprun.start) # a program started and left running, answering with its pid, or 0 when it # could not be started. The arguments arrive as `wire` makes them. The effect above # waits for what it runs and reads it to the end; this one waits for nothing, # and gives the child a session and a /dev/null of its own so it holds no pipe # open behind it. def snaprun.start(cmd: String) -> IO(String): Effect.snaprun.par (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/effect.bend&name=snaprun.par) # several programs run at once, answering with every exit status in the order # the jobs were given. The fields arrive as `par.plan` joins them. The children # write into a directory rather than down a pipe, and `par` below reads those # files back, so this answers statuses alone. def snaprun.par(cmd: String) -> IO(String): File.file.slurp.end (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.slurp.end) # the handle closed, and whatever was gathered def file.slurp.end(file: File, acc: String) -> IO(String): File.file.slurp.cut (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.slurp.cut) # an empty chunk means the end of the file def file.slurp.cut(chunk: String, file: File, acc: String, rest: File -> String -> IO(String)) -> IO(String): File.file.slurp.more (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.slurp.more) # a failed read ends the file as surely as an empty one def file.slurp.more( res: Result<&1, &1, U32 & String, String>, file: File, acc: String, rest: File -> String -> IO(String) ) -> IO(String): File.file.slurp.next (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.slurp.next) # the handle comes back paired with what it read def file.slurp.next( got: File & Result<&1, &1, U32 & String, String>, acc: String, rest: File -> String -> IO(String) ) -> IO(String): File.file.slurp (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.slurp) # the whole file, read in chunks until one is empty, or the fuel is def file.slurp(fuel: Nat, file: File, acc: String) -> IO(String): File.file.unsized (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.unsized) # the reads a file with no size to go by may take: a pipe, a device or a # /proc file reports 0 bytes and a file past 4 GiB fails to report, so these # are read until they end, up to 100000 reads of 64 KiB def file.unsized() -> Nat: File.file.reads.given (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.reads.given) # a size of 0 is no size to go by; any other is read to def file.reads.given(none: Bool, bytes: U32) -> Nat: File.file.reads (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.reads) # the reads a file of this many bytes takes: one for every 64 KiB, one for # the part past the last whole 64 KiB, and one to spare for a short read def file.reads(+bytes: U32) -> Nat: File.file.reads.of (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.reads.of) # the reads the size the host reported allows def file.reads.of(res: Result<&1, &1, U32 & String, U32>) -> Nat: File.file.read.sized (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.read.sized) # a file read whole, with fuel enough for the size it reported def file.read.sized(got: File & Result<&1, &1, U32 & String, U32>) -> IO(String): File.file.read.opened (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.read.opened) # what an opened file holds, or nothing when it would not open def file.read.opened(res: Result<&1, &1, U32 & String, File>) -> IO(Maybe<&2, String>): File.file.read (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.read) # a file's text, or None when it cannot be opened def file.read(path: String) -> IO(Maybe<&2, String>): File.file.text_of (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/file.bend&name=file.text_of) # a file's text, or "" when there is none def file.text_of(got: Maybe<&2, String>) -> String: Par.job.fields (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=job.fields) # one job's fields on the `par` wire: each argument marked with a `+` in # front, then an empty field that ends the job. A marked field is never empty, # so the empty one cannot be mistaken for an argument, whatever the arguments # hold; and the empty job is the empty field alone. def job.fields(argv: List<&2, String>) -> List<&2, String>: Par.par.job.of (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.job.of) # a job accepted as `run` would accept it is sent as it is; any other is sent # as the empty job, which the effect answers as a program that could not be # started, in its own place def par.job.of(ok: Bool, argv: List<&2, String>) -> List<&2, String>: Par.par.job (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.job) # the job `par` sends for an argv def par.job(+argv: List<&2, String>) -> List<&2, String>: Par.par.fields (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.fields) # every job's fields, in the order the jobs were given def par.fields(js: List<&2, List<&2, String>>) -> List<&2, String>: Par.par.plan (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.plan) # what the `par` effect is handed: how many may run at once, how many gigabytes # each was given, where they write, the second they must all be finished by, # and then every job's fields, all joined on NUL def par.plan(js: List<&2, List<&2, String>>, width: String, gb: String, at: String, by: String) -> String: Par.par.nonblank (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.nonblank) # the strings that are not empty, which is what a list of statuses amounts to # once a trailing newline has been counted as a line def par.nonblank(ss: List<&2, String>) -> List<&2, String>: Par.par.of (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.of) # one job's answer, in the shape `run` gives: the status on its own first # line, then everything the program printed, read back out of the file it was # pointed at def par.of(+code: String, got: Maybe<&2, String>) -> String: Par.par.answers (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.answers) # every job's answer: each status paired with the body at its place in the # order, or with none when there is no body there def par.answers(cs: List<&2, String>, bodies: List<&2, Maybe<&2, String>>) -> List<&2, String>: Par.par.bodies (https://jend.leeeet.dev/definition.txt?path=snap@1.4.0.0/src/par.bend&name=par.bodies) # the file each job wrote, one per status, by its place in the order def par.bodies(cs: List<&2, String>, +at: String, +nn: Nat) -> IO(List<&2, Maybe<&2, String>>):