f08e412 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge branch 'master' of github.com:idris-lang/Idris-dev

commitf08e412b5028d190bbef567f761a42601252ea08 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 6 Sep 2015, 19:06 (11 years ago) parenteb38173 a0d8376

7 files changed+85−28

compare with master

unifiedsplit

codegen/idris-c/Main.hs → codegen/idris-codegen-c/Main.hs+14−9 codegen/idris-javascript/Main.hs → codegen/idris-codegen-javascript/Main.hs+12−4 codegen/idris-node/Main.hs → codegen/idris-codegen-node/Main.hs+12−4 docs/proofs/interactive.rst+7−3 docs/reference/elaborator-reflection.rst+2 idris.cabal+36−6 src/IRTS/Compiler.hs+2−2

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

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

1616

1717import Util.System

1818

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

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

20+ inputs :: [FilePath],

2021 interface :: Bool,

2122 output :: FilePath }

2223

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

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"

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

2427 exitWith ExitSuccess

2528

2629getOpts :: IO Opts

2730getOpts = do xs <- getArgs

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

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

2932 where

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

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

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

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

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

3640c_main opts = do runIO setupBundledCC

3741 elabPrims

3842 loadInputs (inputs opts) Nothing

39− mainProg <- if interface opts

43+ mainProg <- if interface opts

4044 then liftM Just elabMain

4145 else return Nothing

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

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

4448

4549main :: IO ()

4650main = do opts <- getOpts

47− if (null (inputs opts))

51+ if (null (inputs opts))

4852 then showUsage

49− else runMain (c_main opts)

50−

51−

52−

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

57+ else runMain (c_main opts)

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

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

1313

1414import Paths_idris

1515

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

16+data Opts = Opts { really :: Bool

17+ , inputs :: [FilePath]

1718 , output :: FilePath

1819 }

1920

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

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"

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

2124 exitWith ExitSuccess

2225

2326getOpts :: IO Opts

2427getOpts = do xs <- getArgs

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

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

2629 where

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

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

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

2933 process opts [] = opts

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

3943main = do opts <- getOpts

4044 if (null (inputs opts))

4145 then showUsage

42− else runMain (jsMain opts)

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

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

1313

1414import Paths_idris

1515

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

16+data Opts = Opts { really :: Bool

17+ , inputs :: [FilePath]

1718 , output :: FilePath

1819 }

1920

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

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"

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

2124 exitWith ExitSuccess

2225

2326getOpts :: IO Opts

2427getOpts = do xs <- getArgs

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

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

2629 where

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

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

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

2933 process opts [] = opts

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

3943main = do opts <- getOpts

4044 if (null (inputs opts))

4145 then showUsage

42− else runMain (jsMain opts)

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

50+ else runMain (jsMain opts)

docs/proofs/interactive.rst+7−3

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

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

2−Interactive Theorem Proving

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

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

2+DEPRECATED: Interactive Theorem Proving

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

5+.. warning::

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

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

59Idris also supports interactive theorem proving via tactics. This

610is 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:

13*********************

24Elaborator Reflection

35*********************

idris.cabal+36−6

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

7676 rts/mini-gmp.h

7777 rts/libtest.c

7878

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+

7992Extra-source-files:

8093 Makefile

8194 config.mk

95+ stack.yaml

8296

8397 rts/*.c

8498 rts/*.h

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

718732 test/docs003/*.idr

719733 test/docs003/expected

720734

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

721751

722752source-repository head

723753 type: git

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

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

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

966996

967−Executable idris-c

997+Executable idris-codegen-c

968998 Main-is: Main.hs

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

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

9701000

9711001 Build-depends: idris

9721002 , base

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

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

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

9791009

980−Executable idris-javascript

1010+Executable idris-codegen-javascript

9811011 Main-is: Main.hs

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

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

9831013

9841014 Build-depends: idris

9851015 , base

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

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

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

9921022

993−Executable idris-node

1023+Executable idris-codegen-node

9941024 Main-is: Main.hs

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

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

9961026

9971027 Build-depends: idris

9981028 , base

src/IRTS/Compiler.hs+2−2

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

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

136136 Via "c" -> codegenC ir

137137 -- Any external code generator

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

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

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

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

140140 exit <- rawSystem cmd args

141141 when (exit /= ExitSuccess) $

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