import REPL.Util.Pickle
import Lean.Replay

open System (FilePath)

namespace Lean.Environment

/--
Pickle an `Environment` to disk.

We only store:
* the list of imports
* the new constants from `Environment.constants`
and when unpickling, we build a fresh `Environment` from the imports,
and then add the new constants.
-/
def pickle (env : Environment) (path : FilePath) : IO Unit :=
  _root_.pickle path (env.header.imports, env.constants.map₂)

/--
Unpickle an `Environment` from disk.

We construct a fresh `Environment` with the relevant imports,
and then replace the new constants.
-/
def unpickle (path : FilePath) : IO (Environment × CompactedRegion) := unsafe do
  let ((imports, map₂), region) ← _root_.unpickle (Array Import × PHashMap Name ConstantInfo) path
  let env ← importModules imports {} 0
  return (← env.replay (HashMap.ofList map₂.toList), region)

end Lean.Environment