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). |