mercury/compiler/simplify_goal_ite.m

%----------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%----------------------------------------------------------------------------%
% Copyright (C) 2014-2022, 2024-2025 The Mercury team.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%----------------------------------------------------------------------------%
%
% File: simplify_goal_ite.m.
%
% This module handles simplification of if-then-else goals and negations.
% (A negation is just like an if-then-else with `fail' as the then-part
% and `true' as the else-part).
%
%----------------------------------------------------------------------------%

:- module check_hlds.simplify.simplify_goal_ite.
:- interface.

:- import_module check_hlds.simplify.common.
:- import_module check_hlds.simplify.simplify_info.
:- import_module hlds.
:- import_module hlds.hlds_goal.
:- import_module hlds.instmap.

    % Handle simplifications of if-then-else goals.
    %
:- pred simplify_goal_ite(
    hlds_goal_expr::in(goal_expr_ite), hlds_goal_expr::out,
    hlds_goal_info::in, hlds_goal_info::out,
    simplify_nested_context::in, instmap::in,
    common_info::in, common_info::out,
    simplify_info::in, simplify_info::out) is det.

    % Handle simplifications of negations.
    %
:- pred simplify_goal_neg(
    hlds_goal_expr::in(goal_expr_neg), hlds_goal_expr::out,
    hlds_goal_info::in, hlds_goal_info::out,
    simplify_nested_context::in, instmap::in,
    common_info::in, common_info::out,
    simplify_info::in, simplify_info::out) is det.

:- implementation.

:- import_module check_hlds.simplify.simplify_goal.
:- import_module hlds.goal_refs.
:- import_module hlds.goal_util.
:- import_module hlds.hlds_data.
:- import_module hlds.hlds_module.
:- import_module hlds.make_goal.
:- import_module hlds.type_util.
:- import_module libs.
:- import_module libs.options.
:- import_module parse_tree.
:- import_module parse_tree.error_spec.
:- import_module parse_tree.prog_data.
:- import_module parse_tree.prog_detism.
:- import_module parse_tree.var_table.

:- import_module bool.
:- import_module list.
:- import_module maybe.
:- import_module one_or_more.
:- import_module require.
:- import_module set.

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

simplify_goal_ite(GoalExpr0, GoalExpr, GoalInfo0, GoalInfo,
        NestedContext0, InstMap0, Common0, Common, !Info) :-
    % (if A then B else C) is logically equivalent to (A, B ; ~A, C).
    % If the determinism of A means that one of these disjuncts cannot succeed,
    % then we replace the if-then-else with the other disjunct. (We could
    % also eliminate A, but we leave that to the recursive invocations.)
    %
    % Note however that rerunning determinism analysis, which we do
    % at the end of simplification, may introduce more occurrences of these;
    % since we don't iterate simplification and determinism analysis until
    % a fixpoint is reached, we don't guarantee to eliminate all such
    % if-then-elses. Hence the code generator must be prepared to handle
    % the case when the condition of an if-then-else has determinism
    % `det' or `failure'.
    %
    % The conjunction operator in the remaining disjunct ought to be
    % a sequential conjunction, because Mercury's if-then-else always
    % guarantees sequentiality, whereas conjunction only guarantees
    % sequentiality if the --no-reorder-conj option is enabled.
    %
    % However, currently reordering is only done in mode analysis,
    % not in the code generator, so we don't yet need a sequential
    % conjunction construct. This will change when constraint pushing
    % is finished, or when we start doing coroutining.

    GoalExpr0 = if_then_else(Vars, Cond0, Then0, Else0),
    Cond0 = hlds_goal(_, CondInfo0),
    CondDetism0 = goal_info_get_determinism(CondInfo0),
    determinism_components(CondDetism0, CondCanFail0, CondSolns0),
    (
        CondCanFail0 = cannot_fail,
        goal_to_conj_list(Cond0, CondGoals),
        goal_to_conj_list(Then0, ThenGoals),
        Goals = CondGoals ++ ThenGoals,
        simplify_goal(hlds_goal(conj(plain_conj, Goals), GoalInfo0),
            hlds_goal(GoalExpr, GoalInfo), NestedContext0, InstMap0,
            Common0, Common, !Info),
        maybe_warn_about_condition(GoalInfo0, NestedContext0, "cannot fail",
            !Info),

        simplify_info_get_deleted_call_callees(!.Info, DeletedCallCallees0),
        SubGoalCalledProcs = goal_proc_refs(Else0),
        set.union(SubGoalCalledProcs,
            DeletedCallCallees0, DeletedCallCallees),
        simplify_info_set_deleted_call_callees(DeletedCallCallees, !Info)
    ;
        CondCanFail0 = can_fail,
        (
            CondSolns0 = at_most_zero,
            % Optimize away the condition and the `then' part.
            det_negation_det(CondDetism0, MaybeNegDetism),
            ( if
                Cond0 = hlds_goal(negation(NegCond), _),
                % XXX BUG! This optimization is only safe if it preserves mode
                % correctness, which means in particular that the negated goal
                % must not clobber any variables. For now I've just disabled
                % the optimization.
                semidet_fail
            then
                Cond = NegCond
            else
                ( if
                    MaybeNegDetism = yes(NegDetism1),
                    (
                        NegDetism1 = detism_erroneous,
                        instmap_delta_init_unreachable(NegInstMapDelta1)
                    ;
                        NegDetism1 = detism_det,
                        instmap_delta_init_reachable(NegInstMapDelta1)
                    )
                then
                    NegDetism = NegDetism1,
                    NegInstMapDelta = NegInstMapDelta1
                else
                    unexpected($pred, "cannot get negated determinism")
                ),
                goal_info_set_determinism(NegDetism, CondInfo0, NegCondInfo0),
                goal_info_set_instmap_delta(NegInstMapDelta,
                    NegCondInfo0, NegCondInfo),
                Cond = hlds_goal(negation(Cond0), NegCondInfo)
            ),
            goal_to_conj_list(Else0, ElseList),
            List = [Cond | ElseList],
            simplify_goal(hlds_goal(conj(plain_conj, List), GoalInfo0),
                hlds_goal(GoalExpr, GoalInfo), NestedContext0, InstMap0,
                Common0, Common, !Info),
            maybe_warn_about_condition(GoalInfo0, NestedContext0,
                "cannot succeed", !Info),

            simplify_info_get_deleted_call_callees(!.Info,
                DeletedCallCallees0),
            SubGoalCalledProcs = goal_proc_refs(Then0),
            set.union(SubGoalCalledProcs,
                DeletedCallCallees0, DeletedCallCallees),
            simplify_info_set_deleted_call_callees(DeletedCallCallees, !Info)
        ;
            ( CondSolns0 = at_most_one
            ; CondSolns0 = at_most_many
            ; CondSolns0 = at_most_many_cc
            ),
            ( if Else0 = hlds_goal(disj([]), _) then
                % (if Cond then Then else fail) is equivalent to (Cond, Then)
                goal_to_conj_list(Cond0, CondGoals),
                goal_to_conj_list(Then0, ThenGoals),
                Goals = CondGoals ++ ThenGoals,
                simplify_goal(hlds_goal(conj(plain_conj, Goals), GoalInfo0),
                    hlds_goal(GoalExpr, GoalInfo), NestedContext0, InstMap0,
                    Common0, Common, !Info),
                simplify_info_set_rerun_quant_instmap_delta(!Info),
                simplify_info_set_rerun_det(!Info)
            else
                simplify_goal_ordinary_ite(Vars, Cond0, Then0, Else0, GoalExpr,
                    GoalInfo0, GoalInfo, NestedContext0, InstMap0,
                    Common0, Common, !Info)
            )
        )
    ).

:- pred maybe_warn_about_condition(hlds_goal_info::in,
    simplify_nested_context::in, string::in,
    simplify_info::in, simplify_info::out) is det.

maybe_warn_about_condition(GoalInfo0, NestedContext0, Problem, !Info) :-
    InsideDuplForSwitch = NestedContext0 ^ snc_inside_dupl_for_switch,
    ( if
        simplify_do_warn_dodgy_simple_code(!.Info),
        % If InsideDuplForSwitch = yes, then not generate the warning,
        % because it is quite likely to be spurious: though the condition
        % cannot fail/succeed in this arm of the switch, it likely can
        % fail/succeed in other arms that derive from the exact same piece
        % of source code.
        InsideDuplForSwitch = no
    then
        Context = goal_info_get_context(GoalInfo0),
        Pieces = [words("Warning: the condition of this if-then-else")] ++
            color_as_incorrect([words(Problem), suffix(".")]) ++ [nl],
        Spec = spec($pred, severity_warning(warn_dodgy_simple_code),
            phase_simplify(report_only_if_in_all_modes), Context, Pieces),
        simplify_info_add_message(Spec, !Info)
    else
        true
    ),
    simplify_info_set_rerun_quant_instmap_delta(!Info),
    simplify_info_set_rerun_det(!Info).

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

:- pred simplify_goal_ordinary_ite(list(prog_var)::in,
    hlds_goal::in, hlds_goal::in, hlds_goal::in, hlds_goal_expr::out,
    hlds_goal_info::in, hlds_goal_info::out,
    simplify_nested_context::in, instmap::in,
    common_info::in, common_info::out,
    simplify_info::in, simplify_info::out) is det.

simplify_goal_ordinary_ite(Vars, Cond0, Then0, Else0, GoalExpr,
        GoalInfo0, GoalInfo, NestedContext0, InstMap0, Common0, Common,
        !Info) :-
    % Recursively simplify the sub-goals, and rebuild the resulting
    % if-then-else.

    simplify_goal(Cond0, Cond, NestedContext0, InstMap0,
        Common0, AfterCondCommon, !Info),
    apply_goal_instmap_delta(Cond, InstMap0, AfterCondInstMap0),
    simplify_goal(Then0, Then, NestedContext0, AfterCondInstMap0,
        AfterCondCommon, _AfterThenCommon, !Info),

    simplify_goal(Else0, Else, NestedContext0, InstMap0,
        Common0, _AfterElseCommon, !Info),

    Cond = hlds_goal(_, CondInfo),
    CondDelta = goal_info_get_instmap_delta(CondInfo),
    Then = hlds_goal(_, ThenInfo),
    ThenDelta = goal_info_get_instmap_delta(ThenInfo),
    instmap_delta_apply_instmap_delta(CondDelta, ThenDelta, test_size,
        CondThenDelta),
    Else = hlds_goal(_, ElseInfo),
    ElseDelta = goal_info_get_instmap_delta(ElseInfo),
    NonLocals = goal_info_get_nonlocals(GoalInfo0),
    some [!ModuleInfo] (
        simplify_info_get_module_info(!.Info, !:ModuleInfo),
        simplify_info_get_var_table(!.Info, VarTable),
        merge_instmap_deltas(VarTable, NonLocals, InstMap0,
            [CondThenDelta, ElseDelta], NewDelta, !ModuleInfo),
        simplify_info_set_module_info(!.ModuleInfo, !Info)
    ),
    goal_info_set_instmap_delta(NewDelta, GoalInfo0, GoalInfo1),
    IfThenElseExpr = if_then_else(Vars, Cond, Then, Else),

    IfThenElseDetism0 = goal_info_get_determinism(GoalInfo0),
    determinism_components(IfThenElseDetism0, IfThenElseCanFail,
        IfThenElseNumSolns),

    CondDetism = goal_info_get_determinism(CondInfo),
    determinism_components(CondDetism, CondCanFail, CondSolns),
    ( if
        % Check again if we can apply one of the above simplifications
        % after having simplified the sub-goals (we need to do this
        % to ensure that the goal is fully simplified, to maintain the
        % invariants that the MLDS backend depends on).
        ( CondCanFail = cannot_fail
        ; CondSolns = at_most_zero
        ; Else = hlds_goal(disj([]), _)
        )
    then
        simplify_goal_expr(IfThenElseExpr, GoalExpr, GoalInfo1, GoalInfo,
            NestedContext0, InstMap0, Common0, Common, !Info)
    else
        % Any structures generated in one branch won't be available after the
        % if-the-else as a whole if execution takes the other branch.
        Common = Common0,

        simplify_info_get_module_info(!.Info, ModuleInfo),
        warn_switch_for_ite_cond(ModuleInfo, VarTable, Cond,
            cond_can_switch_uncommitted, CanSwitch),
        (
            CanSwitch = cond_can_switch_on(SwitchVar),
            Context = goal_info_get_context(CondInfo),
            lookup_var_entry(VarTable, SwitchVar, SwitchVarEntry),
            SwitchVarName = SwitchVarEntry ^ vte_name,
            ( if SwitchVarName = "" then
                OnPieces = []
            else
                OnPieces = [words("on"), quote(SwitchVarName)]
            ),
            Pieces = [words("Warning: this if-then-else")] ++
                color_as_incorrect([words("could be replaced by a switch")] ++
                    OnPieces ++ [suffix(".")]) ++
                [nl],
            Severity = severity_warning(warn_ite_instead_of_switch),
            Spec = spec($pred, Severity, phase_simplify(report_in_any_mode),
                Context, Pieces),
            simplify_info_add_message(Spec, !Info)
        ;
            CanSwitch = cond_can_switch_uncommitted
        ;
            CanSwitch = cond_cannot_switch
        ),
        ( if
            % If-then-elses that are det or semidet may nevertheless contain
            % nondet or multi conditions. If this happens, we put the
            % if-then-else inside a commit scope, since the code generators
            % need to know where they should change the code's execution
            % mechanism.

            simplify_do_mark_code_model_changes(!.Info),
            CondSolns = at_most_many,
            IfThenElseNumSolns \= at_most_many
        then
            determinism_components(InnerDetism, IfThenElseCanFail,
                at_most_many),
            goal_info_set_determinism(InnerDetism, GoalInfo1, InnerInfo),
            GoalExpr = scope(commit(do_not_force_pruning),
                hlds_goal(IfThenElseExpr, InnerInfo))
        else
            GoalExpr = IfThenElseExpr
        ),
        GoalInfo = GoalInfo1
    ).

:- type cond_can_switch
    --->    cond_can_switch_uncommitted
    ;       cond_can_switch_on(prog_var)
    ;       cond_cannot_switch.

:- pred warn_switch_for_ite_cond(module_info::in, var_table::in, hlds_goal::in,
    cond_can_switch::in, cond_can_switch::out) is det.

warn_switch_for_ite_cond(ModuleInfo, VarTable, Cond, !CondCanSwitch) :-
    Cond = hlds_goal(CondExpr, _CondInfo),
    (
        CondExpr = unify(_LHSVar, _RHS, _Mode, Unification, _UContext),
        (
            ( Unification = construct(_, _, _, _, _, _, _)
            ; Unification = assign(_, _)
            ; Unification = simple_test(_, _)
            ),
            !:CondCanSwitch = cond_cannot_switch
        ;
            Unification = deconstruct(LHSVar, _ConsId, _Args, _ArgModes,
                _CanFail, _CanCGC),
            lookup_var_type(VarTable, LHSVar, LHSVarType),
            ( if type_to_type_defn_body(ModuleInfo, LHSVarType, TypeBody) then
                CanSwitchOnType = can_switch_on_type(TypeBody),
                (
                    CanSwitchOnType = no,
                    !:CondCanSwitch = cond_cannot_switch
                ;
                    CanSwitchOnType = yes,
                    (
                        !.CondCanSwitch = cond_can_switch_uncommitted,
                        !:CondCanSwitch = cond_can_switch_on(LHSVar)
                    ;
                        !.CondCanSwitch = cond_can_switch_on(SwitchVar),
                        ( if SwitchVar = LHSVar then
                            true
                        else
                            !:CondCanSwitch = cond_cannot_switch
                        )
                    ;
                        !.CondCanSwitch = cond_cannot_switch
                    )
                )
            else
                % You cannot have a switch on a type with no body (e.g. a
                % builtin type such as int).
                !:CondCanSwitch = cond_cannot_switch
            )
        ;
            Unification = complicated_unify(_, _, _),
            unexpected($pred, "complicated unify")
        )
    ;
        CondExpr = disj(Disjuncts),
        list.foldl(warn_switch_for_ite_cond(ModuleInfo, VarTable), Disjuncts,
            !CondCanSwitch)
    ;
        CondExpr = negation(SubGoal),
        (
            !.CondCanSwitch = cond_can_switch_uncommitted,
            warn_switch_for_ite_cond(ModuleInfo, VarTable, SubGoal,
                !CondCanSwitch)
        ;
            !.CondCanSwitch = cond_can_switch_on(_),
            % The condition cannot do both.
            !:CondCanSwitch = cond_cannot_switch
        ;
            !.CondCanSwitch = cond_cannot_switch
        )
    ;
        ( CondExpr = plain_call(_, _, _, _, _, _)
        ; CondExpr = generic_call(_, _, _, _, _)
        ; CondExpr = call_foreign_proc(_, _, _, _, _, _, _)
        ; CondExpr = conj(_, _)
        ; CondExpr = switch(_, _, _)
        ; CondExpr = scope(_, _)
        ; CondExpr = if_then_else(_, _, _, _)
        ),
        !:CondCanSwitch = cond_cannot_switch
    ;
        CondExpr = shorthand(ShortHand),
        (
            ShortHand = atomic_goal(_, _, _, _, _, _, _),
            !:CondCanSwitch = cond_cannot_switch
        ;
            ShortHand = try_goal(_, _, _),
            !:CondCanSwitch = cond_cannot_switch
        ;
            ShortHand = bi_implication(_, _),
            unexpected($pred, "shorthand")
        )
    ).

:- func can_switch_on_type(hlds_type_body) = bool.

can_switch_on_type(TypeBody) = CanSwitchOnType :-
    (
        TypeBody = hlds_du_type(TypeBodyDu),
        TypeBodyDu = type_body_du(Ctors, _AlphaSortedCtors, _MaybeSuperType,
            _MaybeUserEq, _MaybeRepn, _MaybeForeignType),
        % We don't care about _MaybeUserEq, since the unification with *any*
        % functor of the type indicates that we are deconstructing the physical
        % representation, not the logical value.
        %
        % We don't care about _MaybeRepn, since that contains only
        % implementation details (which may be of interest when a code
        % generator decides *how* to implement the switch, but which cannot
        % affected *whether* we can implement the switch).
        %
        % We don't care about _MaybeForeignType, since the unification with
        % *any* functor of the type means that either there is no foreign type
        % version, or we are using the Mercury version of the type.
        %
        % We *do* care that the type has at least two constructors.
        ( if Ctors = one_or_more(_, [_ | _]) then
            CanSwitchOnType = yes
        else
            CanSwitchOnType = no
        )
    ;
        TypeBody = hlds_eqv_type(_),
        % The type of the variable should have had any equivalences expanded
        % out of it before simplify.
        unexpected($pred, "eqv type")
    ;
        TypeBody = hlds_foreign_type(_),
        % If the type is foreign, how can a Mercury unification use it?
        unexpected($pred, "foreign type")
    ;
        TypeBody = hlds_abstract_type(_),
        % If the type is abstract, how can a Mercury unification use it?
        unexpected($pred, "abstract type")
    ;
        TypeBody = hlds_solver_type(_),
        % Any unifications on constrained variables should be done on the
        % representation type, and the type of the variable in the unification
        % should be the representation type, not the solver type.
        unexpected($pred, "solver type")
    ).

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

simplify_goal_neg(GoalExpr0, GoalExpr, GoalInfo0, GoalInfo,
        NestedContext0, InstMap0, Common0, Common, !Info) :-
    GoalExpr0 = negation(SubGoal0),
    % Can't use calls or unifications seen within a negation,
    % since non-local variables may not be bound within the negation.
    simplify_goal(SubGoal0, SubGoal1, NestedContext0, InstMap0,
        Common0, _Common1, !Info),
    Context = goal_info_get_context(GoalInfo0),
    InsideDuplForSwitch = NestedContext0 ^ snc_inside_dupl_for_switch,
    ( if
        simplify_do_warn_dodgy_simple_code(!.Info),
        % We don't want to generate either of the warnings below for code
        % that has been duplicated for a switch, since the warned-about
        % condition may not (and typically does not) exist in the other copies.
        InsideDuplForSwitch = no
    then
        SubGoal1 = hlds_goal(_, SubGoalInfo1),
        Detism = goal_info_get_determinism(SubGoalInfo1),
        determinism_components(Detism, CanFail, MaxSoln),
        ( if CanFail = cannot_fail then
            Pieces = [words("Warning: the negated goal")] ++
                color_as_incorrect([words("cannot fail.")]) ++
                [nl],
            Spec = spec($pred, severity_warning(warn_dodgy_simple_code),
                phase_simplify(report_only_if_in_all_modes), Context, Pieces),
            simplify_info_add_message(Spec, !Info)
        else if MaxSoln = at_most_zero then
            Pieces = [words("Warning: the negated goal")] ++
                color_as_incorrect([words("cannot succeed.")]) ++
                [nl],
            Spec = spec($pred, severity_warning(warn_dodgy_simple_code),
                phase_simplify(report_only_if_in_all_modes), Context, Pieces),
            simplify_info_add_message(Spec, !Info)
        else
            true
        )
    else
        true
    ),
    ( if
        % Replace `not true' with `fail'.
        SubGoal1 = hlds_goal(conj(plain_conj, []), _)
    then
        hlds_goal(GoalExpr, GoalInfo) = fail_goal_with_context(Context)
    else if
        % Replace `not fail' with `true'.
        SubGoal1 = hlds_goal(disj([]), _)
    then
        hlds_goal(GoalExpr, GoalInfo) = true_goal_with_context(Context)
    else if
        % Remove double negation.
        SubGoal1 =
            hlds_goal(negation(hlds_goal(SubSubGoal, SubSubGoalInfo)), _),
        % XXX BUG! This optimization is only safe if it preserves
        % mode correctness, which means in particular that the
        % the negated goal must not clobber any variables.
        % For now I've just disabled the optimization.
        semidet_fail
    then
        simplify_maybe_wrap_goal(GoalInfo0, SubSubGoalInfo, SubSubGoal,
            GoalExpr, GoalInfo, !Info)
    else
        GoalExpr = negation(SubGoal1),
        GoalInfo = GoalInfo0
    ),
    % Execution continues after the negation scope iff the goal inside the
    % scope failed. In general, we don't know when it failed, so we cannot
    % depend on it having created any structures.
    Common = Common0.

%---------------------------------------------------------------------------%
:- end_module check_hlds.simplify.simplify_goal_ite.
%---------------------------------------------------------------------------%