feat: support refinement class

This commit is contained in:
Shunsuke Shibayama 2023-10-31 02:23:50 +09:00
parent c72de02c2c
commit 678c02faf9
9 changed files with 94 additions and 4 deletions

View file

@ -133,6 +133,28 @@ pub fn singleton(ty: Type, tp: TyParam) -> Type {
#[inline]
pub fn int_interval<P, PErr, Q, QErr>(op: IntervalOp, l: P, r: Q) -> Type
where
P: TryInto<TyParam, Error = PErr>,
PErr: fmt::Debug,
Q: TryInto<TyParam, Error = QErr>,
QErr: fmt::Debug,
{
interval(op, Type::Int, l, r)
}
#[inline]
pub fn closed_range<P, PErr, Q, QErr>(t: Type, l: P, r: Q) -> Type
where
P: TryInto<TyParam, Error = PErr>,
PErr: fmt::Debug,
Q: TryInto<TyParam, Error = QErr>,
QErr: fmt::Debug,
{
interval(IntervalOp::Closed, t, l, r)
}
#[inline]
pub fn interval<P, PErr, Q, QErr>(op: IntervalOp, t: Type, l: P, r: Q) -> Type
where
P: TryInto<TyParam, Error = PErr>,
PErr: fmt::Debug,
@ -161,7 +183,7 @@ where
Predicate::le(name.clone(), r),
),
IntervalOp::Open if l == TyParam::value(NegInf) && r == TyParam::value(Inf) => {
return refinement(name, Type::Int, Predicate::TRUE)
return refinement(name, t, Predicate::TRUE)
}
// l<..<r => {I: classof(l) | I >= l+ε and I <= r-ε}
IntervalOp::Open => Predicate::and(
@ -169,7 +191,7 @@ where
Predicate::le(name.clone(), TyParam::pred(r)),
),
};
refinement(name, Type::Int, pred)
refinement(name, t, pred)
}
pub fn iter(t: Type) -> Type {

View file

@ -49,6 +49,10 @@ pub enum OpKind {
BitXor,
Shl,
Shr,
ClosedRange,
LeftOpenRange,
RightOpenRange,
OpenRange,
}
impl fmt::Display for OpKind {
@ -79,6 +83,10 @@ impl fmt::Display for OpKind {
Self::BitXor => write!(f, "^^"),
Self::Shl => write!(f, "<<"),
Self::Shr => write!(f, ">>"),
Self::ClosedRange => write!(f, ".."),
Self::LeftOpenRange => write!(f, "<.."),
Self::RightOpenRange => write!(f, "..<"),
Self::OpenRange => write!(f, "<..<"),
}
}
}
@ -109,6 +117,10 @@ impl TryFrom<TokenKind> for OpKind {
TokenKind::BitXor => Ok(Self::BitXor),
TokenKind::Shl => Ok(Self::Shl),
TokenKind::Shr => Ok(Self::Shr),
TokenKind::Closed => Ok(Self::ClosedRange),
TokenKind::LeftOpen => Ok(Self::LeftOpenRange),
TokenKind::RightOpen => Ok(Self::RightOpenRange),
TokenKind::Open => Ok(Self::OpenRange),
_ => Err(()),
}
}

View file

@ -955,6 +955,7 @@ impl ValueObj {
ValueObj::Type(TypeObj::Generated(gen))
}
/// closed range (..)
pub fn range(start: Self, end: Self) -> Self {
Self::DataClass {
name: "Range".into(),