This commit is contained in:
Shunsuke Shibayama 2022-10-24 14:32:34 +09:00
parent a8a59147f9
commit 9f85c88e7e
7 changed files with 53 additions and 44 deletions

View file

@ -628,7 +628,7 @@ impl Context {
// REVIEW: maybe this should be `unreachable` // REVIEW: maybe this should be `unreachable`
let tmp_tv_ctx = TyVarInstContext::new(self.level, q.bounds.clone(), self); let tmp_tv_ctx = TyVarInstContext::new(self.level, q.bounds.clone(), self);
let q_callable = self let q_callable = self
.instantiate_t( .instantiate_t_inner(
q.unbound_callable.as_ref().clone(), q.unbound_callable.as_ref().clone(),
&tmp_tv_ctx, &tmp_tv_ctx,
Location::Unknown, Location::Unknown,
@ -640,7 +640,7 @@ impl Context {
// REVIEW: maybe this should be `unreachable` // REVIEW: maybe this should be `unreachable`
let tmp_tv_ctx = TyVarInstContext::new(self.level, q.bounds.clone(), self); let tmp_tv_ctx = TyVarInstContext::new(self.level, q.bounds.clone(), self);
let q_callable = self let q_callable = self
.instantiate_t( .instantiate_t_inner(
q.unbound_callable.as_ref().clone(), q.unbound_callable.as_ref().clone(),
&tmp_tv_ctx, &tmp_tv_ctx,
Location::Unknown, Location::Unknown,

View file

@ -175,7 +175,7 @@ impl<'c> SubstContext<'c> {
pub fn substitute(&self, quant_t: Type) -> TyCheckResult<Type> { pub fn substitute(&self, quant_t: Type) -> TyCheckResult<Type> {
let tv_ctx = TyVarInstContext::new(self.ctx.level, self.bounds.clone(), self.ctx); let tv_ctx = TyVarInstContext::new(self.ctx.level, self.bounds.clone(), self.ctx);
let inst = self.ctx.instantiate_t(quant_t, &tv_ctx, self.loc)?; let inst = self.ctx.instantiate_t_inner(quant_t, &tv_ctx, self.loc)?;
for param in inst.typarams() { for param in inst.typarams() {
self.substitute_tp(&param)?; self.substitute_tp(&param)?;
} }

View file

@ -2136,15 +2136,16 @@ impl Context {
PS::named_nd("P", Int), PS::named_nd("P", Int),
]; ];
let class = Type::from(&m..=&n); let class = Type::from(&m..=&n);
let impls = poly("Add", vec![TyParam::from(&o..=&p)]);
// Interval is a bounding patch connecting M..N and (Add(O..P, M+O..N..P), Sub(O..P, M-P..N-O)) // Interval is a bounding patch connecting M..N and (Add(O..P, M+O..N..P), Sub(O..P, M-P..N-O))
let mut interval = Self::builtin_poly_patch("Interval", class.clone(), params, 2); let mut interval =
Self::builtin_poly_glue_patch("Interval", class.clone(), impls.clone(), params, 2);
let op_t = fn1_met( let op_t = fn1_met(
class.clone(), class.clone(),
Type::from(&o..=&p), Type::from(&o..=&p),
Type::from(m.clone() + o.clone()..=n.clone() + p.clone()), Type::from(m.clone() + o.clone()..=n.clone() + p.clone()),
); );
let mut interval_add = let mut interval_add = Self::builtin_methods(Some(impls), 2);
Self::builtin_methods(Some(poly("Add", vec![TyParam::from(&o..=&p)])), 2);
interval_add.register_builtin_impl("__add__", op_t, Const, Public); interval_add.register_builtin_impl("__add__", op_t, Const, Public);
interval_add.register_builtin_const( interval_add.register_builtin_const(
"Output", "Output",
@ -2174,10 +2175,11 @@ impl Context {
let t = mono_q("T"); let t = mono_q("T");
let u = mono_q("U"); let u = mono_q("U");
let base = or(t.clone(), u.clone()); 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 params = vec![PS::named_nd("T", Type), PS::named_nd("U", Type)];
let mut union_eq = Self::builtin_poly_patch("UnionEq", base.clone(), params, 1); let mut union_eq =
let mut union_eq_impl = Self::builtin_poly_glue_patch("UnionEq", base.clone(), impls.clone(), params, 1);
Self::builtin_methods(Some(poly("Eq", vec![ty_tp(base.clone())])), 1); let mut union_eq_impl = Self::builtin_methods(Some(impls), 1);
let op_t = fn1_met(base.clone(), base.clone(), Bool); let op_t = fn1_met(base.clone(), base.clone(), Bool);
let op_t = quant( let op_t = quant(
op_t, op_t,

View file

@ -730,7 +730,7 @@ impl Context {
other if simple.args.is_empty() => { other if simple.args.is_empty() => {
if let Some(tmp_tv_ctx) = tmp_tv_ctx { if let Some(tmp_tv_ctx) = tmp_tv_ctx {
if let Ok(t) = if let Ok(t) =
self.instantiate_t(mono_q(Str::rc(other)), tmp_tv_ctx, simple.loc()) self.instantiate_t_inner(mono_q(Str::rc(other)), tmp_tv_ctx, simple.loc())
{ {
return Ok(t); return Ok(t);
} }
@ -1190,14 +1190,14 @@ impl Context {
}*/ }*/
// 'T -> ?T // 'T -> ?T
if t.is_mono_q() { if t.is_mono_q() {
let t = self.instantiate_t(*t, tmp_tv_ctx, loc)?; let t = self.instantiate_t_inner(*t, tmp_tv_ctx, loc)?;
Ok(TyParam::t(t)) Ok(TyParam::t(t))
} }
// K('U) -> K(?U) // K('U) -> K(?U)
else { else {
let ctx = self.get_nominal_type_ctx(&t).unwrap(); let ctx = self.get_nominal_type_ctx(&t).unwrap();
let tv_ctx = TyVarInstContext::new(self.level, ctx.bounds(), self); let tv_ctx = TyVarInstContext::new(self.level, ctx.bounds(), self);
let t = self.instantiate_t(*t, &tv_ctx, loc)?; let t = self.instantiate_t_inner(*t, &tv_ctx, loc)?;
Ok(TyParam::t(t)) Ok(TyParam::t(t))
} }
} }
@ -1213,7 +1213,7 @@ impl Context {
} }
/// 'T -> ?T (quantified to free) /// 'T -> ?T (quantified to free)
pub(crate) fn instantiate_t( pub(crate) fn instantiate_t_inner(
&self, &self,
unbound: Type, unbound: Type,
tmp_tv_ctx: &TyVarInstContext, tmp_tv_ctx: &TyVarInstContext,
@ -1254,7 +1254,7 @@ impl Context {
Ok(poly_q(name, params)) Ok(poly_q(name, params))
} }
Refinement(mut refine) => { Refinement(mut refine) => {
refine.t = Box::new(self.instantiate_t(*refine.t, tmp_tv_ctx, loc)?); refine.t = Box::new(self.instantiate_t_inner(*refine.t, tmp_tv_ctx, loc)?);
let mut new_preds = set! {}; let mut new_preds = set! {};
for mut pred in refine.preds.into_iter() { for mut pred in refine.preds.into_iter() {
for tp in pred.typarams_mut() { for tp in pred.typarams_mut() {
@ -1267,16 +1267,18 @@ impl Context {
} }
Subr(mut subr) => { Subr(mut subr) => {
for pt in subr.non_default_params.iter_mut() { for pt in subr.non_default_params.iter_mut() {
*pt.typ_mut() = self.instantiate_t(mem::take(pt.typ_mut()), tmp_tv_ctx, loc)?; *pt.typ_mut() =
self.instantiate_t_inner(mem::take(pt.typ_mut()), tmp_tv_ctx, loc)?;
} }
if let Some(var_args) = subr.var_params.as_mut() { if let Some(var_args) = subr.var_params.as_mut() {
*var_args.typ_mut() = *var_args.typ_mut() =
self.instantiate_t(mem::take(var_args.typ_mut()), tmp_tv_ctx, loc)?; self.instantiate_t_inner(mem::take(var_args.typ_mut()), tmp_tv_ctx, loc)?;
} }
for pt in subr.default_params.iter_mut() { for pt in subr.default_params.iter_mut() {
*pt.typ_mut() = self.instantiate_t(mem::take(pt.typ_mut()), tmp_tv_ctx, loc)?; *pt.typ_mut() =
self.instantiate_t_inner(mem::take(pt.typ_mut()), tmp_tv_ctx, loc)?;
} }
let return_t = self.instantiate_t(*subr.return_t, tmp_tv_ctx, loc)?; let return_t = self.instantiate_t_inner(*subr.return_t, tmp_tv_ctx, loc)?;
let res = subr_t( let res = subr_t(
subr.kind, subr.kind,
subr.non_default_params, subr.non_default_params,
@ -1288,23 +1290,23 @@ impl Context {
} }
Record(mut dict) => { Record(mut dict) => {
for v in dict.values_mut() { for v in dict.values_mut() {
*v = self.instantiate_t(mem::take(v), tmp_tv_ctx, loc)?; *v = self.instantiate_t_inner(mem::take(v), tmp_tv_ctx, loc)?;
} }
Ok(Type::Record(dict)) Ok(Type::Record(dict))
} }
Ref(t) => { Ref(t) => {
let t = self.instantiate_t(*t, tmp_tv_ctx, loc)?; let t = self.instantiate_t_inner(*t, tmp_tv_ctx, loc)?;
Ok(ref_(t)) Ok(ref_(t))
} }
RefMut { before, after } => { RefMut { before, after } => {
let before = self.instantiate_t(*before, tmp_tv_ctx, loc)?; let before = self.instantiate_t_inner(*before, tmp_tv_ctx, loc)?;
let after = after let after = after
.map(|aft| self.instantiate_t(*aft, tmp_tv_ctx, loc)) .map(|aft| self.instantiate_t_inner(*aft, tmp_tv_ctx, loc))
.transpose()?; .transpose()?;
Ok(ref_mut(before, after)) Ok(ref_mut(before, after))
} }
Proj { lhs, rhs } => { Proj { lhs, rhs } => {
let lhs = self.instantiate_t(*lhs, tmp_tv_ctx, loc)?; let lhs = self.instantiate_t_inner(*lhs, tmp_tv_ctx, loc)?;
Ok(proj(lhs, rhs)) Ok(proj(lhs, rhs))
} }
ProjCall { ProjCall {
@ -1328,29 +1330,29 @@ impl Context {
panic!("a quantified type should not be instantiated, instantiate the inner type") panic!("a quantified type should not be instantiated, instantiate the inner type")
} }
FreeVar(fv) if fv.is_linked() => { FreeVar(fv) if fv.is_linked() => {
self.instantiate_t(fv.crack().clone(), tmp_tv_ctx, loc) self.instantiate_t_inner(fv.crack().clone(), tmp_tv_ctx, loc)
} }
FreeVar(fv) => { FreeVar(fv) => {
let (sub, sup) = fv.get_bound_types().unwrap(); let (sub, sup) = fv.get_bound_types().unwrap();
let sub = self.instantiate_t(sub, tmp_tv_ctx, loc)?; let sub = self.instantiate_t_inner(sub, tmp_tv_ctx, loc)?;
let sup = self.instantiate_t(sup, tmp_tv_ctx, loc)?; let sup = self.instantiate_t_inner(sup, tmp_tv_ctx, loc)?;
let new_constraint = Constraint::new_sandwiched(sub, sup, fv.cyclicity()); let new_constraint = Constraint::new_sandwiched(sub, sup, fv.cyclicity());
fv.update_constraint(new_constraint); fv.update_constraint(new_constraint);
Ok(FreeVar(fv)) Ok(FreeVar(fv))
} }
And(l, r) => { And(l, r) => {
let l = self.instantiate_t(*l, tmp_tv_ctx, loc)?; let l = self.instantiate_t_inner(*l, tmp_tv_ctx, loc)?;
let r = self.instantiate_t(*r, tmp_tv_ctx, loc)?; let r = self.instantiate_t_inner(*r, tmp_tv_ctx, loc)?;
Ok(self.intersection(&l, &r)) Ok(self.intersection(&l, &r))
} }
Or(l, r) => { Or(l, r) => {
let l = self.instantiate_t(*l, tmp_tv_ctx, loc)?; let l = self.instantiate_t_inner(*l, tmp_tv_ctx, loc)?;
let r = self.instantiate_t(*r, tmp_tv_ctx, loc)?; let r = self.instantiate_t_inner(*r, tmp_tv_ctx, loc)?;
Ok(self.union(&l, &r)) Ok(self.union(&l, &r))
} }
Not(l, r) => { Not(l, r) => {
let l = self.instantiate_t(*l, tmp_tv_ctx, loc)?; let l = self.instantiate_t_inner(*l, tmp_tv_ctx, loc)?;
let r = self.instantiate_t(*r, tmp_tv_ctx, loc)?; let r = self.instantiate_t_inner(*r, tmp_tv_ctx, loc)?;
Ok(not(l, r)) Ok(not(l, r))
} }
other if other.is_monomorphic() => Ok(other), other if other.is_monomorphic() => Ok(other),
@ -1362,7 +1364,8 @@ impl Context {
match quantified { match quantified {
Quantified(quant) => { Quantified(quant) => {
let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self); let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self);
let t = self.instantiate_t(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?; let t =
self.instantiate_t_inner(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?;
match &t { match &t {
Type::Subr(subr) => { Type::Subr(subr) => {
if let Some(self_t) = subr.self_t() { if let Some(self_t) = subr.self_t() {
@ -1385,7 +1388,8 @@ impl Context {
Refinement(refine) if refine.t.is_quantified() => { Refinement(refine) if refine.t.is_quantified() => {
let quant = enum_unwrap!(*refine.t, Type::Quantified); let quant = enum_unwrap!(*refine.t, Type::Quantified);
let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self); let tmp_tv_ctx = TyVarInstContext::new(self.level, quant.bounds, self);
let t = self.instantiate_t(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?; let t =
self.instantiate_t_inner(*quant.unbound_callable, &tmp_tv_ctx, callee.loc())?;
match &t { match &t {
Type::Subr(subr) => { Type::Subr(subr) => {
if let Some(self_t) = subr.self_t() { if let Some(self_t) = subr.self_t() {

View file

@ -700,9 +700,10 @@ impl Context {
#[allow(clippy::too_many_arguments)] #[allow(clippy::too_many_arguments)]
#[inline] #[inline]
pub fn poly_patch<S: Into<Str>>( pub fn poly_glue_patch<S: Into<Str>>(
name: S, name: S,
base: Type, base: Type,
impls: Type,
params: Vec<ParamSpec>, params: Vec<ParamSpec>,
cfg: ErgConfig, cfg: ErgConfig,
mod_cache: Option<SharedModuleCache>, mod_cache: Option<SharedModuleCache>,
@ -713,7 +714,7 @@ impl Context {
Self::poly( Self::poly(
name.into(), name.into(),
cfg, cfg,
ContextKind::Patch(base), ContextKind::GluePatch(TraitInstance::new(base, impls)),
params, params,
None, None,
mod_cache, mod_cache,
@ -724,15 +725,17 @@ impl Context {
} }
#[inline] #[inline]
pub fn builtin_poly_patch<S: Into<Str>>( pub fn builtin_poly_glue_patch<S: Into<Str>>(
name: S, name: S,
base: Type, base: Type,
impls: Type,
params: Vec<ParamSpec>, params: Vec<ParamSpec>,
capacity: usize, capacity: usize,
) -> Self { ) -> Self {
Self::poly_patch( Self::poly_glue_patch(
name, name,
base, base,
impls,
params, params,
ErgConfig::default(), ErgConfig::default(),
None, None,

View file

@ -57,7 +57,7 @@ impl Context {
let tv_ctx = TyVarInstContext::new(self.level + 1, bounds, self); let tv_ctx = TyVarInstContext::new(self.level + 1, bounds, self);
println!("tv_ctx: {tv_ctx}"); println!("tv_ctx: {tv_ctx}");
let inst = self let inst = self
.instantiate_t(unbound_t, &tv_ctx, Location::Unknown) .instantiate_t_inner(unbound_t, &tv_ctx, Location::Unknown)
.map_err(|_| ())?; .map_err(|_| ())?;
println!("inst: {inst}"); println!("inst: {inst}");
let quantified_again = self.generalize_t(inst); let quantified_again = self.generalize_t(inst);
@ -66,7 +66,7 @@ impl Context {
let unbound_t = *enum_unwrap!(quantified_again, Type::Quantified).unbound_callable; let unbound_t = *enum_unwrap!(quantified_again, Type::Quantified).unbound_callable;
// 同じtv_ctxで2回instantiateしないこと // 同じtv_ctxで2回instantiateしないこと
let inst = self let inst = self
.instantiate_t(unbound_t, &tv_ctx, Location::Unknown) .instantiate_t_inner(unbound_t, &tv_ctx, Location::Unknown)
.map_err(|_| ())?; // (?T(<: Eq('T))[2]) -> ?T(<: Eq('T))[2] .map_err(|_| ())?; // (?T(<: Eq('T))[2]) -> ?T(<: Eq('T))[2]
println!("inst: {inst}"); println!("inst: {inst}");
let quantified_again = self.generalize_t(inst); let quantified_again = self.generalize_t(inst);

View file

@ -171,14 +171,14 @@ impl Context {
// the input type of `is_class` must not be quantified (if the type is Proj). So instantiate it here. // the input type of `is_class` must not be quantified (if the type is Proj). So instantiate it here.
let l = if l.has_qvar() { let l = if l.has_qvar() {
let tv_ctx = TyVarInstContext::new(self.level, bounds.clone(), self); let tv_ctx = TyVarInstContext::new(self.level, bounds.clone(), self);
self.instantiate_t(l.clone(), &tv_ctx, Location::Unknown) self.instantiate_t_inner(l.clone(), &tv_ctx, Location::Unknown)
.unwrap() .unwrap()
} else { } else {
l.clone() l.clone()
}; };
let r = if r.has_qvar() { let r = if r.has_qvar() {
let tv_ctx = TyVarInstContext::new(self.level, bounds.clone(), self); let tv_ctx = TyVarInstContext::new(self.level, bounds.clone(), self);
self.instantiate_t(r.clone(), &tv_ctx, Location::Unknown) self.instantiate_t_inner(r.clone(), &tv_ctx, Location::Unknown)
.unwrap() .unwrap()
} else { } else {
r.clone() r.clone()
@ -637,7 +637,7 @@ impl Context {
let sub_type = if inst.sub_type.has_qvar() { let sub_type = if inst.sub_type.has_qvar() {
let sub_ctx = self.get_nominal_type_ctx(&inst.sub_type).unwrap(); let sub_ctx = self.get_nominal_type_ctx(&inst.sub_type).unwrap();
let tv_ctx = TyVarInstContext::new(self.level, sub_ctx.bounds(), self); let tv_ctx = TyVarInstContext::new(self.level, sub_ctx.bounds(), self);
self.instantiate_t(inst.sub_type, &tv_ctx, Location::Unknown) self.instantiate_t_inner(inst.sub_type, &tv_ctx, Location::Unknown)
.unwrap() .unwrap()
} else { } else {
inst.sub_type inst.sub_type
@ -645,7 +645,7 @@ impl Context {
let sup_trait = if inst.sup_trait.has_qvar() { let sup_trait = if inst.sup_trait.has_qvar() {
let sup_ctx = self.get_nominal_type_ctx(&inst.sup_trait).unwrap(); let sup_ctx = self.get_nominal_type_ctx(&inst.sup_trait).unwrap();
let tv_ctx = TyVarInstContext::new(self.level, sup_ctx.bounds(), self); let tv_ctx = TyVarInstContext::new(self.level, sup_ctx.bounds(), self);
self.instantiate_t(inst.sup_trait, &tv_ctx, Location::Unknown) self.instantiate_t_inner(inst.sup_trait, &tv_ctx, Location::Unknown)
.unwrap() .unwrap()
} else { } else {
inst.sup_trait inst.sup_trait