fab5d73 · Idris-dev · git.iko.soy

.gitattributesnew file+1

@@ -0,0 +1 @@

1+text=auto

.gitignore+1

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

44*.o

55*.a

66*.swp

7+*~

78test/output

89test/test???/output

Setup.hs+14−7

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

1+{-# LANGUAGE CPP #-}

12import Distribution.Simple

23import Distribution.Simple.InstallDirs as I

34import Distribution.Simple.LocalBuildInfo as L

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

1314

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

1516

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+

1624cleanStdLib verbosity

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

1826

1927installStdLib pkg local verbosity copy

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

2129 let idir = datadir dirs

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

30+ let icmd = idrisCmd local

2331 putStrLn $ "Installing libraries in " ++ idir

2432 make verbosity

2533 [ "-C", "lib", "install"

2634 , "TARGET=" ++ idir

2735 , "IDRIS=" ++ icmd

2836 ]

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

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

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

3039 make verbosity

3140 [ "-C", "rts", "install"

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

41+ , "TARGET=" ++ idirRts

3342 , "IDRIS=" ++ icmd

3443 ]

3544

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

3948-- the file after configure.

4049

4150removeLibIdris local verbosity

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

51+ = do let icmd = idrisCmd local

4352 make verbosity

4453 [ "-C", "rts", "clean"

4554 , "IDRIS=" ++ icmd

4655 ]

4756

4857checkStdLib local verbosity

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

58+ = do let icmd = idrisCmd local

5059 putStrLn $ "Building libraries..."

5160 make verbosity

5261 [ "-C", "lib", "check"

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

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

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

7584 }

76−

77−

idris.cabal+1−1

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

8989 Paths_idris

9090

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

92− haskeline>=0.7,

92+ haskeline>=0.7, split,

9393 containers, process, transformers, filepath,

9494 directory, binary, bytestring, pretty

9595

src/IRTS/CodegenC.hs+2−1

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

1414import System.Exit

1515import System.IO

1616import System.Directory

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

1718import Control.Monad

1819

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

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

3031 let h = concatMap toDecl (map fst bc)

3132 let cc = concatMap (uncurry toC) bc

3233 d <- getDataDir

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

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

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

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

3637 case exec of

src/IRTS/Compiler.hs+2−1

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

2323import System.IO

2424import System.Directory

2525import System.Environment

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

2627

2728import Paths_idris

2829

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

7273 case idris_metavars i \\ primDefs of

7374 [] -> return ()

7475 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

7677 ex <- doesFileExist f

7778 if ex then return f else return h

7879 mkObj f = f ++ " "

src/Idris/Imports.hs+4−4

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

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

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

3131 then d_fp

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

32+ else d_fp </> ibcsd

3333 n = dropExtension n_fp

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

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

3535

3636ibcPathWithFallback :: FilePath -> FilePath -> IO FilePath

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

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

4545

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

4747findImport [] 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

4949 ibcp <- ibcPathWithFallback ibcsd fp_full

5050 let idrp = srcPath fp_full

5151 let lidrp = lsrcPath fp_full

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

6868

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

7070findInPath [] 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

7272 e <- doesFileExist p

7373 if e then return p else findInPath ds p

7474

src/Idris/Parser.hs+4−6

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

2525import qualified Text.Parsec.Token as PTok

2626

2727import Data.List

28+import Data.List.Split(splitOn)

2829import Control.Monad.State

2930import Debug.Trace

3031import Data.Maybe

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

255256pfc :: IParser FC

256257pfc = do s <- getPosition

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

258− let f = case dir of

259− "./" -> file

260− _ -> sourceName s

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

261260 return $ FC f (sourceLine s)

262261

263262pImport :: IParser String

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

265− return (map dot f)

266− where dot '.' = '/'

267− dot c = c

264+ return (toPath f)

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

268266

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

270268-- documentation strings

src/Idris/REPL.hs+1−1

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

548548

549549 addPkgDir :: String -> Idris ()

550550 addPkgDir p = do ddir <- liftIO $ getDataDir

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

551+ addImportDir (ddir </> p)

552552

553553getFile :: Opt -> Maybe String

554554getFile (Filename str) = Just str

src/Idris/REPLParser.hs+5−3

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

11module Idris.REPLParser(parseCmd) where

22

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

4+

35import Idris.Parser

46import Idris.AbsSyntax

57import Core.TT

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

1113

1214import Debug.Trace

1315import Data.List

16+import Data.List.Split(splitOn)

1417

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

1619

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

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

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

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

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

30+ return (ModImport (toPath f)))

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

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

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

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

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

6063 <|> do eof; return NOP

6164

62− where dot '.' = '/'

63− dot c = c

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

6466

6567pOption :: IParser Opt

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

src/Main.hs+4−3

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

44import System.IO

55import System.Environment

66import System.Exit

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

78

89import Data.Maybe

910import Data.Version

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

6061 exitWith ExitSuccess

6162

6263showLibs = do dir <- getDataDir

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

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

6465 exitWith ExitSuccess

6566

6667showLibdir = do dir <- getDataDir

67− putStrLn $ dir ++ "/"

68+ putStrLn $ addTrailingPathSeparator dir

6869 exitWith ExitSuccess

6970

7071showIncs = do dir <- getDataDir

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

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

7273 exitWith ExitSuccess

7374

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

src/Pkg/Package.hs+17−24

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

44import System.Directory

55import System.Exit

66import System.IO

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

78

89import Util.System

910

1011import Control.Monad

1112import Data.List

13+import Data.List.Split(splitOn)

1214

1315import Core.TT

1416import Idris.REPL

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

3234 when (and ok) $

3335 do make (makefile pkgdesc)

3436 dir <- getCurrentDirectory

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

37+ setCurrentDirectory $ dir </> sourcedir pkgdesc

3638 case (execout pkgdesc) of

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

3840 (modules pkgdesc)

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

40− buildMod

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

42+ buildMods

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

42− (idris_main pkgdesc)

44+ [idris_main pkgdesc]

4345 setCurrentDirectory dir

4446 when install $ installPkg pkgdesc

4547

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

4850 = do pkgdesc <- parseDesc fp

4951 clean (makefile pkgdesc)

5052 dir <- getCurrentDirectory

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

53+ setCurrentDirectory $ dir </> sourcedir pkgdesc

5254 mapM_ rmIBC (modules pkgdesc)

5355 case execout pkgdesc of

5456 Nothing -> return ()

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

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

5658 putStrLn $ "Removing " ++ exec

5759 system $ "rm -f " ++ exec

5860 return ()

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

6062installPkg :: PkgDesc -> IO ()

6163installPkg pkgdesc

6264 = do dir <- getCurrentDirectory

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

65+ setCurrentDirectory $ dir </> sourcedir pkgdesc

6466 case (execout pkgdesc) of

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

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

6769 mapM_ (installObj (pkgname pkgdesc)) (objs pkgdesc)

6870

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−

7671buildMods :: [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

7873 idris (map Filename f ++ opts)

7974 return ()

80− where slash '.' = '/'

81− slash x = x

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

8276

8377testLib :: Bool -> String -> String -> IO Bool

8478testLib warn p f

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

8680 gcc <- getCC

8781 (tmpf, tmph) <- tempfile

8882 hClose tmph

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

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

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

9085 case e of

9186 ExitSuccess -> return True

9287 _ -> do if warn

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

10297 return ()

10398

10499toIBCFile (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))

106101

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

108103installIBC p m = do let f = toIBCFile m

109104 d <- getDataDir

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

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

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

112107 system $ "mkdir -p " ++ destdir

113108 system $ "install " ++ f ++ " " ++ destdir

114109 return ()

115110 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))

117112

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

119114installObj p o = do d <- getDataDir

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

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

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

122117 system $ "mkdir -p " ++ destdir

123118 system $ "install " ++ o ++ " " ++ destdir

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

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

134129 return ()

135130

136−

137−

src/RTS/CodegenC.hs+2−1

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

1717import System.IO

1818import System.Directory

1919import System.Environment

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

2021import Debug.Trace

2122

2223import Paths_idris

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

4445 case idris_metavars i \\ primDefs of

4546 [] -> return ()

4647 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

4849 ex <- doesFileExist f

4950 if ex then return f else return h

5051