From 41eabc8a9b0548016859fb2c827b09b7dad81517 Mon Sep 17 00:00:00 2001 From: Brandon Dyck Date: Sat, 13 Jan 2018 15:09:36 -0700 Subject: [PATCH 1/3] updated access modifiers --- IQuery/Ajax.idr | 5 ++--- IQuery/Elements.idr | 14 ++++++-------- IQuery/Event.idr | 4 ++-- IQuery/Interval.idr | 3 +-- IQuery/Key.idr | 3 +-- IQuery/State.idr | 46 ++++++++++++++++++++++----------------------- IQuery/Timeout.idr | 3 +-- 7 files changed, 35 insertions(+), 43 deletions(-) diff --git a/IQuery/Ajax.idr b/IQuery/Ajax.idr index e486462..da460a0 100644 --- a/IQuery/Ajax.idr +++ b/IQuery/Ajax.idr @@ -12,7 +12,7 @@ data ReadyState : Type where Loading : ReadyState Done : ReadyState -public +public export data Method : Type where GET : Method POST : Method @@ -64,7 +64,7 @@ onReadyStateChange (MkXHR x) f = send : XMLHttpRequest -> String -> IO () send (MkXHR xhr) r = mkForeign (FFun "%0.send(%1)" [FPtr, FString] FUnit) xhr r -public +public export ajax : Method -> String -> Bool -> List (String, String) -> String -> (Either Int String -> IO ()) -> IO () ajax method url async headers dat callback = do @@ -80,4 +80,3 @@ ajax method url async headers dat callback = do _ => callback $ Left s _ => return () send xhr dat - diff --git a/IQuery/Elements.idr b/IQuery/Elements.idr index bb06fa8..571f2e0 100644 --- a/IQuery/Elements.idr +++ b/IQuery/Elements.idr @@ -2,13 +2,13 @@ module Elements import IQuery.Event -%access public +%access public export -abstract +export data Element : Type where MkElem : Ptr -> Element -abstract +export data NodeList : Type where MkNodeList : Ptr -> NodeList @@ -18,7 +18,7 @@ newElement t = newElementNS : String -> String -> IO Element newElementNS ns t = - map MkElem $ mkForeign + map MkElem $ mkForeign (FFun "document.createElementNS(%0, %1)" [FString, FString] FPtr) ns t setProperty : Element -> String -> String -> IO () @@ -31,7 +31,7 @@ setProperty (MkElem e) name value = ) e name value getProperty : Element -> String -> IO String -getProperty (MkElem e) name = +getProperty (MkElem e) name = mkForeign ( FFun "%0[%1]" [ FPtr , FString @@ -64,7 +64,7 @@ setAttributeNS (MkElem e) ns name value = ) e ns name value getAttribute : Element -> String -> IO String -getAttribute (MkElem e) name = +getAttribute (MkElem e) name = mkForeign ( FFun "%0.getAttribute(%1)" [ FPtr , FString @@ -129,5 +129,3 @@ query q = childNodes : Element -> IO NodeList childNodes (MkElem e) = map MkNodeList $ mkForeign (FFun "%0.childNodes" [FPtr] FPtr) e - - diff --git a/IQuery/Event.idr b/IQuery/Event.idr index da4ab2c..e00679b 100644 --- a/IQuery/Event.idr +++ b/IQuery/Event.idr @@ -4,11 +4,11 @@ import IQuery.Key %access public -abstract +export data Event : Type where MkEvent : Ptr -> Event -public +public export data EventType : Type where Click : EventType DoubleClick : EventType diff --git a/IQuery/Interval.idr b/IQuery/Interval.idr index a727951..5ac99c9 100644 --- a/IQuery/Interval.idr +++ b/IQuery/Interval.idr @@ -2,7 +2,7 @@ module Interval %access public -abstract +export data Interval : Type where MkInterval : Ptr -> Interval @@ -16,4 +16,3 @@ setInterval f t = do clearInterval : Interval -> IO () clearInterval (MkInterval p) = mkForeign (FFun "clearInterval(%0)" [FPtr] FUnit) p - diff --git a/IQuery/Key.idr b/IQuery/Key.idr index 6056ff6..4794a48 100644 --- a/IQuery/Key.idr +++ b/IQuery/Key.idr @@ -1,4 +1,4 @@ -module Key +module IQuery.Key data MouseButton : Type where MouseLeft : MouseButton @@ -283,4 +283,3 @@ fromKeyCode 88 = Just KeyX fromKeyCode 89 = Just KeyY fromKeyCode 90 = Just KeyZ fromKeyCode _ = Nothing - diff --git a/IQuery/State.idr b/IQuery/State.idr index de6f925..0736914 100644 --- a/IQuery/State.idr +++ b/IQuery/State.idr @@ -2,7 +2,7 @@ module IQuery.State %access private -public +public export data StateTy : Type where STInt : StateTy STString : StateTy @@ -11,18 +11,18 @@ data StateTy : Type where -- STRecord : List (String,StateTy) -> StateTy -- STHash : StateTy -> StateTy -public +public export interpSTy : StateTy -> Type interpSTy STInt = Int interpSTy STString = String interpSTy (STMaybe a) = Maybe (interpSTy a) interpSTy (STList a) = List (interpSTy a) -abstract +export data State : StateTy -> Type where MkState : (t : StateTy) -> Ptr -> State t -abstract +export data StateC : StateTy -> Type where MkStateC : Int -> (t : StateTy) -> Ptr -> StateC t @@ -37,13 +37,13 @@ stateVarName = "__IDR__IQUERY__STATE__" stateVarExists : IO Bool stateVarExists = do - o <- mkForeign (FFun ("typeof " ++ stateVarName) [] FString) + o <- mkForeign (FFun ("typeof " ++ stateVarName) [] FString) pure $ if o == "object" then True else False initStateVar : IO Ptr initStateVar = mkForeign (FFun (stateVarName ++ " = {count: 0}") [] FPtr) -getStateVar : IO (Maybe Ptr) +getStateVar : IO (Maybe Ptr) getStateVar = case !stateVarExists of True => map Just $ mkForeign (FFun stateVarName [] FPtr) False => pure Nothing @@ -65,8 +65,8 @@ incCount c = do pure n infixl 5 =>> -public -(=>>) : IO (Maybe (State a)) -> (State a -> IO (Maybe b)) +public export +(=>>) : IO (Maybe (State a)) -> (State a -> IO (Maybe b)) -> IO (Maybe b) s =>> f = do (Just s') <- s @@ -74,7 +74,7 @@ s =>> f = do f s' infixl 5 :=> -public +public export (:=>) : IO (Maybe (State a)) -> (State a -> IO ()) -> IO Bool (:=>) s f = do (Just s') <- s @@ -82,7 +82,7 @@ public f s' pure True -public +public export access : Nat -> State (STList t) -> IO (Maybe (State t)) access n (MkState (STList t) p) = do r <- mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p (fromNat n) @@ -94,60 +94,58 @@ fromState' : State t -> IO (interpSTy t) fromState' (MkState STInt p) = mkForeign (FFun "%0.val" [FPtr] FInt) p fromState' (MkState STString p) = mkForeign (FFun "%0.val" [FPtr] FString) p fromState' (MkState (STMaybe a) p) = do - isNull <- (mkForeign (FFun "(%0.val == null).toString()" [FPtr] FString) p) + isNull <- (mkForeign (FFun "(%0.val == null).toString()" [FPtr] FString) p) case isNull == "true" of True => pure Nothing False => pure $ Just !(fromState' (MkState a p)) fromState' (MkState (STList a) p) = do n <- mkForeign (FFun "%0.val.length" [FPtr] FInt) p - ps <- sequence $ map + ps <- sequence $ map (\n => mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p n) [0..(n-1)] sequence $ map (\p' => fromState' (MkState a p')) ps -public +public export fromState : State t -> IO (Maybe (interpSTy t)) fromState (MkState t p) = do - True <- isObj p + True <- isObj p | False => pure Nothing map Just $ fromState' (MkState t p) -public +public export toState : {t : StateTy} -> interpSTy t -> State t -> IO () -toState v (MkState STInt p) = +toState v (MkState STInt p) = mkForeign (FFun "%0.val = %1" [FPtr, FInt] FUnit) p v toState v (MkState STString p) = do mkForeign (FFun "%0.val = %1" [FPtr, FString] FUnit) p v -toState Nothing (MkState (STMaybe a) p) = +toState Nothing (MkState (STMaybe a) p) = mkForeign (FFun "%0.val = null" [FPtr] FUnit) p toState (Just v) (MkState (STMaybe a) p) = toState v (MkState a p) toState xs (MkState (STList a) p) = do array <- mkForeign (FFun "%0.val = []" [FPtr] FPtr) p sequence_ $ map (\x => do - n <- mkForeign (FFun "%0.push( {} )" [FPtr] FInt) array + n <- mkForeign (FFun "%0.push( {} )" [FPtr] FInt) array box <- mkForeign (FFun "%0[%1]" [FPtr, FInt] FPtr) array (n-1) toState x (MkState a box) ) xs -public +public export get : StateC t -> IO (Maybe (State t)) get (MkStateC _ t p) = do True <- isObj p | False => pure Nothing pure $ Just $ MkState t p -public +public export newState : (t : StateTy) -> interpSTy t -> IO (StateC t) newState t v = do c <- getStateVar' n <- incCount c p <- mkForeign (FFun "%0[%1] = {}" [FPtr,FInt] FPtr) c n - toState v (MkState t p) + toState v (MkState t p) pure $ MkStateC n t p -public +public export destroyState : StateC t -> IO () destroyState (MkStateC n _ _) = do c <- getStateVar' mkForeign (FFun "delete %0[%1]" [FPtr,FInt] FUnit) c n - - diff --git a/IQuery/Timeout.idr b/IQuery/Timeout.idr index 8343c84..1657203 100644 --- a/IQuery/Timeout.idr +++ b/IQuery/Timeout.idr @@ -2,7 +2,7 @@ module Timeout %access public -abstract +export data Timeout : Type where MkTimeout : Ptr -> Timeout @@ -16,4 +16,3 @@ setTimeout f t = do clearTimeout : Timeout -> IO () clearTimeout (MkTimeout p) = mkForeign (FFun "clearTimeout(%0)" [FPtr] FUnit) p - From 824357feb907f773d5ebb6782c4857284d3d3305 Mon Sep 17 00:00:00 2001 From: Brandon Dyck Date: Sun, 14 Jan 2018 12:09:13 -0700 Subject: [PATCH 2/3] use new FFI --- IQuery.idr | 21 +++---- IQuery/Ajax.idr | 78 +++++++++++++------------ IQuery/Elements.idr | 137 +++++++++++++++++--------------------------- IQuery/Event.idr | 43 +++++++------- IQuery/Interval.idr | 17 +++--- IQuery/Key.idr | 4 +- IQuery/State.idr | 92 ++++++++++++++--------------- IQuery/Timeout.idr | 15 +++-- example/state.idr | 18 +++--- 9 files changed, 199 insertions(+), 226 deletions(-) diff --git a/IQuery.idr b/IQuery.idr index a3dbb72..b97f3cd 100644 --- a/IQuery.idr +++ b/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 diff --git a/IQuery/Ajax.idr b/IQuery/Ajax.idr index da460a0..b55f23e 100644 --- a/IQuery/Ajax.idr +++ b/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,15 +33,15 @@ 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 @@ -49,34 +49,38 @@ readyState (MkXHR xhr) = do 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 () diff --git a/IQuery/Elements.idr b/IQuery/Elements.idr index 571f2e0..ab5d048 100644 --- a/IQuery/Elements.idr +++ b/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 diff --git a/IQuery/Event.idr b/IQuery/Event.idr index e00679b..779155c 100644 --- a/IQuery/Event.idr +++ b/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 diff --git a/IQuery/Interval.idr b/IQuery/Interval.idr index 5ac99c9..cad79a9 100644 --- a/IQuery/Interval.idr +++ b/IQuery/Interval.idr @@ -1,18 +1,17 @@ module Interval -%access public +%access public export export data Interval : Type where MkInterval : Ptr -> Interval -setInterval : (() -> IO ()) -> Float -> IO Interval +export +setInterval : (() -> JS_IO ()) -> Double -> JS_IO Interval setInterval f t = do - e <- mkForeign ( - FFun "setInterval(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr - ) f t - return (MkInterval e) + e <- foreign FFI_JS "setInterval(%0,%1)" + (JsFn (() -> JS_IO ()) -> Double -> JS_IO Ptr) (MkJsFn f) t + pure (MkInterval e) -clearInterval : Interval -> IO () -clearInterval (MkInterval p) = - mkForeign (FFun "clearInterval(%0)" [FPtr] FUnit) p +clearInterval : Interval -> JS_IO () +clearInterval (MkInterval p) = foreign FFI_JS "clearInterval(%0)" (Ptr -> JS_IO ()) p diff --git a/IQuery/Key.idr b/IQuery/Key.idr index 4794a48..f1ed1fa 100644 --- a/IQuery/Key.idr +++ b/IQuery/Key.idr @@ -1,4 +1,6 @@ -module IQuery.Key +module Key + +%access public export data MouseButton : Type where MouseLeft : MouseButton diff --git a/IQuery/State.idr b/IQuery/State.idr index 0736914..5f54915 100644 --- a/IQuery/State.idr +++ b/IQuery/State.idr @@ -1,4 +1,4 @@ -module IQuery.State +module State %access private @@ -26,48 +26,49 @@ export data StateC : StateTy -> Type where MkStateC : Int -> (t : StateTy) -> Ptr -> StateC t -isObj : Ptr -> IO Bool +isObj : Ptr -> JS_IO Bool isObj p = do - "object" <- mkForeign (FFun "typeof %0" [FPtr] FString) p + "object" <- foreign FFI_JS "typeof %0" (Ptr -> JS_IO String) p | _ => pure False pure True stateVarName : String stateVarName = "__IDR__IQUERY__STATE__" -stateVarExists : IO Bool +stateVarExists : JS_IO Bool stateVarExists = do - o <- mkForeign (FFun ("typeof " ++ stateVarName) [] FString) + o <- foreign FFI_JS ("typeof " ++ stateVarName) (JS_IO String) pure $ if o == "object" then True else False -initStateVar : IO Ptr -initStateVar = mkForeign (FFun (stateVarName ++ " = {count: 0}") [] FPtr) +initStateVar : JS_IO Ptr +initStateVar = + foreign FFI_JS (stateVarName ++ " = {count: 0}") (JS_IO Ptr) -getStateVar : IO (Maybe Ptr) +getStateVar : JS_IO (Maybe Ptr) getStateVar = case !stateVarExists of - True => map Just $ mkForeign (FFun stateVarName [] FPtr) + True => map Just $ foreign FFI_JS stateVarName (JS_IO Ptr) False => pure Nothing -getStateVar' : IO Ptr +getStateVar' : JS_IO Ptr getStateVar' = case !getStateVar of Just s => pure s Nothing => initStateVar -stateCExists : Ptr -> Int -> IO Bool +stateCExists : Ptr -> Int -> JS_IO Bool stateCExists c n = do - r <- mkForeign (FFun "typeof %0[%1]" [FPtr,FInt] FString) c n + r <- foreign FFI_JS "typeof %0[%1]" (Ptr -> Int -> JS_IO String) c n pure $ if r == "object" then True else False -incCount : Ptr -> IO Int +incCount : Ptr -> JS_IO Int incCount c = do - n <- mkForeign (FFun "%0.count" [FPtr] FInt) c - mkForeign (FFun "%0.count++" [FPtr] FUnit) c + n <- foreign FFI_JS "%0.count" (Ptr -> JS_IO Int) c + foreign FFI_JS "%0.count++" (Ptr -> JS_IO ()) c pure n infixl 5 =>> public export -(=>>) : IO (Maybe (State a)) -> (State a -> IO (Maybe b)) - -> IO (Maybe b) +(=>>) : JS_IO (Maybe (State a)) -> (State a -> JS_IO (Maybe b)) + -> JS_IO (Maybe b) s =>> f = do (Just s') <- s | Nothing => pure Nothing @@ -75,77 +76,78 @@ s =>> f = do infixl 5 :=> public export -(:=>) : IO (Maybe (State a)) -> (State a -> IO ()) -> IO Bool +(:=>) : JS_IO (Maybe (State a)) -> (State a -> JS_IO ()) -> JS_IO Bool (:=>) s f = do (Just s') <- s | Nothing => pure False f s' pure True -public export -access : Nat -> State (STList t) -> IO (Maybe (State t)) +export +access : Nat -> State (STList t) -> JS_IO (Maybe (State t)) access n (MkState (STList t) p) = do - r <- mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p (fromNat n) + r <- foreign FFI_JS "%0.val[%1]" (Ptr -> Int -> JS_IO Ptr) + p (fromNat n) True <- isObj r | False => pure Nothing pure $ Just $ MkState t r -fromState' : State t -> IO (interpSTy t) -fromState' (MkState STInt p) = mkForeign (FFun "%0.val" [FPtr] FInt) p -fromState' (MkState STString p) = mkForeign (FFun "%0.val" [FPtr] FString) p +fromState' : State t -> JS_IO (interpSTy t) +fromState' (MkState STInt p) = foreign FFI_JS "%0.val" (Ptr -> JS_IO Int) p +fromState' (MkState STString p) = foreign FFI_JS "%0.val" (Ptr -> JS_IO String) p fromState' (MkState (STMaybe a) p) = do - isNull <- (mkForeign (FFun "(%0.val == null).toString()" [FPtr] FString) p) + isNull <- foreign FFI_JS "(%0.val == null).toString()" (Ptr -> JS_IO String) p case isNull == "true" of True => pure Nothing False => pure $ Just !(fromState' (MkState a p)) fromState' (MkState (STList a) p) = do - n <- mkForeign (FFun "%0.val.length" [FPtr] FInt) p + n <- foreign FFI_JS "%0.val.length" (Ptr -> JS_IO Int) p ps <- sequence $ map - (\n => mkForeign (FFun "%0.val[%1]" [FPtr,FInt] FPtr) p n) [0..(n-1)] + (foreign FFI_JS "%0.val[%1]" (Ptr -> Int -> JS_IO Ptr) p) [0..(n-1)] sequence $ map (\p' => fromState' (MkState a p')) ps -public export -fromState : State t -> IO (Maybe (interpSTy t)) +export +fromState : State t -> JS_IO (Maybe (interpSTy t)) fromState (MkState t p) = do True <- isObj p | False => pure Nothing map Just $ fromState' (MkState t p) -public export -toState : {t : StateTy} -> interpSTy t -> State t -> IO () +export +toState : {t : StateTy} -> interpSTy t -> State t -> JS_IO () toState v (MkState STInt p) = - mkForeign (FFun "%0.val = %1" [FPtr, FInt] FUnit) p v + foreign FFI_JS "%0.val = %1" (Ptr -> Int -> JS_IO ()) p v toState v (MkState STString p) = do - mkForeign (FFun "%0.val = %1" [FPtr, FString] FUnit) p v + foreign FFI_JS "%0.val = %1" (Ptr -> String -> JS_IO ()) p v toState Nothing (MkState (STMaybe a) p) = - mkForeign (FFun "%0.val = null" [FPtr] FUnit) p + foreign FFI_JS "%0.val = null" (Ptr -> JS_IO ()) p toState (Just v) (MkState (STMaybe a) p) = toState v (MkState a p) toState xs (MkState (STList a) p) = do - array <- mkForeign (FFun "%0.val = []" [FPtr] FPtr) p + array <- foreign FFI_JS "%0.val = []" (Ptr -> JS_IO Ptr) p sequence_ $ map (\x => do - n <- mkForeign (FFun "%0.push( {} )" [FPtr] FInt) array - box <- mkForeign (FFun "%0[%1]" [FPtr, FInt] FPtr) array (n-1) + n <- foreign FFI_JS "%0.push( {} )" (Ptr -> JS_IO Int) array + box <- foreign FFI_JS "%0[%1]" (Ptr -> Int -> JS_IO Ptr) array (n-1) toState x (MkState a box) ) xs -public export -get : StateC t -> IO (Maybe (State t)) +export +get : StateC t -> JS_IO (Maybe (State t)) get (MkStateC _ t p) = do True <- isObj p | False => pure Nothing pure $ Just $ MkState t p -public export -newState : (t : StateTy) -> interpSTy t -> IO (StateC t) +export +newState : (t : StateTy) -> interpSTy t -> JS_IO (StateC t) newState t v = do c <- getStateVar' n <- incCount c - p <- mkForeign (FFun "%0[%1] = {}" [FPtr,FInt] FPtr) c n + p <- foreign FFI_JS "%0[%1] = {}" (Ptr -> Int -> JS_IO Ptr) c n toState v (MkState t p) pure $ MkStateC n t p -public export -destroyState : StateC t -> IO () +export +destroyState : StateC t -> JS_IO () destroyState (MkStateC n _ _) = do c <- getStateVar' - mkForeign (FFun "delete %0[%1]" [FPtr,FInt] FUnit) c n + foreign FFI_JS "delete %0[%1]" (Ptr -> Int -> JS_IO ()) c n diff --git a/IQuery/Timeout.idr b/IQuery/Timeout.idr index 1657203..f086eed 100644 --- a/IQuery/Timeout.idr +++ b/IQuery/Timeout.idr @@ -1,18 +1,17 @@ module Timeout -%access public +%access export export data Timeout : Type where MkTimeout : Ptr -> Timeout -setTimeout : (() -> IO ()) -> Float -> IO Timeout +setTimeout : (() -> JS_IO ()) -> Double -> JS_IO Timeout setTimeout f t = do - e <- mkForeign ( - FFun "setTimeout(%0,%1)" [FFunction FUnit (FAny (IO ())), FFloat] FPtr - ) f t - return (MkTimeout e) + e <- foreign FFI_JS "setTimeout(%0,%1)" + (JsFn (() -> JS_IO ()) -> Double -> JS_IO Ptr) (MkJsFn f) t + pure (MkTimeout e) -clearTimeout : Timeout -> IO () +clearTimeout : Timeout -> JS_IO () clearTimeout (MkTimeout p) = - mkForeign (FFun "clearTimeout(%0)" [FPtr] FUnit) p + foreign FFI_JS "clearTimeout(%0)" (Ptr -> JS_IO ()) p diff --git a/example/state.idr b/example/state.idr index 6149616..6e32ddf 100644 --- a/example/state.idr +++ b/example/state.idr @@ -2,7 +2,7 @@ module Main import IQuery -push : StateC (STList STString) -> Event -> IO Int +push : StateC (STList STString) -> Event -> JS_IO Int push s e = do Just input <- query "input#pushVal" >>= (\x => elemAt x 0) Just xs <- get s =>> fromState @@ -10,30 +10,30 @@ push s e = do get s :=> toState (text :: xs) pure 1 -shift : StateC (STList STString) -> Event -> IO Int +shift : StateC (STList STString) -> Event -> JS_IO Int shift s e = do Just x <- get s =>> access 0 =>> fromState | Nothing => do - alert "stack is empty" + alert "stack is empty" pure 1 alert x Just (_::xs) <- get s =>> fromState get s :=> toState xs pure 1 -setV : Event -> IO Int +setV : Event -> JS_IO Int setV e = do Just el <- !(query "input#val") `elemAt` 0 setValue el "wohoo" pure 1 - -main : IO () + +main : JS_IO () main = do queue <- newState (STList STString) Nil Just p <- !(query "input#pushAct") `elemAt` 0 - onClick p (push queue) + onClick p (push queue) Just s <- !(query "input#shiftAct") `elemAt` 0 - onClick s (shift queue) + onClick s (shift queue) Just sv <- !(query "input#setVal") `elemAt` 0 - onClick sv setV + onClick sv setV pure () From ab39ad0813f6f71d94b56089b41765ad940aa2bf Mon Sep 17 00:00:00 2001 From: Brandon Dyck Date: Sun, 14 Jan 2018 15:07:36 -0700 Subject: [PATCH 3/3] qualify module declarations --- IQuery/Ajax.idr | 2 +- IQuery/Elements.idr | 2 +- IQuery/Event.idr | 4 ++-- IQuery/Interval.idr | 2 +- IQuery/Key.idr | 2 +- IQuery/State.idr | 2 +- IQuery/Timeout.idr | 2 +- 7 files changed, 8 insertions(+), 8 deletions(-) diff --git a/IQuery/Ajax.idr b/IQuery/Ajax.idr index b55f23e..7866046 100644 --- a/IQuery/Ajax.idr +++ b/IQuery/Ajax.idr @@ -1,4 +1,4 @@ -module Ajax +module IQuery.Ajax %access private diff --git a/IQuery/Elements.idr b/IQuery/Elements.idr index ab5d048..7c2037d 100644 --- a/IQuery/Elements.idr +++ b/IQuery/Elements.idr @@ -1,4 +1,4 @@ -module Elements +module IQuery.Elements import IQuery.Event diff --git a/IQuery/Event.idr b/IQuery/Event.idr index 779155c..2bbae40 100644 --- a/IQuery/Event.idr +++ b/IQuery/Event.idr @@ -1,6 +1,6 @@ -module Event +module IQuery.Event -import IQuery.Key +import public IQuery.Key %access export diff --git a/IQuery/Interval.idr b/IQuery/Interval.idr index cad79a9..f6453ab 100644 --- a/IQuery/Interval.idr +++ b/IQuery/Interval.idr @@ -1,4 +1,4 @@ -module Interval +module IQuery.Interval %access public export diff --git a/IQuery/Key.idr b/IQuery/Key.idr index f1ed1fa..efb719f 100644 --- a/IQuery/Key.idr +++ b/IQuery/Key.idr @@ -1,4 +1,4 @@ -module Key +module IQuery.Key %access public export diff --git a/IQuery/State.idr b/IQuery/State.idr index 5f54915..9052a40 100644 --- a/IQuery/State.idr +++ b/IQuery/State.idr @@ -1,4 +1,4 @@ -module State +module IQuery.State %access private diff --git a/IQuery/Timeout.idr b/IQuery/Timeout.idr index f086eed..0167f36 100644 --- a/IQuery/Timeout.idr +++ b/IQuery/Timeout.idr @@ -1,4 +1,4 @@ -module Timeout +module IQuery.Timeout %access export