1module Observe.Value
2
3import Data.UTF8
4import Model.Word32
5import Std.Byte
6import Std.Flag
7import Data.JSON
8import Data.JSONAccess
9import Data.JSONRender
10import Std.Natural
11
12-- AOS VALUES (docs/standards/AOS-1.0-draft-1.md §6, §24.2): the typed value
13-- a schema-governed payload slot holds, as AOS-JSON/1 writes it -- every
14-- integer a canonical decimal STRING (no JSON number, so no counter or tick
15-- ever passes through a float: AOS-VAL-002), a float as its exact bit
16-- pattern in lowercase hex, bytes as lowercase hex -- and the availability
17-- states a slot can be in instead of holding a value (AOS-VAL-003: zero is
18-- never "not measured").
19--
20-- This module is the semantic authority for what a valid tagged value is.
21-- The bootstrap tool's reader (tool/Aos.hs, `checkValue`) implements the
22-- same rules; scripts/ci/observability.sh holds the two to the same verdict
23-- on every fixture. Decoding is strict: a tagged value has EXACTLY the
24-- members its tag names -- an extra member is an error, not ignored.
25
26-- ---------------------------------------------------------------------------
27-- Bytes: digits, hex, identities
28
29family AosMember : Type 0
30constructor AosMemberAbsent
31constructor AosMemberPresent
32field unrestricted aosMemberValue : (family JSON)
33end-family
34
35family AosValue : Type 0
36constructor AosBool
37field unrestricted aosBoolFlag : Nat
38constructor AosU64
39field unrestricted aosU64Value : Nat
40constructor AosI64
41field unrestricted aosI64Negative : Nat
42field unrestricted aosI64Magnitude : Nat
43constructor AosBigInt
44field unrestricted aosBigIntNegative : Nat
45field unrestricted aosBigIntMagnitude : Nat
46constructor AosDecimal
47field unrestricted aosDecimalCoefficientNegative : Nat
48field unrestricted aosDecimalCoefficient : Nat
49field unrestricted aosDecimalScaleNegative : Nat
50field unrestricted aosDecimalScale : Nat
51constructor AosF32
52field unrestricted aosF32Bits : Bytes
53constructor AosF64
54field unrestricted aosF64Bits : Bytes
55constructor AosText
56field unrestricted aosTextBytes : Bytes
57constructor AosBytes
58field unrestricted aosBytesHex : Bytes
59constructor AosRef
60field unrestricted aosRefKind : Bytes
61field unrestricted aosRefIdentity : Bytes
62constructor AosNull
63constructor AosList
64recursive unrestricted aosListItems
65constructor AosItemsEnd
66constructor AosItemsNext
67recursive unrestricted aosItemsHead
68recursive unrestricted aosItemsTail
69constructor AosMap
70recursive unrestricted aosMapMembers
71constructor AosMembersEnd
72constructor AosMembersNext
73field unrestricted aosMembersKey : Bytes
74recursive unrestricted aosMembersValue
75recursive unrestricted aosMembersTail
76end-family
77
78family AosDecoded : Type 0
79constructor AosDecodedValue
80field unrestricted aosDecodedValue : (family AosValue)
81constructor AosDecodeRejected
82end-family
83
84-- 1 when lo <= b <= hi
85def aosByteBetween =
86 (lambda unrestricted b : Byte . (lambda unrestricted lo : Byte . (lambda unrestricted hi : Byte .
87 (naturalAnd (naturalIsZero (byte-less-than b lo)) (naturalIsZero (byte-less-than hi b))))))
88
89def aosIsDigitByte = (lambda unrestricted b : Byte . (aosByteBetween b (byte 48) (byte 57)))
90
91-- 0-9 and a-f: AOS-JSON/1 hex is lowercase only
92def aosIsLowerHexByte =
93 (lambda unrestricted b : Byte . (naturalOr (aosIsDigitByte b) (aosByteBetween b (byte 97) (byte 102))))
94
95def aosAllBytes =
96 (lambda unrestricted predicate : (pi unrestricted b : Byte . Nat) . (lambda unrestricted input : Bytes .
97 (bytes-eliminate (lambda unrestricted current : Bytes . Nat) 1
98 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat .
99 (naturalAnd (predicate head) induction))))
100 input)))
101
102def aosAnyByte =
103 (lambda unrestricted predicate : (pi unrestricted b : Byte . Nat) . (lambda unrestricted input : Bytes .
104 (bytes-eliminate (lambda unrestricted current : Bytes . Nat) 0
105 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat .
106 (naturalOr (predicate head) induction))))
107 input)))
108
109-- the value of a string of decimal digits, most significant first (a left
110-- fold: the accumulator is threaded through the right fold's functions)
111def aosDigitsValue =
112 (lambda unrestricted input : Bytes .
113 (app (bytes-eliminate (lambda unrestricted current : Bytes . (pi unrestricted acc : Nat . Nat))
114 (lambda unrestricted acc : Nat . acc)
115 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes .
116 (lambda unrestricted induction : (pi unrestricted acc : Nat . Nat) .
117 (lambda unrestricted acc : Nat .
118 (induction (naturalAdd (naturalMultiply acc 10) (naturalSaturatingSubtract (byte-to-nat head) 48)))))))
119 input)
120 0))
121
122-- AOS-JSON-004: `0`, or a nonzero digit then digits; at most 4096 digits
123def aosCanonicalUnsigned =
124 (lambda unrestricted input : Bytes .
125 (naturalAnd (naturalNonzero (bytes-length input))
126 (naturalAnd (naturalLessOrEqual (bytes-length input) 4096)
127 (naturalAnd (aosAllBytes aosIsDigitByte input)
128 (naturalOr (naturalEqual (bytes-length input) 1)
129 (naturalIsZero (byte-equal (bytes-head input) (byte 48))))))))
130
131def aosU64Maximum : Nat = 18446744073709551615
132def aosI64Maximum : Nat = 9223372036854775807
133def aosI64MinimumMagnitude : Nat = 9223372036854775808
134
135def aosIsU64Text =
136 (lambda unrestricted input : Bytes .
137 (naturalAnd (aosCanonicalUnsigned input)
138 (naturalAnd (naturalLessOrEqual (bytes-length input) 20)
139 (naturalLessOrEqual (aosDigitsValue input) aosU64Maximum))))
140
141def aosHasMinus =
142 (lambda unrestricted input : Bytes .
143 (naturalAnd (naturalNonzero (bytes-length input)) (byte-equal (bytes-head input) (byte 45))))
144
145-- the digits of a signed integer, its sign removed
146def aosSignedDigits =
147 (lambda unrestricted input : Bytes .
148 (nat-eliminate (lambda unrestricted current : Nat . Bytes) input
149 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . (bytes-tail input)))
150 (aosHasMinus input)))
151
152-- an optional '-' then a canonical unsigned; "-0" is refused
153def aosCanonicalSigned =
154 (lambda unrestricted input : Bytes .
155 (naturalAnd (aosCanonicalUnsigned (aosSignedDigits input))
156 (naturalOr (naturalIsZero (aosHasMinus input))
157 (naturalNonzero (aosDigitsValue (aosSignedDigits input))))))
158
159def aosIsI64Text =
160 (lambda unrestricted input : Bytes .
161 (naturalAnd (aosCanonicalSigned input)
162 (naturalAnd (naturalLessOrEqual (bytes-length (aosSignedDigits input)) 19)
163 (naturalLessOrEqual (aosDigitsValue (aosSignedDigits input))
164 (naturalSelect (aosHasMinus input) aosI64MinimumMagnitude aosI64Maximum)))))
165
166-- exactly `width` lowercase hex digits
167def aosIsHexOfWidth =
168 (lambda unrestricted width : Nat . (lambda unrestricted input : Bytes .
169 (naturalAnd (naturalEqual (bytes-length input) width) (aosAllBytes aosIsLowerHexByte input))))
170
171-- lowercase hex of even length (bytes)
172def aosIsHexBytes =
173 (lambda unrestricted input : Bytes .
174 (naturalAnd (aosAllBytes aosIsLowerHexByte input) (naturalIsZero (naturalModuloUnchecked (bytes-length input) 2))))
175
176-- AOS-ID-003: 32 lowercase hex digits, not all zero
177def aosIsIdentity =
178 (lambda unrestricted input : Bytes .
179 (naturalAnd (aosIsHexOfWidth 32 input)
180 (aosAnyByte (lambda unrestricted b : Byte . (naturalIsZero (byte-equal b (byte 48)))) input)))
181
182-- ---------------------------------------------------------------------------
183-- JSON navigation
184
185-- an object's member by name (absent when the value is not an object)
186def aosMember =
187 (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) .
188 (eliminate JSONValueAccessResult (lambda unrestricted current : (family JSONValueAccessResult) . (family AosMember))
189 (objectLookup name value)
190 (branch JSONValueAccessSucceeded found . (constructor AosMember AosMemberPresent found))
191 (branch JSONValueAccessFailed error . (constructor AosMember AosMemberAbsent)))))
192
193-- the kind of a document value: 1 object, 2 array, 3 string, 4 number,
194-- 5 boolean, 6 null (0: a member or element chain, never a document value)
195def aosKind =
196 (lambda unrestricted value : (family JSON) .
197 (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value
198 (branch JSONObject members membersInduction . 1)
199 (branch JSONObjectEnd . 0)
200 (branch JSONObjectMember key member tail memberInduction tailInduction . 0)
201 (branch JSONArray values valuesInduction . 2)
202 (branch JSONArrayEnd . 0)
203 (branch JSONArrayNext head tail headInduction tailInduction . 0)
204 (branch JSONString text . 3)
205 (branch JSONNumber digits . 4)
206 (branch JSONBoolean flag . 5)
207 (branch JSONNull . 6)))
208
209def aosIsObject = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 1))
210def aosIsArray = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 2))
211def aosIsString = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 3))
212def aosIsBoolean = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 5))
213
214-- a string's bytes (empty for anything else: test `aosIsString` first)
215def aosStringBytes =
216 (lambda unrestricted value : (family JSON) .
217 (eliminate JSON (lambda unrestricted current : (family JSON) . Bytes) value
218 (branch JSONObject members membersInduction . b"")
219 (branch JSONObjectEnd . b"")
220 (branch JSONObjectMember key member tail memberInduction tailInduction . b"")
221 (branch JSONArray values valuesInduction . b"")
222 (branch JSONArrayEnd . b"")
223 (branch JSONArrayNext head tail headInduction tailInduction . b"")
224 (branch JSONString text . text)
225 (branch JSONNumber digits . b"")
226 (branch JSONBoolean flag . b"")
227 (branch JSONNull . b"")))
228
229def aosBooleanFlag =
230 (lambda unrestricted value : (family JSON) .
231 (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value
232 (branch JSONObject members membersInduction . 0)
233 (branch JSONObjectEnd . 0)
234 (branch JSONObjectMember key member tail memberInduction tailInduction . 0)
235 (branch JSONArray values valuesInduction . 0)
236 (branch JSONArrayEnd . 0)
237 (branch JSONArrayNext head tail headInduction tailInduction . 0)
238 (branch JSONString text . 0)
239 (branch JSONNumber digits . 0)
240 (branch JSONBoolean flag . flag)
241 (branch JSONNull . 0)))
242
243-- an object's number of members (0 for anything else: test first)
244def aosObjectSize =
245 (lambda unrestricted value : (family JSON) .
246 (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value
247 (branch JSONObject members membersInduction . membersInduction)
248 (branch JSONObjectEnd . 0)
249 (branch JSONObjectMember key member tail memberInduction tailInduction . (succ tailInduction))
250 (branch JSONArray values valuesInduction . 0)
251 (branch JSONArrayEnd . 0)
252 (branch JSONArrayNext head tail headInduction tailInduction . 0)
253 (branch JSONString text . 0)
254 (branch JSONNumber digits . 0)
255 (branch JSONBoolean flag . 0)
256 (branch JSONNull . 0)))
257
258def aosHas =
259 (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) .
260 (eliminate AosMember (lambda unrestricted current : (family AosMember) . Nat) (aosMember name value)
261 (branch AosMemberAbsent . 0)
262 (branch AosMemberPresent found . 1))))
263
264-- the member's string bytes (b"" when absent or not a string)
265def aosMemberBytes =
266 (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) .
267 (eliminate AosMember (lambda unrestricted current : (family AosMember) . Bytes) (aosMember name value)
268 (branch AosMemberAbsent . b"")
269 (branch AosMemberPresent found . (aosStringBytes found)))))
270
271-- 1 when the member is present and a string
272def aosMemberIsString =
273 (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) .
274 (eliminate AosMember (lambda unrestricted current : (family AosMember) . Nat) (aosMember name value)
275 (branch AosMemberAbsent . 0)
276 (branch AosMemberPresent found . (aosIsString found)))))
277
278-- an object with exactly these member names (no duplicates exist after the
279-- strict parse, so the count and the presence of each decide it)
280def aosHasExactly1 =
281 (lambda unrestricted a : Bytes . (lambda unrestricted value : (family JSON) .
282 (naturalAnd (aosIsObject value) (naturalAnd (naturalEqual (aosObjectSize value) 1) (aosHas a value)))))
283def aosHasExactly2 =
284 (lambda unrestricted a : Bytes . (lambda unrestricted b : Bytes . (lambda unrestricted value : (family JSON) .
285 (naturalAnd (aosIsObject value) (naturalAnd (naturalEqual (aosObjectSize value) 2)
286 (naturalAnd (aosHas a value) (aosHas b value)))))))
287def aosHasExactly3 =
288 (lambda unrestricted a : Bytes . (lambda unrestricted b : Bytes . (lambda unrestricted c : Bytes . (lambda unrestricted value : (family JSON) .
289 (naturalAnd (aosIsObject value) (naturalAnd (naturalEqual (aosObjectSize value) 3)
290 (naturalAnd (aosHas a value) (naturalAnd (aosHas b value) (aosHas c value)))))))))
291
292-- a verdict code: 0 when `first` is 0 (passed), else `first` -- the next
293-- check is not evaluated once one has failed
294def aosThen =
295 (lambda unrestricted first : Nat . (lambda unrestricted next : Nat . (naturalSelect first first next)))
296
297-- `whenTrue` when the flag is nonzero, else `whenFalse`, at any type (the
298-- one not chosen is not evaluated)
299def aosChoose =
300 (lambda erased result : Type 0 . (lambda unrestricted condition : Nat .
301 (lambda unrestricted whenTrue : result . (lambda unrestricted whenFalse : result .
302 (nat-eliminate (lambda unrestricted current : Nat . result) whenFalse
303 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : result . whenTrue))
304 condition)))))
305
306-- ---------------------------------------------------------------------------
307-- Typed values
308
309def aosRejected : (family AosDecoded) = (constructor AosDecoded AosDecodeRejected)
310def aosDecodedAs = (lambda unrestricted value : (family AosValue) . (constructor AosDecoded AosDecodedValue value))
311
312def aosBind =
313 (lambda unrestricted decoded : (family AosDecoded) .
314 (lambda unrestricted continue : (pi unrestricted value : (family AosValue) . (family AosDecoded)) .
315 (eliminate AosDecoded (lambda unrestricted current : (family AosDecoded) . (family AosDecoded)) decoded
316 (branch AosDecodedValue value . (continue value))
317 (branch AosDecodeRejected . aosRejected))))
318
319-- decode when `valid`, else reject
320def aosWhen =
321 (lambda unrestricted valid : Nat . (lambda unrestricted value : (family AosValue) .
322 (aosChoose (family AosDecoded) valid (aosDecodedAs value) aosRejected)))
323
324-- a list's elements, each by `decode` (the decoder with one less fuel)
325def aosDecodeItems =
326 (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) .
327 (lambda unrestricted array : (family JSON) .
328 (eliminate JSON (lambda unrestricted current : (family JSON) . (family AosDecoded)) array
329 (branch JSONObject members membersInduction . aosRejected)
330 (branch JSONObjectEnd . aosRejected)
331 (branch JSONObjectMember key member tail memberInduction tailInduction . aosRejected)
332 (branch JSONArray values valuesInduction .
333 (aosBind valuesInduction (lambda unrestricted items : (family AosValue) . (aosDecodedAs (constructor AosValue AosList items)))))
334 (branch JSONArrayEnd . (aosDecodedAs (constructor AosValue AosItemsEnd)))
335 (branch JSONArrayNext head tail headInduction tailInduction .
336 (aosBind (decode head) (lambda unrestricted first : (family AosValue) .
337 (aosBind tailInduction (lambda unrestricted rest : (family AosValue) .
338 (aosDecodedAs (constructor AosValue AosItemsNext first rest)))))))
339 (branch JSONString text . aosRejected)
340 (branch JSONNumber digits . aosRejected)
341 (branch JSONBoolean flag . aosRejected)
342 (branch JSONNull . aosRejected))))
343
344-- a map's members, each value by `decode`
345def aosDecodeMembers =
346 (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) .
347 (lambda unrestricted object : (family JSON) .
348 (eliminate JSON (lambda unrestricted current : (family JSON) . (family AosDecoded)) object
349 (branch JSONObject members membersInduction .
350 (aosBind membersInduction (lambda unrestricted chain : (family AosValue) . (aosDecodedAs (constructor AosValue AosMap chain)))))
351 (branch JSONObjectEnd . (aosDecodedAs (constructor AosValue AosMembersEnd)))
352 (branch JSONObjectMember key member tail memberInduction tailInduction .
353 (aosBind (decode member) (lambda unrestricted first : (family AosValue) .
354 (aosBind tailInduction (lambda unrestricted rest : (family AosValue) .
355 (aosDecodedAs (constructor AosValue AosMembersNext key first rest)))))))
356 (branch JSONArray values valuesInduction . aosRejected)
357 (branch JSONArrayEnd . aosRejected)
358 (branch JSONArrayNext head tail headInduction tailInduction . aosRejected)
359 (branch JSONString text . aosRejected)
360 (branch JSONNumber digits . aosRejected)
361 (branch JSONBoolean flag . aosRejected)
362 (branch JSONNull . aosRejected))))
363
364-- the member's JSON value (JSONNull when absent: test with aosHas first)
365def aosMemberValue =
366 (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) .
367 (eliminate AosMember (lambda unrestricted current : (family AosMember) . (family JSON)) (aosMember name value)
368 (branch AosMemberAbsent . (constructor JSON JSONNull))
369 (branch AosMemberPresent found . found))))
370
371-- Each tag's decoder: the value's exact member set, then its content.
372def aosDecodeBool =
373 (lambda unrestricted value : (family JSON) . (let unrestricted inner = (aosMemberValue b"v" value)
374 in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosIsBoolean inner))
375 (constructor AosValue AosBool (aosBooleanFlag inner)))))
376
377def aosDecodeU64 =
378 (lambda unrestricted value : (family JSON) . (let unrestricted text = (aosMemberBytes b"v" value)
379 in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (naturalAnd (aosMemberIsString b"v" value) (aosIsU64Text text)))
380 (constructor AosValue AosU64 (aosDigitsValue text)))))
381
382def aosDecodeI64 =
383 (lambda unrestricted value : (family JSON) . (let unrestricted text = (aosMemberBytes b"v" value)
384 in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (naturalAnd (aosMemberIsString b"v" value) (aosIsI64Text text)))
385 (constructor AosValue AosI64 (aosHasMinus text) (aosDigitsValue (aosSignedDigits text))))))
386
387def aosDecodeBigInt =
388 (lambda unrestricted value : (family JSON) . (let unrestricted text = (aosMemberBytes b"v" value)
389 in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (naturalAnd (aosMemberIsString b"v" value) (aosCanonicalSigned text)))
390 (constructor AosValue AosBigInt (aosHasMinus text) (aosDigitsValue (aosSignedDigits text))))))
391
392def aosDecodeDecimal =
393 (lambda unrestricted value : (family JSON) .
394 (let unrestricted coefficient = (aosMemberBytes b"coefficient" value)
395 in (let unrestricted scale = (aosMemberBytes b"scale" value)
396 in (aosWhen
397 (naturalAnd (aosHasExactly3 b"t" b"coefficient" b"scale" value)
398 (naturalAnd (aosMemberIsString b"coefficient" value)
399 (naturalAnd (aosCanonicalSigned coefficient)
400 (naturalAnd (aosMemberIsString b"scale" value) (aosIsI64Text scale)))))
401 (constructor AosValue AosDecimal
402 (aosHasMinus coefficient) (aosDigitsValue (aosSignedDigits coefficient))
403 (aosHasMinus scale) (aosDigitsValue (aosSignedDigits scale)))))))
404
405-- a float's exact bit pattern: `width` lowercase hex digits
406def aosDecodeFloat =
407 (lambda unrestricted width : Nat . (lambda unrestricted value : (family JSON) .
408 (let unrestricted bits = (aosMemberBytes b"bits" value)
409 in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"bits" value) (naturalAnd (aosMemberIsString b"bits" value) (aosIsHexOfWidth width bits)))
410 (aosChoose (family AosValue) (naturalEqual width 8) (constructor AosValue AosF32 bits) (constructor AosValue AosF64 bits))))))
411
412def aosDecodeText =
413 (lambda unrestricted value : (family JSON) .
414 (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosMemberIsString b"v" value))
415 (constructor AosValue AosText (aosMemberBytes b"v" value))))
416
417def aosDecodeBytes =
418 (lambda unrestricted value : (family JSON) . (let unrestricted hex = (aosMemberBytes b"hex" value)
419 in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"hex" value) (naturalAnd (aosMemberIsString b"hex" value) (aosIsHexBytes hex)))
420 (constructor AosValue AosBytes hex))))
421
422def aosDecodeRef =
423 (lambda unrestricted value : (family JSON) .
424 (let unrestricted kind = (aosMemberBytes b"kind" value)
425 in (let unrestricted identity = (aosMemberBytes b"id" value)
426 in (aosWhen
427 (naturalAnd (aosHasExactly3 b"t" b"kind" b"id" value)
428 (naturalAnd (aosMemberIsString b"kind" value)
429 (naturalAnd (naturalNonzero (bytes-length kind))
430 (naturalAnd (aosMemberIsString b"id" value) (naturalNonzero (bytes-length identity))))))
431 (constructor AosValue AosRef kind identity)))))
432
433def aosDecodeNull =
434 (lambda unrestricted value : (family JSON) . (aosWhen (aosHasExactly1 b"t" value) (constructor AosValue AosNull)))
435
436def aosDecodeList =
437 (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) .
438 (lambda unrestricted value : (family JSON) . (let unrestricted inner = (aosMemberValue b"v" value)
439 in (aosChoose (family AosDecoded) (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosIsArray inner))
440 (aosDecodeItems decode inner) aosRejected))))
441
442def aosDecodeMap =
443 (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) .
444 (lambda unrestricted value : (family JSON) . (let unrestricted inner = (aosMemberValue b"v" value)
445 in (aosChoose (family AosDecoded) (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosIsObject inner))
446 (aosDecodeMembers decode inner) aosRejected))))
447
448-- One tagged value, its nested values decoded by `decode` (AOS-JSON-005):
449-- the tag chooses the decoder; an unknown tag is rejected.
450def aosDecodeTagged =
451 (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) .
452 (lambda unrestricted value : (family JSON) .
453 (let unrestricted tag = (aosMemberBytes b"t" value)
454 in (aosChoose (family AosDecoded) (naturalIsZero (aosMemberIsString b"t" value)) aosRejected
455 (aosChoose (family AosDecoded) (bytes-equal tag b"bool") (aosDecodeBool value)
456 (aosChoose (family AosDecoded) (bytes-equal tag b"u64") (aosDecodeU64 value)
457 (aosChoose (family AosDecoded) (bytes-equal tag b"i64") (aosDecodeI64 value)
458 (aosChoose (family AosDecoded) (bytes-equal tag b"bigint") (aosDecodeBigInt value)
459 (aosChoose (family AosDecoded) (bytes-equal tag b"decimal") (aosDecodeDecimal value)
460 (aosChoose (family AosDecoded) (bytes-equal tag b"f32") (aosDecodeFloat 8 value)
461 (aosChoose (family AosDecoded) (bytes-equal tag b"f64") (aosDecodeFloat 16 value)
462 (aosChoose (family AosDecoded) (bytes-equal tag b"text") (aosDecodeText value)
463 (aosChoose (family AosDecoded) (bytes-equal tag b"bytes") (aosDecodeBytes value)
464 (aosChoose (family AosDecoded) (bytes-equal tag b"ref") (aosDecodeRef value)
465 (aosChoose (family AosDecoded) (bytes-equal tag b"null") (aosDecodeNull value)
466 (aosChoose (family AosDecoded) (bytes-equal tag b"list") (aosDecodeList decode value)
467 (aosChoose (family AosDecoded) (bytes-equal tag b"map") (aosDecodeMap decode value)
468 aosRejected)))))))))))))))))
469
470-- The value decoder, its nesting bounded by `fuel` (the stream's declared
471-- depth limit bounds it first: a tagged level is two JSON levels).
472def aosDecodeWithFuel =
473 (lambda unrestricted fuel : Nat .
474 (nat-eliminate
475 (lambda unrestricted current : Nat . (pi unrestricted value : (family JSON) . (family AosDecoded)))
476 (lambda unrestricted value : (family JSON) . aosRejected)
477 (lambda unrestricted predecessor : Nat .
478 (lambda unrestricted inner : (pi unrestricted value : (family JSON) . (family AosDecoded)) .
479 (lambda unrestricted value : (family JSON) . (aosDecodeTagged inner value))))
480 fuel))
481
482def aosDecodeValue = (lambda unrestricted value : (family JSON) . (aosDecodeWithFuel 64 value))
483
484-- 1 when the JSON is a valid tagged value
485def aosIsValue =
486 (lambda unrestricted value : (family JSON) .
487 (eliminate AosDecoded (lambda unrestricted current : (family AosDecoded) . Nat) (aosDecodeValue value)
488 (branch AosDecodedValue decoded . 1)
489 (branch AosDecodeRejected . 0)))
490
491-- ---------------------------------------------------------------------------
492-- Availability (AOS-VAL-003, AOS-JSON-006)
493
494-- 1 when `state` names a non-present availability state
495def aosIsAbsenceState =
496 (lambda unrestricted state : Bytes .
497 (naturalOr (bytes-equal state b"not_recorded")
498 (naturalOr (bytes-equal state b"unsupported")
499 (naturalOr (bytes-equal state b"unavailable")
500 (naturalOr (bytes-equal state b"redacted")
501 (naturalOr (bytes-equal state b"expired")
502 (naturalOr (bytes-equal state b"invalid")
503 (bytes-equal state b"unknown"))))))))
504
505-- ---------------------------------------------------------------------------
506-- Encoding: a value as AOS-JSON/1 writes it
507
508def aosSigned =
509 (lambda unrestricted negative : Nat . (lambda unrestricted magnitude : Nat . (lambda unrestricted fuel : Nat .
510 (aosChoose Bytes negative
511 (bytes-append b"-" (naturalDecimalBytesWithin fuel magnitude))
512 (naturalDecimalBytesWithin fuel magnitude)))))
513
514def aosField =
515 (lambda unrestricted key : Bytes . (lambda unrestricted value : (family JSON) . (lambda unrestricted rest : (family JSON) .
516 (constructor JSON JSONObjectMember key value rest))))
517
518def aosObjectEnd : (family JSON) = (constructor JSON JSONObjectEnd)
519def aosJSONText = (lambda unrestricted text : Bytes . (constructor JSON JSONString text))
520
521-- the value's JSON tree (members in the order the bootstrap writer uses)
522def aosValueJSON =
523 (lambda unrestricted value : (family AosValue) .
524 (eliminate AosValue (lambda unrestricted current : (family AosValue) . (family JSON)) value
525 (branch AosBool flag .
526 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"bool") (aosField b"v" (constructor JSON JSONBoolean flag) aosObjectEnd))))
527 (branch AosU64 n .
528 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"u64") (aosField b"v" (aosJSONText (naturalDecimalBytesWithin 20 n)) aosObjectEnd))))
529 (branch AosI64 negative magnitude .
530 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"i64") (aosField b"v" (aosJSONText (aosSigned negative magnitude 20)) aosObjectEnd))))
531 (branch AosBigInt negative magnitude .
532 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"bigint") (aosField b"v" (aosJSONText (aosSigned negative magnitude 4096)) aosObjectEnd))))
533 (branch AosDecimal coefficientNegative coefficient scaleNegative scale .
534 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"decimal")
535 (aosField b"coefficient" (aosJSONText (aosSigned coefficientNegative coefficient 4096))
536 (aosField b"scale" (aosJSONText (aosSigned scaleNegative scale 20)) aosObjectEnd)))))
537 (branch AosF32 bits .
538 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"f32") (aosField b"bits" (aosJSONText bits) aosObjectEnd))))
539 (branch AosF64 bits .
540 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"f64") (aosField b"bits" (aosJSONText bits) aosObjectEnd))))
541 (branch AosText text .
542 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"text") (aosField b"v" (aosJSONText text) aosObjectEnd))))
543 (branch AosBytes hex .
544 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"bytes") (aosField b"hex" (aosJSONText hex) aosObjectEnd))))
545 (branch AosRef kind identity .
546 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"ref") (aosField b"kind" (aosJSONText kind) (aosField b"id" (aosJSONText identity) aosObjectEnd)))))
547 (branch AosNull .
548 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"null") aosObjectEnd)))
549 (branch AosList items itemsInduction .
550 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"list") (aosField b"v" (constructor JSON JSONArray itemsInduction) aosObjectEnd))))
551 (branch AosItemsEnd . (constructor JSON JSONArrayEnd))
552 (branch AosItemsNext head tail headInduction tailInduction . (constructor JSON JSONArrayNext headInduction tailInduction))
553 (branch AosMap members membersInduction .
554 (constructor JSON JSONObject (aosField b"t" (aosJSONText b"map") (aosField b"v" (constructor JSON JSONObject membersInduction) aosObjectEnd))))
555 (branch AosMembersEnd . (constructor JSON JSONObjectEnd))
556 (branch AosMembersNext key member tail memberInduction tailInduction . (constructor JSON JSONObjectMember key memberInduction tailInduction))))
557
558-- the value's AOS-JSON/1 bytes (b"" if the renderer refuses: it bounds
559-- its output)
560def aosEncodeValue =
561 (lambda unrestricted value : (family AosValue) .
562 (eliminate JSONRenderResult (lambda unrestricted current : (family JSONRenderResult) . Bytes) (renderJSON (aosValueJSON value))
563 (branch JSONRendered bytes . bytes)
564 (branch JSONRenderFailed error . b"")))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.