fab5d73 · Idris-dev · git.iko.soy

.gitattributesnew file+1

compare with master

unifiedsplit

@@ -0,0 +1 @@

1+text=auto

.gitignore+1

@@ -4,5 +4,6 @@ cabal-dev/

4*.o

5*.a

6*.swp

7+*~

7test/output

8test/output

8test/test???/output

9test/test???/output

Setup.hs+14−7

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

1+{-# LANGUAGE CPP #-}

1import Distribution.Simple

2import Distribution.Simple

2import Distribution.Simple.InstallDirs as I

3import Distribution.Simple.InstallDirs as I

3import Distribution.Simple.LocalBuildInfo as L

4import Distribution.Simple.LocalBuildInfo as L

@@ -13,23 +14,31 @@ import System.Process

13

14

14make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make"

15make verbosity = P.runProgramInvocation verbosity . P.simpleProgramInvocation "make"

15

16

17+#ifdef mingw32_HOST_OS

18+-- make on mingw32 exepects unix style separators

19+idrisCmd local = "../dist/build/idris/idris"

20+#else

21+idrisCmd local = ".." </> buildDir local </> "idris" </> "idris"

22+#endif

23+

16cleanStdLib verbosity

24cleanStdLib verbosity

17 = make verbosity [ "-C", "lib", "clean" ]

25 = make verbosity [ "-C", "lib", "clean" ]

18

26

19installStdLib pkg local verbosity copy

27installStdLib pkg local verbosity copy

20 = do let dirs = L.absoluteInstallDirs pkg local copy

28 = do let dirs = L.absoluteInstallDirs pkg local copy

21 let idir = datadir dirs

29 let idir = datadir dirs

22− let icmd = ".." </> buildDir local </> "idris" </> "idris"

30+ let icmd = idrisCmd local

23 putStrLn $ "Installing libraries in " ++ idir

31 putStrLn $ "Installing libraries in " ++ idir

24 make verbosity

32 make verbosity

25 [ "-C", "lib", "install"

33 [ "-C", "lib", "install"

26 , "TARGET=" ++ idir

34 , "TARGET=" ++ idir

27 , "IDRIS=" ++ icmd

35 , "IDRIS=" ++ icmd

28 ]

36 ]

37+ let idirRts = idir </> "rts"

29− putStrLn $ "Installing run time system in " ++ idir ++ "/rts"

38+ putStrLn $ "Installing run time system in " ++ idirRts

30 make verbosity

39 make verbosity

31 [ "-C", "rts", "install"

40 [ "-C", "rts", "install"

32− , "TARGET=" ++ idir ++ "/rts"

41+ , "TARGET=" ++ idirRts

33 , "IDRIS=" ++ icmd

42 , "IDRIS=" ++ icmd

34 ]

43 ]

35

44

@@ -39,14 +48,14 @@ installStdLib pkg local verbosity copy

39-- the file after configure.

48-- the file after configure.

40

49

41removeLibIdris local verbosity

50removeLibIdris local verbosity

42− = do let icmd = ".." </> buildDir local </> "idris" </> "idris"

51+ = do let icmd = idrisCmd local

43 make verbosity

52 make verbosity

44 [ "-C", "rts", "clean"

53 [ "-C", "rts", "clean"

45 , "IDRIS=" ++ icmd

54 , "IDRIS=" ++ icmd

46 ]

55 ]

47

56

48checkStdLib local verbosity

57checkStdLib local verbosity

49− = do let icmd = ".." </> buildDir local </> "idris" </> "idris"

58+ = do let icmd = idrisCmd local

50 putStrLn $ "Building libraries..."

59 putStrLn $ "Building libraries..."

51 make verbosity

60 make verbosity

52 [ "-C", "lib", "check"

61 [ "-C", "lib", "check"

@@ -73,5 +82,3 @@ main = defaultMainWithHooks $ simpleUserHooks

73 , postBuild = \ _ flags _ lbi -> do

82 , postBuild = \ _ flags _ lbi -> do

74 checkStdLib lbi (S.fromFlag $ S.buildVerbosity flags)

83 checkStdLib lbi (S.fromFlag $ S.buildVerbosity flags)

75 }

84 }

76−

77−

idris.cabal+1−1

@@ -89,7 +89,7 @@ Executable idris

89 Paths_idris

90

91 Build-depends: base>=4 && <5, parsec, mtl, Cabal,

92− haskeline>=0.7,

92+ haskeline>=0.7, split,

93 containers, process, transformers, filepath,

94 directory, binary, bytestring, pretty

95

src/IRTS/CodegenC.hs+2−1

@@ -14,6 +14,7 @@ import System.Process

14import System.Exit

15import System.IO

16import System.Directory

17+import System.FilePath ((</>), (<.>))

17import Control.Monad

18import Control.Monad

18

19

19codegenC :: [(Name, SDecl)] ->

20codegenC :: [(Name, SDecl)] ->

@@ -30,7 +31,7 @@ codegenC defs out exec incs objs libs dbg

30 let h = concatMap toDecl (map fst bc)

31 let h = concatMap toDecl (map fst bc)

31 let cc = concatMap (uncurry toC) bc

32 let cc = concatMap (uncurry toC) bc

32 d <- getDataDir

33 d <- getDataDir

33− mprog <- readFile (d ++ "/rts/idris_main.c")

34+ mprog <- readFile (d </> "rts" </> "idris_main" <.> "c")

34 let cout = headers incs ++ debug dbg ++ h ++ cc ++

35 let cout = headers incs ++ debug dbg ++ h ++ cc ++

35 (if (exec == Executable) then mprog else "")

36 (if (exec == Executable) then mprog else "")

36 case exec of

37 case exec of

src/IRTS/Compiler.hs+2−1

@@ -23,6 +23,7 @@ import System.Process

23import System.IO

24import System.Directory

25import System.Environment

26+import System.FilePath ((</>), addTrailingPathSeparator)

26

27

27import Paths_idris

28import Paths_idris

28

29

@@ -72,7 +73,7 @@ compile target f tm

72 case idris_metavars i \\ primDefs of

73 case idris_metavars i \\ primDefs of

73 [] -> return ()

74 [] -> return ()

74 ms -> fail $ "There are undefined metavariables: " ++ show ms

75 ms -> fail $ "There are undefined metavariables: " ++ show ms

75− inDir d h = do let f = d ++ "/" ++ h

76+ inDir d h = do let f = d </> h

76 ex <- doesFileExist f

77 ex <- doesFileExist f

77 if ex then return f else return h

78 if ex then return f else return h

78 mkObj f = f ++ " "

79 mkObj f = f ++ " "

src/Idris/Imports.hs+4−4

@@ -29,9 +29,9 @@ ibcPath :: FilePath -> Bool -> FilePath -> FilePath

29ibcPath ibcsd use_ibcsd fp = let (d_fp, n_fp) = splitFileName fp

30 d = if (not use_ibcsd) || ibcsd == ""

31 then d_fp

32− else d_fp ++ ibcsd ++ "/"

32+ else d_fp </> ibcsd

33 n = dropExtension n_fp

34− in d ++ n ++ ".ibc"

34+ in d </> n <.> "ibc"

35

36ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath

37ibcPathWithFallback ibcsd fp = do let ibcp = ibcPath ibcsd True fp

@@ -45,7 +45,7 @@ ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp

45

46findImport :: [FilePath] -> FilePath -> FilePath -> IO IFileType

47findImport [] ibcsd fp = fail $ "Can't find import " ++ fp

48−findImport (d:ds) ibcsd fp = do let fp_full = d ++ "/" ++ fp

48+findImport (d:ds) ibcsd fp = do let fp_full = d </> fp

49 ibcp <- ibcPathWithFallback ibcsd fp_full

50 let idrp = srcPath fp_full

51 let lidrp = lsrcPath fp_full

@@ -68,7 +68,7 @@ findImport (d:ds) ibcsd fp = do let fp_full = d ++ "/" ++ fp

68

69findInPath :: [FilePath] -> FilePath -> IO FilePath

70findInPath [] fp = fail $ "Can't find file " ++ fp

71−findInPath (d:ds) fp = do let p = d ++ "/" ++ fp

71+findInPath (d:ds) fp = do let p = d </> fp

72 e <- doesFileExist p

73 if e then return p else findInPath ds p

74

src/Idris/Parser.hs+4−6

@@ -25,6 +25,7 @@ import Text.Parsec.String

25import qualified Text.Parsec.Token as PTok

26

27import Data.List

28+import Data.List.Split(splitOn)

28import Control.Monad.State

29import Control.Monad.State

29import Debug.Trace

30import Debug.Trace

30import Data.Maybe

31import Data.Maybe

@@ -255,16 +256,13 @@ notEndBlock = do ist <- getState

255pfc :: IParser FC

256pfc :: IParser FC

256pfc = do s <- getPosition

257pfc = do s <- getPosition

257 let (dir, file) = splitFileName (sourceName s)

258 let (dir, file) = splitFileName (sourceName s)

258− let f = case dir of

259+ let f = if dir == addTrailingPathSeparator "." then file else sourceName s

259− "./" -> file

260− _ -> sourceName s

261 return $ FC f (sourceLine s)

260 return $ FC f (sourceLine s)

262

261

263pImport :: IParser String

262pImport :: IParser String

264pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')

263pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')

265− return (map dot f)

264+ return (toPath f)

266− where dot '.' = '/'

265+ where toPath n = foldl1 (</>) $ splitOn "." n

267− dot c = c

268

266

269-- a program is a list of declarations, possibly with associated

267-- a program is a list of declarations, possibly with associated

270-- documentation strings

268-- documentation strings

src/Idris/REPL.hs+1−1

@@ -548,7 +548,7 @@ idrisMain opts =

548

549 addPkgDir :: String -> Idris ()

550 addPkgDir p = do ddir <- liftIO $ getDataDir

551− addImportDir (ddir ++ "/" ++ p)

551+ addImportDir (ddir </> p)

552

553getFile :: Opt -> Maybe String

554getFile (Filename str) = Just str

src/Idris/REPLParser.hs+5−3

@@ -1,5 +1,7 @@

1module Idris.REPLParser(parseCmd) where

2

3+import System.FilePath ((</>))

4+

3import Idris.Parser

5import Idris.Parser

4import Idris.AbsSyntax

6import Idris.AbsSyntax

5import Core.TT

7import Core.TT

@@ -11,6 +13,7 @@ import qualified Text.ParserCombinators.Parsec.Token as PTok

11

13

12import Debug.Trace

14import Debug.Trace

13import Data.List

15import Data.List

16+import Data.List.Split(splitOn)

14

17

15parseCmd i = runParser pCmd i "(input)"

18parseCmd i = runParser pCmd i "(input)"

16

19

@@ -24,7 +27,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

24 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

27 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

25 <|> try (do cmd ["r", "reload"]; eof; return Reload)

28 <|> try (do cmd ["r", "reload"]; eof; return Reload)

26 <|> try (do cmd ["m", "module"]; f <- identifier; eof;

29 <|> try (do cmd ["m", "module"]; f <- identifier; eof;

27− return (ModImport (map dot f)))

30+ return (ModImport (toPath f)))

28 <|> try (do cmd ["e", "edit"]; eof; return Edit)

31 <|> try (do cmd ["e", "edit"]; eof; return Edit)

29 <|> try (do cmd ["exec", "execute"]; eof; return Execute)

32 <|> try (do cmd ["exec", "execute"]; eof; return Execute)

30 <|> try (do cmd ["ttshell"]; eof; return TTShell)

33 <|> try (do cmd ["ttshell"]; eof; return TTShell)

@@ -59,8 +62,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

59 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

62 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

60 <|> do eof; return NOP

63 <|> do eof; return NOP

61

64

62− where dot '.' = '/'

65+ where toPath n = foldl1 (</>) $ splitOn "." n

63− dot c = c

64

66

65pOption :: IParser Opt

67pOption :: IParser Opt

66pOption = do discard (symbol "errorcontext"); return ErrContext

68pOption = do discard (symbol "errorcontext"); return ErrContext

src/Main.hs+4−3

@@ -4,6 +4,7 @@ import System.Console.Haskeline

4import System.IO

5import System.Environment

6import System.Exit

7+import System.FilePath ((</>), addTrailingPathSeparator)

7

8

8import Data.Maybe

9import Data.Maybe

9import Data.Version

10import Data.Version

@@ -60,15 +61,15 @@ showver = do putStrLn $ "Idris version " ++ ver

60 exitWith ExitSuccess

61 exitWith ExitSuccess

61

62

62showLibs = do dir <- getDataDir

63showLibs = do dir <- getDataDir

63− putStrLn $ "-L" ++ dir ++ "/rts -lidris_rts -lgmp -lpthread"

64+ putStrLn $ "-L" ++ (dir </> "rts") ++ " -lidris_rts -lgmp -lpthread"

64 exitWith ExitSuccess

65 exitWith ExitSuccess

65

66

66showLibdir = do dir <- getDataDir

67showLibdir = do dir <- getDataDir

67− putStrLn $ dir ++ "/"

68+ putStrLn $ addTrailingPathSeparator dir

68 exitWith ExitSuccess

69 exitWith ExitSuccess

69

70

70showIncs = do dir <- getDataDir

71showIncs = do dir <- getDataDir

71− putStrLn $ "-I" ++ dir ++ "/rts"

72+ putStrLn $ "-I" ++ dir </> "rts"

72 exitWith ExitSuccess

73 exitWith ExitSuccess

73

74

74usagemsg = "Idris version " ++ ver ++ "\n" ++

75usagemsg = "Idris version " ++ ver ++ "\n" ++

src/Pkg/Package.hs+17−24

@@ -4,11 +4,13 @@ import System.Process

4import System.Directory

5import System.Exit

6import System.IO

7+import System.FilePath ((</>), addTrailingPathSeparator)

7

8

8import Util.System

9import Util.System

9

10

10import Control.Monad

11import Control.Monad

11import Data.List

12import Data.List

13+import Data.List.Split(splitOn)

12

14

13import Core.TT

15import Core.TT

14import Idris.REPL

16import Idris.REPL

@@ -32,14 +34,14 @@ buildPkg warnonly (install, fp)

32 when (and ok) $

34 when (and ok) $

33 do make (makefile pkgdesc)

35 do make (makefile pkgdesc)

34 dir <- getCurrentDirectory

36 dir <- getCurrentDirectory

35− setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc

37+ setCurrentDirectory $ dir </> sourcedir pkgdesc

36 case (execout pkgdesc) of

38 case (execout pkgdesc) of

37 Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)

39 Nothing -> buildMods (NoREPL : Verbose : idris_opts pkgdesc)

38 (modules pkgdesc)

40 (modules pkgdesc)

39− Just o -> do let exec = dir ++ "/" ++ o

41+ Just o -> do let exec = dir </> o

40− buildMod

42+ buildMods

41 (NoREPL : Verbose : Output exec : idris_opts pkgdesc)

43 (NoREPL : Verbose : Output exec : idris_opts pkgdesc)

42− (idris_main pkgdesc)

44+ [idris_main pkgdesc]

43 setCurrentDirectory dir

45 setCurrentDirectory dir

44 when install $ installPkg pkgdesc

46 when install $ installPkg pkgdesc

45

47

@@ -48,11 +50,11 @@ cleanPkg fp

48 = do pkgdesc <- parseDesc fp

50 = do pkgdesc <- parseDesc fp

49 clean (makefile pkgdesc)

51 clean (makefile pkgdesc)

50 dir <- getCurrentDirectory

52 dir <- getCurrentDirectory

51− setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc

53+ setCurrentDirectory $ dir </> sourcedir pkgdesc

52 mapM_ rmIBC (modules pkgdesc)

54 mapM_ rmIBC (modules pkgdesc)

53 case execout pkgdesc of

55 case execout pkgdesc of

54 Nothing -> return ()

56 Nothing -> return ()

55− Just s -> do let exec = dir ++ "/" ++ s

57+ Just s -> do let exec = dir </> s

56 putStrLn $ "Removing " ++ exec

58 putStrLn $ "Removing " ++ exec

57 system $ "rm -f " ++ exec

59 system $ "rm -f " ++ exec

58 return ()

60 return ()

@@ -60,25 +62,17 @@ cleanPkg fp

60installPkg :: PkgDesc -> IO ()

62installPkg :: PkgDesc -> IO ()

61installPkg pkgdesc

63installPkg pkgdesc

62 = do dir <- getCurrentDirectory

64 = do dir <- getCurrentDirectory

63− setCurrentDirectory $ dir ++ "/" ++ sourcedir pkgdesc

65+ setCurrentDirectory $ dir </> sourcedir pkgdesc

64 case (execout pkgdesc) of

66 case (execout pkgdesc) of

65 Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)

67 Nothing -> mapM_ (installIBC (pkgname pkgdesc)) (modules pkgdesc)

66 Just o -> return () -- do nothing, keep executable locally, for noe

68 Just o -> return () -- do nothing, keep executable locally, for noe

67 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

69 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

68

70

69−buildMod :: [Opt] -> Name -> IO ()

70−buildMod opts n = do let f = map slash $ show n

71− idris (Filename f : opts)

72− return ()

73− where slash '.' = '/'

74− slash x = x

75−

76buildMods :: [Opt] -> [Name] -> IO ()

71buildMods :: [Opt] -> [Name] -> IO ()

77−buildMods opts ns = do let f = map ((map slash) . show) ns

72+buildMods opts ns = do let f = map (toPath . show) ns

78 idris (map Filename f ++ opts)

73 idris (map Filename f ++ opts)

79 return ()

74 return ()

80− where slash '.' = '/'

75+ where toPath n = foldl1 (</>) $ splitOn "." n

81− slash x = x

82

76

83testLib :: Bool -> String -> String -> IO Bool

77testLib :: Bool -> String -> String -> IO Bool

84testLib warn p f

78testLib warn p f

@@ -86,7 +80,8 @@ testLib warn p f

86 gcc <- getCC

80 gcc <- getCC

87 (tmpf, tmph) <- tempfile

81 (tmpf, tmph) <- tempfile

88 hClose tmph

82 hClose tmph

83+ let libtest = d </> "rts" </> "libtest.c"

89− e <- system $ gcc ++ " " ++ d ++ "/rts/libtest.c -l" ++ f ++ " -o " ++ tmpf

84+ e <- system $ gcc ++ " " ++ libtest ++ " -l" ++ f ++ " -o " ++ tmpf

90 case e of

85 case e of

91 ExitSuccess -> return True

86 ExitSuccess -> return True

92 _ -> do if warn

87 _ -> do if warn

@@ -102,22 +97,22 @@ rmIBC m = do let f = toIBCFile m

102 return ()

97 return ()

103

98

104toIBCFile (UN n) = n ++ ".ibc"

99toIBCFile (UN n) = n ++ ".ibc"

105−toIBCFile (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ toIBCFile n

100+toIBCFile (NS n ns) = foldl1 (</>) (reverse (toIBCFile n : ns))

106

101

107installIBC :: String -> Name -> IO ()

102installIBC :: String -> Name -> IO ()

108installIBC p m = do let f = toIBCFile m

103installIBC p m = do let f = toIBCFile m

109 d <- getDataDir

104 d <- getDataDir

110− let destdir = d ++ "/" ++ p ++ "/" ++ getDest m

105+ let destdir = d </> p </> getDest m

111 putStrLn $ "Installing " ++ f ++ " to " ++ destdir

106 putStrLn $ "Installing " ++ f ++ " to " ++ destdir

112 system $ "mkdir -p " ++ destdir

107 system $ "mkdir -p " ++ destdir

113 system $ "install " ++ f ++ " " ++ destdir

108 system $ "install " ++ f ++ " " ++ destdir

114 return ()

109 return ()

115 where getDest (UN n) = ""

110 where getDest (UN n) = ""

116− getDest (NS n ns) = concat (intersperse "/" (reverse ns)) ++ "/" ++ getDest n

111+ getDest (NS n ns) = foldl1 (</>) (reverse (getDest n : ns))

117

112

118installObj :: String -> String -> IO ()

113installObj :: String -> String -> IO ()

119installObj p o = do d <- getDataDir

114installObj p o = do d <- getDataDir

120− let destdir = d ++ "/" ++ p ++ "/"

115+ let destdir = addTrailingPathSeparator (d </> p)

121 putStrLn $ "Installing " ++ o ++ " to " ++ destdir

116 putStrLn $ "Installing " ++ o ++ " to " ++ destdir

122 system $ "mkdir -p " ++ destdir

117 system $ "mkdir -p " ++ destdir

123 system $ "install " ++ o ++ " " ++ destdir

118 system $ "install " ++ o ++ " " ++ destdir

@@ -133,5 +128,3 @@ clean Nothing = return ()

133clean (Just s) = do system $ "make -f " ++ s ++ " clean"

128clean (Just s) = do system $ "make -f " ++ s ++ " clean"

134 return ()

129 return ()

135

130

136−

137−

src/RTS/CodegenC.hs+2−1

@@ -17,6 +17,7 @@ import System.Process

17import System.IO

18import System.Directory

19import System.Environment

20+import System.FilePath ((</>))

20import Debug.Trace

21import Debug.Trace

21

22

22import Paths_idris

23import Paths_idris

@@ -44,7 +45,7 @@ compileC f tm

44 case idris_metavars i \\ primDefs of

45 case idris_metavars i \\ primDefs of

45 [] -> return ()

46 [] -> return ()

46 ms -> fail $ "There are undefined metavariables: " ++ show ms

47 ms -> fail $ "There are undefined metavariables: " ++ show ms

47− inDir d h = do let f = d ++ "/" ++ h

48+ inDir d h = do let f = d </> h

48 ex <- doesFileExist f

49 ex <- doesFileExist f

49 if ex then return f else return h

50 if ex then return f else return h

50

51