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

git.iko.soy/Idris-dev

on master help sign in

Add --ibcsubdir option

535d77bEdwin Brady15 years ago

src/Idris/AbsSyntax.hs+12−2

compare with master

unifiedsplit

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

28 opt_coverage :: Bool,

29 opt_showimp :: Bool,

30 opt_repl :: Bool,

31− opt_verbose :: Bool

31+ opt_verbose :: Bool,

32+ opt_ibcsubdir :: FilePath

32 }

33 }

33 deriving (Show, Eq)

34 deriving (Show, Eq)

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

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

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

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

38-- without typechecking).

39-- without typechecking).

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

317 let opt' = opts { opt_coverage = t }

318 let opt' = opts { opt_coverage = t }

318 put (i { idris_options = opt' })

319 put (i { idris_options = opt' })

319

320

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+

320impShow :: Idris Bool

330impShow :: Idris Bool

321impShow = do i <- get

331impShow = do i <- get

322 return (opt_showimp (idris_options i))

332 return (opt_showimp (idris_options i))

src/Idris/IBC.hs+5−3

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

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

65 [] -> return ()

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

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

67− idrisCatch (do liftIO $ encodeFile f ibcf

68+ liftIO $ encodeFile f ibcf

68 iLOG "Written")

69 iLOG "Written")

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

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

70 return ()

71 return ()

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

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

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

156pImports fs

157pImports fs

157 = do datadir <- liftIO $ getDataDir

158 = do datadir <- liftIO $ getDataDir

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

160+ ibcsd <- valIBCSubDir i

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

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

159− i <- getIState

160 if (f `elem` imported i)

162 if (f `elem` imported i)

161 then iLOG $ "Already read " ++ f

163 then iLOG $ "Already read " ++ f

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

164 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

25 _ -> fp ++ ".lidr"

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

28−ibcPath :: FilePath -> FilePath

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

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

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

30− n ++ ".ibc"

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

31−

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+

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

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

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

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

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

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

49+ ibcp <- ibcPathWithFallback ibcsd fp_full

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

50+ let idrp = srcPath fp_full

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

51+ let lidrp = lsrcPath fp_full

37− ibc <- doesFileExist ibcp

52+ ibc <- doesFileExist ibcp

38− idr <- doesFileExist idrp

53+ idr <- doesFileExist idrp

39− lidr <- doesFileExist lidrp

54+ lidr <- doesFileExist lidrp

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

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

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

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

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

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

43− let isrc = if lidr then LIDR lidrp

58+ let isrc = if lidr

59+ then LIDR lidrp

44− else IDR idrp

60+ else IDR idrp

45− if ibc

61+ if ibc

46− then return (IBC ibcp isrc)

62+ then return (IBC ibcp isrc)

47− else if (idr || lidr)

63+ else if (idr || lidr)

48− then return isrc

64+ then return isrc

49− else findImport ds fp

65+ else findImport ds ibcsd fp

51-- find a specific filename somewhere in a path

67-- find a specific filename somewhere in a path

src/Idris/Parser.hs+4−2

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

58loadModule :: FilePath -> Idris String

59loadModule f

60 = idrisCatch (do datadir <- liftIO $ getDataDir

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

62 i <- getIState

61 i <- getIState

62+ ibcsd <- valIBCSubDir i

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

63 if (f `elem` imported i)

64 if (f `elem` imported i)

64 then iLOG $ "Already read " ++ f

65 then iLOG $ "Already read " ++ f

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

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

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

104 i <- get

105 i <- get

105 mapM_ checkDeclTotality (idris_totcheck i)

106 mapM_ checkDeclTotality (idris_totcheck i)

106 iLOG ("Finished " ++ f)

107 iLOG ("Finished " ++ f)

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

108+ ibcsd <- valIBCSubDir i

109+ let ibc = ibcPathNoFallback ibcsd f

108 iucheck

110 iucheck

109 i <- getIState

111 i <- getIState

110 addHides (hide_list i)

112 addHides (hide_list i)

src/Main.hs+16−5

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

40 | TypeInType

41 | NoCoverage

42 | Verbose

43+ | IBCSubDir String

43 deriving Eq

44 deriving Eq

45main = do xs <- getArgs

46main = do xs <- getArgs

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

51 do let inputs = opt getFile opts

52 do let inputs = opt getFile opts

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

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

53 let output = opt getOutput opts

54 let output = opt getOutput opts

55+ let ibcsubdir = opt getIBCSubDir opts

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

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

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

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

56 setREPL runrepl

58 setREPL runrepl

57 setVerbose runrepl

59 setVerbose runrepl

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

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

59 mapM_ makeOption opts

61 mapM_ makeOption opts

62+ case ibcsubdir of

63+ [] -> setIBCSubDir ""

64+ (d:_) -> setIBCSubDir d

60 elabPrims

65 elabPrims

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

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

62 return ()

67 return ()

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

85getOutput (Output str) = Just str

90getOutput (Output str) = Just str

86getOutput _ = Nothing

91getOutput _ = Nothing

93+getIBCSubDir :: Opt -> Maybe String

94+getIBCSubDir (IBCSubDir str) = Just str

95+getIBCSubDir _ = Nothing

96+

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

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

89opt = mapMaybe

98opt = mapMaybe

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

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

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

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

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

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

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

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

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

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

110

120

111ver = showVersion version

121ver = showVersion version

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

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

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

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

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

122 "Options:\n" ++

132 "Options:\n" ++

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

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

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

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

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

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

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

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

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

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

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

128

139