This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/library/parameters.yap
Vítor Santos Costa 55bd75b8d8 Merge branch 'master' of ssh://git.dcc.fc.up.pt/yap-6.3
Conflicts:
	library/parameters.yap
	packages/myddas/pl/myddas.ypp
2015-03-11 22:31:18 +00:00

571 lines
14 KiB
Prolog

:- module( parameters,
[such_that/2,
op(1060, xfx, such_that),
op(1050, xfx, extra_arguments),
op(1050, xfx, defaults),
op(700, xfx, in),
op(700, xfx, ?=), %initialization
op(750, xfy, #==>),
op(500, yfx, '<=>'),
op(500, yfx, '=>'),
op(800, yfx, '==>') ]
).
%%! @{
/**
@file parameters.yap
@defgroup parameter Automating test generation
@ingroup library
This library aims at facilitating test generation in a logic
program, namely when interfacing to foreign code. It introduces the
following specs:
- Named Arguments: you can refer to an argument through a name. This
allows having optional arguments. As an example, you can say:
maxlength=MaxLength
and the original program is extended to support an optional
parameter Length, eg:
vector( Type, Length, V ) :- alloc( Type, Length, MaxLength, V )
will become
vector( Type, Length, V, MaxLength ) :- alloc( Type, Length, MaxLength, V )
- Tests
You can write type tests and ISO-like tests offline.
- Initializers
It allows default code for variables. In the previous code, the
initializer MaxLength = 1024 would result in two clauses:
vector( Type, Length, V, MaxLength ) :-
alloc( Type, Length, MaxLength, V ).
vector( Type, Length, V ) :-
alloc( Type, Length, 1024, V ).
See myddas.yap for a few examples.
@author Vitor Santos Costa
*/
:- use_module( library(clauses),
[list2conj/2,
conj2list/2]).
:- use_module( library(maplist) ).
:- use_module( library(rbtrees) ).
:- use_module( library(lists) ).
:- use_module( library(bdd) ).
:- dynamic extension/4, init/2, frame/2, exclusive/0.
user:term_expansion(Term,Clauses) :-
Term = ( Spec :- Body),
prolog_load_context(module,Mod),
extension( Mod:Spec, Tests, GoalVars, Names),
hacks:context_variables(UnsortedCurrentNames),
sort( UnsortedCurrentNames, CurrentNames ),
merge_variables( Names, CurrentNames ),
findall( (Mod:ExtHead :- ExtBody),
expand( Spec, Names, GoalVars, Body, Tests, (ExtHead :- ExtBody)),
Clauses ).
find_name( [Name=V0|_] , V, Name) :- V=V0, !.
find_name( [_|UnsortedCurrentNames] , V, Name) :-
find_name( UnsortedCurrentNames , V, Name).
expand( Skel, Names, GoalVars, Body, Tests, Out) :-
Skel =.. [N|As], %
%pick(Vs, As, Os),
append(As, GoalVars, Os),
Head =.. [N|Os],
maplist(original_name(GoalVars), Names, Ts),
LinkGoal =.. [access|Ts],
trace,
formula( Tests, Fs, Dic),
bdd_new(Fs , BDD),
bdd_print( BDD, '/Users/vsc/bdd.dot', Names),
bdd_tree(BDD, Tree),
ptree(Tree, Names, Dic),
% portray_clause((Head:-GExtBody)),
unnumbervars((Head:- LinkGoal,Body), Out).
swap_f(Key-V, Key=V).
ptree( bdd(Root,L,_Vs) , Names, File, Dic) :-
% term_variables(L, LVs),
% Vs =.. [_|LVs],
maplist( bindv,Names),
rb_visit(Dic, Pairs),
maplist( bindv,Pairs),
absolute_file_name( File, [], AbsFile ),
open(AbsFile, write, S) ,
format(S,'digraph "DD" {
size = "7.5,10"
center = true;~n', []),
format(S,' "~w" [label = "~w"];~n', [1, Root]),
maplist( print_node(S), L),
format(S, '}~n', []),
close(S),
fail.
ptree(_, _, _).
bindv( X = '$VAR'(X) ) :- !.
bindv( X - '$VAR'(X) ) :- !.
bindv(_).
print_node(S,pp( Val, Name, Left, Right )) :-
%writeln(Name),
simplify(Name, N),
format(S,' "~w" [label = "~w"];~n', [Val, N]),
format(S,' "~w" -> "~w" [arrowType="none" color="red"] ;~n', [Val, Left]),
format(S,' "~w" -> "~w" [style = dashed arrowType="none"];~n', [Val, Right]).
print_node(S,pn( Val, Name, Left, Right )) :-
simplify(Name, N),
%writeln(Name),
format(S,' "~w" [label = "~w"];~n', [Val, N]),
format(S,' "~w" -> "~w" [arrowType="none" color="red"];~n', [Val,Left]),
( Right == 1 ->
format(S,' "~w" -> "0" [dir=none style = dotted];~n', [Val])
;
format(S,' "~w" -> "~w" [style = dotted type="odot"];~n', [Val, Right])
).
simplify(V,V) :- var(V),!.
simplify('$VAR'(X),Y) :- !, simplify(X,Y).
simplify(c^(X),Y) :- !, simplify(X,Y).
simplify(G, X:M) :- G=.. [X,N], !, simplify(N,M).
simplify(X, X).
/*
pick([LastV,LastV1|More], As, OVs) :-
nonvar(LastV),
LastV = (ID:_Name=V),
nonvar(LastV1),
LastV1 = (ID: _Name1=_V1), !,
(
OVs = [V|NVs],
skip_pick( More, ID, Rest ),
pick_all(Rest, As, NVs)
;
pick( LastV1, As, OVs)
).
pick([Pair|More], As, OVs) :-
nonvar(Pair),
( Pair = (_:N = V) -> false ; Pair = (N = V) ),
( OVs = [V|NVs],
pick_all( More, As, NVs );
pick( More, As, OVs )
).
pick([], As, As).
pick_all([LastV,LastV1|More], As, OVs) :-
nonvar(LastV),
LastV = (ID:_Name=V),
nonvar(LastV1),
LastV1 = (ID: _Name1=_V1), !,
(
OVs = [V|NVs],
skip_pick( More, ID, Rest ),
pick_all(Rest, As, NVs)
;
pick_all( LastV1, As, OVs )
).
pick_all([Pair|More], As, [V|NVs]) :-
nonvar(Pair),
( Pair = (_:_ = V) -> false ; Pair = (_ = V) ),
pick_all(More, As, NVs).
pick_all([], As, As).
skip_pick([El|More], Id, Left ) :-
nonvar(El),
El = ( Id:_=_ ),
!,
skip_pick(More, Id, Left ).
skip_pick(More, _Id, More ).
*/
pick(Els,_As,Names) :-
maplist(fetch_var,Els, Names).
fetch_var(V, V) :- var(V), !.
fetch_var(_:_=V, V) :- var(V), !.
fetch_var(_=V, V) :- var(V), !.
original_name(_,V,V) :- var(V), !.
original_name(HVs,_ID:Name=V,V) :- vmemberck(V, HVs), !, V='$VAR'(Name).
original_name(HVs,Name=V,V) :- vmemberchk(V, HVs), !,V='$VAR'(Name).
original_name(_HVs,_,_V).
vmemberchk(V,[V0|_]) :- V == V0, !.
vmemberchk(V,[_V0|Vs]) :-
vmemberchk(V, Vs).
/* Several cases: the test is
- undecided, we don't know the result yet
... -> b($VAR)
-> satisfeito, pode ser simplificado
atomic(2) ==> G ==> G
atomic(2) ==> true
-> falso, pode ser removido
F ==> global fail
F -> .. ==> true
*/
new_test(Test, B, OUT ) :-
pre_evaluate( Test, O ),
!,
( O == true -> OUT = B ;
O == false -> warning( inconsistent_test( Test ) ) ;
O \= false -> OUT = ( O , B ) ).
%% false just fail.
new_test(Test, B, (Test, B) ) :-
warning( unimplemented_test( Test ) ).
%pre_evaluate( G, _) :- writeln(G), fail.
pre_evaluate( V?=C, true ) :- var(V), !, V = C.
pre_evaluate( _V?=_C, true ).
pre_evaluate( V=C, true ) :- nonvar(V), V \= '$VAR'(_), !, V = C.
pre_evaluate( V=_C, false ) :- var(V), !.
pre_evaluate( V=C, V=C ).
pre_evaluate( var(V), true ) :- var(V), !.
pre_evaluate( var(T), false ) :- T \= '$VAR'(_), !.
pre_evaluate( var(T), var(T) ) :- !.
pre_evaluate( A*B, O ) :-
pre_evaluate( A, O1),
pre_evaluate( B, O2),
(O1 == false -> O = false ;
O1 == true -> O = O2 ;
O2 == false -> O = false ;
O2 == true -> O = O1 ;
O = O1*O2 ).
pre_evaluate( A+B, O ) :-
pre_evaluate( A, O1),
pre_evaluate( B, O2),
(O1 == true -> O = true ;
O1 == false -> O = O2 ;
O2 == true -> O = true ;
O2 == false -> O = O1 ;
O = O1+O2 ).
pre_evaluate( G, O ) :-
type_domain_goal( G, Parameter ), !,
( var( Parameter ) -> O = false ;
Parameter = '$VAR'(_) -> O = G ;
call( G ) -> O = true ; O = false).
pre_evaluate( ( G1 ==> G2), O ) :-
pre_evaluate(G1, O1 ),
( O1 = false -> O = true ;
pre_evaluate( G2, O2 ),
( O1 == true -> O = O2 ;
O2 == false ->
( O1 = false -> O = true
; O = ( O1 -> error(O2) ; true ) ) ;
O2 == true -> O = true ;
O = ( O1 -> ( O2 ; false ) ; true ) ) ).
pre_evaluate( c^G, G ).
pre_evaluate( ( G1 #==> G2), O ) :-
pre_evaluate(G1, O1 ),
( O1 = false -> O = true ;
O1 = true -> O = G2 ;
O = ( O1 -> G2 ; true ) ).
type_domain_goal( nonvar(Parameter), Parameter).
type_domain_goal( atom(Parameter), Parameter).
type_domain_goal( atomic(Parameter), Parameter).
type_domain_goal( number(Parameter), Parameter).
type_domain_goal( float(Parameter), Parameter).
type_domain_goal( nonvar(Parameter), Parameter).
type_domain_goal( compound(Parameter), Parameter).
type_domain_goal( is_list(Parameter), Parameter).
type_domain_goal( integer(Parameter), Parameter).
type_domain_goal( internet_host(Parameter), Parameter).
type_domain_goal( positive_or_zero_integer(Parameter), Parameter).
type_domain_goal( file(Parameter), Parameter).
type_domain_goal( Parameter = A, Parameter) :- atomic(A), !.
type_domain_goal( A = Parameter, Parameter) :- atomic(A).
type_domain_goal( Parameter in _ , Parameter).
new_init( _, _ = G, B, B ) :- var(G), !.
new_init( _, _ = G, B, B ) :- G \= '$VAR'(_), !.
new_init( Vs, _ = Val, (Var = Val, B), B ) :-
member( Var = Val, Vs ), !.
merge_variables( [], _CurrentNames ).
merge_variables( _Names, [] ).
merge_variables( [S0=V0|Names], [S1=V1|CurrentNames] ) :-
compare(Diff, S0, S1),
(Diff == (=) -> V0 = V1, merge_variables( Names, CurrentNames ) ;
Diff == (>) -> merge_variables( [S0=V0|Names], CurrentNames ) ;
/*Diff == (<) ->*/ merge_variables(Names, [S1=V1|CurrentNames] ) ).
(ModName extra_arguments CVs such_that CCs ) :-
term_variables(CVs, Vs),
conj2list(CCs, Cs),
hacks:context_variables(Names),
strip_module( ModName , Mod, NameArity ),
assert( extension( Mod:NameArity, Cs, Vs, Names) ).
cons(G, cons(G)).
cons(G) :-
ground(G), !.
cons(G) :-
call(G), !.
cons(_).
satisfy(( A ==> C)) :-
satisfy(A) -> satisfy(C).
satisfy(domain(X,Vs)) :-
memberchk(X, Vs).
satisfy(atom(X)) :-
atom(X).
satisfy(integer(X)) :-
integer(X).
satisfy(atom(X)) :-
atom(X).
satisfy(internet_host(X)) :-
atom(X) -> true
;
X = ipv4(I1,I2,I3,I4),
integer(I1),
integer(I2),
integer(I3),
integer(I4).
satisfy(positive_or_zero_integer(X)) :-
integer(X),
X >= 0.
satisfy(file(X)) :-
atom(X).
satisfy(c^G) :-
call(G).
satisfy((X in D)) :-
(
D = [_|_] -> memberchk(X, D)
;
D = X
).
ensure(( A ==> C)) :-
satisfy(A) -> ensure(C).
ensure(domain(X,Vs)) :-
(
var(X) -> error(instantiation_error)
;
satisfy( member(X, Vs) ) -> true ; error(domain_error(Vs,X))
).
ensure(atom(X)) :-
(
var(X) -> error(instantiation_error)
;
atom(X) -> true
;
error(type_error(atom,X))
).
ensure(integer(X)) :-
(
var(X) -> error(instantiation_error)
;
integer(X) -> true
;
error(type_error(integer,X))
).
ensure(internet_host(X)) :-
(
var(X) -> error(instantiation_error)
;
atom(X) -> true
;
X = ipv4(I1,I2,I3,I4),
integer(I1),
integer(I2),
integer(I3),
integer(I4)
->
true
;
error(type_error(atom,X))
).
ensure(positive_or_zero_integer(X)) :-
(
var(X) -> error(instantiation_error)
;
\+ integer(X) -> error(type_error(integer,X))
;
X < 0 -> throw(domain_error(not_less_than_zero,X))
;
true
).
ensure(file(X)) :-
(
var(X) -> error(instantiation_error)
;
atom(X) -> true
;
error(type_error(atom,X))
).
ensure((X in D)) :-
(
var(X) -> error(instantiation_error)
;
D = [_|_] -> member(X, D)
;
D == X -> true
;
error(domain_error(D,X))
).
formula( Axioms, FormulaE, Dic) :-
rb_new( Dic0 ),
partition( is_frame, Axioms, _, Goals),
foldl2( eq, Goals, Formula, Dic0, Dic, [], Extras),
append(Formula, Extras, FormulaL),
list2prod( FormulaL, FormulaE).
is_frame( A =:= B ) :- assert( frame(A, B)).
is_frame( level(N, [H|L]) ) :- !, maplist( assertn(level, N), [H|L] ).
is_frame( level(N, L ) ) :- assert( level( N, L) ).
assertn(level, N, L) :- assert( level( N, L) ).
list2prod( [], true).
list2prod( [F], F).
list2prod( [F1,F2|Fs], F1*NF) :-
list2prod( [F2|Fs], NF).
%eq(G,_,_,_,_,_) :- writeln(a:G), fail.
eq(1, 1, Dic, Dic, I, I) :- !.
eq(X, VX, Dic0, Dic, I0, I) :- var(X), !,
add(X, VX, Dic0, Dic, I0, I).
eq(X == Exp, (-TA + TY)*(-TY + TA), Dic0, Dic, I0, I) :- !,
eq(X, TA, Dic0, Dic1, I0, I1),
eq(Exp, TY, Dic1, Dic, I1, I).
eq((X ==> Y), (-TX + TY), Dic0, Dic, I0, I) :- !,
eq( X, TX, Dic0, Dic1, I0, I1),
eq( Y, TY, Dic1, Dic, I1, I).
eq((X :- Y), (TX + -TY), Dic0, Dic, I0, I) :- !,
eq( X, TX, Dic0, Dic1, I0, I1),
eq( Y, TY, Dic1, Dic, I1, I).
eq((X + Y), (TX + TY), Dic0, Dic, I0, I) :- !,
eq( X, TX, Dic0, Dic1, I0, I1),
eq( Y, TY, Dic1, Dic, I1, I).
eq((X * Y), (TX * TY), Dic0, Dic, I0, I) :- !,
eq( X, TX, Dic0, Dic1, I0, I1),
eq( Y, TY, Dic1, Dic, I1, I).
eq(-X, -TX, Dic0, Dic, I0, I) :- !,
eq( X, TX, Dic0, Dic, I0, I).
eq((X xor Y), (TX xor TY), Dic0, Dic, I0, I) :- !,
eq( X, TX, Dic0, Dic1, I0, I1),
eq( Y, TY, Dic1, Dic, I1, I).
eq(X in D, VX = (TAX + (-TAX * (EDX+ (-EDX * Ds )))) , Dic0, Dic, I0, I) :- !,
eq( t_atom(X), TAX, Dic0, Dic1, I0, I1),
add( err(dom(X,D)), EDX, Dic1, Dic2, I1, I2),
add(X, VX, Dic2, Dic3, I2, I3),
t_domain( D, X, VX, Ds, Dic3, Dic, I3, I).
eq(one_of(D), Ds, Dic0, Dic, I0, I) :-
!,
t_domain0( D, Ds, Dic0, Dic, I0, I).
eq(G, NG, Dic0, Dic, I0, I) :-
add( G, NG, Dic0, Dic, I0, I).
add_xors(L, V, I0, I) :-
foldl(add_xor(V), L, I0, I).
add_xor(V, V0, I, I) :- V == V0, !.
add_xor(V, V0, I, [(V-V0)|I]).
xor( VX, DV0s, DV , Disj0, Disj0+Conj) :- !,
foldl( add_all2(VX, DV), DV0s, 1,Conj).
add_all2(VX, G, GD, C, C*(VX=G)
) :- G == GD, ! .
add_all2(VX, _, G, C, C*(-(VX=G))).
list2prod(X, P, X *P).
list2sum(X, P, X +P).
t_domain0( [D], DX, Dic0, Dic, I0, I) :- !,
eq(D , DX , Dic0, Dic, I0, I).
t_domain0( [D1|D2s], (DX1+ (-DX1*D2Xs)), Dic0, Dic, I0, I) :-
eq(D1, DX1, Dic0, Dic1, I0, I1),
t_domain0(D2s, D2Xs, Dic1, Dic, I1, I).
t_domain( [D], X, _VX, VDX, Dic0, Dic, I0, I) :- !,
add( X=D, VDX, Dic0, Dic, I0, I).
t_domain( [D1|D2s], X, VX, VDX + (-VDX*D2S), Dic0, Dic, I0, I) :-
add( X=D1, VDX, Dic0, Dic1, I0, I1),
t_domain(D2s, X, VX, D2S, Dic1, Dic, I1, I ).
t_domain0( [D], VDX, Dic0, Dic, I0, I) :-
!,
add( D, VDX, Dic0, Dic, I0, I).
t_domain0( [D1|D2s], VDX + (-VDX*D2S), Dic0, Dic, I0, I) :-
add( D1, VDX, Dic0, Dic1, I0, I1),
t_domain0(D2s, D2S, Dic1, Dic, I1, I ).
add(AG, V, Dic, Dic, I, I) :-
rb_lookup( AG, V, Dic), !.
add( AG, V, Dic0, Dic, I0, IF) :-
frame(AG, Body), !,
rb_insert( Dic0, AG, V, Dic1),
eq(AG==Body, O, Dic1, Dic, [O|I0], IF).
add( AG, V, Dic0, Dic, I, I) :-
rb_insert( Dic0, AG, V, Dic).
simp_key(G , G) :- var(G), !.
simp_key(_^_:error(_^G) , G) :- !.
simp_key(_^_:G , G) :- !.
simp_key('$VAR'(S):A, SAG) :-
atom(S),
atom(A), !,
SAG =.. [A, S].
simp_key(V:error(E), error(V,E)) :- !.
simp_key(AG, AG).
all_diff(L, Cs) :-
all_pairs(L, [], Ps),
foldl( pair2cs, Ps, true, Cs).
all_pairs([X,Y|L], E0, E) :-
all_pairs([X|L], [[X|Y]|E0], E1),
all_pairs([Y|L], E1, E).
all_pairs([_X], E, E).
pair2cs([X|Y],P,P*(X-> -Y) * (Y -> -X)).
lor(A, B, A+B).
atom(AA, VD, CS, (VD->AA)*CS).