lean_sys/
task.rs

1/*! Tasks */
2use crate::*;
3
4/** Run a closure `Unit -> A` as a `Task A` */
5#[inline(always)]
6pub unsafe fn lean_task_spawn(c: lean_obj_arg, prio: lean_obj_arg) -> lean_obj_res {
7    lean_task_spawn_core(c, lean_unbox(prio) as c_uint, false)
8}
9
10/** `Task.bind (x : Task A) (f : A -> Task B) (prio : Nat) : Task B` */
11#[inline(always)]
12pub unsafe fn lean_task_bind(
13    x: lean_obj_arg,
14    f: lean_obj_arg,
15    sync: u8,
16    prio: lean_obj_arg,
17) -> lean_obj_res {
18    lean_task_bind_core(x, f, lean_unbox(prio) as c_uint, sync != 0, false)
19}
20
21/** `Task.map (f : A -> B) (t : Task A) (prio : Nat) : Task B` */
22#[inline(always)]
23pub unsafe fn lean_task_map(
24    f: lean_obj_arg,
25    t: lean_obj_arg,
26    sync: u8,
27    prio: lean_obj_arg,
28) -> lean_obj_res {
29    lean_task_map_core(f, t, lean_unbox(prio) as c_uint, sync != 0, false)
30}
31
32/** Primitive for implementing `Task.get : Task A -> A` */
33#[inline]
34pub unsafe fn lean_task_get_own(t: b_lean_obj_arg) -> lean_obj_res {
35    let r = lean_task_get(t);
36    lean_inc(r);
37    lean_dec(t);
38    r
39}
40
41extern "C" {
42    pub fn lean_init_task_manager();
43    pub fn lean_init_task_manager_using(num_workers: c_uint);
44    pub fn lean_finalize_task_manager();
45    pub fn lean_task_spawn_core(c: lean_obj_arg, prio: c_uint, keep_alive: bool) -> lean_obj_res;
46    /** Convert a value `a : A` into `Task A` */
47    pub fn lean_task_pure(a: lean_obj_arg) -> lean_obj_res;
48    pub fn lean_task_bind_core(
49        x: lean_obj_arg,
50        f: lean_obj_arg,
51        prio: c_uint,
52        sync: bool,
53        keep_alive: bool,
54    ) -> lean_obj_res;
55    pub fn lean_task_map_core(
56        f: lean_obj_arg,
57        t: lean_obj_arg,
58        prio: c_uint,
59        sync: bool,
60        keep_alive: bool,
61    ) -> lean_obj_res;
62    pub fn lean_task_get(t: b_lean_obj_arg) -> lean_obj_res;
63    /** primitive for implementing `IO.checkCanceled : IO Bool` */
64    pub fn lean_io_check_canceled_core() -> bool;
65    /** primitive for implementing `IO.cancel : Task a -> IO Unit` */
66    pub fn lean_io_cancel_core(t: b_lean_obj_arg);
67    /** primitive for implementing `IO.getTaskState : Task a -> IO TaskState` */
68    pub fn lean_io_get_task_state_core(t: b_lean_obj_arg) -> u8;
69}
lean_sys/task.rs

lean_sys/
task.rs
