git.iko.soy/Idris-dev
on master help sign in
Merge commit '06fffa315afc0d883f36a6ce971df1123aa6d8e3' into javascript

Conflicts: src/IRTS/Compiler.hs src/Idris/AbsSyntaxTree.hs src/Main.hs

commit12dcee503d93aab5ae942e3a4f25a027a7e34de3 authorIrene Knapp <irene.knapp@icloud.com> dateThu 20 Dec 2012, 07:23 (14 years ago) parent11dbfc006fffa3
7 files changed+67−1
compare with master
unifiedsplit
src/IRTS/CodegenJavaScript.hs+59 src/IRTS/Compiler.hs+2 src/IRTS/LParser.hs+1 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/REPL.hs+2 src/Idris/REPLParser.hs+1 src/Main.hs+1
src/IRTS/CodegenJavaScript.hsnew file+59
@@ -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
99import IRTS.CodegenC
1010import IRTS.CodegenJava
1111import IRTS.DumpBC
12+import IRTS.CodegenJavaScript
1213import IRTS.Inliner
1314
1415import Idris.AbsSyntax
@@ -70,6 +71,7 @@ compile target f tm
7071 (concatMap mkLib libs) NONE
7172 ViaJava -> liftIO $ codegenJava c f outty
7273 Bytecode -> liftIO $ dumpBC c f
74+ ToJavaScript -> liftIO $ codegenJavaScript c f outty
7375 Error e -> fail $ show e
7476 where checkMVs = do i <- get
7577 case idris_metavars i \\ primDefs of
src/IRTS/LParser.hs+1
@@ -9,6 +9,7 @@ import IRTS.Bytecode
99import IRTS.CodegenCommon
1010import IRTS.CodegenC
1111import IRTS.CodegenJava
12+import IRTS.CodegenJavaScript
1213import IRTS.Defunctionalise
1314import Paths_idris
1415
src/Idris/AbsSyntaxTree.hs+1−1
@@ -140,7 +140,7 @@ type Idris = StateT IState (InputT IO)
140140
141141-- Commands in the REPL
142142
143−data Target = ViaC | ViaJava | Bytecode
143+data Target = ViaC | ViaJava | Bytecode | ToJavaScript
144144 deriving (Show, Eq)
145145
146146data Command = Quit
src/Idris/REPL.hs+2
@@ -429,6 +429,7 @@ parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)
429429parseArgs ("--check":ns) = NoREPL : (parseArgs ns)
430430parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)
431431parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)
432+parseArgs ("--javascript":ns) = UseTarget ToJavaScript : (parseArgs ns)
432433parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)
433434parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)
434435parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)
@@ -478,6 +479,7 @@ help =
478479 ([":showproof"], "<name>", "Show proof"),
479480 ([":proofs"], "", "Show available proofs"),
480481 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
482+ ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>"),
481483 ([":exec",":execute"], "", "Compile to an executable and run"),
482484 ([":?",":h",":help"], "", "Display this help text"),
483485 ([":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)
3333 <|> try (do cmd ["ttshell"]; eof; return TTShell)
3434 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))
3535 <|> 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))
3637 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))
3738 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
3839 <|> try (do cmd ["proofs"]; eof; return Proofs)
src/Main.hs+1
@@ -93,3 +93,4 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++
9393 "\t--link Show C library directories and exit (for C linking)\n" ++
9494 "\t--include Show C include directories and exit (for C linking)\n" ++
9595 "\t--target [target] Type the target: C, Java, bytecode\n"
96+ "\t--javascript Compile to JavaScript rather than to native code\n" ++