Trait kailua_types::ty::TypeContext
[−]
[src]
pub trait TypeContext { fn gen_report(&self) -> TypeReport; fn last_tvar(&self) -> Option<TVar>; fn gen_tvar(&mut self) -> TVar; fn copy_tvar(&mut self, tvar: TVar) -> TVar; fn assert_tvar_sub(&mut self, lhs: TVar, rhs: &Ty) -> TypeResult<()>; fn assert_tvar_sup(&mut self, lhs: TVar, rhs: &Ty) -> TypeResult<()>; fn assert_tvar_eq(&mut self, lhs: TVar, rhs: &Ty) -> TypeResult<()>; fn assert_tvar_sub_tvar(&mut self, lhs: TVar, rhs: TVar) -> TypeResult<()>; fn assert_tvar_eq_tvar(&mut self, lhs: TVar, rhs: TVar) -> TypeResult<()>; fn get_tvar_bounds(&self, tvar: TVar) -> (Flags, Flags); fn get_tvar_exact_type(&self, tvar: TVar) -> Option<Ty>; fn gen_rvar(&mut self) -> RVar; fn copy_rvar(&mut self, rvar: RVar) -> RVar; fn assert_rvar_sub(&mut self, lhs: RVar, rhs: RVar) -> TypeResult<()>; fn assert_rvar_eq(&mut self, lhs: RVar, rhs: RVar) -> TypeResult<()>; fn assert_rvar_includes(
&mut self,
lhs: RVar,
rhs: &[(Key, Slot)]
) -> TypeResult<()>; fn assert_rvar_closed(&mut self, rvar: RVar) -> TypeResult<()>; fn list_rvar_fields(
&self,
rvar: RVar,
f: &mut FnMut(&Key, &Slot) -> Result<(), ()>
) -> Result<RVar, ()>; fn fmt_class_name(
&self,
cid: ClassId,
f: &mut Formatter,
st: &DisplayState
) -> Result; fn fmt_class_system_name(
&self,
csid: ClassSystemId,
f: &mut Formatter,
st: &DisplayState
) -> Result; fn is_subclass_of(&self, lhs: ClassId, rhs: ClassId) -> bool; fn get_rvar_fields(&self, rvar: RVar) -> Vec<(Key, Slot)> { ... } fn get_type_bounds(&self, ty: &Ty) -> (Flags, Flags) { ... } fn resolve_exact_type(&self, ty: &Ty) -> Option<Ty> { ... } }
A trait that provides every type-related operations.
This interface is used to decouple the dependency between types and the type environment.
In practice, the full implementation is almost always provided by kailua_types::env::Types
.
Required Methods
fn gen_report(&self) -> TypeReport
Generates a new, empty type report.
fn last_tvar(&self) -> Option<TVar>
Returns the latest type variable generated, if any.
fn gen_tvar(&mut self) -> TVar
Generates a new fresh type variable.
fn copy_tvar(&mut self, tvar: TVar) -> TVar
Copies a type variable so that a new variable has the same constraints to the original but is no longer connected to the original.
Mainly used for generalization.
fn assert_tvar_sub(&mut self, lhs: TVar, rhs: &Ty) -> TypeResult<()>
Asserts that the type variable has given upper bound.
fn assert_tvar_sup(&mut self, lhs: TVar, rhs: &Ty) -> TypeResult<()>
Asserts that the type variable has given lower bound.
fn assert_tvar_eq(&mut self, lhs: TVar, rhs: &Ty) -> TypeResult<()>
Asserts that the type variable has given tight bound.
fn assert_tvar_sub_tvar(&mut self, lhs: TVar, rhs: TVar) -> TypeResult<()>
Asserts that the first type variable is a subtype of the second.
fn assert_tvar_eq_tvar(&mut self, lhs: TVar, rhs: TVar) -> TypeResult<()>
Asserts that the first type variable is equal to the second.
fn get_tvar_bounds(&self, tvar: TVar) -> (Flags, Flags)
Returns lower and upper bounds of given type variable as type flags.
fn get_tvar_exact_type(&self, tvar: TVar) -> Option<Ty>
Resolves a given type variable if there is a tight bound.
fn gen_rvar(&mut self) -> RVar
Generates a new fresh row variable.
fn copy_rvar(&mut self, rvar: RVar) -> RVar
Copies a row variable so that a new variable has the same fields to the original but is no longer connected to the original.
Mainly used for generalization.
fn assert_rvar_sub(&mut self, lhs: RVar, rhs: RVar) -> TypeResult<()>
Asserts that the first row variable is a subtype of the second.
The row "subtyping" here is quite restricted in Kailua; the subtyping relation is only checked for types of fields, and the list of fields in both variables should still be same (after necessary extension).
fn assert_rvar_eq(&mut self, lhs: RVar, rhs: RVar) -> TypeResult<()>
Asserts that the first row variable is equal to the second.
fn assert_rvar_includes(
&mut self,
lhs: RVar,
rhs: &[(Key, Slot)]
) -> TypeResult<()>
&mut self,
lhs: RVar,
rhs: &[(Key, Slot)]
) -> TypeResult<()>
Asserts that the row variable contains given fields. If there is a matching field, the types should be equal to each other.
fn assert_rvar_closed(&mut self, rvar: RVar) -> TypeResult<()>
Asserts that the row variable is no longer extensible.
fn list_rvar_fields(
&self,
rvar: RVar,
f: &mut FnMut(&Key, &Slot) -> Result<(), ()>
) -> Result<RVar, ()>
&self,
rvar: RVar,
f: &mut FnMut(&Key, &Slot) -> Result<(), ()>
) -> Result<RVar, ()>
Iterates over a list of field keys and corresponding types.
The closure can stop the iteration by returning Err
.
The iteration order is unspecified but all keys will be unique (guaranteed by type system).
If the iteration ends normally, it will return a row variable corresponding to
the extensible portion of given variable (this may be RVar::any()
if not generated).
For the inextensible records it will return RVar::empty()
.
This "last" row variable is purely for debugging and should not be used otherwise.
fn fmt_class_name(
&self,
cid: ClassId,
f: &mut Formatter,
st: &DisplayState
) -> Result
&self,
cid: ClassId,
f: &mut Formatter,
st: &DisplayState
) -> Result
Prints a type name for given nominal identifier to the formatter.
fn fmt_class_system_name(
&self,
csid: ClassSystemId,
f: &mut Formatter,
st: &DisplayState
) -> Result
&self,
csid: ClassSystemId,
f: &mut Formatter,
st: &DisplayState
) -> Result
Prints a type name for given nominal set identifier to the formatter.
fn is_subclass_of(&self, lhs: ClassId, rhs: ClassId) -> bool
Returns true if given nominal instance type is a subtype of another nominal instance type.
Provided Methods
fn get_rvar_fields(&self, rvar: RVar) -> Vec<(Key, Slot)>
Collects and returns a list of all known fields in the row variable.
fn get_type_bounds(&self, ty: &Ty) -> (Flags, Flags)
Returns a pair of type flags that is an exact lower and upper bound for that type.
Used as an approximate type bound testing like arithmetics. If possible, however, better be replaced with a non-instantiating assertion though.
fn resolve_exact_type(&self, ty: &Ty) -> Option<Ty>
Exactly resolves the type variable inside ty
if possible.
This is a requirement for table indexing and function calls.
Implementors
impl TypeContext for NoTypeContext
impl TypeContext for Types