use new FFI

IQuery.idr

@@ -1,14 +1,11 @@
 module IQuery
 
-import IQuery.Timeout
-import IQuery.Interval
-import IQuery.Event
-import IQuery.Elements
-import IQuery.State
-
-%access public
-
-alert : String -> IO ()
-alert msg =
-  mkForeign (FFun "alert(%0)" [FString] FUnit) msg
-
+import public IQuery.Timeout
+import public IQuery.Interval
+import public IQuery.Event
+import public IQuery.Elements
+import public IQuery.State
+%access public export
+
+alert : String -> JS_IO ()
+alert msg = foreign FFI_JS "alert(%0)" (String -> JS_IO ()) msg

IQuery/Ajax.idr

@@ -17,14 +17,14 @@ data Method : Type where
   GET : Method
   POST : Method
 
-new : IO XMLHttpRequest
-new = [| MkXHR (mkForeign (FFun "new XMLHttpRequest" [] FPtr)) |]
+new : JS_IO XMLHttpRequest
+new = [| MkXHR (foreign FFI_JS "new XMLHttpRequest" (JS_IO Ptr)) |]
 
-open : XMLHttpRequest -> Method -> String -> Bool -> IO ()
+open : XMLHttpRequest -> Method -> String -> Bool -> JS_IO ()
 open (MkXHR xhr) method url async =
-  mkForeign (
-    FFun "%0.open(%1,%2,%3)" [FPtr, FString, FString, FInt] FUnit
-  ) xhr (toMethod method) url (toAsync async)
+  foreign FFI_JS "%0.open(%1,%2,%3)"
+    (Ptr -> String -> String -> Int -> JS_IO ())
+    xhr (toMethod method) url (toAsync async)
   where toMethod : Method -> String
         toMethod GET = "GET"
         toMethod POST = "POST"
@@ -33,50 +33,54 @@ open (MkXHR xhr) method url async =
         toAsync True = 1
         toAsync False = 0
 
-setRequestHeader : XMLHttpRequest -> String -> String -> IO ()
+setRequestHeader : XMLHttpRequest -> String -> String -> JS_IO ()
 setRequestHeader (MkXHR xhr) name value =
-  mkForeign (
-    FFun "%0.setRequestHeader(%1, %2)" [FPtr, FString, FString] FUnit
-  ) xhr name value
+  foreign FFI_JS "%0.setRequestHeader(%1,%2)"
+    (Ptr -> String -> String -> JS_IO ())
+    xhr name value
 
-readyState : XMLHttpRequest -> IO ReadyState
+readyState : XMLHttpRequest -> JS_IO ReadyState
 readyState (MkXHR xhr) = do
-  r <- mkForeign (FFun "%0.readyState" [FPtr] FInt) xhr
+  r <- foreign FFI_JS "%0.readyState" (Ptr -> JS_IO Int) xhr
   pure $ case r of
               1 => Opened
               2 => HeadersReceived
               3 => Loading
               4 => Done
               _ => Unsent
 
-responseText : XMLHttpRequest -> IO String
-responseText (MkXHR xhr) = mkForeign (FFun "%0.responseText" [FPtr] FString) xhr
+responseText : XMLHttpRequest -> JS_IO String
+responseText (MkXHR xhr) =
+  foreign FFI_JS "%0.responseText" (Ptr -> JS_IO String) xhr
 
-status : XMLHttpRequest -> IO Int
-status (MkXHR xhr) = mkForeign (FFun "%0.status" [FPtr] FInt) xhr
+status : XMLHttpRequest -> JS_IO Int
+status (MkXHR xhr) = foreign FFI_JS "%0.status" (Ptr -> JS_IO Int) xhr
 
-onReadyStateChange : XMLHttpRequest -> IO () -> IO ()
-onReadyStateChange (MkXHR x) f =
-  mkForeign (
-    FFun "%0.onreadystatechange=%1" [FPtr, FFunction FUnit (FAny (IO ()))] FUnit
-  ) x (const f)
+onReadyStateChange : XMLHttpRequest -> JS_IO () -> JS_IO ()
+onReadyStateChange (MkXHR x) f = foreign FFI_JS "%0.onreadystatechange=%1"
+  (Ptr -> JsFn (() -> JS_IO ()) -> JS_IO ()) x (MkJsFn $ const f)
 
-send : XMLHttpRequest -> String -> IO ()
-send (MkXHR xhr) r = mkForeign (FFun "%0.send(%1)" [FPtr, FString] FUnit) xhr r
+send : XMLHttpRequest -> String -> JS_IO ()
+send (MkXHR xhr) r =
+  foreign FFI_JS "%0.send(%1)" (Ptr -> String -> JS_IO ()) xhr r
 
-public export
+export
 ajax : Method -> String -> Bool -> List (String, String) -> String ->
-       (Either Int String -> IO ()) -> IO ()
+       (Either Int String -> JS_IO ()) -> JS_IO ()
 ajax method url async headers dat callback = do
-  xhr <- new
-  open xhr method url async
-  traverse (uncurry $ setRequestHeader xhr) headers
-  onReadyStateChange xhr $ do rs <- readyState xhr
-                              case rs of
-                                   Done => do s <- status xhr
-                                              case s of
-                                                  200 => do t <- responseText xhr
-                                                            callback $ Right t
-                                                  _ => callback $ Left s
-                                   _ => return ()
-  send xhr dat
+    xhr <- new
+    open xhr method url async
+    traverse (uncurry $ setRequestHeader xhr) headers
+    onReadyStateChange xhr (mkHandler xhr)
+    send xhr dat
+  where
+    mkHandler : XMLHttpRequest -> JS_IO ()
+    mkHandler xhr = do
+      rs <- readyState (the XMLHttpRequest xhr)
+      case rs of
+           Done => do s <- status xhr
+                      case s of
+                          200 => do t <- responseText xhr
+                                    callback $ Right t
+                          _ => callback $ Left s
+           _ => pure ()

IQuery/Elements.idr

@@ -2,7 +2,7 @@ module Elements
 
 import IQuery.Event
 
-%access public export
+%access export
 
 export
 data Element : Type where
@@ -12,120 +12,87 @@ export
 data NodeList : Type where
   MkNodeList : Ptr -> NodeList
 
-newElement : String -> IO Element
-newElement t =
-  map MkElem $ mkForeign (FFun "document.createElement(%0)" [FString] FPtr) t
+newElement : String -> JS_IO Element
+newElement t = map MkElem $
+  foreign FFI_JS "document.createElement(%0)" (String -> JS_IO Ptr) t
 
-newElementNS : String -> String -> IO Element
-newElementNS ns t =
-  map MkElem $ mkForeign
-    (FFun "document.createElementNS(%0, %1)" [FString, FString] FPtr) ns t
+newElementNS : String -> String -> JS_IO Element
+newElementNS ns t = map MkElem $
+  foreign FFI_JS "document.createElementNS(%0, %1)"
+    (String -> String -> JS_IO Ptr) ns t
 
-setProperty : Element -> String -> String -> IO ()
+setProperty : Element -> String -> String -> JS_IO ()
 setProperty (MkElem e) name value =
-  mkForeign (
-    FFun "%0[%1]=%2" [ FPtr
-                     , FString
-                     , FString
-                     ] FUnit
-  ) e name value
-
-getProperty : Element -> String -> IO String
+  foreign FFI_JS "%0[%1]=%2" (Ptr -> String -> String -> JS_IO ()) e name value
+
+getProperty : Element -> String -> JS_IO String
 getProperty (MkElem e) name =
-  mkForeign (
-    FFun "%0[%1]" [ FPtr
-                  , FString
-                  ] FString
-  ) e name
+  foreign FFI_JS "%0[%1]" (Ptr -> String -> JS_IO String) e name
 
-setValue : Element -> String -> IO ()
+setValue : Element -> String -> JS_IO ()
 setValue = flip setProperty "value"
 
-getValue : Element -> IO String
+getValue : Element -> JS_IO String
 getValue = flip getProperty "value"
 
-setAttribute : Element -> String -> String -> IO ()
+setAttribute : Element -> String -> String -> JS_IO ()
 setAttribute (MkElem e) name value =
-  mkForeign (
-    FFun "%0.setAttribute(%1,%2)" [ FPtr
-                                  , FString
-                                  , FString
-                                  ] FUnit
-  ) e name value
-
-setAttributeNS : Element -> String -> String -> String -> IO ()
+  foreign FFI_JS "%0.setAttribute(%1,%2)" (Ptr -> String -> String -> JS_IO ())
+    e name value
+
+setAttributeNS : Element -> String -> String -> String -> JS_IO ()
 setAttributeNS (MkElem e) ns name value =
-  mkForeign (
-    FFun "%0.setAttributeNS(%1,%2,%3)" [ FPtr
-                                       , FString
-                                       , FString
-                                       , FString
-                                       ] FUnit
-  ) e ns name value
-
-getAttribute : Element -> String -> IO String
+  foreign FFI_JS "%0.setAttributeNS(%1,%2,%3)"
+    (Ptr -> String -> String -> String -> JS_IO ()) e ns name value
+
+getAttribute : Element -> String -> JS_IO String
 getAttribute (MkElem e) name =
-  mkForeign (
-    FFun "%0.getAttribute(%1)" [ FPtr
-                               , FString
-                               ] FString
-  ) e name
+  foreign FFI_JS "%0.getAttribute(%1)" (Ptr -> String -> JS_IO String) e name
 
-appendChild : Element -> Element -> IO ()
+appendChild : Element -> Element -> JS_IO ()
 appendChild (MkElem p) (MkElem c) =
-  mkForeign (
-    FFun "%0.appendChild(%1)" [ FPtr
-                              , FPtr
-                              ] FUnit
-  ) p c
+  foreign FFI_JS "%0.appendChild(%1)" (Ptr -> Ptr -> JS_IO ()) p c
 
-removeChild : Element -> Element -> IO ()
+removeChild : Element -> Element -> JS_IO ()
 removeChild (MkElem p) (MkElem c) =
-  mkForeign (
-    FFun "%0.removeChild(%1)" [ FPtr
-                              , FPtr
-                              ] FUnit
-  ) p c
+  foreign FFI_JS "%0.removeChild(%1)" (Ptr -> Ptr -> JS_IO ()) p c
 
-tagName : Element -> IO String
-tagName (MkElem e) = mkForeign (FFun "%0.tagName" [FPtr] FString) e
+tagName : Element -> JS_IO String
+tagName (MkElem e) = foreign FFI_JS "%0.tagName" (Ptr -> JS_IO String) e
 
-getText : Element -> IO String
-getText (MkElem e) =
-  mkForeign (FFun "%0.textContent" [FPtr] FString) e
+getText : Element -> JS_IO String
+getText (MkElem e) = foreign FFI_JS "%0.textContent" (Ptr -> JS_IO String) e
 
-setText : Element -> String -> IO ()
+setText : Element -> String -> JS_IO ()
 setText (MkElem e) s =
-  mkForeign (FFun "%0.textContent=%1" [FPtr, FString] FUnit) e s
+  foreign FFI_JS "%0.textContent=%1" (Ptr -> String -> JS_IO ()) e s
 
-onEvent : EventType -> Element -> (Event -> IO Int) -> IO ()
+onEvent : EventType -> Element -> (Event -> JS_IO Int) -> JS_IO ()
 onEvent ty (MkElem e) cb =
   let ev = show ty in
-      mkForeign (
-        FFun "%0.addEventListener(%1, %2)" [ FPtr
-                                           , FString
-                                           , FFunction (FAny Event) (FAny (IO Int))
-                                           ] FUnit
-      ) e ev cb
-
-onClick : Element -> (Event -> IO Int) -> IO ()
+      foreign FFI_JS "%0.addEventListener(%1, %2)"
+        (Ptr -> String -> JsFn (Ptr -> JS_IO Int) -> JS_IO ())
+        e ev (MkJsFn (execCallback cb))
+
+onClick : Element -> (Event -> JS_IO Int) -> JS_IO ()
 onClick = onEvent Click
 
-length : NodeList -> IO Int
-length (MkNodeList l) =
-  mkForeign (FFun "%0.length" [FPtr] FInt) l
+length : NodeList -> JS_IO Int
+length (MkNodeList l) = foreign FFI_JS "%0.length" (Ptr -> JS_IO Int) l
 
-elemAt : NodeList -> Int -> IO (Maybe Element)
+elemAt : NodeList -> Int -> JS_IO (Maybe Element)
 elemAt (MkNodeList l) i =
   if !(length $ MkNodeList l) > i then
-    map (Just . MkElem) $ mkForeign (FFun "%0.item(%1)" [FPtr, FInt] FPtr) l i
+    map (Just . MkElem) $
+      foreign FFI_JS "%0.item(%1)" (Ptr -> Int -> JS_IO Ptr) l i
   else
-    return Nothing
+    pure Nothing
 
-query : String -> IO NodeList
+query : String -> JS_IO NodeList
 query q =
-  map MkNodeList $ mkForeign (FFun "document.querySelectorAll(%0)" [FString] FPtr) q
+  map MkNodeList $
+    foreign FFI_JS "document.querySelectorAll(%0)" (String -> JS_IO Ptr) q
 
-childNodes : Element -> IO NodeList
+childNodes : Element -> JS_IO NodeList
 childNodes (MkElem e) =
-  map MkNodeList $ mkForeign (FFun "%0.childNodes" [FPtr] FPtr) e
+  map MkNodeList $ foreign FFI_JS "%0.childNodes" (Ptr -> JS_IO Ptr) e

IQuery/Event.idr

@@ -2,7 +2,7 @@ module Event
 
 import IQuery.Key
 
-%access public
+%access export
 
 export
 data Event : Type where
@@ -33,7 +33,7 @@ data EventType : Type where
   Select : EventType
   Submit : EventType
 
-instance Show EventType where
+Show EventType where
   show Click = "click"
   show DoubleClick = "dblclick"
   show MouseDown = "mousedown"
@@ -58,38 +58,41 @@ instance Show EventType where
   show Submit = "submit"
 
 private
-evProp : {fty : FTy} -> String -> Event -> IO (interpFTy fty)
-evProp {fty} propName (MkEvent e) = mkForeign (
-                                      FFun "%0[%1]" [ FPtr, FString ] fty
-                                    ) e propName
+evProp : {ty : Type} -> {auto fty : FTy FFI_JS [] (Ptr -> String -> JS_IO ty)} ->
+         String -> Event -> JS_IO ty
+evProp {ty} {fty} propName (MkEvent e) =
+  foreign FFI_JS "%0[%1]" (Ptr -> String -> JS_IO ty) e propName
 
 private
-boolProp : String -> Event -> IO Bool
-boolProp propName e = map toBool $ evProp {fty = FInt} propName e
+boolProp : String -> Event -> JS_IO Bool
+boolProp propName e = map toBool $ evProp {ty = Int} propName e
   where toBool : Int -> Bool
         toBool 1 = True
         toBool _ = False
 
-key : Event -> IO (Maybe Key)
-key e = map fromKeyCode $ evProp {fty = FInt} "keyCode" e
+key : Event -> JS_IO (Maybe Key)
+key e = map fromKeyCode $ evProp {ty = Int} "keyCode" e
 
-mouseButton : Event -> IO (Maybe MouseButton)
-mouseButton e = map fromButtonCode $ evProp {fty = FInt} "button" e
+mouseButton : Event -> JS_IO (Maybe MouseButton)
+mouseButton e = map fromButtonCode $ evProp {ty = Int} "button" e
 
-clientX : Event -> IO Int
-clientX = evProp {fty = FInt} "clientX"
+clientX : Event -> JS_IO Int
+clientX = evProp {ty = Int} "clientX"
 
-clientY : Event -> IO Int
-clientY = evProp {fty = FInt} "clientY"
+clientY : Event -> JS_IO Int
+clientY = evProp {ty = Int} "clientY"
 
-altKey : Event -> IO Bool
+altKey : Event -> JS_IO Bool
 altKey = boolProp "altKey"
 
-ctrlKey : Event -> IO Bool
+ctrlKey : Event -> JS_IO Bool
 ctrlKey = boolProp "ctrlKey"
 
-metaKey : Event -> IO Bool
+metaKey : Event -> JS_IO Bool
 metaKey = boolProp "metaKey"
 
-shiftKey : Event -> IO Bool
+shiftKey : Event -> JS_IO Bool
 shiftKey = boolProp "shiftKey"
+
+execCallback : (Event -> JS_IO Int) -> Ptr -> JS_IO Int
+execCallback cb = cb . MkEvent