diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
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.
17dad3f6f7
yap-6.3/CLPQR/clpr/nf.yap
vsc 164980a931 new files 
git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@179 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
2001-11-15 17:17:54 +00:00

836 lines
20 KiB
Prolog
Raw Blame History

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% clp(q,r) version 1.3.3 %
% %
% (c) Copyright 1992,1993,1994,1995 %
% Austrian Research Institute for Artificial Intelligence (OFAI) %
% Schottengasse 3 %
% A-1010 Vienna, Austria %
% %
% File: nf.pl %
% Author: Christian Holzbaur christian@ai.univie.ac.at %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- use_module( library(terms), [term_variables/2]).
:- use_module( geler).
% -------------------------------------------------------------------------
{ Rel } :- var( Rel), !, raise_exception(instantiation_error({Rel},1)).
{ R,Rs } :- !, {R}, {Rs}.
{ R;Rs } :- !, ({R} ; {Rs}). % for entailment checking
{ L < R } :- !, nf( L-R, Nf), submit_lt( Nf).
{ L > R } :- !, nf( R-L, Nf), submit_lt( Nf).
{ L =< R } :- !, nf( L-R, Nf), submit_le( Nf).
{ <=(L,R) } :- !, nf( L-R, Nf), submit_le( Nf).
{ L >= R } :- !, nf( R-L, Nf), submit_le( Nf).
{ L =\= R } :- !, nf( L-R, Nf), submit_ne( Nf).
{ L =:= R } :- !, nf( L-R, Nf), submit_eq( Nf).
{ L = R } :- !, nf( L-R, Nf), submit_eq( Nf).
{ Rel } :- raise_exception( type_error({Rel},1,'a constraint',Rel)).
%
% s -> c = ~s v c = ~(s /\ ~c)
% where s is the store and c is the constraint for which
% we want to know whether it is entailed.
%
entailed( C) :-
negate( C, Cn),
\+ { Cn }.
negate( Rel, _) :- var( Rel), !, raise_exception(instantiation_error(entailed(Rel),1)).
negate( (A,B), (Na;Nb)) :- !, negate( A, Na), negate( B, Nb).
negate( (A;B), (Na,Nb)) :- !, negate( A, Na), negate( B, Nb).
negate( A<B, A>=B) :- !.
negate( A>B, A=<B) :- !.
negate( A=<B, A>B) :- !.
negate( A>=B, A<B) :- !.
negate( A=:=B, A=\=B) :- !.
negate( A=B, A=\=B) :- !.
negate( A=\=B, A=:=B) :- !.
negate( Rel, _) :- raise_exception( type_error(entailed(Rel),1,'a constraint',Rel)).
/*
Cases: a) Nf=[]
b) Nf=[A]
b1) A=k
b2) invertible(A)
b3) linear -> A=0
b4) nonlinear -> geler
c) Nf=[A,B|Rest]
c1) A=k
c11) B=X^+-1, Rest=[] -> B=
c12) invertible(A,B)
c13) linear(B|Rest)
c14) geler
c2) linear(Nf)
c3) nonlinear -> geler
*/
submit_eq( []). % trivial success
submit_eq( [T|Ts]) :-
submit_eq( Ts, T).
submit_eq( [], A) :- submit_eq_b( A).
submit_eq( [B|Bs], A) :- submit_eq_c( A, B, Bs).
submit_eq_b( v(_,[])) :- !, fail. % b1: trivial failure
submit_eq_b( v(_,[X^P])) :- % b2,b3: n*x^p=0 -> x=0
var( X),
P > 0,
!,
arith_eval( 0, Z),
export_binding( X, Z).
submit_eq_b( v(_,[NL^1])) :- % b2
nonvar( NL),
arith_eval( 0, Z),
nl_invertible( NL, X, Z, Inv),
!,
nf( -Inv, S),
nf_add( X, S, New),
submit_eq( New).
submit_eq_b( Term) :- % b4
term_variables( Term, Vs),
geler( Vs, resubmit_eq([Term])).
submit_eq_c( v(I,[]), B, Rest) :- !,
submit_eq_c1( Rest, B, I).
submit_eq_c( A, B, Rest) :- % c2
A=v(_,[X^1]), var(X),
B=v(_,[Y^1]), var(Y),
linear( Rest),
!,
Hom = [A,B|Rest],
% 'solve_='( Hom).
nf_length( Hom, 0, Len),
log_deref( Len, Hom, [], HomD),
solve( HomD).
submit_eq_c( A, B, Rest) :- % c3
Norm = [A,B|Rest],
term_variables( Norm, Vs),
geler( Vs, resubmit_eq(Norm)).
submit_eq_c1( [], v(K,[X^P]), I) :- % c11
var( X),
( P = 1, !, arith_eval( -I/K, Val), export_binding( X, Val)
; P = -1, !, arith_eval( -K/I, Val), export_binding( X, Val)
).
submit_eq_c1( [], v(K,[NL^P]), I) :- % c12
nonvar( NL),
( P = 1, arith_eval( -I/K, Y)
; P = -1, arith_eval( -K/I, Y)
),
nl_invertible( NL, X, Y, Inv),
!,
nf( -Inv, S),
nf_add( X, S, New),
submit_eq( New).
submit_eq_c1( Rest, B, I) :- % c13
B=v(_,[Y^1]), var(Y),
linear( Rest),
!,
% 'solve_='( [v(I,[]),B|Rest]).
Hom = [B|Rest],
nf_length( Hom, 0, Len),
normalize_scalar( I, Nonvar),
log_deref( Len, Hom, [], HomD),
add_linear_11( Nonvar, HomD, LinD),
solve( LinD).
submit_eq_c1( Rest, B, I) :- % c14
Norm = [v(I,[]),B|Rest],
term_variables( Norm, Vs),
geler( Vs, resubmit_eq(Norm)).
% -----------------------------------------------------------------------
submit_lt( []) :- fail. % trivial failure
submit_lt( [A|As]) :-
submit_lt( As, A).
submit_lt( [], v(K,P)) :- submit_lt_b( P, K).
submit_lt( [B|Bs], A) :- submit_lt_c( Bs, A, B).
submit_lt_b( [], I) :- !, arith_eval( I<0).
submit_lt_b( [X^1], K) :-
var(X),
!,
( arith_eval( K>0) ->
ineq_one_s_p_0( X)
;
ineq_one_s_n_0( X)
).
submit_lt_b( P, K) :-
term_variables( P, Vs),
geler( Vs, resubmit_lt([v(K,P)])).
submit_lt_c( [], A, B) :-
A=v(I,[]),
B=v(K,[Y^1]), var(Y),
!,
ineq_one( strict, Y, K, I).
submit_lt_c( Rest, A, B) :-
Norm = [A,B|Rest],
( linear(Norm) ->
'solve_<'( Norm)
;
term_variables( Norm, Vs),
geler( Vs, resubmit_lt(Norm))
).
submit_le( []). % trivial success
submit_le( [A|As]) :-
submit_le( As, A).
submit_le( [], v(K,P)) :- submit_le_b( P, K).
submit_le( [B|Bs], A) :- submit_le_c( Bs, A, B).
submit_le_b( [], I) :- !, arith_eval( I=<0).
submit_le_b( [X^1], K) :-
var(X),
!,
( arith_eval( K>0) ->
ineq_one_n_p_0( X)
;
ineq_one_n_n_0( X)
).
submit_le_b( P, K) :-
term_variables( P, Vs),
geler( Vs, resubmit_le([v(K,P)])).
submit_le_c( [], A, B) :-
A=v(I,[]),
B=v(K,[Y^1]), var(Y),
!,
ineq_one( nonstrict, Y, K, I).
submit_le_c( Rest, A, B) :-
Norm = [A,B|Rest],
( linear(Norm) ->
'solve_=<'( Norm)
;
term_variables( Norm, Vs),
geler( Vs, resubmit_le(Norm))
).
submit_ne( Norm1) :-
( nf_constant( Norm1, K) ->
arith_eval( K=\=0)
; linear( Norm1) ->
'solve_=\\='( Norm1)
;
term_variables( Norm1, Vs),
geler( Vs, resubmit_ne(Norm1))
).
linear( []).
linear( v(_,Ps)) :- linear_ps( Ps).
linear( [A|As]) :-
linear( A),
linear( As).
linear_ps( []).
linear_ps( [V^1]) :- var( V). % excludes sin(_), ...
%
% Goal delays until Term gets linear.
% At this time, Var will be bound to the normalform of Term.
%
:- meta_predicate wait_linear( ?, ?, :).
%
wait_linear( Term, Var, Goal) :-
nf( Term, Nf),
( linear( Nf) ->
Var = Nf,
call( Goal)
;
term_variables( Nf, Vars),
geler( Vars, wait_linear_retry(Nf,Var,Goal))
).
%
% geler clients
%
resubmit_eq( N) :-
repair( N, Norm),
submit_eq( Norm).
resubmit_lt( N) :-
repair( N, Norm),
submit_lt( Norm).
resubmit_le( N) :-
repair( N, Norm),
submit_le( Norm).
resubmit_ne( N) :-
repair( N, Norm),
submit_ne( Norm).
wait_linear_retry( Nf0, Var, Goal) :-
repair( Nf0, Nf),
( linear( Nf) ->
Var = Nf,
call( Goal)
;
term_variables( Nf, Vars),
geler( Vars, wait_linear_retry(Nf,Var,Goal))
).
% -----------------------------------------------------------------------
/*
invertible( [v(Mone,[]),v(One,[X^Px,Y^Py])], Norm) :-
Px+Py =:= 0,
abs(Px) mod 2 =:= 1, % odd powers only ...
arith_eval( 1, One),
arith_eval( -1, Mone),
!,
( Px < 0 ->
{X=\=0}
;
{Y=\=0}
),
nf( X-Y, Norm). % x=y
*/
nl_invertible( sin(X), X, Y, Res) :- arith_eval( asin(Y), Res).
nl_invertible( cos(X), X, Y, Res) :- arith_eval( acos(Y), Res).
nl_invertible( tan(X), X, Y, Res) :- arith_eval( atan(Y), Res).
nl_invertible( exp(B,C), X, A, Res) :-
( nf_constant( B, Kb) ->
arith_eval(A>0),
arith_eval(Kb>0),
arith_eval(Kb=\=1),
X = C,
arith_eval( log(A)/log(Kb), Res)
; nf_constant( C, Kc),
\+ (arith_eval(A=:=0),arith_eval(Kc=<0)),
X = B,
arith_eval( exp(A,1/Kc), Res)
).
% -----------------------------------------------------------------------
nf( X, Norm) :- var(X), !,
Norm = [v(One,[X^1])],
arith_eval( 1, One).
nf( X, Norm) :- number(X), !,
nf_number( X, Norm).
%
nf( rat(N,D), Norm) :- !,
nf_number( rat(N,D), Norm).
%
nf( #(Const), Norm) :-
monash_constant( Const, Value),
!,
( arith_eval( 1, rat(1,1)) ->
nf_number( Value, Norm) % swallows #(zero) ... ok in Q
;
arith_normalize( Value, N), % in R we want it
Norm = [v(N,[])]
).
%
nf( -A, Norm) :- !,
nf( A, An),
arith_eval( -1, K),
nf_mul_factor( v(K,[]), An, Norm).
nf( +A, Norm) :- !,
nf( A, Norm).
%
nf( A+B, Norm) :- !,
nf( A, An),
nf( B, Bn),
nf_add( An, Bn, Norm).
nf( A-B, Norm) :- !,
nf( A, An),
nf( -B, Bn),
nf_add( An, Bn, Norm).
%
nf( A*B, Norm) :- !,
nf( A, An),
nf( B, Bn),
nf_mul( An, Bn, Norm).
nf( A/B, Norm) :- !,
nf( A, An),
nf( B, Bn),
nf_div( Bn, An, Norm).
%
nf( Term, Norm) :-
nonlin_1( Term, Arg, Skel, Sa1),
!,
nf( Arg, An),
nf_nonlin_1( Skel, An, Sa1, Norm).
nf( Term, Norm) :-
nonlin_2( Term, A1,A2, Skel, Sa1, Sa2),
!,
nf( A1, A1n),
nf( A2, A2n),
nf_nonlin_2( Skel, A1n, A2n, Sa1, Sa2, Norm).
%
nf( Term, _) :-
raise_exception( type_error(nf(Term,_),1,'a numeric expression',Term)).
nf_number( N, Res) :-
nf_number( N),
arith_normalize( N, Normal),
( arith_eval( Normal=:=0) ->
Res = []
;
Res = [v(Normal,[])]
).
nf_number( N) :- number( N),
!. /* MC 980507 */
nf_number( N) :- compound( N), N=rat(_,_). % sicstus
nonlin_1( abs(X), X, abs(Y), Y).
nonlin_1( sin(X), X, sin(Y), Y).
nonlin_1( cos(X), X, cos(Y), Y).
nonlin_1( tan(X), X, tan(Y), Y).
nonlin_2( min(A,B), A,B, min(X,Y), X, Y).
nonlin_2( max(A,B), A,B, max(X,Y), X, Y).
nonlin_2( exp(A,B), A,B, exp(X,Y), X, Y).
nonlin_2( pow(A,B), A,B, exp(X,Y), X, Y). % pow->exp
nonlin_2( A^B, A,B, exp(X,Y), X, Y).
nf_nonlin_1( Skel, An, S1, Norm) :-
( nf_constant( An, S1) ->
nl_eval( Skel, Res),
nf_number( Res, Norm)
;
S1 = An,
arith_eval( 1, One),
Norm = [v(One,[Skel^1])]
).
nf_nonlin_2( Skel, A1n, A2n, S1, S2, Norm) :-
( nf_constant( A1n, S1),
nf_constant( A2n, S2) ->
nl_eval( Skel, Res),
nf_number( Res, Norm)
; Skel=exp(_,_),
nf_constant( A2n, Exp),
integerp( Exp, I) ->
nf_power( I, A1n, Norm)
;
S1 = A1n,
S2 = A2n,
arith_eval( 1, One),
Norm = [v(One,[Skel^1])]
).
nl_eval( abs(X), R) :- arith_eval( abs(X), R).
nl_eval( sin(X), R) :- arith_eval( sin(X), R).
nl_eval( cos(X), R) :- arith_eval( cos(X), R).
nl_eval( tan(X), R) :- arith_eval( tan(X), R).
%
nl_eval( min(X,Y), R) :- arith_eval( min(X,Y), R).
nl_eval( max(X,Y), R) :- arith_eval( max(X,Y), R).
nl_eval( exp(X,Y), R) :- arith_eval( exp(X,Y), R).
monash_constant( X, _) :- var(X), !, fail.
monash_constant( p, 3.14259265).
monash_constant( pi, 3.14259265).
monash_constant( e, 2.71828182).
monash_constant( zero, Eps) :- arith_eps( Eps).
%
% check if a Nf consists of just a constant
%
nf_constant( [], Z) :- arith_eval( 0, Z).
nf_constant( [v(K,[])], K).
%
% this depends on the polynf ordering, i.e. [] < [X^1] ...
%
split( [], [], Z) :- arith_eval( 0, Z).
split( [First|T], H, I) :-
( First=v(I,[]) ->
H=T
;
arith_eval( 0, I),
H = [First|T]
).
%
% runtime predicate
%
%:- mode nf_add( +, +, ?).
%
nf_add( [], Bs, Bs).
nf_add( [A|As], Bs, Cs) :-
nf_add( Bs, A, As, Cs).
%:- mode nf_add( +, +, +, ?).
%
nf_add( [], A, As, Cs) :- Cs = [A|As].
nf_add( [B|Bs], A, As, Cs) :-
A = v(Ka,Pa),
B = v(Kb,Pb),
compare( Rel, Pa, Pb),
nf_add_case( Rel, A, As, Cs, B, Bs, Ka, Kb, Pa).
%:- mode nf_add_case( +, +, +, -, +, +, +, +, +).
%
nf_add_case( <, A, As, Cs, B, Bs, _, _, _) :-
Cs=[A|Rest],
nf_add( As, B, Bs, Rest).
nf_add_case( >, A, As, Cs, B, Bs, _, _, _) :-
Cs=[B|Rest],
nf_add( Bs, A, As, Rest).
nf_add_case( =, _, As, Cs, _, Bs, Ka, Kb, Pa) :-
arith_eval( Ka+Kb, Kc),
( arith_eval( Kc=:=0 ) ->
nf_add( As, Bs, Cs)
;
Cs=[v(Kc,Pa)|Rest],
nf_add( As, Bs, Rest)
).
%:- mode nf_mul( +, +, -).
%
nf_mul( A, B, Res) :-
nf_length( A, 0, LenA),
nf_length( B, 0, LenB),
nf_mul_log( LenA, A, [], LenB, B, Res).
nf_mul_log( 0, As, As, _, _, []) :- !.
nf_mul_log( 1, [A|As], As, Lb, B, R) :- !,
nf_mul_factor_log( Lb, B, [], A, R).
nf_mul_log( 2, [A1,A2|As], As, Lb, B, R) :- !,
nf_mul_factor_log( Lb, B, [], A1, A1b),
nf_mul_factor_log( Lb, B, [], A2, A2b),
nf_add( A1b, A2b, R).
nf_mul_log( N, A0, A2, Lb, B, R) :-
P is N>>1,
Q is N-P,
nf_mul_log( P, A0, A1, Lb, B, Rp),
nf_mul_log( Q, A1, A2, Lb, B, Rq),
nf_add( Rp, Rq, R).
%:- mode nf_add_2( +, +, -).
%
nf_add_2( Af, Bf, Res) :- % unfold: nf_add( [Af], [Bf], Res).
Af = v(Ka,Pa),
Bf = v(Kb,Pb),
compare( Rel, Pa, Pb),
nf_add_2_case( Rel, Af, Bf, Res, Ka, Kb, Pa).
%:- mode nf_add_2_case( +, +, +, -, +, +, +).
%
nf_add_2_case( <, Af, Bf, [Af,Bf], _, _, _).
nf_add_2_case( >, Af, Bf, [Bf,Af], _, _, _).
nf_add_2_case( =, _, _, Res, Ka, Kb, Pa) :-
arith_eval( Ka+Kb, Kc),
( arith_eval( Kc=:=0 ) ->
Res = []
;
Res=[v(Kc,Pa)]
).
%
% multiply with a scalar =\= 0
%
nf_mul_k( [], _, []).
nf_mul_k( [v(I,P)|Vs], K, [v(Ki,P)|Vks]) :-
arith_eval( K*I, Ki),
nf_mul_k( Vs, K, Vks).
nf_mul_factor( v(K,[]), Sum, Res) :- !, nf_mul_k( Sum, K, Res).
nf_mul_factor( F, Sum, Res) :-
nf_length( Sum, 0, Len),
nf_mul_factor_log( Len, Sum, [], F, Res).
nf_mul_factor_log( 0, As, As, _, []) :- !.
nf_mul_factor_log( 1, [A|As], As, F, [R]) :- !,
mult( A, F, R).
nf_mul_factor_log( 2, [A,B|As], As, F, Res) :- !,
mult( A, F, Af),
mult( B, F, Bf),
nf_add_2( Af, Bf, Res).
nf_mul_factor_log( N, A0, A2, F, R) :-
P is N>>1,
Q is N-P,
nf_mul_factor_log( P, A0, A1, F, Rp),
nf_mul_factor_log( Q, A1, A2, F, Rq),
nf_add( Rp, Rq, R).
mult( v(Ka,La), v(Kb,Lb), v(Kc,Lc)) :-
arith_eval( Ka*Kb, Kc),
pmerge( La, Lb, Lc).
pmerge( [], Bs, Bs).
pmerge( [A|As], Bs, Cs) :-
pmerge( Bs, A, As, Cs).
%:- mode pmerge(+,+,+,-).
%
pmerge( [], A, As, Res) :- Res = [A|As].
pmerge( [B|Bs], A, As, Res) :-
A=Xa^Ka,
B=Xb^Kb,
compare( R, Xa, Xb),
pmerge_case( R, A, As, Res, B, Bs, Ka, Kb, Xa).
%:- mode pmerge_case( +, +, +, -, +, +, +, +, ?).
%
pmerge_case( <, A, As, Res, B, Bs, _, _, _) :-
Res = [A|Tail],
pmerge( As, B, Bs, Tail).
pmerge_case( >, A, As, Res, B, Bs, _, _, _) :-
Res = [B|Tail],
pmerge( Bs, A, As, Tail).
pmerge_case( =, _, As, Res, _, Bs, Ka, Kb, Xa) :-
Kc is Ka+Kb,
( Kc=:=0 ->
pmerge( As, Bs, Res)
;
Res = [Xa^Kc|Tail],
pmerge( As, Bs, Tail)
).
nf_div( [], _, _) :- !, zero_division.
nf_div( [v(K,P)], Sum, Res) :- !,
arith_eval( 1/K, Ki),
mult_exp( P, -1, Pi),
nf_mul_factor( v(Ki,Pi), Sum, Res).
nf_div( D, A, [v(One,[(A/D)^1])]) :-
arith_eval( 1, One).
zero_division :- fail. % raise_exception(_) ?
mult_exp( [], _, []).
mult_exp( [X^P|Xs], K, [X^I|Tail]) :-
I is K*P,
mult_exp( Xs, K, Tail).
%
% raise to integer powers
%
% | ?- time({(1+X+Y+Z)^15=0}).
% Timing 00:00:02.610 2.610 iterative
% Timing 00:00:00.660 0.660 binomial
nf_power( N, Sum, Norm) :-
integer( N),
compare( Rel, N, 0),
( Rel = < ->
Pn is -N,
% nf_power_pos( Pn, Sum, Inorm),
binom( Sum, Pn, Inorm),
arith_eval( 1, One),
nf_div( Inorm, [v(One,[])], Norm)
; Rel = > ->
% nf_power_pos( N, Sum, Norm)
binom( Sum, N, Norm)
; Rel = = -> % 0^0 is indeterminate but we say 1
arith_eval( 1, One),
Norm = [v(One,[])]
).
%
% N>0
%
nf_power_pos( 1, Sum, Norm) :- !, Sum = Norm.
nf_power_pos( N, Sum, Norm) :-
N1 is N-1,
nf_power_pos( N1, Sum, Pn1),
nf_mul( Sum, Pn1, Norm).
%
% N>0
%
binom( Sum, 1, Power) :- !, Power = Sum.
binom( [], _, []).
binom( [A|Bs], N, Power) :-
( Bs=[] ->
nf_power_factor( A, N, Ap),
Power = [Ap]
; Bs=[_|_] ->
arith_eval( 1, One),
factor_powers( N, A, v(One,[]), Pas),
sum_powers( N, Bs, [v(One,[])], Pbs, []),
combine_powers( Pas, Pbs, 0, N, 1, [], Power)
).
combine_powers( [], [], _, _, _, Pi, Pi).
combine_powers( [A|As], [B|Bs], L, R, C, Pi, Po) :-
nf_mul( A, B, Ab),
arith_normalize( C, Cn),
nf_mul_k( Ab, Cn, Abc),
nf_add( Abc, Pi, Pii),
L1 is L+1,
R1 is R-1,
C1 is C*R//L1,
combine_powers( As, Bs, L1, R1, C1, Pii, Po).
nf_power_factor( v(K,P), N, v(Kn,Pn)) :-
arith_normalize( N, Nn),
arith_eval( exp(K,Nn), Kn),
mult_exp( P, N, Pn).
factor_powers( 0, _, Prev, [[Prev]]) :- !.
factor_powers( N, F, Prev, [[Prev]|Ps]) :-
N1 is N-1,
mult( Prev, F, Next),
factor_powers( N1, F, Next, Ps).
sum_powers( 0, _, Prev, [Prev|Lt], Lt) :- !.
sum_powers( N, S, Prev, L0, Lt) :-
N1 is N-1,
nf_mul( S, Prev, Next),
sum_powers( N1, S, Next, L0, [Prev|Lt]).
% ------------------------------------------------------------------------------
repair( Sum, Norm) :-
nf_length( Sum, 0, Len),
repair_log( Len, Sum, [], Norm).
repair_log( 0, As, As, []) :- !.
repair_log( 1, [v(Ka,Pa)|As], As, R) :- !,
repair_term( Ka, Pa, R).
repair_log( 2, [v(Ka,Pa),v(Kb,Pb)|As], As, R) :- !,
repair_term( Ka, Pa, Ar),
repair_term( Kb, Pb, Br),
nf_add( Ar, Br, R).
repair_log( N, A0, A2, R) :-
P is N>>1,
Q is N-P,
repair_log( P, A0, A1, Rp),
repair_log( Q, A1, A2, Rq),
nf_add( Rp, Rq, R).
repair_term( K, P, Norm) :-
length( P, Len),
arith_eval( 1, One),
repair_p_log( Len, P, [], Pr, [v(One,[])], Sum),
nf_mul_factor( v(K,Pr), Sum, Norm).
repair_p_log( 0, Ps, Ps, [], L0, L0) :- !.
repair_p_log( 1, [X^P|Ps], Ps, R, L0, L1) :- !,
repair_p( X, P, R, L0, L1).
repair_p_log( 2, [X^Px,Y^Py|Ps], Ps, R, L0,L2) :- !,
repair_p( X, Px, Rx, L0, L1),
repair_p( Y, Py, Ry, L1, L2),
pmerge( Rx, Ry, R).
repair_p_log( N, P0, P2, R, L0, L2) :-
P is N>>1,
Q is N-P,
repair_p_log( P, P0, P1, Rp, L0, L1),
repair_p_log( Q, P1, P2, Rq, L1, L2),
pmerge( Rp, Rq, R).
%vsc: added ! (01/06/06)
repair_p( Term, P, [Term^P], L0, L0) :- var( Term), !.
repair_p( Term, P, [], L0, L1) :- nonvar( Term),
repair_p_one( Term, TermN),
nf_power( P, TermN, TermNP),
nf_mul( TermNP, L0, L1).
%
% An undigested term a/b is distinguished from an
% digested one by the fact that its arguments are
% digested -> cuts after repair of args!
%
repair_p_one( Term, TermN) :-
nf_number( Term, TermN), % freq. shortcut for nf/2 case below
!.
repair_p_one( A1/A2, TermN) :-
repair( A1, A1n),
repair( A2, A2n),
!,
nf_div( A2n, A1n, TermN).
repair_p_one( Term, TermN) :-
nonlin_1( Term, Arg, Skel, Sa),
repair( Arg, An),
!,
nf_nonlin_1( Skel, An, Sa, TermN).
repair_p_one( Term, TermN) :-
nonlin_2( Term, A1,A2, Skel, Sa1, Sa2),
repair( A1, A1n),
repair( A2, A2n),
!,
nf_nonlin_2( Skel, A1n, A2n, Sa1, Sa2, TermN).
repair_p_one( Term, TermN) :-
nf( Term, TermN).
%:- mode nf_length( +, +, -).
%
nf_length( [], Li, Li).
nf_length( [_|R], Li, Lo) :-
Lii is Li+1,
nf_length( R, Lii, Lo).
% ------------------------------------------------------------------------------
nf2term( [], Z) :- arith_eval( 0, Z).
nf2term( [F|Fs], T) :-
f02t( F, T0),
yfx( Fs, T0, T).
yfx( [], T0, T0).
yfx( [F|Fs], T0, TN) :-
fn2t( F, Ft, Op),
T1 =.. [Op,T0,Ft],
yfx( Fs, T1, TN).
f02t( v(K,P), T) :-
( P = [] ->
T = K
; arith_eval( K=:=1) ->
p2term( P, T)
; arith_eval( K=:= -1) ->
T = -Pt,
p2term( P, Pt)
;
T = K*Pt,
p2term( P, Pt)
).
fn2t( v(K,P), Term, Op) :-
( arith_eval( K=:=1) ->
Term = Pt, Op = +
; arith_eval( K=:= -1) ->
Term = Pt, Op = -
; arith_eval( K<0) ->
arith_eval( -K, Kf),
Term = Kf*Pt, Op = -
;
Term = K*Pt, Op = +
),
p2term( P, Pt).
p2term( [X^P|Xs], Term) :-
( Xs=[] ->
pe2term( X, Xt),
exp2term( P, Xt, Term)
; Xs=[_|_] ->
Term = Xst*Xtp,
pe2term( X, Xt),
exp2term( P, Xt, Xtp),
p2term( Xs, Xst)
).
exp2term( 1, X, X) :- !.
exp2term(-1, X, One/X) :- !, arith_eval( 1, One).
exp2term( P, X, Term) :-
arith_normalize( P, Pn),
% Term = exp(X,Pn).
Term = X^Pn.
pe2term( X, Term) :- var(X), Term = X.
pe2term( X, Term) :- nonvar(X),
X =.. [F|Args],
pe2term_args( Args, Argst),
Term =.. [F|Argst].
pe2term_args( [], []).
pe2term_args( [A|As], [T|Ts]) :-
nf2term( A, T),
pe2term_args( As, Ts).
Reference in New Issue View Git Blame Copy Permalink