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
182 changes: 182 additions & 0 deletions src/ast/descriptor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<String, SimpleType>),
Closed(HashMap<String, SimpleType>),
#[doc(hidden)]
Zero,
}

impl PropertyType {
Expand All @@ -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 {
Expand Down
41 changes: 41 additions & 0 deletions src/ast/label.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
}
}
83 changes: 81 additions & 2 deletions src/ast/types.rs
Original file line number Diff line number Diff line change
@@ -1,10 +1,89 @@
#[derive(PartialEq, Clone, Debug)]
#[derive(PartialEq, Clone, Debug, Eq)]
pub enum SimpleType {
Base(BaseType),
Star,
Union(Box<SimpleType>, Box<SimpleType>),
List(Box<SimpleType>),
#[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,
Expand Down
Loading