:- set_prolog_flag(verbose,silent).
:- set_prolog_flag(occurs_check,true).
:- op(500,yfx,$).
:- prompt(_, '').
:- use_module(library(readutil)).

%%%% IDEONE compatibility for mutually recursive predicates %%%%
eqty/2.
unify_oemap/2.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

kind(KC,var(X),   K1) :- first(X:K,KC).
kind(KC,F $ G,    K2) :- K2\==row, kind(KC,F,K1->K2),
                         K1\==row, kind(KC,G,K1).
kind(KC,A -> B,    o) :- kind(KC,A,o), kind(KC,B,o).
kind(KC,{R},       o) :- kind(KC,R,row).
kind(KC,[],      row).
kind(KC,[X:T|R], row) :- kind(KC,T,o), kind(KC,R,row).

type(KC,C,var(X),     A) --> { first(X:S,C) }, inst_ty(KC,S,A).
type(KC,C,lam(X,E),A->B) --> type(KC,[X:mono(A)|C],E,B),
                             [ kind(KC,A->B,o) ].
type(KC,C,X $ Y,      B) --> type(KC,C,X,A->B), type(KC,C,Y,A1),
                             !, { eqty(A,A1) }. % note the cut !
type(KC,C,let(X=E0,E),T) --> type(KC,C,E0,A),
                             type(KC,[X:poly(C,A)|C],E,T).
type(KC,C,{XEs},    {R}) --> { zip_with('=',Xs,Es,XEs) },
                             type_many(KC,C,Es,Ts),
                             { zip_with(':',Xs,Ts,R) }.
type(KC,C,sel(L,X),   T) --> { first(X:T,R) }, type(KC,C,L,{R}).

first(K:V,[K1:V1|Xs]) :- K = K1, V=V1.
first(K:V,[K1:V1|Xs]) :- K\==K1, first(K:V, Xs).

inst_ty(KC,poly(C,T),T2) --> { copy_term(t(C,T),t(C,T1)), 
                               free_variables(T,Xs),
                               free_variables(T1,Xs1) },
                             samekinds(KC,Xs,Xs1), { T1=T2 }.
inst_ty(KC,mono(T),   T) --> [].

samekinds(KC,[],    []    ) --> [].
samekinds(KC,[X|Xs],[Y|Ys]) --> { X\==Y },
                                [ kind(KC,X,K), kind(KC,Y,K) ],
                                samekinds(KC,Xs,Ys).
samekinds(KC,[X|Xs],[X|Ys]) --> [], samekinds(KC,Xs,Ys).

zip_with(F,[],    [],    []      ).
zip_with(F,[X|Xs],[Y|Ys],[FXY|Ps]) :- FXY=..[F,X,Y],
                                      zip_with(F,Xs,Ys,Ps).

type_many(KC,C,[],    []    ) --> [].
type_many(KC,C,[E|Es],[T|Ts]) --> type(KC,C,E,T),
                                  type_many(KC,C,Es,Ts).

variablize(var(X)) :- gensym(t,X).

infer_type(KC,C,E,T) :-
  phrase( type(KC,C,E,T), Gs0 ),
  copy_term(Gs0,Gs), 
  (bagof(Ty,X^Y^member(kind(X,Ty,Y),Gs),Tys); Tys=[]),
  free_variables(Tys,Xs),
  maplist(variablize,Xs), % replace free tyvar to var(t)
  maplist(call,Gs). % run all goals in Gs

ctx0([ 'Nat':mono(o)
     , 'List':mono(o->o)
     , 'Pair':mono(o->o->o)
     | _
     ],
     [ 'Zero':mono(Nat)
     , 'Succ':mono(Nat -> Nat)
     , 'Nil' :poly([], List$A)
     , 'Cons':poly([], A->((List$A)->(List$A)))
     , 'Pair':poly([], A0->B0->Pair$A0$B0)
     ])
  :- Nat = var('Nat'), List = var('List'), Pair=var('Pair').

run(N,T) :- ctx0(KC,C),
  Zero = var('Zero'), Succ = var('Succ'),
  Cons = var('Cons'), Nil = var('Nil'),
  Pair = var('Pair'),
  E0 = let(id=lam(x,var(x)),var(id)$var(id)),     % A->A
  E1 = lam(y,let(x=lam(z,var(y)),var(x)$var(x))), % A->A
  E2 = {[z=lam(x,var(x))]},   % {[z:A->A]}
  E3 = lam(r,sel(var(r),x)),  % {[x:A |R]} -> A
  %E4: {[y:A,x:B |R]} -> Pair$A$B
  E4 = lam(r,Pair$sel(var(r),y)$sel(var(r),x)),
  %E5: {[x:(A->A),y:(B->B)]}
  E5 = {[x=lam(x,var(x)),y=lam(x,var(x))]},
  E6 = E4 $ E5, % Pair $ B->B $ A->A
  %E7: {[y:A |R]} -> Pair $ A $ {[y:A| R]}
  E7 = lam(r,Pair$sel(var(r),y)$var(r)),
  E8 = E7 $ {[y=lam(x,var(x))]}, % Pair $ B->B $ {[y:(B->B)| R]}
  E9 = E7 $ {[]},
  E10 = {[]},
  Es = [E0,E1,E2,E3,E4,E5,E6,E7,E8,E9,E10],
  nth0(N,Es,E), infer_type(KC,C,E,T).


% related paper:
%
% Membership-Constraints and Complexity in Logic Programming with Sets,
% Frieder Stolzenburg (1996).
% http://l...content-available-to-author-only...r.com/chapter/10.1007%2F978-94-009-0349-4_15
% http://c...content-available-to-author-only...u.edu/viewdoc/summary?doi=10.1.1.54.8356

% more advanced notion of type equality at work
eqty(A1,A2) :- (var(A1); var(A2)), !, A1=A2.
eqty({R1},{R2}) :- !, unify_oemap(R1,R2). % permutation(R1,R2), !.
eqty(A1->B1,A2->B2) :- !, eqty(A2,A1), !, eqty(B1,B2). % in case of subtyping
eqty(A,A).

% set/map membership with extra-logical builtin \==
% to cut down duplicate answers as sets
memb(X,[X|_]).
memb(X,[Y|L]) :- X \== Y, memb(X,L).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% once inspired by the idea of the paper,
% finite map unification is just like this
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% unify finite maps
unify_map(A,B) :- submap_of(A,B), submap_of(B,A).

submap_of([], _).
submap_of([X:V|R],M) :- first(X:V1,M), eqty(V,V1), submap_of(R,M).


% finite map minus
mapminus(A,[],A).
mapminus([],_,[]).
mapminus([X:V|Ps],B,C) :- first(X:V1,B), !, eqty(V,V1) -> mapminus(Ps,B,C).
mapminus([X:V|Ps],B,[X:V|C]) :- mapminus(Ps,B,C).



% unify open ended maps with possibly uninstantiated variable tail at the end
unify_oemap(A,B) :- ( var(A); var(B) ), !, A=B.
unify_oemap(A,B) :-
        split_heads(A,Xs-T1), make_map(Xs,M1),
        split_heads(B,Ys-T2), make_map(Ys,M2),
        unify_oe_map(M1-T1, M2-T2).

make_map(L,M) :- setof(X:V,first(X:V,L),M). % remove duplicates
make_map([],[]).

split_heads([],[]-[]).
split_heads([X:V|T],[X:V]-T) :- var(T), !, true.
split_heads([X:V|Ps],[X:V|Hs]-T) :- split_heads(Ps,Hs-T).

% helper function for unify_oemap
unify_oe_map(Xs-T1,Ys-T2) :- T1==[], T2==[], unify_map(Xs,Ys).
unify_oe_map(Xs-T1,Ys-T2) :- T1==[], submap_of(Ys,Xs), mapminus(Xs,Ys,T2).
unify_oe_map(Xs-T1,Ys-T2) :- T2==[], submap_of(Xs,Ys), mapminus(Ys,Xs,T1).
unify_oe_map(Xs-T1,Ys-T2) :- 
        mapminus(Ys,Xs,L1), append(L1,T,T1),
        mapminus(Xs,Ys,L2), append(L2,T,T2).

%% ?- unify_oemap([z:string,y:bool|M1],[y:T,x:int|M2]).
%% M1 = [x:int|_G1426],
%% T = bool,
%% M2 = [z:string|_G1426].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

main:-
	process,
	halt.

process:-
    run(0,T0), print(T0), nl,
    run(1,T1), print(T1), nl,
    run(2,T2), print(T2), nl,
    run(3,T3), print(T3), nl,
    run(4,T4), print(T4), nl,
    run(5,T5), print(T5), nl,
    run(6,T6), print(T6), nl,
    run(7,T7), print(T7), nl,
    run(8,T8), print(T8), nl,
    (run(9,T9) -> write("must fail but "), print(T9); print(fail) ), nl,
    run(10,T10), print(T10), nl,
	true.

:- main.