Implement type spec of projection and enum types

This commit is contained in:
Shunsuke Shibayama 2022-10-22 14:01:48 +09:00
parent 4eae5788ca
commit 47bedf67d8
14 changed files with 282 additions and 128 deletions

View file

@ -113,6 +113,12 @@ impl Context {
return self.same_type_of(t, &other_t);
}
},
(TyParam::Value(ValueObj::Type(l)), TyParam::Type(r)) => {
return self.same_type_of(l.typ(), r.as_ref());
}
(TyParam::Type(l), TyParam::Value(ValueObj::Type(r))) => {
return self.same_type_of(l.as_ref(), r.typ());
}
(l, r) if l == r => {
return true;
}
@ -567,8 +573,9 @@ impl Context {
// ({I: Int | I >= 0} :> {I: Int | I >= 1}) == true,
// ({I: Int | I >= 0} :> {N: Nat | N >= 1}) == true,
// ({I: Int | I > 1 or I < -1} :> {I: Int | I >= 0}) == false,
// {1, 2, 3} :> {1, } == true
(Refinement(l), Refinement(r)) => {
if !self.supertype_of(&l.t, &r.t) {
if !self.supertype_of(&l.t, &r.t) && !self.supertype_of(&r.t, &l.t) {
return false;
}
let mut r_preds_clone = r.preds.clone();
@ -777,6 +784,9 @@ impl Context {
}
fn supertype_of_tp(&self, lp: &TyParam, rp: &TyParam, variance: Variance) -> bool {
if lp == rp {
return true;
}
match (lp, rp, variance) {
(TyParam::FreeVar(fv), _, _) if fv.is_linked() => {
self.supertype_of_tp(&fv.crack(), rp, variance)

View file

@ -224,10 +224,13 @@ impl<'c> SubstContext<'c> {
Type::FreeVar(fv) => {
if let Some(name) = fv.unbound_name() {
if let Some(tp) = self.params.get(&name) {
if let TyParam::Type(t) = tp {
self.ctx.sub_unify(param_t, t, Location::Unknown, None)?;
} else {
panic!()
match Type::try_from(tp.clone()) {
Ok(t) => {
self.ctx.sub_unify(param_t, &t, Location::Unknown, None)?;
}
Err(_) => {
todo!("")
}
}
}
}
@ -1254,6 +1257,13 @@ impl Context {
/// NOTE: lとrが型の場合はContextの方で判定する
pub(crate) fn shallow_eq_tp(&self, lhs: &TyParam, rhs: &TyParam) -> bool {
match (lhs, rhs) {
(TyParam::Type(l), _) if l.is_unbound_var() => {
self.subtype_of(&self.get_tp_t(rhs).unwrap(), &Type::Type)
}
(_, TyParam::Type(r)) if r.is_unbound_var() => {
let lhs = self.get_tp_t(lhs).unwrap();
self.subtype_of(&lhs, &Type::Type)
}
(TyParam::Type(l), TyParam::Type(r)) => l == r,
(TyParam::Value(l), TyParam::Value(r)) => l == r,
(TyParam::Erased(l), TyParam::Erased(r)) => l == r,
@ -1287,7 +1297,7 @@ impl Context {
(TyParam::Erased(t), _) => t.as_ref() == &self.get_tp_t(rhs).unwrap(),
(_, TyParam::Erased(t)) => t.as_ref() == &self.get_tp_t(lhs).unwrap(),
(TyParam::MonoQVar(_), _) | (_, TyParam::MonoQVar(_)) => false,
(l, r) => todo!("l: {l}, r: {r}"),
(l, r) => todo!("l: {l:?}, r: {r:?}"),
}
}
}

View file

@ -19,6 +19,7 @@ use ast::{
};
use erg_parser::ast;
use erg_parser::token::TokenKind;
use erg_parser::Parser;
use crate::ty::constructors::*;
use crate::ty::free::{Constraint, Cyclicity, FreeTyVar};
@ -29,7 +30,7 @@ use TyParamOrdering::*;
use Type::*;
use crate::context::{Context, RegistrationMode};
use crate::error::{SingleTyCheckResult, TyCheckError, TyCheckErrors, TyCheckResult};
use crate::error::{TyCheckError, TyCheckErrors, TyCheckResult};
use crate::hir;
use crate::AccessKind;
use RegistrationMode::*;
@ -323,6 +324,7 @@ impl TyVarInstContext {
fn instantiate_qtp(&mut self, quantified: TyParam) -> TyParam {
match quantified {
TyParam::FreeVar(fv) if fv.is_linked() => self.instantiate_qtp(fv.crack().clone()),
TyParam::MonoQVar(n) => {
if let Some(t) = self.get_typaram(&n) {
t.clone()
@ -453,13 +455,9 @@ impl TyVarInstContext {
pub(crate) fn get_tyvar(&self, name: &str) -> Option<&Type> {
self.tyvar_instances.get(name).or_else(|| {
self.typaram_instances.get(name).map(|t| {
if let TyParam::Type(t) = t {
t.as_ref()
} else {
todo!("{t}")
}
})
self.typaram_instances
.get(name)
.map(|tp| <&Type>::try_from(tp).unwrap())
})
}
@ -651,6 +649,14 @@ impl Context {
self.instantiate_simple_t(simple, opt_decl_t, tmp_tv_ctx, not_found_is_qvar)
}
ast::PreDeclTypeSpec::Attr { namespace, t } => {
if let Ok(namespace) = Parser::validate_const_expr(namespace.as_ref().clone()) {
if let Ok(namespace) =
self.instantiate_const_expr_as_type(&namespace, None, tmp_tv_ctx)
{
let rhs = t.ident.inspect();
return Ok(proj(namespace, rhs));
}
}
let ctx = self.get_singular_ctx(namespace.as_ref(), &self.name)?;
if let Some((typ, _)) = ctx.rec_get_type(t.ident.inspect()) {
// TODO: visibility check
@ -698,9 +704,9 @@ impl Context {
// TODO: kw
let mut args = simple.args.pos_args();
if let Some(first) = args.next() {
let t = self.instantiate_const_expr_as_type(&first.expr)?;
let t = self.instantiate_const_expr_as_type(&first.expr, None, tmp_tv_ctx)?;
let len = args.next().unwrap();
let len = self.instantiate_const_expr(&len.expr)?;
let len = self.instantiate_const_expr(&len.expr, None, tmp_tv_ctx)?;
Ok(array_t(t, len))
} else {
Ok(mono("GenericArray"))
@ -709,14 +715,14 @@ impl Context {
"Ref" => {
let mut args = simple.args.pos_args();
let first = args.next().unwrap();
let t = self.instantiate_const_expr_as_type(&first.expr)?;
let t = self.instantiate_const_expr_as_type(&first.expr, None, tmp_tv_ctx)?;
Ok(ref_(t))
}
"RefMut" => {
// TODO after
let mut args = simple.args.pos_args();
let first = args.next().unwrap();
let t = self.instantiate_const_expr_as_type(&first.expr)?;
let t = self.instantiate_const_expr_as_type(&first.expr, None, tmp_tv_ctx)?;
Ok(ref_mut(t, None))
}
other if simple.args.is_empty() => {
@ -773,32 +779,16 @@ impl Context {
// FIXME: kw args
let mut new_params = vec![];
for (i, arg) in simple.args.pos_args().enumerate() {
match &arg.expr {
ast::ConstExpr::Lit(lit) => {
new_params.push(TyParam::Value(self.eval_lit(lit)?));
let params = self.instantiate_const_expr(&arg.expr, Some((ctx, i)), tmp_tv_ctx);
let params = params.or_else(|e| {
if not_found_is_qvar {
// TODO:
Ok(mono_q_tp(arg.expr.to_string()))
} else {
Err(e)
}
ast::ConstExpr::Accessor(ast::ConstAccessor::Local(name)) => {
if &name.inspect()[..] == "_" {
new_params.push(TyParam::erased(ctx.params[i].1.t.clone()));
} else if let Some((typ, _)) = self.rec_get_type(name.inspect()) {
new_params.push(TyParam::t(typ.clone()));
} else if not_found_is_qvar {
new_params.push(mono_q_tp(name.inspect().clone()));
} else {
return Err(TyCheckErrors::from(TyCheckError::no_var_error(
self.cfg.input.clone(),
line!() as usize,
name.loc(),
self.caused_by(),
name.inspect(),
self.get_similar_name(name.inspect()),
)));
}
}
other => {
todo!("instantiating {other}")
}
}
})?;
new_params.push(params);
}
// FIXME: non-builtin
Ok(poly(Str::rc(other), new_params))
@ -806,15 +796,48 @@ impl Context {
}
}
pub(crate) fn instantiate_const_expr(&self, expr: &ast::ConstExpr) -> TyCheckResult<TyParam> {
pub(crate) fn instantiate_const_expr(
&self,
expr: &ast::ConstExpr,
erased_idx: Option<(&Context, usize)>,
tmp_tv_ctx: Option<&TyVarInstContext>,
) -> TyCheckResult<TyParam> {
match expr {
ast::ConstExpr::Lit(lit) => Ok(TyParam::Value(self.eval_lit(lit)?)),
ast::ConstExpr::Accessor(ast::ConstAccessor::Local(name)) => {
if &name.inspect()[..] == "_" {
Ok(TyParam::erased(Type::Uninited))
} else {
Ok(TyParam::Mono(name.inspect().clone()))
let t = if let Some((ctx, i)) = erased_idx {
ctx.params[i].1.t.clone()
} else {
Type::Uninited
};
return Ok(TyParam::erased(t));
}
if let Some(tmp_tv_ctx) = tmp_tv_ctx {
if let Ok(tp) =
self.instantiate_tp(mono_q_tp(name.inspect()), tmp_tv_ctx, name.loc())
{
return Ok(tp);
}
}
if let Some(tv_ctx) = &self.tv_ctx {
if let Some(t) = tv_ctx.get_qvar(mono_q(name.inspect())) {
return Ok(TyParam::t(t));
} else if let Some(tp) = tv_ctx.get_typaram(name.inspect()) {
return Ok(tp.clone());
}
}
if let Some(value) = self.rec_get_const_obj(name.inspect()) {
return Ok(TyParam::Value(value.clone()));
}
Err(TyCheckErrors::from(TyCheckError::no_var_error(
self.cfg.input.clone(),
line!() as usize,
name.loc(),
self.caused_by(),
name.inspect(),
self.get_similar_name(name.inspect()),
)))
}
_ => todo!(),
}
@ -823,23 +846,13 @@ impl Context {
pub(crate) fn instantiate_const_expr_as_type(
&self,
expr: &ast::ConstExpr,
) -> SingleTyCheckResult<Type> {
match expr {
ast::ConstExpr::Accessor(ast::ConstAccessor::Local(name)) => {
if let Some((typ, _)) = self.rec_get_type(name.inspect()) {
Ok(typ.clone())
} else {
Err(TyCheckError::no_var_error(
self.cfg.input.clone(),
line!() as usize,
name.loc(),
self.caused_by(),
name.inspect(),
self.get_similar_name(name.inspect()),
))
}
}
_ => todo!(),
erased_idx: Option<(&Context, usize)>,
tmp_tv_ctx: Option<&TyVarInstContext>,
) -> TyCheckResult<Type> {
match self.instantiate_const_expr(expr, erased_idx, tmp_tv_ctx)? {
TyParam::Type(t) => Ok(*t),
TyParam::Value(ValueObj::Type(t)) => Ok(t.into_typ()),
other => todo!("{other}"),
}
}
@ -901,13 +914,13 @@ impl Context {
mode,
not_found_is_qvar,
)?;
let mut len = self.instantiate_const_expr(&arr.len)?;
let mut len = self.instantiate_const_expr(&arr.len, None, tmp_tv_ctx)?;
if let TyParam::Erased(t) = &mut len {
*t.as_mut() = Type::Nat;
}
Ok(array_t(elem_t, len))
}
TypeSpec::Set(set) => {
TypeSpec::SetWithLen(set) => {
let elem_t = self.instantiate_typespec(
&set.ty,
opt_decl_t,
@ -915,7 +928,7 @@ impl Context {
mode,
not_found_is_qvar,
)?;
let mut len = self.instantiate_const_expr(&set.len)?;
let mut len = self.instantiate_const_expr(&set.len, None, tmp_tv_ctx)?;
if let TyParam::Erased(t) = &mut len {
*t.as_mut() = Type::Nat;
}
@ -976,13 +989,12 @@ impl Context {
TypeSpec::Enum(set) => {
let mut new_set = set! {};
for arg in set.pos_args() {
if let ast::ConstExpr::Lit(lit) = &arg.expr {
new_set.insert(self.eval_lit(lit)?);
} else {
todo!()
}
new_set.insert(self.instantiate_const_expr(&arg.expr, None, tmp_tv_ctx)?);
}
Ok(v_enum(new_set))
let ty = new_set.iter().fold(Type::Never, |t, tp| {
self.union(&t, &self.get_tp_t(tp).unwrap())
});
Ok(tp_enum(ty, new_set))
}
TypeSpec::Interval { op, lhs, rhs } => {
let op = match op.kind {
@ -992,9 +1004,9 @@ impl Context {
TokenKind::Open => IntervalOp::Open,
_ => assume_unreachable!(),
};
let l = self.instantiate_const_expr(lhs)?;
let l = self.instantiate_const_expr(lhs, None, tmp_tv_ctx)?;
let l = self.eval_tp(&l)?;
let r = self.instantiate_const_expr(rhs)?;
let r = self.instantiate_const_expr(rhs, None, tmp_tv_ctx)?;
let r = self.eval_tp(&r)?;
if let Some(Greater) = self.try_cmp(&l, &r) {
panic!("{l}..{r} is not a valid interval type (should be lhs <= rhs)")
@ -1106,20 +1118,16 @@ impl Context {
match quantified {
TyParam::MonoQVar(n) => {
if let Some(tp) = tmp_tv_ctx.get_typaram(&n) {
Ok(tp.clone())
return Ok(tp.clone());
} else if let Some(t) = tmp_tv_ctx.get_tyvar(&n) {
Ok(TyParam::t(t.clone()))
} else if let Some(tv_ctx) = &self.tv_ctx {
tv_ctx.get_qtp(TyParam::MonoQVar(n.clone())).ok_or_else(|| {
TyCheckErrors::from(TyCheckError::tyvar_not_defined_error(
self.cfg.input.clone(),
line!() as usize,
&n,
loc,
AtomicStr::ever("?"),
))
})
} else if let Some(outer) = &self.outer {
return Ok(TyParam::t(t.clone()));
}
if let Some(tv_ctx) = &self.tv_ctx {
if let Some(tp) = tv_ctx.get_qtp(TyParam::MonoQVar(n.clone())) {
return Ok(tp);
}
}
if let Some(outer) = &self.outer {
outer.instantiate_tp(TyParam::MonoQVar(n), tmp_tv_ctx, loc)
} else {
Err(TyCheckErrors::from(TyCheckError::tyvar_not_defined_error(
@ -1131,6 +1139,38 @@ impl Context {
)))
}
}
TyParam::Dict(dict) => {
let dict = dict
.into_iter()
.map(|(k, v)| {
let k = self.instantiate_tp(k, tmp_tv_ctx, loc)?;
let v = self.instantiate_tp(v, tmp_tv_ctx, loc)?;
Ok((k, v))
})
.collect::<TyCheckResult<_>>()?;
Ok(TyParam::Dict(dict))
}
TyParam::Array(arr) => {
let arr = arr
.into_iter()
.map(|v| self.instantiate_tp(v, tmp_tv_ctx, loc))
.collect::<TyCheckResult<_>>()?;
Ok(TyParam::Array(arr))
}
TyParam::Set(set) => {
let set = set
.into_iter()
.map(|v| self.instantiate_tp(v, tmp_tv_ctx, loc))
.collect::<TyCheckResult<_>>()?;
Ok(TyParam::Set(set))
}
TyParam::Tuple(tup) => {
let tup = tup
.into_iter()
.map(|v| self.instantiate_tp(v, tmp_tv_ctx, loc))
.collect::<TyCheckResult<_>>()?;
Ok(TyParam::Tuple(tup))
}
TyParam::UnaryOp { op, val } => {
let res = self.instantiate_tp(*val, tmp_tv_ctx, loc)?;
Ok(TyParam::unary(op, res))
@ -1179,10 +1219,10 @@ impl Context {
match unbound {
MonoQVar(n) => {
if let Some(t) = tmp_tv_ctx.get_tyvar(&n) {
Ok(t.clone())
return Ok(t.clone());
} else if let Some(tp) = tmp_tv_ctx.get_typaram(&n) {
if let TyParam::Type(t) = tp {
Ok(*t.clone())
return Ok(*t.clone());
} else {
todo!(
"typaram_insts: {}\ntyvar_insts:{}\n{tp}",
@ -1190,25 +1230,19 @@ impl Context {
tmp_tv_ctx.tyvar_instances,
)
}
} else if let Some(tv_ctx) = &self.tv_ctx {
tv_ctx.get_qvar(MonoQVar(n.clone())).ok_or_else(|| {
TyCheckErrors::from(TyCheckError::tyvar_not_defined_error(
self.cfg.input.clone(),
line!() as usize,
&n,
loc,
AtomicStr::ever("?"),
))
})
} else {
Err(TyCheckErrors::from(TyCheckError::tyvar_not_defined_error(
self.cfg.input.clone(),
line!() as usize,
&n,
loc,
AtomicStr::ever("?"),
)))
}
if let Some(tv_ctx) = &self.tv_ctx {
if let Some(t) = tv_ctx.get_qvar(MonoQVar(n.clone())) {
return Ok(t);
}
}
Err(TyCheckErrors::from(TyCheckError::tyvar_not_defined_error(
self.cfg.input.clone(),
line!() as usize,
&n,
loc,
AtomicStr::ever("?"),
)))
}
PolyQVar { name, mut params } => {
for param in params.iter_mut() {

View file

@ -181,11 +181,10 @@ impl Context {
}
self.validate_var_sig_t(ident, sig.t_spec.as_ref(), body_t, Normal)?;
let muty = Mutability::from(&ident.inspect()[..]);
let generalized = self.generalize_t(body_t.clone());
self.decls.remove(ident.inspect());
let vis = ident.vis();
let vi = VarInfo::new(
generalized,
body_t.clone(),
muty,
vis,
VarKind::Defined(id),

View file

@ -68,6 +68,7 @@ impl Context {
}
_ => assume_unreachable!(),
},
TyParam::FreeVar(_) => free,
other if other.has_no_unbound_var() => other,
other => todo!("{other}"),
}
@ -241,6 +242,15 @@ impl Context {
after,
)
}
Refinement(refine) => {
let t = self.generalize_t_inner(*refine.t, variance, bounds, lazy_inits);
let preds = refine
.preds
.into_iter()
.map(|pred| self.generalize_pred(pred, variance, bounds, lazy_inits))
.collect();
refinement(refine.var, t, preds)
}
Poly { name, mut params } => {
let params = params
.iter_mut()
@ -314,6 +324,35 @@ impl Context {
}
}
fn generalize_pred(
&self,
pred: Predicate,
variance: Variance,
bounds: &mut Set<TyBound>,
lazy_inits: &mut Set<Str>,
) -> Predicate {
match pred {
Predicate::Const(_) => pred,
Predicate::Equal { lhs, rhs } => {
let rhs = self.generalize_tp(rhs, variance, bounds, lazy_inits);
Predicate::eq(lhs, rhs)
}
Predicate::GreaterEqual { lhs, rhs } => {
let rhs = self.generalize_tp(rhs, variance, bounds, lazy_inits);
Predicate::ge(lhs, rhs)
}
Predicate::LessEqual { lhs, rhs } => {
let rhs = self.generalize_tp(rhs, variance, bounds, lazy_inits);
Predicate::le(lhs, rhs)
}
Predicate::NotEqual { lhs, rhs } => {
let rhs = self.generalize_tp(rhs, variance, bounds, lazy_inits);
Predicate::ne(lhs, rhs)
}
other => todo!("{other}"),
}
}
pub(crate) fn deref_tp(
&self,
tp: TyParam,

View file

@ -1 +1,3 @@
.__import__: |S: Str|(name: {S}, globals := {Str: Obj}) -> Module S
.import_module: |S: Str|(name: {S}, package := Str or NoneType) -> Module S
.reload!: (GenericModule, ) => NoneType

View file

@ -21,7 +21,7 @@ use erg_parser::Parser;
use crate::ty::constructors::{
array_mut, array_t, free_var, func, mono, poly, proc, quant, set_mut, set_t, ty_tp,
};
use crate::ty::free::Constraint;
use crate::ty::free::{Constraint, HasLevel};
use crate::ty::typaram::TyParam;
use crate::ty::value::{GenTypeObj, TypeKind, TypeObj, ValueObj};
use crate::ty::{HasType, ParamTy, Type};
@ -1595,6 +1595,8 @@ impl ASTLowerer {
RegistrationMode::Normal,
false,
)?;
t.lift();
let t = self.ctx.generalize_t(t);
if is_instance_ascription {
self.declare_instance(&ident, &t, py_name)?;
} else {

View file

@ -394,6 +394,9 @@ impl<T> Free<T> {
pub fn as_ptr(&self) -> *mut FreeKind<T> {
self.0.as_ptr()
}
pub fn forced_as_ref(&self) -> &FreeKind<T> {
unsafe { self.as_ptr().as_ref() }.unwrap()
}
pub fn force_replace(&self, new: FreeKind<T>) {
// prevent linking to self
if addr_eq!(*self.borrow(), new) {

View file

@ -482,6 +482,22 @@ impl TryFrom<TyParam> for Type {
match tp {
TyParam::FreeVar(fv) if fv.is_linked() => Type::try_from(fv.crack().clone()),
TyParam::Type(t) => Ok(t.as_ref().clone()),
TyParam::Value(v) => Type::try_from(v),
// TODO: Array, Dict, Set
_ => Err(()),
}
}
}
impl<'a> TryFrom<&'a TyParam> for &'a Type {
type Error = ();
fn try_from(tp: &'a TyParam) -> Result<&'a Type, ()> {
match tp {
TyParam::FreeVar(fv) if fv.is_linked() => {
<&'a Type>::try_from(fv.forced_as_ref().linked().unwrap())
}
TyParam::Type(t) => Ok(t.as_ref()),
TyParam::Value(v) => <&Type>::try_from(v),
// TODO: Array, Dict, Set
_ => Err(()),
}

View file

@ -374,6 +374,33 @@ impl TryFrom<&ValueObj> for f64 {
}
}
impl TryFrom<ValueObj> for Type {
type Error = ();
fn try_from(val: ValueObj) -> Result<Type, ()> {
match val {
ValueObj::Type(t) => match t {
TypeObj::Builtin(t) => Ok(t),
TypeObj::Generated(gen) => Ok(gen.t),
},
ValueObj::Mut(v) => Type::try_from(v.borrow().clone()).map_err(|_| ()),
_ => Err(()),
}
}
}
impl<'a> TryFrom<&'a ValueObj> for &'a Type {
type Error = ();
fn try_from(val: &'a ValueObj) -> Result<Self, ()> {
match val {
ValueObj::Type(t) => match t {
TypeObj::Builtin(t) => Ok(t),
TypeObj::Generated(gen) => Ok(&gen.t),
},
_ => Err(()),
}
}
}
impl HasType for ValueObj {
fn ref_t(&self) -> &Type {
panic!("cannot get reference of the const")