e5f4633c39
which included commits to RCS files with non-trunk default branches. git-svn-id: https://yap.svn.sf.net/svnroot/yap/trunk@5 b08c6af1-5177-4d33-ba66-4b1c6b8b522a
204 lines
3.9 KiB
Prolog
204 lines
3.9 KiB
Prolog
% rational (finite and infinite) tree handler
|
|
% 931119 thom fruehwirth ECRC for eclipse CHR
|
|
% 980130, 980312 thom fruehwirth LMU for sicstus CHR, now simpler and better
|
|
|
|
:- use_module(library(chr)).
|
|
|
|
% need global order on variables
|
|
:- use_module( library('chr/ordering'), [globalize/1,var_compare/3]).
|
|
% var is smaller than any non-var term
|
|
lt(X,Y):- (var(X),var(Y) -> globalize(X),globalize(Y),var_compare(<,X,Y) ; X@<Y).
|
|
le(X,Y):- (var(X) -> true ; X@=<Y).
|
|
|
|
|
|
handler tree.
|
|
|
|
option(debug_compile,on).
|
|
option(already_in_store, off).
|
|
option(already_in_heads, off).
|
|
option(check_guard_bindings, off).
|
|
|
|
constraints (~)/2, ('#~')/2.
|
|
% T1 ~ T2 means: term T1 is syntactically equal to term T2
|
|
% T1 #~ T2 means: term T1 is syntactically different from term T2
|
|
|
|
operator(700,xfx,(~)).
|
|
operator(700,xfx,('#~')).
|
|
|
|
ident @ T ~ T <=> true.
|
|
decompose @ T1 ~ T2 <=> nonvar(T1),nonvar(T2) |
|
|
same_functor(T1,T2),
|
|
T1=..[F|L1],T2=..[F|L2],
|
|
equate(L1,L2).
|
|
orient @ T ~ X <=> lt(X,T) | X ~ T.
|
|
simplify @ X ~ T1 \ X ~ T2 <=> le(T1,T2) | T1 ~ T2.
|
|
|
|
same_functor(T1,T2):- functor(T1,F,N),functor(T2,F,N).
|
|
|
|
equate([],[]).
|
|
equate([X|L1],[Y|L2]):- X ~ Y, equate(L1,L2).
|
|
|
|
|
|
ident @ T #~ T <=> fail.
|
|
decompose @ T1 #~ T2 <=> nonvar(T1),nonvar(T2) |
|
|
(same_functor(T1,T2) ->
|
|
T1=..[F|L1],T2=..[F|L2],
|
|
not_equate(L1,L2)
|
|
;
|
|
true).
|
|
orient @ T #~ X <=> lt(X,T) | X #~ T.
|
|
simplify @ X ~ T1 \ X #~ T2 <=> T1 #~ T2
|
|
pragma already_in_heads.
|
|
|
|
constraints not_equate/2, label/0.
|
|
|
|
not_equate([],[]) <=> fail.
|
|
not_equate([X],[Y]) <=> X #~ Y.
|
|
not_equate([X|L1],[X|L2]) <=> fail.
|
|
not_equate([X|L1],[Y|L2]), X~Y <=> not_equate(L1,L2).
|
|
% not_equate([X|L1],[Y|L2]) <=> ground(X#~Y) | X #~ Y -> true ; not_equate(L1,L2).
|
|
|
|
label, not_equate([X|L1],[Y|L2])#Id <=> true |
|
|
(X #~ Y ; X ~ Y, not_equate(L1,L2)),
|
|
label
|
|
pragma passive(Id).
|
|
|
|
|
|
/*
|
|
|
|
% EXAMPLES ------------------------------------------------------------
|
|
|
|
write(example:10), X#~a,X~b;
|
|
|
|
write(example:11), A~B,B~C,C~D,D~A;
|
|
|
|
write(example:12), A~B,B~C,C~D,D#~A;
|
|
|
|
|
|
write(example:20), A~g(A),A~g(g(A));
|
|
|
|
write(example:21), A#~g(A),A~g(g(A));
|
|
|
|
write(example:22), A~g(A),A#~g(g(A));
|
|
|
|
write(example:23), A~g(g(g(A))),A~g(g(A));
|
|
|
|
write(example:24), A~g(g(g(A))),g(A)~g(g(A));
|
|
|
|
write(example:25), A#~g(g(g(A))),A~g(g(A));
|
|
|
|
write(example:26), A~g(g(g(A))),A#~g(g(A));
|
|
|
|
|
|
write(example:30), X~f(T1),T2~f(T2),X~T1,X~T2;
|
|
|
|
write(example:31), f(X)~T1,T2~f(T2),X~T1,X~T2;
|
|
|
|
write(example:32), X~f(T1),T1~f(T2),X~T1,X~T2;
|
|
|
|
write(example:33), f(X)~T1,f(T1)~T2,X~T1,X~T2;
|
|
|
|
write(example:34), T1~f(T1),T2~f(T2),X~T1,X~T2;
|
|
|
|
|
|
write(example:40), A~f(X),B~f(Y),Y~Z,Z~X,A#~B;
|
|
|
|
write(example:41), A~X,B~Y,Y~Z,Z~X,A#~B;
|
|
|
|
write(example:42), X~f(X,Y),X#~f(X,Y);
|
|
|
|
write(example:43), X~f(X,Y),X#~f(Y,X);
|
|
|
|
write(example:44), X~f(X,Y),X#~f(Y,X),label;
|
|
|
|
write(example:45), X~f(A,B),X#~f(a,b),A~a,B~b;
|
|
|
|
write(example:46), X~f(A,B),X#~f(a,b),A~a,B~b,label;
|
|
|
|
|
|
write(example:50), [X|L] ~ [X,X|L], L ~ [X,X,X,X|Z];
|
|
|
|
write(example:51), [X|L]#~[X,X|L], L ~ [X,X,X,X|Z],label;
|
|
|
|
write(example:52), [X|L] ~ [X,X|L], L#~[X,X,X,X|Z],label;
|
|
|
|
write(example:53), L ~ [X,X|L], L ~ [A,B,C,D];
|
|
|
|
|
|
write(done).
|
|
|
|
|
|
% results of current version with local already_in_heads pragma
|
|
|
|
example:10
|
|
X~b ? ;
|
|
example:11
|
|
B~A,
|
|
A~C,
|
|
D~C ? ;
|
|
example:12example:20
|
|
A~g(A) ? ;
|
|
example:21
|
|
A#~g(A),
|
|
A~g(g(A)) ? ;
|
|
example:22example:23
|
|
A~g(A) ? ;
|
|
example:24
|
|
A~g(A) ? ;
|
|
example:25
|
|
A~g(g(A)),
|
|
A#~g(A) ? ;
|
|
example:26
|
|
A~g(g(g(A))),
|
|
A#~g(g(A)) ? ;
|
|
example:30
|
|
T1~X,
|
|
X~T2,
|
|
T2~f(T1) ? ;
|
|
example:31
|
|
T2~f(T2),
|
|
T1~X,
|
|
X~T2 ? ;
|
|
example:32
|
|
T1~X,
|
|
X~T2,
|
|
T2~f(T2) ? ;
|
|
example:33
|
|
T2~f(T1),
|
|
T1~X,
|
|
X~T2 ? ;
|
|
example:34
|
|
T1~X,
|
|
X~T2,
|
|
T2~f(T1) ? ;
|
|
example:40example:41example:42example:43
|
|
X~f(X,Y),
|
|
not_equate([X,Y],[Y,X]) ? ;
|
|
example:44
|
|
label,
|
|
X~f(X,Y),
|
|
Y#~X ? ;
|
|
example:45
|
|
X~f(A,B),
|
|
not_equate([A,B],[a,b]),
|
|
A~a,
|
|
B~b ? ;
|
|
example:46example:50
|
|
L~Z,
|
|
Z~[X|Z] ? ;
|
|
example:51
|
|
label,
|
|
L~[X,X,X,X|Z],
|
|
Z#~[X|Z] ? ;
|
|
example:52
|
|
label,
|
|
L~[X|L],
|
|
Z#~L ? ;
|
|
example:53done
|
|
true ?
|
|
|
|
*/
|
|
|
|
|
|
% end of handler tree
|