-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathstore.ktr
More file actions
256 lines (229 loc) · 15.6 KB
/
Copy pathstore.ktr
File metadata and controls
256 lines (229 loc) · 15.6 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
// The `prelude.store` sub-module: the project's durable key-value store — named values that outlive
// any single run, holding any Katari value (a document, a `data`, a `file`, a secret sealed at rest).
// Writes are last-write-wins. Each operation is a `request`, so a handler in scope may intervene;
// unhandled, the runtime machine-answers it against the project's durable rows at the project root,
// and the answer is durable, so a replay observes the value the first attempt did.
//
// Keys are ambient: an operation names a path-like key and nothing else, and where it lands is the
// environment's decision. A `workspace` is the key prefix and the serial domain in one install (one
// lane per workspace), an `exclusive` is a critical section of the nearest one, and data several
// workspaces share travels as a `shared` request served above them. A workspace descends only; there
// is no `..`.
//
// Storing a `file` joins its bytes to the project's file library, so it outlives the writing run.
// Overwriting or deleting an entry forgets the reference and leaves the file; only an explicit delete
// through the file API removes it, after which a stored reference reads as `gone`.
@"A lookup that found a value."
data found(@"The stored value." value: unknown)
@"A lookup that found nothing — distinct from a stored `null`."
data absent(@"The key that had no entry, as the environment resolved it (workspace prefixes applied)." key: string)
// One lookup's outcome. (Type synonyms take no docs.)
type lookup = found | absent
@"Read the value at @key@, resolved against the surrounding workspace: `found(value)` or
`absent(key)` — a stored `null` is `found(null)`, so presence and value never blur. Pin an expected
shape with `json.validate[T]` on the found value."
request get(@"The path-like key, relative to the current workspace." key: string) -> lookup
@"Read @key@ as a T, resolved against the surrounding workspace, falling back to @fallback@ when the
key is absent or holds a value that is not one — the typed store read. T is read off @fallback@, so it
is normally inferred rather than written.
Degrading is the semantics here: a durable cell whose shape no longer fits was written by an earlier
version of the program, and starting over from a value the reader understands is the recovery. The
bare `get` is the reader that separates a missing entry from a wrong-typed one, or that reports the
mismatch itself. Under a T admitting `null`, a stored `null`, a mismatch and an absent key all answer
`null`."
agent get_or[T](
@"The path-like key, relative to the current workspace." key: string,
@"The value when the key is absent or does not fit T; its type IS T." fallback: T,
) -> T with get {
match (get(key = key)) {
case found(value => stored) -> {
// `catch` folds the `validation_error` into the answer so a mismatch takes the same arm as an
// absent key.
agent checked() -> T with prelude.throw[json.validation_error] {
json.validate[T](value = stored)
}
match (prelude.catch(task = checked)) {
case json.validation_error(message => _) -> fallback
case validated -> validated
}
}
case absent(key => _) -> fallback
}
}
@"Write @value@ at @key@, resolved against the surrounding workspace, creating or replacing the entry
(last write wins). Any value fits: a document, a data value, a `file`, a secret (sealed at rest). A
stored `file` joins the project's file library and outlives the writing run; overwriting the entry
forgets the reference and leaves the file it replaced, which only an explicit delete through the file
API or the Files page removes."
request set(@"The path-like key, relative to the current workspace." key: string, @"The value to store." value: unknown) -> null
@"Delete the entry at @key@, resolved against the surrounding workspace; deleting a missing key is a
no-op. Deleting an entry that held a `file` forgets the reference and leaves the file in the project's
file library; remove it with an explicit delete through the file API or the Files page."
request delete(@"The path-like key, relative to the current workspace." key: string) -> null
@"A `list` entry: a key holding a value, directly under the listed place."
data leaf(@"The key, relative to the listed place." key: string)
@"A `list` entry: a path segment with more entries below it — descend by listing @path@ deeper."
data branch(@"The segment name, relative to the listed place." name: string)
// One listing's element. (Type synonyms take no docs.)
type entry = leaf | branch
@"List what sits directly under @path@ in the current workspace: a `leaf` per value-holding key and a
`branch` per segment with entries below it (sorted; a name that is both leaf and branch yields both).
The default @path@ of \"\" lists the workspace itself — a listing has no key to carry the prefix, so
the path parameter is how one travels."
request list(@"The subdirectory to list, relative to the current workspace; \"\" is the workspace itself." path: string ?= "") -> array[entry]
// A name that lands in a key or a workspace prefix is structural: "a/b" is two directories, ".." leaves
// the workspace. The charset therefore lives here once, in two shapes for two owners — `safe_segment`
// is total and answers `null` for the app to render, while a malformed workspace path panics, since a
// program routing unvalidated input into its store layout has a defect.
@"Canonicalise @name@ into a store path segment, or `null` when it cannot be one: trimmed,
lower-cased, then required to be non-empty and spelled only in lowercase letters, digits, `-` and `_`.
One offending character rejects the whole name. It is not a sanitiser: stripping the `/` out of \"a/b\"
would answer a different name and land two distinct requests in one place. It is the reader for a name
a model or a user supplied that becomes part of a key; the trimming and lower-casing are part of the
answer, so the value to store under is what comes back."
agent safe_segment(@"The proposed name, exactly as it was supplied — untrimmed and in any case." name: string) -> string | null {
let normalized = string.to_lower(value = string.trim(value = name))
// Katari has no character classes, so membership is one `contains` per code point over the charset.
let legal = for (let character in string.split(value = normalized, separator = ""), var every: boolean = true) {
next with { every = every && string.contains(value = "abcdefghijklmnopqrstuvwxyz0123456789-_", search = character) }
} then (_characters) { every }
if (normalized == "" || !legal) {
null
} else {
normalized
}
}
// Whether a whole workspace path is well formed: one or more `/`-separated segments, each already
// canonical. Comparing against `safe_segment`'s answer rather than re-checking the charset keeps one
// definition of a legal name.
agent is_safe_path(@"The candidate workspace path." path: string) -> boolean {
for (let segment in string.split(value = path, separator = "/"), var every: boolean = true) {
next with { every = every && safe_segment(name = segment) == segment }
} then (_segments) { every }
}
// @path@ back, or a panic when it is not a well-formed workspace path: there is no correct directory to
// fall back to, and a returned value would let the run keep writing under the bad prefix. A program
// cannot raise a panic, so the defect is spelled with the one total-to-partial door the language has,
// a zero divisor. The runtime's message says nothing about paths; this agent's name is what identifies
// it in the trace, which is half of why it exists.
agent panic_on_unsafe_path(@"The candidate workspace path." path: string) -> string {
if (is_safe_path(path = path)) {
path
} else {
let _defect = 1 / 0
path
}
}
@"Run @task@ as a critical section of the nearest enclosing `workspace`: that workspace's sequential
handler calls it in its own body, so two exclusives of one domain run one at a time, including against
a `parallel for` tool batch. Writes are last-write-wins, so this is what makes a read-modify-write
atomic.
Two consequences of the geometry. It binds to the nearest enclosing `workspace`, so an inner domain
shadows an outer one. And because prefix and domain are one install, the task runs inside the prefix of
the workspace serving it: a section that opens a workspace of its own descends further, and repeating
the directory it already stands in spells `app/memory/memory/...`. One lane per workspace, so a section
excludes the other sections of this workspace and interleaves with every other lane's.
The row is fixed to the store operations — everything else is computed before entering and closed over
— so a section never blocks on a model or a network. The answer crosses back as `unknown`; narrow it
with a `match` or `json.validate[T]`. With no workspace installed above the perform, the runtime serves
it at the project root, in one durable, project-wide FIFO across every run."
request exclusive(
@"The critical section; store operations only — compute everything else before entering and close over it." task: agent (value: null) -> unknown with get | set | delete | list,
) -> unknown
@"Open the workspace at @path@ under the current one, for the extent of @continuation@ — the
`use store.workspace(path = \"core\")` form, and the store's one provider. It installs both halves of a
working directory: the prefix (four parallel handlers re-perform each store operation outward with the
prefixed key, and a `list` gets @path@ prepended to its own path parameter, so nested workspaces
accumulate prefixes and the outermost bare perform is project-root
access) and the domain (one sequential handler serves `exclusive` by calling the section in its own
body, so its FIFO applies critical sections one at a time). The prefix handlers sit outside the domain,
which is what makes a section's keys resolve through the workspace it was opened in.
@path@ is one or more `/`-separated segments, each spelled as `safe_segment` requires; a path that is
not — an empty segment, a `..`, an unchecked name — panics here rather than opening a workspace
elsewhere. `safe_segment` is the check for a name that came from outside the program.
The row is coarser than the truth, which shows in the escalation report: all five clauses are installed
and each re-performs its own operation, so this agent's row names all four store operations whatever
the continuation does. It reads as \"reaches the store\" rather than as the set of operations used."
agent workspace[R, effect E](
@"The workspace's path under the current one, e.g. \"core\" or \"workers/scribe\"; `/`-separated `safe_segment`s, and a malformed one panics." path: string,
@"Runs with every store operation prefixed and `exclusive` served; its result is the provider's result." continuation: agent (value: null) -> R with {...E, get, set, delete, list, exclusive},
) -> R with E | get | set | delete | list {
// Clause parameter names are structural, so the `list` clause below binds `path` and shadows this
// agent's own. Rebinding here is also where the descent is checked, before any handler uses it.
let base = panic_on_unsafe_path(path = path)
// Parallel: prefixing is stateless arithmetic, and a sequential handler here would
// serialize a turn's concurrent tool batch through the workspace.
use parallel handler {
request get(key: string) {
next get(key = f"${base}/${key}")
}
request set(key: string, value: unknown) {
next set(key = f"${base}/${key}", value = value)
}
request delete(key: string) {
next delete(key = f"${base}/${key}")
}
request list(path: string) {
// An empty incoming path lists the workspace itself, so only the prefix travels outward.
if (path == "") {
next list(path = base)
} else {
next list(path = f"${base}/${path}")
}
}
}
// Sequential, and inside the prefix: a sequential handler's FIFO is what makes an exclusive a
// critical section, and re-performing from here routes its keys through the four clauses above.
use handler {
request exclusive(task: agent (value: null) -> unknown with get | set | delete | list) {
next task(value = null)
}
}
continuation(value = null)
}
@"Run @task@ at the nearest enclosing `share`'s install site — that site's workspaces, that site's
serial domain — and hand back what it answered: the request by which a desk reaches knowledge living
above its own workspace. A task runs at its server's install site, as with `exclusive`; the server here
is a `share` installed above the desks, so the desk's own workspaces do not travel with the task. It
lands in the shared place and opens whichever subdirectory it wants as its first move, which is what
lets one `share` serve every shared cell instead of one named request per cell. It binds to the nearest
enclosing `share`, so an inner shared place shadows an outer one.
The row is fixed to the store operations plus `exclusive`: a read-modify-write takes atomicity by
wrapping itself in `store.exclusive` inside the task, which lands in the shared place's own domain. The
answer crosses back as `unknown`; narrow it at the perform site. Unlike the four operations and
`exclusive`, this one is not runtime-served — with no `share` above it a `shared` rides to the run root
as an unanswered request rather than resolving to project-root keys, so the effect row is the guard."
request shared(
@"What to do in the shared place; store operations only — compute everything else before entering and close over it." task: agent (value: null) -> unknown with get | set | delete | list | exclusive,
) -> unknown
@"Open the SHARED PLACE for the extent of @continuation@ — the bare `use store.share` form (the shared
place is where it is installed, exactly as a workspace is). It serves `shared` by calling its task in
the clause body, so a task runs here, under this site's workspaces and over this site's serial domain,
while the desks below go on opening their own workspaces and reaching nothing of each other's. The
clause is parallel, so `shared` itself serializes nothing — several desks' reads run at once, and
ordering is `exclusive`'s, taken inside the task.
The install order is the app's workspace, then `share`, then the desks. A task's row carries
`exclusive` and this provider re-performs it outward, so `share` sits inside a workspace for a shared
critical section to land in that workspace's domain; installed above one, `store.exclusive` surfaces in
the enclosing signature and those sections ride to the runtime's project-wide root FIFO. A second
`share` below this one captures every `shared` under it — the dynamic-scope rule, and how a narrower
shared place is expressed.
One `shared` is one capability over the whole shared place, where a request per cell is a capability
per cell. Where a boundary between shared cells is the semantics, a named request for that cell keeps
it; the two compose, since a named proxy installed below this one can perform `shared` in its own
clause."
agent share[R, effect E](
@"Runs with `shared` served; its result is the provider's result." continuation: agent (value: null) -> R with {...E, shared},
) -> R with E | get | set | delete | list | exclusive {
// Parallel: routing a closure to the shared place decides where, not when, and a
// sequential handler would queue every desk that only reads it. Ordering is `exclusive`'s, taken
// inside the task.
use parallel handler {
request shared(task: agent (value: null) -> unknown with get | set | delete | list | exclusive) {
// `next` re-performs from this install site: the task's store operations and its `exclusive`
// escalate through this site's workspaces and domain, not through the caller's.
next task(value = null)
}
}
continuation(value = null)
}