%---------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1996-2011 The University of Melbourne.
% Copyright (C) 2019-2024 The Mercury team.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%---------------------------------------------------------------------------%
%
% File: check_type_inst_mode_defns.m.
% Main author: zs.
%
% This module checks whether the type definition and foreign enum items
% in a module represent a valid set of type definitions.
%
%---------------------------------------------------------------------------%

:- module parse_tree.check_type_inst_mode_defns.
:- interface.

:- import_module parse_tree.error_spec.
:- import_module parse_tree.prog_item.

:- import_module list.

%---------------------------------------------------------------------------%

:- type maybe_insist_on_defn
    --->    do_not_insist_on_defn
    ;       do_insist_on_defn.

    % create_type_ctor_checked_map(InsistOnDefn,
    %   IntTypeDefnMap, ImpTypeDefnMap, ImpForeignEnumMap,
    %   TypeCtorCheckedMap, !Specs):
    %
    % Given the type definitions in both the interface and implementation
    % sections of a module, and foreign enum definitions in the implementation
    % section, check for each type constructor whether all the definitions
    % of that type constructor are consistent with one another.
    %
    % If yes, then include a representation of that consistent set
    % of declarations for that type constructor in TypeCtorCheckedMap.
    %
    % If not, generate one or more error messages.
    %
    % If InsistOnDefn is do_insist_on_defn, then also generate an error
    % if a TypeCtor is not actually defined. If our input comes from
    % a source file InsistOnDefn *should* be do_insist_on_defn, since
    % declaring but not defining a type is an error. (With the very rare
    % exception of a few library types whose definitions are in the
    % runtime system, outside the view of the Mercury compiler.)
    % However, InsistOnDefn should be do_not_insist_on_defn if the
    % input comes from interface files whose creation may have deleted
    % any such originally-present definitions.
    %
    % In addition, generate error messages for any duplicate field names
    % on arguments of du types.
    %
:- pred create_type_ctor_checked_map(maybe_insist_on_defn::in,
    type_ctor_defn_map::in, type_ctor_defn_map::in,
    type_ctor_foreign_enum_map::in, type_ctor_checked_map::out,
    list(error_spec)::in, list(error_spec)::out) is det.

:- pred create_inst_ctor_checked_map(maybe_insist_on_defn::in,
    inst_ctor_defn_map::in, inst_ctor_defn_map::in,
    inst_ctor_checked_map::out,
    list(error_spec)::in, list(error_spec)::out) is det.

:- pred create_mode_ctor_checked_map(maybe_insist_on_defn::in,
    mode_ctor_defn_map::in, mode_ctor_defn_map::in,
    mode_ctor_checked_map::out,
    list(error_spec)::in, list(error_spec)::out) is det.

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

:- implementation.

:- import_module libs.
:- import_module libs.globals.
:- import_module mdbcomp.
:- import_module mdbcomp.builtin_modules.
:- import_module mdbcomp.sym_name.
:- import_module parse_tree.item_util.
:- import_module parse_tree.maybe_error.
:- import_module parse_tree.prog_data.
:- import_module parse_tree.prog_foreign_enum.
:- import_module parse_tree.prog_parse_tree.
:- import_module parse_tree.prog_type.
:- import_module parse_tree.prog_type_repn.

:- import_module bimap.
:- import_module map.
:- import_module maybe.
:- import_module one_or_more.
:- import_module pair.
:- import_module require.
:- import_module set.
:- import_module set_tree234.
:- import_module term.

%---------------------------------------------------------------------------%

create_type_ctor_checked_map(InsistOnDefn, IntTypeDefnMap, ImpTypeDefnMap,
        ImpForeignEnumMap, CheckedMap, !Specs) :-
    map.keys_as_set(IntTypeDefnMap, IntDefnTypeCtors),
    map.keys_as_set(ImpTypeDefnMap, ImpDefnTypeCtors),
    % Foreign_enum items are not allowed in interface sections.
    map.keys_as_set(ImpForeignEnumMap, ImpEnumTypeCtors),
    % This union operation depends on the type_ctors in all four maps
    % being qualified exactly the same way. We could require the type_ctor keys
    % to be all fully qualified or all fully unqualified; we chose the former.
    TypeCtors = set.to_sorted_list(
        set.union_list([
            IntDefnTypeCtors, ImpDefnTypeCtors, ImpEnumTypeCtors
        ])),
    list.foldl2(
        check_type_ctor_defns(InsistOnDefn, IntTypeDefnMap, ImpTypeDefnMap,
            ImpForeignEnumMap),
        TypeCtors, map.init, CheckedMap, !Specs),

    map.foldl(add_type_ctor_to_field_name_map, CheckedMap,
        map.init, FieldNameMap),
    map.foldl(report_any_duplicate_field_names, FieldNameMap, !Specs).

:- pred check_type_ctor_defns(maybe_insist_on_defn::in,
    type_ctor_defn_map::in, type_ctor_defn_map::in,
    type_ctor_foreign_enum_map::in, type_ctor::in,
    type_ctor_checked_map::in, type_ctor_checked_map::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_type_ctor_defns(InsistOnDefn,
        IntTypeDefnMap, ImpTypeDefnMap, ImpForeignEnumMap,
        TypeCtor, !TypeCtorCheckedMap, !Specs) :-
    % A given type constructor may have more than one definition in a module.
    % These definitions may be consistent with one another (such as a du
    % definition in Mercury and a foreign type definition in C), or
    % inconsistent with one another (such as an equivalence definition in
    % Mercury and a foreign_enum definition in Java).
    %
    % We start with the full set of definitions for a type constructor
    % (both type definitions and foreign enum definitions), which may contain
    % inconsistencies. We want to get to a set of definitions which are
    % not just consistent but have been *checked* to be consistent.
    %
    % The overall strategy of this predicate is to go from many possible
    % definitions of a type, which may be inconsistent with one another,
    % to smaller and smaller sets of definitions with fewer and fewer kinds
    % of inconsistencies being possible, until *no* kind of inconsistency
    % is left. At each step, we generate an error message for each definition
    % we discard.
    %
    % Note that an original inconsistent set of definitions may have
    % more than one consistent set of definitions within it. Our algorithm
    % has to pick one. Our approach is to keep definitions that are more
    % likely to be intended (e.g. people rarely define solver types by
    % accident) than others, which are more likely to be mistakes. For example,
    % cut-and-paste errors may yield foreign type definitions that specify
    % the wrong type name or the wrong foreign language.

    % The first stage is to look for and report inconsistencies that manifest
    % themselves as violations of the "at most one definition of TypeCtor
    % of a given kind in a given module section" rule.
    check_any_type_ctor_defns_for_duplicates(IntTypeDefnMap, TypeCtor,
        IntMaybeDefn, !Specs),
    check_any_type_ctor_defns_for_duplicates(ImpTypeDefnMap, TypeCtor,
        ImpMaybeDefn, !Specs),
    check_any_type_ctor_enums_for_duplicates(ImpForeignEnumMap, TypeCtor,
        ImpMaybeEnumCJCs, ImpLeftOverEnumsCJCs, !Specs),

    ( if map.search(ImpForeignEnumMap, TypeCtor, ImpEnumsCJCs) then
        ImpEnumsCJCs = c_java_csharp(ImpEnumsC, ImpEnumsJava, ImpEnumsCsharp),
        ImpEnums = ImpEnumsC ++ ImpEnumsJava ++ ImpEnumsCsharp
    else
        ImpEnums = []
    ),

    IntMaybeDefn = type_ctor_maybe_defn(
        IntAbstractSolverMaybeDefn0, IntSolverMaybeDefn,
        IntAbstractStdMaybeDefn, IntEqvMaybeDefn,
        IntDuMaybeDefn, IntSubMaybeDefn, IntMaybeDefnCJCs),
    ImpMaybeDefn = type_ctor_maybe_defn(
        ImpAbstractSolverMaybeDefn, ImpSolverMaybeDefn0,
        ImpAbstractStdMaybeDefn, ImpEqvMaybeDefn,
        ImpDuMaybeDefn, ImpSubMaybeDefn, ImpMaybeDefnCJCs),
    IntMaybeDefnCJCs = c_java_csharp(IntMaybeDefnC, IntMaybeDefnJava,
        IntMaybeDefnCsharp),
    ImpMaybeDefnCJCs = c_java_csharp(ImpMaybeDefnC, ImpMaybeDefnJava,
        ImpMaybeDefnCsharp),

    % Get the contexts of each different definition, in case we later
    % need to generate error messages for them. This is not very efficient
    % in terms of runtime, but the tiny increase in runtime is worth it
    % because it keeps the later code sane.
    %
    % The reason why delaying taking the contexts of these items until
    % we need them would lead to hard-to-read code is that these values
    % (IntAbstractSolverMaybeDefn, IntEqvMaybeDefn, IntDuMaybeDefn etc)
    % are of different types; specifically, they substitute different types
    % for the T in maybe(item_type_defn_info_general(T)). We therefore
    % cannot put them into a list without first doing something that
    % makes them have the same type. The obvious "something" is looking up
    % the context, which we do here.
    IntContextAbstractSolver = get_maybe_context(IntAbstractSolverMaybeDefn0),
    % IntContextSolver       = get_maybe_context(IntSolverMaybeDefn),
    IntContextAbstractStd    = get_maybe_context(IntAbstractStdMaybeDefn),
    IntContextEqv            = get_maybe_context(IntEqvMaybeDefn),
    IntContextDu             = get_maybe_context(IntDuMaybeDefn),
    IntContextSub            = get_maybe_context(IntSubMaybeDefn),
    ImpContextAbstractSolver = get_maybe_context(ImpAbstractSolverMaybeDefn),
    % ImpContextSolver       = get_maybe_context(ImpSolverMaybeDefn0),
    ImpContextAbstractStd    = get_maybe_context(ImpAbstractStdMaybeDefn),
    ImpContextEqv            = get_maybe_context(ImpEqvMaybeDefn),
    ImpContextDu             = get_maybe_context(ImpDuMaybeDefn),
    ImpContextSub            = get_maybe_context(ImpSubMaybeDefn),
    IntContextC              = get_maybe_context(IntMaybeDefnC),
    IntContextJava           = get_maybe_context(IntMaybeDefnJava),
    IntContextCsharp         = get_maybe_context(IntMaybeDefnCsharp),
    ImpContextC              = get_maybe_context(ImpMaybeDefnC),
    ImpContextJava           = get_maybe_context(ImpMaybeDefnJava),
    ImpContextCsharp         = get_maybe_context(ImpMaybeDefnCsharp),

    % Now we have at most one definition of each kind in each section,
    % and no definition in a section in which that kind is not allowed.
    % The general strategy forward is:
    %
    %   - first we look for a solver type definition
    %   - then we look for an equivalence type definition
    %   - then we look for a subtype definition
    %   - then we look for a (non-subtype) du type definition
    %   - then we look for a foreign type definition
    %   - then we look for an abstract solver type declaration
    %   - then we look for an abstract nonsolver type declaration
    %
    % If we find a definition of a given kind, then we generate an error
    % message for every other kind of definition that occurs later in
    % that list that is not compatible with the one we found. (There won't be
    % any definitions of a kind that is earlier in the list; if there were,
    % we wouldn't have gone on to test for the later kinds.)
    %
    % In each case, we look first in the interface, and then in the
    % implementation. Solver types are the one exception, because finding
    % a nonabstract definition in the interface section is an error.

    % Note that having both an abstract and a nonabstract definition
    % in the interface section is ok. We sometimes put an abstract declaration
    % in one interface section, which we publicize, and a non-abstract
    % definition in another interface section, which we don't publicize.

    report_any_nonabstract_solver_type_in_int(TypeCtor, IntSolverMaybeDefn,
        IntAbstractSolverMaybeDefn0, IntAbstractSolverMaybeDefn,
        ImpSolverMaybeDefn0, ImpSolverMaybeDefn, !Specs),
    ( if
        % Is there a solver type definition (not declaration) in the
        % implementation? There can't be a valid one in the interface.
        ImpSolverMaybeDefn = yes(ImpSolverDefn)
    then
        report_any_redundant_abstract_type_in_imp(TypeCtor, "implementation",
            ImpAbstractSolverMaybeDefn, !Specs),
        % Print error messages for every Std definition.
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                ImpSolverDefn ^ td_context, "solver type", "implementation",
                "definition", "declaration"),
            [IntContextAbstractStd, ImpContextAbstractStd],
            !Specs),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                ImpSolverDefn ^ td_context, "solver type", "implementation",
                "definition", "definition"),
            [IntContextEqv, IntContextDu, IntContextSub,
                IntContextC, IntContextJava, IntContextCsharp,
            ImpContextEqv, ImpContextDu, ImpContextSub,
                ImpContextC, ImpContextJava, ImpContextCsharp],
            !Specs),
        list.foldl(
            report_incompatible_foreign_enum(TypeCtor,
                ImpSolverDefn ^ td_context, "solver type", "implementation"),
            ImpEnums, !Specs),

        CheckedSolverDefn = solver_type_full(IntAbstractSolverMaybeDefn,
            ImpSolverDefn),
        SrcDefns = src_defns_solver(
            map_maybe(wrap_abstract_type_defn, IntAbstractSolverMaybeDefn),
            yes(wrap_solver_type_defn(ImpSolverDefn))),
        CheckedDefn = checked_defn_solver(CheckedSolverDefn, SrcDefns),
        map.det_insert(TypeCtor, CheckedDefn, !TypeCtorCheckedMap)
    else if
        % TypeCtor is NOT defined as a solver type.
        % Is there an equivalence type definition ...
        ( if
            % ... in the interface?
            IntEqvMaybeDefn = yes(IntEqvDefn)
        then
            % XXX CLEANUP Include ImpEqvMaybeDefn
            % in report_any_incompatible_type_decl_or_defn
            EqvDefn = IntEqvDefn,
            EqvWhere = "interface",
            Status = std_eqv_type_mer_exported,
            SrcDefns = src_defns_std([wrap_eqv_type_defn(IntEqvDefn)], [], [])
        else if
            % ... in the implementation?
            ImpEqvMaybeDefn = yes(ImpEqvDefn)
        then
            EqvDefn = ImpEqvDefn,
            EqvWhere = "implementation",
            (
                IntAbstractStdMaybeDefn = yes(AbstractStdDefn),
                Status = std_eqv_type_abstract_exported,
                SrcDefnsInt = [wrap_abstract_type_defn(AbstractStdDefn)]
            ;
                IntAbstractStdMaybeDefn = no,
                Status = std_eqv_type_all_private,
                SrcDefnsInt = []
            ),
            SrcDefnsImp = [wrap_eqv_type_defn(ImpEqvDefn)],
            SrcDefns = src_defns_std(SrcDefnsInt, SrcDefnsImp, [])
        else
            fail
        )
    then
        report_any_redundant_abstract_type_in_imp(TypeCtor, EqvWhere,
            ImpAbstractStdMaybeDefn, !Specs),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                EqvDefn ^ td_context, "equivalence type", EqvWhere,
                "definition", "solver type declaration"),
            [IntContextAbstractSolver, ImpContextAbstractSolver],
            !Specs),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                EqvDefn ^ td_context, "equivalence type", EqvWhere,
                "definition", "definition"),
            [IntContextDu, IntContextSub,
                IntContextC, IntContextJava, IntContextCsharp,
            ImpContextDu, ImpContextSub,
                ImpContextC, ImpContextJava, ImpContextCsharp],
            !Specs),
        list.foldl(
            report_incompatible_foreign_enum(TypeCtor,
                EqvDefn ^ td_context, "equivalence type", EqvWhere),
            ImpEnums, !Specs),
        CheckedStdDefn = std_mer_type_eqv(Status, EqvDefn),
        CheckedDefn = checked_defn_std(CheckedStdDefn, SrcDefns),
        map.det_insert(TypeCtor, CheckedDefn, !TypeCtorCheckedMap)
    else if
        % TypeCtor is NOT defined as a solver or equivalence type.
        % Is there a subtype definition ...
        ( if
            % ... in the interface?
            IntSubMaybeDefn = yes(IntSubDefn)
        then
            SubDefn = IntSubDefn,
            SubSection = ms_interface,
            SubWhere = "interface"
        else if
            % ... in the implementation?
            ImpSubMaybeDefn = yes(ImpSubDefn)
        then
            SubDefn = ImpSubDefn,
            SubSection = ms_implementation,
            SubWhere = "implementation"
        else
            fail
        )
    then
        report_any_redundant_abstract_type_in_imp(TypeCtor, SubWhere,
            ImpAbstractStdMaybeDefn, !Specs),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                SubDefn ^ td_context, "subtype", SubWhere,
                "definition", "solver type declaration"),
            [IntContextAbstractSolver, ImpContextAbstractSolver],
            !Specs),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                SubDefn ^ td_context, "subtype", SubWhere,
                "definition", "definition"),
            [IntContextDu, ImpContextDu],
            !Specs),

        % A subtype's representation is controlled entirely by the
        % representation of its base type. It cannot have its own
        % representation specifications for its constructors.
        ForeignDefns = get_maybe_type_defns([IntMaybeDefnC, ImpMaybeDefnC,
            IntMaybeDefnJava, ImpMaybeDefnJava,
            IntMaybeDefnCsharp, ImpMaybeDefnCsharp]),
        list.foldl(subtype_report_any_foreign_type(TypeCtor, SubDefn),
            ForeignDefns, !Specs),
        list.foldl(subtype_report_any_foreign_enum(TypeCtor, SubDefn),
            ImpEnums, !Specs),

        decide_subtype_status(TypeCtor, SubDefn, SubSection,
            IntAbstractStdMaybeDefn, Status, SrcDefnsInt, SrcDefnsImp),
        CheckedStdDefn = std_mer_type_subtype(Status, SubDefn),
        SrcDefns = src_defns_std(SrcDefnsInt, SrcDefnsImp, []),

        CheckedDefn = checked_defn_std(CheckedStdDefn, SrcDefns),
        map.det_insert(TypeCtor, CheckedDefn, !TypeCtorCheckedMap)
    else if
        % TypeCtor is NOT defined as a solver type, equivalence type,
        % or subtype. Is there a du type definition ...
        ( if
            % ... in the interface?
            IntDuMaybeDefn = yes(IntDuDefn)
        then
            DuDefn = IntDuDefn,
            DuSection = ms_interface,
            DuWhere = "interface"
        else if
            % ... in the implementation?
            ImpDuMaybeDefn = yes(ImpDuDefn)
        then
            DuDefn = ImpDuDefn,
            DuSection = ms_implementation,
            DuWhere = "implementation"
        else
            fail
        )
    then
        report_any_redundant_abstract_type_in_imp(TypeCtor, DuWhere,
            ImpAbstractStdMaybeDefn, !Specs),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                DuDefn ^ td_context, "discriminated union type", DuWhere,
                "definition", "solver type declaration"),
            [IntContextAbstractSolver, ImpContextAbstractSolver],
            !Specs),

        % XXX TYPE_REPN As part of switching over to this new system,
        % we will have to disable users' ability to specify MaybeDirectArgs
        % in source code.
        DetailsDu = DuDefn ^ td_ctor_defn,
        DetailsDu = type_details_du(OoMCtors, _MaybeCanonical,
            _MaybeDirectArgs),
        OoMCtors = one_or_more(HeadCtor, TailCtors),

        % All foreign language definitions must be in the same section,
        % and if TypeCtor has a Mercury definition (as opposed to just
        % a declaration), then they must also be in the same section
        % as the Mercury definition. We report violations of these rules
        % as errors.
        check_du_foreign_type_section(TypeCtor, DuDefn, DuSection,
            IntAbstractStdMaybeDefn, IntMaybeDefnCJCs, ImpMaybeDefnCJCs,
            Status, ChosenSectionCJCs, ChosenMaybeDefnCJCs,
            SrcDefnsDuInt, SrcDefnsDuImp, !Specs),
        ( if
            ctor_is_constant(HeadCtor, HeadName0),
            ctors_are_all_constants(TailCtors, TailNames0)
        then
            (
                TailNames0 = [],
                ( if non_sub_du_type_is_dummy(DetailsDu) then
                    MaybeOnlyConstants =
                        only_plain_constants(HeadName0, [])
                else
                    MaybeOnlyConstants = not_only_plain_constants
                )
            ;
                TailNames0 = [_ | _],
                ( if non_sub_du_type_is_enum(DetailsDu, _NumFunctors) then
                    MaybeOnlyConstants =
                        only_plain_constants(HeadName0, TailNames0)
                else
                    MaybeOnlyConstants = not_only_plain_constants
                )
            )
        else
            MaybeOnlyConstants = not_only_plain_constants
        ),
        (
            MaybeOnlyConstants = not_only_plain_constants,
            (
                ImpEnums = []
            ;
                ImpEnums = [_ | _],
                find_non_enum_ctors([HeadCtor | TailCtors], NonEnumSNAs),
                list.foldl(
                    non_enum_du_report_any_foreign_enum(TypeCtor, DuDefn,
                        NonEnumSNAs),
                    ImpEnums, !Specs)
            ),
            CheckedStdDefn =
                std_mer_type_du_not_all_plain_constants(Status, DuDefn,
                    ChosenMaybeDefnCJCs),
            ChosenMaybeDefnCJCs = c_java_csharp(ChosenMaybeDefnC,
                ChosenMaybeDefnJava, ChosenMaybeDefnCsharp),
            SrcForeignDefns = get_maybe_type_defns([ChosenMaybeDefnC,
                ChosenMaybeDefnJava, ChosenMaybeDefnCsharp]),
            SrcForeignEnums = []
        ;
            MaybeOnlyConstants = only_plain_constants(HeadName, TailNames),
            decide_du_repn_foreign_only_constants(TypeCtor,
                [HeadName | TailNames], ChosenMaybeDefnCJCs,
                ImpMaybeEnumCJCs, ImpLeftOverEnumsCJCs,
                MaybeDefnOrEnumCJCs, SrcForeignDefns, SrcForeignEnums,
                !Specs),
            CheckedStdDefn = std_mer_type_du_all_plain_constants(Status,
                DuDefn, HeadName, TailNames, MaybeDefnOrEnumCJCs)
        ),
        (
            ChosenSectionCJCs = ms_interface,
            SrcDefnsInt = SrcDefnsDuInt ++
                list.map(wrap_foreign_type_defn, SrcForeignDefns),
            SrcDefnsImp = SrcDefnsDuImp
        ;
            ChosenSectionCJCs = ms_implementation,
            SrcDefnsInt = SrcDefnsDuInt,
            SrcDefnsImp = SrcDefnsDuImp ++
                list.map(wrap_foreign_type_defn, SrcForeignDefns)
        ),
        SrcDefns = src_defns_std(SrcDefnsInt, SrcDefnsImp, SrcForeignEnums),

        CheckedDefn = checked_defn_std(CheckedStdDefn, SrcDefns),
        map.det_insert(TypeCtor, CheckedDefn, !TypeCtorCheckedMap)
    else if
        % TypeCtor is NOT defined as a solver, equivalence or du type.
        % Is there a foreign type definition in the interface or
        % in the implementation?
        ( IntMaybeDefnC = yes(_)
        ; IntMaybeDefnJava = yes(_)
        ; IntMaybeDefnCsharp = yes(_)
        ; ImpMaybeDefnC = yes(_)
        ; ImpMaybeDefnJava = yes(_)
        ; ImpMaybeDefnCsharp = yes(_)
        )
    then
        IntForeignContexts = get_maybe_type_defn_contexts([
            IntMaybeDefnC, IntMaybeDefnJava, IntMaybeDefnCsharp]),
        list.sort(IntForeignContexts, SortedIntForeignContexts),
        (
            SortedIntForeignContexts = [FirstForeignContext | _],
            ForeignWhere = "interface"
        ;
            SortedIntForeignContexts = [],
            ImpForeignContexts = get_maybe_type_defn_contexts([
                ImpMaybeDefnC, ImpMaybeDefnJava, ImpMaybeDefnCsharp]),
            list.sort(ImpForeignContexts, SortedImpForeignContexts),
            FirstForeignContext = list.det_head(SortedImpForeignContexts),
            ForeignWhere = "implementation"
        ),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                FirstForeignContext, "foreign type", ForeignWhere,
                "definition", "solver type declaration"),
            [IntContextAbstractSolver, ImpContextAbstractSolver],
            !Specs),
        list.foldl(
            report_incompatible_foreign_enum(TypeCtor,
                FirstForeignContext, "foreign type", ForeignWhere),
            ImpEnums, !Specs),

        decide_only_foreign_type_section(TypeCtor,
            IntAbstractSolverMaybeDefn, ImpAbstractSolverMaybeDefn,
            IntAbstractStdMaybeDefn, ImpAbstractStdMaybeDefn,
            IntMaybeDefnCJCs, ImpMaybeDefnCJCs,
            Status, ChosenAbstractStdDefn, ChosenMaybeDefnCJCs, SrcDefns,
            !Specs),

        CheckedStdDefn = std_mer_type_abstract(Status,
            ChosenAbstractStdDefn, ChosenMaybeDefnCJCs),
        CheckedDefn = checked_defn_std(CheckedStdDefn, SrcDefns),
        map.det_insert(TypeCtor, CheckedDefn, !TypeCtorCheckedMap)
    else if
        % TypeCtor is NOT defined as a solver, equivalence, du or foreign type.
        % Does it have a declaration as a solver type ...
        ( if
            % ... in the interface?
            IntAbstractSolverMaybeDefn = yes(IntAbstractSolverDefn)
        then
            AbstractSolverDefn = IntAbstractSolverDefn,
            AbstractSolverWhere = "interface",
            Status = abstract_solver_type_exported,
            SrcDefnsInt = yes(wrap_abstract_type_defn(IntAbstractSolverDefn)),
            SrcDefnsImp = no
        else if
            % ... in the implementation?
            ImpAbstractSolverMaybeDefn = yes(ImpAbstractSolverDefn)
        then
            AbstractSolverDefn = ImpAbstractSolverDefn,
            AbstractSolverWhere = "implementation",
            Status = abstract_solver_type_private,
            SrcDefnsInt = no,
            SrcDefnsImp = yes(wrap_abstract_type_defn(ImpAbstractSolverDefn))
        else
            fail
        )
    then
        maybe_report_declared_but_undefined_type(InsistOnDefn, TypeCtor,
            AbstractSolverDefn, !Specs),
        list.foldl(
            report_any_incompatible_type_decl_or_defn(TypeCtor,
                AbstractSolverDefn ^ td_context, "solver type",
                AbstractSolverWhere, "declaration", "declaration"),
            [IntContextAbstractStd, ImpContextAbstractStd],
            !Specs),
        list.foldl(
            report_incompatible_foreign_enum(TypeCtor,
                AbstractSolverDefn ^ td_context, "solver type",
                AbstractSolverWhere),
            ImpEnums, !Specs),
        % XXX Should we report any foreign enums using this code?
        % It would say that TypeCtor is not defined, while the code
        % above says it is a solver type.
        % list.foldl(
        %   report_any_foreign_enum_for_undefined_type(TypeCtor,
        %       "undefined"),
        %   [ImpMaybeEnumC, ImpMaybeEnumJava, ImpMaybeEnumCsharp],
        %   !Specs),
        CheckedSolverDefn = solver_type_abstract(Status, AbstractSolverDefn),
        SrcDefns = src_defns_solver(SrcDefnsInt, SrcDefnsImp),
        CheckedDefn = checked_defn_solver(CheckedSolverDefn, SrcDefns),
        map.det_insert(TypeCtor, CheckedDefn, !TypeCtorCheckedMap)
    else if
        % TypeCtor is NOT defined as a solver, equivalence, du or foreign type,
        % and it is NOT declared as a solver type.
        % Does it have a declaration as a non-solver type ...
        ( if
            % ... in the interface?
            IntAbstractStdMaybeDefn = yes(IntAbstractStdDefn)
        then
            % If an abstract exported du type is a dummy type, notag type
            % or an enum type, then the compiler will put into the
            % automatically generated .int/.int2 file for its module
            % both a plain abstract type_defn item in the interface section
            % and *another* type_defn item in the implementation section
            % that is also abstract but nevertheless carries more information,
            % such as abstract_type_fits_in_n_bits(N).
            (
                ImpAbstractStdMaybeDefn = yes(ImpAbstractStdDefn),
                AbstractStdDefn = ImpAbstractStdDefn,
                SrcDefnsInt = [wrap_abstract_type_defn(ImpAbstractStdDefn)]
            ;
                ImpAbstractStdMaybeDefn = no,
                AbstractStdDefn = IntAbstractStdDefn,
                SrcDefnsInt = [wrap_abstract_type_defn(IntAbstractStdDefn)]
            ),
            Status = std_abs_type_abstract_exported,
            SrcDefnsImp = []
        else if
            % ... in the implementation?
            ImpAbstractStdMaybeDefn = yes(ImpAbstractStdDefn)
        then
            AbstractStdDefn = ImpAbstractStdDefn,
            Status = std_abs_type_all_private,
            SrcDefnsInt = [],
            SrcDefnsImp = [wrap_abstract_type_defn(ImpAbstractStdDefn)]
        else
            fail
        )
    then
        maybe_report_declared_but_undefined_type(InsistOnDefn, TypeCtor,
            AbstractStdDefn, !Specs),
        list.foldl(
            report_foreign_enum_for_undefined_type(TypeCtor, "undefined"),
            ImpEnums, !Specs),
        MaybeCJCs = c_java_csharp(no, no, no),
        CheckedStdDefn = std_mer_type_abstract(Status,
            AbstractStdDefn, MaybeCJCs),
        SrcDefns = src_defns_std(SrcDefnsInt, SrcDefnsImp, []),
        CheckedDefn = checked_defn_std(CheckedStdDefn, SrcDefns),
        map.det_insert(TypeCtor, CheckedDefn, !TypeCtorCheckedMap)
    else
        % TypeCtor is NOT defined as a solver, equivalence, du or foreign type,
        % and it is NOT declared either as a solver or as a nonsolver type.
        % This means it has no type definition whatsoever. The only way
        % we can get here is if it has any foreign enum definitions.
        list.foldl(
            report_foreign_enum_for_undefined_type(TypeCtor, "undeclared"),
            ImpEnums, !Specs)
        % There is no actual definition to add to !TypeCtorCheckedMap.
    ).

:- func get_maybe_context(maybe(item_type_defn_info_general(T)))
    = maybe(prog_context).

get_maybe_context(no) = no.
get_maybe_context(yes(TypeDefnInfo)) = yes(TypeDefnInfo ^ td_context).

:- pred check_du_foreign_type_section(type_ctor::in,
    item_type_defn_info_du::in, module_section::in,
    maybe(item_type_defn_info_abstract)::in,
    c_j_cs_maybe_defn::in, c_j_cs_maybe_defn::in,
    std_du_type_status::out, module_section::out, c_j_cs_maybe_defn::out,
    list(item_type_defn_info)::out, list(item_type_defn_info)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_du_foreign_type_section(TypeCtor, DuDefn, DuSection,
        IntAbstractStdMaybeDefn, IntMaybeDefnCJCs, ImpMaybeDefnCJCs,
        Status, ChosenSectionCJCs, ChosenMaybeDefnCJCs,
        SrcDefnsDuInt, SrcDefnsDuImp, !Specs) :-
    IntMaybeDefnCJCs = c_java_csharp(IntMaybeDefnC, IntMaybeDefnJava,
        IntMaybeDefnCsharp),
    ImpMaybeDefnCJCs = c_java_csharp(ImpMaybeDefnC, ImpMaybeDefnJava,
        ImpMaybeDefnCsharp),
    IntDefnsCJCs = get_maybe_type_defns([IntMaybeDefnC, IntMaybeDefnJava,
        IntMaybeDefnCsharp]),
    ImpDefnsCJCs = get_maybe_type_defns([ImpMaybeDefnC, ImpMaybeDefnJava,
        ImpMaybeDefnCsharp]),
    (
        DuSection = ms_interface,
        list.foldl(
            report_mer_foreign_section_mismatch(TypeCtor,
                "definition", "interface", DuDefn),
            ImpDefnsCJCs, !Specs),
        Status = std_du_type_mer_ft_exported,
        ChosenSectionCJCs = ms_interface,
        ChosenMaybeDefnCJCs = IntMaybeDefnCJCs,
        SrcDefnsDuInt = [wrap_du_type_defn(DuDefn)],
        SrcDefnsDuImp = []
    ;
        DuSection = ms_implementation,
        list.foldl(
            report_mer_foreign_section_mismatch(TypeCtor,
                "definition", "implementation", DuDefn),
            IntDefnsCJCs, !Specs),
        (
            IntAbstractStdMaybeDefn = yes(IntAbstractStdDefn),
            Status = std_du_type_abstract_exported,
            SrcDefnsDuInt = [wrap_abstract_type_defn(IntAbstractStdDefn)]
        ;
            IntAbstractStdMaybeDefn = no,
            Status = std_du_type_all_private,
            SrcDefnsDuInt = []
        ),
        ChosenSectionCJCs = ms_implementation,
        ChosenMaybeDefnCJCs = ImpMaybeDefnCJCs,
        SrcDefnsDuImp = [wrap_du_type_defn(DuDefn)]
    ).

:- pred decide_subtype_status(type_ctor::in,
    item_type_defn_info_sub::in, module_section::in,
    maybe(item_type_defn_info_abstract)::in, std_subtype_status::out,
    list(item_type_defn_info)::out, list(item_type_defn_info)::out) is det.

decide_subtype_status(_TypeCtor, SubDefn, SubSection, IntAbstractStdMaybeDefn,
        Status, SrcDefnsInt, SrcDefnsImp) :-
    (
        SubSection = ms_interface,
        Status = std_sub_type_mer_exported,
        SrcDefnsInt = [wrap_sub_type_defn(SubDefn)],
        SrcDefnsImp = []
    ;
        SubSection = ms_implementation,
        (
            IntAbstractStdMaybeDefn = yes(IntAbstractStdDefn),
            Status = std_sub_type_abstract_exported,
            SrcDefnsInt = [wrap_abstract_type_defn(IntAbstractStdDefn)]
        ;
            IntAbstractStdMaybeDefn = no,
            Status = std_sub_type_all_private,
            SrcDefnsInt = []
        ),
        SrcDefnsImp = [wrap_sub_type_defn(SubDefn)]
    ).

:- pred decide_only_foreign_type_section(type_ctor::in,
    maybe(item_type_defn_info_abstract)::in,
    maybe(item_type_defn_info_abstract)::in,
    maybe(item_type_defn_info_abstract)::in,
    maybe(item_type_defn_info_abstract)::in,
    c_j_cs_maybe_defn::in, c_j_cs_maybe_defn::in,
    std_abs_type_status::out,
    item_type_defn_info_abstract::out, c_j_cs_maybe_defn::out,
    src_defns_std::out, list(error_spec)::in, list(error_spec)::out) is det.

decide_only_foreign_type_section(TypeCtor,
        IntAbsSolverMaybeDefn, ImpAbsSolverMaybeDefn,
        IntAbsStdMaybeDefn, ImpAbsStdMaybeDefn,
        IntMaybeDefnCJCs, ImpMaybeDefnCJCs,
        Status, AbsStdDefn, ChosenMaybeDefnCJCs, SrcDefns, !Specs) :-
    IntMaybeDefnCJCs = c_java_csharp(IntMaybeDefnC, IntMaybeDefnJava,
        IntMaybeDefnCsharp),
    ImpMaybeDefnCJCs = c_java_csharp(ImpMaybeDefnC, ImpMaybeDefnJava,
        ImpMaybeDefnCsharp),
    IntDefnsCJCs = get_maybe_type_defns([IntMaybeDefnC, IntMaybeDefnJava,
        IntMaybeDefnCsharp]),
    ImpDefnsCJCs = get_maybe_type_defns([ImpMaybeDefnC, ImpMaybeDefnJava,
        ImpMaybeDefnCsharp]),
    (
        IntAbsStdMaybeDefn = yes(IntAbsStdDefn),
        AbsStdDefn = IntAbsStdDefn,
        IntContexts = get_maybe_type_defn_contexts([IntMaybeDefnC,
            IntMaybeDefnJava, IntMaybeDefnCsharp]),
        list.sort(IntContexts, SortedIntContexts),
        (
            SortedIntContexts = [FirstIntContext | _],
            Status = std_abs_type_ft_exported,
            list.foldl(
                foreign_int_report_any_foreign_defn_in_imp(TypeCtor,
                    FirstIntContext),
                ImpDefnsCJCs, !Specs),
            ChosenMaybeDefnCJCs = IntMaybeDefnCJCs,
            SrcDefnsInt = [wrap_abstract_type_defn(IntAbsStdDefn) |
                list.map(wrap_foreign_type_defn, IntDefnsCJCs)],
            SrcDefnsImp = []
        ;
            SortedIntContexts = [],
            Status = std_abs_type_abstract_exported,
            ChosenMaybeDefnCJCs = ImpMaybeDefnCJCs,
            SrcDefnsInt = [wrap_abstract_type_defn(IntAbsStdDefn)],
            SrcDefnsImp = list.map(wrap_foreign_type_defn, ImpDefnsCJCs)
        )
    ;
        IntAbsStdMaybeDefn = no,
        Status = std_abs_type_all_private,
        (
            ImpAbsStdMaybeDefn = yes(ImpAbsStdDefn),
            AbsStdDefn = ImpAbsStdDefn,
            list.foldl(
                report_mer_foreign_section_mismatch(TypeCtor,
                    "declaration", "implementation", ImpAbsStdDefn),
                IntDefnsCJCs, !Specs)
        ;
            ImpAbsStdMaybeDefn = no,
            IntImpDefnsCJCs = IntDefnsCJCs ++ ImpDefnsCJCs,
            ( if
                ( IntAbsSolverMaybeDefn = yes(_)
                ; ImpAbsSolverMaybeDefn = yes(_)
                )
            then
                % Don't report this foreign type as being for a type_ctor
                % that has no declaration, since it *does* have a declaration;
                % it just declares the type_ctor to be a *solver* type,
                % which cannot have foreign type definitions.
                %
                % Our caller will already have reported this foreign type
                % definition as being incompatible with the solver type
                % declaration.
                true
            else
                list.foldl(
                    report_any_foreign_type_without_declaration(TypeCtor),
                    IntImpDefnsCJCs, !Specs)
            ),
            % IntImpDefnsCJCs cannot be empty because our caller calls us
            % only if at least one of the foreign language definitions
            % is yes(_). This *also* means that we will generate at least one
            % error message above.
            FirstDefn = list.det_head(IntImpDefnsCJCs),
            % Pretend that there *was* an abstract declaration of the type,
            % since it is at least 99% likely that the programmer's response
            % to the above error message will be to add one. Manufacturing
            % this item out of thin air will suppress any error messages
            % that would be inappropriate in the presence of this repair,
            % but they won't lead to any problems, since the presence of
            % the error means that we won't actually do anything with the
            % typr_ctor_checked_defn we are constructing.
            AbsStdDefn = FirstDefn ^ td_ctor_defn := abstract_type_general
        ),
        ChosenMaybeDefnCJCs = ImpMaybeDefnCJCs,
        SrcDefnsInt = [],
        SrcDefnsImp = [wrap_abstract_type_defn(AbsStdDefn) |
            list.map(wrap_foreign_type_defn, ImpDefnsCJCs)]
    ),
    SrcDefns = src_defns_std(SrcDefnsInt, SrcDefnsImp, []).

:- pred decide_du_repn_foreign_only_constants(type_ctor::in,
    list(string)::in, c_j_cs_maybe_defn::in,
    c_j_cs_maybe_enum::in, c_j_cs_enums::in,
    c_j_cs_maybe_defn_or_enum::out,
    list(item_type_defn_info_foreign)::out, list(item_foreign_enum_info)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

decide_du_repn_foreign_only_constants(TypeCtor, CtorNames,
        MaybeDefnCJCs, MaybeEnumCJCs, LeftOverEnumsCJCs,
        MaybeDefnOrEnumCJCs, SrcForeignDefns, SrcForeignEnums, !Specs) :-
    % If TypeCtor has more than one enum definition for a given foreign
    % language, we pick on to return in MaybeEnumCJCs, but we return
    % all the others as well in LeftOverEnumsCJCs so that our caller
    % can generate error messages for them where required.
    set_tree234.list_to_set(CtorNames, CtorNamesSet),
    MaybeDefnCJCs = c_java_csharp(MaybeDefnC, MaybeDefnJava, MaybeDefnCsharp),
    MaybeEnumCJCs = c_java_csharp(MaybeEnumC, MaybeEnumJava, MaybeEnumCsharp),
    LeftOverEnumsCJCs = c_java_csharp(LeftOverEnumsC, LeftOverEnumsJava,
        LeftOverEnumsCsharp),

    decide_du_repn_foreign_only_constants_lang(TypeCtor,
        CtorNames, CtorNamesSet, MaybeDefnC,
        MaybeEnumC, LeftOverEnumsC, MaybeDefnOrEnumC,
        SrcForeignDefnsC, SrcForeignEnumsC, !Specs),
    decide_du_repn_foreign_only_constants_lang(TypeCtor,
        CtorNames, CtorNamesSet, MaybeDefnJava,
        MaybeEnumJava, LeftOverEnumsJava, MaybeDefnOrEnumJava,
        SrcForeignDefnsJava, SrcForeignEnumsJava, !Specs),
    decide_du_repn_foreign_only_constants_lang(TypeCtor,
        CtorNames, CtorNamesSet, MaybeDefnCsharp,
        MaybeEnumCsharp, LeftOverEnumsCsharp, MaybeDefnOrEnumCsharp,
        SrcForeignDefnsCsharp, SrcForeignEnumsCsharp, !Specs),

    SrcForeignDefns =
        SrcForeignDefnsC ++ SrcForeignDefnsJava ++ SrcForeignDefnsCsharp,
    SrcForeignEnums =
        SrcForeignEnumsC ++ SrcForeignEnumsJava ++ SrcForeignEnumsCsharp,
    MaybeDefnOrEnumCJCs = c_java_csharp(MaybeDefnOrEnumC, MaybeDefnOrEnumJava,
        MaybeDefnOrEnumCsharp).

:- pred decide_du_repn_foreign_only_constants_lang(type_ctor::in,
    list(string)::in, set_tree234(string)::in,
    maybe(item_type_defn_info_foreign)::in,
    maybe(item_foreign_enum_info)::in, list(item_foreign_enum_info)::in,
    maybe(foreign_type_or_enum)::out,
    list(item_type_defn_info_foreign)::out,
    list(item_foreign_enum_info)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

decide_du_repn_foreign_only_constants_lang(TypeCtor, CtorNames, CtorNamesSet,
        MaybeDefn, MaybeEnum, LeftOverEnums, MaybeDefnOrEnum,
        SrcForeignDefns, SrcForeignEnums, !Specs) :-
    (
        MaybeEnum = no,
        expect(unify(LeftOverEnums, []), $pred,
            "MaybeEnum = no but LeftOverEnums != []"),
        MaybeCheckedForeignEnum = no
    ;
        MaybeEnum = yes(Enum),
        build_mercury_foreign_enum_map(TypeCtor, CtorNames, CtorNamesSet,
            Enum, HeadMaybeCFE),
        list.map(
            build_mercury_foreign_enum_map(TypeCtor, CtorNames, CtorNamesSet),
            LeftOverEnums, TailMaybeCFEs),
        pick_first_error_free_enum_if_any([HeadMaybeCFE | TailMaybeCFEs],
            MaybeCheckedForeignEnum, CFESpecs),
        !:Specs = CFESpecs ++ !.Specs
    ),
    (
        MaybeDefn = yes(Defn),
        MaybeDefnOrEnum = yes(foreign_type_or_enum_type(Defn)),
        SrcForeignDefns = [Defn],
        SrcForeignEnums = []
    ;
        MaybeDefn = no,
        (
            MaybeCheckedForeignEnum = no,
            MaybeDefnOrEnum = no,
            SrcForeignDefns = [],
            SrcForeignEnums = []
        ;
            MaybeCheckedForeignEnum = yes(CheckedForeignEnum),
            MaybeDefnOrEnum =
                yes(foreign_type_or_enum_enum(CheckedForeignEnum)),
            CheckedForeignEnum = checked_foreign_enum(EnumInfo, _),
            SrcForeignDefns = [],
            SrcForeignEnums = [EnumInfo]
        )
    ).

:- pred pick_first_error_free_enum_if_any(
    list(maybe1(checked_foreign_enum))::in,
    maybe(checked_foreign_enum)::out, list(error_spec)::out) is det.

pick_first_error_free_enum_if_any([], no, []).
pick_first_error_free_enum_if_any([HeadMaybeCFE | TailMaybeCFEs],
        MaybeCFE, Specs) :-
    pick_first_error_free_enum_if_any(TailMaybeCFEs,
        TailMaybeCFE, TailSpecs),
    (
        HeadMaybeCFE = ok1(CFE),
        MaybeCFE = yes(CFE),
        Specs = TailSpecs
    ;
        HeadMaybeCFE = error1(HeadSpecs),
        MaybeCFE = TailMaybeCFE,
        Specs = HeadSpecs ++ TailSpecs
    ).

:- pred build_mercury_foreign_enum_map(type_ctor::in,
    list(string)::in, set_tree234(string)::in,
    item_foreign_enum_info::in,
    maybe1(checked_foreign_enum)::out) is det.

build_mercury_foreign_enum_map(TypeCtor, CtorNames, CtorNamesSet,
        ForeignEnum, MaybeCheckedForeignEnum) :-
    ForeignEnum = item_foreign_enum_info(_Lang, _TypeCtor, MercuryForeignOoM,
        Context, _SeqNum),
    MercuryForeignAL = one_or_more_to_list(MercuryForeignOoM),
    ContextPieces = [words("In"), pragma_decl("foreign_enum"),
        words("declaration for type"), unqual_type_ctor(TypeCtor),
        suffix(":"), nl],

    TypeCtor = type_ctor(TypeCtorSymName, _),
    det_sym_name_get_module_name(TypeCtorSymName, TypeCtorModuleName),

    build_ctor_name_to_foreign_name_map(for_foreign_enum,
        Context, ContextPieces, TypeCtorModuleName, CtorNamesSet,
        MercuryForeignAL, MercuryForeignBiMap, [], Specs),
    (
        Specs = [],
        bimap.apply_forward_map_to_list(MercuryForeignBiMap, CtorNames,
            ForeignNames),
        (
            ForeignNames = [],
            % There should be exactly one ForeignName for every CtorName.
            unexpected($pred, "enum type with no constructors")
        ;
            ForeignNames = [HeadForeignName | TailForeignNames],
            ForeignNameOoM = one_or_more(HeadForeignName, TailForeignNames)
        ),
        CheckedForeignEnum = checked_foreign_enum(ForeignEnum, ForeignNameOoM),
        MaybeCheckedForeignEnum = ok1(CheckedForeignEnum)
    ;
        Specs = [_ | _],
        MaybeCheckedForeignEnum = error1(Specs)
    ).

:- pred find_non_enum_ctors(list(constructor)::in,
    list(sym_name_arity)::out) is det.

find_non_enum_ctors([], []).
find_non_enum_ctors([Ctor | Ctors], NonEnumSNAs) :-
    find_non_enum_ctors(Ctors, NonEnumSNAsTail),
    CtorSymName = Ctor ^ cons_name,
    CtorArity = Ctor ^ cons_num_args,
    ( if CtorArity = 0 then
        NonEnumSNAs = NonEnumSNAsTail
    else
        CtorSNA = sym_name_arity(CtorSymName, CtorArity),
        NonEnumSNAs = [CtorSNA | NonEnumSNAsTail]
    ).

:- pred non_enum_du_report_any_foreign_enum(type_ctor::in,
    item_type_defn_info_du::in, list(sym_name_arity)::in,
    item_foreign_enum_info::in,
    list(error_spec)::in, list(error_spec)::out) is det.

non_enum_du_report_any_foreign_enum(TypeCtor, DuDefn, NonEnumSNAs,
        Enum, !Specs) :-
    (
        NonEnumSNAs = [],
        CtorPieces = []
    ;
        NonEnumSNAs = [_ | _],
        NonEnumSNAPieces = list.map(func(SNA) = unqual_sym_name_arity(SNA),
            NonEnumSNAs),
        SNAPieces = piece_list_to_color_pieces(color_incorrect, "and",
            [suffix(".")], NonEnumSNAPieces),
        ItHasThese = choose_number(NonEnumSNAs,
            words("It has this non-zero arity constructor:"),
            words("It has these non-zero arity constructors:")),
        CtorPieces = [ItHasThese, nl_indent_delta(1)] ++ SNAPieces ++
            [nl_indent_delta(-1)]
    ),
    EnumPieces = [words("Error: the Mercury definition of")] ++
        color_as_subject([unqual_type_ctor(TypeCtor)]) ++
        [words("is not an enumeration type, so")] ++
        color_as_incorrect([words("there must not be any"),
        pragma_decl("foreign_enum"), words("declarations for it.")]) ++ [nl],
    DuPieces = [words("That Mercury definition is here."), nl | CtorPieces],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(Enum ^ fe_context, EnumPieces),
        msg(DuDefn ^ td_context, DuPieces)]),
    !:Specs = [Spec | !.Specs].

:- pred subtype_report_any_foreign_type(type_ctor::in,
    item_type_defn_info_sub::in, item_type_defn_info_foreign::in,
    list(error_spec)::in, list(error_spec)::out) is det.

subtype_report_any_foreign_type(TypeCtor, SubTypeDefn, Foreign, !Specs) :-
    ForeignPieces = [words("Error:")] ++
        color_as_subject([unqual_type_ctor(TypeCtor)]) ++
        [words("is defined to be a subtype, so")] ++
        color_as_incorrect([words("there must not be any"),
        pragma_decl("foreign_type"), words("declarations for it.")]) ++ [nl],
    SubTypePieces = [words("That subtype definition is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(Foreign ^ td_context, ForeignPieces),
        msg(SubTypeDefn ^ td_context, SubTypePieces)]),
    !:Specs = [Spec | !.Specs].

:- pred subtype_report_any_foreign_enum(type_ctor::in,
    item_type_defn_info_sub::in, item_foreign_enum_info::in,
    list(error_spec)::in, list(error_spec)::out) is det.

subtype_report_any_foreign_enum(TypeCtor, SubTypeDefn, Enum, !Specs) :-
    EnumPieces = [words("Error:")] ++
        color_as_subject([unqual_type_ctor(TypeCtor)]) ++
        [words("is defined to be a subtype, so")] ++
        color_as_incorrect([words("there must not be any"),
        pragma_decl("foreign_enum"), words("declarations for it.")]) ++ [nl],
    SubTypePieces = [words("That subtype definition is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(Enum ^ fe_context, EnumPieces),
        msg(SubTypeDefn ^ td_context, SubTypePieces)]),
    !:Specs = [Spec | !.Specs].

:- pred report_mer_foreign_section_mismatch(type_ctor::in,
    string::in, string::in,
    item_type_defn_info_general(T)::in, item_type_defn_info_foreign::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_mer_foreign_section_mismatch(TypeCtor, DeclOrDefn, MerSection, MerDefn,
        ForeignDefn, !Specs) :-
    ForeignPieces = [words("Error: since the Mercury"), words(DeclOrDefn),
        words("of")] ++ color_as_subject([unqual_type_ctor(TypeCtor)]) ++
        color_as_correct([words("is in the"), words(MerSection),
            words("section,")]) ++
        [words("any foreign type definition for it")] ++
        color_as_incorrect([words("must be"), words("in the"),
            words(MerSection), words("section as well.")]) ++
        [nl],
    DuPieces = [words("That Mercury"), words(DeclOrDefn),
        words("is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(ForeignDefn ^ td_context, ForeignPieces),
        msg(MerDefn ^ td_context, DuPieces)]),
    !:Specs = [Spec | !.Specs].

:- pred report_any_foreign_type_without_declaration(type_ctor::in,
    item_type_defn_info_foreign::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_any_foreign_type_without_declaration(TypeCtor, ForeignDefn, !Specs) :-
    Pieces = [words("Error: a"),
        pragma_decl("foreign_type"), words("definition for")] ++
        color_as_subject([unqual_type_ctor(TypeCtor)]) ++
        color_as_incorrect([words("without either"),
            words("a Mercury definition or a Mercury declaration")]) ++
        [words("for"), unqual_type_ctor(TypeCtor), suffix("."), nl],
    Spec = spec($pred, severity_error, phase_tim_check_invalid_type,
        ForeignDefn ^ td_context, Pieces),
    !:Specs = [Spec | !.Specs].

:- pred foreign_int_report_any_foreign_defn_in_imp(type_ctor::in,
    prog_context::in, item_type_defn_info_foreign::in,
    list(error_spec)::in, list(error_spec)::out) is det.

foreign_int_report_any_foreign_defn_in_imp(TypeCtor, IntForeignContext,
        ImpForeignDefn, !Specs) :-
    ImpPieces = [words("Error: since some foreign language definition"),
        words("of")] ++ color_as_subject([unqual_type_ctor(TypeCtor)]) ++
        [words("is in the interface section,")] ++
        color_as_incorrect([words("all other foreign language definitions"),
            words("for it must be in the interface section as well.")]) ++
        [nl],
    IntPieces = [words("That foreign definition in the interface"),
        words("is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(ImpForeignDefn ^ td_context, ImpPieces),
        msg(IntForeignContext, IntPieces)]),
    !:Specs = [Spec | !.Specs].

:- pred report_any_nonabstract_solver_type_in_int(type_ctor::in,
    maybe(item_type_defn_info_solver)::in,
    maybe(item_type_defn_info_abstract)::in,
    maybe(item_type_defn_info_abstract)::out,
    maybe(item_type_defn_info_solver)::in,
    maybe(item_type_defn_info_solver)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

report_any_nonabstract_solver_type_in_int(TypeCtor, IntMaybeDefn,
        IntMaybeAbstractDefn0, IntMaybeAbstractDefn,
        ImpMaybeDefn0, ImpMaybeDefn, !Specs) :-
    (
        IntMaybeDefn = no,
        IntMaybeAbstractDefn = IntMaybeAbstractDefn0,
        ImpMaybeDefn = ImpMaybeDefn0
    ;
        IntMaybeDefn = yes(IntDefn),
        Pieces = [words("Error: a solver type such as")] ++
            color_as_subject([unqual_type_ctor(TypeCtor)]) ++
            [words("may be defined (as opposed to declared)")] ++
            color_as_incorrect(
                [words("only in the implementation section.")]) ++
            [nl],
        Spec = spec($pred, severity_error, phase_tim_check,
            IntDefn ^ td_context, Pieces),
        !:Specs = [Spec | !.Specs],
        % To avoid avalanche errors about this solver type being unknown,
        % ensure that it has a declaration.
        (
            IntMaybeAbstractDefn0 = no,
            IntAbstractDefn = IntDefn ^ td_ctor_defn := abstract_solver_type,
            IntMaybeAbstractDefn = yes(IntAbstractDefn)
        ;
            IntMaybeAbstractDefn0 = yes(_),
            IntMaybeAbstractDefn = IntMaybeAbstractDefn0
        ),
        % However, if there is a declaration in the interface,
        % without an actual definition in the implementation section,
        % that would also get an error message.
        (
            ImpMaybeDefn0 = no,
            ImpMaybeDefn = yes(IntDefn)
        ;
            ImpMaybeDefn0 = yes(_),
            ImpMaybeDefn0 = ImpMaybeDefn
        )
    ).

:- pred report_any_redundant_abstract_type_in_imp(type_ctor::in, string::in,
    maybe(item_type_defn_info_abstract)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_any_redundant_abstract_type_in_imp(TypeCtor, Section,
        MaybeImpAbstractDefn, !Specs) :-
    (
        MaybeImpAbstractDefn = no
    ;
        MaybeImpAbstractDefn = yes(ImpAbstractDefn),
        Pieces = [words("Warning: this declaration of")] ++
            color_as_subject([unqual_type_ctor(TypeCtor)]) ++
            [words("is")] ++ color_as_incorrect([words("redundant,")]) ++
            [words("since the type has a definition in the"),
            words(Section), words("section."), nl],
        Spec = spec($pred, severity_warning, phase_tim_check,
            ImpAbstractDefn ^ td_context, Pieces),
        !:Specs = [Spec | !.Specs]
    ).

:- pred report_any_incompatible_type_decl_or_defn(type_ctor::in,
    prog_context::in, string::in, string::in, string::in,
    string::in, maybe(prog_context)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_any_incompatible_type_decl_or_defn(TypeCtor, UsedContext, Kind, Section,
        SectionDeclOrDefn, DeclOrDefn, MaybeDefnContext, !Specs) :-
    (
        MaybeDefnContext = no
    ;
        MaybeDefnContext = yes(DefnContext),
        MainPieces = [words("Error: this"), words(DeclOrDefn), words("of")] ++
            color_as_subject([unqual_type_ctor(TypeCtor)]) ++
            [words("is")] ++ color_as_incorrect([words("incompatible")]) ++
            [words("with the"), words(Kind), words(SectionDeclOrDefn),
            words("in the"), words(Section), words("section."), nl],
        UsedPieces = [words("That"), words(SectionDeclOrDefn),
            words("is here."), nl],
        Spec = error_spec($pred, severity_error, phase_tim_check_invalid_type,
            [msg(DefnContext, MainPieces),
            msg(UsedContext, UsedPieces)]),
        !:Specs = [Spec | !.Specs]
    ).

:- pred report_incompatible_foreign_enum(type_ctor::in, prog_context::in,
    string::in, string::in, item_foreign_enum_info::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_incompatible_foreign_enum(TypeCtor, UsedContext, Kind, Section, Enum,
        !Specs) :-
    MainPieces = [words("Error: this"), pragma_decl("foreign_enum"),
        words("declaration for")] ++
        color_as_subject([unqual_type_ctor(TypeCtor)]) ++
        [words("is")] ++ color_as_incorrect([words("incompatible")]) ++
        [words("with the"), words(Kind), words("definition in the"),
        words(Section), words("section."), nl],
    UsedPieces = [words("That definition is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(Enum ^ fe_context, MainPieces),
        msg(UsedContext, UsedPieces)]),
    !:Specs = [Spec | !.Specs].

:- pred report_foreign_enum_for_undefined_type(type_ctor::in, string::in,
    item_foreign_enum_info::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_foreign_enum_for_undefined_type(TypeCtor, UndefOrUndecl, Enum,
        !Specs) :-
    Pieces = [words("Error:"), pragma_decl("foreign_enum"),
        words("declaration for the")] ++
        color_as_incorrect([words(UndefOrUndecl), words("type")]) ++
        color_as_subject([unqual_type_ctor(TypeCtor), suffix(".")]) ++ [nl],
    Spec = spec($pred, severity_error, phase_tim_check,
        Enum ^ fe_context, Pieces),
    !:Specs = [Spec | !.Specs].

:- pred maybe_report_declared_but_undefined_type(maybe_insist_on_defn::in,
    type_ctor::in, item_type_defn_info_abstract::in,
    list(error_spec)::in, list(error_spec)::out) is det.

maybe_report_declared_but_undefined_type(InsistOnDefn, TypeCtor, AbsTypeDefn,
        !Specs) :-
    TypeCtor = type_ctor(TypeCtorSymName, _TypeCtorArity),
    det_sym_name_get_module_name(TypeCtorSymName, TypeCtorModuleName),
    BuiltinTypeCtors = builtin_type_ctors_with_no_hlds_type_defn,
    ( if
        InsistOnDefn = do_insist_on_defn,
        % Do not report undefined types in builtin modules, since
        % their implementation (such as c_pointer's) may be handwritten.
        not any_mercury_builtin_module(TypeCtorModuleName),
        % Several of the types defined in type_desc.m do not have
        % Mercury definitions.
        not TypeCtorModuleName = unqualified("type_desc"),
        not list.member(TypeCtor, BuiltinTypeCtors)
    then
        Pieces = [words("Error: the type")] ++
            color_as_subject([unqual_type_ctor(TypeCtor)]) ++
            [words("has this declaration, but")] ++
            color_as_incorrect([words("it has no definition.")]) ++ [nl],
        % XXX should be phase_tim_check_invalid_type
        Spec = spec($pred, severity_error, phase_tim_check,
            AbsTypeDefn ^ td_context, Pieces),
        !:Specs = [Spec | !.Specs]
    else
        true
    ).

    % TypeDefnMap should contain all the type definitions in a given section
    % of a module.
    %
    % For a given type constructor in that module section, there should be
    % at most one definition of each kind (e.g. there must not be two
    % definitions as a du type), though there may be two or more definitions
    % of different kids (e.g. a du definition, a C definition and a Java
    % definition).
    %
:- pred check_any_type_ctor_defns_for_duplicates(type_ctor_defn_map::in,
    type_ctor::in, type_ctor_maybe_defn::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_any_type_ctor_defns_for_duplicates(TypeDefnMap, TypeCtor,
        MaybeDefn, !Specs) :-
    ( if map.search(TypeDefnMap, TypeCtor, AllDefns) then
        AllDefns = type_ctor_all_defns(AbsSolverDefns, SolverDefns,
            AbsNonSolverDefns, EqvDefns, DuDefns, SubDefns, ForeignDefns),
        at_most_one_type_decl_or_defn(dd_decl, "abstract solver type",
            TypeCtor, AbsSolverDefns, AbsSolverMaybeDefn, !Specs),
        at_most_one_type_decl_or_defn(dd_defn, "solver type",
            TypeCtor, SolverDefns, SolverMaybeDefn, !Specs),
        at_most_one_type_decl_or_defn(dd_decl, "abstract type",
            TypeCtor, AbsNonSolverDefns, AbsNonSolverMaybeDefn, !Specs),
        at_most_one_type_decl_or_defn(dd_defn, "equivalence type",
            TypeCtor, EqvDefns, EqvMaybeDefn, !Specs),
        at_most_one_type_decl_or_defn(dd_defn, "discriminated union type",
            TypeCtor, DuDefns, DuMaybeDefn, !Specs),
        at_most_one_type_decl_or_defn(dd_defn, "subtype",
            TypeCtor, SubDefns, SubMaybeDefn, !Specs),
        at_most_one_foreign_type_for_all_langs(TypeCtor,
            ForeignDefns, ForeignMaybeDefn, !Specs),
        MaybeDefn = type_ctor_maybe_defn(AbsSolverMaybeDefn, SolverMaybeDefn,
            AbsNonSolverMaybeDefn, EqvMaybeDefn,
            DuMaybeDefn, SubMaybeDefn, ForeignMaybeDefn)
    else
        MaybeDefn = type_ctor_maybe_defn(no, no, no, no, no, no,
            c_java_csharp(no, no, no))
    ).

:- type decl_or_defn
    --->    dd_decl
    ;       dd_defn.

:- pred at_most_one_type_decl_or_defn(decl_or_defn::in, string::in,
    type_ctor::in, list(item_type_defn_info_general(T))::in,
    maybe(item_type_defn_info_general(T))::out,
    list(error_spec)::in, list(error_spec)::out) is det.

at_most_one_type_decl_or_defn(DeclOrDefn, Kind, TypeCtor,
        TypeDefns, MaybeTypeDefn, !Specs) :-
    (
        TypeDefns = [],
        MaybeTypeDefn = no
    ;
        TypeDefns = [TypeDefn],
        MaybeTypeDefn = yes(TypeDefn)
    ;
        TypeDefns = [_, _ | _],
        CompareTypeDefnsByContext =
            ( pred(TDA::in, TDB::in, Cmp::out) is det :-
                compare(Cmp, TDA ^ td_context, TDB ^ td_context)
            ),
        list.sort(CompareTypeDefnsByContext, TypeDefns, SortedTypeDefns),
        list.det_head_tail(SortedTypeDefns, HeadTypeDefn, TailTypeDefns),
        MaybeTypeDefn = yes(HeadTypeDefn),
        list.foldl(
            report_duplicate_type_decl_or_defn(DeclOrDefn, Kind, TypeCtor,
                HeadTypeDefn),
            TailTypeDefns, !Specs)
    ).

:- pred at_most_one_foreign_type_for_all_langs(type_ctor::in,
    c_j_cs_defns::in, c_j_cs_maybe_defn::out,
    list(error_spec)::in, list(error_spec)::out) is det.

at_most_one_foreign_type_for_all_langs(TypeCtor, DefnsCJCs, MaybeDefnCJCs,
        !Specs) :-
    DefnsCJCs = c_java_csharp(DefnsC, DefnsJava, DefnsCsharp),
    at_most_one_foreign_type_for_lang(TypeCtor, lang_c,
        DefnsC, MaybeDefnC, !Specs),
    at_most_one_foreign_type_for_lang(TypeCtor, lang_java,
        DefnsJava, MaybeDefnJava, !Specs),
    at_most_one_foreign_type_for_lang(TypeCtor, lang_csharp,
        DefnsCsharp, MaybeDefnCsharp, !Specs),
    MaybeDefnCJCs = c_java_csharp(MaybeDefnC, MaybeDefnJava, MaybeDefnCsharp).

:- pred check_any_type_ctor_enums_for_duplicates(
    type_ctor_foreign_enum_map::in, type_ctor::in,
    c_j_cs_maybe_enum::out, c_j_cs_enums::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_any_type_ctor_enums_for_duplicates(ForeignEnumMap, TypeCtor,
        MaybeEnumCJCs, LeftOverEnumCJCse, !Specs) :-
    ( if map.search(ForeignEnumMap, TypeCtor, AllEnums) then
        at_most_one_foreign_enum_for_all_langs(TypeCtor,
            AllEnums, MaybeEnumCJCs, LeftOverEnumCJCse, !Specs)
    else
        MaybeEnumCJCs = c_java_csharp(no, no, no),
        LeftOverEnumCJCse = c_java_csharp([], [], [])
    ).

:- pred at_most_one_foreign_enum_for_all_langs(type_ctor::in,
    c_j_cs_enums::in, c_j_cs_maybe_enum::out, c_j_cs_enums::out,
    list(error_spec)::in, list(error_spec)::out) is det.

at_most_one_foreign_enum_for_all_langs(TypeCtor, AllEnumsCJCs,
        MaybeEnumCJCs, LeftOverEnumsCJCs, !Specs) :-
    AllEnumsCJCs = c_java_csharp(EnumsC, EnumsJava, EnumsCsharp),
    at_most_one_foreign_enum_for_lang(TypeCtor, lang_c,
        EnumsC, MaybeEnumC, LeftOverEnumsC, !Specs),
    at_most_one_foreign_enum_for_lang(TypeCtor, lang_java,
        EnumsJava, MaybeEnumJava, LeftOverEnumsJava, !Specs),
    at_most_one_foreign_enum_for_lang(TypeCtor, lang_csharp,
        EnumsCsharp, MaybeEnumCsharp, LeftOverEnumsCsharp, !Specs),
    MaybeEnumCJCs = c_java_csharp(MaybeEnumC, MaybeEnumJava, MaybeEnumCsharp),
    LeftOverEnumsCJCs = c_java_csharp(LeftOverEnumsC,
        LeftOverEnumsJava, LeftOverEnumsCsharp).

:- pred report_duplicate_type_decl_or_defn(decl_or_defn::in, string::in,
    type_ctor::in,
    item_type_defn_info_general(T1)::in, item_type_defn_info_general(T2)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_duplicate_type_decl_or_defn(DeclOrDefn, Kind, TypeCtor,
        OrigTypeDefn, TypeDefn, !Specs) :-
    (
        DeclOrDefn = dd_decl,
        DeclOrDefnWord = "declaration",
        SeverityWord = "Warning",
        Severity = severity_warning
    ;
        DeclOrDefn = dd_defn,
        DeclOrDefnWord = "definition",
        SeverityWord = "Error",
        Severity = severity_error
    ),
    MainPieces = [words(SeverityWord), suffix(":")] ++
        color_as_incorrect([words("duplicate"), words(Kind),
            words(DeclOrDefnWord)]) ++
        [words("for")] ++
        color_as_subject([unqual_type_ctor(TypeCtor), suffix(".")]) ++ [nl],
    LeastPieces = [words("The original"), words(DeclOrDefnWord),
        words("is here."), nl],
    Spec = error_spec($pred, Severity, phase_tim_check,
        [msg(TypeDefn ^ td_context, MainPieces),
        msg(OrigTypeDefn ^ td_context, LeastPieces)]),
    !:Specs = [Spec | !.Specs].

:- pred at_most_one_foreign_type_for_lang(type_ctor::in, foreign_language::in,
    list(item_type_defn_info_foreign)::in,
    maybe(item_type_defn_info_foreign)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

at_most_one_foreign_type_for_lang(TypeCtor, Lang, TypeDefns,
        MaybeTypeDefn, !Specs) :-
    (
        TypeDefns = [],
        MaybeTypeDefn = no
    ;
        TypeDefns = [TypeDefn],
        MaybeTypeDefn = yes(TypeDefn)
    ;
        TypeDefns = [TypeDefn, _ | _],
        MaybeTypeDefn = yes(TypeDefn),
        list.foldl(accumulate_type_defn_contexts, TypeDefns,
            set.init, Contexts),
        ( if set.remove_least(LeastContext, Contexts, OtherContexts) then
            set.foldl(
                report_duplicate_foreign_defn("type", TypeCtor, Lang,
                    LeastContext),
                OtherContexts, !Specs)
        else
            unexpected($pred, "nonempty set doesn't have least element")
        )
    ).

:- pred at_most_one_foreign_enum_for_lang(type_ctor::in, foreign_language::in,
    list(item_foreign_enum_info)::in,
    maybe(item_foreign_enum_info)::out, list(item_foreign_enum_info)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

at_most_one_foreign_enum_for_lang(TypeCtor, Lang, ForeignEnums,
        MaybeForeignEnum, LeftOverForeignEnums, !Specs) :-
    list.sort(compare_foreign_enum_infos_by_context,
        ForeignEnums, SortedForeignEnums),
    (
        SortedForeignEnums = [],
        MaybeForeignEnum = no,
        LeftOverForeignEnums = []
    ;
        SortedForeignEnums = [ForeignEnum],
        MaybeForeignEnum = yes(ForeignEnum),
        LeftOverForeignEnums = []
    ;
        SortedForeignEnums = [ForeignEnum | LeftOverForeignEnums],
        LeftOverForeignEnums = [_ | _],
        MaybeForeignEnum = yes(ForeignEnum),

        LeastContext = ForeignEnum ^ fe_context,
        LeftOverContexts = list.map(project_foreign_enum_context,
            LeftOverForeignEnums),
        list.foldl(
            report_duplicate_foreign_defn("enum", TypeCtor, Lang,
                LeastContext),
            LeftOverContexts, !Specs)
    ).

:- pred compare_foreign_enum_infos_by_context(
    item_foreign_enum_info::in, item_foreign_enum_info::in,
    comparison_result::out) is det.

compare_foreign_enum_infos_by_context(ForeignEnumA, ForeignEnumB, Cmp) :-
    ContextA = ForeignEnumA ^ fe_context,
    ContextB = ForeignEnumB ^ fe_context,
    compare(Cmp, ContextA, ContextB).

:- func project_foreign_enum_context(item_foreign_enum_info) = prog_context.

project_foreign_enum_context(ForeignEnum) = ForeignEnum ^ fe_context.

:- pred accumulate_type_defn_contexts(item_type_defn_info_general(T)::in,
    set(prog_context)::in, set(prog_context)::out) is det.

accumulate_type_defn_contexts(TypeDefn, !Contexts) :-
    set.insert(get_type_defn_info_context(TypeDefn), !Contexts).

:- func get_type_defn_info_context(item_type_defn_info_general(T))
    = prog_context.

get_type_defn_info_context(TypeDefn) = TypeDefn ^ td_context.

:- pred report_duplicate_foreign_defn(string::in,
    type_ctor::in, foreign_language::in, prog_context::in, prog_context::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_duplicate_foreign_defn(TypeOrEnum, TypeCtor, Lang,
        LeastContext, Context, !Specs) :-
    MainPieces = [words("Error:")] ++
        color_as_incorrect([words("duplicate foreign"), fixed(TypeOrEnum),
            words("definition in"), fixed(foreign_language_string(Lang))]) ++
        [words("for")] ++
        color_as_subject([unqual_type_ctor(TypeCtor), suffix(".")]) ++ [nl],
    LeastPieces = [words("The original definition is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(Context, MainPieces),
        msg(LeastContext, LeastPieces)]),
    !:Specs = [Spec | !.Specs].

:- func get_maybe_type_defns(list(maybe(item_type_defn_info_general(T))))
    = list(item_type_defn_info_general(T)).

get_maybe_type_defns([]) = [].
get_maybe_type_defns([MaybeTypeDefn | MaybeTypeDefns]) = Defns :-
    TailDefns = get_maybe_type_defns(MaybeTypeDefns),
    (
        MaybeTypeDefn = no,
        Defns = TailDefns
    ;
        MaybeTypeDefn = yes(TypeDefn),
        Defns = [TypeDefn | TailDefns]
    ).

:- func get_maybe_type_defn_contexts(list(maybe(item_type_defn_info_foreign)))
    = list(prog_context).

get_maybe_type_defn_contexts([]) = [].
get_maybe_type_defn_contexts([MaybeTypeDefn | MaybeTypeDefns]) = Contexts :-
    TailContexts = get_maybe_type_defn_contexts(MaybeTypeDefns),
    (
        MaybeTypeDefn = no,
        Contexts = TailContexts
    ;
        MaybeTypeDefn = yes(TypeDefn),
        Contexts = [TypeDefn ^ td_context | TailContexts]
    ).

%---------------------------------------------------------------------------%

    % This type maps a field name to the locations where it occurs.
    %
:- type field_name_map ==
    map(field_name_of_type_ctor, one_or_more(field_name_locn)).

:- type field_name_of_type_ctor
    --->    field_name_of_type_ctor(
                string,
                type_ctor
            ).

    % The info we have about each location where a field name occurs:
    %
    % - the context where it occurs, and
    % - the data constructor in which it occurs.
    %
    % The context is first to make sorting easier. This is relevant
    % because we want to consider the textually first occurrence of
    % a field name to be the valid occurrence, and the later ones
    % as the duplicates.
    %
:- type field_name_locn
    --->    field_name_locn(prog_context, string).

:- pred add_type_ctor_to_field_name_map(
    type_ctor::in, type_ctor_checked_defn::in,
    field_name_map::in, field_name_map::out) is det.

add_type_ctor_to_field_name_map(TypeCtor, CheckedDefn, !FieldNameMap) :-
    (
        CheckedDefn = checked_defn_solver(_, _)
    ;
        CheckedDefn = checked_defn_std(CheckedStdDefn, _),
        (
            ( CheckedStdDefn = std_mer_type_eqv(_, _)
            ; CheckedStdDefn = std_mer_type_abstract(_, _, _)
            ; CheckedStdDefn = std_mer_type_du_all_plain_constants(_, _,
                _, _, _)
            )
        ;
            (
                CheckedStdDefn =
                    std_mer_type_du_not_all_plain_constants(_Status,
                        DuDefn, _MaybeDefnCJCs),
                DetailsDu = DuDefn ^ td_ctor_defn,
                DetailsDu = type_details_du(OoMCtors, _MaybeCanon,
                    _MaybeDirectArgs)
            ;
                CheckedStdDefn = std_mer_type_subtype(_Status, SubDefn),
                DetailsSub = SubDefn ^ td_ctor_defn,
                DetailsSub = type_details_sub(_SuperType, OoMCtors)
            ),
            OoMCtors = one_or_more(HeadCtor, TailCtors),
            list.foldl(add_data_ctor_to_field_name_map(TypeCtor),
                [HeadCtor | TailCtors], !FieldNameMap)
        )
    ).

:- pred add_data_ctor_to_field_name_map(type_ctor::in, constructor::in,
    field_name_map::in, field_name_map::out) is det.

add_data_ctor_to_field_name_map(TypeCtor, Ctor, !FieldNameMap) :-
    Ctor = ctor(_Ordinal, _MaybeExist, CtorSymName, CtorArgs,
        _NumArgs, _CtorContext),
    CtorName = unqualify_name(CtorSymName),
    list.foldl(add_data_ctor_arg_to_field_name_map(TypeCtor, CtorName),
        CtorArgs, !FieldNameMap).

:- pred add_data_ctor_arg_to_field_name_map(type_ctor::in, string::in,
    constructor_arg::in, field_name_map::in, field_name_map::out) is det.

add_data_ctor_arg_to_field_name_map(TypeCtor, CtorName, CtorArg,
        !FieldNameMap) :-
    CtorArg = ctor_arg(MaybeCtorFieldName, _Type, _ArgContext),
    (
        MaybeCtorFieldName = no
    ;
        MaybeCtorFieldName = yes(CtorFieldName),
        CtorFieldName = ctor_field_name(FieldSymName, FieldNameContext),
        FieldName = unqualify_name(FieldSymName),
        FieldNameTypeCtor = field_name_of_type_ctor(FieldName, TypeCtor),
        FNLocn = field_name_locn(FieldNameContext, CtorName),
        ( if map.search(!.FieldNameMap, FieldNameTypeCtor, OoMFNLocns0) then
            OoMFNLocns0 = one_or_more(HeadFNLocn, TailFNLocns),
            OoMFNLocns = one_or_more(FNLocn, [HeadFNLocn | TailFNLocns]),
            map.det_update(FieldNameTypeCtor, OoMFNLocns, !FieldNameMap)
        else
            OoMFNLocns = one_or_more(FNLocn, []),
            map.det_insert(FieldNameTypeCtor, OoMFNLocns, !FieldNameMap)
        )
    ).

:- pred report_any_duplicate_field_names(field_name_of_type_ctor::in,
    one_or_more(field_name_locn)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_any_duplicate_field_names(FieldNameTypeCtor, OoMFNLocns, !Specs) :-
    FNLocns = one_or_more_to_list(OoMFNLocns),
    list.sort(FNLocns, SortedFNLocns),
    (
        SortedFNLocns = [],
        unexpected($pred, "SortedFNLocns = []")
    ;
        SortedFNLocns = [_]
        % The expected case; FieldName is defined exactly once.
    ;
        SortedFNLocns = [HeadFNLocn | TailFNLocns],
        TailFNLocns = [_ | _],
        % The case we are looking for; FieldName is defined *more* than once
        % in the same type.
        list.foldl(report_duplicate_field_name(FieldNameTypeCtor, HeadFNLocn),
            TailFNLocns, !Specs)
    ).

:- pred report_duplicate_field_name(field_name_of_type_ctor::in,
    field_name_locn::in, field_name_locn::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_duplicate_field_name(FieldNameTypeCtor, FirstFNLocn, FNLocn, !Specs) :-
    FieldNameTypeCtor = field_name_of_type_ctor(FieldName, TypeCtor),
    FirstFNLocn = field_name_locn(FirstContext, FirstCtorName),
    FNLocn = field_name_locn(Context, CtorName),
    InitPieces = [words("Error:")] ++
        color_as_incorrect([words("duplicate occurrence")]) ++
        [words("of the field name")] ++
        color_as_subject([quote(FieldName)]),
    ( if CtorName = FirstCtorName then
        % The two occurrences of FieldName are in the same data constructor.
        CtorPieces = [words("in the function symbol"), quote(CtorName)]
    else
        % The two occurrences are in different data constructors.
        CtorPieces = []
    ),
    MainPieces = InitPieces ++ CtorPieces ++
        [words("in the definition of the type constructor"),
        unqual_type_ctor(TypeCtor), suffix("."), nl],
    FirstOccurrencePieces = [words("The first occurrence of this field name"),
        words("is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(Context, MainPieces),
        msg(FirstContext, FirstOccurrencePieces)]),
    !:Specs = [Spec | !.Specs].

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

create_inst_ctor_checked_map(InsistOnDefn, IntInstDefnMap, ImpInstDefnMap,
        CheckedMap, !Specs) :-
    map.keys_as_set(IntInstDefnMap, IntDefnInstCtors),
    map.keys_as_set(ImpInstDefnMap, ImpDefnInstCtors),
    % This union operation depends on the type_ctors in all four maps
    % being qualified exactly the same way. We could require the type_ctor keys
    % to be all fully qualified or all fully unqualified; we chose the former.
    InstCtors =
        set.to_sorted_list(set.union(IntDefnInstCtors, ImpDefnInstCtors)),
    list.foldl2(
        check_inst_ctor_defns(InsistOnDefn, IntInstDefnMap, ImpInstDefnMap),
        InstCtors, map.init, CheckedMap, !Specs).

:- pred check_inst_ctor_defns(maybe_insist_on_defn::in,
    inst_ctor_defn_map::in, inst_ctor_defn_map::in, inst_ctor::in,
    inst_ctor_checked_map::in, inst_ctor_checked_map::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_inst_ctor_defns(InsistOnDefn, IntInstDefnMap, ImpInstDefnMap, InstCtor,
        !CheckedMap, !Specs) :-
    check_any_inst_ctor_defns_for_duplicates(IntInstDefnMap, InstCtor,
        IntMaybeAbstractDefn, IntMaybeEqvDefn, !Specs),
    check_any_inst_ctor_defns_for_duplicates(ImpInstDefnMap, InstCtor,
        ImpMaybeAbstractDefn, ImpMaybeEqvDefn, !Specs),
    ( if
        % Does InstCtor have a non-abstract definition ...
        ( if
            % ... in the interface?
            IntMaybeEqvDefn = yes(IntEqvDefn)
        then
            EqvDefn = IntEqvDefn,
            EqvWhere = "interface",
            Status = std_inst_exported,
            SrcDefnsInt = yes(wrap_eqv_inst_defn(IntEqvDefn)),
            SrcDefns = src_defns_inst(SrcDefnsInt, no)
        else if
            % ... in the implementation?
            ImpMaybeEqvDefn = yes(ImpEqvDefn)
        then
            EqvDefn = ImpEqvDefn,
            EqvWhere = "implementation",
            (
                IntMaybeAbstractDefn = yes(IntAbstractDefn),
                Status = std_inst_abstract_exported,
                SrcDefnsInt = yes(wrap_abstract_inst_defn(IntAbstractDefn))
            ;
                IntMaybeAbstractDefn = no,
                Status = std_inst_all_private,
                SrcDefnsInt = no
            ),
            SrcDefnsImp = yes(wrap_eqv_inst_defn(ImpEqvDefn)),
            SrcDefns = src_defns_inst(SrcDefnsInt, SrcDefnsImp)
        else
            fail
        )
    then
        % Having an IntAbstractDefn, as well an IntEqvDefn, is ok.
        % We sometimes put an abstract declaration in one interface section,
        % which we publicize, and a non-abstract definition in another
        % interface section, which we don't publicize.
        report_any_redundant_abstract_inst_in_imp(InstCtor,
            "definition", EqvWhere, ImpMaybeAbstractDefn, !Specs),
        StdDefn = std_inst_defn(Status, wrap_eqv_inst_defn(EqvDefn)),
        CheckedDefn = checked_defn_inst(StdDefn, SrcDefns),
        map.det_insert(InstCtor, CheckedDefn, !CheckedMap)
    else
        % We get called only on InstCtors for which we have
        % at least one definition. Since we don't have any equivalence
        % definitions, we must have at least one abstract declaration.
        (
            IntMaybeAbstractDefn = yes(IntAbstractDefn),
            report_any_redundant_abstract_inst_in_imp(InstCtor,
                "declaration", "interface", ImpMaybeAbstractDefn, !Specs),
            (
                InsistOnDefn = do_not_insist_on_defn,
                Status = std_inst_abstract_exported,
                StdDefn = std_inst_defn(Status,
                    wrap_abstract_inst_defn(IntAbstractDefn)),
                IntDefn = wrap_abstract_inst_defn(IntAbstractDefn),
                SrcDefns = src_defns_inst(yes(IntDefn), no),
                CheckedDefn = checked_defn_inst(StdDefn, SrcDefns),
                map.det_insert(InstCtor, CheckedDefn, !CheckedMap)
            ;
                InsistOnDefn = do_insist_on_defn,
                report_declared_but_undefined_inst(InstCtor, IntAbstractDefn,
                    !Specs)
            )
        ;
            IntMaybeAbstractDefn = no,
            (
                ImpMaybeAbstractDefn = yes(ImpAbstractDefn),
                (
                    InsistOnDefn = do_not_insist_on_defn,
                    Status = std_inst_all_private,
                    StdDefn = std_inst_defn(Status,
                        wrap_abstract_inst_defn(ImpAbstractDefn)),
                    ImpDefn = wrap_abstract_inst_defn(ImpAbstractDefn),
                    SrcDefns = src_defns_inst(no, yes(ImpDefn)),
                    CheckedDefn = checked_defn_inst(StdDefn, SrcDefns),
                    map.det_insert(InstCtor, CheckedDefn, !CheckedMap)
                ;
                    InsistOnDefn = do_insist_on_defn,
                    report_declared_but_undefined_inst(InstCtor,
                        ImpAbstractDefn, !Specs)
                )
            ;
                ImpMaybeAbstractDefn = no,
                unexpected($pred, "no defns at all")
            )
        )
    ).

:- pred check_any_inst_ctor_defns_for_duplicates(inst_ctor_defn_map::in,
    inst_ctor::in, maybe(item_inst_defn_info_abstract)::out,
    maybe(item_inst_defn_info_eqv)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_any_inst_ctor_defns_for_duplicates(InstDefnMap, InstCtor,
        AbstractMaybeDefn, EqvMaybeDefn, !Specs) :-
    ( if map.search(InstDefnMap, InstCtor, AllDefns) then
        AllDefns = inst_ctor_all_defns(AbstractDefns, EqvDefns),
        at_most_one_inst_defn("abstract inst", InstCtor,
            AbstractDefns, AbstractMaybeDefn, !Specs),
        at_most_one_inst_defn("inst", InstCtor,
            EqvDefns, EqvMaybeDefn, !Specs)
    else
        AbstractMaybeDefn = no,
        EqvMaybeDefn = no
    ).

:- pred at_most_one_inst_defn(string::in, inst_ctor::in,
    list(item_inst_defn_info_general(T))::in,
    maybe(item_inst_defn_info_general(T))::out,
    list(error_spec)::in, list(error_spec)::out) is det.

at_most_one_inst_defn(Kind, InstCtor, InstDefns, MaybeInstDefn, !Specs) :-
    (
        InstDefns = [],
        MaybeInstDefn = no
    ;
        InstDefns = [InstDefn],
        MaybeInstDefn = yes(InstDefn)
    ;
        InstDefns = [_, _ | _],
        CompareInstDefnsByContext =
            ( pred(IDA::in, IDB::in, Cmp::out) is det :-
                compare(Cmp, IDA ^ id_context, IDB ^ id_context)
            ),
        list.sort(CompareInstDefnsByContext, InstDefns, SortedInstDefns),
        list.det_head_tail(SortedInstDefns, HeadInstDefn, TailInstDefns),
        MaybeInstDefn = yes(HeadInstDefn),
        list.foldl(
            report_duplicate_inst_defn(Kind, InstCtor, HeadInstDefn),
            TailInstDefns, !Specs)
    ).

:- pred report_duplicate_inst_defn(string::in, inst_ctor::in,
    item_inst_defn_info_general(T1)::in, item_inst_defn_info_general(T2)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_duplicate_inst_defn(Kind, InstCtor, OrigInstDefn, InstDefn, !Specs) :-
    MainPieces = [words("Error")] ++
        color_as_incorrect([words("duplicate"), words(Kind),
            words("definition")]) ++
        [words("for")] ++
        color_as_subject([unqual_inst_ctor(InstCtor), suffix(".")]) ++ [nl],
    LeastPieces = [words("The original definition is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(InstDefn ^ id_context, MainPieces),
        msg(OrigInstDefn ^ id_context, LeastPieces)]),
    !:Specs = [Spec | !.Specs].

:- pred report_any_redundant_abstract_inst_in_imp(inst_ctor::in,
    string::in, string::in,
    maybe(item_inst_defn_info_abstract)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_any_redundant_abstract_inst_in_imp(InstCtor, DeclOrDefn, Section,
        MaybeImpAbstractDefn, !Specs) :-
    (
        MaybeImpAbstractDefn = no
    ;
        MaybeImpAbstractDefn = yes(ImpAbstractDefn),
        Pieces = [words("Warning: this declaration of")] ++
            color_as_subject([unqual_inst_ctor(InstCtor)]) ++
            [words("is")] ++ color_as_incorrect([words("redundant,")]) ++
            [words("since the inst has a"), words(DeclOrDefn),
            words("in the"), words(Section), words("section."), nl],
        Spec = spec($pred, severity_warning, phase_tim_check,
            ImpAbstractDefn ^ id_context, Pieces),
        !:Specs = [Spec | !.Specs]
    ).

:- pred report_declared_but_undefined_inst(inst_ctor::in,
    item_inst_defn_info_abstract::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_declared_but_undefined_inst(InstCtor, AbsInstDefn, !Specs) :-
    Pieces = [words("Error: the inst")] ++
        color_as_subject([unqual_inst_ctor(InstCtor)]) ++
        [words("has this declaration, but")] ++
        color_as_incorrect([words("it has no definition.")]) ++ [nl],
    Spec = spec($pred, severity_error, phase_tim_check_invalid_inst_mode,
        AbsInstDefn ^ id_context, Pieces),
    !:Specs = [Spec | !.Specs].

%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%

create_mode_ctor_checked_map(InsistOnDefn, IntModeDefnMap, ImpModeDefnMap,
        CheckedMap, !Specs) :-
    map.keys_as_set(IntModeDefnMap, IntDefnModeCtors),
    map.keys_as_set(ImpModeDefnMap, ImpDefnModeCtors),
    % This union operation depends on the type_ctors in all four maps
    % being qualified exactly the same way. We could require the type_ctor keys
    % to be all fully qualified or all fully unqualified; we chose the former.
    ModeCtors =
        set.to_sorted_list(set.union(IntDefnModeCtors, ImpDefnModeCtors)),
    list.foldl2(
        check_mode_ctor_defns(InsistOnDefn, IntModeDefnMap, ImpModeDefnMap),
        ModeCtors, map.init, CheckedMap, !Specs).

:- pred check_mode_ctor_defns(maybe_insist_on_defn::in,
    mode_ctor_defn_map::in, mode_ctor_defn_map::in, mode_ctor::in,
    mode_ctor_checked_map::in, mode_ctor_checked_map::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_mode_ctor_defns(InsistOnDefn, IntModeDefnMap, ImpModeDefnMap, ModeCtor,
        !CheckedMap, !Specs) :-
    check_any_mode_ctor_defns_for_duplicates(IntModeDefnMap, ModeCtor,
        IntMaybeAbstractDefn, IntMaybeEqvDefn, !Specs),
    check_any_mode_ctor_defns_for_duplicates(ImpModeDefnMap, ModeCtor,
        ImpMaybeAbstractDefn, ImpMaybeEqvDefn, !Specs),
    ( if
        % Does ModeCtor have a non-abstract definition ...
        ( if
            % ... in the interface?
            IntMaybeEqvDefn = yes(IntEqvDefn)
        then
            EqvDefn = IntEqvDefn,
            EqvWhere = "interface",
            Status = std_mode_exported,
            SrcDefnsInt = yes(wrap_eqv_mode_defn(IntEqvDefn)),
            SrcDefns = src_defns_mode(SrcDefnsInt, no)
        else if
            % ... in the implementation?
            ImpMaybeEqvDefn = yes(ImpEqvDefn)
        then
            EqvDefn = ImpEqvDefn,
            EqvWhere = "implementation",
            (
                IntMaybeAbstractDefn = yes(IntAbstractDefn),
                Status = std_mode_abstract_exported,
                SrcDefnsInt = yes(wrap_abstract_mode_defn(IntAbstractDefn))
            ;
                IntMaybeAbstractDefn = no,
                Status = std_mode_all_private,
                SrcDefnsInt = no
            ),
            SrcDefnsImp = yes(wrap_eqv_mode_defn(ImpEqvDefn)),
            SrcDefns = src_defns_mode(SrcDefnsInt, SrcDefnsImp)
        else
            fail
        )
    then
        % Having an IntAbstractDefn, as well an IntEqvDefn, is ok.
        % We sometimes put an abstract declaration in one interface section,
        % which we publicize, and a non-abstract definition in another
        % interface section, which we don't publicize.
        report_any_redundant_abstract_mode_in_imp(ModeCtor,
            "definition", EqvWhere, ImpMaybeAbstractDefn, !Specs),
        StdDefn = std_mode_defn(Status, wrap_eqv_mode_defn(EqvDefn)),
        CheckedDefn = checked_defn_mode(StdDefn, SrcDefns),
        map.det_insert(ModeCtor, CheckedDefn, !CheckedMap)
    else
        % We get called only on ModeCtors for which we have
        % at least one definition. Since we don't have any equivalence
        % definitions, we must have at least one abstract declaration.
        (
            IntMaybeAbstractDefn = yes(IntAbstractDefn),
            report_any_redundant_abstract_mode_in_imp(ModeCtor,
                "declaration", "interface", ImpMaybeAbstractDefn, !Specs),
            (
                InsistOnDefn = do_not_insist_on_defn,
                Status = std_mode_abstract_exported,
                StdDefn = std_mode_defn(Status,
                    wrap_abstract_mode_defn(IntAbstractDefn)),
                IntDefn = wrap_abstract_mode_defn(IntAbstractDefn),
                SrcDefns = src_defns_mode(yes(IntDefn), no),
                CheckedDefn = checked_defn_mode(StdDefn, SrcDefns),
                map.det_insert(ModeCtor, CheckedDefn, !CheckedMap)
            ;
                InsistOnDefn = do_insist_on_defn,
                report_declared_but_undefined_mode(ModeCtor, IntAbstractDefn,
                    !Specs)
            )
        ;
            IntMaybeAbstractDefn = no,
            (
                ImpMaybeAbstractDefn = yes(ImpAbstractDefn),
                (
                    InsistOnDefn = do_not_insist_on_defn,
                    Status = std_mode_all_private,
                    StdDefn = std_mode_defn(Status,
                        wrap_abstract_mode_defn(ImpAbstractDefn)),
                    ImpDefn = wrap_abstract_mode_defn(ImpAbstractDefn),
                    SrcDefns = src_defns_mode(no, yes(ImpDefn)),
                    CheckedDefn = checked_defn_mode(StdDefn, SrcDefns),
                    map.det_insert(ModeCtor, CheckedDefn, !CheckedMap)
                ;
                    InsistOnDefn = do_insist_on_defn,
                    report_declared_but_undefined_mode(ModeCtor,
                        ImpAbstractDefn, !Specs)
                )
            ;
                ImpMaybeAbstractDefn = no,
                unexpected($pred, "no defns at all")
            )
        )
    ).

:- pred check_any_mode_ctor_defns_for_duplicates(mode_ctor_defn_map::in,
    mode_ctor::in, maybe(item_mode_defn_info_abstract)::out,
    maybe(item_mode_defn_info_eqv)::out,
    list(error_spec)::in, list(error_spec)::out) is det.

check_any_mode_ctor_defns_for_duplicates(ModeDefnMap, ModeCtor,
        AbstractMaybeDefn, EqvMaybeDefn, !Specs) :-
    ( if map.search(ModeDefnMap, ModeCtor, AllDefns) then
        AllDefns = mode_ctor_all_defns(AbstractDefns, EqvDefns),
        at_most_one_mode_defn("abstract mode", ModeCtor,
            AbstractDefns, AbstractMaybeDefn, !Specs),
        at_most_one_mode_defn("mode", ModeCtor,
            EqvDefns, EqvMaybeDefn, !Specs)
    else
        AbstractMaybeDefn = no,
        EqvMaybeDefn = no
    ).

:- pred at_most_one_mode_defn(string::in, mode_ctor::in,
    list(item_mode_defn_info_general(T))::in,
    maybe(item_mode_defn_info_general(T))::out,
    list(error_spec)::in, list(error_spec)::out) is det.

at_most_one_mode_defn(Kind, ModeCtor, ModeDefns, MaybeModeDefn, !Specs) :-
    (
        ModeDefns = [],
        MaybeModeDefn = no
    ;
        ModeDefns = [ModeDefn],
        MaybeModeDefn = yes(ModeDefn)
    ;
        ModeDefns = [_, _ | _],
        CompareModeDefnsByContext =
            ( pred(IDA::in, IDB::in, Cmp::out) is det :-
                compare(Cmp, IDA ^ md_context, IDB ^ md_context)
            ),
        list.sort(CompareModeDefnsByContext, ModeDefns, SortedModeDefns),
        list.det_head_tail(SortedModeDefns, HeadModeDefn, TailModeDefns),
        MaybeModeDefn = yes(HeadModeDefn),
        list.foldl(
            report_duplicate_mode_defn(Kind, ModeCtor, HeadModeDefn),
            TailModeDefns, !Specs)
    ).

:- pred report_duplicate_mode_defn(string::in, mode_ctor::in,
    item_mode_defn_info_general(T1)::in, item_mode_defn_info_general(T2)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_duplicate_mode_defn(Kind, ModeCtor, OrigModeDefn, ModeDefn, !Specs) :-
    MainPieces = [words("Error:")] ++
        color_as_incorrect([words("duplicate"), words(Kind),
            words("definition")]) ++
        [words("for")] ++
        color_as_subject([unqual_mode_ctor(ModeCtor), suffix(".")]) ++ [nl],
    LeastPieces = [words("The original definition is here."), nl],
    Spec = error_spec($pred, severity_error, phase_tim_check,
        [msg(ModeDefn ^ md_context, MainPieces),
        msg(OrigModeDefn ^ md_context, LeastPieces)]),
    !:Specs = [Spec | !.Specs].

:- pred report_any_redundant_abstract_mode_in_imp(mode_ctor::in,
    string::in, string::in,
    maybe(item_mode_defn_info_abstract)::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_any_redundant_abstract_mode_in_imp(TypeCtor, DeclOrDefn, Section,
        MaybeImpAbstractDefn, !Specs) :-
    (
        MaybeImpAbstractDefn = no
    ;
        MaybeImpAbstractDefn = yes(ImpAbstractDefn),
        Pieces = [words("Warning: this declaration of")] ++
            color_as_subject([unqual_mode_ctor(TypeCtor)]) ++
            [words("is")] ++ color_as_incorrect([words("redundant,")]) ++
            [words("since the mode has a"), words(DeclOrDefn),
            words("in the"), words(Section), words("section."), nl],
        Spec = spec($pred, severity_warning, phase_tim_check,
            ImpAbstractDefn ^ md_context, Pieces),
        !:Specs = [Spec | !.Specs]
    ).

:- pred report_declared_but_undefined_mode(mode_ctor::in,
    item_mode_defn_info_abstract::in,
    list(error_spec)::in, list(error_spec)::out) is det.

report_declared_but_undefined_mode(ModeCtor, AbsModeDefn, !Specs) :-
    Pieces = [words("Error: the mode")] ++
        color_as_subject([unqual_mode_ctor(ModeCtor)]) ++
        [words("has this declaration, but")] ++
        color_as_incorrect([words("it has no definition.")]) ++ [nl],
    Spec = spec($pred, severity_error, phase_tim_check_invalid_inst_mode,
        AbsModeDefn ^ md_context, Pieces),
    !:Specs = [Spec | !.Specs].

%---------------------------------------------------------------------------%
:- end_module parse_tree.check_type_inst_mode_defns.
%---------------------------------------------------------------------------%
