1:- module(cil, [unify/2,
    2				find_key/3,
    3				close_btree/1,
    4				distribute_constr/2,
    5				region_constr_of_leaves/4
    6			   ]).    7:- use_module([
    8		library(lists),
    9		library(sort),
   10		library(ordsets)]).   11
   12% for test.
   13% ?- qcompile(util('ptq-fragment')), module(cil).
   14
   15
   16	/****************************************************
   17	*            CIL attributed variables version       *
   18	*            based on attr_unify_hook/2.            *
   19	****************************************************/
   20
   21% for short.
   22% ?- put_attr(con(total), X).
   23put_attr(X, Attr):- put_attr(X, cil, Attr).
   24get_attr(X, Attr):- get_attr(X, cil, Attr).
   25
   26% After Jan's advice.
   27attr_unify_hook(V, Y):-
   28	(	get_attr(Y, cil, A)
   29	->	attr_unify(V, A, Y)
   30	;   attr_unify(V, Y)
   31	).
 attr_unify(+X, +Y) is det
Apply attribute X to Y.
   36attr_unify(btree(X), Y):- is_btree(Y), !, unify(X, Y).
   37attr_unify(con(Rgn, _), Y):- is_btree(Y), !,
   38						  distribute_constr(Y, Rgn).
   39attr_unify(_, _).
 attr_unify(+X, +Y, -Z) is det
Merge attributes of X and Y, and save the merged attribute as that of Z in case it is necessary. Note that here merge includes unification.
   47attr_unify(btree(X), btree(Y), _):- unify(X, Y).
   48attr_unify(btree(X), con(Rgn, D), Z):-
   49	distribute_constr(X, Rgn),
   50	put_attr(Z, con(Rgn, D), Z),
   51	subsume(X, D).
   52attr_unify(con(Rgn, Y), btree(D), Z):-
   53	distribute_constr(D, Rgn),
   54	put_attr(Z, con(Rgn, Y)),
   55	subsume(D, Y).
   56attr_unify(con(Rgn, Y), con(Rgn0, Y0), Z):-
   57	meet_region(Rgn, Rgn0, Rgn1),
   58	add_only_new(Y, Y0, Y1),
   59	put_attr(Z, con(Rgn1, Y1)),
   60	unify(Y, Y0).
   61
   62	/****************************************************
   63	*   Unification over feature sructures				*
   64	****************************************************/
   65
   66% Kernel Of CIL  by K. Mukai 01-DEC-85
   67%
   68% Originally coded in 1985 at ICOT.
   69%
   70% Revised around 2016-11-13.
   71%
   72% This is a unifier over feature structures rewritten on top of
   73% attributed variables in SWI-7.
   74%
   75%
   76% key		:=	<prolog ground term>
   77%
   78% btree		:=	[]			(void tree)
   79%			|	t(key, zterm, btree, btree)
   80%
   81% zterm		:=	btree
   82%			|	<prolog variable>
   83%			|	<prolog atomic term>
   84%			|	<prolog atom>(zterm, ..., zterm)
   85
   86
   87	/***************************************
   88	*   Unifier over feature structues.    *
   89	***************************************/
   90
   91% For test.
   92% ?- module(cil).
   93% ?- X.a=1.
   94% ?- X.a=1, X=Y, Y.a=V.
   95% ?- X=Y, X.a=1, Y.a=V.
   96% ?- X.a=1, Y.a=V, X=Y.
   97% ?- X.a #= Y.b, X={b:1}, X=Y, Y.a=V.
   98% ?- X.a = X.b, X={b:1}.
   99% ?- X={a:2}, Y={b:1}, X=Y.
  100% ?- X=f({a:2}), Y=f({b:1}), X=Y, f(A)= X, B = A.b.
  101% ?- X=f({a:2}), Y=f({b:1}), X=Y.
  102
  103is_btree(t(_,_,_,_)).
  104is_btree({}).
  105%
  106apply_constr(X, con(I,_)):- distribute_constr(X, I).
 distribute_constr(+X, +Rgn) is det
Distribute a region constraint Rgn down to the leaves of X.
  111distribute_constr(X, Rgn):- var(X), !,
  112	(	get_attr(X, A)
  113	-> 	(	A = con(RgnA, D)
  114		-> 	meet_region(RgnA, Rgn, RgnA0),
  115			put_attr(X, con(RgnA0, D))
  116		;	A = btree(A0),
  117			distribute_constr(A0, Rgn)
  118		)
  119	;	put_attr(X, con(Rgn, []))
  120	).
  121distribute_constr({}, _):-!.
  122distribute_constr(t(K,_,L,R), Rgn):-
  123	has_member(Rgn, K),
  124	meet_region(Rgn, lower(K), LowK),
  125	meet_region(Rgn, upper(K), UppK),
  126	distribute_constr(L, LowK),
  127	distribute_constr(R, UppK).
 region_constr_of_leaves(+X, +Rgn, +P, -Q) is det
The list of region constraints on leaves of X with Rgn propagated down is a difference list P by Q.
  134region_constr_of_leaves(X, Rgn, P, Q):- child_of_node(X, K, _, L, R), !,
  135	meet_region(lower(K), Rgn, RgnL),
  136	region_constr_of_leaves(L, RgnL, P, P0),
  137	meet_region(upper(K), Rgn, RgnR),
  138	region_constr_of_leaves(R, RgnR, P0, Q).
  139region_constr_of_leaves(X, Rgn, [put_attr(X, cil, con(Rgn, []))|P], P):- var(X), !.
  140region_constr_of_leaves(_, _, P, P).
 unify(+X, +Y) is det
unify X with Y. Unification dispatcher.
  146unify(X, Y):- (attvar(X); attvar(Y)), !, X=Y.
  147unify(X, Y):- (var(X); var(Y)), !, X=Y.
  148unify(X, Y):- is_btree(X), is_btree(Y),	!, subsume(X, Y).
  149unify(X, X).	% cool !
 subsume(+X:btree, +Y:btree) is det
Merge btree X into btree Y. subsume(X,Y) and subsume(Y,X) implies X=Y.
  155subsume(X, Y):-attvar(X), !,
  156		get_attr(X, A),
  157		(	A=btree(T)
  158		->	subsume(T, Y)
  159		;	A=con(Rgn, S),
  160			add_only_new([Y], S, S0),   % sounds natural !
  161			put_attr(X, con(Rgn, S0))
  162		).
  163subsume(X, Y):-var(X), !,
  164		put_attr(X, con(total, [Y])).
  165subsume(t(K,V,L,R), Y):-
  166		find_key(Y, K, U),
  167		unify(V, U),
  168		subsume(L, Y),
  169		subsume(R, Y).
  170subsume({}, _).
 child_of_node(X, K, V, L, R) is det
True if X is a nonterminal node with key K, value V, left child L, and right child R.
  176child_of_node(X, K, V, L, R):- var(X), !,
  177					   get_attr(X, A),
  178					   A=btree(t(K, V, L, R)).
  179child_of_node(t(K, V, L, R), K, V, L, R).
  180
  181%%%
  182% inspect_node(X, A):-var(X), (get_attr(X, A); A=var(X)), !.
  183% inspect_node(X, X).
 weak_subsume(+X:btree, +Y:btree, -Z:btree) is det
True if Z.a = V iff one of the following holds.
  1. Y.a = V, and V is instantiated.
  2. Y.a = V, and X.a is not instantiated.
  3. X.a = V, V is instantiated, and Y.a uninstantiated.
  191% ?- module(cil).
  192% ?- cil:weak_subsume({a:2}, {a:1}, Z).
  193% ?- cil:weak_subsume({a:2, b:1, c:3}, {a:1, b:X, c:5, d:6}, Z).
  194weak_subsume(X, Y, Z):-attvar(X), !,
  195		get_attr(X, A),
  196		(	A=btree(T)
  197		->	weak_subsume(T, Y, Z)
  198		;	Z = Y
  199		).
  200weak_subsume(X, Y, Y):-var(X), !.
  201weak_subsume(t(K,V,L,R), Y, Z):-
  202		find_key(Y, K, U),
  203		(unify(V, U); true),
  204		!,
  205		weak_subsume(L, Y, Z),
  206		weak_subsume(R, Y, Z).
  207weak_subsume({}, Y, Y).
  208
  209% :- module(cil).
  210%@ true.
  211%@ true.
 close_btree(+X) is det
Close all leaves of X with [] (void tree)

?- {a:1}=X, close_btree(X), X={b:1}. ?- {a:1}=X, close_btree(X).

  219close_btree(X):- child_of_node(X, _, _, L, R), !,
  220				 close_btree(L),
  221				 close_btree(R).
  222close_btree({}):-!.
  223close_btree(t(_, _, L, R)):-close_btree(L),
  224		close_btree(R).
  225
  226% ?- [util('ptq-fragment')].
  227%% is_equal_btree(+X:btree, +Y:btree) is det.
  228%  True if closed X is equaivalent to closed Y as open dict.
  229
  230% ?-is_equal_btree({a:1}, {a:1}).
  231% ?-is_equal_btree({a:1, b:2}, {b:2, a:1}).
  232% ?-is_equal_btree({a:f(2)}, {a:f(1)}).			% false
  233% ?-is_equal_btree({a:f({b:2})}, {a:f({b:3})}).	% false
  234is_equal_btree(X, Y):- is_equal_by_stack([X],[Y]).
  235
  236%
  237is_equal_by_stack(X, Y):- skip_leaves(X, X0),
  238					skip_leaves(Y, Y0),
  239					is_equal_pair(X0, Y0).
  240%
  241is_equal_pair([],[]).
  242is_equal_pair([pair(K, V)|L],[pair(K, U)|M]):-
  243	is_equal_arg(V, U),
  244	is_equal_by_stack(L, M).
  245%
  246is_equal_arg(X, Y):- var(X), var(Y), X==Y, !.
  247is_equal_arg(X, Y):-
  248	(	child_of_node(X, K, V, L, R)
  249	->	(	child_of_node(Y, K0, V0, L0, R0)
  250		->  is_equal_by_stack(	[L,	 pair(K, V),   R],
  251								[L0, pair(K0, V0), R0])
  252		;	false
  253		)
  254	;	(	child_of_node(Y, _, _, _, _)
  255		->  false
  256		;   is_equal_non_btree(X, Y)
  257		)
  258	).
  259%
  260is_equal_non_btree(X, Y):- (var(X); var(Y)), !, X==Y.
  261is_equal_non_btree(X, Y):- (atomic(X); atomic(Y)), !, X==Y.
  262is_equal_non_btree(X, Y):- X=..[F|Xs],
  263				  Y=..[F|Ys],
  264				  maplist(is_equal_arg, Xs, Ys).
  265%
  266skip_leaves([], []).
  267skip_leaves([X|Xs], U):- child_of_node(X, K, V, L, R),!,
  268		skip_leaves([L, pair(K,V), R|Xs], U).
  269skip_leaves([X|Xs], U):- (var(X); X==[]), !,
  270		skip_leaves(Xs, U).
  271skip_leaves(X, X).
 role(+K, ?X, ?V) is det
unify V with the value of the key K in the btree X so that X.K = V
  277user:role(K, X, V):- when(ground(K), find_key(X, K, U)),
  278 				  unify(V, U).
  279
  280%
  281min(X, Y, X):- X@<Y, !.
  282min(_, Y, Y).
  283
  284max(X, Y, Y):- X@<Y, !.
  285max(X, _, X).
True if B has a key K with value V, i.e., B.K = V. This is a primitive of this library.
  291% ?- find_key({a:1}, a, V, R).
  292% ?- find_key(X, a, V).
  293% ?- find_key(t(k, 1, L, R), k, V).
  294find_key(B, K, V):-
  295		(	var(B)
  296		-> 	(	get_attr(B, U)
  297		   	->	(	U=btree(U0)
  298		   		->	find_key(U0, K, V)
  299		   		;	insert_key(U, K, V, B)
  300		   		)
  301		   	;	T = t(K, V, L, R),
  302		   		put_attr(L, con(lower(K),[])),
  303		   		put_attr(R, con(upper(K),[])),
  304		   		put_attr(B, btree(T))
  305		   	)
  306		;	B=t(J,U,L,R),
  307			(   J==K
  308			->  V=U
  309			;   (	J @< K
  310				->	find_key(R, K, V)
  311				;	find_key(L, K, V)
  312				)
  313			)
  314		).
  315
  316%
  317find_key_list([], _, _).
  318find_key_list([Y|Ys], K, V):- find_key(Y, K, V),
  319	find_key_list(Ys, K, V).
Helper predicate for find_key/3 above. True if N is a variable with an attribute t(K, V, L, R) such that L and R have the region constraint con(Rgn, Ys) making all members of Ys having a subtree t(K, V, _, _). i.e, N.K=V, and Y.K=V for all Y in Ys.
  328insert_key(con(Rgn, Ys), K, V, N):-
  329	has_member(Rgn, K),
  330	meet_region(Rgn, lower(K), RgnL),
  331	meet_region(Rgn, upper(K), RgnR),
  332	put_attr(L, con(RgnL, Ys)),
  333	put_attr(R, con(RgnR, Ys)),
  334	put_attr(N, btree(t(K, V, L, R))),
  335	find_key_list(Ys, K, V).
 has_member(+R, +M) is det
True if M falls in region R.
  339has_member(total, _).
  340has_member(seg(L,R), X):- L@<X, X@<R.
  341has_member(lower(U), X):- X@<U.
  342has_member(upper(U), X):- U@<X.
 meet_region(+X, +Y) is det
True if the intersection of X and Y is not empty.
  347meet_region(X, Y):- meet_region(X, Y, Z), Z\==[].
 meet_region(+X, +Y, -Z) is det
True if Z is the intersection of regions X and Y. This is a primitive engine of this open dict library.
  354% ?- meet_region(lower(a), lower(b), X).
  355% ?- meet_region(seg(a, p), seg(b, z), X).
  356% ?- meet_region(seg(a, z), seg(b, z), X).
  357meet_region(total, X, X).
  358meet_region(X, total, X).
  359meet_region([], _, []).
  360meet_region(_, [], []).
  361meet_region(lower(A), lower(B), lower(C)):- min(A, B, C).
  362meet_region(lower(A), upper(B), R):-
  363	(	B @< A -> R = seg(B, A)
  364	;   R = []
  365	).
  366meet_region(lower(C), seg(A,B), R):-
  367	(	C @=< A -> R = []
  368	;	R = seg(A, D),
  369		min(B,C,D)
  370	).
  371meet_region(upper(A), upper(B), upper(C)):- max(A, B, C).
  372meet_region(upper(A), lower(B), R):-
  373	(	A @< B -> R = seg(A, B)
  374	;   R = []
  375	).
  376meet_region(upper(C), seg(A, B), R):-
  377	(	C @>= B
  378	->	R = []
  379	;   R = seg(D, B),
  380		max(A, C, D)
  381	).
  382meet_region(seg(A, B), lower(C), R):-
  383	(	C @=< A -> R = []
  384	;	R = seg(A, D),
  385		min(B,C,D)
  386	).
  387meet_region(seg(A, B), upper(C), R):-
  388	(	C @>= B
  389	->	R = []
  390	;   R = seg(D, B),
  391		max(A, C, D)
  392	).
  393meet_region(seg(A, B), seg(C, D), M):-
  394	max(A,C,L),
  395	min(B,D,R),
  396	(	L @>= R -> M = []
  397	;	M = seg(L, R)
  398	).
  399
  400% % contain(+X, +Y) is det.
  401%  True if region X contains region Y, i.e. Y is a subset of X.
  402% ?- contain(lower(i), lower(j)).
  403% ?- contain(lower(j), lower(j)).
  404
  405contain(total,_).
  406contain(_, []).
  407contain(lower(A), lower(B)) :- B@=<A.
  408contain(lower(A), seg(_,B)) :- B@=<A.
  409contain(upper(A), upper(B)) :- A@=<B.
  410contain(upper(A), seg(B,_)) :- A@=<B.
  411contain(seg(A,B), seg(A0, B0)) :- A@=<A0, B0@=<B.
  412
  413%
  414add_only_new([], X, X):- !.
  415add_only_new([X|Y], Z, U):- memq(X, Z), !,
  416		add_only_new(Y, Z, U).
  417add_only_new([X|Y], Z, [X|U]):-
  418		add_only_new(Y, Z, U).
  419%
  420memq(X, [Y|_]):- X==Y, !.
  421memq(X, [_|Y]):- memq(X, Y)