A Javascript `Object` is primarily a mapping from string to values, and we can use them exactly as such. However, objects can also be used as an intermediary representation for encoding data from and to JSON. This module therefore provides additional functionality: A linear `LinObject` data type for encoding nested datastructure into an intermediary object representation, and an immutable `IObject` data type, mainly for decoding data, but also as an efficient means for having an immutable string to data mapping.
data Object : Typerecord LinObject : TypeObjects, mutable in a linear context. Useful for
efficient, non-monadic encoding of Idris2 values,
for instance to be used in an FFI call to an external
function, or when encoding Idris2 values to JSON through
the Javascript `JSON.stringify` function.
MkLinObject : Object -> LinObjectnewObj : (1 _ : ((1 _ : LinObject) -> a)) -> athaw : (1 _ : LinObject) -> IO Objectlset : (1 _ : LinObject) -> String -> a -> LinObjectlget : (1 _ : LinObject) -> String -> Res AnyPtr (const LinObject)record IObject : Typefreeze : (1 _ : LinObject) -> IObjectget : SafeCast a => IObject -> String -> Maybe adata Value : Typestringify : Value -> Stringobj : (1 _ : LinObject) -> ValuelsetVal : (1 _ : LinObject) -> String -> Value -> LinObjectwithPairs : List (String, Value) -> ((1 _ : LinObject) -> a) -> apairs : List (String, Value) -> Valuevals : List Value -> Valueparse : String -> Either JSErr ValueparseMaybe : String -> Maybe ValuegetObject : Value -> Maybe IObjectgetBool : Value -> Maybe BoolgetStr : Value -> Maybe StringgetNum : Value -> Maybe DoublegetArray : Value -> Maybe (IArray Value)valueAt : IObject -> String -> Maybe Value