mirror of
https://github.com/erg-lang/erg.git
synced 2025-09-28 04:09:05 +00:00
fix: avoid infinite recursion
This commit is contained in:
Shunsuke Shibayama
parent
429e673d6c
commit
3bef190c6e
3 changed files with 51 additions and 31 deletions
|
|
@ -7,7 +7,7 @@ use erg_common::dict::Dict;
|
|||
use erg_common::set::Set;
|
||||
use erg_common::style::colors::DEBUG_ERROR;
|
||||
use erg_common::traits::StructuralEq;
|
||||
use erg_common::{assume_unreachable, fmt_vec, log, set, set_recursion_limit};
|
||||
use erg_common::{assume_unreachable, fmt_vec, log, set};
|
||||
use erg_common::{Str, Triple};
|
||||
|
||||
use crate::context::eval::UndoableLinkedList;
|
||||
|
|
@ -359,7 +359,6 @@ impl Context {
|
|||
/// 単一化、評価等はここでは行わない、スーパータイプになる **可能性があるか** だけ判定する
|
||||
/// ので、lhsが(未連携)型変数の場合は単一化せずにtrueを返す
|
||||
pub(crate) fn structural_supertype_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||
set_recursion_limit!(false, 128);
|
||||
match (lhs, rhs) {
|
||||
// Proc :> Func if params are compatible
|
||||
// * default params can be omitted (e.g. (Int, x := Int) -> Int <: (Int) -> Int)
|
||||
|
|
@ -937,6 +936,11 @@ impl Context {
|
|||
}
|
||||
}
|
||||
|
||||
/// ```erg
|
||||
/// Int.fields() == { imag: Int, real: Int, abs: (self: Int) -> Nat, ... }
|
||||
/// ?T(<: Int).fields() == Int.fields()
|
||||
/// Structural({ .x = Int }).fields() == { x: Int }
|
||||
/// ```
|
||||
pub fn fields(&self, t: &Type) -> Dict<Field, Type> {
|
||||
match t {
|
||||
Type::FreeVar(fv) if fv.is_linked() => self.fields(&fv.unwrap_linked()),
|
||||
|
|
|
|||
|
|
@ -2,14 +2,13 @@
|
|||
use std::iter::repeat;
|
||||
use std::mem;
|
||||
use std::option::Option;
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
|
||||
use erg_common::consts::DEBUG_MODE;
|
||||
use erg_common::fresh::FRESH_GEN;
|
||||
use erg_common::traits::Locational;
|
||||
use erg_common::Str;
|
||||
#[allow(unused_imports)]
|
||||
use erg_common::{dict, fmt_vec, fn_name, log};
|
||||
use erg_common::{get_hash, set_recursion_limit, Str};
|
||||
|
||||
use crate::context::eval::Substituter;
|
||||
use crate::context::instantiate::TyVarCache;
|
||||
|
|
@ -35,7 +34,6 @@ pub struct Unifier<'c, 'l, 'u, L: Locational> {
|
|||
loc: &'l L,
|
||||
undoable: Option<&'u UndoableLinkedList>,
|
||||
change_generalized: bool,
|
||||
recursion_limit: AtomicUsize,
|
||||
param_name: Option<Str>,
|
||||
}
|
||||
|
||||
|
|
@ -52,7 +50,6 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
|
|||
loc,
|
||||
undoable,
|
||||
change_generalized,
|
||||
recursion_limit: AtomicUsize::new(128),
|
||||
param_name,
|
||||
}
|
||||
}
|
||||
|
|
@ -1037,21 +1034,18 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
|
|||
/// ```
|
||||
fn sub_unify(&self, maybe_sub: &Type, maybe_super: &Type) -> TyCheckResult<()> {
|
||||
log!(info "trying {}sub_unify:\nmaybe_sub: {maybe_sub}\nmaybe_super: {maybe_super}", self.undoable.map_or("", |_| "undoable_"));
|
||||
if self.recursion_limit.fetch_sub(1, Ordering::SeqCst) == 0 {
|
||||
self.recursion_limit.store(128, Ordering::SeqCst);
|
||||
log!(err "recursion limit exceeded: {maybe_sub} / {maybe_super}");
|
||||
return Err(TyCheckError::recursion_limit(
|
||||
self.ctx.cfg.input.clone(),
|
||||
line!() as usize,
|
||||
self.loc.loc(),
|
||||
fn_name!(),
|
||||
line!(),
|
||||
)
|
||||
.into());
|
||||
}
|
||||
set_recursion_limit!(
|
||||
panic,
|
||||
"recursion limit exceed: sub_unify({maybe_sub}, {maybe_super})",
|
||||
128
|
||||
);
|
||||
// In this case, there is no new information to be gained
|
||||
// この場合、特に新しく得られる情報はない
|
||||
if maybe_sub == &Type::Never || maybe_super == &Type::Obj || maybe_super.addr_eq(maybe_sub)
|
||||
if maybe_sub == &Type::Never
|
||||
|| maybe_super == &Type::Obj
|
||||
|| maybe_super.addr_eq(maybe_sub)
|
||||
|| (maybe_sub.has_no_unbound_var()
|
||||
&& maybe_super.has_no_unbound_var()
|
||||
&& maybe_sub == maybe_super)
|
||||
{
|
||||
log!(info "no-op:\nmaybe_sub: {maybe_sub}\nmaybe_super: {maybe_super}");
|
||||
return Ok(());
|
||||
|
|
@ -1481,8 +1475,11 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
|
|||
.inspect_err(|_e| sub_fv.undo())?;
|
||||
} else if !self.ctx.subtype_of(&sub, &Never) {
|
||||
sub_fv.undo();
|
||||
let sub_hash = get_hash(maybe_sub);
|
||||
maybe_sub.coerce(self.undoable);
|
||||
return self.sub_unify(maybe_sub, maybe_super);
|
||||
if get_hash(maybe_sub) != sub_hash {
|
||||
return self.sub_unify(maybe_sub, maybe_super);
|
||||
}
|
||||
} else {
|
||||
// e.g. ?T / Structural({ .method = (self: ?T) -> Int })
|
||||
let constr = Constraint::new_sandwiched(
|
||||
|
|
@ -1518,23 +1515,27 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
|
|||
}
|
||||
let sub = mem::take(&mut sub);
|
||||
// min(L, R) != L and R
|
||||
let new_sup = if let Some(new_sup) = self.ctx.min(&supe, maybe_super).either() {
|
||||
let new_super = if let Some(new_sup) = self.ctx.min(&supe, maybe_super).either()
|
||||
{
|
||||
new_sup.clone()
|
||||
} else {
|
||||
self.ctx.intersection(&supe, maybe_super)
|
||||
};
|
||||
self.sub_unify(&sub, &new_sup)?;
|
||||
if !maybe_sub.is_recursive() && (&sub != maybe_sub || &new_super != maybe_super)
|
||||
{
|
||||
self.sub_unify(&sub, &new_super)?;
|
||||
}
|
||||
// ?T(:> Int, <: Int) ==> ?T == Int
|
||||
// ?T(:> List(Int, 3), <: List(?T, ?N)) ==> ?T == List(Int, 3)
|
||||
// ?T(:> List(Int, 3), <: Indexable(?K, ?V)) ==> ?T(:> List(Int, 3), <: Indexable(0..2, Int))
|
||||
if !sub.is_refinement()
|
||||
&& new_sup.qual_name() == sub.qual_name()
|
||||
&& !new_sup.is_unbound_var()
|
||||
&& new_super.qual_name() == sub.qual_name()
|
||||
&& !new_super.is_unbound_var()
|
||||
&& !sub.is_unbound_var()
|
||||
{
|
||||
maybe_sub.link(&sub, self.undoable);
|
||||
} else {
|
||||
maybe_sub.update_tyvar(sub, new_sup, self.undoable, true);
|
||||
maybe_sub.update_tyvar(sub, new_super, self.undoable, true);
|
||||
}
|
||||
}
|
||||
// sub_unify(?T(: Type), Int): (?T(<: Int))
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ use erg_common::fresh::FRESH_GEN;
|
|||
use erg_common::log;
|
||||
use erg_common::set::Set;
|
||||
use erg_common::traits::{LimitedDisplay, Locational, StructuralEq};
|
||||
use erg_common::{enum_unwrap, fmt_option, ref_addr_eq, set, set_recursion_limit, Str};
|
||||
use erg_common::{enum_unwrap, fmt_option, ref_addr_eq, set, Str};
|
||||
|
||||
use erg_parser::ast::Expr;
|
||||
use erg_parser::token::TokenKind;
|
||||
|
|
@ -1005,7 +1005,7 @@ impl Eq for RefineKind {}
|
|||
/// {_: StrWithLen N | N >= 0}
|
||||
/// {T: (Int, Int) | T.0 >= 0, T.1 >= 0}
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct RefinementType {
|
||||
pub var: Str,
|
||||
pub t: Box<Type>,
|
||||
|
|
@ -1029,6 +1029,24 @@ impl<'a> TryFrom<&'a Type> for &'a RefinementType {
|
|||
}
|
||||
}
|
||||
|
||||
impl PartialEq for RefinementType {
|
||||
fn eq(&self, other: &Self) -> bool {
|
||||
self.t == other.t && *self.pred == other.pred.clone().change_subject_name(self.var.clone())
|
||||
}
|
||||
}
|
||||
|
||||
impl Eq for RefinementType {}
|
||||
|
||||
impl Hash for RefinementType {
|
||||
fn hash<H: Hasher>(&self, state: &mut H) {
|
||||
self.t.hash(state);
|
||||
self.pred
|
||||
.clone()
|
||||
.change_subject_name("%RefinementType::hash".into())
|
||||
.hash(state);
|
||||
}
|
||||
}
|
||||
|
||||
impl LimitedDisplay for RefinementType {
|
||||
fn limited_fmt<W: std::fmt::Write>(&self, f: &mut W, limit: isize) -> std::fmt::Result {
|
||||
if limit == 0 {
|
||||
|
|
@ -3616,8 +3634,6 @@ impl Type {
|
|||
fv.crack().destructive_coerce();
|
||||
}
|
||||
Type::FreeVar(fv) if fv.is_unbound_and_sandwiched() => {
|
||||
// TODO: other way to avoid infinite recursion
|
||||
set_recursion_limit!({}, 128);
|
||||
let (sub, _sup) = fv.get_subsup().unwrap();
|
||||
sub.destructive_coerce();
|
||||
self.destructive_link(&sub);
|
||||
|
|
@ -3684,7 +3700,6 @@ impl Type {
|
|||
}
|
||||
}
|
||||
Type::FreeVar(fv) if fv.is_unbound_and_sandwiched() => {
|
||||
set_recursion_limit!({}, 128);
|
||||
let (sub, _sup) = fv.get_subsup().unwrap();
|
||||
sub.undoable_coerce(list);
|
||||
self.undoable_link(&sub, list);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue