14
15
16:- module(
17 quantifiers,
18 [
19 for_all/2,
20 exists/2,
21 let/2,
22
23 list_of/2,
24
25 apply_list/2,
26 call_list/2,
27 call_list/3,
28 call_list/4,
29 call_list/5,
30 call_list/6,
31
32 expand/2,
33 expand/1,
34 evaluate/2,
35
36 indent_term/1,
37
38 op(501, xfx, ..),
39 op(502, yfx, \/),
40
41 op(700, xfx, in),
42 op(990, xfx, where)
43 ]).
102 103
104:- meta_predicate apply_list(1, ?).
110apply_list(Goal, ArgsList):-
111 list_apply(ArgsList, Goal).
112
113
114list_apply([], _).
115list_apply([Args | ArgsList], Goal):-
116 apply(Goal, Args),
117 list_apply(ArgsList, Goal).
118
119
120:- meta_predicate call_list(1, ?). 121:- meta_predicate call_list(2, ?, ?). 122:- meta_predicate call_list(3, ?, ?, ?). 123
124:- meta_predicate list_call(?, 1). 125:- meta_predicate list_call(?, ?, 2). 126:- meta_predicate list_call(?, ?, ?, 3).
132call_list(Goal, Args1):-
133 list_call(Args1, Goal).
134
135list_call([], _).
136list_call([Arg1 | Args1], Goal):-
137 call(Goal, Arg1),
138 list_call(Args1, Goal).
145call_list(Goal, Args1, Args2):-
146 list_call(Args1, Args2, Goal).
147
148list_call([], [], _).
149list_call([Arg1 | Args1], [Arg2 | Args2], Goal):-
150 call(Goal, Arg1, Arg2),
151 list_call(Args1, Args2, Goal).
159call_list(Goal, Args1, Args2, Args3):-
160 list_call(Args1, Args2, Args3, Goal).
161
162list_call([], [], [], _).
163list_call([Arg1 | Args1], [Arg2 | Args2], [Arg3 | Args3], Goal):-
164 call(Goal, Arg1, Arg2, Arg3),
165 list_call(Args1, Args2, Args3, Goal).
172call_list(Goal, Args1, Args2, Args3, Args4):-
173 list_call(Args1, Args2, Args3, Args4, Goal).
174
175list_call([], [], [], [], _).
176list_call([Arg1 | Args1], [Arg2 | Args2], [Arg3 | Args3], [Arg4 | Args4], Goal):-
177 call(Goal, Arg1, Arg2, Arg3, Arg4),
178 list_call(Args1, Args2, Args3, Args4, Goal).
185call_list(Goal, Args1, Args2, Args3, Args4, Args5):-
186 list_call(Args1, Args2, Args3, Args4, Args5, Goal).
187
188list_call([], [], [], [], [], _).
189list_call([Arg1 | Args1], [Arg2 | Args2], [Arg3 | Args3], [Arg4 | Args4], [Arg5 | Args5], Goal):-
190 call(Goal, Arg1, Arg2, Arg3, Arg4, Arg5),
191 list_call(Args1, Args2, Args3, Args4, Args5, Goal).
192
193
194
195
204for_all(VarDomains, Goal) :-
205 var_domains(VarDomains, VarDoms, Condition),
206 for_list(VarDoms, [], [], Condition, Goal).
207
208
209
210
218list_of(VarDomains, Values):-
219 var_domains(VarDomains, VarDoms, Condition),
220 list_list(VarDoms, [], [], Condition, Values).
221
222
223
224var_domains(VarDomains, _VarDoms, _Condition) :-
225 var(VarDomains),
226 !,
227 must_be(nonvar,VarDomains). 228
229var_domains(VarDomains where _Condition, _VarDoms, _Cond) :-
230 var(VarDomains),
231 !,
232 must_be(nonvar, VarDomains).
233
234var_domains(Vars in Domain where Condition, VarDoms, Condition) :-
235 !,
236 (var(Vars)
237 ->
238 VarDoms=[Vars in Domain]
239 ;
240 distribute(Vars, Domain, VarDoms)).
241
242var_domains(VarDomains where Condition, VarDomains, Condition) :-
243 !.
244
245var_domains(Vars in Domain, VarDoms, Condition) :-
246 !,
247 var_domains(Vars in Domain where true, VarDoms, Condition).
248
249var_domains(VarDomains, VarDoms, Condition) :-
250 var_domains(VarDomains where true, VarDoms, Condition).
251
252
253
254distribute([], _, []).
255distribute([Var | Vars], Domain, [Var in Domain | Domains]):-
256 distribute(Vars, Domain, Domains).
257
258
259for_list([], Vars, Values, Condition, Goal):-
260 copy_term(Vars, Condition, Values, Cond),
261 expand(Cond, C),
262 (\+ C 263 ->
264 true
265 ;
266 copy_term(Vars, Goal, Values, G), 267 G 268 ).
269
270
271for_list([D | Domains], Vars, Values, Condition, Goal):-
272 must_be(nonvar, D),
273 D = (V in Domain),
274 expand(Domain, Dom),
275 (next_value(Dom, Min, Greater)
276 ->
277 Vs = [V | Vars],
278 Vals = [Min | Values],
279 280 copy_term([V], Domains, [Min], Doms),
281 for_list(Doms, Vs, Vals, Condition, Goal),
282 (Greater=[]
283 ->
284 true
285 ;
286 for_list([V in Greater | Domains], Vars, Values, Condition, Goal))
287 ;
288 true). 289
290
291list_list([], Vars, Values, Condition, List):-
292 copy_term(Vars, Condition, Values, Cond),
293 expand(Cond, C),
294 (\+ C 295 ->
296 List=[]
297 ;
298 List=Values
299 ).
300
301list_list([D | Domains], Vars, Values, Condition, List):-
302 must_be(nonvar, D),
303 D = (V in Domain),
304 expand(Domain, Dom),
305 (next_value(Dom, Min, Greater)
306 ->
307 Vs = [V | Vars],
308 Vals = [Min | Values],
309 copy_term([V], Domains, [Min], Doms),
310 list_list(Doms, Vs, Vals, Condition, List1), 311 (Greater=[]
312 ->
313 List = List1
314 ;
315 list_list([V in Greater | Domains], Vars, Values, Condition, List2),
316 append(List1, List2, List))
317 ;
318 List = []).
319
320
321next_value(Min .. Max, Mi, Greater):-
322 Mi is Min, 323 Ma is Max,
324 (Mi < Ma
325 ->
326 Mi1 is Mi+1,
327 Greater = Mi1..Ma
328 ;
329 Mi = Ma, 330 Greater = []).
331
332next_value(Domain1 \/ Domain2, Min, Greater):-
333 nextvalue(Domain1, Min, Great),
334 (Great = []
335 ->
336 Greater = Domain2
337 ;
338 Greater = Great \/ Domain2).
339
340next_value([Min | List], Mi, List):-
341 catch(evaluate(Min, Mi), _, Mi=Min).
342
343
344
350exists(Vars, Goal):-
351 copy_term(Vars, Goal, _, RenamedGoal),
352 RenamedGoal.
360let(Bindings, Goal):-
361 var_bindings(Bindings, Vars),
362 copy_term(Vars, f(Bindings, Goal), _, f(BindingsRenamed, GoalRenamed)),
363 bindings(BindingsRenamed),
364 GoalRenamed.
365
366
367var_bindings([], []).
368var_bindings([Binding | Bindings], [X |Vars]) :-
369 (var(Binding)
370 ->
371 X=Binding
372 ;
373 Binding =.. [_, X, _]
374 ),
375 var_bindings(Bindings, Vars).
376
377
379
380bindings([]).
381
382bindings([Binding | Bindings]):-
383 (var(Binding)
384 ->
385 386 bindings(Bindings)
387 ;
388 Binding =.. [Binder, X, Term],
389 must_be(var, X),
390 member(Binder, [=, is, =.., in, ins, #=, #<, #>, #=<, #>=, #\=]), 391 !,
392 expand(Term, Expr),
393 Goal =.. [Binder, X, Expr],
394 Goal,
395 bindings(Bindings)).
396
397
398 399
400
401:- multifile shorthand/3.
409shorthand(if(Condition, Expr1, Expr2), Var, (Condition -> Var=Expr1 ; Var=Expr2)) :-
410 !.
411
425expand(Term, Expr):-
426 (var(Term)
427 ->
428 Expr=Term
429 ;
430 (shorthand(Term, T, Goal)
431 ->
432 Goal
433 ;
434 T=Term),
435 expand_subterms(T, Expr)
436 ).
437
438
439expand_subterms(Term, Expanded):-
440 (compound(Term)
441 ->
442 (Term=[T | Tail]
443 ->
444 Expanded=[ET | ETail],
445 expand_subterms(T, ET),
446 expand_subterms(Tail,ETail)
447 ;
448 Term =.. [F | Subterms],
449 call_list(expand, Subterms, ExpandedSubterms),
450 Expanded =.. [F | ExpandedSubterms]
451 )
452 ;
453 Expanded=Term
454 ).
461expand(Goal) :-
462 expand(Goal, G),
463 G.
470evaluate(Expr, Number):-
471 expand(Expr, E),
472 Number is E.
473
474
475
476
482indent_term(T):-
483 indent_term(0, T).
484
485indent_term(N, Term):-
486 for_all(_ in 1..N, write(' ')),
487 (
488 compound(Term)
489 ->
490 functor(Term, F, A),
491 writeln(F),
492 N1 is N+1,
493 for_all(I in 1..A, exists([Ti], (arg(I, Term, Ti), indent_term(N1, Ti))))
494 ;
495 writeln(Term)
496 )
Bounded quantifiers, let expressions, and expandable shorthand notations.
This module defines bounded quantifiers, let expressions, and a multifile predicate to create new shorthand notations.
for_all/2 bounded universal quantifier with "in" domain and "where" conditions allowing shorthand/3 notations, e.g. Array[Indices] notation for subscripted variables defined in
library(arrays)
. The "in" domain must be a finite (union) interval of integers or a list of values. The "where" condition goal is supposed to be deterministic and just checked for satisfiability without constraining context's variables.list_of/2 list of values satisfying "in" and "where" conditions.
exists/2 existential quantifier.
let/2 existential quantifier for variables bound to expressions allowing shorthand/3 notations.
apply_list/2, call_list/2, /3/4/5 conjunctive application of a goal on a list of arguments.
indent_term/1 just one example of use of quantifiers to pretty print the tree structure of a term.
The "where" condition is a test of satisfiability, not of entailment. The example below illustrates the difference: X=Y is satisfiable for all X, Y hence the goal is executed for all X, Y, while in the fourth query, the condition X==Y is always false hence no constraint is posted:
*/