Core.Binary

Reading and writing 'Defs' from/to a binary file. In order to be saved, a
name must have been flagged using 'toSave'. (Otherwise we'd save out
everything, not just the things in the current file).

Reexports

Definitions

ttcVersion : Int

  TTC files can only be compatible if the version number is the same
  Update with the current date in YYYY_MM_DD_00 format, or bump the auxiliary
  version number if you're changing the version more than once in the same day.

Visibility: export

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

Visibility: export

writeToTTC : (HasNames extra, TTC extra) => Ref Ctxt Defs => Ref UST UState => extra -> String -> String -> Core ()

Visibility: export

updatePair : Ref Ctxt Defs => Maybe PairNames -> Core ()

Visibility: export

updateRewrite : Ref Ctxt Defs => Maybe RewriteNames -> Core ()

Visibility: export

updatePrimNames : PrimNames -> PrimNames -> PrimNames

Visibility: export

updatePrims : Ref Ctxt Defs => PrimNames -> Core ()

Visibility: export

updateForeignImpl : Ref Ctxt Defs => List (Name, String) -> Core ()

Visibility: export

updateNameDirectives : Ref Ctxt Defs => List (Name, List String) -> Core ()

Visibility: export

updateCGDirectives : Ref Ctxt Defs => List (CG, String) -> Core ()

Visibility: export

updateTransforms : Ref Ctxt Defs => List (Name, Transform) -> Core ()

Visibility: export

updateFExports : Ref Ctxt Defs => List (Name, List (String, String)) -> Core ()

Visibility: export

readFromTTC : TTC extra => Ref Ctxt Defs => Ref UST UState => Bool -> FC -> Bool -> String -> ModuleIdent -> Namespace -> Core (Maybe (extra, (Int, List (ModuleIdent, (Bool, Namespace)))))

Visibility: export

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

Visibility: export

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

Visibility: export

readTotalReq : String -> Core (Maybe TotalReq)

Visibility: export

readHashes : String -> Core (Maybe String, Int)

Visibility: export

readImportHashes : String -> Core (List (Namespace, Int))

Visibility: export

readIncData : String -> Core (List (CG, (String, List String)))

Visibility: export