chore: remove unnecessary params

This commit is contained in:
Shunsuke Shibayama 2023-03-03 10:01:05 +09:00
parent 1deb0c4788
commit 5c6ea316f5
13 changed files with 220 additions and 372 deletions

View file

@ -108,16 +108,17 @@ impl<'b> CompletionOrderSetter<'b> {
orders.push(CompletionOrder::NameMatched);
}
#[allow(clippy::blocks_in_if_conditions)]
if self.arg_pt.map_or(false, |pt| {
self.mod_ctx.subtype_of(&self.vi.t, pt.typ(), true)
}) {
if self
.arg_pt
.map_or(false, |pt| self.mod_ctx.subtype_of(&self.vi.t, pt.typ()))
{
orders.push(CompletionOrder::TypeMatched);
} else if self.arg_pt.map_or(false, |pt| {
let Some(return_t) = self.vi.t.return_t() else { return false; };
if return_t.has_qvar() {
return false;
}
self.mod_ctx.subtype_of(return_t, pt.typ(), true)
self.mod_ctx.subtype_of(return_t, pt.typ())
}) {
orders.push(CompletionOrder::ReturnTypeMatched);
}

View file

@ -46,18 +46,16 @@ impl Context {
res
}
pub(crate) fn eq_tp(&self, lhs: &TyParam, rhs: &TyParam, allow_cast: bool) -> bool {
pub(crate) fn eq_tp(&self, lhs: &TyParam, rhs: &TyParam) -> bool {
match (lhs, rhs) {
(TyParam::Type(lhs), TyParam::Type(rhs)) => {
return self.same_type_of(lhs, rhs, allow_cast)
}
(TyParam::Type(lhs), TyParam::Type(rhs)) => return self.same_type_of(lhs, rhs),
(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, allow_cast);
return lop == rop && self.eq_tp(lval, rval);
}
(
TyParam::BinOp {
@ -71,9 +69,7 @@ impl Context {
rhs: rr,
},
) => {
return lop == rop
&& self.eq_tp(ll, rl, allow_cast)
&& self.eq_tp(lr, rr, allow_cast);
return lop == rop && self.eq_tp(ll, rl) && self.eq_tp(lr, rr);
}
(
TyParam::App {
@ -90,11 +86,11 @@ impl Context {
&& largs
.iter()
.zip(rargs.iter())
.all(|(l, r)| self.eq_tp(l, r, allow_cast))
.all(|(l, r)| self.eq_tp(l, r))
}
(TyParam::FreeVar(fv), other) | (other, TyParam::FreeVar(fv)) => match &*fv.borrow() {
FreeKind::Linked(linked) | FreeKind::UndoableLinked { t: linked, .. } => {
return self.eq_tp(linked, other, allow_cast);
return self.eq_tp(linked, other);
}
FreeKind::Unbound { constraint, .. }
| FreeKind::NamedUnbound { constraint, .. } => {
@ -103,14 +99,14 @@ impl Context {
panic!("Uninited type variable: {fv}");
}
let other_t = self.type_of(other);
return self.same_type_of(t, &other_t, allow_cast);
return self.same_type_of(t, &other_t);
}
},
(TyParam::Value(ValueObj::Type(l)), TyParam::Type(r)) => {
return self.same_type_of(l.typ(), r.as_ref(), allow_cast);
return self.same_type_of(l.typ(), r.as_ref());
}
(TyParam::Type(l), TyParam::Value(ValueObj::Type(r))) => {
return self.same_type_of(l.as_ref(), r.typ(), allow_cast);
return self.same_type_of(l.as_ref(), r.typ());
}
(l, r) if l == r => {
return true;
@ -118,25 +114,25 @@ 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(&lt, &rt, allow_cast);
return self.same_type_of(&lt, &rt);
}
_ => {}
}
self.shallow_eq_tp(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 related(&self, lhs: &Type, rhs: &Type) -> bool {
self.supertype_of(lhs, rhs) || self.subtype_of(lhs, rhs)
}
/// 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) {
pub(crate) fn supertype_of(&self, lhs: &Type, rhs: &Type) -> bool {
let res = match Self::cheap_supertype_of(lhs, rhs) {
(Absolutely, judge) => judge,
(Maybe, judge) => {
judge
|| self.structural_supertype_of(lhs, rhs, allow_cast)
|| self.nominal_supertype_of(lhs, rhs, allow_cast)
|| self.structural_supertype_of(lhs, rhs)
|| self.nominal_supertype_of(lhs, rhs)
}
};
log!("answer: {lhs} {DEBUG_ERROR}:>{RESET} {rhs} == {res}");
@ -153,42 +149,32 @@ impl Context {
/// Seq(T) :> Range(T)
/// => Range(T).super_types == [Eq, Mutate, Seq(T), Output(T)]
/// ```
pub fn subtype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
match Self::cheap_subtype_of(lhs, rhs, allow_cast) {
pub fn subtype_of(&self, lhs: &Type, rhs: &Type) -> bool {
match Self::cheap_subtype_of(lhs, rhs) {
(Absolutely, judge) => judge,
(Maybe, judge) => {
judge
|| self.structural_subtype_of(lhs, rhs, allow_cast)
|| self.nominal_subtype_of(lhs, rhs, allow_cast)
judge || self.structural_subtype_of(lhs, rhs) || self.nominal_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 same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
self.supertype_of(lhs, rhs) && self.subtype_of(lhs, rhs)
}
pub(crate) fn cheap_supertype_of(
lhs: &Type,
rhs: &Type,
allow_cast: bool,
) -> (Credibility, bool) {
pub(crate) fn cheap_supertype_of(lhs: &Type, rhs: &Type) -> (Credibility, bool) {
if lhs == rhs {
return (Absolutely, true);
}
match (lhs, rhs) {
(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),
(Obj, _) | (_, Never | Failure) => (Absolutely, true),
(_, Obj) if lhs.is_simple_class() => (Absolutely, false),
(Never | Failure, _) if rhs.is_simple_class() => (Absolutely, false),
(Float | Ratio | Int | Nat | Bool, Bool)
| (Float | Ratio | Int | Nat, Nat)
| (Float | Ratio | Int, Int)
| (Float | Ratio, Ratio)
if allow_cast =>
{
(Absolutely, true)
}
(Type, ClassType | TraitType) if allow_cast => (Absolutely, true),
| (Float | Ratio, Ratio) => (Absolutely, true),
(Type, ClassType | TraitType) => (Absolutely, true),
(Uninited, _) | (_, Uninited) => panic!("used an uninited type variable"),
(
Mono(n),
@ -196,22 +182,18 @@ impl Context {
kind: SubrKind::Func,
..
}),
) if &n[..] == "GenericFunc" && allow_cast => (Absolutely, true),
) if &n[..] == "GenericFunc" => (Absolutely, true),
(
Mono(n),
Subr(SubrType {
kind: SubrKind::Proc,
..
}),
) if &n[..] == "GenericProc" && allow_cast => (Absolutely, true),
(Mono(l), Poly { name: r, .. })
if &l[..] == "GenericArray" && &r[..] == "Array" && allow_cast =>
{
) if &n[..] == "GenericProc" => (Absolutely, true),
(Mono(l), Poly { name: r, .. }) if &l[..] == "GenericArray" && &r[..] == "Array" => {
(Absolutely, true)
}
(Mono(l), Poly { name: r, .. })
if &l[..] == "GenericDict" && &r[..] == "Dict" && allow_cast =>
{
(Mono(l), Poly { name: r, .. }) if &l[..] == "GenericDict" && &r[..] == "Dict" => {
(Absolutely, true)
}
(Mono(l), Mono(r))
@ -219,8 +201,7 @@ impl Context {
&& (&r[..] == "GenericFunc"
|| &r[..] == "GenericProc"
|| &r[..] == "GenericFuncMethod"
|| &r[..] == "GenericProcMethod")
&& allow_cast =>
|| &r[..] == "GenericProcMethod") =>
{
(Absolutely, true)
}
@ -232,35 +213,30 @@ impl Context {
}
}
(_, FreeVar(fv)) | (FreeVar(fv), _) => match fv.get_subsup() {
Some((Type::Never, Type::Obj)) if allow_cast => (Absolutely, true),
Some((Type::Never, Type::Obj)) => (Absolutely, true),
_ => (Maybe, false),
},
(Mono(n), Subr(_) | Quantified(_)) if &n[..] == "GenericCallable" && allow_cast => {
(Absolutely, true)
}
(Mono(n), Subr(_) | Quantified(_)) if &n[..] == "GenericCallable" => (Absolutely, true),
(lhs, rhs) if lhs.is_simple_class() && rhs.is_simple_class() => (Absolutely, false),
_ => (Maybe, false),
}
}
fn cheap_subtype_of(lhs: &Type, rhs: &Type, allow_cast: bool) -> (Credibility, bool) {
Self::cheap_supertype_of(rhs, lhs, allow_cast)
fn cheap_subtype_of(lhs: &Type, rhs: &Type) -> (Credibility, bool) {
Self::cheap_supertype_of(rhs, lhs)
}
/// make judgments that include supertypes in the same namespace & take into account glue patches
/// 同一名前空間にある上位型を含めた判定&接着パッチを考慮した判定を行う
fn nominal_supertype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
if !allow_cast && lhs != rhs {
return false;
}
fn nominal_supertype_of(&self, lhs: &Type, rhs: &Type) -> bool {
if let Some(res) = self.inquire_cache(lhs, rhs) {
return res;
}
if let (Absolutely, judge) = self.classes_supertype_of(lhs, rhs, allow_cast) {
if let (Absolutely, judge) = self.classes_supertype_of(lhs, rhs) {
self.register_cache(lhs, rhs, judge);
return judge;
}
if let (Absolutely, judge) = self.traits_supertype_of(lhs, rhs, allow_cast) {
if let (Absolutely, judge) = self.traits_supertype_of(lhs, rhs) {
self.register_cache(lhs, rhs, judge);
return judge;
}
@ -268,33 +244,27 @@ impl Context {
false
}
fn nominal_subtype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
self.nominal_supertype_of(rhs, lhs, allow_cast)
fn nominal_subtype_of(&self, lhs: &Type, rhs: &Type) -> bool {
self.nominal_supertype_of(rhs, lhs)
}
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(move |ctx| {
if let ContextKind::Patch(base) = &ctx.kind {
return self.supertype_of(base, typ, allow_cast);
return self.supertype_of(base, typ);
}
false
})
}
fn _find_compatible_glue_patch(
&self,
sup: &Type,
sub: &Type,
allow_cast: bool,
) -> Option<&Context> {
fn _find_compatible_glue_patch(&self, sup: &Type, sub: &Type) -> 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, allow_cast)
&& self.subtype_of(&tr_inst.sup_trait, sup, allow_cast)
if self.subtype_of(sub, &tr_inst.sub_type)
&& self.subtype_of(&tr_inst.sup_trait, sup)
{
return Some(patch);
}
@ -303,12 +273,7 @@ impl Context {
None
}
fn classes_supertype_of(
&self,
lhs: &Type,
rhs: &Type,
allow_cast: bool,
) -> (Credibility, bool) {
fn classes_supertype_of(&self, lhs: &Type, rhs: &Type) -> (Credibility, bool) {
if !self.is_class(lhs) || !self.is_class(rhs) {
return (Maybe, false);
}
@ -327,12 +292,12 @@ impl Context {
rhs_sup.clone()
};
// Not `supertype_of` (only structures are compared)
match Self::cheap_supertype_of(lhs, &rhs_sup, allow_cast) {
match Self::cheap_supertype_of(lhs, &rhs_sup) {
(Absolutely, true) => {
return (Absolutely, true);
}
(Maybe, _) => {
if self.structural_supertype_of(lhs, &rhs_sup, allow_cast) {
if self.structural_supertype_of(lhs, &rhs_sup) {
return (Absolutely, true);
}
}
@ -346,19 +311,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, allow_cast: bool) -> (Credibility, bool) {
fn traits_supertype_of(&self, lhs: &Type, rhs: &Type) -> (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, allow_cast) {
match Self::cheap_supertype_of(lhs, rhs_sup) {
(Absolutely, true) => {
return (Absolutely, true);
}
(Maybe, _) => {
if self.structural_supertype_of(lhs, rhs_sup, allow_cast) {
if self.structural_supertype_of(lhs, rhs_sup) {
return (Absolutely, true);
}
}
@ -378,11 +343,11 @@ impl Context {
/// Use `supertype_of` for complete judgement.
/// 単一化、評価等はここでは行わない、スーパータイプになる可能性があるかだけ判定する
/// ので、lhsが(未連携)型変数の場合は単一化せずにtrueを返す
pub(crate) fn structural_supertype_of(&self, lhs: &Type, rhs: &Type, allow_cast: bool) -> bool {
pub(crate) fn structural_supertype_of(&self, lhs: &Type, rhs: &Type) -> bool {
match (lhs, rhs) {
// Proc :> Func if params are compatible
(Subr(ls), Subr(rs)) if ls.kind == rs.kind || ls.kind.is_proc() => {
if !allow_cast && ls.kind != rs.kind {
if ls.kind != rs.kind {
return false;
}
let kw_check = || {
@ -392,7 +357,7 @@ impl Context {
.iter()
.find(|rpt| rpt.name() == lpt.name())
{
if !self.subtype_of(lpt.typ(), rpt.typ(), allow_cast) {
if !self.subtype_of(lpt.typ(), rpt.typ()) {
return false;
}
} else {
@ -406,17 +371,17 @@ impl Context {
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 return_t_judge = self.supertype_of(&ls.return_t, &rs.return_t); // 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(), allow_cast));
.all(|(l, r)| self.subtype_of(l.typ(), r.typ()));
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))
.map(|(l, r)| self.subtype_of(l.typ(), r.typ()))
.unwrap_or(true);
same_params_len
&& return_t_judge
@ -427,14 +392,12 @@ impl Context {
// ?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, allow_cast)
}
(Some((_, l_sup)), Some((r_sub, _))) => self.supertype_of(&l_sup, &r_sub),
_ => {
if lfv.is_linked() {
self.supertype_of(&lfv.crack(), rhs, allow_cast)
self.supertype_of(&lfv.crack(), rhs)
} else if rfv.is_linked() {
self.supertype_of(lhs, &rfv.crack(), allow_cast)
self.supertype_of(lhs, &rfv.crack())
} else {
false
}
@ -448,13 +411,13 @@ impl Context {
(FreeVar(lfv), rhs) => {
match &*lfv.borrow() {
FreeKind::Linked(t) | FreeKind::UndoableLinked { t, .. } => {
self.supertype_of(t, rhs, allow_cast)
self.supertype_of(t, rhs)
}
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, allow_cast);
let res = self.supertype_of(&sup, rhs);
lfv.undo();
res
} else if let Some(lfvt) = lfv.get_type() {
@ -464,7 +427,7 @@ impl Context {
// => Array(Type, 3) :> Array(Typeof(Int), 3)
// => true
let rhs_meta = self.meta_type(rhs);
self.supertype_of(&lfvt, &rhs_meta, allow_cast)
self.supertype_of(&lfvt, &rhs_meta)
} else {
// constraint is uninitalized
log!(err "constraint is uninitialized: {lfv}/{rhs}");
@ -475,18 +438,18 @@ impl Context {
}
(lhs, FreeVar(rfv)) => match &*rfv.borrow() {
FreeKind::Linked(t) | FreeKind::UndoableLinked { t, .. } => {
self.supertype_of(lhs, t, allow_cast)
self.supertype_of(lhs, t)
}
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, allow_cast);
let res = self.supertype_of(lhs, &sub);
rfv.undo();
res
} else if let Some(rfvt) = rfv.get_type() {
let lhs_meta = self.meta_type(lhs);
self.supertype_of(&lhs_meta, &rfvt, allow_cast)
self.supertype_of(&lhs_meta, &rfvt)
} else {
// constraint is uninitalized
log!(err "constraint is uninitialized: {lhs}/{rfv}");
@ -497,7 +460,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, allow_cast) {
if !self.supertype_of(l, r) {
return false;
}
} else {
@ -506,20 +469,20 @@ impl Context {
}
true
}
(Type, Record(rec)) if allow_cast => {
(Type, Record(rec)) => {
for (_, t) in rec.iter() {
if !self.supertype_of(&Type, t, allow_cast) {
if !self.supertype_of(&Type, t) {
return false;
}
}
true
}
(Type, Subr(subr)) => self.supertype_of(&Type, &subr.return_t, allow_cast),
(Type, Subr(subr)) => self.supertype_of(&Type, &subr.return_t),
(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, allow_cast)
self.supertype_of(&Type, &elem_t)
}
(Type, Poly { name, params }) | (Poly { name, params }, Type)
if &name[..] == "Tuple" =>
@ -529,7 +492,7 @@ impl Context {
let Ok(t) = self.convert_tp_into_ty(tp) else {
return false;
};
if !self.supertype_of(&Type, &t, allow_cast) {
if !self.supertype_of(&Type, &t) {
return false;
}
}
@ -550,9 +513,7 @@ impl Context {
let Ok(v) = self.convert_tp_into_ty(v) else {
return false;
};
if !self.supertype_of(&Type, &k, allow_cast)
|| !self.supertype_of(&Type, &v, allow_cast)
{
if !self.supertype_of(&Type, &k) || !self.supertype_of(&Type, &v) {
return false;
}
}
@ -567,7 +528,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, allow_cast) {
if !self.supertype_of(&l.t, &r.t) {
return false;
}
let mut r_preds_clone = r.preds.clone();
@ -575,7 +536,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, allow_cast)
&& self.is_super_pred_of(l_pred, r_pred)
{
r_preds_clone.remove(r_pred);
}
@ -583,13 +544,13 @@ impl Context {
}
r_preds_clone.is_empty()
}
(Nat, re @ Refinement(_)) if allow_cast => {
(Nat, re @ Refinement(_)) => {
let nat = Type::Refinement(Nat.into_refinement());
self.structural_supertype_of(&nat, re, allow_cast)
self.structural_supertype_of(&nat, re)
}
(re @ Refinement(_), Nat) if allow_cast => {
(re @ Refinement(_), Nat) => {
let nat = Type::Refinement(Nat.into_refinement());
self.structural_supertype_of(re, &nat, allow_cast)
self.structural_supertype_of(re, &nat)
}
// Int :> {I: Int | ...} == true
// Int :> {I: Str| ...} == false
@ -597,26 +558,26 @@ impl Context {
// => Eq(Int) :> Eq({1, 2}) :> {1, 2}
// => true
// Bool :> {1} == true
(l, Refinement(r)) if allow_cast => {
if self.supertype_of(l, &r.t, allow_cast) {
(l, Refinement(r)) => {
if self.supertype_of(l, &r.t) {
return true;
}
let l = l.derefine();
if self.supertype_of(&l, &r.t, allow_cast) {
if self.supertype_of(&l, &r.t) {
return true;
}
let l = Type::Refinement(l.into_refinement());
self.structural_supertype_of(&l, rhs, allow_cast)
self.structural_supertype_of(&l, rhs)
}
// ({I: Int | True} :> Int) == true, ({N: Nat | ...} :> Int) == false, ({I: Int | I >= 0} :> Int) == false
(Refinement(l), r) if allow_cast => {
(Refinement(l), r) => {
if l.preds
.iter()
.any(|p| p.mentions(&l.var) && p.can_be_false())
{
return false;
}
self.supertype_of(&l.t, r, allow_cast)
self.supertype_of(&l.t, r)
}
(Quantified(_), Quantified(_)) => {
let Ok(l) = self.instantiate_dummy(lhs.clone()) else {
@ -628,13 +589,13 @@ impl Context {
self.sub_unify(&r, &l, &(), None).is_ok()
}
// (|T: Type| T -> T) !<: Obj -> Never
(Quantified(_), r) if allow_cast => {
(Quantified(_), r) => {
let Ok(inst) = self.instantiate_dummy(lhs.clone()) else {
return false;
};
self.sub_unify(r, &inst, &(), None).is_ok()
}
(l, Quantified(_)) if allow_cast => {
(l, Quantified(_)) => {
let Ok(inst) = self.instantiate_dummy(rhs.clone()) else {
return false;
};
@ -642,42 +603,34 @@ impl Context {
}
// 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, 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))
(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))
}
// not Nat :> not Int == true
(Not(l), Not(r)) => self.subtype_of(l, r, allow_cast),
(Not(l), Not(r)) => self.subtype_of(l, r),
// (Int or Str) :> Nat == Int :> Nat || Str :> Nat == true
// (Num or Show) :> Show == Num :> Show || Show :> Num == true
(Or(l_or, r_or), rhs) if allow_cast => {
self.supertype_of(l_or, rhs, allow_cast) || self.supertype_of(r_or, rhs, allow_cast)
}
(Or(l_or, r_or), rhs) => self.supertype_of(l_or, rhs) || self.supertype_of(r_or, rhs),
// Int :> (Nat or Str) == Int :> Nat && Int :> Str == false
(lhs, Or(l_or, r_or)) if allow_cast => {
self.supertype_of(lhs, l_or, allow_cast) && self.supertype_of(lhs, r_or, allow_cast)
}
(lhs, Or(l_or, r_or)) => self.supertype_of(lhs, l_or) && self.supertype_of(lhs, r_or),
(And(l_1, l_2), And(r_1, r_2)) => {
(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))
(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))
}
// (Num and Show) :> Show == false
(And(l_and, r_and), rhs) if allow_cast => {
self.supertype_of(l_and, rhs, allow_cast)
&& self.supertype_of(r_and, rhs, allow_cast)
(And(l_and, r_and), rhs) => {
self.supertype_of(l_and, rhs) && self.supertype_of(r_and, rhs)
}
// Show :> (Num and Show) == true
(lhs, And(l_and, r_and)) if allow_cast => {
self.supertype_of(lhs, l_and, allow_cast)
|| self.supertype_of(lhs, r_and, allow_cast)
(lhs, And(l_and, r_and)) => {
self.supertype_of(lhs, l_and) || self.supertype_of(lhs, r_and)
}
// RefMut are invariant
(Ref(l), Ref(r)) => self.supertype_of(l, r, allow_cast),
(Ref(l), Ref(r)) => self.supertype_of(l, r),
// TはすべてのRef(T)のメソッドを持つので、Ref(T)のサブタイプ
// REVIEW: RefMut is invariant, maybe
(Ref(l), r) if allow_cast => self.supertype_of(l, r, allow_cast),
(RefMut { before: l, .. }, r) if allow_cast => self.supertype_of(l, r, allow_cast),
(Ref(l), r) => self.supertype_of(l, r),
(RefMut { before: l, .. }, r) => self.supertype_of(l, r),
// `Eq(Set(T, N)) :> Set(T, N)` will be false, such cases are judged by nominal_supertype_of
(
Poly {
@ -698,7 +651,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(&lt, &rt, allow_cast)
self.supertype_of(&lt, &rt)
&& self
.eval_bin_tp(OpKind::Le, llen, rlen)
.map(|tp| matches!(tp, TyParam::Value(ValueObj::Bool(true))))
@ -707,13 +660,13 @@ impl Context {
todo!();
})
} else {
self.poly_supertype_of(lhs, lparams, rparams, allow_cast)
self.poly_supertype_of(lhs, lparams, rparams)
}
}
(Proj { .. }, _) => {
if let Some(cands) = self.get_candidates(lhs) {
for cand in cands.into_iter() {
if self.supertype_of(&cand, rhs, allow_cast) {
if self.supertype_of(&cand, rhs) {
return true;
}
}
@ -723,20 +676,20 @@ impl Context {
(_, Proj { .. }) => {
if let Some(cands) = self.get_candidates(rhs) {
for cand in cands.into_iter() {
if self.supertype_of(lhs, &cand, allow_cast) {
if self.supertype_of(lhs, &cand) {
return true;
}
}
}
false
}
(Structural(l), Structural(r)) => self.structural_supertype_of(l, r, allow_cast),
(Structural(l), Structural(r)) => self.structural_supertype_of(l, r),
// TODO: If visibility does not match, it should be reported as a cause of an error
(Structural(l), r) => {
let r_fields = self.fields(r);
for (l_field, l_ty) in self.fields(l) {
if let Some((r_field, r_ty)) = r_fields.get_key_value(&l_field) {
let compatible = self.supertype_of(&l_ty, r_ty, allow_cast);
let compatible = self.supertype_of(&l_ty, r_ty);
if r_field.vis != l_field.vis || !compatible {
return false;
}
@ -774,7 +727,6 @@ impl Context {
typ: &Type,
lparams: &[TyParam],
rparams: &[TyParam],
allow_cast: bool,
) -> bool {
log!(
"poly_supertype_of: {typ}, {}, {}",
@ -790,25 +742,19 @@ impl Context {
.iter()
.zip(rparams.iter())
.zip(variances.iter())
.all(|((lp, rp), variance)| self.supertype_of_tp(lp, rp, *variance, allow_cast))
.all(|((lp, rp), variance)| self.supertype_of_tp(lp, rp, *variance))
}
fn supertype_of_tp(
&self,
lp: &TyParam,
rp: &TyParam,
variance: Variance,
allow_cast: bool,
) -> bool {
fn supertype_of_tp(&self, lp: &TyParam, rp: &TyParam, variance: Variance) -> 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, allow_cast)
self.supertype_of_tp(&fv.crack(), rp, variance)
}
(_, TyParam::FreeVar(fv), _) if fv.is_linked() => {
self.supertype_of_tp(lp, &fv.crack(), variance, allow_cast)
self.supertype_of_tp(lp, &fv.crack(), variance)
}
// _: Type :> T == true
(TyParam::Erased(t), TyParam::Type(_), _)
@ -820,7 +766,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, allow_cast) {
if !self.supertype_of_tp(l, r, variance) {
return false;
}
}
@ -833,7 +779,7 @@ impl Context {
}
for (k, lv) in ld.iter() {
if let Some(rv) = rd.get(k) {
if !self.supertype_of_tp(lv, rv, variance, allow_cast) {
if !self.supertype_of_tp(lv, rv, variance) {
return false;
}
} else {
@ -842,65 +788,48 @@ impl Context {
}
true
}
(TyParam::Type(l), TyParam::Type(r), Variance::Contravariant) => {
self.subtype_of(l, r, allow_cast)
}
(TyParam::Type(l), TyParam::Type(r), Variance::Covariant) => {
self.supertype_of(l, r, allow_cast)
}
(TyParam::Type(l), TyParam::Type(r), Variance::Invariant) => {
self.same_type_of(l, r, allow_cast)
}
(TyParam::Type(l), TyParam::Type(r), Variance::Contravariant) => self.subtype_of(l, r),
(TyParam::Type(l), TyParam::Type(r), Variance::Covariant) => self.supertype_of(l, r),
(TyParam::Type(l), TyParam::Type(r), Variance::Invariant) => self.same_type_of(l, r),
(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, allow_cast)
self.subtype_of(&fv_t, &rp_t)
} else if variance == Variance::Covariant {
self.supertype_of(&fv_t, &rp_t, allow_cast)
self.supertype_of(&fv_t, &rp_t)
} else {
self.same_type_of(&fv_t, &rp_t, allow_cast)
self.same_type_of(&fv_t, &rp_t)
}
}
_ => self.eq_tp(lp, rp, allow_cast),
_ => self.eq_tp(lp, rp),
}
}
/// lhs <: rhs?
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_subtype_of(&self, lhs: &Type, rhs: &Type) -> bool {
self.structural_supertype_of(rhs, lhs)
}
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 _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 try_cmp(
&self,
l: &TyParam,
r: &TyParam,
allow_cast: bool,
) -> Option<TyParamOrdering> {
pub(crate) fn try_cmp(&self, l: &TyParam, r: &TyParam) -> 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, allow_cast)
self.try_cmp(&l, r)
} else { Some(Any) }
},
(TyParam::FreeVar(fv), p) if fv.is_linked() => {
self.try_cmp(&fv.crack(), p, allow_cast)
self.try_cmp(&fv.crack(), p)
}
(p, TyParam::FreeVar(fv)) if fv.is_linked() => {
self.try_cmp(p, &fv.crack(), allow_cast)
self.try_cmp(p, &fv.crack())
}
(
l @ (TyParam::FreeVar(_) | TyParam::Erased(_)),
@ -908,7 +837,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, allow_cast) || self.subtype_of(&l_t, &r_t, allow_cast) {
if self.supertype_of(&l_t, &r_t) || self.subtype_of(&l_t, &r_t) {
Some(Any)
} else { Some(NotEqual) }
},
@ -928,8 +857,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, allow_cast).unwrap(),
self.try_cmp(&sup, p, allow_cast).unwrap()
self.try_cmp(&inf, p).unwrap(),
self.try_cmp(&sup, p).unwrap()
) {
(Less, Less) => Some(Less),
(Less, Equal) => Some(LessEqual),
@ -963,7 +892,7 @@ impl Context {
todo!("cmp({inf}, {sup}) = {l:?}, cmp({inf}, {sup}) = {r:?}"),
}
} else {
match (self.supertype_of(&lt, &pt, allow_cast), self.subtype_of(&lt, &pt, allow_cast)) {
match (self.supertype_of(&lt, &pt), self.subtype_of(&lt, &pt)) {
(true, true) => Some(Any),
(true, false) => Some(Any),
(false, true) => Some(NotEqual),
@ -972,7 +901,7 @@ impl Context {
}
}
(l, r @ (TyParam::Erased(_) | TyParam::FreeVar(_))) =>
self.try_cmp(r, l, allow_cast).map(|ord| ord.reverse()),
self.try_cmp(r, l).map(|ord| ord.reverse()),
(_l, _r) => {
erg_common::fmt_dbg!(_l, _r,);
None
@ -982,17 +911,13 @@ 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, allow_cast),
self.subtype_of(lhs, rhs, allow_cast),
) {
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
(true, true) => return lhs.clone(), // lhs = rhs
(true, false) => return lhs.clone(), // lhs :> rhs
(false, true) => return rhs.clone(),
@ -1024,7 +949,7 @@ impl Context {
unified_params.push(TyParam::t(self.union(l, r)))
}
(_, _) => {
if self.eq_tp(lp, rp, allow_cast) {
if self.eq_tp(lp, rp) {
unified_params.push(lp.clone());
} else {
return or(lhs.clone(), rhs.clone());
@ -1053,16 +978,12 @@ 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, allow_cast),
self.subtype_of(lhs, rhs, allow_cast),
) {
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
(true, true) => return lhs.clone(), // lhs = rhs
(true, false) => return rhs.clone(), // lhs :> rhs
(false, true) => return lhs.clone(),
@ -1124,7 +1045,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, allow_cast: bool) -> bool {
fn is_super_pred_of(&self, lhs: &Predicate, rhs: &Predicate) -> bool {
match (lhs, rhs) {
(Pred::LessEqual { rhs, .. }, _) if !rhs.has_upper_bound() => true,
(Pred::GreaterEqual { rhs, .. }, _) if !rhs.has_lower_bound() => true,
@ -1137,7 +1058,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, allow_cast)
.try_cmp(rhs, rhs2)
.map(|ord| ord.canbe_eq())
.unwrap_or(false),
// {T >= 0} :> {T >= 1}, {T >= 0} :> {T == 1}
@ -1145,47 +1066,34 @@ impl Context {
Pred::GreaterEqual { rhs, .. },
Pred::GreaterEqual { rhs: rhs2, .. } | Pred::Equal { rhs: rhs2, .. },
) => self
.try_cmp(rhs, rhs2, allow_cast)
.try_cmp(rhs, rhs2)
.map(|ord| ord.canbe_le())
.unwrap_or(false),
(
Pred::LessEqual { rhs, .. },
Pred::LessEqual { rhs: rhs2, .. } | Pred::Equal { rhs: rhs2, .. },
) => self
.try_cmp(rhs, rhs2, allow_cast)
.try_cmp(rhs, rhs2)
.map(|ord| ord.canbe_ge())
.unwrap_or(false),
(lhs @ (Pred::GreaterEqual { .. } | Pred::LessEqual { .. }), Pred::And(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, allow_cast)
&& self.is_super_pred_of(lhs, r, allow_cast)
self.is_super_pred_of(lhs, l) || self.is_super_pred_of(lhs, r)
}
(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, allow_cast)
|| self.is_super_pred_of(r, rhs, allow_cast)
self.is_super_pred_of(l, rhs) || self.is_super_pred_of(r, rhs)
}
(Pred::And(l, r), rhs) => {
self.is_super_pred_of(l, rhs, allow_cast)
&& self.is_super_pred_of(r, rhs, allow_cast)
self.is_super_pred_of(l, rhs) && self.is_super_pred_of(r, rhs)
}
(lhs, rhs) => todo!("{lhs}/{rhs}"),
}
}
pub(crate) fn is_sub_constraint_of(
&self,
l: &Constraint,
r: &Constraint,
allow_cast: bool,
) -> bool {
pub(crate) fn is_sub_constraint_of(&self, l: &Constraint, r: &Constraint) -> bool {
match (l, r) {
// (?I: Nat) <: (?I: Int)
(Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => {
self.subtype_of(lhs, rhs, allow_cast)
}
(Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => self.subtype_of(lhs, rhs),
// (?T <: Int) <: (?T: Type)
(Constraint::Sandwiched { sub: Never, .. }, Constraint::TypeOf(Type)) => true,
// (Int <: ?T) <: (Nat <: ?U)
@ -1203,9 +1111,7 @@ impl Context {
sup: rsup,
..
},
) => {
self.supertype_of(lsub, rsub, allow_cast) && self.subtype_of(lsup, rsup, allow_cast)
}
) => self.supertype_of(lsub, rsub) && self.subtype_of(lsup, rsup),
_ => false,
}
}
@ -1227,7 +1133,7 @@ impl Context {
if lhs == &refine.var =>
{
if let Some(max) = &maybe_max {
if self.try_cmp(rhs, max, true) == Some(Greater) {
if self.try_cmp(rhs, max) == Some(Greater) {
maybe_max = Some(rhs.clone());
}
} else {
@ -1255,7 +1161,7 @@ impl Context {
if lhs == &refine.var =>
{
if let Some(min) = &maybe_min {
if self.try_cmp(rhs, min, true) == Some(Less) {
if self.try_cmp(rhs, min) == Some(Less) {
maybe_min = Some(rhs.clone());
}
} else {
@ -1277,10 +1183,7 @@ 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, true),
self.subtype_of(lhs, rhs, true),
) {
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
(true, true) | (true, false) => Some(rhs),
(false, true) => Some(lhs),
(false, false) => None,
@ -1289,10 +1192,7 @@ 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, true),
self.subtype_of(lhs, rhs, true),
) {
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
(true, true) | (true, false) => Some(lhs),
(false, true) => Some(rhs),
(false, false) => None,

View file

@ -734,7 +734,6 @@ 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)
@ -749,8 +748,7 @@ 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(), allow_cast) =>
if op.is_comparison() && self.supertype_of(&t, &self.get_tp_t(&rhs).unwrap()) =>
{
Ok(TyParam::value(true))
}
@ -760,8 +758,7 @@ 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, allow_cast) =>
if op.is_comparison() && self.supertype_of(&self.get_tp_t(&lhs).unwrap(), &t) =>
{
Ok(TyParam::value(true))
}
@ -1045,7 +1042,6 @@ 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() {
@ -1094,12 +1090,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, allow_cast) {
if !self.supertype_of(impl_trait, sup) {
continue;
}
}
(ClassDefType::ImplTrait { impl_trait, .. }, None) => {
if !self.supertype_of(impl_trait, &sub, allow_cast) {
if !self.supertype_of(impl_trait, &sub) {
continue;
}
}
@ -1223,7 +1219,6 @@ 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) {
@ -1232,7 +1227,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, allow_cast) {
if !self.supertype_of(&trait_, sup) {
return None;
}
}
@ -1630,14 +1625,13 @@ 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, allow_cast)
self.subtype_of(&self.get_tp_t(rhs).unwrap(), &Type::Type)
}
(_, TyParam::Type(r)) if r.is_unbound_var() => {
let lhs = self.get_tp_t(lhs).unwrap();
self.subtype_of(&lhs, &Type::Type, allow_cast)
self.subtype_of(&lhs, &Type::Type)
}
(TyParam::Type(l), TyParam::Type(r)) => l == r,
(TyParam::Value(l), TyParam::Value(r)) => l == r,

View file

@ -538,12 +538,11 @@ 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, allow_cast) {
if self.subtype_of(&sub_t, &super_t) {
let sub_t = if cfg!(feature = "debug") {
sub_t
} else {
@ -559,7 +558,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, allow_cast) {
if self.supertype_of(&sub_t, &super_t) {
Ok(sub_t)
} else {
Err(TyCheckErrors::from(TyCheckError::subtyping_error(
@ -856,9 +855,8 @@ 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, allow_cast) {
if self.subtype_of(class, &Type::Never) {
return true;
}
if class.is_monomorphic() {
@ -869,11 +867,10 @@ 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, allow_cast)
&& self.supertype_of(&inst.sup_trait, trait_, allow_cast)
if self.supertype_of(&inst.sub_type, class)
&& self.supertype_of(&inst.sup_trait, trait_)
{
super_exists = true;
break;
@ -883,11 +880,10 @@ 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, allow_cast)
&& self.supertype_of(&inst.sup_trait, trait_, allow_cast)
if self.supertype_of(&inst.sub_type, class)
&& self.supertype_of(&inst.sup_trait, trait_)
{
super_exists = true;
break;

View file

@ -261,7 +261,6 @@ 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();
@ -269,7 +268,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(), allow_cast) {
if ctx.subtype_of(idx.typ(), kt.typ()) {
return Some(v);
}
}

View file

@ -477,8 +477,7 @@ impl Context {
return Err(e);
}
}
let allow_cast = true;
for patch in self.find_patches_of(obj.ref_t(), allow_cast) {
for patch in self.find_patches_of(obj.ref_t()) {
if let Some(vi) = patch
.locals
.get(ident.inspect())
@ -840,8 +839,7 @@ impl Context {
}
_ => {}
}
let allow_cast = true;
for patch in self.find_patches_of(obj.ref_t(), allow_cast) {
for patch in self.find_patches_of(obj.ref_t()) {
if let Some(vi) = patch
.locals
.get(attr_name.inspect())
@ -1067,8 +1065,7 @@ impl Context {
}
Type::FreeVar(fv) => {
if let Some(sub) = fv.get_sub() {
let allow_cast = true;
if !self.subtype_of(&sub, &mono("GenericCallable"), allow_cast) {
if !self.subtype_of(&sub, &mono("GenericCallable")) {
return Err(self.not_callable_error(obj, attr_name, instance, None));
}
if sub != Never {
@ -1789,15 +1786,11 @@ 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, allow_cast))
{
if buf.iter().all(|buf_inner| self.related(buf_inner, t)) {
found = true;
buf.push(t);
break;
@ -1818,7 +1811,7 @@ impl Context {
if let Some(pos) = concatenated
.iter()
.take(len - idx - 1)
.rposition(|t| self.supertype_of(maybe_sup, t, allow_cast))
.rposition(|t| self.supertype_of(maybe_sup, t))
{
let sup = concatenated.remove(idx);
concatenated.insert(pos, sup); // not `pos + 1` because the element was removed at idx
@ -1910,7 +1903,6 @@ 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()) {
@ -1963,11 +1955,7 @@ impl Context {
Type::Poly { name, .. } => {
return self.get_type(name);
}
Type::Record(rec)
if rec
.values()
.all(|attr| self.supertype_of(&Type, attr, allow_cast)) =>
{
Type::Record(rec) if rec.values().all(|attr| self.supertype_of(&Type, attr)) => {
return self
.get_builtins()
.unwrap_or(self)
@ -2507,10 +2495,9 @@ impl Context {
}
fn get_trait_proj_candidates(&self, trait_: &Type, rhs: &Str) -> Set<Type> {
let allow_cast = true;
let impls = self.get_trait_impls(trait_);
let candidates = impls.into_iter().filter_map(move |inst| {
if self.supertype_of(&inst.sup_trait, trait_, allow_cast) {
if self.supertype_of(&inst.sup_trait, trait_) {
self.eval_t_params(proj(inst.sub_type, rhs), self.level, &())
.ok()
} else {

View file

@ -897,7 +897,7 @@ impl Context {
RegistrationMode::Normal,
false,
)?;
if self.subtype_of(&self.get_tp_t(&tp)?, &spec_t, true) {
if self.subtype_of(&self.get_tp_t(&tp)?, &spec_t) {
Ok(tp)
} else {
Err(TyCheckErrors::from(TyCheckError::subtyping_error(
@ -1157,8 +1157,7 @@ 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)?;
let allow_cast = true;
if let Some(Greater) = self.try_cmp(&l, &r, allow_cast) {
if let Some(Greater) = self.try_cmp(&l, &r) {
panic!("{l}..{r} is not a valid interval type (should be lhs <= rhs)")
}
Ok(int_interval(op, l, r))

View file

@ -668,8 +668,7 @@ impl Context {
let found_t = self.generalize_t(sub_t);
// let found_t = self.eliminate_needless_quant(found_t, crate::context::Variance::Covariant, sig)?;
let py_name = if let Some(vi) = self.decls.remove(name) {
let allow_cast = true;
if !self.supertype_of(&vi.t, &found_t, allow_cast) {
if !self.supertype_of(&vi.t, &found_t) {
let err = TyCheckError::violate_decl_error(
self.cfg.input.clone(),
line!() as usize,
@ -1774,10 +1773,9 @@ 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, allow_cast),
self.subtype_of(lhs.ref_t(), &cast_to, allow_cast),
self.supertype_of(lhs.ref_t(), &cast_to),
self.subtype_of(lhs.ref_t(), &cast_to),
) {
// assert 1 in {1}
(true, true) => Ok(()),

View file

@ -35,7 +35,7 @@ impl Context {
Type::Int,
set! { Predicate::eq(var, TyParam::value(1)) },
);
if self.supertype_of(&lhs, &rhs, true) {
if self.supertype_of(&lhs, &rhs) {
Ok(())
} else {
Err(())
@ -46,8 +46,8 @@ impl Context {
let t = crate::ty::constructors::type_q("T");
let quant = func1(t.clone(), t).quantify();
let subr = func1(Obj, Never);
assert!(!self.subtype_of(&quant, &subr, true));
assert!(self.subtype_of(&subr, &quant, true));
assert!(!self.subtype_of(&quant, &subr));
assert!(self.subtype_of(&subr, &quant));
Ok(())
}
@ -57,7 +57,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, false) {
if self.supertype_of(&pair.sup_trait, &maybe_trait) {
min = self.min(&min, &pair.sub_type).unwrap_or(&min).clone();
}
}

View file

@ -138,7 +138,6 @@ 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
@ -170,15 +169,12 @@ 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, allow_cast) {
if self.supertype_of(&fv_t, &tp_t) {
// 外部未連携型変数の場合、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,
allow_cast,
) || lfv.constraint().unwrap().get_type() == Some(&Type)
if self.is_sub_constraint_of(&lfv.constraint().unwrap(), &new_constraint)
|| lfv.constraint().unwrap().get_type() == Some(&Type)
{
lfv.update_constraint(new_constraint, false);
}
@ -187,9 +183,9 @@ impl Context {
}
Ok(())
} else if allow_divergence
&& (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)
&& (self.eq_tp(tp, &TyParam::value(Inf))
|| self.eq_tp(tp, &TyParam::value(NegInf)))
&& self.subtype_of(&fv_t, &mono("Num"))
{
lfv.link(tp);
Ok(())
@ -210,15 +206,12 @@ 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, allow_cast) {
if self.supertype_of(&fv_t, &tp_t) {
// 外部未連携型変数の場合、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,
allow_cast,
) || rfv.constraint().unwrap().get_type() == Some(&Type)
if self.is_sub_constraint_of(&rfv.constraint().unwrap(), &new_constraint)
|| rfv.constraint().unwrap().get_type() == Some(&Type)
{
rfv.update_constraint(new_constraint, false);
}
@ -227,9 +220,9 @@ impl Context {
}
Ok(())
} else if allow_divergence
&& (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)
&& (self.eq_tp(tp, &TyParam::value(Inf))
|| self.eq_tp(tp, &TyParam::value(NegInf)))
&& self.subtype_of(&fv_t, &mono("Num"))
{
rfv.link(tp);
Ok(())
@ -262,7 +255,7 @@ impl Context {
}
(l, TyParam::Erased(t)) => {
let sub_t = self.get_tp_t(l)?;
if self.subtype_of(&sub_t, t, allow_cast) {
if self.subtype_of(&sub_t, t) {
Ok(())
} else {
Err(TyCheckErrors::from(TyCheckError::subtyping_error(
@ -320,7 +313,6 @@ 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();
@ -350,7 +342,7 @@ impl Context {
(TyParam::Lambda(_l), TyParam::Lambda(_r)) => {
todo!("{_l}/{_r}")
}
(l, r) if self.eq_tp(l, r, allow_cast) => Ok(()),
(l, r) if self.eq_tp(l, r) => Ok(()),
(l, r) => panic!("type-parameter re-unification failed:\nl: {l}\nr: {r}"),
}
}
@ -453,7 +445,6 @@ 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),
@ -509,7 +500,7 @@ impl Context {
}
Ok(())
}
(l, r) if self.same_type_of(l, r, allow_cast) => Ok(()),
(l, r) if self.same_type_of(l, r) => Ok(()),
(l, r) => Err(TyCheckError::re_unification_error(
self.cfg.input.clone(),
line!() as usize,
@ -541,7 +532,6 @@ 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 {
@ -552,7 +542,7 @@ impl Context {
return Ok(());
}
self.occur(maybe_sub, maybe_sup, loc)?;
let maybe_sub_is_sub = self.subtype_of(maybe_sub, maybe_sup, allow_cast);
let maybe_sub_is_sub = self.subtype_of(maybe_sub, maybe_sup);
if !maybe_sub_is_sub {
log!(err "{maybe_sub} !<: {maybe_sup}");
return Err(TyCheckErrors::from(TyCheckError::type_mismatch_error(
@ -669,7 +659,7 @@ impl Context {
}
// sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)
Constraint::TypeOf(ty) => {
if self.supertype_of(&Type, ty, allow_cast) {
if self.supertype_of(&Type, ty) {
*constraint = Constraint::new_supertype_of(maybe_sub.clone());
} else {
todo!()
@ -686,7 +676,7 @@ impl Context {
for (sup_field, sup_ty) in self.fields(sup) {
if let Some((_, sub_ty)) = sub_fields.get_key_value(&sup_field) {
self.sub_unify(sub_ty, &sup_ty, loc, param_name)?;
} else if !self.subtype_of(&fv.get_sub().unwrap(), &Never, allow_cast) {
} else if !self.subtype_of(&fv.get_sub().unwrap(), &Never) {
maybe_sub.coerce();
return self.sub_unify(maybe_sub, maybe_sup, loc, param_name);
} else {
@ -724,7 +714,7 @@ impl Context {
}
// sub_unify(?T(: Type), Int): (?T(<: Int))
Constraint::TypeOf(ty) => {
if self.supertype_of(&Type, ty, allow_cast) {
if self.supertype_of(&Type, ty) {
*constraint = Constraint::new_subtype_of(maybe_sup.clone());
} else {
todo!()
@ -943,7 +933,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, allow_cast) {
if self.subtype_of(&sub.t, &sup.t) {
self.sub_unify(&sub.t, &sup.t, loc, param_name)?;
}
if sup.preds.is_empty() {
@ -991,7 +981,6 @@ 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 =
@ -1008,7 +997,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, allow_cast) {
if self.supertype_of(maybe_sup, sup_trait) {
for (l_maybe_sub, r_maybe_sup) in
sub_trait_instance.typarams().iter().zip(sup_params.iter())
{

View file

@ -246,7 +246,6 @@ 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.deconstruct();
let mut union = Type::Never;
@ -259,11 +258,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,
allow_cast,
) {
if !self
.module
.context
.supertype_of(&type_asc.spec.spec_t, &union)
{
return Err(self.elem_err(&l, &r, &elem));
} // else(OK): e.g. [1, "a": Str or Int]
} else {
@ -484,7 +483,6 @@ 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(_)) => {
@ -493,11 +491,7 @@ impl ASTLowerer {
"SetWithMutType!",
vec![TyParam::t(elem.t()), TyParam::Value(v)],
)
} else if self
.module
.context
.subtype_of(&elem.t(), &Type::Type, allow_cast)
{
} else if self.module.context.subtype_of(&elem.t(), &Type::Type) {
poly("SetType", vec![TyParam::t(elem.t()), TyParam::Value(v)])
} else {
set_t(elem.t(), TyParam::Value(v))
@ -1061,13 +1055,8 @@ 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, allow_cast)
{
if self.module.context.subtype_of(body.ref_t(), &Type::Type) {
for param in params.non_defaults.iter() {
self.inc_ref(&param.vi, param);
}
@ -1857,7 +1846,6 @@ impl ASTLowerer {
let mut errors = CompileErrors::empty();
let trait_type = typ_ctx.0;
let trait_ctx = typ_ctx.1;
let allow_cast = true;
let mut unverified_names = self.module.context.locals.keys().collect::<Set<_>>();
for (decl_name, decl_vi) in trait_ctx.decls.iter() {
if let Some((name, vi)) = self.module.context.get_var_kv(decl_name.inspect()) {
@ -1868,11 +1856,7 @@ impl ASTLowerer {
.replace(trait_type, impl_trait)
.replace(impl_trait, class);
unverified_names.remove(name);
if !self
.module
.context
.supertype_of(&replaced_decl_t, def_t, allow_cast)
{
if !self.module.context.supertype_of(&replaced_decl_t, def_t) {
errors.push(LowerError::trait_member_type_error(
self.cfg.input.clone(),
line!() as usize,
@ -2087,7 +2071,7 @@ impl ASTLowerer {
.sub_unify(&ident_vi.t, &spec_t, &ident, Some(ident.inspect()))?;
} else {
// if subtype ascription
if self.module.context.subtype_of(&ident_vi.t, &spec_t, true) {
if self.module.context.subtype_of(&ident_vi.t, &spec_t) {
return Err(LowerErrors::from(LowerError::subtyping_error(
self.cfg.input.clone(),
line!() as usize,

View file

@ -10,10 +10,11 @@ Point3D|<: Norm|.
norm|T <: Norm| x: T = x.norm()
inplicit_norm x = x.norm()
implicit_norm x = x.norm()
p = Point2D.new {x = 3; y = 4}
print! norm(p)
assert norm(p) == 25
assert norm(Point3D.new {x = 3; y = 4; z = 5}) == 50
# assert norm(1) # this should be an error
assert implicit_norm(p) == 25

View file

@ -3,7 +3,7 @@ y: Ratio = f 1
# Erg's type checking does not necessarily enlarge the type. So this is OK.
z: Int = y
# But this is invalid.
invalid: 10..<20 = z
invalid: 10..<20 = z #ERR
for! [(1, 2)], ((i, j),) =>
k = i + 1 # OK