-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathtime.ktr
More file actions
388 lines (358 loc) · 22.2 KB
/
Copy pathtime.ktr
File metadata and controls
388 lines (358 loc) · 22.2 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
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
// The `prelude.time` sub-module: durable wall-clock time. `now`, `sleep`, `sleep_until` and `watch`
// route to the runtime's `time` reactor (in-runtime, like `http.fetch`), so each performs `io`.
// They are externals rather than prims because a turn must be a deterministic function of its durable
// inputs: routing the clock read outside the turn is what keeps a replayed turn observing the same
// instant, and it is the same reactor that owns the timers `sleep` / `watch` persist and re-arm on.
@"The current wall-clock time, as epoch milliseconds. The instant becomes durable together with the
work that first observes it, so once any downstream step has seen the value it never changes under
replay or recovery. (A restart in the narrow window before that commit re-reads the clock — sound,
because nothing durable saw the first.)"
external agent now() -> number with io from "time"
@"Sleep for @milliseconds@ before resolving with `null`. The wake deadline is persisted: a runtime
restart re-arms the timer, and a deadline that already passed while the runtime was down resolves
immediately on recovery. A @milliseconds@ that is zero or negative resolves at once."
external agent sleep(@"The delay, in milliseconds; zero or negative resolves at once." milliseconds: number) -> null with io from "time"
@"Sleep until the absolute epoch-millisecond instant @time@, then resolve with `null` — the same
durable deadline as `sleep`, pinned to an absolute instant rather than a relative delay. An instant
already in the past resolves immediately."
external agent sleep_until(@"The absolute wake instant, in epoch milliseconds; a past instant resolves at once." time: number) -> null with io from "time"
@"A fixed interval: an occurrence every @milliseconds@ after the watch starts (the first occurrence is
one interval in, not at the start). @milliseconds@ must be positive."
data interval(@"The gap between occurrences, in milliseconds; a non-positive gap panics the watch." milliseconds: number)
@"A cron schedule: the occurrences of the standard cron @expression@ (the 5-field form, or the 6-field
form whose leading field is seconds) read in the IANA @timezone@. The timezone is required and
explicit — there is no ambient default, because \"every day at 09:00\" means a different instant in each
zone."
data cron(
@"5 fields, or 6 with a leading seconds field; a malformed expression panics the watch." expression: string,
@"An IANA zone name; an unknown zone panics the watch." timezone: string,
)
// When each occurrence fires. (Type synonyms take no docs.)
type schedule = interval | cron
@"Call @deliver_to@ once per @schedule@ occurrence, forever, passing the occurrence's scheduled epoch
millisecond as @time@. It never resolves on its own (`-> never`) and runs until the run is cancelled;
@deliver_to@'s effects @E@ flow to the caller's handlers unchanged.
The next occurrence is persisted and re-armed across a restart. If occurrences were missed while the
runtime was down, `watch` fires exactly once immediately on recovery (the earliest missed occurrence's
scheduled time — it does not backfill), then continues on schedule. Deliveries are serialized: the next
occurrence is not armed until the current delivery settles, so a slow @deliver_to@ rate-limits the ticks
rather than queueing them. There is no built-in retry: a @deliver_to@ that throws or panics propagates
and ends the watch, and resilience is composed at the call site with a `supervise` provider and a
converter."
external agent watch[effect E](
@"When occurrences fire: an `interval(...)` or a `cron(...)` value." schedule: schedule,
@"Called once per occurrence; its @time@ is the occurrence's scheduled epoch millisecond, not the delivery instant." deliver_to: agent (time: number) -> null with E,
) -> never with E | io from "time"
@"The task settled first: its value."
data completed[T](@"The task's result." value: T)
@"The deadline passed first; the task's arm was cancelled."
data deadline_passed()
// Which side of a `with_deadline` race settled first. (Type synonyms take no docs.)
type raced[T] = completed[T] | deadline_passed
@"`with_deadline`'s settle channel — performed by whichever arm finishes first, handled (and `break`ed
on) inside `with_deadline` alone. Its `lacks` constraint is what reserves it: a task cannot perform it,
so the handler peel stays sound over the task's still-generic row. The runtime never machine-answers
it, so nothing outside the run resolves it."
request race_settled[T](@"The settling side's outcome." outcome: T) -> null
@"Race @task@ against a @milliseconds@ deadline and return whichever settled first: `completed` with
the task's value, or `deadline_passed` — the loser's arm is cancelled (the ordinary cancel cascade; an
in-flight external call is interrupted at-most-once, like any cancel). The task's own throws escalate
as usual; a handler around or inside the task catches them."
agent with_deadline[T, effect E lacks race_settled](
@"The budget, in milliseconds." milliseconds: number,
@"The task to race; its row may be anything that does not perform `race_settled`." task: agent (value: null) -> T with E,
) -> raced[T] with E | io {
use handler {
request race_settled(outcome: raced[T]) -> null { break outcome }
}
parallel [
race_settled(outcome = completed(value = task(value = null))),
{
sleep(milliseconds = milliseconds)
race_settled(outcome = deadline_passed())
},
]
// Unreachable — an arm always performs `race_settled` before the parallel could complete.
deadline_passed()
}
// The civil calendar below is Howard Hinnant's closed-form `civil_from_days` / `days_from_civil` over
// the proleptic Gregorian calendar, as plain Katari. A wall clock is `civil` fields at a fixed offset
// passed explicitly; resolving a named zone to an offset is a lookup rather than arithmetic, and is
// the `zone_offset` primitive at the foot of the module. Composing the two per instant is what makes a
// named-zone render DST-correct.
@"A wall-clock date-time split into its calendar fields (proleptic Gregorian). Produced by `to_civil`
and folded back by `from_civil`; a plain value carrying NO zone of its own — it means whatever offset
you read it at."
data civil(
@"The calendar year." year: integer,
@"1 (January) to 12 (December)." month: integer,
@"1 to the month's length (`days_in_month`)." day: integer,
@"0 to 23." hour: integer,
@"0 to 59." minute: integer,
@"0 to 59." second: integer,
@"0 to 999." millisecond: integer,
)
@"Split an epoch-millisecond instant into its wall-clock fields at a fixed offset (@offset_minutes@
east of UTC; the default 0 reads UTC). `from_civil` at the same offset is the exact inverse.
Sub-millisecond precision is dropped."
agent to_civil(epoch_milliseconds: number, offset_minutes: integer ?= 0) -> civil {
let total_milliseconds = math.floor(value = epoch_milliseconds) + offset_minutes * 60000
let total_seconds = math.floor(value = total_milliseconds / 1000)
let millisecond = total_milliseconds - total_seconds * 1000
let days = math.floor(value = total_seconds / 86400)
let seconds_of_day = total_seconds - days * 86400
// civil_from_days: shift the epoch to an era based on 1st March 2000 so the leap day falls at the end
// of the 400-year cycle. Every division is a floor, so pre-1970 instants use the same arithmetic.
let shifted = days + 719468
let era = math.floor(value = shifted / 146097)
let day_of_era = shifted - era * 146097
let year_of_era = math.floor(value = (day_of_era - math.floor(value = day_of_era / 1460) + math.floor(value = day_of_era / 36524) - math.floor(value = day_of_era / 146096)) / 365)
let year_from_march = year_of_era + era * 400
let day_of_year = day_of_era - (365 * year_of_era + math.floor(value = year_of_era / 4) - math.floor(value = year_of_era / 100))
let month_prime = math.floor(value = (5 * day_of_year + 2) / 153)
let day = day_of_year - math.floor(value = (153 * month_prime + 2) / 5) + 1
// The March-based month index (0..11) maps back to the calendar month; January and February belong
// to the following calendar year.
let month = if (month_prime < 10) { month_prime + 3 } else { month_prime - 9 }
let year = if (month <= 2) { year_from_march + 1 } else { year_from_march }
civil(
year = year,
month = month,
day = day,
hour = math.floor(value = seconds_of_day / 3600),
minute = math.floor(value = (seconds_of_day % 3600) / 60),
second = seconds_of_day % 60,
millisecond = millisecond,
)
}
@"Fold wall-clock fields back to an epoch-millisecond instant, reading them at a fixed offset
(@offset_minutes@ east of UTC; the default 0 means the fields are UTC) — the exact inverse of
`to_civil` at the same offset. Out-of-range fields fold arithmetically rather than erroring (month 13
is January of the next year, hour 24 is midnight of the next day), so date arithmetic is plain field
arithmetic: `day = value.day + 7` is one week later with every carry handled."
agent from_civil(value: civil, offset_minutes: integer ?= 0) -> number {
// Normalize the month by floor division (floor `%` sends month 0 to December) so the linear folds
// below only ever see 1..12; every other field is linear in the fold and carries by itself.
let month_index = value.month - 1
let year = value.year + math.floor(value = month_index / 12)
let month = month_index % 12 + 1
// days_from_civil: January and February count as months 13/14 of the previous year so the leap day
// ends the year, then the 400/100/4-year leap rules fold the civil date to a day count from 1970.
let year_shifted = if (month <= 2) { year - 1 } else { year }
let era = math.floor(value = year_shifted / 400)
let year_of_era = year_shifted - era * 400
let month_prime = if (month > 2) { month - 3 } else { month + 9 }
let day_of_year = math.floor(value = (153 * month_prime + 2) / 5) + value.day - 1
let day_of_era = year_of_era * 365 + math.floor(value = year_of_era / 4) - math.floor(value = year_of_era / 100) + day_of_year
let days = era * 146097 + day_of_era - 719468
(days * 86400 + value.hour * 3600 + value.minute * 60 + value.second) * 1000 + value.millisecond - offset_minutes * 60000
}
@"The ISO 8601 day of the week — 1 (Monday) to 7 (Sunday) — of the instant's wall-clock date at
@offset_minutes@ (default UTC)."
agent day_of_week(epoch_milliseconds: number, offset_minutes: integer ?= 0) -> integer {
let total_milliseconds = math.floor(value = epoch_milliseconds) + offset_minutes * 60000
let days = math.floor(value = math.floor(value = total_milliseconds / 1000) / 86400)
// 1970-01-01 was a Thursday (ISO 4); `%` is a floor modulo, so pre-epoch days stay correct.
(days + 3) % 7 + 1
}
@"Whether @year@ is a Gregorian leap year (divisible by 4, except centuries not divisible by 400)."
agent is_leap_year(year: integer) -> boolean {
year % 4 == 0 && (year % 100 != 0 || year % 400 == 0)
}
@"The number of days in @month@ (1..12) of @year@ — 28..31, leap-rule aware. A month outside 1..12
first folds into its year like `from_civil` (month 13 is January of the next year)."
agent days_in_month(year: integer, month: integer) -> integer {
let month_index = month - 1
let folded_year = year + math.floor(value = month_index / 12)
match (month_index % 12 + 1) {
case 2 -> if (is_leap_year(year = folded_year)) { 29 } else { 28 }
case 4 -> 30
case 6 -> 30
case 9 -> 30
case 11 -> 30
case _ -> 31
}
}
@"Format an instant as RFC3339 with millisecond precision — `YYYY-MM-DDTHH:MM:SS.mmmZ` at the default
UTC offset, the same wall clock with a `±HH:MM` suffix at a non-zero @offset_minutes@. The wire inverse
of `from_rfc3339`. A year outside 0..9999 renders faithfully (every digit, a leading `-`) even though
strict RFC3339 wants exactly four."
agent to_rfc3339(epoch_milliseconds: number, offset_minutes: integer ?= 0) -> string {
agent pad(value: integer, width: integer) -> string {
string.pad_start(value = string.to_string(value = value), width = width, padding = "0")
}
let fields = to_civil(epoch_milliseconds = epoch_milliseconds, offset_minutes = offset_minutes)
let year = if (fields.year < 0) { "-" ++ pad(value = 0 - fields.year, width = 4) } else { pad(value = fields.year, width = 4) }
let date = f"${year}-${pad(value = fields.month, width = 2)}-${pad(value = fields.day, width = 2)}"
let clock = f"${pad(value = fields.hour, width = 2)}:${pad(value = fields.minute, width = 2)}:${pad(value = fields.second, width = 2)}.${pad(value = fields.millisecond, width = 3)}"
let zone = if (offset_minutes == 0) {
"Z"
} else {
let sign = if (offset_minutes < 0) { "-" } else { "+" }
let magnitude = math.abs(value = offset_minutes)
f"${sign}${pad(value = math.floor(value = magnitude / 60), width = 2)}:${pad(value = magnitude % 60, width = 2)}"
}
f"${date}T${clock}${zone}"
}
@"Parse an RFC3339 timestamp — `YYYY-MM-DDTHH:MM:SS[.fraction]` followed by `Z` or `±HH:MM` — to an
epoch-millisecond UTC instant, or `null` when the string is not one (like `string.to_integer`).
Validated, not clamped: a date that does not exist (February 30th) is `null`, not a silently carried
date. `T` / `Z` also read lowercase; a fraction beyond milliseconds is truncated; a leap second (`:60`)
folds into the next minute."
agent from_rfc3339(value: string) -> number | null {
agent pad(value: integer, width: integer) -> string {
string.pad_start(value = string.to_string(value = value), width = width, padding = "0")
}
agent read_field(start: integer, end: integer) -> integer | null {
string.to_integer(value = string.slice(value = value, start = start, end = end))
}
let length = string.length(value = value)
if (length < 20) {
null
} else {
// Each region is validated by re-rendering: parse the fields, format them back canonically, and
// require equality — one comparison rejects the malformed shapes field-wise reads let through.
let zone_is_utc = string.to_upper(value = string.slice(value = value, start = length - 1, end = length)) == "Z"
let zone_start = if (zone_is_utc) { length - 1 } else { length - 6 }
let offset_minutes = if (zone_is_utc) {
0
} else {
let sign = string.slice(value = value, start = zone_start, end = zone_start + 1)
match ([read_field(start = length - 5, end = length - 3), read_field(start = length - 2, end = length)]) {
case [integer(zone_hour), integer(zone_minute)] ->
if (
(sign == "+" || sign == "-")
&& zone_hour <= 23
&& zone_minute <= 59
&& string.slice(value = value, start = zone_start, end = length) == f"${sign}${pad(value = zone_hour, width = 2)}:${pad(value = zone_minute, width = 2)}"
) {
if (sign == "-") { 0 - (zone_hour * 60 + zone_minute) } else { zone_hour * 60 + zone_minute }
} else {
null
}
case _ -> null
}
}
// The fraction is checked point by point because it can be longer than any integer read allows;
// the first three digits, right-padded with zeros, are the milliseconds and the rest truncates.
let millisecond = if (zone_start == 19) {
0
} else {
let digits = string.slice(value = value, start = 20, end = zone_start)
// Katari has no character classes, so membership is one `contains` per code point.
let all_digits = for (let point in string.split(value = digits, separator = ""), var every: boolean = true) {
next with { every = every && string.contains(value = "0123456789", search = point) }
} then (_points) { every }
let well_formed = (
zone_start > 20
&& string.slice(value = value, start = 19, end = 20) == "."
&& all_digits
)
match ([well_formed, string.to_integer(value = string.slice(value = digits ++ "00", start = 0, end = 3))]) {
case [true, integer(parsed)] -> parsed
case _ -> null
}
}
match ([offset_minutes, millisecond, read_field(start = 0, end = 4), read_field(start = 5, end = 7), read_field(start = 8, end = 10), read_field(start = 11, end = 13), read_field(start = 14, end = 16), read_field(start = 17, end = 19)]) {
case [integer(offset), integer(fraction), integer(year), integer(month), integer(day), integer(hour), integer(minute), integer(second)] -> {
let canonical_head = f"${pad(value = year, width = 4)}-${pad(value = month, width = 2)}-${pad(value = day, width = 2)}T${pad(value = hour, width = 2)}:${pad(value = minute, width = 2)}:${pad(value = second, width = 2)}"
// Validated, not clamped — except second 60, the leap second, which folds forward in
// `from_civil`.
if (
string.to_upper(value = string.slice(value = value, start = 0, end = 19)) != canonical_head
|| month < 1
|| month > 12
|| day < 1
|| day > days_in_month(year = year, month = month)
|| hour > 23
|| minute > 59
|| second > 60
) {
null
} else {
from_civil(
value = civil(year = year, month = month, day = day, hour = hour, minute = minute, second = second, millisecond = fraction),
offset_minutes = offset,
)
}
}
case _ -> null
}
}
}
// The civil labels below render only; advancing a date by whole days is calendar arithmetic and
// belongs to `to_civil` / `from_civil`. There is no pattern language — a program wanting a further
// label composes it from `to_civil`'s fields the way these do. Each takes `offset_minutes` explicitly,
// so composing it with `zone_offset` per instant makes a named zone's rendering DST-correct.
@"The three-letter English label of an ISO weekday — 1 (Monday) through 7 (Sunday), the numbering
`day_of_week` answers. Total: anything outside 1..7 answers `\"???\"` rather than a plausible label."
agent weekday_label(@"The ISO weekday, 1 (Monday) to 7 (Sunday); anything else answers \"???\"." day: integer) -> string {
match (day) {
case 1 -> "Mon"
case 2 -> "Tue"
case 3 -> "Wed"
case 4 -> "Thu"
case 5 -> "Fri"
case 6 -> "Sat"
case 7 -> "Sun"
case _ -> "???"
}
}
@"An offset east of UTC as its `±HH:MM` label, for a person reading it beside a civil time. UTC renders
`+00:00` rather than `Z` (`to_rfc3339` renders for the wire and spells it `Z`), and a non-whole-hour
offset renders faithfully (Asia/Kathmandu's 345 is `+05:45`)."
agent offset_label(@"The offset in minutes EAST of UTC — exactly what `zone_offset` answers." offset_minutes: integer) -> string {
agent pad(value: integer, width: integer) -> string {
string.pad_start(value = string.to_string(value = value), width = width, padding = "0")
}
// The sign is taken from the signed value and the magnitude rendered separately, so `-330` reads
// `-05:30` rather than the `-5:-30` a component-wise render produces.
let sign = if (offset_minutes < 0) { "-" } else { "+" }
let magnitude = math.abs(value = offset_minutes)
f"${sign}${pad(value = math.floor(value = magnitude / 60), width = 2)}:${pad(value = magnitude % 60, width = 2)}"
}
@"The instant's civil DATE at @offset_minutes@ (default UTC) as `YYYY-MM-DD` — the date half of
`to_rfc3339` without the clock, the zone or the `T`. ISO order is string order, so dates in this form
sort with `array.sort`, compare with `<`, and group by store-key prefix. A year outside 0..9999 renders
every digit rather than truncating, which keeps the date exact and drops the sort property."
agent date_label(
@"The instant, in epoch milliseconds." epoch_milliseconds: number,
@"The offset in minutes east of UTC; the default 0 reads UTC." offset_minutes: integer ?= 0,
) -> string {
agent pad(value: integer, width: integer) -> string {
string.pad_start(value = string.to_string(value = value), width = width, padding = "0")
}
let fields = to_civil(epoch_milliseconds = epoch_milliseconds, offset_minutes = offset_minutes)
let year = if (fields.year < 0) { "-" ++ pad(value = 0 - fields.year, width = 4) } else { pad(value = fields.year, width = 4) }
f"${year}-${pad(value = fields.month, width = 2)}-${pad(value = fields.day, width = 2)}"
}
@"The instant as a wall clock reads it at @offset_minutes@ (default UTC) —
`2026-07-26 (Sun) 14:32 +09:00`: the civil date, the weekday, the time to the minute, and the offset,
in one line, so a reader needs no arithmetic. Seconds are absent; `to_rfc3339` is the render for a
machine reader."
agent stamp(
@"The instant, in epoch milliseconds." epoch_milliseconds: number,
@"The offset in minutes east of UTC; the default 0 reads UTC." offset_minutes: integer ?= 0,
) -> string {
agent pad(value: integer, width: integer) -> string {
string.pad_start(value = string.to_string(value = value), width = width, padding = "0")
}
let fields = to_civil(epoch_milliseconds = epoch_milliseconds, offset_minutes = offset_minutes)
let weekday = weekday_label(day = day_of_week(epoch_milliseconds = epoch_milliseconds, offset_minutes = offset_minutes))
let date = date_label(epoch_milliseconds = epoch_milliseconds, offset_minutes = offset_minutes)
f"${date} (${weekday}) ${pad(value = fields.hour, width = 2)}:${pad(value = fields.minute, width = 2)} ${offset_label(offset_minutes = offset_minutes)}"
}
@"The offset of the IANA @zone@ in effect at @epoch_milliseconds@, in MINUTES EAST of UTC — exactly the
`offset_minutes` this module's agents take. Per-instant, so it is DST-correct by construction, and a
zone whose offset is not a whole hour answers it faithfully (\"Asia/Kathmandu\" is 345).
`null` when the runtime's zone database does not know @zone@. The names it does know are exactly the
ones a `cron` schedule's timezone accepts, being the same database: canonical IANA names, historical
aliases, any letter case, and the legacy abbreviations. An abbreviation names a whole zone with its DST
rules rather than the standard offset it resembles (\"PST\" answers -420 in July, not -480).
Deterministic in its arguments: it reads no clock, so a replay recomputes the same offset. The only
drift possible is a zone database update between executions. Pre-1900 instants round to the nearest
minute."
primitive agent zone_offset(
@"The instant to read the offset AT, in epoch milliseconds; fractions floor, like `to_civil`." epoch_milliseconds: number,
@"An IANA zone name (e.g. \"Asia/Tokyo\", \"America/New_York\", \"UTC\"); an unknown name answers null." zone: string,
) -> integer | null