Struct RefinementType 

pub struct RefinementType {
    pub base: String,
    pub predicate: String,
}

A refinement type used in liquid type synthesis.

Fields

base: String

The base type (e.g., “Int”, “Bool”).

predicate: String

The refinement predicate as a string (e.g., “v > 0”).

Implementations

impl RefinementType

pub fn new(base: impl Into<String>, predicate: impl Into<String>) -> Self

Construct a new refinement type.

use oxilean_std::program_synthesis::RefinementType;
let rt = RefinementType::new("Int", "v >= 0");
assert_eq!(rt.base, "Int");

pub fn is_trivial(&self) -> bool

Check whether the predicate is trivially true (empty string).

pub fn strengthen(&self, extra: impl Into<String>) -> Self

Return a strengthened type by conjoining an extra predicate.

pub fn weaken(&self, extra: impl Into<String>) -> Self

Return a weakened type by disjoining an extra predicate.

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.

impl PartialEq for RefinementType

fn eq(&self, other: &RefinementType) -> 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 Eq for RefinementType

impl StructuralPartialEq for RefinementType