pub struct LeanEncoder<'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
def_id: MaybeExternId,
pretty_var_map: PrettyMap<LocalVar>,
sort_deps: SortDeps,
fun_deps: Vec<FunDef>,
kvar_solutions: KVarSolutions,
kvar_decls: Vec<KVarDecl>,
constraint: Constraint,
sort_files: FxHashMap<DataSort, LeanFile>,
fun_files: FxHashMap<FluxDefId, LeanFile>,
}Fields§
§genv: GlobalEnv<'genv, 'tcx>§def_id: MaybeExternId§pretty_var_map: PrettyMap<LocalVar>§sort_deps: SortDeps§fun_deps: Vec<FunDef>§kvar_solutions: KVarSolutions§kvar_decls: Vec<KVarDecl>§constraint: Constraint§sort_files: FxHashMap<DataSort, LeanFile>§fun_files: FxHashMap<FluxDefId, LeanFile>Implementations§
Source§impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx>
impl<'genv, 'tcx> LeanEncoder<'genv, 'tcx>
fn lean_cx(&self) -> LeanCtxt<'_, 'genv, 'tcx>
fn datasort_name(&self, sort: &DataSort) -> String
fn lean_file_for_fun(&self, fun: &FunDef) -> LeanFile
fn var_name(&self, var: &Var) -> String
fn import(&self, file: &LeanFile) -> String
fn new( genv: GlobalEnv<'genv, 'tcx>, def_id: MaybeExternId, pretty_var_map: PrettyMap<LocalVar>, sort_deps: SortDeps, fun_deps: Vec<FunDef>, kvar_solutions: KVarSolutions, kvar_decls: Vec<KVarDecl>, constraint: Constraint, ) -> Result<Self>
fn run(&self) -> Result<()>
fn fun_files(&self) -> FxHashMap<FluxDefId, LeanFile>
fn sort_files(&self) -> FxHashMap<DataSort, LeanFile>
fn generate_lake_project_if_not_present(&self) -> Result<()>
fn generate_opaque_sort_file_if_not_present( &self, sort: &SortDecl, ) -> Result<()>
fn data_decl_dependencies(&self, data_decl: &DataDecl) -> Vec<&LeanFile>
fn generate_struct_file_if_not_present( &self, data_decl: &DataDecl, ) -> Result<()>
fn sort_file(&self, sort: &DataSort) -> &LeanFile
fn fun_file(&self, did: &FluxDefId) -> &LeanFile
fn fun_def_dependencies( &self, did: FluxDefId, fun_def: &FunDef, ) -> Vec<&LeanFile>
fn generate_fun_def_file_if_not_present( &self, did: FluxDefId, fun_def: &FunDef, ) -> Result<()>
fn generate_lib_if_absent(&self) -> Result<()>
fn generate_vc_prelude(&self) -> Result<()>
fn generate_vc_imports(&self, file: &mut File) -> Result<()>
fn generate_vc_file(&self) -> Result<()>
fn generate_proof_if_absent(&self) -> Result<()>
fn record_proof(&self) -> Result<()>
pub fn encode( genv: GlobalEnv<'genv, 'tcx>, def_id: MaybeExternId, pretty_var_map: PrettyMap<LocalVar>, sort_deps: SortDeps, fun_deps: Vec<FunDef>, kvar_decls: Vec<KVarDecl>, constraint: Constraint, kvar_solutions: KVarSolutions, ) -> Result<()>
Auto Trait Implementations§
impl<'genv, 'tcx> Freeze for LeanEncoder<'genv, 'tcx>
impl<'genv, 'tcx> !RefUnwindSafe for LeanEncoder<'genv, 'tcx>
impl<'genv, 'tcx> !Send for LeanEncoder<'genv, 'tcx>
impl<'genv, 'tcx> !Sync for LeanEncoder<'genv, 'tcx>
impl<'genv, 'tcx> Unpin for LeanEncoder<'genv, 'tcx>
impl<'genv, 'tcx> !UnwindSafe for LeanEncoder<'genv, 'tcx>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more