lean_sys/
io.rs

1/*! IO Helper functions */
2
3use crate::*;
4
5#[inline(always)]
6pub const fn lean_io_mk_world() -> lean_obj_res {
7    lean_box(0)
8}
9
10#[inline(always)]
11pub unsafe fn lean_io_result_is_ok(r: b_lean_obj_arg) -> bool {
12    lean_ptr_tag(r) == 0
13}
14
15#[inline(always)]
16pub unsafe fn lean_io_result_is_error(r: b_lean_obj_arg) -> bool {
17    lean_ptr_tag(r) == 1
18}
19
20#[inline(always)]
21pub unsafe fn lean_io_result_get_value(r: b_lean_obj_arg) -> b_lean_obj_res {
22    debug_assert!(lean_io_result_is_ok(r));
23    lean_ctor_get(r, 0)
24}
25
26#[inline(always)]
27pub unsafe fn lean_io_result_get_error(r: b_lean_obj_arg) -> b_lean_obj_res {
28    debug_assert!(lean_io_result_is_error(r));
29    lean_ctor_get(r, 0)
30}
31
32#[inline(always)]
33pub unsafe fn lean_io_result_take_value(r: lean_obj_arg) -> lean_obj_res {
34    debug_assert!(lean_io_result_is_ok(r));
35    let v = lean_ctor_get(r, 0);
36    lean_inc(v);
37    lean_dec(r);
38    v
39}
40
41#[inline(always)]
42pub unsafe fn lean_io_result_mk_ok(a: lean_obj_arg) -> lean_obj_res {
43    let r = lean_alloc_ctor(0, 2, 0);
44    lean_ctor_set(r, 0, a);
45    lean_ctor_set(r, 1, lean_box(0));
46    r
47}
48
49#[inline(always)]
50pub unsafe fn lean_io_result_mk_error(a: lean_obj_arg) -> lean_obj_res {
51    let r = lean_alloc_ctor(1, 2, 0);
52    lean_ctor_set(r, 0, a);
53    lean_ctor_set(r, 1, lean_box(0));
54    r
55}
56
57extern "C" {
58    pub fn lean_io_error_to_string(err: *mut lean_object) -> *mut lean_object;
59    pub fn lean_decode_io_error(errnum: c_int, fname: b_lean_obj_arg) -> lean_obj_res;
60    pub fn lean_decode_uv_error(errnum: c_int, fname: b_lean_obj_arg) -> lean_obj_res;
61
62    pub fn lean_io_result_show_error(r: b_lean_obj_arg);
63    pub fn lean_io_mark_end_initialization();
64
65    pub fn lean_mk_io_error_already_exists(_: u32, _: lean_obj_arg) -> lean_obj_res;
66    pub fn lean_mk_io_error_already_exists_file(
67        _: lean_obj_arg,
68        _: u32,
69        _: lean_obj_arg,
70    ) -> lean_obj_res;
71    pub fn lean_mk_io_error_eof(_: lean_obj_arg) -> lean_obj_res;
72    pub fn lean_mk_io_error_hardware_fault(_: u32, _: lean_obj_arg) -> lean_obj_res;
73    pub fn lean_mk_io_error_illegal_operation(_: u32, _: lean_obj_arg) -> lean_obj_res;
74    pub fn lean_mk_io_error_inappropriate_type(_: u32, _: lean_obj_arg) -> lean_obj_res;
75    pub fn lean_mk_io_error_inappropriate_type_file(
76        _: lean_obj_arg,
77        _: u32,
78        _: lean_obj_arg,
79    ) -> lean_obj_res;
80    pub fn lean_mk_io_error_interrupted(_: lean_obj_arg, _: u32, _: lean_obj_arg) -> lean_obj_res;
81    pub fn lean_mk_io_error_invalid_argument(_: u32, _: lean_obj_arg) -> lean_obj_res;
82    pub fn lean_mk_io_error_invalid_argument_file(
83        _: lean_obj_arg,
84        _: u32,
85        _: lean_obj_arg,
86    ) -> lean_obj_res;
87    pub fn lean_mk_io_error_no_file_or_directory(
88        _: lean_obj_arg,
89        _: u32,
90        _: lean_obj_arg,
91    ) -> lean_obj_res;
92    pub fn lean_mk_io_error_no_such_thing(_: u32, _: lean_obj_arg) -> lean_obj_res;
93    pub fn lean_mk_io_error_no_such_thing_file(
94        _: lean_obj_arg,
95        _: u32,
96        _: lean_obj_arg,
97    ) -> lean_obj_res;
98    pub fn lean_mk_io_error_other_error(_: u32, _: lean_obj_arg) -> lean_obj_res;
99    pub fn lean_mk_io_error_permission_denied(_: u32, _: lean_obj_arg) -> lean_obj_res;
100    pub fn lean_mk_io_error_permission_denied_file(
101        _: lean_obj_arg,
102        _: u32,
103        _: lean_obj_arg,
104    ) -> lean_obj_res;
105    pub fn lean_mk_io_error_protocol_error(_: u32, _: lean_obj_arg) -> lean_obj_res;
106    pub fn lean_mk_io_error_resource_busy(_: u32, _: lean_obj_arg) -> lean_obj_res;
107    pub fn lean_mk_io_error_resource_exhausted(_: u32, _: lean_obj_arg) -> lean_obj_res;
108    pub fn lean_mk_io_error_resource_exhausted_file(
109        _: lean_obj_arg,
110        _: u32,
111        _: lean_obj_arg,
112    ) -> lean_obj_res;
113    pub fn lean_mk_io_error_resource_vanished(_: u32, _: lean_obj_arg) -> lean_obj_res;
114    pub fn lean_mk_io_error_time_expired(_: u32, _: lean_obj_arg) -> lean_obj_res;
115    pub fn lean_mk_io_error_unsatisfied_constraints(_: u32, _: lean_obj_arg) -> lean_obj_res;
116    pub fn lean_mk_io_error_unsupported_operation(_: u32, _: lean_obj_arg) -> lean_obj_res;
117    pub fn lean_mk_io_user_error(s: lean_obj_arg) -> lean_obj_res;
118}
lean_sys/io.rs

lean_sys/
io.rs
