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
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
//! This mod contains everything related to types and collections of types (type tables).
//!
//! # Content
//! * [`Abstract`](trait.Abstract.html) is a trait representing abstract types that will
//! be inferred during the type checking procedure.
//! * Reification is the process of transforming an abstract type into a concrete one.  
//! This process can be fallible or infallible, represented by [`Reifiable`](trait.Reifiable.html),
//! [`TryReifiable`](trait.TryReifiable.html), and [`ReificationErr`](enum.ReificationErr.html).
//! * Generalization is the infallible process of transforming a concrete type into an abstract one represented by [`Generalizable`](trait.Generalizable.html)
//! * [`TypeTable`](trait.TypeTable.html) contains a mapping from a [`TcKey`](../struct.TcKey.html) to an [`Abstract`](trait.Abstract.html) or reified type.

use crate::TcKey;
use std::collections::HashMap;
use std::{fmt::Debug, ops::Index};

/// An abstract type that will be inferred during the type checking procedure.
///
/// This trait that needs to be implemented by all (rust-) types that represent a type in the type checking procedure.
///
/// # Requirements
/// The abstract types need to follow a [lattice structure](https://en.wikipedia.org/wiki/Lattice_(order)) where the top element is the least constrained, most abstract type
/// possible.  
/// ## Refinement
/// This value needs to be provided by the `Abstract::unconstrained` function.  Types will be refined
/// successively using the fallible meet function.  If the types are incompatible, i.e., would result in a contradictory
/// type, the meet needs to return a `Result::Err`.  Otherwise, it returns a `Result::Ok` containing the resulting type.
/// The function needs to follow the rules for abstract meets.  Intuitively, these are:
/// * The result of a meet needs to be more or equally concrete than either argument.  
/// * Meeting two types returns the greatest upper bound, i.e., the type that is more or equally concrete to either argument _and_ there is no other, less concrete type meeting this requirement.
/// This especially entails that meeting any type `T` with an unconstrained type returns `T`.
///
/// ## Arity
/// Type can be recursive, i.e., they have a number of subtypes, their "children".
/// An integer, for example, has no children and is thus 0-ary.  An optional type on the other hand is 1-ary, i.e., it has one sub-type.
/// During the inference process, the arity might be undetermined:  the unconstrained type will resolve to something with an arity, but the value is not clear, yet.
///
/// The type checking procedure keeps track of types and their potential children.  
/// For this, it requires some guarantees when it comes to the arity:
///
/// ### Arity Stability
/// * If a type has a defined arity, it may not change when turning more concrete.  Thus, abstract types with ambiguous arity must not return an arity.
/// * A leaf type, i.e., a fully resolved non-contradictory type must provide an arity.
/// A consequence is that the meet of two types with different, defined arity will result in an error.
///
/// # Example
/// For a full example of an abstract type system, refer to the [crate documentation](../index.html) and the examples. TODO: link!
///
pub trait Abstract: Eq + Sized + Clone + Debug {
    /// Result of a meet of two incompatible type, i.e., it represents a type contradiction.
    /// May contain information regarding why the meet failed.  
    type Err: Debug;

    /// Returns the unconstrained, most abstract type.
    fn unconstrained() -> Self;

    /// Determines whether or not `self` is the unconstrained type.
    fn is_unconstrained(&self) -> bool {
        self == &Self::unconstrained()
    }

    /// Attempts to meet two abstract types.
    /// Refer to the documentation of [Abstract](trait.Abstract.html) for the responsibilities of this function.
    fn meet(&self, other: &Self) -> Result<Self, Self::Err>;

    /// Provides the arity of the `self` if the type is sufficiently resolved to determine it.
    fn arity(&self) -> Option<usize>;

    /// Provide access to the nth child.
    /// # Guarantee
    /// The arity of `self` is defined and greater or equal to `n`: `assert!(self.arity.map(|a| *a >= n).unwrap_or(false)`
    fn nth_child(&self, n: usize) -> &Self;

    /// Generate an instance of Self that is equivalent to `self` except that the children of the newly generated type will be
    /// `children`.
    /// # Guarantee
    /// The arity of `self` is defined and corresponds to the number of element in `children`: assert!(self.arity.map(|a| a == children.collect::<Vec<Self>>().len()).unwrap_or(false))`
    fn with_children<I>(&self, children: I) -> Self
    where
        I: IntoIterator<Item = Self>;
}

/// Indicates that an abstract type could not be reified because it is too general or too restrictive.
///
/// # Example
/// 1. A numeric type cannot be reified into any concrete value because the concrete counterpart could be a natural
/// number, integer, floating point number, .... -> `ReificationErr::TooGeneral`
/// 2. An integer type cannot be reified into a concrete type with fixed memory layout except a default size is
/// defined, e.g. an Int will be reified into an Int32. -> `ReificationErr::TooGeneral`
/// 3. An unbounded integer might not have a concrete counterpart because the system requires a concrete bit size.
/// -> `ReificationErr::Conflicting`
///
/// Note the subtle difference between `ReificationErr::TooGeneral` and `ReificationErr::Conflicting`:
///     + In the `Conflicting` case there is no concrete counterpart
///     + In the `TooGeneral` case the concrete counterpart is not defined or not unique but could exist.
#[derive(Debug, Clone)]
pub enum ReificationErr {
    /// Attempting to reify an abstract type with either no unique concrete counterpart or with no defined default
    /// reification value results in this error.
    TooGeneral(String),
    /// Attempting to reify an abstract type for which no concrete counterpart does exist results in this error.
    Conflicting(String),
}

/// A type implementing this trait can be `reified` into a concrete representation.
/// This transformation cannot fail.  If it is fallible, refer to [`TryReifiable`](trait.TryReifiable.html).
pub trait Reifiable {
    /// The result type of the reification.
    type Reified;
    /// Transforms `self` into the more concrete `Self::Reified` type.
    fn reify(&self) -> Self::Reified;
}

/// A type implementing this trait can potentially be `reified` into a concrete representation.
/// This transformation can fail.  If it is infallible, refer to [`Reifiable`](trait.Reifiable.html).
pub trait TryReifiable {
    /// The result type of the attempted reification.
    type Reified;
    /// Attempts to transform `self` into an more concrete `Self::Reified` type.  
    /// Returns a [`ReificationErr`](enum.ReificationErr.html) if the transformation fails.
    fn try_reify(&self) -> Result<Self::Reified, ReificationErr>;
}

/// A type implementing this trait can be `generalized` into an abstract representation infallibly.
pub trait Generalizable {
    /// The result type of the generalization.
    type Generalized;
    /// Generalizes the given concrete type.
    fn generalize(&self) -> Self::Generalized;
}

/// A trait representing a type table.
///
/// It maps [`TcKey`](../struct.TcKey.html) to `Self::Type` and allows for an automatic transformation into a hashmap.
pub trait TypeTable: Index<TcKey> {
    /// The (rust-) type of the (external-) type stored in this type table.
    type Type;

    /// Transforms itself into a hashmap.
    fn as_hashmap(self) -> HashMap<TcKey, Self::Type>;
}

/// An implementation of [`TypeTable`](trait.TypeTable.html) for type implementing [`Abstract`](trait.Abstract.html).
/// See [`ReifiedTypeTable`](struct.ReifiedTypeTable.html) for an implementation specializing on
/// concrete types.
///
/// Can automatically be generated from a `HashMap<TcKey, AbsTy>` for `AbsTy: Abstract`.
#[derive(Debug, Clone)]
pub struct AbstractTypeTable<AbsTy: Abstract> {
    table: HashMap<TcKey, AbsTy>,
}

impl<AbsTy: Abstract> Index<TcKey> for AbstractTypeTable<AbsTy> {
    type Output = AbsTy;
    fn index(&self, index: TcKey) -> &Self::Output {
        &self.table[&index]
    }
}

impl<AbsTy: Abstract> From<HashMap<TcKey, AbsTy>> for AbstractTypeTable<AbsTy> {
    fn from(map: HashMap<TcKey, AbsTy>) -> Self {
        AbstractTypeTable { table: map }
    }
}

/// An implementation of [`TypeTable`](trait.TypeTable.html) for concrete types.
/// See [`AbstractTypeTable`](struct.AbstractTypeTable.html) for an implementation specializing on
/// abstract types.
///
/// Can automatically be generated from a `HashMap<TcKey, Concrete>`.
#[derive(Debug, Clone)]
pub struct ReifiedTypeTable<Concrete> {
    table: HashMap<TcKey, Concrete>,
}

impl<Concrete> Index<TcKey> for ReifiedTypeTable<Concrete> {
    type Output = Concrete;
    fn index(&self, index: TcKey) -> &Self::Output {
        &self.table[&index]
    }
}

impl<Concrete> From<HashMap<TcKey, Concrete>> for ReifiedTypeTable<Concrete> {
    fn from(map: HashMap<TcKey, Concrete>) -> Self {
        ReifiedTypeTable { table: map }
    }
}

impl<AbsTy: Abstract> TypeTable for AbstractTypeTable<AbsTy> {
    type Type = AbsTy;

    fn as_hashmap(self) -> HashMap<TcKey, Self::Type> {
        self.table
    }
}

impl<Concrete> TypeTable for ReifiedTypeTable<Concrete> {
    type Type = Concrete;

    fn as_hashmap(self) -> HashMap<TcKey, Self::Type> {
        self.table
    }
}

impl<AbsTy> AbstractTypeTable<AbsTy>
where
    AbsTy: Abstract + Reifiable,
{
    /// Transforms an [`AbstractTypeTable`](struct.AbstractTypeTable.html) into a [`ReifiedTypeTable`](struct.ReifiedTypeTable.html)
    /// by reifying all abstract types.
    pub fn reified(self) -> ReifiedTypeTable<AbsTy::Reified> {
        ReifiedTypeTable { table: self.table.into_iter().map(|(key, ty)| (key, ty.reify())).collect() }
    }
}

impl<AbsTy> AbstractTypeTable<AbsTy>
where
    AbsTy: Abstract + TryReifiable,
{
    /// Attempts to transform an [`AbstractTypeTable`](struct.AbstractTypeTable.html) into a [`ReifiedTypeTable`](struct.ReifiedTypeTable.html)
    /// by reifying all abstract types.
    pub fn try_reified(self) -> Result<ReifiedTypeTable<AbsTy::Reified>, ()> {
        self.table
            .into_iter()
            .map(|(key, ty)| ty.try_reify().map(|re| (key, re)))
            .collect::<Result<HashMap<TcKey, AbsTy::Reified>, ReificationErr>>()
            .map_err(|_| ())
            .map(|table| ReifiedTypeTable { table })
    }
}