3c58071 · Idris-dev · git.iko.soy

Makefile+1

compare with master

unifiedsplit

@@ -19,6 +19,7 @@ test:

19relib:

20 make -C lib IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts clean

21 make -C effects IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean

22+ make -C javascript IDRIS=../dist/build/idris/idris RTS=../dist/build/rts/libidris_rts DIST=../dist/build clean

22 $(CABAL) install $(CABALFLAGS)

23 $(CABAL) install $(CABALFLAGS)

23

24

24linecount:

25linecount:

Setup.hs+10

@@ -38,6 +38,7 @@ rtsDir local = ".." </> buildDir local </> "rts" </> "libidris_rts"

38cleanStdLib verbosity

39 = do make verbosity [ "-C", "lib", "clean", "IDRIS=idris" ]

40 make verbosity [ "-C", "effects", "clean", "IDRIS=idris" ]

41+ make verbosity [ "-C", "javascript", "clean", "IDRIS=idris" ]

41

42

42cleanJavaLib verbosity

43cleanJavaLib verbosity

43 = do dirty <- doesDirectoryExist ("java" </> "target")

44 = do dirty <- doesDirectoryExist ("java" </> "target")

@@ -63,6 +64,11 @@ installStdLib pkg local withoutEffects verbosity copy

63 , "TARGET=" ++ idir

64 , "TARGET=" ++ idir

64 , "IDRIS=" ++ icmd

65 , "IDRIS=" ++ icmd

65 ]

66 ]

67+ make verbosity

68+ [ "-C", "javascript", "install"

69+ , "TARGET=" ++ idir

70+ , "IDRIS=" ++ icmd

71+ ]

66 let idirRts = idir </> "rts"

72 let idirRts = idir </> "rts"

67 putStrLn $ "Installing run time system in " ++ idirRts

73 putStrLn $ "Installing run time system in " ++ idirRts

68 make verbosity

74 make verbosity

@@ -109,6 +115,10 @@ checkStdLib local withoutEffects verbosity

109 [ "-C", "effects", "check"

115 [ "-C", "effects", "check"

110 , "IDRIS=" ++ icmd

116 , "IDRIS=" ++ icmd

111 ]

117 ]

118+ make verbosity

119+ [ "-C", "javascript", "check"

120+ , "IDRIS=" ++ icmd

121+ ]

112 make verbosity

122 make verbosity

113 [ "-C", "rts", "check"

123 [ "-C", "rts", "check"

114 , "IDRIS=" ++ icmd

124 , "IDRIS=" ++ icmd

idris.cabal+3

@@ -64,6 +64,9 @@ Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr

64 tutorial/examples/*.idr lib/base.ipkg

65 effects/Makefile effects/*.idr effects/Effect/*.idr

66 effects/effects.ipkg

67+ javascript/Makefile

68+ javascript/*.idr

69+ javascript/javascript.ipkg

67 config.mk

70 config.mk

68 rts/*.c rts/*.h rts/Makefile

71 rts/*.c rts/*.h rts/Makefile

69 js/*.js

72 js/*.js

javascript/JavaScript.idrnew file+101

@@ -0,0 +1,101 @@

1+module JavaScript

2+

3+%access public

4+

5+-- TODO: Get rid of this hack, and find a better way.

6+private

7+isUndefined : Ptr -> IO Bool

8+isUndefined p = do

9+ res <- mkForeign (

10+ FFun "(function(arg) { return arg === undefined;})" [FPtr] FString) p

11+ if res == "false"

12+ then (return False)

13+ else (return True)

14+

15+--------------------------------------------------------------------------------

16+-- Events

17+--------------------------------------------------------------------------------

18+abstract

19+data Event : Type where

20+ MkEvent : Ptr -> Event

21+

22+--------------------------------------------------------------------------------

23+-- Elements

24+--------------------------------------------------------------------------------

25+abstract

26+data Element : Type where

27+ MkElem : Ptr -> Element

28+

29+setText : Element -> String -> IO ()

30+setText (MkElem p) s =

31+ mkForeign (FFun ".textContent=" [FPtr, FString] FUnit) p s

32+

33+

34+setOnClick : Element -> (Event -> IO Bool) -> IO ()

35+setOnClick (MkElem e) f =

36+ mkForeign (

37+ FFun "['onclick']=" [ FPtr

38+ , FFunction (FAny Event) (FAny (IO Bool))

39+ ] FUnit) e f

40+--------------------------------------------------------------------------------

41+-- Nodelists

42+--------------------------------------------------------------------------------

43+abstract

44+data NodeList : Type where

45+ MkNodeList : Ptr -> NodeList

46+

47+elemAt : NodeList -> Nat -> IO (Maybe Element)

48+elemAt (MkNodeList p) i = do

49+ e <- mkForeign (FFun ".item" [FPtr, FInt] FPtr) p (cast i)

50+ d <- isUndefined e

51+ if d

52+ then return $ Just (MkElem e)

53+ else return Nothing

54+

55+--------------------------------------------------------------------------------

56+-- Intervals

57+--------------------------------------------------------------------------------

58+abstract

59+data Interval : Type where

60+ MkInterval : Ptr -> Interval

61+

62+setInterval : (() -> IO ()) -> Float -> IO Interval

63+setInterval f t = do

64+ e <- mkForeign (

65+ FFun "setInterval" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t

66+ return (MkInterval e)

67+

68+clearInterval : Interval -> IO ()

69+clearInterval (MkInterval p) =

70+ mkForeign (FFun "clearInterval" [FPtr] FUnit) p

71+

72+--------------------------------------------------------------------------------

73+-- Timeouts

74+--------------------------------------------------------------------------------

75+data Timeout : Type where

76+ MkTimeout : Ptr -> Timeout

77+

78+setTimeout : (() -> IO ()) -> Float -> IO Timeout

79+setTimeout f t = do

80+ e <- mkForeign (

81+ FFun "setTimeout" [FFunction FUnit (FAny (IO ())), FFloat] FPtr) f t

82+ return (MkTimeout e)

83+

84+clearTimeout : Timeout -> IO ()

85+clearTimeout (MkTimeout p) =

86+ mkForeign (FFun "clearTimeout" [FPtr] FUnit) p

87+

88+--------------------------------------------------------------------------------

89+-- Basic IO

90+--------------------------------------------------------------------------------

91+alert : String -> IO ()

92+alert msg =

93+ mkForeign (FFun "alert" [FString] FUnit) msg

94+

95+--------------------------------------------------------------------------------

96+-- DOM

97+--------------------------------------------------------------------------------

98+query : String -> IO NodeList

99+query q = do

100+ e <- mkForeign (FFun "document.querySelectorAll" [FString] FPtr) q

101+ return (MkNodeList e)

javascript/JavaScript/JSON.idrnew file+46

@@ -0,0 +1,46 @@

1+module JSON

2+

3+import Data.SortedMap

4+

5+data JSONType : Type where

6+ JSONArray : (n : Nat) -> Vect JSONType n -> JSONType

7+ JSONString : JSONType

8+ JSONNumber : JSONType

9+ JSONBool : JSONType

10+ JSONObject : SortedMap String JSONType -> JSONType

11+ JSONNull : JSONType

12+

13+mutual

14+ using (ts : Vect JSONType n, fs : SortedMap String JSONType)

15+ namespace JArray

16+ data JArray : (n : Nat) -> Vect JSONType n -> Type where

17+ Nil : JArray 0 []

18+ (::) : JSON t -> JArray n ts -> JArray (S n) (t :: ts)

19+

20+ namespace JObject

21+ data JObject : SortedMap String JSONType -> Type where

22+ Nil : JObject empty

23+ (::) : (f : (String, JSON t)) ->

24+ JObject fs ->

25+ JObject (insert (fst f) t fs)

26+

27+ data JSON : JSONType -> Type where

28+ JSString : String -> JSON JSONString

29+ JSNumber : Float -> JSON JSONNumber

30+ JSBool : Bool -> JSON JSONBool

31+ JSNull : JSON JSONNull

32+ JSArray : JArray n ts -> JSON (JSONArray n ts)

33+ JSObject : JObject fs -> JSON (JSONObject fs)

34+

35+index : (i : Fin n) -> JSON (JSONArray n ts) -> JSON (index i ts)

36+index fO (JSArray (x :: xs)) = x

37+index (fS i) (JSArray (x :: xs)) = index i (JSArray xs)

38+

39+infixl 8 ++

40+

41+(++) : JSON (JSONArray m ts1) ->

42+ JSON (JSONArray n ts2) ->

43+ JSON (JSONArray (m + n) (ts1 ++ ts2))

44+(++) (JSArray []) ys = ys

45+(++) (JSArray (x :: xs)) ys with ((JSArray xs) ++ ys)

46+ | (JSArray as) = JSArray (x :: as)

javascript/Makefilenew file+13

@@ -0,0 +1,13 @@

1+

2+check: .PHONY

3+ $(IDRIS) --build javascript.ipkg

4+

5+recheck: clean check

6+

7+install:

8+ $(IDRIS) --install javascript.ipkg

9+

10+clean: .PHONY

11+ $(IDRIS) --clean javascript.ipkg

12+

13+.PHONY:

javascript/javascript.ipkgnew file+5

@@ -0,0 +1,5 @@

1+package javascript

2+

3+opts = "-i ../lib"

4+modules = JavaScript, JavaScript.JSON

5+