feat: support and/or guard type

This commit is contained in:
Shunsuke Shibayama 2023-10-31 13:47:42 +09:00
parent a6336fa896
commit 641a60bda6
5 changed files with 116 additions and 38 deletions

View file

@ -1211,6 +1211,14 @@ impl Context {
Record(union)
}
}
(Guard(l), Guard(r)) => {
if l.namespace == r.namespace && l.target == r.target {
let to = self.union(&l.to, &r.to);
Guard(GuardType::new(l.namespace.clone(), l.target.clone(), to))
} else {
or(lhs.clone(), rhs.clone())
}
}
(Structural(l), Structural(r)) => self.union(l, r).structuralize(),
// Int..Obj or Nat..Obj ==> Int..Obj
// Str..Obj or Int..Obj ==> Str..Obj or Int..Obj
@ -1384,7 +1392,14 @@ impl Context {
.unwrap_or_else(Type::Refinement)
}
(Structural(l), Structural(r)) => self.intersection(l, r).structuralize(),
(Guard(_), Guard(_)) => and(lhs.clone(), rhs.clone()),
(Guard(l), Guard(r)) => {
if l.namespace == r.namespace && l.target == r.target {
let to = self.intersection(&l.to, &r.to);
Guard(GuardType::new(l.namespace.clone(), l.target.clone(), to))
} else {
and(lhs.clone(), rhs.clone())
}
}
// {.i = Int} and {.s = Str} == {.i = Int; .s = Str}
(Record(l), Record(r)) => Type::Record(l.clone().concat(r.clone())),
// {i = Int; j = Int} and not {i = Int} == {j = Int}

View file

@ -1768,4 +1768,11 @@ impl Context {
.ok()
.and_then(|tp| ValueObj::try_from(tp).ok())
}
pub(crate) fn expr_to_tp(&self, expr: ast::Expr) -> Option<TyParam> {
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()
}
}