%-----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%-----------------------------------------------------------------------------%
% Copyright (C) 1997-1998, 2003-2008, 2010-2011 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: term_pass2.m.
% Main author of original version: crs.
% Main author of this version: zs.
%
% This file contains the code that tries to prove that procedures terminate.
% For details, please refer to the papers mentioned in termination.m.
%
%-----------------------------------------------------------------------------%

:- module transform_hlds.term_pass2.
:- interface.

:- import_module hlds.
:- import_module hlds.hlds_module.
:- import_module hlds.hlds_pred.
:- import_module transform_hlds.term_util.

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

    % NOTE: This code assumes that the SCC does not call any nonterminating
    % procedures. If it does then, that fact should have been detected
    % during pass 1.
    %
:- pred prove_termination_in_scc(module_info::in, pass_info::in,
    scc::in, int::in, termination_info::out) is det.

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

:- implementation.

:- import_module check_hlds.
:- import_module check_hlds.mode_test.
:- import_module hlds.goal_util.
:- import_module parse_tree.
:- import_module parse_tree.prog_data.
:- import_module parse_tree.prog_data_pragma.
:- import_module transform_hlds.term_errors.
:- import_module transform_hlds.term_traversal.

:- import_module assoc_list.
:- import_module bag.
:- import_module bool.
:- import_module int.
:- import_module list.
:- import_module map.
:- import_module maybe.
:- import_module pair.
:- import_module require.
:- import_module set.
:- import_module term.
:- import_module unit.

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

:- type term_pass2_result
    --->    term_pass2_ok(
                call_weight_info,
                used_args
            )
    ;       term_pass2_error(
                list(term_error)
            ).

:- type call_weight_info
    --->    call_weight_info(list(term_error), call_weight_graph).

:- type call_weight_graph == map(pred_proc_id, call_weight_dst_map).
:- type call_weight_dst_map == map(pred_proc_id, call_weight_edge).

    % The maximum non-infinite weight from proc to proc,
    % and what context it occurs at.
    %
:- type call_weight_edge
    --->    call_weight_edge(int, prog_context).

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

prove_termination_in_scc(ModuleInfo, PassInfo, SCC, SingleArgs, Termination) :-
    set.to_sorted_list(SCC, SCCProcs),
    init_rec_input_suppliers(SCCProcs, ModuleInfo, InitRecSuppliers),
    prove_termination_in_scc_trial(ModuleInfo, PassInfo, down, SCCProcs,
        InitRecSuppliers, Termination0),
    (
        Termination0 = can_loop(Errors),
        ( if
            % On large SCCs, single arg analysis can require many iterations,
            % so we allow the user to limit the size of the SCCs we will try it
            % on.
            list.length(SCCProcs, ProcCount),
            ProcCount =< SingleArgs,

            % Don't try single arg analysis if it cannot cure the reason for
            % the failure of the main analysis.
            not (
                list.member(Error, Errors),
                Error = term_error(_, imported_pred)
            )
        then
            prove_termination_in_scc_single_arg(ModuleInfo, SCCProcs, PassInfo,
                SingleArgTerminates),
            (
                SingleArgTerminates = yes,
                Termination = cannot_loop(unit)
            ;
                SingleArgTerminates = no,
                Termination = Termination0
            )
        else
            Termination = Termination0
        )
    ;
        Termination0 = cannot_loop(unit),
        Termination = Termination0
    ).

    % Initialise the set of recursive input suppliers to be the set of all
    % input variables in all procedures of the SCC.
    %
:- pred init_rec_input_suppliers(list(pred_proc_id)::in, module_info::in,
    used_args::out) is det.

init_rec_input_suppliers([], _, InitMap) :-
    map.init(InitMap).
init_rec_input_suppliers([PPId | PPIds], ModuleInfo, RecSupplierMap) :-
    init_rec_input_suppliers(PPIds, ModuleInfo, RecSupplierMap0),
    module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
    proc_info_get_headvars(ProcInfo, HeadVars),
    proc_info_get_argmodes(ProcInfo, ArgModes),
    partition_call_args(ModuleInfo, ArgModes, HeadVars, InArgs, _OutVars),
    MapIsInput =
        ( pred(HeadVar::in, Bool::out) is det :-
            ( if bag.contains(InArgs, HeadVar) then
                Bool = yes
            else
                Bool = no
            )
        ),
    list.map(MapIsInput, HeadVars, BoolList),
    map.det_insert(PPId, BoolList, RecSupplierMap0, RecSupplierMap).

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

    % Perform single arg analysis on the SCC.
    %
    % We pick one procedure in the SCC (one of those with minimal arity).
    % We set the recursive input suppliers of this procedure to contain only
    % the first input argument, and the recursive input suppliers of the other
    % procedures to the empty set, and try a fixpoint iteration. If it works,
    % great, if not, try again with the next input arg of the selected
    % procedure, until we run out of input arguments of that procedure.
    %
    % While the fixpoint iteration in the main algorithm looks for the greatest
    % fixpoint, in which the recursive input supplier sets cannot increase, in
    % single arg analysis we are looking for a smallest fixpoint starting from
    % a given location, so we must make sure that the recursive input supplier
    % sets cannot decrease.
    %
:- pred prove_termination_in_scc_single_arg(module_info::in,
    list(pred_proc_id)::in, pass_info::in, bool::out) is det.

prove_termination_in_scc_single_arg(ModuleInfo, SCC, PassInfo, Terminates) :-
    (
        SCC = [FirstPPId | LaterPPIds],
        FirstArity = lookup_proc_arity(ModuleInfo, FirstPPId),
        find_min_arity_proc(ModuleInfo, LaterPPIds, FirstPPId, FirstArity,
            TrialPPId, RestSCC),
        prove_termination_in_scc_single_arg_2(ModuleInfo, PassInfo,
            TrialPPId, RestSCC, 1, Terminates)
    ;
        SCC = [],
        unexpected($pred, "empty SCC")
    ).

    % Find a procedure of minimum arity among the given list and the tentative
    % guess.
    %
:- pred find_min_arity_proc(module_info::in, list(pred_proc_id)::in,
    pred_proc_id::in, arity::in, pred_proc_id::out,
    list(pred_proc_id)::out) is det.

find_min_arity_proc(_, [], BestSofarPPId, _, BestSofarPPId, []).
find_min_arity_proc(ModuleInfo, [PPId | PPIds], BestSofarPPId, BestSofarArity,
        BestPPId, RestSCC) :-
    Arity = lookup_proc_arity(ModuleInfo, PPId),
    ( if Arity < BestSofarArity then
        find_min_arity_proc(ModuleInfo, PPIds, PPId, Arity, BestPPId,
            RestSCC0),
        RestSCC = [BestSofarPPId | RestSCC0]
    else
        find_min_arity_proc(ModuleInfo, PPIds, BestSofarPPId, BestSofarArity,
            BestPPId, RestSCC0),
        RestSCC = [PPId | RestSCC0]
    ).

    % Perform single arg analysis on the SCC.
    %
:- pred prove_termination_in_scc_single_arg_2(module_info::in, pass_info::in,
    pred_proc_id::in, list(pred_proc_id)::in, int::in, bool::out) is det.

prove_termination_in_scc_single_arg_2(ModuleInfo, PassInfo,
        TrialPPId, RestSCC, ArgNum0, Terminates) :-
    ( if
        init_rec_input_suppliers_single_arg(ModuleInfo, TrialPPId, RestSCC,
            ArgNum0, InitRecSuppliers)
    then
        prove_termination_in_scc_trial(ModuleInfo, PassInfo, up,
            [TrialPPId | RestSCC], InitRecSuppliers, Termination),
        (
            Termination = cannot_loop(unit),
            Terminates = yes
        ;
            Termination = can_loop(_),
            prove_termination_in_scc_single_arg_2(ModuleInfo, PassInfo,
                TrialPPId, RestSCC, ArgNum0 + 1, Terminates)
        )
    else
        Terminates = no
    ).

:- pred init_rec_input_suppliers_single_arg(module_info::in, pred_proc_id::in,
    list(pred_proc_id)::in, int::in, used_args::out) is semidet.

init_rec_input_suppliers_single_arg(ModuleInfo, TrialPPId, RestSCC, ArgNum,
        RecSupplierMap) :-
    module_info_pred_proc_info(ModuleInfo, TrialPPId, _, ProcInfo),
    proc_info_get_argmodes(ProcInfo, ArgModes),
    init_rec_input_suppliers_add_single_arg(ModuleInfo, ArgModes, ArgNum,
        TrialPPIdRecSuppliers),
    RecSupplierMap0 = map.singleton(TrialPPId, TrialPPIdRecSuppliers),
    init_rec_input_suppliers_single_arg_others(ModuleInfo, RestSCC,
        RecSupplierMap0, RecSupplierMap).

:- pred init_rec_input_suppliers_add_single_arg(module_info::in,
    list(mer_mode)::in, int::in, list(bool)::out) is semidet.

init_rec_input_suppliers_add_single_arg(ModuleInfo, [Mode | Modes], ArgNum,
        BoolList) :-
    ( if
        mode_is_input(ModuleInfo, Mode),
        ArgNum = 1
    then
        list.map(map_to_no, Modes, BoolListTail),
        BoolList = [yes | BoolListTail]
    else if
        ( if
            mode_is_output(ModuleInfo, Mode)
        then
            NextArgNum = ArgNum
        else if
            mode_is_input(ModuleInfo, Mode),
            ArgNum > 1
        then
            NextArgNum = ArgNum - 1
        else
            fail
        )
    then
        init_rec_input_suppliers_add_single_arg(ModuleInfo, Modes, NextArgNum,
            BoolListTail),
        BoolList = [no | BoolListTail]
    else
        fail
    ).

:- pred init_rec_input_suppliers_single_arg_others(module_info::in,
    list(pred_proc_id)::in, used_args::in, used_args::out) is det.

init_rec_input_suppliers_single_arg_others(_, [], !RecSupplierMap).
init_rec_input_suppliers_single_arg_others(ModuleInfo, [PPId | PPIds],
        !RecSupplierMap) :-
    module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
    proc_info_get_headvars(ProcInfo, HeadVars),
    list.map(map_to_no, HeadVars, BoolList),
    map.det_insert(PPId, BoolList, !RecSupplierMap),
    init_rec_input_suppliers_single_arg_others(ModuleInfo, PPIds,
        !RecSupplierMap).

:- func lookup_proc_arity(module_info, pred_proc_id) = arity.

lookup_proc_arity(ModuleInfo, PPId) = Arity :-
    module_info_pred_proc_info(ModuleInfo, PPId, _, ProcInfo),
    proc_info_get_headvars(ProcInfo, HeadVars),
    list.length(HeadVars, Arity).

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

:- type fixpoint_dir
    --->    up
    ;       down.

:- pred prove_termination_in_scc_trial(module_info::in, pass_info::in,
    fixpoint_dir::in, list(pred_proc_id)::in, used_args::in,
    termination_info::out) is det.

prove_termination_in_scc_trial(ModuleInfo, PassInfo, FixDir,
        SCC, InitRecSuppliers, Termination) :-
    prove_termination_in_scc_fixpoint(ModuleInfo, PassInfo, FixDir,
        SCC, InitRecSuppliers, Result),
    (
        Result = term_pass2_ok(CallInfo, _),
        CallInfo = call_weight_info(InfCalls, CallWeights),
        (
            InfCalls = [_ | _],
            PassInfo = pass_info(_, MaxErrors, _),
            list.take_upto(MaxErrors, InfCalls, ReportedInfCalls),
            Termination = can_loop(ReportedInfCalls)
        ;
            InfCalls = [],
            zero_or_positive_weight_cycles(ModuleInfo, CallWeights, Cycles),
            (
                Cycles = [],
                Termination = cannot_loop(unit)
            ;
                Cycles = [_ | _],
                PassInfo = pass_info(_, MaxErrors, _),
                list.take_upto(MaxErrors, Cycles, ReportedCycles),
                Termination = can_loop(ReportedCycles)
            )
        )
    ;
        Result = term_pass2_error(Errors),
        Termination = can_loop(Errors)
    ).

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

:- pred prove_termination_in_scc_fixpoint(module_info::in,
    pass_info::in, fixpoint_dir::in, list(pred_proc_id)::in, used_args::in,
    term_pass2_result::out) is det.

prove_termination_in_scc_fixpoint(ModuleInfo, PassInfo, FixDir,
        SCC, RecSupplierMap0, Result) :-
    map.init(NewRecSupplierMap0),
    map.init(CallWeightGraph0),
    CallInfo0 = call_weight_info([], CallWeightGraph0),
    prove_termination_in_scc_pass(ModuleInfo, PassInfo, FixDir,
        SCC, RecSupplierMap0, NewRecSupplierMap0, CallInfo0, Result1),
    (
        Result1 = term_pass2_ok(_, RecSupplierMap1),
        ( if RecSupplierMap1 = RecSupplierMap0 then
            % We are at a fixed point, so further analysis
            % will not get any better results.
            Result = Result1
        else
            prove_termination_in_scc_fixpoint(ModuleInfo, PassInfo, FixDir,
                SCC, RecSupplierMap1, Result)
        )
    ;
        Result1 = term_pass2_error(_),
        Result = Result1
    ).

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

    % Process a whole SCC, to determine the termination property of each
    % procedure in that SCC.
    %
:- pred prove_termination_in_scc_pass(module_info::in, pass_info::in,
    fixpoint_dir::in, list(pred_proc_id)::in, used_args::in, used_args::in,
    call_weight_info::in, term_pass2_result::out) is det.

prove_termination_in_scc_pass(_, _, _, [], _, NewRecSupplierMap, CallInfo,
        term_pass2_ok(CallInfo, NewRecSupplierMap)).
prove_termination_in_scc_pass(ModuleInfo, PassInfo, FixDir, [PPId | PPIds],
        RecSupplierMap, NewRecSupplierMap0, CallInfo0, Result) :-
    module_info_pred_proc_info(ModuleInfo, PPId, PredInfo, ProcInfo),
    pred_info_get_context(PredInfo, Context),
    proc_info_get_goal(ProcInfo, Goal0),
    % The pretest code we add for compiler-generated unification and comparison
    % predicates uses type casts. It uses them in a way that is guaranteed
    % to terminate, but our analysis is not (yet) able to find this out for
    % itself. We therefore analyse only the non-pretest parts of such goals.
    Goal = maybe_strip_equality_pretest(Goal0),
    proc_info_get_var_table(ProcInfo, VarTable),
    map.init(EmptyMap),
    PassInfo = pass_info(FunctorInfo, MaxErrors, MaxPaths),
    init_term_traversal_params(FunctorInfo, PPId, Context, VarTable,
        EmptyMap, RecSupplierMap, MaxErrors, MaxPaths, Params),
    set.init(PathSet0),
    Info0 = term_traversal_ok(PathSet0, []),
    term_traverse_goal(ModuleInfo, Params, Goal, Info0, Info),
    (
        Info = term_traversal_ok(Paths, CanLoop),
        expect(unify(CanLoop, []), $pred,
            "can_loop detected in pass2 but not pass1"),
        set.to_sorted_list(Paths, PathList),
        upper_bound_active_vars(PathList, ActiveVars),
        map.lookup(RecSupplierMap, PPId, RecSuppliers0),
        proc_info_get_headvars(ProcInfo, Args),
        bag.init(EmptyBag),
        update_rec_input_suppliers(Args, ActiveVars, FixDir,
            RecSuppliers0, RecSuppliers, EmptyBag, RecSuppliers0Bag),
        map.det_insert(PPId, RecSuppliers,
            NewRecSupplierMap0, NewRecSupplierMap1),
        add_call_arcs(PathList, RecSuppliers0Bag, CallInfo0, CallInfo1),
        prove_termination_in_scc_pass(ModuleInfo, PassInfo, FixDir,
            PPIds, RecSupplierMap, NewRecSupplierMap1, CallInfo1, Result)
    ;
        Info = term_traversal_error(Errors, CanLoop),
        expect(unify(CanLoop, []), $pred,
            "can_loop detected in pass2 but not pass1"),
        Result = term_pass2_error(Errors)
    ).

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

:- pred update_rec_input_suppliers(list(prog_var)::in, bag(prog_var)::in,
    fixpoint_dir::in, list(bool)::in, list(bool)::out,
    bag(prog_var)::in, bag(prog_var)::out) is det.

update_rec_input_suppliers([], _, _, [], [], !RecBag).
update_rec_input_suppliers([_ | _], _, _, [], [], _, _) :-
    unexpected($pred, "unmatched variables").
update_rec_input_suppliers([], _, _, [_ | _], [], _, _) :-
    unexpected($pred, "unmatched variables").
update_rec_input_suppliers([Arg | Args], ActiveVars, FixDir,
        [RecInputSupplier0 | RecInputSuppliers0],
        [RecInputSupplier | RecInputSuppliers], !RecBag) :-
    (
        RecInputSupplier0 = yes,
        bag.insert(Arg, !RecBag)
    ;
        RecInputSupplier0 = no
    ),
    (
        FixDir = down,
        % This guarantees that the set of rec input suppliers
        % can only decrease.
        ( if bag.contains(ActiveVars, Arg) then
            RecInputSupplier = RecInputSupplier0
        else
            RecInputSupplier = no
        )
    ;
        FixDir = up,
        % This guarantees that the set of rec input suppliers
        % can only increase.
        ( if bag.contains(ActiveVars, Arg) then
            RecInputSupplier = yes
        else
            RecInputSupplier = RecInputSupplier0
        )
    ),
    update_rec_input_suppliers(Args, ActiveVars, FixDir,
        RecInputSuppliers0, RecInputSuppliers, !RecBag).

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

    % This adds the information from a stage 2 traversal to the graph.
    % The graph's nodes are the procedures in the current SCC. The graph's
    % edges represent calls from one procedure in the SCC to another.
    % The number attached to the edge from p to q shows the upper bound
    % on the difference between the size of the recursive input supplier
    % arguments in the call to q and the size of the recursive input supplier
    % arguments in the head of p. If there is no finite upper bound, then
    % we insert the details of the call into the list of "infinite" calls.
    %
:- pred add_call_arcs(list(term_path_info)::in, bag(prog_var)::in,
    call_weight_info::in, call_weight_info::out) is det.

add_call_arcs([], _RecInputSuppliers, !CallInfo).
add_call_arcs([Path | Paths], RecInputSuppliers, !CallInfo) :-
    Path = term_path_info(PPId, CallSite, GammaConst, GammaVars, ActiveVars),
    (
        CallSite = yes(CallPPIdPrime - ContextPrime),
        CallPPId = CallPPIdPrime,
        Context = ContextPrime
    ;
        CallSite = no,
        unexpected($pred, "no call site in path in stage 2")
    ),
    (
        GammaVars = []
    ;
        GammaVars = [_ | _],
        unexpected($pred, "gamma variables in path in stage 2")
    ),
    !.CallInfo = call_weight_info(InfCalls0, CallWeights0),
    ( if bag.is_subbag(ActiveVars, RecInputSuppliers) then
        ( if map.search(CallWeights0, PPId, NeighbourMap0) then
            ( if map.search(NeighbourMap0, CallPPId, OldEdgeInfo) then
                OldEdgeInfo = call_weight_edge(OldWeight, _OldContext),
                ( if OldWeight >= GammaConst then
                    EdgeInfo = OldEdgeInfo
                else
                    EdgeInfo = call_weight_edge(GammaConst, Context)
                ),
                map.det_update(CallPPId, EdgeInfo, NeighbourMap0, NeighbourMap)
            else
                EdgeInfo = call_weight_edge(GammaConst, Context),
                map.det_insert(CallPPId, EdgeInfo, NeighbourMap0, NeighbourMap)
            ),
            map.det_update(PPId, NeighbourMap, CallWeights0, CallWeights1)
        else
            EdgeInfo = call_weight_edge(GammaConst, Context),
            NeighbourMap = map.singleton(CallPPId, EdgeInfo),
            map.det_insert(PPId, NeighbourMap, CallWeights0, CallWeights1)
        ),
        !:CallInfo = call_weight_info(InfCalls0, CallWeights1)
    else
        InfCall = term_error(Context, inf_call(PPId, CallPPId)),
        InfCalls1 = [InfCall | InfCalls0],
        !:CallInfo = call_weight_info(InfCalls1, CallWeights0)
    ),
    add_call_arcs(Paths, RecInputSuppliers, !CallInfo).

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

    % We use a simple depth first search to find and return the list of all
    % cycles in the call graph of the SCC where the change in the size of the
    % recursive input supplier arguments of the procedure that serves as the
    % start and end point of the circularity are not guaranteed to decrease.
    %
    % Finding one such cycle is enough for us to conclude that we cannot prove
    % termination of the procedures in the SCC. We nevertheless collect
    % all cycles, because it may be useful to print them out (if not all,
    % then maybe a limited set).
    %
:- pred zero_or_positive_weight_cycles(module_info::in, call_weight_graph::in,
    list(term_error)::out) is det.

zero_or_positive_weight_cycles(ModuleInfo, CallWeights, Cycles) :-
    map.to_assoc_list(CallWeights, PPIdsNeighboursMaps),
    zero_or_positive_weight_cycles_from_ppids(ModuleInfo, CallWeights,
        PPIdsNeighboursMaps, Cycles).

:- pred zero_or_positive_weight_cycles_from_ppids(module_info::in,
    call_weight_graph::in, assoc_list(pred_proc_id, call_weight_dst_map)::in,
    list(term_error)::out) is det.

zero_or_positive_weight_cycles_from_ppids(_, _, [], []).
zero_or_positive_weight_cycles_from_ppids(ModuleInfo, CallWeights,
        [PPIdNeighboursMap | PPIdsNeighboursMaps], Cycles) :-
    zero_or_positive_weight_cycles_from_ppid(ModuleInfo, CallWeights,
        PPIdNeighboursMap, CyclesHead),
    zero_or_positive_weight_cycles_from_ppids(ModuleInfo, CallWeights,
        PPIdsNeighboursMaps, CyclesTail),
    Cycles = CyclesHead ++ CyclesTail.

:- pred zero_or_positive_weight_cycles_from_ppid(module_info::in,
    call_weight_graph::in, pair(pred_proc_id, call_weight_dst_map)::in,
    list(term_error)::out) is det.

zero_or_positive_weight_cycles_from_ppid(ModuleInfo, CallWeights,
        PPId - NeighboursMap, Cycles) :-
    map.to_assoc_list(NeighboursMap, NeighboursList),
    PPId = proc(PredId, _ProcId),
    module_info_pred_info(ModuleInfo, PredId, PredInfo),
    pred_info_get_context(PredInfo, Context),
    zero_or_positive_weight_cycles_from_neighbours(CallWeights, PPId,
        Context, 0, NeighboursList, [], Cycles).

:- pred zero_or_positive_weight_cycles_from_neighbours(call_weight_graph::in,
    pred_proc_id::in, prog_context::in, int::in,
    assoc_list(pred_proc_id, call_weight_edge)::in,
    assoc_list(pred_proc_id, prog_context)::in, list(term_error)::out) is det.

zero_or_positive_weight_cycles_from_neighbours(_, _, _, _, [], _, []).
zero_or_positive_weight_cycles_from_neighbours(CallWeights,
        LookforPPId, Context, WeightSoFar,
        [Neighbour | Neighbours], RevVisitedCalls, Cycles) :-
    zero_or_positive_weight_cycles_from_neighbour(CallWeights, LookforPPId,
        Context, WeightSoFar, Neighbour, RevVisitedCalls, CyclesHead),
    zero_or_positive_weight_cycles_from_neighbours(CallWeights, LookforPPId,
        Context, WeightSoFar, Neighbours, RevVisitedCalls, CyclesTail),
    Cycles = CyclesHead ++ CyclesTail.

:- pred zero_or_positive_weight_cycles_from_neighbour(call_weight_graph::in,
    pred_proc_id::in, prog_context::in, int::in,
    pair(pred_proc_id, call_weight_edge)::in,
    assoc_list(pred_proc_id, prog_context)::in, list(term_error)::out) is det.

zero_or_positive_weight_cycles_from_neighbour(CallWeights,
        LookforPPId, ProcContext, WeightSoFar0,
        CurPPId - call_weight_edge(EdgeWeight, Context),
        RevVisitedCalls0, Cycles) :-
    WeightSoFar1 = WeightSoFar0 + EdgeWeight,
    ( if CurPPId = LookforPPId then
        % We have a cycle on the looked for ppid.
        ( if WeightSoFar1 >= 0 then
            RevVisitedCalls = [CurPPId - Context | RevVisitedCalls0],
            list.reverse(RevVisitedCalls, VisitedCalls),
            CycleError = cycle(LookforPPId, VisitedCalls),
            CycleErrorContext = term_error(ProcContext, CycleError),
            Cycles = [CycleErrorContext]
        else
            Cycles = []
        )
    else if assoc_list.search(RevVisitedCalls0, CurPPId, _) then
        % We have a cycle, but not on the looked-for pred_proc_id. We ignore
        % it here; it will be picked up when we process that pred_proc_id.
        Cycles = []
    else
        % No cycle; try all possible edges from this node.
        RevVisitedCalls1 = [CurPPId - Context | RevVisitedCalls0],
        ( if map.search(CallWeights, CurPPId, NeighboursMap) then
            map.to_assoc_list(NeighboursMap, NeighboursList),
            zero_or_positive_weight_cycles_from_neighbours(CallWeights,
                LookforPPId, ProcContext, WeightSoFar1,
                NeighboursList, RevVisitedCalls1, Cycles)
        else
            % In some cases, it is possible for a pred_proc_id to have no
            % entry in CallWeights. This happens e.g. in pretty_printer.m.
            % The array_to_doc_loop function is in an SCC together with
            % the function created from the lambda expression in the
            % argument of format_susp. The lambda function calls
            % array_to_doc_loop, but, while array_to_doc_loop *refers*
            % to the lambda function (which is why they are in the same SCC),
            % it does not *call* the lambda function. And since it cannot call
            % any other procedure in the SCC (there being no others),
            % it will not have an entry in CallWeights.
            Cycles = []
        )
    ).

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

:- pred map_to_no(T::in, bool::out) is det.

map_to_no(_, no).

%-----------------------------------------------------------------------------%
:- end_module transform_hlds.term_pass2.
%-----------------------------------------------------------------------------%
