Something went wrong. Try again.
Coding agent with a memory of all things
Something went wrong. Try again.
2.8 kB · 59 lines
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960# eukhe: lemmas the proofs of area doc_commit share
import Baseimport ../../bend/doc_commit.bend as Cm
# ---- documents ----
# proof_documents: the lemmas behind the laws of LAWS.bend section documents# (Laws.<law> in PROOF.bend delegates here; the lines and endings laws# delegate to PROOF.bend section doc_lines), one section per model of# bend/doc_*.bend. Each section keeps its own name prefix: pc. (an edit of# many files, the write tool, a move, the temp sweep), pv. (seen lines),# ps. (what grep searched, continuations), pdt. (tags).
# ==== commit ====# proof_doc_commit: the edit, write, move and sweep laws of# LAWS.bend section documents (F1, F9, F2, F5, F10): the reply of an edit names# exactly the files that landed, a conflict lands nothing, a sound edit# lands every file; a write never replaces a version the session did not# see; a move never replaces a file; a sweep removes only the free# temporary files of its target, and all of them.# Logic and numbers# -----------------
def documents.pc.BD(b: Bool, t: Type, f: Type) -> Type: match b: case True{}: t case False{}: f
def documents.pc.absurd(-A: Type, e: {True{} == False{} : Bool}) -> A: %e : documents.pc.BD(_, Unit, A) Unit{}
# Sweep# -----
def pc.put_app(+n: Cm.Temp, a: List<&2, Cm.Temp>, +c: List<&2, Cm.Temp>, b: Bool) -> {Cm.sweep.put(n, List.append(&2, Cm.Temp, a, c), b) == List.append(&2, Cm.Temp, Cm.sweep.put(n, a, b), c) : List<&2, Cm.Temp>}: match b: case True{}: {==} case False{}: {==}
def pc.sweep_app(pre: List<&2, Cm.Temp>, +x: List<&2, Cm.Temp>) -> {List.append(&2, Cm.Temp, Cm.sweep(pre), Cm.sweep(x)) == Cm.sweep(List.append(&2, Cm.Temp, pre, x)) : List<&2, Cm.Temp>}: match pre: case Nil{}: {==} case +n <> +rest: %pc.put_app(n, Cm.sweep(rest), Cm.sweep(x), Cm.removes(n)) : {_ == Cm.sweep.put(n, Cm.sweep(List.append(&2, Cm.Temp, rest, x)), Cm.removes(n)) : List<&2, Cm.Temp>} %pc.sweep_app(rest, x) : {Cm.sweep.put(n, List.append(&2, Cm.Temp, Cm.sweep(rest), Cm.sweep(x)), Cm.removes(n)) == Cm.sweep.put(n, _, Cm.removes(n)) : List<&2, Cm.Temp>} {==}
# an entry the sweep keeps: the sweep of the whole is the sweep of the partsdef pc.kept(+pre: List<&2, Cm.Temp>, +n: Cm.Temp, +post: List<&2, Cm.Temp>, no: {False{} == Cm.removes(n) : Bool}) -> {Cm.sweep(List.append(&2, Cm.Temp, pre, n <> post)) == List.append(&2, Cm.Temp, Cm.sweep(pre), Cm.sweep(post)) : List<&2, Cm.Temp>}: %pc.sweep_app(pre, n <> post) : {_ == List.append(&2, Cm.Temp, Cm.sweep(pre), Cm.sweep(post)) : List<&2, Cm.Temp>} %no : {List.append(&2, Cm.Temp, Cm.sweep(pre), Cm.sweep.put(n, Cm.sweep(post), _)) == List.append(&2, Cm.Temp, Cm.sweep(pre), Cm.sweep(post)) : List<&2, Cm.Temp>} {==}