mnemosyne_unify.erl

OTP是开放电信平台的简称

%% ``The contents of this file are subject to the Erlang Public License,
%% Version 1.1, (the "License"); you may not use this file except in
%% compliance with the License. You should have received a copy of the
%% Erlang Public License along with this software. If not, it can be
%% retrieved via the world wide web at http://www.erlang.org/.
%% 
%% Software distributed under the License is distributed on an "AS IS"
%% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See
%% the License for the specific language governing rights and limitations
%% under the License.
%% 
%% The Initial Developer of the Original Code is Ericsson Utvecklings AB.
%% Portions created by Ericsson are Copyright 1999, Ericsson Utvecklings
%% AB. All Rights Reserved.''
%% 
%%     $Id$
%%
-module(mnemosyne_unify).
-export([add_bind_trigger/3, bindings_to_list/1, count_bs_vars/1, 
	 bs_union/2, bs_vars/1, bs_vars_value/1, check_triggers/1,
	 count_bs_vars/2, count_variables/1, count_variables/2, 
	 delete_bindings/3, deref_bindings/1, empty_bindings/0, instantiate/2, 
	 list_to_bindings/1, numbervars/1, numbervars/2, 
	 rename_variables/1, sing_vars/2,
	 unif/3, unify/2, unify/3, variables/1, variables_and_annonymous/1,
	 ground/1]).

%%%================================================================
%%% 		Exports


%%---- Unify the two terms U and V, possibly with the bindings Bs in effect.
%%     Returns false or new bindings


unify(U, V) -> catch unif(U, V, []).

unify(U, V, Bs) -> catch unif(U, V, Bs).


%%---- returns an ordset with the variable names in U

ground(U) ->
    case variables_and_annonymous(U) of
	[] -> true;
	_ -> false
    end.

variables_and_annonymous(U) -> 
    variables(U, ordsets:new()).

variables(U) -> 
    ordsets:del_element('_', variables(U, ordsets:new())).
    

%%---- returns a {Var,Num} list of the frequency of the variables in U

count_variables(U) -> count_variables(U,[]).

%%---- returns a {Var,1} list of the variables (Keys) in Bs
count_bs_vars(Bs) -> count_bs_vars1(Bs,[]).
count_bs_vars(Bs, Dict) -> count_bs_vars1(Bs, Dict).


sing_vars([{V,1}|T], Acc) -> sing_vars(T, [V|Acc]);
sing_vars([_|T], Acc) -> sing_vars(T, Acc);
sing_vars([], Acc) -> Acc.


%%---- returns all (key) variables and all (key) variables bound to a value
%%     respecitvely

bs_vars(Bs) -> get_bound_vars(Bs,all).

bs_vars_value(Bs) -> get_bound_vars(Bs,'#value').


%%---- replace variables by numbers (as in prolog)

numbervars(T) ->  numbervars(T,0).

numbervars(T, N) -> numbervars(T, N, variables(T)).

%%---- returns U but with all variables renamed to new ones

rename_variables(U) ->
    {V,_} = rename_variables(U, []),
    V.

%%---- Binds all variables in U to the value in the bindings Bs

instantiate(U, []) -> U;
instantiate(U, Bs) -> inst(U, Bs).

deref_bindings(Bs) -> deref_bs(Bs,Bs).
%%    list_to_bindings( deref_bs(bindings_to_list(Bs),Bs,[]) ).

%%---- keep or remove the bindings which have the variable in OrdSet

delete_bindings(Tree, KeepRemove, OrdSet) when is_tuple(Tree) ->
    {L,Key,KeyVal,R} = Tree,
    case {KeepRemove,ordsets:is_element(Key,OrdSet)} of
	{keep, false} -> remove(L,R,KeepRemove,OrdSet);
	{remove,true} -> remove(L,R,KeepRemove,OrdSet);
	_ -> {delete_bindings(L, KeepRemove, OrdSet),
	      Key,KeyVal,
	      delete_bindings(R, KeepRemove, OrdSet)}
    end;

delete_bindings([], _, _) ->
    [].
	    
%%---- The empty bindings

empty_bindings() -> [].    

%%---- Conversion    

bindings_to_list(Bs) ->
    bindings_to_list(Bs,[]).

list_to_bindings(L) ->
    list_to_bindings(L, empty_bindings()).

%%---- combine two bindings into one

bs_union(Bs1, []) -> Bs1;
bs_union([], Bs2) -> Bs2;
bs_union(Bs1, Bs2) ->
    list_to_bindings(bindings_to_list(Bs1) ++ bindings_to_list(Bs2)).

%%---- Check triggers, IN COMPILE-TIME

check_triggers(Bs) -> 
    put(when_called, compile_time),
    R = (catch check_triggers(Bs, Bs)),
    erase(when_called),
    case R of
	fail ->  throw(fail);
	Others -> Others
    end.

check_triggers({L,K,V,R}, Bs) ->
    {check_triggers(L,Bs),
     K,
     case V of
	 {'#bind_trigger',Ts} -> 
	     {'#bind_trigger', apply_bind_triggers(Ts,Bs)}; % can throw(fail)
	 _ ->
	     V
     end,
     check_triggers(R,Bs)
    };
check_triggers([],Bs) ->
    [].
    

%%%================================================================
%%% 		Private

%%%----------------------------------------------------------------
unif(X, X, Bs) ->
    Bs;

%% Annonymous variables unifyies with anything:
unif({'#var','_'}, _, Bs) -> Bs;
unif(_, {'#var','_'}, Bs) -> Bs;

unif({'#var',U}, {'#var',V}, Bs) -> 
    case deref(var_val,U,Bs) of 
	{'#var',V} ->				% U is bound to V already
	    Bs;

	{'#var',X} ->				% U is bound to unbound var X
	    bind(X,deref(var_val,V,Bs),Bs);	%   (which might be U)

	{'#value',U_value} ->			% U is bound to non-var already
	    unif({'#var',V}, U_value, Bs)
    end;

unif({'#var',U}, V, Bs) ->		% V is non-var
    bind(U, V, Bs);

unif(U, {'#var',V}, Bs) ->		% U is non-var
    bind(V, U, Bs);

unif([U|Us], [V|Vs], Bs) -> 
    unif(Us, Vs, unif(U,V,Bs));

unif(U, V, Bs) when is_tuple(U), is_tuple(V), size(U)==size(V) ->
    unif(tuple_to_list(U), 
	 tuple_to_list(V),
	 Bs);

unif(_, _, _) ->
    throw(fail).

%%%----------------------------------------------------------------
%%% bind(VariableNAME, Value, Bindings)

bind('_', _, Bs) ->
    Bs;

bind(U, {'#var',V}, Bs) ->
    {'#var',Ulast} = deref(var, U, Bs),
    {'#var',Vlast} = deref(var, V, Bs),
    bind(Ulast, deref(any,Ulast,Bs), Vlast, deref(any,Vlast,Bs), Bs);

bind(U, {'#value',NonVar}, Bs) ->
    {'#var',Ulast} = deref(var, U, Bs),
    bind(Ulast, deref(any,Ulast,Bs), [], {'#value',NonVar}, Bs);

bind(U, NonVar, Bs) ->
    {'#var',Ulast} = deref(var, U, Bs),
    bind(Ulast, deref(any,Ulast,Bs), [], {'#value',NonVar}, Bs).



bind(Ulast, _, Ulast, _, Bs) ->			% Don't bind V to itself!! 
    Bs;

bind(Ulast, {'#var',Ulast}, Vlast, {'#bind_trigger',Cv}, Bs) ->
    mk_binding(Ulast, {'#var',Vlast}, Bs);

bind(Ulast, {'#var',Ulast}, Vlast, Vany, Bs) ->
    mk_binding(Ulast, Vany, Bs);

bind(Ulast, {'#bind_trigger',Cu}, Vlast, VlastAny, Bs) ->
    case VlastAny of
	{'#bind_trigger',Cv} ->
	    rebind(Ulast, {'#var',Vlast}, 
		   rebind(Vlast, 
			  {'#bind_trigger',
			   ordsets:from_list(lists:append(Cv,Cu))},
			  Bs));

	{'#var',Vlast} ->
	    mk_binding(Vlast, {'#var',Ulast}, Bs);

	{'#value',Value} ->
	    NewBs = rebind(Ulast, {'#value',Value}, Bs),
	    apply_bind_triggers(Cu,NewBs),		% can throw(fail)
	    NewBs
    end;

bind(Ulast, {'#value',Uvalue}, Vlast, {'#value',Vvalue}, Bs) ->
    unif(Uvalue, Vvalue, Bs);

bind(Ulast, Uany, Vlast, Vany, Bs) ->
    throw(fail).



%%%----------------------------------------------------------------
%%%
%%%  Triggers
%%%

%%--- returns false or the bindings with the trigger added

add_bind_trigger([], Bind_Trigger, Bs) ->
    apply_bind_triggers([Bind_Trigger], Bs),
    Bs;

add_bind_trigger(Ts, Bind_Trigger, Bs) ->
    add_bind_trigger1(Ts, Bind_Trigger, Bs).



add_bind_trigger1([V|Vs], Bind_Trigger, Bs) ->
    add_bind_trigger1(Vs, 
		     Bind_Trigger,
		     add_bind_trigger1(V,Bind_Trigger,Bs));

add_bind_trigger1([], _, Bs) ->
    Bs;

add_bind_trigger1('_', Bind_Trigger, Bs) ->
    Bs;

add_bind_trigger1(VarName, Bind_Trigger, Bs)  ->
    {'#var', LastVar} = deref(var,VarName,Bs),
    case deref(any,LastVar,Bs) of
	{'#bind_trigger',Tr} ->			% VarName has already triggers
	    rebind(LastVar, 
		   {'#bind_trigger', ordsets:from_list([Bind_Trigger|Tr])},
		   Bs);

	{'#var', LastVar} ->			% set first trigger
	    mk_binding(LastVar, 
		       {'#bind_trigger',ordsets:from_list([Bind_Trigger])}, 
		       Bs);

	{'#value',Value} ->			% Too late! Just check
	    apply_bind_triggers([Bind_Trigger], Bs),%can throw(fail)
	    Bs
    end.

%%---- run when a variable is bound to Value
%%     returns the list of still valid triggers or throw(fail)

apply_bind_triggers(Triggers, Bs) ->