use {
    crate::{
        lexer::InputRegionTag,
        expr::{LTExpr, Statement, TypeTag, TypeError, TypeErrorKind},
        symbols::{Scope, SymbolDef},
    },
    std::{
        ops::Deref,
        sync::{Arc, RwLock},
    },
    laddertypes::{
        parser::ParseLadderType,
        unparser::UnparseLadderType,
        dict::TypeDict
    },
    tisc::{assembler::AssemblyWord, linker::LinkAddr},
    tiny_ansi::TinyAnsi
};

impl LTExpr {
    /*
    pub fn get_type(&self) -> TypeTag {
        Err(TypeError::Todo)
    }*/

    pub fn infer_type(&self, scope: &Arc<RwLock<Scope>>) -> TypeTag
    {
        match self {
            LTExpr::WordLiteral{ region, val } => {
                Ok(scope.write().unwrap().parse(
                    "ℤ_2^64 ~ machine.UInt64 ~ machine.Word"
                ).unwrap())
            }

            LTExpr::StringLiteral{ region, value } => {
                Ok(scope.write().unwrap().parse(
                    "<Seq Char ~ Unicode ~ ℤ_2^32 ~ ℤ_2^64 ~ machine.UInt64>
                    ~ <TermArray 0 machine.UInt64 ~ machine.Word>"
                ).unwrap())
            }

            LTExpr::Symbol { region, typ, symbol } => {
                let mut s = scope.write().unwrap();
                if let Some(sdef) = s.get(symbol) {
                    Ok(sdef.get_type(&mut *s))
                } else {
                    let region = region.clone();
                    Err(vec![ TypeError{ region, kind: TypeErrorKind::NoSymbol } ])
                }
            }

            LTExpr::Ascend { region, typ, expr } => {
                let expr_type = expr.infer_type( scope )?;
                let sub_type = typ.clone();

                /*
                 * todo: check potential overlap of typ with expr_type
                 */
                if let Ok(i) = sub_type.is_syntactic_subtype_of(&expr_type) {
                    let mut lnf = expr_type.get_lnf_vec();
                    let mut sub_lnf = sub_type.get_lnf_vec();

                    for x in 0..i {
                        lnf.insert(x, sub_lnf.remove(0));
                    }
                    let result_type = laddertypes::TypeTerm::Ladder(lnf);
                    Ok(result_type)
                } else {
                    Ok(laddertypes::TypeTerm::Ladder(vec![
                        sub_type,
                        expr_type
                    ]))
                }
            }

            LTExpr::Descend { region, typ, expr } => {
                let expr_type = expr.infer_type(scope)?;
                let super_type = typ.clone();

                if let Ok(i) = expr_type.is_syntactic_subtype_of(&super_type) {
                    let lnf = expr_type.get_lnf_vec();
                    let result_type = laddertypes::TypeTerm::Ladder(lnf[i..].into_iter().cloned().collect());
                    Ok(result_type)
                } else {
                    return Err(vec![ TypeError{
                        region: region.clone(),
                        kind: TypeErrorKind::ArgTypeMismatch {
                            expected: expr_type,
                            received: super_type
                        }
                    } ]);
                }
            }

            LTExpr::Abstraction { region, scope, args, body } => {
                let mut f = Vec::new();

                for (region, name, typ) in args {
                    if let Some(typ) = typ {
                        let typ = typ.clone()?;
                        let sugar_typ = typ.clone().sugar(&mut *scope.write().unwrap());
                        f.push( sugar_typ );

                        scope.write().unwrap().declare_var(name.clone(), typ.clone());
                    }
                }

                let body_type = body.infer_type( scope )?;
                f.push( body_type.sugar(&mut *scope.write().unwrap()) );

                Ok(laddertypes::SugaredTypeTerm::Func(f).desugar( &mut *scope.write().unwrap() ))
            }

            LTExpr::Application{ region, typ, head, body } => {
                let mut head_type = head.infer_type(scope)?;
                let mut args = body.into_iter();

                let mut result_type = head_type;
                let mut sugared_result_type = result_type.sugar(&mut *scope.write().unwrap());

                let mut errors = Vec::new();

                while let laddertypes::SugaredTypeTerm::Func(mut f_types) = sugared_result_type {
                    sugared_result_type = f_types.pop().unwrap();

                    for (argi, expected_arg_type) in f_types.iter().enumerate() {
                        if let Some(arg) = args.next() {

                            let expected_arg_type = expected_arg_type.clone().desugar(&mut *scope.write().unwrap());

                            // check subtype
                            let received_arg_type = arg.infer_type(scope)?;
                            if ! received_arg_type.is_syntactic_subtype_of(&expected_arg_type).is_ok() {
                                errors.push(TypeError{
                                    region: arg.get_region(),
                                    kind: TypeErrorKind::ArgTypeMismatch {
                                        expected: expected_arg_type,
                                        received: received_arg_type
                                    }
                                });
                            }

                        } else {
                            // partial application.
                            f_types.push(sugared_result_type);
                            sugared_result_type = laddertypes::SugaredTypeTerm::Func(
                                f_types[argi .. ].into_iter().cloned().collect()
                            );

                            // todo examine stack ..
                            
                            return
                                if errors.len() == 0 {
                                    result_type = sugared_result_type.desugar(&mut *scope.write().unwrap());
                                    Ok(result_type)
                                } else {
                                    Err(errors)
                                };
                        }
                    }
                }

                while let Some(arg) = args.next() {
                    errors.push(TypeError{
                        region: arg.get_region(),
                        kind: TypeErrorKind::SuperfluousArgument
                    });
                }

                if errors.len() == 0 {
                    result_type = sugared_result_type.desugar(&mut *scope.write().unwrap());
                    Ok(result_type)
                } else {
                    Err(errors)
                }
            }

            LTExpr::Branch { region, condition, if_expr, else_expr } => {
                let received_cond_type = condition.infer_type(scope)?;
                let expected_cond_type = scope.write().unwrap().parse("Bool ~ machine.Word").unwrap();

                if received_cond_type.is_syntactic_subtype_of(&expected_cond_type).is_ok() {

                    let if_expr_type = if_expr.infer_type(scope)?;
                    let else_expr_type = else_expr.infer_type(scope)?;

                    if if_expr_type.is_syntactic_subtype_of(&else_expr_type).is_ok() {
                        Ok(else_expr_type)
                    } else if else_expr_type.is_syntactic_subtype_of(&if_expr_type).is_ok() {
                        Ok(if_expr_type)
                    } else {
                        Err(vec![TypeError{
                           region: region.clone(),
                           kind: TypeErrorKind::BranchMismatch {
                               if_branch: if_expr_type,
                               else_branch: else_expr_type
                           }
                        }])
                    }
                } else {
                    Err(vec![ TypeError{
                        region: condition.get_region(),
                        kind: TypeErrorKind::ArgTypeMismatch {
                            expected: expected_cond_type,
                            received: received_cond_type
                        }
                    }])
                }
            }
            LTExpr::WhileLoop { region, condition, body } => {
                let received_cond_type = condition.infer_type(scope)?;
                let expected_cond_type = scope.write().unwrap().parse("Bool ~ machine.Word").unwrap();

                if received_cond_type.is_syntactic_subtype_of(&expected_cond_type).is_ok() {
                    let body_type = body.infer_type(scope)?;
                    let body_type = body_type.sugar(&mut scope.clone());
                    let loop_type = laddertypes::SugaredTypeTerm::Seq(vec![ body_type ]);
                    Ok(loop_type.desugar(&mut scope.clone()))
                } else {
                    return Err(vec![ TypeError{
                        region: condition.get_region(),
                        kind: TypeErrorKind::ArgTypeMismatch {
                            expected: expected_cond_type,
                            received: received_cond_type
                        }
                    }]);
                }
            }
            LTExpr::ExportBlock{ region, scope, statements } |
            LTExpr::Block{ region, scope, statements } => {
                let mut types = Vec::new();

                for s in statements {
                    match s.infer_type(scope) {
                        Ok(Some(t)) => {
                            if !t.is_empty() {
                                types.insert(0, t);
                            }
                        }
                        Ok(None) => {}
                        Err(e) => {
                            return Err(e);
                        }
                    }
                }

                Ok(
                    if types.len() == 1 { types.pop().unwrap() }
                    else { laddertypes::SugaredTypeTerm::Struct(types) }
                    .desugar(&mut scope.clone())
                )
            }
        }
    }
}

impl Statement {
    pub fn infer_type(&self, scope: &Arc<RwLock<Scope>>) -> Result< Option<laddertypes::SugaredTypeTerm> , Vec<TypeError> > {
        match self {
            Statement::LetAssign{ name_region, typ, var_id, val_expr } => {
                let typ = val_expr.infer_type( scope )?;

                match typ.clone().sugar( &mut scope.clone() ) {
                    laddertypes::SugaredTypeTerm::Func(mut args) => {
                        let out_type = args.pop().unwrap();
                        let out_types =
                            match out_type.clone() {
                                laddertypes::SugaredTypeTerm::Struct(oa) => oa.into_iter().map(|t|t.desugar(&mut scope.clone())).collect(),
                                _ => vec![ out_type.desugar(&mut scope.clone()) ]
                            };
                         let in_types = args.into_iter().map(|t| t.desugar(&mut scope.clone())).collect();

                         scope.write().unwrap()
                             .declare_proc(
                                 var_id.clone(),
                                 in_types,
                                 out_types,
                                 true
                            );

                        return Ok(None);
                    }
                    _ => {
                       let id = scope.write().unwrap().declare_var(var_id.clone(), typ);
                       eprintln!("TYPING declare var = {}", id);
                       Ok(None)
                    }
                }
            },
            Statement::Return(expr) |
            Statement::Expr(expr) => {
                let t = expr.infer_type(scope)?;

                if t != laddertypes::TypeTerm::App(vec![]) {
                    let st = t.sugar(&mut scope.clone());
                    Ok(Some(st))
                } else {
                    Ok(None)
                }
            }
            Statement::Assignment { name_region, var_id, val_expr } => {
                let received_type = val_expr.infer_type(scope)?;
                let expected_type = scope.write().unwrap().get_type(var_id).unwrap();
                if ! received_type.is_syntactic_subtype_of(&expected_type).is_ok() {
                    return Err(vec![ TypeError{
                        region: val_expr.get_region(),
                        kind: TypeErrorKind::AssignMismatch {
                            expected: expected_type,
                            received: received_type
                        }
                    }]);
                } else {
                    Ok(None)
                }
            }
        }
    }
}