2396796 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'javascript' of https://github.com/raichoo/Idris-dev into raichoo-javascript

Conflicts: CHANGELOG

commit2396796312b58bf30796072233937c136eed7d45 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 Feb 2013, 20:42 (14 years ago) parent12189d7 b2f2be4

13 files changed+52−32

compare with master

unifiedsplit

CHANGELOG+1 idris.cabal+3−1 js/Runtime-browser.js+3 js/Runtime.js → js/Runtime-common.js−14 js/Runtime-node.js+6 lib/Makefile+1−1 src/IRTS/CodegenJavaScript.hs+16−5 src/IRTS/Compiler.hs+13−7 src/Idris/AbsSyntaxTree.hs+5−1 src/Idris/REPL.hs+2−1 src/Idris/REPLParser.hs+1−1 src/Main.hs+1−1 tutorial/idris-tutorial.pdf

CHANGELOG+1

@@ -11,6 +11,7 @@ Internal changes:

1111 later information helps to resolve them

1212* Distinguishing parameters and indices in data types

1313* Faster termination/coverage checking

14+* Split 'javascript' target into 'javascript' and 'node'

1415

1516New in 0.9.6:

1617-------------

idris.cabal+3−1

@@ -47,7 +47,9 @@ Build-type: Custom

4747Data-files: rts/libidris_rts.a rts/idris_rts.h rts/idris_gc.h

4848 rts/idris_stdfgn.h rts/idris_main.c rts/idris_gmp.h

4949 rts/libtest.c

50− js/Runtime.js

50+ js/Runtime-common.js

51+ js/Runtime-node.js

52+ js/Runtime-browser.js

5153Extra-source-files: lib/Makefile lib/*.idr lib/Prelude/*.idr

5254 lib/Network/*.idr lib/Control/*.idr

5355 lib/Control/Monad/*.idr lib/Language/*.idr

js/Runtime-browser.jsnew file+3

@@ -0,0 +1,3 @@

1+__IDRRT__.print = function(s) {

2+ console.log(s);

3+};

js/Runtime.js → js/Runtime-common.jsrenamed−14

@@ -1,4 +1,3 @@

1−var require;

21var __IDRRT__ = {};

43/** @constructor */

@@ -38,19 +37,6 @@ __IDRRT__.tailcall = function(f) {

3837 }

3938};

4039

41−__IDRRT__.print = (function(){

42− if (require) {

43− var util = require('util');

44− return function(s) {

45− util.print(s);

46− };

47− } else {

48− return function(s) {

49− console.log(s);

50− };

51− }

52−})();

53−

5440/*

5541 BigInteger Javascript code taken from:

5642 https://github.com/peterolson

js/Runtime-node.jsnew file+6

@@ -0,0 +1,6 @@

1+__IDRRT__.print = (function() {

2+ var util = require('util');

3+ return function(s) {

4+ util.print(s);

5+ };

6+})();

lib/Makefile+1−1

@@ -11,6 +11,6 @@ clean: .PHONY

1111 $(IDRIS) --clean base.ipkg

1212

1313linecount: .PHONY

14− wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Control/Monad/*.idr

14+ wc -l *.idr Network/*.idr Language/*.idr Prelude/*.idr Data/*.idr Control/Monad/*.idr Control/*.idr

1515

1616.PHONY:

src/IRTS/CodegenJavaScript.hs+16−5

@@ -1,6 +1,6 @@

11{-# LANGUAGE PatternGuards #-}

3−module IRTS.CodegenJavaScript (codegenJavaScript) where

3+module IRTS.CodegenJavaScript (codegenJavaScript, JSTarget(..)) where

55import Idris.AbsSyntax

66import IRTS.Bytecode

@@ -20,15 +20,26 @@ import System.IO

2020idrNamespace :: String

2121idrNamespace = "__IDR__"

2222

23+data JSTarget = Node | JavaScript

24+

2325codegenJavaScript

24− :: [(Name, SDecl)]

26+ :: JSTarget

27+ -> [(Name, SDecl)]

2528 -> FilePath

2629 -> OutputType

2730 -> IO ()

28−codegenJavaScript definitions filename outputType = do

31+codegenJavaScript target definitions filename outputType = do

32+ let runtime = case target of

33+ Node -> "-node"

34+ JavaScript -> "-browser"

2935 path <- getDataDir

30− idrRuntime <- readFile (path ++ "/js/Runtime.js")

31− writeFile filename (idrRuntime ++ modules ++ functions ++ mainLoop)

36+ idrRuntime <- readFile $ path ++ "/js/Runtime-common.js"

37+ tgtRuntime <- readFile $ concat [path, "/js/Runtime", runtime, ".js"]

38+ writeFile filename (idrRuntime

39+ ++ tgtRuntime

40+ ++ modules

41+ ++ functions

42+ ++ mainLoop)

3243 where

3344 def = map (first translateNamespace) definitions

3445

src/IRTS/Compiler.hs+13−7

@@ -65,13 +65,19 @@ compile target f tm

6565 Just f -> liftIO $ writeFile f (dumpDefuns defuns)

6666 iLOG "Building output"

6767 case checked of

68− OK c -> case target of

69− ViaC -> liftIO $ codegenC c f outty hdrs

70− (concatMap mkObj objs)

71− (concatMap mkLib libs) NONE

72− ViaJava -> liftIO $ codegenJava c f outty

73− Bytecode -> liftIO $ dumpBC c f

74− ToJavaScript -> liftIO $ codegenJavaScript c f outty

68+ OK c -> liftIO $ case target of

69+ ViaC ->

70+ codegenC c f outty hdrs

71+ (concatMap mkObj objs)

72+ (concatMap mkLib libs) NONE

73+ ViaJava ->

74+ codegenJava c f outty

75+ ViaJavaScript ->

76+ codegenJavaScript JavaScript c f outty

77+ ViaNode ->

78+ codegenJavaScript Node c f outty

79+

80+ Bytecode -> dumpBC c f

7581 Error e -> fail $ show e

7682 where checkMVs = do i <- getIState

7783 case idris_metavars i \\ primDefs of

src/Idris/AbsSyntaxTree.hs+5−1

@@ -140,7 +140,11 @@ type Idris = StateT IState IO

140140

141141-- Commands in the REPL

142142

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

143+data Target = ViaC

144+ | ViaJava

145+ | ViaNode

146+ | ViaJavaScript

147+ | Bytecode

144148 deriving (Show, Eq)

145149

146150data Command = Quit

src/Idris/REPL.hs+2−1

@@ -423,7 +423,8 @@ parseTarget :: String -> Target

423423parseTarget "C" = ViaC

424424parseTarget "Java" = ViaJava

425425parseTarget "bytecode" = Bytecode

426−parseTarget "javascript" = ToJavaScript

426+parseTarget "javascript" = ViaJavaScript

427+parseTarget "node" = ViaNode

427428parseTarget _ = error "unknown target" -- FIXME: partial function

428429

429430parseArgs :: [String] -> [Opt]

src/Idris/REPLParser.hs+1−1

@@ -33,7 +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))

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

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

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

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

src/Main.hs+1−1

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

9292 "\t--libdir Show library install directory and exit\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" ++

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

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

tutorial/idris-tutorial.pdf

Binary file not shown.