unique_quantified_identifiers

get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping) :-
    get_fresh_unique_ids(Ids, [], [], TUniqueIds, UniqueIdMapping),
    reverse(TUniqueIds, UniqueIds).

get_fresh_unique_ids([], UniqueIdsAcc, UniqueIdMappingAcc, UniqueIdsAcc, UniqueIdMappingAcc).

get_fresh_unique_ids([Id|T], UniqueIdsAcc, UniqueIdMappingAcc, UniqueIds, UniqueIdMapping) :-
    Id = b(IdExpr,IdType,_),
    unique_typed_id("_q",IdType,UniqueId),
    get_fresh_unique_ids(T, [UniqueId|UniqueIdsAcc], [(b(IdExpr,IdType,_),UniqueId)|UniqueIdMappingAcc], UniqueIds, UniqueIdMapping).

is_symbol_functor(empty_set).

is_symbol_functor(string_set).

is_symbol_functor(bool_set).

is_symbol_functor(integer_set).

is_symbol_functor(integer).

is_symbol_functor(string).

is_symbol_functor(value).

is_symbol_functor(real).

lookup_in_quantified_scopes(IdExpr, IdType, [Scope|_], NId) :-
    memberchk((b(IdExpr,IdType,_),TNId),Scope),
    !,
    NId = TNId.

lookup_in_quantified_scopes(IdExpr, IdType, [_|T], NId) :-
    lookup_in_quantified_scopes(IdExpr, IdType, T, NId).

reset_id :-
    tools:retractall(id_counter(_)).

set_unique_quantified_identifiers(Pred, NewPred) :-
    set_unique_quantified_identifiers_ast(Pred, [], NewPred).

set_unique_quantified_identifiers_ast(Ast, Scopes, NAst) :-
    Ast = b(Expr,Type,Info),
    set_unique_quantified_identifiers_expr(Expr, Type, Scopes, NExpr),
    NAst = b(NExpr,Type,Info).

set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList) :-
    set_unique_quantified_identifiers_ast_map(AstList, Scopes, Diff-Diff, NAstList).

set_unique_quantified_identifiers_ast_map([], _, Acc-D, Acc) :-
    D = [].

set_unique_quantified_identifiers_ast_map([Ast|T], Scopes, Acc-D, NAstList) :-
    set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
    D = [NAst|ND],
    set_unique_quantified_identifiers_ast_map(T, Scopes, Acc-ND, NAstList).

set_unique_quantified_identifiers_expr(forall(Ids,Lhs,Rhs), _Type, Scopes, NewExpr) :-
    !,
    get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
    set_unique_quantified_identifiers_ast(Lhs, [UniqueIdMapping|Scopes], NLhs),
    set_unique_quantified_identifiers_ast(Rhs, [UniqueIdMapping|Scopes], NRhs),
    NewExpr = forall(UniqueIds,NLhs,NRhs).

set_unique_quantified_identifiers_expr(exists(Ids,Body), _Type, Scopes, NewExpr) :-
    !,
    get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
    set_unique_quantified_identifiers_ast(Body, [UniqueIdMapping|Scopes], NBody),
    NewExpr = exists(UniqueIds,NBody).

set_unique_quantified_identifiers_expr(lambda(Ids,Pred,Expr), _Type, Scopes, NewExpr) :-
    !,
    get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
    set_unique_quantified_identifiers_ast(Pred, [UniqueIdMapping|Scopes], NPred),
    set_unique_quantified_identifiers_ast(Expr, [UniqueIdMapping|Scopes], NExpr),
    NewExpr = lambda(UniqueIds,NPred,NExpr).

set_unique_quantified_identifiers_expr(comprehension_set(Ids,Body), _Type, Scopes, NewExpr) :-
    !,
    get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
    set_unique_quantified_identifiers_ast(Body, [UniqueIdMapping|Scopes], NBody),
    NewExpr = comprehension_set(UniqueIds,NBody).

set_unique_quantified_identifiers_expr(identifier(IdName), Type, Scopes, NId) :-
    !,
    ( lookup_in_quantified_scopes(identifier(IdName), Type, Scopes, NIdAst),
    NIdAst = b(NId,_,_)
    -> true
    ; NId = identifier(IdName)
).

set_unique_quantified_identifiers_expr(record_field(Id,AstElm), _Type, _Scopes, Field) :-
    !,
    Field = record_field(Id,AstElm).

set_unique_quantified_identifiers_expr(set_extension(AstList), _Type, Scopes, NSet) :-
    !,
    set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList),
    NSet = set_extension(NAstList).

set_unique_quantified_identifiers_expr(sequence_extension(AstList), _Type, Scopes, NSeq) :-
    !,
    set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList),
    NSeq = set_extension(NAstList).

set_unique_quantified_identifiers_expr(rec(Fields), _Type, Scopes, NRec) :-
    !,
    set_unique_quantified_identifiers_record_fields(Fields, Scopes, NFields),
    NRec = rec(NFields).

set_unique_quantified_identifiers_expr(struct(Rec), _Type, Scopes, NStruct) :-
    !,
    set_unique_quantified_identifiers_ast(Rec, Scopes, NRec),
    NStruct = struct(NRec).

set_unique_quantified_identifiers_expr(partition(Set, AstList), _Type, Scopes, NPartition) :-
    !,
    set_unique_quantified_identifiers_ast(Set, Scopes, NSet),
    set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList),
    NPartition = partition(NSet, NAstList).

set_unique_quantified_identifiers_expr(Unary, _Type, Scopes, NUnary) :-
    functor(Unary, Functor, Arity),
    Arity == 1,
    \+ is_symbol_functor(Functor),
    !,
    arg(1, Unary, Arg),
    set_unique_quantified_identifiers_ast(Arg, Scopes, NArg),
    functor(NUnary, Functor, Arity),
    arg(1, NUnary, NArg).

set_unique_quantified_identifiers_expr(Unary, _Type, Scopes, NUnary) :-
    functor(Unary, Functor, Arity),
    Arity == 2,
    !,
    arg(1, Unary, Arg1),
    set_unique_quantified_identifiers_ast(Arg1, Scopes, NArg1),
    arg(2, Unary, Arg2),
    set_unique_quantified_identifiers_ast(Arg2, Scopes, NArg2),
    functor(NUnary, Functor, Arity),
    arg(1, NUnary, NArg1),
    arg(2, NUnary, NArg2).

set_unique_quantified_identifiers_expr(let_predicate(Ids,Equalities,Ast), _Type, Scopes, NLet) :-
    !,
    set_unique_quantified_identifiers_ast_map(Equalities, Scopes, NEqualities),
    set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
    NLet = let_predicate(Ids,NEqualities,NAst).

set_unique_quantified_identifiers_expr(let_expression(Ids,Equalities,Ast), _Type, Scopes, NLet) :-
    !,
    set_unique_quantified_identifiers_ast_map(Equalities, Scopes, NEqualities),
    set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
    NLet = let_expression(Ids,NEqualities,NAst).

set_unique_quantified_identifiers_expr(Expr, _, _, Expr).

set_unique_quantified_identifiers_record_fields([], _, []).

set_unique_quantified_identifiers_record_fields([field(Name,Ast)|T], Scopes, [field(Name,NAst)|NT]) :-
    set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
    set_unique_quantified_identifiers_record_fields(T, Scopes, NT).

test(single_quantifier, [setup(reset_id), true(Renamed == Expected)]) :-
    set_unique_quantified_identifiers(b(conjunct(b(conjunct(b(less(b(identifier(y),integer,[]),b(identifier(x),integer,[])),pred,[]),b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[])),pred,[]),b(forall([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(member(b(identifier(x),integer,[]),b(integer_set('NATURAL'),set(integer),[])),pred,[]),b(conjunct(b(less(b(identifier(y),integer,[]),b(identifier(x),integer,[])),pred,[]),b(less(b(integer(0),integer,[]),b(identifier(x),integer,[])),pred,[])),pred,[])),pred,[])),pred,[]), Renamed),
    Expected = b(conjunct(b(conjunct(b(less(b(identifier(y),integer,[]),b(identifier(x),integer,[])),pred,[]),b(less(b(integer(1),integer,[]),b(identifier(x),integer,[])),pred,[])),pred,[]),b(forall([b(identifier('_q1'),integer,[]),b(identifier('_q2'),integer,[])],b(member(b(identifier('_q1'),integer,[]),b(integer_set('NATURAL'),set(integer),[])),pred,[]),b(conjunct(b(less(b(identifier('_q2'),integer,[]),b(identifier('_q1'),integer,[])),pred,[]),b(less(b(integer(0),integer,[]),b(identifier('_q1'),integer,[])),pred,[])),pred,[])),pred,[])),pred,[]).

test(two_nested_quantifiers, [setup(reset_id), true(Renamed == Expected)]) :-
    set_unique_quantified_identifiers(b(forall([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(truth,pred,[]),b(exists([b(identifier(z),integer,[])],b(equal(b(identifier(y),integer,[]),b(add(b(identifier(x),integer,[]),b(unary_minus(b(identifier(z),integer,[])),integer,[])),integer,[])),pred,[])),pred,[])),pred,[]), Renamed),
    Expected = b(forall([b(identifier('_q1'),integer,[]),b(identifier('_q2'),integer,[])],b(truth,pred,[]),b(exists([b(identifier('_q3'),integer,[])],b(equal(b(identifier('_q2'),integer,[]),b(add(b(identifier('_q1'),integer,[]),b(unary_minus(b(identifier('_q3'),integer,[])),integer,[])),integer,[])),pred,[])),pred,[])),pred,[]).

test(two_nested_quantifiers2, [setup(reset_id), true(Renamed == Expected)]) :-
    set_unique_quantified_identifiers(b(forall([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(member(b(identifier(x),integer,[]),b(integer_set('NATURAL1'),set(integer),[])),pred,[]),b(member(b(identifier(y),integer,[]),b(integer_set('NATURAL1'),set(integer),[])),pred,[])),pred,[]),b(conjunct(b(conjunct(b(less(b(integer(0),integer,[]),b(identifier(x),integer,[])),pred,[]),b(less(b(integer(0),integer,[]),b(identifier(y),integer,[])),pred,[])),pred,[]),b(forall([b(identifier(z),integer,[])],b(truth,pred,[]),b(equal(b(identifier(y),integer,[]),b(add(b(identifier(x),integer,[]),b(unary_minus(b(identifier(z),integer,[])),integer,[])),integer,[])),pred,[])),pred,[])),pred,[])),pred,[]), Renamed),
    Expected = b(forall([b(identifier('_q1'),integer,[]),b(identifier('_q2'),integer,[])],b(conjunct(b(member(b(identifier('_q1'),integer,[]),b(integer_set('NATURAL1'),set(integer),[])),pred,[]),b(member(b(identifier('_q2'),integer,[]),b(integer_set('NATURAL1'),set(integer),[])),pred,[])),pred,[]),b(conjunct(b(conjunct(b(less(b(integer(0),integer,[]),b(identifier('_q1'),integer,[])),pred,[]),b(less(b(integer(0),integer,[]),b(identifier('_q2'),integer,[])),pred,[])),pred,[]),b(forall([b(identifier('_q3'),integer,[])],b(truth,pred,[]),b(equal(b(identifier('_q2'),integer,[]),b(add(b(identifier('_q1'),integer,[]),b(unary_minus(b(identifier('_q3'),integer,[])),integer,[])),integer,[])),pred,[])),pred,[])),pred,[])),pred,[]).

test(renamed_id_in_set, [setup(reset_id), true(Renamed == Expected)]) :-
    set_unique_quantified_identifiers(b(forall([b(identifier(x),integer,[]),b(identifier(y),integer,[])],b(conjunct(b(member(b(identifier(x),integer,[]),b(integer_set('NATURAL'),set(integer),[])),pred,[]),b(member(b(identifier(y),integer,[]),b(integer_set('NATURAL'),set(integer),[])),pred,[])),pred,[]),b(subset_strict(b(set_extension([b(identifier(x),integer,[])]),set(integer),[]),b(set_extension([b(identifier(y),integer,[]),b(integer(1),integer,[]),b(integer(2),integer,[]),b(integer(3),integer,[])]),set(integer),[])),pred,[])),pred,[]), Renamed),
    Expected = b(forall([b(identifier('_q1'),integer,[]),b(identifier('_q2'),integer,[])],b(conjunct(b(member(b(identifier('_q1'),integer,[]),b(integer_set('NATURAL'),set(integer),[])),pred,[]),b(member(b(identifier('_q2'),integer,[]),b(integer_set('NATURAL'),set(integer),[])),pred,[])),pred,[]),b(subset_strict(b(set_extension([b(identifier('_q1'),integer,[])]),set(integer),[]),b(set_extension([b(identifier('_q2'),integer,[]),b(integer(1),integer,[]),b(integer(2),integer,[]),b(integer(3),integer,[])]),set(integer),[])),pred,[])),pred,[]).