Crate type_eval 

type_eval provides data and evaluation types to the compiler, unburdened by the limitations of execution code semantics.

Erase requirement of machine representation:

#[deprecated(note="use NumRet<DivExpr> instead")]
use core::ops::Div;
use core::cmp::Eq;
pub const fn safe_div_u32(numerator: u32, denominator: u32) -> Option<u32> {
    if denominator == 0 {
        None
    } else {
        Some(numerator / denominator)
    }
}

use type_eval::{NumRet, /* MemRep */};
fn main() {
    // let safe_dived = safe_div(4u16, 2usize);
    // TODO: memory representatiov will be released very shortly
    // let safe_dived = NumRet<DivExp<U4, U2>>::U32;
}

Enforce predicates/preconditions into the type-system:

 // define functions that carry a proof of evaluation result
 const fn _b0<E: NumExpr<Ret = U0>>() {}
 const fn _b1<E: NumExpr<Ret = U1>>() {}
 const fn _b2<E: NumExpr<Ret = U2>>() {}
 const fn _b3<E: NumExpr<Ret = U3>>() {}
 #[allow(non_upper_case_globals)]
 fn add_sub() {
     const _2_ADD_1__SUB_3: () = _b0::<SubExp<AddExp<U2, U1>, U3>>();
     const _6_SUB__1_ADD_3: () = _b2::<SubExp<U6, AddExp<U1, U3>>>();
     // const COMPILE_FAIL: () = _b2::<SubExp<U7, AddExp<U1, U3>>>();

 }

 fn shift_msb() {
     const _MSB__2_SHL_1: () = _b2::<MSB<ShLExp<U2, U1>>>();
     const _MSB__2_SHL_0: () = _b1::<MSB<ShLExp<U2, U0>>>();

     const _MSB_4__SUB__MSB_3: () = _b1::<SubExp<MSB<U4>, MSB<U3>>>();
     const _MSB_4__ADD__MSB_3: () = _b3::<AddExp<MSB<U4>, MSB<U3>>>();
 }

 fn ifs() {
     // if (1/2) < 1 {0} else {1 / 0}
     const _IF_T_U0_DIV0: () = _b0::<IF<LT<DivExp<U1, U2>, U1>, U0, DivExp<U1, U0>>>();
     // div-by-zero is a compile fail
     // const _COMPILE_FAIL: () = _b0::<DivExp<U1, U0>>();
 }

 fn lt4() {
     // define a function that carries a proof of evaluaton result < 6
     const fn _lt6<E: NumExpr>()
     where
         LT<E::Ret, U6>: BoolExpr<Ret = True>,
     {
     }

     // 2 + 3 < 6
     const _5_LT_6: () = _lt6::<AddExp<U2, U3>>();
     // 2 * 3 !< 6
     // const FAIL: () = _lt6::<MulExp<U2, U3>>();
 }

let’s observe the compilation failure:

fn lt4() {
    // define a function that carries a proof of evaluaton result < 6
    const fn _lt6<E: NumExpr>()
    where
        LT<E::Ret, U6>: BoolExpr<Ret = True>,
    {}

    // 2 * 3 !< 6
    const FAIL: () = _lt6::<MulExp<U2, U3>>();
}

Propogate predicates/preconditions downstream via the type-system:

Enforce co-veraiance of predicates when extending traits In this example, a submatrix of XS/XY dimensions wants to be contained within a “parent” matrix of X/Y dimension

The top-left corner (let’s call it XC/YCof the sub-matrix is constrained so it’s wholely contained within the parent matrix. i.e.

XC + XS < X && YC + YS < Y

 use type_eval::{prelude::*, BoolExpr};
 // A keyboard matrix trait.
 trait KBMatrix
 // TODO: impl non-zero
 // where
 //     GTE<Self::Width, U1>: BoolExpr<Ret = True>,
 //     GTE<Self::Height, U1>: BoolExpr<Ret = True>,
 {
     type Width: NumberVal;
     type Height: NumberVal;
 }
 // a convenience definition to get a parent-matrix width and height
 type ParentWidth<S: SubMatrix> = <S::Parent as KBMatrix>::Width;
 type ParentHeight<S: SubMatrix> = <S::Parent as KBMatrix>::Height;
 // You can define a sub matrix such that the compiler will cause an error
 // if it's not contained within the parent matrix
 trait SubMatrix
 where
     GTE<Self::Width, U1>: BoolExpr<Ret = True>,
     GTE<Self::Height, U1>: BoolExpr<Ret = True>,
     // this is effectively `assert!(x + width <= parent.width)`, but in the type system
     LTE<AddExp<Self::Width, Self::XLoc>, ParentWidth<Self>>: BoolExpr<Ret = True>,
     // this is effectively `assert!(y + height <= parent.height)`, but in the type system
     LTE<AddExp<Self::Height, Self::YLoc>, ParentHeight<Self>>: BoolExpr<Ret = True>,
 {
     type Parent: KBMatrix;
     type Width: NumberVal;
     type XLoc: NumberVal;
     type Height: NumberVal;
     type YLoc: NumberVal;
 }

Modules

_inners

Inner implementation types. Generally not intended for end-use

ctrl_types

Implementors of BoolExpr

num_vals

Integers expressed as types, e.g.: prelude::U0, prelude::U1

op_types

Implementors of NumExpr

prelude

val_types

Constructors for numbers expressed at the type-level

Traits

BoolExpr

An expression returning a prelude::BoolVal

NumExpr

An expression returning a prelude::NumberVal

OrdExpr

An expression returning a prelude::BoolVal

Type Aliases

BoolRet

<T as BoolExpr>::Ret helper

NumRet

<T as NumExpr>::Ret helper

OrdRet

<T as BoolExpr>::Ret helper