Implementation

Types and Predicates

A type is either a refinement of a base type or a dependent arrow that names its argument so the result can mention it.

#![allow(unused)]
fn main() {
use std::fmt;
#[derive(Debug, Clone, PartialEq)]
pub enum BaseTy {
    Int,
    Bool,
}
impl fmt::Display for BaseTy {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            BaseTy::Int => write!(f, "Int"),
            BaseTy::Bool => write!(f, "Bool"),
        }
    }
}
impl Type {
    pub fn base(b: BaseTy) -> Type {
        Type::Refine("v".to_string(), b, Pred::Bool(true))
    }

    pub fn is_trivial(&self) -> bool {
        matches!(self, Type::Refine(_, _, Pred::Bool(true)))
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Pred {
    Bool(bool),
    Int(i64),
    Var(String),
    Bin(BinOp, Box<Pred>, Box<Pred>),
    Not(Box<Pred>),
    Neg(Box<Pred>),
}
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum BinOp {
    Add,
    Sub,
    Mul,
    Eq,
    Ne,
    Lt,
    Le,
    Gt,
    Ge,
    And,
    Or,
    Implies,
}
impl BinOp {
    pub fn is_arith(self) -> bool {
        matches!(self, BinOp::Add | BinOp::Sub | BinOp::Mul)
    }

    pub fn is_cmp(self) -> bool {
        matches!(
            self,
            BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge
        )
    }

    pub fn is_bool(self) -> bool {
        matches!(self, BinOp::And | BinOp::Or | BinOp::Implies)
    }

    pub fn as_str(self) -> &'static str {
        match self {
            BinOp::Add => "+",
            BinOp::Sub => "-",
            BinOp::Mul => "*",
            BinOp::Eq => "=",
            BinOp::Ne => "!=",
            BinOp::Lt => "<",
            BinOp::Le => "<=",
            BinOp::Gt => ">",
            BinOp::Ge => ">=",
            BinOp::And => "&&",
            BinOp::Or => "||",
            BinOp::Implies => "==>",
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Expr {
    Int(i64),
    Bool(bool),
    Var(String),
    Let(String, Box<Expr>, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Lam(String, Type, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Ann(Box<Expr>, Type),
    Bin(BinOp, Box<Expr>, Box<Expr>),
    Not(Box<Expr>),
    Neg(Box<Expr>),
}
impl fmt::Display for Pred {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write_pred(f, self, 0)
    }
}
fn prec(op: BinOp) -> u8 {
    match op {
        BinOp::Or | BinOp::Implies => 1,
        BinOp::And => 2,
        BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge => 3,
        BinOp::Add | BinOp::Sub => 4,
        BinOp::Mul => 5,
    }
}
fn write_pred(f: &mut fmt::Formatter<'_>, p: &Pred, ctx: u8) -> fmt::Result {
    match p {
        Pred::Bool(b) => write!(f, "{}", b),
        Pred::Int(n) => write!(f, "{}", n),
        Pred::Var(x) => write!(f, "{}", x),
        Pred::Not(inner) => {
            write!(f, "!")?;
            write_pred(f, inner, 6)
        }
        Pred::Neg(inner) => {
            write!(f, "-")?;
            write_pred(f, inner, 6)
        }
        Pred::Bin(op, a, b) => {
            let p = prec(*op);
            let need = p < ctx;
            if need {
                write!(f, "(")?;
            }
            write_pred(f, a, p)?;
            write!(f, " {} ", op.as_str())?;
            write_pred(f, b, p + 1)?;
            if need {
                write!(f, ")")?;
            }
            Ok(())
        }
    }
}
impl fmt::Display for Type {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Type::Refine(v, b, Pred::Bool(true)) => {
                let _ = v;
                write!(f, "{}", b)
            }
            Type::Refine(v, b, p) => write!(f, "{{ {} : {} | {} }}", v, b, p),
            Type::Fun(x, t1, t2) => {
                let dep = mentions(t2, x);
                let left = match t1.as_ref() {
                    Type::Fun(_, _, _) => format!("({})", t1),
                    _ => format!("{}", t1),
                };
                if dep {
                    write!(f, "({} : {}) -> {}", x, left, t2)
                } else {
                    write!(f, "{} -> {}", left, t2)
                }
            }
        }
    }
}
pub fn mentions(t: &Type, x: &str) -> bool {
    match t {
        Type::Refine(v, _, p) => v != x && pred_mentions(p, x),
        Type::Fun(y, t1, t2) => mentions(t1, x) || (y != x && mentions(t2, x)),
    }
}
pub fn pred_mentions(p: &Pred, x: &str) -> bool {
    match p {
        Pred::Var(y) => y == x,
        Pred::Bin(_, a, b) => pred_mentions(a, x) || pred_mentions(b, x),
        Pred::Not(a) | Pred::Neg(a) => pred_mentions(a, x),
        _ => false,
    }
}
impl fmt::Display for Expr {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write_expr(f, self, 0)
    }
}
fn expr_prec(e: &Expr) -> u8 {
    match e {
        Expr::Let(_, _, _) | Expr::If(_, _, _) | Expr::Lam(_, _, _) | Expr::Ann(_, _) => 0,
        Expr::Bin(op, _, _) => prec(*op),
        Expr::App(_, _) | Expr::Not(_) | Expr::Neg(_) => 7,
        _ => 8,
    }
}
fn write_expr(f: &mut fmt::Formatter<'_>, e: &Expr, ctx: u8) -> fmt::Result {
    let p = expr_prec(e);
    let need = p < ctx;
    if need {
        write!(f, "(")?;
    }
    match e {
        Expr::Int(n) => write!(f, "{}", n)?,
        Expr::Bool(b) => write!(f, "{}", b)?,
        Expr::Var(x) => write!(f, "{}", x)?,
        Expr::Let(x, v, body) => write!(f, "let {} = {} in {}", x, v, body)?,
        Expr::If(c, a, b) => write!(f, "if {} then {} else {}", c, a, b)?,
        Expr::Lam(x, t, body) => write!(f, "\\{} : {} -> {}", x, t, body)?,
        Expr::App(g, a) => {
            write_expr(f, g, 7)?;
            write!(f, " ")?;
            write_expr(f, a, 8)?;
        }
        Expr::Ann(e, t) => write!(f, "({} : {})", e, t)?,
        Expr::Bin(op, a, b) => {
            write_expr(f, a, p)?;
            write!(f, " {} ", op.as_str())?;
            write_expr(f, b, p + 1)?;
        }
        Expr::Not(a) => {
            write!(f, "!")?;
            write_expr(f, a, 7)?;
        }
        Expr::Neg(a) => {
            write!(f, "-")?;
            write_expr(f, a, 7)?;
        }
    }
    if need {
        write!(f, ")")?;
    }
    Ok(())
}
#[derive(Debug, Clone, PartialEq)]
pub enum Type {
    // { v : B | phi }
    Refine(String, BaseTy, Pred),
    // (x : T1) -> T2
    Fun(String, Box<Type>, Box<Type>),
}
}

The Refine(v, B, phi) constructor is the type \(\{v : B \mid \varphi\}\), with three fields: v is the value variable bound inside the predicate, B is the underlying base type (Int or Bool), and phi is the predicate that must hold of v. The Fun(x, t1, t2) constructor is the dependent arrow (x : t1) -> t2, with three fields: x is the binder name that the result type may reference, t1 is the argument type, and t2 is the result type. The result t2 may freely refer to x in any predicate, which is what gives the arrow its dependency. The shorthand Type::base(B) constructs the unrefined base type as Refine("v", B, true), which is the identity element for the type-level lattice and what the pretty printer collapses to just B.

Predicates are the small logical fragment that Z3 understands.

#![allow(unused)]
fn main() {
use std::fmt;
#[derive(Debug, Clone, PartialEq)]
pub enum BaseTy {
    Int,
    Bool,
}
impl fmt::Display for BaseTy {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            BaseTy::Int => write!(f, "Int"),
            BaseTy::Bool => write!(f, "Bool"),
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Type {
    // { v : B | phi }
    Refine(String, BaseTy, Pred),
    // (x : T1) -> T2
    Fun(String, Box<Type>, Box<Type>),
}
impl Type {
    pub fn base(b: BaseTy) -> Type {
        Type::Refine("v".to_string(), b, Pred::Bool(true))
    }

    pub fn is_trivial(&self) -> bool {
        matches!(self, Type::Refine(_, _, Pred::Bool(true)))
    }
}
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum BinOp {
    Add,
    Sub,
    Mul,
    Eq,
    Ne,
    Lt,
    Le,
    Gt,
    Ge,
    And,
    Or,
    Implies,
}
impl BinOp {
    pub fn is_arith(self) -> bool {
        matches!(self, BinOp::Add | BinOp::Sub | BinOp::Mul)
    }

    pub fn is_cmp(self) -> bool {
        matches!(
            self,
            BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge
        )
    }

    pub fn is_bool(self) -> bool {
        matches!(self, BinOp::And | BinOp::Or | BinOp::Implies)
    }

    pub fn as_str(self) -> &'static str {
        match self {
            BinOp::Add => "+",
            BinOp::Sub => "-",
            BinOp::Mul => "*",
            BinOp::Eq => "=",
            BinOp::Ne => "!=",
            BinOp::Lt => "<",
            BinOp::Le => "<=",
            BinOp::Gt => ">",
            BinOp::Ge => ">=",
            BinOp::And => "&&",
            BinOp::Or => "||",
            BinOp::Implies => "==>",
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Expr {
    Int(i64),
    Bool(bool),
    Var(String),
    Let(String, Box<Expr>, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Lam(String, Type, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Ann(Box<Expr>, Type),
    Bin(BinOp, Box<Expr>, Box<Expr>),
    Not(Box<Expr>),
    Neg(Box<Expr>),
}
impl fmt::Display for Pred {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write_pred(f, self, 0)
    }
}
fn prec(op: BinOp) -> u8 {
    match op {
        BinOp::Or | BinOp::Implies => 1,
        BinOp::And => 2,
        BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge => 3,
        BinOp::Add | BinOp::Sub => 4,
        BinOp::Mul => 5,
    }
}
fn write_pred(f: &mut fmt::Formatter<'_>, p: &Pred, ctx: u8) -> fmt::Result {
    match p {
        Pred::Bool(b) => write!(f, "{}", b),
        Pred::Int(n) => write!(f, "{}", n),
        Pred::Var(x) => write!(f, "{}", x),
        Pred::Not(inner) => {
            write!(f, "!")?;
            write_pred(f, inner, 6)
        }
        Pred::Neg(inner) => {
            write!(f, "-")?;
            write_pred(f, inner, 6)
        }
        Pred::Bin(op, a, b) => {
            let p = prec(*op);
            let need = p < ctx;
            if need {
                write!(f, "(")?;
            }
            write_pred(f, a, p)?;
            write!(f, " {} ", op.as_str())?;
            write_pred(f, b, p + 1)?;
            if need {
                write!(f, ")")?;
            }
            Ok(())
        }
    }
}
impl fmt::Display for Type {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Type::Refine(v, b, Pred::Bool(true)) => {
                let _ = v;
                write!(f, "{}", b)
            }
            Type::Refine(v, b, p) => write!(f, "{{ {} : {} | {} }}", v, b, p),
            Type::Fun(x, t1, t2) => {
                let dep = mentions(t2, x);
                let left = match t1.as_ref() {
                    Type::Fun(_, _, _) => format!("({})", t1),
                    _ => format!("{}", t1),
                };
                if dep {
                    write!(f, "({} : {}) -> {}", x, left, t2)
                } else {
                    write!(f, "{} -> {}", left, t2)
                }
            }
        }
    }
}
pub fn mentions(t: &Type, x: &str) -> bool {
    match t {
        Type::Refine(v, _, p) => v != x && pred_mentions(p, x),
        Type::Fun(y, t1, t2) => mentions(t1, x) || (y != x && mentions(t2, x)),
    }
}
pub fn pred_mentions(p: &Pred, x: &str) -> bool {
    match p {
        Pred::Var(y) => y == x,
        Pred::Bin(_, a, b) => pred_mentions(a, x) || pred_mentions(b, x),
        Pred::Not(a) | Pred::Neg(a) => pred_mentions(a, x),
        _ => false,
    }
}
impl fmt::Display for Expr {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write_expr(f, self, 0)
    }
}
fn expr_prec(e: &Expr) -> u8 {
    match e {
        Expr::Let(_, _, _) | Expr::If(_, _, _) | Expr::Lam(_, _, _) | Expr::Ann(_, _) => 0,
        Expr::Bin(op, _, _) => prec(*op),
        Expr::App(_, _) | Expr::Not(_) | Expr::Neg(_) => 7,
        _ => 8,
    }
}
fn write_expr(f: &mut fmt::Formatter<'_>, e: &Expr, ctx: u8) -> fmt::Result {
    let p = expr_prec(e);
    let need = p < ctx;
    if need {
        write!(f, "(")?;
    }
    match e {
        Expr::Int(n) => write!(f, "{}", n)?,
        Expr::Bool(b) => write!(f, "{}", b)?,
        Expr::Var(x) => write!(f, "{}", x)?,
        Expr::Let(x, v, body) => write!(f, "let {} = {} in {}", x, v, body)?,
        Expr::If(c, a, b) => write!(f, "if {} then {} else {}", c, a, b)?,
        Expr::Lam(x, t, body) => write!(f, "\\{} : {} -> {}", x, t, body)?,
        Expr::App(g, a) => {
            write_expr(f, g, 7)?;
            write!(f, " ")?;
            write_expr(f, a, 8)?;
        }
        Expr::Ann(e, t) => write!(f, "({} : {})", e, t)?,
        Expr::Bin(op, a, b) => {
            write_expr(f, a, p)?;
            write!(f, " {} ", op.as_str())?;
            write_expr(f, b, p + 1)?;
        }
        Expr::Not(a) => {
            write!(f, "!")?;
            write_expr(f, a, 7)?;
        }
        Expr::Neg(a) => {
            write!(f, "-")?;
            write_expr(f, a, 7)?;
        }
    }
    if need {
        write!(f, ")")?;
    }
    Ok(())
}
#[derive(Debug, Clone, PartialEq)]
pub enum Pred {
    Bool(bool),
    Int(i64),
    Var(String),
    Bin(BinOp, Box<Pred>, Box<Pred>),
    Not(Box<Pred>),
    Neg(Box<Pred>),
}
}

The Bool(b) and Int(n) constructors wrap boolean and integer literals. The Var(x) constructor wraps a logical variable name bound somewhere up the environment chain. The Bin(op, a, b) constructor pairs a binary operator with two operand predicates and covers arithmetic, comparison, and boolean operators. The Not(p) constructor is logical negation, used both directly in user-written predicates and to encode the false branch of a reflected conditional. The Neg(p) constructor is arithmetic negation, distinct from Not because it operates at the integer sort rather than the boolean sort. The full operator set lives in BinOp, with helpers that classify each operator by its expected argument and result sorts.

#![allow(unused)]
fn main() {
use std::fmt;
#[derive(Debug, Clone, PartialEq)]
pub enum BaseTy {
    Int,
    Bool,
}
impl fmt::Display for BaseTy {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            BaseTy::Int => write!(f, "Int"),
            BaseTy::Bool => write!(f, "Bool"),
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Type {
    // { v : B | phi }
    Refine(String, BaseTy, Pred),
    // (x : T1) -> T2
    Fun(String, Box<Type>, Box<Type>),
}
impl Type {
    pub fn base(b: BaseTy) -> Type {
        Type::Refine("v".to_string(), b, Pred::Bool(true))
    }

    pub fn is_trivial(&self) -> bool {
        matches!(self, Type::Refine(_, _, Pred::Bool(true)))
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Pred {
    Bool(bool),
    Int(i64),
    Var(String),
    Bin(BinOp, Box<Pred>, Box<Pred>),
    Not(Box<Pred>),
    Neg(Box<Pred>),
}
impl BinOp {
    pub fn is_arith(self) -> bool {
        matches!(self, BinOp::Add | BinOp::Sub | BinOp::Mul)
    }

    pub fn is_cmp(self) -> bool {
        matches!(
            self,
            BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge
        )
    }

    pub fn is_bool(self) -> bool {
        matches!(self, BinOp::And | BinOp::Or | BinOp::Implies)
    }

    pub fn as_str(self) -> &'static str {
        match self {
            BinOp::Add => "+",
            BinOp::Sub => "-",
            BinOp::Mul => "*",
            BinOp::Eq => "=",
            BinOp::Ne => "!=",
            BinOp::Lt => "<",
            BinOp::Le => "<=",
            BinOp::Gt => ">",
            BinOp::Ge => ">=",
            BinOp::And => "&&",
            BinOp::Or => "||",
            BinOp::Implies => "==>",
        }
    }
}
#[derive(Debug, Clone, PartialEq)]
pub enum Expr {
    Int(i64),
    Bool(bool),
    Var(String),
    Let(String, Box<Expr>, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Lam(String, Type, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Ann(Box<Expr>, Type),
    Bin(BinOp, Box<Expr>, Box<Expr>),
    Not(Box<Expr>),
    Neg(Box<Expr>),
}
impl fmt::Display for Pred {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write_pred(f, self, 0)
    }
}
fn prec(op: BinOp) -> u8 {
    match op {
        BinOp::Or | BinOp::Implies => 1,
        BinOp::And => 2,
        BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge => 3,
        BinOp::Add | BinOp::Sub => 4,
        BinOp::Mul => 5,
    }
}
fn write_pred(f: &mut fmt::Formatter<'_>, p: &Pred, ctx: u8) -> fmt::Result {
    match p {
        Pred::Bool(b) => write!(f, "{}", b),
        Pred::Int(n) => write!(f, "{}", n),
        Pred::Var(x) => write!(f, "{}", x),
        Pred::Not(inner) => {
            write!(f, "!")?;
            write_pred(f, inner, 6)
        }
        Pred::Neg(inner) => {
            write!(f, "-")?;
            write_pred(f, inner, 6)
        }
        Pred::Bin(op, a, b) => {
            let p = prec(*op);
            let need = p < ctx;
            if need {
                write!(f, "(")?;
            }
            write_pred(f, a, p)?;
            write!(f, " {} ", op.as_str())?;
            write_pred(f, b, p + 1)?;
            if need {
                write!(f, ")")?;
            }
            Ok(())
        }
    }
}
impl fmt::Display for Type {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Type::Refine(v, b, Pred::Bool(true)) => {
                let _ = v;
                write!(f, "{}", b)
            }
            Type::Refine(v, b, p) => write!(f, "{{ {} : {} | {} }}", v, b, p),
            Type::Fun(x, t1, t2) => {
                let dep = mentions(t2, x);
                let left = match t1.as_ref() {
                    Type::Fun(_, _, _) => format!("({})", t1),
                    _ => format!("{}", t1),
                };
                if dep {
                    write!(f, "({} : {}) -> {}", x, left, t2)
                } else {
                    write!(f, "{} -> {}", left, t2)
                }
            }
        }
    }
}
pub fn mentions(t: &Type, x: &str) -> bool {
    match t {
        Type::Refine(v, _, p) => v != x && pred_mentions(p, x),
        Type::Fun(y, t1, t2) => mentions(t1, x) || (y != x && mentions(t2, x)),
    }
}
pub fn pred_mentions(p: &Pred, x: &str) -> bool {
    match p {
        Pred::Var(y) => y == x,
        Pred::Bin(_, a, b) => pred_mentions(a, x) || pred_mentions(b, x),
        Pred::Not(a) | Pred::Neg(a) => pred_mentions(a, x),
        _ => false,
    }
}
impl fmt::Display for Expr {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write_expr(f, self, 0)
    }
}
fn expr_prec(e: &Expr) -> u8 {
    match e {
        Expr::Let(_, _, _) | Expr::If(_, _, _) | Expr::Lam(_, _, _) | Expr::Ann(_, _) => 0,
        Expr::Bin(op, _, _) => prec(*op),
        Expr::App(_, _) | Expr::Not(_) | Expr::Neg(_) => 7,
        _ => 8,
    }
}
fn write_expr(f: &mut fmt::Formatter<'_>, e: &Expr, ctx: u8) -> fmt::Result {
    let p = expr_prec(e);
    let need = p < ctx;
    if need {
        write!(f, "(")?;
    }
    match e {
        Expr::Int(n) => write!(f, "{}", n)?,
        Expr::Bool(b) => write!(f, "{}", b)?,
        Expr::Var(x) => write!(f, "{}", x)?,
        Expr::Let(x, v, body) => write!(f, "let {} = {} in {}", x, v, body)?,
        Expr::If(c, a, b) => write!(f, "if {} then {} else {}", c, a, b)?,
        Expr::Lam(x, t, body) => write!(f, "\\{} : {} -> {}", x, t, body)?,
        Expr::App(g, a) => {
            write_expr(f, g, 7)?;
            write!(f, " ")?;
            write_expr(f, a, 8)?;
        }
        Expr::Ann(e, t) => write!(f, "({} : {})", e, t)?,
        Expr::Bin(op, a, b) => {
            write_expr(f, a, p)?;
            write!(f, " {} ", op.as_str())?;
            write_expr(f, b, p + 1)?;
        }
        Expr::Not(a) => {
            write!(f, "!")?;
            write_expr(f, a, 7)?;
        }
        Expr::Neg(a) => {
            write!(f, "-")?;
            write_expr(f, a, 7)?;
        }
    }
    if need {
        write!(f, ")")?;
    }
    Ok(())
}
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum BinOp {
    Add,
    Sub,
    Mul,
    Eq,
    Ne,
    Lt,
    Le,
    Gt,
    Ge,
    And,
    Or,
    Implies,
}
}

The arithmetic constructors Add, Sub, and Mul take two integer operands and produce an integer. The comparison constructors Eq, Ne, Lt, Le, Gt, and Ge take two integer operands and produce a boolean. The boolean constructors And, Or, and Implies take two boolean operands and produce a boolean. The split between arithmetic, comparison, and boolean operators is what synth_bin uses to pick the right argument and result types when checking a binary expression, with the is_arith, is_cmp, and is_bool predicate methods classifying each operator into its sort.

Synthesis and Checking

Type-checking is bidirectional. The synthesiser takes an expression and produces its most precise type. The checker takes an expression and a target type and produces a unit success or a refinement-failure error.

#![allow(unused)]
fn main() {
pub fn synth(&mut self, env: &Env, path: &Pred, e: &Expr) -> Result<Type> {
    match e {
        Expr::Int(n) => Ok(singleton_int(*n)),
        Expr::Bool(b) => Ok(singleton_bool(*b)),
        Expr::Var(x) => {
            if let Some(t) = env.lookup(x) {
                Ok(self_refine(x, t))
            } else if let Some(t) = self.prims.get(x) {
                Ok(t.clone())
            } else {
                Err(InferenceError::UnboundVariable { name: x.clone() })
            }
        }
        Expr::Ann(inner, t) => {
            self.check(env, path, inner, t)?;
            Ok(t.clone())
        }
        Expr::App(f, a) => {
            let ft = self.synth(env, path, f)?;
            let (x, t1, t2) = match ft {
                Type::Fun(x, t1, t2) => (x, *t1, *t2),
                other => return Err(InferenceError::NotAFunction { found: other }),
            };
            self.check(env, path, a, &t1)?;
            if let Some(arg_pred) = reflect(env, a) {
                Ok(subst_ty(&t2, &x, &arg_pred))
            } else {
                Ok(t2)
            }
        }
        Expr::Lam(x, t1, body) => {
            let body_env = env.extend(x.clone(), t1.clone());
            let t2 = self.synth(&body_env, path, body)?;
            Ok(Type::Fun(x.clone(), Box::new(t1.clone()), Box::new(t2)))
        }
        Expr::Let(x, v, body) => {
            let tv = self.synth(env, path, v)?;
            let new_env = env.extend(x.clone(), tv.clone());
            let new_path = if let (Type::Refine(_, _, _), Some(vp)) = (&tv, reflect(env, v)) {
                and_pred(
                    path.clone(),
                    Pred::Bin(BinOp::Eq, Box::new(Pred::Var(x.clone())), Box::new(vp)),
                )
            } else {
                path.clone()
            };
            self.synth(&new_env, &new_path, body)
        }
        Expr::If(c, a, b) => {
            self.check(env, path, c, &Type::base(BaseTy::Bool))?;
            let cp = reflect(env, c).unwrap_or(Pred::Bool(true));
            let path_a = and_pred(path.clone(), cp.clone());
            let path_b = and_pred(path.clone(), Pred::Not(Box::new(cp)));
            let ta = self.synth(env, &path_a, a)?;
            let tb = self.synth(env, &path_b, b)?;
            // Return whichever is the more general base type; require both are base.
            match (&ta, &tb) {
                (Type::Refine(_, ba, _), Type::Refine(_, bb, _)) if ba == bb => {
                    Ok(Type::base(ba.clone()))
                }
                _ => Err(InferenceError::Mismatch {
                    expected: ta,
                    found: tb,
                }),
            }
        }
        Expr::Bin(op, a, b) => self.synth_bin(env, path, *op, a, b),
        Expr::Not(a) => {
            self.check(env, path, a, &Type::base(BaseTy::Bool))?;
            if let Some(ap) = reflect(env, a) {
                let v = "v".to_string();
                Ok(Type::Refine(
                    v.clone(),
                    BaseTy::Bool,
                    Pred::Bin(
                        BinOp::Eq,
                        Box::new(Pred::Var(v)),
                        Box::new(Pred::Not(Box::new(ap))),
                    ),
                ))
            } else {
                Ok(Type::base(BaseTy::Bool))
            }
        }
        Expr::Neg(a) => {
            self.check(env, path, a, &Type::base(BaseTy::Int))?;
            if let Some(ap) = reflect(env, a) {
                let v = "v".to_string();
                Ok(Type::Refine(
                    v.clone(),
                    BaseTy::Int,
                    Pred::Bin(
                        BinOp::Eq,
                        Box::new(Pred::Var(v)),
                        Box::new(Pred::Neg(Box::new(ap))),
                    ),
                ))
            } else {
                Ok(Type::base(BaseTy::Int))
            }
        }
    }
}
}

The synthesiser produces singleton types for literals: the literal 5 synthesises { v : Int | v = 5 } rather than the unrefined Int, and true synthesises { v : Bool | v = true }. Carrying the literal forward in the type is what lets 1 + 2 synthesise { v : Int | v = 1 + 2 }, which is the most precise predicate available without evaluating the expression.

The variable case calls self_refine to sharpen the looked-up type with the equation v = x, so a let-bound variable x : { n : Int | n >= 0 } accessed at a use site has the synthesised type { v : Int | v >= 0 && v = x }. The extra conjunct is what lets the result of a chained computation be expressed in terms of the bound names rather than as a sequence of fresh v variables.

Application is where dependent types pay off. The function type is (x : t1) -> t2, the argument is checked against t1, and the result type substitutes the argument for x in t2. The substitution is by subst_ty, which walks the type and replaces every free x in any predicate with the argument expression reflected into the predicate language.

The checker reverses the flow. It takes an expected type and propagates structure inward, switching to synthesis only when no structural rule applies.

#![allow(unused)]
fn main() {
pub fn check(&mut self, env: &Env, path: &Pred, e: &Expr, t: &Type) -> Result<()> {
    match (e, t) {
        (Expr::Lam(x, t1, body), Type::Fun(y, s1, s2)) => {
            self.subtype(env, path, s1, t1)?;
            let body_env = env.extend(x.clone(), t1.clone());
            let s2n = subst_ty(s2, y, &Pred::Var(x.clone()));
            self.check(&body_env, path, body, &s2n)
        }
        (Expr::Let(x, v, body), _) => {
            let tv = self.synth(env, path, v)?;
            let new_env = env.extend(x.clone(), tv.clone());
            let new_path = if let (Type::Refine(_, _, _), Some(vp)) = (&tv, reflect(env, v)) {
                and_pred(
                    path.clone(),
                    Pred::Bin(BinOp::Eq, Box::new(Pred::Var(x.clone())), Box::new(vp)),
                )
            } else {
                path.clone()
            };
            self.check(&new_env, &new_path, body, t)
        }
        (Expr::If(c, a, b), _) => {
            self.check(env, path, c, &Type::base(BaseTy::Bool))?;
            let cp = reflect(env, c).unwrap_or(Pred::Bool(true));
            let path_a = and_pred(path.clone(), cp.clone());
            let path_b = and_pred(path.clone(), Pred::Not(Box::new(cp)));
            self.check(env, &path_a, a, t)?;
            self.check(env, &path_b, b, t)
        }
        _ => {
            let t_syn = self.synth(env, path, e)?;
            self.subtype(env, path, &t_syn, t)
        }
    }
}
}

The lambda case unifies argument types by subtyping, extends the environment with the bound parameter at the source-level type, renames the result type’s bound variable to the lambda’s parameter name, and recurses. The if case checks the condition at Bool, then refines the path condition with the reflected condition in the true branch and its negation in the false branch, and checks both branches at the same expected type. The let case synthesises the bound value, extends the environment, and refines the path condition with the equation x = v when the bound value is reflectable.

Reflection

The reflection function is what makes the bridge between expressions and predicates. Many source expressions are pure enough to be lifted into the predicate language verbatim, and that lifting is what lets the type system carry argument expressions through dependent applications.

#![allow(unused)]
fn main() {
use std::collections::HashMap;
use crate::ast::{BaseTy, BinOp, Expr, Pred, Type};
use crate::errors::{InferenceError, Result};
use crate::smt::{check_valid, Sort, Validity};
#[derive(Debug, Clone, Default)]
pub struct Env {
    bindings: Vec<(String, Type)>,
}
impl Env {
    pub fn new() -> Self {
        Self::default()
    }

    fn extend(&self, x: String, t: Type) -> Self {
        let mut e = self.clone();
        e.bindings.push((x, t));
        e
    }

    fn lookup(&self, x: &str) -> Option<&Type> {
        self.bindings
            .iter()
            .rev()
            .find(|(n, _)| n == x)
            .map(|(_, t)| t)
    }

    fn smt_bindings(&self) -> Vec<(String, Sort, Pred)> {
        let mut out = Vec::new();
        for (name, t) in &self.bindings {
            if let Type::Refine(v, b, p) = t {
                let sort = match b {
                    BaseTy::Int => Sort::Int,
                    BaseTy::Bool => Sort::Bool,
                };
                let renamed = subst_pred(p, v, &Pred::Var(name.clone()));
                out.push((name.clone(), sort, renamed));
            }
        }
        out
    }
}
pub fn subst_pred(p: &Pred, x: &str, with: &Pred) -> Pred {
    match p {
        Pred::Var(y) if y == x => with.clone(),
        Pred::Var(_) | Pred::Bool(_) | Pred::Int(_) => p.clone(),
        Pred::Not(a) => Pred::Not(Box::new(subst_pred(a, x, with))),
        Pred::Neg(a) => Pred::Neg(Box::new(subst_pred(a, x, with))),
        Pred::Bin(op, a, b) => Pred::Bin(
            *op,
            Box::new(subst_pred(a, x, with)),
            Box::new(subst_pred(b, x, with)),
        ),
    }
}
fn subst_ty(t: &Type, x: &str, with: &Pred) -> Type {
    match t {
        Type::Refine(v, b, p) => {
            if v == x {
                t.clone()
            } else {
                Type::Refine(v.clone(), b.clone(), subst_pred(p, x, with))
            }
        }
        Type::Fun(y, t1, t2) => {
            let t1n = subst_ty(t1, x, with);
            let t2n = if y == x {
                (**t2).clone()
            } else {
                subst_ty(t2, x, with)
            };
            Type::Fun(y.clone(), Box::new(t1n), Box::new(t2n))
        }
    }
}
fn and_pred(a: Pred, b: Pred) -> Pred {
    match (a, b) {
        (Pred::Bool(true), p) | (p, Pred::Bool(true)) => p,
        (a, b) => Pred::Bin(BinOp::And, Box::new(a), Box::new(b)),
    }
}
pub struct Checker {
    fresh: usize,
    prims: HashMap<String, Type>,
}
impl Default for Checker {
    fn default() -> Self {
        Self::new()
    }
}
impl Checker {
    pub fn new() -> Self {
        let mut prims = HashMap::new();
        // div : (x : Int) -> { y : Int | y != 0 } -> Int
        let nonzero = Type::Refine(
            "y".into(),
            BaseTy::Int,
            Pred::Bin(
                BinOp::Ne,
                Box::new(Pred::Var("y".into())),
                Box::new(Pred::Int(0)),
            ),
        );
        let div_ty = Type::Fun(
            "_x".into(),
            Box::new(Type::base(BaseTy::Int)),
            Box::new(Type::Fun(
                "_y".into(),
                Box::new(nonzero.clone()),
                Box::new(Type::base(BaseTy::Int)),
            )),
        );
        prims.insert("div".to_string(), div_ty);
        let mod_ty = Type::Fun(
            "_x".into(),
            Box::new(Type::base(BaseTy::Int)),
            Box::new(Type::Fun(
                "_y".into(),
                Box::new(nonzero),
                Box::new(Type::base(BaseTy::Int)),
            )),
        );
        prims.insert("mod".to_string(), mod_ty);
        Self { fresh: 0, prims }
    }

    fn gensym(&mut self, base: &str) -> String {
        let n = self.fresh;
        self.fresh += 1;
        format!("{}_{}", base, n)
    }

    pub fn synth(&mut self, env: &Env, path: &Pred, e: &Expr) -> Result<Type> {
        match e {
            Expr::Int(n) => Ok(singleton_int(*n)),
            Expr::Bool(b) => Ok(singleton_bool(*b)),
            Expr::Var(x) => {
                if let Some(t) = env.lookup(x) {
                    Ok(self_refine(x, t))
                } else if let Some(t) = self.prims.get(x) {
                    Ok(t.clone())
                } else {
                    Err(InferenceError::UnboundVariable { name: x.clone() })
                }
            }
            Expr::Ann(inner, t) => {
                self.check(env, path, inner, t)?;
                Ok(t.clone())
            }
            Expr::App(f, a) => {
                let ft = self.synth(env, path, f)?;
                let (x, t1, t2) = match ft {
                    Type::Fun(x, t1, t2) => (x, *t1, *t2),
                    other => return Err(InferenceError::NotAFunction { found: other }),
                };
                self.check(env, path, a, &t1)?;
                if let Some(arg_pred) = reflect(env, a) {
                    Ok(subst_ty(&t2, &x, &arg_pred))
                } else {
                    Ok(t2)
                }
            }
            Expr::Lam(x, t1, body) => {
                let body_env = env.extend(x.clone(), t1.clone());
                let t2 = self.synth(&body_env, path, body)?;
                Ok(Type::Fun(x.clone(), Box::new(t1.clone()), Box::new(t2)))
            }
            Expr::Let(x, v, body) => {
                let tv = self.synth(env, path, v)?;
                let new_env = env.extend(x.clone(), tv.clone());
                let new_path = if let (Type::Refine(_, _, _), Some(vp)) = (&tv, reflect(env, v)) {
                    and_pred(
                        path.clone(),
                        Pred::Bin(BinOp::Eq, Box::new(Pred::Var(x.clone())), Box::new(vp)),
                    )
                } else {
                    path.clone()
                };
                self.synth(&new_env, &new_path, body)
            }
            Expr::If(c, a, b) => {
                self.check(env, path, c, &Type::base(BaseTy::Bool))?;
                let cp = reflect(env, c).unwrap_or(Pred::Bool(true));
                let path_a = and_pred(path.clone(), cp.clone());
                let path_b = and_pred(path.clone(), Pred::Not(Box::new(cp)));
                let ta = self.synth(env, &path_a, a)?;
                let tb = self.synth(env, &path_b, b)?;
                // Return whichever is the more general base type; require both are base.
                match (&ta, &tb) {
                    (Type::Refine(_, ba, _), Type::Refine(_, bb, _)) if ba == bb => {
                        Ok(Type::base(ba.clone()))
                    }
                    _ => Err(InferenceError::Mismatch {
                        expected: ta,
                        found: tb,
                    }),
                }
            }
            Expr::Bin(op, a, b) => self.synth_bin(env, path, *op, a, b),
            Expr::Not(a) => {
                self.check(env, path, a, &Type::base(BaseTy::Bool))?;
                if let Some(ap) = reflect(env, a) {
                    let v = "v".to_string();
                    Ok(Type::Refine(
                        v.clone(),
                        BaseTy::Bool,
                        Pred::Bin(
                            BinOp::Eq,
                            Box::new(Pred::Var(v)),
                            Box::new(Pred::Not(Box::new(ap))),
                        ),
                    ))
                } else {
                    Ok(Type::base(BaseTy::Bool))
                }
            }
            Expr::Neg(a) => {
                self.check(env, path, a, &Type::base(BaseTy::Int))?;
                if let Some(ap) = reflect(env, a) {
                    let v = "v".to_string();
                    Ok(Type::Refine(
                        v.clone(),
                        BaseTy::Int,
                        Pred::Bin(
                            BinOp::Eq,
                            Box::new(Pred::Var(v)),
                            Box::new(Pred::Neg(Box::new(ap))),
                        ),
                    ))
                } else {
                    Ok(Type::base(BaseTy::Int))
                }
            }
        }
    }

    fn synth_bin(&mut self, env: &Env, path: &Pred, op: BinOp, a: &Expr, b: &Expr) -> Result<Type> {
        let (arg_b, res_b) = if op.is_arith() {
            (BaseTy::Int, BaseTy::Int)
        } else if op.is_cmp() {
            (BaseTy::Int, BaseTy::Bool)
        } else {
            (BaseTy::Bool, BaseTy::Bool)
        };
        self.check(env, path, a, &Type::base(arg_b.clone()))?;
        self.check(env, path, b, &Type::base(arg_b))?;
        let v = "v".to_string();
        if let (Some(ap), Some(bp)) = (reflect(env, a), reflect(env, b)) {
            let rhs = Pred::Bin(op, Box::new(ap), Box::new(bp));
            Ok(Type::Refine(
                v.clone(),
                res_b,
                Pred::Bin(BinOp::Eq, Box::new(Pred::Var(v)), Box::new(rhs)),
            ))
        } else {
            Ok(Type::base(res_b))
        }
    }

    pub fn check(&mut self, env: &Env, path: &Pred, e: &Expr, t: &Type) -> Result<()> {
        match (e, t) {
            (Expr::Lam(x, t1, body), Type::Fun(y, s1, s2)) => {
                self.subtype(env, path, s1, t1)?;
                let body_env = env.extend(x.clone(), t1.clone());
                let s2n = subst_ty(s2, y, &Pred::Var(x.clone()));
                self.check(&body_env, path, body, &s2n)
            }
            (Expr::Let(x, v, body), _) => {
                let tv = self.synth(env, path, v)?;
                let new_env = env.extend(x.clone(), tv.clone());
                let new_path = if let (Type::Refine(_, _, _), Some(vp)) = (&tv, reflect(env, v)) {
                    and_pred(
                        path.clone(),
                        Pred::Bin(BinOp::Eq, Box::new(Pred::Var(x.clone())), Box::new(vp)),
                    )
                } else {
                    path.clone()
                };
                self.check(&new_env, &new_path, body, t)
            }
            (Expr::If(c, a, b), _) => {
                self.check(env, path, c, &Type::base(BaseTy::Bool))?;
                let cp = reflect(env, c).unwrap_or(Pred::Bool(true));
                let path_a = and_pred(path.clone(), cp.clone());
                let path_b = and_pred(path.clone(), Pred::Not(Box::new(cp)));
                self.check(env, &path_a, a, t)?;
                self.check(env, &path_b, b, t)
            }
            _ => {
                let t_syn = self.synth(env, path, e)?;
                self.subtype(env, path, &t_syn, t)
            }
        }
    }

    pub fn subtype(&mut self, env: &Env, path: &Pred, sub: &Type, sup: &Type) -> Result<()> {
        match (sub, sup) {
            (Type::Refine(v1, b1, p1), Type::Refine(v2, b2, p2)) => {
                if b1 != b2 {
                    return Err(InferenceError::Mismatch {
                        expected: sup.clone(),
                        found: sub.clone(),
                    });
                }
                let nm = self.gensym("v");
                let p1r = subst_pred(p1, v1, &Pred::Var(nm.clone()));
                let p2r = subst_pred(p2, v2, &Pred::Var(nm.clone()));
                let sort = match b1 {
                    BaseTy::Int => Sort::Int,
                    BaseTy::Bool => Sort::Bool,
                };
                let mut binds = env.smt_bindings();
                binds.push((nm.clone(), sort, p1r.clone()));
                let obligation = format!("{} => {}", show_pred(&p1r), show_pred(&p2r));
                match check_valid(&binds, path, &p2r)? {
                    Validity::Valid => Ok(()),
                    Validity::Invalid { model } => {
                        Err(InferenceError::RefinementFailed { obligation, model })
                    }
                    Validity::Unknown => Err(InferenceError::RefinementFailed {
                        obligation: format!("{} (z3 returned unknown)", obligation),
                        model: None,
                    }),
                }
            }
            (Type::Fun(x1, a1, r1), Type::Fun(x2, a2, r2)) => {
                self.subtype(env, path, a2, a1)?;
                let body_env = env.extend(x2.clone(), (**a2).clone());
                let r1n = subst_ty(r1, x1, &Pred::Var(x2.clone()));
                self.subtype(&body_env, path, &r1n, r2)
            }
            _ => Err(InferenceError::Mismatch {
                expected: sup.clone(),
                found: sub.clone(),
            }),
        }
    }
}
fn singleton_int(n: i64) -> Type {
    let v = "v".to_string();
    Type::Refine(
        v.clone(),
        BaseTy::Int,
        Pred::Bin(BinOp::Eq, Box::new(Pred::Var(v)), Box::new(Pred::Int(n))),
    )
}
fn singleton_bool(b: bool) -> Type {
    let v = "v".to_string();
    Type::Refine(
        v.clone(),
        BaseTy::Bool,
        Pred::Bin(BinOp::Eq, Box::new(Pred::Var(v)), Box::new(Pred::Bool(b))),
    )
}
fn self_refine(name: &str, t: &Type) -> Type {
    match t {
        Type::Refine(v, b, p) => {
            let nm = "v".to_string();
            let p_renamed = subst_pred(p, v, &Pred::Var(nm.clone()));
            let eq = Pred::Bin(
                BinOp::Eq,
                Box::new(Pred::Var(nm.clone())),
                Box::new(Pred::Var(name.to_string())),
            );
            let combined = and_pred(p_renamed, eq);
            Type::Refine(nm, b.clone(), combined)
        }
        _ => t.clone(),
    }
}
fn show_pred(p: &Pred) -> String {
    format!("{}", p)
}
pub fn infer_type(e: &Expr) -> Result<Type> {
    let mut c = Checker::new();
    let env = Env::new();
    c.synth(&env, &Pred::Bool(true), e)
}
pub fn reflect(env: &Env, e: &Expr) -> Option<Pred> {
    match e {
        Expr::Int(n) => Some(Pred::Int(*n)),
        Expr::Bool(b) => Some(Pred::Bool(*b)),
        Expr::Var(x) => match env.lookup(x)? {
            Type::Refine(_, _, _) => Some(Pred::Var(x.clone())),
            _ => None,
        },
        Expr::Neg(a) => Some(Pred::Neg(Box::new(reflect(env, a)?))),
        Expr::Not(a) => Some(Pred::Not(Box::new(reflect(env, a)?))),
        Expr::Bin(op, a, b) => {
            let ap = reflect(env, a)?;
            let bp = reflect(env, b)?;
            Some(Pred::Bin(*op, Box::new(ap), Box::new(bp)))
        }
        Expr::If(c, t, f) => {
            // if c then t else f  ===  (c && t) || (!c && f)  when reflected
            let cp = reflect(env, c)?;
            let tp = reflect(env, t)?;
            let fp = reflect(env, f)?;
            let left = Pred::Bin(BinOp::And, Box::new(cp.clone()), Box::new(tp));
            let right = Pred::Bin(BinOp::And, Box::new(Pred::Not(Box::new(cp))), Box::new(fp));
            Some(Pred::Bin(BinOp::Or, Box::new(left), Box::new(right)))
        }
        _ => None,
    }
}
}

Literals reflect to literal predicates. Variables reflect to predicate variables when their type is a refinement. Arithmetic and boolean operations reflect compositionally. The if expression reflects to a disjunction of two conjunctions, which is the standard encoding of if c then t else f in pure logic. Lambdas, applications of non-primitive functions, and let bindings do not reflect, so the result type after applying such an expression simply does not refine its result variable in terms of the argument.

Path Conditions

Path conditions are the running conjunction of facts that hold along the current control-flow path. When the checker enters the true branch of an if c then a else b, the path condition gains a conjunct for the reflected c. When it enters the false branch, it gains !c instead. Path conditions flow into Z3 as part of the SMT context when subtyping checks fire, so Z3 sees both the type of every variable in scope and the branch conditions along the way.

The path condition is what makes the absolute-value example check.

((\x : Int -> if x >= 0 then x else 0 - x) : Int -> { v : Int | v >= 0 })

The lambda is checked against the annotated type. The body is an if whose branches must each have type { v : Int | v >= 0 }. In the true branch the path is x >= 0, so subtyping { v : Int | v = x } <: { v : Int | v >= 0 } reduces to the Z3 query “does x >= 0 && v = x imply v >= 0”, which is valid. In the false branch the path is !(x >= 0), the synthesised type is { v : Int | v = 0 - x }, and the obligation !(x >= 0) && v = 0 - x ==> v >= 0 is valid. Without the path conditions Z3 would have no way to discriminate the two branches and the check would fail.

Subtyping and the SMT Backend

The whole machinery converges at the subtyping judgment. Subtyping a refinement against another refinement renames both predicates to a common fresh variable, asserts the subtype’s predicate, and asks Z3 to prove the supertype’s predicate.

#![allow(unused)]
fn main() {
pub fn subtype(&mut self, env: &Env, path: &Pred, sub: &Type, sup: &Type) -> Result<()> {
    match (sub, sup) {
        (Type::Refine(v1, b1, p1), Type::Refine(v2, b2, p2)) => {
            if b1 != b2 {
                return Err(InferenceError::Mismatch {
                    expected: sup.clone(),
                    found: sub.clone(),
                });
            }
            let nm = self.gensym("v");
            let p1r = subst_pred(p1, v1, &Pred::Var(nm.clone()));
            let p2r = subst_pred(p2, v2, &Pred::Var(nm.clone()));
            let sort = match b1 {
                BaseTy::Int => Sort::Int,
                BaseTy::Bool => Sort::Bool,
            };
            let mut binds = env.smt_bindings();
            binds.push((nm.clone(), sort, p1r.clone()));
            let obligation = format!("{} => {}", show_pred(&p1r), show_pred(&p2r));
            match check_valid(&binds, path, &p2r)? {
                Validity::Valid => Ok(()),
                Validity::Invalid { model } => {
                    Err(InferenceError::RefinementFailed { obligation, model })
                }
                Validity::Unknown => Err(InferenceError::RefinementFailed {
                    obligation: format!("{} (z3 returned unknown)", obligation),
                    model: None,
                }),
            }
        }
        (Type::Fun(x1, a1, r1), Type::Fun(x2, a2, r2)) => {
            self.subtype(env, path, a2, a1)?;
            let body_env = env.extend(x2.clone(), (**a2).clone());
            let r1n = subst_ty(r1, x1, &Pred::Var(x2.clone()));
            self.subtype(&body_env, path, &r1n, r2)
        }
        _ => Err(InferenceError::Mismatch {
            expected: sup.clone(),
            found: sub.clone(),
        }),
    }
}
}

The function-type case is the usual contravariant rule: argument types subtype contravariantly, result types covariantly, with the result type’s bound variable renamed to align with the supertype’s binder. The refinement case is the one that emits SMT obligations. Both predicates are renamed to a fresh v, the environment is converted to a list of SMT bindings with their stored refinements as assumptions, the fresh-variable assumption is added, and Z3 is asked whether the goal predicate follows from the conjunction of all the assumptions and the path.

#![allow(unused)]
fn main() {
use std::collections::HashMap;
use z3::ast::{Bool, Int};
use z3::{SatResult, Solver};
use crate::ast::{BinOp, Pred};
use crate::errors::Result;
#[derive(Debug, Clone)]
pub enum Sort {
    Int,
    Bool,
}
#[derive(Debug)]
pub enum Validity {
    Valid,
    Invalid { model: Option<String> },
    Unknown,
}
#[derive(Clone)]
enum Val {
    I(Int),
    B(Bool),
}
fn as_int(env: &HashMap<String, Val>, p: &Pred) -> Int {
    match translate(env, p) {
        Val::I(i) => i,
        Val::B(_) => panic!("expected integer predicate, found boolean"),
    }
}
fn as_bool(env: &HashMap<String, Val>, p: &Pred) -> Bool {
    match translate(env, p) {
        Val::B(b) => b,
        Val::I(_) => panic!("expected boolean predicate, found integer"),
    }
}
fn translate(env: &HashMap<String, Val>, p: &Pred) -> Val {
    match p {
        Pred::Bool(b) => Val::B(Bool::from_bool(*b)),
        Pred::Int(n) => Val::I(Int::from_i64(*n)),
        Pred::Var(x) => env
            .get(x)
            .cloned()
            .unwrap_or_else(|| panic!("unbound variable in predicate: {x}")),
        Pred::Not(a) => Val::B(as_bool(env, a).not()),
        Pred::Neg(a) => Val::I(as_int(env, a).unary_minus()),
        Pred::Bin(op, a, b) => translate_bin(env, *op, a, b),
    }
}
fn translate_bin(env: &HashMap<String, Val>, op: BinOp, a: &Pred, b: &Pred) -> Val {
    match op {
        BinOp::Add => Val::I(Int::add(&[as_int(env, a), as_int(env, b)])),
        BinOp::Sub => Val::I(Int::sub(&[as_int(env, a), as_int(env, b)])),
        BinOp::Mul => Val::I(Int::mul(&[as_int(env, a), as_int(env, b)])),
        BinOp::Lt => Val::B(as_int(env, a).lt(as_int(env, b))),
        BinOp::Le => Val::B(as_int(env, a).le(as_int(env, b))),
        BinOp::Gt => Val::B(as_int(env, a).gt(as_int(env, b))),
        BinOp::Ge => Val::B(as_int(env, a).ge(as_int(env, b))),
        BinOp::Eq => Val::B(eq_dispatch(env, a, b)),
        BinOp::Ne => Val::B(eq_dispatch(env, a, b).not()),
        BinOp::And => Val::B(Bool::and(&[as_bool(env, a), as_bool(env, b)])),
        BinOp::Or => Val::B(Bool::or(&[as_bool(env, a), as_bool(env, b)])),
        BinOp::Implies => Val::B(as_bool(env, a).implies(as_bool(env, b))),
    }
}
fn eq_dispatch(env: &HashMap<String, Val>, a: &Pred, b: &Pred) -> Bool {
    match (translate(env, a), translate(env, b)) {
        (Val::I(x), Val::I(y)) => x.eq(&y),
        (Val::B(x), Val::B(y)) => x.eq(&y),
        _ => panic!("equality between incompatible sorts"),
    }
}
fn render_model(
    model: &z3::Model,
    bindings: &[(String, Sort, Pred)],
    env: &HashMap<String, Val>,
) -> String {
    let mut entries: Vec<(String, String)> = Vec::new();
    for (name, _, _) in bindings {
        let rendered = match env.get(name) {
            Some(Val::I(i)) => model
                .eval(i, true)
                .and_then(|v| v.as_i64())
                .map(|n| n.to_string()),
            Some(Val::B(b)) => model
                .eval(b, true)
                .and_then(|v| v.as_bool())
                .map(|x| x.to_string()),
            None => None,
        };
        if let Some(v) = rendered {
            entries.push((name.clone(), v));
        }
    }
    entries.sort_by(|a, b| a.0.cmp(&b.0));
    entries
        .into_iter()
        .map(|(k, v)| format!("{k} = {v}"))
        .collect::<Vec<_>>()
        .join(", ")
}
pub fn check_valid(
    bindings: &[(String, Sort, Pred)],
    path: &Pred,
    goal: &Pred,
) -> Result<Validity> {
    let solver = Solver::new();

    let mut env: HashMap<String, Val> = HashMap::with_capacity(bindings.len());
    for (name, sort, _) in bindings {
        let v = match sort {
            Sort::Int => Val::I(Int::new_const(name.as_str())),
            Sort::Bool => Val::B(Bool::new_const(name.as_str())),
        };
        env.insert(name.clone(), v);
    }
    for (_, _, p) in bindings {
        solver.assert(as_bool(&env, p));
    }
    if !matches!(path, Pred::Bool(true)) {
        solver.assert(as_bool(&env, path));
    }
    solver.assert(as_bool(&env, goal).not());

    match solver.check() {
        SatResult::Unsat => Ok(Validity::Valid),
        SatResult::Unknown => Ok(Validity::Unknown),
        SatResult::Sat => {
            let model = solver.get_model().map(|m| render_model(&m, bindings, &env));
            Ok(Validity::Invalid { model })
        }
    }
}
}

The solver translates each predicate into Z3’s Bool or Int sort, asserts the bindings and the path, asserts the negation of the goal, and asks for unsat. An unsat answer means the implication is valid. A sat answer means there is a counterexample, which is what gets attached to the RefinementFailed error. An unknown answer is treated as failure, since the refinement system is only sound when its obligations are decidable. This is the only place the implementation depends on Z3, and the translation is small enough to be read in one sitting.