lean-rs 0.1.1

Safe Rust bindings for Lean 4 interop: runtime initialization, object handles, typed ABI conversions, module loading, exported function calls, semantic handles, and callback handles.
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113

//! Lean `Prod` ABI support for small Rust tuples.
//!
//! Rust argument tuples normally describe a function's arity for
//! [`crate::LeanExported`]. These impls are different: they encode a
//! tuple *as one Lean value* when a Lean export itself takes a product
//! argument, e.g. `Expr × Expr × UInt8`.

#![allow(unsafe_code)]

use lean_rs_sys::lean_object;

use crate::abi::structure::{alloc_ctor_with_objects, take_ctor_objects};
use crate::abi::traits::{IntoLean, LeanAbi, TryFromLean, sealed};
use crate::error::LeanResult;
use crate::runtime::LeanRuntime;
use crate::runtime::obj::Obj;

impl<'lean, A, B> IntoLean<'lean> for (A, B)
where
    A: IntoLean<'lean>,
    B: IntoLean<'lean>,
{
    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
        let (a, b) = self;
        alloc_ctor_with_objects(runtime, 0, [a.into_lean(runtime), b.into_lean(runtime)])
    }
}

impl<'lean, A, B> TryFromLean<'lean> for (A, B)
where
    A: TryFromLean<'lean>,
    B: TryFromLean<'lean>,
{
    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
        let [a, b] = take_ctor_objects::<2>(obj, 0, "Prod.mk")?;
        Ok((A::try_from_lean(a)?, B::try_from_lean(b)?))
    }
}

impl<A, B> sealed::SealedAbi for (A, B) {}

impl<'lean, A, B> LeanAbi<'lean> for (A, B)
where
    A: IntoLean<'lean> + TryFromLean<'lean>,
    B: IntoLean<'lean> + TryFromLean<'lean>,
{
    type CRepr = *mut lean_object;

    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
        self.into_lean(runtime).into_raw()
    }

    #[allow(
        clippy::not_unsafe_ptr_arg_deref,
        reason = "sealed trait — called only by LeanExported"
    )]
    fn from_c(c: Self::CRepr, runtime: &'lean LeanRuntime) -> LeanResult<Self> {
        // SAFETY: `c` carries one owned refcount returned from a Lean
        // export whose result type is a product.
        let obj = unsafe { Obj::from_owned_raw(runtime, c) };
        Self::try_from_lean(obj)
    }
}

impl<'lean, A, B, C> IntoLean<'lean> for (A, B, C)
where
    A: IntoLean<'lean>,
    B: IntoLean<'lean>,
    C: IntoLean<'lean>,
{
    fn into_lean(self, runtime: &'lean LeanRuntime) -> Obj<'lean> {
        let (a, b, c) = self;
        (a, (b, c)).into_lean(runtime)
    }
}

impl<'lean, A, B, C> TryFromLean<'lean> for (A, B, C)
where
    A: TryFromLean<'lean>,
    B: TryFromLean<'lean>,
    C: TryFromLean<'lean>,
{
    fn try_from_lean(obj: Obj<'lean>) -> LeanResult<Self> {
        let (a, (b, c)) = <(A, (B, C))>::try_from_lean(obj)?;
        Ok((a, b, c))
    }
}

impl<A, B, C> sealed::SealedAbi for (A, B, C) {}

impl<'lean, A, B, C> LeanAbi<'lean> for (A, B, C)
where
    A: IntoLean<'lean> + TryFromLean<'lean>,
    B: IntoLean<'lean> + TryFromLean<'lean>,
    C: IntoLean<'lean> + TryFromLean<'lean>,
{
    type CRepr = *mut lean_object;

    fn into_c(self, runtime: &'lean LeanRuntime) -> Self::CRepr {
        self.into_lean(runtime).into_raw()
    }

    #[allow(
        clippy::not_unsafe_ptr_arg_deref,
        reason = "sealed trait — called only by LeanExported"
    )]
    fn from_c(c: Self::CRepr, runtime: &'lean LeanRuntime) -> LeanResult<Self> {
        // SAFETY: `c` carries one owned refcount returned from a Lean
        // export whose result type is a product.
        let obj = unsafe { Obj::from_owned_raw(runtime, c) };
        Self::try_from_lean(obj)
    }
}