lean-sys 0.0.8

Bindings to Lean 4's C API
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

/*! Tasks */
use crate::*;

/** Run a closure `Unit -> A` as a `Task A` */
#[inline(always)]
pub unsafe fn lean_task_spawn(c: lean_obj_arg, prio: lean_obj_arg) -> lean_obj_res {
    lean_task_spawn_core(c, lean_unbox(prio) as c_uint, false)
}

/** `Task.bind (x : Task A) (f : A -> Task B) (prio : Nat) : Task B` */
#[inline(always)]
pub unsafe fn lean_task_bind(
    x: lean_obj_arg,
    f: lean_obj_arg,
    sync: u8,
    prio: lean_obj_arg,
) -> lean_obj_res {
    lean_task_bind_core(x, f, lean_unbox(prio) as c_uint, sync != 0, false)
}

/** `Task.map (f : A -> B) (t : Task A) (prio : Nat) : Task B` */
#[inline(always)]
pub unsafe fn lean_task_map(
    f: lean_obj_arg,
    t: lean_obj_arg,
    sync: u8,
    prio: lean_obj_arg,
) -> lean_obj_res {
    lean_task_map_core(f, t, lean_unbox(prio) as c_uint, sync != 0, false)
}

/** Primitive for implementing `Task.get : Task A -> A` */
#[inline]
pub unsafe fn lean_task_get_own(t: b_lean_obj_arg) -> lean_obj_res {
    let r = lean_task_get(t);
    lean_inc(r);
    lean_dec(t);
    r
}

extern "C" {
    pub fn lean_init_task_manager();
    pub fn lean_init_task_manager_using(num_workers: c_uint);
    pub fn lean_finalize_task_manager();
    pub fn lean_task_spawn_core(c: lean_obj_arg, prio: c_uint, keep_alive: bool) -> lean_obj_res;
    /** Convert a value `a : A` into `Task A` */
    pub fn lean_task_pure(a: lean_obj_arg) -> lean_obj_res;
    pub fn lean_task_bind_core(
        x: lean_obj_arg,
        f: lean_obj_arg,
        prio: c_uint,
        sync: bool,
        keep_alive: bool,
    ) -> lean_obj_res;
    pub fn lean_task_map_core(
        f: lean_obj_arg,
        t: lean_obj_arg,
        prio: c_uint,
        sync: bool,
        keep_alive: bool,
    ) -> lean_obj_res;
    pub fn lean_task_get(t: b_lean_obj_arg) -> lean_obj_res;
    /** primitive for implementing `IO.checkCanceled : IO Bool` */
    pub fn lean_io_check_canceled_core() -> bool;
    /** primitive for implementing `IO.cancel : Task a -> IO Unit` */
    pub fn lean_io_cancel_core(t: b_lean_obj_arg);
    /** primitive for implementing `IO.getTaskState : Task a -> IO TaskState` */
    pub fn lean_io_get_task_state_core(t: b_lean_obj_arg) -> u8;
    /** primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a)` */
    pub fn lean_io_wait_any_core(task_list: b_lean_obj_arg) -> b_lean_obj_res;
}