%-----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%-----------------------------------------------------------------------------%
% Compile with: mmc --allow-stubs -C zinc_rt_driver.m.

:- module zinc_rt_driver.
:- interface.

:- import_module bool.
:- import_module io.
:- import_module list.

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

:- type ss ---> ss.
:- type zinc_error ---> zinc_error.
:- type zinc_errors == list(zinc_error).
:- type parse_table ---> parse_table.
:- type symbol_table ---> symbol_table.
:- type search_info ---> search_info.
:- type context_location ---> context_location.

:- type io_stage(A, B, Error) ==
    (pred(A, B, list(Error), list(Error), io, io)).
:- type io_stage(A, B) == io_stage(A, B, zinc_error).
:- inst io_stage_det == ( pred(in, out, out, out, di, uo) is det ).
:- inst io_stage_cc_multi == ( pred(in, out, out, out, di, uo) is cc_multi ).

:- type assertion_ref(T) ---> assertion_ref(T).

:- type search_warning_type
    --->    swt_incompleteness
    ;       swt_other.

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

:- type output_or_errors
    --->    output(string)
    ;       eval_errors(zinc_errors).

:- type problem_kind
    --->    pk_satisfaction
    ;       pk_optimization.

:- type driver_params
    --->    driver_params(
                prog_name           :: string,
                error_context_locn   :: context_location
            ).

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

:- type problem == (pred(bool, bool, symbol_table, parse_table, search_info,
    output_or_errors, ss, ss)).
:- inst problem == (pred(in, in, in, in, in, out, mdi, muo) is nondet).

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

:- implementation.

:- import_module char.
:- import_module exception.
:- import_module int.
:- import_module maybe.
:- import_module string.
:- import_module unit.
:- import_module univ.

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

:- pred evaluation(problem_kind::in, problem::in(problem), solutions_opt::in,
    driver_params::in,
    bool::in, bool::in, maybe(string)::in)
    : io_stage({symbol_table, parse_table}, unit)
    `with_inst` io_stage_cc_multi.

evaluation(ProblemKind, Problem, SolutionsOpt, DParams,
        Verbose, Statistics, MaybeOutputFile,
        {SymTbl, ParseTbl}, unit, Errs, Warns, !IO) :-
    ProgName = DParams ^ prog_name,
    (
        MaybeOutputFile = yes(OutputFileName),
        io.open_output(OutputFileName, OpenResult, !IO),
        (
            OpenResult = ok(File)
        ;
            OpenResult = error(IO_Error),
            throw(IO_Error)
        )
    ;
        MaybeOutputFile = no,
        io.stdout_stream(File, !IO)
    ),
    SearchName = ProgName,
    SearchSpec = "",
    init_terminator_signal(TermSig, !IO),
    create_search_info(SearchName, SearchSpec, TermSig, SearchInfo, !IO),
    ( try [io(!IO)] (
        SolnInfo0 = soln_info(0, []),
        (
            SolutionsOpt = first_solution,
            ProblemFirst = (pred(Soln::out, !.SS::mdi, !:SS::muo) is nondet :-
                Problem(Verbose, Statistics, SymTbl, ParseTbl, SearchInfo,
                    Soln, !SS),
                (
                    ProblemKind = pk_satisfaction,
                    add_search_warning(SearchInfo, swt_incompleteness,
                        "commit to first solution", !SS)
                ;
                    ProblemKind = pk_optimization
                )
            ),
            g12_solve_first(ProblemFirst, MaybeSoln, !IO),
            (
                MaybeSoln = no,
                SolnInfo = SolnInfo0
            ;
                MaybeSoln = yes(_SolnOrErrors),
                io.write_string(File, "solution", !IO),
                SolnInfo = SolnInfo0
            )
        ;
            SolutionsOpt = some_solutions(SolnLimit),
            ProblemSome = (pred(Soln::out, !.SS::mdi, !:SS::muo) is nondet :-
                Problem(Verbose, Statistics, SymTbl, ParseTbl, SearchInfo,
                    Soln, !SS)
            ),
            new_assertion_ref(SolnInfo0, SolnInfoRef, !IO),
            g12_do_while_io(ProblemSome,
                handle_solution_with_limit(File, SolnLimit,
                    SolnInfoRef, SearchInfo, ProblemKind),
                !IO),
            query(SolnInfoRef, SolnInfo, !IO)
        ;
            SolutionsOpt = all_solutions,
            ProblemAll = (pred(Soln::out, !.SS::mdi, !:SS::muo) is nondet :-
                Problem(Verbose, Statistics, SymTbl, ParseTbl, SearchInfo,
                    Soln, !SS)
            ),
            g12_solve_aggregate_acc_io(ProblemAll,
                handle_solution(File),
                SolnInfo0, SolnInfo, !IO)
        )
      )
    then
        SolnInfo = soln_info(_SolnCount, Errs),
        (
            Errs = [],
            io.write_string(File, "eval finished", !IO)
        ;
            Errs = [_ | _]
        )

    catch_any Other ->
        throw(Other)
    ),
    (
        MaybeOutputFile = yes(_),
        io.close_output(File, !IO)
    ;
        MaybeOutputFile = no
    ),
    Warns = [].

:- type soln_info
    --->    soln_info(
                soln_count :: int,
                soln_errors :: zinc_errors
            ).

:- pred handle_solution_with_limit(io.text_output_stream::in,
    int::in, assertion_ref(soln_info)::in, search_info::in, problem_kind::in,
    output_or_errors::in, bool::out, io::di, io::uo) is det.

handle_solution_with_limit(_File, _NumSolnLimit, _SolnInfoRef,
        _SearchInfo, _ProblemKind, _SolnOrErrors, _Continue, !IO).

:- pred handle_solution(io.text_output_stream::in,
    output_or_errors::in, soln_info::in, soln_info::out, io::di, io::uo) is det.

handle_solution(_File, _SolnOrErrors, !SolnInfo, !IO).

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

:- type solutions_opt
    --->    first_solution
    ;       some_solutions(int)
    ;       all_solutions.

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

:- pred new_assertion_ref(T, assertion_ref(T), io, io).
:- mode new_assertion_ref(in, out, di, uo) is det.

new_assertion_ref(V, assertion_ref(V), !IO).

:- pred query(assertion_ref(T), T, io, io).
:- mode query(in, out, di, uo) is det.

query(assertion_ref(V), V, !IO).

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

:- type terminator_signal ---> terminator_signal.

:- pred init_terminator_signal(terminator_signal, io, io).
:- mode init_terminator_signal(out, di, uo) is det.

init_terminator_signal(terminator_signal, !IO).

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

:- pred create_search_info(string, string, terminator_signal,
    search_info, io, io).
:- mode create_search_info(in, in, in, out, di, uo) is det.

create_search_info(_, _, _, search_info, !IO).

:- pred add_search_warning(search_info, search_warning_type, string, ss, ss).
:- mode add_search_warning(in, in, in, mdi, muo) is det.

add_search_warning(_, _, _, !SS).

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

:- type solve(T)            == pred(T, ss, ss).
:- inst solve_det           == (pred(out, mdi, muo) is det).
:- inst solve_semidet       == (pred(out, mdi, muo) is semidet).
:- inst solve_multi         == (pred(out, mdi, muo) is multi).
:- inst solve_nondet        == (pred(out, mdi, muo) is nondet).
:- inst solve_erroneous     == (pred(out, mdi, muo) is erroneous).

:- pred g12_solve_first(solve(T), maybe(T), io, io).
:- mode g12_solve_first(in(solve_semidet), out, di, uo) is cc_multi.
:- mode g12_solve_first(in(solve_nondet), out, di, uo) is cc_multi.

:- pred g12_solve_all(solve(T)::in(solve_nondet), list(T)::out,
    io::di, io::uo) is det.

:- pred g12_solve_aggregate_io(solve(T), pred(T, io, io), io, io).
:- mode g12_solve_aggregate_io(in(solve_nondet),
    in(pred(in, di, uo) is det), di, uo) is cc_multi.
:- mode g12_solve_aggregate_io(in(solve_nondet),
    in(pred(in, di, uo) is cc_multi), di, uo) is cc_multi.

:- pred g12_solve_aggregate_acc_io(solve(T), pred(T, U, U, io, io), U, U,
    io, io).
:- mode g12_solve_aggregate_acc_io(in(solve_nondet),
    in(pred(in, in, out, di, uo) is det), in, out, di, uo) is cc_multi.
:- mode g12_solve_aggregate_acc_io(in(solve_nondet),
    in(pred(in, in, out, di, uo) is cc_multi), in, out, di, uo) is cc_multi.

:- pred g12_do_while_io(solve(T), pred(T, bool, io, io), io, io).
:- mode g12_do_while_io(in(solve_nondet),
    in(pred(in, out, di, uo) is det), di, uo) is cc_multi.
:- mode g12_do_while_io(in(solve_nondet),
    in(pred(in, out, di, uo) is cc_multi), di, uo) is cc_multi.

%-----------------------------------------------------------------------------%
:- end_module zinc_rt_driver.
%-----------------------------------------------------------------------------%