fuzzer

clear_disallowed_types(Env, _, [boolean]) :-
    bf_env:has_option(sat_only, Env), !.

clear_disallowed_types(Env, Types, AllowedTypes) :-
    clear_reals(Env, Types, Types2),
    clear_strings(Env, Types2, AllowedTypes).

clear_reals(Env, Types, AllowedTypes) :-
    bf_env:has_option(use_reals, Env)
    -> Types = AllowedTypes
    ; delete(Types, real, AllowedTypes).

clear_strings(Env, Types, AllowedTypes) :-
    bf_env:has_option(use_strings, Env)
    -> Types = AllowedTypes
    ; delete(Types, string, AllowedTypes).

conjunction([C], C) :- !.

conjunction([C1, C2 | Cs], Res) :-
    Conjunct = b(conjunct(C1, C2), pred, []),
    conjunction([Conjunct | Cs], Res).

cross_prod([T|Ts], CrossProd) :-
    cross_prod_(Ts, T, CrossProd), !.

cross_prod_([], T, T).

cross_prod_([T | Ts], Couple, Result) :-
    % Note: INT*INT*INT = (INT*INT)*INT
    cross_prod_(Ts, couple(Couple, T), Result).

cross_prod_of(Prod, Typelist) :-
    cross_prod_of_(Prod, [], Typelist).

cross_prod_of_(couple(T1, T2), InterList, Typelist) :-
    cross_prod_of_(T1, [T2 | InterList], Typelist).

cross_prod_of_(T1, InterList, [T1 | InterList]).

disallowed_child(first, 2, empty_sequence:_).

disallowed_child(tail, 2, empty_sequence:_).

disallowed_child(front, 2, empty_sequence:_).

disallowed_child(last, 2, empty_sequence:_).

disallowed_child(function, 2, empty_set:_).

disallowed_child(mu, 2, empty_set:_).

disallowed_child(general_intersection, 2, empty_set:_).

disallowed_child(min, 2, empty_set:_).

disallowed_child(max, 2, empty_set:_).

disallowed_child(min_real, 2, empty_set:_).

disallowed_child(max_real, 2, empty_set:_).

fresh_random_id_name([], id0) :- !.

fresh_random_id_name(UsedIds, Name) :-
    findall(IdName, member(IdName:_, UsedIds), IdNames),
    maplist(id_number, IdNames, IdNums),
    max(IdNums, Max),
    NewNum is Max+1,
    id_number(Name, NewNum).

fuzz(Options, Result) :-
    env(Options, Env),
    fuzz(Env, _, Result).

fuzz(Env, NewEnv, Result) :-
    bf_env:has_option(size, Env, Depth),
    bf_env:has_option(conjuncts_min, Env, Min),
    bf_env:has_option(conjuncts_max, Env, Max),
    rand_int_inclusive(Min, Max, Conjuncts),
    fuzz_n_conjuncts(Conjuncts, Depth, Env, NewEnv, Ast),
    repair_used_ids('BanditFuzz Fuzzer', Ast, Result),
    !.

fuzz(1, Type, Env, NewEnv, Result) :- !,
    fuzz_1_value_type(Type, Env, ValueType),
    fuzz_value(ValueType, Env, NewEnv, Result).

fuzz(N, Type, Env, NewEnv, Result) :-
    N > 1,
    allowed_nodes(Env, Type, Allowed),
    random_member_bt(Expr:Type, Allowed),
    Expr =.. [Functor | Children],
    fuzz_node(Functor, Children, Type, N, Env, NewEnv, Result).

fuzz_1_value_type(Type, Env, ValueType) :-
    % Catch unbound variables.
    var(Type), !,
    % Treat as any: Find random type.
    wd_type(Env, Type),
    fuzz_1_value_type(Type, Env, ValueType).

fuzz_1_value_type(ids, _, identifier_list:any) :- !.

fuzz_1_value_type(ids(T), _, identifier_crossprod:T) :- !.

fuzz_1_value_type(Type, Env, Expr:Type) :-
    allowed_leafs(Env, Type, Allowed),
    ((Type == pred ; bf_env:var_max_reached(Env)) ->
    random_member_bt(Expr:Type, Allowed) % pred cannot be an identifier
    ; random_member_bt(Expr:Type, [identifier:Type | Allowed])),
    % Ensure that type is fully ground. `pred` is a special case and always ground.
    (Type == pred -> true ; wd_type(Env, Type)).

fuzz_children([], _, Env, Env, []) :- !.

fuzz_children([Ids | ChildrenTypes], N, Env, NewEnv, [IdList | ChildResults]) :-
    % Special case for when the first child is an identifier list.
    \+ var(Ids),
    Ids =.. [ids | _], !,
    fuzz_1_value_type(Ids, Env, IdsValueType),
    % ID list consists of local identifiers.
    fuzz_value(IdsValueType, Env, _, IdList),
    findall(Id:Type, member(b(identifier(Id), Type, []), IdList), LocalIds),
    with_local_ids(Env, LocalIds, LocalEnv),
    fuzz_children(ChildrenTypes, N, LocalEnv, LocalNewEnv, ChildResults),
    % Leave scope again.
    leave_local_id_scope(LocalNewEnv, NewEnv).

fuzz_children([ChildTypeList|ChildTypes], N, Env, NewEnv, [ChildResult|ChildResults]) :-
    % Special Case for when first child is a list.
    \+ var(ChildTypeList),
    ChildTypeList = [ChildType], !,
    fuzz_list(ChildType, N, Env, InterEnv, ChildResult),
    fuzz_children(ChildTypes, N, InterEnv, NewEnv, ChildResults).

fuzz_children([ChildType|ChildTypes], N, Env, NewEnv, [ChildResult|ChildResults]) :-
    fuzz(N, ChildType, Env, InterEnv, ChildResult),
    fuzz_children(ChildTypes, N, InterEnv, NewEnv, ChildResults).

fuzz_conjuncts(Env, NewEnv, Result) :-
    bf_env:has_option(size, Env, Depth),
    bf_env:has_option(conjuncts_min, Env, Min),
    bf_env:has_option(conjuncts_max, Env, Max),
    rand_int_inclusive(Min, Max, Num),
    fuzz_n_conjuncts(Num, Depth, Env, NewEnv, Result), !.

fuzz_id_cross_prod(Env, NewEnv, IdList, Type) :-
    var(Type), !,
    fuzz_id_list(any, Env, NewEnv, IdList),
    findall(T, member(b(identifier(_), T, _), IdList), TypeList),
    cross_prod(TypeList, Type).

fuzz_id_cross_prod(Env, NewEnv, IdList, Type) :-
    % Type is given already.
    safe_cross_prod_of(Env, Type, IdTypes),
    fuzz_typed_id_list(IdTypes, Env, NewEnv, IdList).

fuzz_id_list(Type, Env, NewEnv, Ids) :-
    bf_env:has_option(list_min, Env, Min),
    bf_env:has_option(list_max, Env, Max),
    rand_int_inclusive(Min, Max, N),
    % Ensure that no shadowing happens.
    % TODO: Allow Shadowing as an option?
    new_id_probability(Env, OldProba),
    with_id_probability(Env, 1, LocalEnv),
    has_option(var_max, Env, VarMax), % Need to ensure Id lists ignore the var_max option.
    add_option(var_max, none, LocalEnv, LocalEnv2),
    fuzz_id_list(N, Type, LocalEnv2, LocalNewEnv, Ids),
    add_option(var_max, VarMax, LocalNewEnv, LocalNewEnv2),
    with_id_probability(LocalNewEnv2, OldProba, NewEnv).

fuzz_id_list(0, _, Env, Env, []) :- !.

fuzz_id_list(N, Type, Env, NewEnv, [Id|Ids]) :-
    N > 0,
    NN is N-1,
    fuzz_value(identifier:Type, Env, InterEnv, Id),
    fuzz_id_list(NN, Type, InterEnv, NewEnv, Ids).

fuzz_list(NodeType, N, Env, NewEnv, Result) :-
    bf_env:has_option(list_min, Env, Min),
    bf_env:has_option(list_max, Env, Max),
    rand_int_inclusive(Min, Max, Num),
    fuzz_n_nodes(Num, NodeType, N, Env, NewEnv, Result).

fuzz_n_conjuncts(Num, Depth, Env, NewEnv, Result) :-
    fuzz_n_conjuncts(Num, Depth, Env, NewEnv, [], Result).

fuzz_n_conjuncts(0, _, Env, Env, Acc, Result) :- !,
    conjunction(Acc, Result).

fuzz_n_conjuncts(Num, Depth, Env, NewEnv, Acc, Result) :-
    Num > 0,
    fuzz(Depth, pred, Env, InterEnv, InterRes),
    NN is Num-1,
    fuzz_n_conjuncts(NN, Depth, InterEnv, NewEnv, [InterRes | Acc], Result).

fuzz_n_nodes(0, _, _, Env, Env, []) :- !.

fuzz_n_nodes(N, NodeType, Depth, Env, NewEnv, [Result | Results]) :-
    N > 0,
    NN is N-1,
    % TODO: Do we need to use a local environment for each sub node or can we
    % build up the environment like happening right now?
    fuzz(Depth, NodeType, Env, InterEnv, Result), !,
    fuzz_n_nodes(NN, NodeType, Depth, InterEnv, NewEnv, Results).

fuzz_node(equal, [_, _], Type, 2, Env, NewEnv, BExpr) :-
    bf_env:has_option(sat_only, Env), !,
    % Fuzz LHS as id.
    fuzz_value(identifier:boolean, Env, NewEnv, Id),
    % Fuzz RHS as value.
    allowed_leafs(NewEnv, boolean, Allowed),
    random_member(Value:boolean, Allowed),
    BValue = b(Value, boolean, []),
    % Create AST.
    safe_create_texpr(equal(Id, BValue), Type, [], BExpr).

fuzz_node(Node, Children, Type, N, Env, NewEnv, BExpr) :-
    NN is N-1,
    restrict_env_if_needed(Node, N, Env, LocalEnv, Changed),
    fuzz_children(Children, NN, LocalEnv, LocalNewEnv, ResultChildren),
    restore_available_nodes_when_changed(Changed, Env, LocalNewEnv, NewEnv),
    NewNode =.. [Node | ResultChildren],
    prepare_info(NewNode, Type, Info),
    safe_create_texpr(NewNode, Type, Info, BExpr),
    !.

fuzz_node(Node, 1, Env, NewEnv, Result) :-
    !,
    % Only allow leaf or primitive types on this level.
    (is_leaf_node(Node), has_type(Node, Type)
    ; primary_type(Node), Type = Node),
    fuzz_value(Node:Type, Env, NewEnv, Result).

fuzz_node(NodeName, N, Env, NewEnv, Result) :-
    findall(T-CTs, node_info(NodeName, T, CTs), TypingOverview),
    random_member_bt(Type-ChildrenTypes, TypingOverview),
    fuzz_node(NodeName, ChildrenTypes, Type, N, Env, NewEnv, BExpr),
    repair_used_ids('BanditFuzz Fuzzer', BExpr, Result).

fuzz_typed_id_list(Types, Env, NewEnv, Ids) :-
    new_id_probability(Env, OldProba),
    with_id_probability(Env, 1, LocalEnv),
    has_option(var_max, Env, VarMax), % Need to ensure Id lists ignore the var_max option.
    add_option(var_max, none, LocalEnv, LocalEnv2),
    fuzz_typed_id_list_(Types, LocalEnv2, LocalNewEnv, Ids),
    add_option(var_max, VarMax, LocalNewEnv, LocalNewEnv2),
    with_id_probability(LocalNewEnv2, OldProba, NewEnv).

fuzz_typed_id_list_([], Env, Env, []) :- !.

fuzz_typed_id_list_([T | Ts], Env, NewEnv, [Id | Ids]) :-
    fuzz_value(identifier:T, Env, InterEnv, Id),
    fuzz_typed_id_list_(Ts, InterEnv, NewEnv, Ids).

fuzz_value(identifier_crossprod:Type, Env, NewEnv, BAst) :-
    !, % Special case.
    wd_type(Env, Type),
    fuzz_value_(identifier_crossprod:Type, Env, NewEnv, BAst).

fuzz_value(Expr:Type, Env, NewEnv, BAst) :-
    (\+ ground(Type) -> wd_type(Env, Type); true), % Ensure Type is fully ground.
    fuzz_value_(Expr:Type, Env, NewEnv, BAst).

fuzz_value_(identifier:Type, Env, NewEnv, b(identifier(Name), IdType, [])) :- !,
    % Note: `any` implies random type; var(Type) as well.
    (Type \= any -> Type = IdType ; random_type(Env, IdType)),
    used_ids(Env, Ids),
    findall(TId, member(TId:IdType, Ids), TypedIds),
    new_id_probability(Env, Proba),
    ( (TypedIds = [] ; \+ bf_env:var_max_reached(Env), maybe(Proba)) ->
    fresh_random_id_name(Ids, Name), add_id_use(Env, Name, Type, NewEnv)
    ;
    random_member(Name, TypedIds), NewEnv = Env
).

fuzz_value_(identifier_list:Type, Env, NewEnv, IdentifierList) :- !,
    % This is a special case for nodes that need a list of identifiers, e.g. `exists`.
    % We generate a list of identifiers of the specified type.
    fuzz_id_list(Type, Env, NewEnv, IdentifierList).

fuzz_value_(identifier_crossprod:Type, Env, NewEnv, IdentifierList) :- !,
    % This is a special case for nodes that need a list of identifiers
    % and have a type of the cross-product of the individual id's types.
    % lambda and comprehension_set are such examples.
    fuzz_id_cross_prod(Env, NewEnv, IdentifierList, Type).

fuzz_value_(integer:integer, Env, Env, b(integer(N), integer, [])) :- !,
    rand_integer(Env, N).

fuzz_value_(real:real, Env, Env, b(real(Real), real, [])) :- !,
    random(R),
    rand_integer(Env, I),
    N is I + R,
    % ProB encodes reals as atoms in b/3.
    number_codes(N, Codes),
    atom_codes(Real, Codes).

fuzz_value_(string:string, Env, Env, b(string(S), string, [])) :- !,
    S = 'FUZZED_STRING'. % TODO: Generate random string.

fuzz_value_(nat_set:set(integer), Env, Env, b(integer_set('NAT'), set(integer), [])) :- !.

fuzz_value_(nat1_set:set(integer), Env, Env, b(integer_set('NAT1'), set(integer), [])) :- !.

fuzz_value_(natural_set:set(integer), Env, Env, b(integer_set('NATURAL'), set(integer), [])) :- !.

fuzz_value_(natural1_set:set(integer), Env, Env, b(integer_set('NATURAL1'), set(integer), [])) :- !.

fuzz_value_(int_set:set(integer), Env, Env, b(integer_set('INT'), set(integer), [])) :- !.

fuzz_value_(integer_set:set(integer), Env, Env, b(integer_set('INTEGER'), set(integer), [])) :- !.

fuzz_value_(Ex:Type, Env, Env, b(Ex, Type, [])).

id_number(Name, Number) :-
    var(Name), !,
    number_chars(Number, NumStr),
    atom_chars(Num , NumStr),
    atom_concat(id, Num, Name).

id_number(Name, Number) :-
    atom_concat(id, Num, Name),
    atom_chars(Num , NumStr),
    number_chars(Number, NumStr).

is_type_cross_prod(T) :-
    cross_prod_of(T, _).

prepare_info(exists(Ids, Pred), _, [used_ids(Used)]) :-
    !,
    find_identifier_uses_for_quantifier_body(Ids, Pred, Used).

prepare_info(forall(Ids, Condition, Pred), _, [used_ids(Used)]) :-
    !,
    Impl = b(implication(Condition, Pred), pred, []),
    find_identifier_uses_for_quantifier_body(Ids, Impl, Used).

prepare_info(_, _, []).

qfuzz(Result) :-
    N = 4,
    bf_env:env(E),
    fuzz(N, pred, E, _, Prelim),
    repair_used_ids('BanditFuzz Fuzzer', Prelim, Result).

qfuzz(RootNode, Result) :-
    N = 4,
    bf_env:env(E),
    fuzz_node(RootNode, N, E, _, Result).

rand_int_inclusive(Min, Max, I) :-
    ExclusiveMax is Max + 1,
    random(Min, ExclusiveMax, I).

rand_integer(Env, I) :-
    has_option(min_int, Env, Min),
    has_option(max_int, Env, Max),
    rand_int_inclusive(Min, Max, I).

random_type(Env, Type) :-
    % TODO: Check environment for allowed types.
    findall(T, primitive_type(T), PrimTypes),
    delete(PrimTypes, pred, ValueTypes), % Disallows identifiers of type `pred`.
    findall(T, higher_order_type(T), HighTypes),
    append(HighTypes, ValueTypes, Types),
    clear_disallowed_types(Env, Types, AllowedTypes),
    random_member_bt(Type, AllowedTypes),
    wd_type(Env, Type).

restore_available_nodes_when_changed(false, _, Env, Env).

restore_available_nodes_when_changed(true, Env, ModifiedEnv, RestoredEnv) :-
    allowed_leafs(Env, Leafs),
    allowed_predicates(Env, Predicates),
    allowed_expressions(Env, Expressions),
    with_leafs(ModifiedEnv, Leafs, Inter1),
    with_predicates(Inter1, Predicates, Inter2),
    with_expressions(Inter2, Expressions, RestoredEnv).

restrict_env_if_needed(Node, D, Env, RestrictedEnv, true) :-
    findall(C, disallowed_child(Node, D, C), Children),
    Children \= [],
    !,
    disallow_nodes(Children, Env, RestrictedEnv).

restrict_env_if_needed(_, _, Env, Env, false).

safe_cross_prod_of(Env, Prod, IdTypes) :-
    bf_env:has_option(list_max, Env, Max),
    cross_prod_of(Prod, IdTypes),
    length(IdTypes, L),
    L =< Max. % Ensures that we stay in max range of given options.

wd_type(Env, Type) :-
    acyclic_term(Type), wd_type_aux(Env, Type).

wd_type_aux(Env, Type) :-
    var(Type), !, random_type(Env, Type).

wd_type_aux(_, Type) :-
    primitive_type(Type), !.

wd_type_aux(Env, Type) :-
    higher_order_type(Type),
    higher_order_sub_types(Type, SubTypes),
    % TODO: Higher-order max nesting depth?
    maplist(wd_type_aux(Env), SubTypes).