This commit is contained in:
Shunsuke Shibayama 2022-09-05 11:11:57 +09:00
parent 25094efd17
commit fb0d2f5737
7 changed files with 23 additions and 25 deletions

View file

@ -232,7 +232,7 @@ impl Context {
{ {
(Absolutely, true) (Absolutely, true)
} }
(_, Type::FreeVar(fv)) | (Type::FreeVar(fv), _) => match fv.crack_bound_types() { (_, Type::FreeVar(fv)) | (Type::FreeVar(fv), _) => match fv.get_bound_types() {
Some((Type::Never, Type::Obj)) => (Absolutely, true), Some((Type::Never, Type::Obj)) => (Absolutely, true),
_ => (Maybe, false), _ => (Maybe, false),
}, },
@ -335,7 +335,7 @@ impl Context {
/// assert sup_conforms(?E(<: Eq(?R)), base: T, sup_trait: Eq(U)) /// assert sup_conforms(?E(<: Eq(?R)), base: T, sup_trait: Eq(U))
/// ``` /// ```
fn sup_conforms(&self, free: &FreeTyVar, base: &Type, sup_trait: &Type) -> bool { fn sup_conforms(&self, free: &FreeTyVar, base: &Type, sup_trait: &Type) -> bool {
let (_sub, sup) = free.crack_bound_types().unwrap(); let (_sub, sup) = free.get_bound_types().unwrap();
free.forced_undoable_link(base); free.forced_undoable_link(base);
let judge = self.supertype_of(&sup, sup_trait); let judge = self.supertype_of(&sup, sup_trait);
free.undo(); free.undo();
@ -345,7 +345,7 @@ impl Context {
/// assert!(sup_conforms(?E(<: Eq(?E)), {Nat, Eq(Nat)})) /// assert!(sup_conforms(?E(<: Eq(?E)), {Nat, Eq(Nat)}))
/// assert!(sup_conforms(?E(<: Eq(?R)), {Nat, Eq(T)})) /// assert!(sup_conforms(?E(<: Eq(?R)), {Nat, Eq(T)}))
fn _sub_conforms(&self, free: &FreeTyVar, inst_pair: &TraitInstance) -> bool { fn _sub_conforms(&self, free: &FreeTyVar, inst_pair: &TraitInstance) -> bool {
let (_sub, sup) = free.crack_bound_types().unwrap(); let (_sub, sup) = free.get_bound_types().unwrap();
log!(info "{free}"); log!(info "{free}");
free.forced_undoable_link(&inst_pair.sub_type); free.forced_undoable_link(&inst_pair.sub_type);
log!(info "{free}"); log!(info "{free}");
@ -403,8 +403,7 @@ impl Context {
} }
// ?T(<: Nat) !:> ?U(:> Int) // ?T(<: Nat) !:> ?U(:> Int)
// ?T(<: Nat) :> ?U(<: Int) (?U can be smaller than ?T) // ?T(<: Nat) :> ?U(<: Int) (?U can be smaller than ?T)
(FreeVar(lfv), FreeVar(rfv)) => { (FreeVar(lfv), FreeVar(rfv)) => match (lfv.get_bound_types(), rfv.get_bound_types()) {
match (lfv.crack_bound_types(), rfv.crack_bound_types()) {
(Some((_, l_sup)), Some((r_sub, _))) => self.supertype_of(&l_sup, &r_sub), (Some((_, l_sup)), Some((r_sub, _))) => self.supertype_of(&l_sup, &r_sub),
_ => { _ => {
if lfv.is_linked() { if lfv.is_linked() {
@ -415,8 +414,7 @@ impl Context {
false false
} }
} }
} },
}
// true if it can be a supertype, false if it cannot (due to type constraints) // true if it can be a supertype, false if it cannot (due to type constraints)
// No type constraints are imposed here, as subsequent type decisions are made according to the possibilities // No type constraints are imposed here, as subsequent type decisions are made according to the possibilities
(FreeVar(lfv), rhs) => { (FreeVar(lfv), rhs) => {

View file

@ -10,7 +10,7 @@ impl Context {
if fv.is_linked() { if fv.is_linked() {
fv.crack().clone() fv.crack().clone()
} else { } else {
let (_sub, sup) = fv.crack_bound_types().unwrap(); let (_sub, sup) = fv.get_bound_types().unwrap();
sup sup
} }
} else { } else {

View file

@ -303,7 +303,7 @@ impl TyVarContext {
} }
fn check_cyclicity_and_link(&self, name: &str, fv_inst: &FreeTyVar, tv: &Type) { fn check_cyclicity_and_link(&self, name: &str, fv_inst: &FreeTyVar, tv: &Type) {
let (sub, sup) = enum_unwrap!(tv, Type::FreeVar).crack_bound_types().unwrap(); let (sub, sup) = enum_unwrap!(tv, Type::FreeVar).get_bound_types().unwrap();
let new_cyclicity = match (sup.contains_tvar(name), sub.contains_tvar(name)) { let new_cyclicity = match (sup.contains_tvar(name), sub.contains_tvar(name)) {
(true, true) => Cyclicity::Both, (true, true) => Cyclicity::Both,
// T <: Super // T <: Super

View file

@ -986,9 +986,9 @@ impl Context {
(Type::FreeVar(lfv), Type::FreeVar(rfv)) (Type::FreeVar(lfv), Type::FreeVar(rfv))
if lfv.constraint_is_sandwiched() && rfv.constraint_is_sandwiched() => if lfv.constraint_is_sandwiched() && rfv.constraint_is_sandwiched() =>
{ {
let (lsub, lsup) = lfv.crack_bound_types().unwrap(); let (lsub, lsup) = lfv.get_bound_types().unwrap();
let l_cyc = lfv.cyclicity(); let l_cyc = lfv.cyclicity();
let (rsub, rsup) = rfv.crack_bound_types().unwrap(); let (rsub, rsup) = rfv.get_bound_types().unwrap();
let r_cyc = rfv.cyclicity(); let r_cyc = rfv.cyclicity();
let cyclicity = l_cyc.combine(r_cyc); let cyclicity = l_cyc.combine(r_cyc);
let new_constraint = if let Some(min) = self.min(&lsup, &rsup) { let new_constraint = if let Some(min) = self.min(&lsup, &rsup) {

View file

@ -609,7 +609,7 @@ impl Context {
TyParam::Value(v) => Ok(enum_t(set![v])), TyParam::Value(v) => Ok(enum_t(set![v])),
TyParam::Erased(t) => Ok((*t).clone()), TyParam::Erased(t) => Ok((*t).clone()),
TyParam::FreeVar(fv) => { TyParam::FreeVar(fv) => {
if let Some(t) = fv.type_of() { if let Some(t) = fv.get_type() {
Ok(t) Ok(t)
} else { } else {
todo!() todo!()
@ -637,7 +637,7 @@ impl Context {
TyParam::Value(v) => Ok(v.class()), TyParam::Value(v) => Ok(v.class()),
TyParam::Erased(t) => Ok((*t).clone()), TyParam::Erased(t) => Ok((*t).clone()),
TyParam::FreeVar(fv) => { TyParam::FreeVar(fv) => {
if let Some(t) = fv.type_of() { if let Some(t) = fv.get_type() {
Ok(t) Ok(t)
} else { } else {
todo!() todo!()

View file

@ -512,19 +512,19 @@ impl<T: Clone + HasLevel> Free<T> {
}) })
} }
pub fn type_of(&self) -> Option<Type> { pub fn get_type(&self) -> Option<Type> {
self.borrow() self.borrow()
.constraint() .constraint()
.and_then(|c| c.get_type().cloned()) .and_then(|c| c.get_type().cloned())
} }
pub fn crack_sup(&self) -> Option<Type> { pub fn get_sup(&self) -> Option<Type> {
self.borrow() self.borrow()
.constraint() .constraint()
.and_then(|c| c.get_super().cloned()) .and_then(|c| c.get_super().cloned())
} }
pub fn crack_bound_types(&self) -> Option<(Type, Type)> { pub fn get_bound_types(&self) -> Option<(Type, Type)> {
self.borrow() self.borrow()
.constraint() .constraint()
.and_then(|c| c.get_sub_sup().map(|(sub, sup)| (sub.clone(), sup.clone()))) .and_then(|c| c.get_sub_sup().map(|(sub, sup)| (sub.clone(), sup.clone())))

View file

@ -1715,7 +1715,7 @@ impl Type {
Self::FreeVar(fv) => { Self::FreeVar(fv) => {
fv.unbound_name().map(|n| &n[..] == name).unwrap_or(false) fv.unbound_name().map(|n| &n[..] == name).unwrap_or(false)
|| fv || fv
.crack_bound_types() .get_bound_types()
.map(|(sub, sup)| sub.contains_tvar(name) || sup.contains_tvar(name)) .map(|(sub, sup)| sub.contains_tvar(name) || sup.contains_tvar(name))
.unwrap_or(false) .unwrap_or(false)
} }