max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove unnecessary getByte/putByte IO primitives

Browse source
This commit is contained in:
Sebastian Ullrich 2020-06-03 14:18:00 +02:00
parent a64e78b90b
commit f4c28fbe5f
2 changed files with 0 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/System/IO.lean
View file

@ -133,11 +133,6 @@ constant Handle.read (h : @& Handle) (bytes : USize) : IO ByteArray := arbitrar
@[extern "lean_io_prim_handle_write"]
constant Handle.write (h : @& Handle) (buffer : @& ByteArray) : IO Unit := arbitrary _
@[extern "lean_io_prim_handle_read_byte"]
constant Handle.getByte (h : @& Handle) : IO UInt8 := arbitrary _
@[extern "lean_io_prim_handle_write_byte"]
constant Handle.putByte (h : @& Handle) (c : UInt8) : IO Unit := arbitrary _
@[extern "lean_io_prim_handle_get_line"]
constant Handle.getLine (h : @& Handle) : IO String := arbitrary _
@[extern "lean_io_prim_handle_put_str"]
@ -178,8 +173,6 @@ def Handle.isEof : Handle → m Bool := Prim.liftIO ∘ Prim.Handle.isEof
def Handle.flush : Handle → m Unit := Prim.liftIO ∘ Prim.Handle.flush
def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := Prim.liftIO (Prim.Handle.read h (USize.ofNat bytes))
def Handle.write (h : Handle) (s : ByteArray) : m Unit := Prim.liftIO (Prim.Handle.write h s)
def Handle.getByte (h : Handle) : m UInt8 := Prim.liftIO (Prim.Handle.getByte h)
def Handle.putByte (h : Handle) (b : UInt8) : m Unit := Prim.liftIO (Prim.Handle.putByte h b)
def Handle.getLine : Handle → m String := Prim.liftIO ∘ Prim.Handle.getLine

21
src/runtime/io.cpp
View file

@ -275,27 +275,6 @@ extern "C" obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) {
}
}
/* Handle.readByte : (@& Handle) → IO UInt8 */
extern "C" obj_res lean_io_prim_handle_read_byte(b_obj_arg h, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
int c = std::fgetc(fp);
if (c != EOF) {
return set_io_result(box(c));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
/* Handle.writeByte : (@& Handle) → UInt8 → IO unit */
extern "C" obj_res lean_io_prim_handle_write_byte(b_obj_arg h, uint8 c, obj_arg /* w */) {
FILE * fp = io_get_handle(h);
if (std::fputc(c, fp) != EOF) {
return set_io_result(box(0));
} else {
return set_io_error(decode_io_error(errno, nullptr));
}
}
static object * g_io_error_eof = nullptr;
/* Handle.read : (@& Handle) → USize → IO ByteArray */