:- 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 ),
(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'), 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 duplicatesmake_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,
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
(10,T10
), print
(T10
), nl,
:- main.
Oi0gc2V0X3Byb2xvZ19mbGFnKHZlcmJvc2Usc2lsZW50KS4KOi0gc2V0X3Byb2xvZ19mbGFnKG9jY3Vyc19jaGVjayx0cnVlKS4KOi0gb3AoNTAwLHlmeCwkKS4KOi0gcHJvbXB0KF8sICcnKS4KOi0gdXNlX21vZHVsZShsaWJyYXJ5KHJlYWR1dGlsKSkuCgolJSUlIElERU9ORSBjb21wYXRpYmlsaXR5IGZvciBtdXR1YWxseSByZWN1cnNpdmUgcHJlZGljYXRlcyAlJSUlCmVxdHkvMi4KdW5pZnlfb2VtYXAvMi4KJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlCgpraW5kKEtDLHZhcihYKSwgICBLMSkgOi0gZmlyc3QoWDpLLEtDKS4Ka2luZChLQyxGICQgRywgICAgSzIpIDotIEsyXD09cm93LCBraW5kKEtDLEYsSzEtPksyKSwKICAgICAgICAgICAgICAgICAgICAgICAgIEsxXD09cm93LCBraW5kKEtDLEcsSzEpLgpraW5kKEtDLEEgLT4gQiwgICAgbykgOi0ga2luZChLQyxBLG8pLCBraW5kKEtDLEIsbykuCmtpbmQoS0Mse1J9LCAgICAgICBvKSA6LSBraW5kKEtDLFIscm93KS4Ka2luZChLQyxbXSwgICAgICByb3cpLgpraW5kKEtDLFtYOlR8Ul0sIHJvdykgOi0ga2luZChLQyxULG8pLCBraW5kKEtDLFIscm93KS4KCnR5cGUoS0MsQyx2YXIoWCksICAgICBBKSAtLT4geyBmaXJzdChYOlMsQykgfSwgaW5zdF90eShLQyxTLEEpLgp0eXBlKEtDLEMsbGFtKFgsRSksQS0+QikgLS0+IHR5cGUoS0MsW1g6bW9ubyhBKXxDXSxFLEIpLAogICAgICAgICAgICAgICAgICAgICAgICAgICAgIFsga2luZChLQyxBLT5CLG8pIF0uCnR5cGUoS0MsQyxYICQgWSwgICAgICBCKSAtLT4gdHlwZShLQyxDLFgsQS0+QiksIHR5cGUoS0MsQyxZLEExKSwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAhLCB7IGVxdHkoQSxBMSkgfS4gJSBub3RlIHRoZSBjdXQgIQp0eXBlKEtDLEMsbGV0KFg9RTAsRSksVCkgLS0+IHR5cGUoS0MsQyxFMCxBKSwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICB0eXBlKEtDLFtYOnBvbHkoQyxBKXxDXSxFLFQpLgp0eXBlKEtDLEMse1hFc30sICAgIHtSfSkgLS0+IHsgemlwX3dpdGgoJz0nLFhzLEVzLFhFcykgfSwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICB0eXBlX21hbnkoS0MsQyxFcyxUcyksCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgeyB6aXBfd2l0aCgnOicsWHMsVHMsUikgfS4KdHlwZShLQyxDLHNlbChMLFgpLCAgIFQpIC0tPiB7IGZpcnN0KFg6VCxSKSB9LCB0eXBlKEtDLEMsTCx7Un0pLgoKZmlyc3QoSzpWLFtLMTpWMXxYc10pIDotIEsgPSBLMSwgVj1WMS4KZmlyc3QoSzpWLFtLMTpWMXxYc10pIDotIEtcPT1LMSwgZmlyc3QoSzpWLCBYcykuCgppbnN0X3R5KEtDLHBvbHkoQyxUKSxUMikgLS0+IHsgY29weV90ZXJtKHQoQyxUKSx0KEMsVDEpKSwgCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICBmcmVlX3ZhcmlhYmxlcyhULFhzKSwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIGZyZWVfdmFyaWFibGVzKFQxLFhzMSkgfSwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICBzYW1la2luZHMoS0MsWHMsWHMxKSwgeyBUMT1UMiB9LgppbnN0X3R5KEtDLG1vbm8oVCksICAgVCkgLS0+IFtdLgoKc2FtZWtpbmRzKEtDLFtdLCAgICBbXSAgICApIC0tPiBbXS4Kc2FtZWtpbmRzKEtDLFtYfFhzXSxbWXxZc10pIC0tPiB7IFhcPT1ZIH0sCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgWyBraW5kKEtDLFgsSyksIGtpbmQoS0MsWSxLKSBdLAogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIHNhbWVraW5kcyhLQyxYcyxZcykuCnNhbWVraW5kcyhLQyxbWHxYc10sW1h8WXNdKSAtLT4gW10sIHNhbWVraW5kcyhLQyxYcyxZcykuCgp6aXBfd2l0aChGLFtdLCAgICBbXSwgICAgW10gICAgICApLgp6aXBfd2l0aChGLFtYfFhzXSxbWXxZc10sW0ZYWXxQc10pIDotIEZYWT0uLltGLFgsWV0sCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgemlwX3dpdGgoRixYcyxZcyxQcykuCgp0eXBlX21hbnkoS0MsQyxbXSwgICAgW10gICAgKSAtLT4gW10uCnR5cGVfbWFueShLQyxDLFtFfEVzXSxbVHxUc10pIC0tPiB0eXBlKEtDLEMsRSxUKSwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIHR5cGVfbWFueShLQyxDLEVzLFRzKS4KCnZhcmlhYmxpemUodmFyKFgpKSA6LSBnZW5zeW0odCxYKS4KCmluZmVyX3R5cGUoS0MsQyxFLFQpIDotCiAgcGhyYXNlKCB0eXBlKEtDLEMsRSxUKSwgR3MwICksCiAgY29weV90ZXJtKEdzMCxHcyksIAogIChiYWdvZihUeSxYXllebWVtYmVyKGtpbmQoWCxUeSxZKSxHcyksVHlzKTsgVHlzPVtdKSwKICBmcmVlX3ZhcmlhYmxlcyhUeXMsWHMpLAogIG1hcGxpc3QodmFyaWFibGl6ZSxYcyksICUgcmVwbGFjZSBmcmVlIHR5dmFyIHRvIHZhcih0KQogIG1hcGxpc3QoY2FsbCxHcykuICUgcnVuIGFsbCBnb2FscyBpbiBHcwoKY3R4MChbICdOYXQnOm1vbm8obykKICAgICAsICdMaXN0Jzptb25vKG8tPm8pCiAgICAgLCAnUGFpcic6bW9ubyhvLT5vLT5vKQogICAgIHwgXwogICAgIF0sCiAgICAgWyAnWmVybyc6bW9ubyhOYXQpCiAgICAgLCAnU3VjYyc6bW9ubyhOYXQgLT4gTmF0KQogICAgICwgJ05pbCcgOnBvbHkoW10sIExpc3QkQSkKICAgICAsICdDb25zJzpwb2x5KFtdLCBBLT4oKExpc3QkQSktPihMaXN0JEEpKSkKICAgICAsICdQYWlyJzpwb2x5KFtdLCBBMC0+QjAtPlBhaXIkQTAkQjApCiAgICAgXSkKICA6LSBOYXQgPSB2YXIoJ05hdCcpLCBMaXN0ID0gdmFyKCdMaXN0JyksIFBhaXI9dmFyKCdQYWlyJykuCgpydW4oTixUKSA6LSBjdHgwKEtDLEMpLAogIFplcm8gPSB2YXIoJ1plcm8nKSwgU3VjYyA9IHZhcignU3VjYycpLAogIENvbnMgPSB2YXIoJ0NvbnMnKSwgTmlsID0gdmFyKCdOaWwnKSwKICBQYWlyID0gdmFyKCdQYWlyJyksCiAgRTAgPSBsZXQoaWQ9bGFtKHgsdmFyKHgpKSx2YXIoaWQpJHZhcihpZCkpLCAgICAgJSBBLT5BCiAgRTEgPSBsYW0oeSxsZXQoeD1sYW0oeix2YXIoeSkpLHZhcih4KSR2YXIoeCkpKSwgJSBBLT5BCiAgRTIgPSB7W3o9bGFtKHgsdmFyKHgpKV19LCAgICUge1t6OkEtPkFdfQogIEUzID0gbGFtKHIsc2VsKHZhcihyKSx4KSksICAlIHtbeDpBIHxSXX0gLT4gQQogICVFNDoge1t5OkEseDpCIHxSXX0gLT4gUGFpciRBJEIKICBFNCA9IGxhbShyLFBhaXIkc2VsKHZhcihyKSx5KSRzZWwodmFyKHIpLHgpKSwKICAlRTU6IHtbeDooQS0+QSkseTooQi0+QildfQogIEU1ID0ge1t4PWxhbSh4LHZhcih4KSkseT1sYW0oeCx2YXIoeCkpXX0sCiAgRTYgPSBFNCAkIEU1LCAlIFBhaXIgJCBCLT5CICQgQS0+QQogICVFNzoge1t5OkEgfFJdfSAtPiBQYWlyICQgQSAkIHtbeTpBfCBSXX0KICBFNyA9IGxhbShyLFBhaXIkc2VsKHZhcihyKSx5KSR2YXIocikpLAogIEU4ID0gRTcgJCB7W3k9bGFtKHgsdmFyKHgpKV19LCAlIFBhaXIgJCBCLT5CICQge1t5OihCLT5CKXwgUl19CiAgRTkgPSBFNyAkIHtbXX0sCiAgRTEwID0ge1tdfSwKICBFcyA9IFtFMCxFMSxFMixFMyxFNCxFNSxFNixFNyxFOCxFOSxFMTBdLAogIG50aDAoTixFcyxFKSwgaW5mZXJfdHlwZShLQyxDLEUsVCkuCgoKJSByZWxhdGVkIHBhcGVyOgolCiUgTWVtYmVyc2hpcC1Db25zdHJhaW50cyBhbmQgQ29tcGxleGl0eSBpbiBMb2dpYyBQcm9ncmFtbWluZyB3aXRoIFNldHMsCiUgRnJpZWRlciBTdG9semVuYnVyZyAoMTk5NikuCiUgaHR0cDovL2wuLi5jb250ZW50LWF2YWlsYWJsZS10by1hdXRob3Itb25seS4uLnIuY29tL2NoYXB0ZXIvMTAuMTAwNyUyRjk3OC05NC0wMDktMDM0OS00XzE1CiUgaHR0cDovL2MuLi5jb250ZW50LWF2YWlsYWJsZS10by1hdXRob3Itb25seS4uLnUuZWR1L3ZpZXdkb2Mvc3VtbWFyeT9kb2k9MTAuMS4xLjU0LjgzNTYKCiUgbW9yZSBhZHZhbmNlZCBub3Rpb24gb2YgdHlwZSBlcXVhbGl0eSBhdCB3b3JrCmVxdHkoQTEsQTIpIDotICh2YXIoQTEpOyB2YXIoQTIpKSwgISwgQTE9QTIuCmVxdHkoe1IxfSx7UjJ9KSA6LSAhLCB1bmlmeV9vZW1hcChSMSxSMikuICUgcGVybXV0YXRpb24oUjEsUjIpLCAhLgplcXR5KEExLT5CMSxBMi0+QjIpIDotICEsIGVxdHkoQTIsQTEpLCAhLCBlcXR5KEIxLEIyKS4gJSBpbiBjYXNlIG9mIHN1YnR5cGluZwplcXR5KEEsQSkuCgolIHNldC9tYXAgbWVtYmVyc2hpcCB3aXRoIGV4dHJhLWxvZ2ljYWwgYnVpbHRpbiBcPT0KJSB0byBjdXQgZG93biBkdXBsaWNhdGUgYW5zd2VycyBhcyBzZXRzCm1lbWIoWCxbWHxfXSkuCm1lbWIoWCxbWXxMXSkgOi0gWCBcPT0gWSwgbWVtYihYLEwpLgoKJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUKJSBvbmNlIGluc3BpcmVkIGJ5IHRoZSBpZGVhIG9mIHRoZSBwYXBlciwKJSBmaW5pdGUgbWFwIHVuaWZpY2F0aW9uIGlzIGp1c3QgbGlrZSB0aGlzCiUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlCgolIHVuaWZ5IGZpbml0ZSBtYXBzCnVuaWZ5X21hcChBLEIpIDotIHN1Ym1hcF9vZihBLEIpLCBzdWJtYXBfb2YoQixBKS4KCnN1Ym1hcF9vZihbXSwgXykuCnN1Ym1hcF9vZihbWDpWfFJdLE0pIDotIGZpcnN0KFg6VjEsTSksIGVxdHkoVixWMSksIHN1Ym1hcF9vZihSLE0pLgoKCiUgZmluaXRlIG1hcCBtaW51cwptYXBtaW51cyhBLFtdLEEpLgptYXBtaW51cyhbXSxfLFtdKS4KbWFwbWludXMoW1g6VnxQc10sQixDKSA6LSBmaXJzdChYOlYxLEIpLCAhLCBlcXR5KFYsVjEpIC0+IG1hcG1pbnVzKFBzLEIsQykuCm1hcG1pbnVzKFtYOlZ8UHNdLEIsW1g6VnxDXSkgOi0gbWFwbWludXMoUHMsQixDKS4KCgoKJSB1bmlmeSBvcGVuIGVuZGVkIG1hcHMgd2l0aCBwb3NzaWJseSB1bmluc3RhbnRpYXRlZCB2YXJpYWJsZSB0YWlsIGF0IHRoZSBlbmQKdW5pZnlfb2VtYXAoQSxCKSA6LSAoIHZhcihBKTsgdmFyKEIpICksICEsIEE9Qi4KdW5pZnlfb2VtYXAoQSxCKSA6LQogICAgICAgIHNwbGl0X2hlYWRzKEEsWHMtVDEpLCBtYWtlX21hcChYcyxNMSksCiAgICAgICAgc3BsaXRfaGVhZHMoQixZcy1UMiksIG1ha2VfbWFwKFlzLE0yKSwKICAgICAgICB1bmlmeV9vZV9tYXAoTTEtVDEsIE0yLVQyKS4KCm1ha2VfbWFwKEwsTSkgOi0gc2V0b2YoWDpWLGZpcnN0KFg6VixMKSxNKS4gJSByZW1vdmUgZHVwbGljYXRlcwptYWtlX21hcChbXSxbXSkuCgpzcGxpdF9oZWFkcyhbXSxbXS1bXSkuCnNwbGl0X2hlYWRzKFtYOlZ8VF0sW1g6Vl0tVCkgOi0gdmFyKFQpLCAhLCB0cnVlLgpzcGxpdF9oZWFkcyhbWDpWfFBzXSxbWDpWfEhzXS1UKSA6LSBzcGxpdF9oZWFkcyhQcyxIcy1UKS4KCiUgaGVscGVyIGZ1bmN0aW9uIGZvciB1bmlmeV9vZW1hcAp1bmlmeV9vZV9tYXAoWHMtVDEsWXMtVDIpIDotIFQxPT1bXSwgVDI9PVtdLCB1bmlmeV9tYXAoWHMsWXMpLgp1bmlmeV9vZV9tYXAoWHMtVDEsWXMtVDIpIDotIFQxPT1bXSwgc3VibWFwX29mKFlzLFhzKSwgbWFwbWludXMoWHMsWXMsVDIpLgp1bmlmeV9vZV9tYXAoWHMtVDEsWXMtVDIpIDotIFQyPT1bXSwgc3VibWFwX29mKFhzLFlzKSwgbWFwbWludXMoWXMsWHMsVDEpLgp1bmlmeV9vZV9tYXAoWHMtVDEsWXMtVDIpIDotIAogICAgICAgIG1hcG1pbnVzKFlzLFhzLEwxKSwgYXBwZW5kKEwxLFQsVDEpLAogICAgICAgIG1hcG1pbnVzKFhzLFlzLEwyKSwgYXBwZW5kKEwyLFQsVDIpLgoKJSUgPy0gdW5pZnlfb2VtYXAoW3o6c3RyaW5nLHk6Ym9vbHxNMV0sW3k6VCx4OmludHxNMl0pLgolJSBNMSA9IFt4OmludHxfRzE0MjZdLAolJSBUID0gYm9vbCwKJSUgTTIgPSBbejpzdHJpbmd8X0cxNDI2XS4KCiUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlJSUlCgptYWluOi0KCXByb2Nlc3MsCgloYWx0LgoKcHJvY2VzczotCiAgICBydW4oMCxUMCksIHByaW50KFQwKSwgbmwsCiAgICBydW4oMSxUMSksIHByaW50KFQxKSwgbmwsCiAgICBydW4oMixUMiksIHByaW50KFQyKSwgbmwsCiAgICBydW4oMyxUMyksIHByaW50KFQzKSwgbmwsCiAgICBydW4oNCxUNCksIHByaW50KFQ0KSwgbmwsCiAgICBydW4oNSxUNSksIHByaW50KFQ1KSwgbmwsCiAgICBydW4oNixUNiksIHByaW50KFQ2KSwgbmwsCiAgICBydW4oNyxUNyksIHByaW50KFQ3KSwgbmwsCiAgICBydW4oOCxUOCksIHByaW50KFQ4KSwgbmwsCiAgICAocnVuKDksVDkpIC0+IHdyaXRlKCJtdXN0IGZhaWwgYnV0ICIpLCBwcmludChUOSk7IHByaW50KGZhaWwpICksIG5sLAogICAgcnVuKDEwLFQxMCksIHByaW50KFQxMCksIG5sLAoJdHJ1ZS4KCjotIG1haW4uCgoK