1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

use crate::type_checker::{AbstractType, TypeCheckKey};
use crate::Generalizable;
use ena::unify::UnifyKey;

/// Represents a constraint on one or several abstract types referred to by `TypeCheckKey`s.
/// Rather than creating these constraints directly, `TypeCheckKey` provides several convenient functions for this
/// purpose.
#[must_use = "the creation of a `TypeConstraint` has no effect, it should be passed to a `TypeChecker`"]
pub enum TypeConstraint<Key: UnifyKey>
where
    Key::Value: AbstractType,
{
    /// Represents the restriction that `target` is more concrete than the meet of all abstract types belonging to the
    /// keys in `args`.
    MoreConcreteThanAll { target: TypeCheckKey<Key>, args: Vec<TypeCheckKey<Key>> },
    /// Represents the restriction that `target` is more concrete than the meet of all abstract types in `args`.
    MoreConcreteThanType { target: TypeCheckKey<Key>, args: Vec<Key::Value> },
}

impl<Key: UnifyKey> TypeCheckKey<Key>
where
    Key::Value: AbstractType,
{
    /// States that the left operand needs to be at least as concrete as the right one.
    /// Imposing these constraints lets the abstract type of `self` become the meet of the current
    /// abstract type of `self` and `other`.
    pub fn more_concrete_than(self, other: Self) -> TypeConstraint<Key> {
        TypeConstraint::MoreConcreteThanAll { target: self, args: vec![other] }
    }

    /// States that `target` needs to be more concrete than all `args` combined.
    /// Imposing this constraint computes the meet of all args and enforces that `self` is more
    /// concrete than the result.
    pub fn is_the_meet_of(self, args: &[Self]) -> TypeConstraint<Key> {
        TypeConstraint::MoreConcreteThanAll { target: self, args: args.to_vec() }
    }

    /// Bounds `self` by `other` where `other` is an abstract type.
    pub fn bound_by_abstract(self, other: Key::Value) -> TypeConstraint<Key> {
        TypeConstraint::MoreConcreteThanType { target: self, args: vec![other] }
    }
}

impl<Key: UnifyKey> TypeCheckKey<Key>
where
    Key::Value: AbstractType,
{
    /// Bounds `self` by the generalization of the concrete type `conc`.
    pub fn bound_by_concrete<CT>(&self, conc: CT) -> TypeConstraint<Key>
    where
        CT: Generalizable<Generalized = Key::Value>,
    {
        self.bound_by_abstract(conc.generalize())
    }
}