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

feat: add IO.FS.rename

Browse source
This commit is contained in:
Mario Carneiro 2023-07-21 22:40:15 -04:00 • committed by Sebastian Ullrich
parent 7809d49a62
commit dd313c6894
2 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -294,6 +294,14 @@ end Handle
@[extern "lean_io_remove_dir"] opaque removeDir : @& FilePath → IO Unit
@[extern "lean_io_create_dir"] opaque createDir : @& FilePath → IO Unit
/--
Moves a file or directory `old` to the new location `new`.
This function coincides with the [POSIX `rename` function](https://pubs.opengroup.org/onlinepubs/9699919799/functions/rename.html),
see there for more information.
-/
@[extern "lean_io_rename"] opaque rename (old new : @& FilePath) : IO Unit
end FS
@[extern "lean_io_getenv"] opaque getEnv (var : @& String) : BaseIO (Option String)

11
src/runtime/io.cpp
View file

@ -657,6 +657,17 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) {
}
}
extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to) {
if (std::rename(string_cstr(from), string_cstr(to)) == 0) {
return io_result_mk_ok(box(0));
} else {
std::ostringstream s;
s << string_cstr(from) << " and/or " << string_cstr(to);
object_ref out{mk_string(s.str())};
return io_result_mk_error(decode_io_error(errno, out.raw()));
}
}
extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg fname, obj_arg) {
if (std::remove(string_cstr(fname)) == 0) {
return io_result_mk_ok(box(0));