fix: undo leak bug & sub-unification bugs

This commit is contained in:
Shunsuke Shibayama 2023-08-22 21:45:25 +09:00
parent 97afccb94a
commit 3724a74649
8 changed files with 211 additions and 117 deletions

View file

@ -1,3 +1,5 @@
use std::fmt;
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum Triple<T, E> {
Ok(T),
@ -5,6 +7,16 @@ pub enum Triple<T, E> {
None,
}
impl<T: fmt::Display, E: fmt::Display> fmt::Display for Triple<T, E> {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match self {
Triple::Ok(ok) => write!(f, "Ok({ok})"),
Triple::Err(err) => write!(f, "Err({err})"),
Triple::None => write!(f, "None"),
}
}
}
impl<T, E> Triple<T, E> {
pub fn none_then(self, err: E) -> Result<T, E> {
match self {

View file

@ -7,6 +7,7 @@ use erg_common::error::Location;
#[allow(unused)]
use erg_common::log;
use erg_common::set::Set;
use erg_common::shared::Shared;
use erg_common::traits::{Locational, Stream};
use erg_common::{dict, fmt_vec, fn_name, option_enum_unwrap, set, Triple};
use erg_common::{ArcArray, Str};
@ -22,7 +23,7 @@ use crate::ty::constructors::{
array_t, dict_t, mono, named_free_var, poly, proj, proj_call, ref_, ref_mut, refinement, set_t,
subr_t, tp_enum, tuple_t, v_enum,
};
use crate::ty::free::{Constraint, FreeTyVar, HasLevel};
use crate::ty::free::{Constraint, HasLevel};
use crate::ty::typaram::{OpKind, TyParam};
use crate::ty::value::{GenTypeObj, TypeObj, ValueObj};
use crate::ty::{ConstSubr, HasType, Predicate, SubrKind, Type, UserConstSubr, ValueArgs};
@ -92,27 +93,52 @@ fn op_to_name(op: OpKind) -> &'static str {
}
}
#[derive(Debug)]
pub struct Substituter<'c> {
ctx: &'c Context,
qt: Type,
#[allow(unused)]
st: Type,
child: Option<Box<Substituter<'c>>>,
#[derive(Debug, Default)]
pub struct UndoableLinkedList {
tys: Shared<Set<Type>>,
tps: Shared<Set<TyParam>>,
}
impl Drop for Substituter<'_> {
impl Drop for UndoableLinkedList {
fn drop(&mut self) {
Self::undo_substitute_typarams(&self.qt);
for t in self.tys.borrow().iter() {
t.undo();
}
for tp in self.tps.borrow().iter() {
tp.undo();
}
}
}
impl UndoableLinkedList {
pub fn new() -> Self {
Self {
tys: Shared::new(set! {}),
tps: Shared::new(set! {}),
}
}
pub fn push_t(&self, t: &Type) {
self.tys.borrow_mut().insert(t.clone());
}
pub fn push_tp(&self, tp: &TyParam) {
self.tps.borrow_mut().insert(tp.clone());
}
}
#[derive(Debug)]
pub struct Substituter<'c> {
ctx: &'c Context,
undoable_linked: UndoableLinkedList,
child: Option<Box<Substituter<'c>>>,
}
impl<'c> Substituter<'c> {
fn new(ctx: &'c Context, qt: Type, st: Type) -> Self {
fn new(ctx: &'c Context) -> Self {
Self {
ctx,
qt,
st,
undoable_linked: UndoableLinkedList::new(),
child: None,
}
}
@ -142,7 +168,7 @@ impl<'c> Substituter<'c> {
log!(err "[{}] [{}]", erg_common::fmt_vec(&qtps), erg_common::fmt_vec(&stps));
return Ok(None); // TODO: e.g. Sub(Int) / Eq and Sub(?T)
}
let mut self_ = Self::new(ctx, qt.clone(), st.clone());
let mut self_ = Self::new(ctx);
let mut errs = EvalErrors::empty();
for (qtp, stp) in qtps.into_iter().zip(stps.into_iter()) {
if let Err(err) = self_.substitute_typaram(qtp, stp) {
@ -171,7 +197,7 @@ impl<'c> Substituter<'c> {
log!(err "[{}] [{}]", erg_common::fmt_vec(&qtps), erg_common::fmt_vec(&stps));
return Ok(None); // TODO: e.g. Sub(Int) / Eq and Sub(?T)
}
let mut self_ = Self::new(ctx, qt.clone(), st.clone());
let mut self_ = Self::new(ctx);
let mut errs = EvalErrors::empty();
for (qtp, stp) in qtps.into_iter().zip(stps.into_iter()) {
if let Err(err) = self_.overwrite_typaram(qtp, stp) {
@ -188,7 +214,7 @@ impl<'c> Substituter<'c> {
fn substitute_typaram(&mut self, qtp: TyParam, stp: TyParam) -> EvalResult<()> {
match qtp {
TyParam::FreeVar(ref fv) if fv.is_generalized() => {
qtp.undoable_link(&stp);
qtp.undoable_link(&stp, &self.undoable_linked);
/*if let Err(errs) = self.sub_unify_tp(&stp, &qtp, None, &(), false) {
log!(err "{errs}");
}*/
@ -226,13 +252,13 @@ impl<'c> Substituter<'c> {
)
})?;
if !qt.is_undoable_linked_var() && qt.is_generalized() && qt.is_free_var() {
qt.undoable_link(&st);
qt.undoable_link(&st, &self.undoable_linked);
} else if qt.is_undoable_linked_var() && qt != st {
// e.g. Array(T, N) <: Add(Array(T, M))
// Array((Int), (3)) <: Add(Array((Int), (4))): OK
// Array((Int), (3)) <: Add(Array((Str), (4))): NG
if let Some(union) = self.ctx.unify(&qt, &st) {
qt.undoable_link(&union);
qt.undoable_link(&union, &self.undoable_linked);
} else {
return Err(EvalError::unification_error(
self.ctx.cfg.input.clone(),
@ -257,7 +283,10 @@ impl<'c> Substituter<'c> {
} else {
qt
};
if let Err(errs) = self.ctx.undoable_sub_unify(&st, &qt, &(), None) {
if let Err(errs) = self
.ctx
.undoable_sub_unify(&st, &qt, &(), &self.undoable_linked, None)
{
log!(err "{errs}");
}
Ok(())
@ -266,7 +295,7 @@ impl<'c> Substituter<'c> {
fn overwrite_typaram(&mut self, qtp: TyParam, stp: TyParam) -> EvalResult<()> {
match qtp {
TyParam::FreeVar(ref fv) if fv.is_undoable_linked() => {
qtp.undoable_link(&stp);
qtp.undoable_link(&stp, &self.undoable_linked);
/*if let Err(errs) = self.sub_unify_tp(&stp, &qtp, None, &(), false) {
log!(err "{errs}");
}*/
@ -276,7 +305,7 @@ impl<'c> Substituter<'c> {
// Whether this could be a problem is under consideration.
// e.g. `T` of Array(T, N) <: Add(T, M)
TyParam::FreeVar(ref fv) if fv.is_generalized() => {
qtp.undoable_link(&stp);
qtp.undoable_link(&stp, &self.undoable_linked);
/*if let Err(errs) = self.sub_unify_tp(&stp, &qtp, None, &(), false) {
log!(err "{errs}");
}*/
@ -314,7 +343,7 @@ impl<'c> Substituter<'c> {
)
})?;
if qt.is_undoable_linked_var() {
qt.undoable_link(&st);
qt.undoable_link(&st, &self.undoable_linked);
}
if !st.is_unbound_var() || !st.is_generalized() {
self.child = Self::overwrite_typarams(self.ctx, &qt, &st)?.map(Box::new);
@ -325,42 +354,15 @@ impl<'c> Substituter<'c> {
} else {
qt
};
if let Err(errs) = self.ctx.undoable_sub_unify(&st, &qt, &(), None) {
if let Err(errs) = self
.ctx
.undoable_sub_unify(&st, &qt, &(), &self.undoable_linked, None)
{
log!(err "{errs}");
}
Ok(())
}
fn undo_substitute_typarams(substituted_q: &Type) {
for tp in substituted_q.typarams().into_iter() {
Self::undo_substitute_typaram(tp);
}
}
fn undo_substitute_typaram(substituted_q_tp: TyParam) {
match substituted_q_tp {
TyParam::FreeVar(fv) if fv.is_undoable_linked() => fv.undo(),
TyParam::Type(t) if t.is_free_var() => {
let Ok(subst) = <&FreeTyVar>::try_from(t.as_ref()) else { unreachable!() };
if subst.is_undoable_linked() {
subst.undo();
}
}
/*TyParam::Type(t) => {
Self::undo_substitute_typarams(&t);
}
TyParam::Value(ValueObj::Type(t)) => {
Self::undo_substitute_typarams(t.typ());
}
TyParam::App { args, .. } => {
for arg in args.into_iter() {
Self::undo_substitute_typaram(arg);
}
}*/
_ => {}
}
}
/// ```erg
/// substitute_self(Iterable('Self), Int)
/// -> Iterable(Int)
@ -372,8 +374,9 @@ impl<'c> Substituter<'c> {
&& t.get_super()
.is_some_and(|sup| ctx.supertype_of(&sup, subtype))
{
t.undoable_link(subtype);
return Some(Self::new(ctx, qt.clone(), subtype.clone()));
let mut _self = Self::new(ctx);
t.undoable_link(subtype, &_self.undoable_linked);
return Some(_self);
}
}
None
@ -2173,7 +2176,7 @@ impl Context {
let proj = proj_call(coerced, attr_name, args);
self.eval_t_params(proj, level, t_loc)
.map(|t| {
lhs.coerce();
lhs.destructive_coerce();
t
})
.map_err(|(_, errs)| errs)

View file

@ -21,7 +21,7 @@ use crate::{feature_error, hir};
use Type::*;
use Variance::*;
use super::eval::Substituter;
use super::eval::{Substituter, UndoableLinkedList};
pub struct Generalizer {
level: usize,
@ -557,21 +557,29 @@ impl<'c, 'q, 'l, L: Locational> Dereferencer<'c, 'q, 'l, L> {
// we need to force linking to avoid infinite loop
// e.g. fv == ?T(<: Int, :> Add(?T))
// fv == ?T(:> ?T.Output, <: Add(Int))
let list = UndoableLinkedList::new();
let fv_t = Type::FreeVar(fv.clone());
match (sub_t.contains_type(&fv_t), super_t.contains_type(&fv_t)) {
let dummy = match (sub_t.contains_type(&fv_t), super_t.contains_type(&fv_t)) {
// REVIEW: to prevent infinite recursion, but this may cause a nonsense error
(true, true) => {
fv.dummy_link();
true
}
(true, false) => {
fv_t.undoable_link(&super_t);
fv_t.undoable_link(&super_t, &list);
false
}
(false, true | false) => {
fv_t.undoable_link(&sub_t);
fv_t.undoable_link(&sub_t, &list);
false
}
}
};
let res = self.validate_subsup(sub_t, super_t);
fv.undo();
if dummy {
fv.undo();
} else {
drop(list);
}
match res {
Ok(ty) => {
// TODO: T(:> Nat <: Int) -> T(:> Nat, <: Int) ==> Int -> Nat

View file

@ -4,8 +4,7 @@ use std::mem;
use erg_common::dict::Dict;
#[allow(unused_imports)]
use erg_common::log;
use erg_common::{dict, Str};
use erg_common::{enum_unwrap, set};
use erg_common::{dict, enum_unwrap, set};
use crate::context::Context;
use crate::feature_error;
@ -482,12 +481,16 @@ pub(crate) fn __named_tuple_getitem__(
}
/// `NamedTuple({ .x = Int; .y = Str }).union() == Int or Str`
/// `GenericNamedTuple.union() == Obj`
pub(crate) fn named_tuple_union(mut args: ValueArgs, ctx: &Context) -> EvalValueResult<TyParam> {
let slf = args
.remove_left_or_key("Self")
.ok_or_else(|| not_passed("Self"))?;
let fields = match ctx.convert_value_into_type(slf) {
Ok(Type::NamedTuple(fields)) => fields,
Ok(Type::Mono(n)) if &n == "GenericNamedTuple" => {
return Ok(ValueObj::builtin_type(Type::Obj).into());
}
Ok(other) => {
return Err(type_mismatch("NamedTuple", other, "Self"));
}
@ -509,7 +512,7 @@ pub(crate) fn as_dict(mut args: ValueArgs, ctx: &Context) -> EvalValueResult<TyP
.ok_or_else(|| not_passed("Self"))?;
let fields = match ctx.convert_value_into_type(slf) {
Ok(Type::Record(fields)) => fields,
Ok(Type::Mono(Str::Static("Record"))) => {
Ok(Type::Mono(n)) if &n == "Record" => {
let dict = dict! { Type::Obj => Type::Obj };
return Ok(ValueObj::builtin_type(Type::from(dict)).into());
}

View file

@ -765,7 +765,7 @@ impl Context {
for ctx in ctxs {
match ctx.rec_get_var_info(ident, AccessKind::BoundAttr, input, namespace) {
Triple::Ok(vi) => {
obj.ref_t().coerce();
obj.ref_t().destructive_coerce();
return Triple::Ok(vi);
}
Triple::Err(e) => {
@ -1133,7 +1133,7 @@ impl Context {
.map_err(|mut errs| errs.remove(0))?;
if &coerced != obj.ref_t() {
let hash = get_hash(obj.ref_t());
obj.ref_t().coerce();
obj.ref_t().destructive_coerce();
if get_hash(obj.ref_t()) != hash {
return self
.search_method_info(obj, attr_name, pos_args, kw_args, input, namespace);
@ -1392,7 +1392,7 @@ impl Context {
}
if sub != Never {
let hash = get_hash(instance);
instance.coerce();
instance.destructive_coerce();
if instance.is_quantified_subr() {
let instance = self.instantiate(instance.clone(), obj)?;
self.substitute_call(obj, attr_name, &instance, pos_args, kw_args)?;

View file

@ -23,17 +23,23 @@ use Predicate as Pred;
use Type::*;
use ValueObj::{Inf, NegInf};
use super::eval::UndoableLinkedList;
use super::initialize::const_func::sub_tpdict_get;
pub struct Unifier<'c, 'l, L: Locational> {
pub struct Unifier<'c, 'l, 'u, L: Locational> {
ctx: &'c Context,
loc: &'l L,
undoable: bool,
undoable: Option<&'u UndoableLinkedList>,
param_name: Option<Str>,
}
impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
pub fn new(ctx: &'c Context, loc: &'l L, undoable: bool, param_name: Option<Str>) -> Self {
impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
pub fn new(
ctx: &'c Context,
loc: &'l L,
undoable: Option<&'u UndoableLinkedList>,
param_name: Option<Str>,
) -> Self {
Self {
ctx,
loc,
@ -43,7 +49,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
}
}
impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
/// ```erg
/// occur(?T, ?T) ==> OK
/// occur(X -> ?T, ?T) ==> Error
@ -645,7 +651,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
/// sub_unify([?T; 0], Mutate): (/* OK */)
/// ```
fn sub_unify(&self, maybe_sub: &Type, maybe_sup: &Type) -> TyCheckResult<()> {
log!(info "trying sub_unify:\nmaybe_sub: {maybe_sub}\nmaybe_sup: {maybe_sup}");
log!(info "trying {}sub_unify:\nmaybe_sub: {maybe_sub}\nmaybe_sup: {maybe_sup}", self.undoable.map_or("", |_| "undoable"));
// In this case, there is no new information to be gained
// この場合、特に新しく得られる情報はない
if maybe_sub == &Type::Never || maybe_sup == &Type::Obj || maybe_sup == maybe_sub {
@ -939,7 +945,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
// * sub_unify(Bool, ?T(<: Bool or Y)): (?T == Bool)
// * sub_unify(Float, ?T(<: Structural{ .imag = ?U })) ==> ?U == Float
if let Some((sub, mut sup)) = sup_fv.get_subsup() {
if sup.is_structural() {
if sup.is_structural() || !sup.is_recursive() {
self.sub_unify(maybe_sub, &sup)?;
}
let new_sub = self.ctx.union(maybe_sub, &sub);
@ -951,7 +957,9 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
{
let (l, r) = new_sub.union_pair().unwrap_or((maybe_sub.clone(), sub));
let unified = self.unify(&l, &r);
if unified.is_none() {
if let Some(unified) = unified {
log!("unify({l}, {r}) == {unified}");
} else {
let maybe_sub = self.ctx.readable_type(maybe_sub.clone());
let new_sub = self.ctx.readable_type(new_sub);
return Err(TyCheckErrors::from(
@ -989,7 +997,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
if let Some((_, sub_ty)) = sub_fields.get_key_value(&sup_field) {
self.sub_unify(sub_ty, &sup_ty)?;
} else if !self.ctx.subtype_of(&sub_fv.get_sub().unwrap(), &Never) {
maybe_sub.coerce();
maybe_sub.coerce(self.undoable);
return self.sub_unify(maybe_sub, maybe_sup);
} else {
// e.g. ?T / Structural({ .method = (self: ?T) -> Int })
@ -1371,6 +1379,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
}
}
if let Some(sup_ty) = min_compatible {
let _substituter = Substituter::substitute_self(sup_ty, maybe_sub, self.ctx);
let sub_instance = self.ctx.instantiate_def_type(sup_ty)?;
let variances = self
.ctx
@ -1402,17 +1411,27 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
/// Unify two types into a single type based on the subtype relation.
///
/// Error if they can't unify without upcasting both types (derefining is allowed) or using the Or type
/// Error if they can't unify without upcasting both types (derefining is allowed) or using Or types
/// ```erg
/// unify(Int, Nat) == Some(Int)
/// unify(Int, Str) == None
/// unify({1.2}, Nat) == Some(Float)
/// unify(Nat, Int!) == Some(Int)
/// unify(Eq, Int) == None
/// unify(Int or Str, Int) == Some(Int or Str)
/// unify(Int or Str, NoneType) == None
/// ```
fn unify(&self, lhs: &Type, rhs: &Type) -> Option<Type> {
#[allow(clippy::single_match)]
match (lhs, rhs) {
(Type::Or(l, r), other) | (other, Type::Or(l, r)) => {
if let Some(t) = self.unify(l, other) {
return self.unify(&t, l);
} else if let Some(t) = self.unify(r, other) {
return self.unify(&t, l);
}
return None;
}
(Type::FreeVar(fv), _) if fv.is_linked() => return self.unify(&fv.crack(), rhs),
(_, Type::FreeVar(fv)) if fv.is_linked() => return self.unify(lhs, &fv.crack()),
// TODO: unify(?T, ?U) ?
@ -1459,7 +1478,7 @@ impl Context {
maybe_sup: &Type,
loc: &impl Locational,
) -> TyCheckResult<()> {
let unifier = Unifier::new(self, loc, false, None);
let unifier = Unifier::new(self, loc, None, None);
unifier.occur(maybe_sub, maybe_sup)
}
@ -1471,7 +1490,7 @@ impl Context {
loc: &impl Locational,
is_structural: bool,
) -> TyCheckResult<()> {
let unifier = Unifier::new(self, loc, is_structural, None);
let unifier = Unifier::new(self, loc, None, None);
unifier.sub_unify_tp(maybe_sub, maybe_sup, variance, is_structural)
}
@ -1482,7 +1501,7 @@ impl Context {
loc: &impl Locational,
param_name: Option<&Str>,
) -> TyCheckResult<()> {
let unifier = Unifier::new(self, loc, false, param_name.cloned());
let unifier = Unifier::new(self, loc, None, param_name.cloned());
unifier.sub_unify(maybe_sub, maybe_sup)
}
@ -1491,14 +1510,15 @@ impl Context {
maybe_sub: &Type,
maybe_sup: &Type,
loc: &impl Locational,
list: &UndoableLinkedList,
param_name: Option<&Str>,
) -> TyCheckResult<()> {
let unifier = Unifier::new(self, loc, true, param_name.cloned());
let unifier = Unifier::new(self, loc, Some(list), param_name.cloned());
unifier.sub_unify(maybe_sub, maybe_sup)
}
pub(crate) fn unify(&self, lhs: &Type, rhs: &Type) -> Option<Type> {
let unifier = Unifier::new(self, &(), false, None);
let unifier = Unifier::new(self, &(), None, None);
unifier.unify(lhs, rhs)
}
}

View file

@ -43,6 +43,8 @@ pub use value::ValueObj;
use value::ValueObj::{Inf, NegInf};
pub use vis::*;
use crate::context::eval::UndoableLinkedList;
use self::constructors::{bounded, free_var, named_free_var, proj_call, subr_t};
pub const STR_OMIT_THRESHOLD: usize = 16;
@ -2558,25 +2560,25 @@ impl Type {
/// ```erg
/// ?T(:> ?U(:> Int)).coerce(): ?T == ?U == Int
/// ```
pub fn coerce(&self) {
pub fn destructive_coerce(&self) {
match self {
Type::FreeVar(fv) if fv.is_linked() => {
fv.crack().coerce();
fv.crack().destructive_coerce();
}
Type::FreeVar(fv) if fv.is_unbound() => {
let (sub, _sup) = fv.get_subsup().unwrap();
sub.coerce();
sub.destructive_coerce();
self.destructive_link(&sub);
}
Type::And(l, r) | Type::Or(l, r) => {
l.coerce();
r.coerce();
l.destructive_coerce();
r.destructive_coerce();
}
Type::Not(l) => l.coerce(),
Type::Not(l) => l.destructive_coerce(),
Type::Poly { params, .. } => {
for p in params {
if let Ok(t) = <&Type>::try_from(p) {
t.coerce();
t.destructive_coerce();
}
}
}
@ -2584,6 +2586,40 @@ impl Type {
}
}
pub fn undoable_coerce(&self, list: &UndoableLinkedList) {
match self {
Type::FreeVar(fv) if fv.is_linked() => {
fv.crack().undoable_coerce(list);
}
Type::FreeVar(fv) if fv.is_unbound() => {
let (sub, _sup) = fv.get_subsup().unwrap();
sub.undoable_coerce(list);
self.undoable_link(&sub, list);
}
Type::And(l, r) | Type::Or(l, r) => {
l.undoable_coerce(list);
r.undoable_coerce(list);
}
Type::Not(l) => l.undoable_coerce(list),
Type::Poly { params, .. } => {
for p in params {
if let Ok(t) = <&Type>::try_from(p) {
t.undoable_coerce(list);
}
}
}
_ => {}
}
}
pub fn coerce(&self, list: Option<&UndoableLinkedList>) {
if let Some(list) = list {
self.undoable_coerce(list);
} else {
self.destructive_coerce();
}
}
pub fn qvars(&self) -> Set<(Str, Constraint)> {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.unsafe_crack().qvars(),
@ -3327,21 +3363,22 @@ impl Type {
/// interior-mut
///
/// `inc/dec_undo_count` due to the number of `substitute_typarams/undo_typarams` must be matched
pub(crate) fn undoable_link(&self, to: &Type) {
pub(crate) fn undoable_link(&self, to: &Type, list: &UndoableLinkedList) {
list.push_t(self);
if self.addr_eq(to) {
self.inc_undo_count();
return;
}
match self {
Self::FreeVar(fv) => fv.undoable_link(to),
Self::Refinement(refine) => refine.t.undoable_link(to),
Self::Refinement(refine) => refine.t.undoable_link(to, list),
_ => panic!("{self} is not a free variable"),
}
}
pub(crate) fn link(&self, to: &Type, undoable: bool) {
if undoable {
self.undoable_link(to);
pub(crate) fn link(&self, to: &Type, list: Option<&UndoableLinkedList>) {
if let Some(list) = list {
self.undoable_link(to, list);
} else {
self.destructive_link(to);
}
@ -3350,7 +3387,7 @@ impl Type {
pub(crate) fn undo(&self) {
match self {
Self::FreeVar(fv) if fv.is_undoable_linked() => fv.undo(),
Self::FreeVar(fv) if fv.constraint_is_sandwiched() => {
/*Self::FreeVar(fv) if fv.constraint_is_sandwiched() => {
let (sub, sup) = fv.get_subsup().unwrap();
sub.undo();
sup.undo();
@ -3359,29 +3396,33 @@ impl Type {
for param in params {
param.undo();
}
}
}*/
_ => {}
}
}
pub(crate) fn undoable_update_constraint(&self, new_constraint: Constraint) {
pub(crate) fn undoable_update_constraint(
&self,
new_constraint: Constraint,
list: &UndoableLinkedList,
) {
let level = self.level().unwrap();
let new = if let Some(name) = self.unbound_name() {
named_free_var(name, level, new_constraint)
} else {
free_var(level, new_constraint)
};
self.undoable_link(&new);
self.undoable_link(&new, list);
}
pub(crate) fn update_constraint(
&self,
new_constraint: Constraint,
undoable: bool,
list: Option<&UndoableLinkedList>,
in_instantiation: bool,
) {
if undoable {
self.undoable_update_constraint(new_constraint);
if let Some(list) = list {
self.undoable_update_constraint(new_constraint, list);
} else {
self.destructive_update_constraint(new_constraint, in_instantiation);
}

View file

@ -11,6 +11,8 @@ use erg_common::{dict, log, ref_addr_eq, set, Str};
use erg_parser::ast::ConstLambda;
use erg_parser::token::TokenKind;
use crate::context::eval::UndoableLinkedList;
use super::constructors::int_interval;
use super::free::{
CanbeFree, Constraint, FreeKind, FreeTyParam, FreeTyVar, HasLevel, Level, GENERIC_LEVEL,
@ -1090,13 +1092,13 @@ impl TyParam {
}
}
pub fn coerce(&self) {
pub fn destructive_coerce(&self) {
match self {
TyParam::FreeVar(fv) if fv.is_linked() => {
fv.crack().coerce();
fv.crack().destructive_coerce();
}
TyParam::Type(t) => t.coerce(),
TyParam::Value(ValueObj::Type(t)) => t.typ().coerce(),
TyParam::Type(t) => t.destructive_coerce(),
TyParam::Value(ValueObj::Type(t)) => t.typ().destructive_coerce(),
_ => {}
}
}
@ -1398,7 +1400,8 @@ impl TyParam {
}
/// interior-mut
pub(crate) fn undoable_link(&self, to: &TyParam) {
pub(crate) fn undoable_link(&self, to: &TyParam, list: &UndoableLinkedList) {
list.push_tp(self);
if self.addr_eq(to) {
self.inc_undo_count();
return;
@ -1409,9 +1412,9 @@ impl TyParam {
}
}
pub(crate) fn link(&self, to: &TyParam, undoable: bool) {
if undoable {
self.undoable_link(to);
pub(crate) fn link(&self, to: &TyParam, list: Option<&UndoableLinkedList>) {
if let Some(list) = list {
self.undoable_link(to, list);
} else {
self.destructive_link(to);
}
@ -1422,33 +1425,37 @@ impl TyParam {
Self::FreeVar(fv) if fv.is_undoable_linked() => fv.undo(),
Self::Type(t) => t.undo(),
Self::Value(ValueObj::Type(t)) => t.typ().undo(),
Self::App { args, .. } => {
/*Self::App { args, .. } => {
for arg in args {
arg.undo();
}
}
}*/
_ => {}
}
}
pub(crate) fn undoable_update_constraint(&self, new_constraint: Constraint) {
pub(crate) fn undoable_update_constraint(
&self,
new_constraint: Constraint,
list: &UndoableLinkedList,
) {
let level = self.level().unwrap();
let new = if let Some(name) = self.unbound_name() {
Self::named_free_var(name, level, new_constraint)
} else {
Self::free_var(level, new_constraint)
};
self.undoable_link(&new);
self.undoable_link(&new, list);
}
pub(crate) fn update_constraint(
&self,
new_constraint: Constraint,
undoable: bool,
list: Option<&UndoableLinkedList>,
in_instantiation: bool,
) {
if undoable {
self.undoable_update_constraint(new_constraint);
if let Some(list) = list {
self.undoable_update_constraint(new_constraint, list);
} else {
self.destructive_update_constraint(new_constraint, in_instantiation);
}