Fix assert casting

This commit is contained in:
Shunsuke Shibayama 2022-10-09 20:29:30 +09:00
parent f94ab31256
commit aa7ae368dc
2 changed files with 47 additions and 11 deletions

View file

@ -1083,7 +1083,7 @@ impl Context {
type_spec: ast::TypeSpec,
call: &mut hir::Call,
) -> TyCheckResult<()> {
let target_t =
let cast_to =
self.instantiate_typespec(&type_spec, None, None, RegistrationMode::Normal)?;
let lhs = enum_unwrap!(
call.args.get_mut_left_or_key("pred").unwrap(),
@ -1092,37 +1092,45 @@ impl Context {
.lhs
.as_mut();
match (
self.supertype_of(lhs.ref_t(), &target_t),
self.subtype_of(lhs.ref_t(), &target_t),
self.supertype_of(lhs.ref_t(), &cast_to),
self.subtype_of(lhs.ref_t(), &cast_to),
) {
// assert 1 in {1}
(true, true) => {}
(true, true) => Ok(()),
// assert x in Int (x: Nat)
(false, true) => {} // TODO: warn (needless)
(false, true) => Ok(()), // TODO: warn (needless)
// assert x in Nat (x: Int)
(true, false) => {
if let hir::Expr::Accessor(ref acc) = lhs {
self.change_var_type(acc, target_t.clone())?;
self.change_var_type(acc, cast_to.clone())?;
}
match lhs.ref_t() {
Type::FreeVar(fv) if fv.is_linked() => {
let constraint = Constraint::new_subtype_of(target_t, Cyclicity::Not);
let constraint = Constraint::new_subtype_of(cast_to, Cyclicity::Not);
fv.replace(FreeKind::new_unbound(self.level, constraint));
}
Type::FreeVar(fv) => {
let new_constraint = Constraint::new_subtype_of(target_t, Cyclicity::Not);
let new_constraint = Constraint::new_subtype_of(cast_to, Cyclicity::Not);
fv.update_constraint(new_constraint);
}
_ => {
*lhs.ref_mut_t() = target_t;
*lhs.ref_mut_t() = cast_to;
}
}
}
// assert x in Str (x: Int)
(false, false) => todo!(),
}
Ok(())
}
// assert x in Str (x: Int)
(false, false) => Err(TyCheckErrors::from(TyCheckError::invalid_type_cast_error(
self.cfg.input.clone(),
line!() as usize,
lhs.loc(),
self.caused_by(),
&lhs.to_string(),
&cast_to,
None,
))),
}
}
fn change_var_type(&mut self, acc: &hir::Accessor, t: Type) -> TyCheckResult<()> {
#[allow(clippy::single_match)]

View file

@ -1568,6 +1568,34 @@ impl LowerError {
caused_by,
)
}
#[allow(clippy::too_many_arguments)]
pub fn invalid_type_cast_error(
input: Input,
errno: usize,
loc: Location,
caused_by: AtomicStr,
name: &str,
cast_to: &Type,
hint: Option<AtomicStr>,
) -> Self {
Self::new(
ErrorCore::new(
errno,
TypeError,
loc,
switch_lang!(
"japanese" => format!("{YELLOW}{name}{RESET}の型を{RED}{cast_to}{RESET}にキャストすることはできません"),
"simplified_chinese" => format!("{YELLOW}{name}{RESET}的类型无法转换为{RED}{cast_to}{RESET}"),
"traditional_chinese" => format!("{YELLOW}{name}{RESET}的類型無法轉換為{RED}{cast_to}{RESET}"),
"english" => format!("the type of {YELLOW}{name}{RESET} cannot be cast to {RED}{cast_to}{RESET}"),
),
hint,
),
input,
caused_by,
)
}
}
#[derive(Debug)]