/*!
Adapted from a file automatically generated by rust-bindgen 0.60.1 from `lean.h`.
Comments adapted from `lean.h`.
*/

mod incomplete_array;
use core::ffi::{c_char, c_int, c_uint, c_void};

pub use incomplete_array::*;

/**
Lean object header.

The reference counter `m_rc` field also encodes whether the object is single threaded (> 0), multi threaded (< 0), or
reference counting is not needed (== 0). We don't use reference counting for objects stored in compact regions, or
marked as persistent.

For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
stored in compact regions, we use the page information to retrieve its size.

During deallocation and 64-bit machines, the fields `m_rc` and `m_cs_sz` store the next object in the deletion TODO list.
These two fields together have 48-bits, and this is enough for modern computers.
In 32-bit machines, the field `m_rc` is sufficient.

The field `m_other` is used to store the number of fields in a constructor object and the element size in a scalar array.
*/
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_object {
    pub m_rc: c_int,
    pub m_cs_sz: u16,
    pub m_other: u8,
    pub m_tag: u8,
}

/// Standard object argument
pub type lean_obj_arg = *mut lean_object;
/// Borrowed object argument
pub type b_lean_obj_arg = *mut lean_object;
/// Unique (aka non shared) object argument
pub type u_lean_obj_arg = *mut lean_object;
/// Standard object result
pub type lean_obj_res = *mut lean_object;
/// Borrowed object result
pub type b_lean_obj_res = *mut lean_object;

#[repr(C)]
#[derive(Debug)]
pub struct lean_ctor_object {
    pub m_header: lean_object,
    pub m_objs: IncompleteArrayField<*mut lean_object>,
}

/// Array arrays
#[repr(C)]
#[derive(Debug)]
pub struct lean_array_object {
    pub m_header: lean_object,
    pub m_size: usize,
    pub m_capacity: usize,
    pub m_data: IncompleteArrayField<*mut lean_object>,
}

/// Scalar arrays
#[repr(C)]
#[derive(Debug)]
pub struct lean_sarray_object {
    pub m_header: lean_object,
    pub m_size: usize,
    pub m_capacity: usize,
    pub m_data: IncompleteArrayField<u8>,
}

#[repr(C)]
#[derive(Debug)]
pub struct lean_string_object {
    pub m_header: lean_object,
    /// Byte length including `\0` terminator
    pub m_size: usize,
    pub m_capacity: usize,
    /// UTF-8 length
    pub m_length: usize,
    pub m_data: IncompleteArrayField<c_char>,
}

#[repr(C)]
#[derive(Debug)]
pub struct lean_closure_object {
    pub m_header: lean_object,
    pub m_fun: *mut c_void,
    /// Number of arguments expected by `m_fun`
    pub m_arity: u16,
    //TODO: already been fixed?
    /// Number of arguments that have been already fixed
    pub m_num_fixed: u16,
    pub m_objs: IncompleteArrayField<*mut lean_object>,
}

#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_ref_object {
    pub m_header: lean_object,
    pub m_value: *mut lean_object,
}

#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_thunk_object {
    pub m_header: lean_object,
    pub m_value: u64,
    pub m_closure: u64,
}

/** Data required for executing a Lean task. It is released as soon as
the task terminates even if the task object itself is still referenced. */
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_task_imp {
    pub m_closure: *mut lean_object,
    pub m_head_dep: *mut lean_task,
    pub m_next_dep: *mut lean_task,
    pub m_prio: c_uint,
    pub m_canceled: u8,
    /// If true, task will not be freed until finished
    pub m_keep_alive: u8,
    pub m_deleted: u8,
}

/** Object of type `Task _`. The lifetime of a `lean_task` object can be represented as a state machine with atomic
state transitions.

In the following, `condition` describes a predicate uniquely identifying a state.

creation:
* Task.spawn ==> Queued
* Task.map/bind ==> Waiting
* Task.pure ==> Finished
* Promise.new ==> Promised

states:
* Queued
  * condition: in `task_manager::m_queues && m_imp != nullptr && !m_imp->m_deleted`
  * invariant: `m_value == nullptr`
  * transition: RC becomes 0 ==> Deactivated (`deactivate_task` lock)
  * transition: dequeued by worker thread            ==> Running     (`spawn_worker` lock)
* Waiting
  * condition: reachable from task via `m_head_dep->m_next_dep->... && !m_imp->m_deleted`
  * invariant: `m_imp != nullptr && m_value == nullptr`
  * invariant: task dependency is Queued/Waiting/Running
    * It cannot become Deactivated because this task should be holding an owned reference to it
  * transition: RC becomes 0 ==> Deactivated (`deactivate_task` lock)
  * transition: task dependency Finished ==> Queued (`handle_finished` under `spawn_worker` lock)
* Promised
  * condition: obtained as result from promise
  * invariant: `m_imp != nullptr && m_value == nullptr`
  * transition: promise resolved ==> Finished (`resolve_core` under `spawn_worker` lock)
  * transition: RC becomes 0 ==> Deactivated (`deactivate_task` lock)
* Running
  * condition: `m_imp != nullptr && m_imp->m_closure == nullptr`
    * The worker takes ownership of the closure when running it
  * invariant: `m_value == nullptr`
  * transition: RC becomes 0 ==> Deactivated (`deactivate_task` lock)
  * transition: finished execution                   ==> Finished    (`spawn_worker` lock)
* Deactivated
  * condition: `m_imp != nullptr && m_imp->m_deleted`
  * invariant: `RC == 0`
  * invariant: `m_imp->m_closure == nullptr && m_imp->m_head_dep == nullptr` (both freed by `deactivate_task_core`)
    * Note that all dependent tasks must have already been Deactivated by the converse of the second Waiting invariant
  * invariant: `m_value == nullptr`
  * transition: dequeued by worker thread   ==> freed
  * transition: finished execution          ==> freed
  * transition: task dependency Finished    ==> freed
  * We must keep the task object alive until one of these transitions because in either case, we have live
    (internal, unowned) references to the task up to that point
  * transition: task dependency Deactivated ==> freed
* Finished
  * condition: `m_value != nullptr`
  * invariant: `m_imp == nullptr`
  * transition: RC becomes 0 ==> freed (`deactivate_task` lock)
*/
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_task {
    pub m_header: lean_object,
    pub m_value: u64,
    pub m_imp: *mut lean_task_imp,
}

pub type lean_task_object = lean_task;
pub type lean_external_finalize_proc = Option<unsafe extern "C" fn(arg1: *mut c_void)>;
pub type lean_external_foreach_proc =
    Option<unsafe extern "C" fn(arg1: *mut c_void, arg2: b_lean_obj_arg)>;

/* Object for wrapping external data. */
#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_external_class {
    pub m_finalize: lean_external_finalize_proc,
    pub m_foreach: lean_external_foreach_proc,
}

#[repr(C)]
#[derive(Debug, Copy, Clone)]
pub struct lean_external_object {
    pub m_header: lean_object,
    pub m_class: *mut lean_external_class,
    pub m_data: *mut c_void,
}