diff --git a/crates/erg_compiler/context/initialize/mod.rs b/crates/erg_compiler/context/initialize/mod.rs index 73160ed94..c78757140 100644 --- a/crates/erg_compiler/context/initialize/mod.rs +++ b/crates/erg_compiler/context/initialize/mod.rs @@ -710,6 +710,17 @@ impl Context { } else { None }; + if DEBUG_MODE { + if let ValueObj::Subr(ConstSubr::Builtin(BuiltinConstSubr { + sig_t: Type::Subr(subr), + .. + })) = &obj + { + if subr.has_qvar() { + panic!("not quantified subr: {subr}"); + } + } + } // TODO: not all value objects are comparable let vi = VarInfo::new( v_enum(set! {obj.clone()}), @@ -741,6 +752,17 @@ impl Context { } else { None }; + if DEBUG_MODE { + if let ValueObj::Subr(ConstSubr::Builtin(BuiltinConstSubr { + sig_t: Type::Subr(subr), + .. + })) = &obj + { + if subr.has_qvar() { + panic!("not quantified subr: {subr}"); + } + } + } // TODO: not all value objects are comparable let vi = VarInfo::new( v_enum(set! {obj.clone()}), diff --git a/crates/erg_compiler/context/instantiate.rs b/crates/erg_compiler/context/instantiate.rs index 2e9045f1f..d9cef6268 100644 --- a/crates/erg_compiler/context/instantiate.rs +++ b/crates/erg_compiler/context/instantiate.rs @@ -16,6 +16,7 @@ use crate::ty::free::FreeTyParam; use crate::ty::free::GENERIC_LEVEL; use crate::ty::free::{Constraint, HasLevel}; use crate::ty::typaram::{TyParam, TyParamLambda}; +use crate::ty::ConstSubr; use crate::ty::ValueObj; use crate::ty::{HasType, Predicate, Type}; use crate::{type_feature_error, unreachable_error}; @@ -499,6 +500,135 @@ impl Context { } } + fn instantiate_pred( + &self, + pred: Predicate, + tmp_tv_cache: &mut TyVarCache, + loc: &impl Locational, + ) -> TyCheckResult { + match pred { + Predicate::And(l, r) => { + let l = self.instantiate_pred(*l, tmp_tv_cache, loc)?; + let r = self.instantiate_pred(*r, tmp_tv_cache, loc)?; + Ok(Predicate::and(l, r)) + } + Predicate::Or(l, r) => { + let l = self.instantiate_pred(*l, tmp_tv_cache, loc)?; + let r = self.instantiate_pred(*r, tmp_tv_cache, loc)?; + Ok(Predicate::or(l, r)) + } + Predicate::Not(pred) => { + let pred = self.instantiate_pred(*pred, tmp_tv_cache, loc)?; + Ok(Predicate::invert(pred)) + } + Predicate::Equal { lhs, rhs } => { + let rhs = self.instantiate_tp(rhs, tmp_tv_cache, loc)?; + Ok(Predicate::eq(lhs, rhs)) + } + Predicate::NotEqual { lhs, rhs } => { + let rhs = self.instantiate_tp(rhs, tmp_tv_cache, loc)?; + Ok(Predicate::ne(lhs, rhs)) + } + Predicate::GreaterEqual { lhs, rhs } => { + let rhs = self.instantiate_tp(rhs, tmp_tv_cache, loc)?; + Ok(Predicate::ge(lhs, rhs)) + } + Predicate::LessEqual { lhs, rhs } => { + let rhs = self.instantiate_tp(rhs, tmp_tv_cache, loc)?; + Ok(Predicate::le(lhs, rhs)) + } + Predicate::Value(value) => { + let value = self.instantiate_value(value, tmp_tv_cache, loc)?; + Ok(Predicate::Value(value)) + } + _ => Ok(pred), + } + } + + fn instantiate_value( + &self, + value: ValueObj, + tmp_tv_cache: &mut TyVarCache, + loc: &impl Locational, + ) -> TyCheckResult { + match value { + ValueObj::Type(mut typ) => { + let t = mem::take(typ.typ_mut()); + let t = self.instantiate_t_inner(t, tmp_tv_cache, loc)?; + *typ.typ_mut() = t; + Ok(ValueObj::Type(typ)) + } + ValueObj::Subr(subr) => match subr { + ConstSubr::Builtin(mut builtin) => { + let t = mem::take(&mut builtin.sig_t); + let t = self.instantiate_t_inner(t, tmp_tv_cache, loc)?; + builtin.sig_t = t; + Ok(ValueObj::Subr(ConstSubr::Builtin(builtin))) + } + ConstSubr::Gen(mut gen) => { + let t = mem::take(&mut gen.sig_t); + let t = self.instantiate_t_inner(t, tmp_tv_cache, loc)?; + gen.sig_t = t; + Ok(ValueObj::Subr(ConstSubr::Gen(gen))) + } + ConstSubr::User(mut user) => { + let t = mem::take(&mut user.sig_t); + let t = self.instantiate_t_inner(t, tmp_tv_cache, loc)?; + user.sig_t = t; + Ok(ValueObj::Subr(ConstSubr::User(user))) + } + }, + ValueObj::Array(arr) => { + let mut new = vec![]; + for v in arr.iter().cloned() { + new.push(self.instantiate_value(v, tmp_tv_cache, loc)?); + } + Ok(ValueObj::Array(new.into())) + } + ValueObj::Tuple(tup) => { + let mut new = vec![]; + for v in tup.iter().cloned() { + new.push(self.instantiate_value(v, tmp_tv_cache, loc)?); + } + Ok(ValueObj::Tuple(new.into())) + } + ValueObj::Set(set) => { + let mut new = Set::new(); + for v in set.into_iter() { + let v = self.instantiate_value(v, tmp_tv_cache, loc)?; + new.insert(v); + } + Ok(ValueObj::Set(new)) + } + ValueObj::Dict(dict) => { + let mut new = Dict::new(); + for (k, v) in dict.into_iter() { + let k = self.instantiate_value(k, tmp_tv_cache, loc)?; + let v = self.instantiate_value(v, tmp_tv_cache, loc)?; + new.insert(k, v); + } + Ok(ValueObj::Dict(new)) + } + ValueObj::Record(rec) => { + let mut new = Dict::new(); + for (k, v) in rec.into_iter() { + let v = self.instantiate_value(v, tmp_tv_cache, loc)?; + new.insert(k, v); + } + Ok(ValueObj::Record(new)) + } + ValueObj::DataClass { name, fields } => { + let mut new = Dict::new(); + for (k, v) in fields.into_iter() { + let v = self.instantiate_value(v, tmp_tv_cache, loc)?; + new.insert(k, v); + } + Ok(ValueObj::DataClass { name, fields: new }) + } + _ => Ok(value), + } + } + /// 'T -> ?T (quantified to free) fn instantiate_t_inner( &self, @@ -557,9 +687,7 @@ impl Context { } Refinement(mut refine) => { refine.t = Box::new(self.instantiate_t_inner(*refine.t, tmp_tv_cache, loc)?); - for tp in refine.pred.typarams_mut() { - *tp = self.instantiate_tp(mem::take(tp), tmp_tv_cache, loc)?; - } + refine.pred = Box::new(self.instantiate_pred(*refine.pred, tmp_tv_cache, loc)?); Ok(Type::Refinement(refine)) } Subr(mut subr) => { diff --git a/crates/erg_compiler/context/instantiate_spec.rs b/crates/erg_compiler/context/instantiate_spec.rs index ca21b1be2..f30637be7 100644 --- a/crates/erg_compiler/context/instantiate_spec.rs +++ b/crates/erg_compiler/context/instantiate_spec.rs @@ -973,7 +973,7 @@ impl Context { tmp_tv_cache, not_found_is_qvar, )?; - let pred = self.instantiate_pred(&set.pred, tmp_tv_cache)?; + let pred = self.instantiate_pred_from_expr(&set.pred, tmp_tv_cache)?; if let Ok(t) = self.instantiate_tp_as_type(iter, set) { return Ok(TyParam::t(refinement(set.var.inspect().clone(), t, pred))); } @@ -1293,7 +1293,7 @@ impl Context { } } - fn instantiate_pred( + fn instantiate_pred_from_expr( &self, expr: &ast::ConstExpr, tmp_tv_cache: &mut TyVarCache, @@ -1308,8 +1308,8 @@ impl Context { Ok(Predicate::Const(local.inspect().clone())) } ast::ConstExpr::BinOp(bin) => { - let lhs = self.instantiate_pred(&bin.lhs, tmp_tv_cache)?; - let rhs = self.instantiate_pred(&bin.rhs, tmp_tv_cache)?; + let lhs = self.instantiate_pred_from_expr(&bin.lhs, tmp_tv_cache)?; + let rhs = self.instantiate_pred_from_expr(&bin.rhs, tmp_tv_cache)?; match bin.op.kind { TokenKind::DblEq | TokenKind::NotEq @@ -1356,7 +1356,7 @@ impl Context { } } ast::ConstExpr::UnaryOp(unop) => { - let pred = self.instantiate_pred(&unop.expr, tmp_tv_cache)?; + let pred = self.instantiate_pred_from_expr(&unop.expr, tmp_tv_cache)?; match unop.op.kind { TokenKind::PreBitNot => Ok(!pred), _ => type_feature_error!( @@ -1634,7 +1634,7 @@ impl Context { ); tmp_tv_cache.push_or_init_typaram(&name, &tp, self); let pred = self - .instantiate_pred(&refine.pred, tmp_tv_cache) + .instantiate_pred_from_expr(&refine.pred, tmp_tv_cache) .map_err(|err| { tmp_tv_cache.remove(name.inspect()); err diff --git a/crates/erg_compiler/ty/const_subr.rs b/crates/erg_compiler/ty/const_subr.rs index 97004f22a..dfefc4833 100644 --- a/crates/erg_compiler/ty/const_subr.rs +++ b/crates/erg_compiler/ty/const_subr.rs @@ -80,7 +80,7 @@ impl ValueArgs { pub struct BuiltinConstSubr { name: Str, subr: fn(ValueArgs, &Context) -> EvalValueResult, - sig_t: Type, + pub(crate) sig_t: Type, as_type: Option, } @@ -157,7 +157,7 @@ pub struct GenConstSubr { name: Str, data: ClosureData, subr: fn(ClosureData, ValueArgs, &Context) -> EvalValueResult, - sig_t: Type, + pub(crate) sig_t: Type, as_type: Option, } diff --git a/crates/erg_compiler/ty/predicate.rs b/crates/erg_compiler/ty/predicate.rs index 386e6da59..de4372260 100644 --- a/crates/erg_compiler/ty/predicate.rs +++ b/crates/erg_compiler/ty/predicate.rs @@ -494,22 +494,6 @@ impl Predicate { } } - pub fn typarams_mut(&mut self) -> Vec<&mut TyParam> { - match self { - Self::Value(_) | Self::Const(_) => vec![], - Self::Equal { rhs, .. } - | Self::GreaterEqual { rhs, .. } - | Self::LessEqual { rhs, .. } - | Self::NotEqual { rhs, .. } => vec![rhs], - Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs - .typarams_mut() - .into_iter() - .chain(rhs.typarams_mut()) - .collect(), - Self::Not(pred) => pred.typarams_mut(), - } - } - pub fn invert(self) -> Self { match self { Self::Value(ValueObj::Bool(b)) => Self::Value(ValueObj::Bool(!b)),