language-servers/erg
1
0
Fork 0
mirror of https://github.com/erg-lang/erg.git synced 2025-09-27 19:59:07 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: support inherited refinement types

Browse source
This commit is contained in:
Shunsuke Shibayama 2023-10-31 12:24:41 +09:00
parent 678c02faf9
commit a6336fa896
6 changed files with 125 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

11
crates/erg_compiler/codegen.rs
View file

@ -1350,12 +1350,19 @@ impl PyCodeGenerator {
// fn emit_poly_type_def(&mut self, sig: SubrSignature, body: DefBody) {}
/// Y = Inherit X => class Y(X): ...
/// N = Inherit 1..10 => class N(Nat): ...
fn emit_require_type(&mut self, obj: GenTypeObj, require_or_sup: Option<Expr>) -> usize {
log!(info "entered {} ({obj}, {})", fn_name!(), fmt_option!(require_or_sup));
match obj {
GenTypeObj::Class(_) => 0,
GenTypeObj::Subclass(_) => {
self.emit_expr(require_or_sup.unwrap());
GenTypeObj::Subclass(typ) => {
let require_or_sup = require_or_sup.unwrap();
let typ = if require_or_sup.is_acc() {
require_or_sup
} else {
Expr::try_from_type(typ.sup.typ().derefine()).unwrap_or(require_or_sup)
};
self.emit_expr(typ);
1 // TODO: not always 1
}
_ => todo!(),

79
crates/erg_compiler/context/compare.rs
View file

@ -3,6 +3,7 @@ use std::option::Option; // conflicting to Type::Option
use erg_common::consts::DEBUG_MODE;
use erg_common::dict::Dict;
use erg_common::set::Set;
use erg_common::style::colors::DEBUG_ERROR;
use erg_common::traits::StructuralEq;
use erg_common::{assume_unreachable, log};
@ -524,46 +525,53 @@ impl Context {
}
true
}
(Type, Record(rec)) => {
(Bool, Guard { .. }) => true,
(Mono(n), NamedTuple(_)) => &n[..] == "GenericNamedTuple" || &n[..] == "GenericTuple",
(Mono(n), Record(_)) => &n[..] == "Record",
(ty @ (Type | ClassType | TraitType), Record(rec)) => {
for (_, t) in rec.iter() {
if !self.supertype_of(&Type, t) {
if !self.supertype_of(ty, t) {
return false;
}
}
true
}
(Bool, Guard { .. }) => true,
(Mono(n), NamedTuple(_)) => &n[..] == "GenericNamedTuple" || &n[..] == "GenericTuple",
(Mono(n), Record(_)) => &n[..] == "Record",
(Type, Subr(subr)) => self.supertype_of(&Type, &subr.return_t),
(Type, Poly { name, params }) if &name[..] == "Set" => {
(ty @ (Type | ClassType | TraitType), Subr(subr)) => {
self.supertype_of(ty, &subr.return_t)
}
(Type | ClassType | TraitType, Poly { name, params }) if &name[..] == "Set" => {
self.convert_tp_into_value(params[0].clone()).is_ok()
}
(Type, Poly { name, params })
(Type | ClassType, Poly { name, params }) if &name[..] == "Range" => {
self.convert_tp_into_value(params[0].clone()).is_ok()
}
(ty @ (Type | ClassType | TraitType), Poly { name, params })
if &name[..] == "Array" || &name[..] == "UnsizedArray" || &name[..] == "Set" =>
{
let elem_t = self.convert_tp_into_type(params[0].clone()).unwrap();
self.supertype_of(&Type, &elem_t)
self.supertype_of(ty, &elem_t)
}
(Type, Poly { name, params }) if &name[..] == "Tuple" => {
(ty @ (Type | ClassType | TraitType), Poly { name, params })
if &name[..] == "Tuple" =>
{
// Type :> Tuple Ts == Type :> Ts
// e.g. Type :> Tuple [Int, Str] == false
// Type :> Tuple [Type, Type] == true
if let Ok(arr_t) = self.convert_tp_into_type(params[0].clone()) {
return self.supertype_of(&Type, &arr_t);
return self.supertype_of(ty, &arr_t);
} else if let Ok(tps) = Vec::try_from(params[0].clone()) {
for tp in tps {
let Ok(t) = self.convert_tp_into_type(tp) else {
return false;
};
if !self.supertype_of(&Type, &t) {
if !self.supertype_of(ty, &t) {
return false;
}
}
}
true
}
(Type, Poly { name, params }) if &name[..] == "Dict" => {
(ty @ (Type | ClassType | TraitType), Poly { name, params }) if &name[..] == "Dict" => {
// Type :> Dict T == Type :> T
// e.g.
// Type :> Dict {"a": 1} == false
@ -583,7 +591,7 @@ impl Context {
let Ok(v) = self.convert_tp_into_type(v) else {
return false;
};
if !self.supertype_of(&Type, &k) || !self.supertype_of(&Type, &v) {
if !self.supertype_of(ty, &k) || !self.supertype_of(ty, &v) {
return false;
}
}
@ -1547,6 +1555,37 @@ impl Context {
}
}
// {I >= 0} :> {I >= 1}
// mode == "and", reduced: {I >= 0}, pred: {I >= 1}
// => reduced: {I >= 1} ((I >= 0 and I >= 1) == I >= 1)
// mode == "and", reduced: {I >= 1}, pred: {I >= 0}
// => reduced: {I >= 1}
// mode == "or", reduced: {I >= 0}, pred: {I >= 1}
// => reduced: {I >= 0} ((I >= 0 or I >= 1) == I >= 0)
fn reduce_preds<'s>(&self, mode: &str, preds: Set<&'s Predicate>) -> Set<&'s Predicate> {
let mut reduced = Set::<&'s Predicate>::new();
for pred in preds {
// remove unnecessary pred
// TODO: remove all unnecessary preds
if let Some(&old) = reduced.iter().find(|existing| match mode {
"and" => self.is_super_pred_of(existing, pred),
"or" => self.is_sub_pred_of(existing, pred),
_ => unreachable!(),
}) {
reduced.remove(old);
}
// insert if necessary
if reduced.iter().all(|existing| match mode {
"and" => !self.is_sub_pred_of(existing, pred),
"or" => !self.is_super_pred_of(existing, pred),
_ => unreachable!(),
}) {
reduced.insert(pred);
}
}
reduced
}
/// see doc/LANG/compiler/refinement_subtyping.md
/// ```python
/// assert is_super_pred({I >= 0}, {I == 0})
@ -1610,8 +1649,8 @@ impl Context {
// NG: (self.is_super_pred_of(l1, l2) && self.is_super_pred_of(r1, r2))
// || (self.is_super_pred_of(l1, r2) && self.is_super_pred_of(r1, l2))
(Pred::And(_, _), Pred::And(_, _)) => {
let lhs_ands = lhs.ands();
let rhs_ands = rhs.ands();
let lhs_ands = self.reduce_preds("and", lhs.ands());
let rhs_ands = self.reduce_preds("and", rhs.ands());
for r_val in rhs_ands.iter() {
if lhs_ands
.get_by(r_val, |l, r| self.is_super_pred_of(l, r))
@ -1627,8 +1666,8 @@ impl Context {
// NG: (self.is_super_pred_of(l1, l2) && self.is_super_pred_of(r1, r2))
// || (self.is_super_pred_of(l1, r2) && self.is_super_pred_of(r1, l2))
(Pred::Or(_, _), Pred::Or(_, _)) => {
let lhs_ors = lhs.ors();
let rhs_ors = rhs.ors();
let lhs_ors = self.reduce_preds("or", lhs.ors());
let rhs_ors = self.reduce_preds("or", rhs.ors());
for r_val in rhs_ors.iter() {
if lhs_ors
.get_by(r_val, |l, r| self.is_super_pred_of(l, r))
@ -1656,6 +1695,10 @@ impl Context {
}
}
fn is_sub_pred_of(&self, lhs: &Predicate, rhs: &Predicate) -> bool {
self.is_super_pred_of(rhs, lhs)
}
pub(crate) fn is_sub_constraint_of(&self, l: &Constraint, r: &Constraint) -> bool {
match (l, r) {
// (?I: Nat) <: (?I: Int)

6
crates/erg_compiler/context/eval.rs
View file

@ -21,8 +21,8 @@ use erg_parser::token::{Token, TokenKind};
use crate::ty::constructors::{
array_t, bounded, closed_range, dict_t, mono, mono_q, named_free_var, poly, proj, proj_call,
ref_, ref_mut, refinement, set_t, subr_t, subtypeof, tp_enum, tuple_t, unknown_len_array_t,
v_enum,
ref_, ref_mut, refinement, set_t, subr_t, subtypeof, tp_enum, try_v_enum, tuple_t,
unknown_len_array_t, v_enum,
};
use crate::ty::free::HasLevel;
use crate::ty::typaram::{OpKind, TyParam};
@ -2015,7 +2015,7 @@ impl Context {
let elem = self.convert_value_into_type(*elem)?;
Ok(unknown_len_array_t(elem))
}
ValueObj::Set(set) => Ok(v_enum(set)),
ValueObj::Set(set) => try_v_enum(set).map_err(ValueObj::Set),
ValueObj::Dict(dic) => {
let dic = dic
.into_iter()

15
crates/erg_compiler/hir.rs
View file

@ -2716,6 +2716,14 @@ impl Expr {
}
}
pub fn is_acc(&self) -> bool {
match self {
Self::Accessor(_) => true,
Self::TypeAsc(tasc) => tasc.expr.is_acc(),
_ => false,
}
}
pub fn last_name(&self) -> Option<&VarName> {
match self {
Expr::Accessor(acc) => Some(acc.last_name()),
@ -2884,6 +2892,13 @@ impl Expr {
_ => 5,
}
}
// TODO: structural types
pub fn try_from_type(typ: Type) -> Result<Expr, Type> {
Ok(Expr::Accessor(Accessor::Ident(
Identifier::public_with_line(Token::DUMMY, typ.local_name(), 0),
)))
}
}
/// Toplevel grammar unit

10
crates/erg_compiler/ty/constructors.rs
View file

@ -100,9 +100,9 @@ pub fn module_from_path<P: Into<PathBuf>>(path: P) -> Type {
module(TyParam::Value(s))
}
pub fn v_enum(s: Set<ValueObj>) -> Type {
pub fn try_v_enum(s: Set<ValueObj>) -> Result<Type, Set<ValueObj>> {
if !is_homogeneous(&s) {
panic!("{s} is not homogeneous");
return Err(s);
}
let name = FRESH_GEN.fresh_varname();
let t = inner_class(&s);
@ -111,7 +111,11 @@ pub fn v_enum(s: Set<ValueObj>) -> Type {
.map(|o| Predicate::eq(name.clone(), TyParam::value(o)))
.fold(Predicate::FALSE, |acc, p| acc | p);
let refine = RefinementType::new(name, t, preds);
Type::Refinement(refine)
Ok(Type::Refinement(refine))
}
pub fn v_enum(s: Set<ValueObj>) -> Type {
try_v_enum(s).unwrap_or_else(|set| panic!("not homogeneous: {}", set))
}
pub fn tp_enum(ty: Type, s: Set<TyParam>) -> Type {

30
examples/refinement.er Normal file
View file

@ -0,0 +1,30 @@
_: {"a", "b", "c"} = "a" # OK
_: {"a", "b", "c"} = "d" # ERR
# 1..12 == {1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12} as type
_: 1..12 = 1 # OK
_: 1..12 = 13 # ERR
Suite = Class { "Heart", "Spade", "Club", "Diamond" }
Suite.
is_heart self = self::base == "Heart"
Number = Class 1..13
Number.
is_ace self = self::base == 1
Card = Class { .suite = Suite; .number = Number }
Card.
from_str_and_num suite: Str, num: Nat =
assert suite in {"Heart", "Spade", "Club", "Diamond"}
assert num in 1..13
Card.new { .suite = Suite.new suite; .number = Number.new num }
is_ace_of_heart self = self.suite.is_heart() and self.number.is_ace()
c = Card.new { .suite = Suite.new "Heart"; .number = Number.new 1 }
assert c.is_ace_of_heart()
Nat8 = Inherit 1..255
Nat8.
as_ascii self = chr self
n = Nat8.new 97
assert n.as_ascii() == "a"