型解析：型ユニフィケーション in Erlang 暫定

場合分けを17ステップに集約して、Erlangにしてみた。色々と問題もあるが、まーとりあえず動く。このエントリーに張り付けておく。

%% -*- coding: utf-8 -*-
%% unify.erl

-module(unify).
-compile(export_all).

%-define(DBG, 1).

-ifdef(DBG).
-define(P(F, A), io:format(F, A)).
-else.
-define(P(F, A), ok).
-endif.

%% A* は、便宜上 {star, {opt, A}} となっている。


%% @doc クリーネスターで終わる配列型の長さを増やして正規化。
extend_var_array(Len, List) when length(List) =< Len ->
    Last = {star, Item} = lists:last(List),
    ?P("extend_var_array~n* Item=~w~n", [Item]),
    lists:sublist(List, length(List) -1) ++ 
	lists:duplicate(Len - length(List), Item) ++
	[Last].

%% @doc 固定された配列＝タプル型の長さを増やして正規化。長さは必ず増えることになる。
extend_fixed_array(Len, List) when length(List) < Len ->
    List ++ 
	lists:duplicate(Len - length(List) - 1, {opt, never}) ++
	[{star, {opt, never}}].

%% @doc 配列型の長さを増やして正規化
extend_array(Len, List) ->
    case is_stared(List) of
	true ->
	    extend_var_array(Len, List);
	false ->
	    extend_fixed_array(Len, List)
    end.

%% @doc 配列の最後がクリーネスターかどうか
is_stared([]) ->
    false;
is_stared(List) ->
    Last = lists:last(List),
    case Last of
	{star, _} ->
	    true;
	_ ->
	    false
    end.
%% @doc is_stared/1 と同じだが、trueなら0、falseなら1を返す
stared_offset(List) ->
    case is_stared(List) of
	true  -> 0;
	false -> 1
    end.

%% 使ってない
get_array_default([]) ->
    {opt, never};
get_array_default(List) ->
    Last = lists:last(List),
    case Last of
	{star, Val} ->
	    Val;
	_ ->
	    {opt, never}
    end.

get_object_default(Proplist) ->
  case proplists:get_value(star, Proplist) of
      undefined ->
	  {opt, never};
      Val ->
	  Val
  end.

extend_object(KeysList, Proplist) ->
    DefaultValue = get_object_default(Proplist),
    lists:map(
      fun(K) ->
	      case proplists:get_value(K, Proplist) of
		  undefined ->
		      {K, DefaultValue};
		  Val ->
		      {K, Val}
	      end
      end,
      KeysList).

%% 必ずstarを含めて返す（必要なら追加する）、結果はソート済み
object_keys(Proplist) ->
    PL = 
	case proplists:get_value(star, Proplist) of
	    undefined -> [{star, {opt, never}} |Proplist];
	    _ -> Proplist
	end,
    X = lists:sort(proplists:get_keys(PL)), 
    X.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%                  ユニフィケーション
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% unify/4 の第1引数はロケーションパス、第4引数には結果が累積される。

unify(S, T) -> unify([], S, T, []).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%              ユニフィケーションの場合分け 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% join
unify(Loc, {join, List}, T, AccRes) -> %// 10*[1-11] 
    NewAccRes = [{Loc, {gothru, left_join}} |AccRes],
    unify_join(Loc, List, T, NewAccRes);

%% never を含む場合 
unify(Loc, never, T, AccRes) -> %// 1*[1-11] 
  [{Loc, {true, left_never}} |AccRes];
unify(Loc, S, never, AccRes) -> %// [2-9]*1
  [{Loc, {false, right_never}} |AccRes];

%% 右側がインターセクション型のとき 
%% 注意：左側にインターセクション型は出現しない、これでオシマイ
unify(Loc, S, {inter, Var, W}, AccRes) -> %// [2-9]*10
    NewAccRes = [{Loc, {incl, S, Var}} | AccRes],
    unify(Loc, S, W, NewAccRes);

%% 両側がオプショナル型のとき
unify(Loc, {opt, V}, {opt, W}, AccRes) -> %// 9*8
    NewAccRes = [{Loc, {gothru, both_opt}} | AccRes],
    unify(Loc, V, W, NewAccRes);

%% 右側だけがオプショナル型のとき 
unify(Loc, S, {opt, W}, AccRes) -> %// [2-8]*8
    NewAccRes = [{Loc, {gothru, right_opt}} | AccRes],
    unify(Loc, S, W, NewAccRes);
    
%% 左側だけがオプショナル型のとき
unify(Loc, {opt, V}, T, AccRes) -> % // 9*8
    NewAccRes = [{Loc, {exists, V}} | AccRes],
    unify(Loc, V, T, NewAccRes);

%% any を含むとき
unify(Loc, _S, any, AccRes) -> %// [2-8]*2
    [{Loc, {true, right_any}} | AccRes];
unify(Loc, any, S, AccRes) -> %// 2*[3-7,9,11]
  [{Loc, {incl, any, S}} |AccRes];

%% 変数を含むとき
unify(Loc, S, Var = {var, Y}, AccRes) -> %// [3-8]*11
    [{Loc, {incl, S, Var}} | AccRes];
unify(Loc, Var = {var, X}, T, AccRes) -> %// 8*[3-7,9]
    [{Loc, {incl, Var, T}} | AccRes];

%% a. 右側が排他的ユニオン型のとき
unify(Loc, T, {xunion, List}, AccRes) -> %// [3-7]*9
    NewAccRes = [{Loc, {gothru, right_xunion}}|AccRes],
    unify_with_xunion(Loc, T, List, NewAccRes);

%%%% ここからは左側の型で場合分け 

%% 3.1. is_number(S)
unify(Loc, S, T, AccRes) when is_number(S) -> %// 3.1*[3-7]
    ?P("unify/4 3.1: Loc=~w, S=~w, T=~w, A=~w~n", [Loc, S, T, AccRes]),
    unify_number(Loc, S, T, AccRes);

%% 3.2. is_list(S) listはErlangの文字列（ただし基本ラテン文字に限定）
unify(Loc, S, T, AccRes) when is_list(S) -> %// 3.2*[3-7]
    unify_string(Loc, S, T, AccRes);

%% 3.3. S = true, false, null %// 3.3*[3-7]
unify(Loc, true, true, AccRes) -> 
  [{Loc, {true, eq_true}} |AccRes];
unify(Loc, true, boolean, AccRes) ->
  [{Loc, {true, true_is_boolean}} |AccRes];
unify(Loc, true, S, AccRes) ->
  [{Loc, {false, left_true_but, S}} |AccRes];

unify(Loc, false, false, AccRes) ->
  [{Loc, {true, eq_false}} |AccRes];
unify(Loc, false, boolean, AccRes) ->
  [{Loc, {true, false_is_boolean}} |AccRes];
unify(Loc, false, S, AccRes) ->
  [{Loc, {false, left_false_but, S}} |AccRes];

unify(Loc, null, null, AccRes) ->
  [{Loc, {true, eq_null}} |AccRes];
unify(Loc, null, S, AccRes) ->
  [{Loc, {false, left_null_but, S}} |AccRes];

%% 4. スカラー型 %// 4*[3-7]
%% integer
unify(Loc, integer, integer, AccRes) ->
  [{Loc, {true, eq_integer}} |AccRes];
unify(Loc, integer, number, AccRes) ->
  [{Loc, {true, integer_is_number}} |AccRes];
unify(Loc, integer, S, AccRes) ->
  [{Loc, {false, left_integer_but, S}} |AccRes];
%% number
unify(Loc, number, number, AccRes) ->
  [{Loc, {true, eq_number}} |AccRes];
unify(Loc, number, S, AccRes) ->
  [{Loc, {false, left_number_but, S}} |AccRes];
%% string
unify(Loc, string, string, AccRes) ->
  [{Loc, {true, eq_string}} |AccRes];
unify(Loc, string, S, AccRes) ->
  [{Loc, {false, left_string_but, S}} |AccRes];
%% boolean
unify(Loc, boolean, boolean, AccRes) ->
  [{Loc, {true, eq_boolean}} |AccRes];
unify(Loc, boolean, S, AccRes) ->
  [{Loc, {false, left_boolean_but, S}} |AccRes];

%% 5. 配列型 %// 5*[3-7]
unify(Loc, {array, ListV}, {array, ListW}, AccRes) ->
    Len1 = length(ListV) + stared_offset(ListV),
    Len2 = length(ListW) + stared_offset(ListW),
    Len = lists:max([Len1, Len2]),
    ?P("unify 5. Len1=~w, Len2=~w, Len=~w~n", [Len1, Len2, Len]),

    List1 = extend_array(Len, ListV),
    List2 = extend_array(Len, ListW),
    NewAccRes = [{Loc, {gothru, both_array}} |AccRes],
    unify_array(Loc, List1, List2, NewAccRes);

%% 6. オブジェクト型 %// 6*[3-7]
unify(Loc, {object, ProplistV}, {object, ProplistW}, AccRes) ->
    Key1 = object_keys(ProplistV),
    Key2 = object_keys(ProplistW),
    Key = lists:umerge(Key1, Key2), % lists:umerge/2 はソート済みリストにしか機能しない

    Proplist1 = extend_object(Key, ProplistV),
    Proplist2 = extend_object(Key, ProplistW),
    NewAccRes = [{Loc, {gothru, both_object}} |AccRes],
    unify_object(Loc, Proplist1, Proplist2, NewAccRes);

%% 7. （明示的）タグ付き型 %// 
unify(Loc, {tag, Tag, V}, {tag, Tag, W}, AccRes) ->
    NewAccRes = [{Loc, {gothru, both_tag}} |AccRes],
    unify([{tag, Tag}|Loc], V, W, NewAccRes);
unify(Loc, {tag, Tag1, V}, {tag, Tag2, W}, AccRes) ->
    [{Loc, {false, tag_not_eq, Tag2}} |AccRes];
unify(Loc, {tag, Tag, V}, S, AccRes) ->    
    [{Loc, {false, left_tag_but, S}} |AccRes];

%% 番外：スター型 {star, Type}
unify(Loc, {star, V}, {star, W}, AccRes) ->
    NewAccRes = [{Loc, {gothru, both_star}} |AccRes],
    unify(Loc, V, W, NewAccRes);
unify(Loc, {star, V}, W, AccRes) ->
    [{Loc, {false, left_star_but, W}} |AccRes];

%% 他はあり得ないはず
unify(Loc, S, T, AccRes) ->
  [{Loc, {something_wrong, S, T}} |AccRes].


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%     ユニフィケーションの下請け関数
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

unify_join(Loc, List, T, AccRes)->
    {_N, Res} = lists:foldl(
		  fun(S, {N, A}) ->
			  {N+1, unify([{join, N}|Loc], S, T, A)}
		  end,
		  {1, AccRes},
		  List),
    Res.
%%
%% 3.1 is_number(S)
%% 左が数値リテラルの場合

%% 3.1 T = M  右も数値リテラル %// 3.1*[3-7]
unify_number(Loc, Num, M, AccRes) when Num == M ->
   [{Loc, {true, eq_number_literal}} |AccRes];
%% 3.1 T = integer 右はスカラー型
unify_number(Loc, Num, integer, AccRes) when is_integer(Num) ->
   [{Loc, {true, literal_is_integer}} |AccRes];
%% 3.1 T = number 右はスカラー型
unify_number(Loc, Num, number, AccRes) ->
   [{Loc, {true, literal_is_number}} |AccRes];
%% 3.1 その他
unify_number(Loc, _Num, S, AccRes) ->
   [{Loc, {false, left_number_literal_but, S}} |AccRes].

%%
%% 3.2 is_list(S)
%% 左が文字列リテラルの場合 %// 3.2*[3-7]

%% 3.2 T = Str 
unify_string(Loc, Str, X, AccRes) when is_list(X), Str == X ->
   [{Loc, {true, eq_string_literal}} |AccRes];

%% 3.2 T = string
unify_string(Loc, Str, string, AccRes) ->
   [{Loc, {true, string_literal_is_string}} |AccRes];

%% その他
unify_string(Loc, Str, S, AccRes) ->
   [{Loc, {false, left_string_literal_but, S}} |AccRes].


%%
%% 5. 左が配列型の場合
%% 
unify_array(Loc, List1, List2, AccRes) ->
    ?P("unify_array~n* List1=~w,~n* List2=~w~n", [List1, List2]),
    Zipped = lists:zip(List1, List2),
    {_N, Result} = lists:foldl(fun({S, T}, A) -> unify_item_pair(Loc, S, T, A) end, {0, AccRes}, Zipped),
    Result.

unify_item_pair(Loc, S, T, {N, Acc}) ->
    ?P("unify_item_pair: S=~w, T=~w, N=~w, Acc=~w~n", [S, T, N, Acc]),
    Result = unify([N|Loc], S, T, Acc),
    {N + 1, Result}.

%%
%% 6. 左がオブジェクト型の場合
%%
unify_object(Loc, Proplist1, Proplist2, AccRes) ->
    Zipped = lists:zip(Proplist1, Proplist2),
    lists:foldl(fun({K_S, K_T}, A) -> unify_prop_pair(Loc, K_S, K_T, A) end, AccRes, Zipped).

unify_prop_pair(Loc, {K, S}, {K, T}, Acc) ->
    unify([K|Loc], S, T, Acc).

%% 下請け：右側が排他的ユニオンのときの処理
%% タグの付与はこのなかでやるので事前にやっておく必要はない。
unify_with_xunion(Loc, S, List, AccRes) -> %// [3-7]*9
    TaggedS = to_tagged(S),
    TaggedList = list_to_tagged(List),
    R = lists:foldl(
	  fun(T, FoldAcc) ->
		  match_and_unify(Loc, TaggedS, T, AccRes, FoldAcc)
	  end,
	  false,
	  TaggedList),
    case R of
	false ->
      	    [{Loc, {false, xunion_not_match}}|AccRes];
	R ->
	    R
    end.

match_and_unify(Loc, {tag, Tag1, V}, {tag, Tag2, W}, AccRes, FoldAcc) ->
    R = if 
	    Tag1 == Tag2 ->
		?P("match_and_unify: ~w, ~w~n", [V, W]),
		unify(Loc, V, W, AccRes);
	    true ->
		false
	end,
    case R of
	false ->
	    FoldAcc;
	R ->
	    R
    end.

%% 排他的ユニオンの成分（選択肢）に any と neverは入れない。
%% neverはなくても同じだし、anyは排他的になるはずがない。
%% ユニオンの入れ子は結合法則で前もって取り除いて、フラットにしておく。

%% 数値と文字列
to_tagged(N) when is_number(N) ->
    {tag, number, N};
to_tagged(S) when is_list(S) ->
    {tag, string, S};
%% 予約定数
to_tagged(true)  ->
    {tag, boolean, true};
to_tagged(false)  ->
    {tag, boolean, false};
to_tagged(null)  ->
    {tag, null, null};
%% スカラー型
to_tagged(integer) ->
    {tag, number, integer};
to_tagged(number) ->
    {tag, number, number};
to_tagged(string) ->
    {tag, string, string};
to_tagged(boolean) ->
    {tag, boolean, boolean};
%% 配列型
to_tagged({array, List}) ->
    {tag, array, {array, List}};
%% オブジェクト型
to_tagged({object, Proplist}) ->
    {tag, object, {object, Proplist}};
%% タグ付き型
to_tagged({tag, _Tag, _S} = T) ->
    T.

list_to_tagged(List) ->
    lists:map(fun to_tagged/1, List).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%              実験と観察のツール
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

json_path(List) ->
    lists:foldr(
      fun(Comp, A) -> 
	     case Comp of
		 {tag, Tag} -> lists:concat([A, "@", Tag]);
		 {join, Num} -> lists:concat([A, "(", Num, ")"]);
		 Other -> lists:concat([A, ".", Other]) 
	     end
      end,
      [36], % 36 = dollar
      List).

print_result(Res) ->
    S = lists:flatten(str_print_result(Res)),
    io:fwrite("~s", [S]).

str_print_result(Res) ->
    lists:map(
      fun str_print_proposition/1,
      lists:reverse(Res)).

str_print_proposition({Loc, {true, Reason}}) ->
    io_lib:format("~s : TRUE because ~s~n", [json_path(Loc), Reason]);

str_print_proposition({Loc, {false, Reason}}) ->
    io_lib:format("~s : FALSE because ~s~n", [json_path(Loc), Reason]);

str_print_proposition({Loc, {false, Reason, Right}}) ->
    io_lib:format("~s : FALSE because ~s (~p)~n", [json_path(Loc), Reason, Right]);

str_print_proposition({Loc, {incl, Left, Right}}) ->
    io_lib:format("~s : ~p <_ ~p~n", [json_path(Loc), Left, Right]);

str_print_proposition({Loc, {exists, V}} ) ->
    io_lib:format("~s : exists (~p)~n", [json_path(Loc), V]);

str_print_proposition({Loc, {gothru, Kind}}) ->
    io_lib:format("~s : ~s ==>~n", [json_path(Loc), Kind]);

str_print_proposition({Loc, {something_wrong, S, T}}) ->
    io_lib:format("~s : Error! ~p, ~p~n", [json_path(Loc), S, T]).

do_unify(S, T) ->
    io:format("~n*** UNIFY(~p, ~p) ***~n", [S, T]),
    print_result(unify(S, T)).

%% @doc ファイルからユニファイすべき組のリストを読んで、全部ユニファイする。
test_all(Filename) ->
    {ok, List} = file:consult(Filename),
    lists:foreach(
      fun ({Left, Right}) -> do_unify(Left, Right) end,
      List).

file_test(Infile, Outfile) ->
    {ok, List} = file:consult(Infile),
    OutList = lists:map(
		fun ({Left, Right}) -> file_do_unify(Left, Right) end,
		List),
    file:write_file(Outfile, OutList).

file_do_unify(S, T) ->
    io_lib:format("~n*** UNIFY(~p, ~p) ***~n", [S, T]) ++
	str_print_result(unify(S, T)).