string_eqc.erl

-module(string_eqc).
-compile([export_all,nowarn_export_all]).
-include_lib("eqc/include/eqc.hrl").

%%%
%%% Test most new functions in the new string module (PR #1330).
%%%


flat_chardata() ->
    oneof([charlist(),unicode_binary()]).

nfd_chardata() ->
    ?LET(L, chardata(), decompose_chardata(L)).

chardata() ->
    oneof([charlist(),deep_charlist(),unicode_binary()]).

charlist() ->
    list(character()).

deep_charlist() ->
    ?SIZED(Size, deep_charlist(Size)).

deep_charlist(0) ->
    charlist();
deep_charlist(N) ->
    list(frequency([{5,character()},
                    {4,charlist()},
                    {1,?LAZY(deep_charlist(N-1))},
                    {4,unicode_binary()}])).

unicode_binary() ->
    ?LET(L, charlist(), unicode:characters_to_binary(L)).

character() ->
    frequency([{1,choose(0, 255)},
               {2,choose(256, 16#D800-1)},
               {1,choose(16#E000, 16#10FFFF)}]).

primitive_character() ->
    frequency([{1,choose($!, $~)},
               {1,choose(16#C0, 16#FF)},
               {1,choose(16#388, 16#3FF)},
               {1,choose(16#400, 16#45F)}]).

primitive_charlist() ->
    list(primitive_character()).

separators(Sep) ->
    Gen = elements(Sep),
    frequency([{4,vector(1, Gen)},
               {2,vector(2, Gen)},
               {1,vector(3, Gen)}]).

disjoint_separator(S) ->
    ?SUCHTHAT(Sep, primitive_character(), not lists:member(Sep, S)).

mixed_guidance() ->
    frequency([{8,{list,?SIZED(Size, mixed_guidance(Size))}},
               {1,list},
               {1,binary}]).

mixed_guidance(0) ->
    leaf_type();
mixed_guidance(N) ->
    frequency([{3,?SHRINK({split,oneof([1,2,3]),
                           ?LAZY({mixed_guidance(N-1),
                                  mixed_guidance(N-1)})}, [list])},
               {1,?SHRINK(?LAZY({list,mixed_guidance(N-1)}),[list])},
               {5,list},
               {3,?SHRINK(binary, [list])}]).

make_mixed(binary, []) ->
    <<>>;
make_mixed(binary, S) ->
    unicode:characters_to_binary(S);
make_mixed(list, S) ->
    S;
make_mixed({list,G}, S) ->
    [make_mixed(G, S)];
make_mixed({split,Mul,{MixLeft,MixRight}}, S) ->
    {Left,Right} = lists:split(length(S)*Mul div 4, S),
    [make_mixed(MixLeft, Left)|make_mixed(MixRight, Right)].

%%%
%%% Test lexemes/2.
%%%

string_and_separator() ->
    ?LET(S0, non_empty(primitive_charlist()),
         frequency([
                    {1,{S0,[],[S0]}},
                    {4,?LAZY(nonmatching_separators(S0))},
                    {18,?LAZY(nonempty_separators(S0))}])).

positions(String) ->
    ?LET(Ps, list(choose(0, length(String))),
         lists:reverse(lists:usort(Ps))).

nonempty_separators(S0) ->
    ?LET({SepSet,Ps}, {resize(5, non_empty(list(disjoint_separator(S0)))),
                       positions(S0)},
         ?LET(Seps, vector(length(Ps), separators(SepSet)),
              begin
                  S = insert_separators(Ps, S0, Seps),
                  Res = result(Ps, S0, []),
                  {S,SepSet,Res}
              end)).

nonmatching_separators(S) ->
    ?LET(SepSet, non_empty(list(disjoint_separator(S))),
         {S,SepSet,[S]}).

insert_separators([P|Ps], S0, [Sep|Seps]) ->
    {A,B} = lists:split(P, S0),
    S = A ++ Sep ++ B,
    insert_separators(Ps, S, Seps);
insert_separators([], S, _Seps) ->
    S.

result([P|Ps], S0, Acc) ->
    case lists:split(P, S0) of
        {A,[]} ->
            result(Ps, A, Acc);
        {A,[_|_]=B} ->
            result(Ps, A, [B|Acc])
    end;
result([], [_|_]=S, Acc) ->
    [S|Acc];
result([], [], Acc) ->
    Acc.

leaf_type() ->
    frequency([{5,list},{3,?SHRINK(binary, [list])}]).


prop_lexemes() ->
    ?FORALL({{S,Sep,Res0},Guidance}, {string_and_separator(),mixed_guidance()},
            conjunction(
              [{flat,
                ?LAZY(Res0 =:= string:lexemes(S, Sep))},
               {flat_decomposed,
                ?LAZY(decompose_list(Res0) =:=
                          string:lexemes(decompose(S), decompose_list(Sep)))},
               {binary,
                ?LAZY(begin
                          Bin = unicode:characters_to_binary(S),
                          Res = [unicode:characters_to_binary(E) || E <- Res0],
                          Res =:= string:lexemes(Bin, Sep)
                      end)},
               {mixed,
                ?LAZY(begin
                          Mixed = [make_mixed(Guidance, S)],
                          are_all_equal(string:lexemes(Mixed, Sep), Res0)
                      end)},
               {mixed_decomposed,
                ?LAZY(
                   begin
                       SepDecomposed = decompose_list(Sep),
                       SDecomposed = unicode:characters_to_nfd_list(S),
                       MixedDecomposed = [make_mixed(Guidance, SDecomposed)],
                       ResDecomposed = decompose_list(Res0),
                       ?WHENFAIL(io:format("string:lexemes(~p, ~p) -> ~p\n",
                                           [MixedDecomposed,
                                            SepDecomposed,
                                            ResDecomposed]),
                                 are_all_equal(string:lexemes(MixedDecomposed,
                                                              SepDecomposed),
                                               ResDecomposed))
                   end
                   )}
              ])).

prop_nth_lexeme() ->
    ?FORALL({{S,Sep,Res},Guidance}, {string_and_separator(),mixed_guidance()},
            ?FORALL(N, choose(1, length(Res)),
                    begin
                        Lexeme = lists:nth(N, Res),
                        conjunction(
                          [{flat,
                            ?LAZY(Lexeme =:= string:nth_lexeme(S, N, Sep))},
                           {binary,
                            ?LAZY(
                               begin
                                   Bin = unicode:characters_to_binary(S),
                                   BinLexeme = unicode:characters_to_binary(Lexeme),
                                   BinLexeme =:= string:nth_lexeme(Bin, N, Sep)
                               end)},
                           {mixed,
                            ?LAZY(
                               begin
                                   Mixed = make_mixed(Guidance, S),
                                   ?WHENFAIL(io:format("~p\n", [Mixed]),
                                             string:equal(Lexeme, string:nth_lexeme(Mixed, N, Sep)))
                            end)}
                          ])
                    end)).

decompose(L) ->
    unicode:characters_to_nfd_list(L).

decompose_list(whitespace=Ws) ->
    Ws;
decompose_list(L) ->
    [case unicode:characters_to_nfd_list([C]) of
         [C] -> C;
         Other -> Other
     end || C <- L].

are_all_equal([H1|T1], [H2|T2]) ->
    string:equal(H1, H2) andalso are_all_equal(T1, T2);
are_all_equal([], []) ->
    true;
are_all_equal(_, _) ->
    false.

%%%
%%% Test take().
%%%

take_string() ->
    ?LET(Middle, non_empty(primitive_charlist()),
         ?LET(SepSet, non_empty(list(disjoint_separator(Middle))),
              ?LET(SepPart, list(elements(SepSet)),
                   {SepPart,Middle,SepSet}))).

prop_take() ->
    ?FORALL({Data,G}, {take_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                FlatEq = fun erlang:'=:='/2,
                BinaryEq = fun(Bin, Str) ->
                                   Bin =:= unicode:characters_to_binary(Str)
                           end,
                MixedEq = fun string:equal/2,
                conjunction([
                             {flat,?LAZY(do_prop_take(Data, Id, FlatEq))},
                             {binary,?LAZY(do_prop_take(Data, ToBin, BinaryEq))},
                             {mixed,?LAZY(do_prop_take(Data, ToMixed, MixedEq))}
                            ])
            end).

do_prop_take({SepPart,Middle,_SepSet}=Data, Transform, Eq) ->
    EmptySepData = {[],SepPart++Middle,[]},
    conjunction([
                 {nonempty_separator,?LAZY(do_prop_take_0(Data, Transform, Eq))},
                 {empty_separator,?LAZY(do_prop_take_0(EmptySepData, Transform, Eq))}
                ]).

do_prop_take_0({SepPart0,Middle0,SepSet0}=Data, Transform, Eq) ->
    SepPart = unicode:characters_to_nfd_list(SepPart0),
    Middle = unicode:characters_to_nfd_list(Middle0),
    SepSet = decompose_list(SepSet0),
    DecomposedData = {SepPart,Middle,SepSet},
    conjunction([{nfc,?LAZY(do_prop_take_1(Data, Transform, Eq))},
                 {nfd,?LAZY(do_prop_take_1(DecomposedData, Transform, Eq))}]).

do_prop_take_1({SepPart,Middle,SepSet}, Transform, Eq) ->
    Leading = Transform(SepPart ++ Middle),
    Trailing = Transform(Middle ++ SepPart),
    conjunction([
                 {leading,
                  ?WHENFAIL(io:format("string:take(~tp, ~tp) -> {~tp,~tp}\n",
                                      [Leading,SepSet,SepPart,Middle]),
                            begin
                                {La,Lb} = string:take(Leading, SepSet),
                                Eq(La, SepPart) andalso Eq(Lb, Middle)
                            end)},
                 {trailing,
                  ?WHENFAIL(io:format("string:take(~tp, ~tp, false, trailing) ->"
                                      " {~tp,~tp}\n",
                                      [Trailing,SepSet,SepPart,Middle]),
                            begin
                                {Ta,Tb} = string:take(Trailing, SepSet, false, trailing),
                                Eq(Ta, Middle) andalso Eq(Tb, SepPart)
                            end)},
                {leading_complement,
                 ?WHENFAIL(io:format("string:take(~tp, ~tp, true) -> {~tp,~tp}\n",
                                     [Leading,SepSet,SepPart,Middle]),
                            begin
                                {LCa,LCb} = string:take(Trailing, SepSet, true),
                                Eq(LCa, Middle) andalso Eq(LCb, SepPart)
                            end)},
                {trailing_complement,
                 ?WHENFAIL(io:format("string:take(~tp, ~tp, true, trailing) ->"
                                     " {~tp,~tp}\n",
                                     [Leading,SepSet,SepPart,Middle]),
                            begin
                                {TCa,TCb} = string:take(Leading, SepSet, true, trailing),
                                Eq(TCa, SepPart) andalso Eq(TCb, Middle)
                            end)}
                ]).

%%%
%%% Test trim().
%%%

trim_string() ->
    ?LET(Middle, non_empty(primitive_charlist()),
         ?LET(SepSet, non_empty(list(disjoint_separator(Middle))),
              ?LET(SepPart, list(elements(SepSet)),
                   {SepPart,Middle,SepSet}))).

prop_trim() ->
    ?FORALL({Data,G}, {trim_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                FlatEq = fun erlang:'=:='/2,
                BinaryEq = fun(Bin, Str) ->
                                   Bin =:= unicode:characters_to_binary(Str)
                           end,
                MixedEq = fun string:equal/2,
                conjunction([
                             {flat,?LAZY(do_prop_trim(Data, Id, FlatEq))},
                             {binary,?LAZY(do_prop_trim(Data, ToBin, BinaryEq))},
                             {mixed,?LAZY(do_prop_trim(Data, ToMixed, MixedEq))}
                            ])
            end).

do_prop_trim({SepPart,Middle,_SepSet}=Data, Transform, Eq) ->
    EmptySepData = {[],SepPart++Middle,[]},
    WsData = ws_data(Data),
    conjunction([
                 {nonempty_separator,?LAZY(do_prop_trim_0(Data, Transform, Eq))},
                 {empty_separator,?LAZY(do_prop_trim_0(EmptySepData, Transform, Eq))},
                 {ws_separator,?LAZY(do_prop_trim_0(WsData, Transform, Eq))}
                ]).

ws_data({SepPart0,Middle,SepSet}) ->
    Ws = "\r\n\s\t\r\n\r\n\s\t",
    Map = map_ws(SepSet, Ws, Ws, #{}),
    SepPart = [maps:get(C, Map) || C <- SepPart0],
    {SepPart,Middle,whitespace}.

map_ws([H|T], [W|Ws], MoreWs, Map) ->
    map_ws(T, Ws, MoreWs, Map#{H=>W});
map_ws([_|_]=Seps, [], MoreWs, Map) ->
    map_ws(Seps, MoreWs, MoreWs, Map);
map_ws([], _, _, Map) ->
    Map.

do_prop_trim_0({SepPart0,Middle0,SepSet0}=Data, Transform, Eq) ->
    SepPart = unicode:characters_to_nfd_list(SepPart0),
    Middle = unicode:characters_to_nfd_list(Middle0),
    SepSet = decompose_list(SepSet0),
    DecomposedData = {SepPart,Middle,SepSet},
    conjunction([{nfc,?LAZY(do_prop_trim_1(Data, Transform, Eq))},
                 {nfd,?LAZY(do_prop_trim_1(DecomposedData, Transform, Eq))}]).

do_prop_trim_1({SepPart,Middle,SepSet}, Transform, Eq) ->
    Leading = Transform(SepPart ++ Middle),
    Trailing = Transform(Middle ++ SepPart),
    Both = Transform(SepPart ++ Middle ++ SepPart),
    IsCorrect = fun(Result) -> Eq(Result, Middle) end,
    conjunction([
                 {leading,
                  ?LAZY(apply_trim(Leading, leading, SepSet, IsCorrect))},
                 {trailingv,
                  ?LAZY(apply_trim(Trailing, trailing, SepSet, IsCorrect))},
                 {leading,
                  ?LAZY(apply_trim(Both, both, SepSet, IsCorrect))}]).

apply_trim(S, both, whitespace, IsCorrect) ->
    ?WHENFAIL(io:format("string:trim(~tp)\n", [S]),
              IsCorrect(string:trim(S)));
apply_trim(S, Direction, whitespace, IsCorrect) ->
    ?WHENFAIL(io:format("string:trim(~tp, ~tp)\n", [S,Direction]),
              IsCorrect(string:trim(S, Direction)));
apply_trim(S, Direction, Separators, IsCorrect) ->
    ?WHENFAIL(io:format("string:trim(~tp, ~tp, ~tp)\n", [S,Direction,Separators]),
              IsCorrect(string:trim(S, Direction, Separators))).

%%%
%%% Test split().
%%%

split_string() ->
    ?LET(S0, primitive_charlist(),
         ?LET({Sep,Positions}, {non_empty(list(disjoint_separator(S0))),
                                non_empty(positions(S0))},
              begin
                  S = split_insert_separators(Positions, S0, Sep),
                  Res = split_result(Positions, S0, []),
                  {S,Sep,Res}
              end)).

split_insert_separators([P|Ps], S0, Sep) ->
    {A,B} = lists:split(P, S0),
    S = A ++ Sep ++ B,
    split_insert_separators(Ps, S, Sep);
split_insert_separators([], S, _Sep) ->
    S.

split_result([P|Ps], S, Acc) ->
    {A,B} = lists:split(P, S),
    split_result(Ps, A, [B|Acc]);
split_result([], S, Acc) ->
    [S|Acc].

prop_split() ->
    ?FORALL({Data,G}, {split_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                FlatEq = fun erlang:'=:='/2,
                BinaryEq = fun(Bin, Str) ->
                                   Bin =:= unicode:characters_to_binary(Str)
                           end,
                MixedEq = fun string:equal/2,
                conjunction([
                             {flat,?LAZY(do_prop_split(Data, Id, FlatEq))},
                             {binary,?LAZY(do_prop_split(Data, ToBin, BinaryEq))},
                             {mixed,?LAZY(do_prop_split(Data, ToMixed, MixedEq))}
                            ])
            end).

do_prop_split({S0,Sep0,Res0}=Data, Transform, Eq) ->
    S = unicode:characters_to_nfd_list(S0),
    Sep = decompose_list(Sep0),
    Res = decompose_list(Res0),
    DecomposedData = {S,Sep,Res},
    conjunction([{nfc,?LAZY(do_prop_split_1(Data, Transform, Eq))},
                 {nfd,?LAZY(do_prop_split_1(DecomposedData, Transform, Eq))}]).


do_prop_split_1({S0,Sep,Res}, Transform, Eq) ->
    S = Transform(S0),
    LeadingTrailing =
        case Res of
            [_,_,_|_] ->
                [H|T] = Res,
                LeadingRes = [H,lists:flatten(lists:join(Sep, T))],
                Last = lists:last(Res),
                AllButLast = lists:droplast(Res),
                TrailingRes = [lists:flatten(lists:join(Sep, AllButLast)),Last],
                [{leading,?LAZY(apply_split(S, Sep, leading, LeadingRes, Eq))},
                 {trailing,?LAZY(apply_split(S, Sep, trailing, TrailingRes, Eq))}];
            _ ->
                []
        end,
    conjunction([{all,?LAZY(apply_split(S, Sep, all, Res, Eq))}|LeadingTrailing]).

apply_split(S, Sep, Direction, Res, Eq) ->
    ?WHENFAIL(io:format("string:split(~tp, ~tp, ~tp) ->\n ~p\n", [S,Sep,Direction,Res]),
              split_all_equal(string:split(S, Sep, Direction), Res, Eq)).

split_all_equal([H1|T1], [H2|T2], Eq) ->
    Eq(H1, H2) andalso split_all_equal(T1, T2, Eq);
split_all_equal([], [], _) ->
    true;
split_all_equal(_, _, _) ->
    false.

%%%
%%% Test replace().
%%%

replace_string() ->
    ?LET({S0,Repl}, {primitive_charlist(),primitive_charlist()},
         ?LET({Pat,Positions}, {non_empty(list(disjoint_separator(S0))),
                                non_empty(positions(S0))},
              begin
                  S = split_insert_separators(Positions, S0, Pat),
                  Res = split_result(Positions, S0, []),
                  {S,Pat,Repl,Res}
              end)).

prop_replace() ->
    ?FORALL({Data,G}, {replace_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                conjunction([
                             {flat,?LAZY(do_prop_replace(Data, Id))},
                             {binary,?LAZY(do_prop_replace(Data, ToBin))},
                             {mixed,?LAZY(do_prop_replace(Data, ToMixed))}
                            ])
            end).

do_prop_replace({S0,Pat0,Repl0,Res0}=Data, Transform) ->
    S = unicode:characters_to_nfd_list(S0),
    Repl = unicode:characters_to_nfd_list(Repl0),
    Pat = decompose_list(Pat0),
    Res = decompose_list(Res0),
    DecomposedData = {S,Pat,Repl,Res},
    conjunction([{nfc,?LAZY(do_prop_replace_1(Data, Transform))},
                 {nfd,?LAZY(do_prop_replace_1(DecomposedData, Transform))}]).


do_prop_replace_1({S0,Pat,Repl0,Res}, Transform) ->
    S = Transform(S0),
    Repl = Transform(Repl0),
    ResAll = lists:join(Repl0, Res),
    LeadingTrailing =
        case Res of
            [_,_,_|_] ->
                [H|T] = Res,
                LeadingRes = [H,Repl0,lists:join(Pat, T)],
                Last = lists:last(Res),
                AllButLast = lists:droplast(Res),
                TrailingRes = [lists:join(Pat, AllButLast),Repl0,Last],
                [{leading,?LAZY(apply_replace(S, Pat, Repl, leading, LeadingRes))},
                 {trailing,?LAZY(apply_replace(S, Pat, Repl, trailing, TrailingRes))}
                ];
            _ ->
                []
        end,
    conjunction([{all,?LAZY(apply_replace(S, Pat, Repl, all, ResAll))}|LeadingTrailing]).

apply_replace(S, Pat, Repl, Direction, Res) ->
    ?WHENFAIL(io:format("string:replace(~tp, ~tp, ~tp, ~tp) ->\n ~p\n",
                        [S,Pat,Repl,Direction,Res]),
              string:equal(string:replace(S, Pat, Repl, Direction), Res)).

%%%
%%% Test slice().
%%%

slice_string() ->
    ?LET(S, primitive_charlist(),
         begin
             L = length(S),
             ?LET(Pos, choose(0, L),
                  ?LET(Len, choose(0, L-Pos),
                       begin
                           Res = lists:sublist(S, Pos+1, Len),
                           {S,Pos,Len,Res}
                       end))
         end).

prop_slice() ->
    ?FORALL({Data,G}, {slice_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                FlatEq = fun erlang:'=:='/2,
                BinaryEq = fun(Bin, Str) ->
                                   Bin =:= unicode:characters_to_binary(Str)
                           end,
                MixedEq = fun string:equal/2,
                conjunction([
                             {flat,?LAZY(do_prop_slice(Data, Id, FlatEq))},
                             {binary,?LAZY(do_prop_slice(Data, ToBin, BinaryEq))},
                             {mixed,?LAZY(do_prop_slice(Data, ToMixed, MixedEq))}
                            ])
            end).

do_prop_slice({S0,Pos,Len,Res0}=Data, Transform, Eq) ->
    S = unicode:characters_to_nfd_list(S0),
    Res = unicode:characters_to_nfd_list(Res0),
    DecomposedData = {S,Pos,Len,Res},
    conjunction([
                 {nfc,?LAZY(do_prop_slice_1(Data, Transform, Eq))},
                 {nfd,?LAZY(do_prop_slice_1(DecomposedData, Transform, Eq))}
                ]).

do_prop_slice_1({S0,Pos,Len,Res}, Transform, Eq) ->
    S = Transform(S0),
    apply_slice(S, Pos, Len, Res, Eq).

apply_slice(S, Pos, Len, Res, Eq) ->
    ?WHENFAIL(io:format("string:slice(~tp, ~tp, ~tp)\n", [S,Pos,Len]),
              Eq(string:slice(S, Pos, Len), Res)).

%%%
%%% Test prefix().
%%%

prefix_string() ->
    ?LET(S, primitive_charlist(),
         ?LET(Other, non_empty(list(disjoint_separator(S))),
              {S,Other})).

prop_prefix() ->
    ?FORALL({Data,G}, {prefix_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                FlatEq = fun erlang:'=:='/2,
                BinaryEq = fun(Bin, Str) ->
                                   Bin =:= unicode:characters_to_binary(Str)
                           end,
                MixedEq = fun string:equal/2,
                conjunction([
                             {flat,?LAZY(do_prop_prefix(Data, Id, FlatEq))},
                             {binary,?LAZY(do_prop_prefix(Data, ToBin, BinaryEq))},
                             {mixed,?LAZY(do_prop_prefix(Data, ToMixed, MixedEq))}
                            ])
            end).

do_prop_prefix({S0,Other0}=Data, Transform, Eq) ->
    S = unicode:characters_to_nfd_list(S0),
    Other = unicode:characters_to_nfd_list(Other0),
    DecomposedData = {S,Other},
    conjunction([
                 {nfc,?LAZY(do_prop_prefix_1(Data, Transform, Eq))},
                 {nfd,?LAZY(do_prop_prefix_1(DecomposedData, Transform, Eq))}
                ]).

do_prop_prefix_1({S0,Other0}, Transform, Eq) ->
    S = Transform(S0),
    Other = Transform(Other0),
    Str = Transform(Other0 ++ S0),
    conjunction([
                 {match,?LAZY(apply_prefix(Str, Other, Eq, S))},
                 {nomatch,?LAZY(apply_prefix(S, Other, fun erlang:'=:='/2, nomatch))}
                ]).

apply_prefix(Str, Other, Eq, Res) ->
    ?WHENFAIL(io:format("string:prefix(~tp, ~tp)\n", [Str,Other]),
              Eq(string:prefix(Str, Other), Res)).

%%%
%%% Test find().
%%%

find_string() ->
    ?LET(S0, primitive_charlist(),
         ?LET({Pat,Pos}, {non_empty(list(disjoint_separator(S0))),
                          choose(0, length(S0))},
              {lists:split(Pos, S0),Pat})).

prop_find() ->
    ?FORALL({Data,G}, {find_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                FlatEq = fun erlang:'=:='/2,
                BinaryEq = fun(Bin, Str) ->
                                   Bin =:= unicode:characters_to_binary(Str)
                           end,
                MixedEq = fun string:equal/2,
                conjunction([
                             {flat,?LAZY(do_prop_find(Data, Id, FlatEq))},
                             {binary,?LAZY(do_prop_find(Data, ToBin, BinaryEq))},
                             {mixed,?LAZY(do_prop_find(Data, ToMixed, MixedEq))}
                            ])
            end).

do_prop_find({{L0,R0},Pat0}=Data, Transform, Eq) ->
    L = unicode:characters_to_nfd_list(L0),
    R = unicode:characters_to_nfd_list(R0),
    Pat = unicode:characters_to_nfd_list(Pat0),
    DecomposedData = {{L,R},Pat},
    conjunction([
                 {nfc,?LAZY(do_prop_find_1(Data, Transform, Eq))},
                 {nfd,?LAZY(do_prop_find_1(DecomposedData, Transform, Eq))}
                ]).

do_prop_find_1({{L,R},Pat0}, Transform, Eq) ->
    S1 = Transform(L ++ Pat0 ++ R),
    Pat = Transform(Pat0),
    conjunction([{leading1,
                  ?LAZY(apply_find(S1, Pat, leading, Eq, Pat0 ++ R))},
                 {leading2,
                  ?LAZY(begin
                            S = Transform(L ++ Pat0 ++ R ++ Pat0),
                            apply_find(S, Pat, leading, Eq, Pat0 ++ R ++ Pat0)
                        end)},
                 {trailing1,
                  ?LAZY(apply_find(S1, Pat, trailing, Eq, Pat0 ++ R))},
                 {trailing2,
                  ?LAZY(begin
                            S = Transform(Pat0 ++ L ++ Pat0 ++ R),
                            apply_find(S, Pat, trailing, Eq, Pat0 ++ R)
                        end)},
                 {leading_nomatch,
                  ?LAZY(begin
                            S = Transform(L ++ R),
                            apply_find(S, Pat, leading, fun erlang:'=:='/2, nomatch)
                        end)},
                 {trailing_nomatch,
                  ?LAZY(begin
                            S = Transform(L ++ R),
                            apply_find(S, Pat, trailing, fun erlang:'=:='/2, nomatch)
                        end)}
                ]).

apply_find(S, Pat, Dir, Eq, Res) ->
    ?WHENFAIL(io:format("string:find(~tp, ~tp, ~tp) -> ~p\n", [S,Pat,Dir,Res]),
              Eq(string:find(S, Pat, Dir), Res)).

%%%
%%% Test chomp().
%%%

chomp_string() ->
    MainPart = list(frequency([{10,primitive_character()},
                               {1,$\r},
                               {1,$\n},
                               {1,"\r\n"}])),
    Ending = list(oneof([$\r,$\n,"\r\n"])),
    ?LET(S0, [MainPart,Ending],
         begin
             S = lists:flatten(S0),
             Res = chomp_result(S),
             {S,Res}
         end).

chomp_result(S0) ->
    S1 = lists:reverse(S0),
    lists:reverse(chomp_result_1(S1)).

chomp_result_1([$\n,$\r|T]) ->
    chomp_result_1(T);
chomp_result_1([$\n|T]) ->
    chomp_result_1(T);
chomp_result_1(T) ->
    T.

prop_chomp() ->
    ?FORALL({Data,G}, {chomp_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                FlatEq = fun erlang:'=:='/2,
                BinaryEq = fun(Bin, Str) ->
                                   Bin =:= unicode:characters_to_binary(Str)
                           end,
                MixedEq = fun string:equal/2,
                conjunction([
                             {flat,?LAZY(do_prop_chomp(Data, Id, FlatEq))},
                             {binary,?LAZY(do_prop_chomp(Data, ToBin, BinaryEq))},
                             {mixed,?LAZY(do_prop_chomp(Data, ToMixed, MixedEq))}
                            ])
            end).

do_prop_chomp({S0,Res}, Transform, Eq) ->
    S = Transform(S0),
    ?WHENFAIL(io:format("string:chomp(~tp)\n", [S]),
              Eq(string:chomp(S), Res)).

%%%
%%% Test equal().
%%%


prop_equal() ->
    ?FORALL({Data,G}, {charlist(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                conjunction([
                             {flat,?LAZY(do_prop_equal(Data, Id))},
                             {binary,?LAZY(do_prop_equal(Data, ToBin))},
                             {mixed,?LAZY(do_prop_equal(Data, ToMixed))}
                            ])
            end).

do_prop_equal(S0, Transform) ->
    S = Transform(S0),
    conjunction([
                 {plain,?LAZY(apply_equal(S, S0, false, none))},
                 {casefold,
                  ?LAZY(begin
                            Casefolded = string:casefold(S0),
                            apply_equal(S, Casefolded, true, none)
                        end)},
                 {nfd,
                  ?LAZY(begin
                            Decomposed = unicode:characters_to_nfd_list(S0),
                            apply_equal(S, Decomposed, false, nfd)
                        end)}
                ]).

apply_equal(A, B, IgnoreCase, Norm) ->
    ?WHENFAIL(io:format("string:equal(~tp, ~tp, ~tp, ~tp)\n",
                        [A,B,IgnoreCase,Norm]),
              string:equal(A, B, IgnoreCase, Norm) andalso
              string:equal(B, A, IgnoreCase, Norm)).

%%%
%%% Test pad().
%%%

pad_string() ->
    {charlist(),nat()}.

prop_pad() ->
    ?FORALL({Data,G}, {pad_string(),mixed_guidance()},
            begin
                Id = fun(Id) -> Id end,
                ToBin = fun unicode:characters_to_binary/1,
                ToMixed = fun(S) -> make_mixed(G, S) end,
                conjunction([
                             {flat,?LAZY(do_prop_pad(Data, Id))},
                             {binary,?LAZY(do_prop_pad(Data, ToBin))},
                             {mixed,?LAZY(do_prop_pad(Data, ToMixed))}
                            ])
            end).

do_prop_pad(Data, Transform) ->
    conjunction([
                 {space,?LAZY(do_prop_pad_1(Data, Transform, $\s))},
                 {x,?LAZY(do_prop_pad_1(Data, Transform, $x))}]).

do_prop_pad_1({S0,PadLen}, Transform, PadChar) ->
    S = Transform(S0),
    StrLen = string:length(S0),
    Length = StrLen + PadLen,
    PadString = lists:duplicate(PadLen, PadChar),
    conjunction([
                 {trailing,
                  ?LAZY(begin
                            Res = S0 ++ PadString,
                            apply_pad(S, Length, trailing, PadChar, Res)
                        end)},
                 {leading,
                  ?LAZY(begin
                            Res = PadString ++ S0,
                            apply_pad(S, Length, leading, PadChar, Res)
                        end)},
                 {both,
                  ?LAZY(begin
                            LeftPadString = lists:duplicate(PadLen div 2, PadChar),
                            RightPadString = lists:duplicate(PadLen div 2 +
                                                                 PadLen rem 2,
                                                             PadChar),
                            Res = LeftPadString ++ S0 ++ RightPadString,
                            apply_pad(S, Length, both, PadChar, Res)
                        end)}
                 ]).

apply_pad(S, Length, Dir, Char, Res) ->
    ?WHENFAIL(io:format("string:pad(~tp, ~tp, ~tp, ~tp)\n",
                        [S,Length,Dir,Char]),
              string:equal(string:pad(S, Length, Dir, Char), Res)).

%%%
%%% Other properties.
%%%

prop_graphemes_length() ->
    ?FORALL(S, nfd_chardata(),
            begin
                Graphemes = string:to_graphemes(S),
                string:length(Graphemes) =:= string:length(S)
            end).

prop_graphemes() ->
    ?FORALL(S, nfd_chardata(),
            begin
                Graphemes = string:to_graphemes(S),
                get_graphemes(S) =:= Graphemes
            end).

prop_is_empty() ->
    ?FORALL(S, chardata(),
            begin
                Bin = if is_binary(S) -> S;
                         true -> unicode:characters_to_binary(S)
                      end,
                IsEmpty = Bin =:= <<>>,
                IsEmpty =:= string:is_empty(S)
            end).

prop_idempotent_casefold() ->
    idempotent(fun string:casefold/1).

prop_idempotent_lowercase() ->
    idempotent(fun string:lowercase/1).

prop_idempotent_titlecase() ->
    idempotent(fun string:titlecase/1).

prop_idempotent_uppercase() ->
    idempotent(fun string:uppercase/1).

prop_deep_casefold() ->
    deep(casefold).

prop_deep_lowercase() ->
    deep(lowercase).

prop_deep_titlecase() ->
    deep(titlecase).

prop_deep_uppercase() ->
    deep(uppercase).

prop_next_codepoint() ->
    ?FORALL(S0, chardata(),
            begin
                S = do_prop_next_codepoint(S0),
                string:equal(S0, S)
            end).

do_prop_next_codepoint(S) ->
    case string:next_codepoint(S) of
        [C|T] ->
            [C|do_prop_next_codepoint(T)];
        [] ->
            []
    end.

idempotent(F) ->
    ?FORALL(S, chardata(),
            begin
                Res = F(S),
                Res =:= F(Res)
            end).

deep(F) ->
    ?FORALL({S,G}, {charlist(),mixed_guidance()},
            begin
                Mixed = make_mixed(G, S),
                ?WHENFAIL(io:format("string:~p(~tp)\n", [F,Mixed]),
                          string:equal(string:F(S), string:F(Mixed)))
            end).

flatten(Bin) when is_binary(Bin) ->
    Bin;
flatten(L) ->
    unicode:characters_to_list(L).

decompose_chardata(Bin) when is_binary(Bin) ->
    unicode:characters_to_nfd_binary(Bin);
decompose_chardata([H|T]) when is_integer(H) ->
    case unicode:characters_to_nfd_list([H]) of
        [H] ->
            [H|decompose_chardata(T)];
        [_|_]=Chars ->
            decompose_chardata(Chars ++ T)
    end;
decompose_chardata([H|T]) ->
    [decompose_chardata(H)|decompose_chardata(T)];
decompose_chardata([]) ->
    [].

get_graphemes(S) ->
    case string:next_grapheme(S) of
        [C|T] ->
            [C|get_graphemes(T)];
        [] ->
            []
    end.