//! Type checking for the AST.
//! This module implements a bi-unification type-checking algorithm to infer
//! types for each node in the AST.

// Visitor pattern has lots of unused arguments
#![allow(unused_variables)]

use std::collections::HashMap;

use super::{Ast, Index, intern, visitor::AstVisitorTrait};

type Id = u32;

enum Type {
    Reified(intern::Index),
    Variable(Id),
}

/// Variance of a type parameter or constraint.
/// A function of type `A -> B` is covariant in `B` and contravariant in `A`.
/// This means that a type `T` may be substituted for `A` if `T` is a subtype of `A`, but
/// a type `T` may only be substituted for `B` if `T` is a supertype of `B`.
///
/// Namely, in a type system with `int` and `nat <: int`, for a function `f: int
/// -> int` in the expression `let u: int = 3; let t: nat = f(u);`, `u` may
/// safely be used as an argument to `f` because `nat <: int`, but `f(u`)` may
/// not be assigned to `t` because `int <: nat` is not true.
enum Variance {
    #[doc(alias = "Positive")]
    Covariant,
    #[doc(alias = "Negative")]
    Contravariant,
}

#[derive(Debug, Clone, Copy)]
struct Value(Id);
#[derive(Debug, Clone, Copy)]
struct Use(Id);

/// Typechecking error.
#[derive(Debug, Clone, thiserror::Error)]
enum Error {
    #[error("Unimplemented feature")]
    Unimplemented,
}

type Result<T> = std::result::Result<T, Error>;

struct Bindings {
    inner: HashMap<super::Index, Value>,
}

struct TypeChecker<'a> {
    pool: &'a mut intern::InternPool,
}

// Core
impl TypeChecker<'_> {
    pub fn new(pool: &mut intern::InternPool) -> TypeChecker {
        TypeChecker { pool }
    }

    fn var(&mut self) -> (Value, Use) {
        todo!()
    }
}

// Frontend

impl<'a> AstVisitorTrait<&'a Ast> for TypeChecker<'_> {
    type Error = Error;
    type Value = Value;

    const UNIMPL: Self::Error = Error::Unimplemented;

    fn visit_constant_impl(
        &mut self,
        ast: &'a Ast,
        idx: Index,
        ty: Index,
        value: intern::Index,
    ) -> std::result::Result<Self::Value, Self::Error> {
        // constants may be of type `comptime_int`, which is a special type that
        // cannot exist at runtime.

        todo!()
    }
}