~subsetpark/erasmus

9ae94bd02440b21e216b81d82cea2d99c57208b7 — Zach Smith 2 months ago a0aba0b
Update pantagruel
1 files changed, 31 insertions(+), 27 deletions(-)

M priv/zk.pant
M priv/zk.pant => priv/zk.pant +31 -27
@@ 16,29 16,16 @@ Note = [Line].
index notes: [Note].
---

// Indexing does two things:
// Indexing updates each note, in place. All backlinks to each note are placed
// at the beginning of it, and all references contained within it are deduped
// and placed at the end.

// 1. It updates each note, in place. All backlinks to each note are placed at
// the beginning of it, and all references contained within it are placed at
// the end.

all n<: notes =>
        n' = backlinks n + body n + references n
all (n, n') <: notes =>
        n' = backlinks n + body n + uniq (references n)
        and name n' = name n.

// 2. It maintains an Index. Indices aren't notes - they aren't affected by
// indexing, in particular. They are simply a list of links to each note in the
// set, ordered by creation time.

some1 i: Index =>
        all n<: notes' => ref_note n in i
        and all (n, m)<: notes' =>
                created_at n < created_at m -> i (ref_note n) < i (ref_note m).

;

Index = [Line].

// A Reference is a line of text that's read and written by the system. Both
// backlinks and (forward) references are simply collections of References.



@@ 48,10 35,11 @@ references n: Note => [Reference].

name n: Note => String.
body n: Note => [Line].
created_at n: Note => Date.

ref s: String => Reference.
ref_note n: Note => Reference.
is_ref l: Line => Bool.

uniq xs: [Any] => [Any].
---

// To refer to a given name, we simply insert a line with a recognized string


@@ 61,13 49,9 @@ ref_note n: Note => Reference.
// rather than the first part, in the case of names with spaces.

ref s = "%ref:" + escape s + "\n".
is_ref l <-> some s: String => l = "%ref:" + s + "\n".

// It follows then that a reference to a note is simply a reference to its
// filename.

ref_note n = ref (name n).

body n = [all line<: n, ~(line in references m) => line].
body n = [all line<: n, ~(is_ref line) => line].

// As mentioned above, to *index* a note is to take the note body, prepend all
// of the backlinks to that note, and append all the references to other notes


@@ 75,7 59,7 @@ body n = [all line<: n, ~(line in references m) => line].
// to any note that links to this one; a (forward) reference is a reference to
// any note which is linked to by this one.

backlinks n = {all m: Note, bracketed (name n) in m => ref_note m}.
backlinks n = {all m: Note, bracketed (name n) in m => reference_to_name m}.
references n = [all s: String, bracketed s in n => ref s].

// It's worth noting that references can be ordered as they appear in the note


@@ 93,14 77,34 @@ bracketed s: String => String.

escape s: String => String.

reference_to_name n: Note => Reference.
reference_source r: Reference => String.
---

bracketed s = "{" + s + "}".

// A reference to a note is simply a reference to its filename.

reference_to_name n = ref (name n).

reference_source r = bracketed (name (referent r)).

// As a possible elaboration, we can imagine maintaining an index. Indices
// aren't notes - they aren't affected by indexing, in particular. They are
// simply a list of links to each note in the set, ordered by creation time.

some1 i: Index =>
        all n' <: notes' => reference_to_name n in i
        and all (n', m) <: notes' =>
                created_at n < created_at m -> i (reference_to_name n) < i (reference_to_name m).

// However, this isn't necessary because we can always `ls` our files.

;

referent r: Reference => Note.

Index = [Line].
created_at n: Note => Date.
---