[m-rev.] for post-commit review: improve pretty_printer speed by a lot

[Peter Wang]

On Tue, 30 Aug 2022 13:35:36 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> +output_indent_stack(Stream, IndentStack, !IO) :-
> +    (
> +        IndentStack = indent_empty
> +    ;
> +        IndentStack = indent_user(PrevStack, IndentStr, _NumCPs),
> +        output_indent_stack(Stream, PrevStack, !IO),
> +        stream.put(Stream, IndentStr, !IO)
> +    ;
> +        IndentStack = indent_std(PrevStack, IndentLevels, _NumCPs),
> +        output_indent_stack(Stream, PrevStack, !IO),
> +        output_std_indent_levels(Stream, IndentLevels, !IO)
> +    ).
> +
> +:- pred output_std_indent_levels(Stream::in, int::in,
> +    State::di, State::uo) is det <= stream.writer(Stream, string, State).
> +:- pragma type_spec(pred(output_std_indent_levels/4),
> +    (Stream = io.output_stream, State = io.state)).
> +
> +output_std_indent_levels(Stream, NumLevels, !IO) :-
> +    % We try to amortize the overhead of stream.put over as large a part
> +    % of the overall indentation as we can.
> +    ( if NumLevels >= 30 then

Both work, but I think NumLevels > 30 is clearer.

> +        ( if std_indent(30, IndentStr) then
> +            stream.put(Stream, IndentStr, !IO),
> +            output_std_indent_levels(Stream, NumLevels - 30, !IO)
> +        else
> +            unexpected($pred, "std_indent failed 30+")
> +        )
> +    else if NumLevels > 0 then
> +        ( if std_indent(NumLevels, IndentStr) then
> +            stream.put(Stream, IndentStr, !IO)
> +        else
> +            unexpected($pred, "std_indent failed <30")
> +        )
> +    else
> +        true
> +    ).

> @@ -1055,6 +1130,104 @@ decrement_func_limit(triangular(N), triangular(N - 1)).
>  %---------------------------------------------------------------------------%
>  %---------------------------------------------------------------------------%
>  
> +:- type indent_stack
> +    --->    indent_empty
> +            % No indent at all. Number of code points is zero.
> +    ;       indent_user(
> +                % The indentation after which this indentation is added.
> +                user_prevstack          :: indent_stack,
> +
> +                % Indentation added by a non-standard indent() function.
> +                user_indent_string      :: string,
> +
> +                % The total number of code points in user_prevstack and
> +                % user_extra_indent. Must be the sum of

user_indent_string

> +                % count_indent_codepoints(user_prevstack) and
> +                % string.count_codepoints(user_indent_string).
> +                user_total_code_points  :: int
> +            )
> +    ;       indent_std(
> +                % The indentation after which this indentation is added.
> +                std_prevstack           :: indent_stack,
> +
> +                % The number of extra standard indent levels added
> +                % after std_prevstack. Each indent level consists of two
> +                % spaces.
> +                std_extra_indent_levels :: int,
> +
> +                % The total number of code points in user_prevstack and
> +                % user_extra_indent. Must be the sum of
> +                % count_indent_codepoints(user_prevstack) and
> +                % 2 * std_extra_indent_levels.

std_prevstack and std_extra_indent_levels

> +                std_total_code_points   :: int
> +            ).

Peter