forked from luminousfennell/polybta
/
Shake.hs
256 lines (219 loc) · 9.37 KB
/
Shake.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
{-# LANGUAGE OverloadedStrings, RecordWildCards #-}
import Development.Shake hiding ((*>))
import Development.Shake.FilePath
import Control.Applicative
import Data.Maybe
import Data.Monoid
import Control.Exception
import Control.Monad
import qualified Data.List as List
import qualified Text.Regex.Applicative as Re
import qualified System.IO as Sys
import qualified System.Directory as Sys
import qualified System.Environment as Sys
import qualified Data.Char as Char
import qualified Data.ByteString as BS
import qualified Data.Text as Text
import qualified Data.Text.Encoding as Text
import qualified Options.Applicative as Opt
import Test.Tasty
import Test.Tasty.HUnit hiding (assert)
import Debug.Trace
-- TODO: Can we cope with modules in subdirectories?
-- TODO: changing the stdlib given at the command line should rebuild everything
-- TODO: add default include dirs?
-- TODO: allow for "--" separation of agda args and agda files?
-- -------------------------------------------------------------------
-- Types & Conversions
-- -------------------------------------------------------------------
type Module = String
moduleToTarget :: Module -> FilePath
moduleToTarget m = "_build" </> replace '.' '/' m <.> "want"
sourceToModule :: FilePath -> Module
sourceToModule src = assert (isRelative src) $ replace '/' '.' (dropExtension src)
-- -------------------------------------------------------------------
-- Constants
-- -------------------------------------------------------------------
-- Agda does not reliably produce output files, so we create dummy files with extension "wantedExt"
wantedExt :: String
wantedExt = ".want"
-- The directory for build files
buildDir :: FilePath
buildDir = "_build"
-- List of modules provided by agda's stdlib
-- TODO: find a way to read those from the actual stdlib dir
manualAgdaLibs :: [Module]
manualAgdaLibs =
[ "Data.Bool"
, "Data.Unit"
, "Category.Functor"
, "Relation.Binary.PropositionalEquality"
, "Relation.Nullary"
, "Relation.Binary"
, "Data.Empty"
, "Data.Sum"
, "Data.Product"
, "Data.List"
, "Data.Nat"
, "Function"
, "Data.Nat.Properties"
, "Algebra.FunctionProperties"
, "Data.Fin"
, "Level"
, "Category.Monad"
, "Data.Maybe"
, "Relation.Nullary.Decidable"
, "Data.Vec"
]
-- -------------------------------------------------------------------
-- Rules
-- -------------------------------------------------------------------
data PlanArgs = PlanArgs { pArg_ignored :: [Module]
, pArg_agdaArgs :: [String]
, pArg_sources :: [FilePath]
, pArg_root :: FilePath
}
plan :: PlanArgs -> Rules ()
plan PlanArgs{..} = do
let modules = map sourceToModule pArg_sources
want (wantedTargets modules)
(buildDir </> "*" <.> wantedExt) %> \out -> do
let sourceDir = takeDirectory out </> ".."
source = sourceDir </> takeFileName out -<.> "agda"
need [source]
listedDeps <- liftIO $ getDepModules source
let deps = wantedTargets listedDeps
need deps
command_ [] "agda" (source:pArg_agdaArgs)
liftIO $ writeFile out ""
return ()
where wantedTargets ms = [moduleToTarget m | m <- ms, (not (m `elem` pArg_ignored))]
-- -------------------------------------------------------------------
-- Commandline options
-- -------------------------------------------------------------------
data Opt = Opt { optSources :: [FilePath]
, optIncludes :: [FilePath]
}
deriving Show
getOpt :: IO Opt
getOpt = Opt.execParser (Opt.info (Opt.helper <*> parseOpt)
(Opt.fullDesc
<> Opt.progDesc "Build Agda sources with dependencies."))
where parseOpt :: Opt.Parser Opt
parseOpt = Opt
<$> many (Opt.strArgument (Opt.help "Source file"
<> Opt.metavar "FILE"))
<*> many (Opt.strOption (Opt.short 'i'
<> Opt.help "add directory to library path"
<> Opt.metavar "DIR"))
-- -------------------------------------------------------------------
-- Program
-- -------------------------------------------------------------------
main :: IO ()
main = do
Opt{..} <- getOpt
failingModules <- parseFailingModules <$> Sys.readFile "failing-modules.txt"
-- TODO: do not hard-code --allow-unsolved-metas
here <- Sys.getCurrentDirectory
let mkAbsolute p = if (isRelative p) then here </> p else p
let pArg_agdaArgs = concat [["-i", mkAbsolute i] | i <- optIncludes] ++ ["--allow-unsolved-metas"]
pArg_sources = map takeFileName optSources
pArg_ignored = manualAgdaLibs ++ failingModules
pArg_root = "."
shake shakeOptions (plan PlanArgs{..})
reportFailing failingModules
reportFailing :: [Module] -> IO ()
reportFailing ms = do
putStrLn "These modules are ignored:"
forM_ ms $ \m -> do
putStr " * "
putStrLn m
getDepModules :: FilePath -> IO [Module]
getDepModules f = do
contents <- readUtf8File f
return $ parseImports contents
-- TODO: do I want these?
getSources :: IO [FilePath]
getSources = filter (".agda" `List.isSuffixOf`) <$> Sys.getDirectoryContents "."
getLib :: IO [FilePath]
getLib = undefined
-- -------------------------------------------------------------------
-- Parsers
-- -------------------------------------------------------------------
parseFailingModules :: String -> [Module]
parseFailingModules file = filter (not . ignored) (map trim (lines file))
where trim = reverse . dropWhile Char.isSpace . reverse . dropWhile Char.isSpace
ignored s = null s || "#" `List.isPrefixOf` s
parseImports :: String -> [Module]
parseImports = catMaybes . map (Re.match p_import) . lines
where p_import = spaces *> optional ("open " *> spaces)
*> "import " *> spaces *> parseIdent <* Re.many Re.anySym
spaces = Re.few (Re.psym (Char.isSpace))
parseIdent :: Re.RE Char String
parseIdent = many (Re.psym (\c -> not (c `elem` "()")
&& not (Char.isSpace c)))
-- -------------------------------------------------------------------
-- Utils
-- -------------------------------------------------------------------
readUtf8File :: FilePath -> IO String
readUtf8File f = Text.unpack . Text.decodeUtf8 <$> BS.readFile f
replace :: Char -> Char -> String -> String
replace old new s = map (\c -> if c == old then new else c) s
stripDirectory :: FilePath -> FilePath -> Maybe FilePath
stripDirectory dir p = List.stripPrefix (addTrailingPathSeparator dir) p
-- -------------------------------------------------------------------
-- Tests
-- -------------------------------------------------------------------
tests :: TestTree
tests = testGroup "Tests" [
testGroup "Conversions" [
testCase "src -> module" $
sourceToModule "M1/A.agda" @?= "M1.A"
, testCase "module -> target" $
moduleToTarget "M1.A" @?= "_build/M1/A.want"
, testCase "src -> module (toplevel)" $
sourceToModule "Abc.agda" @?= "Abc"
, testCase "module -> target" $
moduleToTarget "Abc" @?= "_build/Abc.want"
]
, testGroup "Import parser" [
testCase "simple import (one line)" $
parseImports "import Data.Char" @?= ["Data.Char"]
, testCase "import with tail (one line)" $
parseImports "import Data.Char(abs,def)" @?= ["Data.Char"]
, testCase "import with space and tail (one line)" $
parseImports "import Data.Char (abs,def)" @?= ["Data.Char"]
, testCase "several imports (with open)" $
parseImports ("import Data.Char \n\
\ open import Data.Num (abs,def) hiding xxx\n\
\ import Category.Monad (join, (>>=))")
@?= ["Data.Char", "Data.Num", "Category.Monad"]
, testCase "imports interleaved with stuff" $
parseImports ("module HelloWorld where\n\
\ import Data.Char\n\n\n\
\ IamTestingSomething\n\
\ module Sub1 where\n\
\ open import Category.Monad\n\n\
\ againTesting")
@?= ["Data.Char", "Category.Monad"]
]
, testGroup "Failing modules" $ [
testCase "ignore empty" $
parseFailingModules "" @?= []
, testCase "ignore empties" $
parseFailingModules "\n \n\n" @?= []
, testCase "parse 1" $
parseFailingModules "Data.Char" @?= ["Data.Char"]
, testCase "ignore comment" $
parseFailingModules "#Hello World" @?= []
, testCase "ignore comments and empties" $
parseFailingModules " #Hello World\n\
\ \n\n\
\# What is up!...\n" @?= []
, testCase "example ignore file" $
parseFailingModules "\
\# List of modules that are expected to fail, one per line\n\
\PE-STLCFix\n\
\PHOAS2DB-Correctness\n" @?= (["PE-STLCFix", "PHOAS2DB-Correctness"] :: [Module])
]
]