1:- module(ifmap, [ ds_cover/3, parse_comma_list/2, parse_comma_list/3, 2 theory_to_cla/2, 3 cla/2, 4 show_cla/1, show_theory_cla/1, 5 theory_sum_tokens/2, 6 ds_theory_cover_with_constraint/5, 7% ds_cover_with_constraint/2, ds_cover_with_constraint/3, 8 invertable_type_map/4, 9 invertable_token_map/3, invertable_token_map/4 10 ]). % [2015/04/19], [2015/12/20] 11 12 13:- style_check(-singleton). 14:- use_module(library(ordsets)). 15:- use_module(pac('expand-pac')). 16:- use_module(util(misc)). 17:- use_module(util(meta2)). 18:- use_module(util(snippets)). 19:- use_module(pac(basic)). 20:- use_module(util(file)). 21:- use_module(util(obj)). 22:- use_module(util('emacs-handler')). 23:- use_module(util(coalgebra)). 24:- use_module(util(math)). 25 26term_expansion --> pac:expand_pac. 27 28:- use_module(pac(op)). 29 30:- op(700, xfx, =>). 31 32 /********************** 33 * tiny helpers * 34 **********************/ 35 36id_map(X):- maplist(pred([A-A]), X).
41% ?- show_theory_cla(theory([a,b], [[a => b]])). 42show_theory_cla(Theory) :- once(theory_to_cla(Theory, Z)), 43 once(show_cla(Z)). 44 45% 46tok(cla(X,_,_), X). 47typ(cla(_,X,_), X). 48sup(cla(_,_,X), X). 49 50 /******************************** 51 * ds programming helpers * 52 ********************************/ 53 54% ?- partition_to_restricted_massoc([[a:x, b:y, c:z]], a,[b,c], R). 55% ?- partition_to_restricted_massoc([[a:x, b:y, c:z], [a:u, a:v, c:z]],a,[b,c], R). 56 57partition_to_restricted_massoc(P, I, S, A):- 58 maplist(pred([I, S], [X, Y] 59 :- foldr( 60 pred([I,S], ([J:U, L-R, L-[J:U|R]] 61 :- memberchk(J, S), ! ) 62 & ([I:U, L-R, [I:U|L]-R]:- ! ) 63 & [_, LR, LR]), 64 X, []-[], Y)), 65 P, A). 66 67% ?- subst_types_back([[1:x]=>[2:y]], ds([a,b],dummy,dummy), T). 68%@ T = [([a:x]=>[b:y])]. 69 70subst_types_back(Theory, ds(Keys, _, _), Theory0):- !, 71 keys_to_assoc(Keys, A), 72 maplist(pred(A, [=>(L, R), =>(L0, R0)] 73 :- ( maplist(pred(A, [I:T, K:T] 74 :- memberchk(K-I, A)), 75 L, L0), 76 maplist(pred(A, [I:T, K:T] 77 :- memberchk(K-I, A)), 78 R, R0) 79 )), 80 Theory, Theory0). 81subst_types_back(Theory, ds(Cs, Ms), Theory0):- zip(Keys, C0s, Cs), 82 subst_types_back(Theory, ds(Keys,C0s,Ms), Theory0). 83 84% ?- get_key_pos(a, ds([b-1, d-3, a-2], any), K). 85% ?- get_key_pos(a, ds([b, d, a], [b, d, a], any), K). 86get_key_pos(K, ds(A,_,_), I):- get_key_pos(K, A, 1, I). 87get_key_pos(K, ds(Cs,_), I) :- get_key_assoc_pos(K, Cs, 1, I). 88% 89get_key_pos(K, [K|_], I, I):-!. 90get_key_pos(K, [_|A], I, J):- I0 is I+1, 91 get_key_pos(K, A, I0, J). 92% 93get_key_assoc_pos(K, [K-_|_], I, I):-!. 94get_key_assoc_pos(K, [_|Cs], I, J):- I0 is I+1, 95 get_key_assoc_pos(K, Cs, I0, J). 96% 97get_cla(K, ds(Ds,_), X):- memberchk(K-X, Ds), !. 98get_cla(K, ds(L, Ds,_), X):- get_cla(K, L, Ds, X). 99% 100get_cla(K, [K|_], [X|_], X):-!. 101get_cla(K, [_|Ks], [_|Ds], X):- get_cla(K, Ks, Ds, X). 102 103% ?- ds_build([a:cla([x],[t], [t-[x]])], DS). 104% ?- ds_build(a:cla([x],[t], [t-[x]]), DS), keyed_ds_cover(DS, CLA). 105% ?- ds_build((a-cla([x],[t], [t-[x]])); (a-cla([x],[t], [t-[x]])), DS), keyed_ds_cover(DS, CLA). 106% ?- ds_build((a-cla([x],[t], [t-[x]]));(b-cla([x],[t], [t-[x]])), DS), keyed_ds_cover(DS, CLA). 107% ?- ds_build((a-cla([x],[t], [t-[x]]));(b-cla([x],[t], [t-[x]])); im(a,b,[t-t],[x-x]), DS), keyed_ds_cover(DS, CLA). 108% ?- ds_build((a-cla([x],[t], [t-[x]])); (b-cla([x],[t], [t-[x]])); im(a,b,[t-t],[x-x]); im(b,a,[t-t],[x-x]), DS), keyed_ds_cover(DS, CLA). 109 110ds_build(A, ds(Clfs, Morphs)):- 111 once(ds_build(A, Clfs, [], Morphs, [])). 112% 113ds_build([], X, X, Y, Y):-!. 114ds_build([A], X, X0, Y, Y0):-!, ds_build(A, X, X0, Y, Y0). 115ds_build([A|B], X, X0, Y, Y0):-!, ds_build(A;B, X, X0, Y, Y0). 116ds_build(A ; B, X, X0, Y, Y0):-!, 117 ds_build(A, X, X1, Y, Y1), 118 ds_build(B, X1, X0, Y1, Y0). 119ds_build(A, X, X0, Y, Y0):- ds_add_basic(A, X, X0, Y, Y0), !. 120 121% 122ds_add_basic(Name := A, [Name:A|X], X, Y, Y). 123ds_add_basic(Name = A, [Name:A|X], X, Y, Y). 124ds_add_basic(Name - A, [Name:A|X], X, Y, Y). 125ds_add_basic(Name : A, [Name:A|X], X, Y, Y). 126ds_add_basic(B, X, X, [B|Y], Y). 127 128% ?- restrict_index_set([a-[1:a,2:b]], [1], R). 129% ?- restrict_index_set([a-[1:a,2:b], b-[2:c]], [1], R). 130% ?- restrict_index_set([a-[1:a,2:b], b-[2:c, 1:d]], [1], R). 131% ?- restrict_index_set([a-[1:a,2:b], b-[2:c, 1:d]], [1,2], R). 132restrict_index_set(T, I, T1):- 133 maplist(pred(I, [A-S, A-S0] 134 :- foldr( 135 pred(I, ([J:X, L, [J:X|L]]:- memberchk(J, I)) 136 & 137 ([_, L, L])) , 138 S, [], S0)), 139 T, T0), 140 foldr(pred([_-[], L, L] & [X, L, [X|L]]), T0, [], T1). 141 142% ?- eval(ifmap:cla @ flip @ empty, X). 143% ?- ifmap:cla(flip(cla([1,2],[a,b], [a-[1,2], b-[1,2]])), R). 144% ?- ifmap:cla(empty, X). 145% ?- eval(ifmap:cla::((pow @ empty)), V). 146% ?- eval(ifmap:cla::((pow @ empty)), V). 147% ?- ifmap:numcla(1, 10, X). 148 149% ?- eval(ifmap:cla :: (+) @ :numcla(1,3) @ :numcla(4,5), R). 150% ?- eval(ifmap:cla :: pow @ ((+) @ :numcla(1,3) @ :numcla(4,5)), R). 151% ?- eval(ifmap:cla :: merge @ :numcla(1,3)@ :numcla(2,4), X). 152% ?- eval(ifmap:cla(pow :: merge @ :numcla(1,3)@ :numcla(2,4)), X). 153% ?- eval(ifmap:cla(clean_disj(pow(cla([y,x,y],[a,b],[a-[x,x],b-[y]])))), Boole). 154 155% ?- ifmap:cla(tok(empty), X). 156% ?- ifmap:cla(typ(empty), X). 157% ?- ifmap:cla(pow(cla([1,2],[a,b], [a-[1],b-[2]])), X). 158% ?- ifmap:cla(supp(empty), X). 159% ?- ifmap:cla(merge(cla([1],[a],[a-[1]]), empty), X). 160% ?- ifmap:cla(merge(cla([1],[a],[a-[1]]), cla([1],[a],[a-[1]])), X). 161 162% ?- cla(flip(cla([1],[a],[a-[1]])), R). 163% ?- cla(flip(cla([1],[a],[a-[1,2]])), R). 164% ?- cla(pow(cla([1],[a, b],[a-[1], b-[2]])), R). 165% ?- cla(cla([1],[a], [a-[1]]) + cla([2],[b], [b-[2]]), R). 166 167cla(empty, cla([],[],[])):-!. 168cla(singleton(X), cla([A],[],[])):-!, cla(X, A). 169cla(tok(X), A):-!, cla(X, cla(A, _, _)). 170cla(typ(X), A):-!, cla(X, cla(_, A, _)). 171cla(supp(X), A):-!, cla(X, cla(_, _,A)). 172cla(flip(X), cla(Q, P, R)):-!, cla(X, cla(P, Q, R0)), 173 flip_powfun(R0, R). 174cla(pow(X), cla(K,A0,S0)):-!, 175 cla(X, cla(K, A, S)), 176 set(pow(A), A0), 177 power_cla(S, A0, S0). 178cla(X + Y, A1):-!, cla(X, A2), 179 cla(Y, A3), 180 cla_binary_sum(A2, A3, A1). 181cla(merge(A, B), cla(A1, A2, A3)):-!, 182 cla(A, cla(X, S, U)), 183 cla(B, cla(Y, T, V)), 184 misc:set(X + Y, A1), 185 misc:set(S + T, A2), 186 merge_support(U, V, A3). 187cla(cleaning_boole(X), A1):-!,cla(X, A2), 188 disjoint_boole_sort(A2, A1). 189cla(sort(X), A1):-!, cla(X, A2), 190 sort_cla(A2, A1). 191cla(normal(X), A1):-!, cla(X, A2), 192 cla_normalize(A2, A3), 193 canonical_cla(A3, A1). 194cla(X, X):-!. 195 196% ?- ifmap:support([a-[1,2]], 1, a). 197% ?- ifmap:support([a-[1,2]], 1, a). 198% ?- ifmap:support([], 3, a). 199fun_support(S, X, A):- member(B-U, S), B==A, !, 200 memberchk(X, U). 201% 202support(S, X, A):- S = [_|_], !, fun_support(S, X, A). 203support(P, X, A):- P\==[], call(P, X, A). 204 205% 206disjoint_boole_sort(cla(X,A,S), cla(X0,A0,S0)):- 207 sort(X, X0), 208 maplist(pred([P,Q]:- sort(P, Q)), A, A1), 209 sort(A1, A0), 210 sort_support(S, S1), 211 keysort(S1, S0). 212 213% ?- ifmap:sort_support([[a,a]-[1,2,2],[b,a]-[3,5,4]], R). 214%@ R = [[a]-[1, 2], [a, b]-[3, 4, 5]]. 215sort_support([_-[]|R], S):- !, sort_support(R, S). 216sort_support([K-A|R], [K0-A0|S]):- is_list(K), !, 217 sort(K, K0), 218 sort(A, A0), 219 sort_support(R, S). 220sort_support([K-A|R], [K-A0|S]):- 221 sort(A, A0), 222 sort_support(R, S). 223sort_support([], []). 224 225% ?- merge_support([a-[2]],[a-[3]], R). 226% ?- merge_support([b-[2], a-[1]], [a-[3]], R). 227merge_support(X, Y, Z):- sort_support(X, X0), 228 sort_support(Y, Y0), 229 merge_sorted_support(X0, Y0, Z). 230% 231merge_sorted_support([], X, X). 232merge_sorted_support(X, [], X). 233merge_sorted_support([A-U|R], [A-V|S], X):- !, 234 union(U,V,W), 235 merge_sorted_support([A-W|R], S, X). 236merge_sorted_support([A-U|R], [B-V|S], [A-U|X]):- A@<B, !, 237 merge_sorted_support(R, [B-V|S], X). 238merge_sorted_support(R, [B-V|S], [B-V|X]):- merge_sorted_support(R, S, X). 239 240% ?- eval((cla::(+)) @ (:numcla(1,2)) @ (:numcla(3,4)), R ). 241numcla(N0, N, cla(X, X, S)):- numlist(N0, N, X), 242 maplist(pred([I, I-[I]]), X, S). 243 244% ?- X = cla([1,2],[a,b],[a-[1]]), ifmap:cla(normal(X), Y). 245% ?- X = cla([1,2],[a,b],[a-[1],b-[2]]), cla(normal(X+X+X), Y), cla(sum(Y,Y), Z). 246% ?- cla(flip(cla([1,2,3], [a,b,c], [a-[1,2], b-[2,3], c-[1,3]])), F). 247cla_binary_sum(cla(X,Y,Z), cla(P,Q,R), cla(U,V,W)):- 248 set(X - P, U), 249 maplist(pred([A, (2:A)]), Q, Q0), 250 foldr(pred([A, L, [(1:A)|L]]), Y, Q0, V), 251 maplist(pred(X, [A-B, (2:A)- B0]:- set(X-B, B0)), R, R0), 252 foldr(pred(P, [A-B, L, [(1:A)- B0|L]] :- set(B-P, B0)), Z, R0, W). 253 254% 255cla_normalize(cla(X, Y, Z), cla(X0, Y0, Z0)):- 256 maplist(normalize_token, X, X0), 257 normalize_type(Y, Y0, D), 258 maplist(pred(D, [S-U, S0-U0]:- (maplist(normalize_token, U, U0), 259 fresh_index_var(S,[], P, V, S0), 260 memberchk(P-V,D))), 261 Z, Z0). 262 263% ?- normalize_token((a-(b-c)), X). 264normalize_token(A, X) :- normalize_token(A, X, []). 265 266normalize_token(A-B, X, Y):- !, normalize_token(A, X, X0), 267 normalize_token(B, X0, Y). 268normalize_token(A, [A|X], X). 269 270% 271normalize_type(X, Y, Assoc):- 272 maplist(pred([A, B, P-V]:- fresh_index_var(A, [], P, V, B)), X, Y, Assoc0), 273 keysort(Assoc0, Assoc1), 274 consecutive_merge(Assoc1, Assoc), 275 length(Assoc, L), 276 numlist(1, L, S), 277 maplist(pred([X-Y, Y]), Assoc, S). 278% 279consecutive_merge([], []). 280consecutive_merge([X,X|Y], Z):- !, consecutive_merge([X|Y],Z). 281consecutive_merge([X|Y], [X|Z]):- consecutive_merge(Y, Z). 282 283% ?- fun_to_powfun_flip([a-1, b-2], R). 284fun_to_powfun_flip(X, Y):-flip_zip(X, Y0), 285 sort(Y0, Y1), 286 rel_to_fun(Y1, Y). 287 288% ?- flip_zip([a-b, c-d], R). 289%@ R = [b-a, d-c]. 290flip_zip([],[]). 291flip_zip([A-B|R],[B-A|R0]):- flip_zip(R, R0). 292 293 294fun_to_zip(F, X, Z):- maplist(pred(F, [A, A-V]:- call(F, A, V)), X, Z). 295 296:- meta_predicate map(,,,). 297% ?- map(=, =, =, a, X). 298 299map(F, G, H, X, Y):- call(F, X, X0), 300 call(G, X0, Y0), 301 call(H, Y0, Y), 302 !. 303% 304sort_rel(X,Y) :- sort(X, Y). 305 306% [2013/07/18] 307%! flip_powfun(?S:fn, ?F:fn) is det. 308% flip the support relation S to a fn F so that 309% y in F(x) <==> x in S(y). 310% Property: if F is a sorted fn then so is S, and 311% vice versa. 312% ?- H=[a-[1,2], b-[2,3], c-[1,3]], flip_powfun(H, F), flip_powfun(F, G). 313% ?- H=[a-[1,2], b-[2,3], c-[1,3]], flip_powfun(H, F), flip_powfun(G, F). 314% ?- H=[a-[1,2], b-[2,3], c-[1,3]], flip_powfun(H, F), flip_powfun(G, F), flip_powfun(F, G). 315 316flip_powfun(X, Y):- 317 ( nonvar(X) -> 318 X = FnA, 319 Y = FnB 320 ; X = FnB, 321 Y = FnA 322 ), 323 powfun_to_rel(FnA, R, []), 324 flip_rel(R, R0), 325 sort(R0, R1), 326 rel_to_powfun(R1, FnB, []). 327% 328flip_rel([], []). 329flip_rel([A-B|R], [B-A|S]):- flip_rel(R, S). 330 331% ?- N = 100, findall(I-I, between(1, N, I), Zip), 332% time(repeat(1000, rel_powfun_by_findall(Zip, R))). 333 334% ?- rel_powfun_by_findall([1-a, 1-b, 2-b],R). 335rel_powfun_by_findall(X, Y):- 336 findall(A-L, (member(A-_, X), bagof(U, member(A-U, X), L)), Y0), 337 sort(Y0, Y). 338 339% ?- N = 1000, findall(I-I, between(1, N, I), Zip), 340% time(repeat(1000, rel_powfun_by_findall(Zip, R))). 341%@ % 1,016,015,001 inferences, 80.323 CPU in 80.792 seconds (99% CPU, 12649090 Lips) 342%@ N = 1000, 343%@ Zip = [1-1, 2-2, 3-3, 4-4, 5-5, 6-6, 7-7, 8-8, ... - ...|...]. 344 345% ?- N = 1000, findall(I-I, between(1, N, I), Zip), 346% time(repeat(1000, rel_powfun(Zip, R))). 347%@ % 2,006,001 inferences, 0.162 CPU in 0.162 seconds (100% CPU, 12371954 Lips) 348%@ N = 1000, 349%@ Zip = [1-1, 2-2, 3-3, 4-4, 5-5, 6-6, 7-7, 8-8, ... - ...|...].
rel_powfun([1-a, 1-b, 2-b],R).
?- S = [1-a, 1-b, 2-b], rel_powfun(S, R), ifmap:rel_powfun(S0, R).358rel_powfun(X, Y):- 359 ( var(X) -> powfun_to_rel(Y, X) 360 ; rel_to_powfun(X, Y, []) 361 ). 362% 363rel_to_powfun([], Y, Y). 364rel_to_powfun([A-B|R], [A-[B|P]|Y], Z):- 365 rel_to_powfun(R, A, R0, P, []), 366 rel_to_powfun(R0, Y, Z). 367% 368rel_to_powfun([], _, [], P, P). 369rel_to_powfun([A-B|R], A, U, [B|P], Q):-!, 370 rel_to_powfun(R, A, U, P, Q). 371rel_to_powfun(R, _, R, P, P). 372 373rel_to_powfun_flip(R, F):- rel_to_powfun(R, F0), flip_powfun(F0, F).
381% ?- rel_powfun([a-b, a-c, b-d], X), ifmap:fun_to_rel(X, Y). 382powfun_to_rel(X, Y):- powfun_to_rel(X, Y0, []), keysort(Y0, Y). 383 384% 385powfun_to_rel([], Y, Y). 386powfun_to_rel([U-L|X], Y, Z):- 387 powfun_to_rel(L, U, Y, Y0), 388 powfun_to_rel(X, Y0, Z). 389% 390powfun_to_rel([], _, Z, Z). 391powfun_to_rel([V|Vs], U, [U-V|Y], Z):- 392 powfun_to_rel(Vs, U, Y, Z). 393 394% 395fresh_index_var(J:A, P, [J|Q], V, B):- !, fresh_index_var(A, P, Q, V, B). 396fresh_index_var(A, P, [0|P], V, V:A). 397 398% ?- numcla(1,2,A), ifmap:numcla(3,4,B), ifmap:cla_list_sum([A,B], C). 399% ?- cla_list_sum([cla([],[a,b],[])], X). 400cla_list_sum(R0, cla(X, Y, Z)):- 401 maplist(pred([cla(A,_,_), A]), R0, R1), 402 maplist(pred([cla(_,A,_), A]), R0, R2), 403 maplist(pred([cla(_,_,A), A]), R0, R3), 404 choices(R1, X), 405 type_sum(R2, 1, [], Y), 406 fresh_support_index(R3, 1, [], Z0), 407 reverse(R1, P), 408 expand_support(Z0, P, [[]], [], Z). 409 410% 411cla_list(A+B, X, Y):- !, cla_list(A, X, Y0), cla_list(B, Y0, Y). 412cla_list(A, [A|X], X). 413 414 415 /************************************************* 416 * ds_core: colimit of distributed system. * 417 *************************************************/ 418 419 420% ?- ds_core([cla([x],[a], [a-[x]])], [im(1->1, [a-a], [x-x])], Cla). 421%@ Cla = cla([[x]], [[1:a]], [[1:a]-[[x]]]). 422ds_core(Cs, Is, cla(Tok, Typ, Sup)):- initial_type_sum(Cs, 1, Singletons, []), 423 ds_type_colimit(Is, Singletons, Typ), 424 ds_token_limit(Cs, Is, Tok), 425 core_support_rel_as_fun(Cs, Typ, Tok, Sup). 426 427% ?- initial_type_sum([cla([], [a,b], [])], 1, R, []). 428% ?- initial_type_sum([cla([], [a,b], []), cla([], [a,b], [])], 1, R, []). 429initial_type_sum([], _, X, X). 430initial_type_sum([cla(_,As,_)|Cs], I, X, Y):- raise_to_singleton(As, I, X, Z), 431 J is I + 1, 432 initial_type_sum(Cs, J, Z, Y). 433% 434raise_to_singleton([], _I, X, X). 435raise_to_singleton([A|As], I, [[I:A]|X], Y):- raise_to_singleton(As, I, X, Y). 436 437% ?- indexed_union_find_by_map([a-b], 1, 2, [], X). 438% ?- indexed_union_find_by_map([a-b, c-b], 1, 2, [], X). 439% ?- indexed_union_find_by_map([a-b, c-b, d-e], 1, 2, [], X). 440indexed_union_find_by_map([], _, _, X, X). 441indexed_union_find_by_map([A-B|Rest], I, J, X, Y):- 442 union_find(I:A, J:B, X, Z), 443 indexed_union_find_by_map(Rest, I, J, Z, Y). 444 445% ?- ds_type_colimit([im(1->2, [a-a], [])], [], X). 446% ?- ds_type_colimit([im(1->2, [a-a, b-a], [])], [], X). 447% ?- ds_type_colimit([im(1->2, [a-a, b-a, c-d], [])], [], X). 448% ?- ds_type_colimit([im(1->2, [a-a, b-a, c-d], []), im(2->1, [a-a, b-a, c-d], [])], [], X). 449ds_type_colimit([], X, X). 450ds_type_colimit([im(I->J, F, _)|R], X, Y):- 451 indexed_union_find_by_map(F, I, J, X, Z), 452 ds_type_colimit(R, Z, Y). 453 454% ?- ds_type_sum([cla([], [a,b], [])], S). 455% ?- ds_type_sum([cla([], [a,b], []), cla([], [a,b,c], [])], S). 456ds_type_sum(DS, S):- length(DS, N), 457 numlist(1, N, Ns), 458 ds_type_sum(DS, Ns, S, []). 459% 460ds_type_sum([], [], S, S). 461ds_type_sum([Cla|R], [J|Js], S, S0):- typ(Cla, T), 462 attach_index(T, J, S, S1), 463 ds_type_sum(R, Js, S1, S0). 464% 465attach_index([], _, S, S). 466attach_index([X|Xs], J, [J:X|S], S0):- attach_index(Xs, J, S, S0). 467 468% ?- ds_token_limit([cla([x],[a], [a-[x]])], [im(1->1, [a-a], [x-x])], Limit). 469%@ Limit = [[x]]. 470% ?- ds_token_limit([cla([x],[a], [a-[x]]), cla([x],[a], [a-[x]])], [im(1->2, [a-a], [x-x]), 471% im(2->1, [a-a], [x-x])], Limit). 472%@ Limit = [[x, x]]. 473ds_token_limit(Cla_list, Ims, Limit):-token_choices(Cla_list, Tok_choices), 474 filter_choices_by_ims(Tok_choices, Ims, Limit). 475 476% ?- token_choices([], R). 477% ?- token_choices([cla([a,b], [], [])], R). 478% ?- token_choices([cla([a,b], [], []), cla([a,b], [], [])], R). 479token_choices([], [[]]). 480token_choices([Cla|As], X):- token_choices(As, X0), 481 tok(Cla, Tok), 482 choices(Tok, X0, X, []). 483% 484choices([], _, Y, Y). 485choices([A|As], Ch, X, Y):- 486 cons_choice(Ch, A, X, X0), 487 choices(As, Ch, X0, Y). 488% 489cons_choice([], _A, X, X). 490cons_choice([B|Bs], A, [[A|B]|X], Y):- cons_choice(Bs, A, X, Y). 491 492% ?- filter_choices_by_ims([[a, b, c],[b, c, a]], [im(2->1, [], [a-b]), im(3->2, [], [b-c])], R). 493%@ R = [[a, b, c]]. 494% ?- filter_choices_by_ims([[b, a]], [im(1->2, [], [a-b]), im(2->1, [], [b-a])], R). 495%@ R = [[b, a]]. 496filter_choices_by_ims([], _, []). 497filter_choices_by_ims([X|R], Ims, Z):- 498 ( ims_compatible(Ims, X) -> Z = [X|U] 499 ; Z = U 500 ), 501 filter_choices_by_ims(R, Ims, U). 502 503% ?- ims_compatible([im(1->2, [], [b-a]), im(2->1, [], [a-b])], [a, b]). 504ims_compatible([], _). 505ims_compatible([im(I->J, _, F)|R], X):- nth1(I, X, Xi), 506 nth1(J, X, Xj), 507 memberchk(Xj-Xi, F), 508 ims_compatible(R, X). 509 510% ?- ds_core_support([cla(_,_,[a-[b]]), cla(_,_,[a-[b]])], [b, b], [1:a, 2:a]). 511% ?- ds_core_support([cla(_,_,[a-[b]]), cla(_,_,[a-[b]])], [b, b], []). 512ds_core_support(Cs, Choice, Ts):- core_support(Ts, Choice, Cs). 513% 514core_support([], _, _). 515core_support([J:T|R], Choice, Cs):- 516 nth1(J, Cs, C), 517 sup(C, S), 518 nth1(J, V, X), 519 memberchk(T-U, S), 520 memberchk(X, U), 521 core_support(R, Choice, Cs). 522 523% ?- core_support_rel_as_fun([cla([x],[a], [a-[x]])], [[1:a]], [[x]], Fun). 524%@ Fun = [[1:a]-[[x]]]. 525core_support_rel_as_fun(Cs, Colimit_types, Choices, Fun):- 526 support_as_fun(Colimit_types, Choices, Fun, Cs). 527% 528support_as_fun([], _Choices, [], _). 529support_as_fun([T|Ts], Choices, [T-S|R], Cs):- 530 core_support(Choices, T, S, Cs), 531 support_as_fun(Ts, Choices, R, Cs). 532% 533core_support([], _T, [], _Cs). 534core_support([Vec|R], T, Y, Cs):- 535 ( core_support(T, Vec, Cs) -> Y = [Vec|U] 536 ; Y = U 537 ), 538 core_support(R, T, U, Cs). 539 540% ?- choices([[a,c],[b,d]], X). 541% ?- type_sum([[a,b],[c,d,e]], 1, [], X). 542 543type_sum([], _, C, C). 544type_sum([Y|R], I, C, D):- J is I + 1, 545 maplist(pred(I, [A, I:A]), Y, Y0), 546 append(Y0, C, C0), 547 type_sum(R, J, C0, D). 548 549% 550fresh_support_index([], _, C, C). 551fresh_support_index([S|R], I, C, D):- J is I + 1, 552 maplist(pred(I, [A-U, (I:A)-U]), S, S0), 553 fresh_support_index(R, J, [S0|C], D). 554 555% 556expand_support([], _, _, C, C). 557expand_support([S|R], [U|V], M, C, D):- 558 maplist(pred(U, [S-X,S-Y] 559 :- scons(U,X,Y)), C, C0), 560 foldr(pred([U,M], [W-L, Z, [W-N|Z]] 561 :- scons(L, M, N)), 562 S, C0, C1), 563 scons(U, M, M0), 564 expand_support(R, V, M0, C1, D). 565 566% 567refresh_cla(X, cla(A, B, C), Tmap):- canonical_cla(X, cla(A, _, S)), 568 once(rename_types(S, C, Tmap)), 569 zip(B, _, C). 570% 571canonical_cla(cla(X,Y,Z), cla(X0, Y0, Z0)):- 572 sort(X, X0), 573 sort(Y, Y0), 574 maplist(pred([A-B, A-B0] :- sort(B, B0)), Z, Z1), 575 sort(Z1, Z0). 576 577% ?- eval(#(pred([[A-B],[B-A]]))@[1-a], R). 578% ?- eval(pred([[A-B],[B-A]])@[1-a], R). 579% ?- eval(ifmap:rel(-[1-a,2-b,3-c]), R). 580% ?- eval(ifmap:rel(-[1-a,2-b,3-c,4-a]), R). 581% ?- eval(ifmap:fn@(quote(choice)@(misc:set(pow([a,b]) \ singleton([])))), X). 582% ?- eval(ifmap:fn@(quote(choice)@ [[a,b],[c,d]]), R). 583% ?- eval(fn::[], X). 584% ?- eval(fn::[1-a,2-b], X). 585% ?- eval(misc:set(pow([a,b])), V). 586% ?- eval(ifmap:rel(-[a-1, b-2]),V). 587 588% ?- eval_fun(ifmap:fn::dom([1-a,2-b]), X). 589% ?- eval_fun(ifmap:fn:: -([1-a,2-b]), X). 590% ?- eval_fun(id([a,b]), R). 591% ?- eval_fun([a-a, b-b], F), eval_fun((F;F;F;F), G). 592% ?- eval_fun(-([a-1, b-2]), R). 593% ?- eval_fun(-([a-1, b-2, c-1]), R). 594% ?- eval_fun(-[a-1, b-2], V). 595% ?- eval_fun(-[a-1, b-2, c-1], V). 596 597eval_fun([], fun([])):-!. 598eval_fun(fun(A, B, C), fun(A, B, C)):-!. 599eval_fun(fun(A, B), fun(A, B)):-!. 600eval_fun(fun(A), fun(A)):-!. 601eval_fun([A|B], fun(D, R, [A|B])):-!, zip(D, R0, [A|B]), sort(R0, R). 602eval_fun(dom(fun(D,_,_)), D):-!. 603eval_fun(dom(fun(D,_)), D):-!. 604eval_fun(dom(fun(D)), D):-!. 605eval_fun(dom(X), A1):-!, eval_fun(X, A2), eval_fun(dom(A2), A1). 606eval_fun(ran(fun(_, R, _)), R):-!. 607eval_fun(ran(fun(_, G)), R):-!, fun_range(G, R). 608eval_fun(ran(fun(G)), R):-!, fun_range(G, R). 609eval_fun(ran(X), A1):-!, eval_fun(X, A2), eval_fun(ran(A2), A1). 610eval_fun(fld(fun(D, R, _)), F):-!, ord_union(D, R, F). 611eval_fun(fld(fun(_, G)), F):-!, fun_field(G, F). 612eval_fun(fld(fun(G)), F):-!, fun_field(G, F). 613eval_fun(fld(X), A1):-!, eval_fun(X, A2), eval_fun(fld(A2), A1). 614eval_fun(graph(fun(A1, A2, G)), G):-!. 615eval_fun(graph(fun(A1, G)), G):-!. 616eval_fun(graph(fun(G)), G):-!. 617eval_fun(graph(X), A1):-!,eval_fun(X, A2), eval_fun(graph(A2), A1). 618eval_fun(id(A), A1):-!, misc:set(A, A2), id_fun(A2, A1). 619eval_fun((F;G), A1):-!, eval_fun(F, A2), 620 eval_fun(G, A3), 621 fun_compose(A2, A3, A1). 622eval_fun(F+G, A1):-!, 623 eval_fun(F, A2), 624 eval_fun(G, A3), 625 fun_sum(A2, A3, A1). 626eval_fun(F*G, A1):-!, 627 eval_fun(F, A2), 628 eval_fun(G, A3), 629 fun_prod(A2, A3, A1). 630eval_fun(-fun(D, R, G), fun(R, D, A1)):-!, 631 fun_to_powfun_flip(G, A1). 632eval_fun(-fun(_, G), fun(A2)):-!, 633 fun_to_powfun_flip(G, A2). 634eval_fun(-fun(G), fun(A1)):-!, 635 fun_to_powfun_flip(G, A1). 636eval_fun(-X, A1):-!, 637 eval_fun(X, A2), 638 eval_fun(-A2, A1). 639eval_fun(choice(F), A1):-!, 640 misc:set(F, A2), 641 maplist(pred([[A|B], [A|B]-A]), A2, A1). 642eval_fun(quote(X), X):-!. % A bug ! 643 644% ?- rel(-[a-1, b-2], V). 645% ?- rel(id(pow([a,b])), R). 646 647rel(X, X):-is_list(X),!. 648rel(id(S), A1):-!, 649 misc:set(S, A2), 650 maplist(pred([A, A-A]), A2, A1). 651rel(dom(F), A1):-!, 652 misc:set(F, A2), 653 rel_domain(A2, A1). 654rel(ran(F), A1):-!, 655 misc:set(F, A2), 656 rel_range(A2, A1). 657rel(fld(F), A1):-!, 658 misc:set(F, A2), 659 rel_field(A2, A1). 660rel((F;G), A1):-!, 661 rel(F, A2), 662 rel(G, A3), 663 rel_compose(A2, A3, A1). 664rel(flip(F), A1):-!, 665 rel(F, A2), 666 maplist(pred([A-B, B-A]), A2, A1). 667rel(coa(F), A1):-!, 668 rel(F, A2), 669 sort(A2, A3), 670 rel_to_powfun(A3, A1). 671rel(-F, A1):-!, 672 misc:set(F, A2), 673 rel_powfun(A2, A3), 674 flip_powfun(A3, A1). 675% 676ap(fun(_, F, _), X, Y):- call(F, X, Y). 677 678% 679id_fun(X, Y):- maplist(pred([A, A-A]), X, Y). 680 681% 682power_flip_map(cla(_, _, R), R, L):- section(R, L). 683 684section(X, Y):- foldr(pred( [A-[X|_], L, [A-X|L]] 685 & 686 [_, L, L] 687 ), 688 X, [], Y). 689% 690ifmap_to_flip_inclusion(cla(X, A, _), Upper, ID):- 691 maplist(pred([P, P-[P]]), A, Upper), 692 maplist(pred([Q, Q-Q]), X, ID). 693 694% 695dom_of(F, D) :- zip(D0, _, F), sort(D0, D). 696ran_of(F, R) :- zip(_, R0, F), sort(R0, R). 697fld_of(F, Field):- zip(A, B, F), 698 sort(B, B0), 699 ord_union(A, B0, Field). 700 701% 702rel_domain(rel(G), D) :- dom_of(G, D). 703rel_domain(rel(D, _), D). 704rel_domain(rel(D, _, _), D). 705rel_domain(X, Y):- dom_of(X, Y). 706% 707rel_range(rel(G), R) :- ran_of(G, R). 708rel_range(rel(_, G), R) :- ran_of(G, R). 709rel_range(rel(_, R, _), R). 710rel_range(G, R):- ran_of(G, R). 711% 712rel_field(rel(G), F):- fld_of(G, F). 713rel_field(rel(_, G), F):- fld_of(G, F). 714rel_field(rel(_, _, G), F):- fld_of(G, F). 715rel_field(G, F):- fld_of(G, F). 716% 717rel_graph(rel(G), G). 718rel_graph(rel(_, G), G). 719rel_graph(rel(_, _, G), G). 720rel_graph(G, G). 721 722% 723fun_domain(fun(G), D) :- dom_of(G, D). 724fun_domain(fun(D, _), D). 725fun_domain(fun(D, _, _), D). 726fun_domain(X, Y):- dom_of(X, Y). 727% 728fun_range(fun(G), R) :- ran_of(G, R). 729fun_range(fun(_, G), R) :- ran_of(G, R). 730fun_range(fun(_, R, _), R). 731fun_range(G, R):- ran_of(G, R). 732% 733fun_field(fun(G), F) :- fld_of(G, F). 734fun_field(fun(_, G), F) :- fld_of(G, F). 735fun_field(fun(_, _, G), F):- fld_of(G, F). 736fun_field(G, F) :- fld_of(G, F). 737% 738fun_graph(fun(G), G). 739fun_graph(fun(_, G), G). 740fun_graph(fun(_, _, G), G). 741fun_graph(G, G). 742 743% % 744% zip([], [], []). 745% zip([A|A0], [B|B0], [A-B|R]):- !, zip(A0, B0, R). 746% zip([A|A0], [B|B0], [(A,B)|R]):- zip(A0, B0, R). 747 748comma_zip([], [], []). 749comma_zip([A|A0], [B|B0], [(A,B)|R]):- 750 comma_zip(A0, B0, R). 751 752% ?- ifmap_to_flip_inclusion(cla([1],[a,b], []), U, L). 753% ?- eval_fun(dom([a-b,c-d]), D). 754% ?- eval_fun(ran([a-b,c-d]), D). 755% ?- eval_fun(fld([a-b,c-d]), D). 756% ?- rel(-[a-1, b-1, c-2], R). 757% ?- coarsest_partition([a,b,c,d], [[a,b,c],[a,b,d]], P0), 758% maplist(sort, P0, P1), sort(P1, P). 759 760% The coarsest partition of a set by a family of sets. 761coarsest_partition(X, S, P):- length(S, L), 762 numlist(1, L, N), 763 zip(S, N, Z), 764 maplist(pred(Z, [A, I-A]:- indexes(A, Z, I)), X, Y), 765 keysort(Y, Y0), 766 index_merge(Y0, P). 767 768% ?- indexes(a, [[a]-1,[a]-2], X). 769indexes(_, [], []). 770indexes(A, [S-J|R], [J|P]):- memberchk(A, S), !, 771 indexes(A, R, P). 772indexes(A, [_|R], P):- indexes(A, R, P). 773 774% ?- index_merge([a-1,a-2,b-4, b-5], R). 775index_merge([], []). 776index_merge([A-M|X], Y):- index_merge(A, X, [M], Y). 777 778% 779index_merge(_, [], S, [S]). 780index_merge(A, [A-I|R], S, Y):- !, 781 index_merge(A, R, [I|S], Y). 782index_merge(_, [B-I|R], S, [S|Y]):- 783 index_merge(B, R, [I], Y). 784 785% ?- power_type_cla([a,b], C). 786% ?- power_type_cla([a,b,c], C). 787power_type_cla(T, cla(Ks, T, S)):- 788 set(pow(T), PowT), 789 length(PowT, N), 790 numlist(1, N, Ks), 791 zip(Ks, PowT, A), 792 power_type_support(T, A, S). 793% 794power_type_support([], _, []). 795power_type_support([P|P0], A, [P-Ks|R]):- 796 power_type_extension(P, A, Ks), 797 power_type_support(P0, A, R). 798 799power_type_extension(_, [], []). 800power_type_extension(P, [K-U|R], [K|Ks]):- 801 memberchk(P, U), !, 802 power_type_extension(P, R, Ks). 803power_type_extension(P, [_|R], Ks):- power_type_extension(P, R, Ks). 804 805% ?- power_cla([x-[a], y-[b]], [[x], [x,y]], R). 806power_cla(S, P, S0):- 807 maplist( 808 pred(S, ([A, A-U] :- maplist( 809 pred(S, ([B, U0] :- memberchk(B-U0, S); U0 =[])), 810 A, V), 811 append(V, U))), 812 P, S0). 813 814% ?- fun_sum([a-c, d-e],[b-c, d-e], R). 815% ?- fun_sum([a-c, b-c],[a-c, d-c], R). 816fun_sum(F, G, H):- 817 maplist(pred([X-Y, (0,X)-Y]), F, F0), 818 maplist(pred([U-V, (1,U)-V]), G, G0), 819 append(F0, G0, H). 820 821% ?- fun_prod([2-a,1-b], [1-c, 2-d], R). 822fun_prod(F, G, H):- 823 sort(F, F0), 824 sort(G, G0), 825 maplist(pred([X-Y, _-Z, X-(Y-Z)]), F0, G0, H).
fun_compose([a-1, b-2], [1-x, 2-y], R).830fun_compose(A, B, fun(D, R, F)):- 831 fun_domain(A, D), 832 fun_range(B, R), 833 fun_graph(A, F1), 834 fun_graph(B, F2), 835 fun_compose(F1, F2, F, []). 836% 837fun_compose([X-Y|F], G, [X-Z|H], H0):- 838 member(Y-Z, G), 839 !, 840 fun_compose(F, G, H, H0). 841fun_compose([], _, H, H). 842 843% ?- info_map_compose(im(1, 2, [a-b, c-d], [y-x, v-u]), im(2, 3, [b-e,d-f],[l-y, m-v]), R). 844% ?- info_map_compose(im(1, 2, [a-b], [y-x]), im(2, 3, [b-e],[l-y]), R). 845 846info_map_compose(im(A, B, F0, G0), im(B, C, F1, G1), im(A, C, F, G)):- 847 fun_compose(F0, F1, F), 848 fun_compose(G1, G0, G). 849 850% ?- ds_cover([cla([x],[a], [a-[x]])], [], R). 851% ?- ds_cover([cla([x,y],[a,b], []), cla([x,y], [a, b],[])], [], R). 852% ?- ds_cover([cla([x,y],[a,b], []), cla([x,y], [a, b],[])], [im(1,2,[a-a,b-b],[x-x,y-y])], R). 853ds_cover(ds(C, I), CLA):-!, ds_cover(C, I, CLA). 854% 855ds_cover(Cla_list, Imorph_list, cla(X, A, R)):- 856 cla_list_sum(Cla_list, Sum), 857 Sum = cla(X0, A0, R0), % like open bases of the product topology. 858 colimit_cover(Imorph_list, A0, A), 859 limit_cover(Imorph_list, X0, X), 860 merge_types(A, R0, R1), 861 maplist(pred(X, [T-S, T-S0]:- intersection(S, X, S0)), R1, R). 862% 863zip_colon([], [], []). 864zip_colon([X|Xs], [Y|Ys], [X:Y|Zs]):- zip_colon(Xs, Ys, Zs). 865 866% ?- keyed_ds_cover([k1:cla([x],[a], [a-[x]])], [], R). 867keyed_ds_cover(ds(X,Y), Z):-!, keyed_ds_cover(X, Y, Z). 868% 869keyed_ds_cover(Keyed_cla_list, Imorph_list, CLA):- 870 zip_colon(Keys, Cla_list, Keyed_cla_list), 871 length(Keys, Len), 872 numlist(1, Len, Ns), 873 maplist(pred([K, I, K-I]), Keys, Ns, KeyAssoc), 874 maplist(pred(KeyAssoc, ( [im(K, I, U, L), im(K0, I0, U, L)] 875 :- memberchk(K-K0, KeyAssoc), 876 memberchk(I-I0, KeyAssoc))), 877 Imorph_list, Imorph_list0), 878 ds_cover(Cla_list, Imorph_list0, Center_cla), 879 back_to_keyed_cla(Center_cla, CLA, KeyAssoc). 880 881% 882back_to_keyed_cla(cla(X, A, R), cla(X, A0, R0), KeyAssoc):- 883 maplist( 884 pred(KeyAssoc, 885 [U, U0]:- 886 maplist( 887 pred([U, U0, KeyAssoc], 888 [I:W, J:W]:- memberchk(J-I, KeyAssoc) 889 ), 890 U, U0) 891 ), 892 A, A0), 893 maplist( 894 pred(KeyAssoc, 895 [U-Z, V-Z]:- 896 maplist( 897 pred([U, V, KeyAssoc], 898 [W:Y, W0:Y] :- memberchk(W0-W, KeyAssoc) 899 ), 900 U, V) 901 ), 902 R, R0). 903 904 905% ?- ifmap:index_cla_name([a,b], [1-x,2-y], R). 906index_cla_name(A, Ms, Ns):- 907 maplist(pred(A, [I-X, um(K, X)]:- nth1(I, A, K)), 908 Ms, Ns). 909 910% ?- cover_imap([a-[1:x]], [], R). 911% ?- cover_imap([a-[1:x,2:y]],[],R). 912% ?- cover_imap([a-[1:x,2:y], b-[1:u, 2:v]], [], R). 913cover_imap([], X, X). 914cover_imap([N-A|B], X, Y):- cover_imap(A, N, X, X0), 915 cover_imap(B, X0, Y). 916% 917cover_imap([], _, X, X). 918cover_imap([J:A|R], N, X, Y):- select(J:S, X, X0), !, 919 cover_imap(R, N, [J:[A:N|S]|X0], Y). 920cover_imap([J:A|R], N, X, Y):- 921 cover_imap(R, N, [J:[A:N]|X], Y). 922 923% ?- keys_to_assoc([a, b, c], Z). 924keys_to_assoc(K, Z):- 925 foldr(pred([A, (I, U), (J, [A-J|U])] :- I is J + 1), K, (_, []), (1, Z)). 926 927% ?- rename_types([[a, b]- x, [c,d]-y], Y, Z). 928rename_types([], [], []):-!. 929rename_types(X, Y, Z):- 930 maplist(pred([A-_, A] & [A, A]), X, X0), 931 length(X0, Len), 932 numlist(1, Len, Ns), 933 maplist(pred([N, A-B, N-A, N-B] & [N, A, N-A, N]), Ns, X, Y, Z). 934 935% ?- inverse_partition_map([a-[1,2], b-[3,4]], Y). 936inverse_partition_map(X, Y):- 937 foldr(pred([A-S, U, V] 938 :- foldr(pred(A, [P, L,[P-A|L]]), S, U, V)), 939 X, [], Y). 940 941% ?- merge_types([[a,b]], [a-[1,2], b-[3,4]], R). 942% ?- merge_types([[a,b, c]], [a-[1,2], b-[3,4]], R). 943merge_types([], _, []). 944merge_types([A|As], R, [A-M|Bs]):- 945 merge_types(A, R, Xs, R0), 946 append(Xs, M), 947 merge_types(As, R0, Bs). 948 949% 950merge_types([], R, [], R). 951merge_types([T|Ts], R, [X|Xs], Q):- 952 select(T-X, R, R0), 953 !, 954 merge_types(Ts, R0, Xs, Q). 955merge_types([_|Ts], R, Xs, Q):- merge_types(Ts, R, Xs, Q). 956 957% ?- colimit_cover([], [1:a], L). 958colimit_cover(Ms, A, Limit):- 959 maplist(pred( 960 ([im(I, J, Ps, _), Qs]:- maplist(pred([I,J], [X-Y, (I:X)-(J:Y)]), Ps, Qs)) 961 & 962 ([im(I, J, Ps), Qs]:- maplist(pred([I,J], [X-Y, (I:X)-(J:Y)]), Ps, Qs))), 963 Ms, List_of_lists), 964 append(List_of_lists, Pairs), 965 maplist(pred([C, [C]]), A, A0), 966 union_find(Pairs, A0, Limit). 967 968% 969limit_cover([], X, X). 970limit_cover([im(I, J, _, Qs)|Ms], X, Y):- 971 filter(J, I, Qs, X, X0), 972 limit_cover(Ms, X0, Y). 973 974% 975filter(_, _, [], X, X). 976filter(I, J, [A-B|R], X, Y):- 977 filter(I, J, A, B, X, X0), 978 filter(I, J, R, X0, Y). 979 980filter(_, _, _, _, [], []). 981filter(I, J, A, B, [V|X], Y):- nth1(I, V, A), !, 982 nth1(J, V, C), 983 ( B==C 984 -> Y=[V|Y0], 985 filter(I, J, A, B, X, Y0) 986 ; filter(I, J, A, B, X, Y) 987 ). 988filter(I, J, A, B, [V|X], [V|Y]):- filter(I, J, A, B, X, Y). 989 990 /********************************************************* 991 * Parsing a distributed system in a suface syntax * 992 *********************************************************/ 993 994% ?- ds_parse_cover_with_constraint([a,b,c], Y). 995ds_parse_cover_with_constraint(X, X). 996 997% ;; > ; > \s\t 998% ?- parse_comma_list("", Y). 999% ?- parse_comma_list("a", Y). 1000% ?- parse_comma_list("a, b\n", Y). 1001% ?- parse_comma_list("a", Y). 1002% ?- parse_comma_list("a,b", Y). 1003% ?- parse_comma_list("a,b\n", Y). 1004% ?- parse_comma_list("a,' ' ,c", Y). 1005% ?- parse_comma_list("a,b\n\n\n", Y). 1006 1007parse_comma_list(codes, X, Y):-!, string_codes(Z, X), 1008 parse_comma_list(Z, Y). 1009parse_comma_list(string, X, Y):- parse_comma_list(X, Y). 1010% 1011parse_comma_list(X, Y):- term_string(T, X), 1012 ( T== end_of_file -> Y = [] 1013 ; comma_list(T, Y) 1014 ). 1015 1016% ?- parse_classifications(";", Y). 1017% ?- parse_classifications("a:b, c, d, k", Y). 1018parse_classifications(X, Y):- parse_comma_list(X, Z), 1019 maplist(sort_cla, Z, Y). 1020% 1021sort_cla(X:cla(Y, Z, U), X:cla(Y0, Z0, U0)) :- 1022 sort(Y, Y0), 1023 sort(Z, Z0), 1024 maplist(pred([P-Q, P-Q0]:- sort(Q, Q0)), U, U1), 1025 sort(U1, U0). 1026% 1027parse_informorphisms(X, Y):- parse_comma_list(X, Y). 1028% 1029parse_constraints(X, Y):- parse_comma_list(X, Y). 1030 1031 /********************************* 1032 * ds_cover_with_constraint * 1033 *********************************/ 1034 1035% 1036codes_string(X, Y):- string_codes(Y, X). 1037% 1038string_term(X, Y):- term_string(Y, X). 1039 1040% ?- maplist(parse_list(string), ["a,b", "x,y,z", "1,2,3"], X). 1041% ?- maplist(parse_list, ["a,b", "\s\t\n", "1,2,3"], X). 1042% ?- maplist(parse_list(codes), [`a,b`, `x,y,z`, `1,2,3`], X). 1043parse_list(X, Y):- parse_list(codes, X, Y). 1044% 1045parse_list(string, X, Y):-!, string_term(X, Z), comma_list(Z, Y). 1046parse_list(codes, X, Y):- string_codes(Z, X), 1047 string_term(Z, U), 1048 comma_list(U, Y). 1049 1050ds_cover_with_constraint([X, Y, Z], A):- 1051 ds_cover_with_constraint(X, Y, Z, A). 1052 1053% 1054ds_cover_with_constraint(Cla_list0, Imorph_list0, Con0, OutString):- 1055 ds_keys(Cla_list0, Keys, Cla_list), 1056 ds_prepare(Imorph_list0, Con0, Imorph_list, Con, Keys), 1057 ds_check(Cla_list, Imorph_list, Con), 1058 ds_cover_with_constraint(Cla_list, Imorph_list, Con, Tokens, Types), 1059 maplist(map_token_vector(Keys), Tokens, Tokens0), 1060 maplist(map_type(Keys), Types, Types0), 1061 term_string(Tokens0, U), 1062 term_string(Types0, V), 1063 atomics_to_string([U,"\n",V], OutString). 1064 1065% ?- ifmap:ds_cover_with_constraint([[cla([],[a,b],[])], [], []], X, Y). 1066% ?- ifmap:ds_cover_with_constraint([[cla([],[a,b],[]),cla([], [x,y],[])], [], []], X, Y). 1067ds_cover_with_constraint([Cla_list0, Imorph_list0, Con0], Types0, Tokens0):- 1068 ds_keys(Cla_list0, Keys, Cla_list), 1069 catch(( 1070 ds_prepare(Imorph_list0, Con0, Imorph_list, Con, Keys), 1071 ds_check(Cla_list, Imorph_list, Con), 1072 ds_cover_with_constraint(Cla_list, Imorph_list, 1073 Con, Tokens, Types), 1074 maplist(map_token_vector(Keys), Tokens, Tokens0), 1075 maplist(map_type(Keys), Types0, Types)), 1076 Error, 1077 ( ds_error_atomics(Keys, Error, M), 1078 atomics_to_string(M, OutString), 1079 writeln(OutString), 1080 fail 1081 )). 1082 1083% ?- indexed_cla_intern([a:cla([],[],[])], X, Y, Z, U). 1084% ?- trace, indexed_cla_intern([a:cla([],[],[]), b:cla([],[],[])], X, Y, Z, U). 1085% ?- indexed_cla_intern([a:cla([],[],[]), a:cla([],[],[])], X, Y, Z, U). % multiple index Error. 1086 1087indexed_cla_intern(Indexed_cla, Index_list, Cla_list, Vec_cla, Zip_index_num):- 1088 zip_colon(Index_list, Cla_list, Indexed_cla), 1089 Vec_cla =..[v|Cla_list], 1090 length(Indexed_cla, N), 1091 numlist(1, N, Ns), 1092 zip(Index_list, Ns, Zip_index_num), 1093 functor(Vec_cla, _, L), 1094 sort(Index_list, S), 1095 length(S, K), 1096 ( K \== N -> throw("multiple index found.") 1097 ; true 1098 ). 1099 1100% ?- ifmap:ds_keys([a,b,c], R, V). 1101% ?- ifmap:ds_keys([a,b:c,c], R, V). 1102ds_keys(X, Y, Z):- ds_keys(X, Y, Z, 1). 1103 1104% 1105ds_keys([A:X|R], [A|U], [X|V], I):- J is I + 1, 1106 ds_keys(R, U, V, J). 1107ds_keys([X|R], [I|U], [X|V], I):- J is I + 1, 1108 ds_keys(R, U, V, J). 1109ds_keys([], [], [], _). 1110 1111% ?- ifmap:key_index_prefix([a,b], X, 1:c). 1112% ?- ifmap:key_index_prefix([a,b], b:c, X). 1113key_index_prefix(Keys, K:X, I:X):- var(K), !, integer(I), nth1(I, Keys, K). 1114key_index_prefix(Keys, K:X, J:X):- key_index(Keys, K, 1, J). 1115key_index_prefix(_, X, X). 1116 1117% ?- key_index([a,b,c], b, I). 1118key_index(Key_list, Key, Index):- key_index(Key_list, Key, 1, Index). 1119% 1120key_index([K|_], K, I, I):-!. 1121key_index([_|R], K, I, J):- I0 is I + 1, key_index(R, K, I0, J). 1122 1123% ?- ifmap:map_type([a,b], [a:x, b:y], R), ifmap:map_type([a,b], S, R). 1124map_type(Keys, Type, Type0):- maplist(key_index_prefix(Keys), Type, Type0). 1125 1126% ?- map_token_vector([1,2], [a, b], X). 1127map_token_vector(Keys, Vec, Vec0):- maplist(pred([K, T, K:T]), Keys, Vec, Vec0). 1128 1129% ?- ds_prepare([], [], X, Y, []). 1130% ?- ds_prepare([im(u->v,[a-b], [])], [[u:a] => [v:b]], X, Y, [u,v]). 1131ds_prepare(Im, Con, Im0, Con0, Keys):- 1132 check_duplicate_free(Keys), 1133 maplist(pred(Keys, ([im(A->B, U, L), im(I->J, U, L)] 1134 :- key_index(Keys, A, I), 1135 key_index(Keys, B, J)) 1136 & ([im(A->B, U), im(I->J, U)] 1137 :- key_index(Keys, A, I), 1138 key_index(Keys, B, J)) 1139 ), 1140 Im, Im0), 1141 maplist(pred(Keys, ([L => R, L0 => R0]:- 1142 maplist(pred(Keys, 1143 [U:X, U0:X]:-key_index(Keys, U, U0)), L, L0), 1144 maplist(pred(Keys, 1145 [U:X, U0:X]:-key_index(Keys, U, U0)), R, R0))), 1146 Con, Con0). 1147 1148% 1149check_duplicate_free(X):- sort(X, X0), 1150 length(X, N), 1151 length(X0, N0), 1152 ( N == N0 -> true 1153 ; throw(multiple_index(A)) 1154 ). 1155 1156 1157 /***************************** 1158 * Check ds & build core * 1159 *****************************/ 1160 1161% ?- check_ds_build_core([], [], Core). 1162% ?- check_ds_build_core([cla([x],[a], [a-[x]])], [im(1->1, [a-a], [x-x])], Core). 1163% ?- check_ds_build_core([], [im(1->1, [a-a], [x-x])], Core). % << throw 1164check_ds_build_core(Cs, Ims, Core):- 1165 ds_check(Cs, Ims), 1166 ds_core(Cs, Ims, Core). 1167 1168% ?- ds_check([], []). 1169% ?- ds_check([cla([x],[a], [a-[x]])], [im(1->1, [a-a], [x-x])]). 1170ds_check(Cla_list, Imorph_list):- 1171 maplist(cla_check, Cla_list), 1172 maplist(im_check(Cla_list), Imorph_list). 1173 1174ds_check(Cla_list, Imorph_list, Con):- 1175 maplist(cla_check, Cla_list), 1176 maplist(im_check(Cla_list), Imorph_list), 1177 maplist(con_check(Cla_list), Con). 1178 1179cla_check(cla(X, A, S)):- forall( member(U-L, S), 1180 ( memberchk(U, A), 1181 subset(L, X) -> true 1182 ; throw('an unspecified token appears a supporter'(U-L)) 1183 )). 1184 1185% 1186im_check(Cla_list, im(I->J, FA, FX)):- 1187 is_map(FA), 1188 is_map(FX), 1189 nth1(I, Cla_list, Ci), 1190 nth1(J, Cla_list, Cj), 1191 Ci=cla(Xi, Ai,_), 1192 Cj=cla(Xj, Aj,_), 1193 is_map(FA, Ai, Aj), 1194 is_map(FX, Xj, Xi), 1195 check_imorph(Ci, Cj, FA, FX), 1196 !. 1197im_check(Cla_list, im(I->J, FA)):- 1198 nth1(I, Cla_list, cla(_, Ti, _)), 1199 nth1(J, Cla_list, cla(_, Tj, _)), 1200 is_map(FA), 1201 is_map(FA, Ti, Tj), 1202 !. 1203im_check(_, IM):- throw(failure(im_check(IM))). 1204 1205% 1206con_check(Cla_list, L=>R):- 1207 length(Cla_list, N), 1208 forall( ( member(A, L) ; member(A, R)), 1209 ( A = J:T, 1210 integer(J), 1211 1=<J, 1212 J=<N, 1213 nth1(J, Cla_list, cla(_, Typs, _)), 1214 memberchk(T, Typs))), 1215 !. 1216con_check(_, Seq):- throw(failure(con_check(Seq))). 1217 1218 1219% Error Messages 1220ds_error_atomics(_, unknown(X), X). 1221ds_error_atomics(_, cla_check(X), 1222 ["Classification check fail: ", X0, "\n[]"]):- term_string(X, X0). 1223ds_error_atomics(Keys, im_check(X), 1224 ["Informorphism check fail: ", X0, "\n[]"]):- 1225 X =.. [IM,I,J|R], 1226 maplist(key_index_prefix(Keys), [I0, J0], [I, J]), 1227 X1 =..[IM,I0, J0|R], 1228 term_string(X1, X0). 1229ds_error_atomics(Keys, con_check(L-R), 1230 ["Constraint check fail: ", X0, "\n[]"]):- 1231 maplist(key_index_prefix(Keys), L0, L), 1232 maplist(key_index_prefix(Keys), R0, R), 1233 term_string(L0-R0, X0). 1234ds_error_atomics(_, cla_not_with_key(X), 1235 ["Missing Key: ", X0, "\n[]"]) :- term_string(X, X0). 1236ds_error_atomics(_, duplicate_key(X), 1237 ["Duplicate Key: ", X0, "\n[]"]):- term_string(X, X0). 1238ds_error_atomics(_, X, ["other error: ", X0, "\n[]"]):- term_string(X, X0). 1239 1240% ?- ifmap:sum_by_constraint([[1:a,2:a]-[]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1241% ?- ifmap:sum_by_constraint([[1:a]-[2:a], [1:a]-[2:a]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1242% ?- ifmap:ds_cover_with_constraint([cla([x,y],[a],[a-[x,y]]),cla([x,y],[a],[a-[x,y]])], [im(1,2, [a-a],[x-x])], [[1:a,2:a]-[]], U, V). 1243% ?- ifmap:ds_cover_with_constraint([cla([x,y],[a],[a-[x,y]]),cla([x,y],[a],[a-[x,y]])], [im(1,2, [a-a],[x-x])], [[1:a]-[2:a]], U, V). 1244% ?- ifmap:ds_cover_with_constraint([cla([x,y],[a],[a-[x,y]]),cla([x,y],[a],[a-[x 1245 1246% ?- ifmap:ds_cover_with_constraint([cla([x,y],[a,b],[b-[y], a-[x]]),cla([x,y],[a],[a-[x,y]])], [im(1,2, [a-a,b-a],[x-x])], [[1:a]-[2:a],[2:a]-[1:a]], U, V). 1247%@ U = [], 1248% ?- ifmap:ds_cover_with_constraint([cla([x,y],[a,b],[b-[y], a-[x]]),cla([x,y],[a],[a-[x,y]])], [im(1,2, [a-a,b-a],[x-x])], [[1:a]-[2:a],[2:a]-[1:a]], U, V). 1249ds_cover_with_constraint(Cla_list, Imorph_list, Con, Tokens, Types):- 1250 sum_by_constraint(Con, Cla_list, CoreTokens), 1251 maplist(pred([cla(_,A,_), A]), Cla_list, TypS), 1252 type_sum(TypS, 1, [], IndexedTypes), 1253 colimit_cover(Imorph_list, IndexedTypes, Types), 1254 limit_cover_by_invertability(Imorph_list, CoreTokens, Tokens). 1255 1256% ?- ifmap:ds_theory_cover_with_constraint([theory([a],[[a]=>[a]])], [], [], X, Y). 1257% ?- ifmap:ds_theory_cover_with_constraint([theory([a],[[a]=>[a]]), theory([a],[[a]=>[a]])], [], [], X, Y). 1258% ?- ifmap:ds_theory_cover_with_constraint([theory([a],[[a]=>[a]]), theory([a],[[a]=>[a]])]), [im(1,2,[a-a])], [], X, Y). 1259% ?- ifmap:ds_theory_cover_with_constraint([theory([a],[a=>a]), theory([a],[a=>a])], [im(1,2,[a-a])], [[1:a]-[2:a]], X, Y). 1260ds_theory_cover_with_constraint(Theories, Imorph_list, Con, Tokens, Types):- 1261 theory_sum_tokens(Theories, CoreTokens), 1262 filter_with_constraints(CoreTokens, Con, CoreTokens0), 1263 maplist(pred([theory(A,_), A]), Theories, TypS), 1264 type_sum(TypS, 1, [], IndexedTypes), 1265 colimit_cover(Imorph_list, IndexedTypes, Types), 1266 limit_cover_by_invertability(Imorph_list, CoreTokens0, Tokens). 1267 1268% ?- ifmap:check_info_map(cla([x],[a], [a-[x]]), cla([y],[b],[b-[y]]), [a-b],[y-x]). 1269limit_cover_by_invertability([im(I, J, Zip, _)|Ms], X, Y):-!, 1270 limit_cover_by_invertability(X, Zip, I, J, X0), 1271 limit_cover_by_invertability(Ms, X0, Y). 1272limit_cover_by_invertability([im(I, J, Zip)|Ms], X, Y):-!, 1273 limit_cover_by_invertability(X, Zip, I, J, X0), 1274 limit_cover_by_invertability(Ms, X0, Y). 1275limit_cover_by_invertability([], X, X). 1276% 1277limit_cover_by_invertability([V|R], Z, I, J, [V|R0]):- 1278 limit_cover_by_invertability(Z, V, I, J), 1279 !, 1280 limit_cover_by_invertability(R, Z, I, J, R0). 1281limit_cover_by_invertability([_|R], Z, I, J, R0):-!, 1282 limit_cover_by_invertability(R, Z, I, J, R0). 1283limit_cover_by_invertability([], _, _, _, []). 1284 1285% 1286limit_cover_by_invertability(Zip, Vec, I, J):- 1287 nth1(I, Vec, Li-Ri), 1288 nth1(J, Vec, Lj-Rj), 1289 map_from_to(Li, Zip, Lj), 1290 map_from_to(Ri, Zip, Rj). 1291 1292% ?- ifmap:map_from_to([a,b], [a-1,b-2], [1,2]). 1293map_from_to([X|Y], Z, T):- memberchk(X-U, Z), 1294 memberchk(U, T), 1295 map_from_to(Y, Z, T). 1296map_from_to([], _, _). 1297 1298 1299% ?- ifmap:check_info_map(cla([x],[a], [a-[x]]), cla([y],[b],[b-[y]]), [a-b],[y-x]). 1300% ?- ifmap:check_info_map(cla([x],[a,b], [a-[x]]), cla([y],[b],[b-[y]]), [a-b],[y-x]). 1301ds_check_info_map(ds(FCs, IM)):- 1302 maplist(pred(FCs, [M] :- check_info_map(M, FCs)), IM). 1303 1304% 1305check_info_map(im(I, J, U, L), Cs):- !, 1306 memberchk(I-A, Cs), 1307 memberchk(J-B, Cs), 1308 check_info_map(A, B, U, L). 1309% 1310check_info_map(cla(_,A0, R0), cla(X1,_,R1), Upper_map, Lower_map):- 1311 forall((member(P, X1), 1312 member(T, A0), 1313 memberchk(P-Q, Lower_map), 1314 memberchk(T-S, Upper_map)), 1315 iff(support(R0, Q, T), support(R1, P, S))). 1316 1317% ?- set_equal([a,a,b], [b,a,b]). 1318set_equal(X, Y):- subset(X, Y), subset(Y, X). 1319 1320% ?- check_informorphism( cla([x],[a], [a-[x]]), cla([x],[a],[a-[x]]), 1321% [a-a],[x-x]). 1322% ?- check_informorphism( cla([x],[a], [a-[y]]), cla([x],[a],[a-[x]]), 1323% [a-a],[x-x]). % << false 1324 1325check_informorphism(C, D, U, L):- check_imorph(C, D, U, L). 1326 1327% check_informorphism(cla(X0, A0, R0), cla(X1, A1, R1), Upper_map, Lower_map):- 1328% zip(U, U0, Upper_map), 1329% set_equal(U, A0), 1330% subset(U0, A1), 1331% zip(V, V0, Lower_map), 1332% set_equal(V, X1), 1333% subset(V0, X0), 1334% forall( (member(P, X1), member(T, A0)), 1335% forall( (memberchk(P-Q, Lower_map), memberchk(T-S, Upper_map)), 1336% iff(support(R0, Q, T), support(R1, P, S)))). 1337 1338 1339% ?- check_imorph( cla([x],[a], [a-[x]]), cla([x],[a],[a-[x]]), 1340% [a-a],[x-x]). 1341% ?- check_imorph( cla([x],[a], [a-[y]]), cla([x],[a],[a-[x]]), 1342% [a-a],[x-x]). % << false 1343 1344% ?- time(repeat(10000, (check_imorph( cla([x],[a], [a-[x]]), cla([x],[a],[a-[x]]), [a-a],[x-x])))). 1345%@ % 220,001 inferences, 0.012 CPU in 0.012 seconds (98% CPU, 18585875 Lips) 1346%@ true. 1347 1348check_imorph(cla(X0, A0, R0), cla(X1, A1, R1), Upper_map, Lower_map):- 1349 forall( ( member(U-V, Upper_map), 1350 memberchk(U-Su, R0), 1351 memberchk(V-Sv, R1)), 1352 ( fun_inverse_image(Lower_map, Su, G), 1353 set_equal(G, Sv) 1354 )). 1355 1356% 1357check_adjoint_upper(X, Y, Upper, Ms, Mt):- 1358 forall(member(P-Q, Upper), 1359 iff(support(Ms, Y, P), support(Mt, X, Q))). 1360 1361check_adjoint_lower(X, Y, Lower, Ms, Mt):- 1362 forall(member(P-Q, Lower), 1363 iff(support(Ms, Q, X), support(Mt, P, Y))). 1364 1365% ?- X=cla([1,2],[a,b], [a-[1,2],b-[2]]), Y = cla([3,4],[c,d],[c-[3,4],d-[3]]), ifmap: build_info_map(X, Y, I). 1366% ?- X=cla([1,2],[a,b], [a-[1,2],b-[2]]), Y = cla([3,4],[c,d],[c-[3,4],d-[3]]), setof(I, ifmap: build_info_map(X, Y, I), S), length(S, N). 1367% ?- X=cla([1,2],[a,b], [a-[1,2],b-[2]]), Y = cla([3,4],[c,d],[c-[3,4],d-[3]]), ifmap: extend_info_map(X, Y, im([], []), IM). 1368% ?- X=cla([1,2],[a,b], [a-[1,2],b-[2]]), Y = cla([3,4],[c,d],[c-[3,4],d-[3]]), ifmap: extend_info_map(X, Y, im([b-d], [4-2]), Extended). 1369% ?- ifmap: extend_info_map(cla([x,z],[a,b],[a-[x], b-[z]]), cla([y,z],[c,d],[c-[y], d-[z]]), im([a-b],[]), R). 1370 1371extend_info_map(cla(X,A,S), cla(Y,B,T), im(U,L), im(U0,L0)):- 1372 zip(P, _, U), 1373 zip(Q, _, L), 1374 subtract(A, P, A0), 1375 subtract(Y, Q, Y0), 1376 build_adjoint(cla(X, A0, S), cla(Y0, B, T), U, L, U0, L0). 1377 1378% 1379build_info_map(C,D,im(U, L)):- build_adjoint(C,D,[],[],U,L). 1380 1381% 1382build_adjoint(cla(X, [A|As], R), cla([V|Vs], S, T), U, L, U0, L0):- !, 1383 member(B, S), 1384 check_adjoint_upper(A, B, U, R, T), 1385 member(W, X), 1386 check_adjoint_lower(V, W, L, R, T), 1387 build_adjoint(cla(X, As, R), cla(Vs, S, T), [A-B|U], [V-W|L], U0, L0). 1388build_adjoint(cla(X, [A|As],R), cla([], S, T), U, L, U0, L0):- !, 1389 member(B, S), 1390 check_adjoint_upper(A, B, U, R, T), 1391 build_adjoint(cla(X, As, R), cla([], S, T), [A-B|U], L, U0, L0). 1392build_adjoint(cla(X,[],R), cla([V|Vs], S, T), U, L, U0, L0):- !, 1393 member(W, X), 1394 check_adjoint_lower(V, W, L, R, T), 1395 build_adjoint(cla(X, [], R), cla(Vs, S, T), U, [V-W|L], U0, L0). 1396build_adjoint(cla(_,[],_), cla([], _,_), U, L, U, L). 1397 1398% ?- ifmap:rel_compose([a-1, a-2], [2-x, 2-y], R). 1399rel_compose(F, G, H):- rel_compose(F, G, H, []). 1400 1401rel_compose([], _, H, H). 1402rel_compose([X|R], G, H, K):- rel_compose_one(X, G, H, H0), 1403 rel_compose(R, G, H0, K). 1404 1405% 1406rel_compose_one(_,[], H, H). 1407rel_compose_one(X-Y, [Y-Z|G], [X-Z|H], K):- !, 1408 rel_compose_one(X-Y, G, H, K). 1409rel_compose_one(U, [_|G], H, K):- rel_compose_one(U, G, H, K). 1410 1411% ?- fun_inverse_image([a-1, b-2, c-2], [1], R). 1412% ?- fun_inverse_image([a-1, b-2, c-2], [1,2], R). 1413fun_inverse_image([], _, []). 1414fun_inverse_image([X-Y|R], A, [X|M]):- 1415 memberchk(Y, A), !, 1416 fun_inverse_image(R, A, M). 1417fun_inverse_image([_|R], A, M):- 1418 fun_inverse_image(R, A, M). 1419 1420% ?- ifmap:image_of_map([a-b,b-a,c-a], R). 1421image_of_map(Fn, Image):- zip(_,Vals, Fn), sort(Vals, Image). 1422 1423% ?- ifmap:find_map([a,b], [1,2,3], F). 1424find_map([A|As], R, [A-B|F]):- member(B, R), find_map(As, R, F). 1425find_map([], _, []).
1431% ?- invertable_type_map([],cla([],[],[]), cla([],[],[]), R). 1432% ?- invertable_type_map([],cla([],[a],[]), cla([],[],[]), R). 1433% ?- invertable_type_map([a-s],cla([1],[a],[a-[1]]), cla([2],[s],[s-[2]])). 1434% ?- invertable_type_map([a-s,b-t],cla([1],[a,b],[a-[1],b-[1]]), cla([2,3],[s,t],[s-[2],t-[3]])). 1435% ?- invertable_type_map([a-s,b-t],cla([1],[a,b],[a-[1],b-[2]]), cla([3],[s,t],[s-[3],t-[3]])). 1436% ?- invertable_type_map([a-s],cla([1],[a],[a-[1]]), cla([2],[s],[s-[2]]),R). 1437% ?- invertable_type_map([a-s],cla([1],[a],[a-[1]]), cla([2],[s],[s-[2]]),R). 1438 1439invertable_type_map(Map, SourceCla, TargetCla):- 1440 invertable_type_map(Map, SourceCla, TargetCla, _). 1441 1442% ?- is_map([a-b],[a],[b,c]). 1443% ?- is_map([a-b],[a,d],[b,c]). 1444% ?- is_map([a-b],[a],[]). 1445% ?- is_map([],[],[]). 1446is_map(Map, D, R) :- zip(D0, R0, Map), 1447 subset(D0, D), 1448 subset(D, D0), 1449 subset(R0, R). 1450 1451% 1452is_map(Zip):- sort(Zip, Zip0), 1453 check_unique_key(Zip0). 1454 1455% ?- check_unique_key([a-b,c-d]). 1456% ?- check_unique_key([a-b,a-d]). 1457check_unique_key([A-_, A-_|_]):- !,fail. 1458check_unique_key([_,X|M]):- check_unique_key([X|M]). 1459check_unique_key([_]). 1460check_unique_key([]). 1461 1462% 1463invertable_type_map(Map, theory(X,Y), TargetCla, AtomMap):- !, 1464 theory_to_cla(theory(X, Y), Z), 1465 invertable_type_map(Map, Z, TargetCla, AtomMap). 1466invertable_type_map(Map, SourceCla, theory(X, Y), AtomMap):- !, 1467 theory_to_cla(theory(X, Y), Z), 1468 invertable_type_map(Map, SourceCla, Z, AtomMap). 1469invertable_type_map(=, SourceCla, TargetCla, AtomMap):- !, 1470 typ(SourceCla, T), 1471 zip(T, T, Id_T), 1472 invertable_type_map(Id_T, SourceCla, TargetCla, AtomMap). 1473invertable_type_map(Map, SourceCla, TargetCla, AtomMap):- 1474 typ(SourceCla, U), 1475 typ(TargetCla, V), 1476 is_map(Map, U, V), 1477 image_of_map(Map, IoM), 1478 cla_restrict(IoM, TargetCla, TargetCla0), 1479 cla_boolean_atoms(SourceCla, cla(_,_,A)), 1480 cla_boolean_atoms(TargetCla0, cla(_,_,B)), 1481 zip(AtomsA,_,A), 1482 zip(AtomsB,_,B), 1483 sort_atoms(AtomsA, AtomsA0), 1484 sort_atoms(AtomsB, AtomsB0), 1485 exists_atom_map(Map, AtomsA0, AtomsB0, AtomMap). 1486 1487% ?- ifmap:invertable_token_map([1-3,2-4], cla([3,4],[a,b],[a-[3], b-[4]]), cla([1,2],[a,b],[a-[1], b-[2]]), R). 1488% ?- ifmap:invertable_token_map([1-3,2-3], cla([3,4],[a,b],[a-[3], b-[4]]), cla([1,2],[a,b],[a-[1], b-[2]]), R). 1489%@ R = [a-[a, b], b-[]]. 1490 1491invertable_token_map(Map, cla(Xa, Aa, Sa), cla(Xb, _Ab, Sb), TypeMap):- 1492 is_map(Map, Xb, Xa), 1493 maplist(invert_token_map_one(Map, Sa, Sb), Aa, TypeMap). 1494 1495invert_token_map_one(TokMap, Sa, Sb, A, A-B):- 1496 memberchk(A-U, Sa), 1497 collect_types_by_adjoint(Sb, TokMap, U, B, []). 1498 1499invertable_token_map(M, C1, C2) :- invertable_token_map(M, C1, C2, _). 1500 1501% ?- collect_types_by_adjoint([a-[1,2]],[1-3,2-4], [3,4], R, []). 1502collect_types_by_adjoint([], _, _, B, B). 1503collect_types_by_adjoint([A-V|S], TokMap, U, [A|R], R0):- 1504 member(K, V), 1505 memberchk(K-U0, TokMap), 1506 memberchk(U0, U), 1507 !, % checking adjointness. 1508 forall(member(P, V), (memberchk(P-Q, TokMap), memberchk(Q, U))), 1509 collect_types_by_adjoint(S, TokMap, U, R, R0). 1510collect_types_by_adjoint([_|S], TokMap, U, R, R0):- 1511 collect_types_by_adjoint(S, TokMap, U, R, R0).
1516% ?- sort_atoms([p([b,a],[2,1])], R). 1517sort_atoms(X, Y) :- maplist(pred(([p(U,V), p(U0,V0)] 1518 :- sort(U, U0), 1519 sort(V, V0))), 1520 X, Y).
1528% ?- exists_atom_map([a-b], [p([a],[])], [p([b],[])], R). 1529% ?- exists_atom_map([a-x,b-x], [p([a,b],[])], [p([x],[])], R). 1530exists_atom_map(Map, SourceAtoms, TargetAtoms, AtomMap):- 1531 fun_to_powfun_flip(Map, SetDict), 1532 invertable_atom_set(TargetAtoms, SetDict, SourceAtoms, AtomMap). 1533 1534% ?- invertable_atom_set([p([a],[])], [a-[b]], [p([b],[])], R). 1535invertable_atom_set([Q|As], Dict, Bs, [Q-P|AtomMap]):- 1536 Q = p(U, _), 1537 union_set_dict(U, Dict, U0), 1538 P = p(U0, _), 1539 memberchk(P, Bs), 1540 invertable_atom_set(As, Dict, Bs, AtomMap). 1541invertable_atom_set([], _, _, []). 1542 1543% ?- ifmap:union_set_dict([a,b], [a-[y, u],b-[z, v]], R). 1544union_set_dict(A, Dict, Set) :- proj_dict(A, Dict, S), 1545 append(S, S0), 1546 sort(S0, Set). 1547 1548% ?- proj_dict([a,b], [a-b,c-d], R). 1549% ?- proj_dict([a,b, x], [a-b,c-d], R). 1550% ?- proj_dict([c], [a-b,c-d], R). 1551proj_dict([A|R], Dict, [U|P]):- memberchk(A-U, Dict), 1552 !, 1553 proj_dict(R, Dict, P). 1554proj_dict([_|R], Dict, P) :- proj_dict(R, Dict, P). 1555proj_dict([], _, []). 1556 1557% ?- subst_multiple([a-[1,2], b-[3,4]], f(g(a,b),a), R). 1558%@ R = [f(g(1, 3), 1), f(g(1, 3), 2), f(g(1, 4), 1), f(g(1, 4), 2), f(g(2, 3), 1), f(g(2, 3), 2), f(g(2, 4), 1), f(g(..., ...), 2)]. 1559% ?- subst_multiple([a-[1,2], b-[3,4]], [a,b]->[b], R). 1560% ?- subst_multiple_massoc([[a1,a2]-[1,2], [b1,b2]-[3,4]], f(g(a1,b2),a2), R). 1561% ?- subst_multiple_massoc([[a1,a2]-[1,2], [b1,b2]-[3,4]], f(g(a1,b2),a2), R), 1562% subst_multiple([a-[1,2], b-[3,4]], f(g(a,b),a), R0), R=R0. 1563 1564subst_multiple(M, X, Y):- memberchk(X-Y, M), !. 1565subst_multiple(M, X, Y):- X=..[F|Xs], 1566 maplist(subst_multiple(M), Xs, Zs), 1567 choices(Zs, Us), 1568 maplist(pred(F, [A, B]:- B=..[F|A]), Us, Y). 1569 1570subst_multiple_massoc(M, X, Y):- member(K-Y, M), memberchk(X, K), !. 1571subst_multiple_massoc(M, X, Y):- X=..[F|Xs], 1572 maplist(subst_multiple_massoc(M), Xs, Zs), 1573 choices(Zs, Us), 1574 maplist(pred(F, [A, B]:- B=..[F|A]), Us, Y). 1575 1576% ?- subst_theory_multiple([[a]-[b,c]], [[a]=>[a]], R). 1577subst_theory_multiple(M, X, Y):- 1578 maplist(subst_sequent_multiple(M), X, X0), 1579 append(X0, Y). 1580 1581subst_sequent_multiple(M, =>(L, R), S):- 1582 maplist(pred(M, [X, U]:- (member(V-U, M), memberchk(X, V))), L, L0), 1583 maplist(pred(M, [X, U]:- (member(V-U, M), memberchk(X, V))), R, R0), 1584 choices(L0, C), 1585 choices(R0, D), 1586 choices([C,D], E), 1587 maplist(pred([[X, Y], =>(X, Y)]), E, S). 1588 1589% Moving theory forward / backward along a function. 1590% 1591% ?- move_theory_backward([x-a, y-a], [[a]=>[a], [a]=>[a]], R). 1592move_theory_forward(M, Theory, Theory0):- 1593 maplist(pred(M, ( [=>(L, R), =>(L0, R0)] 1594 :- 1595 maplist( pred(M, ([A, B]:- memberchk(A-B, M)) 1596 & 1597 [A, A]), 1598 L, L0), 1599 maplist( pred(M, ([A, B]:- memberchk(A-B, M)) 1600 & 1601 [A, A]), 1602 R, R0))), 1603 Theory, Theory1), 1604 simplify_theory(Theory1, Theory0). 1605 1606% 1607move_theory_backward(M, X, Y):- 1608 fun_to_powfun_flip(M, M0), 1609 maplist(move_sequent_backward(M0), X, X0), 1610 append(X0, Y0), 1611 simplify_theory(Y0, Y). 1612% 1613move_sequent_backward(M, =>(L, R), S):- 1614 maplist(pred(M, [X, U]:- memberchk(X-U, M)), L, L0), 1615 maplist(pred(M, [X, U]:- memberchk(X-U, M)), R, R0), 1616 choices(L0, C), 1617 choices(R0, D), 1618 choices([C,D], E), 1619 maplist(pred([[X, Y], =>(X, Y)]), E, S). 1620 1621% % Clustering; divide a graph into blocks. 1622union_find(X, Y):- union_find(X, [], Y). 1623 1624% ?- union_find([(a,b),(x,y), (x,x), (y, z), (b,c)], R). 1625% ?- union_find([(a-b),(x-y), (x-x), (y-z), (b-c)], R). 1626% ?- union_find([(a=b),(x=y), (x=x), (y=z), (b=c)], R). 1627 1628union_find([], X, X). 1629union_find([P|R], C, D):- (P = (X, Y); P = (X-Y); P = ( X = Y )), !, 1630 union_find(X, Y, C, C1), 1631 union_find(R, C1, D). 1632% 1633union_find(X, Y, Z, U):-select_cluster(X, Z, C, Z0), 1634 ( memberchk(Y, C) -> U=[C|Z0] 1635 ; select_cluster(Y, Z0, C0, Z1), 1636 append(C,C0, C1), 1637 U=[C1|Z1] 1638 ). 1639 1640% ?- select_cluster(a, [[a,b],[c,d]], C, X). 1641select_cluster(X, [], [X], []):-!. 1642select_cluster(X, [Y|Z], Y, Z):- memberchk(X, Y), !. 1643select_cluster(X, [Y|Z], U, [Y|V]):- select_cluster(X, Z, U, V). 1644 1645 1646% ?- theory_to_cla(theory([a,b], [[a,b]=>[]]), M). 1647% ?- theory_to_cla(theory([a,b], [[a,b]=>[],[a]=>[b]]), M). 1648% ?- theory_to_cla(theory([bird, penguine, fly], [[bird]=>[fly], [penguine]=>[bird], []=>[penguin], [fly, penguine]=>[]]), C). 1649% ?- theory_to_cla(theory([bird, fly, penguine], [[penguine]=>[bird], [fly, penguine]=>[]]), C2), C1 = cla([a, b], [bird, fly], [bird-[a], fly-[a,b]]), ifmap:build_info_map(C2, C1, R). 1650% ?- theory_to_cla(theory([a], [[a]=>[], []=>[a]]), C). 1651% ?- theory_to_cla(theory([a,b,c], [[]=>[a], []=>[b], []=>[c]]), C). 1652% ?- theory_to_cla(theory([bird, fly, penguine], [[penguine]=>[bird], [fly, penguine]=>[]]), C2). 1653% ?- theory_to_cla(theory([bird, fly, penguine], [[penguine]=>[bird], [fly, penguine]=>[], [bird]=>[fly]]), C2). 1654 1655% ?- theory_to_cla( 1656% theory([bird, fly, penguine], 1657% [[penguine]=>[bird], [fly, penguine]=>[]]), 1658% C2), 1659% C1 = cla([a, b], [bird, fly], [bird-[a], fly-[a,b]]), 1660% build_info_map(C1, C2, im(U, L)), 1661% ds_cover([C1, C2], [im(1, 2, U, L)], P). 1662 1663% ?- theory_to_cla( 1664% theory([bird, fly, penguine], 1665% [[penguine]=>[bird], [fly, penguine]=>[]]), 1666% C2), 1667% C1 = cla([a, b], [bird, fly], [bird-[a], fly-[a,b]]), 1668% build_info_map(C1, C2, im(U, L)), 1669% keyed_ds_cover([cla1:C1, cla2:C2], [im(cla1, cla2, U, L)], P). 1670 1671theory_to_cla(theory(S, SeqL), cla(T, S, Supp)):- set(pow(S), P), !, 1672 collect_token(P, SeqL, M), 1673 fresh_token(M, T, Supp). 1674 1675% ?- theory_sum_tokens([theory([a], [[a]=>[], []=>[a]])], C). 1676% ?- theory_sum_tokens([theory([a], [[a]=>[a]]), 1677% theory([a], [[a]=>[a]])], C). 1678% ?- theory_sum_tokens([theory([a], [[a]=>[a]]), 1679% theory([a], [[a]=>[a]]), theory([a], [[a]=>[a]])], C). 1680 1681theory_sum_tokens(Theories, Tokens):- 1682 maplist(theory_to_seqs, Theories, ListofTokenSets), 1683 choices(ListofTokenSets, Tokens). 1684 1685% ?- ifmap:theory_to_seqs(theory([bird, fly, penguine], [[penguine]=>[bird], [fly, penguine]=>[], [bird]=>[fly]]), C2). 1686theory_to_seqs(theory(S, Con), Seqs):- 1687 set(pow(S), P), !, 1688 collect_token(P, Con, Atoms), 1689 maplist(atom_to_seq(S), Atoms, Seqs). 1690 1691% 1692atom_to_seq(S, Atom0, Atom-Comp):- sort(Atom0, Atom), 1693 subtract(S, Atom, Comp0), 1694 sort(Comp0, Comp). 1695 1696% 1697collect_token([], _, []). 1698collect_token([P|R], L, [P|S]):- satisfy_all(P, L), !, 1699 collect_token(R, L, S). 1700collect_token([_|R], L, S):- collect_token(R, L, S). 1701 1702% ?- satisfy([a,b], [a]=>[b]). 1703satisfy(X, =>(Y, Z)):- subset(Y, X), !, 1704 member(A, Z), 1705 member(A, X). 1706satisfy(_, _). 1707% 1708satisfy_all(X, L):- maplist(satisfy(X), L). 1709 1710% 1711fresh_token(P, X, S):- length(P, N), 1712 ( N == 0 1713 -> X=[], S=[] 1714 ; numlist(1, N, X), 1715 zip(X, P, Z), 1716 flip_powfun(Z, S) 1717 ). 1718 1719% ?- simplify_theory([[a,b]=>[c,d], [a]=>[d], [b]=>[c]], R). 1720simplify_theory(Sequents, Sequents0):- 1721 maplist(pred([=>(L,R), =>(L0, R0)] 1722 :- (sort(L, L0), sort(R, R0))), 1723 Sequents, Sequents1), 1724 sort(Sequents1, Sequents2), 1725 simplify_theory(Sequents2, [], Sequents3), 1726 reverse(Sequents3, Sequents0). 1727 1728% 1729simplify_theory([], X, X). 1730simplify_theory([Q|S], X, Y):- weakened_identity(Q), !, 1731 simplify_theory(S, X, Y). 1732simplify_theory([Q|S], X, Y):- member(P, X), sequent_stronger(P, Q), !, 1733 simplify_theory(S, X, Y). 1734simplify_theory([Q|S], X, Y):- sequent_remove_weaker(Q, X, X0), 1735 simplify_theory(S, [Q|X0], Y). 1736 1737% 1738sequent_remove_weaker(_, [], []). 1739sequent_remove_weaker(Q, [P|X], Y) :- sequent_stronger(Q, P), !, 1740 sequent_remove_weaker(Q, X, Y). 1741sequent_remove_weaker(Q, [P|X], [P|Y]) :- sequent_remove_weaker(Q, X, Y). 1742 1743% 1744sequent_stronger(=>(L, R), =>(L0, R0)):- subset(L, L0), subset(R, R0). 1745 1746% 1747weakened_identity(=>(L, R)):- member(A, L), member(A, R). 1748 1749% ?- ifmap:cla_boolean_atoms([a],[x], [x-[]], A,B,C). 1750% ?- cla_boolean_atoms([a,b],[x], [x-[a]], A,B,C). 1751% ?- cla_boolean_atoms([a,b], [x,y], [x-[a],y-[b]], A,B,C). 1752% ?- cla_boolean_atoms([a,b], [x,y], [], A,B,C). 1753% ?- ifmap:cla_boolean_atoms([a,b], [x,y], [x-[a],y-[b]], A,B,C). 1754 1755cla_boolean_atoms(cla(Tok, Typ, Sup), cla(Tok0, Typ0, Sup0)):- 1756 cla_boolean_atoms(Tok, Typ, Sup, Tok0, Typ0, Sup0). 1757 1758% 1759cla_boolean_atoms(Tok, Typ, Sup, Tok0, Typ0, Sup0):- 1760 cla_boolean_atoms(Typ, Sup, [p([],[])-Tok], Sup0), 1761 maplist(pred([A, B, A-B]), Typ1, Tok1, Sup0), 1762 sort(Typ1, Typ0), 1763 sort(Tok1, Tok0). 1764 1765% 1766cla_complete_boolean_atoms(cla(Tok, Typ, Sup), 1767 cla(Tok, Typ0, Sup0)):- 1768 complete_support(Typ, Sup, Sup1), 1769 refine_boolean_atoms(Tok, Sup1, Typ0, Sup0). 1770 1771% 1772cla_boolean_atoms([A|As], Sup, R0, R):- 1773 ( memberchk(A-X, Sup); X = []), 1774 !, 1775 cla_boolean_atoms_(R0, A, X, [], R1), 1776 cla_boolean_atoms(As, Sup, R1, R). 1777cla_boolean_atoms([], _, R, R). 1778 1779% 1780cla_boolean_atoms_([p(L,R)-X|P], A, Y, U0, U1):- 1781 intersection(X, Y, X0), 1782 subtract(X, Y, X1), 1783 add_non_empty([p([A|L], R)-X0, p(L,[A|R])-X1], U0, U2), 1784 cla_boolean_atoms_(P, A, Y, U2, U1). 1785cla_boolean_atoms_([], _, _, R, R). 1786 1787% ?- ifmap:add_non_empty([a-[], b-[c]], R, R0). 1788add_non_empty([_-[]|A], R, R0) :- !, add_non_empty(A, R, R0). 1789add_non_empty([X|A], R, R0):- !, add_non_empty(A, [X|R], R0). 1790add_non_empty([], R, R). 1791 1792% ?- ifmap:cla_restrict([b], cla(_,_,[a-[1],b-[2]]), R). 1793%@ R = cla([2], [b], [b-[2]]). 1794% ?- ifmap:(numcla(1,3, A), numcla(1, 3, B), cla(A+B, C), cla_restrict([1:1, 2:1], C, D)). 1795cla_restrict(S0, cla(_, _, P), cla(X0, S0, P0)):- 1796 collect(pred(S0, [A-_]:- memberchk(A, S0)), P, P0), 1797 zip(_, Xs, P0), 1798 union(Xs, X0). 1799 1800% ?- ifmap:rename_literals([a,a,~(a)], [a-b], R). 1801% ?- ifmap:rename_literals([a,a,~(a), b, ~(c)], [a-b], R). 1802 1803is_super(X-_, S):- !, subset(S, X). 1804is_super(X, S):- subset(S, X). 1805 1806% ?- ifmap:inverse_type_map([a-1, b-2], cla(_, _, [[a]-a,[b]-b]), cla(_,_, [[1]-1, [2]-2]), G). 1807% ?- ifmap:inverse_type_map([a-1, b-2], [[a],[b]], [[1], [2]], G). 1808inverse_type_map(F, cla(_, _, Sup), Trgt, G):- !, 1809 zip(Src,_,Sup), 1810 inverse_type_map(F, Src, Trgt, G). 1811inverse_type_map(F, Src, cla(_, _, Sup), G):- !, 1812 zip(Trgt, _,Sup), 1813 inverse_type_map(F, Src, Trgt, G). 1814inverse_type_map(F, Src, Trgt, G):- 1815 maplist(pred(F, [X, X-Y]:- 1816 rename_literals_with_complementary_rule(X, F, Y)), 1817 Src, Zip), 1818 maplist(pred(Trgt, ( [A-B, A-C]:- 1819 collect_supersets(Trgt, B, C))), 1820 Zip, Zip0), 1821 flip_powfun(Zip0, G). 1822 1823 1824% ?- ifmap:type_support_by_tok_vec(1:a, [[a]-[]]). 1825% ?- ifmap:type_support_by_tok_vec(1:b, [[a]-[]]). 1826% ?- ifmap:type_support_by_tok_vec(2:b, [[a]-[], [b]-[]]). 1827% ?- ifmap:type_support_by_tok_vec(2:b, [[a]-[], [a, c]-[]]). 1828 1829type_support_by_tok_vec(N:A, Svec):- type_support_by_tok_vec(N, A, Svec). 1830 1831type_support_by_tok_vec(1, A, [L-_|_]):- !, memberchk(A, L). 1832type_support_by_tok_vec(2, A, [_,L-_|_]):- !, memberchk(A, L). 1833type_support_by_tok_vec(3, A, [_,_,L-_|_]):- !, memberchk(A, L). 1834type_support_by_tok_vec(N, A, Svec):- nth1(N, Svec, L-_), 1835 memberchk(A, L). 1836 1837% 1838types_support_by_tok_vec([A|As], V):- 1839 type_support_by_tok_vec(A, V), 1840 types_support_by_tok_vec(As, V). 1841types_support_by_tok_vec([], _). 1842 1843% ?- ifmap:tok_vec_respect_seq([[a]-[b]], [1:a]-[1:b]). 1844% ?- ifmap:tok_vec_respect_seq([[a, b]-[1:c]], [1:a]-[1:b]). 1845% ?- ifmap:tok_vec_respect_seq([[a]-[b]], [1:b]-[1:b]). 1846% ?- ifmap:tok_vec_respect_seq([[a]-[b]], []-[1:a]). 1847% ?- ifmap:tok_vec_respect_seq([[a]-[b]], []-[1:c]). 1848 1849tok_vec_respect_seq(Svec, L-R):- types_support_by_tok_vec(L, Svec), !, 1850 member(A, R), 1851 type_support_by_tok_vec(A, Svec), 1852 !. 1853tok_vec_respect_seq(_, _). 1854 1855% 1856full_respect_by_tok_vec([A|Con], Svec):- !, 1857 tok_vec_respect_seq(Svec, A), 1858 full_respect_by_tok_vec(Con, Svec). 1859full_respect_by_tok_vec([], _). 1860 1861% ?- ifmap:filter_with_constraints([], [], R). 1862% ?- ifmap:filter_with_constraints([[[a]-[]]], [[1:a]-[1:a]], R). 1863% ?- ifmap:filter_with_constraints([[[a]-[]]], [[1:a]-[1:b]], R). 1864 1865filter_with_constraints([Vec|Vecs], Con, [Vec|Vecs0]):- 1866 full_respect_by_tok_vec(Con, Vec), 1867 filter_with_constraints(Vecs, Con, Vecs0). 1868filter_with_constraints([_|Vecs], Con, Vecs0):- 1869 filter_with_constraints(Vecs, Con, Vecs0). 1870filter_with_constraints([], _, []). 1871 1872% ?-ifmap:subst_key([a-1],[a:t]-[], R). 1873subst_key(Zip, L-R, L0-R0):- 1874 maplist(pred(Zip, [A:U, B:U] :- memberchk(A-B, Zip)), L, L0), 1875 maplist(pred(Zip, [A:U, B:U] :- memberchk(A-B, Zip)), R, R0). 1876 1877% ?- ifmap:channel_by_constraint([[k:a]-[k:a]],[k-cla([x],[a],[a-[x]])], Core, KeyZip). 1878% ?- ifmap:channel_by_constraint([[m:a]-[k:a], [k:a]-[m:a]],[k-cla([x],[a],[a-[x]]), m-cla([x],[a],[a-[x]])], Core, KeyZip). 1879% ?- ifmap:channel_by_constraint([[k:a,m:a]-[]],[k-cla([x],[a],[a-[x]]), m-cla([x],[a],[a-[x]])], Core, KeyZip). 1880%@ Core = [[]], 1881%@ KeyZip = [k-1, m-2] . 1882 1883channel_by_constraint(Con, KeyedCs, Core, KeyZip):- 1884 zip(Keys, _Cs, KeyedCs), 1885 length(Keys, N), 1886 numlist(1, N, Ns), 1887 zip(Keys, Ns, KeyZip), 1888 maplist(subst_key(KeyZip), Con, Con0), 1889 sum_by_constraint(Con0, _ListOfSeqSet, Core). 1890 1891% ?- ifmap:sum_by_constraint([[1:a,2:a]-[]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1892% ?- ifmap:sum_by_constraint([[1:a]-[2:a], [1:a]-[2:a]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1893 1894sum_by_constraint(Con, Cs, Core):- 1895 maplist(convert_seq_set, Cs, ListOfSeqSet), 1896 misc:choices(ListOfSeqSet, SeqVecSet), 1897 filter_with_constraints(SeqVecSet, Con, Core). 1898 1899% ?- ifmap:convert_seq_set(cla([x],[a],[a-[x]]), R). 1900% ?- ifmap:convert_seq_set(cla([x],[a],[a-[x],b-[x]]), R). 1901 1902convert_seq_set(Cla, SeqSet):- 1903 ifmap:cla_complete_boolean_atoms(Cla, cla(_, Pairs, _)), 1904 maplist(pred([p(U,V), U-V]), Pairs, SeqSet).
Typ = [p(U1,V1), ..., p(Um, Vm)], and Sup0 = [p(U1,V1) - P1, ..., p(Um, Vm) - Pm]
such as follows: P1, ..., Pm are the atoms obtained by partitioning Tok
with given support Sup (cf. Channel theory), and the extension of p(Ui, Vi)
is Pi (i = 1, ..., m), where the notion of the extension is defined as follows.
The extension of Ti is Xi (i=1,..,n). The extension of p(U, V) is
the set of tokens in Tok which is a member of the extension
of any element of U, and on the other hand is not an elemenent
of the extension of W for any W in V.
1925% ?- ifmap:refine_boolean_atoms([a,b], [], A,B). 1926% ?- ifmap:refine_boolean_atoms([], [x], A,B). 1927% ?- ifmap:refine_boolean_atoms([a,b], [x-[a],y-[b]], A,B). 1928% ?- ifmap:refine_boolean_atoms([a], [x-[a]], A,B). 1929% ?- ifmap:refine_boolean_atoms([a,b], [x-[a],y-[b]], A,B). 1930 1931refine_boolean_atoms([], _, [], []):- !. 1932refine_boolean_atoms(Tok, Sup, Typ0, Sup0):- 1933 refine_boolean_atoms(Sup, [p([],[])-Tok], Sup0), 1934 zip(Typ0, _, Sup0). 1935 1936% 1937refine_boolean_atoms([A-X|As], R0, R):- 1938 refine_boolean_atoms_update(R0, A, X, R1), 1939 refine_boolean_atoms(As, R1, R). 1940refine_boolean_atoms([], R, R). 1941 1942% 1943refine_boolean_atoms_update([p(U,V)-X|R], A, Y, S):- 1944 intersection(X, Y, X1), 1945 subtract(X, Y, X2), 1946 ( X1 ==[] 1947 -> S = S1 1948 ; S = [p([A|U], V)-X1|S1] 1949 ), 1950 ( X2 == [] 1951 -> S1 = S2 1952 ; S1 = [p(U,[A|V])-X2| S2] 1953 ), 1954 refine_boolean_atoms_update(R, A, Y, S2). 1955refine_boolean_atoms_update([], _, _, []). 1956 1957% ?- ifmap: (numcla(1,3, A), numcla(1, 3, B), cla(A+B, C), cla_restrict(C, [1:1, 2:1], D)). 1958 1959%% eval_boolean_type(+C:cla, +E:boolen_exp, -V:list) det 1960% is True if 1961% V is unified with the list of tokens of C which satisfies E. 1962 1963% ?- ifmap:eval_boolean_type(a, cla(_,_, [a-[1]]), R). 1964% ?- ifmap:eval_boolean_type(a+a & a, cla(_,_, [a-[1]]), R). 1965 1966% An example use of flip options. 1967eval_boolean_type(A&B,A1,A2):-!, 1968 eval_boolean_type(A,A1,A3), 1969 eval_boolean_type(B,A1,A4), 1970 misc:set(A3&A4,A2). 1971eval_boolean_type(A+B,A1,A2):-!, 1972 eval_boolean_type(A,A1,A3), 1973 eval_boolean_type(B,A1,A4), 1974 misc:set(A3+A4,A2). 1975eval_boolean_type(A,cla(A1,A2,Sup),X):-!, 1976 memberchk(A-X,Sup). 1977 1978% 1979rename_literals_with_complementary_rule(X, F, Y):- 1980 rename_literals(X, F, Y0), 1981 complementary_rule(Y0, Y1), 1982 sort(Y1, Y). 1983 1984% ?- ifmap: rename_literals([a,a,~(a)], [a-b], R). 1985% ?- ifmap: rename_literals([a,a,~(a), b, ~(c)], [a-b], R). 1986rename_literals([X|R], F, [Y|R0]):- 1987 ( X = ~(X0), Y = ~(V) ; X0 = X, Y = V ), 1988 ( memberchk(X0-V, F) ; V = X0 ), 1989 rename_literals(R, F, R0). 1990rename_literals([], _, []). 1991 1992% 1993complementary_rule(Y, []):- member(~(X), Y), member(X, Y), !. 1994complementary_rule(Y, Y). 1995 1996% ?- ifmap:collect_supersets([[a,b,c]], [b,a], X). 1997% ?- ifmap:collect_supersets([[a,b,c]-[], [b]-c], [b,a], X). 1998collect_supersets([X|Y], S, [X|Y0]):- is_super(X, S), !, 1999 collect_supersets(Y, S, Y0). 2000collect_supersets([_|Y], S, Y0):- collect_supersets(Y, S, Y0). 2001collect_supersets([], _, []). 2002 2003% ?- ifmap:complete_support([a,b], [c-[]], C). 2004%@ C = [b-[], a-[], c-[]]. 2005complete_support([A|R], S, S0) :- 2006 ( memberchk(A-_, S) 2007 -> S1 = S 2008 ; S1 = [A-[]|S] 2009 ), 2010 complete_support(R, S1, S0). 2011complete_support([], X, X). 2012 2013 /********************** 2014 * view channel * 2015 **********************/ 2016 2017 2018% ?- show_graph(pred([A-B, (A, f, B)]), [a-b,b-d]). 2019% ?- show_graph((=), [(a,f,b),(b, g, c)]). 2020 2021:- meta_predicate show_graph_tmp(, ). 2022show_graph(F, DG):- maplist(F, DG, Arrows), 2023 show_graph_tmp(digraph_viz, Arrows). 2024% 2025show_graph_tmp(Pred, Aut):- 2026 expand_file_name('~/tmp/DOTTEMP.dot', [DOT]), 2027 expand_file_name('~/tmp/DOTTEMP.', [M]), 2028 file(DOT, write, call(Pred, Aut)), 2029 pshell(dot(-'T'(ps2), -o(M+ps), M+dot); 2030 ps2pdf(M+ps, M+pdf); 2031 open(-a('Preview'), M+pdf)). 2032% 2033digraph_viz(Arrows) :- 2034 format("digraph g {~n",[]), 2035 format("rankdir=LR;~n",[]), 2036 coalgebra:move_in_dot(Arrows), 2037 format("}~n",[]). 2038% 2039ifmap_counter_config( 2040 [ dir_name(ifmap), 2041 stem(ifmap), 2042 counter_name(ifmap_counter) 2043 ]). 2044 2045% ?- cd('/Users/cantor/Desktop'). 2046% ?- trace, update_counter_file(testfile, Count, 2), integer(Count). 2047% Assuming the counter file is at current working directory. 2048update_counter_file(FileName, Count):- 2049 update_counter_file(FileName, Count, 99). 2050% 2051update_counter_file(FileName, Count, Max):- 2052 ( exists_file(FileName) -> 2053 open(FileName, read, S), 2054 read(S, U), 2055 close(S), 2056 V is U + 1 2057 ; V = 0 2058 ), 2059 ( V > Max -> Count = 0 2060 ; Count = V 2061 ), 2062 open(FileName, write, W), 2063 write(W, Count), 2064 write(W, ".\n"), 2065 close(W). 2066 2067read_counter_file(Counter, Count):- 2068 open(Counter, read, S), 2069 read(S, Count), 2070 close(S). 2071 2072% ?- completing_counter_config([],X). 2073%@ X = [counter_name(counter), dir_name(anonymous), directory('/Users/cantor/public_html/paccgi7')] . 2074% ?- ifmap_counter_config(C), completing_counter_config(C, C0). 2075% 2076completing_counter_config(X, Y):- 2077 check_directory_prefix(X, X0), 2078 memberchk(directory(D), X0), 2079 working_directory(Old, D), 2080 check_counter_directory_name(X0, X1), 2081 memberchk(dir_name(E), X1), 2082 cd(E), 2083 check_counter_name(X1, Y), 2084 cd(Old). 2085% 2086check_directory_prefix(X, Y):- 2087 ( memberchk(directory(_), X) -> Y = X 2088 ; getenv(home_html_root, D), 2089 Y = [directory(D)|X] 2090 ). 2091% 2092check_counter_directory_name(X, Y):- 2093 ( memberchk(dir_name(N), X) -> Y = X 2094 ; N = anonymous, 2095 Y = [dir_name(N)|X] 2096 ), 2097 pshell(mkdir(-p, N)). 2098% 2099check_counter_name(X, Y):- 2100 ( memberchk(counter_name(_), X) -> Y = X 2101 ; Y = [counter_name(counter)|X] 2102 ). 2103 2104% ?- theory_to_cla( 2105% theory( [tweety, penguin, bird, fly], 2106% [ [penguin] => [bird], 2107% [bird] => [fly] 2108% ] ), CLA). 2109 2110% ?- theory_to_cla_html(theory([a],[[]=>[a]]), pdf, A), pshell(open(A)). 2111% ?- theory_to_cla_html(theory([a,b],[[b]=>[a], [a]=>[b]]), pdf, A), 2112% pshell(open(A)). 2113% ?- theory_to_cla_html(theory([a],[[]=>[a]]), jpg, A), pshell(open(A)). 2114% ?- theory_to_cla_html(theory([a],[[]=>[a]]), svg, A), pshell(open(A)). 2115 2116theory_to_cla_html(X, T, URL):- 2117 theory_to_cla(X, Cla), 2118 cla_html(Cla, T, URL). 2119% 2120cla_html(Cla, T, URL):- 2121 ifmap_counter_config(Conf), 2122 completing_counter_config([out(T)|Conf], Conf0), 2123 obj_get([counter_name(CN), stem(Stem), directory(D), dir_name(M)],Conf0), 2124 working_directory(Old, D), 2125 cd(M), 2126 update_counter_file(CN, Count), 2127 atomic_list_concat([Stem, Count, '.html'], Targethtml), 2128 create_cla_html(Cla, Conf0, Targethtml), 2129 getenv(host_html_root, H), 2130 cd(Old), 2131 atomic_list_concat([H, / , M , / ,Targethtml], URL). 2132 2133% 2134create_cla_html(Cla, Conf, Target):- 2135 cla_to_new_dot(Cla, Conf, Conf0), 2136 divtag(Conf0, Divtag), 2137 HTML = [ "<html><body>\n", 2138 Divtag, 2139 "</body></html>\n" 2140 ], 2141 file(Target, write, smash(HTML)). 2142 2143% 2144cla_to_new_dot(cla(L, M, N)) --> !, 2145 { A = subgraph(cluster_token, L) }, 2146 { B = subgraph(cluster_type, M) }, 2147 graph_to_new_dot(A; B; [L,M,N]). 2148cla_to_new_dot(G) --> graph_to_new_dot(G). 2149 2150% 2151graph_to_new_dot(G, Conf, Conf0):- 2152 obj_get([counter_name(CN), stem(ST)], Conf), 2153 read_counter_file(CN, Count), 2154 atom_concat(ST, Count, Base), 2155 graph_to_dot_write(G, [base(Base)|Conf], Conf0). 2156% 2157graph_to_dot_write(G, Opts, Opts) :- % for DCG use. 2158 once(term_to_graph(G, H, E, N)), 2159 once(graph_to_dot(digraph(g, H, E, N), Digraph)), 2160 obj_get([base(B), out(T)], Opts), 2161 atomic_list_concat([ B, (.), dot], Dot), 2162 atomic_list_concat([ B, (.), T], Tout), 2163 smash(Digraph, DigraphStr), 2164 file(Dot, write, write(DigraphStr)), 2165 sh(dot(-'T'(T), -o(Tout), Dot)). 2166% 2167divtag(Opts, Divtag) :- 2168 obj_get([base(Base), out(T)], Opts), 2169 atomics_to_string([Base, ".", T], Loc), 2170 Divtag = [ 2171 "<p><div ", 2172 "id='diagram' ", 2173% "style='border : solid 2px #ff0000; ", 2174 "style='border : solid 1px red; ", 2175 "width : 1200px; ", % was 600px 2176 "height : 700px; ", % was 300px 2177 "overflow : auto; '><br/>\n", 2178 "<img src=\"", Loc, "\"/>\n", 2179 "</div></p>\n" 2180 ].
2185% ?- show_cla(cla([a,b],[1,2], [1-[a], 2-[b]])). 2186% ?- show_cla(cla([a,b],[1,2], [1-[a,b], 2-[b]])). 2187% ?- show_cla(cla([1],[a], [a-[1]])). 2188% ?- show_cla(cla([1,2],[a], [a-[1,2]])). 2189 2190show_cla(Cla):- cla_to_dot(Cla, DotStr), 2191 T = pdf, 2192 tmp_file_stream(DOT, F0, [encoding(utf8), extension(dot)]), 2193 close(F0), 2194 tmp_file_stream(PDF, F1, [encoding(utf8), extension(pdf)]), 2195 close(F1), 2196 file(DOT, write, write(DotStr)), 2197 pshell(dot(-'T'(T), -o(PDF), DOT); open(PDF)). 2198 2199% old_show_cla(Cla):- cla_to_dot(Cla, DotStr), 2200% T = pdf, 2201% expand_file_name("~/tmp/TEMP.dot", [DOT]), 2202% expand_file_name("~/tmp/TEMP.pdf", [PDF]), 2203% file(DOT, write, write(DotStr)), 2204% pshell(dot(-'T'(T), -o(PDF), DOT); open(PDF)). 2205 2206% 2207cla_to_dot(cla(L, M, N), Dot):- 2208 A = subgraph(cluster_token, L), 2209 B = subgraph(cluster_type, M), 2210 graph_to_dot_string(A; B; [L,M,N], Dot). 2211% 2212graph_to_dot_string(G, Dot):- 2213 once(term_to_graph(G, H, E, N)), 2214 once(graph_to_dot(digraph(g, H, E, N), Digraph)), 2215 smash(Digraph, Dot)