use crate::ast::*;
use tracing::instrument;

use derive_more::Display;
use std::collections::HashMap;
use std::fmt;

#[derive(Display)]
pub enum CheckerError {
    #[display("Unbound: {_0}")]
    Unbound(String),
    #[display("Rebinding: {_0}")]
    Rebinding(String),
    #[display("The following functionality is unimplemented: {_0}")]
    Unimplemented(String),
    #[display("Element claimed to belong to {claimed} but actually belongs to {real}")]
    WrongSetForElement { claimed: Set, real: Set },
    #[display("Element {element} does belong to set {claimed}: {reason}")]
    ElementDoesNotBelong {
        element: Element,
        claimed: Set,
        reason: String,
    },
    #[display("Case analysis {_0} does not have consistent set for scrutinee")]
    IncosistentCaseScrutineeSet(Element),
    #[display("Incomplete case analysis: covered [{}] but required [{}]",
        found.join(", "),
        required.join(", ")
    )]
    IncompleteCaseAnalysis {
        found: Vec<String>,
        required: Vec<String>,
    },
}

#[derive(Display, Clone)]
#[display("{field_set} @ {owner_set}")]
pub struct SetField {
    pub field_set: Set,
    pub owner_set: Set,
}

#[derive(Display, Clone)]
#[display("{element} : {set}")]
pub struct CheckedElement {
    pub element: Element,
    pub set: Set,
}

#[derive(Default, Clone)]
pub struct CheckerState {
    wf_sets: HashMap<String, Set>,
    wf_elements: HashMap<String, CheckedElement>,
    wf_signatures: HashMap<String, Signature>,
    wf_instances: HashMap<String, Instance>,
    record_fields: HashMap<String, SetField>,
    variant_fields: HashMap<String, SetField>,
}

impl fmt::Display for CheckerState {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        fn section<K, V>(f: &mut fmt::Formatter<'_>, name: &str, map: &HashMap<K, V>) -> fmt::Result
        where
            K: fmt::Display + Ord,
            V: fmt::Display,
        {
            writeln!(f, "  {name} = {{")?;
            let mut entries: Vec<_> = map.iter().collect();
            entries.sort_by(|a, b| a.0.cmp(b.0));
            for (k, v) in entries {
                writeln!(f, "    {k} ~> {v},")?;
            }
            writeln!(f, "  }},")
        }

        writeln!(f, "CheckState {{")?;
        section(f, "sets", &self.wf_sets)?;
        section(f, "elements", &self.wf_elements)?;
        section(f, "record_fields", &self.record_fields)?;
        section(f, "variant_fields", &self.variant_fields)?;
        section(f, "signatures", &self.wf_signatures)?;
        section(f, "instances", &self.wf_instances)?;
        writeln!(f, " }}")?;
        Ok(())
    }
}

// The invariant we're maintaining is that everything is fully evaluated before
// we commit it to be stored in the state.
impl CheckerState {
    // Because of our invariant we don't actually need to do anything
    // non-trivial here.
    #[instrument(skip(self), level = "debug", fields(%set_a, %set_b))]
    pub fn set_equal(&self, set_a: &Set, set_b: &Set) -> bool {
        set_a == set_b
    }

    #[instrument(skip(self), level = "debug")]
    fn assert_unbound_set(&self, name: &String) -> Result<(), CheckerError> {
        if self.wf_sets.contains_key(name) {
            Err(CheckerError::Rebinding(name.clone()))
        } else {
            Ok(())
        }
    }

    #[instrument(skip(self), level = "debug")]
    fn assert_unbound_element(&self, name: &String) -> Result<(), CheckerError> {
        if self.wf_elements.contains_key(name) {
            Err(CheckerError::Rebinding(name.clone()))
        } else {
            Ok(())
        }
    }

    #[instrument(skip(self), level = "debug", fields(%name, %set_ref, %belongs_to))]
    fn assert_correct_owner(
        &self,
        name: &String,
        set_ref: &SetField,
        belongs_to: &Set,
    ) -> Result<(), CheckerError> {
        if !self.set_equal(&set_ref.owner_set, belongs_to) {
            Err(CheckerError::Rebinding(name.clone()))
        } else {
            Ok(())
        }
    }

    #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))]
    fn add_record_field(
        &mut self,
        name: &String,
        field_set: &Set,
        owner_set: &Set,
    ) -> Result<(), CheckerError> {
        if let Some(set_ref) = self.record_fields.get(name) {
            self.assert_correct_owner(name, set_ref, owner_set)?;
        };
        self.record_fields.insert(
            name.clone(),
            SetField {
                field_set: field_set.clone(),
                owner_set: owner_set.clone(),
            },
        );
        Ok(())
    }

    #[instrument(skip(self), level = "debug", fields(%name, %field_set, %owner_set))]
    fn add_variant_field(
        &mut self,
        name: &String,
        field_set: &Set,
        owner_set: &Set,
    ) -> Result<(), CheckerError> {
        if let Some(set_ref) = self.variant_fields.get(name) {
            self.assert_correct_owner(name, set_ref, owner_set)?;
        };
        self.variant_fields.insert(
            name.clone(),
            SetField {
                field_set: field_set.clone(),
                owner_set: owner_set.clone(),
            },
        );
        Ok(())
    }

    #[instrument(skip(self), level = "debug", fields(%name, %set))]
    pub fn add_set(&mut self, name: &String, set: Set) -> Result<(), CheckerError> {
        self.assert_unbound_set(name)?;
        match &set {
            Set::Record(fields) => {
                for RecordField {
                    name: rfn,
                    set: field_set,
                } in fields
                {
                    self.add_record_field(rfn, field_set, &set)?;
                }
            }
            Set::Variant(fields) => {
                for VariantField {
                    name: vfn,
                    set: field_set,
                } in fields
                {
                    self.add_variant_field(vfn, field_set, &set)?;
                }
            }
            _ => (),
        };
        self.wf_sets.insert(name.clone(), set);
        Ok(())
    }

    pub fn add_element(
        &mut self,
        name: String,
        element: Element,
        set: Set,
    ) -> Result<(), CheckerError> {
        self.assert_unbound_element(&name)?;
        self.wf_elements
            .insert(name, CheckedElement { element, set });
        Ok(())
    }

    pub fn lookup_set(&self, name: &String) -> Result<&Set, CheckerError> {
        self.wf_sets
            .get(name)
            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
    }

    pub fn lookup_element(&self, name: &String) -> Result<&CheckedElement, CheckerError> {
        self.wf_elements
            .get(name)
            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
    }

    pub fn lookup_record_field(&self, name: &String) -> Result<&SetField, CheckerError> {
        self.record_fields
            .get(name)
            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
    }

    pub fn lookup_variant_field(&self, name: &String) -> Result<&SetField, CheckerError> {
        self.variant_fields
            .get(name)
            .map_or(Err(CheckerError::Unbound(name.clone())), Ok)
    }
}