chore: fill missing arms

This commit is contained in:
Shunsuke Shibayama 2024-02-25 11:20:11 +09:00
parent c74513f507
commit ac80cbba87
6 changed files with 73 additions and 5 deletions

View file

@ -29,3 +29,11 @@ jobs:
-H "Accept: application/vnd.github.v3+json" \
https://api.github.com/repos/mtshiba/ergscripts/dispatches \
-d '{"event_type":"notification-push-main","client_payload":{"msg": "a change has been pushed to main"}}'
- name: notify to pytypes
run: |
curl \
-X POST \
-H "Authorization: token ${{ secrets.TOKEN }}" \
-H "Accept: application/vnd.github.v3+json" \
https://api.github.com/repos/erg-lang/pytypes/dispatches \
-d '{"event_type":"notification-push-main","client_payload":{"msg": "a change has been pushed to main"}}'

View file

@ -1093,6 +1093,11 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
// * sub_unify({0}, ?T(:> {1}, <: Nat)): (?T(:> {0, 1}, <: Nat))
// * sub_unify(Bool, ?T(<: Bool or Y)): (?T == Bool)
// * sub_unify(Float, ?T(<: Structural{ .imag = ?U })) ==> ?U == Float
if let Type::Refinement(refine) = maybe_sub {
if refine.t.addr_eq(maybe_sup) {
return Ok(());
}
}
if let Some((sub, mut sup)) = sup_fv.get_subsup() {
if sup.is_structural() || !sup.is_recursive() {
self.sub_unify(maybe_sub, &sup)?;

View file

@ -238,7 +238,9 @@ impl Constraint {
pub fn eliminate_recursion(self, target: &Type) -> Self {
match self {
Self::Sandwiched { sub, sup } => {
if sub.addr_eq(target) {
if sub.addr_eq(target) && sup.addr_eq(target) {
Self::new_type_of(Type::Type)
} else if sub.addr_eq(target) {
Self::new_subtype_of(sup)
} else if sup.addr_eq(target) {
Self::new_supertype_of(sub)

View file

@ -3760,7 +3760,7 @@ impl Type {
}
}
fn addr_eq(&self, other: &Type) -> bool {
pub(crate) fn addr_eq(&self, other: &Type) -> bool {
match (self, other) {
(Self::FreeVar(slf), _) if slf.is_linked() => slf.crack().addr_eq(other),
(_, Self::FreeVar(otr)) if otr.is_linked() => otr.crack().addr_eq(self),

View file

@ -194,6 +194,22 @@ impl StructuralEq for Predicate {
| (Self::LessEqual { rhs, .. }, Self::LessEqual { rhs: r2, .. }) => {
rhs.structural_eq(r2)
}
(Self::GeneralEqual { lhs, rhs }, Self::GeneralEqual { lhs: l, rhs: r })
| (Self::GeneralLessEqual { lhs, rhs }, Self::GeneralLessEqual { lhs: l, rhs: r })
| (
Self::GeneralGreaterEqual { lhs, rhs },
Self::GeneralGreaterEqual { lhs: l, rhs: r },
)
| (Self::GeneralNotEqual { lhs, rhs }, Self::GeneralNotEqual { lhs: l, rhs: r }) => {
lhs.structural_eq(l) && rhs.structural_eq(r)
}
(
Self::Attr { receiver, name },
Self::Attr {
receiver: r,
name: n,
},
) => receiver.structural_eq(r) && name == n,
(
Self::Call {
receiver,
@ -593,6 +609,10 @@ impl Predicate {
args: new_args,
}
}
Self::Attr { receiver, name } => Self::Attr {
receiver: receiver.substitute(var, tp),
name,
},
_ => self,
}
}
@ -604,6 +624,11 @@ impl Predicate {
| Self::LessEqual { lhs, .. }
| Self::GreaterEqual { lhs, .. }
| Self::NotEqual { lhs, .. } => &lhs[..] == name,
Self::GeneralEqual { lhs, rhs }
| Self::GeneralLessEqual { lhs, rhs }
| Self::GeneralGreaterEqual { lhs, rhs }
| Self::GeneralNotEqual { lhs, rhs } => lhs.mentions(name) || rhs.mentions(name),
Self::Not(pred) => pred.mentions(name),
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs.mentions(name) || rhs.mentions(name),
_ => false,
}
@ -779,6 +804,10 @@ impl Predicate {
Self::GreaterEqual { lhs, rhs } => Self::lt(lhs, rhs),
Self::LessEqual { lhs, rhs } => Self::gt(lhs, rhs),
Self::NotEqual { lhs, rhs } => Self::eq(lhs, rhs),
Self::GeneralEqual { lhs, rhs } => Self::GeneralNotEqual { lhs, rhs },
Self::GeneralLessEqual { lhs, rhs } => Self::GeneralGreaterEqual { lhs, rhs },
Self::GeneralGreaterEqual { lhs, rhs } => Self::GeneralLessEqual { lhs, rhs },
Self::GeneralNotEqual { lhs, rhs } => Self::GeneralEqual { lhs, rhs },
Self::Not(pred) => *pred,
other => Self::Not(Box::new(other)),
}

View file

@ -1246,7 +1246,11 @@ impl TyParam {
Self::Type(t) => t.contains_type(target),
Self::Erased(t) => t.contains_type(target),
Self::Proj { obj, .. } => obj.contains_type(target),
Self::ProjCall { obj, args, .. } => {
obj.contains_type(target) || args.iter().any(|t| t.contains_type(target))
}
Self::Array(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.contains_type(target)),
Self::UnsizedArray(elem) => elem.contains_type(target),
Self::Set(ts) => ts.iter().any(|t| t.contains_type(target)),
Self::Dict(ts) => ts
.iter()
@ -1272,12 +1276,18 @@ impl TyParam {
Self::Type(t) => t.contains_tp(target),
Self::Erased(t) => t.contains_tp(target),
Self::Proj { obj, .. } => obj.contains_tp(target),
Self::ProjCall { obj, args, .. } => {
obj.contains_tp(target) || args.iter().any(|t| t.contains_tp(target))
}
Self::Array(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.contains_tp(target)),
Self::UnsizedArray(elem) => elem.contains_tp(target),
Self::Set(ts) => ts.iter().any(|t| t.contains_tp(target)),
Self::Dict(ts) => ts
.iter()
.any(|(k, v)| k.contains_tp(target) || v.contains_tp(target)),
Self::Record(rec) => rec.iter().any(|(_, tp)| tp.contains_tp(target)),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, tp)| tp.contains_tp(target))
}
Self::Lambda(lambda) => lambda.body.iter().any(|tp| tp.contains_tp(target)),
Self::UnaryOp { val, .. } => val.contains_tp(target),
Self::BinOp { lhs, rhs, .. } => lhs.contains_tp(target) || rhs.contains_tp(target),
@ -1302,11 +1312,12 @@ impl TyParam {
Self::Array(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.contains_tp(self)),
Self::UnsizedArray(elem) => elem.contains_tp(self),
Self::Set(ts) => ts.iter().any(|t| t.contains_tp(self)),
Self::Record(rec) => rec.iter().any(|(_, t)| t.contains_tp(self)),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, t)| t.contains_tp(self))
}
Self::Dict(ts) => ts
.iter()
.any(|(k, v)| k.contains_tp(self) || v.contains_tp(self)),
Self::DataClass { fields, .. } => fields.iter().any(|(_, t)| t.contains_tp(self)),
Self::Type(t) => t.contains_tp(self),
Self::Value(ValueObj::Type(t)) => t.typ().contains_tp(self),
Self::Erased(t) => t.contains_tp(self),
@ -1334,7 +1345,11 @@ impl TyParam {
}
Self::Type(t) => t.has_unbound_var(),
Self::Proj { obj, .. } => obj.has_unbound_var(),
Self::ProjCall { obj, args, .. } => {
obj.has_unbound_var() || args.iter().any(|t| t.has_unbound_var())
}
Self::Array(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.has_unbound_var()),
Self::UnsizedArray(elem) => elem.has_unbound_var(),
Self::Set(ts) => ts.iter().any(|t| t.has_unbound_var()),
Self::Dict(kv) => kv
.iter()
@ -1361,7 +1376,11 @@ impl TyParam {
Self::FreeVar(fv) => fv.is_undoable_linked(),
Self::Type(t) => t.has_undoable_linked_var(),
Self::Proj { obj, .. } => obj.has_undoable_linked_var(),
Self::ProjCall { obj, args, .. } => {
obj.has_undoable_linked_var() || args.iter().any(|t| t.has_undoable_linked_var())
}
Self::Array(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.has_undoable_linked_var()),
Self::UnsizedArray(elem) => elem.has_undoable_linked_var(),
Self::Set(ts) => ts.iter().any(|t| t.has_undoable_linked_var()),
Self::Dict(kv) => kv
.iter()
@ -1386,9 +1405,13 @@ impl TyParam {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().union_size(),
Self::Type(t) => t.union_size(),
Self::Proj { obj, .. } => obj.union_size(),
Self::ProjCall { obj, args, .. } => obj
.union_size()
.max(args.iter().map(|t| t.union_size()).max().unwrap_or(1)),
Self::Array(ts) | Self::Tuple(ts) => {
ts.iter().map(|t| t.union_size()).max().unwrap_or(1)
}
Self::UnsizedArray(elem) => elem.union_size(),
Self::Set(ts) => ts.iter().map(|t| t.union_size()).max().unwrap_or(1),
Self::Dict(kv) => kv
.iter()
@ -1797,6 +1820,7 @@ impl TyParam {
t.dereference();
}
}
Self::UnsizedArray(elem) => elem.dereference(),
Self::Set(ts) => {
let ts_ = std::mem::take(ts);
*ts = ts_