Struct Env 

pub(crate) struct Env<'db> {
    pub log: LogHandle<'db>,
    universe: Universe,
    runtime: Runtime<'db>,
    pub scope: Arc<Scope<'db, 'db>>,
    variable_universes: Arc<Map<SymVariable<'db>, Universe>>,
    variable_tys: Arc<Map<SymVariable<'db>, VariableTypeCell<'db>>>,
    pub return_ty: Option<SymTy<'db>>,
    assumptions: Arc<Vec<Assumption<'db>>>,
}

Fields

log: LogHandle<'db>

universe: Universe

runtime: Runtime<'db>

Reference to the runtime

scope: Arc<Scope<'db, 'db>>

Lexical scope for name resolution

variable_universes: Arc<Map<SymVariable<'db>, Universe>>

Universe of each free generic variable that is in scope.

variable_tys: Arc<Map<SymVariable<'db>, VariableTypeCell<'db>>>

Type for in-scope variables. Local variables are stored directly in symbolic form but function parameters are stored initially as AST types. Those types are symbolified lazily. See VariableType for details.

return_ty: Option<SymTy<'db>>

If None, not type checking a function or method.

assumptions: Arc<Vec<Assumption<'db>>>

Assumptions declared

Implementations

impl<'db> Env<'db>

pub async fn require( &mut self, a: impl AsyncFnOnce(&mut Env<'db>) -> Errors<bool>, because: impl FnOnce(&mut Env<'db>) -> Because<'db>, or_else: &dyn OrElse<'db>, ) -> Errors<()>

pub fn require_for_all<T>( &mut self, items: impl IntoIterator<Item = T>, f: impl AsyncFn(&mut Env<'db>, T) -> Errors<()>, ) -> impl Future<Output = Errors<()>>

pub fn require_all(&mut self) -> RequireAll<'_, 'db>

pub fn require_both( &mut self, a: impl AsyncFnOnce(&mut Self) -> Errors<()>, b: impl AsyncFnOnce(&mut Self) -> Errors<()>, ) -> impl Future<Output = Errors<()>>

pub fn join<A, B>( &mut self, a: impl AsyncFnOnce(&mut Self) -> A, b: impl AsyncFnOnce(&mut Self) -> B, ) -> impl Future<Output = (A, B)>

where A: Serialize, B: Serialize,

pub fn either( &mut self, a: impl AsyncFnOnce(&mut Env<'db>) -> Errors<bool>, b: impl AsyncFnOnce(&mut Env<'db>) -> Errors<bool>, ) -> impl Future<Output = Errors<bool>>

pub fn for_all<T>( &mut self, items: impl IntoIterator<Item = T>, test_fn: impl AsyncFn(&mut Env<'db>, T) -> Errors<bool>, ) -> impl Future<Output = Errors<bool>>

Returns true if any of the items satisfies the predicate. Returns false if not. Stops executing as soon as either an error or a true result is found.

pub fn exists<T>( &mut self, items: impl IntoIterator<Item = T>, test_fn: impl AsyncFn(&mut Env<'db>, T) -> Errors<bool>, ) -> impl Future<Output = Errors<bool>>

Returns true if any of the items satisfies the predicate. Returns false if not. Stops executing as soon as either an error or a true result is d.

pub fn both( &mut self, a: impl AsyncFnOnce(&mut Env<'db>) -> Errors<bool>, b: impl AsyncFnOnce(&mut Env<'db>) -> Errors<bool>, ) -> impl Future<Output = Errors<bool>>

True if both a and b are true. Stops as soon as one is found to be false.

pub fn term_bounds( &self, perm: SymPerm<'db>, infer: InferVarIndex, ) -> SymGenericTermBoundIterator<'db>

Returns an iterator over the bounds on an inference variable that appears under perm, yielding terms:

• If this is a permission inference variable, the result are series of permission terms. These are directly converted from the RedPerm bounds you get if you call Self::red_perm_bounds.
• If this is a type inference variable, the result are series of type terms. They do not include the permission inference variable.

pub fn red_perm_bounds(&self, infer: InferVarIndex) -> RedPermBoundIterator<'db>

Returns an iterator over the red perm bounds on a permission inference variable.

pub fn red_ty_bounds(&self, infer: InferVarIndex) -> RedTyBoundIterator<'db>

Returns an iterator over the red ty bounds on a type inference variable. Note that each type inference variable has an associated permission inference variable and that this permission is not reflected in the red ty bound. Use Self::term_bounds to get back the complete inferred type.

pub fn loop_on_inference_var<T>( &self, infer: InferVarIndex, op: impl FnMut(&InferenceVarData<'db>) -> Option<T>, ) -> impl Future<Output = Option<T>>

where T: Serialize,

pub async fn for_each_bound( &mut self, direction: Direction, infer: InferVarIndex, op: impl AsyncFnMut(&mut Env<'db>, &RedTy<'db>, ArcOrElse<'db>) -> Errors<()>, ) -> Errors<()>

Invoke op for each new lower (or upper, depending on direction) bound on ?X.

impl<'db> Env<'db>

pub(crate) fn new(runtime: &Runtime<'db>, scope: Scope<'db, 'db>) -> Self

Create an empty environment

pub fn into_scope(self) -> Scope<'db, 'db>

Extract the scope from the environment.

Panics

If the scope has an outstanding reference.

pub fn universe(&self) -> Universe

pub fn db(&self) -> &'db dyn Db

Get the database

pub fn runtime(&self) -> &Runtime<'db>

Access the lower-level type checking runtime

pub fn fork( &self, log: impl FnOnce(&LogHandle<'db>) -> LogHandle<'db>, ) -> Env<'db>

Create a new environment from this environment. The log will be adjusted per the log function.

pub fn var_is_declared_to_be( &self, var: SymVariable<'db>, predicate: Predicate, ) -> bool

True if the given variable is declared to meet the given predicate.

fn assumed( &self, var: SymVariable<'db>, kind: impl Fn(AssumptionKind) -> bool, ) -> bool

pub fn open_universally<T>(&mut self, value: &T) -> T::LeafTerm

where T: BoundTerm<'db>,

Open the given symbols as universally quantified. Creates a new universe.

pub fn existential_substitution( &mut self, span: Span<'db>, variables: &[SymVariable<'db>], ) -> Vec<SymGenericTerm<'db>>

Create a substitution for binder consisting of inference variables

pub fn increment_universe(&mut self)

pub fn set_variable_sym_ty(&mut self, lv: SymVariable<'db>, ty: SymTy<'db>)

Sets the symbolic type for a program variable. Used during environment construction but typically you should use Self::push_program_variable_with_ty instead.

pub fn set_variable_ast_ty( &mut self, lv: SymVariable<'db>, decl: VariableDecl<'db>, )

Sets the AST type for a parameter that is in scope already. This AST type will be lazily symbolified when requested.

pub fn push_program_variable_with_ty( &mut self, lv: SymVariable<'db>, ty: SymTy<'db>, )

Extends the scope with a new program variable given its type.

pub fn set_return_ty(&mut self, ty: SymTy<'db>)

Set the return type of the current function.

pub fn return_ty(&self) -> Option<SymTy<'db>>

pub async fn variable_ty(&mut self, lv: SymVariable<'db>) -> SymTy<'db>

Returns the type of the given variable.

Panics

If the variable is not present.

pub fn fresh_inference_var( &mut self, kind: SymGenericKind, span: Span<'db>, ) -> InferVarIndex

Create a fresh inference variable of the given kind.

pub fn fresh_inference_var_term( &mut self, kind: SymGenericKind, span: Span<'db>, ) -> SymGenericTerm<'db>

A fresh term with an inference variable of the given kind.

pub fn fresh_ty_inference_var(&mut self, span: Span<'db>) -> SymTy<'db>

Create a fresh type inference variable.

pub(super) fn spawn_require_assignable_type( &mut self, live_after: LivePlaces, value_ty: SymTy<'db>, place_ty: SymTy<'db>, or_else: &dyn OrElse<'db>, )

Spawn a subtask that will require value_ty be assignable to place_ty.

pub(super) fn spawn_require_equal_types( &self, live_after: LivePlaces, expected_ty: SymTy<'db>, found_ty: SymTy<'db>, or_else: &dyn OrElse<'db>, )

Spawn a subtask that will require expected_ty be equal to found_ty.

pub(super) fn spawn_require_my_numeric_type( &mut self, live_after: LivePlaces, ty: SymTy<'db>, or_else: &dyn OrElse<'db>, )

Check that the value is a numeric type and has the permission my.

pub(super) fn spawn_require_numeric_type( &mut self, ty: SymTy<'db>, or_else: &dyn OrElse<'db>, )

Check that the value is a numeric type with any permission.

pub(super) fn spawn_require_future_type( &self, live_after: LivePlaces, ty: SymTy<'db>, awaited_ty: SymTy<'db>, or_else: &dyn OrElse<'db>, )

pub(super) fn spawn_require_where_clause( &self, where_clause: SymWhereClause<'db>, or_else: &dyn OrElse<'db>, )

pub fn spawn_if_not_never( &mut self, tys: &[SymTy<'db>], op: impl AsyncFnOnce(&mut Env<'db>) + 'db, )

Check whether any type in tys is known to be never (or error). If so, do nothing. Otherwise, if no type in tys is known to be never, invoke op (asynchronously).

pub fn describe_ty<'a>(&'a self, ty: SymTy<'db>) -> impl Display + 'a

pub fn spawn<R>( &mut self, task_description: TaskDescription<'db>, op: impl AsyncFnOnce(&mut Self) -> R + 'db, )

where R: DeferResult,

pub(crate) fn require_expr_has_bool_ty( &mut self, live_after: LivePlaces, expr: SymExpr<'db>, )

pub fn is_leased_var(&self, _var: SymVariable<'db>) -> bool

Check if the given (perm, type) variable is declared as mutable.

pub(crate) fn infer_var_span(&self, v: InferVarIndex) -> Span<'db>

Span for code that prompted creation of inference variable v.

pub(crate) fn infer_var_kind(&self, v: InferVarIndex) -> InferVarKind

Kind of this inference variable.

pub(crate) fn variances(&self, n: SymTyName<'db>) -> Vec<Variance>

pub fn perm_infer(&self, infer: InferVarIndex) -> InferVarIndex

If infer is a type variable, returns the permission variable associated with infer. If infer is a permission variable, just returns infer.

pub fn report(&self, diagnostic: Diagnostic) -> Reported

pub fn log(&self, message: &'static str, values: &[&dyn Serialize])

pub fn indent<R>( &mut self, message: &'static str, values: &[&dyn Serialize], op: impl AsyncFnOnce(&mut Self) -> R, ) -> impl Future<Output = R>

where R: Serialize,

pub async fn indent_with_compiler_location<R>( &mut self, compiler_location: &'static Location<'static>, message: &'static str, values: &[&dyn Serialize], op: impl AsyncFnOnce(&mut Self) -> R, ) -> R

where R: Serialize,

pub fn log_result<T>( &mut self, compiler_location: &'static Location<'static>, value: T, ) -> T

where T: Serialize,

pub(crate) fn bound_vars(&self) -> Vec<SymVariable<'db>>

Return a vector with all variables that are “bound” in the environment. These correspond to in-scope function parameters, generic types, etc.

pub fn insert_sub_infer_var_pair( &mut self, lower: InferVarIndex, upper: InferVarIndex, ) -> bool

Record that lower <: upper must hold, returning true if this is the first time that this has been recorded or false if it has been recorded before.

Panics

If lower == upper, as that is just always true, why record it?

pub fn red_bound( &self, infer: InferVarIndex, direction: Direction, ) -> RedBound<'_, 'db>

Return a struct that gives ability to peek, modify, or block on the lower or upper red-ty-bound on the given inference variable.

Trait Implementations

impl<'db> Debug for Env<'db>

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

Formats the value using the given formatter.