3 | module Core.Binary

  5 | import public Core.Binary.Prims

  6 | import Core.Context.Log

  7 | import Core.Options

  8 | import Core.TTC

  9 | import Core.UnifyState

 11 | import Data.String

 13 | import System.File

 15 | import Libraries.Data.NameMap

 16 | import Libraries.Data.NatSet

 18 | import public Libraries.Utils.Binary

 20 | %default covering

 26 | ttcVersion : Int

 27 | ttcVersion = 2025_08_16_00

 30 | checkTTCVersion : String -> Int -> Int -> Core ()

 31 | checkTTCVersion file ver exp

 32 |   = when (ver /= exp) (throw $ TTCError $ Format file ver exp)

 34 | record TTCFile extra where

 35 |   constructor MkTTCFile

 36 |   version : Int

 37 |   totalReq : TotalReq

 38 |   sourceHash : Maybe String

 39 |   ifaceHash : Int

 40 |   importHashes : List (Namespace, Int)

 41 |   incData : List (CG, String, List String)

 42 |   context : List (Name, Binary)

 43 |   userHoles : List Name

 44 |   autoHints : List (Name, Bool)

 45 |   typeHints : List (Name, Name, Bool)

 46 |   imported : List (ModuleIdent, Bool, Namespace)

 47 |   nextVar : Int

 48 |   currentNS : Namespace

 49 |   nestedNS : List Namespace

 50 |   pairnames : Maybe PairNames

 51 |   rewritenames : Maybe RewriteNames

 52 |   primnames : PrimNames

 53 |   foreignImpl : List (Name, String)

 54 |   namedirectives : List (Name, List String)

 55 |   cgdirectives : List (CG, String)

 56 |   transforms : List (Name, Transform)

 57 |   foreignExports : List (Name, (List (String, String)))

 58 |   extraData : extra

 60 | HasNames a => HasNames (List a) where

 61 |   full c ns = full_aux c [] ns

 62 |     where full_aux : Context -> List a -> List a -> Core (List a)

 63 |           full_aux c res [] = pure (reverse res)

 64 |           full_aux c res (n :: ns) = full_aux c (!(full c n):: res) ns

 67 |   resolved c ns = resolved_aux c [] ns

 68 |     where resolved_aux : Context -> List a -> List a -> Core (List a)

 69 |           resolved_aux c res [] = pure (reverse res)

 70 |           resolved_aux c res (n :: ns) = resolved_aux c (!(resolved c n) :: res) ns

 71 | HasNames (Int, FC, Name) where

 72 |   full c (i, fc, n) = pure (i, fc, !(full c n))

 73 |   resolved c (i, fc, n) = pure (i, fc, !(resolved c n))

 75 | HasNames (Name, Bool) where

 76 |   full c (n, b) = pure (!(full c n), b)

 77 |   resolved c (n, b) = pure (!(resolved c n), b)

 79 | HasNames (Name, List a) where

 80 |   full c (n, b) = pure (!(full c n), b)

 81 |   resolved c (n, b) = pure (!(resolved c n), b)

 83 | HasNames (Name, Transform) where

 84 |   full c (n, b) = pure (!(full c n), !(full c b))

 85 |   resolved c (n, b) = pure (!(resolved c n), !(resolved c b))

 87 | HasNames (Name, Name, Bool) where

 88 |   full c (n1, n2, b) = pure (!(full c n1), !(full c n2), b)

 89 |   resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)

 91 | HasNames e => HasNames (TTCFile e) where

 92 |   full gam (MkTTCFile version totalReq sourceHash ifaceHash iHashes incData

 93 |                       context userHoles

 94 |                       autoHints typeHints

 95 |                       imported nextVar currentNS nestedNS

 96 |                       pairnames rewritenames primnames foreignImpl

 97 |                       namedirectives cgdirectives trans

 98 |                       fexp extra)

 99 |       = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData

100 |                          context userHoles

101 |                          !(traverse (full gam) autoHints)

102 |                          !(traverse (full gam) typeHints)

103 |                          imported nextVar currentNS nestedNS

104 |                          !(fullPair gam pairnames)

105 |                          !(fullRW gam rewritenames)

106 |                          !(fullPrim gam primnames)

107 |                          !(traverse fullForeign foreignImpl)

108 |                          !(full gam namedirectives)

109 |                          cgdirectives

110 |                          !(full gam trans)

111 |                          !(full gam fexp)

112 |                          !(full gam extra)

113 |     where

114 |       fullPair : Context -> Maybe PairNames -> Core (Maybe PairNames)

115 |       fullPair gam Nothing = pure Nothing

116 |       fullPair gam (Just (MkPairNs t f s))

117 |           = pure $ Just $ MkPairNs !(full gam t) !(full gam f) !(full gam s)

119 |       fullRW : Context -> Maybe RewriteNames -> Core (Maybe RewriteNames)

120 |       fullRW gam Nothing = pure Nothing

121 |       fullRW gam (Just (MkRewriteNs e r))

122 |           = pure $ Just $ MkRewriteNs !(full gam e) !(full gam r)

124 |       fullPrim : Context -> PrimNames -> Core PrimNames

125 |       fullPrim gam (MkPrimNs mi ms mc md mt mn mdl)

126 |           = [| MkPrimNs (full gam mi)

127 |                         (full gam ms)

128 |                         (full gam mc)

129 |                         (full gam md)

130 |                         (full gam mt)

131 |                         (full gam mn)

132 |                         (full gam mdl) |]

134 |       fullForeign : (Name, String) -> Core (Name, String)

135 |       fullForeign (n,s) = pure $ (!(full gam n), s)

137 |   -- I don't think we ever actually want to call this, because after we read

138 |   -- from the file we're going to add them to learn what the resolved names

139 |   -- are supposed to be! But for completeness, let's do it right.

140 |   resolved gam (MkTTCFile version totalReq sourceHash ifaceHash iHashes incData

141 |                       context userHoles

142 |                       autoHints typeHints

143 |                       imported nextVar currentNS nestedNS

144 |                       pairnames rewritenames primnames foreignImpl

145 |                       namedirectives cgdirectives trans

146 |                       fexp extra)

147 |       = pure $ MkTTCFile version totalReq sourceHash ifaceHash iHashes incData

148 |                          context userHoles

149 |                          !(traverse (resolved gam) autoHints)

150 |                          !(traverse (resolved gam) typeHints)

151 |                          imported nextVar currentNS nestedNS

152 |                          !(resolvedPair gam pairnames)

153 |                          !(resolvedRW gam rewritenames)

154 |                          !(resolvedPrim gam primnames)

155 |                          !(traverse resolvedForeign foreignImpl)

156 |                          !(resolved gam namedirectives)

157 |                          cgdirectives

158 |                          !(resolved gam trans)

159 |                          !(resolved gam fexp)

160 |                          !(resolved gam extra)

161 |     where

162 |       resolvedPair : Context -> Maybe PairNames -> Core (Maybe PairNames)

163 |       resolvedPair gam Nothing = pure Nothing

164 |       resolvedPair gam (Just (MkPairNs t f s))

165 |           = pure $ Just $ MkPairNs !(resolved gam t) !(resolved gam f) !(resolved gam s)

167 |       resolvedRW : Context -> Maybe RewriteNames -> Core (Maybe RewriteNames)

168 |       resolvedRW gam Nothing = pure Nothing

169 |       resolvedRW gam (Just (MkRewriteNs e r))

170 |           = pure $ Just $ MkRewriteNs !(resolved gam e) !(resolved gam r)

172 |       resolvedPrim : Context -> PrimNames -> Core PrimNames

173 |       resolvedPrim gam (MkPrimNs mi ms mc md mt mn mdl)

174 |           = pure $ MkPrimNs !(resolved gam mi)

175 |                             !(resolved gam ms)

176 |                             !(resolved gam mc)

177 |                             !(resolved gam md)

178 |                             !(resolved gam mt)

179 |                             !(resolved gam mn)

180 |                             !(resolved gam mdl)

182 |       resolvedForeign : (Name, String) -> Core (Name, String)

183 |       resolvedForeign (n,s) = pure $ (!(resolved gam n), s)

187 | writeTTCFile : (HasNames extra, TTC extra) =>

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

189 |                Ref Bin Binary -> TTCFile extra -> Core ()

190 | writeTTCFile b file_in

191 |       = do file <- toFullNames file_in

192 |            toBuf "TT2"

193 |            toBuf @{Wasteful} (version file)

194 |            toBuf (totalReq file)

195 |            toBuf (sourceHash file)

196 |            toBuf (ifaceHash file)

197 |            toBuf (importHashes file)

198 |            toBuf (incData file)

199 |            toBuf (imported file)

200 |            toBuf (extraData file)

201 |            toBuf (context file)

202 |            toBuf (userHoles file)

203 |            toBuf (autoHints file)

204 |            toBuf (typeHints file)

205 |            toBuf (nextVar file)

206 |            toBuf (currentNS file)

207 |            toBuf (nestedNS file)

208 |            toBuf (pairnames file)

209 |            toBuf (rewritenames file)

210 |            toBuf (primnames file)

211 |            toBuf (foreignImpl file)

212 |            toBuf (namedirectives file)

213 |            toBuf (cgdirectives file)

214 |            toBuf (transforms file)

215 |            toBuf (foreignExports file)

217 | readTTCFile : TTC extra =>

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

219 |               Bool -> String -> Maybe (Namespace) ->

220 |               Ref Bin Binary -> Core (TTCFile extra)

221 | readTTCFile readall file as b

222 |       = do hdr <- fromBuf

223 |            when (hdr /= "TT2") $

224 |              corrupt ("TTC header in " ++ file ++ " " ++ show hdr)

225 |            ver <- fromBuf @{Wasteful}

226 |            checkTTCVersion file ver ttcVersion

227 |            totalReq <- fromBuf

228 |            sourceFileHash <- fromBuf

229 |            ifaceHash <- fromBuf

230 |            importHashes <- fromBuf

231 |            incData <- fromBuf

232 |            imp <- fromBuf

233 |            ex <- fromBuf

234 |            if not readall

235 |               then pure (MkTTCFile ver totalReq

236 |                                    sourceFileHash ifaceHash importHashes

237 |                                    incData [] [] [] [] []

238 |                                    0 (mkNamespace "") [] Nothing

239 |                                    Nothing

240 |                                    (MkPrimNs Nothing Nothing Nothing Nothing Nothing Nothing Nothing)

241 |                                    [] [] [] [] [] ex)

242 |               else do

243 |                  defs <- fromBuf

244 |                  uholes <- fromBuf

245 |                  autohs <- fromBuf

246 |                  typehs <- fromBuf

247 |                  nextv <- fromBuf

248 |                  cns <- fromBuf

249 |                  nns <- fromBuf

250 |                  pns <- fromBuf

251 |                  rws <- fromBuf

252 |                  prims <- fromBuf

253 |                  foreignImpl <- fromBuf

254 |                  nds <- fromBuf

255 |                  cgds <- fromBuf

256 |                  trans <- fromBuf

257 |                  fexp <- fromBuf

258 |                  pure (MkTTCFile ver totalReq

259 |                                  sourceFileHash ifaceHash importHashes incData

260 |                                  (map (replaceNS cns) defs) uholes

261 |                                  autohs typehs imp nextv cns nns

262 |                                  pns rws prims foreignImpl nds cgds trans fexp ex)

263 |   where

264 |     -- We don't store full names in 'defs' - we remove the namespace if it's

265 |     -- the same as the current namespace. So, this puts it back.

266 |     replaceNS : Namespace -> (Name, a) -> (Name, a)

267 |     replaceNS ns n@(NS _ _, d) = n

268 |     replaceNS ns (n, d) = (NS ns n, d)

271 | getSaveDefs : Namespace -> List Name -> List (Name, Binary) -> Defs ->

272 |               Core (List (Name, Binary))

273 | getSaveDefs modns [] acc _ = pure acc

274 | getSaveDefs modns (n :: ns) acc defs

275 |     = do Just gdef <- lookupCtxtExact n (gamma defs)

276 |               | Nothing => getSaveDefs modns ns acc defs -- 'n' really should exist though!

277 |          -- No need to save builtins

278 |          case definition gdef of

279 |               Builtin _ => getSaveDefs modns ns acc defs

280 |               _ => do bin <- initBinaryS 16384

281 |                       toBuf (trimNS modns !(full (gamma defs) gdef))

282 |                       b <- get Bin

283 |                       getSaveDefs modns ns ((trimName (fullname gdef), b) :: acc) defs

284 |   where

285 |     trimName : Name -> Name

286 |     trimName n@(NS defns d) = if defns == modns then d else n

287 |     trimName n = n

292 | writeToTTC : (HasNames extra, TTC extra) =>

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

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

295 |              extra -> (sourceFileName : String) ->

296 |              (ttcFileName : String) -> Core ()

297 | writeToTTC extradata sourceFileName ttcFileName

298 |     = do bin <- initBinary

299 |          defs <- get Ctxt

300 |          ust <- get UST

301 |          gdefs <- getSaveDefs (currentNS defs) (keys (toSave defs)) [] defs

302 |          sourceHash <- hashFileWith defs.options.hashFn sourceFileName

303 |          totalReq <- getDefaultTotalityOption

304 |          log "ttc.write" 5 $ unwords

305 |            [ "Writing", ttcFileName

306 |            , "with source hash", show sourceHash

307 |            , "and interface hash", show (ifaceHash defs)

308 |            ]

309 |          writeTTCFile bin

310 |                    (MkTTCFile ttcVersion totalReq

311 |                               sourceHash

312 |                               (ifaceHash defs) (importHashes defs)

313 |                               (incData defs)

314 |                               gdefs

315 |                               (keys (userHoles defs))

316 |                               (saveAutoHints defs)

317 |                               (saveTypeHints defs)

318 |                               (imported defs)

319 |                               (nextName ust)

320 |                               (currentNS defs)

321 |                               (nestedNS defs)

322 |                               (pairnames (options defs))

323 |                               (rewritenames (options defs))

324 |                               (primnames (options defs))

325 |                               (foreignImpl (options defs))

326 |                               (NameMap.toList (namedirectives defs))

327 |                               (cgdirectives defs)

328 |                               (saveTransforms defs)

329 |                               (NameMap.toList (foreignExports defs))

330 |                               extradata)

332 |          Right ok <- coreLift $ writeToFile ttcFileName !(get Bin)

333 |                | Left err => throw (InternalError (ttcFileName ++ ": " ++ show err))

334 |          pure ()

336 | addGlobalDef : {auto c : Ref Ctxt Defs} ->

337 |                (modns : ModuleIdent) -> Namespace ->

338 |                (importAs : Maybe Namespace) ->

339 |                (Name, Binary) -> Core ()

340 | addGlobalDef modns filens asm (n, def)

341 |     = do defs <- get Ctxt

342 |          codedentry <- lookupContextEntry n (gamma defs)

343 |          -- Don't update the coded entry because some names might not be

344 |          -- resolved yet

345 |          entry <- maybe (pure Nothing)

346 |                         (\ p => do x <- decode (gamma defs) (fst p) False (snd p)

347 |                                    pure (Just x))

348 |                         codedentry

349 |          unless (completeDef entry) $

350 |            ignore $ addContextEntry filens n def

352 |          whenJust asm $ \ as => addContextAlias (asName modns as n) n

354 |   where

355 |     -- If the definition already exists, don't overwrite it with an empty

356 |     -- definition or hole. This might happen if a function is declared in one

357 |     -- module and defined in another.

358 |     completeDef : Maybe GlobalDef -> Bool

359 |     completeDef Nothing = False

360 |     completeDef (Just def)

361 |         = case definition def of

362 |                None => False

363 |                Hole {} => False

364 |                _ => True

366 | addTypeHint : {auto c : Ref Ctxt Defs} ->

367 |               FC -> (Name, Name, Bool) -> Core ()

368 | addTypeHint fc (tyn, hintn, d)

369 |    = do logC "ttc.read" 10 (pure (show !(getFullName hintn) ++ " for " ++

370 |                             show !(getFullName tyn)))

371 |         addHintFor fc tyn hintn d True

373 | addAutoHint : {auto c : Ref Ctxt Defs} -> (Name, Bool) -> Core ()

374 | addAutoHint (hintn_in, d)

375 |     = do hintn <- toResolvedNames hintn_in

376 |          update Ctxt { autoHints $= insert hintn d }

379 | updatePair : {auto c : Ref Ctxt Defs} -> Maybe PairNames -> Core ()

380 | updatePair p = update Ctxt { options->pairnames $= (p <+>) }

383 | updateRewrite : {auto c : Ref Ctxt Defs} -> Maybe RewriteNames -> Core ()

384 | updateRewrite r = update Ctxt { options->rewritenames $= (r <+>) }

387 | updatePrimNames : PrimNames -> PrimNames -> PrimNames

388 | updatePrimNames p

389 |     = { fromIntegerName $= (p.fromIntegerName <+>),

390 |         fromStringName  $= (p.fromStringName  <+>),

391 |         fromCharName    $= (p.fromCharName    <+>),

392 |         fromDoubleName  $= (p.fromDoubleName  <+>),

393 |         fromTTImpName   $= (p.fromTTImpName   <+>),

394 |         fromNameName    $= (p.fromNameName    <+>),

395 |         fromDeclsName   $= (p.fromDeclsName   <+>)

396 |       }

399 | updatePrims : {auto c : Ref Ctxt Defs} -> PrimNames -> Core ()

400 | updatePrims p = update Ctxt { options->primnames $= updatePrimNames p }

403 | updateForeignImpl : {auto c : Ref Ctxt Defs} -> List (Name, String) -> Core ()

404 | updateForeignImpl xs = update Ctxt { options->foreignImpl $= (xs ++) }

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

408 |                        List (Name, List String) -> Core ()

409 | updateNameDirectives [] = pure ()

410 | updateNameDirectives ((t, ns) :: nds)

411 |     = do update Ctxt { namedirectives $= insert t ns }

412 |          updateNameDirectives nds

415 | updateCGDirectives : {auto c : Ref Ctxt Defs} ->

416 |                      List (CG, String) -> Core ()

417 | updateCGDirectives cgs = update Ctxt { cgdirectives $= nub . (cgs ++) }

420 | updateTransforms : {auto c : Ref Ctxt Defs} ->

421 |                    List (Name, Transform) -> Core ()

422 | updateTransforms [] = pure ()

423 | updateTransforms ((n, t) :: ts)

424 |     = do addT !(toResolvedNames n) !(toResolvedNames t)

425 |          updateTransforms ts

426 |   where

427 |     addT : Name -> Transform -> Core ()

428 |     addT n t

429 |         = do defs <- get Ctxt

430 |              case lookup n (transforms defs) of

431 |                   Nothing =>

432 |                      put Ctxt ({ transforms $= insert n [t] } defs)

433 |                   Just ts =>

434 |                      put Ctxt ({ transforms $= insert n (t :: ts) } defs)

437 | updateFExports : {auto c : Ref Ctxt Defs} ->

438 |                  List (Name, (List (String, String))) -> Core ()

439 | updateFExports [] = pure ()

440 | updateFExports ((n, conv) :: ns)

441 |     = do defs <- get Ctxt

442 |          put Ctxt ({ foreignExports $= insert n conv } defs)

443 |          updateFExports ns

445 | getNSas : (String, (ModuleIdent, Bool, Namespace)) ->

446 |           (ModuleIdent, Namespace)

447 | getNSas (a, (b, c, d)) = (b, d)

455 | readFromTTC : TTC extra =>

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

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

458 |               Bool -> -- set nested namespaces (for records, to use at the REPL)

459 |               FC ->

460 |               Bool -> -- importing as public

461 |               (fname : String) -> -- file containing the module

462 |               (modNS : ModuleIdent) -> -- module namespace

463 |               (importAs : Namespace) -> -- namespace to import as

464 |               Core (Maybe (extra, Int,

465 |                            List (ModuleIdent, Bool, Namespace)))

466 | readFromTTC nestedns loc reexp fname modNS importAs

467 |     = do defs <- get Ctxt

468 |          -- If it's already in the context, with the same visibility flag,

469 |          -- don't load it again (we do need to load it again if it's visible

470 |          -- this time, because we need to reexport the dependencies.)

471 |          let False = (modNS, reexp, importAs) `elem` map snd (allImported defs)

472 |               | True => pure Nothing

473 |          put Ctxt ({ allImported $= ((fname, (modNS, reexp, importAs)) :: ) } defs)

475 |          Right buffer <- coreLift $ readFromFile fname

476 |                | Left err => throw (InternalError (fname ++ ": " ++ show err))

477 |          bin <- newRef Bin buffer -- for reading the file into

478 |          let as = if importAs == miAsNamespace modNS

479 |                      then Nothing

480 |                      else Just importAs

482 |          -- If it's already imported, but without reexporting, then all we're

483 |          -- interested in is returning which other modules to load.

484 |          -- Otherwise, add the data

485 |          if alreadyDone modNS importAs (allImported defs)

486 |             then do ttc <- readTTCFile False fname as bin

487 |                     let ex = extraData ttc

488 |                     pure (Just (ex, ifaceHash ttc, imported ttc))

489 |             else do

490 |                ttc <- readTTCFile True fname as bin

491 |                let ex = extraData ttc

492 |                traverse_ (addGlobalDef modNS (currentNS ttc) as) (context ttc)

493 |                traverse_ (addUserHole True) (userHoles ttc)

494 |                setNS (currentNS ttc)

495 |                when nestedns $ setNestedNS (nestedNS ttc)

496 |                -- Only do the next batch if the module hasn't been loaded

497 |                -- in any form

498 |                unless (modNS `elem` map (fst . getNSas) (allImported defs)) $

499 |                -- Set up typeHints and autoHints based on the loaded data

500 |                  do traverse_ (addTypeHint loc) (typeHints ttc)

501 |                     traverse_ addAutoHint (autoHints ttc)

502 |                     addImportedInc modNS (incData ttc)

503 |                     -- Set up pair/rewrite etc names

504 |                     updatePair (pairnames ttc)

505 |                     updateRewrite (rewritenames ttc)

506 |                     updatePrims (primnames ttc)

507 |                     updateForeignImpl (foreignImpl ttc)

508 |                     updateNameDirectives (reverse (namedirectives ttc))

509 |                     updateCGDirectives (cgdirectives ttc)

510 |                     updateTransforms (transforms ttc)

511 |                     updateFExports (foreignExports ttc)

513 |                when (not reexp) clearSavedHints

514 |                resetFirstEntry

516 |                -- Finally, update the unification state with the holes from the

517 |                -- ttc

518 |                update UST { nextName := nextVar ttc }

519 |                pure (Just (ex, ifaceHash ttc, imported ttc))

520 |   where

521 |     alreadyDone : ModuleIdent -> Namespace ->

522 |                   List (String, (ModuleIdent, Bool, Namespace)) ->

523 |                   Bool

524 |     alreadyDone modns importAs [] = False

525 |       -- If we've already imported 'modns' as 'importAs', or we're importing

526 |       -- 'modns' as itself and it's already imported as anything, then no

527 |       -- need to load again.

528 |     alreadyDone modns importAs ((_, (m, _, a)) :: rest)

529 |         = (modns == m && importAs == a)

530 |           || (modns == m && miAsNamespace modns == importAs)

531 |           || alreadyDone modns importAs rest

536 | getTotalReq : String -> Ref Bin Binary -> Core TotalReq

537 | getTotalReq file b

538 |     = do hdr <- fromBuf {a = String}

539 |          when (hdr /= "TT2") $

540 |            corrupt ("TTC header in " ++ file ++ " " ++ show hdr)

541 |          ver <- fromBuf @{Wasteful}

542 |          checkTTCVersion file ver ttcVersion

543 |          fromBuf -- `totalReq`

548 | getHashes : String -> Ref Bin Binary -> Core (Maybe String, Int)

549 | getHashes file b

550 |     = do ignore $ getTotalReq file b

551 |          sourceFileHash <- fromBuf

552 |          interfaceHash <- fromBuf

553 |          pure (sourceFileHash, interfaceHash)

557 | getImportHashes : String -> Ref Bin Binary ->

558 |                   Core (List (Namespace, Int))

559 | getImportHashes file b

560 |     = do ignore $ getHashes file b

561 |          fromBuf -- `importHashes`

565 | getIncData : String -> Ref Bin Binary ->

566 |              Core (List (CG, String, List String))

567 | getIncData file b

568 |     = do ignore $ getImportHashes file b

569 |          fromBuf -- `incData`

572 | readTotalReq : (fileName : String) -> -- file containing the module

573 |                Core (Maybe TotalReq)

574 | readTotalReq fileName

575 |     = do Right buffer <- coreLift $ readFromFile fileName

576 |             | Left err => pure Nothing

577 |          b <- newRef Bin buffer

578 |          catch (Just <$> getTotalReq fileName b)

579 |                (\err => pure Nothing)

582 | readHashes : (fileName : String) -> -- file containing the module

583 |                 Core (Maybe String, Int)

584 | readHashes fileName

585 |     = do Right buffer <- coreLift $ readFromFile fileName

586 |             | Left err => pure (Nothing, 0)

587 |          b <- newRef Bin buffer

588 |          catch (getHashes fileName b)

589 |                (\err => pure (Nothing, 0))

592 | readImportHashes : (fname : String) -> -- file containing the module

593 |                    Core (List (Namespace, Int))

594 | readImportHashes fname

595 |     = do Right buffer <- coreLift $ readFromFile fname

596 |             | Left err => pure []

597 |          b <- newRef Bin buffer

598 |          catch (do res <- getImportHashes fname b

599 |                    pure res)

600 |                (\err => pure [])

603 | readIncData : (fname : String) -> -- file containing the module

604 |               Core (List (CG, String, List String))

605 | readIncData fname

606 |     = do Right buffer <- coreLift $ readFromFile fname

607 |             | Left err => pure []

608 |          b <- newRef Bin buffer

609 |          catch (do res <- getIncData fname b

610 |                    pure res)

611 |                (\err => pure [])