git.iko.soy/Idris-dev
on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commite4cf620eed28bed17f99cb671be3071730ac6611 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 31 Jan 2015, 12:30 (12 years ago) parent8096500d745c2e
9 files changed+49−24
compare with master
unifiedsplit
README.md+28−12 idris.cabal+3 src/IRTS/CodegenC.hs+1−1 src/Idris/Error.hs−1 src/Idris/Parser.hs+8−9 src/Idris/REPL.hs+2−1 test/interactive007/expected+1 test/interactive007/input+4 test/interactive007/run+2
README.md+28−12
@@ -7,14 +7,18 @@ Idris (http://idris-lang.org/) is a general-purpose functional programming
77language with dependent types.
88
99## Standard Installation Instructions
10−This repository represents the latest development version of the language, and may contain bugs that are being actively worked on.
11−For those who wish to use a more stable version of Idris please consider installing the latest version that has been released on Hackage.
10+This repository represents the latest development version of the language,
11+and may contain bugs that are being actively worked on.
12+For those who wish to use a more stable version of Idris please consider
13+installing the latest version that has been released on Hackage.
1214Installation instructions for various platforms can be [found on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installation-Instructions).
1315
1416## Installing Development Versions
1517
16−If you like to work against the latest development version, please consider using Cabal Sandboxes to minimise disruption to your local Haskell setup.
17−Instructions for install Idris HEAD within a cabal sandbox are [available on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installing-an-Idris-Development-version-in-a-sandbox).
18+If you like to work against the latest development version, please consider
19+using Cabal Sandboxes to minimise disruption to your local Haskell setup.
20+Instructions for installing Idris HEAD within a cabal sandbox are
21+[available on the Idris Wiki](https://github.com/idris-lang/Idris-dev/wiki/Installing-an-Idris-Development-version-in-a-sandbox).
1822
1923To configure, edit config.mk. The default values should work for most people.
2024
@@ -31,17 +35,21 @@ for the same architecture as your Haskell compiler (e.g. 64 bit libraries
3135for 64 bit ghc). By default, Idris builds without it. To build with it, pass
3236the flag `-f FFI`.
3337
34−To build with `libffi` by default, create a `custom.mk` file and add the following line to it:
38+To build with `libffi` by default, create a `custom.mk` file and add the
39+following line to it:
3540
3641`CABALFLAGS += -f FFI`
3742
3843The file custom.mk-alldeps is a suitable example.
3944
40−The continues integration builds on travis-ci.org are build using the ghc-flag -Werror. To enable this behaviour locally also, please compile using `make CI=true` or adding the following line into `custom.mk`:
45+The continuous integration builds on travis-ci.org are built using the
46+ghc-flag -Werror. To enable this behaviour locally also, please compile
47+using `make CI=true` or adding the following line into `custom.mk`:
4148
4249`CI = true`
4350
44−If you are only compiling for installing the most current version, you can ommit the CI flag, but please make sure you use it if you want to contribute.
51+If you are only compiling for installing the most current version, you can
52+omit the CI flag, but please make sure you use it if you want to contribute.
4553
4654## Code Generation
4755
@@ -49,13 +57,21 @@ Idris has support for external code generators. Supplied with the distribution
4957is a C code generator to compile executables, and a JavaScript code generator
5058with support for node.js and browser JavaScript.
5159
52−At this moment in time there are two external repositories with
53−a [Java code generator](https://github.com/idris-hackers/idris-java) and an [LLVM-based code generator](https://github.com/idris-hackers/idris-llvm).
60+At this moment in time there are two external repositories with a
61+[Java code generator](https://github.com/idris-hackers/idris-java) and an
62+[LLVM-based code generator](https://github.com/idris-hackers/idris-llvm).
5463
5564## More Information
5665
57−If you would like to find out more information, or ask questions, we currently have a [Wiki](https://github.com/idris-lang/Idris-dev/wiki); a [mailing list](https://groups.google.com/forum/#!forum/idris-lang), and an `IRC` channel `#idris` on freenode. To join the IRC channel, point your irc client to `chat.freenode.net` then `/join #idris`.
66+If you would like to find out more information, or ask questions, we
67+currently have a [Wiki](https://github.com/idris-lang/Idris-dev/wiki);
68+a [mailing list](https://groups.google.com/forum/#!forum/idris-lang),
69+and an `IRC` channel `#idris` on freenode. To join the IRC channel,
70+point your irc client to `chat.freenode.net` then `/join #idris`.
5871
59−For those further interested in using Idris for projects, the [Idris Hackers](https://github.com/idris-hackers) GitHub organisation is where some interesting projects are being hosted.
72+For those further interested in using Idris for projects, the
73+[Idris Hackers](https://github.com/idris-hackers) GitHub organisation is
74+where some interesting projects are being hosted.
6075
61−For those interested in contributing to Idris directly we kindly ask that prospective developers please consult [CONTRIBUTING.md] first.
76+For those interested in contributing to Idris directly we kindly ask that
77+prospective developers please consult the [Contributing Guide](CONTRIBUTING.md) first.
idris.cabal+3
@@ -455,6 +455,9 @@ Extra-source-files:
455455 test/interactive006/input
456456 test/interactive006/*.idr
457457 test/interactive006/expected
458+ test/interactive007/run
459+ test/interactive007/input
460+ test/interactive007/expected
458461
459462 test/io001/run
460463 test/io001/*.idr
src/IRTS/CodegenC.hs+1−1
@@ -69,7 +69,7 @@ codegenC' defs out exec incs objs libs flags dbg
6969 let args = [gccDbg dbg] ++
7070 gccFlags ++
7171 -- # Any flags defined here which alter the RTS API must also be added to config.mk
72− ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS",
72+ ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",
7373 "-I."] ++ objs ++ ["-x", "c"] ++
7474 (if (exec == Executable) then [] else ["-c"]) ++
7575 [tmpn] ++
src/Idris/Error.hs−1
@@ -5,7 +5,6 @@ module Idris.Error where
55import Prelude hiding (catch)
66import Idris.AbsSyntax
77import Idris.Delaborate
8−import Idris.Output
98
109import Idris.Core.Evaluate (ctxtAlist)
1110import Idris.Core.TT
src/Idris/Parser.hs+8−9
@@ -220,10 +220,10 @@ decl' syn = fixity
220220-}
221221syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
222222syntaxDecl syn = do s <- syntaxRule syn
223− i <- get
223+ i <- get
224224 put (i `addSyntax` s)
225225 fc <- getFC
226− return (PSyntax fc s)
226+ return (PSyntax fc s)
227227
228228-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
229229addSyntax :: IState -> Syntax -> IState
@@ -1210,14 +1210,14 @@ parseProg syn fname input mrk
12101210{- | Load idris module and show error if something wrong happens -}
12111211loadModule :: FilePath -> Idris (Maybe String)
12121212loadModule f
1213− = idrisCatch (fmap Just (loadModule' f))
1213+ = idrisCatch (loadModule' f)
12141214 (\e -> do setErrSpan (getErrSpan e)
12151215 ist <- getIState
12161216 iWarn (getErrSpan e) $ pprintErr ist e
12171217 return Nothing)
12181218
12191219{- | Load idris module -}
1220−loadModule' :: FilePath -> Idris String
1220+loadModule' :: FilePath -> Idris (Maybe String)
12211221loadModule' f
12221222 = do i <- getIState
12231223 let file = takeWhile (/= ' ') f
@@ -1225,7 +1225,8 @@ loadModule' f
12251225 ids <- allImportDirs
12261226 fp <- findImport ids ibcsd file
12271227 if file `elem` imported i
1228− then iLOG $ "Already read " ++ file
1228+ then do iLOG $ "Already read " ++ file
1229+ return Nothing
12291230 else do putIState (i { imported = file : imported i })
12301231 case fp of
12311232 IDR fn -> loadSource False fn Nothing
@@ -1236,9 +1237,7 @@ loadModule' f
12361237 case src of
12371238 IDR sfn -> loadSource False sfn Nothing
12381239 LIDR sfn -> loadSource True sfn Nothing)
1239− let (dir, fh) = splitFileName file
1240− return (dropExtension fh)
1241−
1240+ return $ Just file
12421241
12431242{- | Load idris code from file -}
12441243loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris ()
@@ -1277,7 +1276,7 @@ loadSource lidr f toline
12771276 let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in
12781277 ids <- allImportDirs
12791278 ibcsd <- valIBCSubDir i
1280− mapM_ (\(re, f) ->
1279+ mapM_ (\(re, f) ->
12811280 do fp <- findImport ids ibcsd f
12821281 case fp of
12831282 LIDR fn -> ifail $ "No ibc for " ++ f
src/Idris/REPL.hs+2−1
@@ -629,6 +629,7 @@ processInput cmd orig inputs efile
629629 Success (Right Reload) ->
630630 do putIState $ orig { idris_options = idris_options i
631631 , idris_colourTheme = idris_colourTheme i
632+ , imported = imported i
632633 }
633634 clearErr
634635 mods <- loadInputs inputs Nothing
@@ -1181,7 +1182,7 @@ process fn (SetConsoleWidth w) = setWidth w
11811182
11821183process fn (Apropos pkgs a) =
11831184 do orig <- getIState
1184− when (not (null pkgs)) $
1185+ when (not (null pkgs)) $
11851186 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs
11861187 mapM_ loadPkgIndex pkgs
11871188 ist <- getIState
test/interactive007/expectednew file+1
@@ -0,0 +1 @@
1+Idris> *Data/ZZ> *Data/ZZ> *Data/ZZ> *Data/ZZ> Bye bye
test/interactive007/inputnew file+4
@@ -0,0 +1,4 @@
1+:module Data.ZZ
2+:module Data.ZZ
3+:r
4+:module Data.ZZ
test/interactive007/runnew file+2
@@ -0,0 +1,2 @@
1+#!/usr/bin/env bash
2+idris --nobanner --nocolor < input