From 5ea3fcd08f4f7917a08dd60b1688179fbb042cb3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?V=C3=ADtor=20Santos=20Costa?= Date: Wed, 4 Mar 2015 09:52:34 +0000 Subject: [PATCH] men at work --- library/parameters.yap | 526 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 526 insertions(+) create mode 100644 library/parameters.yap diff --git a/library/parameters.yap b/library/parameters.yap new file mode 100644 index 000000000..1e74b7b88 --- /dev/null +++ b/library/parameters.yap @@ -0,0 +1,526 @@ + +:- 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. + +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), + trace, + append(As, GoalVars, Os), + Head =.. [N|Os], + maplist(original_name(GoalVars), Names, Ts), + LinkGoal =.. [access|Ts], + 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). + +ptree( bdd(_,L,_Vs) , Names, Dic) :- +% term_variables(L, LVs), +% Vs =.. [_|LVs], +% trace, +maplist( bindv,Names), + rb_visit(Dic, Pairs), + maplist( bindv,Pairs), + open('bdd.dot', write, S) , + format(S,'digraph "DD" { + size = "7.5,10" + center = true;~n', []), + maplist( print_node(S), L), + format(S, '}~n', []), + close(S), + fail. +ptree(_, _, _). + +bindv( X = '$VAR'(X) ). +bindv( X - '$VAR'(X) ). + +print_node(S,pp( Val, Name, Left, Right )) :- + simplify(Name, N), + format(S,' "~w" [label = "~w"];~n', [Val, N]), + format(S,' "~w" -> "~w";~n', [Val, Right]), + format(S,' "~w" -> "~w" [style = dashed];~n', [Val, Left]). +print_node(S,pn( Val, Name, Left, Right )) :- + simplify(Name, N), + format(S,' "~w" [label = "~w"];~n', [Val, N]), + format(S,' "~w" -> "~w";~n', [Val, Right]), + format(S,' "~w" -> "~w" [style = dashed];~n', [Val, Left]). + +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_init, Axioms, _Inits, OGoals), + partition( is_frame, OGoals, _Frames, Goals), + foldl2( eq, Goals, Formula, Dic0, Dic, [], Extras), + append(Formula, Extras, FormulaL), + maplist(writeln,FormulaL), + list2prod( FormulaL, FormulaE). + +is_init( A ?= B ) :- assert(init(A, B)). + +is_frame( A =:= B ) :- assert( frame(A, B)). + +list2prod( [], true). +list2prod( [F], F). +list2prod( [F1,F2|Fs], F1*NF) :- + list2prod( [F2|Fs], NF). + +%eq(G,_,_,_,_,_) :- writeln(a:G), fail. +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, 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, VX, Ds, Dic3, Dic, I3, I). + +eq(G, NG, Dic0, Dic, I0, I) :- + add( G, NG, Dic0, Dic, I0, I). + +t_domain( [D], VX, VD = VX, Dic0, Dic, I0, I) :- !, + add(D, VD, Dic0, Dic, I0, I). +t_domain( [D1|D2s], (VX==VX=D)* + D2S, _, Dic0, Dic, I0, I) :- + add( X=D1, VDX, Dic0, Dic1, I0, I1), + add( X, VX, Dic0, Dic1, I0, I1), + maplist(diff(XD1), D2s, Dic1, Dic, I1, I), + t_domain(D2S, X, ). + +diff(XD, DO, Dic0, Dic, [-XD*VDO+ (XD * -VDO)|I0], I) :- + new(DO, VDO, Dic0, Dic, I0, 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(_^_: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).