diff --git a/src/ast/descriptor.rs b/src/ast/descriptor.rs index 5552fe5..509f370 100644 --- a/src/ast/descriptor.rs +++ b/src/ast/descriptor.rs @@ -77,12 +77,45 @@ impl DescriptorType { properties, } } + + /// Returns the top-level wildcard descriptor: (*,*). + /// Matches any label and allows any properties. + pub fn star() -> Self { + DescriptorType { + label: LabelType::Star, + properties: PropertyType::open(), + } + } + + /// Computes the greatest lower bound (meet) of two descriptors. + /// This merges both label and property constraints. + pub fn meet(a: &DescriptorType, b: &DescriptorType) -> DescriptorType { + DescriptorType { + label: LabelType::meet(a.label.clone(), b.label.clone()), + properties: PropertyType::meet(&a.properties, &b.properties), + } + } + + /// Returns true if descriptor t1 is a subtype of descriptor t2. + /// This requires both label and property subtyping to hold. + pub fn is_subtype(t1: &DescriptorType, t2: &DescriptorType) -> bool { + LabelType::is_subtype(&t1.label, &t2.label) + && PropertyType::is_subtype(&t1.properties, &t2.properties) + } + + /// Returns true if the descriptor is unsatisfiable (i.e., some inconsistency). + /// A descriptor is empty if its property type is empty. + pub fn is_empty(t: &DescriptorType) -> bool { + PropertyType::is_empty(&t.properties) + } } #[derive(PartialEq, Clone, Debug)] pub enum PropertyType { Open(HashMap), Closed(HashMap), + #[doc(hidden)] + Zero, } impl PropertyType { @@ -93,6 +126,155 @@ impl PropertyType { pub fn closed() -> Self { PropertyType::Closed(HashMap::new()) } + + /// Returns the set of keys in this property type. + pub fn keys(&self) -> std::collections::HashSet<&String> { + match self { + PropertyType::Open(m) | PropertyType::Closed(m) => m.keys().collect(), + PropertyType::Zero => std::collections::HashSet::new(), + } + } + + /// Gets the type associated with a key. + /// Returns Star for missing keys in Open types, Zero for missing keys in Closed types. + pub fn get(&self, key: &str) -> SimpleType { + match self { + PropertyType::Open(m) => m.get(key).cloned().unwrap_or(SimpleType::Star), + PropertyType::Closed(m) => m.get(key).cloned().unwrap_or(SimpleType::Zero), + PropertyType::Zero => SimpleType::Zero, + } + } + + /// Adds or overrides an attribute with the given type. + pub fn extend(&mut self, key: String, t: SimpleType) { + match self { + PropertyType::Open(m) | PropertyType::Closed(m) => { + m.insert(key, t); + } + PropertyType::Zero => {} + } + } + + /// Computes the meet (greatest lower bound) of two property types. + /// + /// The result is: + /// - Closed only if both are Closed and have the same keys. + /// - Open if both are Open. + /// - Closed if one is Open and the other Closed, but their keys are compatible. + /// - Zero otherwise. + pub fn meet(a: &PropertyType, b: &PropertyType) -> PropertyType { + match (a, b) { + // Case 1: Both closed with identical keys + (PropertyType::Closed(_), PropertyType::Closed(_)) if a.keys() == b.keys() => { + let mut c = PropertyType::closed(); + for k in a.keys() { + c.extend(k.clone(), SimpleType::meet(&a.get(k), &b.get(k))); + } + c + } + + // Case 2: Both open — union of keys + (PropertyType::Open(_), PropertyType::Open(_)) => { + let mut c = PropertyType::open(); + let all_keys: std::collections::HashSet<_> = + a.keys().union(&b.keys()).cloned().collect(); + for k in all_keys { + let t = if a.keys().contains(k) && b.keys().contains(k) { + SimpleType::meet(&a.get(k), &b.get(k)) + } else if a.keys().contains(k) { + a.get(k) + } else { + b.get(k) + }; + c.extend(k.clone(), t); + } + c + } + + // Case 3: Open ⊓ Closed, where open keys ⊆ closed keys + (PropertyType::Open(_), PropertyType::Closed(_)) if a.keys().is_subset(&b.keys()) => { + let mut c = PropertyType::closed(); + for k in b.keys() { + let t = if a.keys().contains(&k) { + SimpleType::meet(&a.get(k), &b.get(k)) + } else { + b.get(k) + }; + c.extend(k.clone(), t); + } + c + } + + // Case 4: Closed ⊓ Open, symmetric + (PropertyType::Closed(_), PropertyType::Open(_)) if b.keys().is_subset(&a.keys()) => { + let mut c = PropertyType::closed(); + for k in a.keys() { + let t = if b.keys().contains(&k) { + SimpleType::meet(&a.get(k), &b.get(k)) + } else { + a.get(k) + }; + c.extend(k.clone(), t); + } + c + } + + // All other cases (incompatible or involving Zero) + _ => PropertyType::Zero, + } + } + + /// Returns true if t1 is a subtype of t2. + /// Open types allow extra keys; closed types must match exactly. + pub fn is_subtype(t1: &PropertyType, t2: &PropertyType) -> bool { + match (t1, t2) { + (PropertyType::Open(_), PropertyType::Open(_)) => { + // Check common keys + t1.keys() + .intersection(&t2.keys()) + .all(|k| SimpleType::is_subtype(&t1.get(k), &t2.get(k))) + } + + (PropertyType::Closed(_), PropertyType::Closed(_)) => { + // Must have same keys + t1.keys() == t2.keys() + && t2 + .keys() + .iter() + .all(|k| SimpleType::is_subtype(&t1.get(k), &t2.get(k))) + } + + (PropertyType::Closed(_), PropertyType::Open(_)) => { + // Open keys must be subset of closed keys + t2.keys().is_subset(&t1.keys()) + && t2 + .keys() + .iter() + .all(|k| SimpleType::is_subtype(&t1.get(k), &t2.get(k))) + } + + (PropertyType::Open(_), PropertyType::Closed(_)) => { + // Open keys must be subset of closed keys + t1.keys().is_subset(&t2.keys()) + && t1 + .keys() + .iter() + .all(|k| SimpleType::is_subtype(&t1.get(k), &t2.get(k))) + } + + _ => false, + } + } + + /// Returns true if any attribute in the property type is statically empty (⊥). + pub fn is_empty(t: &PropertyType) -> bool { + match t { + PropertyType::Open(_) | PropertyType::Closed(_) => { + !t.keys().is_empty() && t.keys().iter().any(|k| SimpleType::is_empty(&t.get(k))) + } + PropertyType::Zero => true, + } + } } impl Default for PropertyType { diff --git a/src/ast/label.rs b/src/ast/label.rs index 27f403a..a319d55 100644 --- a/src/ast/label.rs +++ b/src/ast/label.rs @@ -15,4 +15,45 @@ impl LabelType { pub fn or(l1: LabelType, l2: LabelType) -> Self { LabelType::Or(Box::new(l1), Box::new(l2)) } + + /// Constructs a conjunction (AND) of labels from a list of strings. + /// E.g., ["A", "B", "C"] → A & B & C + pub fn from_list(labels: &[String]) -> Self { + match labels { + [] => LabelType::Star, + [single] => LabelType::Label(single.clone()), + [first, rest @ ..] => { + LabelType::and(LabelType::Label(first.clone()), LabelType::from_list(rest)) + } + } + } + + /// Computes the meet (greatest lower bound) of two label types under logical entailment. + pub fn meet(a: LabelType, b: LabelType) -> LabelType { + match (&a, &b) { + (LabelType::Star, _) => b, + (_, LabelType::Star) => a, + _ if LabelType::is_subtype(&a, &b) => a, + _ if LabelType::is_subtype(&b, &a) => b, + _ => LabelType::and(a, b), + } + } + + /// Determines whether label type `l1` is a subtype of `l2`. + pub fn is_subtype(l1: &LabelType, l2: &LabelType) -> bool { + match (l1, l2) { + (LabelType::Star, _) | (_, LabelType::Star) => true, + (LabelType::Label(a), LabelType::Label(b)) => a == b, + (_, LabelType::And(left, right)) => { + LabelType::is_subtype(l1, left) && LabelType::is_subtype(l1, right) + } + (LabelType::And(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, + } + } } diff --git a/src/ast/types.rs b/src/ast/types.rs index 6a4b20b..2147cc8 100644 --- a/src/ast/types.rs +++ b/src/ast/types.rs @@ -1,10 +1,89 @@ -#[derive(PartialEq, Clone, Debug)] +#[derive(PartialEq, Clone, Debug, Eq)] pub enum SimpleType { Base(BaseType), Star, + Union(Box, Box), + List(Box), + #[doc(hidden)] + Zero, } -#[derive(PartialEq, Clone, Debug)] +impl SimpleType { + /// Computes the least upper bound (gradual union) of two types. + /// Special case: union with ⊥ yields the other type. + pub fn union(t1: &SimpleType, t2: &SimpleType) -> SimpleType { + match (t1, t2) { + (SimpleType::Zero, _) => t2.clone(), + (_, SimpleType::Zero) => t1.clone(), + _ if t1 == t2 => t1.clone(), + _ => SimpleType::Union(Box::new(t1.clone()), Box::new(t2.clone())), + } + } + + /// Computes the greatest lower bound of two types. + /// Used to detect inconsistencies across disjoint branches or filters. + pub fn meet(a: &SimpleType, b: &SimpleType) -> SimpleType { + match (a, b) { + (SimpleType::Star, _) => b.clone(), + (_, SimpleType::Star) => a.clone(), + (SimpleType::Union(t1, t2), _) => { + let meet1 = SimpleType::meet(t1, b); + let meet2 = SimpleType::meet(t2, b); + SimpleType::union(&meet1, &meet2) + } + (_, SimpleType::Union(t1, t2)) => { + let meet1 = SimpleType::meet(a, t1); + let meet2 = SimpleType::meet(a, t2); + SimpleType::union(&meet1, &meet2) + } + _ if SimpleType::gradual_eq(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::Union(t1a, t1b), _) => { + SimpleType::is_subtype(t1a, t2) && SimpleType::is_subtype(t1b, t2) + } + (_, SimpleType::Union(t2a, t2b)) => { + SimpleType::is_subtype(t1, t2a) || SimpleType::is_subtype(t1, t2b) + } + _ => t1 == t2, + } + } + + /// Checks whether the type is empty (⊥) or composed only of empty subtypes. + pub fn is_empty(t: &SimpleType) -> bool { + match t { + SimpleType::Zero => true, + SimpleType::Union(t1, t2) => SimpleType::is_empty(t1) && SimpleType::is_empty(t2), + SimpleType::List(inner) => SimpleType::is_empty(inner), + _ => false, + } + } +} + +#[derive(PartialEq, Clone, Debug, Eq)] pub enum BaseType { Int, Bool,