module Observe.Value import Data.UTF8 import Model.Word32 import Std.Byte import Std.Flag import Data.JSON import Data.JSONAccess import Data.JSONRender import Std.Natural -- AOS VALUES (docs/standards/AOS-1.0-draft-1.md §6, §24.2): the typed value -- a schema-governed payload slot holds, as AOS-JSON/1 writes it -- every -- integer a canonical decimal STRING (no JSON number, so no counter or tick -- ever passes through a float: AOS-VAL-002), a float as its exact bit -- pattern in lowercase hex, bytes as lowercase hex -- and the availability -- states a slot can be in instead of holding a value (AOS-VAL-003: zero is -- never "not measured"). -- -- This module is the semantic authority for what a valid tagged value is. -- The bootstrap tool's reader (tool/Aos.hs, `checkValue`) implements the -- same rules; scripts/ci/observability.sh holds the two to the same verdict -- on every fixture. Decoding is strict: a tagged value has EXACTLY the -- members its tag names -- an extra member is an error, not ignored. -- --------------------------------------------------------------------------- -- Bytes: digits, hex, identities family AosMember : Type 0 constructor AosMemberAbsent constructor AosMemberPresent field unrestricted aosMemberValue : (family JSON) end-family family AosValue : Type 0 constructor AosBool field unrestricted aosBoolFlag : Nat constructor AosU64 field unrestricted aosU64Value : Nat constructor AosI64 field unrestricted aosI64Negative : Nat field unrestricted aosI64Magnitude : Nat constructor AosBigInt field unrestricted aosBigIntNegative : Nat field unrestricted aosBigIntMagnitude : Nat constructor AosDecimal field unrestricted aosDecimalCoefficientNegative : Nat field unrestricted aosDecimalCoefficient : Nat field unrestricted aosDecimalScaleNegative : Nat field unrestricted aosDecimalScale : Nat constructor AosF32 field unrestricted aosF32Bits : Bytes constructor AosF64 field unrestricted aosF64Bits : Bytes constructor AosText field unrestricted aosTextBytes : Bytes constructor AosBytes field unrestricted aosBytesHex : Bytes constructor AosRef field unrestricted aosRefKind : Bytes field unrestricted aosRefIdentity : Bytes constructor AosNull constructor AosList recursive unrestricted aosListItems constructor AosItemsEnd constructor AosItemsNext recursive unrestricted aosItemsHead recursive unrestricted aosItemsTail constructor AosMap recursive unrestricted aosMapMembers constructor AosMembersEnd constructor AosMembersNext field unrestricted aosMembersKey : Bytes recursive unrestricted aosMembersValue recursive unrestricted aosMembersTail end-family family AosDecoded : Type 0 constructor AosDecodedValue field unrestricted aosDecodedValue : (family AosValue) constructor AosDecodeRejected end-family -- 1 when lo <= b <= hi def aosByteBetween = (lambda unrestricted b : Byte . (lambda unrestricted lo : Byte . (lambda unrestricted hi : Byte . (naturalAnd (naturalIsZero (byte-less-than b lo)) (naturalIsZero (byte-less-than hi b)))))) def aosIsDigitByte = (lambda unrestricted b : Byte . (aosByteBetween b (byte 48) (byte 57))) -- 0-9 and a-f: AOS-JSON/1 hex is lowercase only def aosIsLowerHexByte = (lambda unrestricted b : Byte . (naturalOr (aosIsDigitByte b) (aosByteBetween b (byte 97) (byte 102)))) def aosAllBytes = (lambda unrestricted predicate : (pi unrestricted b : Byte . Nat) . (lambda unrestricted input : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . Nat) 1 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat . (naturalAnd (predicate head) induction)))) input))) def aosAnyByte = (lambda unrestricted predicate : (pi unrestricted b : Byte . Nat) . (lambda unrestricted input : Bytes . (bytes-eliminate (lambda unrestricted current : Bytes . Nat) 0 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : Nat . (naturalOr (predicate head) induction)))) input))) -- the value of a string of decimal digits, most significant first (a left -- fold: the accumulator is threaded through the right fold's functions) def aosDigitsValue = (lambda unrestricted input : Bytes . (app (bytes-eliminate (lambda unrestricted current : Bytes . (pi unrestricted acc : Nat . Nat)) (lambda unrestricted acc : Nat . acc) (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes . (lambda unrestricted induction : (pi unrestricted acc : Nat . Nat) . (lambda unrestricted acc : Nat . (induction (naturalAdd (naturalMultiply acc 10) (naturalSaturatingSubtract (byte-to-nat head) 48))))))) input) 0)) -- AOS-JSON-004: `0`, or a nonzero digit then digits; at most 4096 digits def aosCanonicalUnsigned = (lambda unrestricted input : Bytes . (naturalAnd (naturalNonzero (bytes-length input)) (naturalAnd (naturalLessOrEqual (bytes-length input) 4096) (naturalAnd (aosAllBytes aosIsDigitByte input) (naturalOr (naturalEqual (bytes-length input) 1) (naturalIsZero (byte-equal (bytes-head input) (byte 48)))))))) def aosU64Maximum : Nat = 18446744073709551615 def aosI64Maximum : Nat = 9223372036854775807 def aosI64MinimumMagnitude : Nat = 9223372036854775808 def aosIsU64Text = (lambda unrestricted input : Bytes . (naturalAnd (aosCanonicalUnsigned input) (naturalAnd (naturalLessOrEqual (bytes-length input) 20) (naturalLessOrEqual (aosDigitsValue input) aosU64Maximum)))) def aosHasMinus = (lambda unrestricted input : Bytes . (naturalAnd (naturalNonzero (bytes-length input)) (byte-equal (bytes-head input) (byte 45)))) -- the digits of a signed integer, its sign removed def aosSignedDigits = (lambda unrestricted input : Bytes . (nat-eliminate (lambda unrestricted current : Nat . Bytes) input (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Bytes . (bytes-tail input))) (aosHasMinus input))) -- an optional '-' then a canonical unsigned; "-0" is refused def aosCanonicalSigned = (lambda unrestricted input : Bytes . (naturalAnd (aosCanonicalUnsigned (aosSignedDigits input)) (naturalOr (naturalIsZero (aosHasMinus input)) (naturalNonzero (aosDigitsValue (aosSignedDigits input)))))) def aosIsI64Text = (lambda unrestricted input : Bytes . (naturalAnd (aosCanonicalSigned input) (naturalAnd (naturalLessOrEqual (bytes-length (aosSignedDigits input)) 19) (naturalLessOrEqual (aosDigitsValue (aosSignedDigits input)) (naturalSelect (aosHasMinus input) aosI64MinimumMagnitude aosI64Maximum))))) -- exactly `width` lowercase hex digits def aosIsHexOfWidth = (lambda unrestricted width : Nat . (lambda unrestricted input : Bytes . (naturalAnd (naturalEqual (bytes-length input) width) (aosAllBytes aosIsLowerHexByte input)))) -- lowercase hex of even length (bytes) def aosIsHexBytes = (lambda unrestricted input : Bytes . (naturalAnd (aosAllBytes aosIsLowerHexByte input) (naturalIsZero (naturalModuloUnchecked (bytes-length input) 2)))) -- AOS-ID-003: 32 lowercase hex digits, not all zero def aosIsIdentity = (lambda unrestricted input : Bytes . (naturalAnd (aosIsHexOfWidth 32 input) (aosAnyByte (lambda unrestricted b : Byte . (naturalIsZero (byte-equal b (byte 48)))) input))) -- --------------------------------------------------------------------------- -- JSON navigation -- an object's member by name (absent when the value is not an object) def aosMember = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (eliminate JSONValueAccessResult (lambda unrestricted current : (family JSONValueAccessResult) . (family AosMember)) (objectLookup name value) (branch JSONValueAccessSucceeded found . (constructor AosMember AosMemberPresent found)) (branch JSONValueAccessFailed error . (constructor AosMember AosMemberAbsent))))) -- the kind of a document value: 1 object, 2 array, 3 string, 4 number, -- 5 boolean, 6 null (0: a member or element chain, never a document value) def aosKind = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value (branch JSONObject members membersInduction . 1) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . 0) (branch JSONArray values valuesInduction . 2) (branch JSONArrayEnd . 0) (branch JSONArrayNext head tail headInduction tailInduction . 0) (branch JSONString text . 3) (branch JSONNumber digits . 4) (branch JSONBoolean flag . 5) (branch JSONNull . 6))) def aosIsObject = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 1)) def aosIsArray = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 2)) def aosIsString = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 3)) def aosIsBoolean = (lambda unrestricted value : (family JSON) . (naturalEqual (aosKind value) 5)) -- a string's bytes (empty for anything else: test `aosIsString` first) def aosStringBytes = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Bytes) value (branch JSONObject members membersInduction . b"") (branch JSONObjectEnd . b"") (branch JSONObjectMember key member tail memberInduction tailInduction . b"") (branch JSONArray values valuesInduction . b"") (branch JSONArrayEnd . b"") (branch JSONArrayNext head tail headInduction tailInduction . b"") (branch JSONString text . text) (branch JSONNumber digits . b"") (branch JSONBoolean flag . b"") (branch JSONNull . b""))) def aosBooleanFlag = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value (branch JSONObject members membersInduction . 0) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . 0) (branch JSONArray values valuesInduction . 0) (branch JSONArrayEnd . 0) (branch JSONArrayNext head tail headInduction tailInduction . 0) (branch JSONString text . 0) (branch JSONNumber digits . 0) (branch JSONBoolean flag . flag) (branch JSONNull . 0))) -- an object's number of members (0 for anything else: test first) def aosObjectSize = (lambda unrestricted value : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . Nat) value (branch JSONObject members membersInduction . membersInduction) (branch JSONObjectEnd . 0) (branch JSONObjectMember key member tail memberInduction tailInduction . (succ tailInduction)) (branch JSONArray values valuesInduction . 0) (branch JSONArrayEnd . 0) (branch JSONArrayNext head tail headInduction tailInduction . 0) (branch JSONString text . 0) (branch JSONNumber digits . 0) (branch JSONBoolean flag . 0) (branch JSONNull . 0))) def aosHas = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (eliminate AosMember (lambda unrestricted current : (family AosMember) . Nat) (aosMember name value) (branch AosMemberAbsent . 0) (branch AosMemberPresent found . 1)))) -- the member's string bytes (b"" when absent or not a string) def aosMemberBytes = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (eliminate AosMember (lambda unrestricted current : (family AosMember) . Bytes) (aosMember name value) (branch AosMemberAbsent . b"") (branch AosMemberPresent found . (aosStringBytes found))))) -- 1 when the member is present and a string def aosMemberIsString = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (eliminate AosMember (lambda unrestricted current : (family AosMember) . Nat) (aosMember name value) (branch AosMemberAbsent . 0) (branch AosMemberPresent found . (aosIsString found))))) -- an object with exactly these member names (no duplicates exist after the -- strict parse, so the count and the presence of each decide it) def aosHasExactly1 = (lambda unrestricted a : Bytes . (lambda unrestricted value : (family JSON) . (naturalAnd (aosIsObject value) (naturalAnd (naturalEqual (aosObjectSize value) 1) (aosHas a value))))) def aosHasExactly2 = (lambda unrestricted a : Bytes . (lambda unrestricted b : Bytes . (lambda unrestricted value : (family JSON) . (naturalAnd (aosIsObject value) (naturalAnd (naturalEqual (aosObjectSize value) 2) (naturalAnd (aosHas a value) (aosHas b value))))))) def aosHasExactly3 = (lambda unrestricted a : Bytes . (lambda unrestricted b : Bytes . (lambda unrestricted c : Bytes . (lambda unrestricted value : (family JSON) . (naturalAnd (aosIsObject value) (naturalAnd (naturalEqual (aosObjectSize value) 3) (naturalAnd (aosHas a value) (naturalAnd (aosHas b value) (aosHas c value))))))))) -- a verdict code: 0 when `first` is 0 (passed), else `first` -- the next -- check is not evaluated once one has failed def aosThen = (lambda unrestricted first : Nat . (lambda unrestricted next : Nat . (naturalSelect first first next))) -- `whenTrue` when the flag is nonzero, else `whenFalse`, at any type (the -- one not chosen is not evaluated) def aosChoose = (lambda erased result : Type 0 . (lambda unrestricted condition : Nat . (lambda unrestricted whenTrue : result . (lambda unrestricted whenFalse : result . (nat-eliminate (lambda unrestricted current : Nat . result) whenFalse (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : result . whenTrue)) condition))))) -- --------------------------------------------------------------------------- -- Typed values def aosRejected : (family AosDecoded) = (constructor AosDecoded AosDecodeRejected) def aosDecodedAs = (lambda unrestricted value : (family AosValue) . (constructor AosDecoded AosDecodedValue value)) def aosBind = (lambda unrestricted decoded : (family AosDecoded) . (lambda unrestricted continue : (pi unrestricted value : (family AosValue) . (family AosDecoded)) . (eliminate AosDecoded (lambda unrestricted current : (family AosDecoded) . (family AosDecoded)) decoded (branch AosDecodedValue value . (continue value)) (branch AosDecodeRejected . aosRejected)))) -- decode when `valid`, else reject def aosWhen = (lambda unrestricted valid : Nat . (lambda unrestricted value : (family AosValue) . (aosChoose (family AosDecoded) valid (aosDecodedAs value) aosRejected))) -- a list's elements, each by `decode` (the decoder with one less fuel) def aosDecodeItems = (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) . (lambda unrestricted array : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . (family AosDecoded)) array (branch JSONObject members membersInduction . aosRejected) (branch JSONObjectEnd . aosRejected) (branch JSONObjectMember key member tail memberInduction tailInduction . aosRejected) (branch JSONArray values valuesInduction . (aosBind valuesInduction (lambda unrestricted items : (family AosValue) . (aosDecodedAs (constructor AosValue AosList items))))) (branch JSONArrayEnd . (aosDecodedAs (constructor AosValue AosItemsEnd))) (branch JSONArrayNext head tail headInduction tailInduction . (aosBind (decode head) (lambda unrestricted first : (family AosValue) . (aosBind tailInduction (lambda unrestricted rest : (family AosValue) . (aosDecodedAs (constructor AosValue AosItemsNext first rest))))))) (branch JSONString text . aosRejected) (branch JSONNumber digits . aosRejected) (branch JSONBoolean flag . aosRejected) (branch JSONNull . aosRejected)))) -- a map's members, each value by `decode` def aosDecodeMembers = (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) . (lambda unrestricted object : (family JSON) . (eliminate JSON (lambda unrestricted current : (family JSON) . (family AosDecoded)) object (branch JSONObject members membersInduction . (aosBind membersInduction (lambda unrestricted chain : (family AosValue) . (aosDecodedAs (constructor AosValue AosMap chain))))) (branch JSONObjectEnd . (aosDecodedAs (constructor AosValue AosMembersEnd))) (branch JSONObjectMember key member tail memberInduction tailInduction . (aosBind (decode member) (lambda unrestricted first : (family AosValue) . (aosBind tailInduction (lambda unrestricted rest : (family AosValue) . (aosDecodedAs (constructor AosValue AosMembersNext key first rest))))))) (branch JSONArray values valuesInduction . aosRejected) (branch JSONArrayEnd . aosRejected) (branch JSONArrayNext head tail headInduction tailInduction . aosRejected) (branch JSONString text . aosRejected) (branch JSONNumber digits . aosRejected) (branch JSONBoolean flag . aosRejected) (branch JSONNull . aosRejected)))) -- the member's JSON value (JSONNull when absent: test with aosHas first) def aosMemberValue = (lambda unrestricted name : Bytes . (lambda unrestricted value : (family JSON) . (eliminate AosMember (lambda unrestricted current : (family AosMember) . (family JSON)) (aosMember name value) (branch AosMemberAbsent . (constructor JSON JSONNull)) (branch AosMemberPresent found . found)))) -- Each tag's decoder: the value's exact member set, then its content. def aosDecodeBool = (lambda unrestricted value : (family JSON) . (let unrestricted inner = (aosMemberValue b"v" value) in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosIsBoolean inner)) (constructor AosValue AosBool (aosBooleanFlag inner))))) def aosDecodeU64 = (lambda unrestricted value : (family JSON) . (let unrestricted text = (aosMemberBytes b"v" value) in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (naturalAnd (aosMemberIsString b"v" value) (aosIsU64Text text))) (constructor AosValue AosU64 (aosDigitsValue text))))) def aosDecodeI64 = (lambda unrestricted value : (family JSON) . (let unrestricted text = (aosMemberBytes b"v" value) in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (naturalAnd (aosMemberIsString b"v" value) (aosIsI64Text text))) (constructor AosValue AosI64 (aosHasMinus text) (aosDigitsValue (aosSignedDigits text)))))) def aosDecodeBigInt = (lambda unrestricted value : (family JSON) . (let unrestricted text = (aosMemberBytes b"v" value) in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (naturalAnd (aosMemberIsString b"v" value) (aosCanonicalSigned text))) (constructor AosValue AosBigInt (aosHasMinus text) (aosDigitsValue (aosSignedDigits text)))))) def aosDecodeDecimal = (lambda unrestricted value : (family JSON) . (let unrestricted coefficient = (aosMemberBytes b"coefficient" value) in (let unrestricted scale = (aosMemberBytes b"scale" value) in (aosWhen (naturalAnd (aosHasExactly3 b"t" b"coefficient" b"scale" value) (naturalAnd (aosMemberIsString b"coefficient" value) (naturalAnd (aosCanonicalSigned coefficient) (naturalAnd (aosMemberIsString b"scale" value) (aosIsI64Text scale))))) (constructor AosValue AosDecimal (aosHasMinus coefficient) (aosDigitsValue (aosSignedDigits coefficient)) (aosHasMinus scale) (aosDigitsValue (aosSignedDigits scale))))))) -- a float's exact bit pattern: `width` lowercase hex digits def aosDecodeFloat = (lambda unrestricted width : Nat . (lambda unrestricted value : (family JSON) . (let unrestricted bits = (aosMemberBytes b"bits" value) in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"bits" value) (naturalAnd (aosMemberIsString b"bits" value) (aosIsHexOfWidth width bits))) (aosChoose (family AosValue) (naturalEqual width 8) (constructor AosValue AosF32 bits) (constructor AosValue AosF64 bits)))))) def aosDecodeText = (lambda unrestricted value : (family JSON) . (aosWhen (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosMemberIsString b"v" value)) (constructor AosValue AosText (aosMemberBytes b"v" value)))) def aosDecodeBytes = (lambda unrestricted value : (family JSON) . (let unrestricted hex = (aosMemberBytes b"hex" value) in (aosWhen (naturalAnd (aosHasExactly2 b"t" b"hex" value) (naturalAnd (aosMemberIsString b"hex" value) (aosIsHexBytes hex))) (constructor AosValue AosBytes hex)))) def aosDecodeRef = (lambda unrestricted value : (family JSON) . (let unrestricted kind = (aosMemberBytes b"kind" value) in (let unrestricted identity = (aosMemberBytes b"id" value) in (aosWhen (naturalAnd (aosHasExactly3 b"t" b"kind" b"id" value) (naturalAnd (aosMemberIsString b"kind" value) (naturalAnd (naturalNonzero (bytes-length kind)) (naturalAnd (aosMemberIsString b"id" value) (naturalNonzero (bytes-length identity)))))) (constructor AosValue AosRef kind identity))))) def aosDecodeNull = (lambda unrestricted value : (family JSON) . (aosWhen (aosHasExactly1 b"t" value) (constructor AosValue AosNull))) def aosDecodeList = (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) . (lambda unrestricted value : (family JSON) . (let unrestricted inner = (aosMemberValue b"v" value) in (aosChoose (family AosDecoded) (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosIsArray inner)) (aosDecodeItems decode inner) aosRejected)))) def aosDecodeMap = (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) . (lambda unrestricted value : (family JSON) . (let unrestricted inner = (aosMemberValue b"v" value) in (aosChoose (family AosDecoded) (naturalAnd (aosHasExactly2 b"t" b"v" value) (aosIsObject inner)) (aosDecodeMembers decode inner) aosRejected)))) -- One tagged value, its nested values decoded by `decode` (AOS-JSON-005): -- the tag chooses the decoder; an unknown tag is rejected. def aosDecodeTagged = (lambda unrestricted decode : (pi unrestricted value : (family JSON) . (family AosDecoded)) . (lambda unrestricted value : (family JSON) . (let unrestricted tag = (aosMemberBytes b"t" value) in (aosChoose (family AosDecoded) (naturalIsZero (aosMemberIsString b"t" value)) aosRejected (aosChoose (family AosDecoded) (bytes-equal tag b"bool") (aosDecodeBool value) (aosChoose (family AosDecoded) (bytes-equal tag b"u64") (aosDecodeU64 value) (aosChoose (family AosDecoded) (bytes-equal tag b"i64") (aosDecodeI64 value) (aosChoose (family AosDecoded) (bytes-equal tag b"bigint") (aosDecodeBigInt value) (aosChoose (family AosDecoded) (bytes-equal tag b"decimal") (aosDecodeDecimal value) (aosChoose (family AosDecoded) (bytes-equal tag b"f32") (aosDecodeFloat 8 value) (aosChoose (family AosDecoded) (bytes-equal tag b"f64") (aosDecodeFloat 16 value) (aosChoose (family AosDecoded) (bytes-equal tag b"text") (aosDecodeText value) (aosChoose (family AosDecoded) (bytes-equal tag b"bytes") (aosDecodeBytes value) (aosChoose (family AosDecoded) (bytes-equal tag b"ref") (aosDecodeRef value) (aosChoose (family AosDecoded) (bytes-equal tag b"null") (aosDecodeNull value) (aosChoose (family AosDecoded) (bytes-equal tag b"list") (aosDecodeList decode value) (aosChoose (family AosDecoded) (bytes-equal tag b"map") (aosDecodeMap decode value) aosRejected))))))))))))))))) -- The value decoder, its nesting bounded by `fuel` (the stream's declared -- depth limit bounds it first: a tagged level is two JSON levels). def aosDecodeWithFuel = (lambda unrestricted fuel : Nat . (nat-eliminate (lambda unrestricted current : Nat . (pi unrestricted value : (family JSON) . (family AosDecoded))) (lambda unrestricted value : (family JSON) . aosRejected) (lambda unrestricted predecessor : Nat . (lambda unrestricted inner : (pi unrestricted value : (family JSON) . (family AosDecoded)) . (lambda unrestricted value : (family JSON) . (aosDecodeTagged inner value)))) fuel)) def aosDecodeValue = (lambda unrestricted value : (family JSON) . (aosDecodeWithFuel 64 value)) -- 1 when the JSON is a valid tagged value def aosIsValue = (lambda unrestricted value : (family JSON) . (eliminate AosDecoded (lambda unrestricted current : (family AosDecoded) . Nat) (aosDecodeValue value) (branch AosDecodedValue decoded . 1) (branch AosDecodeRejected . 0))) -- --------------------------------------------------------------------------- -- Availability (AOS-VAL-003, AOS-JSON-006) -- 1 when `state` names a non-present availability state def aosIsAbsenceState = (lambda unrestricted state : Bytes . (naturalOr (bytes-equal state b"not_recorded") (naturalOr (bytes-equal state b"unsupported") (naturalOr (bytes-equal state b"unavailable") (naturalOr (bytes-equal state b"redacted") (naturalOr (bytes-equal state b"expired") (naturalOr (bytes-equal state b"invalid") (bytes-equal state b"unknown")))))))) -- --------------------------------------------------------------------------- -- Encoding: a value as AOS-JSON/1 writes it def aosSigned = (lambda unrestricted negative : Nat . (lambda unrestricted magnitude : Nat . (lambda unrestricted fuel : Nat . (aosChoose Bytes negative (bytes-append b"-" (naturalDecimalBytesWithin fuel magnitude)) (naturalDecimalBytesWithin fuel magnitude))))) def aosField = (lambda unrestricted key : Bytes . (lambda unrestricted value : (family JSON) . (lambda unrestricted rest : (family JSON) . (constructor JSON JSONObjectMember key value rest)))) def aosObjectEnd : (family JSON) = (constructor JSON JSONObjectEnd) def aosJSONText = (lambda unrestricted text : Bytes . (constructor JSON JSONString text)) -- the value's JSON tree (members in the order the bootstrap writer uses) def aosValueJSON = (lambda unrestricted value : (family AosValue) . (eliminate AosValue (lambda unrestricted current : (family AosValue) . (family JSON)) value (branch AosBool flag . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"bool") (aosField b"v" (constructor JSON JSONBoolean flag) aosObjectEnd)))) (branch AosU64 n . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"u64") (aosField b"v" (aosJSONText (naturalDecimalBytesWithin 20 n)) aosObjectEnd)))) (branch AosI64 negative magnitude . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"i64") (aosField b"v" (aosJSONText (aosSigned negative magnitude 20)) aosObjectEnd)))) (branch AosBigInt negative magnitude . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"bigint") (aosField b"v" (aosJSONText (aosSigned negative magnitude 4096)) aosObjectEnd)))) (branch AosDecimal coefficientNegative coefficient scaleNegative scale . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"decimal") (aosField b"coefficient" (aosJSONText (aosSigned coefficientNegative coefficient 4096)) (aosField b"scale" (aosJSONText (aosSigned scaleNegative scale 20)) aosObjectEnd))))) (branch AosF32 bits . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"f32") (aosField b"bits" (aosJSONText bits) aosObjectEnd)))) (branch AosF64 bits . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"f64") (aosField b"bits" (aosJSONText bits) aosObjectEnd)))) (branch AosText text . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"text") (aosField b"v" (aosJSONText text) aosObjectEnd)))) (branch AosBytes hex . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"bytes") (aosField b"hex" (aosJSONText hex) aosObjectEnd)))) (branch AosRef kind identity . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"ref") (aosField b"kind" (aosJSONText kind) (aosField b"id" (aosJSONText identity) aosObjectEnd))))) (branch AosNull . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"null") aosObjectEnd))) (branch AosList items itemsInduction . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"list") (aosField b"v" (constructor JSON JSONArray itemsInduction) aosObjectEnd)))) (branch AosItemsEnd . (constructor JSON JSONArrayEnd)) (branch AosItemsNext head tail headInduction tailInduction . (constructor JSON JSONArrayNext headInduction tailInduction)) (branch AosMap members membersInduction . (constructor JSON JSONObject (aosField b"t" (aosJSONText b"map") (aosField b"v" (constructor JSON JSONObject membersInduction) aosObjectEnd)))) (branch AosMembersEnd . (constructor JSON JSONObjectEnd)) (branch AosMembersNext key member tail memberInduction tailInduction . (constructor JSON JSONObjectMember key memberInduction tailInduction)))) -- the value's AOS-JSON/1 bytes (b"" if the renderer refuses: it bounds -- its output) def aosEncodeValue = (lambda unrestricted value : (family AosValue) . (eliminate JSONRenderResult (lambda unrestricted current : (family JSONRenderResult) . Bytes) (renderJSON (aosValueJSON value)) (branch JSONRendered bytes . bytes) (branch JSONRenderFailed error . b"")))