use std::rc::Rc;

use crate::ast::*;
use crate::util::ScopeStack;

pub type TypeName = Rc<String>;

pub struct TypeContext<'a> {
  variable_map: ScopeStack<'a, Rc<String>, ()>,
  evar_count: u32
}

/// `InferResult` is the monad in which type inference takes place.
type InferResult<T> = Result<T, TypeError>;

#[derive(Debug, Clone)]
struct TypeError { msg: String }

impl TypeError {
  fn new<A>(msg: &str) -> InferResult<A> {
    Err(TypeError { msg: msg.to_string() })
  }
}

#[derive(Debug)]
pub enum Type {
  Const(TypeConst),
  Arrow(Box<Type>, Box<Type>)
}

#[derive(Debug)]
pub enum TypeConst {
  Unit,
  Nat,
  Int,
  Float,
  StringT,
  Bool,
  Order,
  UserDefined
}

impl Type {
  fn arrow(a: Type, b: Type) -> Type {
    Type::Arrow(Box::new(a), Box::new(b))
  }

  fn to_string(&self) -> String {
    use self::Type::*;
    use self::TypeConst::*;
    match self {
      Const(Unit) => format!("()"),
      Const(Nat) => format!("Nat"),
      Const(Int) => format!("Int"),
      Const(Float) => format!("Float"),
      Const(StringT) => format!("String"),
      Const(Bool) => format!("Bool"),
      Const(Order) => format!("Order"),
      _ => format!("UNKNOWN TYPE"),
    }
  }
}

/*
/// `Type` is parameterized by whether the type variables can be just universal, or universal or
/// existential.
#[derive(Debug, Clone)]
enum Type<A> {
  Var(A),
  Const(TConst),
  Arrow(Box<Type<A>>, Box<Type<A>>),
}

#[derive(Debug, Clone)]
enum TVar {
  Univ(UVar),
  Exist(ExistentialVar)
}

#[derive(Debug, Clone)]
struct UVar(Rc<String>);

#[derive(Debug, Clone)]
struct ExistentialVar(u32);

impl Type<UVar> {
  fn to_tvar(&self) -> Type<TVar> {
    match self {
      Type::Var(UVar(name)) => Type::Var(TVar::Univ(UVar(name.clone()))),
      Type::Const(ref c) => Type::Const(c.clone()),
      Type::Arrow(a, b) => Type::Arrow(
        Box::new(a.to_tvar()),
        Box::new(b.to_tvar())
      )
    }
  }
}

impl Type<TVar> {
  fn skolemize(&self) -> Type<UVar> {
    match self {
      Type::Var(TVar::Univ(uvar)) => Type::Var(uvar.clone()),
      Type::Var(TVar::Exist(_)) => Type::Var(UVar(Rc::new(format!("sk")))),
      Type::Const(ref c) => Type::Const(c.clone()),
      Type::Arrow(a, b) => Type::Arrow(
        Box::new(a.skolemize()),
        Box::new(b.skolemize())
      )
    }
  }
}

impl TypeIdentifier {
  fn to_monotype(&self) -> Type<UVar> {
    match self {
      TypeIdentifier::Tuple(_) => Type::Const(TConst::Nat),
      TypeIdentifier::Singleton(TypeSingletonName { name, .. }) => {
        match &name[..] {
          "Nat" => Type::Const(TConst::Nat),
          "Int" => Type::Const(TConst::Int),
          "Float" => Type::Const(TConst::Float),
          "Bool" => Type::Const(TConst::Bool),
          "String" => Type::Const(TConst::StringT),
          _ => Type::Const(TConst::Nat),
        }
      }
    }
  }
}

#[derive(Debug, Clone)]
enum TConst {
  User(Rc<String>),
  Unit,
  Nat,
  Int,
  Float,
  StringT,
  Bool,
}

impl TConst {
  fn user(name: &str) -> TConst {
    TConst::User(Rc::new(name.to_string()))
  }
}
*/

impl<'a> TypeContext<'a> {
  pub fn new() -> TypeContext<'a> {
    TypeContext { 
      variable_map: ScopeStack::new(None),
      evar_count: 0
    }
  }

  pub fn typecheck(&mut self, ast: &AST) -> Result<String, String> {
    let mut returned_type = Type::Const(TypeConst::Unit);
    for statement in ast.0.iter() {
      returned_type = self.typecheck_statement(statement.node()).map_err(|err| { err.msg })?
    }
    Ok(returned_type.to_string())
  }

  fn typecheck_statement(&mut self, statement: &Statement) -> InferResult<Type> {
    match statement {
      Statement::ExpressionStatement(e) => self.typecheck_expr(e.node()),
      Statement::Declaration(decl) => self.typecheck_decl(decl),
    }
  }

  fn typecheck_decl(&mut self, _decl: &Declaration) -> InferResult<Type> {
    Ok(Type::Const(TypeConst::Unit))
  }

  fn typecheck_expr(&mut self, expr: &Expression) -> InferResult<Type> {
    match expr {
      Expression(expr_type, Some(_anno)) => {
        //TODO here
        self.typecheck_expr_type(expr_type)
      },
      Expression(expr_type, None) => self.typecheck_expr_type(expr_type)
    }
  }

  fn typecheck_expr_type(&mut self, expr: &ExpressionType) -> InferResult<Type> {
    use self::ExpressionType::*;
    Ok(match expr {
      NatLiteral(_) => Type::Const(TypeConst::Nat),
      BoolLiteral(_) => Type::Const(TypeConst::Bool),
      _ => Type::Const(TypeConst::Unit)
    })
  }
}