Struct RefinementType 

pub struct RefinementType {
    pub base_type: String,
    pub name: Option<String>,
    pub predicates: Vec<RefinementPredicate>,
    pub description: Option<String>,
}

A refinement type combining a base type with predicates.

Fields

base_type: String

Base type name

name: Option<String>

Optional refined name (e.g., “PositiveInt” for Int{x > 0})

predicates: Vec<RefinementPredicate>

Predicates that constrain values

description: Option<String>

Description of the refinement

Implementations

impl RefinementType

pub fn new(base_type: impl Into<String>) -> Self

Create a new refinement type with a base type.

pub fn with_name(self, name: impl Into<String>) -> Self

Set the refined name.

pub fn with_predicate(self, predicate: RefinementPredicate) -> Self

Add a predicate to the refinement.

pub fn with_description(self, description: impl Into<String>) -> Self

Set the description.

pub fn check(&self, value: f64) -> bool

Check if a value satisfies this refinement type.

pub fn check_with_context( &self, value: f64, context: &RefinementContext, ) -> bool

Check if a value satisfies this refinement type with context.

pub fn type_name(&self) -> &str

Get the effective name of this type.

pub fn is_subtype_of(&self, other: &RefinementType) -> bool

Check if this is a subtype of another refinement type.

A refinement type A is a subtype of B if:

1. They have the same base type
2. A’s predicates imply B’s predicates

This implementation uses semantic implication checking for common predicate patterns, providing a practical alternative to full SMT solving while handling most real-world cases.

pub fn free_variables(&self) -> Vec<String>

Get all free variables referenced in predicates.

pub fn to_string_repr(&self) -> String

Convert to human-readable representation.

Trait Implementations

impl Clone for RefinementType

fn clone(&self) -> RefinementType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RefinementType

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

Formats the value using the given formatter.