Module refinement 

Refinement types for constraint-based type checking.

Refinement types extend base types with logical predicates that constrain the valid values of that type. This enables more precise type checking and verification.

Examples

use tensorlogic_ir::refinement::{RefinementType, Refinement};
use tensorlogic_ir::TLExpr;

// Positive integers: {x: Int | x > 0}
let positive_int = RefinementType::new(
    "x",
    "Int",
    TLExpr::gt(TLExpr::pred("x", vec![]), TLExpr::constant(0.0))
);

// Bounded values: {x: Float | x >= 0.0 && x <= 1.0}
let probability = RefinementType::new(
    "x",
    "Float",
    TLExpr::and(
        TLExpr::gte(TLExpr::pred("x", vec![]), TLExpr::constant(0.0)),
        TLExpr::lte(TLExpr::pred("x", vec![]), TLExpr::constant(1.0))
    )
);

Structs

LiquidTypeInference

Liquid types: refinement types with inference.

Refinement

Refinement: a logical predicate that refines a type.

RefinementContext

Refinement type checking context.

RefinementType

Refinement type: base type with a refinement predicate.