0 | ||| Javascript utilities. If these prove to be useful in
  1 | ||| applications, they should eventually go into their
  2 | ||| own package.
  3 | module JS.Util
  4 |
  5 | import Control.Monad.Reader
  6 | import Control.Monad.RWS
  7 | import Control.Monad.State
  8 | import Control.Monad.Writer
  9 | import public Control.Monad.Either
 10 | import Data.Maybe
 11 |
 12 | %default total
 13 |
 14 | %foreign "javascript:lambda:v=>typeof(v)"
 15 | prim__typeOf : AnyPtr -> String
 16 |
 17 | ||| Inspect the type of a value at runtime by means of
 18 | ||| Javascript function `typeof`.
 19 | export %inline
 20 | typeof : a -> String
 21 | typeof v = prim__typeOf (believe_me v)
 22 |
 23 | %foreign "javascript:lambda:(a,b)=>a === b?1:0"
 24 | prim__eqv : AnyPtr -> AnyPtr -> Bool
 25 |
 26 | ||| Heterogeneous pointer equality. This calls the Javascript
 27 | ||| `===` operator internally.
 28 | export %inline
 29 | eqv : a -> b -> Bool
 30 | eqv x y = prim__eqv (believe_me x) (believe_me y)
 31 |
 32 | %foreign "javascript:lambda:x=>String(x)"
 33 | prim__show : AnyPtr -> String
 34 |
 35 | ||| Displays a JS value by passing it to `String(...)`.
 36 | export %inline
 37 | jsShow : a -> String
 38 | jsShow v = prim__show (believe_me v)
 39 |
 40 | --------------------------------------------------------------------------------
 41 | --          IO
 42 | --------------------------------------------------------------------------------
 43 |
 44 | %foreign "javascript:lambda:x=>console.log(x)"
 45 | prim__consoleLog : String -> PrimIO ()
 46 |
 47 | export
 48 | consoleLog : HasIO io => String -> io ()
 49 | consoleLog s = primIO $ prim__consoleLog s
 50 |
 51 | public export
 52 | data JSErr : Type where
 53 |   Caught    : (msg : String) -> JSErr
 54 |   CastErr   : (inFunction : String) -> (value : a) -> JSErr
 55 |   IsNothing : (callSite : String) -> JSErr
 56 |
 57 | export
 58 | dispErr : JSErr -> String
 59 | dispErr (CastErr inFunction value) = #"""
 60 |   Error when casting a Javascript value in function \#{inFunction}.
 61 |     The value was: \#{jsShow value}.
 62 |     The value's type was \#{typeof value}.
 63 |   """#
 64 |
 65 | dispErr (IsNothing callSite) =
 66 |   #"Trying to extract a value from Nothing at \#{callSite}"#
 67 |
 68 | dispErr (Caught msg) = msg
 69 |
 70 |
 71 | public export
 72 | JSIO : Type -> Type
 73 | JSIO = EitherT JSErr IO
 74 |
 75 | public export
 76 | interface HasIO io => LiftJSIO io where
 77 |   liftJSIO : JSIO a -> io a
 78 |
 79 | export %inline
 80 | LiftJSIO JSIO where
 81 |   liftJSIO = id
 82 |
 83 | export %inline
 84 | LiftJSIO m => LiftJSIO (StateT s m) where
 85 |   liftJSIO m = ST $ \st => (st,) <$> liftJSIO m
 86 |
 87 | export %inline
 88 | LiftJSIO m => LiftJSIO (ReaderT e m) where
 89 |   liftJSIO m = MkReaderT $ \_ => liftJSIO m
 90 |
 91 | export %inline
 92 | LiftJSIO m => LiftJSIO (WriterT w m) where
 93 |   liftJSIO m = MkWriterT $ \vw => (,vw) <$> liftJSIO m
 94 |
 95 | export %inline
 96 | LiftJSIO m => LiftJSIO (RWST r w w m) where
 97 |   liftJSIO m = MkRWST $ \_,vs,vw => (,vs,vw) <$> liftJSIO m
 98 |
 99 | export
100 | runJSWith : Lazy (JSErr -> IO a) -> JSIO a -> IO a
101 | runJSWith f (MkEitherT io) = io >>= either f pure
102 |
103 | export
104 | runJS : JSIO () -> IO ()
105 | runJS = runJSWith (consoleLog . dispErr)
106 |
107 | export
108 | runJSWithDefault : Lazy a -> JSIO a -> IO a
109 | runJSWithDefault a = runJSWith (\e => consoleLog (dispErr e) $> a)
110 |
111 | export %inline
112 | primJS : PrimIO a -> JSIO a
113 | primJS = primIO
114 |
115 | export
116 | unMaybe : (callSite : String) -> JSIO (Maybe a) -> JSIO a
117 | unMaybe callSite io = do
118 |   Just a <- io | Nothing => throwError $ IsNothing callSite
119 |   pure a
120 |
121 | --------------------------------------------------------------------------------
122 | --          Error handling
123 | --------------------------------------------------------------------------------
124 |
125 | %foreign "javascript:lambda:(u,io) => {try { return [1,io()]; } catch (e) { return [0,String(e)] }}"
126 | prim__tryIO : forall a . IO a -> PrimIO AnyPtr
127 |
128 | %foreign "javascript:lambda:(x,y,f,v) => {try { return [1,f(v)]; } catch (e) { return [0,String(e)] }}"
129 | prim__try : forall a,b . (a -> b) -> a -> AnyPtr
130 |
131 | %foreign "javascript:lambda:x => x[0]"
132 | prim__errTag : AnyPtr -> Double
133 |
134 | %foreign "javascript:lambda:x => x[1]"
135 | prim__errVal : AnyPtr -> AnyPtr
136 |
137 | toEither : AnyPtr -> Either JSErr a
138 | toEither ptr =
139 |   if 1 == prim__errTag ptr
140 |     then Right (believe_me (prim__errVal ptr))
141 |     else Left $ Caught (believe_me (prim__errVal ptr))
142 |
143 | ||| Tries to execute an IO action, wrapping any runtime exception
144 | ||| in its stringified version in a `Left . Caught`.
145 | export
146 | tryIO : IO a -> JSIO a
147 | tryIO io = do
148 |   ptr <- primIO $ prim__tryIO io
149 |   if 1 == prim__errTag ptr
150 |      then pure (believe_me (prim__errVal ptr))
151 |      else throwError $ Caught (believe_me (prim__errVal ptr))
152 |
153 | ||| Error handling in pure functions. This should only be used
154 | ||| in foreign function calls that might fail but or otherwise
155 | ||| pure calculations.
156 | export
157 | try : (a -> b) -> a -> Either JSErr b
158 | try f a = toEither $ prim__try f a
159 |
160 | --------------------------------------------------------------------------------
161 | --          Common external types
162 | --------------------------------------------------------------------------------
163 |
164 | ||| See [spec](https://html.spec.whatwg.org/#windowproxy)
165 | export
166 | data WindowProxy : Type where [external]
167 |