mirror of
https://github.com/erg-lang/erg.git
synced 2025-09-30 12:51:10 +00:00
Add initialization check
This commit is contained in:
parent
9d69eab174
commit
3d35db4e3b
4 changed files with 43 additions and 61 deletions
|
@ -257,10 +257,6 @@ impl Context {
|
||||||
self.register_cache(lhs, rhs, judge);
|
self.register_cache(lhs, rhs, judge);
|
||||||
return judge;
|
return judge;
|
||||||
}
|
}
|
||||||
/*if self._find_compatible_patch(lhs, rhs).is_some() {
|
|
||||||
self.register_cache(lhs, rhs, true);
|
|
||||||
return true;
|
|
||||||
}*/
|
|
||||||
self.register_cache(lhs, rhs, false);
|
self.register_cache(lhs, rhs, false);
|
||||||
false
|
false
|
||||||
}
|
}
|
||||||
|
@ -269,14 +265,13 @@ impl Context {
|
||||||
self.nominal_supertype_of(rhs, lhs)
|
self.nominal_supertype_of(rhs, lhs)
|
||||||
}
|
}
|
||||||
|
|
||||||
fn _find_compatible_patch(&self, sup: &Type, sub: &Type) -> Option<Str> {
|
fn _find_compatible_patch(&self, sup: &Type, sub: &Type) -> Option<&Context> {
|
||||||
// let subst_ctx = SubstContext::try_new(sub, self, Location::Unknown)?;
|
|
||||||
for patch in self._all_patches().into_iter() {
|
for patch in self._all_patches().into_iter() {
|
||||||
if let ContextKind::GluePatch(tr_inst) = &patch.kind {
|
if let ContextKind::GluePatch(tr_inst) = &patch.kind {
|
||||||
if self.subtype_of(sub, &tr_inst.sub_type)
|
if self.subtype_of(sub, &tr_inst.sub_type)
|
||||||
&& self.subtype_of(&tr_inst.sup_trait, sup)
|
&& self.subtype_of(&tr_inst.sup_trait, sup)
|
||||||
{
|
{
|
||||||
return Some(patch.name.clone());
|
return Some(patch);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -436,11 +431,14 @@ impl Context {
|
||||||
}
|
}
|
||||||
FreeKind::Unbound { constraint: _, .. }
|
FreeKind::Unbound { constraint: _, .. }
|
||||||
| FreeKind::NamedUnbound { constraint: _, .. } => {
|
| FreeKind::NamedUnbound { constraint: _, .. } => {
|
||||||
let (sub, _sup) = rfv.get_subsup().unwrap();
|
if let Some((sub, _sup)) = rfv.get_subsup() {
|
||||||
rfv.forced_undoable_link(lhs);
|
rfv.forced_undoable_link(lhs);
|
||||||
let res = self.supertype_of(lhs, &sub);
|
let res = self.supertype_of(lhs, &sub);
|
||||||
rfv.undo();
|
rfv.undo();
|
||||||
res
|
res
|
||||||
|
} else {
|
||||||
|
todo!("{lhs} / {rhs}");
|
||||||
|
}
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
(Type::Record(lhs), Type::Record(rhs)) => {
|
(Type::Record(lhs), Type::Record(rhs)) => {
|
||||||
|
@ -660,53 +658,6 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/*fn is_super_constr(&self, constr: &Constraint, rhs: &Type) -> bool {
|
|
||||||
match constr {
|
|
||||||
// `(?T <: Int) :> Nat` can be true, `(?T <: Nat) :> Int` is false
|
|
||||||
// `(?T <: Eq(?T)) :> Nat` can be true, but this requires special judgment
|
|
||||||
// `(?T :> X) :> Y` is true
|
|
||||||
// `(?T :> Str) :> Int` is true (?T :> Str or Int)
|
|
||||||
// `(Nat <: ?T <: Ratio) :> Nat` can be true
|
|
||||||
Constraint::Sandwiched { sup, .. } => self.supertype_of(sup, rhs),
|
|
||||||
// (?v: Type, rhs): OK
|
|
||||||
// (?v: Nat, rhs): Something wrong
|
|
||||||
// Class <: Type, but Nat <!: Type (Nat: Type)
|
|
||||||
Constraint::TypeOf(t) => {
|
|
||||||
if self.supertype_of(&Type, t) {
|
|
||||||
true
|
|
||||||
} else {
|
|
||||||
panic!()
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Constraint::Uninited => unreachable!(),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn is_sub_constr(&self, lhs: &Type, constr: &Constraint) -> bool {
|
|
||||||
match constr {
|
|
||||||
// ?T cannot be `Never`
|
|
||||||
// `Nat :> (?T <: Int)` can be true
|
|
||||||
// `Int :> (?T <: Nat)` can be true
|
|
||||||
// * so sup is unrelated
|
|
||||||
// `Str :> (?T <: Int)` is false
|
|
||||||
// `Int :> (?T :> Nat)` can be true, `Nat :> (?T :> Int)` is false
|
|
||||||
// `Int :> (Nat <: ?T <: Ratio)` can be true, `Nat :> (Int <: ?T <: Ratio)` is false
|
|
||||||
// Eq(Int) :> ?M(:> Int, <: Mul(?M) and Add(?M))
|
|
||||||
Constraint::Sandwiched {
|
|
||||||
sub,
|
|
||||||
sup: _,
|
|
||||||
} => self.supertype_of(lhs, sub),
|
|
||||||
Constraint::TypeOf(t) => {
|
|
||||||
if self.supertype_of(&Type, t) {
|
|
||||||
true
|
|
||||||
} else {
|
|
||||||
panic!()
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Constraint::Uninited => unreachable!(),
|
|
||||||
}
|
|
||||||
}*/
|
|
||||||
|
|
||||||
pub(crate) fn poly_supertype_of(
|
pub(crate) fn poly_supertype_of(
|
||||||
&self,
|
&self,
|
||||||
typ: &Type,
|
typ: &Type,
|
||||||
|
|
|
@ -1412,8 +1412,11 @@ impl Context {
|
||||||
match t {
|
match t {
|
||||||
Type::FreeVar(fv) if fv.is_linked() => self.get_nominal_super_type_ctxs(&fv.crack()),
|
Type::FreeVar(fv) if fv.is_linked() => self.get_nominal_super_type_ctxs(&fv.crack()),
|
||||||
Type::FreeVar(fv) => {
|
Type::FreeVar(fv) => {
|
||||||
let sup = fv.get_sup().unwrap();
|
if let Some(sup) = fv.get_sup() {
|
||||||
self.get_nominal_super_type_ctxs(&sup)
|
self.get_nominal_super_type_ctxs(&sup)
|
||||||
|
} else {
|
||||||
|
self.get_nominal_super_type_ctxs(&Type)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
Type::And(l, r) => {
|
Type::And(l, r) => {
|
||||||
match (
|
match (
|
||||||
|
@ -2087,6 +2090,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
// TODO:
|
||||||
/// Int.meta_type() == ClassType (<: Type)
|
/// Int.meta_type() == ClassType (<: Type)
|
||||||
/// Show.meta_type() == TraitType (<: Type)
|
/// Show.meta_type() == TraitType (<: Type)
|
||||||
/// [Int; 3].meta_type() == [ClassType; 3] (<: Type)
|
/// [Int; 3].meta_type() == [ClassType; 3] (<: Type)
|
||||||
|
|
|
@ -20,6 +20,7 @@ use erg_parser::token::TokenKind;
|
||||||
use erg_parser::Parser;
|
use erg_parser::Parser;
|
||||||
|
|
||||||
use crate::ty::constructors::*;
|
use crate::ty::constructors::*;
|
||||||
|
use crate::ty::free::CanbeFree;
|
||||||
use crate::ty::free::{Constraint, HasLevel};
|
use crate::ty::free::{Constraint, HasLevel};
|
||||||
use crate::ty::typaram::{IntervalOp, TyParam, TyParamOrdering};
|
use crate::ty::typaram::{IntervalOp, TyParam, TyParamOrdering};
|
||||||
use crate::ty::value::ValueObj;
|
use crate::ty::value::ValueObj;
|
||||||
|
@ -835,6 +836,30 @@ impl Context {
|
||||||
for bound in bounds.iter() {
|
for bound in bounds.iter() {
|
||||||
self.instantiate_ty_bound(bound, &mut tv_cache, mode)?;
|
self.instantiate_ty_bound(bound, &mut tv_cache, mode)?;
|
||||||
}
|
}
|
||||||
|
for tv in tv_cache.tyvar_instances.values() {
|
||||||
|
if tv.constraint().unwrap().is_uninited() {
|
||||||
|
return Err(TyCheckErrors::from(TyCheckError::no_var_error(
|
||||||
|
self.cfg.input.clone(),
|
||||||
|
line!() as usize,
|
||||||
|
bounds.loc(),
|
||||||
|
self.caused_by(),
|
||||||
|
&tv.local_name(),
|
||||||
|
self.get_similar_name(&tv.local_name()),
|
||||||
|
)));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
for tp in tv_cache.typaram_instances.values() {
|
||||||
|
if tp.constraint().unwrap().is_uninited() {
|
||||||
|
return Err(TyCheckErrors::from(TyCheckError::no_var_error(
|
||||||
|
self.cfg.input.clone(),
|
||||||
|
line!() as usize,
|
||||||
|
bounds.loc(),
|
||||||
|
self.caused_by(),
|
||||||
|
&tp.to_string(),
|
||||||
|
self.get_similar_name(&tp.to_string()),
|
||||||
|
)));
|
||||||
|
}
|
||||||
|
}
|
||||||
Ok(tv_cache)
|
Ok(tv_cache)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -22,4 +22,6 @@
|
||||||
|
|
||||||
if! __name__ == "__main__", do!:
|
if! __name__ == "__main__", do!:
|
||||||
v = .Version.new(0, 0, 1)
|
v = .Version.new(0, 0, 1)
|
||||||
|
assert v.minor == 0
|
||||||
|
assert v.pre == None
|
||||||
assert v != .Version.new(0, 0, 2)
|
assert v != .Version.new(0, 0, 2)
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue