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> { //TODO make these kinds of error-producing functions CoW-ready
    Err(TypeError { msg: msg.to_string() })
  }
}

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

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

//TODO find a better way to capture the to/from string logic
impl Type {
  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(Ordering) => format!("Ordering"),
      _ => format!("UNKNOWN TYPE"),
    }
  }

  fn from_string(string: &str) -> Option<Type> {
    use self::Type::*;
    use self::TypeConst::*;
    Some(match string {
      "()" | "Unit" => Const(Unit),
      "Nat" => Const(Nat),
      "Int" => Const(Int),
      "Float" => Const(Float),
      "String" => Const(StringT),
      "Bool" => Const(Bool),
      "Ordering" => Const(Ordering),
      _ => return None
    })
  }
}

/*
/// `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
    }
  }

  fn get_type_from_name(&self, name: &TypeIdentifier) -> InferResult<Type> {
    use self::TypeIdentifier::*;
    Ok(match name {
      Singleton(TypeSingletonName { name, params }) =>  {
        match Type::from_string(&name) {
          Some(ty) => ty,
          None => return TypeError::new("Unknown type name")
        }
      },
      Tuple(_) => return TypeError::new("tuples aren't ready yet"),
    })

  }

  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
        let t1 = self.typecheck_expr_type(expr_type)?;
        let t2 = self.get_type_from_name(anno)?;
        self.unify(t2, t1)
      },
      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),
      FloatLiteral(_) => Type::Const(TypeConst::Float),
      StringLiteral(_) => Type::Const(TypeConst::StringT),
      _ => Type::Const(TypeConst::Unit)
    })
  }


  fn unify(&mut self, t1: Type, t2: Type) -> InferResult<Type> {
    println!("Unify ain't done yo");
    Ok(t1)
  }
}