use crate::constraint_graph::ConstraintGraph;
use crate::keys::{Constraint, TcKey};
use crate::types::{Abstract, AbstractTypeTable};
use std::collections::HashMap;
use std::fmt::Debug;
use std::hash::Hash;
pub trait TcVar: Debug + Eq + Hash + Clone {}
#[derive(Debug, Clone)]
pub struct TypeChecker<AbsTy: Abstract, Var: TcVar> {
variables: HashMap<Var, TcKey>,
graph: ConstraintGraph<AbsTy>,
keys: Vec<TcKey>,
}
impl<AbsTy: Abstract, Var: TcVar> Default for TypeChecker<AbsTy, Var> {
fn default() -> Self {
TypeChecker::new()
}
}
impl<AbsTy: Abstract, Var: TcVar> TypeChecker<AbsTy, Var> {
pub fn new() -> Self {
TypeChecker { keys: Vec::new(), variables: HashMap::new(), graph: ConstraintGraph::new() }
}
fn next_key(&self) -> TcKey {
TcKey::new(self.keys.len())
}
pub fn new_term_key(&mut self) -> TcKey {
let key = self.next_key();
self.graph.add(key);
self.keys.push(key); key
}
pub fn get_var_key(&mut self, var: &Var) -> TcKey {
if let Some(tck) = self.variables.get(var) {
*tck
} else {
let key = self.new_term_key();
self.variables.insert(var.clone(), key);
key
}
}
pub fn get_child_key(&mut self, parent: TcKey, nth: usize) -> Result<TcKey, TcErr<AbsTy>> {
let next_key = self.next_key(); let child = self.graph.nth_child(parent, nth, || next_key)?;
if child != next_key {
self.keys.push(child);
}
Ok(child)
}
pub fn impose(&mut self, constr: Constraint<AbsTy>) -> Result<(), TcErr<AbsTy>> {
match constr {
Constraint::Conjunction(cs) => {
cs.into_iter().map(|c| self.impose(c)).collect::<Result<(), TcErr<AbsTy>>>()?
}
Constraint::Equal(a, b) => self.graph.equate(a, b)?,
Constraint::MoreConc { target, bound } => self.graph.add_upper_bound(target, bound),
Constraint::MoreConcExplicit(target, bound) => self.graph.explicit_bound(target, bound)?,
}
Ok(())
}
pub fn all_keys(&self) -> impl Iterator<Item = &TcKey> {
self.keys.iter()
}
pub fn type_check(self) -> Result<AbstractTypeTable<AbsTy>, TcErr<AbsTy>> {
self.graph.solve().map(AbstractTypeTable::from)
}
}
#[derive(Debug, Clone)]
pub enum TcErr<AbsTy: Abstract> {
KeyEquation(TcKey, TcKey, AbsTy::Err),
TypeBound(TcKey, AbsTy::Err),
ChildAccessOutOfBound(TcKey, AbsTy, usize),
}