Enum DependentType 

pub enum DependentType {
    Base(ParametricType),
    Vector {
        length: IndexExpr,
        element_type: Box<DependentType>,
    },
    Matrix {
        rows: IndexExpr,
        cols: IndexExpr,
        element_type: Box<DependentType>,
    },
    Tensor {
        shape: Vec<IndexExpr>,
        element_type: Box<DependentType>,
    },
    DependentFunction {
        param_name: String,
        param_type: Box<DependentType>,
        return_type: Box<DependentType>,
    },
    Refinement {
        var_name: String,
        base_type: Box<DependentType>,
        predicate: Term,
    },
    Constrained {
        base_type: Box<DependentType>,
        constraints: Vec<DimConstraint>,
    },
}

Dependent type: types that depend on runtime values.

Examples:

• Vec<n, T>: Vector of length n with elements of type T
• Matrix<m, n, T>: Matrix with dimensions m×n
• (x: Int) -> Vec<x, Bool>: Function returning a vector of length x

Variants

Base(ParametricType)

Base parametric type (non-dependent)

Vector

Vector with dependent length: Vec<n, T>

Fields

length: IndexExpr

element_type: Box<DependentType>

Matrix

Matrix with dependent dimensions: Matrix<rows, cols, T>

Fields

rows: IndexExpr

cols: IndexExpr

element_type: Box<DependentType>

Tensor

Tensor with dependent shape: Tensor<[d1, d2, …], T>

Fields

shape: Vec<IndexExpr>

element_type: Box<DependentType>

DependentFunction

Dependent function type: (x: T1) -> T2(x)

Fields

param_name: String

param_type: Box<DependentType>

return_type: Box<DependentType>

Refinement

Refinement type: {x: T | P(x)}

Fields

var_name: String

base_type: Box<DependentType>

predicate: Term

Constrained

Constrained type: T where C

Fields

base_type: Box<DependentType>

constraints: Vec<DimConstraint>

Implementations

impl DependentType

pub fn base(param_type: ParametricType) -> Self

Create a base non-dependent type

pub fn vector(length: IndexExpr, element_type: impl Into<String>) -> Self

Create a dependent vector type

pub fn matrix( rows: IndexExpr, cols: IndexExpr, element_type: impl Into<String>, ) -> Self

Create a dependent matrix type

pub fn tensor(shape: Vec<IndexExpr>, element_type: impl Into<String>) -> Self

Create a dependent tensor type

pub fn dependent_function( param_name: impl Into<String>, param_type: DependentType, return_type: DependentType, ) -> Self

Create a dependent function type

pub fn refinement( var_name: impl Into<String>, base_type: DependentType, predicate: Term, ) -> Self

Create a refinement type

pub fn with_constraints(self, constraints: Vec<DimConstraint>) -> Self

Add constraints to a type

pub fn free_index_vars(&self) -> HashSet<String>

Get all free index variables

pub fn is_well_formed(&self) -> bool

Check if this type is well-formed (no unbound index variables)

Trait Implementations

impl Clone for DependentType

fn clone(&self) -> DependentType

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for DependentType

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for DependentType

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Display for DependentType

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for DependentType

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for DependentType

fn eq(&self, other: &DependentType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for DependentType

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for DependentType

impl StructuralPartialEq for DependentType