12dcee5 · Idris-dev · git.iko.soy

src/IRTS/CodegenJavaScript.hsnew file+59

compare with master

unifiedsplit

@@ -0,0 +1,59 @@

1+module IRTS.CodegenJavaScript (codegenJavaScript ) where

2+

3+import Idris.AbsSyntax

4+import IRTS.Bytecode

5+import IRTS.Lang

6+import IRTS.Simplified

7+import IRTS.CodegenCommon

8+import Core.TT

9+import Paths_idris

10+import Util.System

11+

12+import Data.Char

13+import Data.List

14+import System.IO

15+

16+codegenJavaScript

17+ :: [(Name, SDecl)]

18+ -> FilePath

19+ -> OutputType

20+ -> IO ()

21+codegenJavaScript definitions filename outputType = do

22+ let body = concat $ map (translateDeclaration . snd) definitions

23+ output = concat [header, body, footer]

24+ writeFile filename output

25+

26+

27+header :: String

28+header =

29+ concat $ map (\line -> line ++ "\n")

30+ ["define(function(require) {",

31+ "var m = {};"]

32+

33+

34+footer :: String

35+footer =

36+ concat $ map (\line -> line ++ "\n")

37+ ["return m;",

38+ "});"]

39+

40+

41+translateName :: Name -> String

42+translateName = show

43+

44+

45+translateDeclaration :: SDecl -> String

46+translateDeclaration (SFun name parameterNames stackSize body) =

47+ concat ["m[\"", translateName name, "\"] = function(s) { ",

48+ translateExpression body, " ",

49+ intercalate " " $ take (length parameterNames) $ repeat "s.pop();",

50+ " };\n"]

51+

52+

53+translateExpression :: SExp -> String

54+translateExpression (SLet name value body) =

55+ intercalate " "

56+ $ [translateExpression value,

57+ translateExpression body,

58+ "s.pop();", "s.pop();"]

59+translateExpression _ = "..."

src/IRTS/Compiler.hs+2

@@ -9,6 +9,7 @@ import IRTS.CodegenCommon

9import IRTS.CodegenC

10import IRTS.CodegenJava

11import IRTS.DumpBC

12+import IRTS.CodegenJavaScript

12import IRTS.Inliner

13import IRTS.Inliner

13

14

14import Idris.AbsSyntax

15import Idris.AbsSyntax

@@ -70,6 +71,7 @@ compile target f tm

70 (concatMap mkLib libs) NONE

71 (concatMap mkLib libs) NONE

71 ViaJava -> liftIO $ codegenJava c f outty

72 ViaJava -> liftIO $ codegenJava c f outty

72 Bytecode -> liftIO $ dumpBC c f

73 Bytecode -> liftIO $ dumpBC c f

74+ ToJavaScript -> liftIO $ codegenJavaScript c f outty

73 Error e -> fail $ show e

75 Error e -> fail $ show e

74 where checkMVs = do i <- get

76 where checkMVs = do i <- get

75 case idris_metavars i \\ primDefs of

77 case idris_metavars i \\ primDefs of

src/IRTS/LParser.hs+1

@@ -9,6 +9,7 @@ import IRTS.Bytecode

9import IRTS.CodegenCommon

10import IRTS.CodegenC

11import IRTS.CodegenJava

12+import IRTS.CodegenJavaScript

12import IRTS.Defunctionalise

13import IRTS.Defunctionalise

13import Paths_idris

14import Paths_idris

14

15

src/Idris/AbsSyntaxTree.hs+1−1

@@ -140,7 +140,7 @@ type Idris = StateT IState (InputT IO)

140

141-- Commands in the REPL

142

143−data Target = ViaC | ViaJava | Bytecode

143+data Target = ViaC | ViaJava | Bytecode | ToJavaScript

144 deriving (Show, Eq)

145

146data Command = Quit

src/Idris/REPL.hs+2

@@ -429,6 +429,7 @@ parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

429parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

430parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)

431parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)

432+parseArgs ("--javascript":ns) = UseTarget ToJavaScript : (parseArgs ns)

432parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

433parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

433parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

434parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

434parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

435parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

@@ -478,6 +479,7 @@ help =

478 ([":showproof"], "<name>", "Show proof"),

479 ([":showproof"], "<name>", "Show proof"),

479 ([":proofs"], "", "Show available proofs"),

480 ([":proofs"], "", "Show available proofs"),

480 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

481 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

482+ ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>"),

481 ([":exec",":execute"], "", "Compile to an executable and run"),

483 ([":exec",":execute"], "", "Compile to an executable and run"),

482 ([":?",":h",":help"], "", "Display this help text"),

484 ([":?",":h",":help"], "", "Display this help text"),

483 ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),

485 ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),

src/Idris/REPLParser.hs+1

@@ -33,6 +33,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

33 <|> try (do cmd ["ttshell"]; eof; return TTShell)

34 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))

35 <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))

36+ <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ToJavaScript f))

36 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

37 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

37 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

38 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

38 <|> try (do cmd ["proofs"]; eof; return Proofs)

39 <|> try (do cmd ["proofs"]; eof; return Proofs)

src/Main.hs+1

@@ -93,3 +93,4 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

93 "\t--link Show C library directories and exit (for C linking)\n" ++

94 "\t--include Show C include directories and exit (for C linking)\n" ++

95 "\t--target [target] Type the target: C, Java, bytecode\n"

96+ "\t--javascript Compile to JavaScript rather than to native code\n" ++