0 | module JS.Marshall
  1 |
  2 | import Control.Monad.Either
  3 | import JS.Inheritance
  4 | import JS.Util
  5 |
  6 | %default total
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          Marshalling from and to JS
 10 | --------------------------------------------------------------------------------
 11 |
 12 | ||| Interface supporting the use of a value as an
 13 | ||| argument in a foreign function call.
 14 | |||
 15 | ||| Implementations for primitives and external type should be
 16 | ||| done using `believe_me`, as they are alredy in the correct
 17 | ||| representation. Idris2 types should be converted to primitives
 18 | ||| or external constants first.
 19 | public export
 20 | interface ToFFI a ffiRepr | a where
 21 |   toFFI : a -> ffiRepr
 22 |
 23 | export
 24 | ToFFI AnyPtr AnyPtr where toFFI = id
 25 |
 26 | export
 27 | ToFFI Bits8 Bits8 where toFFI = id
 28 |
 29 | export
 30 | ToFFI Bits16 Bits16 where toFFI = id
 31 |
 32 | export
 33 | ToFFI Bits32 Bits32 where toFFI = id
 34 |
 35 | export
 36 | ToFFI Bits64 Bits64 where toFFI = id
 37 |
 38 | export
 39 | ToFFI Int8 Int8 where toFFI = id
 40 |
 41 | export
 42 | ToFFI Int16 Int16 where toFFI = id
 43 |
 44 | export
 45 | ToFFI Int32 Int32 where toFFI = id
 46 |
 47 | export
 48 | ToFFI Int64 Int64 where toFFI = id
 49 |
 50 | export
 51 | ToFFI Int Int where toFFI = id
 52 |
 53 | export
 54 | ToFFI Char Char where toFFI = id
 55 |
 56 | export
 57 | ToFFI Integer Integer where toFFI = id
 58 |
 59 | export
 60 | ToFFI Double Double where toFFI = id
 61 |
 62 | export
 63 | ToFFI String String where toFFI = id
 64 |
 65 | export
 66 | ToFFI WindowProxy WindowProxy where toFFI = id
 67 |
 68 | ||| Interface supporting the use of a value as a
 69 | ||| return type in a foreign function call.
 70 | public export
 71 | interface FromFFI a ffiRepr | a where
 72 |   fromFFI : ffiRepr -> Maybe a
 73 |
 74 | export
 75 | FromFFI AnyPtr AnyPtr where fromFFI = Just
 76 |
 77 | export
 78 | FromFFI Bits8 Bits8 where fromFFI = Just
 79 |
 80 | export
 81 | FromFFI Bits16 Bits16 where fromFFI = Just
 82 |
 83 | export
 84 | FromFFI Bits32 Bits32 where fromFFI = Just
 85 |
 86 | export
 87 | FromFFI Bits64 Bits64 where fromFFI = Just
 88 |
 89 | export
 90 | FromFFI Int8 Int8 where fromFFI = Just
 91 |
 92 | export
 93 | FromFFI Int16 Int16 where fromFFI = Just
 94 |
 95 | export
 96 | FromFFI Int32 Int32 where fromFFI = Just
 97 |
 98 | export
 99 | FromFFI Int64 Int64 where fromFFI = Just
100 |
101 | export
102 | FromFFI Char Char where fromFFI = Just
103 |
104 | export
105 | FromFFI Int Int where fromFFI = Just
106 |
107 | export
108 | FromFFI Integer Integer where fromFFI = Just
109 |
110 | export
111 | FromFFI Double Double where fromFFI = Just
112 |
113 | export
114 | FromFFI String String where fromFFI = Just
115 |
116 | export
117 | FromFFI WindowProxy WindowProxy where fromFFI = Just
118 |
119 | export
120 | tryFromFFI : FromFFI a ffiRepr => (fun : Lazy String) -> ffiRepr -> JSIO a
121 | tryFromFFI fun ptr = case fromFFI ptr of
122 |   Nothing => throwError $ CastErr fun ptr
123 |   Just v  => pure v
124 |
125 | export
126 | tryJS : FromFFI a ffiRepr => (fun : Lazy String) -> PrimIO ffiRepr -> JSIO a
127 | tryJS fun prim = primJS prim >>= tryFromFFI fun
128 |