0 | ||| A Javascript `Object` is primarily a mapping from string
  1 | ||| to values, and we can use them exactly as such. However,
  2 | ||| objects can also be used as an intermediary representation
  3 | ||| for encoding data from and to JSON.
  4 | |||
  5 | ||| This module therefore provides additional functionality:
  6 | |||
  7 | ||| A linear `LinObject` data type for encoding nested datastructure
  8 | ||| into an intermediary object representation, and an immutable
  9 | ||| `IObject` data type, mainly for decoding data, but also as an efficient
 10 | ||| means for having an immutable string to data mapping.
 11 | module JS.Object
 12 |
 13 | import JS.Any
 14 | import JS.Array
 15 | import JS.Boolean
 16 | import JS.Inheritance
 17 | import JS.Marshall
 18 | import JS.Nullable
 19 | import JS.Util
 20 |
 21 | %default total
 22 |
 23 | export
 24 | data Object : Type where [external]
 25 |
 26 | export
 27 | ToFFI Object Object where toFFI = id
 28 |
 29 | export
 30 | FromFFI Object Object where fromFFI = Just
 31 |
 32 | public export
 33 | JSType Object where
 34 |   parents = []
 35 |   mixins = []
 36 |
 37 | --------------------------------------------------------------------------------
 38 | --          Linear Objects
 39 | --------------------------------------------------------------------------------
 40 |
 41 | %foreign "javascript:lambda:() => {return {}}"
 42 | prim__new : () -> Object
 43 |
 44 | %foreign "javascript:lambda:(o,str) => o[str]"
 45 | prim__get : Object -> String -> AnyPtr
 46 |
 47 | %foreign "javascript:lambda:(u,o,str,v) => { o[str] = v; return o }"
 48 | prim__set : forall a . Object -> String -> a -> Object
 49 |
 50 | %foreign "javascript:lambda:(u,o) => JSON.stringify(o)"
 51 | prim__stringify : forall a . a -> String
 52 |
 53 | %foreign "javascript:lambda:s => JSON.parse(s)"
 54 | prim__parse : String -> AnyPtr
 55 |
 56 | ||| Objects, mutable in a linear context. Useful for
 57 | ||| efficient, non-monadic encoding of Idris2 values,
 58 | ||| for instance to be used in an FFI call to an external
 59 | ||| function, or when encoding Idris2 values to JSON through
 60 | ||| the Javascript `JSON.stringify` function.
 61 | export
 62 | record LinObject where
 63 |   constructor MkLinObject
 64 |   obj : Object
 65 |
 66 | export
 67 | newObj : (1 f : (1 _ : LinObject) -> a) -> a
 68 | newObj f = f (MkLinObject (prim__new ()))
 69 |
 70 | export
 71 | thaw : (1 _ : LinObject) -> IO Object
 72 | thaw (MkLinObject obj) = pure obj
 73 |
 74 | export
 75 | lset : (1 _ : LinObject) -> (fld : String) -> a -> LinObject
 76 | lset (MkLinObject o) f a = MkLinObject $ prim__set o f a
 77 |
 78 | export
 79 | lget : (1 _ : LinObject) -> (fld : String) -> Res AnyPtr (const $ LinObject)
 80 | lget (MkLinObject obj) fld = prim__get obj fld # MkLinObject obj
 81 |
 82 | --------------------------------------------------------------------------------
 83 | --          Immutable Objects
 84 | --------------------------------------------------------------------------------
 85 |
 86 | export
 87 | record IObject where
 88 |   constructor MkIObject
 89 |   obj : Object
 90 |
 91 | export
 92 | freeze : (1 _ : LinObject) -> IObject
 93 | freeze (MkLinObject obj) = MkIObject obj
 94 |
 95 | export
 96 | get : SafeCast a => IObject -> String -> Maybe a
 97 | get (MkIObject obj) str = safeCast $ prim__get obj str
 98 |
 99 | --------------------------------------------------------------------------------
100 | --          JSON Values
101 | --------------------------------------------------------------------------------
102 |
103 | public export
104 | data Value : Type where
105 |   Arr     : IArray Value -> Value
106 |   Boolean : Bool         -> Value
107 |   Null    : Value
108 |   Num     : Double       -> Value
109 |   Obj     : IObject      -> Value
110 |   Str     : String       -> Value
111 |
112 | toAny : Value -> Any
113 | toAny (Obj     x) = MkAny x
114 | toAny (Boolean x) = MkAny $ toFFI x
115 | toAny (Arr     x) = MkAny $ assert_total (map toAny x)
116 | toAny (Str     x) = MkAny x
117 | toAny (Num     x) = MkAny x
118 | toAny Null        = MkAny (null {a = ()})
119 |
120 | --------------------------------------------------------------------------------
121 | --          JSON Encoding
122 | --------------------------------------------------------------------------------
123 |
124 | export
125 | stringify : Value -> String
126 | stringify = prim__stringify . toFFI . toAny
127 |
128 | export
129 | obj : (1 _ : LinObject) -> Value
130 | obj (MkLinObject o) = Obj $ MkIObject o
131 |
132 | export
133 | lsetVal : (1 _ : LinObject) -> (fld : String) -> Value -> LinObject
134 | lsetVal o f v = lset o f (toFFI $ toAny v)
135 |
136 | export
137 | withPairs : List (String,Value) -> ((1 _ : LinObject) -> a) -> a
138 | withPairs ps f = newObj (run ps)
139 |
140 |   where
141 |     run : List (String,Value) -> (1 _ : LinObject) -> a
142 |     run []            o = f o
143 |     run ((s,v) :: ps) o = run ps (lsetVal o s v)
144 |
145 | export
146 | pairs : List (String,Value) -> Value
147 | pairs ps = withPairs ps obj
148 |
149 | export
150 | vals : List Value -> Value
151 | vals = Arr . fromList
152 |
153 | --------------------------------------------------------------------------------
154 | --          JSON decoding
155 | --------------------------------------------------------------------------------
156 |
157 | toVal : Any -> Maybe Value
158 | toVal (MkAny ptr) =
159 |       (Str <$> safeCast ptr)
160 |   <|> (Boolean <$> (safeCast ptr >>= fromFFI))
161 |   <|> (if isArray ptr then array ptr else Nothing)
162 |   <|> (if isNull ptr then Just Null else Nothing)
163 |   <|> (Num <$> safeCast ptr)
164 |   <|> (Obj . MkIObject <$> unsafeCastOnTypeof "object" ptr)
165 |
166 |   where
167 |     array : a -> Maybe Value
168 |     array a =
169 |       let arr := the (IArray Any) (believe_me a)
170 |        in assert_total $ Arr <$> traverse toVal arr
171 |
172 | export
173 | parse : String -> Either JSErr Value
174 | parse s = do
175 |   ptr <- try prim__parse s
176 |   maybe
177 |     (Left $ Caught #"Unable to decode JSON: \#{s}"#)
178 |     Right
179 |    (toVal (MkAny ptr))
180 |
181 | export
182 | parseMaybe : String -> Maybe Value
183 | parseMaybe = either (const Nothing) Just . parse
184 |
185 | export
186 | getObject : Value -> Maybe IObject
187 | getObject (Obj x) = Just x
188 | getObject _       = Nothing
189 |
190 | export
191 | getBool : Value -> Maybe Bool
192 | getBool (Boolean x) = Just x
193 | getBool _       = Nothing
194 |
195 | export
196 | getStr : Value -> Maybe String
197 | getStr (Str x) = Just x
198 | getStr _       = Nothing
199 |
200 | export
201 | getNum : Value -> Maybe Double
202 | getNum (Num x) = Just x
203 | getNum _       = Nothing
204 |
205 | export
206 | getArray : Value -> Maybe (IArray Value)
207 | getArray (Arr x) = Just x
208 | getArray _       = Nothing
209 |
210 | export
211 | valueAt : IObject -> String -> Maybe Value
212 | valueAt (MkIObject obj) = toVal . MkAny . prim__get obj
213 |