f08e412 · Idris-dev · git.iko.soy

codegen/idris-c/Main.hs → codegen/idris-codegen-c/Main.hsrenamed+14−9

compare with master

unifiedsplit

@@ -16,17 +16,21 @@ import Paths_idris

16

17import Util.System

18

19+data Opts = Opts { really :: Bool,

19−data Opts = Opts { inputs :: [FilePath],

20+ inputs :: [FilePath],

20 interface :: Bool,

21 interface :: Bool,

21 output :: FilePath }

22 output :: FilePath }

22

23

24+showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

25+ putStrLn "To call the code generator manually, pass the --yes-really option.\n"

23−showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"

26+ putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"

24 exitWith ExitSuccess

27 exitWith ExitSuccess

25

28

26getOpts :: IO Opts

29getOpts :: IO Opts

27getOpts = do xs <- getArgs

30getOpts = do xs <- getArgs

28− return $ process (Opts [] False "a.out") xs

31+ return $ process (Opts False [] False "a.out") xs

29 where

32 where

33+ process opts ("--yes-really":xs) = process (opts { really = True }) xs

30 process opts ("-o":o:xs) = process (opts { output = o }) xs

34 process opts ("-o":o:xs) = process (opts { output = o }) xs

31 process opts ("--interface":xs) = process (opts { interface = True }) xs

35 process opts ("--interface":xs) = process (opts { interface = True }) xs

32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

36 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

@@ -36,7 +40,7 @@ c_main :: Opts -> Idris ()

36c_main opts = do runIO setupBundledCC

40c_main opts = do runIO setupBundledCC

37 elabPrims

41 elabPrims

38 loadInputs (inputs opts) Nothing

42 loadInputs (inputs opts) Nothing

39− mainProg <- if interface opts

43+ mainProg <- if interface opts

40 then liftM Just elabMain

44 then liftM Just elabMain

41 else return Nothing

45 else return Nothing

42 ir <- compile (Via "c") (output opts) mainProg

46 ir <- compile (Via "c") (output opts) mainProg

@@ -44,9 +48,10 @@ c_main opts = do runIO setupBundledCC

44

48

45main :: IO ()

49main :: IO ()

46main = do opts <- getOpts

50main = do opts <- getOpts

47− if (null (inputs opts))

51+ if (null (inputs opts))

48 then showUsage

52 then showUsage

53+ else if (not $ really opts)

54+ then do putStrLn "This code generator is intended to be called by the Idris compiler. \

55+ \Please pass Idris the '--codegen' flag to choose a backend."

56+ exitWith ExitSuccess

49− else runMain (c_main opts)

57+ else runMain (c_main opts)

50−

51−

52−

codegen/idris-javascript/Main.hs → codegen/idris-codegen-javascript/Main.hsrenamed+12−4

@@ -13,17 +13,21 @@ import System.Exit

13

14import Paths_idris

15

16+data Opts = Opts { really :: Bool

16−data Opts = Opts { inputs :: [FilePath]

17+ , inputs :: [FilePath]

17 , output :: FilePath

18 , output :: FilePath

18 }

19 }

19

20

21+showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

22+ putStrLn "To call the code generator manually, pass the --yes-really option.\n"

20−showUsage = do putStrLn "Usage: idris-javascript <ibc-files> [-o <output-file>]"

23+ putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"

21 exitWith ExitSuccess

24 exitWith ExitSuccess

22

25

23getOpts :: IO Opts

26getOpts :: IO Opts

24getOpts = do xs <- getArgs

27getOpts = do xs <- getArgs

25− return $ process (Opts [] "main.js") xs

28+ return $ process (Opts False [] "main.js") xs

26 where

29 where

30+ process opts ("--yes-really":xs) = process (opts { really = True }) xs

27 process opts ("-o":o:xs) = process (opts { output = o }) xs

31 process opts ("-o":o:xs) = process (opts { output = o }) xs

28 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

29 process opts [] = opts

33 process opts [] = opts

@@ -39,4 +43,8 @@ main :: IO ()

39main = do opts <- getOpts

43main = do opts <- getOpts

40 if (null (inputs opts))

44 if (null (inputs opts))

41 then showUsage

45 then showUsage

46+ else if (not $ really opts)

47+ then do putStrLn "This code generator is intended to be called by the Idris compiler. \

48+ \Please pass Idris the '--codegen' flag to choose a backend."

49+ exitWith ExitSuccess

42− else runMain (jsMain opts)

50+ else runMain (jsMain opts)

codegen/idris-node/Main.hs → codegen/idris-codegen-node/Main.hsrenamed+12−4

@@ -13,17 +13,21 @@ import System.Exit

13

14import Paths_idris

15

16+data Opts = Opts { really :: Bool

16−data Opts = Opts { inputs :: [FilePath]

17+ , inputs :: [FilePath]

17 , output :: FilePath

18 , output :: FilePath

18 }

19 }

19

20

21+showUsage = do putStrLn "A code generator which is intended to be called by the compiler, not by a user."

22+ putStrLn "To call the code generator manually, pass the --yes-really option.\n"

20−showUsage = do putStrLn "Usage: idris-node <ibc-files> [-o <output-file>]"

23+ putStrLn "Usage: idris-codegen-c [--yes-really] <ibc-files> [-o <output-file>]"

21 exitWith ExitSuccess

24 exitWith ExitSuccess

22

25

23getOpts :: IO Opts

26getOpts :: IO Opts

24getOpts = do xs <- getArgs

27getOpts = do xs <- getArgs

25− return $ process (Opts [] "main.js") xs

28+ return $ process (Opts False [] "main.js") xs

26 where

29 where

30+ process opts ("--yes-really":xs) = process (opts { really = True }) xs

27 process opts ("-o":o:xs) = process (opts { output = o }) xs

31 process opts ("-o":o:xs) = process (opts { output = o }) xs

28 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

32 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

29 process opts [] = opts

33 process opts [] = opts

@@ -39,4 +43,8 @@ main :: IO ()

39main = do opts <- getOpts

43main = do opts <- getOpts

40 if (null (inputs opts))

44 if (null (inputs opts))

41 then showUsage

45 then showUsage

46+ else if (not $ really opts)

47+ then do putStrLn "This code generator is intended to be called by the Idris compiler. \

48+ \Please pass Idris the '--codegen' flag to choose a backend."

49+ exitWith ExitSuccess

42− else runMain (jsMain opts)

50+ else runMain (jsMain opts)

docs/proofs/interactive.rst+7−3

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

1−***************************

1+***************************************

2−Interactive Theorem Proving

2+DEPRECATED: Interactive Theorem Proving

3−***************************

3+***************************************

4+

5+.. warning::

6+ The interactive theorem-proving interface documented here has been

7+ deprecated in favor of :ref:`elaborator-reflection`.

4

8

5Idris also supports interactive theorem proving via tactics. This

9Idris also supports interactive theorem proving via tactics. This

6is generally not recommended to be used directly, but rather used as a

10is generally not recommended to be used directly, but rather used as a

docs/reference/elaborator-reflection.rst+2

@@ -1,3 +1,5 @@

1+.. _elaborator-reflection:

2+

1*********************

3*********************

2Elaborator Reflection

4Elaborator Reflection

3*********************

5*********************

idris.cabal+36−6

@@ -76,9 +76,23 @@ Data-files: idrisdoc/styles.css

76 rts/mini-gmp.h

77 rts/libtest.c

78

79+Extra-doc-files:

80+ CHANGELOG

81+ CITATION.md

82+ CONTRIBUTING.md

83+ CONTRIBUTORS

84+ README.md

85+ idris-tutorial.pdf

86+ man/idris.1

87+ samples/effects/*.idr

88+ samples/misc/*.idr

89+ samples/misc/*.lidr

90+ samples/tutorial/*.idr

91+

79Extra-source-files:

92Extra-source-files:

80 Makefile

93 Makefile

81 config.mk

94 config.mk

95+ stack.yaml

82

96

83 rts/*.c

97 rts/*.c

84 rts/*.h

98 rts/*.h

@@ -718,6 +732,22 @@ Extra-source-files:

718 test/docs003/*.idr

732 test/docs003/*.idr

719 test/docs003/expected

733 test/docs003/expected

720

734

735+ benchmarks/ALL

736+ benchmarks/*.pl

737+ benchmarks/README

738+

739+ benchmarks/fasta/fasta.idr

740+ benchmarks/fasta/fasta.ipkg

741+

742+ benchmarks/pidigits/pidigits.idr

743+ benchmarks/pidigits/pidigits.ipkg

744+

745+ benchmarks/quasigroups/board

746+ benchmarks/quasigroups/*.idr

747+ benchmarks/quasigroups/qgsolve.ipkg

748+

749+ benchmarks/trivial/sortvec.idr

750+ benchmarks/trivial/sortvec.ipkg

721

751

722source-repository head

752source-repository head

723 type: git

753 type: git

@@ -964,9 +994,9 @@ Executable idris

964 ghc-prof-options: -auto-all -caf-all

994 ghc-prof-options: -auto-all -caf-all

965 ghc-options: -threaded -rtsopts -funbox-strict-fields

995 ghc-options: -threaded -rtsopts -funbox-strict-fields

966

996

967−Executable idris-c

997+Executable idris-codegen-c

968 Main-is: Main.hs

998 Main-is: Main.hs

969− hs-source-dirs: codegen/idris-c

999+ hs-source-dirs: codegen/idris-codegen-c

970

1000

971 Build-depends: idris

1001 Build-depends: idris

972 , base

1002 , base

@@ -977,9 +1007,9 @@ Executable idris-c

977 ghc-prof-options: -auto-all -caf-all

1007 ghc-prof-options: -auto-all -caf-all

978 ghc-options: -threaded -rtsopts -funbox-strict-fields

1008 ghc-options: -threaded -rtsopts -funbox-strict-fields

979

1009

980−Executable idris-javascript

1010+Executable idris-codegen-javascript

981 Main-is: Main.hs

1011 Main-is: Main.hs

982− hs-source-dirs: codegen/idris-javascript

1012+ hs-source-dirs: codegen/idris-codegen-javascript

983

1013

984 Build-depends: idris

1014 Build-depends: idris

985 , base

1015 , base

@@ -990,9 +1020,9 @@ Executable idris-javascript

990 ghc-prof-options: -auto-all -caf-all

1020 ghc-prof-options: -auto-all -caf-all

991 ghc-options: -threaded -rtsopts -funbox-strict-fields

1021 ghc-options: -threaded -rtsopts -funbox-strict-fields

992

1022

993−Executable idris-node

1023+Executable idris-codegen-node

994 Main-is: Main.hs

1024 Main-is: Main.hs

995− hs-source-dirs: codegen/idris-node

1025+ hs-source-dirs: codegen/idris-codegen-node

996

1026

997 Build-depends: idris

1027 Build-depends: idris

998 , base

1028 , base

src/IRTS/Compiler.hs+2−2

@@ -135,8 +135,8 @@ generate codegen mainmod ir

135 -- Built-in code generators (FIXME: lift these out!)

136 Via "c" -> codegenC ir

137 -- Any external code generator

138− Via cg -> do let cmd = "idris-" ++ cg

138+ Via cg -> do let cmd = "idris-codegen-" ++ cg

139− args = [mainmod, "-o", outputFile ir] ++ compilerFlags ir

139+ args = ["--yes-really", mainmod, "-o", outputFile ir] ++ compilerFlags ir

140 exit <- rawSystem cmd args

141 when (exit /= ExitSuccess) $

142 putStrLn ("FAILURE: " ++ show cmd ++ " " ++ show args)