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 comma_list(T, Y). 1013 1014% ?- parse_classifications(";", Y). 1015% ?- parse_classifications("a:b, c, d, k", Y). 1016parse_classifications(X, Y):- parse_comma_list(X, Z), 1017 maplist(sort_cla, Z, Y). 1018% 1019sort_cla(X:cla(Y, Z, U), X:cla(Y0, Z0, U0)) :- 1020 sort(Y, Y0), 1021 sort(Z, Z0), 1022 maplist(pred([P-Q, P-Q0]:- sort(Q, Q0)), U, U1), 1023 sort(U1, U0). 1024% 1025parse_informorphisms(X, Y):- parse_comma_list(X, Y). 1026% 1027parse_constraints(X, Y):- parse_comma_list(X, Y). 1028 1029 /********************************* 1030 * ds_cover_with_constraint * 1031 *********************************/ 1032 1033% 1034codes_string(X, Y):- string_codes(Y, X). 1035% 1036string_term(X, Y):- term_string(Y, X). 1037 1038% ?- maplist(parse_list(string), ["a,b", "x,y,z", "1,2,3"], X). 1039% ?- maplist(parse_list, ["a,b", "\s\t\n", "1,2,3"], X). 1040% ?- maplist(parse_list(codes), [`a,b`, `x,y,z`, `1,2,3`], X). 1041parse_list(X, Y):- parse_list(codes, X, Y). 1042% 1043parse_list(string, X, Y):-!, string_term(X, Z), comma_list(Z, Y). 1044parse_list(codes, X, Y):- string_codes(Z, X), 1045 string_term(Z, U), 1046 comma_list(U, Y). 1047 1048ds_cover_with_constraint([X, Y, Z], A):- 1049 ds_cover_with_constraint(X, Y, Z, A). 1050 1051% 1052ds_cover_with_constraint(Cla_list0, Imorph_list0, Con0, OutString):- 1053 ds_keys(Cla_list0, Keys, Cla_list), 1054 ds_prepare(Imorph_list0, Con0, Imorph_list, Con, Keys), 1055 ds_check(Cla_list, Imorph_list, Con), 1056 ds_cover_with_constraint(Cla_list, Imorph_list, Con, Tokens, Types), 1057 maplist(map_token_vector(Keys), Tokens, Tokens0), 1058 maplist(map_type(Keys), Types, Types0), 1059 term_string(Tokens0, U), 1060 term_string(Types0, V), 1061 atomics_to_string([U,"\n",V], OutString). 1062 1063% ?- ifmap:ds_cover_with_constraint([[cla([],[a,b],[])], [], []], X, Y). 1064% ?- ifmap:ds_cover_with_constraint([[cla([],[a,b],[]),cla([], [x,y],[])], [], []], X, Y). 1065ds_cover_with_constraint([Cla_list0, Imorph_list0, Con0], Types0, Tokens0):- 1066 ds_keys(Cla_list0, Keys, Cla_list), 1067 catch(( 1068 ds_prepare(Imorph_list0, Con0, Imorph_list, Con, Keys), 1069 ds_check(Cla_list, Imorph_list, Con), 1070 ds_cover_with_constraint(Cla_list, Imorph_list, 1071 Con, Tokens, Types), 1072 maplist(map_token_vector(Keys), Tokens, Tokens0), 1073 maplist(map_type(Keys), Types0, Types)), 1074 Error, 1075 ( ds_error_atomics(Keys, Error, M), 1076 atomics_to_string(M, OutString), 1077 writeln(OutString), 1078 fail 1079 )). 1080 1081% ?- indexed_cla_intern([a:cla([],[],[])], X, Y, Z, U). 1082% ?- trace, indexed_cla_intern([a:cla([],[],[]), b:cla([],[],[])], X, Y, Z, U). 1083% ?- indexed_cla_intern([a:cla([],[],[]), a:cla([],[],[])], X, Y, Z, U). % multiple index Error. 1084 1085indexed_cla_intern(Indexed_cla, Index_list, Cla_list, Vec_cla, Zip_index_num):- 1086 zip_colon(Index_list, Cla_list, Indexed_cla), 1087 Vec_cla =..[v|Cla_list], 1088 length(Indexed_cla, N), 1089 numlist(1, N, Ns), 1090 zip(Index_list, Ns, Zip_index_num), 1091 functor(Vec_cla, _, L), 1092 sort(Index_list, S), 1093 length(S, K), 1094 ( K \== N -> throw("multiple index found.") 1095 ; true 1096 ). 1097 1098% ?- ifmap:ds_keys([a,b,c], R, V). 1099% ?- ifmap:ds_keys([a,b:c,c], R, V). 1100ds_keys(X, Y, Z):- ds_keys(X, Y, Z, 1). 1101 1102% 1103ds_keys([A:X|R], [A|U], [X|V], I):- J is I + 1, 1104 ds_keys(R, U, V, J). 1105ds_keys([X|R], [I|U], [X|V], I):- J is I + 1, 1106 ds_keys(R, U, V, J). 1107ds_keys([], [], [], _). 1108 1109% ?- ifmap:key_index_prefix([a,b], X, 1:c). 1110% ?- ifmap:key_index_prefix([a,b], b:c, X). 1111key_index_prefix(Keys, K:X, I:X):- var(K), !, integer(I), nth1(I, Keys, K). 1112key_index_prefix(Keys, K:X, J:X):- key_index(Keys, K, 1, J). 1113key_index_prefix(_, X, X). 1114 1115% ?- key_index([a,b,c], b, I). 1116key_index(Key_list, Key, Index):- key_index(Key_list, Key, 1, Index). 1117% 1118key_index([K|_], K, I, I):-!. 1119key_index([_|R], K, I, J):- I0 is I + 1, key_index(R, K, I0, J). 1120 1121% ?- ifmap:map_type([a,b], [a:x, b:y], R), ifmap:map_type([a,b], S, R). 1122map_type(Keys, Type, Type0):- maplist(key_index_prefix(Keys), Type, Type0). 1123 1124% ?- map_token_vector([1,2], [a, b], X). 1125map_token_vector(Keys, Vec, Vec0):- maplist(pred([K, T, K:T]), Keys, Vec, Vec0). 1126 1127% ?- ds_prepare([], [], X, Y, []). 1128% ?- ds_prepare([im(u->v,[a-b], [])], [[u:a] => [v:b]], X, Y, [u,v]). 1129ds_prepare(Im, Con, Im0, Con0, Keys):- 1130 check_duplicate_free(Keys), 1131 maplist(pred(Keys, ([im(A->B, U, L), im(I->J, U, L)] 1132 :- key_index(Keys, A, I), 1133 key_index(Keys, B, J)) 1134 & ([im(A->B, U), im(I->J, U)] 1135 :- key_index(Keys, A, I), 1136 key_index(Keys, B, J)) 1137 ), 1138 Im, Im0), 1139 maplist(pred(Keys, ([L => R, L0 => R0]:- 1140 maplist(pred(Keys, 1141 [U:X, U0:X]:-key_index(Keys, U, U0)), L, L0), 1142 maplist(pred(Keys, 1143 [U:X, U0:X]:-key_index(Keys, U, U0)), R, R0))), 1144 Con, Con0). 1145 1146% 1147check_duplicate_free(X):- sort(X, X0), 1148 length(X, N), 1149 length(X0, N0), 1150 ( N == N0 -> true 1151 ; throw(multiple_index(A)) 1152 ). 1153 1154 1155 /***************************** 1156 * Check ds & build core * 1157 *****************************/ 1158 1159% ?- check_ds_build_core([], [], Core). 1160% ?- check_ds_build_core([cla([x],[a], [a-[x]])], [im(1->1, [a-a], [x-x])], Core). 1161% ?- check_ds_build_core([], [im(1->1, [a-a], [x-x])], Core). % << throw 1162check_ds_build_core(Cs, Ims, Core):- 1163 ds_check(Cs, Ims), 1164 ds_core(Cs, Ims, Core). 1165 1166% ?- ds_check([], []). 1167% ?- ds_check([cla([x],[a], [a-[x]])], [im(1->1, [a-a], [x-x])]). 1168ds_check(Cla_list, Imorph_list):- 1169 maplist(cla_check, Cla_list), 1170 maplist(im_check(Cla_list), Imorph_list). 1171 1172ds_check(Cla_list, Imorph_list, Con):- 1173 maplist(cla_check, Cla_list), 1174 maplist(im_check(Cla_list), Imorph_list), 1175 maplist(con_check(Cla_list), Con). 1176 1177cla_check(cla(X, A, S)):- forall( member(U-L, S), 1178 ( memberchk(U, A), 1179 subset(L, X) -> true 1180 ; throw('an unspecified token appears a supporter'(U-L)) 1181 )). 1182 1183% 1184im_check(Cla_list, im(I->J, FA, FX)):- 1185 is_map(FA), 1186 is_map(FX), 1187 nth1(I, Cla_list, Ci), 1188 nth1(J, Cla_list, Cj), 1189 Ci=cla(Xi, Ai,_), 1190 Cj=cla(Xj, Aj,_), 1191 is_map(FA, Ai, Aj), 1192 is_map(FX, Xj, Xi), 1193 check_imorph(Ci, Cj, FA, FX), 1194 !. 1195im_check(Cla_list, im(I->J, FA)):- 1196 nth1(I, Cla_list, cla(_, Ti, _)), 1197 nth1(J, Cla_list, cla(_, Tj, _)), 1198 is_map(FA), 1199 is_map(FA, Ti, Tj), 1200 !. 1201im_check(_, IM):- throw(failure(im_check(IM))). 1202 1203% 1204con_check(Cla_list, L=>R):- 1205 length(Cla_list, N), 1206 forall( ( member(A, L) ; member(A, R)), 1207 ( A = J:T, 1208 integer(J), 1209 1=<J, 1210 J=<N, 1211 nth1(J, Cla_list, cla(_, Typs, _)), 1212 memberchk(T, Typs))), 1213 !. 1214con_check(_, Seq):- throw(failure(con_check(Seq))). 1215 1216 1217% Error Messages 1218ds_error_atomics(_, unknown(X), X). 1219ds_error_atomics(_, cla_check(X), 1220 ["Classification check fail: ", X0, "\n[]"]):- term_string(X, X0). 1221ds_error_atomics(Keys, im_check(X), 1222 ["Informorphism check fail: ", X0, "\n[]"]):- 1223 X =.. [IM,I,J|R], 1224 maplist(key_index_prefix(Keys), [I0, J0], [I, J]), 1225 X1 =..[IM,I0, J0|R], 1226 term_string(X1, X0). 1227ds_error_atomics(Keys, con_check(L-R), 1228 ["Constraint check fail: ", X0, "\n[]"]):- 1229 maplist(key_index_prefix(Keys), L0, L), 1230 maplist(key_index_prefix(Keys), R0, R), 1231 term_string(L0-R0, X0). 1232ds_error_atomics(_, cla_not_with_key(X), 1233 ["Missing Key: ", X0, "\n[]"]) :- term_string(X, X0). 1234ds_error_atomics(_, duplicate_key(X), 1235 ["Duplicate Key: ", X0, "\n[]"]):- term_string(X, X0). 1236ds_error_atomics(_, X, ["other error: ", X0, "\n[]"]):- term_string(X, X0). 1237 1238% ?- ifmap:sum_by_constraint([[1:a,2:a]-[]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1239% ?- ifmap:sum_by_constraint([[1:a]-[2:a], [1:a]-[2:a]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1240% ?- 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). 1241% ?- 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). 1242% ?- ifmap:ds_cover_with_constraint([cla([x,y],[a],[a-[x,y]]),cla([x,y],[a],[a-[x 1243 1244% ?- 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). 1245%@ U = [], 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). 1247ds_cover_with_constraint(Cla_list, Imorph_list, Con, Tokens, Types):- 1248 sum_by_constraint(Con, Cla_list, CoreTokens), 1249 maplist(pred([cla(_,A,_), A]), Cla_list, TypS), 1250 type_sum(TypS, 1, [], IndexedTypes), 1251 colimit_cover(Imorph_list, IndexedTypes, Types), 1252 limit_cover_by_invertability(Imorph_list, CoreTokens, Tokens). 1253 1254% ?- ifmap:ds_theory_cover_with_constraint([theory([a],[[a]=>[a]])], [], [], X, Y). 1255% ?- ifmap:ds_theory_cover_with_constraint([theory([a],[[a]=>[a]]), theory([a],[[a]=>[a]])], [], [], X, Y). 1256% ?- ifmap:ds_theory_cover_with_constraint([theory([a],[[a]=>[a]]), theory([a],[[a]=>[a]])]), [im(1,2,[a-a])], [], X, Y). 1257% ?- 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). 1258ds_theory_cover_with_constraint(Theories, Imorph_list, Con, Tokens, Types):- 1259 theory_sum_tokens(Theories, CoreTokens), 1260 filter_with_constraints(CoreTokens, Con, CoreTokens0), 1261 maplist(pred([theory(A,_), A]), Theories, TypS), 1262 type_sum(TypS, 1, [], IndexedTypes), 1263 colimit_cover(Imorph_list, IndexedTypes, Types), 1264 limit_cover_by_invertability(Imorph_list, CoreTokens0, Tokens). 1265 1266% ?- ifmap:check_info_map(cla([x],[a], [a-[x]]), cla([y],[b],[b-[y]]), [a-b],[y-x]). 1267limit_cover_by_invertability([im(I, J, Zip, _)|Ms], X, Y):-!, 1268 limit_cover_by_invertability(X, Zip, I, J, X0), 1269 limit_cover_by_invertability(Ms, X0, Y). 1270limit_cover_by_invertability([im(I, J, Zip)|Ms], X, Y):-!, 1271 limit_cover_by_invertability(X, Zip, I, J, X0), 1272 limit_cover_by_invertability(Ms, X0, Y). 1273limit_cover_by_invertability([], X, X). 1274% 1275limit_cover_by_invertability([V|R], Z, I, J, [V|R0]):- 1276 limit_cover_by_invertability(Z, V, I, J), 1277 !, 1278 limit_cover_by_invertability(R, Z, I, J, R0). 1279limit_cover_by_invertability([_|R], Z, I, J, R0):-!, 1280 limit_cover_by_invertability(R, Z, I, J, R0). 1281limit_cover_by_invertability([], _, _, _, []). 1282 1283% 1284limit_cover_by_invertability(Zip, Vec, I, J):- 1285 nth1(I, Vec, Li-Ri), 1286 nth1(J, Vec, Lj-Rj), 1287 map_from_to(Li, Zip, Lj), 1288 map_from_to(Ri, Zip, Rj). 1289 1290% ?- ifmap:map_from_to([a,b], [a-1,b-2], [1,2]). 1291map_from_to([X|Y], Z, T):- memberchk(X-U, Z), 1292 memberchk(U, T), 1293 map_from_to(Y, Z, T). 1294map_from_to([], _, _). 1295 1296 1297% ?- ifmap:check_info_map(cla([x],[a], [a-[x]]), cla([y],[b],[b-[y]]), [a-b],[y-x]). 1298% ?- ifmap:check_info_map(cla([x],[a,b], [a-[x]]), cla([y],[b],[b-[y]]), [a-b],[y-x]). 1299ds_check_info_map(ds(FCs, IM)):- 1300 maplist(pred(FCs, [M] :- check_info_map(M, FCs)), IM). 1301 1302% 1303check_info_map(im(I, J, U, L), Cs):- !, 1304 memberchk(I-A, Cs), 1305 memberchk(J-B, Cs), 1306 check_info_map(A, B, U, L). 1307% 1308check_info_map(cla(_,A0, R0), cla(X1,_,R1), Upper_map, Lower_map):- 1309 forall((member(P, X1), 1310 member(T, A0), 1311 memberchk(P-Q, Lower_map), 1312 memberchk(T-S, Upper_map)), 1313 iff(support(R0, Q, T), support(R1, P, S))). 1314 1315% ?- set_equal([a,a,b], [b,a,b]). 1316set_equal(X, Y):- subset(X, Y), subset(Y, X). 1317 1318% ?- check_informorphism( cla([x],[a], [a-[x]]), cla([x],[a],[a-[x]]), 1319% [a-a],[x-x]). 1320% ?- check_informorphism( cla([x],[a], [a-[y]]), cla([x],[a],[a-[x]]), 1321% [a-a],[x-x]). % << false 1322 1323check_informorphism(C, D, U, L):- check_imorph(C, D, U, L). 1324 1325% check_informorphism(cla(X0, A0, R0), cla(X1, A1, R1), Upper_map, Lower_map):- 1326% zip(U, U0, Upper_map), 1327% set_equal(U, A0), 1328% subset(U0, A1), 1329% zip(V, V0, Lower_map), 1330% set_equal(V, X1), 1331% subset(V0, X0), 1332% forall( (member(P, X1), member(T, A0)), 1333% forall( (memberchk(P-Q, Lower_map), memberchk(T-S, Upper_map)), 1334% iff(support(R0, Q, T), support(R1, P, S)))). 1335 1336 1337% ?- check_imorph( cla([x],[a], [a-[x]]), cla([x],[a],[a-[x]]), 1338% [a-a],[x-x]). 1339% ?- check_imorph( cla([x],[a], [a-[y]]), cla([x],[a],[a-[x]]), 1340% [a-a],[x-x]). % << false 1341 1342% ?- time(repeat(10000, (check_imorph( cla([x],[a], [a-[x]]), cla([x],[a],[a-[x]]), [a-a],[x-x])))). 1343%@ % 220,001 inferences, 0.012 CPU in 0.012 seconds (98% CPU, 18585875 Lips) 1344%@ true. 1345 1346check_imorph(cla(X0, A0, R0), cla(X1, A1, R1), Upper_map, Lower_map):- 1347 forall( ( member(U-V, Upper_map), 1348 memberchk(U-Su, R0), 1349 memberchk(V-Sv, R1)), 1350 ( fun_inverse_image(Lower_map, Su, G), 1351 set_equal(G, Sv) 1352 )). 1353 1354% 1355check_adjoint_upper(X, Y, Upper, Ms, Mt):- 1356 forall(member(P-Q, Upper), 1357 iff(support(Ms, Y, P), support(Mt, X, Q))). 1358 1359check_adjoint_lower(X, Y, Lower, Ms, Mt):- 1360 forall(member(P-Q, Lower), 1361 iff(support(Ms, Q, X), support(Mt, P, Y))). 1362 1363% ?- 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). 1364% ?- 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). 1365% ?- 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). 1366% ?- 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). 1367% ?- 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). 1368 1369extend_info_map(cla(X,A,S), cla(Y,B,T), im(U,L), im(U0,L0)):- 1370 zip(P, _, U), 1371 zip(Q, _, L), 1372 subtract(A, P, A0), 1373 subtract(Y, Q, Y0), 1374 build_adjoint(cla(X, A0, S), cla(Y0, B, T), U, L, U0, L0). 1375 1376% 1377build_info_map(C,D,im(U, L)):- build_adjoint(C,D,[],[],U,L). 1378 1379% 1380build_adjoint(cla(X, [A|As], R), cla([V|Vs], S, T), U, L, U0, L0):- !, 1381 member(B, S), 1382 check_adjoint_upper(A, B, U, R, T), 1383 member(W, X), 1384 check_adjoint_lower(V, W, L, R, T), 1385 build_adjoint(cla(X, As, R), cla(Vs, S, T), [A-B|U], [V-W|L], U0, L0). 1386build_adjoint(cla(X, [A|As],R), cla([], S, T), U, L, U0, L0):- !, 1387 member(B, S), 1388 check_adjoint_upper(A, B, U, R, T), 1389 build_adjoint(cla(X, As, R), cla([], S, T), [A-B|U], L, U0, L0). 1390build_adjoint(cla(X,[],R), cla([V|Vs], S, T), U, L, U0, L0):- !, 1391 member(W, X), 1392 check_adjoint_lower(V, W, L, R, T), 1393 build_adjoint(cla(X, [], R), cla(Vs, S, T), U, [V-W|L], U0, L0). 1394build_adjoint(cla(_,[],_), cla([], _,_), U, L, U, L). 1395 1396% ?- ifmap:rel_compose([a-1, a-2], [2-x, 2-y], R). 1397rel_compose(F, G, H):- rel_compose(F, G, H, []). 1398 1399rel_compose([], _, H, H). 1400rel_compose([X|R], G, H, K):- rel_compose_one(X, G, H, H0), 1401 rel_compose(R, G, H0, K). 1402 1403% 1404rel_compose_one(_,[], H, H). 1405rel_compose_one(X-Y, [Y-Z|G], [X-Z|H], K):- !, 1406 rel_compose_one(X-Y, G, H, K). 1407rel_compose_one(U, [_|G], H, K):- rel_compose_one(U, G, H, K). 1408 1409% ?- fun_inverse_image([a-1, b-2, c-2], [1], R). 1410% ?- fun_inverse_image([a-1, b-2, c-2], [1,2], R). 1411fun_inverse_image([], _, []). 1412fun_inverse_image([X-Y|R], A, [X|M]):- 1413 memberchk(Y, A), !, 1414 fun_inverse_image(R, A, M). 1415fun_inverse_image([_|R], A, M):- 1416 fun_inverse_image(R, A, M). 1417 1418% ?- ifmap:image_of_map([a-b,b-a,c-a], R). 1419image_of_map(Fn, Image):- zip(_,Vals, Fn), sort(Vals, Image). 1420 1421% ?- ifmap:find_map([a,b], [1,2,3], F). 1422find_map([A|As], R, [A-B|F]):- member(B, R), find_map(As, R, F). 1423find_map([], _, []).
1429% ?- invertable_type_map([],cla([],[],[]), cla([],[],[]), R). 1430% ?- invertable_type_map([],cla([],[a],[]), cla([],[],[]), R). 1431% ?- invertable_type_map([a-s],cla([1],[a],[a-[1]]), cla([2],[s],[s-[2]])). 1432% ?- invertable_type_map([a-s,b-t],cla([1],[a,b],[a-[1],b-[1]]), cla([2,3],[s,t],[s-[2],t-[3]])). 1433% ?- invertable_type_map([a-s,b-t],cla([1],[a,b],[a-[1],b-[2]]), cla([3],[s,t],[s-[3],t-[3]])). 1434% ?- invertable_type_map([a-s],cla([1],[a],[a-[1]]), cla([2],[s],[s-[2]]),R). 1435% ?- invertable_type_map([a-s],cla([1],[a],[a-[1]]), cla([2],[s],[s-[2]]),R). 1436 1437invertable_type_map(Map, SourceCla, TargetCla):- 1438 invertable_type_map(Map, SourceCla, TargetCla, _). 1439 1440% ?- is_map([a-b],[a],[b,c]). 1441% ?- is_map([a-b],[a,d],[b,c]). 1442% ?- is_map([a-b],[a],[]). 1443% ?- is_map([],[],[]). 1444is_map(Map, D, R) :- zip(D0, R0, Map), 1445 subset(D0, D), 1446 subset(D, D0), 1447 subset(R0, R). 1448 1449% 1450is_map(Zip):- sort(Zip, Zip0), 1451 check_unique_key(Zip0). 1452 1453% ?- check_unique_key([a-b,c-d]). 1454% ?- check_unique_key([a-b,a-d]). 1455check_unique_key([A-_, A-_|_]):- !,fail. 1456check_unique_key([_,X|M]):- check_unique_key([X|M]). 1457check_unique_key([_]). 1458check_unique_key([]). 1459 1460% 1461invertable_type_map(Map, theory(X,Y), TargetCla, AtomMap):- !, 1462 theory_to_cla(theory(X, Y), Z), 1463 invertable_type_map(Map, Z, TargetCla, AtomMap). 1464invertable_type_map(Map, SourceCla, theory(X, Y), AtomMap):- !, 1465 theory_to_cla(theory(X, Y), Z), 1466 invertable_type_map(Map, SourceCla, Z, AtomMap). 1467invertable_type_map(=, SourceCla, TargetCla, AtomMap):- !, 1468 typ(SourceCla, T), 1469 zip(T, T, Id_T), 1470 invertable_type_map(Id_T, SourceCla, TargetCla, AtomMap). 1471invertable_type_map(Map, SourceCla, TargetCla, AtomMap):- 1472 typ(SourceCla, U), 1473 typ(TargetCla, V), 1474 is_map(Map, U, V), 1475 image_of_map(Map, IoM), 1476 cla_restrict(IoM, TargetCla, TargetCla0), 1477 cla_boolean_atoms(SourceCla, cla(_,_,A)), 1478 cla_boolean_atoms(TargetCla0, cla(_,_,B)), 1479 zip(AtomsA,_,A), 1480 zip(AtomsB,_,B), 1481 sort_atoms(AtomsA, AtomsA0), 1482 sort_atoms(AtomsB, AtomsB0), 1483 exists_atom_map(Map, AtomsA0, AtomsB0, AtomMap). 1484 1485% ?- 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). 1486% ?- 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). 1487%@ R = [a-[a, b], b-[]]. 1488 1489invertable_token_map(Map, cla(Xa, Aa, Sa), cla(Xb, _Ab, Sb), TypeMap):- 1490 is_map(Map, Xb, Xa), 1491 maplist(invert_token_map_one(Map, Sa, Sb), Aa, TypeMap). 1492 1493invert_token_map_one(TokMap, Sa, Sb, A, A-B):- 1494 memberchk(A-U, Sa), 1495 collect_types_by_adjoint(Sb, TokMap, U, B, []). 1496 1497invertable_token_map(M, C1, C2) :- invertable_token_map(M, C1, C2, _). 1498 1499% ?- collect_types_by_adjoint([a-[1,2]],[1-3,2-4], [3,4], R, []). 1500collect_types_by_adjoint([], _, _, B, B). 1501collect_types_by_adjoint([A-V|S], TokMap, U, [A|R], R0):- 1502 member(K, V), 1503 memberchk(K-U0, TokMap), 1504 memberchk(U0, U), 1505 !, % checking adjointness. 1506 forall(member(P, V), (memberchk(P-Q, TokMap), memberchk(Q, U))), 1507 collect_types_by_adjoint(S, TokMap, U, R, R0). 1508collect_types_by_adjoint([_|S], TokMap, U, R, R0):- 1509 collect_types_by_adjoint(S, TokMap, U, R, R0).
1514% ?- sort_atoms([p([b,a],[2,1])], R). 1515sort_atoms(X, Y) :- maplist(pred(([p(U,V), p(U0,V0)] 1516 :- sort(U, U0), 1517 sort(V, V0))), 1518 X, Y).
1526% ?- exists_atom_map([a-b], [p([a],[])], [p([b],[])], R). 1527% ?- exists_atom_map([a-x,b-x], [p([a,b],[])], [p([x],[])], R). 1528exists_atom_map(Map, SourceAtoms, TargetAtoms, AtomMap):- 1529 fun_to_powfun_flip(Map, SetDict), 1530 invertable_atom_set(TargetAtoms, SetDict, SourceAtoms, AtomMap). 1531 1532% ?- invertable_atom_set([p([a],[])], [a-[b]], [p([b],[])], R). 1533invertable_atom_set([Q|As], Dict, Bs, [Q-P|AtomMap]):- 1534 Q = p(U, _), 1535 union_set_dict(U, Dict, U0), 1536 P = p(U0, _), 1537 memberchk(P, Bs), 1538 invertable_atom_set(As, Dict, Bs, AtomMap). 1539invertable_atom_set([], _, _, []). 1540 1541% ?- ifmap:union_set_dict([a,b], [a-[y, u],b-[z, v]], R). 1542union_set_dict(A, Dict, Set) :- proj_dict(A, Dict, S), 1543 append(S, S0), 1544 sort(S0, Set). 1545 1546% ?- proj_dict([a,b], [a-b,c-d], R). 1547% ?- proj_dict([a,b, x], [a-b,c-d], R). 1548% ?- proj_dict([c], [a-b,c-d], R). 1549proj_dict([A|R], Dict, [U|P]):- memberchk(A-U, Dict), 1550 !, 1551 proj_dict(R, Dict, P). 1552proj_dict([_|R], Dict, P) :- proj_dict(R, Dict, P). 1553proj_dict([], _, []). 1554 1555% ?- subst_multiple([a-[1,2], b-[3,4]], f(g(a,b),a), R). 1556%@ 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)]. 1557% ?- subst_multiple([a-[1,2], b-[3,4]], [a,b]->[b], R). 1558% ?- subst_multiple_massoc([[a1,a2]-[1,2], [b1,b2]-[3,4]], f(g(a1,b2),a2), R). 1559% ?- subst_multiple_massoc([[a1,a2]-[1,2], [b1,b2]-[3,4]], f(g(a1,b2),a2), R), 1560% subst_multiple([a-[1,2], b-[3,4]], f(g(a,b),a), R0), R=R0. 1561 1562subst_multiple(M, X, Y):- memberchk(X-Y, M), !. 1563subst_multiple(M, X, Y):- X=..[F|Xs], 1564 maplist(subst_multiple(M), Xs, Zs), 1565 choices(Zs, Us), 1566 maplist(pred(F, [A, B]:- B=..[F|A]), Us, Y). 1567 1568subst_multiple_massoc(M, X, Y):- member(K-Y, M), memberchk(X, K), !. 1569subst_multiple_massoc(M, X, Y):- X=..[F|Xs], 1570 maplist(subst_multiple_massoc(M), Xs, Zs), 1571 choices(Zs, Us), 1572 maplist(pred(F, [A, B]:- B=..[F|A]), Us, Y). 1573 1574% ?- subst_theory_multiple([[a]-[b,c]], [[a]=>[a]], R). 1575subst_theory_multiple(M, X, Y):- 1576 maplist(subst_sequent_multiple(M), X, X0), 1577 append(X0, Y). 1578 1579subst_sequent_multiple(M, =>(L, R), S):- 1580 maplist(pred(M, [X, U]:- (member(V-U, M), memberchk(X, V))), L, L0), 1581 maplist(pred(M, [X, U]:- (member(V-U, M), memberchk(X, V))), R, R0), 1582 choices(L0, C), 1583 choices(R0, D), 1584 choices([C,D], E), 1585 maplist(pred([[X, Y], =>(X, Y)]), E, S). 1586 1587% Moving theory forward / backward along a function. 1588% 1589% ?- move_theory_backward([x-a, y-a], [[a]=>[a], [a]=>[a]], R). 1590move_theory_forward(M, Theory, Theory0):- 1591 maplist(pred(M, ( [=>(L, R), =>(L0, R0)] 1592 :- 1593 maplist( pred(M, ([A, B]:- memberchk(A-B, M)) 1594 & 1595 [A, A]), 1596 L, L0), 1597 maplist( pred(M, ([A, B]:- memberchk(A-B, M)) 1598 & 1599 [A, A]), 1600 R, R0))), 1601 Theory, Theory1), 1602 simplify_theory(Theory1, Theory0). 1603 1604% 1605move_theory_backward(M, X, Y):- 1606 fun_to_powfun_flip(M, M0), 1607 maplist(move_sequent_backward(M0), X, X0), 1608 append(X0, Y0), 1609 simplify_theory(Y0, Y). 1610% 1611move_sequent_backward(M, =>(L, R), S):- 1612 maplist(pred(M, [X, U]:- memberchk(X-U, M)), L, L0), 1613 maplist(pred(M, [X, U]:- memberchk(X-U, M)), R, R0), 1614 choices(L0, C), 1615 choices(R0, D), 1616 choices([C,D], E), 1617 maplist(pred([[X, Y], =>(X, Y)]), E, S). 1618 1619% % Clustering; divide a graph into blocks. 1620union_find(X, Y):- union_find(X, [], Y). 1621 1622% ?- union_find([(a,b),(x,y), (x,x), (y, z), (b,c)], R). 1623% ?- union_find([(a-b),(x-y), (x-x), (y-z), (b-c)], R). 1624% ?- union_find([(a=b),(x=y), (x=x), (y=z), (b=c)], R). 1625 1626union_find([], X, X). 1627union_find([P|R], C, D):- (P = (X, Y); P = (X-Y); P = ( X = Y )), !, 1628 union_find(X, Y, C, C1), 1629 union_find(R, C1, D). 1630% 1631union_find(X, Y, Z, U):-select_cluster(X, Z, C, Z0), 1632 ( memberchk(Y, C) -> U=[C|Z0] 1633 ; select_cluster(Y, Z0, C0, Z1), 1634 append(C,C0, C1), 1635 U=[C1|Z1] 1636 ). 1637 1638% ?- select_cluster(a, [[a,b],[c,d]], C, X). 1639select_cluster(X, [], [X], []):-!. 1640select_cluster(X, [Y|Z], Y, Z):- memberchk(X, Y), !. 1641select_cluster(X, [Y|Z], U, [Y|V]):- select_cluster(X, Z, U, V). 1642 1643 1644% ?- theory_to_cla(theory([a,b], [[a,b]=>[]]), M). 1645% ?- theory_to_cla(theory([a,b], [[a,b]=>[],[a]=>[b]]), M). 1646% ?- theory_to_cla(theory([bird, penguine, fly], [[bird]=>[fly], [penguine]=>[bird], []=>[penguin], [fly, penguine]=>[]]), C). 1647% ?- 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). 1648% ?- theory_to_cla(theory([a], [[a]=>[], []=>[a]]), C). 1649% ?- theory_to_cla(theory([a,b,c], [[]=>[a], []=>[b], []=>[c]]), C). 1650% ?- theory_to_cla(theory([bird, fly, penguine], [[penguine]=>[bird], [fly, penguine]=>[]]), C2). 1651% ?- theory_to_cla(theory([bird, fly, penguine], [[penguine]=>[bird], [fly, penguine]=>[], [bird]=>[fly]]), C2). 1652 1653% ?- theory_to_cla( 1654% theory([bird, fly, penguine], 1655% [[penguine]=>[bird], [fly, penguine]=>[]]), 1656% C2), 1657% C1 = cla([a, b], [bird, fly], [bird-[a], fly-[a,b]]), 1658% build_info_map(C1, C2, im(U, L)), 1659% ds_cover([C1, C2], [im(1, 2, U, L)], P). 1660 1661% ?- theory_to_cla( 1662% theory([bird, fly, penguine], 1663% [[penguine]=>[bird], [fly, penguine]=>[]]), 1664% C2), 1665% C1 = cla([a, b], [bird, fly], [bird-[a], fly-[a,b]]), 1666% build_info_map(C1, C2, im(U, L)), 1667% keyed_ds_cover([cla1:C1, cla2:C2], [im(cla1, cla2, U, L)], P). 1668 1669theory_to_cla(theory(S, SeqL), cla(T, S, Supp)):- set(pow(S), P), !, 1670 collect_token(P, SeqL, M), 1671 fresh_token(M, T, Supp). 1672 1673% ?- theory_sum_tokens([theory([a], [[a]=>[], []=>[a]])], C). 1674% ?- theory_sum_tokens([theory([a], [[a]=>[a]]), 1675% theory([a], [[a]=>[a]])], C). 1676% ?- theory_sum_tokens([theory([a], [[a]=>[a]]), 1677% theory([a], [[a]=>[a]]), theory([a], [[a]=>[a]])], C). 1678 1679theory_sum_tokens(Theories, Tokens):- 1680 maplist(theory_to_seqs, Theories, ListofTokenSets), 1681 choices(ListofTokenSets, Tokens). 1682 1683% ?- ifmap:theory_to_seqs(theory([bird, fly, penguine], [[penguine]=>[bird], [fly, penguine]=>[], [bird]=>[fly]]), C2). 1684theory_to_seqs(theory(S, Con), Seqs):- 1685 set(pow(S), P), !, 1686 collect_token(P, Con, Atoms), 1687 maplist(atom_to_seq(S), Atoms, Seqs). 1688 1689% 1690atom_to_seq(S, Atom0, Atom-Comp):- sort(Atom0, Atom), 1691 subtract(S, Atom, Comp0), 1692 sort(Comp0, Comp). 1693 1694% 1695collect_token([], _, []). 1696collect_token([P|R], L, [P|S]):- satisfy_all(P, L), !, 1697 collect_token(R, L, S). 1698collect_token([_|R], L, S):- collect_token(R, L, S). 1699 1700% ?- satisfy([a,b], [a]=>[b]). 1701satisfy(X, =>(Y, Z)):- subset(Y, X), !, 1702 member(A, Z), 1703 member(A, X). 1704satisfy(_, _). 1705% 1706satisfy_all(X, L):- maplist(satisfy(X), L). 1707 1708% 1709fresh_token(P, X, S):- length(P, N), 1710 ( N == 0 1711 -> X=[], S=[] 1712 ; numlist(1, N, X), 1713 zip(X, P, Z), 1714 flip_powfun(Z, S) 1715 ). 1716 1717% ?- simplify_theory([[a,b]=>[c,d], [a]=>[d], [b]=>[c]], R). 1718simplify_theory(Sequents, Sequents0):- 1719 maplist(pred([=>(L,R), =>(L0, R0)] 1720 :- (sort(L, L0), sort(R, R0))), 1721 Sequents, Sequents1), 1722 sort(Sequents1, Sequents2), 1723 simplify_theory(Sequents2, [], Sequents3), 1724 reverse(Sequents3, Sequents0). 1725 1726% 1727simplify_theory([], X, X). 1728simplify_theory([Q|S], X, Y):- weakened_identity(Q), !, 1729 simplify_theory(S, X, Y). 1730simplify_theory([Q|S], X, Y):- member(P, X), sequent_stronger(P, Q), !, 1731 simplify_theory(S, X, Y). 1732simplify_theory([Q|S], X, Y):- sequent_remove_weaker(Q, X, X0), 1733 simplify_theory(S, [Q|X0], Y). 1734 1735% 1736sequent_remove_weaker(_, [], []). 1737sequent_remove_weaker(Q, [P|X], Y) :- sequent_stronger(Q, P), !, 1738 sequent_remove_weaker(Q, X, Y). 1739sequent_remove_weaker(Q, [P|X], [P|Y]) :- sequent_remove_weaker(Q, X, Y). 1740 1741% 1742sequent_stronger(=>(L, R), =>(L0, R0)):- subset(L, L0), subset(R, R0). 1743 1744% 1745weakened_identity(=>(L, R)):- member(A, L), member(A, R). 1746 1747% ?- ifmap:cla_boolean_atoms([a],[x], [x-[]], A,B,C). 1748% ?- cla_boolean_atoms([a,b],[x], [x-[a]], A,B,C). 1749% ?- cla_boolean_atoms([a,b], [x,y], [x-[a],y-[b]], A,B,C). 1750% ?- cla_boolean_atoms([a,b], [x,y], [], A,B,C). 1751% ?- ifmap:cla_boolean_atoms([a,b], [x,y], [x-[a],y-[b]], A,B,C). 1752 1753cla_boolean_atoms(cla(Tok, Typ, Sup), cla(Tok0, Typ0, Sup0)):- 1754 cla_boolean_atoms(Tok, Typ, Sup, Tok0, Typ0, Sup0). 1755 1756% 1757cla_boolean_atoms(Tok, Typ, Sup, Tok0, Typ0, Sup0):- 1758 cla_boolean_atoms(Typ, Sup, [p([],[])-Tok], Sup0), 1759 maplist(pred([A, B, A-B]), Typ1, Tok1, Sup0), 1760 sort(Typ1, Typ0), 1761 sort(Tok1, Tok0). 1762 1763% 1764cla_complete_boolean_atoms(cla(Tok, Typ, Sup), 1765 cla(Tok, Typ0, Sup0)):- 1766 complete_support(Typ, Sup, Sup1), 1767 refine_boolean_atoms(Tok, Sup1, Typ0, Sup0). 1768 1769% 1770cla_boolean_atoms([A|As], Sup, R0, R):- 1771 ( memberchk(A-X, Sup); X = []), 1772 !, 1773 cla_boolean_atoms_(R0, A, X, [], R1), 1774 cla_boolean_atoms(As, Sup, R1, R). 1775cla_boolean_atoms([], _, R, R). 1776 1777% 1778cla_boolean_atoms_([p(L,R)-X|P], A, Y, U0, U1):- 1779 intersection(X, Y, X0), 1780 subtract(X, Y, X1), 1781 add_non_empty([p([A|L], R)-X0, p(L,[A|R])-X1], U0, U2), 1782 cla_boolean_atoms_(P, A, Y, U2, U1). 1783cla_boolean_atoms_([], _, _, R, R). 1784 1785% ?- ifmap:add_non_empty([a-[], b-[c]], R, R0). 1786add_non_empty([_-[]|A], R, R0) :- !, add_non_empty(A, R, R0). 1787add_non_empty([X|A], R, R0):- !, add_non_empty(A, [X|R], R0). 1788add_non_empty([], R, R). 1789 1790% ?- ifmap:cla_restrict([b], cla(_,_,[a-[1],b-[2]]), R). 1791%@ R = cla([2], [b], [b-[2]]). 1792% ?- ifmap:(numcla(1,3, A), numcla(1, 3, B), cla(A+B, C), cla_restrict([1:1, 2:1], C, D)). 1793cla_restrict(S0, cla(_, _, P), cla(X0, S0, P0)):- 1794 collect(pred(S0, [A-_]:- memberchk(A, S0)), P, P0), 1795 zip(_, Xs, P0), 1796 union(Xs, X0). 1797 1798% ?- ifmap:rename_literals([a,a,~(a)], [a-b], R). 1799% ?- ifmap:rename_literals([a,a,~(a), b, ~(c)], [a-b], R). 1800 1801is_super(X-_, S):- !, subset(S, X). 1802is_super(X, S):- subset(S, X). 1803 1804% ?- ifmap:inverse_type_map([a-1, b-2], cla(_, _, [[a]-a,[b]-b]), cla(_,_, [[1]-1, [2]-2]), G). 1805% ?- ifmap:inverse_type_map([a-1, b-2], [[a],[b]], [[1], [2]], G). 1806inverse_type_map(F, cla(_, _, Sup), Trgt, G):- !, 1807 zip(Src,_,Sup), 1808 inverse_type_map(F, Src, Trgt, G). 1809inverse_type_map(F, Src, cla(_, _, Sup), G):- !, 1810 zip(Trgt, _,Sup), 1811 inverse_type_map(F, Src, Trgt, G). 1812inverse_type_map(F, Src, Trgt, G):- 1813 maplist(pred(F, [X, X-Y]:- 1814 rename_literals_with_complementary_rule(X, F, Y)), 1815 Src, Zip), 1816 maplist(pred(Trgt, ( [A-B, A-C]:- 1817 collect_supersets(Trgt, B, C))), 1818 Zip, Zip0), 1819 flip_powfun(Zip0, G). 1820 1821 1822% ?- ifmap:type_support_by_tok_vec(1:a, [[a]-[]]). 1823% ?- ifmap:type_support_by_tok_vec(1:b, [[a]-[]]). 1824% ?- ifmap:type_support_by_tok_vec(2:b, [[a]-[], [b]-[]]). 1825% ?- ifmap:type_support_by_tok_vec(2:b, [[a]-[], [a, c]-[]]). 1826 1827type_support_by_tok_vec(N:A, Svec):- type_support_by_tok_vec(N, A, Svec). 1828 1829type_support_by_tok_vec(1, A, [L-_|_]):- !, memberchk(A, L). 1830type_support_by_tok_vec(2, A, [_,L-_|_]):- !, memberchk(A, L). 1831type_support_by_tok_vec(3, A, [_,_,L-_|_]):- !, memberchk(A, L). 1832type_support_by_tok_vec(N, A, Svec):- nth1(N, Svec, L-_), 1833 memberchk(A, L). 1834 1835% 1836types_support_by_tok_vec([A|As], V):- 1837 type_support_by_tok_vec(A, V), 1838 types_support_by_tok_vec(As, V). 1839types_support_by_tok_vec([], _). 1840 1841% ?- ifmap:tok_vec_respect_seq([[a]-[b]], [1:a]-[1:b]). 1842% ?- ifmap:tok_vec_respect_seq([[a, b]-[1:c]], [1:a]-[1:b]). 1843% ?- ifmap:tok_vec_respect_seq([[a]-[b]], [1:b]-[1:b]). 1844% ?- ifmap:tok_vec_respect_seq([[a]-[b]], []-[1:a]). 1845% ?- ifmap:tok_vec_respect_seq([[a]-[b]], []-[1:c]). 1846 1847tok_vec_respect_seq(Svec, L-R):- types_support_by_tok_vec(L, Svec), !, 1848 member(A, R), 1849 type_support_by_tok_vec(A, Svec), 1850 !. 1851tok_vec_respect_seq(_, _). 1852 1853% 1854full_respect_by_tok_vec([A|Con], Svec):- !, 1855 tok_vec_respect_seq(Svec, A), 1856 full_respect_by_tok_vec(Con, Svec). 1857full_respect_by_tok_vec([], _). 1858 1859% ?- ifmap:filter_with_constraints([], [], R). 1860% ?- ifmap:filter_with_constraints([[[a]-[]]], [[1:a]-[1:a]], R). 1861% ?- ifmap:filter_with_constraints([[[a]-[]]], [[1:a]-[1:b]], R). 1862 1863filter_with_constraints([Vec|Vecs], Con, [Vec|Vecs0]):- 1864 full_respect_by_tok_vec(Con, Vec), 1865 filter_with_constraints(Vecs, Con, Vecs0). 1866filter_with_constraints([_|Vecs], Con, Vecs0):- 1867 filter_with_constraints(Vecs, Con, Vecs0). 1868filter_with_constraints([], _, []). 1869 1870% ?-ifmap:subst_key([a-1],[a:t]-[], R). 1871subst_key(Zip, L-R, L0-R0):- 1872 maplist(pred(Zip, [A:U, B:U] :- memberchk(A-B, Zip)), L, L0), 1873 maplist(pred(Zip, [A:U, B:U] :- memberchk(A-B, Zip)), R, R0). 1874 1875% ?- ifmap:channel_by_constraint([[k:a]-[k:a]],[k-cla([x],[a],[a-[x]])], Core, KeyZip). 1876% ?- 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). 1877% ?- ifmap:channel_by_constraint([[k:a,m:a]-[]],[k-cla([x],[a],[a-[x]]), m-cla([x],[a],[a-[x]])], Core, KeyZip). 1878%@ Core = [[]], 1879%@ KeyZip = [k-1, m-2] . 1880 1881channel_by_constraint(Con, KeyedCs, Core, KeyZip):- 1882 zip(Keys, _Cs, KeyedCs), 1883 length(Keys, N), 1884 numlist(1, N, Ns), 1885 zip(Keys, Ns, KeyZip), 1886 maplist(subst_key(KeyZip), Con, Con0), 1887 sum_by_constraint(Con0, _ListOfSeqSet, Core). 1888 1889% ?- ifmap:sum_by_constraint([[1:a,2:a]-[]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1890% ?- ifmap:sum_by_constraint([[1:a]-[2:a], [1:a]-[2:a]],[cla([x],[a],[a-[x]]), cla([x],[a],[a-[x]])], Core). 1891 1892sum_by_constraint(Con, Cs, Core):- 1893 maplist(convert_seq_set, Cs, ListOfSeqSet), 1894 misc:choices(ListOfSeqSet, SeqVecSet), 1895 filter_with_constraints(SeqVecSet, Con, Core). 1896 1897% ?- ifmap:convert_seq_set(cla([x],[a],[a-[x]]), R). 1898% ?- ifmap:convert_seq_set(cla([x],[a],[a-[x],b-[x]]), R). 1899 1900convert_seq_set(Cla, SeqSet):- 1901 ifmap:cla_complete_boolean_atoms(Cla, cla(_, Pairs, _)), 1902 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.
1923% ?- ifmap:refine_boolean_atoms([a,b], [], A,B). 1924% ?- ifmap:refine_boolean_atoms([], [x], A,B). 1925% ?- ifmap:refine_boolean_atoms([a,b], [x-[a],y-[b]], A,B). 1926% ?- ifmap:refine_boolean_atoms([a], [x-[a]], A,B). 1927% ?- ifmap:refine_boolean_atoms([a,b], [x-[a],y-[b]], A,B). 1928 1929refine_boolean_atoms([], _, [], []):- !. 1930refine_boolean_atoms(Tok, Sup, Typ0, Sup0):- 1931 refine_boolean_atoms(Sup, [p([],[])-Tok], Sup0), 1932 zip(Typ0, _, Sup0). 1933 1934% 1935refine_boolean_atoms([A-X|As], R0, R):- 1936 refine_boolean_atoms_update(R0, A, X, R1), 1937 refine_boolean_atoms(As, R1, R). 1938refine_boolean_atoms([], R, R). 1939 1940% 1941refine_boolean_atoms_update([p(U,V)-X|R], A, Y, S):- 1942 intersection(X, Y, X1), 1943 subtract(X, Y, X2), 1944 ( X1 ==[] 1945 -> S = S1 1946 ; S = [p([A|U], V)-X1|S1] 1947 ), 1948 ( X2 == [] 1949 -> S1 = S2 1950 ; S1 = [p(U,[A|V])-X2| S2] 1951 ), 1952 refine_boolean_atoms_update(R, A, Y, S2). 1953refine_boolean_atoms_update([], _, _, []). 1954 1955% ?- ifmap: (numcla(1,3, A), numcla(1, 3, B), cla(A+B, C), cla_restrict(C, [1:1, 2:1], D)). 1956 1957%% eval_boolean_type(+C:cla, +E:boolen_exp, -V:list) det 1958% is True if 1959% V is unified with the list of tokens of C which satisfies E. 1960 1961% ?- ifmap:eval_boolean_type(a, cla(_,_, [a-[1]]), R). 1962% ?- ifmap:eval_boolean_type(a+a & a, cla(_,_, [a-[1]]), R). 1963 1964% An example use of flip options. 1965eval_boolean_type(A&B,A1,A2):-!, 1966 eval_boolean_type(A,A1,A3), 1967 eval_boolean_type(B,A1,A4), 1968 misc:set(A3&A4,A2). 1969eval_boolean_type(A+B,A1,A2):-!, 1970 eval_boolean_type(A,A1,A3), 1971 eval_boolean_type(B,A1,A4), 1972 misc:set(A3+A4,A2). 1973eval_boolean_type(A,cla(A1,A2,Sup),X):-!, 1974 memberchk(A-X,Sup). 1975 1976% 1977rename_literals_with_complementary_rule(X, F, Y):- 1978 rename_literals(X, F, Y0), 1979 complementary_rule(Y0, Y1), 1980 sort(Y1, Y). 1981 1982% ?- ifmap: rename_literals([a,a,~(a)], [a-b], R). 1983% ?- ifmap: rename_literals([a,a,~(a), b, ~(c)], [a-b], R). 1984rename_literals([X|R], F, [Y|R0]):- 1985 ( X = ~(X0), Y = ~(V) ; X0 = X, Y = V ), 1986 ( memberchk(X0-V, F) ; V = X0 ), 1987 rename_literals(R, F, R0). 1988rename_literals([], _, []). 1989 1990% 1991complementary_rule(Y, []):- member(~(X), Y), member(X, Y), !. 1992complementary_rule(Y, Y). 1993 1994% ?- ifmap:collect_supersets([[a,b,c]], [b,a], X). 1995% ?- ifmap:collect_supersets([[a,b,c]-[], [b]-c], [b,a], X). 1996collect_supersets([X|Y], S, [X|Y0]):- is_super(X, S), !, 1997 collect_supersets(Y, S, Y0). 1998collect_supersets([_|Y], S, Y0):- collect_supersets(Y, S, Y0). 1999collect_supersets([], _, []). 2000 2001% ?- ifmap:complete_support([a,b], [c-[]], C). 2002%@ C = [b-[], a-[], c-[]]. 2003complete_support([A|R], S, S0) :- 2004 ( memberchk(A-_, S) 2005 -> S1 = S 2006 ; S1 = [A-[]|S] 2007 ), 2008 complete_support(R, S1, S0). 2009complete_support([], X, X). 2010 2011 /********************** 2012 * view channel * 2013 **********************/ 2014 2015 2016% ?- show_graph(pred([A-B, (A, f, B)]), [a-b,b-d]). 2017% ?- show_graph((=), [(a,f,b),(b, g, c)]). 2018 2019:- meta_predicate show_graph_tmp( , ). 2020show_graph(F, DG):- maplist(F, DG, Arrows), 2021 show_graph_tmp(digraph_viz, Arrows). 2022% 2023show_graph_tmp(Pred, Aut):- 2024 expand_file_name('~/tmp/DOTTEMP.dot', [DOT]), 2025 expand_file_name('~/tmp/DOTTEMP.', [M]), 2026 file(DOT, write, call(Pred, Aut)), 2027 pshell(dot(-'T'(ps2), -o(M+ps), M+dot); 2028 ps2pdf(M+ps, M+pdf); 2029 open(-a('Preview'), M+pdf)). 2030% 2031digraph_viz(Arrows) :- 2032 format("digraph g {~n",[]), 2033 format("rankdir=LR;~n",[]), 2034 coalgebra:move_in_dot(Arrows), 2035 format("}~n",[]). 2036% 2037ifmap_counter_config( 2038 [ dir_name(ifmap), 2039 stem(ifmap), 2040 counter_name(ifmap_counter) 2041 ]). 2042 2043% ?- cd('/Users/cantor/Desktop'). 2044% ?- trace, update_counter_file(testfile, Count, 2), integer(Count). 2045% Assuming the counter file is at current working directory. 2046update_counter_file(FileName, Count):- 2047 update_counter_file(FileName, Count, 99). 2048% 2049update_counter_file(FileName, Count, Max):- 2050 ( exists_file(FileName) -> 2051 open(FileName, read, S), 2052 read(S, U), 2053 close(S), 2054 V is U + 1 2055 ; V = 0 2056 ), 2057 ( V > Max -> Count = 0 2058 ; Count = V 2059 ), 2060 open(FileName, write, W), 2061 write(W, Count), 2062 write(W, ".\n"), 2063 close(W). 2064 2065read_counter_file(Counter, Count):- 2066 open(Counter, read, S), 2067 read(S, Count), 2068 close(S). 2069 2070% ?- completing_counter_config([],X). 2071%@ X = [counter_name(counter), dir_name(anonymous), directory('/Users/cantor/public_html/paccgi7')] . 2072% ?- ifmap_counter_config(C), completing_counter_config(C, C0). 2073% 2074completing_counter_config(X, Y):- 2075 check_directory_prefix(X, X0), 2076 memberchk(directory(D), X0), 2077 working_directory(Old, D), 2078 check_counter_directory_name(X0, X1), 2079 memberchk(dir_name(E), X1), 2080 cd(E), 2081 check_counter_name(X1, Y), 2082 cd(Old). 2083% 2084check_directory_prefix(X, Y):- 2085 ( memberchk(directory(_), X) -> Y = X 2086 ; getenv(home_html_root, D), 2087 Y = [directory(D)|X] 2088 ). 2089% 2090check_counter_directory_name(X, Y):- 2091 ( memberchk(dir_name(N), X) -> Y = X 2092 ; N = anonymous, 2093 Y = [dir_name(N)|X] 2094 ), 2095 pshell(mkdir(-p, N)). 2096% 2097check_counter_name(X, Y):- 2098 ( memberchk(counter_name(_), X) -> Y = X 2099 ; Y = [counter_name(counter)|X] 2100 ). 2101 2102% ?- theory_to_cla( 2103% theory( [tweety, penguin, bird, fly], 2104% [ [penguin] => [bird], 2105% [bird] => [fly] 2106% ] ), CLA). 2107 2108% ?- theory_to_cla_html(theory([a],[[]=>[a]]), pdf, A), pshell(open(A)). 2109% ?- theory_to_cla_html(theory([a,b],[[b]=>[a], [a]=>[b]]), pdf, A), 2110% pshell(open(A)). 2111% ?- theory_to_cla_html(theory([a],[[]=>[a]]), jpg, A), pshell(open(A)). 2112% ?- theory_to_cla_html(theory([a],[[]=>[a]]), svg, A), pshell(open(A)). 2113 2114theory_to_cla_html(X, T, URL):- 2115 theory_to_cla(X, Cla), 2116 cla_svg(Cla, T, URL). 2117 2118% theory_to_cla_html_orig(X, T, URL):- 2119% theory_to_cla(X, Cla), 2120% cla_html(Cla, T, URL). 2121 2122% 2123% cla_html(Cla, T, URL):- 2124% ifmap_counter_config(Conf), 2125% completing_counter_config([out(T)|Conf], Conf0), 2126% obj_get([counter_name(CN), stem(Stem), directory(D), dir_name(M)],Conf0), 2127% working_directory(Old, D), 2128% cd(M), 2129% update_counter_file(CN, Count), 2130% atomic_list_concat([Stem, Count, '.html'], Targethtml), 2131% create_cla_html(Cla, Conf0, Targethtml), 2132% getenv(host_html_root, H), 2133% cd(Old), 2134% atomic_list_concat([H, / , M , / ,Targethtml], URL). 2135 2136cla_svg(Cla, T, SVGPath):- 2137 ifmap_counter_config(Conf), 2138 completing_counter_config([out(T)|Conf], Conf0), 2139 obj_get([counter_name(CN), stem(Stem), directory(D), dir_name(M)],Conf0), 2140 working_directory(Old, D), 2141 cd(M), 2142 update_counter_file(CN, Count), 2143 atomics_to_string([Stem, Count, '.svg'], SVG), 2144 create_cla_svg(Cla, Conf0, SVG), 2145 cd(Old), 2146 atomics_to_string([M, /, SVG], SVGPath). 2147 2148create_cla_svg(Cla, Conf, Loc):- 2149 cla_to_new_dot(Cla, Conf, Conf0), 2150 obj_get([base(Base), out(T)], Conf0), 2151 atomics_to_string([Base, ".", T], Loc). 2152 2153% 2154% create_cla_html(Cla, Conf, Target):- 2155% cla_to_new_dot(Cla, Conf, Conf0), 2156% divtag(Conf0, Divtag), 2157% HTML = [ "<html><body>\n", 2158% Divtag, 2159% "</body></html>\n" 2160% ], 2161% file(Target, write, smash(HTML)). 2162 2163% 2164cla_to_new_dot(cla(L, M, N)) --> !, 2165 { A = subgraph(cluster_token, L) }, 2166 { B = subgraph(cluster_type, M) }, 2167 graph_to_new_dot(A; B; [L,M,N]). 2168cla_to_new_dot(G) --> graph_to_new_dot(G). 2169 2170% 2171graph_to_new_dot(G, Conf, Conf0):- 2172 obj_get([counter_name(CN), stem(ST)], Conf), 2173 read_counter_file(CN, Count), 2174 atom_concat(ST, Count, Base), 2175 graph_to_dot_write(G, [base(Base)|Conf], Conf0). 2176% 2177graph_to_dot_write(G, Opts, Opts) :- % for DCG use. 2178 once(term_to_graph(G, H, E, N)), 2179 once(graph_to_dot(digraph(g, H, E, N), Digraph)), 2180 obj_get([base(B), out(T)], Opts), 2181 atomic_list_concat([ B, (.), dot], Dot), 2182 atomic_list_concat([ B, (.), T], Tout), 2183 smash(Digraph, DigraphStr), 2184 file(Dot, write, write(DigraphStr)), 2185 pshell(dot(-'T'(T), -o(Tout), Dot)). 2186% 2187% divtag(Opts, Divtag) :- 2188% obj_get([base(Base), out(T)], Opts), 2189% atomics_to_string([Base, ".", T], Loc), 2190% Divtag = [ 2191% "<p><div ", 2192% "id='diagram' ", 2193% % "style='border : solid 2px #ff0000; ", 2194% "style='border : solid 1px red; ", 2195% "width : 1200px; ", % was 600px 2196% "height : 700px; ", % was 300px 2197% "overflow : auto; '><br/>\n", 2198% "<img src=\"", Loc, "\"/>\n", 2199% "</div></p>\n" 2200% ].
2205% ?- show_cla(cla([a,b],[1,2], [1-[a], 2-[b]])). 2206% ?- show_cla(cla([a,b],[1,2], [1-[a,b], 2-[b]])). 2207% ?- show_cla(cla([1],[a], [a-[1]])). 2208% ?- show_cla(cla([1,2],[a], [a-[1,2]])). 2209 2210show_cla(Cla):- cla_to_dot(Cla, DotStr), 2211 T = pdf, 2212 tmp_file_stream(DOT, F0, [encoding(utf8), extension(dot)]), 2213 close(F0), 2214 tmp_file_stream(PDF, F1, [encoding(utf8), extension(pdf)]), 2215 close(F1), 2216 file(DOT, write, write(DotStr)), 2217 pshell(dot(-'T'(T), -o(PDF), DOT); open(PDF)). 2218 2219% old_show_cla(Cla):- cla_to_dot(Cla, DotStr), 2220% T = pdf, 2221% expand_file_name("~/tmp/TEMP.dot", [DOT]), 2222% expand_file_name("~/tmp/TEMP.pdf", [PDF]), 2223% file(DOT, write, write(DotStr)), 2224% pshell(dot(-'T'(T), -o(PDF), DOT); open(PDF)). 2225 2226% 2227cla_to_dot(cla(L, M, N), Dot):- 2228 A = subgraph(cluster_token, L), 2229 B = subgraph(cluster_type, M), 2230 graph_to_dot_string(A; B; [L,M,N], Dot). 2231% 2232graph_to_dot_string(G, Dot):- 2233 once(term_to_graph(G, H, E, N)), 2234 once(graph_to_dot(digraph(g, H, E, N), Digraph)), 2235 smash(Digraph, Dot)