Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/ast/descriptor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,6 +228,7 @@ impl PropertyType {
/// Open types allow extra keys; closed types must match exactly.
pub fn is_subtype(t1: &PropertyType, t2: &PropertyType) -> bool {
match (t1, t2) {
(PropertyType::Zero, _) => true,
(PropertyType::Open(_), PropertyType::Open(_)) => {
// Check common keys
t1.keys()
Expand Down
4 changes: 3 additions & 1 deletion src/ast/label.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,10 +50,12 @@ impl LabelType {
(LabelType::And(left, right), _) => {
LabelType::is_subtype(left, l2) || LabelType::is_subtype(right, l2)
}
(LabelType::Or(left, right), _) => {
LabelType::is_subtype(left, l2) && LabelType::is_subtype(right, l2)
}
(_, LabelType::Or(left, right)) => {
LabelType::is_subtype(l1, left) || LabelType::is_subtype(l1, right)
}
_ => false,
}
}
}
21 changes: 3 additions & 18 deletions src/ast/types.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,34 +36,19 @@ impl SimpleType {
let meet2 = SimpleType::meet(a, t2);
SimpleType::union(&meet1, &meet2)
}
_ if SimpleType::gradual_eq(a, b) => a.clone(),
_ if a == b => a.clone(),
_ => SimpleType::Zero, // Incompatible types
}
}

/// Returns true if t1 and t2 are considered equal under the gradual type system.
/// StarType is treated as equal to anything.
pub fn gradual_eq(t1: &SimpleType, t2: &SimpleType) -> bool {
match (t1, t2) {
(SimpleType::Star, _) | (_, SimpleType::Star) => true,
(SimpleType::Union(t1a, t1b), _) => {
SimpleType::gradual_eq(t1a, t2) || SimpleType::gradual_eq(t1b, t2)
}
(_, SimpleType::Union(t2a, t2b)) => {
SimpleType::gradual_eq(t1, t2a) || SimpleType::gradual_eq(t1, t2b)
}
_ => t1 == t2,
}
}

/// Returns true if t1 is a (gradual) subtype of t2.
/// Used in type tests and type refinements.
pub fn is_subtype(t1: &SimpleType, t2: &SimpleType) -> bool {
match (t1, t2) {
(SimpleType::Star, _) | (_, SimpleType::Star) => true,
(_, SimpleType::Zero) => true,
(SimpleType::Zero, _) => true,
(SimpleType::Union(t1a, t1b), _) => {
SimpleType::is_subtype(t1a, t2) && SimpleType::is_subtype(t1b, t2)
SimpleType::is_subtype(t1a, t2) || SimpleType::is_subtype(t1b, t2)
}
(_, SimpleType::Union(t2a, t2b)) => {
SimpleType::is_subtype(t1, t2a) || SimpleType::is_subtype(t1, t2b)
Expand Down
6 changes: 3 additions & 3 deletions src/typechecker/checker.rs
Original file line number Diff line number Diff line change
Expand Up @@ -243,8 +243,8 @@ impl Typechecker {

match Self::binop_delta(op) {
Some((expected_t1, expected_t2, result_t)) => {
if SimpleType::gradual_eq(&t1, &expected_t1)
&& SimpleType::gradual_eq(&t2, &expected_t2)
if SimpleType::meet(&t1, &expected_t1) != SimpleType::Zero
&& SimpleType::meet(&t2, &expected_t2) != SimpleType::Zero
{
result_t
} else {
Expand All @@ -270,7 +270,7 @@ impl Typechecker {

match Self::unop_delta(op) {
Some((expected_t, result_t)) => {
if SimpleType::gradual_eq(&t, &expected_t) {
if SimpleType::meet(&t, &expected_t) != SimpleType::Zero {
result_t
} else {
self.warnings
Expand Down
5 changes: 3 additions & 2 deletions src/typechecker/variable_type.rs
Original file line number Diff line number Diff line change
Expand Up @@ -216,6 +216,7 @@ impl VariableType {
/// General meet operator (greatest lower bound).
pub fn meet(a: &VariableType, b: &VariableType) -> Result<VariableType, String> {
match (a, b) {
(VariableType::Zero, _) | (_, VariableType::Zero) => Ok(VariableType::Zero),
(VariableType::List(inner_a), VariableType::List(inner_b)) => Ok(VariableType::List(
Box::new(VariableType::meet(inner_a, inner_b)?),
)),
Expand All @@ -227,14 +228,13 @@ impl VariableType {
let r1 = VariableType::meet(t1, b);
let r2 = VariableType::meet(t2, b);
match (r1, r2) {
(Ok(v1), Ok(v2)) => Ok(VariableType::Union(Box::new(v1), Box::new(v2))),
(Ok(v1), Ok(v2)) => Ok(VariableType::join(v1, v2)),
(Ok(v1), Err(_)) => Ok(v1),
(Err(_), Ok(v2)) => Ok(v2),
(Err(e1), Err(_)) => Err(e1),
}
}
(_, VariableType::Union(_, _)) => VariableType::meet(b, a),
(VariableType::Zero, _) | (_, VariableType::Zero) => Ok(VariableType::Zero),
_ => Err(format!(
"Meet undefined between variable types {:?} and {:?}",
a, b
Expand Down Expand Up @@ -263,6 +263,7 @@ impl VariableType {
/// Checks if t1 is a subtype of t2.
pub fn is_subtype(t1: &VariableType, t2: &VariableType) -> bool {
match (t1, t2) {
(VariableType::Zero, _) => true,
(VariableType::Node(n1), VariableType::Node(n2)) => {
DescriptorType::is_subtype(&n1.0, &n2.0)
}
Expand Down
Loading