Struct FixpointCtxt 

pub struct FixpointCtxt<'genv, 'tcx, T: Eq + Hash> {
    comments: Vec<String>,
    genv: GlobalEnv<'genv, 'tcx>,
    kvars: KVarGen,
    scx: SortEncodingCtxt,
    kcx: KVarEncodingCtxt,
    ecx: ExprEncodingCtxt<'genv, 'tcx>,
    tags: IndexVec<TagIdx, T>,
    tags_inv: UnordMap<T, TagIdx>,
}

Fields

comments: Vec<String>

genv: GlobalEnv<'genv, 'tcx>

kvars: KVarGen

scx: SortEncodingCtxt

kcx: KVarEncodingCtxt

ecx: ExprEncodingCtxt<'genv, 'tcx>

tags: IndexVec<TagIdx, T>

tags_inv: UnordMap<T, TagIdx>

Implementations

impl<'genv, 'tcx, Tag> FixpointCtxt<'genv, 'tcx, Tag>

where Tag: Hash + Eq + Copy,

fn fixpoint_to_sort_ctor( &self, ctor: &SortCtor, ) -> Result<SortCtor, FixpointParseError>

pub(crate) fn fixpoint_to_sort( &self, fsort: &Sort, ) -> Result<Sort, FixpointParseError>

pub(crate) fn fixpoint_to_expr( &self, fexpr: &Expr, ) -> Result<Expr, FixpointParseError>

fn fixpoint_app_to_expr( &self, fhead: &Expr, fargs: &[Expr], ) -> Result<Expr, FixpointParseError>

impl<'genv, 'tcx, Tag> FixpointCtxt<'genv, 'tcx, Tag>

where Tag: Hash + Eq + Copy,

pub fn new( genv: GlobalEnv<'genv, 'tcx>, def_id: MaybeExternId, kvars: KVarGen, ) -> Self

pub fn check( self, cache: &mut FixQueryCache, def_id: MaybeExternId, constraint: Constraint, kind: FixpointQueryKind, scrape_quals: bool, solver: SmtSolver, ) -> QueryResult<Answer<Tag>>

fn parse_kvar_solutions( &self, result: &FixpointResult<TagIdx>, ) -> QueryResult<Solution>

fn convert_solution(&self, expr: &str) -> QueryResult<Binder<Expr>>

fn convert_kvar_bind(&self, b: &KVarBind) -> QueryResult<(KVid, Binder<Expr>)>

pub fn generate_and_check_lean_lemmas( self, constraint: Constraint, ) -> QueryResult<()>

fn run_task_with_cache( genv: GlobalEnv<'_, '_>, task: Task, def_id: DefId, kind: FixpointQueryKind, cache: &mut FixQueryCache, ) -> FixpointResult<TagIdx>

fn tag_idx(&mut self, tag: Tag) -> TagIdx

where Tag: Debug,

pub(crate) fn with_name_map<R>( &mut self, name: Name, f: impl FnOnce(&mut Self, LocalVar) -> R, ) -> R

pub(crate) fn sort_to_fixpoint(&mut self, sort: &Sort) -> Sort

pub(crate) fn var_to_fixpoint(&self, var: &Var) -> Var

pub(crate) fn head_to_fixpoint( &mut self, expr: &Expr, mk_tag: impl Fn(Option<ESpan>) -> Tag + Copy, ) -> QueryResult<Constraint>

where Tag: Debug,

Encodes an expression in head position as a fixpoint::Constraint “peeling out” implications and foralls.

pub(crate) fn assumption_to_fixpoint( &mut self, pred: &Expr, ) -> QueryResult<(Vec<Bind>, Pred)>

Encodes an expression in assumptive position as a fixpoint::Pred. Returns the encoded predicate and a list of bindings produced by ANF-ing kvars.

fn assumption_to_fixpoint_aux( &mut self, expr: &Expr, bindings: &mut Vec<Bind>, preds: &mut Vec<Pred>, ) -> QueryResult

Auxiliary function to merge nested conjunctions in a single predicate

fn kvar_to_fixpoint( &mut self, kvar: &KVar, bindings: &mut Vec<Bind>, ) -> QueryResult<Pred>