refactor: Type::update_constraint

This commit is contained in:
Shunsuke Shibayama 2023-08-07 01:08:59 +09:00
parent a690e0b61a
commit b7ca9a16f3
4 changed files with 23 additions and 29 deletions

View file

@ -313,7 +313,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
.is_sub_constraint_of(&sub_fv.constraint().unwrap(), &new_constraint)
|| sub_fv.constraint().unwrap().get_type() == Some(&Type)
{
maybe_sub.replace_constraint(new_constraint, self.undoable, false);
maybe_sub.update_constraint(new_constraint, self.undoable, false);
}
} else {
maybe_sub.link(sup_tp, self.undoable);
@ -353,7 +353,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
.is_sub_constraint_of(&sup_fv.constraint().unwrap(), &new_constraint)
|| sup_fv.constraint().unwrap().get_type() == Some(&Type)
{
maybe_sup.replace_constraint(new_constraint, self.undoable, false);
maybe_sup.update_constraint(new_constraint, self.undoable, false);
}
} else {
maybe_sup.link(sub_tp, self.undoable);
@ -594,7 +594,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
let pred = Predicate::ge(FRESH_GEN.fresh_varname(), evaled);
let new_type = self.ctx.type_from_pred(pred);
let new_constr = Constraint::new_type_of(Type::from(new_type));
target.replace_constraint(new_constr, self.undoable, false);
target.update_constraint(new_constr, self.undoable, false);
}
Ok(())
}
@ -777,20 +777,20 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
.cmp(&sup_fv.level().unwrap_or(GENERIC_LEVEL))
{
std::cmp::Ordering::Less => {
maybe_sub.replace_constraint(new_constraint, self.undoable, false);
maybe_sub.update_constraint(new_constraint, self.undoable, false);
maybe_sup.link(maybe_sub, self.undoable);
}
std::cmp::Ordering::Greater => {
maybe_sup.replace_constraint(new_constraint, self.undoable, false);
maybe_sup.update_constraint(new_constraint, self.undoable, false);
maybe_sub.link(maybe_sup, self.undoable);
}
std::cmp::Ordering::Equal => {
// choose named one
if sup_fv.is_named_unbound() {
maybe_sup.replace_constraint(new_constraint, self.undoable, false);
maybe_sup.update_constraint(new_constraint, self.undoable, false);
maybe_sub.link(maybe_sup, self.undoable);
} else {
maybe_sup.replace_constraint(new_constraint, self.undoable, false);
maybe_sup.update_constraint(new_constraint, self.undoable, false);
maybe_sup.link(maybe_sub, self.undoable);
}
}
@ -869,7 +869,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
maybe_sup.link(&union, self.undoable);
} else {
let new_constraint = Constraint::new_sandwiched(union, intersec);
maybe_sup.replace_constraint(new_constraint, self.undoable, false);
maybe_sup.update_constraint(new_constraint, self.undoable, false);
}
}
// (Int or ?T) <: (?U or Int)
@ -955,14 +955,14 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
maybe_sup.link(&new_sub, self.undoable); // Bool <: ?T <: Bool or Y ==> ?T == Bool
} else {
let constr = Constraint::new_sandwiched(new_sub, mem::take(&mut sup));
maybe_sup.replace_constraint(constr, self.undoable, true);
maybe_sup.update_constraint(constr, self.undoable, true);
}
}
// sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)
else if let Some(ty) = sup_fv.get_type() {
if self.ctx.supertype_of(&Type, &ty) {
let constr = Constraint::new_supertype_of(maybe_sub.clone());
maybe_sup.replace_constraint(constr, self.undoable, true);
maybe_sup.update_constraint(constr, self.undoable, true);
} else {
todo!("{maybe_sub} <: {maybe_sup}")
}
@ -1022,14 +1022,14 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
maybe_sub.link(&sub, self.undoable);
} else {
let constr = Constraint::new_sandwiched(sub, new_sup);
maybe_sub.replace_constraint(constr, self.undoable, true);
maybe_sub.update_constraint(constr, self.undoable, true);
}
}
// sub_unify(?T(: Type), Int): (?T(<: Int))
else if let Some(ty) = sub_fv.get_type() {
if self.ctx.supertype_of(&Type, &ty) {
let constr = Constraint::new_subtype_of(maybe_sup.clone());
maybe_sub.replace_constraint(constr, self.undoable, true);
maybe_sub.update_constraint(constr, self.undoable, true);
} else {
todo!("{maybe_sub} <: {maybe_sup}")
}

View file

@ -227,7 +227,7 @@ impl Constraint {
pub trait CanbeFree {
fn unbound_name(&self) -> Option<Str>;
fn constraint(&self) -> Option<Constraint>;
fn update_constraint(&self, constraint: Constraint, in_instantiation: bool);
fn destructive_update_constraint(&self, constraint: Constraint, in_instantiation: bool);
}
impl<T: CanbeFree + Send + Clone> Free<T> {
@ -1054,7 +1054,7 @@ impl<T: CanbeFree + Send + Clone> Free<T> {
*constraint = new_constraint;
}
FreeKind::Linked(t) | FreeKind::UndoableLinked { t, .. } => {
t.update_constraint(new_constraint, in_inst_or_gen);
t.destructive_update_constraint(new_constraint, in_inst_or_gen);
}
}
}

View file

@ -1210,7 +1210,7 @@ impl CanbeFree for Type {
}
}
fn update_constraint(&self, new_constraint: Constraint, in_instantiation: bool) {
fn destructive_update_constraint(&self, new_constraint: Constraint, in_instantiation: bool) {
if let Some(fv) = self.as_free() {
fv.update_constraint(new_constraint, in_instantiation);
}
@ -3221,7 +3221,7 @@ impl Type {
self.undoable_link(&new);
}
pub(crate) fn replace_constraint(
pub(crate) fn update_constraint(
&self,
new_constraint: Constraint,
undoable: bool,
@ -3230,7 +3230,7 @@ impl Type {
if undoable {
self.undoable_update_constraint(new_constraint);
} else {
self.update_constraint(new_constraint, in_instantiation);
self.destructive_update_constraint(new_constraint, in_instantiation);
}
}

View file

@ -3,7 +3,6 @@ use std::fmt;
use std::ops::{Add, Div, Mul, Neg, Range, RangeInclusive, Sub};
use std::sync::Arc;
use erg_common::consts::DEBUG_MODE;
use erg_common::dict::Dict;
use erg_common::set::Set;
use erg_common::traits::{LimitedDisplay, StructuralEq};
@ -462,16 +461,17 @@ impl CanbeFree for TyParam {
}
}
fn update_constraint(&self, new_constraint: Constraint, in_instantiation: bool) {
fn destructive_update_constraint(&self, new_constraint: Constraint, in_instantiation: bool) {
match self {
Self::FreeVar(fv) => {
fv.update_constraint(new_constraint, in_instantiation);
}
Self::Type(t) => {
t.update_constraint(new_constraint, in_instantiation);
t.destructive_update_constraint(new_constraint, in_instantiation);
}
Self::Value(ValueObj::Type(ty)) => {
ty.typ().update_constraint(new_constraint, in_instantiation);
ty.typ()
.destructive_update_constraint(new_constraint, in_instantiation);
}
_ => {}
}
@ -1281,12 +1281,6 @@ impl TyParam {
self.inc_undo_count();
return;
}
if to.contains_tp(self) {
if DEBUG_MODE {
panic!("cyclic: {self} / {to}");
}
return;
}
match self {
Self::FreeVar(fv) => fv.undoable_link(to),
_ => panic!("{self} is not a free variable"),
@ -1325,7 +1319,7 @@ impl TyParam {
self.undoable_link(&new);
}
pub(crate) fn replace_constraint(
pub(crate) fn update_constraint(
&self,
new_constraint: Constraint,
undoable: bool,
@ -1334,7 +1328,7 @@ impl TyParam {
if undoable {
self.undoable_update_constraint(new_constraint);
} else {
self.update_constraint(new_constraint, in_instantiation);
self.destructive_update_constraint(new_constraint, in_instantiation);
}
}