fix: predicate instantiation bug

erg-lang · Aug 22, 2023 · 97afccb · 97afccb
1 parent 89f9c42
commit 97afccb
Show file tree

Hide file tree

Showing 5 changed files with 161 additions and 27 deletions.
diff --git 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
@@ -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<Predicate> {
+        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<ValueObj> {
+        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
@@ -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
@@ -80,7 +80,7 @@ impl ValueArgs {
 pub struct BuiltinConstSubr {
     name: Str,
     subr: fn(ValueArgs, &Context) -> EvalValueResult<TyParam>,
-    sig_t: Type,
+    pub(crate) sig_t: Type,
     as_type: Option<Type>,
 }
 
@@ -157,7 +157,7 @@ pub struct GenConstSubr {
     name: Str,
     data: ClosureData,
     subr: fn(ClosureData, ValueArgs, &Context) -> EvalValueResult<TyParam>,
-    sig_t: Type,
+    pub(crate) sig_t: Type,
     as_type: Option<Type>,
 }
 

diff --git 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)),