535d77b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add --ibcsubdir option

(thanks to Dirk Ullrich)

commit535d77b34125b8b5a924d105c64a44f569464086 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 30 Mar 2012, 13:19 (15 years ago) parent6c08816

5 files changed+75−34

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+12−2 src/Idris/IBC.hs+5−3 src/Idris/Imports.hs+38−22 src/Idris/Parser.hs+4−2 src/Main.hs+16−5

src/Idris/AbsSyntax.hs+12−2

@@ -28,11 +28,12 @@ data IOption = IOption { opt_logLevel :: Int,

2828 opt_coverage :: Bool,

2929 opt_showimp :: Bool,

3030 opt_repl :: Bool,

31− opt_verbose :: Bool

31+ opt_verbose :: Bool,

32+ opt_ibcsubdir :: FilePath

3233 }

3334 deriving (Show, Eq)

3435

35−defaultOpts = IOption 0 False False True False True True

36+defaultOpts = IOption 0 False False True False True True ""

3637

3738-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

3839-- without typechecking).

@@ -317,6 +318,15 @@ setCoverage t = do i <- get

317318 let opt' = opts { opt_coverage = t }

318319 put (i { idris_options = opt' })

319320

321+setIBCSubDir :: FilePath -> Idris ()

322+setIBCSubDir fp = do i <- get

323+ let opts = idris_options i

324+ let opt' = opts { opt_ibcsubdir =fp }

325+ put (i { idris_options = opt' })

326+

327+valIBCSubDir :: IState -> Idris FilePath

328+valIBCSubDir i = return (opt_ibcsubdir (idris_options i))

329+

320330impShow :: Idris Bool

321331impShow = do i <- get

322332 return (opt_showimp (idris_options i))

src/Idris/IBC.hs+5−3

@@ -64,7 +64,8 @@ writeIBC src f

6464 (_:_) -> fail "Can't write ibc when there are unsolved metavariables"

6565 [] -> return ()

6666 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

67− idrisCatch (do liftIO $ encodeFile f ibcf

67+ idrisCatch (do liftIO $ createDirectoryIfMissing True (dropFileName f)

68+ liftIO $ encodeFile f ibcf

6869 iLOG "Written")

6970 (\c -> do iLOG $ "Failed " ++ show c)

7071 return ()

@@ -155,8 +156,9 @@ timestampOlder src ibc = do srct <- getModificationTime src

155156pImports :: [FilePath] -> Idris ()

156157pImports fs

157158 = do datadir <- liftIO $ getDataDir

158− mapM_ (\f -> do fp <- liftIO $ findImport [".", datadir] f

159− i <- getIState

159+ mapM_ (\f -> do i <- getIState

160+ ibcsd <- valIBCSubDir i

161+ fp <- liftIO $ findImport [".", datadir] ibcsd f

160162 if (f `elem` imported i)

161163 then iLOG $ "Already read " ++ f

162164 else do putIState (i { imported = f : imported i })

src/Idris/Imports.hs+38−22

@@ -25,28 +25,44 @@ lsrcPath fp = let (n, ext) = splitExtension fp in

2525 _ -> fp ++ ".lidr"

2626

2727-- Get name of byte compiled version of an import

28−ibcPath :: FilePath -> FilePath

29−ibcPath fp = let (n, ext) = splitExtension fp in

30− n ++ ".ibc"

31−

32−findImport :: [FilePath] -> FilePath -> IO IFileType

33−findImport [] fp = fail $ "Can't find import " ++ fp

34−findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)

35− let idrp = srcPath (d ++ "/" ++ fp)

36− let lidrp = lsrcPath (d ++ "/" ++ fp)

37− ibc <- doesFileExist ibcp

38− idr <- doesFileExist idrp

39− lidr <- doesFileExist lidrp

40−-- when idr $ putStrLn $ idrp ++ " ok"

41−-- when lidr $ putStrLn $ lidrp ++ " ok"

42−-- when ibc $ putStrLn $ ibcp ++ " ok"

43− let isrc = if lidr then LIDR lidrp

44− else IDR idrp

45− if ibc

46− then return (IBC ibcp isrc)

47− else if (idr || lidr)

48− then return isrc

49− else findImport ds fp

28+ibcPath :: FilePath -> Bool -> FilePath -> FilePath

29+ibcPath 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 ++ "/"

33+ n = dropExtension n_fp

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

35+

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

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

38+ ibc <- doesFileExist ibcp

39+ return (if ibc

40+ then ibcp

41+ else ibcPath ibcsd False fp)

42+

43+ibcPathNoFallback :: FilePath -> FilePath -> FilePath

44+ibcPathNoFallback ibcsd fp = ibcPath ibcsd True fp

45+

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

47+findImport [] ibcsd fp = fail $ "Can't find import " ++ 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

52+ ibc <- doesFileExist ibcp

53+ idr <- doesFileExist idrp

54+ lidr <- doesFileExist lidrp

55+-- when idr $ putStrLn $ idrp ++ " ok"

56+-- when lidr $ putStrLn $ lidrp ++ " ok"

57+-- when ibc $ putStrLn $ ibcp ++ " ok"

58+ let isrc = if lidr

59+ then LIDR lidrp

60+ else IDR idrp

61+ if ibc

62+ then return (IBC ibcp isrc)

63+ else if (idr || lidr)

64+ then return isrc

65+ else findImport ds ibcsd fp

5066

5167-- find a specific filename somewhere in a path

5268

src/Idris/Parser.hs+4−2

@@ -58,8 +58,9 @@ lchar = lexeme.char

5858loadModule :: FilePath -> Idris String

5959loadModule f

6060 = idrisCatch (do datadir <- liftIO $ getDataDir

61− fp <- liftIO $ findImport [".", datadir] f

6261 i <- getIState

62+ ibcsd <- valIBCSubDir i

63+ fp <- liftIO $ findImport [".", datadir] ibcsd f

6364 if (f `elem` imported i)

6465 then iLOG $ "Already read " ++ f

6566 else do putIState (i { imported = f : imported i })

@@ -104,7 +105,8 @@ loadSource lidr f

104105 i <- get

105106 mapM_ checkDeclTotality (idris_totcheck i)

106107 iLOG ("Finished " ++ f)

107− let ibc = dropExtension f ++ ".ibc"

108+ ibcsd <- valIBCSubDir i

109+ let ibc = ibcPathNoFallback ibcsd f

108110 iucheck

109111 i <- getIState

110112 addHides (hide_list i)

src/Main.hs+16−5

@@ -40,6 +40,7 @@ data Opt = Filename String

4040 | TypeInType

4141 | NoCoverage

4242 | Verbose

43+ | IBCSubDir String

4344 deriving Eq

4445

4546main = do xs <- getArgs

@@ -51,12 +52,16 @@ runIdris opts =

5152 do let inputs = opt getFile opts

5253 let runrepl = not (NoREPL `elem` opts)

5354 let output = opt getOutput opts

55+ let ibcsubdir = opt getIBCSubDir opts

5456 when (Ver `elem` opts) $ liftIO showver

5557 when (Usage `elem` opts) $ liftIO usage

5658 setREPL runrepl

5759 setVerbose runrepl

5860 when (Verbose `elem` opts) $ setVerbose True

5961 mapM_ makeOption opts

62+ case ibcsubdir of

63+ [] -> setIBCSubDir ""

64+ (d:_) -> setIBCSubDir d

6065 elabPrims

6166 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

6267 return ()

@@ -85,6 +90,10 @@ getOutput :: Opt -> Maybe String

8590getOutput (Output str) = Just str

8691getOutput _ = Nothing

8792

93+getIBCSubDir :: Opt -> Maybe String

94+getIBCSubDir (IBCSubDir str) = Just str

95+getIBCSubDir _ = Nothing

96+

8897opt :: (Opt -> Maybe a) -> [Opt] -> [a]

8998opt = mapMaybe

9099

@@ -106,6 +115,7 @@ parseArgs ("--nocoverage":ns) = liftM (NoCoverage : ) (parseArgs ns)

106115parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

107116parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

108117parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)

118+parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)

109119parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

110120

111121ver = showVersion version

@@ -120,9 +130,10 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

120130 "--------------" ++ map (\x -> '-') ver ++ "\n" ++

121131 "Usage: idris [input file] [options]\n" ++

122132 "Options:\n" ++

123− "\t--check Type check only\n" ++

124− "\t-o [file] Generate executable\n" ++

125− "\t--noprelude Don't import the prelude\n" ++

126− "\t--typeintype Disable universe checking\n" ++

127− "\t--log [level] Set debugging log level\n"

133+ "\t--check Type check only\n" ++

134+ "\t-o [file] Generate executable\n" ++

135+ "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++

136+ "\t--noprelude Don't import the prelude\n" ++

137+ "\t--typeintype Disable universe checking\n" ++

138+ "\t--log [level] Set debugging log level\n"

128139