feat: add ==/!= narrowing

This commit is contained in:
Shunsuke Shibayama 2023-03-29 01:32:29 +09:00
parent fc3fe5de0c
commit ccf02405d8
10 changed files with 293 additions and 54 deletions

View file

@ -5,6 +5,7 @@ use erg_common::dict::Dict;
use erg_common::error::MultiErrorDisplay;
use erg_common::style::colors::DEBUG_ERROR;
use erg_common::traits::StructuralEq;
use erg_common::Str;
use erg_common::{assume_unreachable, log};
use crate::ty::constructors::{and, not, or, poly};
@ -12,7 +13,7 @@ use crate::ty::free::{Constraint, FreeKind};
use crate::ty::typaram::{OpKind, TyParam, TyParamOrdering};
use crate::ty::value::ValueObj;
use crate::ty::value::ValueObj::Inf;
use crate::ty::{Field, Predicate, RefinementType, SubrKind, SubrType, Type};
use crate::ty::{Field, GuardType, Predicate, RefinementType, SubrKind, SubrType, Type};
use Predicate as Pred;
use TyParamOrdering::*;
@ -1011,6 +1012,12 @@ impl Context {
self.intersection(&fv.crack(), other)
}
(Refinement(l), Refinement(r)) => Type::Refinement(self.intersection_refinement(l, r)),
(other, Refinement(refine)) | (Refinement(refine), other) => {
let other = other.clone().into_refinement();
let intersec = self.intersection_refinement(&other, refine);
self.try_squash_refinement(intersec)
.unwrap_or_else(Type::Refinement)
}
(Structural(l), Structural(r)) => self.intersection(l, r).structuralize(),
// {.i = Int} and {.s = Str} == {.i = Int; .s = Str}
(Record(l), Record(r)) => Type::Record(l.clone().concat(r.clone())),
@ -1022,12 +1029,15 @@ impl Context {
_ => Type::Never,
},
(l, r) if self.is_trait(l) && self.is_trait(r) => and(l.clone(), r.clone()),
(_, Not(r)) => self.diff(lhs, r),
(Not(l), _) => self.diff(rhs, l),
(_l, _r) => Type::Never,
}
}
/// ```erg
/// {I: Int | I > 0} and {I: Int | I < 10} == {I: Int | I > 0 and I < 10}
/// {x: Int or NoneType | True} and {x: Obj | x != None} == {x: Int or NoneType | x != None} (== Int)
/// ```
fn intersection_refinement(
&self,
@ -1040,6 +1050,58 @@ impl Context {
RefinementType::new(lhs.var.clone(), intersec, *lhs.pred.clone() & rhs_pred)
}
/// ```erg
/// {x: Int | True}.try_squash() == Ok(Int)
/// {x: Int or NoneType | x != None}.squash() == Ok(Int)
/// {x: Str or Bool | x != False}.squash() == Err({x: Str or Bool | x != False})
/// {x: Str or Bool | x != True and x != False}.squash() == Ok(Str)
/// {x: Nat or {-1} | x != 2}.squash() == Err({x: Int | (x >= 0 or x == -1) and x != 2 })
/// ```
pub(crate) fn try_squash_refinement(
&self,
refine: RefinementType,
) -> Result<Type, RefinementType> {
let unions = refine.t.union_types();
let complement = Type::from(self.type_from_pred(refine.pred.clone().invert()));
let union = unions
.into_iter()
.filter(|t| !self.subtype_of(t, &complement))
.fold(Never, |union, t| self.union(&union, &t));
if &union != refine.t.as_ref() {
Ok(union)
} else {
Err(refine)
}
}
/// (x == 1) => {x: Int | x == 1}
/// (x == c) where c: Str => {x: Str | x == c}
fn type_from_pred(&self, pred: Predicate) -> RefinementType {
let t = self.get_pred_type(&pred);
let name = pred.subject().unwrap_or("_");
RefinementType::new(Str::rc(name), t, pred)
}
fn get_pred_type(&self, pred: &Predicate) -> Type {
match pred {
Predicate::Equal { rhs, .. }
| Predicate::NotEqual { rhs, .. }
| Predicate::GreaterEqual { rhs, .. }
| Predicate::LessEqual { rhs, .. } => self.get_tp_t(rhs).unwrap_or(Obj),
Predicate::Not(pred) => self.get_pred_type(pred),
Predicate::Value(val) => val.class(),
// x == 1 or x == "a" => Int or Str
Predicate::Or(lhs, rhs) => {
self.union(&self.get_pred_type(lhs), &self.get_pred_type(rhs))
}
// REVIEW:
Predicate::And(lhs, rhs) => {
self.intersection(&self.get_pred_type(lhs), &self.get_pred_type(rhs))
}
Predicate::Const(name) => todo!("get_pred_type({name})"),
}
}
/// returns complement (not A)
#[allow(clippy::only_used_in_recursion)]
pub(crate) fn complement(&self, ty: &Type) -> Type {
@ -1047,10 +1109,32 @@ impl Context {
FreeVar(fv) if fv.is_linked() => self.complement(&fv.crack()),
Not(t) => *t.clone(),
Refinement(r) => Type::Refinement(r.clone().invert()),
Guard(guard) => Type::Guard(GuardType::new(
guard.var.clone(),
self.complement(&guard.to),
)),
other => not(other.clone()),
}
}
/// Returns difference of two types (`A - B` == `A and not B`).
/// ```erg
/// (A or B).diff(B) == A
/// ```
pub fn diff(&self, lhs: &Type, rhs: &Type) -> Type {
match (self.supertype_of(lhs, rhs), self.subtype_of(lhs, rhs)) {
(true, true) => return Type::Never, // lhs = rhs
(false, false) => return lhs.clone(),
_ => {}
}
match lhs {
Type::FreeVar(fv) if fv.is_linked() => self.diff(&fv.crack(), rhs),
// Type::And(l, r) => self.intersection(&self.diff(l, rhs), &self.diff(r, rhs)),
Type::Or(l, r) => self.union(&self.diff(l, rhs), &self.diff(r, rhs)),
_ => lhs.clone(),
}
}
/// see doc/LANG/compiler/refinement_subtyping.md
/// ```python
/// assert is_super_pred({I >= 0}, {I == 0})

View file

@ -176,7 +176,7 @@ impl Context {
_ => {
let (verb, preposition, _sequence) = Self::get_verb_and_preposition(&expected)?;
found
.union_types()
.union_pair()
.map(|(t1, t2)| format!("cannot {verb} {t1} {preposition} {t2}"))
.or_else(|| {
expected.inner_ts().get(0).map(|expected_inner| {

View file

@ -124,11 +124,26 @@ impl Context {
let name = self.erg_to_py_names.get(name).map_or(name, |s| &s[..]);
self.locals
.get_key_value(name)
.or_else(|| self.get_param_kv(name))
.or_else(|| self.decls.get_key_value(name))
.or_else(|| self.future_defined_locals.get_key_value(name))
.or_else(|| self.get_outer().and_then(|ctx| ctx.get_var_kv(name)))
}
fn get_param_kv(&self, name: &str) -> Option<(&VarName, &VarInfo)> {
#[cfg(feature = "py_compatible")]
let name = self.erg_to_py_names.get(name).map_or(name, |s| &s[..]);
self.params
.iter()
.find(|(opt_name, _)| {
opt_name
.as_ref()
.map(|n| &n.inspect()[..] == name)
.unwrap_or(false)
})
.map(|(opt_name, vi)| (opt_name.as_ref().unwrap(), vi))
}
pub fn get_singular_ctxs_by_hir_expr(
&self,
obj: &hir::Expr,

View file

@ -1351,4 +1351,12 @@ impl Context {
self.instantiate_typespec(&t_spec, None, &mut dummy, RegistrationMode::Normal, false)
.ok()
}
pub(crate) fn expr_to_value(&self, expr: ast::Expr) -> Option<ValueObj> {
let const_expr = Parser::validate_const_expr(expr).ok()?;
let mut dummy = TyVarCache::new(self.level, self);
self.instantiate_const_expr(&const_expr, None, &mut dummy, false)
.ok()
.and_then(|tp| ValueObj::try_from(tp).ok())
}
}

View file

@ -52,6 +52,40 @@ pub trait ContextProvider {
const BUILTINS: &Str = &Str::ever("<builtins>");
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum ControlKind {
If,
While,
For,
Match,
Try,
With,
}
impl TryFrom<&str> for ControlKind {
type Error = ();
fn try_from(s: &str) -> Result<Self, Self::Error> {
match s {
"if" | "if!" => Ok(ControlKind::If),
"while!" => Ok(ControlKind::While),
"for" | "for!" => Ok(ControlKind::For),
"match" | "match!" => Ok(ControlKind::Match),
"try" | "try!" => Ok(ControlKind::Try),
"with" | "with!" => Ok(ControlKind::With),
_ => Err(()),
}
}
}
impl ControlKind {
pub const fn is_if(&self) -> bool {
matches!(self, ControlKind::If)
}
pub const fn is_conditional(&self) -> bool {
matches!(self, ControlKind::If | ControlKind::While)
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct TraitImpl {
pub sub_type: Type,
@ -1078,6 +1112,12 @@ impl Context {
pub fn shared(&self) -> &SharedCompilerResource {
self.shared.as_ref().unwrap()
}
pub fn control_kind(&self) -> Option<ControlKind> {
self.higher_order_caller
.last()
.and_then(|caller| ControlKind::try_from(&caller[..]).ok())
}
}
#[derive(Debug, Clone, Default)]