mirror of
https://github.com/erg-lang/erg.git
synced 2025-08-03 02:13:11 +00:00
fix(typechecker): type generalization & dereference bugs
* `Context::subtype_of` now has `allow_cast` param. If this is `false`, cast-aware comparisons are not performed.
This commit is contained in:
parent
3fea50f8bc
commit
4dcca2b06d
18 changed files with 689 additions and 247 deletions
|
@ -156,6 +156,15 @@ impl<K: Hash + Eq, V> Dict<K, V> {
|
|||
self.dict.get(k)
|
||||
}
|
||||
|
||||
pub fn get_by(&self, k: &K, cmp: impl Fn(&K, &K) -> bool) -> Option<&V> {
|
||||
for (k_, v) in self.dict.iter() {
|
||||
if cmp(k, k_) {
|
||||
return Some(v);
|
||||
}
|
||||
}
|
||||
None
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn get_mut<Q: ?Sized>(&mut self, k: &Q) -> Option<&mut V>
|
||||
where
|
||||
|
|
|
@ -125,6 +125,14 @@ impl<T: Hash + Eq> Set<T> {
|
|||
self.elems.get(value)
|
||||
}
|
||||
|
||||
pub fn get_by<Q>(&self, value: &Q, cmp: impl Fn(&Q, &Q) -> bool) -> Option<&T>
|
||||
where
|
||||
T: Borrow<Q>,
|
||||
Q: ?Sized + Hash + Eq,
|
||||
{
|
||||
self.elems.iter().find(|&v| cmp(v.borrow(), value))
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn fast_eq(&self, other: &Set<T>) -> bool {
|
||||
self.elems == other.elems
|
||||
|
@ -192,6 +200,10 @@ impl<T: Hash + Eq + Clone> Set<T> {
|
|||
self.elems.union(&other.elems)
|
||||
}
|
||||
|
||||
pub fn union_from_iter<I: Iterator<Item = T>>(&self, iter: I) -> Set<T> {
|
||||
self.union(&iter.collect())
|
||||
}
|
||||
|
||||
/// ```
|
||||
/// # use erg_common::set;
|
||||
/// assert_eq!(set!{1, 2, 3}.intersection(&set!{2, 3, 4}), set!{2, 3});
|
||||
|
@ -212,6 +224,27 @@ impl<T: Hash + Eq + Clone> Set<T> {
|
|||
self.intersection(&iter.collect())
|
||||
}
|
||||
|
||||
/// ```
|
||||
/// # use erg_common::set;
|
||||
/// # use erg_common::set::Set;
|
||||
/// assert_eq!(Set::multi_intersection([set!{1, 3}, set!{1, 2}].into_iter()), set!{1});
|
||||
/// assert_eq!(Set::multi_intersection([set!{1, 3}, set!{1, 2}, set!{2}].into_iter()), set!{1, 2});
|
||||
/// assert_eq!(Set::multi_intersection([set!{1, 3}, set!{1, 2}, set!{2, 3}].into_iter()), set!{1, 2, 3});
|
||||
/// ```
|
||||
pub fn multi_intersection<I>(mut i: I) -> Set<T>
|
||||
where
|
||||
I: Iterator<Item = Set<T>> + Clone,
|
||||
{
|
||||
let mut res = set! {};
|
||||
while let Some(s) = i.next() {
|
||||
res = res.union_from_iter(
|
||||
s.into_iter()
|
||||
.filter(|x| i.clone().any(|set| set.contains(x))),
|
||||
);
|
||||
}
|
||||
res
|
||||
}
|
||||
|
||||
pub fn difference(&self, other: &Set<T>) -> Set<T> {
|
||||
let u = self.elems.difference(&other.elems);
|
||||
Self {
|
||||
|
|
|
@ -1179,6 +1179,10 @@ pub trait AddrEq {
|
|||
}
|
||||
}
|
||||
|
||||
pub trait StructuralEq {
|
||||
fn structural_eq(&self, other: &Self) -> bool;
|
||||
}
|
||||
|
||||
pub trait __Str__ {
|
||||
fn __str__(&self) -> String;
|
||||
}
|
||||
|
|
|
@ -3,6 +3,7 @@ use std::option::Option; // conflicting to Type::Option
|
|||
|
||||
use erg_common::error::MultiErrorDisplay;
|
||||
use erg_common::style::colors::DEBUG_ERROR;
|
||||
use erg_common::traits::StructuralEq;
|
||||
|
||||
use crate::ty::constructors::{and, not, or, poly};
|
||||
use crate::ty::free::{Constraint, FreeKind};
|
||||
|
@ -44,16 +45,18 @@ impl Context {
|
|||
res
|
||||
}
|
||||
|
||||
pub(crate) fn eq_tp(&self, lhs: &TyParam, rhs: &TyParam) -> bool {
|
||||
pub(crate) fn eq_tp(&self, lhs: &TyParam, rhs: &TyParam, allow_cast: bool) -> bool {
|
||||
match (lhs, rhs) {
|
||||
(TyParam::Type(lhs), TyParam::Type(rhs)) => return self.same_type_of(lhs, rhs),
|
||||
(TyParam::Type(lhs), TyParam::Type(rhs)) => {
|
||||
return self.same_type_of(lhs, rhs, allow_cast)
|
||||
}
|
||||
(TyParam::Mono(l), TyParam::Mono(r)) => {
|
||||
if let (Some(l), Some(r)) = (self.rec_get_const_obj(l), self.rec_get_const_obj(r)) {
|
||||
return l == r;
|
||||
}
|
||||
}
|
||||
(TyParam::UnaryOp { op: lop, val: lval }, TyParam::UnaryOp { op: rop, val: rval }) => {
|
||||
return lop == rop && self.eq_tp(lval, rval);
|
||||
return lop == rop && self.eq_tp(lval, rval, allow_cast);
|
||||
}
|
||||
(
|
||||
TyParam::BinOp {
|
||||
|
@ -67,7 +70,9 @@ impl Context {
|
|||
rhs: rr,
|
||||
},
|
||||
) => {
|
||||
return lop == rop && self.eq_tp(ll, rl) && self.eq_tp(lr, rr);
|
||||
return lop == rop
|
||||
&& self.eq_tp(ll, rl, allow_cast)
|
||||
&& self.eq_tp(lr, rr, allow_cast);
|
||||
}
|
||||
(
|
||||
TyParam::App {
|
||||
|
@ -84,11 +89,11 @@ impl Context {
|
|||
&& largs
|
||||
.iter()
|
||||
.zip(rargs.iter())
|
||||
.all(|(l, r)| self.eq_tp(l, r))
|
||||
.all(|(l, r)| self.eq_tp(l, r, allow_cast))
|
||||
}
|
||||
(TyParam::FreeVar(fv), other) | (other, TyParam::FreeVar(fv)) => match &*fv.borrow() {
|
||||
FreeKind::Linked(linked) | FreeKind::UndoableLinked { t: linked, .. } => {
|
||||
return self.eq_tp(linked, other);
|
||||
return self.eq_tp(linked, other, allow_cast);
|
||||
}
|
||||
FreeKind::Unbound { constraint, .. }
|
||||
| FreeKind::NamedUnbound { constraint, .. } => {
|
||||
|
@ -97,14 +102,14 @@ impl Context {
|
|||
panic!("Uninited type variable: {fv}");
|
||||
}
|
||||
let other_t = self.type_of(other);
|
||||
return self.same_type_of(t, &other_t);
|
||||
return self.same_type_of(t, &other_t, allow_cast);
|
||||
}
|
||||
},
|
||||
(TyParam::Value(ValueObj::Type(l)), TyParam::Type(r)) => {
|
||||
return self.same_type_of(l.typ(), r.as_ref());
|
||||
return self.same_type_of(l.typ(), r.as_ref(), allow_cast);
|
||||
}
|
||||
(TyParam::Type(l), TyParam::Value(ValueObj::Type(r))) => {
|
||||
return self.same_type_of(l.as_ref(), r.typ());
|
||||
return self.same_type_of(l.as_ref(), r.typ(), allow_cast);
|
||||
}
|
||||
(l, r) if l == r => {
|
||||
return true;
|
||||
|
@ -112,24 +117,24 @@ impl Context {
|
|||
(l, r) if l.has_unbound_var() || r.has_unbound_var() => {
|
||||
let lt = self.get_tp_t(l).unwrap();
|
||||
let rt = self.get_tp_t(r).unwrap();
|
||||
return self.same_type_of(<, &rt);
|
||||
return self.same_type_of(<, &rt, allow_cast);
|
||||
}
|
||||
_ => {}
|
||||
}
|
||||
self.shallow_eq_tp(lhs, rhs)
|
||||
}
|
||||
|
||||
pub(crate) fn related(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
self.supertype_of(lhs, rhs) || self.subtype_of(lhs, rhs)
|
||||
pub(crate) fn related(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
self.supertype_of(lhs, rhs, allow_cast) || self.subtype_of(lhs, rhs, allow_cast)
|
||||
}
|
||||
|
||||
pub(crate) fn supertype_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
let res = match self.cheap_supertype_of(lhs, rhs) {
|
||||
pub(crate) fn supertype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
let res = match Self::cheap_supertype_of(lhs, rhs, allow_cast) {
|
||||
(Absolutely, judge) => judge,
|
||||
(Maybe, judge) => {
|
||||
judge
|
||||
|| self.structural_supertype_of(lhs, rhs)
|
||||
|| self.nominal_supertype_of(lhs, rhs)
|
||||
|| self.structural_supertype_of(lhs, rhs, allow_cast)
|
||||
|| self.nominal_supertype_of(lhs, rhs, allow_cast)
|
||||
}
|
||||
};
|
||||
log!("answer: {lhs} {DEBUG_ERROR}:>{RESET} {rhs} == {res}");
|
||||
|
@ -141,72 +146,90 @@ impl Context {
|
|||
/// => Module.super_types == [Named]
|
||||
/// Seq(T) :> Range(T)
|
||||
/// => Range(T).super_types == [Eq, Mutate, Seq('T), Output('T)]
|
||||
pub(crate) fn subtype_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
match self.cheap_subtype_of(lhs, rhs) {
|
||||
pub(crate) fn subtype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
match Self::cheap_subtype_of(lhs, rhs, allow_cast) {
|
||||
(Absolutely, judge) => judge,
|
||||
(Maybe, judge) => {
|
||||
judge || self.structural_subtype_of(lhs, rhs) || self.nominal_subtype_of(lhs, rhs)
|
||||
judge
|
||||
|| self.structural_subtype_of(lhs, rhs, allow_cast)
|
||||
|| self.nominal_subtype_of(lhs, rhs, allow_cast)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
self.supertype_of(lhs, rhs) && self.subtype_of(lhs, rhs)
|
||||
pub(crate) fn same_type_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
self.supertype_of(lhs, rhs, allow_cast) && self.subtype_of(lhs, rhs, allow_cast)
|
||||
}
|
||||
|
||||
pub(crate) fn cheap_supertype_of(&self, lhs: &Type, rhs: &Type) -> (Credibility, bool) {
|
||||
pub(crate) fn cheap_supertype_of(
|
||||
lhs: &Type,
|
||||
rhs: &Type,
|
||||
allow_cast: bool,
|
||||
) -> (Credibility, bool) {
|
||||
if lhs == rhs {
|
||||
return (Absolutely, true);
|
||||
}
|
||||
match (lhs, rhs) {
|
||||
(Obj, _) | (_, Never | Failure) => (Absolutely, true),
|
||||
(_, Obj) if lhs.is_simple_class() => (Absolutely, false),
|
||||
(Never | Failure, _) if rhs.is_simple_class() => (Absolutely, false),
|
||||
(Obj, _) | (_, Never | Failure) if allow_cast => (Absolutely, true),
|
||||
(_, Obj) if lhs.is_simple_class() && allow_cast => (Absolutely, false),
|
||||
(Never | Failure, _) if rhs.is_simple_class() && allow_cast => (Absolutely, false),
|
||||
(Float | Ratio | Int | Nat | Bool, Bool)
|
||||
| (Float | Ratio | Int | Nat, Nat)
|
||||
| (Float | Ratio | Int, Int)
|
||||
| (Float | Ratio, Ratio)
|
||||
| (Float, Float) => (Absolutely, true),
|
||||
(Type, ClassType | TraitType) => (Absolutely, true),
|
||||
(Type::Uninited, _) | (_, Type::Uninited) => panic!("used an uninited type variable"),
|
||||
if allow_cast =>
|
||||
{
|
||||
(Absolutely, true)
|
||||
}
|
||||
(Type, ClassType | TraitType) if allow_cast => (Absolutely, true),
|
||||
(Uninited, _) | (_, Uninited) => panic!("used an uninited type variable"),
|
||||
(
|
||||
Type::Mono(n),
|
||||
Mono(n),
|
||||
Subr(SubrType {
|
||||
kind: SubrKind::Func,
|
||||
..
|
||||
}),
|
||||
) if &n[..] == "GenericFunc" => (Absolutely, true),
|
||||
) if &n[..] == "GenericFunc" && allow_cast => (Absolutely, true),
|
||||
(
|
||||
Type::Mono(n),
|
||||
Mono(n),
|
||||
Subr(SubrType {
|
||||
kind: SubrKind::Proc,
|
||||
..
|
||||
}),
|
||||
) if &n[..] == "GenericProc" => (Absolutely, true),
|
||||
(Type::Mono(l), Type::Poly { name: r, .. })
|
||||
if &l[..] == "GenericArray" && &r[..] == "Array" =>
|
||||
) if &n[..] == "GenericProc" && allow_cast => (Absolutely, true),
|
||||
(Mono(l), Poly { name: r, .. })
|
||||
if &l[..] == "GenericArray" && &r[..] == "Array" && allow_cast =>
|
||||
{
|
||||
(Absolutely, true)
|
||||
}
|
||||
(Type::Mono(l), Type::Poly { name: r, .. })
|
||||
if &l[..] == "GenericDict" && &r[..] == "Dict" =>
|
||||
(Mono(l), Poly { name: r, .. })
|
||||
if &l[..] == "GenericDict" && &r[..] == "Dict" && allow_cast =>
|
||||
{
|
||||
(Absolutely, true)
|
||||
}
|
||||
(Type::Mono(l), Type::Mono(r))
|
||||
(Mono(l), Mono(r))
|
||||
if &l[..] == "GenericCallable"
|
||||
&& (&r[..] == "GenericFunc"
|
||||
|| &r[..] == "GenericProc"
|
||||
|| &r[..] == "GenericFuncMethod"
|
||||
|| &r[..] == "GenericProcMethod") =>
|
||||
|| &r[..] == "GenericProcMethod")
|
||||
&& allow_cast =>
|
||||
{
|
||||
(Absolutely, true)
|
||||
}
|
||||
(_, Type::FreeVar(fv)) | (Type::FreeVar(fv), _) => match fv.get_subsup() {
|
||||
Some((Type::Never, Type::Obj)) => (Absolutely, true),
|
||||
(FreeVar(l), FreeVar(r)) => {
|
||||
log!(err "{l}/{r}/{}", l.structural_eq(r));
|
||||
if l.structural_eq(r) {
|
||||
(Absolutely, true)
|
||||
} else {
|
||||
(Maybe, false)
|
||||
}
|
||||
}
|
||||
(_, FreeVar(fv)) | (FreeVar(fv), _) => match fv.get_subsup() {
|
||||
Some((Type::Never, Type::Obj)) if allow_cast => (Absolutely, true),
|
||||
_ => (Maybe, false),
|
||||
},
|
||||
(Type::Mono(n), Subr(_) | Quantified(_)) if &n[..] == "GenericCallable" => {
|
||||
(Mono(n), Subr(_) | Quantified(_)) if &n[..] == "GenericCallable" && allow_cast => {
|
||||
(Absolutely, true)
|
||||
}
|
||||
(lhs, rhs) if lhs.is_simple_class() && rhs.is_simple_class() => (Absolutely, false),
|
||||
|
@ -214,21 +237,24 @@ impl Context {
|
|||
}
|
||||
}
|
||||
|
||||
fn cheap_subtype_of(&self, lhs: &Type, rhs: &Type) -> (Credibility, bool) {
|
||||
self.cheap_supertype_of(rhs, lhs)
|
||||
fn cheap_subtype_of(lhs: &Type, rhs: &Type, allow_cast: bool) -> (Credibility, bool) {
|
||||
Self::cheap_supertype_of(rhs, lhs, allow_cast)
|
||||
}
|
||||
|
||||
/// make judgments that include supertypes in the same namespace & take into account glue patches
|
||||
/// 同一名前空間にある上位型を含めた判定&接着パッチを考慮した判定を行う
|
||||
fn nominal_supertype_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
fn nominal_supertype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
if !allow_cast && lhs != rhs {
|
||||
return false;
|
||||
}
|
||||
if let Some(res) = self.inquire_cache(lhs, rhs) {
|
||||
return res;
|
||||
}
|
||||
if let (Absolutely, judge) = self.classes_supertype_of(lhs, rhs) {
|
||||
if let (Absolutely, judge) = self.classes_supertype_of(lhs, rhs, allow_cast) {
|
||||
self.register_cache(lhs, rhs, judge);
|
||||
return judge;
|
||||
}
|
||||
if let (Absolutely, judge) = self.traits_supertype_of(lhs, rhs) {
|
||||
if let (Absolutely, judge) = self.traits_supertype_of(lhs, rhs, allow_cast) {
|
||||
self.register_cache(lhs, rhs, judge);
|
||||
return judge;
|
||||
}
|
||||
|
@ -236,27 +262,33 @@ impl Context {
|
|||
false
|
||||
}
|
||||
|
||||
fn nominal_subtype_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
self.nominal_supertype_of(rhs, lhs)
|
||||
fn nominal_subtype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
self.nominal_supertype_of(rhs, lhs, allow_cast)
|
||||
}
|
||||
|
||||
pub(crate) fn find_patches_of<'a>(
|
||||
&'a self,
|
||||
typ: &'a Type,
|
||||
allow_cast: bool,
|
||||
) -> impl Iterator<Item = &'a Context> {
|
||||
self.all_patches().into_iter().filter(|ctx| {
|
||||
self.all_patches().into_iter().filter(move |ctx| {
|
||||
if let ContextKind::Patch(base) = &ctx.kind {
|
||||
return self.supertype_of(base, typ);
|
||||
return self.supertype_of(base, typ, allow_cast);
|
||||
}
|
||||
false
|
||||
})
|
||||
}
|
||||
|
||||
fn _find_compatible_glue_patch(&self, sup: &Type, sub: &Type) -> Option<&Context> {
|
||||
fn _find_compatible_glue_patch(
|
||||
&self,
|
||||
sup: &Type,
|
||||
sub: &Type,
|
||||
allow_cast: bool,
|
||||
) -> Option<&Context> {
|
||||
for patch in self.all_patches().into_iter() {
|
||||
if let ContextKind::GluePatch(tr_inst) = &patch.kind {
|
||||
if self.subtype_of(sub, &tr_inst.sub_type)
|
||||
&& self.subtype_of(&tr_inst.sup_trait, sup)
|
||||
if self.subtype_of(sub, &tr_inst.sub_type, allow_cast)
|
||||
&& self.subtype_of(&tr_inst.sup_trait, sup, allow_cast)
|
||||
{
|
||||
return Some(patch);
|
||||
}
|
||||
|
@ -265,7 +297,12 @@ impl Context {
|
|||
None
|
||||
}
|
||||
|
||||
fn classes_supertype_of(&self, lhs: &Type, rhs: &Type) -> (Credibility, bool) {
|
||||
fn classes_supertype_of(
|
||||
&self,
|
||||
lhs: &Type,
|
||||
rhs: &Type,
|
||||
allow_cast: bool,
|
||||
) -> (Credibility, bool) {
|
||||
if !self.is_class(lhs) || !self.is_class(rhs) {
|
||||
return (Maybe, false);
|
||||
}
|
||||
|
@ -284,12 +321,12 @@ impl Context {
|
|||
rhs_sup.clone()
|
||||
};
|
||||
// Not `supertype_of` (only structures are compared)
|
||||
match self.cheap_supertype_of(lhs, &rhs_sup) {
|
||||
match Self::cheap_supertype_of(lhs, &rhs_sup, allow_cast) {
|
||||
(Absolutely, true) => {
|
||||
return (Absolutely, true);
|
||||
}
|
||||
(Maybe, _) => {
|
||||
if self.structural_supertype_of(lhs, &rhs_sup) {
|
||||
if self.structural_supertype_of(lhs, &rhs_sup, allow_cast) {
|
||||
return (Absolutely, true);
|
||||
}
|
||||
}
|
||||
|
@ -303,19 +340,19 @@ impl Context {
|
|||
// e.g. Eq(Nat) :> Nat
|
||||
// Nat.super_traits = [Add(Nat), Eq(Nat), Sub(Float), ...]
|
||||
// e.g. Eq :> ?L or ?R (if ?L <: Eq and ?R <: Eq)
|
||||
fn traits_supertype_of(&self, lhs: &Type, rhs: &Type) -> (Credibility, bool) {
|
||||
fn traits_supertype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> (Credibility, bool) {
|
||||
if !self.is_trait(lhs) {
|
||||
return (Maybe, false);
|
||||
}
|
||||
if let Some((_, rhs_ctx)) = self.get_nominal_type_ctx(rhs) {
|
||||
for rhs_sup in rhs_ctx.super_traits.iter() {
|
||||
// Not `supertype_of` (only structures are compared)
|
||||
match self.cheap_supertype_of(lhs, rhs_sup) {
|
||||
match Self::cheap_supertype_of(lhs, rhs_sup, allow_cast) {
|
||||
(Absolutely, true) => {
|
||||
return (Absolutely, true);
|
||||
}
|
||||
(Maybe, _) => {
|
||||
if self.structural_supertype_of(lhs, rhs_sup) {
|
||||
if self.structural_supertype_of(lhs, rhs_sup, allow_cast) {
|
||||
return (Absolutely, true);
|
||||
}
|
||||
}
|
||||
|
@ -335,7 +372,7 @@ impl Context {
|
|||
/// Use `supertype_of` for complete judgement.
|
||||
/// 単一化、評価等はここでは行わない、スーパータイプになる可能性があるかだけ判定する
|
||||
/// ので、lhsが(未連携)型変数の場合は単一化せずにtrueを返す
|
||||
pub(crate) fn structural_supertype_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
pub(crate) fn structural_supertype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
match (lhs, rhs) {
|
||||
// Proc :> Func if params are compatible
|
||||
(Subr(ls), Subr(rs)) if ls.kind == rs.kind || ls.kind.is_proc() => {
|
||||
|
@ -346,7 +383,7 @@ impl Context {
|
|||
.iter()
|
||||
.find(|rpt| rpt.name() == lpt.name())
|
||||
{
|
||||
if !self.subtype_of(lpt.typ(), rpt.typ()) {
|
||||
if !self.subtype_of(lpt.typ(), rpt.typ(), allow_cast) {
|
||||
return false;
|
||||
}
|
||||
} else {
|
||||
|
@ -357,27 +394,38 @@ impl Context {
|
|||
};
|
||||
// () -> Never <: () -> Int <: () -> Object
|
||||
// (Object) -> Int <: (Int) -> Int <: (Never) -> Int
|
||||
ls.non_default_params.len() == rs.non_default_params.len()
|
||||
// REVIEW:
|
||||
&& ls.default_params.len() == rs.default_params.len()
|
||||
&& self.supertype_of(&ls.return_t, &rs.return_t) // covariant
|
||||
&& ls.non_default_params.iter()
|
||||
let same_params_len = ls.non_default_params.len() == rs.non_default_params.len()
|
||||
// REVIEW:
|
||||
&& ls.default_params.len() == rs.default_params.len();
|
||||
let return_t_judge = self.supertype_of(&ls.return_t, &rs.return_t, allow_cast); // covariant
|
||||
let non_defaults_judge = ls
|
||||
.non_default_params
|
||||
.iter()
|
||||
.zip(rs.non_default_params.iter())
|
||||
.all(|(l, r)| self.subtype_of(l.typ(), r.typ()))
|
||||
&& ls.var_params.as_ref().zip(rs.var_params.as_ref()).map(|(l, r)| {
|
||||
self.subtype_of(l.typ(), r.typ())
|
||||
}).unwrap_or(true)
|
||||
&& kw_check() // contravariant
|
||||
.all(|(l, r)| self.subtype_of(l.typ(), r.typ(), allow_cast));
|
||||
let var_params_judge = ls
|
||||
.var_params
|
||||
.as_ref()
|
||||
.zip(rs.var_params.as_ref())
|
||||
.map(|(l, r)| self.subtype_of(l.typ(), r.typ(), allow_cast))
|
||||
.unwrap_or(true);
|
||||
same_params_len
|
||||
&& return_t_judge
|
||||
&& non_defaults_judge
|
||||
&& var_params_judge
|
||||
&& kw_check() // contravariant
|
||||
}
|
||||
// ?T(<: Nat) !:> ?U(:> Int)
|
||||
// ?T(<: Nat) :> ?U(<: Int) (?U can be smaller than ?T)
|
||||
(FreeVar(lfv), FreeVar(rfv)) => match (lfv.get_subsup(), rfv.get_subsup()) {
|
||||
(Some((_, l_sup)), Some((r_sub, _))) => self.supertype_of(&l_sup, &r_sub),
|
||||
(Some((_, l_sup)), Some((r_sub, _))) => {
|
||||
self.supertype_of(&l_sup, &r_sub, allow_cast)
|
||||
}
|
||||
_ => {
|
||||
if lfv.is_linked() {
|
||||
self.supertype_of(&lfv.crack(), rhs)
|
||||
self.supertype_of(&lfv.crack(), rhs, allow_cast)
|
||||
} else if rfv.is_linked() {
|
||||
self.supertype_of(lhs, &rfv.crack())
|
||||
self.supertype_of(lhs, &rfv.crack(), allow_cast)
|
||||
} else {
|
||||
false
|
||||
}
|
||||
|
@ -391,13 +439,13 @@ impl Context {
|
|||
(FreeVar(lfv), rhs) => {
|
||||
match &*lfv.borrow() {
|
||||
FreeKind::Linked(t) | FreeKind::UndoableLinked { t, .. } => {
|
||||
self.supertype_of(t, rhs)
|
||||
self.supertype_of(t, rhs, allow_cast)
|
||||
}
|
||||
FreeKind::Unbound { constraint: _, .. }
|
||||
| FreeKind::NamedUnbound { constraint: _, .. } => {
|
||||
if let Some((_sub, sup)) = lfv.get_subsup() {
|
||||
lfv.forced_undoable_link(rhs);
|
||||
let res = self.supertype_of(&sup, rhs);
|
||||
let res = self.supertype_of(&sup, rhs, allow_cast);
|
||||
lfv.undo();
|
||||
res
|
||||
} else if let Some(lfvt) = lfv.get_type() {
|
||||
|
@ -407,7 +455,7 @@ impl Context {
|
|||
// => Array(Type, 3) :> Array(Typeof(Int), 3)
|
||||
// => true
|
||||
let rhs_meta = self.meta_type(rhs);
|
||||
self.supertype_of(&lfvt, &rhs_meta)
|
||||
self.supertype_of(&lfvt, &rhs_meta, allow_cast)
|
||||
} else {
|
||||
// constraint is uninitalized
|
||||
log!(err "constraint is uninitialized: {lfv}/{rhs}");
|
||||
|
@ -418,18 +466,18 @@ impl Context {
|
|||
}
|
||||
(lhs, FreeVar(rfv)) => match &*rfv.borrow() {
|
||||
FreeKind::Linked(t) | FreeKind::UndoableLinked { t, .. } => {
|
||||
self.supertype_of(lhs, t)
|
||||
self.supertype_of(lhs, t, allow_cast)
|
||||
}
|
||||
FreeKind::Unbound { constraint: _, .. }
|
||||
| FreeKind::NamedUnbound { constraint: _, .. } => {
|
||||
if let Some((sub, _sup)) = rfv.get_subsup() {
|
||||
rfv.forced_undoable_link(lhs);
|
||||
let res = self.supertype_of(lhs, &sub);
|
||||
let res = self.supertype_of(lhs, &sub, allow_cast);
|
||||
rfv.undo();
|
||||
res
|
||||
} else if let Some(rfvt) = rfv.get_type() {
|
||||
let lhs_meta = self.meta_type(lhs);
|
||||
self.supertype_of(&lhs_meta, &rfvt)
|
||||
self.supertype_of(&lhs_meta, &rfvt, allow_cast)
|
||||
} else {
|
||||
// constraint is uninitalized
|
||||
log!(err "constraint is uninitialized: {lhs}/{rfv}");
|
||||
|
@ -440,7 +488,7 @@ impl Context {
|
|||
(Type::Record(lhs), Type::Record(rhs)) => {
|
||||
for (k, l) in lhs.iter() {
|
||||
if let Some(r) = rhs.get(k) {
|
||||
if !self.supertype_of(l, r) {
|
||||
if !self.supertype_of(l, r, allow_cast) {
|
||||
return false;
|
||||
}
|
||||
} else {
|
||||
|
@ -451,18 +499,18 @@ impl Context {
|
|||
}
|
||||
(Type, Record(rec)) => {
|
||||
for (_, t) in rec.iter() {
|
||||
if !self.supertype_of(&Type, t) {
|
||||
if !self.supertype_of(&Type, t, allow_cast) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
true
|
||||
}
|
||||
(Type, Subr(subr)) => self.supertype_of(&Type, &subr.return_t),
|
||||
(Type, Subr(subr)) => self.supertype_of(&Type, &subr.return_t, allow_cast),
|
||||
(Type, Poly { name, params }) | (Poly { name, params }, Type)
|
||||
if &name[..] == "Array" || &name[..] == "Set" =>
|
||||
{
|
||||
let elem_t = self.convert_tp_into_ty(params[0].clone()).unwrap();
|
||||
self.supertype_of(&Type, &elem_t)
|
||||
self.supertype_of(&Type, &elem_t, allow_cast)
|
||||
}
|
||||
(Type, Poly { name, params }) | (Poly { name, params }, Type)
|
||||
if &name[..] == "Tuple" =>
|
||||
|
@ -472,7 +520,7 @@ impl Context {
|
|||
let Ok(t) = self.convert_tp_into_ty(tp) else {
|
||||
return false;
|
||||
};
|
||||
if !self.supertype_of(&Type, &t) {
|
||||
if !self.supertype_of(&Type, &t, allow_cast) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
@ -493,7 +541,9 @@ impl Context {
|
|||
let Ok(v) = self.convert_tp_into_ty(v) else {
|
||||
return false;
|
||||
};
|
||||
if !self.supertype_of(&Type, &k) || !self.supertype_of(&Type, &v) {
|
||||
if !self.supertype_of(&Type, &k, allow_cast)
|
||||
|| !self.supertype_of(&Type, &v, allow_cast)
|
||||
{
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
@ -508,7 +558,7 @@ impl Context {
|
|||
// {1, 2, 3} :> {1, } == true
|
||||
(Refinement(l), Refinement(r)) => {
|
||||
// no relation or l.t <: r.t (not equal)
|
||||
if !self.supertype_of(&l.t, &r.t) {
|
||||
if !self.supertype_of(&l.t, &r.t, allow_cast) {
|
||||
return false;
|
||||
}
|
||||
let mut r_preds_clone = r.preds.clone();
|
||||
|
@ -516,7 +566,7 @@ impl Context {
|
|||
for r_pred in r.preds.iter() {
|
||||
if l_pred.subject().unwrap_or("") == &l.var[..]
|
||||
&& r_pred.subject().unwrap_or("") == &r.var[..]
|
||||
&& self.is_super_pred_of(l_pred, r_pred)
|
||||
&& self.is_super_pred_of(l_pred, r_pred, allow_cast)
|
||||
{
|
||||
r_preds_clone.remove(r_pred);
|
||||
}
|
||||
|
@ -526,11 +576,11 @@ impl Context {
|
|||
}
|
||||
(Nat, re @ Refinement(_)) => {
|
||||
let nat = Type::Refinement(Nat.into_refinement());
|
||||
self.structural_supertype_of(&nat, re)
|
||||
self.structural_supertype_of(&nat, re, allow_cast)
|
||||
}
|
||||
(re @ Refinement(_), Nat) => {
|
||||
let nat = Type::Refinement(Nat.into_refinement());
|
||||
self.structural_supertype_of(re, &nat)
|
||||
self.structural_supertype_of(re, &nat, allow_cast)
|
||||
}
|
||||
// Int :> {I: Int | ...} == true
|
||||
// Int :> {I: Str| ...} == false
|
||||
|
@ -539,15 +589,15 @@ impl Context {
|
|||
// => true
|
||||
// Bool :> {1} == true
|
||||
(l, Refinement(r)) => {
|
||||
if self.supertype_of(l, &r.t) {
|
||||
if self.supertype_of(l, &r.t, allow_cast) {
|
||||
return true;
|
||||
}
|
||||
let l = l.derefine();
|
||||
if self.supertype_of(&l, &r.t) {
|
||||
if self.supertype_of(&l, &r.t, allow_cast) {
|
||||
return true;
|
||||
}
|
||||
let l = Type::Refinement(l.into_refinement());
|
||||
self.structural_supertype_of(&l, rhs)
|
||||
self.structural_supertype_of(&l, rhs, allow_cast)
|
||||
}
|
||||
// ({I: Int | True} :> Int) == true, ({N: Nat | ...} :> Int) == false, ({I: Int | I >= 0} :> Int) == false
|
||||
(Refinement(l), r) => {
|
||||
|
@ -557,17 +607,18 @@ impl Context {
|
|||
{
|
||||
return false;
|
||||
}
|
||||
self.supertype_of(&l.t, r)
|
||||
self.supertype_of(&l.t, r, allow_cast)
|
||||
}
|
||||
(Quantified(l), Quantified(r)) => self.structural_subtype_of(l, r, allow_cast),
|
||||
(Quantified(quant), r) => {
|
||||
if quant.has_uninited_qvars() {
|
||||
let mut tmp_tv_cache = TyVarCache::new(self.level, self);
|
||||
let inst = self
|
||||
.instantiate_t_inner(*quant.clone(), &mut tmp_tv_cache, &())
|
||||
.unwrap();
|
||||
self.supertype_of(&inst, r)
|
||||
self.supertype_of(&inst, r, allow_cast)
|
||||
} else {
|
||||
self.supertype_of(quant, r)
|
||||
self.supertype_of(quant, r, allow_cast)
|
||||
}
|
||||
}
|
||||
(l, Quantified(quant)) => {
|
||||
|
@ -576,41 +627,49 @@ impl Context {
|
|||
let inst = self
|
||||
.instantiate_t_inner(*quant.clone(), &mut tmp_tv_cache, &())
|
||||
.unwrap();
|
||||
self.supertype_of(l, &inst)
|
||||
self.supertype_of(l, &inst, allow_cast)
|
||||
} else {
|
||||
self.supertype_of(l, quant)
|
||||
self.supertype_of(l, quant, allow_cast)
|
||||
}
|
||||
}
|
||||
// Int or Str :> Str or Int == (Int :> Str && Str :> Int) || (Int :> Int && Str :> Str) == true
|
||||
(Or(l_1, l_2), Or(r_1, r_2)) => {
|
||||
(self.supertype_of(l_1, r_1) && self.supertype_of(l_2, r_2))
|
||||
|| (self.supertype_of(l_1, r_2) && self.supertype_of(l_2, r_1))
|
||||
(self.supertype_of(l_1, r_1, allow_cast) && self.supertype_of(l_2, r_2, allow_cast))
|
||||
|| (self.supertype_of(l_1, r_2, allow_cast)
|
||||
&& self.supertype_of(l_2, r_1, allow_cast))
|
||||
}
|
||||
// not Nat :> not Int == true
|
||||
(Not(l), Not(r)) => self.subtype_of(l, r),
|
||||
(Not(l), Not(r)) => self.subtype_of(l, r, allow_cast),
|
||||
// (Int or Str) :> Nat == Int :> Nat || Str :> Nat == true
|
||||
// (Num or Show) :> Show == Num :> Show || Show :> Num == true
|
||||
(Or(l_or, r_or), rhs) => self.supertype_of(l_or, rhs) || self.supertype_of(r_or, rhs),
|
||||
(Or(l_or, r_or), rhs) => {
|
||||
self.supertype_of(l_or, rhs, allow_cast) || self.supertype_of(r_or, rhs, allow_cast)
|
||||
}
|
||||
// Int :> (Nat or Str) == Int :> Nat && Int :> Str == false
|
||||
(lhs, Or(l_or, r_or)) => self.supertype_of(lhs, l_or) && self.supertype_of(lhs, r_or),
|
||||
(lhs, Or(l_or, r_or)) => {
|
||||
self.supertype_of(lhs, l_or, allow_cast) && self.supertype_of(lhs, r_or, allow_cast)
|
||||
}
|
||||
(And(l_1, l_2), And(r_1, r_2)) => {
|
||||
(self.supertype_of(l_1, r_1) && self.supertype_of(l_2, r_2))
|
||||
|| (self.supertype_of(l_1, r_2) && self.supertype_of(l_2, r_1))
|
||||
(self.supertype_of(l_1, r_1, allow_cast) && self.supertype_of(l_2, r_2, allow_cast))
|
||||
|| (self.supertype_of(l_1, r_2, allow_cast)
|
||||
&& self.supertype_of(l_2, r_1, allow_cast))
|
||||
}
|
||||
// (Num and Show) :> Show == false
|
||||
(And(l_and, r_and), rhs) => {
|
||||
self.supertype_of(l_and, rhs) && self.supertype_of(r_and, rhs)
|
||||
self.supertype_of(l_and, rhs, allow_cast)
|
||||
&& self.supertype_of(r_and, rhs, allow_cast)
|
||||
}
|
||||
// Show :> (Num and Show) == true
|
||||
(lhs, And(l_and, r_and)) => {
|
||||
self.supertype_of(lhs, l_and) || self.supertype_of(lhs, r_and)
|
||||
self.supertype_of(lhs, l_and, allow_cast)
|
||||
|| self.supertype_of(lhs, r_and, allow_cast)
|
||||
}
|
||||
// RefMut are invariant
|
||||
(Ref(l), Ref(r)) => self.supertype_of(l, r),
|
||||
(Ref(l), Ref(r)) => self.supertype_of(l, r, allow_cast),
|
||||
// TはすべてのRef(T)のメソッドを持つので、Ref(T)のサブタイプ
|
||||
// REVIEW: RefMut is invariant, maybe
|
||||
(Ref(l), r) => self.supertype_of(l, r),
|
||||
(RefMut { before: l, .. }, r) => self.supertype_of(l, r),
|
||||
(Ref(l), r) => self.supertype_of(l, r, allow_cast),
|
||||
(RefMut { before: l, .. }, r) => self.supertype_of(l, r, allow_cast),
|
||||
// `Eq(Set(T, N)) :> Set(T, N)` will be false, such cases are judged by nominal_supertype_of
|
||||
(
|
||||
Poly {
|
||||
|
@ -631,7 +690,7 @@ impl Context {
|
|||
let rt = self.convert_tp_into_ty(rparams[0].clone()).unwrap();
|
||||
let llen = lparams[1].clone();
|
||||
let rlen = rparams[1].clone();
|
||||
self.supertype_of(<, &rt)
|
||||
self.supertype_of(<, &rt, allow_cast)
|
||||
&& self
|
||||
.eval_bin_tp(OpKind::Le, llen, rlen)
|
||||
.map(|tp| matches!(tp, TyParam::Value(ValueObj::Bool(true))))
|
||||
|
@ -640,13 +699,13 @@ impl Context {
|
|||
todo!();
|
||||
})
|
||||
} else {
|
||||
self.poly_supertype_of(lhs, lparams, rparams)
|
||||
self.poly_supertype_of(lhs, lparams, rparams, allow_cast)
|
||||
}
|
||||
}
|
||||
(Proj { .. }, _) => {
|
||||
if let Some(cands) = self.get_candidates(lhs) {
|
||||
for cand in cands.into_iter() {
|
||||
if self.supertype_of(&cand, rhs) {
|
||||
if self.supertype_of(&cand, rhs, allow_cast) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
@ -656,7 +715,7 @@ impl Context {
|
|||
(_, Proj { .. }) => {
|
||||
if let Some(cands) = self.get_candidates(rhs) {
|
||||
for cand in cands.into_iter() {
|
||||
if self.supertype_of(lhs, &cand) {
|
||||
if self.supertype_of(lhs, &cand, allow_cast) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
@ -672,6 +731,7 @@ impl Context {
|
|||
typ: &Type,
|
||||
lparams: &[TyParam],
|
||||
rparams: &[TyParam],
|
||||
allow_cast: bool,
|
||||
) -> bool {
|
||||
log!(
|
||||
"poly_supertype_of: {typ}, {}, {}",
|
||||
|
@ -687,19 +747,25 @@ impl Context {
|
|||
.iter()
|
||||
.zip(rparams.iter())
|
||||
.zip(variances.iter())
|
||||
.all(|((lp, rp), variance)| self.supertype_of_tp(lp, rp, *variance))
|
||||
.all(|((lp, rp), variance)| self.supertype_of_tp(lp, rp, *variance, allow_cast))
|
||||
}
|
||||
|
||||
fn supertype_of_tp(&self, lp: &TyParam, rp: &TyParam, variance: Variance) -> bool {
|
||||
fn supertype_of_tp(
|
||||
&self,
|
||||
lp: &TyParam,
|
||||
rp: &TyParam,
|
||||
variance: Variance,
|
||||
allow_cast: bool,
|
||||
) -> bool {
|
||||
if lp == rp {
|
||||
return true;
|
||||
}
|
||||
match (lp, rp, variance) {
|
||||
(TyParam::FreeVar(fv), _, _) if fv.is_linked() => {
|
||||
self.supertype_of_tp(&fv.crack(), rp, variance)
|
||||
self.supertype_of_tp(&fv.crack(), rp, variance, allow_cast)
|
||||
}
|
||||
(_, TyParam::FreeVar(fv), _) if fv.is_linked() => {
|
||||
self.supertype_of_tp(lp, &fv.crack(), variance)
|
||||
self.supertype_of_tp(lp, &fv.crack(), variance, allow_cast)
|
||||
}
|
||||
// _: Type :> T == true
|
||||
(TyParam::Erased(t), TyParam::Type(_), _)
|
||||
|
@ -711,7 +777,7 @@ impl Context {
|
|||
(TyParam::Array(lp), TyParam::Array(rp), _)
|
||||
| (TyParam::Tuple(lp), TyParam::Tuple(rp), _) => {
|
||||
for (l, r) in lp.iter().zip(rp.iter()) {
|
||||
if !self.supertype_of_tp(l, r, variance) {
|
||||
if !self.supertype_of_tp(l, r, variance, allow_cast) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
@ -724,7 +790,7 @@ impl Context {
|
|||
}
|
||||
for (k, lv) in ld.iter() {
|
||||
if let Some(rv) = rd.get(k) {
|
||||
if !self.supertype_of_tp(lv, rv, variance) {
|
||||
if !self.supertype_of_tp(lv, rv, variance, allow_cast) {
|
||||
return false;
|
||||
}
|
||||
} else {
|
||||
|
@ -733,51 +799,65 @@ impl Context {
|
|||
}
|
||||
true
|
||||
}
|
||||
(TyParam::Type(l), TyParam::Type(r), Variance::Contravariant) => self.subtype_of(l, r),
|
||||
(TyParam::Type(l), TyParam::Type(r), Variance::Contravariant) => {
|
||||
self.subtype_of(l, r, allow_cast)
|
||||
}
|
||||
(TyParam::Type(l), TyParam::Type(r), Variance::Covariant) => {
|
||||
// if matches!(r.as_ref(), &Type::Refinement(_)) { log!(info "{l}, {r}, {}", self.structural_supertype_of(l, r, bounds, Some(lhs_variance))); }
|
||||
self.supertype_of(l, r)
|
||||
self.supertype_of(l, r, allow_cast)
|
||||
}
|
||||
(TyParam::Type(l), TyParam::Type(r), Variance::Invariant) => {
|
||||
self.same_type_of(l, r, allow_cast)
|
||||
}
|
||||
(TyParam::FreeVar(fv), _, _) if fv.is_unbound() => {
|
||||
let fv_t = fv.get_type().unwrap();
|
||||
let rp_t = self.get_tp_t(rp).unwrap();
|
||||
if variance == Variance::Contravariant {
|
||||
self.subtype_of(&fv_t, &rp_t)
|
||||
self.subtype_of(&fv_t, &rp_t, allow_cast)
|
||||
} else if variance == Variance::Covariant {
|
||||
self.supertype_of(&fv_t, &rp_t)
|
||||
self.supertype_of(&fv_t, &rp_t, allow_cast)
|
||||
} else {
|
||||
self.same_type_of(&fv_t, &rp_t)
|
||||
self.same_type_of(&fv_t, &rp_t, allow_cast)
|
||||
}
|
||||
}
|
||||
// Invariant
|
||||
_ => self.eq_tp(lp, rp),
|
||||
_ => self.eq_tp(lp, rp, allow_cast),
|
||||
}
|
||||
}
|
||||
|
||||
/// lhs <: rhs?
|
||||
pub(crate) fn structural_subtype_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
self.structural_supertype_of(rhs, lhs)
|
||||
pub(crate) fn structural_subtype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
|
||||
self.structural_supertype_of(rhs, lhs, allow_cast)
|
||||
}
|
||||
|
||||
pub(crate) fn _structural_same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
self.structural_supertype_of(lhs, rhs) && self.structural_subtype_of(lhs, rhs)
|
||||
pub(crate) fn _structural_same_type_of(
|
||||
&self,
|
||||
lhs: &Type,
|
||||
rhs: &Type,
|
||||
allow_cast: bool,
|
||||
) -> bool {
|
||||
self.structural_supertype_of(lhs, rhs, allow_cast)
|
||||
&& self.structural_subtype_of(lhs, rhs, allow_cast)
|
||||
}
|
||||
|
||||
pub(crate) fn try_cmp(&self, l: &TyParam, r: &TyParam) -> Option<TyParamOrdering> {
|
||||
pub(crate) fn try_cmp(
|
||||
&self,
|
||||
l: &TyParam,
|
||||
r: &TyParam,
|
||||
allow_cast: bool,
|
||||
) -> Option<TyParamOrdering> {
|
||||
match (l, r) {
|
||||
(TyParam::Value(l), TyParam::Value(r)) =>
|
||||
l.try_cmp(r).map(Into::into),
|
||||
// TODO: 型を見て判断する
|
||||
(TyParam::BinOp{ op, lhs, rhs }, r) => {
|
||||
if let Ok(l) = self.eval_bin_tp(*op, lhs.as_ref().clone(), rhs.as_ref().clone()) {
|
||||
self.try_cmp(&l, r)
|
||||
self.try_cmp(&l, r, allow_cast)
|
||||
} else { Some(Any) }
|
||||
},
|
||||
(TyParam::FreeVar(fv), p) if fv.is_linked() => {
|
||||
self.try_cmp(&fv.crack(), p)
|
||||
self.try_cmp(&fv.crack(), p, allow_cast)
|
||||
}
|
||||
(p, TyParam::FreeVar(fv)) if fv.is_linked() => {
|
||||
self.try_cmp(p, &fv.crack())
|
||||
self.try_cmp(p, &fv.crack(), allow_cast)
|
||||
}
|
||||
(
|
||||
l @ (TyParam::FreeVar(_) | TyParam::Erased(_)),
|
||||
|
@ -785,7 +865,7 @@ impl Context {
|
|||
) /* if v.is_unbound() */ => {
|
||||
let l_t = self.get_tp_t(l).unwrap();
|
||||
let r_t = self.get_tp_t(r).unwrap();
|
||||
if self.supertype_of(&l_t, &r_t) || self.subtype_of(&l_t, &r_t) {
|
||||
if self.supertype_of(&l_t, &r_t, allow_cast) || self.subtype_of(&l_t, &r_t, allow_cast) {
|
||||
Some(Any)
|
||||
} else { Some(NotEqual) }
|
||||
},
|
||||
|
@ -805,8 +885,8 @@ impl Context {
|
|||
// (n: Int, 1) -> (-inf..inf, 1) -> (cmp(-inf, 1), cmp(inf, 1)) -> (Less, Greater) -> Any
|
||||
// (n: 5..10, 2) -> (cmp(5..10, 2), cmp(5..10, 2)) -> (Greater, Greater) -> Greater
|
||||
match (
|
||||
self.try_cmp(&inf, p).unwrap(),
|
||||
self.try_cmp(&sup, p).unwrap()
|
||||
self.try_cmp(&inf, p, allow_cast).unwrap(),
|
||||
self.try_cmp(&sup, p, allow_cast).unwrap()
|
||||
) {
|
||||
(Less, Less) => Some(Less),
|
||||
(Less, Equal) => Some(LessEqual),
|
||||
|
@ -840,7 +920,7 @@ impl Context {
|
|||
todo!("cmp({inf}, {sup}) = {l:?}, cmp({inf}, {sup}) = {r:?}"),
|
||||
}
|
||||
} else {
|
||||
match (self.supertype_of(<, &pt), self.subtype_of(<, &pt)) {
|
||||
match (self.supertype_of(<, &pt, allow_cast), self.subtype_of(<, &pt, allow_cast)) {
|
||||
(true, true) => Some(Any),
|
||||
(true, false) => Some(Any),
|
||||
(false, true) => Some(NotEqual),
|
||||
|
@ -849,7 +929,7 @@ impl Context {
|
|||
}
|
||||
}
|
||||
(l, r @ (TyParam::Erased(_) | TyParam::FreeVar(_))) =>
|
||||
self.try_cmp(r, l).map(|ord| ord.reverse()),
|
||||
self.try_cmp(r, l, allow_cast).map(|ord| ord.reverse()),
|
||||
(_l, _r) => {
|
||||
erg_common::fmt_dbg!(_l, _r,);
|
||||
None
|
||||
|
@ -859,13 +939,17 @@ impl Context {
|
|||
|
||||
/// returns union of two types (A or B)
|
||||
pub(crate) fn union(&self, lhs: &Type, rhs: &Type) -> Type {
|
||||
let allow_cast = true;
|
||||
if lhs == rhs {
|
||||
return lhs.clone();
|
||||
}
|
||||
// `?T or ?U` will not be unified
|
||||
// `Set!(?T, 3) or Set(?T, 3)` wii be unified to Set(?T, 3)
|
||||
if !lhs.is_unbound_var() && !rhs.is_unbound_var() {
|
||||
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
|
||||
match (
|
||||
self.supertype_of(lhs, rhs, allow_cast),
|
||||
self.subtype_of(lhs, rhs, allow_cast),
|
||||
) {
|
||||
(true, true) => return lhs.clone(), // lhs = rhs
|
||||
(true, false) => return lhs.clone(), // lhs :> rhs
|
||||
(false, true) => return rhs.clone(),
|
||||
|
@ -897,7 +981,7 @@ impl Context {
|
|||
unified_params.push(TyParam::t(self.union(l, r)))
|
||||
}
|
||||
(_, _) => {
|
||||
if self.eq_tp(lp, rp) {
|
||||
if self.eq_tp(lp, rp, allow_cast) {
|
||||
unified_params.push(lp.clone());
|
||||
} else {
|
||||
return or(lhs.clone(), rhs.clone());
|
||||
|
@ -926,12 +1010,16 @@ impl Context {
|
|||
|
||||
/// returns intersection of two types (A and B)
|
||||
pub(crate) fn intersection(&self, lhs: &Type, rhs: &Type) -> Type {
|
||||
let allow_cast = true;
|
||||
if lhs == rhs {
|
||||
return lhs.clone();
|
||||
}
|
||||
// ?T and ?U will not be unified
|
||||
if !lhs.is_unbound_var() && !rhs.is_unbound_var() {
|
||||
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
|
||||
match (
|
||||
self.supertype_of(lhs, rhs, allow_cast),
|
||||
self.subtype_of(lhs, rhs, allow_cast),
|
||||
) {
|
||||
(true, true) => return lhs.clone(), // lhs = rhs
|
||||
(true, false) => return rhs.clone(), // lhs :> rhs
|
||||
(false, true) => return lhs.clone(),
|
||||
|
@ -993,7 +1081,7 @@ impl Context {
|
|||
/// assert is_super_pred({T >= 0}, {I == 0})
|
||||
/// assert !is_super_pred({I < 0}, {I == 0})
|
||||
/// ```
|
||||
fn is_super_pred_of(&self, lhs: &Predicate, rhs: &Predicate) -> bool {
|
||||
fn is_super_pred_of(&self, lhs: &Predicate, rhs: &Predicate, allow_cast: bool) -> bool {
|
||||
match (lhs, rhs) {
|
||||
(Pred::LessEqual { rhs, .. }, _) if !rhs.has_upper_bound() => true,
|
||||
(Pred::GreaterEqual { rhs, .. }, _) if !rhs.has_lower_bound() => true,
|
||||
|
@ -1006,7 +1094,7 @@ impl Context {
|
|||
| (Pred::NotEqual { .. }, Pred::Equal { .. }) => false,
|
||||
(Pred::Equal { rhs, .. }, Pred::Equal { rhs: rhs2, .. })
|
||||
| (Pred::NotEqual { rhs, .. }, Pred::NotEqual { rhs: rhs2, .. }) => self
|
||||
.try_cmp(rhs, rhs2)
|
||||
.try_cmp(rhs, rhs2, allow_cast)
|
||||
.map(|ord| ord.canbe_eq())
|
||||
.unwrap_or(false),
|
||||
// {T >= 0} :> {T >= 1}, {T >= 0} :> {T == 1}
|
||||
|
@ -1014,34 +1102,47 @@ impl Context {
|
|||
Pred::GreaterEqual { rhs, .. },
|
||||
Pred::GreaterEqual { rhs: rhs2, .. } | Pred::Equal { rhs: rhs2, .. },
|
||||
) => self
|
||||
.try_cmp(rhs, rhs2)
|
||||
.try_cmp(rhs, rhs2, allow_cast)
|
||||
.map(|ord| ord.canbe_le())
|
||||
.unwrap_or(false),
|
||||
(
|
||||
Pred::LessEqual { rhs, .. },
|
||||
Pred::LessEqual { rhs: rhs2, .. } | Pred::Equal { rhs: rhs2, .. },
|
||||
) => self
|
||||
.try_cmp(rhs, rhs2)
|
||||
.try_cmp(rhs, rhs2, allow_cast)
|
||||
.map(|ord| ord.canbe_ge())
|
||||
.unwrap_or(false),
|
||||
(lhs @ (Pred::GreaterEqual { .. } | Pred::LessEqual { .. }), Pred::And(l, r)) => {
|
||||
self.is_super_pred_of(lhs, l) || self.is_super_pred_of(lhs, r)
|
||||
self.is_super_pred_of(lhs, l, allow_cast)
|
||||
|| self.is_super_pred_of(lhs, r, allow_cast)
|
||||
}
|
||||
(lhs, Pred::Or(l, r)) => {
|
||||
self.is_super_pred_of(lhs, l, allow_cast)
|
||||
&& self.is_super_pred_of(lhs, r, allow_cast)
|
||||
}
|
||||
(lhs, Pred::Or(l, r)) => self.is_super_pred_of(lhs, l) && self.is_super_pred_of(lhs, r),
|
||||
(Pred::Or(l, r), rhs @ (Pred::GreaterEqual { .. } | Pred::LessEqual { .. })) => {
|
||||
self.is_super_pred_of(l, rhs) || self.is_super_pred_of(r, rhs)
|
||||
self.is_super_pred_of(l, rhs, allow_cast)
|
||||
|| self.is_super_pred_of(r, rhs, allow_cast)
|
||||
}
|
||||
(Pred::And(l, r), rhs) => {
|
||||
self.is_super_pred_of(l, rhs) && self.is_super_pred_of(r, rhs)
|
||||
self.is_super_pred_of(l, rhs, allow_cast)
|
||||
&& self.is_super_pred_of(r, rhs, allow_cast)
|
||||
}
|
||||
(lhs, rhs) => todo!("{lhs}/{rhs}"),
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn is_sub_constraint_of(&self, l: &Constraint, r: &Constraint) -> bool {
|
||||
pub(crate) fn is_sub_constraint_of(
|
||||
&self,
|
||||
l: &Constraint,
|
||||
r: &Constraint,
|
||||
allow_cast: bool,
|
||||
) -> bool {
|
||||
match (l, r) {
|
||||
// (?I: Nat) <: (?I: Int)
|
||||
(Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => self.subtype_of(lhs, rhs),
|
||||
(Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => {
|
||||
self.subtype_of(lhs, rhs, allow_cast)
|
||||
}
|
||||
// (?T <: Int) <: (?T: Type)
|
||||
(Constraint::Sandwiched { sub: Never, .. }, Constraint::TypeOf(Type)) => true,
|
||||
// (Int <: ?T) <: (Nat <: ?U)
|
||||
|
@ -1059,7 +1160,9 @@ impl Context {
|
|||
sup: rsup,
|
||||
..
|
||||
},
|
||||
) => self.supertype_of(lsub, rsub) && self.subtype_of(lsup, rsup),
|
||||
) => {
|
||||
self.supertype_of(lsub, rsub, allow_cast) && self.subtype_of(lsup, rsup, allow_cast)
|
||||
}
|
||||
_ => false,
|
||||
}
|
||||
}
|
||||
|
@ -1081,7 +1184,7 @@ impl Context {
|
|||
if lhs == &refine.var =>
|
||||
{
|
||||
if let Some(max) = &maybe_max {
|
||||
if self.try_cmp(rhs, max) == Some(Greater) {
|
||||
if self.try_cmp(rhs, max, true) == Some(Greater) {
|
||||
maybe_max = Some(rhs.clone());
|
||||
}
|
||||
} else {
|
||||
|
@ -1109,7 +1212,7 @@ impl Context {
|
|||
if lhs == &refine.var =>
|
||||
{
|
||||
if let Some(min) = &maybe_min {
|
||||
if self.try_cmp(rhs, min) == Some(Less) {
|
||||
if self.try_cmp(rhs, min, true) == Some(Less) {
|
||||
maybe_min = Some(rhs.clone());
|
||||
}
|
||||
} else {
|
||||
|
@ -1131,7 +1234,10 @@ impl Context {
|
|||
/// 関係なければNoneを返す
|
||||
pub(crate) fn min<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
|
||||
// If they are the same, either one can be returned.
|
||||
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
|
||||
match (
|
||||
self.supertype_of(lhs, rhs, true),
|
||||
self.subtype_of(lhs, rhs, true),
|
||||
) {
|
||||
(true, true) | (true, false) => Some(rhs),
|
||||
(false, true) => Some(lhs),
|
||||
(false, false) => None,
|
||||
|
@ -1140,7 +1246,10 @@ impl Context {
|
|||
|
||||
pub(crate) fn _max<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
|
||||
// If they are the same, either one can be returned.
|
||||
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
|
||||
match (
|
||||
self.supertype_of(lhs, rhs, true),
|
||||
self.subtype_of(lhs, rhs, true),
|
||||
) {
|
||||
(true, true) | (true, false) => Some(lhs),
|
||||
(false, true) => Some(rhs),
|
||||
(false, false) => None,
|
||||
|
|
|
@ -724,6 +724,7 @@ impl Context {
|
|||
lhs: TyParam,
|
||||
rhs: TyParam,
|
||||
) -> EvalResult<TyParam> {
|
||||
let allow_cast = true;
|
||||
match (lhs, rhs) {
|
||||
(TyParam::Value(ValueObj::Mut(lhs)), TyParam::Value(rhs)) => self
|
||||
.eval_bin(op, lhs.borrow().clone(), rhs)
|
||||
|
@ -738,7 +739,8 @@ impl Context {
|
|||
// _: Nat <= 10 => true
|
||||
// TODO: maybe this is wrong, we should do the type-checking of `<=`
|
||||
(TyParam::Erased(t), rhs)
|
||||
if op.is_comparison() && self.supertype_of(&t, &self.get_tp_t(&rhs).unwrap()) =>
|
||||
if op.is_comparison()
|
||||
&& self.supertype_of(&t, &self.get_tp_t(&rhs).unwrap(), allow_cast) =>
|
||||
{
|
||||
Ok(TyParam::value(true))
|
||||
}
|
||||
|
@ -748,7 +750,8 @@ impl Context {
|
|||
(_, TyParam::FreeVar(_)) if op.is_comparison() => Ok(TyParam::value(true)),
|
||||
// 10 <= _: Nat => true
|
||||
(lhs, TyParam::Erased(t))
|
||||
if op.is_comparison() && self.supertype_of(&self.get_tp_t(&lhs).unwrap(), &t) =>
|
||||
if op.is_comparison()
|
||||
&& self.supertype_of(&self.get_tp_t(&lhs).unwrap(), &t, allow_cast) =>
|
||||
{
|
||||
Ok(TyParam::value(true))
|
||||
}
|
||||
|
@ -952,6 +955,7 @@ impl Context {
|
|||
level: usize,
|
||||
t_loc: &impl Locational,
|
||||
) -> EvalResult<Type> {
|
||||
let allow_cast = true;
|
||||
// Currently Erg does not allow projection-types to be evaluated with type variables included.
|
||||
// All type variables will be dereferenced or fail.
|
||||
let (sub, opt_sup) = match lhs.clone() {
|
||||
|
@ -993,12 +997,12 @@ impl Context {
|
|||
for (class, methods) in ty_ctx.methods_list.iter() {
|
||||
match (&class, &opt_sup) {
|
||||
(ClassDefType::ImplTrait { impl_trait, .. }, Some(sup)) => {
|
||||
if !self.supertype_of(impl_trait, sup) {
|
||||
if !self.supertype_of(impl_trait, sup, allow_cast) {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
(ClassDefType::ImplTrait { impl_trait, .. }, None) => {
|
||||
if !self.supertype_of(impl_trait, &sub) {
|
||||
if !self.supertype_of(impl_trait, &sub, allow_cast) {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
|
@ -1121,6 +1125,7 @@ impl Context {
|
|||
level: usize,
|
||||
t_loc: &impl Locational,
|
||||
) -> Option<Type> {
|
||||
let allow_cast = true;
|
||||
// e.g. sub: Int, opt_sup: Add(?T), rhs: Output, methods: Int.methods
|
||||
// sub: [Int; 4], opt_sup: Add([Int; 2]), rhs: Output, methods: [T; N].methods
|
||||
if let Ok(obj) = methods.get_const_local(&Token::symbol(rhs), &self.name) {
|
||||
|
@ -1129,7 +1134,7 @@ impl Context {
|
|||
// opt_sup: Add([Int; 2]), methods.impl_of(): Add([T; M])
|
||||
match (&opt_sup, methods.impl_of()) {
|
||||
(Some(sup), Some(trait_)) => {
|
||||
if !self.supertype_of(&trait_, sup) {
|
||||
if !self.supertype_of(&trait_, sup, allow_cast) {
|
||||
return None;
|
||||
}
|
||||
}
|
||||
|
@ -1522,13 +1527,14 @@ impl Context {
|
|||
/// NOTE: If l and r are types, the Context is used to determine the type.
|
||||
/// NOTE: lとrが型の場合はContextの方で判定する
|
||||
pub(crate) fn shallow_eq_tp(&self, lhs: &TyParam, rhs: &TyParam) -> bool {
|
||||
let allow_cast = true;
|
||||
match (lhs, rhs) {
|
||||
(TyParam::Type(l), _) if l.is_unbound_var() => {
|
||||
self.subtype_of(&self.get_tp_t(rhs).unwrap(), &Type::Type)
|
||||
self.subtype_of(&self.get_tp_t(rhs).unwrap(), &Type::Type, allow_cast)
|
||||
}
|
||||
(_, TyParam::Type(r)) if r.is_unbound_var() => {
|
||||
let lhs = self.get_tp_t(lhs).unwrap();
|
||||
self.subtype_of(&lhs, &Type::Type)
|
||||
self.subtype_of(&lhs, &Type::Type, allow_cast)
|
||||
}
|
||||
(TyParam::Type(l), TyParam::Type(r)) => l == r,
|
||||
(TyParam::Value(l), TyParam::Value(r)) => l == r,
|
||||
|
|
|
@ -456,11 +456,12 @@ impl Context {
|
|||
qnames: &Set<Str>,
|
||||
loc: &impl Locational,
|
||||
) -> TyCheckResult<Type> {
|
||||
let allow_cast = true;
|
||||
if self.is_trait(&super_t) {
|
||||
self.check_trait_impl(&sub_t, &super_t, &set! {}, loc)?;
|
||||
}
|
||||
// REVIEW: Even if type constraints can be satisfied, implementation may not exist
|
||||
if self.subtype_of(&sub_t, &super_t) {
|
||||
if self.subtype_of(&sub_t, &super_t, allow_cast) {
|
||||
let sub_t = if cfg!(feature = "debug") {
|
||||
sub_t
|
||||
} else {
|
||||
|
@ -476,7 +477,7 @@ impl Context {
|
|||
Variance::Contravariant => Ok(super_t),
|
||||
Variance::Invariant => {
|
||||
// need to check if sub_t == super_t
|
||||
if self.supertype_of(&sub_t, &super_t) {
|
||||
if self.supertype_of(&sub_t, &super_t, allow_cast) {
|
||||
Ok(sub_t)
|
||||
} else {
|
||||
Err(TyCheckErrors::from(TyCheckError::subtyping_error(
|
||||
|
@ -754,8 +755,9 @@ impl Context {
|
|||
}
|
||||
|
||||
pub(crate) fn trait_impl_exists(&self, class: &Type, trait_: &Type) -> bool {
|
||||
let allow_cast = true;
|
||||
// `Never` implements any trait
|
||||
if self.subtype_of(class, &Type::Never) {
|
||||
if self.subtype_of(class, &Type::Never, allow_cast) {
|
||||
return true;
|
||||
}
|
||||
if class.is_monomorphic() {
|
||||
|
@ -766,10 +768,11 @@ impl Context {
|
|||
}
|
||||
|
||||
fn mono_class_trait_impl_exist(&self, class: &Type, trait_: &Type) -> bool {
|
||||
let allow_cast = true;
|
||||
let mut super_exists = false;
|
||||
for inst in self.get_trait_impls(trait_).into_iter() {
|
||||
if self.supertype_of(&inst.sub_type, class)
|
||||
&& self.supertype_of(&inst.sup_trait, trait_)
|
||||
if self.supertype_of(&inst.sub_type, class, allow_cast)
|
||||
&& self.supertype_of(&inst.sup_trait, trait_, allow_cast)
|
||||
{
|
||||
super_exists = true;
|
||||
break;
|
||||
|
@ -779,10 +782,11 @@ impl Context {
|
|||
}
|
||||
|
||||
fn poly_class_trait_impl_exists(&self, class: &Type, trait_: &Type) -> bool {
|
||||
let allow_cast = true;
|
||||
let mut super_exists = false;
|
||||
for inst in self.get_trait_impls(trait_).into_iter() {
|
||||
if self.supertype_of(&inst.sub_type, class)
|
||||
&& self.supertype_of(&inst.sup_trait, trait_)
|
||||
if self.supertype_of(&inst.sub_type, class, allow_cast)
|
||||
&& self.supertype_of(&inst.sup_trait, trait_, allow_cast)
|
||||
{
|
||||
super_exists = true;
|
||||
break;
|
||||
|
@ -1030,18 +1034,14 @@ impl Context {
|
|||
Ok(())
|
||||
}
|
||||
hir::Expr::Def(def) => {
|
||||
*def.sig.ref_mut_t() = self.deref_tyvar(
|
||||
mem::take(def.sig.ref_mut_t()),
|
||||
Covariant,
|
||||
&set! {},
|
||||
&def.sig,
|
||||
)?;
|
||||
let qnames = if let Type::Quantified(quant) = def.sig.ref_t() {
|
||||
let Ok(subr) = <&SubrType>::try_from(quant.as_ref()) else { unreachable!() };
|
||||
subr.essential_qnames()
|
||||
} else {
|
||||
set! {}
|
||||
};
|
||||
*def.sig.ref_mut_t() =
|
||||
self.deref_tyvar(mem::take(def.sig.ref_mut_t()), Covariant, &qnames, &def.sig)?;
|
||||
if let Some(params) = def.sig.params_mut() {
|
||||
self.resolve_params_t(params, &qnames)?;
|
||||
}
|
||||
|
@ -1051,14 +1051,14 @@ impl Context {
|
|||
Ok(())
|
||||
}
|
||||
hir::Expr::Lambda(lambda) => {
|
||||
lambda.t =
|
||||
self.deref_tyvar(mem::take(&mut lambda.t), Covariant, &set! {}, lambda)?;
|
||||
let qnames = if let Type::Quantified(quant) = lambda.ref_t() {
|
||||
let Ok(subr) = <&SubrType>::try_from(quant.as_ref()) else { unreachable!() };
|
||||
subr.essential_qnames()
|
||||
} else {
|
||||
set! {}
|
||||
};
|
||||
lambda.t =
|
||||
self.deref_tyvar(mem::take(&mut lambda.t), Covariant, &qnames, lambda)?;
|
||||
self.resolve_params_t(&mut lambda.params, &qnames)?;
|
||||
for chunk in lambda.body.iter_mut() {
|
||||
self.resolve_expr_t(chunk)?;
|
||||
|
|
|
@ -235,6 +235,7 @@ pub fn __array_getitem__(mut args: ValueArgs, ctx: &Context) -> EvalValueResult<
|
|||
}
|
||||
|
||||
pub fn __dict_getitem__(mut args: ValueArgs, ctx: &Context) -> EvalValueResult<ValueObj> {
|
||||
let allow_cast = true;
|
||||
let slf = args.remove_left_or_key("Self").unwrap();
|
||||
let slf = enum_unwrap!(slf, ValueObj::Dict);
|
||||
let index = args.remove_left_or_key("Index").unwrap();
|
||||
|
@ -242,7 +243,7 @@ pub fn __dict_getitem__(mut args: ValueArgs, ctx: &Context) -> EvalValueResult<V
|
|||
for (k, v) in slf.iter() {
|
||||
match (&index, k) {
|
||||
(ValueObj::Type(idx), ValueObj::Type(kt)) => {
|
||||
if ctx.subtype_of(idx.typ(), kt.typ()) {
|
||||
if ctx.subtype_of(idx.typ(), kt.typ(), allow_cast) {
|
||||
return Some(v);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -476,7 +476,8 @@ impl Context {
|
|||
return Err(e);
|
||||
}
|
||||
}
|
||||
for patch in self.find_patches_of(obj.ref_t()) {
|
||||
let allow_cast = true;
|
||||
for patch in self.find_patches_of(obj.ref_t(), allow_cast) {
|
||||
if let Some(vi) = patch
|
||||
.locals
|
||||
.get(ident.inspect())
|
||||
|
@ -835,7 +836,8 @@ impl Context {
|
|||
}
|
||||
_ => {}
|
||||
}
|
||||
for patch in self.find_patches_of(obj.ref_t()) {
|
||||
let allow_cast = true;
|
||||
for patch in self.find_patches_of(obj.ref_t(), allow_cast) {
|
||||
if let Some(vi) = patch
|
||||
.locals
|
||||
.get(attr_name.inspect())
|
||||
|
@ -1061,7 +1063,8 @@ impl Context {
|
|||
}
|
||||
Type::FreeVar(fv) => {
|
||||
if let Some(sub) = fv.get_sub() {
|
||||
if !self.subtype_of(&sub, &mono("GenericCallable")) {
|
||||
let allow_cast = true;
|
||||
if !self.subtype_of(&sub, &mono("GenericCallable"), allow_cast) {
|
||||
return Err(self.not_callable_error(obj, attr_name, instance, None));
|
||||
}
|
||||
if sub != Never {
|
||||
|
@ -1748,11 +1751,15 @@ impl Context {
|
|||
/// => [Never, Nat, Int, Str!, Str, Module, Obj]
|
||||
/// ```
|
||||
pub fn sort_types<'a>(&self, types: impl Iterator<Item = &'a Type>) -> Vec<&'a Type> {
|
||||
let allow_cast = true;
|
||||
let mut buffers: Vec<Vec<&Type>> = vec![];
|
||||
for t in types {
|
||||
let mut found = false;
|
||||
for buf in buffers.iter_mut() {
|
||||
if buf.iter().all(|buf_inner| self.related(buf_inner, t)) {
|
||||
if buf
|
||||
.iter()
|
||||
.all(|buf_inner| self.related(buf_inner, t, allow_cast))
|
||||
{
|
||||
found = true;
|
||||
buf.push(t);
|
||||
break;
|
||||
|
@ -1773,7 +1780,7 @@ impl Context {
|
|||
if let Some(pos) = concatenated
|
||||
.iter()
|
||||
.take(len - idx - 1)
|
||||
.rposition(|t| self.supertype_of(maybe_sup, t))
|
||||
.rposition(|t| self.supertype_of(maybe_sup, t, allow_cast))
|
||||
{
|
||||
let sup = concatenated.remove(idx);
|
||||
concatenated.insert(pos, sup); // not `pos + 1` because the element was removed at idx
|
||||
|
@ -1864,6 +1871,7 @@ impl Context {
|
|||
&'a self,
|
||||
typ: &Type,
|
||||
) -> Option<(&'a Type, &'a Context)> {
|
||||
let allow_cast = true;
|
||||
match typ {
|
||||
Type::FreeVar(fv) if fv.is_linked() => {
|
||||
if let Some(res) = self.get_nominal_type_ctx(&fv.crack()) {
|
||||
|
@ -1952,7 +1960,11 @@ impl Context {
|
|||
}
|
||||
}
|
||||
}
|
||||
Type::Record(rec) if rec.values().all(|attr| self.supertype_of(&Type, attr)) => {
|
||||
Type::Record(rec)
|
||||
if rec
|
||||
.values()
|
||||
.all(|attr| self.supertype_of(&Type, attr, allow_cast)) =>
|
||||
{
|
||||
return self
|
||||
.get_builtins()
|
||||
.unwrap_or(self)
|
||||
|
@ -2389,13 +2401,14 @@ impl Context {
|
|||
}
|
||||
|
||||
fn get_proj_candidates(&self, lhs: &Type, rhs: &Str) -> Set<Type> {
|
||||
let allow_cast = true;
|
||||
#[allow(clippy::single_match)]
|
||||
match lhs {
|
||||
Type::FreeVar(fv) => {
|
||||
if let Some(sup) = fv.get_super() {
|
||||
let insts = self.get_trait_impls(&sup);
|
||||
let candidates = insts.into_iter().filter_map(move |inst| {
|
||||
if self.supertype_of(&inst.sup_trait, &sup) {
|
||||
if self.supertype_of(&inst.sup_trait, &sup, allow_cast) {
|
||||
self.eval_t_params(proj(inst.sub_type, rhs), self.level, &())
|
||||
.ok()
|
||||
} else {
|
||||
|
|
|
@ -1005,7 +1005,8 @@ impl Context {
|
|||
let l = self.eval_tp(l)?;
|
||||
let r = self.instantiate_const_expr(rhs, None, tmp_tv_cache)?;
|
||||
let r = self.eval_tp(r)?;
|
||||
if let Some(Greater) = self.try_cmp(&l, &r) {
|
||||
let allow_cast = true;
|
||||
if let Some(Greater) = self.try_cmp(&l, &r, allow_cast) {
|
||||
panic!("{l}..{r} is not a valid interval type (should be lhs <= rhs)")
|
||||
}
|
||||
Ok(int_interval(op, l, r))
|
||||
|
|
|
@ -678,7 +678,8 @@ impl Context {
|
|||
sub_t.lift();
|
||||
let found_t = self.generalize_t(sub_t);
|
||||
let py_name = if let Some(vi) = self.decls.remove(name) {
|
||||
if !self.supertype_of(&vi.t, &found_t) {
|
||||
let allow_cast = true;
|
||||
if !self.supertype_of(&vi.t, &found_t, allow_cast) {
|
||||
let err = TyCheckError::violate_decl_error(
|
||||
self.cfg.input.clone(),
|
||||
line!() as usize,
|
||||
|
@ -1800,9 +1801,10 @@ impl Context {
|
|||
false,
|
||||
)?;
|
||||
let Some(hir::Expr::BinOp(hir::BinOp { lhs, .. })) = call.args.get_mut_left_or_key("pred") else { todo!("{}", call.args) };
|
||||
let allow_cast = true;
|
||||
match (
|
||||
self.supertype_of(lhs.ref_t(), &cast_to),
|
||||
self.subtype_of(lhs.ref_t(), &cast_to),
|
||||
self.supertype_of(lhs.ref_t(), &cast_to, allow_cast),
|
||||
self.subtype_of(lhs.ref_t(), &cast_to, allow_cast),
|
||||
) {
|
||||
// assert 1 in {1}
|
||||
(true, true) => Ok(()),
|
||||
|
|
|
@ -17,7 +17,7 @@ impl Context {
|
|||
panic!("variable not found: {varname}");
|
||||
};
|
||||
println!("{varname}: {}", vi.t);
|
||||
if self.subtype_of(&vi.t, ty) && self.subtype_of(ty, &vi.t) {
|
||||
if self.same_type_of(&vi.t, ty, false) {
|
||||
Ok(())
|
||||
} else {
|
||||
println!("{varname} is not the type of {ty}");
|
||||
|
@ -34,7 +34,7 @@ impl Context {
|
|||
Type::Int,
|
||||
set! { Predicate::eq(var, TyParam::value(1)) },
|
||||
);
|
||||
if self.supertype_of(&lhs, &rhs) {
|
||||
if self.supertype_of(&lhs, &rhs, false) {
|
||||
Ok(())
|
||||
} else {
|
||||
Err(())
|
||||
|
@ -47,7 +47,7 @@ impl Context {
|
|||
let maybe_trait = poly(name, params);
|
||||
let mut min = Type::Obj;
|
||||
for pair in self.get_trait_impls(&maybe_trait) {
|
||||
if self.supertype_of(&pair.sup_trait, &maybe_trait) {
|
||||
if self.supertype_of(&pair.sup_trait, &maybe_trait, false) {
|
||||
min = self.min(&min, &pair.sub_type).unwrap_or(&min).clone();
|
||||
}
|
||||
}
|
||||
|
|
|
@ -138,6 +138,7 @@ impl Context {
|
|||
loc: &impl Locational,
|
||||
allow_divergence: bool,
|
||||
) -> TyCheckResult<()> {
|
||||
let allow_cast = true;
|
||||
if maybe_sub.has_no_unbound_var()
|
||||
&& maybe_sup.has_no_unbound_var()
|
||||
&& maybe_sub == maybe_sup
|
||||
|
@ -169,12 +170,15 @@ impl Context {
|
|||
} // &fv is dropped
|
||||
let fv_t = lfv.constraint().unwrap().get_type().unwrap().clone(); // lfvを参照しないよいにcloneする(あとでborrow_mutするため)
|
||||
let tp_t = self.get_tp_t(tp)?;
|
||||
if self.supertype_of(&fv_t, &tp_t) {
|
||||
if self.supertype_of(&fv_t, &tp_t, allow_cast) {
|
||||
// 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
|
||||
if lfv.level() < Some(self.level) {
|
||||
let new_constraint = Constraint::new_subtype_of(tp_t);
|
||||
if self.is_sub_constraint_of(&lfv.constraint().unwrap(), &new_constraint)
|
||||
|| lfv.constraint().unwrap().get_type() == Some(&Type)
|
||||
if self.is_sub_constraint_of(
|
||||
&lfv.constraint().unwrap(),
|
||||
&new_constraint,
|
||||
allow_cast,
|
||||
) || lfv.constraint().unwrap().get_type() == Some(&Type)
|
||||
{
|
||||
lfv.update_constraint(new_constraint, false);
|
||||
}
|
||||
|
@ -183,9 +187,9 @@ impl Context {
|
|||
}
|
||||
Ok(())
|
||||
} else if allow_divergence
|
||||
&& (self.eq_tp(tp, &TyParam::value(Inf))
|
||||
|| self.eq_tp(tp, &TyParam::value(NegInf)))
|
||||
&& self.subtype_of(&fv_t, &mono("Num"))
|
||||
&& (self.eq_tp(tp, &TyParam::value(Inf), allow_cast)
|
||||
|| self.eq_tp(tp, &TyParam::value(NegInf), allow_cast))
|
||||
&& self.subtype_of(&fv_t, &mono("Num"), allow_cast)
|
||||
{
|
||||
lfv.link(tp);
|
||||
Ok(())
|
||||
|
@ -206,12 +210,15 @@ impl Context {
|
|||
} // &fv is dropped
|
||||
let fv_t = rfv.constraint().unwrap().get_type().unwrap().clone(); // fvを参照しないよいにcloneする(あとでborrow_mutするため)
|
||||
let tp_t = self.get_tp_t(tp)?;
|
||||
if self.supertype_of(&fv_t, &tp_t) {
|
||||
if self.supertype_of(&fv_t, &tp_t, allow_cast) {
|
||||
// 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
|
||||
if rfv.level() < Some(self.level) {
|
||||
let new_constraint = Constraint::new_subtype_of(tp_t);
|
||||
if self.is_sub_constraint_of(&rfv.constraint().unwrap(), &new_constraint)
|
||||
|| rfv.constraint().unwrap().get_type() == Some(&Type)
|
||||
if self.is_sub_constraint_of(
|
||||
&rfv.constraint().unwrap(),
|
||||
&new_constraint,
|
||||
allow_cast,
|
||||
) || rfv.constraint().unwrap().get_type() == Some(&Type)
|
||||
{
|
||||
rfv.update_constraint(new_constraint, false);
|
||||
}
|
||||
|
@ -220,9 +227,9 @@ impl Context {
|
|||
}
|
||||
Ok(())
|
||||
} else if allow_divergence
|
||||
&& (self.eq_tp(tp, &TyParam::value(Inf))
|
||||
|| self.eq_tp(tp, &TyParam::value(NegInf)))
|
||||
&& self.subtype_of(&fv_t, &mono("Num"))
|
||||
&& (self.eq_tp(tp, &TyParam::value(Inf), allow_cast)
|
||||
|| self.eq_tp(tp, &TyParam::value(NegInf), allow_cast))
|
||||
&& self.subtype_of(&fv_t, &mono("Num"), allow_cast)
|
||||
{
|
||||
rfv.link(tp);
|
||||
Ok(())
|
||||
|
@ -252,7 +259,7 @@ impl Context {
|
|||
}
|
||||
(l, TyParam::Erased(t)) => {
|
||||
let sub_t = self.get_tp_t(l)?;
|
||||
if self.subtype_of(&sub_t, t) {
|
||||
if self.subtype_of(&sub_t, t, allow_cast) {
|
||||
Ok(())
|
||||
} else {
|
||||
Err(TyCheckErrors::from(TyCheckError::subtyping_error(
|
||||
|
@ -310,6 +317,7 @@ impl Context {
|
|||
after: &TyParam,
|
||||
loc: &impl Locational,
|
||||
) -> SingleTyCheckResult<()> {
|
||||
let allow_cast = true;
|
||||
match (before, after) {
|
||||
(TyParam::Value(ValueObj::Mut(l)), TyParam::Value(ValueObj::Mut(r))) => {
|
||||
*l.borrow_mut() = r.borrow().clone();
|
||||
|
@ -336,7 +344,7 @@ impl Context {
|
|||
self.reunify_tp(lhs, lhs2, loc)?;
|
||||
self.reunify_tp(rhs, rhs2, loc)
|
||||
}
|
||||
(l, r) if self.eq_tp(l, r) => Ok(()),
|
||||
(l, r) if self.eq_tp(l, r, allow_cast) => Ok(()),
|
||||
(l, r) => panic!("type-parameter re-unification failed:\nl: {l}\nr: {r}"),
|
||||
}
|
||||
}
|
||||
|
@ -439,6 +447,7 @@ impl Context {
|
|||
after_t: &Type,
|
||||
loc: &impl Locational,
|
||||
) -> SingleTyCheckResult<()> {
|
||||
let allow_cast = true;
|
||||
match (before_t, after_t) {
|
||||
(Type::FreeVar(fv), r) if fv.is_linked() => self.reunify(&fv.crack(), r, loc),
|
||||
(l, Type::FreeVar(fv)) if fv.is_linked() => self.reunify(l, &fv.crack(), loc),
|
||||
|
@ -494,7 +503,7 @@ impl Context {
|
|||
}
|
||||
Ok(())
|
||||
}
|
||||
(l, r) if self.same_type_of(l, r) => Ok(()),
|
||||
(l, r) if self.same_type_of(l, r, allow_cast) => Ok(()),
|
||||
(l, r) => Err(TyCheckError::re_unification_error(
|
||||
self.cfg.input.clone(),
|
||||
line!() as usize,
|
||||
|
@ -526,6 +535,7 @@ impl Context {
|
|||
param_name: Option<&Str>,
|
||||
) -> TyCheckResult<()> {
|
||||
log!(info "trying sub_unify:\nmaybe_sub: {maybe_sub}\nmaybe_sup: {maybe_sup}");
|
||||
let allow_cast = true;
|
||||
// In this case, there is no new information to be gained
|
||||
// この場合、特に新しく得られる情報はない
|
||||
if maybe_sub == &Type::Never || maybe_sup == &Type::Obj || maybe_sup == maybe_sub {
|
||||
|
@ -536,7 +546,7 @@ impl Context {
|
|||
return Ok(());
|
||||
}
|
||||
self.occur(maybe_sub, maybe_sup, loc)?;
|
||||
let maybe_sub_is_sub = self.subtype_of(maybe_sub, maybe_sup);
|
||||
let maybe_sub_is_sub = self.subtype_of(maybe_sub, maybe_sup, allow_cast);
|
||||
if !maybe_sub_is_sub {
|
||||
log!(err "{maybe_sub} !<: {maybe_sup}");
|
||||
return Err(TyCheckErrors::from(TyCheckError::type_mismatch_error(
|
||||
|
@ -647,7 +657,7 @@ impl Context {
|
|||
}
|
||||
// sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)
|
||||
Constraint::TypeOf(ty) => {
|
||||
if self.supertype_of(&Type, ty) {
|
||||
if self.supertype_of(&Type, ty, allow_cast) {
|
||||
*constraint = Constraint::new_supertype_of(maybe_sub.clone());
|
||||
} else {
|
||||
todo!()
|
||||
|
@ -687,7 +697,7 @@ impl Context {
|
|||
}
|
||||
// sub_unify(?T(: Type), Int): (?T(<: Int))
|
||||
Constraint::TypeOf(ty) => {
|
||||
if self.supertype_of(&Type, ty) {
|
||||
if self.supertype_of(&Type, ty, allow_cast) {
|
||||
*constraint = Constraint::new_subtype_of(maybe_sup.clone());
|
||||
} else {
|
||||
todo!()
|
||||
|
@ -867,7 +877,7 @@ impl Context {
|
|||
// TODO: Judgment for any number of preds
|
||||
(Refinement(sub), Refinement(sup)) => {
|
||||
// {I: Int or Str | I == 0} <: {I: Int}
|
||||
if self.subtype_of(&sub.t, &sup.t) {
|
||||
if self.subtype_of(&sub.t, &sup.t, allow_cast) {
|
||||
self.sub_unify(&sub.t, &sup.t, loc, param_name)?;
|
||||
}
|
||||
if sup.preds.is_empty() {
|
||||
|
@ -915,6 +925,7 @@ impl Context {
|
|||
sup_params: &[TyParam],
|
||||
loc: &impl Locational,
|
||||
) -> TyCheckResult<()> {
|
||||
let allow_cast = true;
|
||||
if let Some((sub_def_t, sub_ctx)) = self.get_nominal_type_ctx(maybe_sub) {
|
||||
let mut tv_cache = TyVarCache::new(self.level, self);
|
||||
let _sub_def_instance =
|
||||
|
@ -931,7 +942,7 @@ impl Context {
|
|||
for sup_trait in sub_ctx.super_traits.iter() {
|
||||
let sub_trait_instance =
|
||||
self.instantiate_t_inner(sup_trait.clone(), &mut tv_cache, loc)?;
|
||||
if self.supertype_of(maybe_sup, sup_trait) {
|
||||
if self.supertype_of(maybe_sup, sup_trait, allow_cast) {
|
||||
for (l_maybe_sub, r_maybe_sup) in
|
||||
sub_trait_instance.typarams().iter().zip(sup_params.iter())
|
||||
{
|
||||
|
|
|
@ -246,6 +246,7 @@ impl ASTLowerer {
|
|||
|
||||
fn lower_normal_array(&mut self, array: ast::NormalArray) -> LowerResult<hir::NormalArray> {
|
||||
log!(info "entered {}({array})", fn_name!());
|
||||
let allow_cast = true;
|
||||
let mut new_array = vec![];
|
||||
let (elems, _) = array.elems.into_iters();
|
||||
let mut union = Type::Never;
|
||||
|
@ -258,11 +259,11 @@ impl ASTLowerer {
|
|||
(false, false) => {
|
||||
if let hir::Expr::TypeAsc(type_asc) = &elem {
|
||||
// e.g. [1, "a": Str or NoneType]
|
||||
if !self
|
||||
.module
|
||||
.context
|
||||
.supertype_of(&type_asc.spec.spec_t, &union)
|
||||
{
|
||||
if !self.module.context.supertype_of(
|
||||
&type_asc.spec.spec_t,
|
||||
&union,
|
||||
allow_cast,
|
||||
) {
|
||||
return Err(self.elem_err(&l, &r, &elem));
|
||||
} // else(OK): e.g. [1, "a": Str or Int]
|
||||
} else {
|
||||
|
@ -483,6 +484,7 @@ impl ASTLowerer {
|
|||
}
|
||||
|
||||
fn gen_set_with_length_type(&mut self, elem: &hir::Expr, len: &ast::Expr) -> Type {
|
||||
let allow_cast = true;
|
||||
let maybe_len = self.module.context.eval_const_expr(len);
|
||||
match maybe_len {
|
||||
Ok(v @ ValueObj::Nat(_)) => {
|
||||
|
@ -491,7 +493,11 @@ impl ASTLowerer {
|
|||
"SetWithMutType!",
|
||||
vec![TyParam::t(elem.t()), TyParam::Value(v)],
|
||||
)
|
||||
} else if self.module.context.subtype_of(&elem.t(), &Type::Type) {
|
||||
} else if self
|
||||
.module
|
||||
.context
|
||||
.subtype_of(&elem.t(), &Type::Type, allow_cast)
|
||||
{
|
||||
poly("SetType", vec![TyParam::t(elem.t()), TyParam::Value(v)])
|
||||
} else {
|
||||
set_t(elem.t(), TyParam::Value(v))
|
||||
|
@ -1029,8 +1035,13 @@ impl ASTLowerer {
|
|||
}
|
||||
errs
|
||||
})?;
|
||||
let allow_cast = true;
|
||||
// suppress warns of lambda types, e.g. `(x: Int, y: Int) -> Int`
|
||||
if self.module.context.subtype_of(body.ref_t(), &Type::Type) {
|
||||
if self
|
||||
.module
|
||||
.context
|
||||
.subtype_of(body.ref_t(), &Type::Type, allow_cast)
|
||||
{
|
||||
for param in params.non_defaults.iter() {
|
||||
self.inc_ref(¶m.vi, param);
|
||||
}
|
||||
|
@ -1733,6 +1744,7 @@ impl ASTLowerer {
|
|||
impl_trait: Option<(Type, &TypeSpecWithOp)>,
|
||||
class: &Type,
|
||||
) -> SingleLowerResult<()> {
|
||||
let allow_cast = true;
|
||||
if let Some((impl_trait, t_spec)) = impl_trait {
|
||||
let mut unverified_names = self.module.context.locals.keys().collect::<Set<_>>();
|
||||
if let Some(trait_obj) = self
|
||||
|
@ -1755,11 +1767,11 @@ impl ASTLowerer {
|
|||
decl_t.clone().replace(&impl_trait, class);
|
||||
unverified_names.remove(name);
|
||||
// def_t must be subtype of decl_t
|
||||
if !self
|
||||
.module
|
||||
.context
|
||||
.supertype_of(&replaced_decl_t, def_t)
|
||||
{
|
||||
if !self.module.context.supertype_of(
|
||||
&replaced_decl_t,
|
||||
def_t,
|
||||
allow_cast,
|
||||
) {
|
||||
self.errs.push(LowerError::trait_member_type_error(
|
||||
self.cfg.input.clone(),
|
||||
line!() as usize,
|
||||
|
@ -1804,7 +1816,11 @@ impl ASTLowerer {
|
|||
let replaced_decl_t =
|
||||
decl_vi.t.clone().replace(&impl_trait, class);
|
||||
unverified_names.remove(name);
|
||||
if !self.module.context.supertype_of(&replaced_decl_t, def_t) {
|
||||
if !self.module.context.supertype_of(
|
||||
&replaced_decl_t,
|
||||
def_t,
|
||||
allow_cast,
|
||||
) {
|
||||
self.errs.push(LowerError::trait_member_type_error(
|
||||
self.cfg.input.clone(),
|
||||
line!() as usize,
|
||||
|
|
|
@ -2,6 +2,8 @@ id x = x
|
|||
|
||||
if__ cond, then, else = if cond, then, else
|
||||
|
||||
for__! i, proc! = for! i, proc!
|
||||
|
||||
add x, y = x + y
|
||||
|
||||
abs_ x = x.abs()
|
||||
|
|
|
@ -7,7 +7,7 @@ use erg_compiler::error::CompileErrors;
|
|||
use erg_compiler::lower::ASTLowerer;
|
||||
|
||||
use erg_compiler::ty::constructors::{
|
||||
func0, func1, func2, kw, mono, nd_func, or, poly, subtype_q, ty_tp, type_q,
|
||||
func0, func1, func2, kw, mono, nd_func, nd_proc, or, poly, proc1, subtype_q, ty_tp, type_q,
|
||||
};
|
||||
use erg_compiler::ty::Type::*;
|
||||
|
||||
|
@ -39,6 +39,16 @@ fn test_infer_types() -> Result<(), ()> {
|
|||
)
|
||||
.quantify();
|
||||
module.context.assert_var_type("if__", &if_t)?;
|
||||
let for_t = nd_proc(
|
||||
vec![
|
||||
kw("i", poly("Iterable", vec![ty_tp(t.clone())])),
|
||||
kw("proc!", proc1(t.clone(), NoneType)),
|
||||
],
|
||||
None,
|
||||
NoneType,
|
||||
)
|
||||
.quantify();
|
||||
module.context.assert_var_type("for__!", &for_t)?;
|
||||
let a = subtype_q("A", poly("Add", vec![ty_tp(t.clone())]));
|
||||
let o = a.clone().proj("Output");
|
||||
let add_t = func2(a, t, o).quantify();
|
||||
|
|
|
@ -4,7 +4,7 @@ use std::hash::{Hash, Hasher};
|
|||
use std::mem;
|
||||
|
||||
use erg_common::shared::Shared;
|
||||
use erg_common::traits::LimitedDisplay;
|
||||
use erg_common::traits::{LimitedDisplay, StructuralEq};
|
||||
use erg_common::Str;
|
||||
use erg_common::{addr_eq, log};
|
||||
|
||||
|
@ -47,6 +47,7 @@ pub trait HasLevel {
|
|||
|
||||
/// __NOTE__: you should use `Free::get_type/get_subsup` instead of deconstructing the constraint by `match`.
|
||||
/// Constraints may contain cycles, in which case using `match` to get the contents will cause memory pollutions.
|
||||
/// So this does not implement `structural_eq`.
|
||||
#[derive(Clone)]
|
||||
pub enum Constraint {
|
||||
// : Type --> (:> Never, <: Obj)
|
||||
|
@ -548,6 +549,21 @@ impl<T> Free<T> {
|
|||
}
|
||||
}
|
||||
|
||||
impl<T: StructuralEq + CanbeFree + Clone + Default> StructuralEq for Free<T> {
|
||||
fn structural_eq(&self, other: &Self) -> bool {
|
||||
if let (Some((l, r)), Some((l2, r2))) = (self.get_subsup(), other.get_subsup()) {
|
||||
self.forced_undoable_link(&T::default());
|
||||
let res = l.structural_eq(&l2) && r.structural_eq(&r2);
|
||||
self.undo();
|
||||
res
|
||||
} else if let (Some(l), Some(r)) = (self.get_type(), other.get_type()) {
|
||||
l.structural_eq(&r)
|
||||
} else {
|
||||
self.constraint_is_uninited() && other.constraint_is_uninited()
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<T: Clone> Free<T> {
|
||||
pub fn clone_inner(&self) -> FreeKind<T> {
|
||||
self.0.clone_inner()
|
||||
|
|
|
@ -22,7 +22,7 @@ use erg_common::fresh::fresh_varname;
|
|||
#[allow(unused_imports)]
|
||||
use erg_common::log;
|
||||
use erg_common::set::Set;
|
||||
use erg_common::traits::LimitedDisplay;
|
||||
use erg_common::traits::{LimitedDisplay, StructuralEq};
|
||||
use erg_common::vis::Field;
|
||||
use erg_common::{enum_unwrap, fmt_option, fmt_set_split_with, set, Str};
|
||||
|
||||
|
@ -293,6 +293,39 @@ impl LimitedDisplay for SubrType {
|
|||
}
|
||||
}
|
||||
|
||||
impl StructuralEq for SubrType {
|
||||
fn structural_eq(&self, other: &Self) -> bool {
|
||||
let kw_check = || {
|
||||
for lpt in self.default_params.iter() {
|
||||
if let Some(rpt) = self
|
||||
.default_params
|
||||
.iter()
|
||||
.find(|rpt| rpt.name() == lpt.name())
|
||||
{
|
||||
if !lpt.typ().structural_eq(rpt.typ()) {
|
||||
return false;
|
||||
}
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
true
|
||||
};
|
||||
let non_defaults_judge = self
|
||||
.non_default_params
|
||||
.iter()
|
||||
.zip(other.non_default_params.iter())
|
||||
.all(|(l, r)| l.typ().structural_eq(r.typ()));
|
||||
let var_params_judge = self
|
||||
.var_params
|
||||
.iter()
|
||||
.zip(other.var_params.iter())
|
||||
.all(|(l, r)| l.typ().structural_eq(r.typ()));
|
||||
let return_t_judge = self.return_t.structural_eq(&other.return_t);
|
||||
non_defaults_judge && var_params_judge && return_t_judge && kw_check()
|
||||
}
|
||||
}
|
||||
|
||||
impl SubrType {
|
||||
pub fn new(
|
||||
kind: SubrKind,
|
||||
|
@ -341,15 +374,21 @@ impl SubrType {
|
|||
qvars
|
||||
}
|
||||
|
||||
/// ```erg
|
||||
/// essential_qnames(|T, U| (T, U) -> Int) == {}
|
||||
/// essential_qnames(|T, U| (T, U) -> (T, U)) == {T, U}
|
||||
/// essential_qnames(|T, A| (T) -> A(<: T)) == {T}
|
||||
/// essential_qnames(|T, U| (T, T) -> U) == {T}
|
||||
/// ```
|
||||
pub fn essential_qnames(&self) -> Set<Str> {
|
||||
let param_ts_qnames = self
|
||||
let qnames_sets = self
|
||||
.non_default_params
|
||||
.iter()
|
||||
.flat_map(|pt| pt.typ().qnames())
|
||||
.chain(self.var_params.iter().flat_map(|pt| pt.typ().qnames()))
|
||||
.chain(self.default_params.iter().flat_map(|pt| pt.typ().qnames()));
|
||||
let return_t_qnames = self.return_t.qnames();
|
||||
return_t_qnames.intersec_from_iter(param_ts_qnames)
|
||||
.map(|pt| pt.typ().qnames())
|
||||
.chain(self.var_params.iter().map(|pt| pt.typ().qnames()))
|
||||
.chain(self.default_params.iter().map(|pt| pt.typ().qnames()))
|
||||
.chain([self.return_t.qnames()]);
|
||||
Set::multi_intersection(qnames_sets)
|
||||
}
|
||||
|
||||
pub fn has_qvar(&self) -> bool {
|
||||
|
@ -1155,6 +1194,105 @@ impl HasLevel for Type {
|
|||
}
|
||||
}
|
||||
|
||||
impl StructuralEq for Type {
|
||||
fn structural_eq(&self, other: &Self) -> bool {
|
||||
match (self, other) {
|
||||
(Self::FreeVar(fv), other) | (other, Self::FreeVar(fv)) if fv.is_linked() => {
|
||||
fv.crack().structural_eq(other)
|
||||
}
|
||||
(Self::FreeVar(fv), Self::FreeVar(fv2)) => fv.structural_eq(fv2),
|
||||
(Self::Refinement(refine), Self::Refinement(refine2)) => {
|
||||
refine.t.structural_eq(&refine2.t) && refine.preds == refine2.preds
|
||||
}
|
||||
(Self::Record(rec), Self::Record(rec2)) => {
|
||||
for (k, v) in rec.iter() {
|
||||
if let Some(v2) = rec2.get(k) {
|
||||
if !v.structural_eq(v2) {
|
||||
return false;
|
||||
}
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
true
|
||||
}
|
||||
(Self::Subr(subr), Self::Subr(subr2)) => subr.structural_eq(subr2),
|
||||
(
|
||||
Self::Callable { param_ts, return_t },
|
||||
Self::Callable {
|
||||
param_ts: param_ts2,
|
||||
return_t: return_t2,
|
||||
},
|
||||
) => {
|
||||
param_ts
|
||||
.iter()
|
||||
.zip(param_ts2.iter())
|
||||
.all(|(t, t2)| t.structural_eq(t2))
|
||||
&& return_t.structural_eq(return_t2)
|
||||
}
|
||||
(Self::Quantified(quant), Self::Quantified(quant2)) => quant.structural_eq(quant2),
|
||||
(
|
||||
Self::Poly { name, params },
|
||||
Self::Poly {
|
||||
name: name2,
|
||||
params: params2,
|
||||
},
|
||||
) => {
|
||||
name == name2
|
||||
&& params
|
||||
.iter()
|
||||
.zip(params2)
|
||||
.all(|(p, p2)| p.structural_eq(p2))
|
||||
}
|
||||
(Self::Ref(t), Self::Ref(t2)) => t.structural_eq(t2),
|
||||
(
|
||||
Self::RefMut { before, after },
|
||||
Self::RefMut {
|
||||
before: before2,
|
||||
after: after2,
|
||||
},
|
||||
) => {
|
||||
before.structural_eq(before2)
|
||||
&& after
|
||||
.as_ref()
|
||||
.zip(after2.as_ref())
|
||||
.map_or(true, |(a, b)| a.structural_eq(b))
|
||||
}
|
||||
(
|
||||
Self::Proj { lhs, rhs },
|
||||
Self::Proj {
|
||||
lhs: lhs2,
|
||||
rhs: rhs2,
|
||||
},
|
||||
) => lhs.structural_eq(lhs2) && rhs == rhs2,
|
||||
(
|
||||
Self::ProjCall {
|
||||
lhs,
|
||||
attr_name,
|
||||
args,
|
||||
},
|
||||
Self::ProjCall {
|
||||
lhs: lhs2,
|
||||
attr_name: attr_name2,
|
||||
args: args2,
|
||||
},
|
||||
) => {
|
||||
lhs.structural_eq(lhs2)
|
||||
&& attr_name == attr_name2
|
||||
&& args
|
||||
.iter()
|
||||
.zip(args2.iter())
|
||||
.all(|(a, b)| a.structural_eq(b))
|
||||
}
|
||||
// TODO: commutative
|
||||
(Self::And(l, r), Self::And(l2, r2)) => l.structural_eq(l2) && r.structural_eq(r2),
|
||||
(Self::Or(l, r), Self::Or(l2, r2)) => l.structural_eq(l2) && r.structural_eq(r2),
|
||||
(Self::Not(ty), Self::Not(ty2)) => ty.structural_eq(ty2),
|
||||
_ => self == other,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Type {
|
||||
pub const OBJ: &'static Self = &Self::Obj;
|
||||
pub const NONE: &'static Self = &Self::NoneType;
|
||||
|
@ -1607,19 +1745,22 @@ impl Type {
|
|||
|
||||
pub fn qvars(&self) -> Set<(Str, Constraint)> {
|
||||
match self {
|
||||
Self::FreeVar(fv) if fv.is_linked() => fv.forced_as_ref().linked().unwrap().qvars(),
|
||||
Self::FreeVar(fv) if fv.is_linked() => fv.crack().qvars(),
|
||||
Self::FreeVar(fv) if !fv.constraint_is_uninited() => {
|
||||
let base = set! {(fv.unbound_name().unwrap(), fv.constraint().unwrap())};
|
||||
fv.forced_undoable_link(&Type::Failure);
|
||||
let res = if let Some((sub, sup)) = fv.get_subsup() {
|
||||
base.concat(sub.qvars()).concat(sup.qvars())
|
||||
if let Some((sub, sup)) = fv.get_subsup() {
|
||||
fv.forced_undoable_link(&Type::Failure);
|
||||
let res = base.concat(sub.qvars()).concat(sup.qvars());
|
||||
fv.undo();
|
||||
res
|
||||
} else if let Some(ty) = fv.get_type() {
|
||||
base.concat(ty.qvars())
|
||||
fv.forced_undoable_link(&Type::Failure);
|
||||
let res = base.concat(ty.qvars());
|
||||
fv.undo();
|
||||
res
|
||||
} else {
|
||||
base
|
||||
};
|
||||
fv.undo();
|
||||
res
|
||||
}
|
||||
}
|
||||
Self::Ref(ty) => ty.qvars(),
|
||||
Self::RefMut { before, after } => before
|
||||
|
|
|
@ -6,7 +6,7 @@ use std::rc::Rc;
|
|||
use erg_common::dict::Dict;
|
||||
use erg_common::set;
|
||||
use erg_common::set::Set;
|
||||
use erg_common::traits::LimitedDisplay;
|
||||
use erg_common::traits::{LimitedDisplay, StructuralEq};
|
||||
use erg_common::Str;
|
||||
use erg_common::{dict, log};
|
||||
|
||||
|
@ -582,6 +582,74 @@ impl HasLevel for TyParam {
|
|||
}
|
||||
}
|
||||
|
||||
impl StructuralEq for TyParam {
|
||||
fn structural_eq(&self, other: &Self) -> bool {
|
||||
match (self, other) {
|
||||
(Self::Type(l), Self::Type(r)) => l.structural_eq(r),
|
||||
(Self::Array(l), Self::Array(r)) => l.iter().zip(r).all(|(l, r)| l.structural_eq(r)),
|
||||
(Self::Tuple(l), Self::Tuple(r)) => l.iter().zip(r).all(|(l, r)| l.structural_eq(r)),
|
||||
(Self::Dict(l), Self::Dict(r)) => {
|
||||
for (key, val) in l.iter() {
|
||||
if let Some(r_val) = r.get_by(key, |l, r| l.structural_eq(r)) {
|
||||
if !val.structural_eq(r_val) {
|
||||
return false;
|
||||
}
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
true
|
||||
}
|
||||
(Self::Set(l), Self::Set(r)) => {
|
||||
for l_val in l.iter() {
|
||||
if r.get_by(l_val, |l, r| l.structural_eq(r)).is_none() {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
true
|
||||
}
|
||||
(
|
||||
Self::Proj { obj, attr },
|
||||
Self::Proj {
|
||||
obj: r_obj,
|
||||
attr: r_attr,
|
||||
},
|
||||
) => obj.structural_eq(r_obj) && attr == r_attr,
|
||||
(
|
||||
Self::App {
|
||||
name: ln,
|
||||
args: lps,
|
||||
},
|
||||
Self::App {
|
||||
name: rn,
|
||||
args: rps,
|
||||
},
|
||||
) => ln == rn && lps.iter().zip(rps).all(|(l, r)| l.structural_eq(r)),
|
||||
(
|
||||
Self::UnaryOp { op, val },
|
||||
Self::UnaryOp {
|
||||
op: r_op,
|
||||
val: r_val,
|
||||
},
|
||||
) => op == r_op && val.structural_eq(r_val),
|
||||
(
|
||||
Self::BinOp { op, lhs, rhs },
|
||||
Self::BinOp {
|
||||
op: r_op,
|
||||
lhs: r_lhs,
|
||||
rhs: r_rhs,
|
||||
},
|
||||
) => op == r_op && lhs.structural_eq(r_lhs) && rhs.structural_eq(r_rhs),
|
||||
(Self::Erased(l), Self::Erased(r)) => l.structural_eq(r),
|
||||
(Self::FreeVar(fv), other) | (other, Self::FreeVar(fv)) if fv.is_linked() => {
|
||||
fv.crack().structural_eq(other)
|
||||
}
|
||||
(Self::FreeVar(l), Self::FreeVar(r)) => l.structural_eq(r),
|
||||
_ => self == other,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl TyParam {
|
||||
pub fn t(t: Type) -> Self {
|
||||
Self::Type(Box::new(t))
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue