0 | module Idris.ProcessIdr

  2 | import Compiler.RefC.RefC

  3 | import Compiler.Scheme.Chez

  4 | import Compiler.Scheme.ChezSep

  5 | import Compiler.Scheme.Racket

  6 | import Compiler.Scheme.Gambit

  7 | import Compiler.ES.Node

  8 | import Compiler.ES.Javascript

  9 | import Compiler.Common

 10 | import Compiler.Inline

 11 | import Compiler.Interpreter.VMCode

 13 | import Core.Binary

 14 | import Core.Directory

 15 | import Core.Env

 16 | import Core.Hash

 17 | import Core.Metadata

 18 | import Core.Unify

 20 | import Parser.Unlit

 22 | import TTImp.Elab.Check

 23 | import TTImp.ProcessDecls

 24 | import TTImp.ProcessDecls.Totality

 25 | import TTImp.TTImp

 27 | import Idris.Desugar

 28 | import Idris.Desugar.Mutual

 29 | import Idris.Parser

 30 | import Idris.REPL.Common

 31 | import Idris.Syntax

 32 | import Idris.Syntax.TTC

 33 | import Idris.Pretty

 34 | import Idris.Doc.String

 36 | import Data.SortedMap

 37 | import Data.String

 39 | import System.File

 41 | %default covering

 46 | missingIncremental : {auto c : Ref Ctxt Defs} ->

 47 |                    String -> Core Bool

 48 | missingIncremental ttcFile

 49 |   = catch (do s <- getSession

 50 |               if s.codegen `elem` s.incrementalCGs

 51 |                 then do

 52 |                   incData <- readIncData ttcFile

 53 |                   pure $ isNothing $ lookup s.codegen incData

 54 |                 else

 55 |                   pure False)

 56 |           (\error => pure False)

 58 | processDecls : {auto c : Ref Ctxt Defs} ->

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

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

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

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

 63 |                List PDecl -> Core (List Error)

 65 | processDecl : {auto c : Ref Ctxt Defs} ->

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

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

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

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

 70 |               PDecl -> Core (List Error)

 75 | processDecl (MkWithData _ $ PNamespace ns ps)

 76 |     = withExtendedNS ns $ processDecls ps

 77 | processDecl (MkWithData _ $ PMutual ps)

 78 |     = let (tys, defs) = splitMutual ps in

 79 |       processDecls (tys ++ defs)

 81 | processDecl decl

 82 |     = catch (do impdecls <- desugarDecl [] decl

 83 |                 traverse_ (Check.processDecl [] (MkNested []) Env.empty) impdecls

 84 |                 pure [])

 85 |             (\err => do giveUpConstraints -- or we'll keep trying...

 86 |                         pure [err])

 88 | processDecls decls

 89 |     = do errs <- concat <$> traverse processDecl decls

 90 |          Nothing <- checkDelayedHoles

 91 |              | Just err => pure (if null errs then [err] else errs)

 92 |          pure errs

 94 | readModule : {auto c : Ref Ctxt Defs} ->

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

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

 97 |              (full : Bool) -> -- load everything transitively (needed for REPL and compiling)

 98 |              FC ->

 99 |              (visible : Bool) -> -- Is import visible to top level module?

100 |              (imp : ModuleIdent) -> -- Module name to import

101 |              (as : Namespace) -> -- Namespace to import into

102 |              Core ()

103 | readModule full loc vis imp as

104 |     = do defs <- get Ctxt

105 |          let False = (imp, vis, as) `elem` map snd (allImported defs)

106 |              | True => when vis (setVisible (miAsNamespace imp))

107 |          Right fname <- nsToPath loc imp

108 |                | Left err => throw err

109 |          Just (syn, hash, more) <- readFromTTC False {extra = SyntaxInfo}

110 |                                                   loc vis fname imp as

111 |               | Nothing => when vis (setVisible (miAsNamespace imp)) -- already loaded, just set visibility

112 |          extendSyn syn

114 |          defs <- get Ctxt

115 |          modNS <- getNS

116 |          when vis $ setVisible (miAsNamespace imp)

117 |          traverse_ (\ mimp =>

118 |                        do let m = fst mimp

119 |                           let reexp = fst (snd mimp)

120 |                           let as = snd (snd mimp)

121 |                           when (reexp || full) $ readModule full loc reexp m as) more

122 |          setNS modNS

124 | readImport : {auto c : Ref Ctxt Defs} ->

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

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

127 |              Bool -> Import -> Core ()

128 | readImport full imp

129 |     = do readModule full (loc imp) True (path imp) (nameAs imp)

130 |          addImported (path imp, reexport imp, nameAs imp)

134 | addImport : {auto c : Ref Ctxt Defs} ->

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

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

137 |             Import -> Core ()

138 | addImport imp

139 |     = do topNS <- getNS

140 |          readImport True imp

141 |          setNS topNS

143 | readImportMeta : {auto c : Ref Ctxt Defs} ->

144 |                  Import -> Core (Bool, (Namespace, Int))

145 | readImportMeta imp

146 |     = do Right ttcFileName <- nsToPath (loc imp) (path imp)

147 |                | Left err => throw err

148 |          (_, interfaceHash) <- readHashes ttcFileName

149 |          pure (reexport imp, (nameAs imp, interfaceHash))

151 | prelude : Import

152 | prelude = MkImport (MkFC (Virtual Interactive) (0, 0) (0, 0)) False

153 |                      (nsAsModuleIdent preludeNS) preludeNS

156 | readPrelude : {auto c : Ref Ctxt Defs} ->

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

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

159 |               Bool -> Core ()

160 | readPrelude full

161 |     = do readImport full prelude

162 |          setNS mainNS

166 | readAsMain : {auto c : Ref Ctxt Defs} ->

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

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

169 |              (fname : String) -> Core ()

170 | readAsMain fname

171 |     = do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}

172 |                                              True EmptyFC True fname (nsAsModuleIdent emptyNS) emptyNS

173 |               | Nothing => throw (InternalError "Already loaded")

175 |          replNS <- getNS

176 |          replNestedNS <- getNestedNS

177 |          extendSyn syn

179 |          -- Read the main file's top level imported modules, so we have access

180 |          -- to their names (and any of their public imports)

181 |          ustm <- get UST

182 |          traverse_ (\ mimp =>

183 |                        do let m = fst mimp

184 |                           let as = snd (snd mimp)

185 |                           readModule True emptyFC True m as

186 |                           addImported (m, True, as)) more

188 |          -- also load the prelude, if required, so that we have access to it

189 |          -- at the REPL.

190 |          when (not (noprelude !getSession)) $

191 |               readModule True emptyFC True (nsAsModuleIdent preludeNS) preludeNS

193 |          -- We're in the namespace from the first TTC, so use the next name

194 |          -- from that for the fresh metavariable name generation

195 |          -- TODO: Maybe we should record this per namespace, since this is

196 |          -- a little bit of a hack? Or maybe that will have too much overhead.

197 |          update UST { nextName := nextName ustm }

199 |          setNS replNS

200 |          setNestedNS replNestedNS

202 | addPrelude : List Import -> List Import

203 | addPrelude imps

204 |   = if not (nsAsModuleIdent preludeNS `elem` map path imps)

205 |        then prelude :: imps

206 |        else imps

209 | readHeader : {auto c : Ref Ctxt Defs} ->

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

211 |              (path : String) -> (origin : ModuleIdent) -> Core Module

212 | readHeader path origin

213 |     = do Right res <- coreLift (readFile path)

214 |             | Left err => throw (FileErr path err)

215 |          -- Stop at the first :, that's definitely not part of the header, to

216 |          -- save lexing the whole file unnecessarily

217 |          setCurrentElabSource res -- for error printing purposes

218 |          let Right (ws, decor, mod)

219 |             = runParserTo (PhysicalIdrSrc origin)

220 |                           (isLitFile path) (is ':') res

221 |                           (progHdr (PhysicalIdrSrc origin))

222 |             | Left err => throw err

223 |          traverse_ recordWarning ws

224 |          pure mod

226 | %foreign "scheme:collect"

227 | prim__gc : Int -> PrimIO ()

229 | gc : IO ()

230 | gc = primIO $ prim__gc 4

233 | addPublicHash : {auto c : Ref Ctxt Defs} ->

234 |                 (Bool, (Namespace, Int)) -> Core ()

235 | addPublicHash (True, (mod, h)) = do addHash mod

236 |                                     addHash h

237 |                                     log "module.hash" 15 "Adding hash for a public import of \{show mod}"

238 | addPublicHash _ = pure ()

243 | isTTCOutdated : {auto c : Ref Ctxt Defs} ->

244 |                 (ttcFile : String) ->

245 |                 (sourceFiles : List String) ->

246 |                 Core Bool

247 | isTTCOutdated ttcFile sourceFiles

248 |   = do ttcTime  <- modTime ttcFile

249 |        srcTimes <- traverse modTime sourceFiles

250 |        log "module.hash" 20 $

251 |          unlines $

252 |            "Checking whether source code mod times are newer than \{show ttcTime}; src times:"

253 |            :: zipWith (\ src, tm => "\{src} : \{show tm}") sourceFiles srcTimes

254 |        pure $ any (>= ttcTime) srcTimes

258 | unchangedHash : (hashFn : Maybe String) -> (ttcFileName : String) -> (sourceFileName : String) -> Core Bool

259 | unchangedHash hashFn ttcFileName sourceFileName

260 |   = do Just sourceCodeHash        <- hashFileWith hashFn sourceFileName

261 |              | _ => pure False

262 |        (Just storedSourceHash, _) <- readHashes ttcFileName

263 |              | _ => pure False

264 |        pure $ sourceCodeHash == storedSourceHash

267 | getCG : {auto o : Ref ROpts REPLOpts} ->

268 |         CG -> Core (Maybe Codegen)

269 | getCG Chez = pure $ Just codegenChez

270 | getCG ChezSep = pure $ Just codegenChezSep

271 | getCG Racket = pure $ Just codegenRacket

272 | getCG Gambit = pure $ Just codegenGambit

273 | getCG Node = pure $ Just codegenNode

274 | getCG Javascript = pure $ Just codegenJavascript

275 | getCG RefC = pure $ Just codegenRefC

276 | getCG VMCodeInterp = pure $ Just codegenVMCodeInterp

277 | getCG (Other s) = getCodegen s

280 | findCG : {auto o : Ref ROpts REPLOpts} ->

281 |          {auto c : Ref Ctxt Defs} -> Core (Maybe Codegen)

283 |     = do defs <- get Ctxt

284 |          getCG (codegen (session (options defs)))

289 | processMod : {auto c : Ref Ctxt Defs} ->

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

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

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

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

294 |              (sourceFileName : String) ->

295 |              (ttcFileName : String) ->

296 |              (msg : Doc IdrisAnn) ->

297 |              (sourcecode : String) ->

298 |              (origin : ModuleIdent) ->

299 |              Core (Maybe (List Error))

300 | processMod sourceFileName ttcFileName msg sourcecode origin

301 |     = catch (do

302 |         setCurrentElabSource sourcecode

303 |         session <- getSession

305 |         -- Just read the header to start with (this is to get the imports and

306 |         -- see if we can avoid rebuilding if none have changed)

307 |         moduleHeader <- readHeader sourceFileName origin

308 |         let ns = moduleNS moduleHeader

310 |         -- Add an implicit prelude import

311 |         let allImports =

312 |           if (session.noprelude || moduleNS moduleHeader == nsAsModuleIdent preludeNS)

313 |              then imports moduleHeader

314 |              else addPrelude $ imports moduleHeader

316 |         importMetas <- traverse readImportMeta allImports

317 |         let importInterfaceHashes = snd <$> importMetas

319 |         defs <- get Ctxt

320 |         log "module.hash" 5 $ "Interface hash of " ++ show ns ++ ": " ++ show (ifaceHash defs)

321 |         log "module.hash" 5 $ "Import Interface hashes of " ++ show ns ++ " hashes:\n" ++

322 |           show (sort importInterfaceHashes)

323 |         storedImportInterfaceHashes <- readImportHashes ttcFileName

324 |         log "module.hash" 5 $ "Stored interface hashes of " ++ ttcFileName ++ ":\n" ++

325 |           show (sort storedImportInterfaceHashes)

327 |         let isUnchanged = if session.checkHashesInsteadOfModTime

328 |                              then unchangedHash (defs.options.hashFn)

329 |                              else (\ttc,src => not <$> (isTTCOutdated ttc [src]))

330 |         sourceUnchanged <- isUnchanged ttcFileName sourceFileName

332 |         incrementalOK <- not <$> missingIncremental ttcFileName

334 |         -- If neither the source nor the interface hashes of imports have changed then no rebuilding is needed

335 |         if (sourceUnchanged && sort importInterfaceHashes == sort storedImportInterfaceHashes && incrementalOK)

336 |            then -- Hashes the same, source up to date, just set the ns

337 |                 -- for the REPL

338 |                 do setNS (miAsNamespace ns)

339 |                    pure Nothing

340 |            else -- needs rebuilding

341 |              do iputStrLn msg

342 |                 Right (ws, MkState decor hnames, mod) <-

343 |                     logTime 2 ("Parsing " ++ sourceFileName) $

344 |                       pure $ runParser (PhysicalIdrSrc origin)

345 |                                        (isLitFile sourceFileName)

346 |                                        sourcecode

347 |                                        (do p <- prog (PhysicalIdrSrc origin); eoi; pure p)

348 |                   | Left err => pure (Just [err])

349 |                 traverse_ recordWarning ws

351 |                 -- save the doc info for the current module

352 |                 log "doc.module" 10 $ unlines

353 |                   [ "Recording doc", documentation moduleHeader

354 |                   , "and imports " ++ show (imports moduleHeader)

355 |                   , "for module " ++ show (moduleNS moduleHeader)

356 |                   ]

357 |                 addModDocInfo

358 |                   (moduleNS moduleHeader)

359 |                   (documentation moduleHeader)

360 |                   (filter reexport $ imports moduleHeader)

362 |                 addSemanticDecorations decor

363 |                 update Syn { holeNames := hnames }

365 |                 initHash

366 |                 traverse_ addPublicHash (sort importMetas)

367 |                 resetNextVar

368 |                 when (ns /= nsAsModuleIdent mainNS) $

369 |                       when (ns /= origin) $

370 |                           throw (GenericMsg mod.headerLoc

371 |                                    ("Module name " ++ show ns ++

372 |                                     " does not match file name " ++ show sourceFileName))

374 |                 -- read import ttcs in full here

375 |                 -- Note: We should only import .ttc - assumption is that there's

376 |                 -- a phase before this which builds the dependency graph

377 |                 -- (also that we only build child dependencies if rebuilding

378 |                 -- changes the interface - will need to store a hash in .ttc!)

379 |                 logTime 2 "Reading imports" $

380 |                    traverse_ (readImport False) allImports

382 |                 -- Before we process the source, make sure the "hide_everywhere"

383 |                 -- names are set to private (TODO, maybe if we want this?)

386 |                 setNS (miAsNamespace ns)

387 |                 errs <- logTime 2 "Processing decls" $

388 |                             processDecls (decls mod)

389 |                 totErrs <- logTime 3 ("Totality check overall")

390 |                             getTotalityErrors

391 |                 let errs = errs ++ totErrs

394 |                 when (isNil errs) $

395 |                    logTime 2 "Compile defs" $ compileAndInlineAll

397 |                 -- Save the import hashes for the imports we just read.

398 |                 -- If they haven't changed next time, and the source

399 |                 -- file hasn't changed, no need to rebuild.

400 |                 update Ctxt { importHashes := importInterfaceHashes }

401 |                 pure (Just errs))

402 |           (\err => pure (Just [err]))

407 | process : {auto c : Ref Ctxt Defs} ->

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

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

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

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

412 |           (msgPrefix : Doc IdrisAnn) ->

413 |           (buildMsg : Doc IdrisAnn) ->

414 |           FileName ->

415 |           (moduleIdent : ModuleIdent) ->

416 |           Core (List Error)

417 | process msgPrefix buildMsg sourceFileName ident

418 |     = do Right res <- coreLift (readFile sourceFileName)

419 |                | Left err => pure [FileErr sourceFileName err]

420 |          catch (do ttcFileName <- getTTCFileName sourceFileName "ttc"

421 |                    Just errs <- logTime 1 ("Elaborating " ++ sourceFileName) $

422 |                                    processMod sourceFileName ttcFileName

423 |                                               (msgPrefix <++> "Building" <++> buildMsg)

424 |                                               res ident

425 |                      | Nothing => do log "module" 10 $ show $ msgPrefix <++> "Skipping" <++> buildMsg

426 |                                      pure [] -- skipped it

427 |                    if isNil errs

428 |                       then

429 |                         do ns <- ctxtPathToNS sourceFileName

430 |                            makeBuildDirectory ns

431 |                            traverse_

432 |                               (\cg =>

433 |                                   do Just cgdata <- getCG cg

434 |                                           | Nothing =>

435 |                                               coreLift $ putStrLn $ "No incremental code generator for " ++ show cg

436 |                                      Just res <- incCompile cgdata sourceFileName

437 |                                           | Nothing => pure ()

438 |                                      setIncData cg res)

439 |                               (incrementalCGs !getSession)

441 |                            writeToTTC !(get Syn) sourceFileName ttcFileName

442 |                            ttmFileName <- getTTCFileName sourceFileName "ttm"

443 |                            writeToTTM ttmFileName

444 |                            pure []

445 |                       else do pure errs)

446 |                (\err => pure [err])