Struct RefineTree

pub struct RefineTree {
    root: NodePtr,
}

A refinement tree tracks the “tree-like structure” of refinement variables and predicates generated during refinement type-checking. This tree can be encoded as a fixpoint constraint whose satisfiability implies the safety of a function.

We try to hide the representation of the tree as much as possible and only a couple of operations can be used to manipulate the structure of the tree explicitly. Instead, the tree is mostly constructed implicitly via a restricted api provided by Cursor. Some methods operate on nodes of the tree which we try to keep abstract, but it is important to remember that there’s an underlying tree.

The current implementation uses Rc and RefCell to represent the tree, but we ensure statically that the RefineTree is the single owner of the data and require a mutable reference to it for all mutations, i.e., we could in theory replace the RefCell with an UnsafeCell (or a GhostCell).

Fields

root: NodePtr

Implementations

impl RefineTree

pub(crate) fn new(params: Vec<(Var, Sort)>) -> RefineTree

pub(crate) fn simplify(&mut self, genv: GlobalEnv<'_, '_>)

pub(crate) fn into_fixpoint( self, cx: &mut FixpointCtxt<'_, '_, Tag>, ) -> QueryResult<Constraint>

pub(crate) fn cursor_at_root(&mut self) -> Cursor<'_>

pub(crate) fn replace_evars(&mut self, evars: &EVarStore) -> Result<(), EVid>

Trait Implementations

impl Debug for RefineTree

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

Formats the value using the given formatter.

impl Pretty for RefineTree

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

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_, '_>