Change Eq(R) to Eq

This commit is contained in:
Shunsuke Shibayama 2022-10-25 01:53:52 +09:00
parent 9f85c88e7e
commit d56549f528
15 changed files with 231 additions and 196 deletions

View file

@ -21,7 +21,7 @@ use Type::*;
use crate::context::cache::{SubtypePair, GLOBAL_TYPE_CACHE};
use crate::context::eval::SubstContext;
use crate::context::instantiate::TyVarInstContext;
use crate::context::{Context, TraitInstance, Variance};
use crate::context::{Context, TypeRelationInstance, Variance};
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum Credibility {
@ -258,25 +258,10 @@ impl Context {
self.register_cache(lhs, rhs, judge);
return judge;
}
// FIXME: rec_get_patch
for patch in self.patches.values() {
if let ContextKind::GluePatch(tr_inst) = &patch.kind {
if tr_inst.sub_type.has_qvar() || tr_inst.sup_trait.has_qvar() {
todo!("{tr_inst}");
} else {
// e.g.
// P = Patch X, Impl: Ord
// Rhs <: X => Rhs <: Ord
// Ord <: Lhs => Rhs <: Ord <: Lhs
if self.supertype_of(&tr_inst.sub_type, rhs)
&& self.subtype_of(&tr_inst.sup_trait, lhs)
{
self.register_cache(lhs, rhs, true);
return true;
}
}
}
}
/*if self._find_compatible_patch(lhs, rhs).is_some() {
self.register_cache(lhs, rhs, true);
return true;
}*/
self.register_cache(lhs, rhs, false);
false
}
@ -285,6 +270,41 @@ impl Context {
self.nominal_supertype_of(rhs, lhs)
}
fn _find_compatible_patch(&self, sup: &Type, sub: &Type) -> Option<Str> {
let subst_ctx = SubstContext::try_new(sub, self, Location::Unknown)?;
for patch in self._all_patches().into_iter() {
if let ContextKind::GluePatch(tr_inst) = &patch.kind {
if tr_inst.sub_type.has_qvar() || tr_inst.sup_trait.has_qvar() {
if let (Ok(sub_type), Ok(sup_trait)) = (
subst_ctx.substitute(tr_inst.sub_type.clone()),
subst_ctx.substitute(tr_inst.sup_trait.clone()),
) {
let l1 = self.subtype_of(sub, &sub_type);
let l2 = self.subtype_of(&sup_trait, sup);
if l1 && l2 {
return Some(patch.name.clone());
}
}
} else {
// e.g.
// P = Patch X, Impl: Y
// # => TypeRelationInstance { X <: Y }
// X <: Y => Sub <: Y (if Sub <: X)
// X <: Y => X <: Sup (if Y <: Sup)
// # => OK if Sub <: X and Y <: Sup
// Rhs <: X => Rhs <: Ord
// Ord <: Lhs => Rhs <: Ord <: Lhs
if self.subtype_of(sub, &tr_inst.sub_type)
&& self.subtype_of(&tr_inst.sup_trait, sup)
{
return Some(patch.name.clone());
}
}
}
}
None
}
fn classes_supertype_of(&self, lhs: &Type, rhs: &Type) -> (Credibility, bool) {
if !self.is_class(lhs) || !self.is_class(rhs) {
return (Maybe, false);
@ -321,6 +341,7 @@ impl Context {
// e.g. Eq(Nat) :> Nat
// Nat.super_traits = [Add(Nat), Eq(Nat), Sub(Float), ...]
// e.g. Eq :> ?L or ?R (if ?L <: Eq and ?R <: Eq)
fn traits_supertype_of(&self, lhs: &Type, rhs: &Type) -> (Credibility, bool) {
if !self.is_trait(lhs) {
return (Maybe, false);
@ -369,7 +390,7 @@ impl Context {
/// assert!(sup_conforms(?E(<: Eq(?E)), {Nat, Eq(Nat)}))
/// 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: &TypeRelationInstance) -> bool {
let (_sub, sup) = free.get_bound_types().unwrap();
log!(info "{free}");
free.forced_undoable_link(&inst_pair.sub_type);
@ -648,11 +669,20 @@ impl Context {
.unwrap();
self.structural_supertype_of(l, &q_callable)
}
// Int or Str :> Str or Int == (Int :> Str && Str :> Int) || (Int :> Int && Str :> Str) == true
(Or(l_1, l_2), Or(r_1, r_2)) => {
(self.supertype_of(l_1, r_1) && self.supertype_of(l_2, r_2))
|| (self.supertype_of(l_1, r_2) && self.supertype_of(l_2, r_1))
}
// (Int or Str) :> Nat == Int :> Nat || Str :> Nat == true
// (Num or Show) :> Show == Num :> Show || Show :> Num == true
(Or(l_or, r_or), rhs) => self.supertype_of(l_or, rhs) || self.supertype_of(r_or, rhs),
// Int :> (Nat or Str) == Int :> Nat && Int :> Str == false
(lhs, Or(l_or, r_or)) => self.supertype_of(lhs, l_or) && self.supertype_of(lhs, r_or),
(And(l_1, l_2), And(r_1, r_2)) => {
(self.supertype_of(l_1, r_1) && self.supertype_of(l_2, r_2))
|| (self.supertype_of(l_1, r_2) && self.supertype_of(l_2, r_1))
}
// (Num and Show) :> Show == false
(And(l_and, r_and), rhs) => {
self.supertype_of(l_and, rhs) && self.supertype_of(r_and, rhs)

View file

@ -136,9 +136,11 @@ impl<'c> SubstContext<'c> {
///
/// `ctx` is used to obtain information on the names and variance of the parameters.
pub fn new(substituted: &Type, ctx: &'c Context, loc: Location) -> Self {
let ty_ctx = ctx
.get_nominal_type_ctx(substituted)
.unwrap_or_else(|| todo!("{substituted} not found"));
Self::try_new(substituted, ctx, loc).unwrap()
}
pub fn try_new(substituted: &Type, ctx: &'c Context, loc: Location) -> Option<Self> {
let ty_ctx = ctx.get_nominal_type_ctx(substituted)?;
let bounds = ty_ctx.type_params_bounds();
let param_names = ty_ctx.params.iter().map(|(opt_name, _)| {
opt_name
@ -146,13 +148,14 @@ impl<'c> SubstContext<'c> {
.map_or_else(|| Str::ever("_"), |n| n.inspect().clone())
});
if param_names.len() != substituted.typarams().len() {
let param_names = param_names.collect::<Vec<_>>();
/*let param_names = param_names.collect::<Vec<_>>();
panic!(
"{} param_names: {param_names:?} != {} substituted_params: [{}]",
ty_ctx.name,
substituted.qual_name(),
erg_common::fmt_vec(&substituted.typarams())
);
);*/
return None;
}
let params = param_names
.zip(substituted.typarams().into_iter())
@ -165,12 +168,12 @@ impl<'c> SubstContext<'c> {
}
}
// REVIEW: 順番は保証されるか? 引数がunnamed_paramsに入る可能性は?
SubstContext {
Some(SubstContext {
ctx,
bounds,
params,
loc,
}
})
}
pub fn substitute(&self, quant_t: Type) -> TyCheckResult<Type> {
@ -229,7 +232,7 @@ impl<'c> SubstContext<'c> {
self.ctx.sub_unify(param_t, &t, Location::Unknown, None)?;
}
Err(_) => {
todo!("")
todo!("{tp}")
}
}
}
@ -276,7 +279,7 @@ impl<'c> SubstContext<'c> {
self.substitute_tp(param)?;
}
}
t => todo!("{t:?}"),
_t => {}
}
Ok(())
}

View file

@ -8,6 +8,8 @@ use std::path::PathBuf;
use erg_common::config::ErgConfig;
use erg_common::dict;
// use erg_common::error::Location;
#[allow(unused_imports)]
use erg_common::log;
use erg_common::vis::Visibility;
use erg_common::Str;
use erg_common::{set, unique_in_place};
@ -25,7 +27,7 @@ use erg_parser::ast::VarName;
use crate::context::initialize::const_func::*;
use crate::context::instantiate::ConstTemplate;
use crate::context::{
ClassDefType, Context, ContextKind, DefaultInfo, MethodInfo, ParamSpec, TraitInstance,
ClassDefType, Context, ContextKind, DefaultInfo, MethodInfo, ParamSpec, TypeRelationInstance,
};
use crate::mod_cache::SharedModuleCache;
use crate::varinfo::{Mutability, VarInfo, VarKind};
@ -236,11 +238,11 @@ impl Context {
.insert(name.clone(), ValueObj::builtin_t(t.clone()));
for impl_trait in ctx.super_traits.iter() {
if let Some(impls) = self.trait_impls.get_mut(&impl_trait.qual_name()) {
impls.insert(TraitInstance::new(t.clone(), impl_trait.clone()));
impls.insert(TypeRelationInstance::new(t.clone(), impl_trait.clone()));
} else {
self.trait_impls.insert(
impl_trait.qual_name(),
set![TraitInstance::new(t.clone(), impl_trait.clone())],
set![TypeRelationInstance::new(t.clone(), impl_trait.clone())],
);
}
}
@ -303,11 +305,11 @@ impl Context {
.insert(name.clone(), ValueObj::builtin_t(t.clone()));
for impl_trait in ctx.super_traits.iter() {
if let Some(impls) = self.trait_impls.get_mut(&impl_trait.qual_name()) {
impls.insert(TraitInstance::new(t.clone(), impl_trait.clone()));
impls.insert(TypeRelationInstance::new(t.clone(), impl_trait.clone()));
} else {
self.trait_impls.insert(
impl_trait.qual_name(),
set![TraitInstance::new(t.clone(), impl_trait.clone())],
set![TypeRelationInstance::new(t.clone(), impl_trait.clone())],
);
}
}
@ -358,6 +360,14 @@ impl Context {
.insert(method_name.clone(), vec![name.clone()]);
}
}
if let ContextKind::GluePatch(tr_inst) = &ctx.kind {
if let Some(impls) = self.trait_impls.get_mut(&tr_inst.sup_trait.qual_name()) {
impls.insert(tr_inst.clone());
} else {
self.trait_impls
.insert(tr_inst.sup_trait.qual_name(), set![tr_inst.clone()]);
}
}
self.patches.insert(name, ctx);
}
}
@ -459,35 +469,21 @@ impl Context {
// Erg does not have a trait equivalent to `PartialEq` in Rust
// This means, Erg's `Float` cannot be compared with other `Float`
// use `l - r < EPSILON` to check if two floats are almost equal
let mut eq = Self::builtin_poly_trait("Eq", vec![PS::t("R", WithDefault)], 2);
eq.register_superclass(poly("Output", vec![ty_tp(mono_q("R"))]), &output);
// __eq__: |Self <: Eq()| Self.(Self) -> Bool
let op_t = fn1_met(mono_q("Self"), mono_q("R"), Bool);
let op_t = quant(
op_t,
set! {
subtypeof(mono_q("Self"), poly("Eq", vec![ty_tp(mono_q("R"))])),
static_instance("R", Type)
},
);
let mut eq = Self::builtin_mono_trait("Eq", 2);
// __eq__: |Self <: Eq| Self.(Self) -> Bool
let op_t = fn1_met(mono_q("Self"), mono_q("Self"), Bool);
let op_t = quant(op_t, set! { subtypeof(mono_q("Self"), mono("Eq")) });
eq.register_builtin_decl("__eq__", op_t, Public);
/* Partial_ord */
let mut partial_ord =
Self::builtin_poly_trait("PartialOrd", vec![PS::t("R", WithDefault)], 2);
partial_ord.register_superclass(poly("Eq", vec![ty_tp(mono_q("R"))]), &eq);
let op_t = fn1_met(mono_q("Self"), mono_q("R"), or(mono("Ordering"), NoneType));
let op_t = quant(
op_t,
set! {
subtypeof(mono_q("Self"), poly("PartialOrd", vec![ty_tp(mono_q("R"))])),
static_instance("R", Type)
},
);
partial_ord.register_builtin_decl("__partial_cmp__", op_t, Public);
/* Ord */
let mut ord = Self::builtin_mono_trait("Ord", 2);
ord.register_superclass(poly("Eq", vec![ty_tp(mono("Self"))]), &eq);
ord.register_superclass(poly("PartialOrd", vec![ty_tp(mono("Self"))]), &partial_ord);
ord.register_superclass(mono("Eq"), &eq);
let op_t = fn1_met(
mono_q("Self"),
mono_q("Self"),
or(mono("Ordering"), NoneType),
);
let op_t = quant(op_t, set! { subtypeof(mono_q("Self"), mono("Ord")) });
ord.register_builtin_decl("__cmp__", op_t, Public);
// FIXME: poly trait
/* Num */
let num = Self::builtin_mono_trait("Num", 2);
@ -620,20 +616,7 @@ impl Context {
Const,
None,
);
self.register_builtin_type(
poly("Eq", vec![ty_tp(mono_q("R"))]),
eq,
Private,
Const,
None,
);
self.register_builtin_type(
poly("PartialOrd", vec![ty_tp(mono_q("R"))]),
partial_ord,
Private,
Const,
None,
);
self.register_builtin_type(mono("Eq"), eq, Private, Const, None);
self.register_builtin_type(mono("Ord"), ord, Private, Const, None);
self.register_builtin_type(mono("Num"), num, Private, Const, None);
self.register_builtin_type(
@ -655,14 +638,6 @@ impl Context {
self.register_builtin_type(poly("Mul", ty_params.clone()), mul, Private, Const, None);
self.register_builtin_type(poly("Div", ty_params.clone()), div, Private, Const, None);
self.register_builtin_type(poly("FloorDiv", ty_params), floor_div, Private, Const, None);
self.register_const_param_defaults(
"Eq",
vec![ConstTemplate::Obj(ValueObj::builtin_t(mono_q("Self")))],
);
self.register_const_param_defaults(
"PartialOrd",
vec![ConstTemplate::app("Self", vec![], vec![])],
);
self.register_const_param_defaults(
"Add",
vec![ConstTemplate::Obj(ValueObj::builtin_t(mono_q("Self")))],
@ -719,15 +694,14 @@ impl Context {
float.register_builtin_py_impl("Imag", Float, Const, Public, Some("imag"));
float.register_marker_trait(mono("Num"));
float.register_marker_trait(mono("Ord"));
let mut float_partial_ord =
Self::builtin_methods(Some(poly("PartialOrd", vec![ty_tp(Float)])), 2);
float_partial_ord.register_builtin_impl(
let mut float_ord = Self::builtin_methods(Some(mono("Ord")), 2);
float_ord.register_builtin_impl(
"__cmp__",
fn1_met(Float, Float, mono("Ordering")),
Const,
Public,
);
float.register_trait(Float, float_partial_ord);
float.register_trait(Float, float_ord);
// Float doesn't have an `Eq` implementation
let op_t = fn1_met(Float, Float, Float);
let mut float_add = Self::builtin_methods(Some(poly("Add", vec![ty_tp(Float)])), 2);
@ -773,16 +747,15 @@ impl Context {
ratio.register_builtin_py_impl("Imag", Ratio, Const, Public, Some("imag"));
ratio.register_marker_trait(mono("Num"));
ratio.register_marker_trait(mono("Ord"));
let mut ratio_partial_ord =
Self::builtin_methods(Some(poly("PartialOrd", vec![ty_tp(Ratio)])), 2);
ratio_partial_ord.register_builtin_impl(
let mut ratio_ord = Self::builtin_methods(Some(mono("Ord")), 2);
ratio_ord.register_builtin_impl(
"__cmp__",
fn1_met(Ratio, Ratio, mono("Ordering")),
Const,
Public,
);
ratio.register_trait(Ratio, ratio_partial_ord);
let mut ratio_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(Ratio)])), 2);
ratio.register_trait(Ratio, ratio_ord);
let mut ratio_eq = Self::builtin_methods(Some(mono("Eq")), 2);
ratio_eq.register_builtin_impl("__eq__", fn1_met(Ratio, Ratio, Bool), Const, Public);
ratio.register_trait(Ratio, ratio_eq);
let op_t = fn1_met(Ratio, Ratio, Ratio);
@ -825,21 +798,18 @@ impl Context {
let mut int = Self::builtin_mono_class("Int", 2);
int.register_superclass(Float, &float); // TODO: Float -> Ratio
int.register_marker_trait(mono("Num"));
int.register_marker_trait(mono("Ord"));
int.register_marker_trait(poly("Eq", vec![ty_tp(Int)]));
// class("Rational"),
// class("Integral"),
int.register_builtin_impl("abs", fn0_met(Int, Nat), Immutable, Public);
let mut int_partial_ord =
Self::builtin_methods(Some(poly("PartialOrd", vec![ty_tp(Int)])), 2);
int_partial_ord.register_builtin_impl(
let mut int_ord = Self::builtin_methods(Some(mono("Ord")), 2);
int_ord.register_builtin_impl(
"__partial_cmp__",
fn1_met(Int, Int, or(mono("Ordering"), NoneType)),
Const,
Public,
);
int.register_trait(Int, int_partial_ord);
let mut int_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(Int)])), 2);
int.register_trait(Int, int_ord);
let mut int_eq = Self::builtin_methods(Some(mono("Eq")), 2);
int_eq.register_builtin_impl("__eq__", fn1_met(Int, Int, Bool), Const, Public);
int.register_trait(Int, int_eq);
// __div__ is not included in Int (cast to Ratio)
@ -890,19 +860,17 @@ impl Context {
Some("times"),
);
nat.register_marker_trait(mono("Num"));
nat.register_marker_trait(mono("Ord"));
let mut nat_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(Nat)])), 2);
let mut nat_eq = Self::builtin_methods(Some(mono("Eq")), 2);
nat_eq.register_builtin_impl("__eq__", fn1_met(Nat, Nat, Bool), Const, Public);
nat.register_trait(Nat, nat_eq);
let mut nat_partial_ord =
Self::builtin_methods(Some(poly("PartialOrd", vec![ty_tp(Nat)])), 2);
nat_partial_ord.register_builtin_impl(
let mut nat_ord = Self::builtin_methods(Some(mono("Ord")), 2);
nat_ord.register_builtin_impl(
"__cmp__",
fn1_met(Nat, Nat, mono("Ordering")),
Const,
Public,
);
nat.register_trait(Nat, nat_partial_ord);
nat.register_trait(Nat, nat_ord);
// __sub__, __div__ is not included in Nat (cast to Int/ Ratio)
let op_t = fn1_met(Nat, Nat, Nat);
let mut nat_add = Self::builtin_methods(Some(poly("Add", vec![ty_tp(Nat)])), 2);
@ -931,17 +899,15 @@ impl Context {
bool_.register_builtin_impl("__and__", fn1_met(Bool, Bool, Bool), Const, Public);
bool_.register_builtin_impl("__or__", fn1_met(Bool, Bool, Bool), Const, Public);
bool_.register_marker_trait(mono("Num"));
bool_.register_marker_trait(mono("Ord"));
let mut bool_partial_ord =
Self::builtin_methods(Some(poly("PartialOrd", vec![ty_tp(Bool)])), 2);
bool_partial_ord.register_builtin_impl(
let mut bool_ord = Self::builtin_methods(Some(mono("Ord")), 2);
bool_ord.register_builtin_impl(
"__cmp__",
fn1_met(Bool, Bool, mono("Ordering")),
Const,
Public,
);
bool_.register_trait(Bool, bool_partial_ord);
let mut bool_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(Bool)])), 2);
bool_.register_trait(Bool, bool_ord);
let mut bool_eq = Self::builtin_methods(Some(mono("Eq")), 2);
bool_eq.register_builtin_impl("__eq__", fn1_met(Bool, Bool, Bool), Const, Public);
bool_.register_trait(Bool, bool_eq);
let mut bool_mutizable = Self::builtin_methods(Some(mono("Mutizable")), 2);
@ -983,7 +949,7 @@ impl Context {
Immutable,
Public,
);
let mut str_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(Str)])), 2);
let mut str_eq = Self::builtin_methods(Some(mono("Eq")), 2);
str_eq.register_builtin_impl("__eq__", fn1_met(Str, Str, Bool), Const, Public);
str_.register_trait(Str, str_eq);
let mut str_seq = Self::builtin_methods(Some(poly("Seq", vec![ty_tp(Str)])), 2);
@ -1015,7 +981,7 @@ impl Context {
/* NoneType */
let mut nonetype = Self::builtin_mono_class("NoneType", 10);
nonetype.register_superclass(Obj, &obj);
let mut nonetype_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(NoneType)])), 2);
let mut nonetype_eq = Self::builtin_methods(Some(mono("Eq")), 2);
nonetype_eq.register_builtin_impl(
"__eq__",
fn1_met(NoneType, NoneType, Bool),
@ -1036,13 +1002,13 @@ impl Context {
Public,
);
type_.register_marker_trait(mono("Named"));
let mut type_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(Type)])), 2);
let mut type_eq = Self::builtin_methods(Some(mono("Eq")), 2);
type_eq.register_builtin_impl("__eq__", fn1_met(Type, Type, Bool), Const, Public);
type_.register_trait(Type, type_eq);
let mut class_type = Self::builtin_mono_class("ClassType", 2);
class_type.register_superclass(Type, &type_);
class_type.register_marker_trait(mono("Named"));
let mut class_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(ClassType)])), 2);
let mut class_eq = Self::builtin_methods(Some(mono("Eq")), 2);
class_eq.register_builtin_impl(
"__eq__",
fn1_met(ClassType, ClassType, Bool),
@ -1053,7 +1019,7 @@ impl Context {
let mut trait_type = Self::builtin_mono_class("TraitType", 2);
trait_type.register_superclass(Type, &type_);
trait_type.register_marker_trait(mono("Named"));
let mut trait_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(TraitType)])), 2);
let mut trait_eq = Self::builtin_methods(Some(mono("Eq")), 2);
trait_eq.register_builtin_impl(
"__eq__",
fn1_met(TraitType, TraitType, Bool),
@ -1065,8 +1031,7 @@ impl Context {
let mut generic_module = Self::builtin_mono_class("GenericModule", 2);
generic_module.register_superclass(Obj, &obj);
generic_module.register_marker_trait(mono("Named"));
let mut generic_module_eq =
Self::builtin_methods(Some(poly("Eq", vec![ty_tp(g_module_t.clone())])), 2);
let mut generic_module_eq = Self::builtin_methods(Some(mono("Eq")), 2);
generic_module_eq.register_builtin_impl(
"__eq__",
fn1_met(g_module_t.clone(), g_module_t.clone(), Bool),
@ -1152,7 +1117,7 @@ impl Context {
None,
)));
array_.register_builtin_const("__getitem__", Public, get_item);
let mut array_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(arr_t.clone())])), 2);
let mut array_eq = Self::builtin_methods(Some(mono("Eq")), 2);
array_eq.register_builtin_impl(
"__eq__",
fn1_met(arr_t.clone(), arr_t.clone(), Bool),
@ -1205,7 +1170,7 @@ impl Context {
vec![TyParam::t(mono_q("T")), TyParam::mono_q("N").mutate()],
));
set_.register_builtin_const("MutType!", Public, mut_type);
let mut set_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(set_t.clone())])), 2);
let mut set_eq = Self::builtin_methods(Some(mono("Eq")), 2);
set_eq.register_builtin_impl(
"__eq__",
fn1_met(set_t.clone(), set_t.clone(), Bool),
@ -1221,8 +1186,7 @@ impl Context {
let g_dict_t = mono("GenericDict");
let mut generic_dict = Self::builtin_mono_class("GenericDict", 2);
generic_dict.register_superclass(Obj, &obj);
let mut generic_dict_eq =
Self::builtin_methods(Some(poly("Eq", vec![ty_tp(g_dict_t.clone())])), 2);
let mut generic_dict_eq = Self::builtin_methods(Some(mono("Eq")), 2);
generic_dict_eq.register_builtin_impl(
"__eq__",
fn1_met(g_dict_t.clone(), g_dict_t.clone(), Bool),
@ -1271,8 +1235,7 @@ impl Context {
/* GenericTuple */
let mut generic_tuple = Self::builtin_mono_class("GenericTuple", 1);
generic_tuple.register_superclass(Obj, &obj);
let mut tuple_eq =
Self::builtin_methods(Some(poly("Eq", vec![ty_tp(mono("GenericTuple"))])), 2);
let mut tuple_eq = Self::builtin_methods(Some(mono("Eq")), 2);
tuple_eq.register_builtin_impl(
"__eq__",
fn1_met(mono("GenericTuple"), mono("GenericTuple"), Bool),
@ -1551,7 +1514,7 @@ impl Context {
range.register_superclass(Type, &type_);
range.register_marker_trait(poly("Output", vec![ty_tp(mono_q("T"))]));
range.register_marker_trait(poly("Seq", vec![ty_tp(mono_q("T"))]));
let mut range_eq = Self::builtin_methods(Some(poly("Eq", vec![ty_tp(range_t.clone())])), 2);
let mut range_eq = Self::builtin_methods(Some(mono("Eq")), 2);
range_eq.register_builtin_impl(
"__eq__",
fn1_met(range_t.clone(), range_t.clone(), Bool),
@ -2059,12 +2022,12 @@ impl Context {
},
);
self.register_builtin_impl("__div__", op_t, Const, Private);
let op_t = bin_op(l.clone(), r.clone(), proj(mono_q("L"), "Output"));
let op_t = bin_op(l.clone(), r, proj(mono_q("L"), "Output"));
let op_t = quant(
op_t,
set! {
static_instance("R", Type),
subtypeof(l.clone(), poly("FloorDiv", params.clone()))
subtypeof(l.clone(), poly("FloorDiv", params))
},
);
self.register_builtin_impl("__floordiv__", op_t, Const, Private);
@ -2079,17 +2042,11 @@ impl Context {
self.register_builtin_impl("__mod__", op_t, Const, Private);
let e = mono_q("E");
let op_t = bin_op(e.clone(), e.clone(), Bool);
let op_t = quant(op_t, set! {subtypeof(e, poly("Eq", vec![]))});
let op_t = quant(op_t, set! {subtypeof(e, mono("Eq"))});
self.register_builtin_impl("__eq__", op_t.clone(), Const, Private);
self.register_builtin_impl("__ne__", op_t, Const, Private);
let op_t = bin_op(l.clone(), r, Bool);
let op_t = quant(
op_t,
set! {
static_instance("R", Type),
subtypeof(l, poly("PartialOrd", params))
},
);
let op_t = bin_op(l.clone(), l.clone(), Bool);
let op_t = quant(op_t, set! { subtypeof(l, mono("Ord")) });
self.register_builtin_impl("__lt__", op_t.clone(), Const, Private);
self.register_builtin_impl("__le__", op_t.clone(), Const, Private);
self.register_builtin_impl("__gt__", op_t.clone(), Const, Private);
@ -2172,22 +2129,18 @@ impl Context {
// ord.register_impl("__le__", op_t.clone(), Const, Public);
// ord.register_impl("__gt__", op_t.clone(), Const, Public);
// ord.register_impl("__ge__", op_t, Const, Public);
let t = mono_q("T");
let u = mono_q("U");
let base = or(t.clone(), u.clone());
let impls = poly("Eq", vec![ty_tp(base.clone())]);
let params = vec![PS::named_nd("T", Type), PS::named_nd("U", Type)];
let mut union_eq =
Self::builtin_poly_glue_patch("UnionEq", base.clone(), impls.clone(), params, 1);
let mut union_eq_impl = Self::builtin_methods(Some(impls), 1);
let t = mono_q("L");
let base = or(t.clone(), NoneType);
let impls = mono("Eq");
let params = vec![PS::named_nd("L", Type)];
let mut option_eq =
Self::builtin_poly_glue_patch("OptionEq", base.clone(), impls.clone(), params, 1);
let mut option_eq_impl = Self::builtin_methods(Some(impls), 1);
let op_t = fn1_met(base.clone(), base.clone(), Bool);
let op_t = quant(
op_t,
set! {subtypeof(t.clone(), poly("Eq", vec![ty_tp(t)])), subtypeof(u.clone(), poly("Eq", vec![ty_tp(u)]))},
);
union_eq_impl.register_builtin_impl("__eq__", op_t, Const, Public);
union_eq.register_trait(base, union_eq_impl);
self.register_builtin_patch("UnionEq", union_eq, Private, Const);
let op_t = quant(op_t, set! {subtypeof(t, mono("Eq"))});
option_eq_impl.register_builtin_impl("__eq__", op_t, Const, Public);
option_eq.register_trait(base, option_eq_impl);
self.register_builtin_patch("OptionEq", option_eq, Private, Const);
}
pub(crate) fn init_builtins(mod_cache: &SharedModuleCache) {

View file

@ -24,7 +24,7 @@ use crate::ty::value::{GenTypeObj, TypeObj, ValueObj};
use crate::ty::{HasType, ParamTy, SubrKind, SubrType, TyBound, Type};
use crate::context::instantiate::ConstTemplate;
use crate::context::{Context, RegistrationMode, TraitInstance, Variance};
use crate::context::{Context, RegistrationMode, TypeRelationInstance, Variance};
use crate::error::{
binop_to_dname, readable_name, unaryop_to_dname, SingleTyCheckResult, TyCheckError,
TyCheckErrors, TyCheckResult,
@ -1695,7 +1695,7 @@ impl Context {
None
}
pub(crate) fn get_trait_impls(&self, t: &Type) -> Set<TraitInstance> {
pub(crate) fn get_trait_impls(&self, t: &Type) -> Set<TypeRelationInstance> {
match t {
// And(Add, Sub) == intersection({Int <: Add(Int), Bool <: Add(Bool) ...}, {Int <: Sub(Int), ...})
// == {Int <: Add(Int) and Sub(Int), ...}
@ -1710,7 +1710,7 @@ impl Context {
let lti = l_impls.iter().find(|ti| &ti.sub_type == base).unwrap();
let rti = r_impls.iter().find(|ti| &ti.sub_type == base).unwrap();
let sup_trait = self.intersection(&lti.sup_trait, &rti.sup_trait);
isec.insert(TraitInstance::new(lti.sub_type.clone(), sup_trait));
isec.insert(TypeRelationInstance::new(lti.sub_type.clone(), sup_trait));
}
isec
}
@ -1724,7 +1724,7 @@ impl Context {
}
}
pub(crate) fn get_simple_trait_impls(&self, t: &Type) -> Set<TraitInstance> {
pub(crate) fn get_simple_trait_impls(&self, t: &Type) -> Set<TypeRelationInstance> {
let current = if let Some(impls) = self.trait_impls.get(&t.qual_name()) {
impls.clone()
} else {
@ -1747,6 +1747,14 @@ impl Context {
}
}
pub(crate) fn _all_patches(&self) -> Vec<&Context> {
if let Some(outer) = self.get_outer().or_else(|| self.get_builtins()) {
[outer._all_patches(), self.patches.values().collect()].concat()
} else {
self.patches.values().collect()
}
}
// TODO: erg std
pub(crate) fn resolve_path(&self, path: &Path) -> PathBuf {
if let Ok(path) = self.cfg.input.local_resolve(path) {

View file

@ -48,24 +48,24 @@ use Visibility::*;
const BUILTINS: &Str = &Str::ever("<builtins>");
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct TraitInstance {
pub struct TypeRelationInstance {
pub sub_type: Type,
pub sup_trait: Type,
}
impl std::fmt::Display for TraitInstance {
impl std::fmt::Display for TypeRelationInstance {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
write!(
f,
"TraitInstancePair{{{} <: {}}}",
"TypeRelationInstance{{{} <: {}}}",
self.sub_type, self.sup_trait
)
}
}
impl TraitInstance {
impl TypeRelationInstance {
pub const fn new(sub_type: Type, sup_trait: Type) -> Self {
TraitInstance {
Self {
sub_type,
sup_trait,
}
@ -231,7 +231,7 @@ pub enum ContextKind {
StructuralTrait,
Patch(Type),
StructuralPatch(Type),
GluePatch(TraitInstance),
GluePatch(TypeRelationInstance), // TODO: deprecate (integrate into Patch)
Module,
Instant,
Dummy,
@ -338,7 +338,7 @@ pub struct Context {
/// K: name of a trait, V: (type, monomorphised trait that the type implements)
/// K: トレイトの名前, V: (型, その型が実装する単相化トレイト)
/// e.g. { "Named": [(Type, Named), (Func, Named), ...], "Add": [(Nat, Add(Nat)), (Int, Add(Int)), ...], ... }
pub(crate) trait_impls: Dict<Str, Set<TraitInstance>>,
pub(crate) trait_impls: Dict<Str, Set<TypeRelationInstance>>,
/// stores declared names (not initialized)
pub(crate) decls: Dict<VarName, VarInfo>,
// stores defined names
@ -714,7 +714,7 @@ impl Context {
Self::poly(
name.into(),
cfg,
ContextKind::GluePatch(TraitInstance::new(base, impls)),
ContextKind::GluePatch(TypeRelationInstance::new(base, impls)),
params,
None,
mod_cache,

View file

@ -21,7 +21,8 @@ use crate::ty::{HasType, ParamTy, SubrType, Type};
use crate::build_hir::HIRBuilder;
use crate::context::{
ClassDefType, Context, ContextKind, DefaultInfo, MethodInfo, RegistrationMode, TraitInstance,
ClassDefType, Context, ContextKind, DefaultInfo, MethodInfo, RegistrationMode,
TypeRelationInstance,
};
use crate::error::readable_name;
use crate::error::{
@ -988,11 +989,11 @@ impl Context {
.insert(name.clone(), ValueObj::Type(TypeObj::Generated(gen)));
for impl_trait in ctx.super_traits.iter() {
if let Some(impls) = self.trait_impls.get_mut(&impl_trait.qual_name()) {
impls.insert(TraitInstance::new(t.clone(), impl_trait.clone()));
impls.insert(TypeRelationInstance::new(t.clone(), impl_trait.clone()));
} else {
self.trait_impls.insert(
impl_trait.qual_name(),
set![TraitInstance::new(t.clone(), impl_trait.clone())],
set![TypeRelationInstance::new(t.clone(), impl_trait.clone())],
);
}
}

View file

@ -4,7 +4,7 @@ use erg_common::Str;
// use erg_common::error::Location;
use erg_common::{enum_unwrap, set};
use crate::ty::constructors::{func1, mono_q, poly, quant, refinement};
use crate::ty::constructors::{func1, mono, mono_q, poly, quant, refinement};
use crate::ty::typaram::TyParam;
use crate::ty::{Predicate, TyBound, Type};
use Type::*;
@ -48,7 +48,7 @@ impl Context {
pub fn test_instantiation_and_generalization(&self) -> Result<(), ()> {
let t = mono_q("T");
let eq = poly("Eq", vec![TyParam::t(t.clone())]);
let eq = mono("Eq");
let bound = TyBound::subtype_of(t.clone(), eq);
let bounds = set! {bound};
let unbound_t = func1(t.clone(), t);

View file

@ -637,8 +637,13 @@ impl Context {
let sub_type = if inst.sub_type.has_qvar() {
let sub_ctx = self.get_nominal_type_ctx(&inst.sub_type).unwrap();
let tv_ctx = TyVarInstContext::new(self.level, sub_ctx.bounds(), self);
self.instantiate_t_inner(inst.sub_type, &tv_ctx, Location::Unknown)
.unwrap()
if let Ok(t) =
self.instantiate_t_inner(inst.sub_type.clone(), &tv_ctx, Location::Unknown)
{
t
} else {
continue;
}
} else {
inst.sub_type
};
@ -1414,10 +1419,6 @@ impl Context {
)));
}
match (maybe_sub, maybe_sup) {
(Type::FreeVar(lfv), _) if lfv.is_linked() =>
self.sub_unify(&lfv.crack(), maybe_sup, loc, param_name),
(_, Type::FreeVar(rfv)) if rfv.is_linked() =>
self.sub_unify(maybe_sub, &rfv.crack(), loc, param_name),
// lfv's sup can be shrunk (take min), rfv's sub can be expanded (take union)
// lfvのsupは縮小可能(minを取る)、rfvのsubは拡大可能(unionを取る)
// sub_unify(?T[0](:> Never, <: Int), ?U[1](:> Never, <: Nat)): (/* ?U[1] --> ?T[0](:> Never, <: Nat))
@ -1455,6 +1456,10 @@ impl Context {
}
Ok(())
}
(Type::FreeVar(lfv), _) if lfv.is_linked() =>
self.sub_unify(&lfv.crack(), maybe_sup, loc, param_name),
(_, Type::FreeVar(rfv)) if rfv.is_linked() =>
self.sub_unify(maybe_sub, &rfv.crack(), loc, param_name),
(_, Type::FreeVar(rfv)) if rfv.is_unbound() => {
// NOTE: cannot `borrow_mut` because of cycle reference
let rfv_ref = unsafe { rfv.as_ptr().as_mut().unwrap() };
@ -1473,13 +1478,18 @@ impl Context {
// 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))
// * sub_unify(Bool, ?T(<: Bool or Y)): (?T == Bool)
Constraint::Sandwiched { sub, sup, cyclicity } => {
/*if let Some(new_sub) = self.max(maybe_sub, sub) {
*constraint =
Constraint::new_sandwiched(new_sub.clone(), mem::take(sup), *cyclicity);
} else {*/
let new_sub = self.union(maybe_sub, sub);
*constraint = Constraint::new_sandwiched(new_sub, mem::take(sup), *cyclicity);
if sup.contains_union(&new_sub) {
rfv.link(&new_sub); // Bool <: ?T <: Bool or Y ==> ?T == Bool
} else {
*constraint = Constraint::new_sandwiched(new_sub, mem::take(sup), *cyclicity);
}
// }
}
// sub_unify(Nat, ?T(: Type)): (/* ?T(:> Nat) */)

View file

@ -1,6 +1,6 @@
# e.g. `nightly.0`
.Identifier = Class { .name = Str; .num = Nat }
.Identifier|.Identifier <: Eq(.Identifier)|.
.Identifier|.Identifier <: Eq|.
__eq__ self, other: .Identifier =
self.name == other.name and self.num == other.num
@ -16,9 +16,9 @@
[_, True, _, True, True] -> True
_ -> False
]#
.Version|.Version <: Eq(.Version)|.
.Version|.Version <: Eq|.
__eq__ self, other: .Version =
self.major == other.major and self.minor == other.minor and self.patch == other.patch # and self.pre == other.pre
self.major == other.major and self.minor == other.minor and self.patch == other.patch and self.pre == "" # other.pre
if! __name__ == "__main__", do!:
v = .Version.new(0, 0, 1)

View file

@ -27,7 +27,7 @@ use crate::ty::value::{GenTypeObj, TypeObj, ValueObj};
use crate::ty::{HasType, ParamTy, Type};
use crate::context::instantiate::TyVarInstContext;
use crate::context::{ClassDefType, Context, ContextKind, RegistrationMode, TraitInstance};
use crate::context::{ClassDefType, Context, ContextKind, RegistrationMode, TypeRelationInstance};
use crate::error::{
CompileError, CompileErrors, LowerError, LowerErrors, LowerResult, LowerWarnings,
SingleLowerResult,
@ -411,9 +411,8 @@ impl ASTLowerer {
Ok(normal_set)
*/
let elems = hir::Args::from(new_set);
let sup = poly("Eq", vec![TyParam::t(elem_t.clone())]);
// check if elem_t is Eq
if let Err(errs) = self.ctx.sub_unify(&elem_t, &sup, elems.loc(), None) {
if let Err(errs) = self.ctx.sub_unify(&elem_t, &mono("Eq"), elems.loc(), None) {
self.errs.extend(errs.into_iter());
}
Ok(hir::NormalSet::new(set.l_brace, set.r_brace, elem_t, elems))
@ -514,10 +513,9 @@ impl ASTLowerer {
new_kvs.push(hir::KeyValue::new(key, value));
}
for key_t in union.keys() {
let sup = poly("Eq", vec![TyParam::t(key_t.clone())]);
let loc = Location::concat(&dict.l_brace, &dict.r_brace);
// check if key_t is Eq
if let Err(errs) = self.ctx.sub_unify(key_t, &sup, loc, None) {
if let Err(errs) = self.ctx.sub_unify(key_t, &mono("Eq"), loc, None) {
self.errs.extend(errs.into_iter());
}
}
@ -1239,8 +1237,23 @@ impl ASTLowerer {
) -> SingleLowerResult<()> {
if let Some((impl_trait, loc)) = impl_trait {
// assume the class has implemented the trait, regardless of whether the implementation is correct
let trait_ctx = self.ctx.get_nominal_type_ctx(&impl_trait).unwrap().clone();
let (_, class_ctx) = self.ctx.get_mut_nominal_type_ctx(class).unwrap();
let trait_ctx = if let Some(trait_ctx) = self.ctx.get_nominal_type_ctx(&impl_trait) {
trait_ctx.clone()
} else {
// TODO: maybe parameters are wrong
return Err(LowerError::no_var_error(
self.cfg.input.clone(),
line!() as usize,
loc,
self.ctx.caused_by(),
&impl_trait.local_name(),
None,
));
};
let (_, class_ctx) = self
.ctx
.get_mut_nominal_type_ctx(class)
.unwrap_or_else(|| todo!("{class} not found"));
class_ctx.register_supertrait(impl_trait.clone(), &trait_ctx);
let mut unverified_names = self.ctx.locals.keys().collect::<Set<_>>();
if let Some(trait_obj) = self.ctx.rec_get_const_obj(&impl_trait.local_name()) {
@ -1354,11 +1367,11 @@ impl ASTLowerer {
let trait_impls = &mut self.ctx.outer.as_mut().unwrap().trait_impls;
// TODO: polymorphic trait
if let Some(impls) = trait_impls.get_mut(&trait_.qual_name()) {
impls.insert(TraitInstance::new(class.clone(), trait_.clone()));
impls.insert(TypeRelationInstance::new(class.clone(), trait_.clone()));
} else {
trait_impls.insert(
trait_.qual_name(),
set! {TraitInstance::new(class.clone(), trait_.clone())},
set! {TypeRelationInstance::new(class.clone(), trait_.clone())},
);
}
}

View file

@ -1384,9 +1384,11 @@ impl LimitedDisplay for Type {
rhs.limited_fmt(f, limit - 1)
}
Self::Or(lhs, rhs) => {
write!(f, "(")?;
lhs.limited_fmt(f, limit - 1)?;
write!(f, " or ")?;
rhs.limited_fmt(f, limit - 1)
rhs.limited_fmt(f, limit - 1)?;
write!(f, ")")
}
Self::Poly { name, params } => {
write!(f, "{name}(")?;
@ -1977,6 +1979,14 @@ impl Type {
}
}
/// assert!((A or B).contains_union(B))
pub fn contains_union(&self, typ: &Type) -> bool {
match self {
Type::Or(t1, t2) => t1.contains_union(typ) || t2.contains_union(typ),
_ => self == typ,
}
}
pub fn tvar_name(&self) -> Option<Str> {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().tvar_name(),

View file

@ -13,10 +13,12 @@ A typical Union is the `Option` type. The `Option` type is a `T or NoneType` pat
IntOrStr = Int or Str
assert dict.get("some key") in (Int or NoneType)
# Implicitly become `T != NoneType`
Option T = T or NoneType
```
Note that Union types are commutative but not associative. That is, `X or Y or Z` is `(X or Y) or Z`, not `X or (Y or Z)`.
Allowing this would result in, for example, `Int or Option(Str)`, `Option(Int) or Str` and `Option(Int or Str)` being of the same type.
## Intersection
Intersection types are got by combining types with the `and` operation.
@ -85,4 +87,4 @@ Diff, Complement types are not true algebraic types because they can always be s
<p align='center'>
<a href='./12_refinement.md'>Previous</a> | <a href='./14_dependent.md'>Next</a>
</p>
</p>

View file

@ -15,10 +15,12 @@ Union型では型について複数の可能性を与える事ができる。名
IntOrStr = Int or Str
assert dict.get("some key") in (Int or NoneType)
# 暗黙に`T != NoneType`となる
Option T = T or NoneType
```
Union型は可換ですが結合的ではないことに注意してください。すなわち、`X or Y or Z``(X or Y) or Z`であって`X or (Y or Z)`とはなりません。
これを認めると、例えば`Int or Option(Str)``Option(Int) or Str``Option(Int or Str)`が同じ型になってしまいます。
## 交差型
Intersection型は型同士を`and`演算で結合して得られます。
@ -87,4 +89,4 @@ Diff, Complement型は必ず簡約できるので真の代数演算型ではあ
<p align='center'>
<a href='./12_refinement.md'>Previous</a> | <a href='./14_dependent.md'>Next</a>
</p>
</p>

View file

@ -10,7 +10,7 @@ Point|Point <: Mul(Point)|.
Output = Nat
__mul__ self, other: Point =
self::x * other::x + self::y * other::y
Point|Point <: Eq(Point)|.
Point|Point <: Eq|.
__eq__ self, other: Point =
self::x == other::x and self::y == other::y

View file

@ -1,7 +1,10 @@
stop_or_call n, f: (Nat -> Nat), g: (Nat -> Nat) =
cond n <= 0:
1
g (f (n - 1))
if n <= 0:
do 1
do:
m = n - 1
assert m in Nat
g (f m)
fact(n: Nat): Nat =
stop_or_call n, fact, (r, ) -> r * n