% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------e
% Copyright (C) 1993-2008 The University of Melbourne.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%-----------------------------------------------------------------------------%
%
% File: prog_io.m.
% Main authors: fjh, zs.
%
% This module defines predicates for parsing Mercury programs.
%
% In some ways the representation of programs here is considerably
% more complex than is necessary for the compiler.
% The basic reason for this is that it was designed to preserve
% as much information about the source code as possible, so that
% this representation could also be used for other tools such
% as pretty-printers.
% Currently the only information that is lost is that comments and
% whitespace are stripped, any redundant parenthesization
% are lost, distinctions between different spellings of the same
% operator (eg "\+" vs "not") are lost, and DCG clauses get expanded.
% It would be a good idea to preserve all those too (well, maybe not
% the redundant parentheses), but right now it's not worth the effort.
%
% So that means that this phase of compilation is purely parsing.
% No simplifications are done (other than DCG expansion).
% The results of this phase specify
% basically the same information as is contained in the source code,
% but in a parse tree rather than a flat file.
% Simplifications are done only by make_hlds.m, which transforms
% the parse tree which we built here into the HLDS.
%
% Some of this code is a rather bad example of cut-and-paste style reuse.
% It should be cleaned up to eliminate most of the duplication.
% But that task really needs to wait until we implement higher-order
% predicates.  For the moment, just be careful that any changes
% you make are reflected correctly in all similar parts of this file.
%
% Implication and equivalence implemented by squirrel, who would also
% like to get her hands on this file and give it a good clean up and
% put it into good clean "mercury" style!
%
% Wishlist:
%
% 1.  implement importing/exporting operators with a particular fixity
%     eg. :- import_op prefix(+). % only prefix +, not infix
%     (not important, but should be there for reasons of symmetry.)
% 2.  improve the handling of type and inst parameters
% 3.  improve the error reporting (most of the semidet preds should
%     be det and should return a meaningful indication of where an
%     error occurred).

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

:- module parse_tree.prog_io.
:- interface.

:- import_module libs.file_util.
:- import_module libs.timestamp.
:- import_module mdbcomp.prim_data.
:- import_module parse_tree.error_util.
:- import_module parse_tree.prog_data.
:- import_module parse_tree.prog_item.
:- import_module parse_tree.prog_io_util.

:- import_module io.
:- import_module list.
:- import_module maybe.
:- import_module term.
:- import_module varset.

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

% This module (prog_io) exports the following predicates:

:- type module_error
    --->    no_module_errors        % no errors
    ;       some_module_errors      % some syntax errors
    ;       fatal_module_errors.    % couldn't open the file

:- type maybe_return_timestamp
    --->    do_return_timestamp
    ;       do_not_return_timestamp.

    % read_module(OpenFile, FileName, DefaultModuleName, ReturnTimestamp,
    %   MaybeFileInfo, ActualModuleName, Program, Specs, Error,
    %   MaybeModuleTimestamp, !IO):
    %
    % Reads and parses the file opened by OpenFile using the default module
    % name DefaultModuleName. If ReturnTimestamp is `yes', attempt to return
    % the modification timestamp in MaybeModuleTimestamp. Error is
    % `fatal_module_errors' if the file coudn't be opened, `some_module_errors'
    % if a syntax error was detected, and `no_module_errors' otherwise.
    % MaybeFileInfo is the information about the file (usually the file or
    % directory name) returned by OpenFile. ActualModuleName is the module name
    % specified in the `:- module' declaration, if any, or the
    % DefaultModuleName if there is no `:- module' declaration.
    % Specs is a list of warning/error messages. Program is the parse tree.
    %
:- pred read_module(open_file(FileInfo)::in(open_file),
    module_name::in, maybe_return_timestamp::in, maybe(FileInfo)::out,
    module_name::out, list(item)::out, list(error_spec)::out,
    module_error::out, maybe(io.res(timestamp))::out, io::di, io::uo) is det.

:- pred read_module_if_changed(open_file(FileInfo)::in(open_file),
    module_name::in, timestamp::in, maybe(FileInfo)::out, module_name::out,
    list(item)::out, list(error_spec)::out, module_error::out,
    maybe(io.res(timestamp))::out, io::di, io::uo) is det.

    % Same as read_module, but use intermod_directories instead of
    % search_directories when searching for the file.
    % Also report an error if the actual module name doesn't match
    % the expected module name.
    %
:- pred read_opt_file(file_name::in, module_name::in, list(item)::out,
    list(error_spec)::out, module_error::out, io::di, io::uo) is det.

    % check_module_has_expected_name(FileName, ExpectedName, ActualName):
    %
    % Check that two module names are equal, and report an error if they
    % aren't.
    %
:- pred check_module_has_expected_name(file_name::in, module_name::in,
    module_name::in, io::di, io::uo) is det.

    % search_for_module_source(Dirs, InterfaceDirs, ModuleName,
    %   FoundSourceFileName, !IO):
    %
    % Look for the source for ModuleName in Dirs. This will also search for
    % files matching partially qualified versions of ModuleName, but only if
    % a more qualified `.m' or `.int' file doesn't exist in InterfaceDirs.
    % in InterfaceDirs. For example, module foo.bar.baz can be found in
    % foo.bar.m, bar.baz.m or bar.m.
    %
:- pred search_for_module_source(list(dir_name)::in, list(dir_name)::in,
    module_name::in, maybe_error(file_name)::out, io::di, io::uo) is det.

    % Read the first item from the given file to find the module name.
    %
:- pred find_module_name(file_name::in, maybe(module_name)::out,
    io::di, io::uo) is det.

    % parse_item(ModuleName, VarSet, Term, MaybeItem):
    %
    % Parse Term. If successful, MaybeItem is bound to the parsed item,
    % otherwise it is bound to an appropriate error message. Qualify
    % appropriate parts of the item, with ModuleName as the module name.
    %
:- pred parse_item(module_name::in, varset::in, term::in, maybe1(item)::out)
    is det.

    % parse_decl(ModuleName, VarSet, Term, Result):
    %
    % Parse Term as a declaration. If successful, Result is bound to the
    % parsed item, otherwise it is bound to an appropriate error message.
    % Qualify appropriate parts of the item, with ModuleName as the module
    % name.
    %
:- pred parse_decl(module_name::in, varset::in, term::in, maybe1(item)::out)
    is det.

    % parse_type_defn_head(ModuleName, VarSet, Head, HeadResult):
    %
    % Check the head of a type definition for errors.
    %
:- pred parse_type_defn_head(module_name::in, varset::in, term::in,
    maybe2(sym_name, list(type_param))::out) is det.

    % parse_type_decl_where_part_if_present(TypeSymName, Arity,
    %   IsSolverType, Inst, ModuleName, Term0, Term, Result):
    %
    % Checks if Term0 is a term of the form `<body> where <attributes>'.
    % If so, returns the `<body>' in Term and the parsed `<attributes>'
    % in Result. If not, returns Term = Term0 and Result = no.
    %
:- pred parse_type_decl_where_part_if_present(is_solver_type::in,
    module_name::in, varset::in, term::in, term::out,
    maybe2(maybe(solver_type_details), maybe(unify_compare))::out) is det.

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

% A QualifiedTerm is one of
%   Name(Args)
%   Module.Name(Args)
% (or if Args is empty, one of
%   Name
%   Module.Name)
% where Module is a SymName. For backwards compatibility, we allow `__'
% as an alternative to `.'.

    % Sym_name_and_args takes a term and returns a sym_name that is its
    % top function symbol, and a list of its argument terms. It fails
    % if the input is not valid syntax for a QualifiedTerm.
    %
:- pred sym_name_and_args(term(T)::in, sym_name::out, list(term(T))::out)
    is semidet.

    % parse_qualified_term(Term, _ContainingTerm, VarSet, ContextPieces,
    %   Result):
    %
    % Parse Term into a sym_name that is its top function symbol and a
    % list of its argument terms, and if successful return them in Result.
    % (parse_qualified_term thus does the same job as sym_name_and_args
    % if it succeeds.) However, in case it does not succced,
    % parse_qualified_term also takes as input Varset (from which the variables
    % in Term are taken), the term containing Term, and a format_component
    % list describing the context from which it was called, e.g.
    % "In clause head:". XXX Currently, _ContainingTerm isn't used;
    % maybe it should be deleted.
    %
    % Note: parse_qualified_term is used for places where a symbol is _used_,
    % where no default module name exists for the sym_name. For places
    % where a symbol is _defined_, use parse_implicitly_qualified_term.
    %
    % If you care only about the case where Result = ok2(SymName, Args),
    % use sym_name_and_args.
    %
:- pred parse_qualified_term(term(T)::in, term(T)::in, varset::in,
    list(format_component)::in, maybe_functor(T)::out) is det.

    % parse_implicitly_qualified_term(ModuleName, Term, _ContainingTerm,
    %   VarSet, ContextPieces, Result):
    %
    % Parse Term into a sym_name that is its top function symbol and a
    % list of its argument terms, and if successful return them in Result.
    % This predicate thus does almost the same job as the predicate
    % parse_implicitly_qualified_term above, the difference being that
    % that if the sym_name is qualified, then we check whether it is qualified
    % with ModuleName, and if it isn't qualified, then we qualify it with
    % Modulename (unless ModuleName is root_module_name). This is the
    % right thing to do for clause heads, which is the intended job of
    % parse_implicitly_qualified_term.
    %
:- pred parse_implicitly_qualified_term(module_name::in, term(T)::in,
    term(T)::in, varset::in, list(format_component)::in, maybe_functor(T)::out)
    is det.

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

    % Replace all occurrences of inst_var(I) with
    % constrained_inst_var(I, ground(shared, none)).
    %
:- pred constrain_inst_vars_in_mode(mer_mode::in, mer_mode::out) is det.

    % Replace all occurrences of inst_var(I) with
    % constrained_inst_var(I, Inst) where I -> Inst is in the inst_var_sub.
    % If I is not in the inst_var_sub, default to ground(shared, none).
    %
:- pred constrain_inst_vars_in_mode(inst_var_sub::in,
    mer_mode::in, mer_mode::out) is det.

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

    % Check that for each constrained_inst_var all occurrences have the
    % same constraint.
    %
:- pred inst_var_constraints_are_consistent_in_modes(list(mer_mode)::in)
    is semidet.

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

:- implementation.

:- import_module libs.compiler_util.
:- import_module libs.globals.
:- import_module libs.options.
:- import_module parse_tree.file_names.
:- import_module parse_tree.mercury_to_mercury.
:- import_module parse_tree.prog_io_dcg.
:- import_module parse_tree.prog_io_goal.
:- import_module parse_tree.prog_io_pragma.
:- import_module parse_tree.prog_io_typeclass.
:- import_module parse_tree.prog_io_util.
:- import_module parse_tree.prog_mode.
:- import_module parse_tree.prog_out.
:- import_module parse_tree.prog_type.
:- import_module parse_tree.prog_util.
:- import_module recompilation.
:- import_module recompilation.version.

:- import_module assoc_list.
:- import_module bool.
:- import_module dir.
:- import_module int.
:- import_module map.
:- import_module pair.
:- import_module parser.
:- import_module set.
:- import_module string.
:- import_module term_io.
:- import_module unit.

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

read_module(OpenFile, DefaultModuleName, ReturnTimestamp, FileData,
        ModuleName, Items, Specs, Error, MaybeModuleTimestamp, !IO) :-
    read_module_2(OpenFile, DefaultModuleName, no, ReturnTimestamp,
        FileData, ModuleName, Items, Specs, Error, MaybeModuleTimestamp, !IO).

read_module_if_changed(OpenFile, DefaultModuleName, OldTimestamp, FileData,
        ModuleName, Items, Specs, Error, MaybeModuleTimestamp, !IO) :-
    read_module_2(OpenFile, DefaultModuleName, yes(OldTimestamp),
        do_return_timestamp,
        FileData, ModuleName, Items, Specs, Error,MaybeModuleTimestamp, !IO).

read_opt_file(FileName, DefaultModuleName, Items, Specs, Error, !IO) :-
    globals.io_lookup_accumulating_option(intermod_directories, Dirs, !IO),
    read_module_2(search_for_file(Dirs, FileName), DefaultModuleName, no,
        do_not_return_timestamp, _, ModuleName, Items, Specs, Error, _, !IO),
    check_module_has_expected_name(FileName, DefaultModuleName, ModuleName,
        !IO).

check_module_has_expected_name(FileName, ExpectedName, ActualName, !IO) :-
    ( ActualName \= ExpectedName ->
        Pieces = [words("Error: file"), quote(FileName),
            words("contains the wrong module."), nl,
            words("Expected module"), sym_name(ExpectedName), suffix(","),
            words("found module"), sym_name(ActualName), suffix("."), nl],
        write_error_pieces_plain(Pieces, !IO),
        io.set_exit_status(1, !IO)
    ;
        true
    ).

    % This implementation uses io.read_term to read in the program one term
    % at a time, and then converts those terms into clauses and declarations,
    % checking for errors as it goes. Note that rather than using difference
    % lists, we just build up the lists of items and messages in reverse order
    % and then reverse them afterwards. (Using difference lists would require
    % late-input modes.)
    %
:- pred read_module_2(open_file(T)::in(open_file), module_name::in,
    maybe(timestamp)::in, maybe_return_timestamp::in, maybe(T)::out,
    module_name::out, list(item)::out, list(error_spec)::out,
    module_error::out, maybe(io.res(timestamp))::out, io::di, io::uo) is det.

read_module_2(OpenFile, DefaultModuleName, MaybeOldTimestamp, ReturnTimestamp,
        MaybeFileData, ModuleName, Items, Specs, Error,
        MaybeModuleTimestamp, !IO) :-
    io.input_stream(OldInputStream, !IO),
    OpenFile(OpenResult, !IO),
    (
        OpenResult = ok(FileData),
        MaybeFileData = yes(FileData),
        (
            ReturnTimestamp = do_return_timestamp,
            io.input_stream_name(InputStreamName, !IO),
            io.file_modification_time(InputStreamName, TimestampResult, !IO),
            (
                TimestampResult = ok(Timestamp),
                MaybeModuleTimestamp = yes(ok(time_t_to_timestamp(Timestamp)))
            ;
                TimestampResult = error(IOError),
                MaybeModuleTimestamp = yes(error(IOError))
            )
        ;
            ReturnTimestamp = do_not_return_timestamp,
            MaybeModuleTimestamp = no
        ),
        (
            MaybeOldTimestamp = yes(OldTimestamp),
            MaybeModuleTimestamp = yes(ok(OldTimestamp))
        ->
            % XXX Currently smart recompilation won't work
            % if ModuleName \= DefaultModuleName.
            % In that case, smart recompilation will be disabled
            % and read_module should never be passed an old timestamp.

            ModuleName = DefaultModuleName,
            Items = [],
            Specs = [],
            Error = no_module_errors
        ;
            read_all_items(DefaultModuleName, ModuleName, Items,
                Specs, Error, !IO)
        ),
        io.set_input_stream(OldInputStream, ModuleInputStream, !IO),
        io.close_input(ModuleInputStream, !IO)
    ;
        OpenResult = error(ErrorMsg),
        MaybeFileData = no,
        ModuleName = DefaultModuleName,
        Items = [],
        MaybeModuleTimestamp = no,

        io.progname_base("mercury_compile", Progname, !IO),
        Pieces = [fixed(Progname), suffix(":"), words(ErrorMsg), nl],
        Spec = error_spec(severity_error, phase_read_files,
            [error_msg(no, treat_as_first, 0, [always(Pieces)])]),
        Specs = [Spec],
        Error = fatal_module_errors
    ).

search_for_module_source(Dirs, InterfaceDirs,
        ModuleName, MaybeFileName, !IO) :-
    search_for_module_source_2(Dirs, ModuleName, ModuleName,
        MaybeFileName0, !IO),
    (
        MaybeFileName0 = ok(SourceFileName),
        (
            string.remove_suffix(dir.basename(SourceFileName),
                ".m", SourceFileBaseName),
            file_name_to_module_name(SourceFileBaseName, SourceFileModuleName),
            ModuleName \= SourceFileModuleName
        ->
            % The module name doesn't match the file name. Return an error
            % if there is a more qualified matching `.m' or `.int' file in
            % the interface search path. This avoids having a file `read.m'
            % in the current directory prevent the compiler from finding
            % `bit_buffer.read.int' in the standard library.
            %
            io.input_stream(SourceStream, !IO),
            search_for_module_source_2(InterfaceDirs, ModuleName,
                ModuleName, MaybeFileName2, !IO),
            ( MaybeFileName2 = ok(_) ->
                io.seen(!IO)
            ;
                true
            ),
            (
                MaybeFileName2 = ok(SourceFileName2),
                SourceFileName2 \= SourceFileName,
                string.remove_suffix(dir.basename(SourceFileName2), ".m",
                    SourceFileBaseName2),
                file_name_to_module_name(SourceFileBaseName2,
                    SourceFileModuleName2),
                match_sym_name(SourceFileModuleName, SourceFileModuleName2)
            ->
                io.close_input(SourceStream, !IO),
                MaybeFileName = error(find_source_error(ModuleName,
                                    Dirs, yes(SourceFileName2)))
            ;
                module_name_to_file_name(ModuleName, ".int",
                    do_not_create_dirs, IntFile, !IO),
                search_for_file_returning_dir(InterfaceDirs, IntFile,
                    MaybeIntDir, !IO),
                ( MaybeIntDir = ok(_) ->
                    io.seen(!IO)
                ;
                    true
                ),
                (
                    MaybeIntDir = ok(IntDir),
                    IntDir \= dir.this_directory
                ->
                    io.close_input(SourceStream, !IO),
                    MaybeFileName = error(find_source_error(ModuleName,
                                        Dirs, yes(IntDir/IntFile)))
                ;
                    io.set_input_stream(SourceStream, _, !IO),
                    MaybeFileName = MaybeFileName0
                )
            )
        ;
            MaybeFileName = MaybeFileName0
        )
    ;
        MaybeFileName0 = error(_),
        MaybeFileName = MaybeFileName0
    ).

:- func find_source_error(module_name, list(dir_name),
            maybe(file_name)) = string.

find_source_error(ModuleName, Dirs, MaybeBetterMatch) = Msg :-
    ModuleNameStr = sym_name_to_string(ModuleName),
    Msg0 = "cannot find source for module `" ++ ModuleNameStr ++
            "' in directories " ++ string.join_list(", ", Dirs),
    (
        MaybeBetterMatch = no, Msg = Msg0
    ;
        MaybeBetterMatch = yes(BetterMatchFile),
        Msg = Msg0 ++ ", but found " ++ BetterMatchFile
                    ++ " in interface search path"
    ).

:- pred search_for_module_source_2(list(dir_name)::in, module_name::in,
    module_name::in, maybe_error(file_name)::out, io::di, io::uo) is det.

search_for_module_source_2(Dirs, ModuleName, PartialModuleName, Result, !IO) :-
    module_name_to_file_name(PartialModuleName, ".m", do_not_create_dirs,
        FileName, !IO),
    search_for_file(Dirs, FileName, Result0, !IO),
    (
        Result0 = ok(_),
        Result = Result0
    ;
        Result0 = error(_),
        ( PartialModuleName1 = drop_one_qualifier(PartialModuleName) ->
            search_for_module_source_2(Dirs, ModuleName, PartialModuleName1,
                Result, !IO)
        ;
            Result = error(find_source_error(ModuleName, Dirs, no))
        )
    ).

:- func drop_one_qualifier(module_name) = module_name is semidet.

drop_one_qualifier(qualified(ParentQual, ChildName)) =
    drop_one_qualifier_2(ParentQual, ChildName).

:- func drop_one_qualifier_2(module_name, string) = module_name.

drop_one_qualifier_2(ParentQual, ChildName) =  PartialQual :-
    (
        ParentQual = unqualified(_ParentName),
        PartialQual = unqualified(ChildName)
    ;
        ParentQual = qualified(GrandParentQual, ParentName),
        PartialGrandParentQual = drop_one_qualifier_2(GrandParentQual,
            ParentName),
        PartialQual = qualified(PartialGrandParentQual, ChildName)
    ).

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

:- type module_end
    --->    module_end_no
    ;       module_end_yes(module_name, prog_context).

    % Extract the final `:- end_module' declaration if any.
    %
:- pred get_end_module(module_name::in, list(item)::in, list(item)::out,
    module_end::out) is det.

get_end_module(ModuleName, RevItems0, RevItems, EndModule) :-
    (
        % Note: if the module name in the end_module declaration does not match
        % what we expect, given the source file name, then we assume that it is
        % for a nested module, and so we leave it alone. If it is not for a
        % nested module, the error will be caught by make_hlds.

        RevItems0 = [Item | RevItemsPrime],
        Item = item_module_defn(ItemModuleDefn),
        ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
        ModuleDefn = md_end_module(ModuleName)
    ->
        RevItems = RevItemsPrime,
        EndModule = module_end_yes(ModuleName, Context)
    ;
        RevItems = RevItems0,
        EndModule = module_end_no
    ).

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

    % Check that the module starts with a :- module declaration,
    % and that the end_module declaration (if any) is correct,
    % and construct the final parsing result.
    %
:- pred check_end_module(module_end::in, list(item)::in, list(item)::out,
    list(error_spec)::in, list(error_spec)::out,
    module_error::in, module_error::out) is det.

check_end_module(EndModule, !Items, !Specs, !Error) :-
    % Double-check that the first item is a `:- module ModuleName' declaration,
    % and remove it from the front of the item list.
    (
        !.Items = [Item | !:Items],
        Item = item_module_defn(ItemModuleDefn),
        ItemModuleDefn = item_module_defn_info(md_module(ModuleName1), _)
    ->
        % Check that the end module declaration (if any) matches
        % the begin module declaration.
        (
            EndModule = module_end_yes(EndModuleName, EndModuleContext),
            ModuleName1 \= EndModuleName
        ->
            Pieces = [words("Error:"),
                quote(":- end_module"), words("declaration"),
                words("does not match"),
                quote(":- module"), words("declaration."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(EndModuleContext, [always(Pieces)])]),
            !:Specs = [Spec | !.Specs],
            !:Error = some_module_errors
        ;
            true
        )
    ;
        % If there's no `:- module' declaration at this point, it is
        % an internal error -- read_first_item should have inserted one.
        unexpected(this_file,
            "check_end_module: no `:- module' declaration")
    ).

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

    % Create a dummy term. Used for error messages that are not associated
    % with any particular term or context.
    %
:- pred dummy_term(term::out) is det.

dummy_term(Term) :-
    term.context_init(Context),
    dummy_term_with_context(Context, Term).

    % Create a dummy term with the specified context.
    % Used for error messages that are associated with some specific
    % context, but for which we don't want to print out the term
    % (or for which the term isn't available to be printed out).
    %
:- pred dummy_term_with_context(term.context::in, term::out) is det.

dummy_term_with_context(Context, Term) :-
    Term = term.functor(term.atom(""), [], Context).

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

find_module_name(FileName, MaybeModuleName, !IO) :-
    io.open_input(FileName, OpenRes, !IO),
    (
        OpenRes = ok(InputStream),
        io.set_input_stream(InputStream, OldInputStream, !IO),
        ( string.remove_suffix(FileName, ".m", PartialFileName0) ->
            PartialFileName = PartialFileName0
        ;
            PartialFileName = FileName
        ),
        ( dir.basename(PartialFileName, BaseName0) ->
            BaseName = BaseName0
        ;
            BaseName = ""
        ),
        file_name_to_module_name(BaseName, DefaultModuleName),
        read_first_item(DefaultModuleName, FileName, _,
            ModuleName, _, _, Specs, _, !IO),
        MaybeModuleName = yes(ModuleName),
        % XXX _NumErrors
        globals.io_get_globals(Globals, !IO),
        write_error_specs(Specs, Globals, 0, _NumWarnings, 0, _NumErrors, !IO),
        io.set_input_stream(OldInputStream, _, !IO),
        io.close_input(InputStream, !IO)
    ;
        OpenRes = error(Error),
        ErrorMsg = io.error_message(Error),
        io.progname_base("mercury_compile", Progname, !IO),
        Pieces = [fixed(Progname), suffix(":"), words("error opening"),
            quote(FileName), suffix(":"), words(ErrorMsg), suffix("."), nl],
        Spec = error_spec(severity_error, phase_read_files,
            [error_msg(no, treat_as_first, 0, [always(Pieces)])]),
        globals.io_get_globals(Globals, !IO),
        % XXX _NumErrors
        write_error_spec(Spec, Globals, 0, _NumWarnings, 0, _NumErrors, !IO),
        MaybeModuleName = no
    ).

    % Read a source file from standard in, first reading in
    % the input term by term and then parsing those terms and producing
    % a high-level representation.
    % Parsing is actually a 3-stage process instead of the
    % normal two-stage process:
    %   lexical analysis (chars -> tokens),
    %   parsing stage 1 (tokens -> terms),
    %   parsing stage 2 (terms -> items).
    % The final stage produces a list of program items, each of which
    % may be a declaration or a clause.
    %
    % We use a continuation-passing style here.
    %
:- pred read_all_items(module_name::in, module_name::out,
    list(item)::out, list(error_spec)::out, module_error::out,
    io::di, io::uo) is det.

read_all_items(DefaultModuleName, ModuleName, Items, Specs, Error, !IO) :-
    % Read all the items (the first one is handled specially).
    io.input_stream(Stream, !IO),
    io.input_stream_name(Stream, SourceFileName0, !IO),
    read_first_item(DefaultModuleName, SourceFileName0, SourceFileName,
        ModuleName, RevItems0, MaybeSecondTerm, Specs0, Error0, !IO),
    (
        MaybeSecondTerm = yes(SecondTerm),
        % XXX Should this be SourceFileName instead of SourceFileName0?
        read_term_to_item_result(ModuleName, SourceFileName0, SecondTerm,
            MaybeSecondItem),

        read_items_loop_2(MaybeSecondItem, ModuleName, SourceFileName,
            RevItems0, RevItems1, Specs0, Specs1, Error0, Error1, !IO)
    ;
        MaybeSecondTerm = no,
        read_items_loop(ModuleName, SourceFileName,
            RevItems0, RevItems1, Specs0, Specs1, Error0, Error1, !IO)
    ),

    % Get the end_module declaration (if any), check that it matches
    % the initial module declaration (if any), and remove both of them
    % from the final item list.
    get_end_module(ModuleName, RevItems1, RevItems, EndModule),
    check_end_module(EndModule, Items0, Items, Specs1, Specs, Error1, Error),
    list.reverse(RevItems, Items0).

    % We need to jump through a few hoops when reading the first item,
    % to allow the initial `:- module' declaration to be optional.
    % The reason is that in order to parse an item, we need to know
    % which module it is defined in (because we do some module
    % qualification and checking of module qualifiers at parse time),
    % but the initial `:- module' declaration and the declaration
    % that follows it occur in different scopes, so we need to know
    % what it is that we're parsing before we can parse it!
    % We solve this dilemma by first parsing it in the root scope,
    % and then if it turns out to not be a `:- module' declaration
    % we reparse it in the default module scope. Blecchh.
    %
:- pred read_first_item(module_name::in, file_name::in, file_name::out,
    module_name::out, list(item)::out, maybe(read_term)::out,
    list(error_spec)::out, module_error::out, io::di, io::uo) is det.

read_first_item(DefaultModuleName, !SourceFileName, ModuleName,
        Items, MaybeSecondTerm, Specs, Error, !IO) :-
    % Parse the first term, treating it as occurring within the scope
    % of the special "root" module (so that any `:- module' declaration
    % is taken to be a non-nested module unless explicitly qualified).
    parser.read_term_filename(!.SourceFileName, MaybeFirstTerm, !IO),
    root_module_name(RootModuleName),
    read_term_to_item_result(RootModuleName, !.SourceFileName, MaybeFirstTerm,
        MaybeFirstItem),
    (
        % Apply and then skip `pragma source_file' decls, by calling ourselves
        % recursively with the new source file name.
        MaybeFirstItem = read_item_ok(FirstItem),
        FirstItem = item_pragma(FirstItemPragma),
        FirstItemPragma = item_pragma_info(_,
            pragma_source_file(!:SourceFileName), _)
    ->
        read_first_item(DefaultModuleName, !SourceFileName,
            ModuleName, Items, MaybeSecondTerm, Specs, Error, !IO)
    ;
        % Check if the first term was a `:- module' decl.
        MaybeFirstItem = read_item_ok(FirstItem),
        FirstItem = item_module_defn(FirstItemModuleDefn),
        FirstItemModuleDefn = item_module_defn_info(ModuleDefn, FirstContext),
        ModuleDefn = md_module(StartModuleName)
    ->
        % If so, then check that it matches the expected module name,
        % and if not, report a warning.
        ( match_sym_name(StartModuleName, DefaultModuleName) ->
            ModuleName = DefaultModuleName,
            Specs = []
        ; match_sym_name(DefaultModuleName, StartModuleName) ->
            ModuleName = StartModuleName,
            Specs = []
        ;
            % XXX I think this should be an error, not a warning. -zs
            Pieces = [words("Warning: source file"), quote(!.SourceFileName),
                words("contains module named"), sym_name(StartModuleName),
                suffix("."), nl],
            Severity = severity_conditional(warn_wrong_module_name, yes,
                severity_warning, no),
            Msgs = [option_is_set(warn_wrong_module_name, yes,
                [always(Pieces)])],
            Spec = error_spec(Severity, phase_term_to_parse_tree,
                [simple_msg(FirstContext, Msgs)]),
            Specs = [Spec],

            % Which one should we use here? We used to use the default module
            % name (computed from the filename) but now we use the declared
            % one.
            ModuleName = StartModuleName
        ),
        make_module_decl(ModuleName, FirstContext, FixedFirstItem),
        Items = [FixedFirstItem],
        Error = no_module_errors,
        MaybeSecondTerm = no
    ;
        % If the first term was not a `:- module' decl, then issue a warning
        % (if warning enabled), and insert an implicit `:- module ModuleName'
        % decl.
        ( MaybeFirstItem = read_item_ok(FirstItem) ->
            FirstContext = get_item_context(FirstItem)
        ;
            term.context_init(!.SourceFileName, 1, FirstContext)
        ),
        % XXX I think this should be an error, not a warning. -zs
        Pieces = [words("Warning: module should start with a"),
            quote(":- module"), words("declaration."), nl],
        Severity = severity_conditional(warn_missing_module_name, yes,
            severity_warning, no),
        Msgs  = [option_is_set(warn_missing_module_name, yes,
            [always(Pieces)])],
        Spec = error_spec(Severity, phase_term_to_parse_tree,
            [simple_msg(FirstContext, Msgs)]),
        Specs = [Spec],

        ModuleName = DefaultModuleName,
        make_module_decl(ModuleName, FirstContext, FixedFirstItem),

        % Reparse the first term, this time treating it as occuring within
        % the scope of the implicit `:- module' decl rather than in the
        % root module.
        MaybeSecondTerm = yes(MaybeFirstTerm),
        Items = [FixedFirstItem],
        Error = no_module_errors
    ).

:- pred make_module_decl(module_name::in, term.context::in, item::out) is det.

make_module_decl(ModuleName, Context, Item) :-
    ModuleDefn = md_module(ModuleName),
    ItemInfo = item_module_defn_info(ModuleDefn, Context),
    Item = item_module_defn(ItemInfo).

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

    % The code below was carefully optimized to run efficiently in NU-Prolog.
    % We used to call read_item(MaybeItem) - which does all the work for
    % a single item - via io.gc_call/1, which called the goal with
    % garbage collection. But optimizing for NU-Prolog is no longer a concern.

:- pred read_items_loop(module_name::in, file_name::in,
    list(item)::in, list(item)::out,
    list(error_spec)::in, list(error_spec)::out,
    module_error::in, module_error::out, io::di, io::uo) is det.

read_items_loop(ModuleName, SourceFileName, !Items, !Specs, !Error, !IO) :-
    read_item(ModuleName, SourceFileName, MaybeItem, !IO),
    read_items_loop_2(MaybeItem, ModuleName, SourceFileName, !Items,
        !Specs, !Error, !IO).

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

:- pred read_items_loop_2(read_item_result::in, module_name::in,
    file_name::in, list(item)::in, list(item)::out,
    list(error_spec)::in, list(error_spec)::out,
    module_error::in, module_error::out, io::di, io::uo) is det.

read_items_loop_2(MaybeItemOrEOF, !.ModuleName, !.SourceFileName, !Items,
        !Specs, !Error, !IO) :-
    (
        MaybeItemOrEOF = read_item_eof
        % If the next item was end-of-file, then we're done.
    ;
        % If the next item had some errors, then insert them
        % in the list of errors and continue looping.

        MaybeItemOrEOF = read_item_errors(ItemSpecs),
        !:Specs = ItemSpecs ++ !.Specs,
        !:Error = some_module_errors,
        read_items_loop(!.ModuleName, !.SourceFileName, !Items,
            !Specs, !Error, !IO)
    ;
        MaybeItemOrEOF = read_item_ok(Item),
        read_items_loop_ok(Item, !ModuleName, !SourceFileName, !Items,
            !Specs, !Error, !IO),
        read_items_loop(!.ModuleName, !.SourceFileName, !Items,
            !Specs, !Error, !IO)
    ).

:- pred read_items_loop_ok(item::in, module_name::in, module_name::out,
    file_name::in, file_name::out, list(item)::in, list(item)::out,
    list(error_spec)::in, list(error_spec)::out,
    module_error::in, module_error::out, io::di, io::uo) is det.

read_items_loop_ok(Item0, !ModuleName, !SourceFileName, !Items,
        !Specs, !Error, !IO) :-
    (
        Item0 = item_nothing(ItemNothing0),
        ItemNothing0 = item_nothing_info(yes(Warning), Context0)
    ->
        Warning = item_warning(MaybeOption, Msg, Term),
        (
            MaybeOption = yes(Option),
            globals.io_lookup_bool_option(Option, Warn, !IO)
        ;
            MaybeOption = no,
            Warn = yes
        ),
        (
            Warn = yes,
            Pieces = [words("Warning: "), words(Msg), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            !:Specs = [Spec | !.Specs],

            globals.io_lookup_bool_option(halt_at_warn, Halt, !IO),
            (
                Halt = yes,
                !:Error = some_module_errors
            ;
                Halt = no
            )
        ;
            Warn = no
        ),
        ItemNothing = item_nothing_info(no, Context0),
        Item = item_nothing(ItemNothing)
    ;
        Item = Item0
    ),

    % If the next item was a valid item, check whether it was a declaration
    % that affects the current parsing context -- i.e. either a `module' or
    % `end_module' declaration, or a `pragma source_file' declaration.
    % If so, set the new parsing context according. Next, unless the item
    % is a `pragma source_file' declaration, insert it into the item list.
    % Then continue looping.
    (
        Item = item_pragma(ItemPragma),
        ItemPragma = item_pragma_info(_, PragmaType, _),
        PragmaType = pragma_source_file(NewSourceFileName)
    ->
        !:SourceFileName = NewSourceFileName
    ;
        Item = item_module_defn(ItemModuleDefn)
    ->
        ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
        ( ModuleDefn = md_module(NestedModuleName) ->
            !:ModuleName = NestedModuleName,
            !:Items = [Item | !.Items]
        ; ModuleDefn = md_end_module(NestedModuleName) ->
            root_module_name(RootModuleName),
            sym_name_get_module_name_default(NestedModuleName, RootModuleName,
                ParentModuleName),
            !:ModuleName = ParentModuleName,
            !:Items = [Item | !.Items]
        ; ModuleDefn = md_import(Modules) ->
            ImportItems = list.map(make_pseudo_import_module_decl(Context),
                Modules),
            !:Items = ImportItems ++ !.Items
        ; ModuleDefn = md_use(Modules) ->
            UseItems = list.map(make_pseudo_use_module_decl(Context),
                Modules),
            !:Items = UseItems ++ !.Items
        ; ModuleDefn = md_include_module(Modules) ->
            IncludeItems = list.map(make_pseudo_include_module_decl(Context),
                Modules),
            !:Items = IncludeItems ++ !.Items
        ;
            !:Items = [Item | !.Items]
        )
    ;
        !:Items = [Item | !.Items]
    ).

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

:- func make_pseudo_import_module_decl(prog_context, module_specifier) = item.

make_pseudo_import_module_decl(Context, ModuleSpecifier) = Item :-
    ModuleDefn = md_import([ModuleSpecifier]),
    ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
    Item = item_module_defn(ItemModuleDefn).

:- func make_pseudo_use_module_decl(prog_context, module_specifier) = item.

make_pseudo_use_module_decl(Context, ModuleSpecifier) = Item :-
    ModuleDefn = md_use([ModuleSpecifier]),
    ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
    Item = item_module_defn(ItemModuleDefn).

:- func make_pseudo_include_module_decl(prog_context, module_name) = item.

make_pseudo_include_module_decl(Context, ModuleSpecifier) = Item :-
    ModuleDefn = md_include_module([ModuleSpecifier]),
    ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
    Item = item_module_defn(ItemModuleDefn).

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

:- type read_item_result
    --->    read_item_eof
    ;       read_item_errors(list(error_spec))
    ;       read_item_ok(item).

    % Read_item/1 reads a single item, and if it is a valid term parses it.
    %
:- pred read_item(module_name::in, file_name::in, read_item_result::out,
    io::di, io::uo) is det.

read_item(ModuleName, SourceFileName, MaybeItem, !IO) :-
    parser.read_term_filename(SourceFileName, MaybeTerm, !IO),
    read_term_to_item_result(ModuleName, SourceFileName, MaybeTerm, MaybeItem).

:- pred read_term_to_item_result(module_name::in, string::in, read_term::in,
    read_item_result::out) is det.

read_term_to_item_result(ModuleName, FileName, ReadTermResult,
        ReadItemResult) :-
    (
        ReadTermResult = eof,
        ReadItemResult = read_item_eof
    ;
        ReadTermResult = error(ErrorMsg, LineNumber),
        % XXX Do we need to add an "Error:" prefix?
        Pieces = [words(ErrorMsg), suffix("."), nl],
        Context = term.context_init(FileName, LineNumber),
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(Context, [always(Pieces)])]),
        ReadItemResult = read_item_errors([Spec])
    ;
        ReadTermResult = term(VarSet, Term),
        parse_item(ModuleName, VarSet, Term, MaybeItem),
        convert_item(MaybeItem, ReadItemResult)
    ).

:- pred convert_item(maybe1(item)::in, read_item_result::out) is det.

convert_item(ok1(Item), read_item_ok(Item)).
convert_item(error1(Specs), read_item_errors(Specs)).

parse_item(ModuleName, VarSet, Term, Result) :-
    ( Term = term.functor(term.atom(":-"), [Decl], _DeclContext) ->
        % It's a declaration.
        parse_decl(ModuleName, VarSet, Decl, Result)
    ; Term = term.functor(term.atom("-->"), [DCG_H, DCG_B], DCG_Context) ->
        % It's a DCG clause.
        parse_dcg_clause(ModuleName, VarSet, DCG_H, DCG_B, DCG_Context, Result)
    ;
        % It's either a fact or a rule.
        ( Term = term.functor(term.atom(":-"), [H, B], TermContext) ->
            % It's a rule.
            Head = H,
            Body = B,
            TheContext = TermContext
        ;
            % It's a fact.
            Head = Term,
            TheContext = get_term_context(Head),
            Body = term.functor(term.atom("true"), [], TheContext)
        ),
        varset.coerce(VarSet, ProgVarSet),
        process_clause(ModuleName, Term, Head, Body, ProgVarSet, TheContext,
            Result)
    ).

:- pred process_clause(module_name::in, term::in, term::in, term::in,
    prog_varset::in, term.context::in, maybe1(item)::out) is det.

process_clause(ModuleName, Term, Head, Body0, ProgVarSet0, Context, Result) :-
    GoalContextPieces = [],
    parse_goal(Body0, GoalContextPieces, MaybeBody, ProgVarSet0, ProgVarSet),
    (
        MaybeBody = ok1(Body),
        varset.coerce(ProgVarSet, VarSet),
        (
            Head = term.functor(term.atom("="), [FuncHead0, FuncResult], _),
            FuncHead = desugar_field_access(FuncHead0)
        ->
            HeadContextPieces = [words("In equation head:")],
            parse_implicitly_qualified_term(ModuleName, FuncHead, Head,
                VarSet, HeadContextPieces, MaybeFunctor),
            process_func_clause(MaybeFunctor, FuncResult, ProgVarSet, Body,
                Context, Result)
        ;
            HeadContextPieces = [words("In clause head:")],
            parse_implicitly_qualified_term(ModuleName, Head, Term,
                VarSet, HeadContextPieces, MaybeFunctor),
            process_pred_clause(MaybeFunctor, ProgVarSet, Body, Context,
                Result)
        )
    ;
        MaybeBody = error1(Specs),
        Result = error1(Specs)
    ).

:- pred process_pred_clause(maybe_functor::in, prog_varset::in, goal::in,
    prog_context::in, maybe1(item)::out) is det.

process_pred_clause(MaybeFunctor, VarSet, Body, Context, MaybeItem) :-
    (
        MaybeFunctor = ok2(Name, Args0),
        list.map(term.coerce, Args0, Args),
        ItemClause = item_clause_info(user, VarSet, pf_predicate, Name,
            Args, Body, Context),
        Item = item_clause(ItemClause),
        MaybeItem = ok1(Item)
    ;
        MaybeFunctor = error2(Specs),
        MaybeItem = error1(Specs)
    ).

:- pred process_func_clause(maybe_functor::in, term::in, prog_varset::in,
    goal::in, prog_context::in, maybe1(item)::out) is det.

process_func_clause(MaybeFunctor, Result0, VarSet, Body, Context, MaybeItem) :-
    (
        MaybeFunctor = ok2(Name, Args0),
        list.append(Args0, [Result0], Args1),
        list.map(term.coerce, Args1, Args),
        ItemClause = item_clause_info(user, VarSet, pf_function, Name,
            Args, Body, Context),
        Item = item_clause(ItemClause),
        MaybeItem = ok1(Item)
    ;
        MaybeFunctor = error2(Specs),
        MaybeItem = error1(Specs)
    ).

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

:- type decl_attribute
    --->    decl_attr_purity(purity)
    ;       decl_attr_quantifier(quantifier_type, list(var))
    ;       decl_attr_constraints(quantifier_type, term)
            % the term here is the (not yet parsed) list of constraints
    ;       decl_attr_solver_type.

:- type quantifier_type
    --->    quant_type_exist
    ;       quant_type_univ.

    % The term associated with each decl_attribute is the term containing
    % both the attribute and the declaration that that attribute modifies;
    % this term is used when printing out error messages for cases when
    % attributes are used on declarations where they are not allowed.
:- type decl_attrs == assoc_list(decl_attribute, term.context).

parse_decl(ModuleName, VarSet, Term, Result) :-
    parse_decl_2(ModuleName, VarSet, Term, [], Result).

    % parse_decl_2(ModuleName, VarSet, Term, Attributes, Result):
    %
    % Succeeds if Term is a declaration and binds Result to a representation
    % of that declaration. Attributes is a list of enclosing declaration
    % attributes, in the order innermost to outermost.
    %
:- pred parse_decl_2(module_name::in, varset::in, term::in, decl_attrs::in,
    maybe1(item)::out) is det.

parse_decl_2(ModuleName, VarSet, Term, Attributes, Result) :-
    ( Term = term.functor(term.atom(Atom), Args, Context) ->
        (
            parse_decl_attribute(Atom, Args, Attribute, SubTerm)
        ->
            NewAttributes = [Attribute - Context | Attributes],
            parse_decl_2(ModuleName, VarSet, SubTerm, NewAttributes, Result)
        ;
            process_decl(ModuleName, VarSet, Atom, Args, Attributes, Context,
                ResultPrime)
        ->
            ResultPrime = Result
        ;
            TermStr = mercury_term_to_string(VarSet, no, Term),
            Pieces = [words("Error: unrecognized declaration:"), nl,
                words(TermStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(Context, [always(Pieces)])]),
            Result = error1([Spec])
        )
    ;
        Context = get_term_context(Term),
        Pieces = [words("Error: atom expected after `:-'."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(Context, [always(Pieces)])]),
        Result = error1([Spec])
    ).

    % process_decl(ModuleName, VarSet, Attributes, Atom, Args, Result):
    %
    % Succeeds if Atom(Args) is a declaration and binds Result to a
    % representation of that declaration. Attributes is a list of
    % enclosing declaration attributes, in the order outermost to innermost.
    %
:- pred process_decl(module_name::in, varset::in, string::in, list(term)::in,
    decl_attrs::in, prog_context::in, maybe1(item)::out) is semidet.

% XXX Break this up into one predicate per declaration,
% with this predicate doing nothing except switching between them.
process_decl(ModuleName, VarSet, "type", [TypeDecl], Attributes, Context,
        Result) :-
    parse_type_decl(ModuleName, VarSet, TypeDecl, Attributes, Context, Result).

process_decl(ModuleName, VarSet, "pred", [PredDecl], Attributes, Context,
        Result) :-
    parse_type_decl_pred(ModuleName, VarSet, PredDecl, Attributes, Context,
        Result).

process_decl(ModuleName, VarSet, "func", [FuncDecl], Attributes, Context,
        Result) :-
    parse_type_decl_func(ModuleName, VarSet, FuncDecl, Attributes, Context,
        Result).

process_decl(ModuleName, VarSet, "mode", [ModeDecl], Attributes,
        Context, Result) :-
    parse_mode_decl(ModuleName, VarSet, ModeDecl, Attributes, Context, Result).

process_decl(ModuleName, VarSet, "inst", [InstDecl], Attributes,
        Context, Result) :-
    parse_inst_decl(ModuleName, VarSet, InstDecl, Context, Result0),
    check_no_attributes(Result0, Attributes, Result).

process_decl(_ModuleName, VarSet, "import_module", [ModuleSpec], Attributes,
        Context, Result) :-
    parse_symlist_decl(parse_module_specifier(VarSet), make_import,
        ModuleSpec, Attributes, Context, Result).

process_decl(_ModuleName, VarSet, "use_module", [ModuleSpec], Attributes,
        Context, Result) :-
    parse_symlist_decl(parse_module_specifier(VarSet), make_use,
        ModuleSpec, Attributes, Context, Result).

process_decl(_ModuleName, VarSet, "export_module", [ModuleSpec], Attributes,
        Context, Result) :-
    parse_symlist_decl(parse_module_specifier(VarSet), make_export,
        ModuleSpec, Attributes, Context, Result).

process_decl(_ModuleName, _VarSet, "interface", [], Attributes, Context,
        Result) :-
    ItemModuleDefn = item_module_defn_info(md_interface, Context),
    Item = item_module_defn(ItemModuleDefn),
    Result0 = ok1(Item),
    check_no_attributes(Result0, Attributes, Result).

process_decl(_ModuleName, _VarSet, "implementation", [], Attributes, Context,
        Result) :-
    ItemModuleDefn = item_module_defn_info(md_implementation, Context),
    Item = item_module_defn(ItemModuleDefn),
    Result0 = ok1(Item),
    check_no_attributes(Result0, Attributes, Result).

process_decl(ModuleName, VarSet, "external", Args, Attributes, Context,
        Result) :-
    (
        Args = [PredSpec],
        MaybeBackend = no
    ;
        Args = [BackendArg, PredSpec],
        BackendArg = term.functor(term.atom(Functor), [], _),
        (
            Functor = "high_level_backend",
            Backend = high_level_backend
        ;
            Functor = "low_level_backend",
            Backend = low_level_backend
        ),
        MaybeBackend = yes(Backend)
    ),
    parse_implicitly_qualified_symbol_name_specifier(ModuleName, VarSet,
        PredSpec, Result0),
    process_maybe1(make_external(MaybeBackend, Context), Result0, Result1),
    check_no_attributes(Result1, Attributes, Result).

process_decl(DefaultModuleName, VarSet, "module", [ModuleName], Attributes,
        Context, Result) :-
    parse_module_name(DefaultModuleName, VarSet, ModuleName, Result0),
    (
        Result0 = ok1(ModuleNameSym),
        ModuleDefn = md_module(ModuleNameSym),
        ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
        Item = item_module_defn(ItemModuleDefn),
        Result1 = ok1(Item)
    ;
        Result0 = error1(Specs),
        Result1 = error1(Specs)
    ),
    check_no_attributes(Result1, Attributes, Result).

process_decl(DefaultModuleName, VarSet, "include_module", [ModuleNames],
        Attributes, Context, Result) :-
    parse_list(parse_module_name(DefaultModuleName, VarSet), ModuleNames,
        Result0),
    (
        Result0 = ok1(ModuleNameSyms),
        ModuleDefn = md_include_module(ModuleNameSyms),
        ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
        Item = item_module_defn(ItemModuleDefn),
        Result1 = ok1(Item)
    ;
        Result0 = error1(Specs),
        Result1 = error1(Specs)
    ),
    check_no_attributes(Result1, Attributes, Result).

process_decl(DefaultModuleName, VarSet, "end_module", [ModuleName],
        Attributes, Context, Result) :-
    % The name in an `end_module' declaration not inside the scope of the
    % module being ended, so the default module name here is the parent
    % of the previous default module name.

    root_module_name(RootModuleName),
    sym_name_get_module_name_default(DefaultModuleName, RootModuleName,
        ParentOfDefaultModuleName),
    parse_module_name(ParentOfDefaultModuleName, VarSet, ModuleName, Result0),
    (
        Result0 = ok1(ModuleNameSym),
        ModuleDefn = md_end_module(ModuleNameSym),
        ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
        Item = item_module_defn(ItemModuleDefn),
        Result1 = ok1(Item)
    ;
        Result0 = error1(Specs),
        Result1 = error1(Specs)
    ),
    check_no_attributes(Result1, Attributes, Result).

process_decl(ModuleName, VarSet, "pragma", Pragma, Attributes, Context,
        Result):-
    parse_pragma(ModuleName, VarSet, Pragma, Context, Result0),
    check_no_attributes(Result0, Attributes, Result).

process_decl(ModuleName, VarSet, "promise", Assertion, Attributes, Context,
        Result):-
    parse_promise(ModuleName, promise_type_true, VarSet,
        Assertion, Attributes, Context, Result0),
    check_no_attributes(Result0, Attributes, Result).

process_decl(ModuleName, VarSet, "promise_exclusive", PromiseGoal, Attributes,
        Context, Result):-
    parse_promise(ModuleName, promise_type_exclusive, VarSet,
        PromiseGoal, Attributes, Context, Result).

process_decl(ModuleName, VarSet, "promise_exhaustive", PromiseGoal, Attributes,
        Context, Result):-
    parse_promise(ModuleName, promise_type_exhaustive, VarSet,
        PromiseGoal, Attributes, Context, Result).

process_decl(ModuleName, VarSet, "promise_exclusive_exhaustive", PromiseGoal,
        Attributes, Context, Result):-
    parse_promise(ModuleName, promise_type_exclusive_exhaustive, VarSet,
        PromiseGoal, Attributes, Context, Result).

process_decl(ModuleName, VarSet, "typeclass", Args, Attributes, Context,
        Result):-
    parse_typeclass(ModuleName, VarSet, Args, Context, Result0),
    (
        Result0 = ok1(ItemTypeClass),
        Result1 = ok1(item_typeclass(ItemTypeClass))
    ;
        Result0 = error1(Specs),
        Result1 = error1(Specs)
    ),
    check_no_attributes(Result1, Attributes, Result).

process_decl(ModuleName, VarSet, "instance", Args, Attributes, Context,
        Result):-
    parse_instance(ModuleName, VarSet, Args, Context, Result0),
    (
        Result0 = ok1(ItemInstance),
        Result1 = ok1(item_instance(ItemInstance))
    ;
        Result0 = error1(Specs),
        Result1 = error1(Specs)
    ),
    check_no_attributes(Result1, Attributes, Result).

process_decl(ModuleName, VarSet, "version_numbers",
        [VersionNumberTerm, ModuleNameTerm, VersionNumbersTerm],
        Attributes, Context, Result) :-
    parse_module_specifier(VarSet, ModuleNameTerm, ModuleNameResult),
    (
        VersionNumberTerm = term.functor(term.integer(VersionNumber), [], _),
        VersionNumber = version_numbers_version_number
    ->
        (
            ModuleNameResult = ok1(ModuleName),
            recompilation.version.parse_version_numbers(VersionNumbersTerm,
                Result0),
            (
                Result0 = ok1(VersionNumbers),
                ModuleDefn = md_version_numbers(ModuleName, VersionNumbers),
                ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
                Item = item_module_defn(ItemModuleDefn),
                Result1 = ok1(Item),
                check_no_attributes(Result1, Attributes, Result)
            ;
                Result0 = error1(Specs),
                Result = error1(Specs)
            )
        ;
            % XXX _Spec
            ModuleNameResult = error1(_Spec),
            Pieces = [words("Error: invalid module name in"),
                quote(":- version_numbers"), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(ModuleNameTerm),
                    [always(Pieces)])]),
            Result = error1([Spec])
        )
    ;
        (
            VersionNumberTerm = term.functor(_, _, _VersionNumberContext),
            Msg = "interface file needs to be recreated, " ++
                "the version numbers are out of date",
            dummy_term_with_context(Context, DummyTerm),
            Warning = item_warning(yes(warn_smart_recompilation),
                Msg, DummyTerm),
            ItemNothing = item_nothing_info(yes(Warning), Context),
            Item = item_nothing(ItemNothing),
            Result = ok1(Item)
        ;
            VersionNumberTerm = term.variable(_, VersionNumberContext),
            Pieces = [words("Error: invalid version number in"),
                quote(":- version_numbers"), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(VersionNumberContext, [always(Pieces)])]),
            Result = error1([Spec])
        )
    ).

process_decl(ModuleName, VarSet, InitDecl, Args, Attributes, Context,
        Result) :-
    ( InitDecl = "initialise" ; InitDecl = "initialize" ),
    parse_initialise_decl(ModuleName, VarSet, Args, Context, Result0),
    check_no_attributes(Result0, Attributes, Result).

process_decl(ModuleName, VarSet, FinalDecl, Args, Attributes, Context,
        Result) :-
    ( FinalDecl = "finalise" ; FinalDecl = "finalize" ),
    parse_finalise_decl(ModuleName, VarSet, Args, Context, Result0),
    check_no_attributes(Result0, Attributes, Result).

process_decl(ModuleName, VarSet, "mutable", Args, Attributes, Context,
        Result) :-
    parse_mutable_decl(ModuleName, VarSet, Args, Context, Result0),
    check_no_attributes(Result0, Attributes, Result).

:- pred parse_decl_attribute(string::in, list(term)::in, decl_attribute::out,
    term::out) is semidet.

parse_decl_attribute("impure", [Decl],
        decl_attr_purity(purity_impure), Decl).
parse_decl_attribute("semipure", [Decl],
        decl_attr_purity(purity_semipure), Decl).
parse_decl_attribute("<=", [Decl, Constraints],
        decl_attr_constraints(quant_type_univ, Constraints), Decl).
parse_decl_attribute("=>", [Decl, Constraints],
        decl_attr_constraints(quant_type_exist, Constraints), Decl).
parse_decl_attribute("some", [TVars, Decl],
        decl_attr_quantifier(quant_type_exist, TVarsList), Decl) :-
    parse_list_of_vars(TVars, TVarsList).
parse_decl_attribute("all", [TVars, Decl],
        decl_attr_quantifier(quant_type_univ, TVarsList), Decl) :-
    parse_list_of_vars(TVars, TVarsList).
parse_decl_attribute("solver", [Decl], decl_attr_solver_type, Decl).

:- pred check_no_attributes(maybe1(T)::in, decl_attrs::in, maybe1(T)::out)
    is det.

check_no_attributes(Result0, Attributes, Result) :-
    (
        Result0 = ok1(_),
        Attributes = [Attr - Context | _]
    ->
        % XXX Shouldn't we mention EVERY element of Attributes?
        Pieces = [words("Error:"), words(attribute_description(Attr)),
            words("not allowed here."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(Context, [always(Pieces)])]),
        Result = error1([Spec])
    ;
        Result = Result0
    ).

:- func attribute_description(decl_attribute) = string.

attribute_description(decl_attr_purity(_)) = "purity specifier".
attribute_description(decl_attr_quantifier(quant_type_univ, _)) =
    "universal quantifier (`all')".
attribute_description(decl_attr_quantifier(quant_type_exist, _)) =
    "existential quantifier (`some')".
attribute_description(decl_attr_constraints(quant_type_univ, _)) =
    "type class constraint (`<=')".
attribute_description(decl_attr_constraints(quant_type_exist, _)) =
    "existentially quantified type class constraint (`=>')".
attribute_description(decl_attr_solver_type) = "solver type specifier".

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

:- pred parse_promise(module_name::in, promise_type::in, varset::in,
    list(term)::in, decl_attrs::in, prog_context::in, maybe1(item)::out)
    is semidet.

parse_promise(ModuleName, PromiseType, VarSet, [Term], Attributes, Context,
        Result) :-
    varset.coerce(VarSet, ProgVarSet0),
    ContextPieces = [],
    parse_goal(Term, ContextPieces, MaybeGoal0, ProgVarSet0, ProgVarSet),
    (
        MaybeGoal0 = ok1(Goal0),
        % Get universally quantified variables.
        (
            PromiseType = promise_type_true,
            ( Goal0 = all_expr(UnivVars0, AllGoal) - _Context ->
                UnivVars0 = UnivVars,
                Goal = AllGoal
            ;
                UnivVars = [],
                Goal = Goal0
            )
        ;
            ( PromiseType = promise_type_exclusive
            ; PromiseType = promise_type_exhaustive
            ; PromiseType = promise_type_exclusive_exhaustive
            ),
            get_quant_vars(quant_type_univ, ModuleName, Attributes, _,
                [], UnivVars0),
            list.map(term.coerce_var, UnivVars0, UnivVars),
            Goal0 = Goal
        ),
        ItemPromise = item_promise_info(PromiseType, Goal, ProgVarSet,
            UnivVars, Context),
        Item = item_promise(ItemPromise),
        Result = ok1(Item)
    ;
        MaybeGoal0 = error1(Specs),
        Result = error1(Specs)
    ).

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

:- pred parse_type_decl(module_name::in, varset::in, term::in, decl_attrs::in,
    prog_context::in, maybe1(item)::out) is det.

parse_type_decl(ModuleName, VarSet, TypeDecl, Attributes, Context, Result) :-
    (
        TypeDecl = term.functor(term.atom(Name), Args, _),
        parse_type_decl_type(ModuleName, VarSet, Name, Args, Attributes, Cond,
            TypeDeclResultPrime)
    ->
        TypeDeclResult = TypeDeclResultPrime,
        Cond1 = Cond
    ;
        process_abstract_type(ModuleName, VarSet, TypeDecl, Attributes,
            TypeDeclResult),
        Cond1 = cond_true
    ),
    % We should check the condition for errors (don't bother at the moment,
    % since we ignore conditions anyhow :-).
    process_maybe1(make_type_defn(VarSet, Cond1, Context), TypeDeclResult,
        Result).

:- pred make_type_defn(varset::in, condition::in, prog_context::in,
    processed_type_body::in, item::out) is det.

make_type_defn(VarSet0, Cond, Context, ProcessedTypeBody, Item) :-
    ProcessedTypeBody = processed_type_body(Name, Args, TypeDefn),
    varset.coerce(VarSet0, VarSet),
    ItemTypeDefn = item_type_defn_info(VarSet, Name, Args, TypeDefn, Cond,
        Context),
    Item = item_type_defn(ItemTypeDefn).

:- pred make_external(maybe(backend)::in, prog_context::in,
    sym_name_specifier::in, item::out) is det.

make_external(MaybeBackend, Context, SymSpec, Item) :-
    ModuleDefn = md_external(MaybeBackend, SymSpec),
    ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
    Item = item_module_defn(ItemModuleDefn).

:- pred get_is_solver_type(is_solver_type::out,
    decl_attrs::in, decl_attrs::out) is det.

get_is_solver_type(IsSolverType, !Attributes) :-
    ( !.Attributes = [decl_attr_solver_type - _ | !:Attributes] ->
        IsSolverType = solver_type
    ;
        IsSolverType = non_solver_type
    ).

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

    % parse_type_decl_type(Term, Condition, Result) succeeds if Term is
    % a "type" type declaration, and binds Condition to the condition for
    % that declaration (if any), and Result to a representation of the
    % declaration.
    %
:- pred parse_type_decl_type(module_name::in, varset::in, string::in,
    list(term)::in, decl_attrs::in, condition::out,
    maybe1(processed_type_body)::out) is semidet.

parse_type_decl_type(ModuleName, VarSet, Connective, [HeadTerm, BodyTerm],
        Attributes0, Condition, Result) :-
    (
        Connective = "--->",
        get_condition(BodyTerm, Body, Condition),
        get_is_solver_type(IsSolverType, Attributes0, Attributes),
        (
            IsSolverType = solver_type,
            Pieces = [words("Error: a solver type:"),
                words("cannot have data constructors."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            IsSolverType = non_solver_type,
            du_type_rhs_ctors_and_where_terms(Body, CtorsTerm, MaybeWhereTerm),
            CtorsResult = convert_constructors(ModuleName, VarSet, CtorsTerm),
            (
                CtorsResult = error1(Specs),
                Result = error1(Specs)
            ;
                CtorsResult = ok1(Ctors),
                WhereResult = parse_type_decl_where_term(non_solver_type,
                    ModuleName, VarSet, MaybeWhereTerm),
                (
                    WhereResult = error2(Specs),
                    Result = error1(Specs)
                ;
                    % The code to process `where' attributes will return
                    % an error result if solver attributes are given for
                    % a non-solver type. Because this is a du type, if the
                    % unification with WhereResult succeeds then
                    % _NoSolverTypeDetails is guaranteed to be `no'.
                    WhereResult = ok2(_NoSolverTypeDetails, MaybeUserEqComp),
                    process_du_type(ModuleName, VarSet, HeadTerm, BodyTerm,
                        Ctors, MaybeUserEqComp, Result0),
                    check_no_attributes(Result0, Attributes, Result)
                )
            )
        )
    ;
        Connective = "==",
        get_condition(BodyTerm, Body, Condition),
        process_eqv_type(ModuleName, VarSet, HeadTerm, Body, Result0),
        check_no_attributes(Result0, Attributes0, Result)
    ;
        Connective = "where",
        get_condition(BodyTerm, Body, Condition),
        get_is_solver_type(IsSolverType, Attributes0, Attributes),
        (
            IsSolverType = non_solver_type,
            Pieces = [words("Error: only solver types can be defined"),
                words("by a `where' block alone."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            IsSolverType = solver_type,
            Result0 = parse_type_decl_where_term(solver_type, ModuleName,
                VarSet, yes(Body)),
            (
                Result0 = error2(Specs),
                Result = error1(Specs)
            ;
                Result0 = ok2(MaybeSolverTypeDetails, MaybeUserEqComp),
                process_solver_type(ModuleName, VarSet, HeadTerm,
                    MaybeSolverTypeDetails, MaybeUserEqComp, Result1),
                check_no_attributes(Result1, Attributes, Result)
            )
        )
    ).

:- pred du_type_rhs_ctors_and_where_terms(term::in,
    term::out, maybe(term)::out) is det.

du_type_rhs_ctors_and_where_terms(Term, CtorsTerm, MaybeWhereTerm) :-
    (
        Term = term.functor(term.atom("where"), Args, _Context),
        Args = [CtorsTerm0, WhereTerm]
    ->
        CtorsTerm      = CtorsTerm0,
        MaybeWhereTerm = yes(WhereTerm)
    ;
        CtorsTerm      = Term,
        MaybeWhereTerm = no
    ).

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

    % parse_type_decl_pred(ModuleName, VarSet, Pred, Attributes, Result)
    % succeeds if Pred is a predicate type declaration, and binds Result
    % to a representation of the declaration.
    %
:- pred parse_type_decl_pred(module_name::in, varset::in, term::in,
    decl_attrs::in, prog_context::in, maybe1(item)::out) is det.

parse_type_decl_pred(ModuleName, VarSet, Pred, Attributes, Context, Result) :-
    get_condition(Pred, Body, Condition),
    get_determinism(VarSet, Body, Body2, MaybeDeterminism),
    get_with_inst(Body2, Body3, WithInst),
    get_with_type(VarSet, Body3, Body4, WithTypeResult),
    ( WithTypeResult = ok1(WithType),
        process_type_decl_pred_or_func(pf_predicate, ModuleName, WithType,
            WithInst, MaybeDeterminism, VarSet, Body4, Condition, Attributes,
            Context, Result)
    ;
        WithTypeResult = error1(Specs),
        Result = error1(Specs)
    ).

:- pred process_type_decl_pred_or_func(pred_or_func::in, module_name::in,
    maybe(mer_type)::in, maybe1(maybe(mer_inst))::in,
    maybe1(maybe(determinism))::in, varset::in, term::in, condition::in,
    decl_attrs::in, prog_context::in, maybe1(item)::out) is det.

process_type_decl_pred_or_func(PredOrFunc, ModuleName, WithType, WithInst0,
        MaybeDeterminism0, VarSet, Body, Condition, Attributes, Context,
        Result) :-
    (
        MaybeDeterminism0 = ok1(MaybeDeterminism),
        (
            WithInst0 = ok1(WithInst),
            ( MaybeDeterminism = yes(_), WithInst = yes(_) ->
                Pieces = [words("Error:"), quote("with_inst"),
                    words("and determinism both specified."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Body), [always(Pieces)])]),
                Result = error1([Spec])
            ; WithInst = yes(_), WithType = no ->
                Pieces = [words("Error:"), quote("with_inst"),
                    words("specified without"), quote("with_type"),
                    suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Body), [always(Pieces)])]),
                Result = error1([Spec])
            ;
                (
                    % Function declarations with `with_type` annotations
                    % have the same form as predicate declarations.
                    PredOrFunc = pf_function,
                    WithType = no
                ->
                    process_func(ModuleName, VarSet, Body, Condition,
                        MaybeDeterminism, Attributes, Context, Result)
                ;
                    process_pred_decl(PredOrFunc, ModuleName, VarSet, Body,
                        Condition, WithType, WithInst, MaybeDeterminism,
                        Attributes, Context, Result)
                )
            )
        ;
            WithInst0 = error1(Specs),
            Result = error1(Specs)
        )
    ;
        MaybeDeterminism0 = error1(Specs),
        Result = error1(Specs)
    ).

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

    % parse_type_decl_func(ModuleName, VarSet, Func, Attributes, Result)
    % succeeds if Func is a function type declaration, and binds Result to
    % a representation of the declaration.
    %
:- pred parse_type_decl_func(module_name::in, varset::in, term::in,
    decl_attrs::in, prog_context::in, maybe1(item)::out) is det.

parse_type_decl_func(ModuleName, VarSet, Func, Attributes, Context, Result) :-
    get_condition(Func, Body, Condition),
    get_determinism(VarSet, Body, Body2, MaybeDeterminism),
    get_with_inst(Body2, Body3, WithInst),
    get_with_type(VarSet, Body3, Body4, WithTypeResult),
    (
        WithTypeResult = ok1(WithType),
        process_type_decl_pred_or_func(pf_function, ModuleName,
            WithType, WithInst, MaybeDeterminism, VarSet, Body4,
            Condition, Attributes, Context, Result)
    ;
        WithTypeResult = error1(Specs),
        Result = error1(Specs)
    ).

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

    % parse_mode_decl_pred(ModuleName, Pred, Condition, Result) succeeds
    % if Pred is a predicate mode declaration, and binds Condition to the
    % condition for that declaration (if any), and Result to a
    % representation of the declaration.
    %
:- pred parse_mode_decl_pred(module_name::in, varset::in, term::in,
    decl_attrs::in, prog_context::in, maybe1(item)::out) is det.

parse_mode_decl_pred(ModuleName, VarSet, Pred, Attributes, Context, Result) :-
    get_condition(Pred, Body, Condition),
    get_determinism(VarSet, Body, Body2, MaybeDeterminism0),
    get_with_inst(Body2, Body3, WithInst0),
    (
        MaybeDeterminism0 = ok1(MaybeDeterminism),
        (
            WithInst0 = ok1(WithInst),
            (
                MaybeDeterminism = yes(_),
                WithInst = yes(_)
            ->
                Pieces = [words("Error:"), quote("with_inst"),
                    words("and determinism both specified."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Body), [always(Pieces)])]),
                Result = error1([Spec])

            ;
                process_mode(ModuleName, VarSet, Body3, Condition, Attributes,
                    WithInst, MaybeDeterminism, Context, Result)
            )
        ;
            WithInst0 = error1(Specs),
            Result = error1(Specs)
        )
    ;
        MaybeDeterminism0 = error1(Specs),
        Result = error1(Specs)
    ).

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

:- pred parse_initialise_decl(module_name::in, varset::in, list(term)::in,
    prog_context::in, maybe1(item)::out) is semidet.

parse_initialise_decl(_ModuleName, VarSet, [Term], Context, Result) :-
    parse_symbol_name_specifier(VarSet, Term, MaybeSymNameSpecifier),
    (
        MaybeSymNameSpecifier = error1(Specs),
        Result = error1(Specs)
    ;
        MaybeSymNameSpecifier = ok1(SymNameSpecifier),
        (
            SymNameSpecifier = name(_),
            TermStr = describe_error_term(VarSet, Term),
            Pieces = [words("Error:"), quote("initialise"),
                words("declaration"), words("requires arity, found"),
                words(TermStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            SymNameSpecifier = name_arity(SymName, Arity),
            (
                ( Arity = 0 ; Arity = 2 )
            ->
                ItemInitialise = item_initialise_info(user, SymName, Arity,
                    Context),
                Item = item_initialise(ItemInitialise),
                Result = ok1(Item)
            ;
                TermStr = describe_error_term(VarSet, Term),
                Pieces = [words("Error:"), quote("initialise"),
                    words("declaration specifies a predicate"),
                    words("whose arity is not zero or two:"),
                    words(TermStr), suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Term), [always(Pieces)])]),
                Result = error1([Spec])
            )
        )
    ).

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

:- pred parse_finalise_decl(module_name::in, varset::in, list(term)::in,
    prog_context::in, maybe1(item)::out) is semidet.

parse_finalise_decl(_ModuleName, VarSet, [Term], Context, Result) :-
    parse_symbol_name_specifier(VarSet, Term, MaybeSymNameSpecifier),
    (
        MaybeSymNameSpecifier = error1(Specs),
        Result = error1(Specs)
    ;
        MaybeSymNameSpecifier = ok1(SymNameSpecifier),
        (
            SymNameSpecifier = name(_),
            TermStr = describe_error_term(VarSet, Term),
            Pieces = [words("Error:"), quote("finalise"),
                words("declaration"), words("requires arity, found"),
                words(TermStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            SymNameSpecifier = name_arity(SymName, Arity),
            (
                ( Arity = 0 ; Arity = 2 )
            ->
                ItemFinalise = item_finalise_info(user, SymName, Arity,
                    Context),
                Item = item_finalise(ItemFinalise),
                Result = ok1(Item)
            ;
                TermStr = describe_error_term(VarSet, Term),
                Pieces = [words("Error:"), quote("finalise"),
                    words("declaration specifies a predicate"),
                    words("whose arity is not zero or two:"),
                    words(TermStr), suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Term), [always(Pieces)])]),
                Result = error1([Spec])
            )
        )
    ).

%-----------------------------------------------------------------------------%
%
% Mutable declarations
%
% See prog_mutable.m for implementation details.
%

:- pred parse_mutable_decl(module_name::in, varset::in, list(term)::in,
    prog_context::in, maybe1(item)::out) is semidet.

parse_mutable_decl(_ModuleName, VarSet, Terms, Context, Result) :-
    Terms = [NameTerm, TypeTerm, ValueTerm, InstTerm | OptMutAttrsTerm],
    parse_mutable_name(NameTerm, NameResult),
    parse_mutable_type(VarSet, TypeTerm, TypeResult),
    term.coerce(ValueTerm, Value),
    varset.coerce(VarSet, ProgVarSet),
    parse_mutable_inst(VarSet, InstTerm, InstResult),

    % The list of attributes is optional.
    (
        OptMutAttrsTerm = [],
        MutAttrsResult = ok1(default_mutable_attributes)
    ;
        OptMutAttrsTerm = [MutAttrsTerm],
        parse_mutable_attrs(VarSet, MutAttrsTerm, MutAttrsResult)
    ),
    (
        NameResult = ok1(Name),
        TypeResult = ok1(Type),
        InstResult = ok1(Inst),
        MutAttrsResult = ok1(MutAttrs)
    ->
        % We *must* attach the varset to the mutable item because if the
        % initial value is non-ground, then the initial value will be a
        % variable and the mutable initialisation predicate will contain
        % references to it.  Ignoring the varset may lead to later compiler
        % passes attempting to reuse this variable when fresh variables are
        % allocated.
        ItemMutable = item_mutable_info(Name, Type, Value, Inst, MutAttrs,
            ProgVarSet, Context),
        Item = item_mutable(ItemMutable),
        Result = ok1(Item)
    ;
        Specs = get_any_errors1(NameResult) ++ get_any_errors1(TypeResult) ++
            get_any_errors1(InstResult) ++ get_any_errors1(MutAttrsResult),
        Result = error1(Specs)
    ).

:- pred parse_mutable_name(term::in, maybe1(string)::out) is det.

parse_mutable_name(NameTerm, NameResult) :-
    ( NameTerm = term.functor(atom(Name), [], _) ->
        NameResult = ok1(Name)
    ;
        Pieces = [words("Error: invalid mutable name."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(NameTerm), [always(Pieces)])]),
        NameResult = error1([Spec])
    ).

:- pred parse_mutable_type(varset::in, term::in, maybe1(mer_type)::out) is det.

parse_mutable_type(VarSet, TypeTerm, TypeResult) :-
    ( term.contains_var(TypeTerm, _) ->
        TypeTermStr = describe_error_term(VarSet, TypeTerm),
        Pieces = [words("Error: the type in a mutable declaration"),
            words("cannot contain variables:"),
            words(TypeTermStr), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(TypeTerm), [always(Pieces)])]),
        TypeResult = error1([Spec])
    ;
        ContextPieces = [],
        parse_type(TypeTerm, VarSet, ContextPieces, TypeResult)
    ).

:- pred parse_mutable_inst(varset::in, term::in, maybe1(mer_inst)::out) is det.

parse_mutable_inst(VarSet, InstTerm, InstResult) :-
    ( term.contains_var(InstTerm, _) ->
        InstTermStr = describe_error_term(VarSet, InstTerm),
        Pieces = [words("Error: the inst in a mutable declaration"),
            words("cannot contain variables:"),
            words(InstTermStr), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(InstTerm), [always(Pieces)])]),
        InstResult = error1([Spec])
    ; convert_inst(no_allow_constrained_inst_var, InstTerm, Inst) ->
        InstResult = ok1(Inst)
    ;
        Pieces = [words("Error: invalid inst in mutable declaration."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(InstTerm), [always(Pieces)])]),
        InstResult = error1([Spec])
    ).

:- type collected_mutable_attribute
    --->    mutable_attr_trailed(mutable_trailed)
    ;       mutable_attr_foreign_name(foreign_name)
    ;       mutable_attr_attach_to_io_state(bool)
    ;       mutable_attr_constant(bool)
    ;       mutable_attr_thread_local(mutable_thread_local).

:- pred parse_mutable_attrs(varset::in, term::in,
    maybe1(mutable_var_attributes)::out) is det.

parse_mutable_attrs(VarSet, MutAttrsTerm, MutAttrsResult) :-
    Attributes0 = default_mutable_attributes,
    ConflictingAttributes = [
        mutable_attr_trailed(mutable_trailed) -
            mutable_attr_trailed(mutable_untrailed),
        mutable_attr_trailed(mutable_trailed) -
            mutable_attr_thread_local(mutable_thread_local),
        mutable_attr_constant(yes) - mutable_attr_trailed(mutable_trailed),
        mutable_attr_constant(yes) - mutable_attr_attach_to_io_state(yes),
        mutable_attr_constant(yes) -
            mutable_attr_thread_local(mutable_thread_local)
    ],
    (
        list_term_to_term_list(MutAttrsTerm, MutAttrTerms),
        map_parser(parse_mutable_attr, MutAttrTerms, MaybeAttrList),
        MaybeAttrList = ok1(CollectedMutAttrs)
    ->
        % We check for trailed/untrailed, constant/trailed,
        % trailed/thread_local, constant/attach_to_io_state,
        % constant/thread_local conflicts here and deal with conflicting
        % foreign_name attributes in make_hlds_passes.m.
        (
            list.member(Conflict1 - Conflict2, ConflictingAttributes),
            list.member(Conflict1, CollectedMutAttrs),
            list.member(Conflict2, CollectedMutAttrs)
        ->
            % XXX Should generate more specific error message.
            MutAttrsStr = mercury_term_to_string(VarSet, no, MutAttrsTerm),
            Pieces = [words("Error: conflicting attributes"),
                words("in attribute list:"), nl,
                words(MutAttrsStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(MutAttrsTerm),
                    [always(Pieces)])]),
            MutAttrsResult = error1([Spec])
        ;
            list.foldl(process_mutable_attribute, CollectedMutAttrs,
                Attributes0, Attributes),
            MutAttrsResult = ok1(Attributes)
        )
    ;
        MutAttrsStr = mercury_term_to_string(VarSet, no, MutAttrsTerm),
        Pieces = [words("Error: malformed attribute list"),
            words("in mutable declaration:"),
            words(MutAttrsStr), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(MutAttrsTerm), [always(Pieces)])]),
        MutAttrsResult = error1([Spec])
    ).

:- pred process_mutable_attribute(collected_mutable_attribute::in,
    mutable_var_attributes::in, mutable_var_attributes::out) is det.

process_mutable_attribute(mutable_attr_trailed(Trailed), !Attributes) :-
    set_mutable_var_trailed(Trailed, !Attributes).
process_mutable_attribute(mutable_attr_foreign_name(ForeignName),
        !Attributes) :-
    set_mutable_add_foreign_name(ForeignName, !Attributes).
process_mutable_attribute(mutable_attr_attach_to_io_state(AttachToIOState),
        !Attributes) :-
    set_mutable_var_attach_to_io_state(AttachToIOState, !Attributes).
process_mutable_attribute(mutable_attr_constant(Constant), !Attributes) :-
    set_mutable_var_constant(Constant, !Attributes),
    (
        Constant = yes,
        set_mutable_var_trailed(mutable_untrailed, !Attributes),
        set_mutable_var_attach_to_io_state(no, !Attributes)
    ;
        Constant = no
    ).
process_mutable_attribute(mutable_attr_thread_local(ThrLocal), !Attributes) :-
    set_mutable_var_thread_local(ThrLocal, !Attributes).

:- pred parse_mutable_attr(term::in,
    maybe1(collected_mutable_attribute)::out) is det.

parse_mutable_attr(MutAttrTerm, MutAttrResult) :-
    (
        MutAttrTerm = term.functor(term.atom(String), [], _),
        (
            String  = "untrailed",
            MutAttr = mutable_attr_trailed(mutable_untrailed)
        ;
            String = "trailed",
            MutAttr = mutable_attr_trailed(mutable_trailed)
        ;
            String  = "attach_to_io_state",
            MutAttr = mutable_attr_attach_to_io_state(yes)
        ;
            String = "constant",
            MutAttr = mutable_attr_constant(yes)
        ;
            String = "thread_local",
            MutAttr = mutable_attr_thread_local(mutable_thread_local)
        )
    ->
        MutAttrResult = ok1(MutAttr)
    ;
        MutAttrTerm = term.functor(term.atom("foreign_name"), Args, _),
        Args = [LangTerm, ForeignNameTerm],
        parse_foreign_language(LangTerm, Lang),
        ForeignNameTerm = term.functor(term.string(ForeignName), [], _)
    ->
        MutAttr = mutable_attr_foreign_name(foreign_name(Lang, ForeignName)),
        MutAttrResult = ok1(MutAttr)
    ;
        Pieces = [words("Error: unrecognised attribute"),
            words("in mutable declaration."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(MutAttrTerm), [always(Pieces)])]),
        MutAttrResult = error1([Spec])
    ).

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

    % The optional `where ...' part of the type definition syntax
    % is a comma separated list of special type `attributes'.
    %
    % The possible attributes (in this order) are either
    % - `type_is_abstract_noncanonical' on its own appears only in .int2
    %   files and indicates that the type has user-defined equality and/or
    %   comparison, but that what these predicates are is not known at
    %   this point
    % or
    % - `representation is <<type name>>' (required for solver types)
    % - `initialisation is <<pred name>>' (required for solver types)
    % - `ground is <<inst>>' (required for solver types)
    % - `any is <<inst>>' (required for solver types)
    % - `equality is <<pred name>>' (optional)
    % - `comparison is <<pred name>>' (optional).
    %
parse_type_decl_where_part_if_present(IsSolverType, ModuleName, VarSet,
        Term0, Term, Result) :-
    (
        Term0 = term.functor(term.atom("where"), Args0, _Context),
        Args0 = [Term1, WhereTerm]
    ->
        Term = Term1,
        Result = parse_type_decl_where_term(IsSolverType, ModuleName,
            VarSet, yes(WhereTerm))
    ;
        Term = Term0,
        Result = ok2(no, no)
    ).

    % The maybe2 wrapper allows us to return an error code or a pair
    % of results.  Either result half may be empty, hence the maybe
    % wrapper around each of those.
    %
:- func parse_type_decl_where_term(is_solver_type, module_name, varset,
    maybe(term)) = maybe2(maybe(solver_type_details), maybe(unify_compare)).

parse_type_decl_where_term(IsSolverType, ModuleName, VarSet, MaybeTerm0) =
        MaybeWhereDetails :-
    (
        MaybeTerm0 = no,
        MaybeWhereDetails = ok2(no, no)
    ;
        MaybeTerm0 = yes(Term0),
        some [!MaybeTerm] (
            !:MaybeTerm = MaybeTerm0,
            parse_where_attribute(parse_where_type_is_abstract_noncanonical,
                TypeIsAbstractNoncanonicalResult, !MaybeTerm),
            parse_where_attribute(parse_where_is("representation",
                    parse_where_type_is(ModuleName, VarSet)),
                RepresentationIsResult, !MaybeTerm),
            parse_where_attribute(parse_where_initialisation_is(ModuleName,
                    VarSet),
                InitialisationIsResult, !MaybeTerm),
            parse_where_attribute(parse_where_is("ground",
                    parse_where_inst_is(ModuleName)),
                GroundIsResult, !MaybeTerm),
            parse_where_attribute(parse_where_is("any",
                    parse_where_inst_is(ModuleName)),
                AnyIsResult, !MaybeTerm),
            parse_where_attribute(parse_where_is("constraint_store",
                    parse_where_mutable_is(ModuleName)),
                CStoreIsResult, !MaybeTerm),
            parse_where_attribute(parse_where_is("equality",
                    parse_where_pred_is(ModuleName, VarSet)),
                EqualityIsResult, !MaybeTerm),
            parse_where_attribute(parse_where_is("comparison",
                    parse_where_pred_is(ModuleName, VarSet)),
                ComparisonIsResult, !MaybeTerm),
            parse_where_end(!.MaybeTerm, WhereEndResult)
        ),
        MaybeWhereDetails = make_maybe_where_details(
            IsSolverType,
            TypeIsAbstractNoncanonicalResult,
            RepresentationIsResult,
            InitialisationIsResult,
            GroundIsResult,
            AnyIsResult,
            CStoreIsResult,
            EqualityIsResult,
            ComparisonIsResult,
            WhereEndResult,
            Term0
        )
    ).

    % parse_where_attribute(Parser, Result, MaybeTerm0, MaybeTerm)
    % handles
    % - where MaybeTerm0 may contain nothing
    % - where MaybeTerm0 may be a comma-separated pair
    % - applies Parser to the appropriate (sub)term to obtain Result
    % - sets MaybeTerm depending upon whether the Result is an error
    % or not and whether there is more to parse because MaybeTerm0
    % was a comma-separated pair.
    %
:- pred parse_where_attribute((func(term) = maybe1(maybe(T)))::in,
    maybe1(maybe(T))::out, maybe(term)::in, maybe(term)::out) is det.

parse_where_attribute(Parser, Result, MaybeTerm0, MaybeRest) :-
    (
        MaybeTerm0 = no,
        MaybeRest = no,
        Result = ok1(no)
    ;
        MaybeTerm0 = yes(Term0),
        (
            Term0 = term.functor(term.atom(","), [Term1, Term], _Context)
        ->
            Result         = Parser(Term1),
            MaybeRestIfYes = yes(Term)
        ;
            Result         = Parser(Term0),
            MaybeRestIfYes = no
        ),
        (
            Result = error1(_),
            MaybeRest = no
        ;
            Result = ok1(no),
            MaybeRest = yes(Term0)
        ;
            Result = ok1(yes(_)),
            MaybeRest = MaybeRestIfYes
        )
    ).

    % Parser for `where ...' attributes of the form
    % `attributename is attributevalue'.
    %
:- func parse_where_is(string, func(term) = maybe1(T), term) =
    maybe1(maybe(T)).

parse_where_is(Name, Parser, Term) = Result :-
    ( Term = term.functor(term.atom("is"), [LHS, RHS], _) ->
        ( LHS = term.functor(term.atom(Name), [], _) ->
            RHSResult = Parser(RHS),
            (
                RHSResult = ok1(ParsedRHS),
                Result    = ok1(yes(ParsedRHS))
            ;
                RHSResult = error1(Specs),
                Result    = error1(Specs)
            )
        ;
            Result = ok1(no)
        )
    ;
        Pieces = [words("Error: expected"), quote("is"), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(Term), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- func parse_where_type_is_abstract_noncanonical(term) = maybe1(maybe(unit)).

parse_where_type_is_abstract_noncanonical(Term) =
    (
        Term = term.functor(term.atom("type_is_abstract_noncanonical"), [],
            _Context)
    ->
        ok1(yes(unit))
    ;
        ok1(no)
    ).

:- func parse_where_initialisation_is(module_name, varset, term) =
    maybe1(maybe(sym_name)).

parse_where_initialisation_is(ModuleName, VarSet, Term) = Result :-
    Result0 = parse_where_is("initialisation",
        parse_where_pred_is(ModuleName, VarSet),
        Term),
    (
        Result0 = ok1(no)
    ->
        Result1 = parse_where_is("initialization",
            parse_where_pred_is(ModuleName, VarSet), Term)
    ;
        Result1 = Result0
    ),
    promise_pure (
        (
            Result1 = ok1(yes(_)),
            semipure
                semipure_get_solver_auto_init_supported(AutoInitSupported),
            (
                AutoInitSupported = yes,
                Result = Result1
            ;
                AutoInitSupported = no,
                Pieces = [words("Error: unknown attribute"),
                    words("in solver type definition."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Term), [always(Pieces)])]),
                Result = error1([Spec])
            )
        ;
            ( Result1 = ok1(no)
            ; Result1 = error1(_)
            ),
            Result  = Result1
        )
    ).

:- func parse_where_pred_is(module_name, varset, term) = maybe1(sym_name).

parse_where_pred_is(ModuleName, VarSet, Term) = Result :-
    parse_implicitly_qualified_symbol_name(ModuleName, VarSet, Term, Result).

:- func parse_where_inst_is(module_name, term) = maybe1(mer_inst).

parse_where_inst_is(_ModuleName, Term) = Result :-
    (
        prog_io_util.convert_inst(no_allow_constrained_inst_var, Term, Inst),
        not prog_mode.inst_contains_unconstrained_var(Inst)
    ->
        Result = ok1(Inst)
    ;
        Pieces = [words("Error: expected a ground, unconstrained inst."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(Term), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- func parse_where_type_is(module_name, varset, term) = maybe1(mer_type).

parse_where_type_is(_ModuleName, VarSet, Term) = Result :-
    % XXX We should pass meaningful ContextPieces.
    ContextPieces = [],
    parse_type(Term, VarSet, ContextPieces, Result).

:- func parse_where_mutable_is(module_name, term) = maybe1(list(item)).

parse_where_mutable_is(ModuleName, Term) = Result :-
    ( Term = term.functor(term.atom("mutable"), _Args, _Ctxt) ->
        parse_mutable_decl_term(ModuleName, Term, Result0),
        (
            Result0 = ok1(Mutable),
            Result  = ok1([Mutable])
        ;
            Result0 = error1(Specs),
            Result  = error1(Specs)
        )
    ; list_term_to_term_list(Term, Terms) ->
        map_parser(parse_mutable_decl_term(ModuleName), Terms, Result)
    ;
        Pieces = [words("Error: expected a mutable declaration"),
            words("or a list of mutable declarations."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(Term), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- pred parse_mutable_decl_term(module_name::in, term::in, maybe1(item)::out)
    is det.

parse_mutable_decl_term(ModuleName, Term, Result) :-
    (
        Term = term.functor(term.atom("mutable"), Args, Context),
        varset.init(VarSet),
        parse_mutable_decl(ModuleName, VarSet, Args, Context, Result0)
    ->
        Result = Result0
    ;
        Pieces = [words("Error: expected a mutable declaration."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(Term), [always(Pieces)])]),
        Result = error1([Spec])

    ).

:- pred parse_where_end(maybe(term)::in, maybe1(maybe(unit))::out) is det.

parse_where_end(no, ok1(yes(unit))).
parse_where_end(yes(Term), error1([Spec])) :-
    Pieces = [words("Error: attributes are either badly ordered"),
        words("or contain an unrecognised attribute."), nl],
    Spec = error_spec(severity_error, phase_term_to_parse_tree,
        [simple_msg(get_term_context(Term), [always(Pieces)])]).

:- func make_maybe_where_details(is_solver_type, maybe1(maybe(unit)),
    maybe1(maybe(mer_type)), maybe1(maybe(init_pred)),
    maybe1(maybe(mer_inst)), maybe1(maybe(mer_inst)),
    maybe1(maybe(list(item))),
    maybe1(maybe(equality_pred)), maybe1(maybe(comparison_pred)),
    maybe1(maybe(unit)), term)
    = maybe2(maybe(solver_type_details), maybe(unify_compare)).

make_maybe_where_details(IsSolverType, TypeIsAbstractNoncanonicalResult,
        RepresentationIsResult, InitialisationIsResult,
        GroundIsResult, AnyIsResult, CStoreIsResult,
        EqualityIsResult, ComparisonIsResult, WhereEndResult, WhereTerm)
        = Result :-
    (
        TypeIsAbstractNoncanonicalResult = ok1(TypeIsAbstractNoncanonical),
        RepresentationIsResult = ok1(RepresentationIs),
        InitialisationIsResult = ok1(InitialisationIs),
        GroundIsResult = ok1(GroundIs),
        AnyIsResult = ok1(AnyIs),
        CStoreIsResult = ok1(CStoreIs),
        EqualityIsResult = ok1(EqualityIs),
        ComparisonIsResult = ok1(ComparisonIs),
        WhereEndResult = ok1(WhereEnd)
    ->
        Result = make_maybe_where_details_2(IsSolverType,
            TypeIsAbstractNoncanonical, RepresentationIs, InitialisationIs,
            GroundIs, AnyIs, CStoreIs, EqualityIs, ComparisonIs,
            WhereEnd, WhereTerm)
    ;
        TypeIsAbstractNoncanonicalSpecs =
            get_any_errors1(TypeIsAbstractNoncanonicalResult),
        RepresentationIsSpecs = get_any_errors1(RepresentationIsResult),
        InitialisationIsSpecs = get_any_errors1(InitialisationIsResult),
        GroundIsSpecs = get_any_errors1(GroundIsResult),
        AnyIsSpecs = get_any_errors1(AnyIsResult),
        CStoreIsSpecs = get_any_errors1(CStoreIsResult),
        EqualityIsSpecs = get_any_errors1(EqualityIsResult),
        ComparisonIsSpecs = get_any_errors1(ComparisonIsResult),
        WhereEndSpecs = get_any_errors1(WhereEndResult),
        Specs = TypeIsAbstractNoncanonicalSpecs ++ RepresentationIsSpecs ++
            InitialisationIsSpecs ++ GroundIsSpecs ++ AnyIsSpecs ++
            CStoreIsSpecs ++ EqualityIsSpecs ++ ComparisonIsSpecs ++
            WhereEndSpecs,
        Result = error2(Specs)
    ).

:- func make_maybe_where_details_2(is_solver_type, maybe(unit),
    maybe(mer_type), maybe(init_pred), maybe(mer_inst), maybe(mer_inst),
    maybe(list(item)), maybe(equality_pred), maybe(comparison_pred),
    maybe(unit), term)
    = maybe2(maybe(solver_type_details), maybe(unify_compare)).

make_maybe_where_details_2(IsSolverType, TypeIsAbstractNoncanonical,
        RepresentationIs, InitialisationIs, GroundIs, AnyIs, CStoreIs,
        EqualityIs, ComparisonIs, _WhereEnd, WhereTerm) = Result :-
    (
        TypeIsAbstractNoncanonical = yes(_),
        % rafe: XXX I think this is wrong. There isn't a problem with having
        % the solver_type_details and type_is_abstract_noncanonical.
        (
            RepresentationIs = maybe.no,
            InitialisationIs = maybe.no,
            GroundIs         = maybe.no,
            AnyIs            = maybe.no,
            EqualityIs       = maybe.no,
            ComparisonIs     = maybe.no,
            CStoreIs         = maybe.no
        ->
            Result = ok2(no, yes(abstract_noncanonical_type(IsSolverType)))
        ;
            Pieces = [words("Error:"),
                quote("where type_is_abstract_noncanonical"),
                words("excludes other"), quote("where ..."),
                words("attributes."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(WhereTerm), [always(Pieces)])]),
            Result = error2([Spec])
        )
    ;
        TypeIsAbstractNoncanonical = maybe.no,
        (
            IsSolverType = solver_type,
            (
                RepresentationIs = yes(RepnType),
                InitialisationIs = MaybeInitialisation,
                GroundIs         = MaybeGroundInst,
                AnyIs            = MaybeAnyInst,
                EqualityIs       = MaybeEqPred,
                ComparisonIs     = MaybeCmpPred,
                CStoreIs         = MaybeMutableItems
            ->
                (
                    MaybeGroundInst = yes(GroundInst)
                ;
                    MaybeGroundInst = no,
                    GroundInst = ground_inst
                ),
                (
                    MaybeAnyInst = yes(AnyInst)
                ;
                    MaybeAnyInst = no,
                    AnyInst = ground_inst
                ),
                (
                    MaybeMutableItems = yes(MutableItems)
                ;
                    MaybeMutableItems = no,
                    MutableItems = []
                ),
                (
                    MaybeInitialisation = yes(InitPred),
                    HowToInit = solver_init_automatic(InitPred)
                ;
                    MaybeInitialisation = no,
                    HowToInit = solver_init_explicit
                ),
                SolverTypeDetails = solver_type_details(
                    RepnType, HowToInit, GroundInst, AnyInst, MutableItems),
                MaybeSolverTypeDetails = yes(SolverTypeDetails),
                (
                    MaybeEqPred = no,
                    MaybeCmpPred = no
                ->
                    MaybeUnifyCompare = no
                ;
                    MaybeUnifyCompare = yes(unify_compare(
                        MaybeEqPred, MaybeCmpPred))
                ),
                Result = ok2(MaybeSolverTypeDetails, MaybeUnifyCompare)
            ;
                RepresentationIs = no
            ->
                Pieces = [words("Error: solver type definitions must have a"),
                    quote("representation"), words("attribute."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(WhereTerm),
                        [always(Pieces)])]),
                Result = error2([Spec])
            ;
               unexpected(this_file, "make_maybe_where_details_2: " ++
                    "shouldn't have reached this point! (1)")
            )
        ;
            IsSolverType = non_solver_type,
            (
                ( RepresentationIs = yes(_)
                ; InitialisationIs = yes(_)
                ; GroundIs         = yes(_)
                ; AnyIs            = yes(_)
                ; CStoreIs         = yes(_)
                )
            ->
                Pieces = [words("Error: solver type attribute given"),
                    words("for non-solver type."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(WhereTerm),
                        [always(Pieces)])]),
                Result = error2([Spec])
            ;
                EqualityIs = MaybeEqPred,
                ComparisonIs = MaybeCmpPred,
                Result = ok2(no, yes(unify_compare(MaybeEqPred, MaybeCmpPred)))
            )
        )
    ).

    % get_determinism(VarSet, BodyTerm0, BodyTerm, MaybeMaybeDeterminism) binds
    % MaybeMaybeDeterminism to ok1(yes()) wrapped around the determinism
    % of BodyTerm0, if any, and binds BodyTerm to the other part of BodyTerm0.
    % If BodyTerm0 does not contain a determinism, then MaybeMaybeDeterminism
    % is bound to ok1(no).
    %
:- pred get_determinism(varset::in, term::in, term::out,
    maybe1(maybe(determinism))::out) is det.

get_determinism(VarSet, BodyTerm0, BodyTerm, MaybeMaybeDeterminism) :-
    (
        BodyTerm0 = term.functor(term.atom("is"), Args, _),
        Args = [BodyTerm1, DeterminismTerm]
    ->
        BodyTerm = BodyTerm1,
        (
            DeterminismTerm = term.functor(term.atom(DeterminismFunctor),
                [], _),
            standard_det(DeterminismFunctor, Determinism)
        ->
            MaybeMaybeDeterminism = ok1(yes(Determinism))
        ;
            BodyTermStr = describe_error_term(VarSet, BodyTerm),
            Pieces = [words("Error: invalid determinism category"),
                words(BodyTermStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(DeterminismTerm),
                    [always(Pieces)])]),
            MaybeMaybeDeterminism = error1([Spec])
        )
    ;
        BodyTerm = BodyTerm0,
        MaybeMaybeDeterminism = ok1(no)
    ).

    % Process the `with_inst` part of a declaration of the form:
    % :- mode p(int) `with_inst` (pred(in, out) is det).
    %
:- pred get_with_inst(term::in, term::out, maybe1(maybe(mer_inst))::out)
    is det.

get_with_inst(BodyTerm0, BodyTerm, WithInst) :-
    (
        BodyTerm0 = term.functor(term.atom("with_inst"),
            [BodyTerm1, InstTerm], _)
    ->
        ( convert_inst(allow_constrained_inst_var, InstTerm, Inst) ->
            WithInst = ok1(yes(Inst))
        ;
            Pieces = [words("Error: invalid inst in"), quote("with_inst"),
                suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(BodyTerm0), [always(Pieces)])]),
            WithInst = error1([Spec])
        ),
        BodyTerm = BodyTerm1
    ;
        BodyTerm = BodyTerm0,
        WithInst = ok1(no)
    ).

:- pred get_with_type(varset::in, term::in, term::out,
    maybe1(maybe(mer_type))::out) is det.

get_with_type(VarSet, BodyTerm0, BodyTerm, Result) :-
    (
        BodyTerm0 = term.functor(TypeQualifier, [BodyTerm1, TypeTerm1], _),
        (
            TypeQualifier = term.atom("with_type")
        ;
            TypeQualifier = term.atom(":")
        )
    ->
        BodyTerm = BodyTerm1,
        % XXX Should supply more correct ContextPieces.
        ContextPieces = [],
        parse_type(TypeTerm1, VarSet, ContextPieces, Result0),
        (
            Result0 = ok1(Type),
            Result = ok1(yes(Type))
        ;
            Result0 = error1(Specs),
            Result = error1(Specs)
        )
    ;
        BodyTerm = BodyTerm0,
        Result = ok1(no)
    ).

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

    % get_condition(Term0, Term, Condition) binds Condition
    % to a representation of the 'where' condition of Term0, if any,
    % and binds Term to the other part of Term0. If Term0 does not
    % contain a condition, then Condition is bound to true.
    %
:- pred get_condition(term::in, term::out, condition::out) is det.

get_condition(Body, Body, cond_true).

% % NU-Prolog supported type declarations of the form
% %   :- pred p(T) where p(X) : sorted(X).
% % or
% %   :- type sorted_list(T) = list(T) where X : sorted(X).
% %   :- pred p(sorted_list(T).
% % There is some code here to support that sort of thing, but
% % probably we would now need to use a different syntax, since
% % Mercury now uses `where' for different purposes (e.g. specifying
% % user-defined equality predicates, and also for type classes ...)
%
% get_condition(B, Body, Condition) :-
%   (
%       B = term.functor(term.atom("where"), [Body1, Condition1],
%           _Context)
%   ->
%       Body = Body1,
%       Condition = where(Condition1)
%   ;
%       Body = B,
%       Condition = true
%   ).

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

:- type processed_type_body
    --->    processed_type_body(
                sym_name,
                list(type_param),
                type_defn
            ).

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

:- pred process_solver_type(module_name::in, varset::in, term::in,
    maybe(solver_type_details)::in, maybe(unify_compare)::in,
    maybe1(processed_type_body)::out) is det.

process_solver_type(ModuleName, VarSet, HeadTerm,
        MaybeSolverTypeDetails, MaybeUserEqComp, Result) :-
    (
        MaybeSolverTypeDetails = yes(SolverTypeDetails),
        parse_type_defn_head(ModuleName, VarSet, HeadTerm, Result0),
        (
            Result0 = error2(Specs),
            Result  = error1(Specs)
        ;
            Result0 = ok2(Name, Params),
            (
                RepnType = SolverTypeDetails ^ representation_type,
                type_contains_var(RepnType, Var),
                not list.member(Var, Params)
            ->
                HeadTermStr = describe_error_term(VarSet, HeadTerm),
                Pieces = [words("Error: free type variable"),
                    words("in representation type:"),
                    words(HeadTermStr), suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(HeadTerm),
                        [always(Pieces)])]),
                Result = error1([Spec])
            ;
                Result = ok1(processed_type_body(Name, Params,
                    parse_tree_solver_type(SolverTypeDetails,
                        MaybeUserEqComp)))
            )
        )
    ;
        MaybeSolverTypeDetails = no,
        Pieces = [words("Solver type with no solver_type_details."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
        Result = error1([Spec])
    ).

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

    % This is for "Head == Body" (equivalence) definitions.
    %
:- pred process_eqv_type(module_name::in, varset::in, term::in, term::in,
    maybe1(processed_type_body)::out) is det.

process_eqv_type(ModuleName, VarSet, HeadTerm, BodyTerm, Result) :-
    parse_type_defn_head(ModuleName, VarSet, HeadTerm, Result0),
    process_eqv_type_2(Result0, VarSet, BodyTerm, Result).

:- pred process_eqv_type_2(maybe2(sym_name, list(type_param))::in,
    varset::in, term::in, maybe1(processed_type_body)::out) is det.

process_eqv_type_2(error2(Specs), _, _, error1(Specs)).
process_eqv_type_2(ok2(Name, Params), VarSet, BodyTerm0, Result) :-
    % Check that all the variables in the body occur in the head.
    (
        term.contains_var(BodyTerm0, Var),
        term.coerce_var(Var, TVar),
        \+ list.member(TVar, Params)
    ->
        BodyTerm0Str = describe_error_term(VarSet, BodyTerm0),
        Pieces = [words("Error: free type parameter"),
            words("in RHS of type definition:"),
            words(BodyTerm0Str), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(BodyTerm0), [always(Pieces)])]),
        Result = error1([Spec])
    ;
        % XXX Should pass more correct ContextPieces.
        ContextPieces = [],
        parse_type(BodyTerm0, VarSet, ContextPieces, BodyResult),
        (
            BodyResult = ok1(BodyTerm),
            Result = ok1(processed_type_body(Name, Params,
                parse_tree_eqv_type(BodyTerm)))
        ;
            BodyResult = error1(Specs),
            Result = error1(Specs)
        )
    ).

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

    % process_du_type(ModuleName, HeadTerm, BodyTerm, Ctors,
    %   MaybeUserEqComp, Result):
    %
    % Checks that its arguments are well formed, and if they are,
    % binds Result to a representation of the type information about the
    % TypeHead.
    % This is for "Head ---> Body [where ...]" (constructor) definitions.
    %
:- pred process_du_type(module_name::in, varset::in, term::in, term::in,
    list(constructor)::in, maybe(unify_compare)::in,
    maybe1(processed_type_body)::out) is det.

process_du_type(ModuleName, VarSet, HeadTerm, BodyTerm, Ctors, MaybeUserEqComp,
        Result) :-
    parse_type_defn_head(ModuleName, VarSet, HeadTerm, Result0),
    (
        Result0 = error2(Specs),
        Result  = error1(Specs)
    ;
        Result0 = ok2(Functor, Params),
        process_du_ctors(Params, VarSet, BodyTerm, Ctors, [], Specs),
        (
            Specs = [],
            TypeDefn = parse_tree_du_type(Ctors, MaybeUserEqComp),
            ProcessedTypeBody = processed_type_body(Functor, Params, TypeDefn),
            Result = ok1(ProcessedTypeBody)
        ;
            Specs = [_ | _],
            Result = error1(Specs)
        )
    ).

:- pred process_du_ctors(list(type_param)::in, varset::in, term::in,
    list(constructor)::in, list(error_spec)::in, list(error_spec)::out) is det.

process_du_ctors(_Params, _, _, [], !Specs).
process_du_ctors(Params, VarSet, BodyTerm, [Ctor | Ctors], !Specs) :-
    Ctor = ctor(ExistQVars, Constraints, _CtorName, CtorArgs, _Context),
    (
        % Check that all type variables in the ctor are either explicitly
        % existentially quantified or occur in the head of the type.

        CtorArgTypes = list.map(func(C) = C ^ arg_type, CtorArgs),
        type_vars_list(CtorArgTypes, VarsInCtorArgTypes0),
        list.sort_and_remove_dups(VarsInCtorArgTypes0, VarsInCtorArgTypes),
        list.filter(list.contains(ExistQVars ++ Params), VarsInCtorArgTypes,
            _ExistQOrParamVars, NotExistQOrParamVars),
        NotExistQOrParamVars = [_ | _]
    ->
        % There should be no duplicate names to remove.
        varset.coerce(VarSet, GenericVarSet),
        NotExistQOrParamVarsStr =
            mercury_vars_to_string(GenericVarSet, no, NotExistQOrParamVars),
        Pieces = [words("Error: free type"),
            words(choose_number(NotExistQOrParamVars,
                "parameter", "parameters")),
            words(NotExistQOrParamVarsStr),
            words("in RHS of type definition."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(BodyTerm), [always(Pieces)])]),
        !:Specs = [Spec | !.Specs]
    ;
        % Check that all type variables in existential quantifiers do not
        % occur in the head (maybe this should just be a warning, not an error?
        % If we were to allow it, we would need to rename them apart.)

        set.list_to_set(ExistQVars, ExistQVarsSet),
        set.list_to_set(Params, ParamsSet),
        set.intersect(ExistQVarsSet, ParamsSet, ExistQParamsSet),
        set.non_empty(ExistQParamsSet)
    ->
        % There should be no duplicate names to remove.
        set.to_sorted_list(ExistQParamsSet, ExistQParams),
        varset.coerce(VarSet, GenericVarSet),
        ExistQParamVarsStr =
            mercury_vars_to_string(GenericVarSet, no, ExistQParams),
        Pieces = [words("Error:"),
            words(choose_number(ExistQParams,
                "type variable", "type variables")),
            words(ExistQParamVarsStr),
            words(choose_number(ExistQParams, "has", "have")),
            words("overlapping scopes"),
            words("(explicit type quantifier shadows argument type)."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(BodyTerm), [always(Pieces)])]),
        !:Specs = [Spec | !.Specs]
    ;
        % Check that all type variables in existential quantifiers occur
        % somewhere in the constructor argument types or constraints.

        CtorArgTypes = list.map(func(C) = C ^ arg_type, CtorArgs),
        type_vars_list(CtorArgTypes, VarsInCtorArgTypes0),
        list.sort_and_remove_dups(VarsInCtorArgTypes0, VarsInCtorArgTypes),
        constraint_list_get_tvars(Constraints, ConstraintTVars),
        list.filter(list.contains(VarsInCtorArgTypes ++ ConstraintTVars),
            ExistQVars, _OccursExistQVars, NotOccursExistQVars),
        NotOccursExistQVars = [_ | _]
    ->
        % There should be no duplicate names to remove.
        varset.coerce(VarSet, GenericVarSet),
        NotOccursExistQVarsStr =
            mercury_vars_to_string(GenericVarSet, no, NotOccursExistQVars),
        Pieces = [words("Error:"),
            words(choose_number(NotOccursExistQVars,
                "type variable", "type variables")),
            words(NotOccursExistQVarsStr),
            words("in existential quantifier"),
            words(choose_number(NotOccursExistQVars,
                "does not occur", "do not occur")),
            words("in arguments or constraints of constructor."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(BodyTerm), [always(Pieces)])]),
        !:Specs = [Spec | !.Specs]
    ;
        % Check that all type variables in existential constraints occur in
        % the existential quantifiers.

        ConstraintArgTypeLists =
            list.map(prog_constraint_get_arg_types, Constraints),
        list.condense(ConstraintArgTypeLists, ConstraintArgTypes),
        type_vars_list(ConstraintArgTypes, VarsInCtorArgTypes0),
        list.sort_and_remove_dups(VarsInCtorArgTypes0, VarsInCtorArgTypes),
        list.filter(list.contains(ExistQVars), VarsInCtorArgTypes,
            _ExistQArgTypes, NotExistQArgTypes),
        NotExistQArgTypes = [_ | _]
    ->
        varset.coerce(VarSet, GenericVarSet),
        NotExistQArgTypesStr =
            mercury_vars_to_string(GenericVarSet, no, NotExistQArgTypes),
        Pieces = [words("Error:"),
            words(choose_number(NotExistQArgTypes,
                "type variable", "type variables")),
            words(NotExistQArgTypesStr),
            words("in class constraints,"),
            words(choose_number(NotExistQArgTypes,
                "which was", "which were")),
            words("introduced with"), quote("=>"),
            words("must be explicitly existentially quantified"),
            words("using"), quote("some"), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(BodyTerm), [always(Pieces)])]),
        !:Specs = [Spec | !.Specs]
    ;
        true
    ),
    process_du_ctors(Params, VarSet, BodyTerm, Ctors, !Specs).

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

    % process_abstract_type(ModuleName, TypeHead, Result):
    %
    % Checks that its argument is well formed, and if it is, binds Result
    % to a representation of the type information about the TypeHead.
    %
:- pred process_abstract_type(module_name::in, varset::in, term::in,
    decl_attrs::in, maybe1(processed_type_body)::out) is det.

process_abstract_type(ModuleName, VarSet, HeadTerm, Attributes0, Result) :-
    parse_type_defn_head(ModuleName, VarSet, HeadTerm, Result0),
    get_is_solver_type(IsSolverType, Attributes0, Attributes),
    process_abstract_type_2(Result0, IsSolverType, Result1),
    check_no_attributes(Result1, Attributes, Result).

:- pred process_abstract_type_2(maybe2(sym_name, list(type_param))::in,
    is_solver_type::in, maybe1(processed_type_body)::out) is det.

process_abstract_type_2(error2(Specs), _, error1(Specs)).
process_abstract_type_2(ok2(Functor, Params), IsSolverType, Result) :-
    Result = ok1(processed_type_body(Functor, Params,
        parse_tree_abstract_type(IsSolverType))).

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

parse_type_defn_head(ModuleName, VarSet, HeadTerm, Result) :-
    (
        HeadTerm = term.variable(_, Context),
        Pieces = [words("Error: variable on LHS of type definition."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(Context, [always(Pieces)])]),
        Result = error2([Spec])
    ;
        HeadTerm = term.functor(_, _, _),
        ContextPieces = [words("In type definition:")],
        parse_implicitly_qualified_term(ModuleName, HeadTerm, HeadTerm,
            VarSet, ContextPieces, Headresult),
        parse_type_defn_head_2(Headresult, VarSet, HeadTerm, Result)
    ).

:- pred parse_type_defn_head_2(maybe_functor::in, varset::in, term::in,
    maybe2(sym_name, list(tvar))::out) is det.

parse_type_defn_head_2(error2(Specs), _, _, error2(Specs)).
parse_type_defn_head_2(ok2(Name, Args), VarSet, HeadTerm, Result) :-
    parse_type_defn_head_3(Name, Args, VarSet, HeadTerm, Result).

:- pred parse_type_defn_head_3(sym_name::in, list(term)::in, varset::in,
    term::in, maybe2(sym_name, list(tvar))::out) is det.

parse_type_defn_head_3(Name, Args, VarSet, HeadTerm, Result) :-
    % Check that all the head args are variables.
    ( term_list_to_var_list(Args, Params0) ->
        % Check that all the head arg variables are distinct.
        (
            list.member(_, Params0, [Param | OtherParams]),
            list.member(Param, OtherParams)
        ->
            Pieces = [words("Error: repeated type parameters"),
                words("in LHS of type definition."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
            Result = error2([Spec])
        ;
            list.map(term.coerce_var, Params0, Params),
            Result = ok2(Name, Params)
        )
    ;
        HeadTermStr = describe_error_term(VarSet, HeadTerm),
        Pieces = [words("Error: type parameters must be variables:"),
            words(HeadTermStr), suffix(".") ,nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
        Result = error2([Spec])
    ).

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

    % Convert a list of terms separated by semi-colons (known as a
    % "disjunction", even thought the terms aren't goals in this case)
    % into a list of constructors.
    %
:- func convert_constructors(module_name, varset, term) =
    maybe1(list(constructor)).

convert_constructors(ModuleName, VarSet, BodyTerm) = Result :-
    disjunction_to_list(BodyTerm, BodyTermList),
    Result = convert_constructors_2(ModuleName, VarSet, BodyTermList).

    % True if input argument is a valid list of constructors.
    %
:- func convert_constructors_2(module_name, varset, list(term)) =
    maybe1(list(constructor)).

convert_constructors_2(_ModuleName, _, []) = ok1([]).
convert_constructors_2(ModuleName, VarSet, [Term | Terms]) = Result :-
    Result0 = convert_constructor(ModuleName, VarSet, Term),
    (
        Result0 = error1(Specs),
        Result  = error1(Specs)
    ;
        Result0 = ok1(Constructor),
        Result1 = convert_constructors_2(ModuleName, VarSet, Terms),
        (
            Result1 = error1(Specs),
            Result  = error1(Specs)
        ;
            Result1 = ok1(Constructors),
            Result  = ok1([Constructor | Constructors])
        )
    ).

:- func convert_constructor(module_name, varset, term) = maybe1(constructor).

convert_constructor(ModuleName, VarSet, Term0) = Result :-
    ( Term0 = term.functor(term.atom("some"), [Vars, Term1], _Context) ->
        ( parse_list_of_vars(Vars, ExistQVars0) ->
            list.map(term.coerce_var, ExistQVars0, ExistQVars),
            Result = convert_constructor_2(ModuleName, VarSet, ExistQVars,
                Term0, Term1)
        ;
            Term0Str = describe_error_term(VarSet, Term0),
            Pieces = [words("Error: syntax error in variable list at"),
                words(Term0Str), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term0), [always(Pieces)])]),
            Result = error1([Spec])
        )
    ;
        ExistQVars = [],
        Result = convert_constructor_2(ModuleName, VarSet, ExistQVars,
            Term0, Term0)
    ).

:- func convert_constructor_2(module_name, varset, list(tvar), term, term) =
    maybe1(constructor).

convert_constructor_2(ModuleName, VarSet, ExistQVars, Term0, Term1) = Result :-
    get_existential_constraints_from_term(ModuleName, VarSet, Term1, Term2,
        Result0),
    (
        Result0 = error1(Specs),
        Result  = error1(Specs)
    ;
        Result0 = ok1(Constraints),
        (
            % Note that as a special case, one level of curly braces around
            % the constructor are ignored. This is to allow you to define
            % ';'/2 and 'some'/2 constructors.
            Term2 = term.functor(term.atom("{}"), [Term3], _Context)
        ->
            Term4 = Term3
        ;
            Term4 = Term2
        ),
        Result = convert_constructor_3(ModuleName, VarSet, ExistQVars,
            Constraints, Term0, Term4)
    ).

:- func convert_constructor_3(module_name, varset, list(tvar),
    list(prog_constraint), term, term) = maybe1(constructor).

convert_constructor_3(ModuleName, VarSet, ExistQVars, Constraints,
        Term0, Term1) = Result :-
    ContextPieces = [words("In constructor definition:")],
    parse_implicitly_qualified_term(ModuleName, Term1, Term0, VarSet,
        ContextPieces, Result0),
    (
        Result0 = error2(Specs),
        Result  = error1(Specs)
    ;
        Result0 = ok2(Functor, ArgTerms),
        Result1 = convert_constructor_arg_list(ModuleName, VarSet, ArgTerms),
        (
            Result1 = error1(Specs),
            Result  = error1(Specs)
        ;
            Result1 = ok1(Args),
            Ctxt = get_term_context(Term1),
            Result  = ok1(ctor(ExistQVars, Constraints, Functor, Args, Ctxt))
        )
    ).

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

    % parse a `:- pred p(...)' declaration or a
    % `:- func f(...) `with_type` t' declaration
    %
:- pred process_pred_decl(pred_or_func::in, module_name::in, varset::in,
    term::in, condition::in, maybe(mer_type)::in, maybe(mer_inst)::in,
    maybe(determinism)::in, decl_attrs::in, prog_context::in,
    maybe1(item)::out) is det.

process_pred_decl(PredOrFunc, ModuleName, VarSet, PredType, Cond, WithType,
        WithInst, MaybeDet, Attributes0, Context, Result) :-
    get_class_context_and_inst_constraints(ModuleName, VarSet,
        Attributes0, Attributes, MaybeClassContext),
    (
        MaybeClassContext = ok3(ExistQVars, Constraints, InstConstraints),
        ContextPieces = [words("In")] ++ pred_or_func_decl_pieces(PredOrFunc)
            ++ [suffix(":")],
        parse_implicitly_qualified_term(ModuleName, PredType, PredType,
            VarSet, ContextPieces, PredTypeResult),
        process_pred_decl_2(PredOrFunc, PredTypeResult, PredType, VarSet,
            WithType, WithInst, MaybeDet, Cond, ExistQVars,
            Constraints, InstConstraints, Attributes, Context, Result)
    ;
        MaybeClassContext = error3(Specs),
        Result = error1(Specs)
    ).

:- pred process_pred_decl_2(pred_or_func::in, maybe_functor::in, term::in,
    varset::in, maybe(mer_type)::in, maybe(mer_inst)::in,
    maybe(determinism)::in, condition::in, existq_tvars::in,
    prog_constraints::in, inst_var_sub::in, decl_attrs::in, prog_context::in,
    maybe1(item)::out) is det.

process_pred_decl_2(_, error2(Specs), _, _, _, _, _, _, _, _, _, _, _,
        error1(Specs)).
process_pred_decl_2(PredOrFunc, ok2(F, As0), PredTypeTerm, VarSet,
        WithType, WithInst, MaybeDet, Cond, ExistQVars,
        ClassContext, InstConstraints, Attributes0, Context, Result) :-
    ( convert_type_and_mode_list(InstConstraints, As0, As) ->
        ( verify_type_and_mode_list(As) ->
            (
                WithInst = yes(_),
                As = [type_only(_) | _]
            ->
                Pieces = [words("Error:"), quote("with_inst"),
                    words("specified without argument modes."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(PredTypeTerm),
                        [always(Pieces)])]),
                Result = error1([Spec])
            ;
                WithInst = no,
                WithType = yes(_),
                As = [type_and_mode(_, _) | _]
            ->
                Pieces = [words("Error: arguments have modes but"),
                    quote("with_inst"), words("not specified."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(PredTypeTerm),
                        [always(Pieces)])]),
                Result = error1([Spec])
            ;
                \+ inst_var_constraints_are_consistent_in_type_and_modes(As)
            ->
                PredTypeTermStr = describe_error_term(VarSet, PredTypeTerm),
                Pieces = [words("Error: inconsistent constraints on"),
                    words("inst variables in")] ++
                    pred_or_func_decl_pieces(PredOrFunc) ++
                    [suffix(":"), nl, words(PredTypeTermStr), suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(PredTypeTerm),
                        [always(Pieces)])]),
                Result = error1([Spec])
            ;
                get_purity(Purity, Attributes0, Attributes),
                varset.coerce(VarSet, TVarSet),
                varset.coerce(VarSet, IVarSet),
                Origin = user,
                ItemPredDecl = item_pred_decl_info(Origin, TVarSet, IVarSet,
                    ExistQVars, PredOrFunc, F, As, WithType, WithInst,
                    MaybeDet, Cond, Purity, ClassContext, Context),
                Item = item_pred_decl(ItemPredDecl),
                Result0 = ok1(Item),
                check_no_attributes(Result0, Attributes, Result)
            )
        ;
            Pieces = [words("Error: some but not all arguments have modes."),
                nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(PredTypeTerm),
                    [always(Pieces)])]),
            Result = error1([Spec])
        )
    ;
        PredTypeTermStr = describe_error_term(VarSet, PredTypeTerm),
        Pieces = [words("Error: syntax error in")] ++
            pred_or_func_decl_pieces(PredOrFunc) ++
            [words("at"), words(PredTypeTermStr), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(PredTypeTerm), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- pred get_purity(purity::out, decl_attrs::in, decl_attrs::out) is det.

get_purity(Purity, !Attributes) :-
    ( !.Attributes = [decl_attr_purity(Purity0) - _ | !:Attributes] ->
        Purity = Purity0
    ;
        Purity = purity_pure
    ).

:- func pred_or_func_decl_pieces(pred_or_func) = list(format_component).

pred_or_func_decl_pieces(pf_function) =
    [quote(":- func"), words("declaration")].
pred_or_func_decl_pieces(pf_predicate) =
    [quote(":- pred"), words("declaration")].

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

    % We could perhaps get rid of some code duplication between here and
    % prog_io_typeclass.m?

    % get_class_context_and_inst_constraints(ModuleName, Attributes0,
    %   Attributes, MaybeContext, MaybeInstConstraints):
    %
    % Parse type quantifiers, type class constraints and inst constraints
    % from the declaration attributes in Attributes0.
    % MaybeContext is either bound to the correctly parsed context, or
    % an appropriate error message (if there was a syntax error).
    % MaybeInstConstraints is either bound to a map containing the inst
    % constraints or an appropriate error message (if there was a syntax
    % error).
    % Attributes is bound to the remaining attributes.
    %
:- pred get_class_context_and_inst_constraints(module_name::in, varset::in,
    decl_attrs::in, decl_attrs::out,
    maybe3(existq_tvars, prog_constraints, inst_var_sub)::out) is det.

get_class_context_and_inst_constraints(ModuleName, VarSet, RevAttributes0,
        RevAttributes, MaybeContext) :-
    % Constraints and quantifiers should occur in the following order
    % (outermost to innermost):
    %
    %                               operator        precedence
    %                               --------        ----------
    %   1. universal quantifiers    all             950
    %   2. existential quantifiers  some            950
    %   3. universal constraints    <=              920
    %   4. existential constraints  =>              920 [*]
    %   5. the decl itself          pred or func    800
    %
    % When we reach here, Attributes0 contains declaration attributes
    % in the opposite order -- innermost to outermost -- so we reverse
    % them before we start.
    %
    % [*] Note that the semantic meaning of `=>' is not quite the same
    % as implication; logically speaking it's more like conjunction.
    % Oh well, at least it has the right precedence.
    %
    % In theory it could make sense to allow the order of 2 & 3 to be
    % swapped, or (in the case of multiple constraints & multiple
    % quantifiers) to allow arbitrary interleaving of 2 & 3, but in
    % practice it seems there would be little benefit in allowing that
    % flexibility, so we don't.
    %
    % Universal quantification is the default, so we just ignore
    % universal quantifiers.  (XXX It might be a good idea to check
    % that any universally quantified type variables do actually
    % occur somewhere in the type declaration, and are not also
    % existentially quantified, and if not, issue a warning or
    % error message.)

    list.reverse(RevAttributes0, Attributes0),
    get_quant_vars(quant_type_univ, ModuleName, Attributes0, Attributes1,
        [], _UnivQVars),
    get_quant_vars(quant_type_exist, ModuleName, Attributes1, Attributes2,
        [], ExistQVars0),
    list.map(term.coerce_var, ExistQVars0, ExistQVars),
    get_constraints(quant_type_univ, ModuleName, VarSet, Attributes2,
        Attributes3, MaybeUnivConstraints),
    get_constraints(quant_type_exist, ModuleName, VarSet, Attributes3,
        Attributes, MaybeExistConstraints),
    list.reverse(Attributes, RevAttributes),

    combine_quantifier_results(MaybeUnivConstraints, MaybeExistConstraints,
        ExistQVars, MaybeContext).

:- pred combine_quantifier_results(maybe_class_and_inst_constraints::in,
    maybe_class_and_inst_constraints::in, existq_tvars::in,
    maybe3(existq_tvars, prog_constraints, inst_var_sub)::out) is det.

combine_quantifier_results(error2(Specs1), error2(Specs2), _,
        error3(Specs1 ++ Specs2)).
combine_quantifier_results(error2(Specs), ok2(_, _), _, error3(Specs)).
combine_quantifier_results(ok2(_, _), error2(Specs), _, error3(Specs)).
combine_quantifier_results(ok2(UnivConstraints, InstConstraints0),
    ok2(ExistConstraints, InstConstraints1), ExistQVars,
    ok3(ExistQVars, constraints(UnivConstraints, ExistConstraints),
        InstConstraints0 `map.old_merge` InstConstraints1)).

:- pred get_quant_vars(quantifier_type::in, module_name::in,
    decl_attrs::in, decl_attrs::out, list(var)::in, list(var)::out) is det.

get_quant_vars(QuantType, ModuleName, !Attributes, !Vars) :-
    (
        !.Attributes = [decl_attr_quantifier(QuantType, QuantVars) - _
            | !:Attributes]
    ->
        list.append(!.Vars, QuantVars, !:Vars),
        get_quant_vars(QuantType, ModuleName, !Attributes, !Vars)
    ;
        true
    ).

:- pred get_constraints(quantifier_type::in, module_name::in, varset::in,
    decl_attrs::in, decl_attrs::out, maybe_class_and_inst_constraints::out)
    is det.

get_constraints(QuantType, ModuleName, VarSet, !Attributes,
        MaybeConstraints) :-
    (
        !.Attributes = [
            decl_attr_constraints(QuantType, ConstraintsTerm) - _Term
            | !:Attributes]
    ->
        parse_class_and_inst_constraints(ModuleName, VarSet, ConstraintsTerm,
            MaybeConstraints0),
        % there may be more constraints of the same type --
        % collect them all and combine them
        get_constraints(QuantType, ModuleName, VarSet, !Attributes,
            MaybeConstraints1),
        combine_constraint_list_results(MaybeConstraints1,
            MaybeConstraints0, MaybeConstraints)
    ;
        MaybeConstraints = ok2([], map.init)
    ).

:- pred combine_constraint_list_results(maybe_class_and_inst_constraints::in,
    maybe_class_and_inst_constraints::in,
    maybe_class_and_inst_constraints::out) is det.

combine_constraint_list_results(error2(Specs1), error2(Specs2),
        error2(Specs1 ++ Specs2)).
combine_constraint_list_results(error2(Specs), ok2(_, _), error2(Specs)).
combine_constraint_list_results(ok2(_, _), error2(Specs), error2(Specs)).
combine_constraint_list_results(ok2(CC0, IC0), ok2(CC1, IC1),
        ok2(CC0 ++ CC1, IC0 `map.old_merge` IC1)).

:- pred get_existential_constraints_from_term(module_name::in, varset::in,
    term::in, term::out, maybe1(list(prog_constraint))::out) is det.

get_existential_constraints_from_term(ModuleName, VarSet, !PredTypeTerm,
        MaybeExistentialConstraints) :-
    (
        !.PredTypeTerm = term.functor(term.atom("=>"),
            [!:PredTypeTerm, ExistentialConstraints], _)
    ->
        parse_class_constraints(ModuleName, VarSet, ExistentialConstraints,
            MaybeExistentialConstraints)
    ;
        MaybeExistentialConstraints = ok1([])
    ).

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

    % Verify that among the arguments of a :- pred declaration,
    % either all arguments specify a mode or none of them do.
    %
:- pred verify_type_and_mode_list(list(type_and_mode)::in) is semidet.

verify_type_and_mode_list([]).
verify_type_and_mode_list([First | Rest]) :-
    verify_type_and_mode_list_2(Rest, First).

:- pred verify_type_and_mode_list_2(list(type_and_mode)::in, type_and_mode::in)
    is semidet.

verify_type_and_mode_list_2([], _).
verify_type_and_mode_list_2([Head | Tail], First) :-
    (
        Head = type_only(_),
        First = type_only(_)
    ;
        Head = type_and_mode(_, _),
        First = type_and_mode(_, _)
    ),
    verify_type_and_mode_list_2(Tail, First).

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

    % Parse a `:- func p(...)' declaration.
    %
:- pred process_func(module_name::in, varset::in, term::in, condition::in,
    maybe(determinism)::in, decl_attrs::in, prog_context::in,
    maybe1(item)::out) is det.

process_func(ModuleName, VarSet, Term, Cond, MaybeDet, Attributes0,
        Context, Result) :-
    get_class_context_and_inst_constraints(ModuleName, VarSet,
        Attributes0, Attributes, MaybeContext),
    (
        MaybeContext = ok3(ExistQVars, Constraints, InstConstraints),
        process_func_2(ModuleName, VarSet, Term, Cond, MaybeDet, ExistQVars,
            Constraints, InstConstraints, Attributes, Context, Result)
    ;
        MaybeContext = error3(Specs),
        Result = error1(Specs)
    ).

:- pred process_func_2(module_name::in, varset::in, term::in, condition::in,
    maybe(determinism)::in, existq_tvars::in, prog_constraints::in,
    inst_var_sub::in, decl_attrs::in, prog_context::in, maybe1(item)::out)
    is det.

process_func_2(ModuleName, VarSet, Term, Cond, MaybeDet, ExistQVars,
        Constraints, InstConstraints, Attributes, Context, Result) :-
    (
        Term = term.functor(term.atom("="),
            [FuncTerm0, ReturnTypeTerm], _Context),
        FuncTerm = desugar_field_access(FuncTerm0)
    ->
        ContextPieces = [words("In"), quote(":- func"), words("declaration")],
        parse_implicitly_qualified_term(ModuleName, FuncTerm, Term,
            VarSet, ContextPieces, FuncTermResult),
        process_func_3(FuncTermResult, FuncTerm, ReturnTypeTerm, Term, VarSet,
            MaybeDet, Cond, ExistQVars, Constraints, InstConstraints,
            Attributes, Context, Result)
    ;
        Pieces = [words("Error:"), quote("="), words("expected in"),
            quote(":- func"), words("declaration."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(Term), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- pred process_func_3(maybe_functor::in, term::in, term::in, term::in,
    varset::in, maybe(determinism)::in, condition::in, existq_tvars::in,
    prog_constraints::in, inst_var_sub::in, decl_attrs::in,
    prog_context::in, maybe1(item)::out) is det.

process_func_3(error2(Specs), _, _, _, _, _, _, _, _, _, _, _,
        error1(Specs)).
process_func_3(ok2(F, As0), FuncTerm, ReturnTypeTerm, FullTerm, VarSet,
        MaybeDet, Cond, ExistQVars, ClassContext, InstConstraints,
        Attributes0, Context, Result) :-
    ( convert_type_and_mode_list(InstConstraints, As0, As) ->
        (
            \+ verify_type_and_mode_list(As)
        ->
            Pieces = [words("Error: some but not all arguments have modes."),
                nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(FuncTerm), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            convert_type_and_mode(InstConstraints, ReturnTypeTerm, ReturnType)
        ->
            (
                As = [type_and_mode(_, _) | _],
                ReturnType = type_only(_)
            ->
                Pieces = [words("Error: function arguments have modes,"),
                    words("but function result does not."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(FuncTerm), [always(Pieces)])]),
                Result = error1([Spec])

            ;
                As = [type_only(_) | _],
                ReturnType = type_and_mode(_, _)
            ->
                Pieces = [words("Error: function result has mode,"),
                    words("but function arguments do not."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(FuncTerm), [always(Pieces)])]),
                Result = error1([Spec])
            ;
                get_purity(Purity, Attributes0, Attributes),
                varset.coerce(VarSet, TVarSet),
                varset.coerce(VarSet, IVarSet),
                list.append(As, [ReturnType], Args),
                (
                    inst_var_constraints_are_consistent_in_type_and_modes(Args)
                ->
                    Origin = user,
                    Result0 = ok1(Item),
                    Item = item_pred_decl(ItemPredDecl),
                    ItemPredDecl = item_pred_decl_info(Origin, TVarSet, IVarSet,
                        ExistQVars, pf_function, F, Args, no, no, MaybeDet,
                        Cond, Purity, ClassContext, Context),
                    check_no_attributes(Result0, Attributes, Result)
                ;
                    FullTermStr = describe_error_term(VarSet, FullTerm),
                    Pieces = [words("Error: inconsistent constraints"),
                        words("on inst variables in function declaration:"),
                        nl, words(FullTermStr), suffix("."), nl],
                    Spec = error_spec(severity_error, phase_term_to_parse_tree,
                        [simple_msg(get_term_context(FullTerm),
                            [always(Pieces)])]),
                    Result = error1([Spec])
                )
            )
        ;
            Pieces = [words("Error: syntax error in return type of"),
                quote(":- func"), words("declaration."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(ReturnTypeTerm),
                    [always(Pieces)])]),
            Result = error1([Spec])
        )
    ;
        FuncTermStr = describe_error_term(VarSet, FuncTerm),
        Pieces = [words("Error: syntax error in arguments of"),
            quote(":- func"), words("declaration at"),
            words(FuncTermStr), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(FuncTerm), [always(Pieces)])]),
        Result = error1([Spec])
    ).

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

    % Perform one of the following field-access syntax rewrites if possible:
    %
    %   A ^ f(B, ...)       --->    f(B, ..., A)
    %   (A ^ f(B, ...) := X)    --->    'f :='(B, ..., A, X)
    %
:- func desugar_field_access(term) = term.

desugar_field_access(Term) =
    (
        Term = functor(atom("^"), [A, RHS], _),
        RHS  = functor(atom(FieldName), Bs, Context)
    ->
        functor(atom(FieldName), Bs ++ [A], Context)
    ;
        Term = functor(atom(":="), [LHS, X], _),
        LHS  = functor(atom("^"), [A, RHS], Context),
        RHS  = functor(atom(FieldName), Bs, Context)
    ->
        functor(atom(FieldName ++ " :="), Bs ++ [A, X], Context)
    ;
        Term
    ).

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

    % Parse a `:- mode p(...)' declaration.
    %
:- pred process_mode(module_name::in, varset::in, term::in, condition::in,
    decl_attrs::in, maybe(mer_inst)::in, maybe(determinism)::in,
    prog_context::in, maybe1(item)::out) is det.

process_mode(ModuleName, VarSet, Term, Cond, Attributes, WithInst, MaybeDet,
        Context, Result) :-
    (
        WithInst = no,
        Term = term.functor(term.atom("="), [FuncTerm0, ReturnTypeTerm],
            _Context),
        FuncTerm = desugar_field_access(FuncTerm0)
    ->
        ContextPieces = [words("In function"), quote(":- mode"),
            words("declaration")],
        parse_implicitly_qualified_term(ModuleName, FuncTerm, Term,
            VarSet, ContextPieces, R),
        process_func_mode(R, ModuleName, FuncTerm, ReturnTypeTerm,
            Term, VarSet, MaybeDet, Cond, Attributes, Context, Result)
    ;
        ContextPieces = [words("In"), quote(":- mode"), words("declaration")],
        parse_implicitly_qualified_term(ModuleName, Term, Term,
            VarSet, ContextPieces, R),
        process_mode_decl(R, ModuleName, Term, VarSet,
            WithInst, MaybeDet, Cond, Attributes, Context, Result)
    ).

:- pred process_mode_decl(maybe_functor::in, module_name::in, term::in,
    varset::in, maybe(mer_inst)::in, maybe(determinism)::in, condition::in,
    decl_attrs::in, prog_context::in, maybe1(item)::out) is det.

process_mode_decl(error2(Specs), _, _, _, _, _, _, _, _, error1(Specs)).
process_mode_decl(ok2(F, As0), ModuleName, PredModeTerm, VarSet, WithInst,
        MaybeDet, Cond, Attributes0, Context, Result) :-
    ( convert_mode_list(allow_constrained_inst_var, As0, As1) ->
        get_class_context_and_inst_constraints(ModuleName, VarSet,
            Attributes0, Attributes, MaybeConstraints),
        (
            MaybeConstraints = ok3(_, _, InstConstraints),
            list.map(constrain_inst_vars_in_mode(InstConstraints), As1, As),
            varset.coerce(VarSet, ProgVarSet),
            ( inst_var_constraints_are_consistent_in_modes(As) ->
                (
                    WithInst = no,
                    PredOrFunc = yes(pf_predicate)
                ;
                    WithInst = yes(_),
                    % We don't know whether it's a predicate or a function
                    % until we expand out the inst.
                    PredOrFunc = no
                ),
                ItemModeDecl = item_mode_decl_info(ProgVarSet, PredOrFunc,
                    F, As, WithInst, MaybeDet, Cond, Context),
                Item = item_mode_decl(ItemModeDecl),
                Result0 = ok1(Item)
            ;
                PredModeTermStr = describe_error_term(VarSet, PredModeTerm),
                Pieces = [words("Error: inconsistent constraints"),
                    words("on inst variables"),
                    words("in predicate mode declaration:"), nl,
                    words(PredModeTermStr), suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(PredModeTerm),
                        [always(Pieces)])]),
                Result0 = error1([Spec])
            )
        ;
            MaybeConstraints = error3(Specs),
            Result0 = error1(Specs)
        ),
        check_no_attributes(Result0, Attributes, Result)
    ;
        PredModeTermStr = describe_error_term(VarSet, PredModeTerm),
        Pieces = [words("Error: syntax error in mode declaration at"),
            words(PredModeTermStr), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(PredModeTerm), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- pred process_func_mode(maybe_functor::in, module_name::in, term::in,
    term::in, term::in, varset::in, maybe(determinism)::in, condition::in,
    decl_attrs::in, prog_context::in, maybe1(item)::out) is det.

process_func_mode(error2(Specs), _, _, _, _, _, _, _, _, _, error1(Specs)).
process_func_mode(ok2(F, As0), ModuleName, FuncMode, RetMode0, FullTerm,
        VarSet, MaybeDet, Cond, Attributes0, Context, Result) :-
    (
        convert_mode_list(allow_constrained_inst_var, As0, As1)
    ->
        get_class_context_and_inst_constraints(ModuleName, VarSet,
            Attributes0, Attributes, MaybeConstraints),
        (
            MaybeConstraints = ok3(_, _, InstConstraints),
            list.map(constrain_inst_vars_in_mode(InstConstraints), As1, As),
            (
                convert_mode(allow_constrained_inst_var, RetMode0, RetMode1)
            ->
                constrain_inst_vars_in_mode(InstConstraints,
                    RetMode1, RetMode),
                varset.coerce(VarSet, InstVarSet),
                list.append(As, [RetMode], ArgModes),
                ( inst_var_constraints_are_consistent_in_modes(ArgModes) ->
                    ItemModeDecl = item_mode_decl_info(InstVarSet,
                        yes(pf_function), F, ArgModes, no, MaybeDet, Cond,
                        Context),
                    Item = item_mode_decl(ItemModeDecl),
                    Result0 = ok1(Item)
                ;
                    FullTermStr = describe_error_term(VarSet, FullTerm),
                    Pieces = [words("Error: inconsistent constraints"),
                        words("on inst variables"),
                        words("in function mode declaration:"), nl,
                        words(FullTermStr), suffix("."), nl],
                    Spec = error_spec(severity_error, phase_term_to_parse_tree,
                        [simple_msg(get_term_context(FullTerm),
                            [always(Pieces)])]),
                    Result0 = error1([Spec])
                )
            ;
                Pieces = [words("Error: syntax error in return mode"),
                    words("of function mode declaration."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(RetMode0),
                        [always(Pieces)])]),
                Result0 = error1([Spec])
            )
        ;
            MaybeConstraints = error3(Specs),
            Result0 = error1(Specs)
        ),
        check_no_attributes(Result0, Attributes, Result)
    ;
        % XXX Should say which argument.
        FuncModeStr = describe_error_term(VarSet, FuncMode),
        Pieces = [words("Error: syntax error in arguments of"),
            words("function mode declaration at"),
            words(FuncModeStr), suffix("."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(FuncMode), [always(Pieces)])]),
        Result = error1([Spec])
    ).

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

constrain_inst_vars_in_mode(Mode0, Mode) :-
    constrain_inst_vars_in_mode(map.init, Mode0, Mode).

constrain_inst_vars_in_mode(InstConstraints, I0 -> F0, I -> F) :-
    constrain_inst_vars_in_inst(InstConstraints, I0, I),
    constrain_inst_vars_in_inst(InstConstraints, F0, F).
constrain_inst_vars_in_mode(InstConstraints, user_defined_mode(Name, Args0),
        user_defined_mode(Name, Args)) :-
    list.map(constrain_inst_vars_in_inst(InstConstraints), Args0, Args).

:- pred constrain_inst_vars_in_inst(inst_var_sub::in,
    mer_inst::in, mer_inst::out) is det.

constrain_inst_vars_in_inst(_, any(U, none), any(U, none)).
constrain_inst_vars_in_inst(InstConstraints,
        any(U, higher_order(PredInstInfo0)),
        any(U, higher_order(PredInstInfo))) :-
    constrain_inst_vars_in_pred_inst_info(InstConstraints, PredInstInfo0,
        PredInstInfo).
constrain_inst_vars_in_inst(_, free, free).
constrain_inst_vars_in_inst(_, free(T), free(T)).
constrain_inst_vars_in_inst(InstConstraints, bound(U, BIs0), bound(U, BIs)) :-
    list.map(
        (pred(bound_functor(C, Is0)::in, bound_functor(C, Is)::out) is det :-
            list.map(constrain_inst_vars_in_inst(InstConstraints), Is0, Is)),
        BIs0, BIs).
constrain_inst_vars_in_inst(_, ground(U, none), ground(U, none)).
constrain_inst_vars_in_inst(InstConstraints,
        ground(U, higher_order(PredInstInfo0)),
        ground(U, higher_order(PredInstInfo))) :-
    constrain_inst_vars_in_pred_inst_info(InstConstraints, PredInstInfo0,
        PredInstInfo).
constrain_inst_vars_in_inst(InstConstraints,
        constrained_inst_vars(Vars0, Inst0),
        constrained_inst_vars(Vars, Inst)) :-
    constrain_inst_vars_in_inst(InstConstraints, Inst0, Inst1),
    ( Inst1 = constrained_inst_vars(Vars2, Inst2) ->
        Vars = Vars0 `set.union` Vars2,
        Inst = Inst2
    ;
        Vars = Vars0,
        Inst = Inst1
    ).
constrain_inst_vars_in_inst(_, not_reached, not_reached).
constrain_inst_vars_in_inst(InstConstraints, inst_var(Var),
        constrained_inst_vars(set.make_singleton_set(Var), Inst)) :-
    ( map.search(InstConstraints, Var, Inst0) ->
        Inst = Inst0
    ;
        Inst = ground(shared, none)
    ).
constrain_inst_vars_in_inst(InstConstraints, defined_inst(Name0),
        defined_inst(Name)) :-
    constrain_inst_vars_in_inst_name(InstConstraints, Name0, Name).
constrain_inst_vars_in_inst(InstConstraints, abstract_inst(N, Is0),
        abstract_inst(N, Is)) :-
    list.map(constrain_inst_vars_in_inst(InstConstraints), Is0, Is).

:- pred constrain_inst_vars_in_pred_inst_info(inst_var_sub::in,
    pred_inst_info::in, pred_inst_info::out) is det.

constrain_inst_vars_in_pred_inst_info(InstConstraints, PII0, PII) :-
    PII0 = pred_inst_info(PredOrFunc, Modes0, Det),
    list.map(constrain_inst_vars_in_mode(InstConstraints), Modes0, Modes),
    PII = pred_inst_info(PredOrFunc, Modes, Det).

:- pred constrain_inst_vars_in_inst_name(inst_var_sub::in,
    inst_name::in, inst_name::out) is det.

constrain_inst_vars_in_inst_name(InstConstraints, Name0, Name) :-
    ( Name0 = user_inst(SymName, Args0) ->
        list.map(constrain_inst_vars_in_inst(InstConstraints), Args0, Args),
        Name = user_inst(SymName, Args)
    ;
        Name = Name0
    ).

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

inst_var_constraints_are_consistent_in_modes(Modes) :-
    inst_var_constraints_are_consistent_in_modes(Modes, map.init, _).

:- pred inst_var_constraints_are_consistent_in_modes(list(mer_mode)::in,
    inst_var_sub::in, inst_var_sub::out) is semidet.

inst_var_constraints_are_consistent_in_modes(Modes, !Sub) :-
    list.foldl(inst_var_constraints_are_consistent_in_mode, Modes, !Sub).

:- pred inst_var_constraints_are_consistent_in_type_and_modes(
    list(type_and_mode)::in) is semidet.

inst_var_constraints_are_consistent_in_type_and_modes(TypeAndModes) :-
    list.foldl((pred(TypeAndMode::in, in, out) is semidet -->
        (
            { TypeAndMode = type_only(_) }
        ;
            { TypeAndMode = type_and_mode(_, Mode) },
            inst_var_constraints_are_consistent_in_mode(Mode)
        )), TypeAndModes, map.init, _).

:- pred inst_var_constraints_are_consistent_in_mode(mer_mode::in,
    inst_var_sub::in, inst_var_sub::out) is semidet.

inst_var_constraints_are_consistent_in_mode(InitialInst -> FinalInst, !Sub) :-
    inst_var_constraints_are_consistent_in_inst(InitialInst, !Sub),
    inst_var_constraints_are_consistent_in_inst(FinalInst, !Sub).
inst_var_constraints_are_consistent_in_mode(user_defined_mode(_, ArgInsts),
        !Sub) :-
    inst_var_constraints_are_consistent_in_insts(ArgInsts, !Sub).

:- pred inst_var_constraints_are_consistent_in_insts(list(mer_inst)::in,
    inst_var_sub::in, inst_var_sub::out) is semidet.

inst_var_constraints_are_consistent_in_insts(Insts, !Sub) :-
    list.foldl(inst_var_constraints_are_consistent_in_inst, Insts, !Sub).

:- pred inst_var_constraints_are_consistent_in_inst(mer_inst::in,
    inst_var_sub::in, inst_var_sub::out) is semidet.

inst_var_constraints_are_consistent_in_inst(any(_, HOInstInfo), !Sub) :-
    (
        HOInstInfo = none
    ;
        HOInstInfo = higher_order(pred_inst_info(_, Modes, _)),
        inst_var_constraints_are_consistent_in_modes(Modes, !Sub)
    ).
inst_var_constraints_are_consistent_in_inst(free, !Sub).
inst_var_constraints_are_consistent_in_inst(free(_), !Sub).
inst_var_constraints_are_consistent_in_inst(bound(_, BoundInsts), !Sub) :-
    list.foldl(
        (pred(bound_functor(_, Insts)::in, in, out) is semidet -->
            inst_var_constraints_are_consistent_in_insts(Insts)),
        BoundInsts, !Sub).
inst_var_constraints_are_consistent_in_inst(ground(_, HOInstInfo), !Sub) :-
    (
        HOInstInfo = none
    ;
        HOInstInfo = higher_order(pred_inst_info(_, Modes, _)),
        inst_var_constraints_are_consistent_in_modes(Modes, !Sub)
    ).
inst_var_constraints_are_consistent_in_inst(not_reached, !Sub).
inst_var_constraints_are_consistent_in_inst(inst_var(_), !Sub) :-
    unexpected(this_file, "inst_var_constraints_are_consistent_in_inst: " ++
        "unconstrained inst_var").
inst_var_constraints_are_consistent_in_inst(defined_inst(InstName), !Sub) :-
    ( InstName = user_inst(_, Insts) ->
        inst_var_constraints_are_consistent_in_insts(Insts, !Sub)
    ;
        true
    ).
inst_var_constraints_are_consistent_in_inst(abstract_inst(_, Insts), !Sub) :-
    inst_var_constraints_are_consistent_in_insts(Insts, !Sub).
inst_var_constraints_are_consistent_in_inst(
        constrained_inst_vars(InstVars, Inst), !Sub) :-
    set.fold((pred(InstVar::in, in, out) is semidet -->
        ( Inst0 =^ map.elem(InstVar) ->
            % Check that the inst_var constraint is consistent with
            % the previous constraint on this inst_var.
            { Inst = Inst0 }
        ;
            ^ map.elem(InstVar) := Inst
        )), InstVars, !Sub),
    inst_var_constraints_are_consistent_in_inst(Inst, !Sub).

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

    % Parse a `:- inst <InstDefn>.' declaration.
    %
:- pred parse_inst_decl(module_name::in, varset::in, term::in,
    prog_context::in, maybe1(item)::out) is det.

parse_inst_decl(ModuleName, VarSet, InstDefn, Context, Result) :-
    % XXX Some of the tests here could be factored out.
    (
        InstDefn = term.functor(term.atom("=="), [H, B], _Context)
    ->
        get_condition(B, Body, Condition),
        convert_inst_defn(ModuleName, VarSet, H, Body, R),
        process_maybe1(make_inst_defn(VarSet, Condition, Context), R, Result)
    ;
        % XXX This is for `abstract inst' declarations,
        % which are not really supported.
        InstDefn = term.functor(term.atom("is"), Args, _Context),
        Args = [Head, term.functor(term.atom("private"), [], _)]
    ->
        Condition = cond_true,
        convert_abstract_inst_defn(ModuleName, VarSet, Head, R),
        process_maybe1(make_inst_defn(VarSet, Condition, Context), R, Result)
    ;
        InstDefn = term.functor(term.atom("--->"), [H, B], _Context)
    ->
        get_condition(B, Body, Condition),
        Body1 = term.functor(term.atom("bound"), [Body], Context),
        convert_inst_defn(ModuleName, VarSet, H, Body1, R),
        % We should check the condition for errors. We don't bother
        % at the moment, since we ignore conditions anyhow :-)
        process_maybe1(make_inst_defn(VarSet, Condition, Context), R, Result)
    ;
        Pieces = [words("Error:"), quote("=="), words("expected in"),
            quote(":- inst"), words("definition."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(InstDefn), [always(Pieces)])]),
        Result = error1([Spec])
    ).

    % Parse a `:- inst <Head> ---> <Body>.' definition.
    %
:- pred convert_inst_defn(module_name::in, varset::in, term::in, term::in,
    maybe1(processed_inst_body)::out) is det.

convert_inst_defn(ModuleName, VarSet, HeadTerm, BodyTerm, Result) :-
    ContextPieces = [words("In inst definition:")],
    parse_implicitly_qualified_term(ModuleName, HeadTerm, BodyTerm,
        VarSet, ContextPieces, QualResult),
    convert_inst_defn_2(QualResult, VarSet, HeadTerm, BodyTerm, Result).

:- pred convert_inst_defn_2(maybe_functor::in, varset::in, term::in, term::in,
    maybe1(processed_inst_body)::out) is det.

convert_inst_defn_2(error2(Specs), _, _, _, error1(Specs)).
convert_inst_defn_2(ok2(Name, ArgTerms), VarSet, HeadTerm, BodyTerm, Result) :-
    (
        % Check that all the head args are variables.
        term.term_list_to_var_list(ArgTerms, Args)
    ->
        (
            % Check that all the head arg variables are distinct.
            list.member(Arg2, Args, [Arg2 | OtherArgs]),
            list.member(Arg2, OtherArgs)
        ->
            % XXX Should improve the error message here.
            Pieces = [words("Error: repeated inst parameters"),
                words("in LHS of inst definition."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            % Check that all the variables in the body occur in the head.
            term.contains_var(BodyTerm, Var2),
            \+ list.member(Var2, Args)
        ->
            Pieces = [words("Error: free inst parameter"),
                words("in RHS of inst definition."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(BodyTerm), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            % Check that the inst is a valid user-defined inst, i.e. that it
            % does not have the form of one of the builtin insts.
            \+ (
                convert_inst(no_allow_constrained_inst_var, HeadTerm,
                    UserInst),
                UserInst = defined_inst(user_inst(_, _))
            )
        ->
            % XXX Name the builtin inst.
            Pieces = [words("Error: attempt to redefine builtin inst."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            % Should improve the error message here.
            (
                convert_inst(no_allow_constrained_inst_var, BodyTerm,
                    ConvertedBody)
            ->
                list.map(term.coerce_var, Args, InstArgs),
                Result = ok1(processed_inst_body(Name, InstArgs,
                        eqv_inst(ConvertedBody)))
            ;
                BodyTermStr = describe_error_term(VarSet, BodyTerm),
                Pieces = [words("Error: syntax error in inst body at"),
                    words(BodyTermStr), suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(BodyTerm),
                        [always(Pieces)])]),
                Result = error1([Spec])
            )
        )
    ;
        % XXX If term_list_to_var_list returned the non-var's term or context,
        % we could use it here.
        Pieces = [words("Error: inst parameters must be variables."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(HeadTerm), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- type processed_inst_body
    --->    processed_inst_body(
                sym_name,
                list(inst_var),
                inst_defn
            ).

:- pred convert_abstract_inst_defn(module_name::in, varset::in, term::in,
    maybe1(processed_inst_body)::out) is det.

convert_abstract_inst_defn(ModuleName, VarSet, HeadTerm, Result) :-
    ContextPieces = [words("In inst definition:")],
    parse_implicitly_qualified_term(ModuleName, HeadTerm, HeadTerm,
        VarSet, ContextPieces, HeadResult),
    convert_abstract_inst_defn_2(HeadResult, HeadTerm, Result).

:- pred convert_abstract_inst_defn_2(maybe_functor::in, term::in,
    maybe1(processed_inst_body)::out) is det.

convert_abstract_inst_defn_2(error2(Specs), _, error1(Specs)).
convert_abstract_inst_defn_2(ok2(Name, ArgTerms), Head, Result) :-
    (
        % Check that all the head args are variables.
        term.term_list_to_var_list(ArgTerms, Args)
    ->
        (
            % Check that all the head arg variables are distinct.
            list.member(Arg2, Args, [Arg2 | OtherArgs]),
            list.member(Arg2, OtherArgs)
        ->
            % XXX We should we list the repeated parameters?
            Pieces = [words("Error: repeated inst parameters"),
                words("in abstract inst definition."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Head), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            list.map(term.coerce_var, Args, InstArgs),
            Result = ok1(processed_inst_body(Name, InstArgs, abstract_inst))
        )
    ;
        % XXX If term_list_to_var_list returned the non-var's term or context,
        % we could use it here.
        Pieces = [words("Error: inst parameters must be variables."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(Head), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- pred make_inst_defn(varset::in, condition::in, prog_context::in,
    processed_inst_body::in, item::out) is det.

make_inst_defn(VarSet0, Cond, Context, ProcessedInstBody, Item) :-
    ProcessedInstBody = processed_inst_body(Name, Params, InstDefn),
    varset.coerce(VarSet0, VarSet),
    ItemInstDefn = item_inst_defn_info(VarSet, Name, Params, InstDefn, Cond,
        Context),
    Item = item_inst_defn(ItemInstDefn).

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

    % Parse a `:- mode foo == ...' definition.
    %
:- pred parse_mode_decl(module_name::in, varset::in, term::in, decl_attrs::in,
    prog_context::in, maybe1(item)::out) is det.

parse_mode_decl(ModuleName, VarSet, ModeDefn, Attributes, Context, Result) :-
    ( mode_op(ModeDefn, H, B) ->
        get_condition(B, Body, Condition),
        convert_mode_defn(ModuleName, VarSet, H, Body, R),
        process_maybe1(make_mode_defn(VarSet, Condition, Context), R, Result)
    ;
        parse_mode_decl_pred(ModuleName, VarSet, ModeDefn, Attributes,
            Context, Result)
    ).

:- pred mode_op(term::in, term::out, term::out) is semidet.

mode_op(term.functor(term.atom(Op), [H, B], _), H, B) :-
    Op = "==".

:- type processed_mode_body
    --->    processed_mode_body(
                sym_name,
                list(inst_var),
                mode_defn
            ).

:- pred convert_mode_defn(module_name::in, varset::in, term::in, term::in,
    maybe1(processed_mode_body)::out) is det.

convert_mode_defn(ModuleName, VarSet, HeadTerm, BodyTerm, Result) :-
    ContextPieces = [words("In mode definition:")],
    parse_implicitly_qualified_term(ModuleName, HeadTerm, HeadTerm,
        VarSet, ContextPieces, HeadResult),
    convert_mode_defn_2(HeadResult, HeadTerm, BodyTerm, Result).

:- pred convert_mode_defn_2(maybe_functor::in, term::in, term::in,
    maybe1(processed_mode_body)::out) is det.

convert_mode_defn_2(error2(Specs), _, _, error1(Specs)).
convert_mode_defn_2(ok2(Name, ArgTerms), Head, Body, Result) :-
    (
        % Check that all the head args are variables.
        term.term_list_to_var_list(ArgTerms, Args)
    ->
        (
            % Check that all the head arg variables are distinct.
            list.member(Arg2, Args, [Arg2 | OtherArgs]),
            list.member(Arg2, OtherArgs)
        ->
            % Check that all the head arg variables are distinct.
            % XXX We should list the duplicated head arg variables.
            Pieces = [words("Error: repeated parameters"),
                words("in LHS of mode definition."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Head), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            % Check that all the variables in the body occur in the head.
            term.contains_var(Body, Var2),
            \+ list.member(Var2, Args)
        ->
            % XXX Shouldn't we be using the Body's context?
            % XXX We should list the Var2s for which the condition holds.
            Pieces = [words("Error: free inst parameter"),
                words("in RHS of mode definition."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Head), [always(Pieces)])]),
            Result = error1([Spec])
        ;
            (
                convert_mode(no_allow_constrained_inst_var, Body,
                    ConvertedBody)
            ->
                list.map(term.coerce_var, Args, InstArgs),
                Result = ok1(processed_mode_body(Name, InstArgs,
                    eqv_mode(ConvertedBody)))
            ;
                % XXX We should improve the error message here.
                Pieces = [words("Error: syntax error"),
                    words("in mode definition body."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Body), [always(Pieces)])]),
                Result = error1([Spec])
            )
        )
    ;
        % XXX If term_list_to_var_list returned the non-var's term or context,
        % we could use it here.
        Pieces = [words("Error: mode parameters must be variables."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(get_term_context(Head), [always(Pieces)])]),
        Result = error1([Spec])
    ).

:- pred convert_type_and_mode_list(inst_var_sub::in, list(term)::in,
    list(type_and_mode)::out) is semidet.

convert_type_and_mode_list(_, [], []).
convert_type_and_mode_list(InstConstraints, [H0 | T0], [H | T]) :-
    convert_type_and_mode(InstConstraints, H0, H),
    convert_type_and_mode_list(InstConstraints, T0, T).

:- pred convert_type_and_mode(inst_var_sub::in, term::in, type_and_mode::out)
    is semidet.

convert_type_and_mode(InstConstraints, Term, Result) :-
    ( Term = term.functor(term.atom("::"), [TypeTerm, ModeTerm], _Context) ->
        maybe_parse_type(TypeTerm, Type),
        convert_mode(allow_constrained_inst_var, ModeTerm, Mode0),
        constrain_inst_vars_in_mode(InstConstraints, Mode0, Mode),
        Result = type_and_mode(Type, Mode)
    ;
        maybe_parse_type(Term, Type),
        Result = type_only(Type)
    ).

:- pred make_mode_defn(varset::in, condition::in, prog_context::in,
    processed_mode_body::in, item::out) is det.

make_mode_defn(VarSet0, Cond, Context, ProcessedModeBody, Item) :-
    ProcessedModeBody = processed_mode_body(Name, Params, ModeDefn),
    varset.coerce(VarSet0, VarSet),
    ItemModeDefn = item_mode_defn_info(VarSet, Name, Params, ModeDefn, Cond,
        Context),
    Item = item_mode_defn(ItemModeDefn).

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

:- type maker(T1, T2) == pred(T1, T2).
:- mode maker == (pred(in, out) is det).

:- pred parse_symlist_decl(parser(module_specifier)::parser,
    maker(list(module_specifier), module_defn)::maker,
    term::in, decl_attrs::in, prog_context::in, maybe1(item)::out) is det.

parse_symlist_decl(ParserPred, MakeModuleDefnPred, Term, Attributes, Context,
        Result) :-
    parse_list(ParserPred, Term, Result0),
    process_maybe1(make_module_defn(MakeModuleDefnPred, Context),
        Result0, Result1),
    check_no_attributes(Result1, Attributes, Result).

:- pred make_module_defn(maker(list(module_specifier), module_defn)::maker,
    prog_context::in, list(module_specifier)::in, item::out) is det.

make_module_defn(MakeModuleDefnPred, Context, ModuleSpecs, Item) :-
    call(MakeModuleDefnPred, ModuleSpecs, ModuleDefn),
    ItemModuleDefn = item_module_defn_info(ModuleDefn, Context),
    Item = item_module_defn(ItemModuleDefn).

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

:- pred process_maybe1(maker(T1, T2)::maker, maybe1(T1)::in, maybe1(T2)::out)
    is det.

process_maybe1(Maker, ok1(X), ok1(Y)) :-
    call(Maker, X, Y).
process_maybe1(_, error1(Specs), error1(Specs)).

:- pred process_maybe1_to_t(maker(T1, maybe1(T2))::maker,
    maybe1(T1)::in, maybe1(T2)::out) is det.

process_maybe1_to_t(Maker, ok1(X), Y) :-
    call(Maker, X, Y).
process_maybe1_to_t(_, error1(Specs), error1(Specs)).

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

    % A ModuleSpecifier is just an sym_name.
    %
:- pred parse_module_specifier(varset::in, term::in,
    maybe1(module_specifier)::out) is det.

parse_module_specifier(VarSet, Term, Result) :-
    parse_symbol_name(VarSet, Term, Result).

    % A ModuleName is an implicitly-quantified sym_name.
    %
    % We check for module names starting with capital letters as a special
    % case, so that we can report a better error message for that case.
    %
:- pred parse_module_name(module_name::in, varset::in, term::in,
    maybe1(module_name)::out) is det.

parse_module_name(DefaultModuleName, VarSet, Term, Result) :-
    (
        Term = term.variable(_, Context),
        Pieces = [words("Error: module names starting with capital letters"),
            words("must be quoted using single quotes"),
            words("(e.g. "":- module 'Foo'."")."), nl],
        Spec = error_spec(severity_error, phase_term_to_parse_tree,
            [simple_msg(Context, [always(Pieces)])]),
        Result = error1([Spec])
    ;
        Term = term.functor(_, _, _),
        parse_implicitly_qualified_symbol_name(DefaultModuleName, VarSet,
            Term, Result)
    ).

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

    % A SymbolNameSpecifier is one of
    %   SymbolName
    %   SymbolName/Arity
    %       Matches only symbols of the specified arity.
    %
:- pred parse_symbol_name_specifier(varset::in, term::in,
    maybe1(sym_name_specifier)::out) is det.

parse_symbol_name_specifier(VarSet, Term, Result) :-
    root_module_name(DefaultModule),
    parse_implicitly_qualified_symbol_name_specifier(DefaultModule, VarSet,
        Term, Result).

:- pred parse_implicitly_qualified_symbol_name_specifier(module_name::in,
    varset::in, term::in, maybe1(sym_name_specifier)::out) is det.

parse_implicitly_qualified_symbol_name_specifier(DefaultModule, VarSet, Term,
        Result) :-
    ( Term = term.functor(term.atom("/"), [NameTerm, ArityTerm], _Context) ->
        ( ArityTerm = term.functor(term.integer(Arity), [], _Context2) ->
            ( Arity >= 0 ->
                parse_implicitly_qualified_symbol_name(DefaultModule, VarSet,
                    NameTerm, NameResult),
                process_maybe1(make_name_arity_specifier(Arity),
                    NameResult, Result)
            ;
                Pieces = [words("Error: arity in symbol name specifier"),
                    words("must be a non-negative integer."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Term), [always(Pieces)])]),
                Result = error1([Spec])
            )
        ;
            Pieces = [words("Error: arity in symbol name specifier"),
                words("must be an integer."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            Result = error1([Spec])
        )
    ;
        parse_implicitly_qualified_symbol_name(DefaultModule, VarSet, Term,
            SymbolNameResult),
        process_maybe1(make_name_specifier, SymbolNameResult, Result)
    ).

:- pred make_name_arity_specifier(arity::in, sym_name::in,
    sym_name_specifier::out) is det.

make_name_arity_specifier(Arity, Name, name_arity(Name, Arity)).

:- pred make_name_specifier(sym_name::in, sym_name_specifier::out) is det.

make_name_specifier(Name, name(Name)).

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

    % A SymbolName is one of
    %   Name
    %       Matches symbols with the specified name in the
    %       current namespace.
    %   Module.Name
    %       Matches symbols with the specified name exported
    %       by the specified module (where Module is itself a SymbolName).
    %
    % We also allow the syntax `Module__Name' as an alternative
    % for `Module.Name'.
    %
:- pred parse_symbol_name(varset(T)::in, term(T)::in, maybe1(sym_name)::out)
    is det.

parse_symbol_name(VarSet, Term, Result) :-
    (
        Term = term.functor(term.atom(FunctorName), [ModuleTerm, NameTerm],
            TermContext),
        ( FunctorName = ":"
        ; FunctorName = "."
        )
    ->
        ( NameTerm = term.functor(term.atom(Name), [], _Context1) ->
            parse_symbol_name(VarSet, ModuleTerm, ModuleResult),
            (
                ModuleResult = ok1(Module),
                Result = ok1(qualified(Module, Name))
            ;
                ModuleResult = error1(_ModuleResultSpecs),
                % XXX We should say "module name" OR "identifier", not both.
                Pieces = [words("Error: module name identifier"),
                    words("expected before"), quote(FunctorName),
                    words("in qualified symbol name."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(TermContext, [always(Pieces)])]),
                % XXX Should we include _ModuleResultSpecs?
                Result = error1([Spec])
            )
        ;
            Pieces = [words("Error: identifier expected after"),
                quote(FunctorName), words("in qualified symbol name."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(TermContext, [always(Pieces)])]),
            Result = error1([Spec])
        )
    ;
        ( Term = term.functor(term.atom(Name), [], _) ->
            SymName = string_to_sym_name_sep(Name, "__"),
            Result = ok1(SymName)
        ;
            TermStr = describe_error_term(VarSet, Term),
            Pieces = [words("Error: symbol name expected at"),
                words(TermStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            Result = error1([Spec])
        )
    ).

:- pred parse_implicitly_qualified_symbol_name(module_name::in, varset::in,
    term::in, maybe1(sym_name)::out) is det.

parse_implicitly_qualified_symbol_name(DefaultModName, VarSet, Term, Result) :-
    parse_symbol_name(VarSet, Term, Result0),
    (
        Result0 = ok1(SymName),
        (
            root_module_name(DefaultModName)
        ->
            Result = Result0
        ;
            SymName = qualified(ModName, _),
            \+ match_sym_name(ModName, DefaultModName)
        ->
            Pieces = [words("Error: module qualifier in definition"),
                words("does not match preceding"), quote(":- module"),
                words("declaration."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            Result = error1([Spec])

        ;
            UnqualName = unqualify_name(SymName),
            Result = ok1(qualified(DefaultModName, UnqualName))
        )
    ;
        Result0 = error1(_),
        Result = Result0
    ).

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

parse_implicitly_qualified_term(DefaultModuleName, Term, ContainingTerm,
        VarSet, ContextPieces, Result) :-
    parse_qualified_term(Term, ContainingTerm, VarSet, ContextPieces, Result0),
    ( Result0 = ok2(SymName, Args) ->
        (
            root_module_name(DefaultModuleName)
        ->
            Result = Result0
        ;
            SymName = qualified(ModuleName, _),
            \+ match_sym_name(ModuleName, DefaultModuleName)
        ->
            Pieces = [words("Error: module qualifier in definition"),
                words("does not match preceding"), quote(":- module"),
                words("declaration."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            Result = error2([Spec])
        ;
            UnqualName = unqualify_name(SymName),
            Result = ok2(qualified(DefaultModuleName, UnqualName), Args)
        )
    ;
        Result = Result0
    ).

sym_name_and_args(Term, SymName, Args) :-
    % The values of VarSet and ContextPieces do not matter here, since
    % we succeed only if they aren't used.
    VarSet = varset.init,
    ContextPieces = [],
    parse_qualified_term(Term, Term, VarSet, ContextPieces,
        ok2(SymName, Args)).

parse_qualified_term(Term, _ContainingTerm, VarSet, ContextPieces, Result) :-
    % XXX We should delete the _ContainingTerm argument.
    (
        Term = term.functor(Functor, FunctorArgs, TermContext),
        Functor = term.atom("."),
        FunctorArgs = [ModuleTerm, NameArgsTerm]
    ->
        ( NameArgsTerm = term.functor(term.atom(Name), Args, _) ->
            varset.coerce(VarSet, GenericVarSet),
            parse_symbol_name(GenericVarSet, ModuleTerm, ModuleResult),
            (
                ModuleResult = ok1(Module),
                Result = ok2(qualified(Module, Name), Args)
            ;
                ModuleResult = error1(_),
                ModuleTermStr = describe_error_term(GenericVarSet, ModuleTerm),
                % XXX We should say "module name" OR "identifier", not both.
                Pieces = ContextPieces ++ [lower_case_next_if_not_first,
                    words("Error: module name identifier expected before '.'"),
                    words("in qualified symbol name, not"),
                    words(ModuleTermStr), suffix("."), nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(TermContext, [always(Pieces)])]),
                Result = error2([Spec])
            )
        ;
            varset.coerce(VarSet, GenericVarSet),
            TermStr = describe_error_term(GenericVarSet, Term),
            Pieces = ContextPieces ++ [lower_case_next_if_not_first,
                words("Error: identifier expected after '.'"),
                words("in qualified symbol name, not"),
                words(TermStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(TermContext, [always(Pieces)])]),
            Result = error2([Spec])
        )
    ;
        varset.coerce(VarSet, GenericVarSet),
        ( Term = term.functor(term.atom(Name), Args, _) ->
            SymName = string_to_sym_name_sep(Name, "__"),
            Result = ok2(SymName, Args)
        ;
            TermStr = describe_error_term(GenericVarSet, Term),
            Pieces = ContextPieces ++ [lower_case_next_if_not_first,
                words("Error: atom expected at"),
                words(TermStr), suffix("."), nl],
            Spec = error_spec(severity_error, phase_term_to_parse_tree,
                [simple_msg(get_term_context(Term), [always(Pieces)])]),
            Result = error2([Spec])
        )
    ).

%-----------------------------------------------------------------------------%
%
% Predicates used to convert a sym_list to a program item.

:- pred make_use(list(module_specifier)::in, module_defn::out) is det.

make_use(Syms, md_use(Syms)).

:- pred make_import(list(module_specifier)::in, module_defn::out) is det.

make_import(Syms, md_import(Syms)).

:- pred make_export(list(module_specifier)::in, module_defn::out) is det.

make_export(Syms, md_export(Syms)).

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

:- func convert_constructor_arg_list(module_name, varset, list(term)) =
    maybe1(list(constructor_arg)).

convert_constructor_arg_list(_, _, []) = ok1([]).
convert_constructor_arg_list(ModuleName, VarSet, [Term | Terms]) = Result :-
    ( Term = term.functor(term.atom("::"), [NameTerm, TypeTerm], _) ->
        ContextPieces = [words("In field name:")],
        parse_implicitly_qualified_term(ModuleName, NameTerm, Term,
            VarSet, ContextPieces, NameResult),
        (
            NameResult = error2(Specs),
            Result = error1(Specs)
        ;
            NameResult = ok2(SymName, SymNameArgs),
            (
                SymNameArgs = [_ | _],
                % XXX Should we add "... at function symbol ..."?
                Pieces = [words("Error: syntax error in constructor name."),
                    nl],
                Spec = error_spec(severity_error, phase_term_to_parse_tree,
                    [simple_msg(get_term_context(Term), [always(Pieces)])]),
                Result = error1([Spec])
            ;
                SymNameArgs = [],
                MaybeFieldName = yes(SymName),
                Result = convert_constructor_arg_list_2(ModuleName, VarSet,
                    MaybeFieldName, TypeTerm, Terms)
            )
        )
    ;
        MaybeFieldName = no,
        TypeTerm = Term,
        Result = convert_constructor_arg_list_2(ModuleName, VarSet,
            MaybeFieldName, TypeTerm, Terms)
    ).

:- func convert_constructor_arg_list_2(module_name, varset, maybe(sym_name),
    term, list(term)) = maybe1(list(constructor_arg)).

convert_constructor_arg_list_2(ModuleName, VarSet, MaybeFieldName,
        TypeTerm, Terms) = Result :-
    ContextPieces = [words("In type definition:")],
    parse_type(TypeTerm, VarSet, ContextPieces, TypeResult),
    (
        TypeResult = ok1(Type),
        Context = get_term_context(TypeTerm),
        Arg = ctor_arg(MaybeFieldName, Type, Context),
        Result0 = convert_constructor_arg_list(ModuleName, VarSet, Terms),
        (
            Result0 = error1(Specs),
            Result  = error1(Specs)
        ;
            Result0 = ok1(Args),
            Result  = ok1([Arg | Args])
        )
    ;
        TypeResult = error1(Specs),
        Result = error1(Specs)
    ).

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

    % We use the empty module name ('') as the "root" module name; when adding
    % default module qualifiers in parse_implicitly_qualified_{term,symbol},
    % if the default module is the root module then we don't add any qualifier.
    %
:- pred root_module_name(module_name::out) is det.

root_module_name(unqualified("")).

%-----------------------------------------------------------------------------%
%
% You can uncomment this section for debugging.
%

% :- interface.
%
% :- pred write_item_to_stream(io.output_stream::in, item::in, io::di, io::uo)
%     is det.
%
% :- pred write_item_to_stdout(item::in, io::di, io::uo) is det.
%
% :- pred write_items_to_file(string::in, list(item)::in, io::di, io::uo)
%     is det.
%
% :- implementation.
%
% :- import_module pretty_printer.
%
% write_item_to_stream(Stream, Item, !IO) :-
%     write_doc(Stream, format(Item), !IO),
%     io.nl(Stream, !IO).
%
% write_item_to_stdout(Item, !IO) :-
%     write_item_to_stream(io.stdout_stream, Item, !IO).
%
% write_items_to_file(FileName, Items, !IO) :-
%     io.open_output(FileName, Result, !IO),
%     (
%         Result = ok(Stream),
%         list.foldl(write_item_to_stream(Stream), Items, !IO)
%     ;
%         Result = error(_)
%     ).

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

:- func this_file = string.

this_file = "prog_io.m".

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