0 | module Idris.ModTree

  2 | import Core.Binary

  3 | import Core.Directory

  4 | import Core.Metadata

  5 | import Core.InitPrimitives

  6 | import Core.UnifyState

  8 | import Idris.Parser

  9 | import Idris.ProcessIdr

 10 | import Idris.REPL.Common

 11 | import Idris.Syntax

 12 | import Idris.Pretty

 14 | import Data.Either

 15 | import Data.String

 17 | import System.Directory

 19 | import Libraries.Data.StringMap

 21 | %default covering

 23 | record ModTree where

 24 |   constructor MkModTree

 25 |   nspace : ModuleIdent

 26 |   sourceFile : Maybe String

 27 |   deps : List ModTree

 30 | Show ModTree where

 31 |   show t = show (sourceFile t) ++ " " ++ show (nspace t) ++ "<-" ++ show (deps t)

 41 | public export

 42 | record BuildMod where

 43 |   constructor MkBuildMod

 44 |   buildFile : String

 45 |   buildNS : ModuleIdent

 46 |   imports : List ModuleIdent

 49 | Show BuildMod where

 50 |   show t = buildFile t ++ " [" ++ showSep ", " (map show (imports t)) ++ "]"

 52 | data AllMods : Type where

 54 | mkModTree : {auto c : Ref Ctxt Defs} ->

 55 |             {auto o : Ref ROpts REPLOpts} ->

 56 |             {auto a : Ref AllMods (List (ModuleIdent, ModTree))} ->

 57 |             FC ->

 58 |             (done : List ModuleIdent) -> -- if 'mod' is here we have a cycle

 59 |             (modFP : Maybe FileName) -> -- Sometimes we know already know what the file name is

 60 |             (mod : ModuleIdent) ->      -- Otherwise we'll compute it from the module name

 61 |             Core ModTree

 62 | mkModTree loc done modFP mod

 63 |   = if mod `elem` done

 64 |        then throw (CyclicImports (done ++ [mod]))

 65 |        else

 66 |           -- Read imports from source file. If the source file isn't

 67 |           -- available, it's not our responsibility

 68 |           catch (do all <- get AllMods

 69 |                     -- If we've seen it before, reuse what we found

 70 |                     case lookup mod all of

 71 |                          Nothing =>

 72 |                            do file <- maybe (nsToSource loc mod) pure modFP

 73 |                               modInfo <- readHeader file mod

 74 |                               let imps = map path (imports modInfo)

 75 |                               if mod `elem` imps

 76 |                                 then coreFail $ CyclicImports [mod, mod]

 77 |                                 else do

 78 |                                   ms <- traverse (mkModTree loc (mod :: done) Nothing) imps

 79 |                                   let mt = MkModTree mod (Just file) ms

 80 |                                   update AllMods ((mod, mt) ::)

 81 |                                   pure mt

 82 |                          Just m => pure m)

 83 |                 -- Couldn't find source, assume it's in a package directory

 84 |                 (\err =>

 85 |                     case err of

 86 |                          CyclicImports {} => throw err

 87 |                          ParseFail {} => throw err

 88 |                          LexFail {} => throw err

 89 |                          LitFail {} => throw err

 90 |                          _ => pure (MkModTree mod Nothing []))

 92 | data DoneMod : Type where

 93 | data BuildOrder : Type where

 97 | mkBuildMods : {auto d : Ref DoneMod (StringMap ())} ->

 98 |               {auto o : Ref BuildOrder (List BuildMod)} ->

 99 |               ModTree -> Core ()

100 | mkBuildMods mod

101 |     = whenJust (sourceFile mod) $ \ sf =>

102 |             do done <- get DoneMod

103 |                case lookup sf done of

104 |                     Just _ => pure ()

105 |                     Nothing =>

106 |                        do -- build dependencies

107 |                           traverse_ mkBuildMods (deps mod)

108 |                           -- build it now

109 |                           update BuildOrder

110 |                                    (MkBuildMod sf mod.nspace

111 |                                                (map nspace mod.deps) ::)

112 |                           update DoneMod $ insert sf ()

118 | getBuildMods : {auto c : Ref Ctxt Defs} ->

119 |                {auto o : Ref ROpts REPLOpts} ->

120 |                FC -> (done : List BuildMod) ->

121 |                (mainFile : String) ->

122 |                Core (List BuildMod)

123 | getBuildMods loc done fname

124 |     = do a <- newRef AllMods []

125 |          fname_ns <- ctxtPathToNS fname

126 |          if fname_ns `elem` map buildNS done

127 |             then pure []

128 |             else

129 |               do t <- mkModTree {a} loc [] (Just fname) fname_ns

130 |                  dm <- newRef DoneMod empty

131 |                  o <- newRef BuildOrder []

132 |                  mkBuildMods {d=dm} {o} t

133 |                  pure (reverse !(get BuildOrder))

135 | checkTotalReq : {auto c : Ref Ctxt Defs} ->

136 |                 String -> String -> TotalReq -> Core Bool

137 | checkTotalReq sourceFile ttcFile expected

138 |   = catch (do log "totality.requirement" 20 $

139 |                 "Reading totalReq from " ++ ttcFile

140 |               Just got <- readTotalReq ttcFile

141 |                 | Nothing => pure False

142 |               log "totality.requirement" 20 $ unwords

143 |                 [ "Got", show got, "and expected", show expected ++ ":"

144 |                 , "we", ifThenElse (got < expected) "should" "shouldn't"

145 |                 , "rebuild" ]

146 |               -- if what we got (i.e. what we used when we checked the file the

147 |               -- first time around) was strictly less stringent than what we

148 |               -- expect now then we need to rebuild.

149 |               pure (got < expected))

150 |           (\error => pure False)

152 | needsBuildingTime : {auto c : Ref Ctxt Defs} ->

153 |                     (sourceFile : String) -> (ttcFile : String) ->

154 |                     (depFiles : List String) -> Core Bool

155 | needsBuildingTime sourceFile ttcFile depFiles

156 |   = isTTCOutdated ttcFile (sourceFile :: depFiles)

158 | needsBuildingDepHash : {auto c : Ref Ctxt Defs} ->

159 |                  String -> Core Bool

160 | needsBuildingDepHash depFileName

161 |   = catch (do defs                   <- get Ctxt

162 |               depTTCFileName         <- getTTCFileName depFileName "ttc"

163 |               not <$> unchangedHash defs.options.hashFn depTTCFileName depFileName)

164 |           (\error => pure False)

168 | needsBuildingHash : {auto c : Ref Ctxt Defs} ->

169 |                     (sourceFile : String) -> (ttcFile : String) ->

170 |                     (depFiles : List String) -> Core Bool

171 | needsBuildingHash sourceFile ttcFile depFiles

172 |   = do defs                <- get Ctxt

173 |        sourceUnchanged <- unchangedHash defs.options.hashFn ttcFile sourceFile

174 |        depFilesHashDiffers <- any id <$> traverse needsBuildingDepHash depFiles

175 |        pure $ (not sourceUnchanged) || depFilesHashDiffers

178 | needsBuilding :

179 |   {auto c : Ref Ctxt Defs} ->

180 |   {auto o : Ref ROpts REPLOpts} ->

181 |   (sourceFile, ttcFile : String) -> List String -> Core Bool

182 | needsBuilding sourceFile ttcFile depFiles

183 |   = do -- if the ttc file does not exist there is no point in asking

184 |        -- whether we need to rebuild it

185 |        True <- coreLift $ exists ttcFile

186 |          | False => pure True

187 |        -- check if hash match

188 |        checkHashesInsteadOfTime <- checkHashesInsteadOfModTime <$> getSession

189 |        False <- ifThenElse checkHashesInsteadOfTime

190 |                            needsBuildingHash

191 |                            needsBuildingTime

192 |                   sourceFile ttcFile depFiles

193 |          | True => pure True

195 |        log "import" 20 $ "\{ifThenElse checkHashesInsteadOfTime "Hashes" "Mod Times"} still valid for " ++ sourceFile

197 |        False <- missingIncremental ttcFile

198 |          | True => pure True

200 |        -- in case we're loading the main file, make sure the TTC is

201 |        -- using the appropriate default totality requirement

202 |        Just f <- mainfile <$> get ROpts

203 |          | Nothing => pure False

204 |        log "totality.requirement" 10 $ concat {t = List}

205 |          [ "Checking totality requirement of "

206 |          , sourceFile

207 |          , " (main file is "

208 |          , f

209 |          , ")"

210 |          ]

211 |        let True = sourceFile == f

212 |          | False => pure False

213 |        True <- checkTotalReq sourceFile ttcFile !(totalReq <$> getSession)

214 |          | False => pure False

215 |        -- if it needs rebuilding then remove the buggy .ttc file to avoid going

216 |        -- into an infinite loop!

217 |        Right () <- coreLift $ removeFile ttcFile

218 |          | Left err => throw (FileErr ttcFile err)

219 |        pure True

222 | buildMod : {auto c : Ref Ctxt Defs} ->

223 |            {auto s : Ref Syn SyntaxInfo} ->

224 |            {auto o : Ref ROpts REPLOpts} ->

225 |            FC -> Nat -> Nat -> BuildMod ->

226 |            Core (List Error)

227 | buildMod loc num len mod

228 |    = do clearCtxt; addPrimitives

229 |         lazyActive True; setUnboundImplicits True

231 |         let sourceFile = buildFile mod

232 |         let modNamespace = buildNS mod

233 |         ttcFile <- getTTCFileName sourceFile "ttc"

234 |         -- We'd expect any errors in nsToPath to have been caught by now

235 |         -- since the imports have been built! But we still have to check.

236 |         depFilesE <- traverse (nsToPath loc) (imports mod)

237 |         let (ferrs, depFiles) = partitionEithers depFilesE

239 |         log "import" 20 $ unwords $

240 |           [ "Checking whether to rebuild "

241 |           , sourceFile

242 |           , "(" ++ ttcFile ++ ")"

243 |           , "with dependencies:"

244 |           ] ++ depFiles

245 |         rebuild <- needsBuilding sourceFile ttcFile depFiles

247 |         u <- newRef UST initUState

248 |         m <- newRef MD (initMetadata (PhysicalIdrSrc modNamespace))

249 |         put Syn initSyntax

251 |         errs <- ifThenElse (not rebuild) (pure []) $

252 |            do let pad = minus (length $ show len) (length $ show num)

253 |               let msgPrefix : Doc IdrisAnn

254 |                   = pretty0 (replicate pad ' ') <+> byShow num

255 |                     <+> slash <+> byShow len <+> colon

256 |               let buildMsg : Doc IdrisAnn

257 |                   = pretty0 mod.buildNS

258 |                     <++> parens (pretty0 sourceFile)

259 |               log "import.file" 10 $ "Processing " ++ sourceFile

260 |               process {u} {m} msgPrefix buildMsg sourceFile modNamespace

262 |         ws <- emitWarningsAndErrors (if null errs then ferrs else errs)

263 |         pure (ws ++ if null errs then ferrs else ferrs ++ errs)

266 | buildMods : {auto c : Ref Ctxt Defs} ->

267 |             {auto s : Ref Syn SyntaxInfo} ->

268 |             {auto o : Ref ROpts REPLOpts} ->

269 |             FC -> Nat -> Nat -> List BuildMod ->

270 |             Core (List Error)

271 | buildMods fc num len [] = pure []

272 | buildMods fc num len (m :: ms)

273 |     = case !(buildMod fc num len m) of

274 |            [] => buildMods fc (1 + num) len ms

275 |            errs => pure errs

278 | buildDeps : {auto c : Ref Ctxt Defs} ->

279 |             {auto s : Ref Syn SyntaxInfo} ->

280 |             {auto m : Ref MD Metadata} ->

281 |             {auto u : Ref UST UState} ->

282 |             {auto o : Ref ROpts REPLOpts} ->

283 |             (mainFile : String) ->

284 |             Core (List Error)

285 | buildDeps fname

286 |     = do mods <- getBuildMods EmptyFC [] fname

287 |          log "import" 20 $ "Needs to rebuild: " ++ show mods

288 |          ok <- buildMods EmptyFC 1 (length mods) mods

289 |          case ok of

290 |               [] => do -- On success, reload the main ttc in a clean context

291 |                        clearCtxt; addPrimitives

292 |                        modIdent <- ctxtPathToNS fname

293 |                        put MD (initMetadata (PhysicalIdrSrc modIdent))

294 |                        mainttc <- getTTCFileName fname "ttc"

295 |                        log "import" 10 $ "Reloading " ++ show mainttc ++ " from " ++ fname

296 |                        readAsMain mainttc

298 |                        -- Load the associated metadata for interactive editing

299 |                        mainttm <- getTTCFileName fname "ttm"

300 |                        log "import" 10 $ "Reloading " ++ show mainttm

301 |                        readFromTTM mainttm

302 |                        pure []

303 |               errs => pure errs -- Error happened, give up

305 | getAllBuildMods : {auto c : Ref Ctxt Defs} ->

306 |                   {auto o : Ref ROpts REPLOpts} ->

307 |                   FC -> (done : List BuildMod) ->

308 |                   (allFiles : List String) ->

309 |                   Core (List BuildMod)

310 | getAllBuildMods fc done [] = pure done

311 | getAllBuildMods fc done (f :: fs)

312 |     = do ms <- getBuildMods fc done f

313 |          getAllBuildMods fc (ms ++ done) fs

316 | buildAll : {auto c : Ref Ctxt Defs} ->

317 |            {auto s : Ref Syn SyntaxInfo} ->

318 |            {auto o : Ref ROpts REPLOpts} ->

319 |            (allFiles : List String) ->

320 |            Core (List Error)

321 | buildAll allFiles

322 |     = do mods <- getAllBuildMods EmptyFC [] allFiles

323 |          -- There'll be duplicates, so if something is already built, drop it

324 |          let mods' = dropLater mods

325 |          buildMods EmptyFC 1 (length mods') mods'

326 |   where

327 |     dropLater : List BuildMod -> List BuildMod

328 |     dropLater [] = []

329 |     dropLater (b :: bs)

330 |         = b :: dropLater (filter (\x => buildFile x /= buildFile b) bs)