use crate::prelude::*;

fn fact_for_obj_satisfies_param_type_shallow(
    arg: Obj,
    param_type: &ParamType,
    line_file: LineFile,
) -> Fact {
    match param_type {
        ParamType::Set(_) => {
            Fact::AtomicFact(AtomicFact::IsSetFact(IsSetFact::new(arg, line_file)))
        }
        ParamType::NonemptySet(_) => Fact::AtomicFact(AtomicFact::IsNonemptySetFact(
            IsNonemptySetFact::new(arg, line_file),
        )),
        ParamType::FiniteSet(_) => Fact::AtomicFact(AtomicFact::IsFiniteSetFact(
            IsFiniteSetFact::new(arg, line_file),
        )),
        ParamType::Obj(obj) => {
            Fact::AtomicFact(AtomicFact::InFact(InFact::new(arg, obj.clone(), line_file)))
        }
        ParamType::Struct(st) => Fact::AtomicFact(AtomicFact::InFact(InFact::new(
            arg,
            Obj::StructObj(st.clone()),
            line_file,
        ))),
    }
}

impl Runtime {
    /// After `store_identifier_obj`, run param-type-specific work (type facts, storage, and later hooks).
    pub(crate) fn define_parameter_by_binding_param_type(
        &mut self,
        name: &str,
        param_type: &ParamType,
    ) -> Result<InferResult, RuntimeError> {
        match param_type {
            ParamType::Obj(obj) => match obj {
                Obj::FamilyObj(family_ty) => {
                    self.define_parameter_by_binding_family(name, family_ty)
                }
                _ => self.define_parameter_by_binding_obj(name, obj),
            },
            ParamType::Set(set) => self.define_parameter_by_binding_set(name, set),
            ParamType::NonemptySet(nonempty_set) => {
                self.define_parameter_by_binding_nonempty_set(name, nonempty_set)
            }
            ParamType::FiniteSet(finite_set) => {
                self.define_parameter_by_binding_finite_set(name, finite_set)
            }
            ParamType::Struct(struct_ty) => {
                self.define_parameter_by_binding_struct(name, struct_ty)
            }
        }
    }

    fn define_parameter_by_binding_family(
        &mut self,
        name: &str,
        family_ty: &FamilyObj,
    ) -> Result<InferResult, RuntimeError> {
        self.infer_membership_in_family_for_param_binding(name, family_ty)
    }

    fn define_parameter_by_binding_obj(
        &mut self,
        name: &str,
        obj: &Obj,
    ) -> Result<InferResult, RuntimeError> {
        let type_fact = Fact::AtomicFact(AtomicFact::InFact(InFact::new(
            Obj::Identifier(Identifier::new(name.to_string())),
            obj.clone(),
            default_line_file(),
        )));
        self.store_fact_without_well_defined_verified_and_infer(type_fact)
            .map_err(RuntimeError::from)
    }

    fn define_parameter_by_binding_set(
        &mut self,
        name: &str,
        _set: &Set,
    ) -> Result<InferResult, RuntimeError> {
        let type_fact = Fact::AtomicFact(AtomicFact::IsSetFact(IsSetFact::new(
            Obj::Identifier(Identifier::new(name.to_string())),
            default_line_file(),
        )));
        self.store_fact_without_well_defined_verified_and_infer(type_fact)
            .map_err(RuntimeError::from)
    }

    fn define_parameter_by_binding_nonempty_set(
        &mut self,
        name: &str,
        _nonempty_set: &NonemptySet,
    ) -> Result<InferResult, RuntimeError> {
        let type_fact = Fact::AtomicFact(AtomicFact::IsNonemptySetFact(IsNonemptySetFact::new(
            Obj::Identifier(Identifier::new(name.to_string())),
            default_line_file(),
        )));
        self.store_fact_without_well_defined_verified_and_infer(type_fact)
            .map_err(RuntimeError::from)
    }

    fn define_parameter_by_binding_finite_set(
        &mut self,
        name: &str,
        _finite_set: &FiniteSet,
    ) -> Result<InferResult, RuntimeError> {
        let type_fact = Fact::AtomicFact(AtomicFact::IsFiniteSetFact(IsFiniteSetFact::new(
            Obj::Identifier(Identifier::new(name.to_string())),
            default_line_file(),
        )));
        self.store_fact_without_well_defined_verified_and_infer(type_fact)
            .map_err(RuntimeError::from)
    }

    pub(crate) fn define_parameter_by_binding_struct(
        &mut self,
        name: &str,
        struct_ty: &StructObj,
    ) -> Result<InferResult, RuntimeError> {
        self.register_param_as_struct_instance(name, struct_ty.clone());

        let mut infer_result = InferResult::new();

        let new_fact = Fact::AtomicFact(AtomicFact::InFact(InFact::new(
            Obj::Identifier(Identifier::new(name.to_string())),
            Obj::StructObj(struct_ty.clone()),
            default_line_file(),
        )));
        infer_result.new_infer_result_inside(
            self.store_fact_without_well_defined_verified_and_infer(new_fact)
                .map_err(RuntimeError::from)?,
        );

        let struct_name = struct_ty.name.to_string();
        let Some(def) = self.get_cloned_definition_of_struct(&struct_name) else {
            return Ok(infer_result);
        };

        let base_map = ParamGroupWithStructFieldType::param_defs_and_args_to_param_to_arg_map(
            &def.param_defs,
            &struct_ty.args,
        );
        let lf = default_line_file();
        for (field_name, field_st) in def.fields.iter() {
            let arg = Obj::FieldAccess(FieldAccess::new(name.to_string(), field_name.clone()));
            let param_type = self.inst_param_type(&field_st.to_param_type(), &base_map)?;
            let f = fact_for_obj_satisfies_param_type_shallow(arg, &param_type, lf.clone());
            infer_result.new_infer_result_inside(
                self.store_fact_without_well_defined_verified_and_infer(f)
                    .map_err(RuntimeError::from)?,
            );
        }

        let iff_facts = self.instantiated_struct_def_or_and_facts_for_def(struct_ty, &def, name)?;
        for ocf in iff_facts {
            infer_result.new_infer_result_inside(
                self.store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer(ocf)
                    .map_err(RuntimeError::from)?,
            );
        }

        Ok(infer_result)
    }

    pub fn register_param_as_struct_instance(&mut self, env_key: &str, inst: StructObj) {
        let key = env_key.to_string();
        self.top_level_env()
            .known_identifier_satisfy_struct
            .insert(key.clone(), inst);
        self.top_level_env()
            .cache_well_defined_obj
            .insert(key.clone(), ());
        self.top_level_env().defined_identifiers.insert(key, ());
    }

    pub fn define_params_with_type(
        &mut self,
        param_defs: &[ParamGroupWithParamType],
        check_type_nonempty: bool,
    ) -> Result<InferResult, RuntimeError> {
        let mut infer_result = InferResult::new();
        for param_def in param_defs.iter() {
            self.verify_param_type_well_defined(&param_def.param_type, &VerifyState::new(0, false))
                .map_err(|well_defined_error| {
                    let param_names_text = param_def.params.join(", ");
                    let error_line_file = well_defined_error.line_file().clone();
                    RuntimeError::new_define_params_error_with_msg_previous_error_position(
                        format!(
                            "define params with type: failed to verify type well-defined for params [{}] with type {}",
                            param_names_text, param_def.param_type
                        ),
                        Some(well_defined_error.into()),
                        error_line_file,
                    )
                })?;
            self.verify_param_type_nonempty_if_required(&param_def.param_type, check_type_nonempty)
                .map_err(|inner_exec_error| {
                    let param_names_text = param_def.params.join(", ");
                    RuntimeError::new_define_params_error_with_msg_previous_error_position(
                        format!(
                            "define params with type: nonempty check failed for params [{}] with type {}",
                            param_names_text, param_def.param_type
                        ),
                        Some(RuntimeError::from(inner_exec_error)),
                        default_line_file(),
                    )
                })?;

            for name in param_def.params.iter() {
                self.store_identifier_obj(name).map_err(|runtime_error| {
                    RuntimeError::new_define_params_error_with_msg_previous_error_position(
                        format!(
                            "define params with type: failed to declare parameter `{}`",
                            name
                        ),
                        Some(RuntimeError::from(runtime_error)),
                        default_line_file(),
                    )
                })?;
                let fact_infer_result = self
                    .define_parameter_by_binding_param_type(name, &param_def.param_type)
                    .map_err(|runtime_error| {
                        RuntimeError::new_define_params_error_with_msg_previous_error_position(
                            format!(
                                "define params with type: failed to apply param type for parameter `{}` with type {}",
                                name, param_def.param_type
                            ),
                            Some(runtime_error),
                            default_line_file(),
                        )
                    })?;
                infer_result.new_infer_result_inside(fact_infer_result);
            }
        }
        Ok(infer_result)
    }
}
