use thiserror::Error;

use merc_syntax::SortExpression;

use merc_syntax::UntypedDataSpecification;

use merc_utilities::MercError;

use crate::is_nonempty_sort;

use crate::target_sort;

/// Checks if a signature is well-typed, i.e. it satisfies the conditions of 15.1.7.

    // Check that there are no constructors defined for the basic sorts.

        // There are not more constructors for basic sorts.

        // Function sorts are not constructor sorts

    }

    // Check that all sorts are syntactically non-empty.

    }

#[derive(Debug, Error)]

pub enum WellTypedError {

    #[error("Constructor '{}' and mapping '{}' have the same identifier", constructor, map)]

    ConstructorAndMappingConflict { constructor: String, map: String },

    #[error(

        "Constructors cannot be defined for basic sorts, but constructor '{}' is defined for sort '{}'",

        constructor,

        sort

    )]

    ConstructorForBasicSort { constructor: String, sort: String },

    #[error(

        "Constructors cannot be defined for function sorts, but constructor '{}' is defined for sort '{}'",

        constructor,

        sort

    )]

    ConstructorForFunctionSort { constructor: String, sort: String },

    #[error("Sort '{}' is syntactically empty", sort)]

    EmptySort { sort: String },

    #[error("Alias cycle detected: {:?}", sorts)]

    AliasCycle { sorts: Vec<String> },

    #[error("Error: '{}'", 0)]

    Custom(MercError),

    // These are name resolution errors, but we include them here to avoid having to define a separate error type for name resolution.

    #[error("Duplicate sort declaration: '{}'", sort)]

    DuplicateSortDeclaration { sort: String },

    #[error("Undefined sort: '{}'", sort)]

    UndefinedSort { sort: String },

}

/// Checks that the constructors and mappings are disjoint, i.e. that no identifier is both a constructor and a mapping.

        {

    }

/// The set of basic sorts `BS` are exactly the sorts Bool, Pos, Int, Nat, and Real. Definition 15.1.2.

#[cfg(test)]

mod tests {

    use merc_syntax::UntypedDataSpecification;

    use crate::DataSpecification;

    use crate::WellTypedError;

    #[test]

        )

        }

}