Macro mononym::proof [−][src]
macro_rules! proof {
($($proof : ident $(< $($proof_param : ident), + $(,) ? >) ?
($($suchthat : ident $(: $suchtype : ty) ?), * $(,) ?) ;) +) => { ... };
}
Expand description
Macro to help define a new proof type.
Suppose we want to write a module that tests whether a
named i64
is greater or equal to 0, and return a proof
of it. We could define the proof type manually as follows:
mod natural {
use mononym::*;
use core::marker::PhantomData;
pub struct IsNatural<NumVal: HasType<i64>>(PhantomData<NumVal>);
impl <NumVal: HasType<i64>> IsNatural<NumVal> {
fn new() -> Self {
Self(PhantomData)
}
}
pub fn is_natural<NumVal: HasType<i64>>(
num: &Named<NumVal, i64>,
) -> Option<IsNatural<NumVal>>
{
if *num.value() >= 0 {
Some(IsNatural::new())
} else {
None
}
}
}
We define IsNatural
as a proof type for a named i64
value
with the name NumVal
that shows that the number is greater
or equal to 0. The type has a private
PhantomData
body, as the
existence of the proof value alone is sufficient. It provides
a private new()
method that allows functions to construct
the proof object.
The function is_natural
then accepts a named number value
with the name NumVal
, and only constructs the
proof IsNatural<NumVal>
using IsNatural::new()
if the condition is satisfied.
As we define more proof types, the need to manually define
the proof structs and methods can become tedious. The
proof!
macro simplifies the definition such as
above so that we can write our code as follows:
mod natural {
use mononym::*;
proof! {
IsNatural(num: i64);
}
pub fn is_natural<NumVal: HasType<i64>>(
num: &Named<NumVal, i64>,
) -> Option<IsNatural<NumVal>>
{
if *num.value() >= 0 {
Some(IsNatural::new())
} else {
None
}
}
}
Note that the new version of the natural
module is the same as
the original version. proof!
takes care of generating
the struct definition and the private new
method, so that
we do not need to keep repeating the same boilerplate definition.