Idris2Doc : JS.Marshall

JS.Marshall

(source)
Definitions
interface ToFFI : Type -> Type -> Type
  Interface supporting the use of a value as an
  argument in a foreign function call.
  
  Implementations for primitives and external type should be
  done using `believe_me`, as they are alredy in the correct
  representation. Idris2 types should be converted to primitives
  or external constants first.

  Parameters: a, ffiRepr
Methods:
  
toFFI : a -> ffiRepr

Implementations:
  
ToFFI ByteString ByteString
  
ToFFI JSInt64 JSInt64
  
ToFFI JSBits64 JSBits64
  
ToFFI Any AnyPtr
  
ToFFI ArrayBuffer ArrayBuffer
  
ToFFI UInt8ClampedArray UInt8ClampedArray
  
ToFFI UInt8Array UInt8Array
  
ToFFI UInt16Array UInt16Array
  
ToFFI UInt32Array UInt32Array
  
ToFFI Int8Array Int8Array
  
ToFFI Int16Array Int16Array
  
ToFFI Int32Array Int32Array
  
ToFFI Float32Array Float32Array
  
ToFFI Float64Array Float64Array
  
ToFFI DataView DataView
  
ToFFI (Array a) (Array a)
  
ToFFI a b => ToFFI (List a) (IO (Array b))
  
ToFFI Bool Boolean
  
ToFFI Object Object
  
ToFFI (Promise a) (Promise a)
  
ToFFI (Record a b) (Record a b)
  
ToFFI a b => ToFFI (Maybe a) (Nullable b)
  
ToFFI Undefined Undefined
  
ToFFI a b => ToFFI (Optional a) (UndefOr b)
  
ToFFI AnyPtr AnyPtr
  
ToFFI Bits8 Bits8
  
ToFFI Bits16 Bits16
  
ToFFI Bits32 Bits32
  
ToFFI Bits64 Bits64
  
ToFFI Int8 Int8
  
ToFFI Int16 Int16
  
ToFFI Int32 Int32
  
ToFFI Int64 Int64
  
ToFFI Int Int
  
ToFFI Char Char
  
ToFFI Integer Integer
  
ToFFI Double Double
  
ToFFI String String
  
ToFFI WindowProxy WindowProxy
  
NPP ToFFI [a, b] [m, n] => ToFFI (HSum [a, b]) (Union2 m n)
  
ToFFI (Union2 a b) (Union2 a b)
  
NPP ToFFI [a, b, c] [m, n, o] => ToFFI (HSum [a, b, c]) (Union3 m n o)
  
ToFFI (Union3 a b c) (Union3 a b c)
  
NPP ToFFI [a, b, c, d] [m, n, o, p] => ToFFI (HSum [a, b, c, d]) (Union4 m n o p)
  
ToFFI (Union4 a b c d) (Union4 a b c d)
  
NPP ToFFI [a, b, c, d, e] [m, n, o, p, q] => ToFFI (HSum [a, b, c, d, e]) (Union5 m n o p q)
  
ToFFI (Union5 a b c d e) (Union5 a b c d e)
  
NPP ToFFI [a, b, c, d, e, f] [m, n, o, p, q, r] => ToFFI (HSum [a, b, c, d, e, f]) (Union6 m n o p q r)
  
ToFFI (Union6 a b c d e f) (Union6 a b c d e f)
  
NPP ToFFI [a, b, c, d, e, f, g] [m, n, o, p, q, r, s] => ToFFI (HSum [a, b, c, d, e, f, g]) (Union7 m n o p q r s)
  
ToFFI (Union7 a b c d e f g) (Union7 a b c d e f g)
  
NPP ToFFI [a, b, c, d, e, f, g, h] [m, n, o, p, q, r, s, t] => ToFFI (HSum [a, b, c, d, e, f, g, h]) (Union8 m n o p q r s t)
  
ToFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i] [m, n, o, p, q, r, s, t, u] => ToFFI (HSum [a, b, c, d, e, f, g, h, i]) (Union9 m n o p q r s t u)
  
ToFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i, j] [m, n, o, p, q, r, s, t, u, v] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j]) (Union10 m n o p q r s t u v)
  
ToFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k] [m, n, o, p, q, r, s, t, u, v, w] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k]) (Union11 m n o p q r s t u v w)
  
ToFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l] [m, n, o, p, q, r, s, t, u, v, w, x] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l]) (Union12 m n o p q r s t u v w x)
  
ToFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1] [m, n, o, p, q, r, s, t, u, v, w, x, y] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1]) (Union13 m n o p q r s t u v w x y)
  
ToFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2]) (Union14 m n o p q r s t u v w x y z)
  
ToFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3]) (Union15 m n o p q r s t u v w x y z z1)
  
ToFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o)
  
NPP ToFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => ToFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4]) (Union16 m n o p q r s t u v w x y z z1 z2)
  
ToFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p)
toFFI : ToFFI a ffiRepr => a -> ffiRepr
  Totality: total
  Visibility: public export
interface FromFFI : Type -> Type -> Type
  Interface supporting the use of a value as a
  return type in a foreign function call.

  Parameters: a, ffiRepr
Methods:
  
fromFFI : ffiRepr -> Maybe a

Implementations:
  
FromFFI ByteString ByteString
  
FromFFI JSInt64 JSInt64
  
FromFFI JSBits64 JSBits64
  
FromFFI Any AnyPtr
  
FromFFI ArrayBuffer ArrayBuffer
  
FromFFI UInt8ClampedArray UInt8ClampedArray
  
FromFFI UInt8Array UInt8Array
  
FromFFI UInt16Array UInt16Array
  
FromFFI UInt32Array UInt32Array
  
FromFFI Int8Array Int8Array
  
FromFFI Int16Array Int16Array
  
FromFFI Int32Array Int32Array
  
FromFFI Float32Array Float32Array
  
FromFFI Float64Array Float64Array
  
FromFFI DataView DataView
  
FromFFI (Array a) (Array a)
  
FromFFI Bool Boolean
  
FromFFI Object Object
  
FromFFI (Promise a) (Promise a)
  
FromFFI (Record a b) (Record a b)
  
FromFFI a b => FromFFI (Maybe a) (Nullable b)
  
FromFFI Undefined Undefined
  
FromFFI a b => FromFFI (Optional a) (UndefOr b)
  
FromFFI AnyPtr AnyPtr
  
FromFFI Bits8 Bits8
  
FromFFI Bits16 Bits16
  
FromFFI Bits32 Bits32
  
FromFFI Bits64 Bits64
  
FromFFI Int8 Int8
  
FromFFI Int16 Int16
  
FromFFI Int32 Int32
  
FromFFI Int64 Int64
  
FromFFI Char Char
  
FromFFI Int Int
  
FromFFI Integer Integer
  
FromFFI Double Double
  
FromFFI String String
  
FromFFI WindowProxy WindowProxy
  
NPP FromFFI [a, b] [m, n] => All SafeCast [m, n] => FromFFI (HSum [a, b]) (Union2 m n)
  
FromFFI (Union2 a b) (Union2 a b)
  
NPP FromFFI [a, b, c] [m, n, o] => All SafeCast [m, n, o] => FromFFI (HSum [a, b, c]) (Union3 m n o)
  
FromFFI (Union3 a b c) (Union3 a b c)
  
NPP FromFFI [a, b, c, d] [m, n, o, p] => All SafeCast [m, n, o, p] => FromFFI (HSum [a, b, c, d]) (Union4 m n o p)
  
FromFFI (Union4 a b c d) (Union4 a b c d)
  
NPP FromFFI [a, b, c, d, e] [m, n, o, p, r] => All SafeCast [m, n, o, p, r] => FromFFI (HSum [a, b, c, d, e]) (Union5 m n o p r)
  
FromFFI (Union5 a b c d e) (Union5 a b c d e)
  
NPP FromFFI [a, b, c, d, e, f] [m, n, o, p, r, s] => All SafeCast [m, n, o, p, r, s] => FromFFI (HSum [a, b, c, d, e, f]) (Union6 m n o p r s)
  
FromFFI (Union6 a b c d e f) (Union6 a b c d e f)
  
NPP FromFFI [a, b, c, d, e, f, g] [m, n, o, p, r, s, t] => All SafeCast [m, n, o, p, r, s, t] => FromFFI (HSum [a, b, c, d, e, f, g]) (Union7 m n o p r s t)
  
FromFFI (Union7 a b c d e f g) (Union7 a b c d e f g)
  
NPP FromFFI [a, b, c, d, e, f, g, h] [m, n, o, p, r, s, t, u] => All SafeCast [m, n, o, p, r, s, t, u] => FromFFI (HSum [a, b, c, d, e, f, g, h]) (Union8 m n o p r s t u)
  
FromFFI (Union8 a b c d e f g h) (Union8 a b c d e f g h)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i] [m, n, o, p, r, s, t, u, v] => All SafeCast [m, n, o, p, r, s, t, u, v] => FromFFI (HSum [a, b, c, d, e, f, g, h, i]) (Union9 m n o p r s t u v)
  
FromFFI (Union9 a b c d e f g h i) (Union9 a b c d e f g h i)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i, j] [m, n, o, p, r, s, t, u, v, w] => All SafeCast [m, n, o, p, r, s, t, u, v, w] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j]) (Union10 m n o p r s t u v w)
  
FromFFI (Union10 a b c d e f g h i j) (Union10 a b c d e f g h i j)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k] [m, n, o, p, q, r, s, t, u, v, w] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k]) (Union11 m n o p q r s t u v w)
  
FromFFI (Union11 a b c d e f g h i j k) (Union11 a b c d e f g h i j k)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l] [m, n, o, p, q, r, s, t, u, v, w, x] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l]) (Union12 m n o p q r s t u v w x)
  
FromFFI (Union12 a b c d e f g h i j k l) (Union12 a b c d e f g h i j k l)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1] [m, n, o, p, q, r, s, t, u, v, w, x, y] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1]) (Union13 m n o p q r s t u v w x y)
  
FromFFI (Union13 a b c d e f g h i j k l m) (Union13 a b c d e f g h i j k l m)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2] [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2]) (Union14 m n o p q r s t u v w x y z)
  
FromFFI (Union14 a b c d e f g h i j k l m n) (Union14 a b c d e f g h i j k l m n)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3]) (Union15 m n o p q r s t u v w x y z z1)
  
FromFFI (Union15 a b c d e f g h i j k l m n o) (Union15 a b c d e f g h i j k l m n o)
  
NPP FromFFI [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4] [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => All SafeCast [m, n, o, p, q, r, s, t, u, v, w, x, y, z, z1, z2] => FromFFI (HSum [a, b, c, d, e, f, g, h, i, j, k, l, a1, a2, a3, a4]) (Union16 m n o p q r s t u v w x y z z1 z2)
  
FromFFI (Union16 a b c d e f g h i j k l m n o p) (Union16 a b c d e f g h i j k l m n o p)
fromFFI : FromFFI a ffiRepr => ffiRepr -> Maybe a
  Totality: total
  Visibility: public export
tryFromFFI : FromFFI a ffiRepr => Lazy String -> ffiRepr -> JSIO a
  Totality: total
  Visibility: export
tryJS : FromFFI a ffiRepr => Lazy String -> PrimIO ffiRepr -> JSIO a
  Totality: total
  Visibility: export