gzclose.c.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Zlib.«gzread.c»
2import ZlibF.Zlib.«gzwrite.c»
3
4/-!
5# gzclose.c — faithful translation
6
7`NO_GZCOMPRESS` is undefined, so the `#ifndef NO_GZCOMPRESS` branch is live.
8-/
9
10namespace Zlib.Gzclose
11open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib
12
13/-- `int ZEXPORT gzclose(gzFile file)` -/
14def gzclose (file : GzFilePtr) : G Int32 := do
15  -- if (file == NULL) return Z_STREAM_ERROR;
16  if file.isNone then return Z_STREAM_ERROR
17  -- state = (gz_statep)file;
18  let state := castState file
19  -- return state->mode == GZ_READ ? gzclose_r(file) : gzclose_w(file);
20  if (← ldS state).mode == GZ_READ then Zlib.Gzread.gzclose_r file else Zlib.Gzwrite.gzclose_w file
21
22end Zlib.Gzclose