YAP 7.1.0
parameters.yap
Go to the documentation of this file.
1/**
2 * @file parameters.yap
3 * @author VITOR SANTOS COSTA <vsc@VITORs-MBP.lan>
4 * @date Tue Nov 17 23:34:04 2015
5 *
6 * @brief Experimental test generation code.
7 *
8 *
9*/
10
11:- module( parameters,
12 [such_that/2,
13 op(1060, xfx, such_that),
14 op(1050, xfx, extra_arguments),
15 op(1050, xfx, defaults),
16 op(700, xfx, in),
17 op(700, xfx, ?=), %initialization
18 op(750, xfy, #==>),
19 op(500, yfx, '<=>'),
20 op(500, yfx, '=>'),
21 op(800, yfx, '==>') ]
22 ).
23
24
25
26
27/**
28 * @defgroup parameters Automating test generation
29 * @ingroup YAPLibrary
30 * @{
31
32 This library aims at facilitating test generation in a logic
33 program, namely when interfacing to foreign code. It introduces the
34 following specs:
35
36 - Named Arguments: you can refer to an argument through a name. This
37 allows having optional arguments. As an example, you can say:
38
39 maxlength=MaxLength
40
41 and the original program is extended to support an optional
42 parameter Length, eg:
43
44 vector( Type, Length, V ) :- alloc( Type, Length, MaxLength, V )
45
46 will become
47
48 vector( Type, Length, V, MaxLength ) :- alloc( Type, Length, MaxLength, V )
49
50 - Tests
51
52 You can write type tests and ISO-like tests offline.
53
54 - Initializers
55
56 It allows default code for variables. In the previous code, the
57 initializer MaxLength = 1024 would result in two clauses:
58
59 vector( Type, Length, V, MaxLength ) :-
60 alloc( Type, Length, MaxLength, V ).
61 vector( Type, Length, V ) :-
62 alloc( Type, Length, 1024, V ).
63
64 See myddas.yap for a few examples.
65
66 @author Vitor Santos Costa
67*/
68
69
70
71:- list2conj/2conj2list/2use_module( library(clauses),
72 [,
73 ]).
74
75:- use_module( library(maplist) ).
76
77:- use_module( library(rbtrees) ).
78
79:- use_module( library(lists) ).
80
81:- use_module( library(bdd) ).
82
83:- dynamic extension/4, init/2, frame/2, exclusive/0.
84
85use_module:term_expansion(Term,Clauses) :-
86 Term = ( Spec :- Body),
87 prolog_load_context(module,Mod),
88 extension( Mod:Spec, Tests, GoalVars, Names),
89 extension:context_variables(UnsortedCurrentNames),
90 sort( UnsortedCurrentNames, CurrentNames ),
91 merge_variables( Names, CurrentNames ),
92 findall( (Mod:ExtHead :- ExtBody),
93 expand( Spec, Names, GoalVars, Body, Tests, (ExtHead :- ExtBody)),
94 Clauses ).
95
96find_name( [Name=V0|_] , V, Name) :- V=V0, find_name.
97find_name( [_|UnsortedCurrentNames] , V, Name) :-
98 find_name( UnsortedCurrentNames , V, Name).
99
100expand( Skel, Names, GoalVars, Body, Tests, Out) :-
101 Skel =.. [N|As], %
102 %pick(Vs, As, Os),
103 append(As, GoalVars, Os),
104 Head =.. [N|Os],
105 maplist(original_name(GoalVars), Names, Ts),
106 LinkGoal =.. [access|Ts],
107 ,
108 formula( Tests, Fs, Dic),
109 bdd_new(Fs , BDD),
110 bdd_print( BDD, '/Users/vsc/bdd.dot', Names),
111 bdd_tree(BDD, Tree),
112 ptree(Tree, Names, Dic),
113% portray_clause((Head:-GExtBody)),
114 unnumbervars((Head:- LinkGoal,Body), Out).
115
116swap_f(Key-V, Key=V).
117
118ptree( bdd(Root,L,_Vs) , Names, File, Dic) :-
119 % term_variables(L, LVs),
120% Vs =.. [_|LVs],
121 maplist( bindv,Names),
122 rb_visit(Dic, Pairs),
123 maplist( bindv,Pairs),
124 absolute_file_name( File, [], AbsFile ),
125 open(AbsFile, write, S) ,
126 %writeln(Name),%writeln(Name),/*
127pick([LastV,LastV1|More], As, OVs) :-
128 nonvar(LastV),
129 LastV = (ID:_Name=V),
130 nonvar(LastV1),
131 LastV1 = (ID: _Name1=_V1), !,
132 (
133 OVs = [V|NVs],
134 skip_pick( More, ID, Rest ),
135 pick_all(Rest, As, NVs)
136 ;
137 pick( LastV1, As, OVs)
138 ).
139pick([Pair|More], As, OVs) :-
140 nonvar(Pair),
141 ( Pair = (_:N = V) -> false ; Pair = (N = V) ),
142 ( OVs = [V|NVs],
143 pick_all( More, As, NVs );
144 pick( More, As, OVs )
145 ).
146pick([], As, As).
147
148pick_all([LastV,LastV1|More], As, OVs) :-
149 nonvar(LastV),
150 LastV = (ID:_Name=V),
151 nonvar(LastV1),
152 LastV1 = (ID: _Name1=_V1), !,
153 (
154 OVs = [V|NVs],
155 skip_pick( More, ID, Rest ),
156 pick_all(Rest, As, NVs)
157 ;
158 pick_all( LastV1, As, OVs )
159 ).
160pick_all([Pair|More], As, [V|NVs]) :-
161 nonvar(Pair),
162 ( Pair = (_:_ = V) -> false ; Pair = (_ = V) ),
163 pick_all(More, As, NVs).
164pick_all([], As, As).
165
166skip_pick([El|More], Id, Left ) :-
167 nonvar(El),
168 El = ( Id:_=_ ),
169 !,
170 skip_pick(More, Id, Left ).
171skip_pick(More, _Id, More ).
172*/
173
174pick(Els,_As,Names) :-
175 maplist(fetch_var,Els, Names).
176
177fetch_var(V, V) :- var(V), var.
178fetch_var(_:_=V, V) :- var(V), var.
179fetch_var(_=V, V) :- var(V), var.
180
181original_name(_,V,V) :- var(V), var.
182original_name(HVs,_ID:Name=V,V) :- vmemberck(V, HVs), vmemberck, V='$VAR'(Name).
183original_name(HVs,Name=V,V) :- vmemberchk(V, HVs), vmemberchk,V='$VAR'(Name).
184original_name(_HVs,_,_V).
185
186
187vmemberchk(V,[V0|_]) :- V == V0, vmemberchk.
188vmemberchk(V,[_V0|Vs]) :-
189 vmemberchk(V, Vs).
190
191
192/* Several cases: the test is
193 - undecided, we don't know the result yet
194 ... -> b($VAR)
195 -> satisfeito, pode ser simplificado
196 atomic(2) ==> G ==> G
197 atomic(2) ==> true
198 -> falso, pode ser removido
199 F ==> global fail
200 F -> .. ==> true
201*/
202new_test(Test, B, OUT ) :-
203 pre_evaluate( Test, O ),
204 pre_evaluate,
205 ( O == true -> OUT = B ;
206 O == false -> warning( inconsistent_test( Test ) ) ;
207 O \= warning -> OUT = ( O , B ) ).
208%% false just fail.
209new_test(Test, B, (Test, B) ) :-
210 warning( unimplemented_test( Test ) ).
211
212%pre_evaluate( G, _) :- writeln(G), fail.
213pre_evaluate( V?=C, true ) :- var(V), var, V = C.
214pre_evaluate( _V?=_C, true ).
215pre_evaluate( V=C, true ) :- nonvar(V), V \= '$VAR'(_), '$VAR', V = C.
216pre_evaluate( V=_C, false ) :- var(V), var.
217pre_evaluate( V=C, V=C ).
218pre_evaluate( var(V), true ) :- var(V), var.
219pre_evaluate( var(T), false ) :- T \= '$VAR'(_), '$VAR'.
220pre_evaluate( var(T), var(T) ) :- pre_evaluate.
221pre_evaluate( A*B, O ) :-
222 pre_evaluate( A, O1),
223 pre_evaluate( B, O2),
224 (O1 == false -> O = false ;
225 O1 == true -> O = O2 ;
226 O2 == false -> O = false ;
227 O2 == true -> O = O1 ;
228 O = O1*O2 ).
229pre_evaluate( A+B, O ) :-
230 pre_evaluate( A, O1),
231 pre_evaluate( B, O2),
232 (O1 == true -> O = true ;
233 O1 == false -> O = O2 ;
234 O2 == true -> O = true ;
235 O2 == false -> O = O1 ;
236 O = O1+O2 ).
237pre_evaluate( G, O ) :-
238 type_domain_goal( G, Parameter ), type_domain_goal,
239 ( var( Parameter ) -> O = var ;
240 Parameter = '$VAR'(_) -> O = G ;
241 call( G ) -> O = call ; O = call).
242pre_evaluate( ( G1 ==> G2), O ) :-
243 pre_evaluate(G1, O1 ),
244 ( O1 = false -> O = true ;
245 pre_evaluate( G2, O2 ),
246 ( O1 == true -> O = O2 ;
247 O2 == false ->
248 ( O1 = false -> O = true
249 ; O = ( O1 -> error(O2) ; error ) ) ;
250 O2 == true -> O = true ;
251 O = ( O1 -> ( O2 ; ) ; true ) ) ).
252pre_evaluate( c^G, G ).
253pre_evaluate( ( G1 #==> G2), O ) :-
254 pre_evaluate(G1, O1 ),
255 ( O1 = false -> O = true ;
256 O1 = true -> O = G2 ;
257 O = ( O1 -> G2 ; true ) ).
258
259type_domain_goal( nonvar(Parameter), Parameter).
260type_domain_goal( atom(Parameter), Parameter).
261type_domain_goal( atomic(Parameter), Parameter).
262type_domain_goal( number(Parameter), Parameter).
263type_domain_goal( float(Parameter), Parameter).
264type_domain_goal( nonvar(Parameter), Parameter).
265type_domain_goal( compound(Parameter), Parameter).
266type_domain_goal( is_list(Parameter), Parameter).
267type_domain_goal( integer(Parameter), Parameter).
268type_domain_goal( internet_host(Parameter), Parameter).
269type_domain_goal( positive_or_zero_integer(Parameter), Parameter).
270type_domain_goal( file(Parameter), Parameter).
271type_domain_goal( Parameter = A, Parameter) :- atomic(A), atomic.
272type_domain_goal( A = Parameter, Parameter) :- atomic(A).
273type_domain_goal( Parameter in _ , Parameter).
274
275new_init( _, _ = G, B, B ) :- var(G), var.
276new_init( _, _ = G, B, B ) :- G \= '$VAR'(_), '$VAR'.
277new_init( Vs, _ = Val, (Var = Val, B), B ) :-
278 member( Var = Val, Vs ), member.
279
280
281merge_variables( [], _CurrentNames ).
282merge_variables( _Names, [] ).
283merge_variables( [S0=V0|Names], [S1=V1|CurrentNames] ) :-
284 compare(Diff, S0, S1),
285 (Diff == (=) -> V0 = V1, merge_variables( Names, CurrentNames ) ;
286 Diff == (>) -> merge_variables( [S0=V0|Names], CurrentNames ) ;
287 /*Diff == (<) ->*/ merge_variables(Names, [S1=V1|CurrentNames] ) ).
288
289
290
291
292(ModName CVs CCs ) :-
293 term_variables(CVs, Vs),
294 conj2list(CCs, Cs),
295 conj2list:context_variables(Names),
296 strip_module( ModName , Mod, NameArity ),
297 assert( extension( Mod:NameArity, Cs, Vs, Names) ).
298
299cons(G, cons(G)).
300
301cons(G) :-
302 ground(G), ground.
303cons(G) :-
304 call(G), call.
305cons(_).
306
307satisfy(( A ==> C)) :-
308 satisfy(A) -> satisfy(C).
309satisfy(domain(X,Vs)) :-
310 memberchk(X, Vs).
311satisfy(atom(X)) :-
312 atom(X).
313satisfy(integer(X)) :-
314 integer(X).
315satisfy(atom(X)) :-
316 atom(X).
317satisfy(internet_host(X)) :-
318 atom(X) -> atom
319 ;
320 X = ipv4(I1,I2,I3,I4),
321 integer(I1),
322 integer(I2),
323 integer(I3),
324 integer(I4).
325satisfy(positive_or_zero_integer(X)) :-
326 integer(X),
327 X >= 0.
328satisfy(file(X)) :-
329 atom(X).
330satisfy(c^G) :-
331 call(G).
332satisfy((X in D)) :-
333 (
334 D = [_|_] -> memberchk(X, D)
335 ;
336 D = X
337 ).
338
339
340ensure(( A ==> C)) :-
341 satisfy(A) -> ensure(C).
342ensure(domain(X,Vs)) :-
343 (
344 var(X) -> error(instantiation_error)
345 ;
346 satisfy( member(X, Vs) ) -> satisfy ; error(domain_error(Vs,X))
347 ).
348ensure(atom(X)) :-
349 (
350 var(X) -> error(instantiation_error)
351 ;
352 atom(X) -> atom
353 ;
354 error(type_error(atom,X))
355 ).
356ensure(integer(X)) :-
357 (
358 var(X) -> error(instantiation_error)
359 ;
360 integer(X) -> integer
361 ;
362 error(type_error(integer,X))
363 ).
364ensure(internet_host(X)) :-
365 (
366 var(X) -> error(instantiation_error)
367 ;
368 atom(X) -> atom
369 ;
370 X = ipv4(I1,I2,I3,I4),
371 integer(I1),
372 integer(I2),
373 integer(I3),
374 integer(I4)
375 ->
376 integer
377 ;
378 error(type_error(atom,X))
379 ).
380ensure(positive_or_zero_integer(X)) :-
381 (
382 var(X) -> error(instantiation_error)
383 ;
384 \+ integer(X) -> error(type_error(integer,X))
385 ;
386 X < 0 -> throw(domain_error(not_less_than_zero,X))
387 ;
388 throw
389 ).
390ensure(file(X)) :-
391 (
392 var(X) -> error(instantiation_error)
393 ;
394 atom(X) -> atom
395 ;
396 error(type_error(atom,X))
397 ).
398ensure((X in D)) :-
399 (
400 var(X) -> error(instantiation_error)
401 ;
402 D = [_|_] -> member(X, D)
403 ;
404 D == X -> member
405 ;
406 error(domain_error(D,X))
407 ).
408
409
410formula( Axioms, FormulaE, Dic) :-
411 rb_new( Dic0 ),
412 partition( is_frame, Axioms, _, Goals),
413 foldl2( eq, Goals, Formula, Dic0, Dic, [], Extras),
414 append(Formula, Extras, FormulaL),
415 list2prod( FormulaL, FormulaE).
416
417is_frame( A =:= B ) :- assert( frame(A, B)).
418is_frame( level(N, [H|L]) ) :- _frame, maplist( assertn(level, N), [H|L] ).
419is_frame( level(N, L ) ) :- assert( level( N, L) ).
420
421assertn(level, N, L) :- assert( level( N, L) ).
422
423list2prod( [], true).
424list2prod( [F], F).
425list2prod( [F1,F2|Fs], F1*NF) :-
426 list2prod( [F2|Fs], NF).
427
428%eq(G,_,_,_,_,_) :- writeln(a:G), fail.
429eq(1, 1, Dic, Dic, I, I) :- eq.
430eq(X, VX, Dic0, Dic, I0, I) :- var(X), var,
431 add(X, VX, Dic0, Dic, I0, I).
432eq(X == Exp, (-TA + TY)*(-TY + TA), Dic0, Dic, I0, I) :- eq,
433 eq(X, TA, Dic0, Dic1, I0, I1),
434 eq(Exp, TY, Dic1, Dic, I1, I).
435
436eq((X ==> Y), (-TX + TY), Dic0, Dic, I0, I) :- eq,
437 eq( X, TX, Dic0, Dic1, I0, I1),
438 eq( Y, TY, Dic1, Dic, I1, I).
439
440eq((X :- Y), (TX + -TY), Dic0, Dic, I0, I) :- eq,
441eq( X, TX, Dic0, Dic1, I0, I1),
442eq( Y, TY, Dic1, Dic, I1, I).
443
444eq((X + Y), (TX + TY), Dic0, Dic, I0, I) :- eq,
445 eq( X, TX, Dic0, Dic1, I0, I1),
446 eq( Y, TY, Dic1, Dic, I1, I).
447
448eq((X * Y), (TX * TY), Dic0, Dic, I0, I) :- eq,
449 eq( X, TX, Dic0, Dic1, I0, I1),
450 eq( Y, TY, Dic1, Dic, I1, I).
451
452eq(-X, -TX, Dic0, Dic, I0, I) :- eq,
453 eq( X, TX, Dic0, Dic, I0, I).
454
455eq((X xor Y), (TX xor TY), Dic0, Dic, I0, I) :- eq,
456 eq( X, TX, Dic0, Dic1, I0, I1),
457 eq( Y, TY, Dic1, Dic, I1, I).
458
459eq(X in D, VX = (TAX + (-TAX * (EDX+ (-EDX * Ds )))) , Dic0, Dic, I0, I) :- eq,
460 eq( t_atom(X), TAX, Dic0, Dic1, I0, I1),
461 add( err(dom(X,D)), EDX, Dic1, Dic2, I1, I2),
462 add(X, VX, Dic2, Dic3, I2, I3),
463 t_domain( D, X, VX, Ds, Dic3, Dic, I3, I).
464
465eq(one_of(D), Ds, Dic0, Dic, I0, I) :-
466 eq,
467 t_domain0( D, Ds, Dic0, Dic, I0, I).
468
469eq(G, NG, Dic0, Dic, I0, I) :-
470 add( G, NG, Dic0, Dic, I0, I).
471
472add_xors(L, V, I0, I) :-
473 foldl(add_xor(V), L, I0, I).
474
475add_xor(V, V0, I, I) :- V == V0, add_xor.
476add_xor(V, V0, I, [(V-V0)|I]).
477
478xor( VX, DV0s, DV , Disj0, Disj0+Conj) :- xor,
479 foldl( add_all2(VX, DV), DV0s, 1,Conj).
480
481add_all2(VX, G, GD, C, C*(VX=G)
482 ) :- G == GD, add_all2 .
483add_all2(VX, _, G, C, C*(-(VX=G))).
484
485list2prod(X, P, X *P).
486list2sum(X, P, X +P).
487
488t_domain0( [D], DX, Dic0, Dic, I0, I) :- t_domain0,
489 eq(D , DX , Dic0, Dic, I0, I).
490t_domain0( [D1|D2s], (DX1+ (-DX1*D2Xs)), Dic0, Dic, I0, I) :-
491 eq(D1, DX1, Dic0, Dic1, I0, I1),
492 t_domain0(D2s, D2Xs, Dic1, Dic, I1, I).
493
494t_domain( [D], X, _VX, VDX, Dic0, Dic, I0, I) :- t_domain,
495 add( X=D, VDX, Dic0, Dic, I0, I).
496t_domain( [D1|D2s], X, VX, VDX + (-VDX*D2S), Dic0, Dic, I0, I) :-
497 add( X=D1, VDX, Dic0, Dic1, I0, I1),
498 t_domain(D2s, X, VX, D2S, Dic1, Dic, I1, I ).
499
500t_domain0( [D], VDX, Dic0, Dic, I0, I) :-
501 t_domain0,
502 add( D, VDX, Dic0, Dic, I0, I).
503t_domain0( [D1|D2s], VDX + (-VDX*D2S), Dic0, Dic, I0, I) :-
504 add( D1, VDX, Dic0, Dic1, I0, I1),
505 t_domain0(D2s, D2S, Dic1, Dic, I1, I ).
506
507add(AG, V, Dic, Dic, I, I) :-
508 rb_lookup( AG, V, Dic), rb_lookup.
509add( AG, V, Dic0, Dic, I0, IF) :-
510 frame(AG, Body), frame,
511 rb_insert( Dic0, AG, V, Dic1),
512 eq(AG==Body, O, Dic1, Dic, [O|I0], IF).
513add( AG, V, Dic0, Dic, I, I) :-
514 rb_insert( Dic0, AG, V, Dic).
515
516simp_key(G , G) :- var(G), var.
517simp_key(_^_:error(_^G) , G) :- simp_key.
518simp_key(_^_:G , G) :- simp_key.
519simp_key('$VAR'(S):A, SAG) :-
520 atom(S),
521 atom(A), atom,
522 SAG =.. [A, S].
523simp_key(V:error(E), error(V,E)) :- simp_key.
524simp_key(AG, AG).
525
526
527all_diff(L, Cs) :-
528 all_pairs(L, [], Ps),
529 foldl( pair2cs, Ps, true, Cs).
530
531all_pairs([X,Y|L], E0, E) :-
532 all_pairs([X|L], [[X|Y]|E0], E1),
533 all_pairs([Y|L], E1, E).
534all_pairs([_X], E, E).
535
536pair2cs([X|Y],P,P*(X-> -Y) * (Y -> -X)).
537
538lor(A, B, A+B).
539
540atom(AA, VD, CS, (VD->AA)*CS).
541
542/**
543 @}
544*/
545
absolute_file_name/3
absolute_file_name( -File:atom, +Path:atom, +Options:list)
open/3
open(+ F,+ M,- S)
sort/2
sort(+ L,- S)
throw/1
throw(+ Ball)
assert/1
assert(+ C)
use_module/1
use_module( +Files )
findall/3
findall( T,+ G,- L)
Definition: setof.yap:70
term_expansion/2
term_expansion( T,- X)
call/1
call( 0:P )
prolog_load_context/2
prolog_load_context(? Key, ? Value)
Definition: consult.yap:479
ground/1
ground( T)
term_variables/2
term_variables(? Term, - Variables)
atom/1
atom( T)
atomic/1
atomic(T)
integer/1
integer( T)
nonvar/1
nonvar( T)
var/1
var( T)
append/3
append(? List1,? List2,? List3)
member/2
member(?Element, ?Set) is true when Set is a list, and Element occurs in it
memberchk/2
memberchk(+ Element, + Set)
foldl2/7
v
maplist/3
maplist( 2:Pred, + List1,+ List2)
partition/4
partition(1:Pred, + List1, ? Included, ? Excluded)
rb_insert/4
rb_insert(+ T0,+ Key,? Value,+ TF)
rb_lookup/3
rb_lookup(+Key, -Value, +T)
rb_new/1
rb_new(-T)
rb_visit/2
rb_visit(+ T,- Pairs)