Skip to content

Commit

Permalink
chore: relax occur check
Browse files Browse the repository at this point in the history
fix #512
  • Loading branch information
mtshiba committed May 24, 2024
1 parent 559b465 commit cb385a8
Show file tree
Hide file tree
Showing 6 changed files with 73 additions and 31 deletions.
6 changes: 6 additions & 0 deletions crates/els/inlay_hint.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

use erg_common::spawn::safe_yield;
use erg_compiler::erg_parser::parse::Parsable;
use erg_compiler::hir::GuardClause;
use erg_compiler::varinfo::AbsLocation;
use lsp_types::InlayHintLabelPart;
use serde::Deserialize;
Expand Down Expand Up @@ -154,6 +155,11 @@ impl<'s, C: BuildRunnable, P: Parsable> InlayHintGenerator<'s, C, P> {
let hint = self.type_anot(ln_end, col_end, &d_param.sig.vi.t, false);
result.push(hint);
}
for guard in params.guards.iter() {
if let GuardClause::Bind(def) = guard {
result.extend(self.get_var_def_hint(def));
}
}
result
}

Expand Down
68 changes: 41 additions & 27 deletions crates/erg_compiler/context/unify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -66,9 +66,9 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
/// occur(X -> ?T, X -> ?T) ==> OK
/// occur(?T, ?T -> X) ==> Error
/// occur(?T, Option(?T)) ==> Error
/// occur(?T or ?U, ?T) ==> OK
/// occur(?T or Int, Int or ?T) ==> OK
/// occur(?T(<: Str) or ?U(<: Int), ?T(<: Str)) ==> Error
/// occur(?T(<: ?U or Y), ?U) ==> OK
/// occur(?T, ?T.Output) ==> OK
/// ```
fn occur(&self, maybe_sub: &Type, maybe_sup: &Type) -> TyCheckResult<()> {
Expand Down Expand Up @@ -150,13 +150,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
Ok(())
}*/
(FreeVar(fv), Poly { params, .. }) if fv.is_unbound() => {
for param in params.iter().filter_map(|tp| {
if let TyParam::Type(t) = tp {
Some(t)
} else {
None
}
}) {
for param in params.iter().filter_map(|tp| <&Type>::try_from(tp).ok()) {
self.occur_inner(maybe_sub, param)?;
}
Ok(())
Expand Down Expand Up @@ -192,15 +186,17 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
self.ctx.caused_by(),
)))
} else {
if let Some((sub_t, sup_t)) = sub.get_subsup() {
if let Some((sub_t, _sup_t)) = sub.get_subsup() {
sub.do_avoiding_recursion(|| {
self.occur_inner(&sub_t, maybe_sup)?;
self.occur_inner(&sup_t, maybe_sup)
// occur(?T(<: ?U or Y), ?U) ==> OK
self.occur_inner(&sub_t, maybe_sup)
// self.occur_inner(&sup_t, maybe_sup)
})?;
}
if let Some((sub_t, sup_t)) = sup.get_subsup() {
if let Some((_sub_t, sup_t)) = sup.get_subsup() {
sup.do_avoiding_recursion(|| {
self.occur_inner(maybe_sub, &sub_t)?;
// occur(?U, ?T(:> ?U or Y)) ==> OK
// self.occur_inner(maybe_sub, &sub_t)?;
self.occur_inner(maybe_sub, &sup_t)
})?;
}
Expand Down Expand Up @@ -259,25 +255,13 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
Ok(())
}
(Poly { params, .. }, FreeVar(fv)) if fv.is_unbound() => {
for param in params.iter().filter_map(|tp| {
if let TyParam::Type(t) = tp {
Some(t)
} else {
None
}
}) {
for param in params.iter().filter_map(|tp| <&Type>::try_from(tp).ok()) {
self.occur_inner(param, maybe_sup)?;
}
Ok(())
}
(FreeVar(fv), Poly { params, .. }) if fv.is_unbound() => {
for param in params.iter().filter_map(|tp| {
if let TyParam::Type(t) = tp {
Some(t)
} else {
None
}
}) {
for param in params.iter().filter_map(|tp| <&Type>::try_from(tp).ok()) {
self.occur_inner(maybe_sub, param)?;
}
Ok(())
Expand Down Expand Up @@ -1957,3 +1941,33 @@ impl Context {
unifier.unify(lhs, rhs)
}
}

#[cfg(test)]
mod test {
use crate::context::unify::{mono_q, subtypeof, type_q};
use crate::fn_t;

use super::Type;
use Type::*;

#[test]
fn test_occur() {
let ctx = super::Context::default();
let unifier = super::Unifier::new(&ctx, &(), None, false, None);

assert!(unifier.occur(&Type, &Type).is_ok());
let t = type_q("T");
assert!(unifier.occur(&t, &t).is_ok());
let or_t = t.clone() | Type;
let or2_t = Type | t.clone();
assert!(unifier.occur(&Int, &(Int | Str)).is_ok());
assert!(unifier.occur(&t, &or_t).is_err());
assert!(unifier.occur(&or_t, &or2_t).is_ok());
let subr_t = fn_t!(Type => t.clone());
assert!(unifier.occur(&t, &subr_t).is_err());
assert!(unifier.occur(&subr_t, &subr_t).is_ok());

let u = mono_q("U", subtypeof(t.clone() | Int));
assert!(unifier.occur(&u, &t).is_ok());
}
}
2 changes: 1 addition & 1 deletion crates/erg_compiler/lib/pystd/os.d/__init__.d.er
Original file line number Diff line number Diff line change
Expand Up @@ -422,6 +422,6 @@ The name of the operating system dependent module imported. The following names
topdown := Bool,
onerror := Subroutine,
followlinks := Bool
) => Iterator [Str, [Str; _], [Str; _]]
) => Iterator((Str, [Str; _], [Str; _]),)
.write!: (fd: Nat or FileDescriptor, str: Bytes) => Nat
.writev!: (fd: Nat or FileDescriptor, buffers: Ref(ByteArray!)) => Nat
14 changes: 14 additions & 0 deletions crates/erg_compiler/ty/constructors.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,20 @@ use erg_common::fresh::FRESH_GEN;

use crate::ty::*;

#[macro_export]
macro_rules! fn_t {
($input: expr => $ret: expr) => {
Type::Subr($crate::ty::SubrType::new(
$crate::ty::SubrKind::Func,
vec![$crate::ty::ParamTy::Pos($input)],
None,
vec![],
None,
$ret,
))
};
}

#[inline]
pub fn pos(ty: Type) -> ParamTy {
ParamTy::Pos(ty)
Expand Down
7 changes: 4 additions & 3 deletions crates/erg_compiler/ty/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3637,10 +3637,11 @@ impl Type {
let constraint = Constraint::new_sandwiched(sub.derefine(), sup.derefine());
Self::FreeVar(Free::new_named_unbound(name, level, constraint))
})
} else {
let t = fv.get_type().unwrap().derefine();
let constraint = Constraint::new_type_of(t);
} else if let Some(t) = fv.get_type() {
let constraint = Constraint::new_type_of(t.derefine());
Self::FreeVar(Free::new_named_unbound(name, level, constraint))
} else {
Self::FreeVar(fv.clone())
}
}
Self::Refinement(refine) => refine.t.as_ref().clone(),
Expand Down
7 changes: 7 additions & 0 deletions tests/should_ok/iterator.er
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,10 @@ for! filter(x -> x > 1, 0..3), i =>
assert i > 1
for! map(x -> "\{x}", [1, 2, 3]), s =>
assert str(s) == s

for! enumerate([["aaa"], ["aaaa"]]), ((_, a),) =>
print! a.filter(s -> "a" in s)

os = pyimport "os"
for! os.walk!("assets"), ((path, dirs, files),) =>
print! files.filter(i -> i != "a").to_list()

0 comments on commit cb385a8

Please sign in to comment.