mirror of
https://github.com/erg-lang/erg.git
synced 2025-08-04 02:39:20 +00:00
chore: union/intersection subtyping
This commit is contained in:
parent
8c02e2dcc9
commit
5f8d744e47
6 changed files with 68 additions and 16 deletions
|
@ -9,7 +9,7 @@ use erg_common::{assume_unreachable, log};
|
|||
use erg_common::{Str, Triple};
|
||||
|
||||
use crate::context::initialize::const_func::sub_tpdict_get;
|
||||
use crate::ty::constructors::{and, bounded, not, or, poly};
|
||||
use crate::ty::constructors::{self, and, bounded, not, or, poly};
|
||||
use crate::ty::free::{Constraint, FreeKind, FreeTyVar};
|
||||
use crate::ty::typaram::{TyParam, TyParamOrdering};
|
||||
use crate::ty::value::ValueObj;
|
||||
|
@ -1263,15 +1263,18 @@ impl Context {
|
|||
|
||||
/// ```erg
|
||||
/// union_add(Int or ?T(:> NoneType), Nat) == Int or ?T
|
||||
/// union_add(Nat or ?T(:> NoneType), Int) == Int or ?T
|
||||
/// union_add(Int or ?T(:> NoneType), Str) == Int or ?T or Str
|
||||
/// ```
|
||||
fn union_add(&self, union: &Type, elem: &Type) -> Type {
|
||||
let union_ts = union.union_types();
|
||||
let bounded = union_ts.into_iter().map(|t| t.lower_bounded());
|
||||
let ors = union.ors();
|
||||
let bounded = ors.iter().map(|t| t.lower_bounded());
|
||||
for t in bounded {
|
||||
if self.supertype_of(&t, elem) {
|
||||
return union.clone();
|
||||
}
|
||||
} /* else if ors.contains(&t) && self.subtype_of(&t, elem) {
|
||||
return constructors::ors(ors.exclude(&t).include(elem.clone()));
|
||||
} */
|
||||
}
|
||||
or(union.clone(), elem.clone())
|
||||
}
|
||||
|
@ -1353,12 +1356,34 @@ impl Context {
|
|||
},
|
||||
(_, Not(r)) => self.diff(lhs, r),
|
||||
(Not(l), _) => self.diff(rhs, l),
|
||||
// A and B and A == A and B
|
||||
(other, and @ And(_, _)) | (and @ And(_, _), other) => {
|
||||
self.intersection_add(and, other)
|
||||
}
|
||||
// overloading
|
||||
(l, r) if l.is_subr() && r.is_subr() => and(lhs.clone(), rhs.clone()),
|
||||
_ => self.simple_intersection(lhs, rhs),
|
||||
}
|
||||
}
|
||||
|
||||
/// ```erg
|
||||
/// intersection_add(Nat and ?T(:> NoneType), Int) == Nat and ?T
|
||||
/// intersection_add(Int and ?T(:> NoneType), Nat) == Nat and ?T
|
||||
/// intersection_add(Int and ?T(:> NoneType), Str) == Never
|
||||
/// ```
|
||||
fn intersection_add(&self, intersection: &Type, elem: &Type) -> Type {
|
||||
let ands = intersection.ands();
|
||||
let bounded = ands.iter().map(|t| t.lower_bounded());
|
||||
for t in bounded {
|
||||
if self.subtype_of(&t, elem) {
|
||||
return intersection.clone();
|
||||
} else if self.supertype_of(&t, elem) {
|
||||
return constructors::ands(ands.exclude(&t).include(elem.clone()));
|
||||
}
|
||||
}
|
||||
and(intersection.clone(), elem.clone())
|
||||
}
|
||||
|
||||
fn simple_intersection(&self, lhs: &Type, rhs: &Type) -> Type {
|
||||
// ?T and ?U will not be unified
|
||||
if lhs.is_unbound_var() || rhs.is_unbound_var() {
|
||||
|
@ -1405,7 +1430,7 @@ impl Context {
|
|||
&self,
|
||||
refine: RefinementType,
|
||||
) -> Result<Type, RefinementType> {
|
||||
let unions = refine.t.union_types();
|
||||
let unions = refine.t.ors();
|
||||
let complement = Type::from(self.type_from_pred(refine.pred.clone().invert()));
|
||||
let union = unions
|
||||
.into_iter()
|
||||
|
|
|
@ -953,7 +953,7 @@ impl Context {
|
|||
self.caused_by(),
|
||||
subr_t.non_default_params,
|
||||
subr_t.default_params,
|
||||
intersecs,
|
||||
intersecs.iter(),
|
||||
))
|
||||
}
|
||||
}
|
||||
|
|
|
@ -692,10 +692,10 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
|
|||
}
|
||||
match (maybe_sub, maybe_sup) {
|
||||
(FreeVar(sub_fv), _) if sub_fv.is_linked() => {
|
||||
self.sub_unify(&sub_fv.crack(), maybe_sup)?;
|
||||
self.sub_unify(sub_fv.unsafe_crack(), maybe_sup)?;
|
||||
}
|
||||
(_, FreeVar(sup_fv)) if sup_fv.is_linked() => {
|
||||
self.sub_unify(maybe_sub, &sup_fv.crack())?;
|
||||
self.sub_unify(maybe_sub, sup_fv.unsafe_crack())?;
|
||||
}
|
||||
// lfv's sup can be shrunk (take min), rfv's sub can be expanded (take union)
|
||||
// lfvのsupは縮小可能(minを取る)、rfvのsubは拡大可能(unionを取る)
|
||||
|
@ -957,7 +957,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
|
|||
// This increases the quality of error reporting
|
||||
// (Try commenting out this part and run tests/should_err/subtyping.er to see the error report changes on lines 29-30)
|
||||
if maybe_sub.union_size().max(sub.union_size()) < new_sub.union_size()
|
||||
&& new_sub.union_types().iter().any(|t| !t.is_unbound_var())
|
||||
&& new_sub.ors().iter().any(|t| !t.is_unbound_var())
|
||||
{
|
||||
let (l, r) = new_sub.union_pair().unwrap_or((maybe_sub.clone(), sub));
|
||||
let unified = self.unify(&l, &r);
|
||||
|
|
|
@ -5,7 +5,7 @@ use erg_common::io::Input;
|
|||
use erg_common::set::Set;
|
||||
use erg_common::style::{StyledStr, StyledString, StyledStrings, Stylize};
|
||||
use erg_common::traits::{Locational, NoTypeDisplay};
|
||||
use erg_common::{fmt_iter, fmt_option_map, fmt_vec, fmt_vec_split_with, switch_lang, Str};
|
||||
use erg_common::{fmt_iter, fmt_iter_split_with, fmt_option_map, fmt_vec, switch_lang, Str};
|
||||
|
||||
use crate::error::*;
|
||||
use crate::ty::{ParamTy, Predicate, TyParam, Type};
|
||||
|
@ -1308,23 +1308,23 @@ passed keyword args: {kw_args_len}"
|
|||
)
|
||||
}
|
||||
|
||||
pub fn overload_error(
|
||||
pub fn overload_error<'a>(
|
||||
input: Input,
|
||||
errno: usize,
|
||||
loc: Location,
|
||||
caused_by: String,
|
||||
pos_args: Vec<ParamTy>,
|
||||
kw_args: Vec<ParamTy>,
|
||||
found: Vec<Type>,
|
||||
found: impl Iterator<Item = &'a Type>,
|
||||
) -> Self {
|
||||
Self::new(
|
||||
ErrorCore::new(
|
||||
vec![],
|
||||
switch_lang!(
|
||||
"japanese" => format!("オーバーロード解決に失敗しました\nオーバーロード型:\n* {}\n渡された位置引数: {}\n渡された名前付き引数: {}", fmt_vec_split_with(&found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
"simplified_chinese" => format!("无法解析重载\n重载类型:\n* {}\n位置参数: {}\n命名参数: {}", fmt_vec_split_with(&found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
"traditional_chinese" => format!("無法解析重載\n重載類型:\n* {}\n位置參數: {}\n命名參數: {}", fmt_vec_split_with(&found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
"english" => format!("cannot resolve overload\noverloaded type:\n* {}\npassed positional arguments: {}\npassed named arguments: {}", fmt_vec_split_with(&found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
"japanese" => format!("オーバーロード解決に失敗しました\nオーバーロード型:\n* {}\n渡された位置引数: {}\n渡された名前付き引数: {}", fmt_iter_split_with(found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
"simplified_chinese" => format!("无法解析重载\n重载类型:\n* {}\n位置参数: {}\n命名参数: {}", fmt_iter_split_with(found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
"traditional_chinese" => format!("無法解析重載\n重載類型:\n* {}\n位置參數: {}\n命名參數: {}", fmt_iter_split_with(found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
"english" => format!("cannot resolve overload\noverloaded type:\n* {}\npassed positional arguments: {}\npassed named arguments: {}", fmt_iter_split_with(found, "\n* "), fmt_vec(&pos_args), fmt_vec(&kw_args)),
|
||||
),
|
||||
errno,
|
||||
TypeError,
|
||||
|
|
|
@ -451,6 +451,7 @@ pub fn and(lhs: Type, rhs: Type) -> Type {
|
|||
Type::And(Box::new(Type::And(l, r)), Box::new(other))
|
||||
}
|
||||
}
|
||||
(Type::Obj, other) | (other, Type::Obj) => other,
|
||||
(lhs, rhs) => Type::And(Box::new(lhs), Box::new(rhs)),
|
||||
}
|
||||
}
|
||||
|
@ -466,10 +467,19 @@ pub fn or(lhs: Type, rhs: Type) -> Type {
|
|||
Type::Or(Box::new(Type::Or(l, r)), Box::new(other))
|
||||
}
|
||||
}
|
||||
(Type::Never, other) | (other, Type::Never) => other,
|
||||
(lhs, rhs) => Type::Or(Box::new(lhs), Box::new(rhs)),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn ors(tys: impl IntoIterator<Item = Type>) -> Type {
|
||||
tys.into_iter().fold(Type::Never, or)
|
||||
}
|
||||
|
||||
pub fn ands(tys: impl IntoIterator<Item = Type>) -> Type {
|
||||
tys.into_iter().fold(Type::Obj, and)
|
||||
}
|
||||
|
||||
pub fn not(ty: Type) -> Type {
|
||||
Type::Not(Box::new(ty))
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue