1 :- module(unique_quantified_identifiers, [set_unique_quantified_identifiers/2]).
2
3 :- use_module(library(lists), [reverse/2]).
4 :- use_module(probsrc(bsyntaxtree), [unique_typed_id/3]).
5
6 :- set_prolog_flag(double_quotes, codes).
7
8 set_unique_quantified_identifiers(Pred, NewPred) :-
9 set_unique_quantified_identifiers_ast(Pred, [], NewPred).
10
11 %% set_unique_quantified_identifiers_ast(+Ast, +Scopes, -NAst).
12 set_unique_quantified_identifiers_ast(Ast, Scopes, NAst) :-
13 Ast = b(Expr,Type,Info),
14 set_unique_quantified_identifiers_expr(Expr, Type, Scopes, NExpr),
15 NAst = b(NExpr,Type,Info).
16
17 %% set_unique_quantified_identifiers_ast_map(+AstList, +Scopes, -NAstList).
18 set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList) :-
19 set_unique_quantified_identifiers_ast_map(AstList, Scopes, Diff-Diff, NAstList).
20
21 %% set_unique_quantified_identifiers_ast_map(+AstList, +Scopes, +DiffListAcc, -NAstList).
22 set_unique_quantified_identifiers_ast_map([], _, Acc-D, Acc) :-
23 D = [].
24 set_unique_quantified_identifiers_ast_map([Ast|T], Scopes, Acc-D, NAstList) :-
25 set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
26 D = [NAst|ND],
27 set_unique_quantified_identifiers_ast_map(T, Scopes, Acc-ND, NAstList).
28
29 %% set_unique_quantified_identifiers_expr(+Expr, +Type, +Scopes, -NewExpr).
30 % Scopes is a list of lists where the first list corresponds to the last
31 % quantified scope where we lookup identifier names first.
32 set_unique_quantified_identifiers_expr(forall(Ids,Lhs,Rhs), _Type, Scopes, NewExpr) :-
33 !,
34 get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
35 set_unique_quantified_identifiers_ast(Lhs, [UniqueIdMapping|Scopes], NLhs),
36 set_unique_quantified_identifiers_ast(Rhs, [UniqueIdMapping|Scopes], NRhs),
37 NewExpr = forall(UniqueIds,NLhs,NRhs).
38 set_unique_quantified_identifiers_expr(exists(Ids,Body), _Type, Scopes, NewExpr) :-
39 !,
40 get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
41 set_unique_quantified_identifiers_ast(Body, [UniqueIdMapping|Scopes], NBody),
42 NewExpr = exists(UniqueIds,NBody).
43 set_unique_quantified_identifiers_expr(lambda(Ids,Pred,Expr), _Type, Scopes, NewExpr) :-
44 !,
45 get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
46 set_unique_quantified_identifiers_ast(Pred, [UniqueIdMapping|Scopes], NPred),
47 set_unique_quantified_identifiers_ast(Expr, [UniqueIdMapping|Scopes], NExpr),
48 NewExpr = lambda(UniqueIds,NPred,NExpr).
49 set_unique_quantified_identifiers_expr(comprehension_set(Ids,Body), _Type, Scopes, NewExpr) :-
50 !,
51 get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping),
52 set_unique_quantified_identifiers_ast(Body, [UniqueIdMapping|Scopes], NBody),
53 NewExpr = comprehension_set(UniqueIds,NBody).
54 set_unique_quantified_identifiers_expr(identifier(IdName), Type, Scopes, NId) :-
55 !,
56 ( lookup_in_quantified_scopes(identifier(IdName), Type, Scopes, NIdAst),
57 NIdAst = b(NId,_,_)
58 -> true
59 ; NId = identifier(IdName)
60 ).
61 set_unique_quantified_identifiers_expr(record_field(Id,AstElm), _Type, _Scopes, Field) :-
62 !,
63 Field = record_field(Id,AstElm).
64 set_unique_quantified_identifiers_expr(set_extension(AstList), _Type, Scopes, NSet) :-
65 !,
66 set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList),
67 NSet = set_extension(NAstList).
68 set_unique_quantified_identifiers_expr(sequence_extension(AstList), _Type, Scopes, NSeq) :-
69 !,
70 set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList),
71 NSeq = set_extension(NAstList).
72 set_unique_quantified_identifiers_expr(rec(Fields), _Type, Scopes, NRec) :-
73 !,
74 set_unique_quantified_identifiers_record_fields(Fields, Scopes, NFields),
75 NRec = rec(NFields).
76 set_unique_quantified_identifiers_expr(struct(Rec), _Type, Scopes, NStruct) :-
77 !,
78 set_unique_quantified_identifiers_ast(Rec, Scopes, NRec),
79 NStruct = struct(NRec).
80 set_unique_quantified_identifiers_expr(partition(Set, AstList), _Type, Scopes, NPartition) :-
81 !,
82 set_unique_quantified_identifiers_ast(Set, Scopes, NSet),
83 set_unique_quantified_identifiers_ast_map(AstList, Scopes, NAstList),
84 NPartition = partition(NSet, NAstList).
85 set_unique_quantified_identifiers_expr(Unary, _Type, Scopes, NUnary) :-
86 functor(Unary, Functor, Arity),
87 Arity == 1,
88 \+ is_symbol_functor(Functor),
89 !,
90 arg(1, Unary, Arg),
91 set_unique_quantified_identifiers_ast(Arg, Scopes, NArg),
92 functor(NUnary, Functor, Arity),
93 arg(1, NUnary, NArg).
94 set_unique_quantified_identifiers_expr(Unary, _Type, Scopes, NUnary) :-
95 functor(Unary, Functor, Arity),
96 Arity == 2,
97 !,
98 arg(1, Unary, Arg1),
99 set_unique_quantified_identifiers_ast(Arg1, Scopes, NArg1),
100 arg(2, Unary, Arg2),
101 set_unique_quantified_identifiers_ast(Arg2, Scopes, NArg2),
102 functor(NUnary, Functor, Arity),
103 arg(1, NUnary, NArg1),
104 arg(2, NUnary, NArg2).
105 set_unique_quantified_identifiers_expr(let_predicate(Ids,Equalities,Ast), _Type, Scopes, NLet) :-
106 !,
107 set_unique_quantified_identifiers_ast_map(Equalities, Scopes, NEqualities),
108 set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
109 NLet = let_predicate(Ids,NEqualities,NAst).
110 set_unique_quantified_identifiers_expr(let_expression(Ids,Equalities,Ast), _Type, Scopes, NLet) :-
111 !,
112 set_unique_quantified_identifiers_ast_map(Equalities, Scopes, NEqualities),
113 set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
114 NLet = let_expression(Ids,NEqualities,NAst).
115 set_unique_quantified_identifiers_expr(Expr, _, _, Expr).
116
117 %% set_unique_quantified_identifiers_record_fields(+Field, +Scopes, -NewFields).
118 set_unique_quantified_identifiers_record_fields([], _, []).
119 set_unique_quantified_identifiers_record_fields([field(Name,Ast)|T], Scopes, [field(Name,NAst)|NT]) :-
120 set_unique_quantified_identifiers_ast(Ast, Scopes, NAst),
121 set_unique_quantified_identifiers_record_fields(T, Scopes, NT).
122
123 %% lookup_in_quantified_scopes(+IdExpr, +IdType, +Scopes, -NId).
124 % Return new identifier if in scope or fail.
125 lookup_in_quantified_scopes(IdExpr, IdType, [Scope|_], NId) :-
126 memberchk((b(IdExpr,IdType,_),TNId),Scope),
127 !,
128 NId = TNId.
129 lookup_in_quantified_scopes(IdExpr, IdType, [_|T], NId) :-
130 lookup_in_quantified_scopes(IdExpr, IdType, T, NId).
131
132 %% get_fresh_unique_ids(+Ids, -UniqueIds, -UniqueIdMapping).
133 % It is important to keep the order of variables, e.g., if -UniqueIds is used in comprehension_set/2.
134 get_fresh_unique_ids(Ids, UniqueIds, UniqueIdMapping) :-
135 get_fresh_unique_ids(Ids, [], [], TUniqueIds, UniqueIdMapping),
136 reverse(TUniqueIds, UniqueIds).
137
138 get_fresh_unique_ids([], UniqueIdsAcc, UniqueIdMappingAcc, UniqueIdsAcc, UniqueIdMappingAcc).
139 get_fresh_unique_ids([Id|T], UniqueIdsAcc, UniqueIdMappingAcc, UniqueIds, UniqueIdMapping) :-
140 Id = b(IdExpr,IdType,_),
141 unique_typed_id("_q",IdType,UniqueId),
142 get_fresh_unique_ids(T, [UniqueId|UniqueIdsAcc], [(b(IdExpr,IdType,_),UniqueId)|UniqueIdMappingAcc], UniqueIds, UniqueIdMapping).
143
144 is_symbol_functor(empty_set).
145 is_symbol_functor(string_set).
146 is_symbol_functor(bool_set).
147 is_symbol_functor(integer_set).
148 is_symbol_functor(integer).
149 is_symbol_functor(string).
150 is_symbol_functor(value).
151 is_symbol_functor(real).
152
153 :- use_module(library(plunit)).
154 %:- use_module(extension('prolog_fuzzer/fuzzing')).
155
156 :- begin_tests(set_unique_quantified_identifiers).
157
158 reset_id :-
159 tools:retractall(id_counter(_)).
160
161 test(single_quantifier, [setup(reset_id), true(Renamed == Expected)]) :-
162 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),
163 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,[]).
164
165 test(two_nested_quantifiers, [setup(reset_id), true(Renamed == Expected)]) :-
166 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),
167 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,[]).
168
169 test(two_nested_quantifiers2, [setup(reset_id), true(Renamed == Expected)]) :-
170 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),
171 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,[]).
172
173 test(renamed_id_in_set, [setup(reset_id), true(Renamed == Expected)]) :-
174 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),
175 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,[]).
176
177 :- end_tests(set_unique_quantified_identifiers).
178
179 %fuzz_test :-
180 % fuzz(unique_quantified_identifiers:set_unique_quantified_identifiers, 2, 100000, prob_ast_pred([]):var).