mirror of
https://github.com/erg-lang/erg.git
synced 2025-09-30 12:51:10 +00:00
Fixed a type inference bugs
Pass source code line numbers instead of error numbers as a temporary hack
This commit is contained in:
parent
1078345a98
commit
791107cdd3
9 changed files with 305 additions and 312 deletions
|
@ -89,10 +89,6 @@ pub trait HasLevel {
|
||||||
// REVIEW: TyBoundと微妙に役割が被っている
|
// REVIEW: TyBoundと微妙に役割が被っている
|
||||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||||
pub enum Constraint {
|
pub enum Constraint {
|
||||||
/// :> T
|
|
||||||
SupertypeOf(Type),
|
|
||||||
/// <: T
|
|
||||||
SubtypeOf(Type),
|
|
||||||
/// :> Sub, <: Sup
|
/// :> Sub, <: Sup
|
||||||
Sandwiched {
|
Sandwiched {
|
||||||
sub: Type,
|
sub: Type,
|
||||||
|
@ -106,9 +102,15 @@ pub enum Constraint {
|
||||||
impl fmt::Display for Constraint {
|
impl fmt::Display for Constraint {
|
||||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Self::SupertypeOf(sub) => write!(f, ":> {sub}"),
|
Self::Sandwiched { sub, sup } => {
|
||||||
Self::SubtypeOf(sup) => write!(f, "<: {sup}"),
|
if sub.rec_eq(&Type::Never) {
|
||||||
Self::Sandwiched { sub, sup } => write!(f, ":> {sub}, <: {sup}"),
|
write!(f, "<: {sup}")
|
||||||
|
} else if sup.rec_eq(&Type::Obj) {
|
||||||
|
write!(f, ":> {sub}")
|
||||||
|
} else {
|
||||||
|
write!(f, ":> {sub}, <: {sup}")
|
||||||
|
}
|
||||||
|
}
|
||||||
Self::TypeOf(ty) => write!(f, ": {}", ty),
|
Self::TypeOf(ty) => write!(f, ": {}", ty),
|
||||||
Self::Uninited => write!(f, "<uninited>"),
|
Self::Uninited => write!(f, "<uninited>"),
|
||||||
}
|
}
|
||||||
|
@ -120,6 +122,14 @@ impl Constraint {
|
||||||
Self::Sandwiched { sub, sup }
|
Self::Sandwiched { sub, sup }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub const fn subtype_of(sup: Type) -> Self {
|
||||||
|
Self::sandwiched(Type::Never, sup)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub const fn supertype_of(sub: Type) -> Self {
|
||||||
|
Self::sandwiched(sub, Type::Obj)
|
||||||
|
}
|
||||||
|
|
||||||
pub const fn is_uninited(&self) -> bool {
|
pub const fn is_uninited(&self) -> bool {
|
||||||
matches!(self, Self::Uninited)
|
matches!(self, Self::Uninited)
|
||||||
}
|
}
|
||||||
|
@ -133,7 +143,6 @@ impl Constraint {
|
||||||
|
|
||||||
pub fn sub_type(&self) -> Option<&Type> {
|
pub fn sub_type(&self) -> Option<&Type> {
|
||||||
match self {
|
match self {
|
||||||
Self::SupertypeOf(ty) => Some(ty),
|
|
||||||
Self::Sandwiched { sub, .. } => Some(sub),
|
Self::Sandwiched { sub, .. } => Some(sub),
|
||||||
_ => None,
|
_ => None,
|
||||||
}
|
}
|
||||||
|
@ -141,7 +150,6 @@ impl Constraint {
|
||||||
|
|
||||||
pub fn super_type(&self) -> Option<&Type> {
|
pub fn super_type(&self) -> Option<&Type> {
|
||||||
match self {
|
match self {
|
||||||
Self::SubtypeOf(ty) => Some(ty),
|
|
||||||
Self::Sandwiched { sup, .. } => Some(sup),
|
Self::Sandwiched { sup, .. } => Some(sup),
|
||||||
_ => None,
|
_ => None,
|
||||||
}
|
}
|
||||||
|
@ -156,7 +164,6 @@ impl Constraint {
|
||||||
|
|
||||||
pub fn super_type_mut(&mut self) -> Option<&mut Type> {
|
pub fn super_type_mut(&mut self) -> Option<&mut Type> {
|
||||||
match self {
|
match self {
|
||||||
Self::SubtypeOf(ty) => Some(ty),
|
|
||||||
Self::Sandwiched { sup, .. } => Some(sup),
|
Self::Sandwiched { sup, .. } => Some(sup),
|
||||||
_ => None,
|
_ => None,
|
||||||
}
|
}
|
||||||
|
@ -989,21 +996,35 @@ impl TyParamOrdering {
|
||||||
|
|
||||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||||
pub enum TyBound {
|
pub enum TyBound {
|
||||||
// e.g. A <: Add => Subtype{sub: A, sup: Add}, A <: {a: Int} => Subtype{sub: A, sup: {a: Int}}
|
// e.g.
|
||||||
Subtype { sub: Type, sup: Type },
|
// A :> Int => Sandwiched{sub: Int, mid: A, sup: Obj}
|
||||||
Supertype { sup: Type, sub: Type },
|
// A <: {I: Int | I > 0} => Sandwiched{sub: Never, mid: A, sup: {I: Int | I > 0}}
|
||||||
Sandwiched { sub: Type, mid: Type, sup: Type },
|
/// Sub <: Mid <: Sup
|
||||||
|
Sandwiched {
|
||||||
|
sub: Type,
|
||||||
|
mid: Type,
|
||||||
|
sup: Type,
|
||||||
|
},
|
||||||
// TyParam::MonoQuantVarに型の情報が含まれているので、boundsからは除去される
|
// TyParam::MonoQuantVarに型の情報が含まれているので、boundsからは除去される
|
||||||
// e.g. N: Nat => Instance{name: N, t: Nat}
|
// e.g. N: Nat => Instance{name: N, t: Nat}
|
||||||
Instance { name: Str, t: Type },
|
Instance {
|
||||||
|
name: Str,
|
||||||
|
t: Type,
|
||||||
|
},
|
||||||
}
|
}
|
||||||
|
|
||||||
impl fmt::Display for TyBound {
|
impl fmt::Display for TyBound {
|
||||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Self::Subtype { sub, sup } => write!(f, "{sub} <: {sup}"),
|
Self::Sandwiched { sub, mid, sup } => {
|
||||||
Self::Supertype { sup, sub } => write!(f, "{sup} :> {sub}"),
|
if sub.rec_eq(&Type::Never) {
|
||||||
Self::Sandwiched { sub, mid, sup } => write!(f, "{sub} <: {mid} <: {sup}"),
|
write!(f, "{mid} <: {sup}")
|
||||||
|
} else if sup.rec_eq(&Type::Obj) {
|
||||||
|
write!(f, "{sub} <: {mid}")
|
||||||
|
} else {
|
||||||
|
write!(f, "{sub} <: {mid} <: {sup}")
|
||||||
|
}
|
||||||
|
}
|
||||||
Self::Instance { name, t } => write!(f, "'{name}: {t}"),
|
Self::Instance { name, t } => write!(f, "'{name}: {t}"),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -1016,10 +1037,6 @@ impl HasLevel for TyBound {
|
||||||
|
|
||||||
fn update_level(&self, level: usize) {
|
fn update_level(&self, level: usize) {
|
||||||
match self {
|
match self {
|
||||||
Self::Subtype { sub, sup } | Self::Supertype { sup, sub } => {
|
|
||||||
sub.update_level(level);
|
|
||||||
sup.update_level(level);
|
|
||||||
}
|
|
||||||
Self::Sandwiched { sub, mid, sup } => {
|
Self::Sandwiched { sub, mid, sup } => {
|
||||||
sub.update_level(level);
|
sub.update_level(level);
|
||||||
mid.update_level(level);
|
mid.update_level(level);
|
||||||
|
@ -1033,10 +1050,6 @@ impl HasLevel for TyBound {
|
||||||
|
|
||||||
fn lift(&self) {
|
fn lift(&self) {
|
||||||
match self {
|
match self {
|
||||||
Self::Subtype { sub, sup } | Self::Supertype { sup, sub } => {
|
|
||||||
sub.lift();
|
|
||||||
sup.lift();
|
|
||||||
}
|
|
||||||
Self::Sandwiched { sub, mid, sup } => {
|
Self::Sandwiched { sub, mid, sup } => {
|
||||||
sub.lift();
|
sub.lift();
|
||||||
mid.lift();
|
mid.lift();
|
||||||
|
@ -1050,16 +1063,14 @@ impl HasLevel for TyBound {
|
||||||
}
|
}
|
||||||
|
|
||||||
impl TyBound {
|
impl TyBound {
|
||||||
pub const fn subtype(sub: Type, sup: Type) -> Self {
|
|
||||||
Self::Subtype { sub, sup }
|
|
||||||
}
|
|
||||||
pub const fn supertype(sup: Type, sub: Type) -> Self {
|
|
||||||
Self::Supertype { sup, sub }
|
|
||||||
}
|
|
||||||
pub const fn sandwiched(sub: Type, mid: Type, sup: Type) -> Self {
|
pub const fn sandwiched(sub: Type, mid: Type, sup: Type) -> Self {
|
||||||
Self::Sandwiched { sub, mid, sup }
|
Self::Sandwiched { sub, mid, sup }
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub const fn subtype_of(sub: Type, sup: Type) -> Self {
|
||||||
|
Self::sandwiched(Type::Never, sub, sup)
|
||||||
|
}
|
||||||
|
|
||||||
pub const fn static_instance(name: &'static str, t: Type) -> Self {
|
pub const fn static_instance(name: &'static str, t: Type) -> Self {
|
||||||
Self::Instance {
|
Self::Instance {
|
||||||
name: Str::ever(name),
|
name: Str::ever(name),
|
||||||
|
@ -1076,14 +1087,11 @@ impl TyBound {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn mentions_as_subtype(&self, name: &str) -> bool {
|
pub fn mentions_as_subtype(&self, name: &str) -> bool {
|
||||||
matches!(self, Self::Subtype{ sub, .. } if sub.name() == name)
|
matches!(self, Self::Sandwiched{ sub, .. } if sub.name() == name)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn has_unbound_var(&self) -> bool {
|
pub fn has_unbound_var(&self) -> bool {
|
||||||
match self {
|
match self {
|
||||||
Self::Subtype { sub, sup } | Self::Supertype { sub, sup } => {
|
|
||||||
sub.has_unbound_var() || sup.has_unbound_var()
|
|
||||||
}
|
|
||||||
Self::Sandwiched { sub, mid, sup } => {
|
Self::Sandwiched { sub, mid, sup } => {
|
||||||
sub.has_unbound_var() || mid.has_unbound_var() || sup.has_unbound_var()
|
sub.has_unbound_var() || mid.has_unbound_var() || sup.has_unbound_var()
|
||||||
}
|
}
|
||||||
|
@ -1093,8 +1101,6 @@ impl TyBound {
|
||||||
|
|
||||||
pub const fn t(&self) -> &Type {
|
pub const fn t(&self) -> &Type {
|
||||||
match self {
|
match self {
|
||||||
Self::Subtype { sup, .. } => sup,
|
|
||||||
Self::Supertype { sub, .. } => sub,
|
|
||||||
Self::Sandwiched { .. } => todo!(),
|
Self::Sandwiched { .. } => todo!(),
|
||||||
Self::Instance { t, .. } => t,
|
Self::Instance { t, .. } => t,
|
||||||
}
|
}
|
||||||
|
@ -1102,8 +1108,6 @@ impl TyBound {
|
||||||
|
|
||||||
pub fn lhs(&self) -> &str {
|
pub fn lhs(&self) -> &str {
|
||||||
match self {
|
match self {
|
||||||
Self::Subtype { sub, .. } => sub.name(),
|
|
||||||
Self::Supertype { sup, .. } => sup.name(),
|
|
||||||
Self::Sandwiched { mid, .. } => mid.name(),
|
Self::Sandwiched { mid, .. } => mid.name(),
|
||||||
Self::Instance { name, .. } => name,
|
Self::Instance { name, .. } => name,
|
||||||
}
|
}
|
||||||
|
@ -1444,26 +1448,15 @@ pub struct SubrType {
|
||||||
|
|
||||||
impl fmt::Display for SubrType {
|
impl fmt::Display for SubrType {
|
||||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
if self.default_params.is_empty() {
|
write!(
|
||||||
write!(
|
f,
|
||||||
f,
|
"{}({}, {}) {} {}",
|
||||||
"{}({}) {} {}",
|
self.kind.prefix(),
|
||||||
self.kind.prefix(),
|
fmt_vec(&self.non_default_params),
|
||||||
fmt_vec(&self.non_default_params),
|
fmt_vec(&self.default_params),
|
||||||
self.kind.arrow(),
|
self.kind.arrow(),
|
||||||
self.return_t,
|
self.return_t,
|
||||||
)
|
)
|
||||||
} else {
|
|
||||||
write!(
|
|
||||||
f,
|
|
||||||
"{}({} |= {}) {} {}",
|
|
||||||
self.kind.prefix(),
|
|
||||||
fmt_vec(&self.non_default_params),
|
|
||||||
fmt_vec(&self.default_params),
|
|
||||||
self.kind.arrow(),
|
|
||||||
self.return_t,
|
|
||||||
)
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -2971,9 +2964,10 @@ pub mod type_constrs {
|
||||||
TyBound::static_instance(name, t)
|
TyBound::static_instance(name, t)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
/// Sub <: Sup
|
||||||
#[inline]
|
#[inline]
|
||||||
pub fn subtype(sub: Type, sup: Type) -> TyBound {
|
pub fn subtypeof(sub: Type, sup: Type) -> TyBound {
|
||||||
TyBound::subtype(sub, sup)
|
TyBound::sandwiched(Type::Never, sub, sup)
|
||||||
}
|
}
|
||||||
|
|
||||||
#[inline]
|
#[inline]
|
||||||
|
|
|
@ -255,48 +255,6 @@ impl TyVarContext {
|
||||||
|
|
||||||
fn instantiate_bound(&mut self, bound: TyBound, ctx: &Context) {
|
fn instantiate_bound(&mut self, bound: TyBound, ctx: &Context) {
|
||||||
match bound {
|
match bound {
|
||||||
TyBound::Subtype { sub, sup } => {
|
|
||||||
let sup = match sup {
|
|
||||||
Type::Poly { name, params } => {
|
|
||||||
self.instantiate_poly(sub.name(), &name, params, ctx)
|
|
||||||
}
|
|
||||||
Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
|
|
||||||
sup => sup,
|
|
||||||
};
|
|
||||||
let constraint = Constraint::SubtypeOf(sup);
|
|
||||||
if let Some(tv) = self.tyvar_instances.get(sub.name()) {
|
|
||||||
tv.update_constraint(constraint);
|
|
||||||
} else if let Some(tp) = self.typaram_instances.get(sub.name()) {
|
|
||||||
tp.update_constraint(constraint);
|
|
||||||
} else {
|
|
||||||
let name = Str::rc(sub.name());
|
|
||||||
self.push_tyvar(
|
|
||||||
name.clone(),
|
|
||||||
Type::named_free_var(name, self.level, constraint),
|
|
||||||
);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
TyBound::Supertype { sup, sub } => {
|
|
||||||
let sub = match sub {
|
|
||||||
Type::Poly { name, params } => {
|
|
||||||
self.instantiate_poly(sup.name(), &name, params, ctx)
|
|
||||||
}
|
|
||||||
Type::MonoProj { lhs, rhs } => Type::mono_proj(self.instantiate_t(*lhs), rhs),
|
|
||||||
sub => sub,
|
|
||||||
};
|
|
||||||
let constraint = Constraint::SupertypeOf(sub);
|
|
||||||
if let Some(tv) = self.tyvar_instances.get(sup.name()) {
|
|
||||||
tv.update_constraint(constraint);
|
|
||||||
} else if let Some(tp) = self.typaram_instances.get(sup.name()) {
|
|
||||||
tp.update_constraint(constraint);
|
|
||||||
} else {
|
|
||||||
let name = Str::rc(sup.name());
|
|
||||||
self.push_tyvar(
|
|
||||||
name.clone(),
|
|
||||||
Type::named_free_var(name, self.level, constraint),
|
|
||||||
);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
TyBound::Sandwiched { sub, mid, sup } => {
|
TyBound::Sandwiched { sub, mid, sup } => {
|
||||||
let sub = match sub {
|
let sub = match sub {
|
||||||
Type::Poly { name, params } => {
|
Type::Poly { name, params } => {
|
||||||
|
@ -803,6 +761,7 @@ impl Context {
|
||||||
ast::VarPattern::VarName(v) => {
|
ast::VarPattern::VarName(v) => {
|
||||||
if sig.t_spec.is_none() && opt_t.is_none() {
|
if sig.t_spec.is_none() && opt_t.is_none() {
|
||||||
Err(TyCheckError::no_type_spec_error(
|
Err(TyCheckError::no_type_spec_error(
|
||||||
|
line!() as usize,
|
||||||
sig.loc(),
|
sig.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
v.inspect(),
|
v.inspect(),
|
||||||
|
@ -810,6 +769,7 @@ impl Context {
|
||||||
} else {
|
} else {
|
||||||
if self.registered(v.inspect(), v.inspect().is_uppercase()) {
|
if self.registered(v.inspect(), v.inspect().is_uppercase()) {
|
||||||
return Err(TyCheckError::duplicate_decl_error(
|
return Err(TyCheckError::duplicate_decl_error(
|
||||||
|
line!() as usize,
|
||||||
sig.loc(),
|
sig.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
v.inspect(),
|
v.inspect(),
|
||||||
|
@ -849,6 +809,7 @@ impl Context {
|
||||||
let kind = id.map_or(VarKind::Declared, VarKind::Defined);
|
let kind = id.map_or(VarKind::Declared, VarKind::Defined);
|
||||||
if self.registered(name, name.is_uppercase()) {
|
if self.registered(name, name.is_uppercase()) {
|
||||||
return Err(TyCheckError::duplicate_decl_error(
|
return Err(TyCheckError::duplicate_decl_error(
|
||||||
|
line!() as usize,
|
||||||
sig.loc(),
|
sig.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
name,
|
name,
|
||||||
|
@ -858,6 +819,7 @@ impl Context {
|
||||||
let vi = VarInfo::new(t, muty, Private, kind);
|
let vi = VarInfo::new(t, muty, Private, kind);
|
||||||
if let Some(_decl) = self.decls.remove(name) {
|
if let Some(_decl) = self.decls.remove(name) {
|
||||||
return Err(TyCheckError::duplicate_decl_error(
|
return Err(TyCheckError::duplicate_decl_error(
|
||||||
|
line!() as usize,
|
||||||
sig.loc(),
|
sig.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
name,
|
name,
|
||||||
|
@ -901,6 +863,7 @@ impl Context {
|
||||||
ast::VarPattern::VarName(v) => {
|
ast::VarPattern::VarName(v) => {
|
||||||
if self.registered(v.inspect(), v.inspect().is_uppercase()) {
|
if self.registered(v.inspect(), v.inspect().is_uppercase()) {
|
||||||
Err(TyCheckError::reassign_error(
|
Err(TyCheckError::reassign_error(
|
||||||
|
line!() as usize,
|
||||||
v.loc(),
|
v.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
v.inspect(),
|
v.inspect(),
|
||||||
|
@ -940,6 +903,7 @@ impl Context {
|
||||||
ast::ParamPattern::VarName(v) => {
|
ast::ParamPattern::VarName(v) => {
|
||||||
if self.registered(v.inspect(), v.inspect().is_uppercase()) {
|
if self.registered(v.inspect(), v.inspect().is_uppercase()) {
|
||||||
Err(TyCheckError::reassign_error(
|
Err(TyCheckError::reassign_error(
|
||||||
|
line!() as usize,
|
||||||
v.loc(),
|
v.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
v.inspect(),
|
v.inspect(),
|
||||||
|
@ -1067,6 +1031,7 @@ impl Context {
|
||||||
self.unify(spec_ret_t, body_t, Some(sig.loc()), None)
|
self.unify(spec_ret_t, body_t, Some(sig.loc()), None)
|
||||||
.map_err(|e| {
|
.map_err(|e| {
|
||||||
TyCheckError::return_type_error(
|
TyCheckError::return_type_error(
|
||||||
|
line!() as usize,
|
||||||
e.core.loc,
|
e.core.loc,
|
||||||
e.caused_by,
|
e.caused_by,
|
||||||
readable_name(name.inspect()),
|
readable_name(name.inspect()),
|
||||||
|
@ -1077,6 +1042,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
if self.registered(name.inspect(), name.inspect().is_uppercase()) {
|
if self.registered(name.inspect(), name.inspect().is_uppercase()) {
|
||||||
Err(TyCheckError::reassign_error(
|
Err(TyCheckError::reassign_error(
|
||||||
|
line!() as usize,
|
||||||
name.loc(),
|
name.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
name.inspect(),
|
name.inspect(),
|
||||||
|
@ -1127,6 +1093,7 @@ impl Context {
|
||||||
if let Some(vi) = self.decls.remove(name) {
|
if let Some(vi) = self.decls.remove(name) {
|
||||||
if !self.rec_full_supertype_of(&vi.t, &found_t) {
|
if !self.rec_full_supertype_of(&vi.t, &found_t) {
|
||||||
return Err(TyCheckError::violate_decl_error(
|
return Err(TyCheckError::violate_decl_error(
|
||||||
|
line!() as usize,
|
||||||
sig.loc(),
|
sig.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
name.inspect(),
|
name.inspect(),
|
||||||
|
@ -1164,6 +1131,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
return Err(TyCheckError::type_mismatch_error(
|
return Err(TyCheckError::type_mismatch_error(
|
||||||
|
line!() as usize,
|
||||||
mod_name.loc(),
|
mod_name.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
"import::name",
|
"import::name",
|
||||||
|
@ -1174,6 +1142,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
_ => {
|
_ => {
|
||||||
return Err(TyCheckError::feature_error(
|
return Err(TyCheckError::feature_error(
|
||||||
|
line!() as usize,
|
||||||
mod_name.loc(),
|
mod_name.loc(),
|
||||||
"non-literal importing",
|
"non-literal importing",
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
|
@ -1184,7 +1153,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn _push_subtype_bound(&mut self, sub: Type, sup: Type) {
|
pub(crate) fn _push_subtype_bound(&mut self, sub: Type, sup: Type) {
|
||||||
self.bounds.push(TyBound::subtype(sub, sup));
|
self.bounds.push(TyBound::subtype_of(sub, sup));
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn _push_instance_bound(&mut self, name: Str, t: Type) {
|
pub(crate) fn _push_instance_bound(&mut self, name: Str, t: Type) {
|
||||||
|
@ -1219,12 +1188,6 @@ impl Context {
|
||||||
FreeKind::Unbound { id, constraint, .. } => {
|
FreeKind::Unbound { id, constraint, .. } => {
|
||||||
let name = id.to_string();
|
let name = id.to_string();
|
||||||
let bound = match constraint {
|
let bound = match constraint {
|
||||||
Constraint::SubtypeOf(sup) => {
|
|
||||||
TyBound::subtype(Type::mono(name.clone()), sup.clone())
|
|
||||||
}
|
|
||||||
Constraint::SupertypeOf(sub) => {
|
|
||||||
TyBound::supertype(Type::mono(name.clone()), sub.clone())
|
|
||||||
}
|
|
||||||
Constraint::Sandwiched { sub, sup } => {
|
Constraint::Sandwiched { sub, sup } => {
|
||||||
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
||||||
}
|
}
|
||||||
|
@ -1237,12 +1200,6 @@ impl Context {
|
||||||
name, constraint, ..
|
name, constraint, ..
|
||||||
} => {
|
} => {
|
||||||
let bound = match constraint {
|
let bound = match constraint {
|
||||||
Constraint::SubtypeOf(sup) => {
|
|
||||||
TyBound::subtype(Type::mono(name.clone()), sup.clone())
|
|
||||||
}
|
|
||||||
Constraint::SupertypeOf(sub) => {
|
|
||||||
TyBound::supertype(Type::mono(name.clone()), sub.clone())
|
|
||||||
}
|
|
||||||
Constraint::Sandwiched { sub, sup } => {
|
Constraint::Sandwiched { sub, sup } => {
|
||||||
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
||||||
}
|
}
|
||||||
|
@ -1280,12 +1237,6 @@ impl Context {
|
||||||
FreeKind::Unbound { id, constraint, .. } => {
|
FreeKind::Unbound { id, constraint, .. } => {
|
||||||
let name = id.to_string();
|
let name = id.to_string();
|
||||||
let bound = match constraint {
|
let bound = match constraint {
|
||||||
Constraint::SubtypeOf(sup) => {
|
|
||||||
TyBound::subtype(Type::mono(name.clone()), sup.clone())
|
|
||||||
}
|
|
||||||
Constraint::SupertypeOf(sub) => {
|
|
||||||
TyBound::supertype(Type::mono(name.clone()), sub.clone())
|
|
||||||
}
|
|
||||||
Constraint::Sandwiched { sub, sup } => {
|
Constraint::Sandwiched { sub, sup } => {
|
||||||
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
||||||
}
|
}
|
||||||
|
@ -1298,12 +1249,6 @@ impl Context {
|
||||||
name, constraint, ..
|
name, constraint, ..
|
||||||
} => {
|
} => {
|
||||||
let bound = match constraint {
|
let bound = match constraint {
|
||||||
Constraint::SubtypeOf(sup) => {
|
|
||||||
TyBound::subtype(Type::mono(name.clone()), sup.clone())
|
|
||||||
}
|
|
||||||
Constraint::SupertypeOf(sub) => {
|
|
||||||
TyBound::supertype(Type::mono(name.clone()), sub.clone())
|
|
||||||
}
|
|
||||||
Constraint::Sandwiched { sub, sup } => {
|
Constraint::Sandwiched { sub, sup } => {
|
||||||
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
TyBound::sandwiched(sub.clone(), Type::mono(name.clone()), sup.clone())
|
||||||
}
|
}
|
||||||
|
@ -1581,6 +1526,7 @@ impl Context {
|
||||||
let params_len = subr.non_default_params.len() + subr.default_params.len();
|
let params_len = subr.non_default_params.len() + subr.default_params.len();
|
||||||
if params_len < pos_args.len() + kw_args.len() {
|
if params_len < pos_args.len() + kw_args.len() {
|
||||||
return Err(TyCheckError::too_many_args_error(
|
return Err(TyCheckError::too_many_args_error(
|
||||||
|
line!() as usize,
|
||||||
callee.loc(),
|
callee.loc(),
|
||||||
&callee.to_string(),
|
&callee.to_string(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
|
@ -1609,6 +1555,7 @@ impl Context {
|
||||||
.map(|s| readable_name(&s[..]))
|
.map(|s| readable_name(&s[..]))
|
||||||
.unwrap_or("");
|
.unwrap_or("");
|
||||||
TyCheckError::type_mismatch_error(
|
TyCheckError::type_mismatch_error(
|
||||||
|
line!() as usize,
|
||||||
e.core.loc,
|
e.core.loc,
|
||||||
e.caused_by,
|
e.caused_by,
|
||||||
&name[..],
|
&name[..],
|
||||||
|
@ -1619,6 +1566,7 @@ impl Context {
|
||||||
if let Some(name) = ¶m_ty.name {
|
if let Some(name) = ¶m_ty.name {
|
||||||
if passed_params.contains(name) {
|
if passed_params.contains(name) {
|
||||||
return Err(TyCheckError::multiple_args_error(
|
return Err(TyCheckError::multiple_args_error(
|
||||||
|
line!() as usize,
|
||||||
callee.loc(),
|
callee.loc(),
|
||||||
&callee.to_string(),
|
&callee.to_string(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
|
@ -1643,6 +1591,7 @@ impl Context {
|
||||||
self.sub_unify(kw_arg.expr.ref_t(), param_ty, None, Some(kw_arg.loc()))?;
|
self.sub_unify(kw_arg.expr.ref_t(), param_ty, None, Some(kw_arg.loc()))?;
|
||||||
} else {
|
} else {
|
||||||
return Err(TyCheckError::unexpected_kw_arg_error(
|
return Err(TyCheckError::unexpected_kw_arg_error(
|
||||||
|
line!() as usize,
|
||||||
kw_arg.keyword.loc(),
|
kw_arg.keyword.loc(),
|
||||||
&callee.to_string(),
|
&callee.to_string(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
|
@ -1689,12 +1638,10 @@ impl Context {
|
||||||
|
|
||||||
fn deref_constraint(&self, constraint: Constraint) -> TyCheckResult<Constraint> {
|
fn deref_constraint(&self, constraint: Constraint) -> TyCheckResult<Constraint> {
|
||||||
match constraint {
|
match constraint {
|
||||||
Constraint::SubtypeOf(sup) => Ok(Constraint::SubtypeOf(self.deref_tyvar(sup)?)),
|
|
||||||
Constraint::Sandwiched { sub, sup } => Ok(Constraint::sandwiched(
|
Constraint::Sandwiched { sub, sup } => Ok(Constraint::sandwiched(
|
||||||
self.deref_tyvar(sub)?,
|
self.deref_tyvar(sub)?,
|
||||||
self.deref_tyvar(sup)?,
|
self.deref_tyvar(sup)?,
|
||||||
)),
|
)),
|
||||||
Constraint::SupertypeOf(sub) => Ok(Constraint::SupertypeOf(self.deref_tyvar(sub)?)),
|
|
||||||
Constraint::TypeOf(t) => Ok(Constraint::TypeOf(self.deref_tyvar(t)?)),
|
Constraint::TypeOf(t) => Ok(Constraint::TypeOf(self.deref_tyvar(t)?)),
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
}
|
}
|
||||||
|
@ -1702,25 +1649,35 @@ impl Context {
|
||||||
|
|
||||||
/// e.g.
|
/// e.g.
|
||||||
/// ```
|
/// ```
|
||||||
/// deref_tyvar(?T(<: Int)[n]): ?T => Int (if self.level <= n)
|
/// deref_tyvar(?T(:> Never, <: Int)[n]): ?T => Int (if self.level <= n)
|
||||||
/// deref_tyvar((Int)): (Int) => Int
|
/// deref_tyvar((Int)): (Int) => Int
|
||||||
/// ```
|
/// ```
|
||||||
fn deref_tyvar(&self, t: Type) -> TyCheckResult<Type> {
|
fn deref_tyvar(&self, t: Type) -> TyCheckResult<Type> {
|
||||||
match t {
|
match t {
|
||||||
// ?T(<: Int)[n] => Int
|
// ?T(:> Nat, <: Int)[n] => Nat (self.level <= n)
|
||||||
Type::FreeVar(fv) if fv.constraint_is_subtypeof() || fv.constraint_is_sandwiched() => {
|
// ?T(:> Nat, <: Sub ?U(:> {1}))[n] => Nat
|
||||||
if self.level <= fv.level().unwrap() {
|
Type::FreeVar(fv) if fv.constraint_is_sandwiched() => {
|
||||||
Ok(fv.crack_constraint().super_type().unwrap().clone())
|
let constraint = fv.crack_constraint();
|
||||||
|
let (sub, sup) = constraint.sub_sup_type().unwrap();
|
||||||
|
if self.rec_full_same_type_of(sub, sup) {
|
||||||
|
self.unify(sub, sub, None, None)?;
|
||||||
|
let t = sub.clone();
|
||||||
|
drop(constraint);
|
||||||
|
fv.link(&t);
|
||||||
|
self.deref_tyvar(Type::FreeVar(fv))
|
||||||
|
} else if self.level == 0 || self.level <= fv.level().unwrap() {
|
||||||
|
let t = sub.clone();
|
||||||
|
drop(constraint);
|
||||||
|
fv.link(&t);
|
||||||
|
self.deref_tyvar(Type::FreeVar(fv))
|
||||||
} else {
|
} else {
|
||||||
|
drop(constraint);
|
||||||
Ok(Type::FreeVar(fv))
|
Ok(Type::FreeVar(fv))
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// ?T(<: Add(?R(<: T), ?O(<: U)) => ?T(<: Add(T, U))
|
|
||||||
Type::FreeVar(fv) if fv.is_unbound() => {
|
Type::FreeVar(fv) if fv.is_unbound() => {
|
||||||
if self.level == 0 {
|
if self.level == 0 {
|
||||||
match &*fv.crack_constraint() {
|
match &*fv.crack_constraint() {
|
||||||
Constraint::SupertypeOf(t) | Constraint::SubtypeOf(t) => Ok(t.clone()),
|
|
||||||
Constraint::Sandwiched { sub, .. } => Ok(sub.clone()),
|
|
||||||
Constraint::TypeOf(_) => {
|
Constraint::TypeOf(_) => {
|
||||||
Err(TyCheckError::dummy_infer_error(fn_name!(), line!()))
|
Err(TyCheckError::dummy_infer_error(fn_name!(), line!()))
|
||||||
}
|
}
|
||||||
|
@ -1907,7 +1864,7 @@ impl Context {
|
||||||
if self.rec_full_supertype_of(&fv_t, &tp_t) {
|
if self.rec_full_supertype_of(&fv_t, &tp_t) {
|
||||||
// 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
|
// 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
|
||||||
if fv.level() < Some(self.level) {
|
if fv.level() < Some(self.level) {
|
||||||
let new_constraint = Constraint::SubtypeOf(tp_t);
|
let new_constraint = Constraint::subtype_of(tp_t);
|
||||||
if self.is_sub_constraint_of(
|
if self.is_sub_constraint_of(
|
||||||
fv.borrow().constraint().unwrap(),
|
fv.borrow().constraint().unwrap(),
|
||||||
&new_constraint,
|
&new_constraint,
|
||||||
|
@ -2025,6 +1982,7 @@ impl Context {
|
||||||
self.unify_tp(le_rhs, &TyParam::value(Inf), None, None, true)
|
self.unify_tp(le_rhs, &TyParam::value(Inf), None, None, true)
|
||||||
}
|
}
|
||||||
_ => Err(TyCheckError::pred_unification_error(
|
_ => Err(TyCheckError::pred_unification_error(
|
||||||
|
line!() as usize,
|
||||||
l_pred,
|
l_pred,
|
||||||
r_pred,
|
r_pred,
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
|
@ -2039,6 +1997,7 @@ impl Context {
|
||||||
self.unify_tp(ge_rhs, &TyParam::value(NegInf), None, None, true)
|
self.unify_tp(ge_rhs, &TyParam::value(NegInf), None, None, true)
|
||||||
}
|
}
|
||||||
_ => Err(TyCheckError::pred_unification_error(
|
_ => Err(TyCheckError::pred_unification_error(
|
||||||
|
line!() as usize,
|
||||||
l_pred,
|
l_pred,
|
||||||
r_pred,
|
r_pred,
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
|
@ -2052,12 +2011,14 @@ impl Context {
|
||||||
self.unify_tp(rhs, ge_rhs, None, None, false)
|
self.unify_tp(rhs, ge_rhs, None, None, false)
|
||||||
}
|
}
|
||||||
_ => Err(TyCheckError::pred_unification_error(
|
_ => Err(TyCheckError::pred_unification_error(
|
||||||
|
line!() as usize,
|
||||||
l_pred,
|
l_pred,
|
||||||
r_pred,
|
r_pred,
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
)),
|
)),
|
||||||
},
|
},
|
||||||
_ => Err(TyCheckError::pred_unification_error(
|
_ => Err(TyCheckError::pred_unification_error(
|
||||||
|
line!() as usize,
|
||||||
l_pred,
|
l_pred,
|
||||||
r_pred,
|
r_pred,
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
|
@ -2123,7 +2084,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
} // &fv is dropped
|
} // &fv is dropped
|
||||||
let new_constraint = Constraint::SubtypeOf(t.clone());
|
let new_constraint = Constraint::subtype_of(t.clone());
|
||||||
// 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
|
// 外部未連携型変数の場合、linkしないで制約を弱めるだけにする(see compiler/inference.md)
|
||||||
// fv == ?T(: Type)の場合は?T(<: U)にする
|
// fv == ?T(: Type)の場合は?T(<: U)にする
|
||||||
if fv.level() < Some(self.level) {
|
if fv.level() < Some(self.level) {
|
||||||
|
@ -2142,6 +2103,7 @@ impl Context {
|
||||||
&& !self.formal_supertype_of(&r.t, &l.t, None, None)
|
&& !self.formal_supertype_of(&r.t, &l.t, None, None)
|
||||||
{
|
{
|
||||||
return Err(TyCheckError::unification_error(
|
return Err(TyCheckError::unification_error(
|
||||||
|
line!() as usize,
|
||||||
lhs_t,
|
lhs_t,
|
||||||
rhs_t,
|
rhs_t,
|
||||||
lhs_loc,
|
lhs_loc,
|
||||||
|
@ -2196,6 +2158,7 @@ impl Context {
|
||||||
) => {
|
) => {
|
||||||
if ln != rn {
|
if ln != rn {
|
||||||
return Err(TyCheckError::unification_error(
|
return Err(TyCheckError::unification_error(
|
||||||
|
line!() as usize,
|
||||||
lhs_t,
|
lhs_t,
|
||||||
rhs_t,
|
rhs_t,
|
||||||
lhs_loc,
|
lhs_loc,
|
||||||
|
@ -2212,6 +2175,7 @@ impl Context {
|
||||||
todo!()
|
todo!()
|
||||||
}
|
}
|
||||||
(l, r) => Err(TyCheckError::unification_error(
|
(l, r) => Err(TyCheckError::unification_error(
|
||||||
|
line!() as usize,
|
||||||
l,
|
l,
|
||||||
r,
|
r,
|
||||||
lhs_loc,
|
lhs_loc,
|
||||||
|
@ -2257,6 +2221,7 @@ impl Context {
|
||||||
if ln != rn {
|
if ln != rn {
|
||||||
let before_t = Type::poly(ln.clone(), lps.clone());
|
let before_t = Type::poly(ln.clone(), lps.clone());
|
||||||
return Err(TyCheckError::re_unification_error(
|
return Err(TyCheckError::re_unification_error(
|
||||||
|
line!() as usize,
|
||||||
&before_t,
|
&before_t,
|
||||||
after_t,
|
after_t,
|
||||||
bef_loc,
|
bef_loc,
|
||||||
|
@ -2271,6 +2236,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
(l, r) if self.formal_same_type_of(l, r, None, None) => Ok(()),
|
(l, r) if self.formal_same_type_of(l, r, None, None) => Ok(()),
|
||||||
(l, r) => Err(TyCheckError::re_unification_error(
|
(l, r) => Err(TyCheckError::re_unification_error(
|
||||||
|
line!() as usize,
|
||||||
l,
|
l,
|
||||||
r,
|
r,
|
||||||
bef_loc,
|
bef_loc,
|
||||||
|
@ -2306,6 +2272,7 @@ impl Context {
|
||||||
if !maybe_sub_is_sub {
|
if !maybe_sub_is_sub {
|
||||||
let loc = sub_loc.or(sup_loc).unwrap_or(Location::Unknown);
|
let loc = sub_loc.or(sup_loc).unwrap_or(Location::Unknown);
|
||||||
return Err(TyCheckError::type_mismatch_error(
|
return Err(TyCheckError::type_mismatch_error(
|
||||||
|
line!() as usize,
|
||||||
loc,
|
loc,
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
"<???>",
|
"<???>",
|
||||||
|
@ -2318,57 +2285,47 @@ impl Context {
|
||||||
match &mut *fv.borrow_mut() {
|
match &mut *fv.borrow_mut() {
|
||||||
FreeKind::NamedUnbound { constraint, .. }
|
FreeKind::NamedUnbound { constraint, .. }
|
||||||
| FreeKind::Unbound { constraint, .. } => match constraint {
|
| FreeKind::Unbound { constraint, .. } => match constraint {
|
||||||
// sub_unify(Nat, ?T(:> Int)): (/* OK */)
|
// sub !<: l => OK (sub will widen)
|
||||||
// sub_unify(Int, ?T(:> Nat)): (?T :> Int)
|
// sup !:> l => Error
|
||||||
// sub_unify(Str, ?T(:> Int)): (/* ?T = Str or Int */) // TODO:
|
// * sub_unify(Str, ?T(:> _, <: Int)): (/* Error */)
|
||||||
Constraint::SupertypeOf(sub) => {
|
// * sub_unify(Ratio, ?T(:> _, <: Int)): (/* Error */)
|
||||||
if self.rec_full_supertype_of(l, sub) {
|
// sub = max(l, sub) if max exists
|
||||||
*constraint = Constraint::SupertypeOf(l.clone());
|
// * sub_unify(Nat, ?T(:> Int, <: _)): (/* OK */)
|
||||||
} else if self.rec_full_subtype_of(l, sub) {
|
// * sub_unify(Int, ?T(:> Nat, <: Obj)): (?T(:> Int, <: Obj))
|
||||||
/* OK */
|
// * sub_unify(Nat, ?T(:> Never, <: Add(?R, ?O))): (?T(:> Nat, <: Add(?R, ?O))
|
||||||
|
// sub = union(l, sub) if max does not exist
|
||||||
|
// * sub_unify(Str, ?T(:> Int, <: Obj)): (?T(:> Str or Int, <: Obj))
|
||||||
|
// * sub_unify({0}, ?T(:> {1}, <: Nat)): (?T(:> {0, 1}, <: Nat))
|
||||||
|
// nested variable is prohibited
|
||||||
|
// ☓ sub_unify({0}, ?T(:> ?U, <: Ord))
|
||||||
|
Constraint::Sandwiched { sub, sup } => {
|
||||||
|
if !self.rec_full_supertype_of(sup, l) {
|
||||||
|
return Err(TyCheckError::subtyping_error(
|
||||||
|
line!() as usize,
|
||||||
|
l,
|
||||||
|
sup, // TODO: this?
|
||||||
|
sub_loc,
|
||||||
|
sup_loc,
|
||||||
|
self.caused_by(),
|
||||||
|
));
|
||||||
|
}
|
||||||
|
if let Some(new_sub) = self.max(l, sub) {
|
||||||
|
*constraint =
|
||||||
|
Constraint::sandwiched(new_sub.clone(), mem::take(sup));
|
||||||
|
} else {
|
||||||
|
let new_sub = self.union(l, sub);
|
||||||
|
*constraint = Constraint::sandwiched(new_sub, mem::take(sup));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
// sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)
|
||||||
|
Constraint::TypeOf(ty) => {
|
||||||
|
if self.rec_full_supertype_of(&Type, ty) {
|
||||||
|
*constraint = Constraint::supertype_of(l.clone());
|
||||||
} else {
|
} else {
|
||||||
todo!()
|
todo!()
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// sub_unify(Nat, ?T(<: Int)): (Nat <: ?T <: Int)
|
_ => unreachable!(),
|
||||||
// sub_unify(Nat, ?T(<: Add(?R, ?O))): (Nat <: ?T <: Add(?R, ?O))
|
|
||||||
// sub_unify(Int, ?T(<: Nat)): (/* Error */)
|
|
||||||
// sub_unify(Str, ?T(<: Int)): (/* Error */)
|
|
||||||
Constraint::SubtypeOf(sup) => {
|
|
||||||
if !self.rec_full_subtype_of(l, sup) {
|
|
||||||
return Err(TyCheckError::subtyping_error(
|
|
||||||
l,
|
|
||||||
sup,
|
|
||||||
sub_loc,
|
|
||||||
sup_loc,
|
|
||||||
self.caused_by(),
|
|
||||||
));
|
|
||||||
} else {
|
|
||||||
*constraint = Constraint::sandwiched(l.clone(), mem::take(sup));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
// sub_unify(Nat, (Int <: ?T <: Ratio)): (/* OK */)
|
|
||||||
// sub_unify(Int, (Nat <: ?T <: Ratio)): (Int <: ?T <: Ratio)
|
|
||||||
// sub_unify(Str, (Nat <: ?T <: Ratio)): (/* Error */)
|
|
||||||
// sub_unify({0}, ({1} <: ?T <: Nat)): ({0, 1} <: ?T <: Nat))
|
|
||||||
Constraint::Sandwiched { sub, sup } => {
|
|
||||||
if self.rec_full_no_relation_of(l, sup) {
|
|
||||||
return Err(TyCheckError::subtyping_error(
|
|
||||||
l,
|
|
||||||
sup, // TODO:
|
|
||||||
sub_loc,
|
|
||||||
sup_loc,
|
|
||||||
self.caused_by(),
|
|
||||||
));
|
|
||||||
} else {
|
|
||||||
let union = self.union(l, sub);
|
|
||||||
*constraint = Constraint::sandwiched(union, mem::take(sub));
|
|
||||||
}
|
|
||||||
}
|
|
||||||
Constraint::TypeOf(_t) => {
|
|
||||||
*constraint = Constraint::SupertypeOf(l.clone());
|
|
||||||
}
|
|
||||||
_ => {}
|
|
||||||
},
|
},
|
||||||
_ => {}
|
_ => {}
|
||||||
}
|
}
|
||||||
|
@ -2378,47 +2335,47 @@ impl Context {
|
||||||
match &mut *fv.borrow_mut() {
|
match &mut *fv.borrow_mut() {
|
||||||
FreeKind::NamedUnbound { constraint, .. }
|
FreeKind::NamedUnbound { constraint, .. }
|
||||||
| FreeKind::Unbound { constraint, .. } => match constraint {
|
| FreeKind::Unbound { constraint, .. } => match constraint {
|
||||||
// sub_unify(?T(:> Int), Nat): (/* Error */)
|
// sub !<: r => Error
|
||||||
// sub_unify(?T(:> Nat), Int): (Nat <: ?T <: Int)
|
// * sub_unify(?T(:> Int, <: _), Nat): (/* Error */)
|
||||||
// sub_unify(?T(:> Nat), Str): (/* Error */)
|
// * sub_unify(?T(:> Nat, <: _), Str): (/* Error */)
|
||||||
Constraint::SupertypeOf(sub) => {
|
// sup !:> r => Error
|
||||||
if !self.rec_full_subtype_of(sub, r) {
|
// * sub_unify(?T(:> _, <: Str), Int): (/* Error */)
|
||||||
|
// * sub_unify(?T(:> _, <: Int), Nat): (/* Error */)
|
||||||
|
// sub <: r, sup :> r => sup = min(sup, r) if min exists
|
||||||
|
// * sub_unify(?T(:> Never, <: Nat), Int): (/* OK */)
|
||||||
|
// * sub_unify(?T(:> Nat, <: Obj), Int): (?T(:> Nat, <: Int))
|
||||||
|
// sup = union(sup, r) if min does not exist
|
||||||
|
// * sub_unify(?T(:> Never, <: {1}), {0}): (?T(:> Never, <: {0, 1}))
|
||||||
|
Constraint::Sandwiched { sub, sup } => {
|
||||||
|
if !self.rec_full_subtype_of(sub, r)
|
||||||
|
|| !self.rec_full_supertype_of(sup, r)
|
||||||
|
{
|
||||||
return Err(TyCheckError::subtyping_error(
|
return Err(TyCheckError::subtyping_error(
|
||||||
|
line!() as usize,
|
||||||
sub,
|
sub,
|
||||||
r,
|
r,
|
||||||
sub_loc,
|
sub_loc,
|
||||||
sup_loc,
|
sup_loc,
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
));
|
));
|
||||||
|
}
|
||||||
|
if let Some(new_sup) = self.min(sup, r) {
|
||||||
|
*constraint =
|
||||||
|
Constraint::sandwiched(mem::take(sub), new_sup.clone());
|
||||||
} else {
|
} else {
|
||||||
*constraint = Constraint::sandwiched(sub.clone(), r.clone());
|
let new_sup = self.union(sup, r);
|
||||||
|
*constraint = Constraint::sandwiched(mem::take(sub), new_sup);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
// sub_unify(?T(<: Int), Nat): (?T(<: Nat))
|
|
||||||
// sub_unify(?T(<: Nat), Int): (/* OK */)
|
|
||||||
// sub_unify(?T(<: Str), Int): (/* Error */) // TODO:
|
|
||||||
Constraint::SubtypeOf(sup) if self.rec_full_supertype_of(sup, r) => {
|
|
||||||
*constraint = Constraint::SubtypeOf(r.clone());
|
|
||||||
}
|
|
||||||
// sub_unify((Int <: ?T <: Ratio), Nat): (/* Error */)
|
|
||||||
// sub_unify((Nat <: ?T <: Ratio), Int): (/* OK */)
|
|
||||||
// sub_unify((Nat <: ?T <: Int), Str): (/* Error */)
|
|
||||||
Constraint::Sandwiched { sub, sup: _ }
|
|
||||||
if !self.rec_full_subtype_of(sub, r) =>
|
|
||||||
{
|
|
||||||
return Err(TyCheckError::subtyping_error(
|
|
||||||
sub,
|
|
||||||
r,
|
|
||||||
sub_loc,
|
|
||||||
sup_loc,
|
|
||||||
self.caused_by(),
|
|
||||||
))
|
|
||||||
}
|
|
||||||
// sub_unify(?T(: Type), Int): (?T(<: Int))
|
// sub_unify(?T(: Type), Int): (?T(<: Int))
|
||||||
Constraint::TypeOf(_t) => {
|
Constraint::TypeOf(ty) => {
|
||||||
*constraint = Constraint::SubtypeOf(r.clone());
|
if self.rec_full_supertype_of(&Type, ty) {
|
||||||
|
*constraint = Constraint::subtype_of(r.clone());
|
||||||
|
} else {
|
||||||
|
todo!()
|
||||||
|
}
|
||||||
}
|
}
|
||||||
_ => {}
|
_ => unreachable!(),
|
||||||
},
|
},
|
||||||
_ => {}
|
_ => {}
|
||||||
}
|
}
|
||||||
|
@ -2502,6 +2459,7 @@ impl Context {
|
||||||
ast::VarPattern::Discard(token) => {
|
ast::VarPattern::Discard(token) => {
|
||||||
if self.unify(&spec_t, body_t, None, Some(sig.loc())).is_err() {
|
if self.unify(&spec_t, body_t, None, Some(sig.loc())).is_err() {
|
||||||
return Err(TyCheckError::type_mismatch_error(
|
return Err(TyCheckError::type_mismatch_error(
|
||||||
|
line!() as usize,
|
||||||
token.loc(),
|
token.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
"_",
|
"_",
|
||||||
|
@ -2513,6 +2471,7 @@ impl Context {
|
||||||
ast::VarPattern::VarName(n) => {
|
ast::VarPattern::VarName(n) => {
|
||||||
if self.unify(&spec_t, body_t, None, Some(sig.loc())).is_err() {
|
if self.unify(&spec_t, body_t, None, Some(sig.loc())).is_err() {
|
||||||
return Err(TyCheckError::type_mismatch_error(
|
return Err(TyCheckError::type_mismatch_error(
|
||||||
|
line!() as usize,
|
||||||
n.loc(),
|
n.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
n.inspect(),
|
n.inspect(),
|
||||||
|
@ -2804,7 +2763,7 @@ impl Context {
|
||||||
// REVIEW: 型境界の左辺に来れるのは型変数だけか?
|
// REVIEW: 型境界の左辺に来れるのは型変数だけか?
|
||||||
// TODO: 高階型変数
|
// TODO: 高階型変数
|
||||||
match bound {
|
match bound {
|
||||||
TypeBoundSpec::Subtype { sub, sup } => Ok(TyBound::subtype(
|
TypeBoundSpec::Subtype { sub, sup } => Ok(TyBound::subtype_of(
|
||||||
Type::mono_q(sub.inspect().clone()),
|
Type::mono_q(sub.inspect().clone()),
|
||||||
self.instantiate_typespec(sup, mode)?,
|
self.instantiate_typespec(sup, mode)?,
|
||||||
)),
|
)),
|
||||||
|
@ -2857,6 +2816,7 @@ impl Context {
|
||||||
Ok(ctx)
|
Ok(ctx)
|
||||||
} else {
|
} else {
|
||||||
Err(TyCheckError::no_var_error(
|
Err(TyCheckError::no_var_error(
|
||||||
|
line!() as usize,
|
||||||
obj.loc(),
|
obj.loc(),
|
||||||
namespace.clone(),
|
namespace.clone(),
|
||||||
name.inspect(),
|
name.inspect(),
|
||||||
|
@ -2883,6 +2843,7 @@ impl Context {
|
||||||
let t = pos_arg.expr.ref_t();
|
let t = pos_arg.expr.ref_t();
|
||||||
if !matches!(&pos_arg.expr, hir::Expr::Lambda(_)) {
|
if !matches!(&pos_arg.expr, hir::Expr::Lambda(_)) {
|
||||||
return Err(TyCheckError::type_mismatch_error(
|
return Err(TyCheckError::type_mismatch_error(
|
||||||
|
line!() as usize,
|
||||||
pos_arg.loc(),
|
pos_arg.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
"match",
|
"match",
|
||||||
|
@ -2901,6 +2862,7 @@ impl Context {
|
||||||
}
|
}
|
||||||
if lambda.params.len() != 1 {
|
if lambda.params.len() != 1 {
|
||||||
return Err(TyCheckError::argument_error(
|
return Err(TyCheckError::argument_error(
|
||||||
|
line!() as usize,
|
||||||
pos_args[i + 1].loc(),
|
pos_args[i + 1].loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
1,
|
1,
|
||||||
|
@ -2917,6 +2879,7 @@ impl Context {
|
||||||
&& !self.formal_supertype_of(&union_pat_t, expr_t, None, None)
|
&& !self.formal_supertype_of(&union_pat_t, expr_t, None, None)
|
||||||
{
|
{
|
||||||
return Err(TyCheckError::match_error(
|
return Err(TyCheckError::match_error(
|
||||||
|
line!() as usize,
|
||||||
pos_args[0].loc(),
|
pos_args[0].loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
expr_t,
|
expr_t,
|
||||||
|
@ -2957,6 +2920,7 @@ impl Context {
|
||||||
return parent.get_var_t(name, namespace);
|
return parent.get_var_t(name, namespace);
|
||||||
}
|
}
|
||||||
Err(TyCheckError::no_var_error(
|
Err(TyCheckError::no_var_error(
|
||||||
|
line!() as usize,
|
||||||
name.loc(),
|
name.loc(),
|
||||||
namespace.clone(),
|
namespace.clone(),
|
||||||
name.inspect(),
|
name.inspect(),
|
||||||
|
@ -2993,6 +2957,7 @@ impl Context {
|
||||||
parent.get_attr_t(obj, name, namespace)
|
parent.get_attr_t(obj, name, namespace)
|
||||||
} else {
|
} else {
|
||||||
Err(TyCheckError::no_attr_error(
|
Err(TyCheckError::no_attr_error(
|
||||||
|
line!() as usize,
|
||||||
name.loc(),
|
name.loc(),
|
||||||
namespace.clone(),
|
namespace.clone(),
|
||||||
&self_t,
|
&self_t,
|
||||||
|
@ -3177,12 +3142,7 @@ impl Context {
|
||||||
self.rec_full_supertype_of(rhs, lhs)
|
self.rec_full_supertype_of(rhs, lhs)
|
||||||
}
|
}
|
||||||
|
|
||||||
/// !(L :> R || L <: R)
|
pub(crate) fn rec_full_same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
||||||
pub(crate) fn rec_full_no_relation_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
|
||||||
!self.rec_full_supertype_of(lhs, rhs) && !self.rec_full_subtype_of(lhs, rhs)
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) fn _rec_full_same_type_of(&self, lhs: &Type, rhs: &Type) -> bool {
|
|
||||||
self.rec_full_supertype_of(lhs, rhs) && self.rec_full_subtype_of(lhs, rhs)
|
self.rec_full_supertype_of(lhs, rhs) && self.rec_full_subtype_of(lhs, rhs)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -3323,12 +3283,8 @@ impl Context {
|
||||||
FreeKind::Unbound { constraint, .. }
|
FreeKind::Unbound { constraint, .. }
|
||||||
| FreeKind::NamedUnbound { constraint, .. } => match constraint {
|
| FreeKind::NamedUnbound { constraint, .. } => match constraint {
|
||||||
// `(?T <: Int) :> Nat` can be true, `(?T <: Nat) :> Int` is false
|
// `(?T <: Int) :> Nat` can be true, `(?T <: Nat) :> Int` is false
|
||||||
Constraint::SubtypeOf(sup) => {
|
|
||||||
self.formal_supertype_of(sup, rhs, bounds, lhs_variance)
|
|
||||||
}
|
|
||||||
// `(?T :> X) :> Y` is true
|
// `(?T :> X) :> Y` is true
|
||||||
// `(?T :> Str) :> Int` is true (?T :> Str or Int)
|
// `(?T :> Str) :> Int` is true (?T :> Str or Int)
|
||||||
Constraint::SupertypeOf(_sub) => true,
|
|
||||||
// `(Nat <: ?T <: Ratio) :> Nat` can be true
|
// `(Nat <: ?T <: Ratio) :> Nat` can be true
|
||||||
Constraint::Sandwiched { sup, .. } => {
|
Constraint::Sandwiched { sup, .. } => {
|
||||||
self.formal_supertype_of(sup, rhs, bounds, lhs_variance)
|
self.formal_supertype_of(sup, rhs, bounds, lhs_variance)
|
||||||
|
@ -3356,14 +3312,7 @@ impl Context {
|
||||||
// `Nat :> (?T <: Int)` can be true
|
// `Nat :> (?T <: Int)` can be true
|
||||||
// `Int :> (?T <: Nat)` can be true
|
// `Int :> (?T <: Nat)` can be true
|
||||||
// `Str :> (?T <: Int)` is false
|
// `Str :> (?T <: Int)` is false
|
||||||
Constraint::SubtypeOf(sup) => {
|
|
||||||
self.formal_supertype_of(lhs, sup, bounds, lhs_variance)
|
|
||||||
|| self.formal_subtype_of(lhs, sup, bounds, lhs_variance)
|
|
||||||
}
|
|
||||||
// `Int :> (?T :> Nat)` can be true, `Nat :> (?T :> Int)` is false
|
// `Int :> (?T :> Nat)` can be true, `Nat :> (?T :> Int)` is false
|
||||||
Constraint::SupertypeOf(sub) => {
|
|
||||||
self.formal_supertype_of(lhs, sub, bounds, lhs_variance)
|
|
||||||
}
|
|
||||||
// `Int :> (Nat <: ?T <: Ratio)` can be true, `Nat :> (Int <: ?T <: Ratio)` is false
|
// `Int :> (Nat <: ?T <: Ratio)` can be true, `Nat :> (Int <: ?T <: Ratio)` is false
|
||||||
Constraint::Sandwiched { sub, sup: _ } => {
|
Constraint::Sandwiched { sub, sup: _ } => {
|
||||||
self.formal_supertype_of(lhs, sub, bounds, lhs_variance)
|
self.formal_supertype_of(lhs, sub, bounds, lhs_variance)
|
||||||
|
@ -3752,17 +3701,14 @@ impl Context {
|
||||||
|
|
||||||
fn is_sub_constraint_of(&self, l: &Constraint, r: &Constraint) -> bool {
|
fn is_sub_constraint_of(&self, l: &Constraint, r: &Constraint) -> bool {
|
||||||
match (l, r) {
|
match (l, r) {
|
||||||
// |T <: Nat| <: |T <: Int|
|
|
||||||
// |I: Nat| <: |I: Int|
|
// |I: Nat| <: |I: Int|
|
||||||
(Constraint::SubtypeOf(lhs), Constraint::SubtypeOf(rhs))
|
(Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => {
|
||||||
| (Constraint::TypeOf(lhs), Constraint::TypeOf(rhs)) => {
|
|
||||||
self.rec_full_subtype_of(lhs, rhs)
|
self.rec_full_subtype_of(lhs, rhs)
|
||||||
}
|
}
|
||||||
|
// |T <: Int| <: |T: Type|
|
||||||
|
(Constraint::Sandwiched { sub: Never, .. }, Constraint::TypeOf(Type)) => true,
|
||||||
// |Int <: T| <: |Nat <: T|
|
// |Int <: T| <: |Nat <: T|
|
||||||
(Constraint::SupertypeOf(lhs), Constraint::SupertypeOf(rhs)) => {
|
// |T <: Nat| <: |T <: Int|
|
||||||
self.rec_full_supertype_of(lhs, rhs)
|
|
||||||
}
|
|
||||||
(Constraint::SubtypeOf(_), Constraint::TypeOf(Type)) => true,
|
|
||||||
// |Int <: T <: Ratio| <: |Nat <: T <: Complex|
|
// |Int <: T <: Ratio| <: |Nat <: T <: Complex|
|
||||||
(
|
(
|
||||||
Constraint::Sandwiched {
|
Constraint::Sandwiched {
|
||||||
|
@ -3853,6 +3799,18 @@ impl Context {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn max<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> Option<&'t Type> {
|
||||||
|
// 同じならどちらを返しても良い
|
||||||
|
match (
|
||||||
|
self.rec_full_supertype_of(lhs, rhs),
|
||||||
|
self.rec_full_subtype_of(lhs, rhs),
|
||||||
|
) {
|
||||||
|
(true, true) | (true, false) => Some(lhs),
|
||||||
|
(false, true) => Some(rhs),
|
||||||
|
(false, false) => None,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
fn cmp_t<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> TyParamOrdering {
|
fn cmp_t<'t>(&self, lhs: &'t Type, rhs: &'t Type) -> TyParamOrdering {
|
||||||
match self.min(lhs, rhs) {
|
match self.min(lhs, rhs) {
|
||||||
Some(l) if l == lhs => TyParamOrdering::Less,
|
Some(l) if l == lhs => TyParamOrdering::Less,
|
||||||
|
@ -3886,6 +3844,7 @@ impl Context {
|
||||||
return parent.get_local(name, namespace);
|
return parent.get_local(name, namespace);
|
||||||
}
|
}
|
||||||
Err(TyCheckError::no_var_error(
|
Err(TyCheckError::no_var_error(
|
||||||
|
line!() as usize,
|
||||||
name.loc(),
|
name.loc(),
|
||||||
namespace.clone(),
|
namespace.clone(),
|
||||||
name.inspect(),
|
name.inspect(),
|
||||||
|
@ -3911,6 +3870,7 @@ impl Context {
|
||||||
parent._get_attr(obj, name, namespace)
|
parent._get_attr(obj, name, namespace)
|
||||||
} else {
|
} else {
|
||||||
Err(TyCheckError::no_attr_error(
|
Err(TyCheckError::no_attr_error(
|
||||||
|
line!() as usize,
|
||||||
name.loc(),
|
name.loc(),
|
||||||
namespace.clone(),
|
namespace.clone(),
|
||||||
&self_t,
|
&self_t,
|
||||||
|
@ -3973,6 +3933,7 @@ impl Context {
|
||||||
let mut uninited_errs = TyCheckErrors::empty();
|
let mut uninited_errs = TyCheckErrors::empty();
|
||||||
for (name, vi) in self.decls.iter() {
|
for (name, vi) in self.decls.iter() {
|
||||||
uninited_errs.push(TyCheckError::uninitialized_error(
|
uninited_errs.push(TyCheckError::uninitialized_error(
|
||||||
|
line!() as usize,
|
||||||
name.loc(),
|
name.loc(),
|
||||||
self.caused_by(),
|
self.caused_by(),
|
||||||
name.inspect(),
|
name.inspect(),
|
||||||
|
|
|
@ -97,8 +97,11 @@ impl SideEffectChecker {
|
||||||
(true, _) => {
|
(true, _) => {
|
||||||
if !allow_inner_effect {
|
if !allow_inner_effect {
|
||||||
let expr = Expr::Def(def.clone());
|
let expr = Expr::Def(def.clone());
|
||||||
self.errs
|
self.errs.push(EffectError::has_effect(
|
||||||
.push(EffectError::has_effect(&expr, self.full_path()));
|
line!() as usize,
|
||||||
|
&expr,
|
||||||
|
self.full_path(),
|
||||||
|
));
|
||||||
}
|
}
|
||||||
for chunk in def.body.block.iter() {
|
for chunk in def.body.block.iter() {
|
||||||
self.check_expr(chunk, allow_inner_effect);
|
self.check_expr(chunk, allow_inner_effect);
|
||||||
|
@ -165,8 +168,11 @@ impl SideEffectChecker {
|
||||||
// 引数がproceduralでも関数呼び出しなら副作用なし
|
// 引数がproceduralでも関数呼び出しなら副作用なし
|
||||||
Expr::Call(call) => {
|
Expr::Call(call) => {
|
||||||
if self.is_procedural(&call.obj) && !allow_self_effect {
|
if self.is_procedural(&call.obj) && !allow_self_effect {
|
||||||
self.errs
|
self.errs.push(EffectError::has_effect(
|
||||||
.push(EffectError::has_effect(expr, self.full_path()));
|
line!() as usize,
|
||||||
|
expr,
|
||||||
|
self.full_path(),
|
||||||
|
));
|
||||||
}
|
}
|
||||||
call.args
|
call.args
|
||||||
.pos_args
|
.pos_args
|
||||||
|
@ -192,8 +198,11 @@ impl SideEffectChecker {
|
||||||
self.path_stack.push((Str::ever("<lambda>"), Private));
|
self.path_stack.push((Str::ever("<lambda>"), Private));
|
||||||
}
|
}
|
||||||
if !allow_self_effect && is_proc {
|
if !allow_self_effect && is_proc {
|
||||||
self.errs
|
self.errs.push(EffectError::has_effect(
|
||||||
.push(EffectError::has_effect(expr, self.full_path()));
|
line!() as usize,
|
||||||
|
expr,
|
||||||
|
self.full_path(),
|
||||||
|
));
|
||||||
}
|
}
|
||||||
lambda
|
lambda
|
||||||
.body
|
.body
|
||||||
|
|
|
@ -248,10 +248,10 @@ impl TyCheckError {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn feature_error(loc: Location, name: &str, caused_by: Str) -> Self {
|
pub fn feature_error(errno: usize, loc: Location, name: &str, caused_by: Str) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
FeatureError,
|
FeatureError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -277,11 +277,11 @@ impl TyCheckError {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn duplicate_decl_error(loc: Location, caused_by: Str, name: &str) -> Self {
|
pub fn duplicate_decl_error(errno: usize, loc: Location, caused_by: Str, name: &str) -> Self {
|
||||||
let name = readable_name(name);
|
let name = readable_name(name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
NameError,
|
NameError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -295,6 +295,7 @@ impl TyCheckError {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn violate_decl_error(
|
pub fn violate_decl_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
name: &str,
|
name: &str,
|
||||||
|
@ -304,7 +305,7 @@ impl TyCheckError {
|
||||||
let name = readable_name(name);
|
let name = readable_name(name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -317,11 +318,11 @@ impl TyCheckError {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn no_type_spec_error(loc: Location, caused_by: Str, name: &str) -> Self {
|
pub fn no_type_spec_error(errno: usize, loc: Location, caused_by: Str, name: &str) -> Self {
|
||||||
let name = readable_name(name);
|
let name = readable_name(name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -335,6 +336,7 @@ impl TyCheckError {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn no_var_error(
|
pub fn no_var_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
name: &str,
|
name: &str,
|
||||||
|
@ -351,7 +353,7 @@ impl TyCheckError {
|
||||||
});
|
});
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
NameError,
|
NameError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -365,6 +367,7 @@ impl TyCheckError {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn no_attr_error(
|
pub fn no_attr_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
obj_t: &Type,
|
obj_t: &Type,
|
||||||
|
@ -381,7 +384,7 @@ impl TyCheckError {
|
||||||
});
|
});
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
AttributeError,
|
AttributeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -395,6 +398,7 @@ impl TyCheckError {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn callable_impl_error<'a, C: Locational + Display>(
|
pub fn callable_impl_error<'a, C: Locational + Display>(
|
||||||
|
errno: usize,
|
||||||
callee: &C,
|
callee: &C,
|
||||||
param_ts: impl Iterator<Item = &'a Type>,
|
param_ts: impl Iterator<Item = &'a Type>,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
|
@ -402,7 +406,7 @@ impl TyCheckError {
|
||||||
let param_ts = fmt_iter(param_ts);
|
let param_ts = fmt_iter(param_ts);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
NotImplementedError,
|
NotImplementedError,
|
||||||
callee.loc(),
|
callee.loc(),
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -420,6 +424,7 @@ impl TyCheckError {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn type_mismatch_error(
|
pub fn type_mismatch_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
name: &str,
|
name: &str,
|
||||||
|
@ -428,7 +433,7 @@ impl TyCheckError {
|
||||||
) -> Self {
|
) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -442,6 +447,7 @@ impl TyCheckError {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn return_type_error(
|
pub fn return_type_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
name: &str,
|
name: &str,
|
||||||
|
@ -450,7 +456,7 @@ impl TyCheckError {
|
||||||
) -> Self {
|
) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -463,10 +469,16 @@ impl TyCheckError {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn uninitialized_error(loc: Location, caused_by: Str, name: &str, t: &Type) -> Self {
|
pub fn uninitialized_error(
|
||||||
|
errno: usize,
|
||||||
|
loc: Location,
|
||||||
|
caused_by: Str,
|
||||||
|
name: &str,
|
||||||
|
t: &Type,
|
||||||
|
) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
NameError,
|
NameError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -479,10 +491,16 @@ impl TyCheckError {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn argument_error(loc: Location, caused_by: Str, expect: usize, found: usize) -> Self {
|
pub fn argument_error(
|
||||||
|
errno: usize,
|
||||||
|
loc: Location,
|
||||||
|
caused_by: Str,
|
||||||
|
expect: usize,
|
||||||
|
found: usize,
|
||||||
|
) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -495,10 +513,10 @@ impl TyCheckError {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn match_error(loc: Location, caused_by: Str, expr_t: &Type) -> Self {
|
pub fn match_error(errno: usize, loc: Location, caused_by: Str, expr_t: &Type) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -511,10 +529,10 @@ impl TyCheckError {
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn infer_error(loc: Location, caused_by: Str, expr: &str) -> Self {
|
pub fn infer_error(errno: usize, loc: Location, caused_by: Str, expr: &str) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -535,11 +553,11 @@ impl TyCheckError {
|
||||||
Self::new(ErrorCore::unreachable(fn_name, line), "".into())
|
Self::new(ErrorCore::unreachable(fn_name, line), "".into())
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn reassign_error(loc: Location, caused_by: Str, name: &str) -> Self {
|
pub fn reassign_error(errno: usize, loc: Location, caused_by: Str, name: &str) -> Self {
|
||||||
let name = readable_name(name);
|
let name = readable_name(name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
AssignError,
|
AssignError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -553,6 +571,7 @@ impl TyCheckError {
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn too_many_args_error(
|
pub fn too_many_args_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
callee_name: &str,
|
callee_name: &str,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
|
@ -563,7 +582,7 @@ impl TyCheckError {
|
||||||
let name = readable_name(callee_name);
|
let name = readable_name(callee_name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -587,6 +606,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn multiple_args_error(
|
pub fn multiple_args_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
callee_name: &str,
|
callee_name: &str,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
|
@ -595,7 +615,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
let name = readable_name(callee_name);
|
let name = readable_name(callee_name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -609,6 +629,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn unexpected_kw_arg_error(
|
pub fn unexpected_kw_arg_error(
|
||||||
|
errno: usize,
|
||||||
loc: Location,
|
loc: Location,
|
||||||
callee_name: &str,
|
callee_name: &str,
|
||||||
caused_by: Str,
|
caused_by: Str,
|
||||||
|
@ -617,7 +638,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
let name = readable_name(callee_name);
|
let name = readable_name(callee_name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -630,11 +651,11 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn unused_warning(loc: Location, name: &str, caused_by: Str) -> Self {
|
pub fn unused_warning(errno: usize, loc: Location, name: &str, caused_by: Str) -> Self {
|
||||||
let name = readable_name(name);
|
let name = readable_name(name);
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
UnusedWarning,
|
UnusedWarning,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -648,6 +669,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn unification_error(
|
pub fn unification_error(
|
||||||
|
errno: usize,
|
||||||
lhs_t: &Type,
|
lhs_t: &Type,
|
||||||
rhs_t: &Type,
|
rhs_t: &Type,
|
||||||
lhs_loc: Option<Location>,
|
lhs_loc: Option<Location>,
|
||||||
|
@ -662,7 +684,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
};
|
};
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -676,6 +698,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn re_unification_error(
|
pub fn re_unification_error(
|
||||||
|
errno: usize,
|
||||||
lhs_t: &Type,
|
lhs_t: &Type,
|
||||||
rhs_t: &Type,
|
rhs_t: &Type,
|
||||||
lhs_loc: Option<Location>,
|
lhs_loc: Option<Location>,
|
||||||
|
@ -690,7 +713,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
};
|
};
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -704,6 +727,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn subtyping_error(
|
pub fn subtyping_error(
|
||||||
|
errno: usize,
|
||||||
sub_t: &Type,
|
sub_t: &Type,
|
||||||
sup_t: &Type,
|
sup_t: &Type,
|
||||||
sub_loc: Option<Location>,
|
sub_loc: Option<Location>,
|
||||||
|
@ -718,7 +742,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
};
|
};
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
loc,
|
loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -731,10 +755,15 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn pred_unification_error(lhs: &Predicate, rhs: &Predicate, caused_by: Str) -> Self {
|
pub fn pred_unification_error(
|
||||||
|
errno: usize,
|
||||||
|
lhs: &Predicate,
|
||||||
|
rhs: &Predicate,
|
||||||
|
caused_by: Str,
|
||||||
|
) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
TypeError,
|
TypeError,
|
||||||
Location::Unknown,
|
Location::Unknown,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -747,10 +776,10 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
)
|
)
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn has_effect<S: Into<Str>>(expr: &Expr, caused_by: S) -> Self {
|
pub fn has_effect<S: Into<Str>>(errno: usize, expr: &Expr, caused_by: S) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
HasEffect,
|
HasEffect,
|
||||||
expr.loc(),
|
expr.loc(),
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
@ -764,6 +793,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
}
|
}
|
||||||
|
|
||||||
pub fn move_error<S: Into<Str>>(
|
pub fn move_error<S: Into<Str>>(
|
||||||
|
errno: usize,
|
||||||
name: &str,
|
name: &str,
|
||||||
name_loc: Location,
|
name_loc: Location,
|
||||||
moved_loc: Location,
|
moved_loc: Location,
|
||||||
|
@ -771,7 +801,7 @@ passed keyword args: {RED}{kw_args_len}{RESET}"
|
||||||
) -> Self {
|
) -> Self {
|
||||||
Self::new(
|
Self::new(
|
||||||
ErrorCore::new(
|
ErrorCore::new(
|
||||||
0,
|
errno,
|
||||||
MoveError,
|
MoveError,
|
||||||
name_loc,
|
name_loc,
|
||||||
switch_lang!(
|
switch_lang!(
|
||||||
|
|
|
@ -399,14 +399,6 @@ impl Evaluator {
|
||||||
level: usize,
|
level: usize,
|
||||||
) -> EvalResult<TyBound> {
|
) -> EvalResult<TyBound> {
|
||||||
match bound {
|
match bound {
|
||||||
TyBound::Subtype { sub, sup } => Ok(TyBound::subtype(
|
|
||||||
self.eval_t_params(sub, ctx, level)?,
|
|
||||||
self.eval_t_params(sup, ctx, level)?,
|
|
||||||
)),
|
|
||||||
TyBound::Supertype { sup, sub } => Ok(TyBound::supertype(
|
|
||||||
self.eval_t_params(sup, ctx, level)?,
|
|
||||||
self.eval_t_params(sub, ctx, level)?,
|
|
||||||
)),
|
|
||||||
TyBound::Sandwiched { sub, mid, sup } => {
|
TyBound::Sandwiched { sub, mid, sup } => {
|
||||||
let sub = self.eval_t_params(sub, ctx, level)?;
|
let sub = self.eval_t_params(sub, ctx, level)?;
|
||||||
let mid = self.eval_t_params(mid, ctx, level)?;
|
let mid = self.eval_t_params(mid, ctx, level)?;
|
||||||
|
|
|
@ -122,7 +122,7 @@ impl Context {
|
||||||
let op_t = quant(
|
let op_t = quant(
|
||||||
op_t,
|
op_t,
|
||||||
set! {
|
set! {
|
||||||
subtype(mono_q("Self"), poly("Eq", vec![ty_tp(mono_q("R"))])),
|
subtypeof(mono_q("Self"), poly("Eq", vec![ty_tp(mono_q("R"))])),
|
||||||
static_instance("R", Type)
|
static_instance("R", Type)
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
|
@ -137,7 +137,7 @@ impl Context {
|
||||||
let op_t = quant(
|
let op_t = quant(
|
||||||
op_t,
|
op_t,
|
||||||
set! {
|
set! {
|
||||||
subtype(mono_q("Self"), poly("PartialOrd", vec![ty_tp(mono_q("R"))])),
|
subtypeof(mono_q("Self"), poly("PartialOrd", vec![ty_tp(mono_q("R"))])),
|
||||||
static_instance("R", Type)
|
static_instance("R", Type)
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
|
@ -157,13 +157,13 @@ impl Context {
|
||||||
let t = fn0_met(self_t.clone(), Nat);
|
let t = fn0_met(self_t.clone(), Nat);
|
||||||
let t = quant(
|
let t = quant(
|
||||||
t,
|
t,
|
||||||
set! {subtype(self_t.clone(), poly("Seq", vec![TyParam::erased(Type)]))},
|
set! {subtypeof(self_t.clone(), poly("Seq", vec![TyParam::erased(Type)]))},
|
||||||
);
|
);
|
||||||
seq.register_decl("__len__", t, Public);
|
seq.register_decl("__len__", t, Public);
|
||||||
let t = Type::fn1_met(self_t.clone(), Nat, mono_q("T"));
|
let t = Type::fn1_met(self_t.clone(), Nat, mono_q("T"));
|
||||||
let t = quant(
|
let t = quant(
|
||||||
t,
|
t,
|
||||||
set! {subtype(self_t, poly("Seq", vec![ty_tp(mono_q("T"))])), static_instance("T", Type)},
|
set! {subtypeof(self_t, poly("Seq", vec![ty_tp(mono_q("T"))])), static_instance("T", Type)},
|
||||||
);
|
);
|
||||||
// Seq.get: |Self <: Seq(T)| Self.(Nat) -> T
|
// Seq.get: |Self <: Seq(T)| Self.(Nat) -> T
|
||||||
seq.register_decl("get", t, Public);
|
seq.register_decl("get", t, Public);
|
||||||
|
@ -180,7 +180,7 @@ impl Context {
|
||||||
vec![poly("Output", vec![ty_tp(mono_q("R"))])],
|
vec![poly("Output", vec![ty_tp(mono_q("R"))])],
|
||||||
Self::TOP_LEVEL,
|
Self::TOP_LEVEL,
|
||||||
);
|
);
|
||||||
let self_bound = subtype(mono_q("Self"), poly("Add", ty_params.clone()));
|
let self_bound = subtypeof(mono_q("Self"), poly("Add", ty_params.clone()));
|
||||||
let op_t = fn1_met(
|
let op_t = fn1_met(
|
||||||
poly_q("Self", ty_params.clone()),
|
poly_q("Self", ty_params.clone()),
|
||||||
r.clone(),
|
r.clone(),
|
||||||
|
@ -195,7 +195,7 @@ impl Context {
|
||||||
vec![poly("Output", vec![ty_tp(mono_q("R"))])],
|
vec![poly("Output", vec![ty_tp(mono_q("R"))])],
|
||||||
Self::TOP_LEVEL,
|
Self::TOP_LEVEL,
|
||||||
);
|
);
|
||||||
let self_bound = subtype(mono_q("Self"), poly("Sub", ty_params.clone()));
|
let self_bound = subtypeof(mono_q("Self"), poly("Sub", ty_params.clone()));
|
||||||
let op_t = fn1_met(
|
let op_t = fn1_met(
|
||||||
poly_q("Self", ty_params.clone()),
|
poly_q("Self", ty_params.clone()),
|
||||||
r.clone(),
|
r.clone(),
|
||||||
|
@ -275,7 +275,7 @@ impl Context {
|
||||||
fn init_builtin_classes(&mut self) {
|
fn init_builtin_classes(&mut self) {
|
||||||
let mut obj = Self::mono_class("Obj", vec![], vec![], Self::TOP_LEVEL);
|
let mut obj = Self::mono_class("Obj", vec![], vec![], Self::TOP_LEVEL);
|
||||||
let t = fn0_met(mono_q("Self"), mono_q("Self"));
|
let t = fn0_met(mono_q("Self"), mono_q("Self"));
|
||||||
let t = quant(t, set! {subtype(mono_q("Self"), mono("Obj"))});
|
let t = quant(t, set! {subtypeof(mono_q("Self"), mono("Obj"))});
|
||||||
obj.register_impl("clone", t, Const, Public);
|
obj.register_impl("clone", t, Const, Public);
|
||||||
obj.register_impl("__module__", Str, Const, Public);
|
obj.register_impl("__module__", Str, Const, Public);
|
||||||
obj.register_impl("__sizeof__", fn0_met(Obj, Nat), Const, Public);
|
obj.register_impl("__sizeof__", fn0_met(Obj, Nat), Const, Public);
|
||||||
|
@ -676,7 +676,7 @@ impl Context {
|
||||||
op_t,
|
op_t,
|
||||||
set! {
|
set! {
|
||||||
static_instance("R", Type),
|
static_instance("R", Type),
|
||||||
subtype(l.clone(), poly("Add", params.clone()))
|
subtypeof(l.clone(), poly("Add", params.clone()))
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
self.register_impl("__add__", op_t, Const, Private);
|
self.register_impl("__add__", op_t, Const, Private);
|
||||||
|
@ -685,7 +685,7 @@ impl Context {
|
||||||
op_t,
|
op_t,
|
||||||
set! {
|
set! {
|
||||||
static_instance("R", Type),
|
static_instance("R", Type),
|
||||||
subtype(l.clone(), poly("Sub", params.clone()))
|
subtypeof(l.clone(), poly("Sub", params.clone()))
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
self.register_impl("__sub__", op_t, Const, Private);
|
self.register_impl("__sub__", op_t, Const, Private);
|
||||||
|
@ -694,7 +694,7 @@ impl Context {
|
||||||
op_t,
|
op_t,
|
||||||
set! {
|
set! {
|
||||||
static_instance("R", Type),
|
static_instance("R", Type),
|
||||||
subtype(l.clone(), poly("Mul", params.clone()))
|
subtypeof(l.clone(), poly("Mul", params.clone()))
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
self.register_impl("__mul__", op_t, Const, Private);
|
self.register_impl("__mul__", op_t, Const, Private);
|
||||||
|
@ -703,27 +703,27 @@ impl Context {
|
||||||
op_t,
|
op_t,
|
||||||
set! {
|
set! {
|
||||||
static_instance("R", Type),
|
static_instance("R", Type),
|
||||||
subtype(l, poly("Mul", params.clone()))
|
subtypeof(l, poly("Mul", params.clone()))
|
||||||
},
|
},
|
||||||
);
|
);
|
||||||
self.register_impl("__div__", op_t, Const, Private);
|
self.register_impl("__div__", op_t, Const, Private);
|
||||||
let m = mono_q("M");
|
let m = mono_q("M");
|
||||||
let op_t = Type::func2(m.clone(), m.clone(), m.clone());
|
let op_t = Type::func2(m.clone(), m.clone(), m.clone());
|
||||||
let op_t = quant(op_t, set! {subtype(m, poly("Mul", vec![]))});
|
let op_t = quant(op_t, set! {subtypeof(m, poly("Mul", vec![]))});
|
||||||
// TODO: add bound: M == MulO
|
// TODO: add bound: M == MulO
|
||||||
self.register_impl("__pow__", op_t, Const, Private);
|
self.register_impl("__pow__", op_t, Const, Private);
|
||||||
let d = mono_q("D");
|
let d = mono_q("D");
|
||||||
let op_t = Type::func2(d.clone(), d.clone(), d.clone());
|
let op_t = Type::func2(d.clone(), d.clone(), d.clone());
|
||||||
let op_t = quant(op_t, set! {subtype(d, poly("Div", vec![]))});
|
let op_t = quant(op_t, set! {subtypeof(d, poly("Div", vec![]))});
|
||||||
self.register_impl("__mod__", op_t, Const, Private);
|
self.register_impl("__mod__", op_t, Const, Private);
|
||||||
let e = mono_q("E");
|
let e = mono_q("E");
|
||||||
let op_t = Type::func2(e.clone(), e.clone(), Bool);
|
let op_t = Type::func2(e.clone(), e.clone(), Bool);
|
||||||
let op_t = quant(op_t, set! {subtype(e, poly("Eq", vec![]))});
|
let op_t = quant(op_t, set! {subtypeof(e, poly("Eq", vec![]))});
|
||||||
self.register_impl("__eq__", op_t.clone(), Const, Private);
|
self.register_impl("__eq__", op_t.clone(), Const, Private);
|
||||||
self.register_impl("__ne__", op_t, Const, Private);
|
self.register_impl("__ne__", op_t, Const, Private);
|
||||||
let o = mono_q("O");
|
let o = mono_q("O");
|
||||||
let op_t = Type::func2(o.clone(), o.clone(), Bool);
|
let op_t = Type::func2(o.clone(), o.clone(), Bool);
|
||||||
let op_t = quant(op_t, set! {subtype(o, mono("Ord"))});
|
let op_t = quant(op_t, set! {subtypeof(o, mono("Ord"))});
|
||||||
self.register_impl("__lt__", op_t.clone(), Const, Private);
|
self.register_impl("__lt__", op_t.clone(), Const, Private);
|
||||||
self.register_impl("__le__", op_t.clone(), Const, Private);
|
self.register_impl("__le__", op_t.clone(), Const, Private);
|
||||||
self.register_impl("__gt__", op_t.clone(), Const, Private);
|
self.register_impl("__gt__", op_t.clone(), Const, Private);
|
||||||
|
@ -734,18 +734,18 @@ impl Context {
|
||||||
// TODO: Boolの+/-は警告を出したい
|
// TODO: Boolの+/-は警告を出したい
|
||||||
let n = mono_q("N");
|
let n = mono_q("N");
|
||||||
let op_t = fn0_met(n.clone(), n.clone());
|
let op_t = fn0_met(n.clone(), n.clone());
|
||||||
let op_t = quant(op_t, set! {subtype(n, mono("Num"))});
|
let op_t = quant(op_t, set! {subtypeof(n, mono("Num"))});
|
||||||
self.register_decl("__pos__", op_t.clone(), Private);
|
self.register_decl("__pos__", op_t.clone(), Private);
|
||||||
self.register_decl("__neg__", op_t, Private);
|
self.register_decl("__neg__", op_t, Private);
|
||||||
let t = mono_q("T");
|
let t = mono_q("T");
|
||||||
let op_t = Type::func2(t.clone(), t.clone(), Type::range(t.clone()));
|
let op_t = Type::func2(t.clone(), t.clone(), Type::range(t.clone()));
|
||||||
let op_t = quant(op_t, set! {subtype(t.clone(), mono("Ord"))});
|
let op_t = quant(op_t, set! {subtypeof(t.clone(), mono("Ord"))});
|
||||||
self.register_decl("__rng__", op_t.clone(), Private);
|
self.register_decl("__rng__", op_t.clone(), Private);
|
||||||
self.register_decl("__lorng__", op_t.clone(), Private);
|
self.register_decl("__lorng__", op_t.clone(), Private);
|
||||||
self.register_decl("__rorng__", op_t.clone(), Private);
|
self.register_decl("__rorng__", op_t.clone(), Private);
|
||||||
self.register_decl("__orng__", op_t, Private);
|
self.register_decl("__orng__", op_t, Private);
|
||||||
let op_t = Type::func1(mono_q("T"), Type::mono_proj(mono_q("T"), "MutType!"));
|
let op_t = Type::func1(mono_q("T"), Type::mono_proj(mono_q("T"), "MutType!"));
|
||||||
let op_t = quant(op_t, set! {subtype(mono_q("T"), mono("Mutate"))});
|
let op_t = quant(op_t, set! {subtypeof(mono_q("T"), mono("Mutate"))});
|
||||||
self.register_impl("__mutate__", op_t, Const, Private);
|
self.register_impl("__mutate__", op_t, Const, Private);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -51,7 +51,14 @@ impl ASTLowerer {
|
||||||
found: &Type,
|
found: &Type,
|
||||||
) -> LowerResult<()> {
|
) -> LowerResult<()> {
|
||||||
self.ctx.unify(expect, found, Some(loc), None).map_err(|_| {
|
self.ctx.unify(expect, found, Some(loc), None).map_err(|_| {
|
||||||
LowerError::type_mismatch_error(loc, self.ctx.caused_by(), name, expect, found)
|
LowerError::type_mismatch_error(
|
||||||
|
line!() as usize,
|
||||||
|
loc,
|
||||||
|
self.ctx.caused_by(),
|
||||||
|
name,
|
||||||
|
expect,
|
||||||
|
found,
|
||||||
|
)
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -109,6 +109,7 @@ impl OwnershipChecker {
|
||||||
{
|
{
|
||||||
let moved_loc = *moved_loc;
|
let moved_loc = *moved_loc;
|
||||||
self.errs.push(OwnershipError::move_error(
|
self.errs.push(OwnershipError::move_error(
|
||||||
|
line!() as usize,
|
||||||
local.inspect(),
|
local.inspect(),
|
||||||
local.loc(),
|
local.loc(),
|
||||||
moved_loc,
|
moved_loc,
|
||||||
|
|
|
@ -1261,9 +1261,8 @@ impl TypeSpec {
|
||||||
|
|
||||||
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
|
||||||
pub enum TypeBoundSpec {
|
pub enum TypeBoundSpec {
|
||||||
Subtype { sub: VarName, sup: TypeSpec }, // e.g. S <: Show
|
Subtype { sub: VarName, sup: TypeSpec }, // e.g. S <: Show
|
||||||
Instance { name: VarName, ty: TypeSpec }, // e.g. N: Nat
|
Instance { name: VarName, ty: TypeSpec }, // e.g. N: Nat
|
||||||
// Predicate, // TODO: e.g. N > 5
|
|
||||||
}
|
}
|
||||||
|
|
||||||
impl NestedDisplay for TypeBoundSpec {
|
impl NestedDisplay for TypeBoundSpec {
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue