2396796 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

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

11 later information helps to resolve them

12* Distinguishing parameters and indices in data types

13* Faster termination/coverage checking

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

14

15

15New in 0.9.6:

16New in 0.9.6:

16-------------

17-------------

idris.cabal+3−1

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

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

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

49 rts/libtest.c

50− js/Runtime.js

50+ js/Runtime-common.js

51+ js/Runtime-node.js

52+ js/Runtime-browser.js

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

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

52 lib/Network/*.idr lib/Control/*.idr

54 lib/Network/*.idr lib/Control/*.idr

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

55 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;

2var __IDRRT__ = {};

1var __IDRRT__ = {};

3

2

4/** @constructor */

3/** @constructor */

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

38 }

37 }

39};

38};

40

39

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−

54/*

40/*

55 BigInteger Javascript code taken from:

41 BigInteger Javascript code taken from:

56 https://github.com/peterolson

42 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

11 $(IDRIS) --clean base.ipkg

12

13linecount: .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

15

16.PHONY:

src/IRTS/CodegenJavaScript.hs+16−5

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

1{-# LANGUAGE PatternGuards #-}

2

3−module IRTS.CodegenJavaScript (codegenJavaScript) where

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

4

5import Idris.AbsSyntax

6import IRTS.Bytecode

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

20idrNamespace :: String

21idrNamespace = "__IDR__"

22

23+data JSTarget = Node | JavaScript

24+

23codegenJavaScript

25codegenJavaScript

26+ :: JSTarget

24− :: [(Name, SDecl)]

27+ -> [(Name, SDecl)]

25 -> FilePath

28 -> FilePath

26 -> OutputType

29 -> OutputType

27 -> IO ()

30 -> 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"

29 path <- getDataDir

35 path <- getDataDir

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

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

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

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

38+ writeFile filename (idrRuntime

39+ ++ tgtRuntime

40+ ++ modules

41+ ++ functions

42+ ++ mainLoop)

32 where

43 where

33 def = map (first translateNamespace) definitions

44 def = map (first translateNamespace) definitions

34

45

src/IRTS/Compiler.hs+13−7

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

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

66 iLOG "Building output"

67 case checked of

68− OK c -> case target of

68+ OK c -> liftIO $ case target of

69+ ViaC ->

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

70+ codegenC c f outty hdrs

70− (concatMap mkObj objs)

71+ (concatMap mkObj objs)

71− (concatMap mkLib libs) NONE

72+ (concatMap mkLib libs) NONE

73+ ViaJava ->

72− ViaJava -> liftIO $ codegenJava c f outty

74+ codegenJava c f outty

75+ ViaJavaScript ->

76+ codegenJavaScript JavaScript c f outty

77+ ViaNode ->

78+ codegenJavaScript Node c f outty

79+

73− Bytecode -> liftIO $ dumpBC c f

80+ Bytecode -> dumpBC c f

74− ToJavaScript -> liftIO $ codegenJavaScript c f outty

75 Error e -> fail $ show e

81 Error e -> fail $ show e

76 where checkMVs = do i <- getIState

82 where checkMVs = do i <- getIState

77 case idris_metavars i \\ primDefs of

83 case idris_metavars i \\ primDefs of

src/Idris/AbsSyntaxTree.hs+5−1

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

140

141-- Commands in the REPL

142

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

143+data Target = ViaC

144+ | ViaJava

145+ | ViaNode

146+ | ViaJavaScript

147+ | Bytecode

144 deriving (Show, Eq)

148 deriving (Show, Eq)

145

149

146data Command = Quit

150data Command = Quit

src/Idris/REPL.hs+2−1

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

423parseTarget "C" = ViaC

424parseTarget "Java" = ViaJava

425parseTarget "bytecode" = Bytecode

426−parseTarget "javascript" = ToJavaScript

426+parseTarget "javascript" = ViaJavaScript

427+parseTarget "node" = ViaNode

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

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

428

429

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

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

src/Idris/REPLParser.hs+1−1

@@ -33,7 +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 ["js", "javascript"]; f <- identifier; eof; return (Compile ViaJavaScript f))

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

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

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

src/Main.hs+1−1

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

92 "\t--libdir Show library install directory and exit\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, javascript\n"

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

tutorial/idris-tutorial.pdf

Binary file not shown.