1% MODULE argument_types EXPORTS 2:- module( argument_types, 3 [ argument_types/0, 4 type_restriction/2, 5 type_equal/2, 6 type_equal/4, 7 replace_t/4, 8 type_sub/2, 9 type_of/3, 10 types_of/3, 11 compare_types/3, 12 define_type/0, 13 verify_types/0 14 ]). 15 16 17% IMPORTS 18:- use_module(home(kb), 19 [get_example/3, get_clause/5, 20 store_clauses/2,store_clause/4, 21 known/6,delete_clause/1]). 22:- use_module(home(lgg), 23 [set_lgg/2]). 24:- use_module(home(div_utils), 25 [body2list/2, myforall/2, different_predicates/2, 26 nth_arg/3, remove_v/3, make_unique/2, shares_var/2, 27 mysetof/3]). 28:- use_module(home(var_utils), 29 [only_vars/2]). 30:- use_module(home(td_basic), 31 [append_body/3]). 32:- use_module(home(interpreter), 33 [t_interpreter/2]). 34:- use_module(home(show_utils), 35 [show_kb_types/0]). 36:- use_module_if_exists(library(subsumes), 37 [variant/2]). 38:- use_module_if_exists(library(occurs), 39 [contains_var/2]). 40:- use_module_if_exists(library(basics), 41 [member/2]). 42:- use_module_if_exists(library(strings), 43 [gensym/2]). 44 45% METAPREDICATES 46% none 47 48 49:- dynamic type_restriction/2. 50 51%*********************************************************************** 52%* 53%* module: argument_types.pl 54%* 55%* author: I.Stahl date:12/92 56%* 57%* changed: 58%* 59%* 60%* description: algorithm for determining argument types 61%* results for each predicate p within the pos examples 62%* in a kb entry 63%* type_restriction(p(V1,..,Vn),[type1(V1),...,typen(Vn)]) 64%* 65%* 66%* see also: 67%* 68%*********************************************************************** 69 70 71%*********************************************************************** 72%* 73%* predicate: argument_types/0 74%* 75%* syntax: - 76%* 77%* args: none 78%* 79%* 80%* description: toplevel predicate for determining argument types 81%* results for each predicate p within the pos examples 82%* in a kb entry 83%* type_restriction(p(V1,..,Vn),[type1(V1),...,typen(Vn)]) 84%* 85%* 86%* example: 87%* 88%* peculiarities: none 89%* 90%* 91%* see also: 92%* 93%*********************************************************************** 94 95argument_types:- 96 mysetof(E,I^get_example(I,E,'+'),Elist), % Elist = [E1,...,En] pos examples 97 different_predicates(Elist,Elist1), % Elist1 = [[E1,..,Em],...] 98 % list of lists of pos examples with 99 % the same predicate symbol 100 argument_types(Elist1). 101 102 103argument_types([]). 104argument_types([E|R]):- 105 argument_types(R), 106 arg_types(E). 107 108arg_types([E|R]):- 109 functor(E,P,N), 110 functor(P1,P,N), 111 ( type_restriction(P1,_) -> 112 true 113 ; assertz(type_restriction(P1,[])) % assert a type restriction for the 114 % predicate if not already present 115 ), 116 arg_types(N,[E|R],P,N). 117 118 119 120 121%*********************************************************************** 122%* 123%* predicate: arg_types/4 124%* 125%* syntax: arg_types(+Counter,+Examplelist,+Pred_symbol,+Pred_arity) 126%* 127%* args: 128%* 129%* 130%* description: 131%* for each argument position (1 to Pred_arity) of the predicate Pred_symbol 132%* the type of the terms occurring at that position is determined. 133%* If the same type occurred already elsewhere, the old definition is taken 134%* in order to avoid duplicate type definitions 135%* 136%* example: 137%* 138%* peculiarities: none 139%* 140%* 141%* see also: 142%* 143%*********************************************************************** 144 145arg_types(0,_,_,_):- !. 146arg_types(N,EL,P,M):- 147 N1 is N - 1, 148 arg_types(N1,EL,P,M), 149 nth_arg(EL,N,S), 150 gensym(type,Type), 151 arg_type(S,[],[],CL,Type), 152 minimize_cl(CL,Type,Type1), 153 adapt_type_restriction(M,P,N,Type1). 154 155 156%*********************************************************************** 157%* 158%* predicate: arg_type/5 159%* 160%* syntax: arg_type(+Set_of_Argterms,+Ancestors,+Clause_list,-Clause_list,+Typename) 161%* 162%* args: 163%* 164%* 165%* description: 166%* Ancestors are all types calling Typename in their definition. Clauselist 167%* contains all clauses defining Typename 168%* 169%* example: 170%* 171%* peculiarities: none 172%* 173%* 174%* see also: 175%* 176%*********************************************************************** 177 178arg_type(S,Ancestors,CL,CL2,T):- 179 different_predicates(S,Slist), % splits the set of Argterms according to 180 % different functors, Slist = [[T1,..,Tm],..] 181 182 init_cl(Slist,T,CL0), % for each set of Argterms in Slist, generate 183 % a clause head with pred symbol Typename 184 append(CL,CL0,CL1), 185 refine_cl(Slist,[T|Ancestors],CL0,CL1,CL2). % generate clause bodies 186 187init_cl([],_,[]). 188init_cl([EL|R],T,[(T1:-true)|R1]):- 189 init_cl(R,T,R1), 190 set_lgg(EL,E), 191 T1 =.. [T,E]. 192 193 194%*********************************************************************** 195%* 196%* predicate: refine_cl/5 197%* 198%* syntax: refine_cl(+Slist,+Ancestors,+Clauses,+Clauselist,-Clauselist) 199%* 200%* args: 201%* 202%* 203%* description: 204%* for each set of Argterms in Slist and each corresponding clause head 205%* in Clauses and Clauselist, add a body literal for each variable in the 206%* clause head. This body literal may be atom(_),atomic(_),number(_), 207%* typex(_),where typex is in Ancestors, or typez(_), where typez is a 208%* new type (recursive call of the algorithm) 209%* 210%* example: 211%* 212%* peculiarities: none 213%* 214%* 215%* see also: 216%* 217%*********************************************************************** 218 219refine_cl([],_,_,CL,CL). 220refine_cl([S|R],A,[(Head:- _)|R1],CL,CL2):- 221 refine_cl(R,A,R1,CL,CL1), 222 arg(1,Head,E), 223 ( var(E) -> 224 test_var_instantiations(E,S,Head,A,CL1,CL2) 225 % if the head argument is a variable, test its instantiations 226 % in S and add the corresponding literal to the body of Head 227 ; functor(E,_,N), 228 ref_cl(N,E,S,Head,A,CL1,CL2) 229 % if the head argument is no variable, 230 % decompose it, test the variables it contains 231 % and add the corresponding literals to the body 232 % of Head 233 ). 234 235 236%*********************************************************************** 237%* 238%* predicate: ref_cl/7 239%* 240%* syntax: ref_cl(+Counter,+Argument,+Argterms,+Head,+Ancestors, 241%* +Clauselist, -Clauselist) 242%* 243%* args: 244%* 245%* description: decompose the head argument and test the variables it contains; 246%* add the corresponding literals to the body of Head 247%* 248%* 249%* example: 250%* 251%* peculiarities: none 252%* 253%* 254%* see also: 255%* 256%*********************************************************************** 257 258ref_cl(0,_,_,_,_,CL,CL):- !. 259ref_cl(N,E,S,H,A,CL,CL2):- 260 N1 is N - 1, 261 ref_cl(N1,E,S,H,A,CL,CL1), 262 arg(N,E,X),nth_arg(S,N,Sn), 263 ( var(X) -> 264 test_var_instantiations(X,Sn,H,A,CL1,CL2) 265 ; functor(X,_,M), 266 ref_cl(M,X,Sn,H,A,CL1,CL2) 267 ). 268 269 270 271%*********************************************************************** 272%* 273%* predicate: test_var_instantiation/6 274%* 275%* syntax: test_var_instantiations(+Var,+Argterms,+Head,+Ancestors, 276%* +Clauselist,-Clauselist) 277%* 278%* args: 279%* 280%* 281%* description: 282%* Argterms are the instantiations of Var. If all instantiations of Var 283%* are atoms/number/atomic, the literal atom(Var)/number(Var)/atomic(Var) is 284%* added to the body of Head in Clauselist. Else if the definition of a typex 285%* in Ancestors covers all instantiations of Var, typex(Var) is added to the 286%* body of Head in Clauselist (recursive definition). Else a new symbol typen 287%* is created, the literal typen(Var) is added to the body of Head in Clauselist 288%* and a definition of typen is induced by a recursive call of arg_type. 289%* 290%* example: 291%* 292%* peculiarities: none 293%* 294%* see also: 295%* 296%*********************************************************************** 297 298test_var_instantiations(X,S,H,_,CL,CL1):- 299 myforall(S,atom),!, 300 Lit =.. [atom,X], 301 add_literal(CL,H,Lit,CL1). 302 303test_var_instantiations(X,S,H,_,CL,CL1):- 304 myforall(S,number),!, 305 Lit =.. [number,X], 306 add_literal(CL,H,Lit,CL1). 307 308test_var_instantiations(X,S,H,_,CL,CL1):- 309 myforall(S,atomic),!, 310 Lit =.. [atomic,X], 311 add_literal(CL,H,Lit,CL1). 312 313test_var_instantiations(X,S,H,A,CL,CL1):- 314 test_ancestor(S,A,CL,APred),!, 315 Lit =.. [APred,X], 316 add_literal(CL,H,Lit,CL1). 317 318test_var_instantiations(X,S,H,A,CL,CL1):- 319 gensym(type,T), 320 Lit =.. [T,X], 321 add_literal(CL,H,Lit,CL0), 322 arg_type(S,A,CL0,CL1,T). 323 324 325test_ancestor(S,[APred|_],CL,APred):- 326 myforall_interpreted(S,APred,CL),!. 327test_ancestor(S,[_|R],CL,APred):- 328 test_ancestor(S,R,CL,APred). 329 330 331%*********************************************************************** 332%* 333%* predicate: myforall_interpreted/3 334%* 335%* syntax: myforall_interpreted(+Argterms,+Pred,+Clauselist) 336%* 337%* args: 338%* 339%* 340%* description: tests for each argument term T in Argterms whether Pred(T) 341%* follows from Clauselist. For that purpose, a special interpreter 342%* t_interpreter is used that works on Clauselist as program instead 343%* of the knowledge base. 344%* 345%* example: 346%* 347%* peculiarities: none 348%* 349%* 350%* see also: 351%* 352%*********************************************************************** 353 354myforall_interpreted([],_,_). 355myforall_interpreted([E|R],Pred,CL):- 356 C =.. [Pred,E], 357 t_interpreter(C,CL), 358 myforall_interpreted(R,Pred,CL). 359 360 361%*********************************************************************** 362%* 363%* predicate: add_literal/4 364%* 365%* syntax: add_literal(+Clauselist,+Head,+Lit,-Clauselist1) 366%* 367%* args: 368%* 369%* description: adds literal Lit to the clause (Head:- B) within Clauselist 370%* 371%* example: 372%* 373%* peculiarities: none 374%* 375%* 376%* see also: 377%* 378%*********************************************************************** 379 380add_literal([(H:-B)|R],H1, Lit, [(H:- (Lit,B))|R]):- 381 H == H1,!. 382add_literal([C|R],H,Lit,[C|R1]):- 383 add_literal(R,H,Lit,R1). 384 385 386%*********************************************************************** 387%* 388%* predicate: adapt_type_restriction/4 389%* 390%* syntax: adapt_type_restriction(+Pred_arity,+Pred_name,+A,+Type) 391%* 392%* args: 393%* 394%* description: 395%* Type is the type of the Ath Argposition of the predicate Pred_name. The 396%* type restriction is type_restriction(p(V1,..,Vn),L). If there is not yet 397%* an entry typex(VA) in L, Type(VA) is added to L. Else let the definition 398%* of typex be typex(Hx1):- Bx1. and of Type be Type(H1):- B1. 399%* ... ... 400%* typex(Hxm):- Bxm. Type(Ho):- Bo. 401%* Then we add a new type Tnew(VA) to L with the definition 402%* Tnew(Hx1):- Bx1. Tnew(H1):- B1. 403%* ... ... 404%* Tnew(Hxm):- Bxm. Tnew(Ho):- Bo. 405%* The definitions of typex and Type remain. 406%* 407%* example: 408%* 409%* peculiarities: none 410%* 411%* see also: 412%* 413%*********************************************************************** 414 415adapt_type_restriction(M,P,N,T):- 416 functor(P1,P,M), 417 retract(type_restriction(P1,L)), 418 arg(N,P1,P1n), 419 ( (member(T1,L),T1 =.. [T2,X], X == P1n) -> 420 gensym(type,Tnew), 421 D =.. [Tnew,P1n], 422 remove_v([T1],L,L1), 423 assertz(type_restriction(P1,[D|L1])), 424 adapt_tr(Tnew,T,T2) 425 ; D =.. [T,P1n], 426 assertz(type_restriction(P1,[D|L])) 427 ). 428 429adapt_tr(Tnew,T1,T2):- 430 functor(HT1,T1,1),functor(HT2,T2,1), 431 mysetof((HT1:-B1),I^Clist^(get_clause(I,HT1,B1,Clist,type)),C1), 432 mysetof((HT2:-B2),I^Clist^(get_clause(I,HT2,B2,Clist,type)),C2), 433 append(C1,C2,C3), 434 adapt_tr1(C3,Tnew,C4), 435 make_unique(C4,C5), 436 store_clauses(C5,type). 437 438adapt_tr1([],_,[]). 439adapt_tr1([(H:-B)|R],T,[(H1:-B)|R1]):- 440 adapt_tr1(R,T,R1), 441 H =.. [_|Arg], H1 =.. [T|Arg]. 442 443 444%*********************************************************************** 445%* 446%* predicate: minimize_cl/3 447%* 448%* syntax: minimize_cl(+CL,+Typename,-Typename) 449%* 450%* args: 451%* 452%* description: CL is the list of clauses defining the type Typename. 453%* If CL contains definitions that occur already in the database, 454%* or if it contains duplicate definitions, it is minimized. 455%* 456%* example: 457%* 458%* peculiarities: none 459%* 460%* 461%* see also: 462%* 463%*********************************************************************** 464 465minimize_cl(CL,Type,Type1):- 466 mysetof((H:-B),I^Clist^(get_clause(I,H,B,Clist,type)), Old_types), 467 mysetof(T, H^B^R^(member((H:-B),Old_types),H =.. [T|R]), Oldt_names), 468 mysetof(T, H^B^R^(member((H:-B),CL),H =.. [T|R]), Newt_names), 469 append(Old_types,CL,Clauses), 470 minimize_cl(Oldt_names,Newt_names,Clauses,CL,Type,Type1). 471 472minimize_cl([],Newt_names,Clauses,CL,Type,Type1):- 473 minim_cl(Newt_names,Clauses,CL,Type,Type1). 474minimize_cl([T|R],Newt_names,Clauses,CL,Type,Type2):- 475 mysetof(T1,(member(T1,Newt_names),type_equal(T,T1,[T:T1],Clauses)),Tlist), 476 replace_t(CL,Tlist,T,CL1), 477 make_unique(CL1,CL2), 478 remove_v(Tlist,Newt_names,Newt_names1), 479 ( member(Type,Tlist) -> 480 Type1 = T 481 ; Type1 = Type 482 ), 483 minimize_cl(R,Newt_names1,Clauses,CL2,Type1,Type2). 484 485minim_cl([],_,CL,Type,Type):- 486 min_cl(CL,CL1), 487 store_clauses(CL1,type). % the remaining (minimized) set of clauses is stored 488 % in the database 489minim_cl([T|R],Clauses,CL,Type,Type2):- 490 mysetof(T1,(member(T1,R),type_equal(T,T1,[T:T1],Clauses)),Tlist), 491 replace_t(CL,Tlist,T,CL1), 492 make_unique(CL1,CL2), 493 remove_v(Tlist,R,R1), 494 ( member(Type,Tlist) -> 495 Type1 = T 496 ; Type1 = Type 497 ), 498 minim_cl(R1,Clauses,CL2,Type1,Type2). 499 500min_cl([],[]). 501min_cl([(H:-B)|R],[(H:-B1)|R1]):- 502 min_cl(R,R1), 503 min_cl1(B,B1). 504 505min_cl1((A,true),A):-!. 506min_cl1(true,true):- !. 507min_cl1((A,B),(A,B1)):- 508 min_cl1(B,B1). 509 510 511%*********************************************************************** 512%* 513%* predicate: replace_t/4 514%* 515%* syntax: replace_t(+CL,+List_of_typenames,+Typename,-CL) 516%* 517%* args: 518%* 519%* description: replaces in CL each occurrence of a typename 520%* in List_of_typenames by Typename 521%* 522%* example: 523%* 524%* peculiarities: none 525%* 526%* see also: 527%* 528%*********************************************************************** 529 530replace_t([],_,_,[]). 531replace_t([(H:-_)|R],Tlist,T,R1):- 532 H =.. [T1|_], member(T1,Tlist),!, 533 replace_t(R,Tlist,T,R1). 534replace_t([(H:-B)|R],Tlist,T,[(H:-B1)|R1]):- 535 repl_t(B,Tlist,T,B1), 536 replace_t(R,Tlist,T,R1). 537 538repl_t((A,B),Tlist,T,(A1,B1)):- !, 539 repl_t(A,Tlist,T,A1), 540 repl_t(B,Tlist,T,B1). 541repl_t(A,Tlist,T,A1):- 542 A =.. [T1|R], 543 ( member(T1,Tlist) -> 544 A1 =.. [T|R] 545 ; A1 = A 546 ). 547 548 549%***********************************************************************************% 550%* 551%* predicate: type_equal/2 552%* 553%* syntax: type_equal(+Type_name1,+Type_name2) 554%* 555%* args: 556%* 557%* description: Tests whether the types Type_name1 and Type_name2 are defined 558%* identically 559%* 560%* example: 561%* 562%* peculiarities: 563%* 564%* see also: 565%* 566%********************************************************************************** 567 568type_equal(T,T):- !. 569type_equal(T1,T2):- 570 mysetof((H1:-B1), I^CL^R^(get_clause(I,H1,B1,CL,type), H1 =.. [T1|R]),Clauses1), 571 mysetof((H2:-B2), I^CL^R^(get_clause(I,H2,B2,CL,type), H2 =.. [T2|R]),Clauses2), 572 append(Clauses1,Clauses2,Clauses), 573 type_equal(T1,T2,[T1:T2],Clauses). 574 575type_equal(T,T,_,_):- !. 576type_equal(T1,T2,Ancestors,Clauses):- 577 mysetof((H:-B),R^(member((H:-B),Clauses), H =.. [T1|R]),Clist1), 578 mysetof((H:-B),R^(member((H:-B),Clauses), H =.. [T2|R]),Clist2), 579 compare_clauses(Clist1,Clist2,Clauses,Ancestors). 580 581 582%*********************************************************************** 583%* 584%* predicate: compare_clauses/4 585%* 586%* syntax: compare_clauses(+Clist1,+Clist2,+Clauses12,+Ancestors) 587%* 588%* args: Clist1 .. clauses defining Type_name1 589%* Clist2 .. clauses defining Type_name2 590%* Clauses12 .. all clauses defining Type_name1 and Type_name2 591%* Ancestors .. types already tested on equality 592%* 593%* description: tests whether Type_name1 and Type_name2 are identically 594%* defined by comparing the defining clauses 595%* 596%* example: 597%* 598%* peculiarities: none 599%* 600%* 601%* see also: 602%* 603%*********************************************************************** 604 605compare_clauses([],[],_,_). 606compare_clauses([(H1:-B1)|R],CL2,Clauses,Ancestors):- 607 find_variant_clause(CL2,H1,CL21,(H2:-B2)), 608 arg(1,H1,E1),arg(1,H2,E2), 609 comp_clauses(E1,E2,B1,B2,Clauses,Ancestors), 610 compare_clauses(R,CL21,Clauses,Ancestors). 611 612comp_clauses(E1,E2,B1,B2,C,A):- 613 var(E1),!, 614 def_literal(E1,B1,L1),def_literal(E2,B2,L2), 615 L1 =.. [T1|_], L2 =.. [T2|_], 616 c_clauses(T1,T2,C,A). 617comp_clauses(E1,E2,B1,B2,C,A):- 618 functor(E1,_,N), 619 comp_clauses(N,E1,E2,B1,B2,C,A). 620comp_clauses(0,_,_,_,_,_,_):- !. 621comp_clauses(N,E1,E2,B1,B2,C,A):- 622 N1 is N - 1, 623 comp_clauses(N1,E1,E2,B1,B2,C,A), 624 arg(N,E1,E1n),arg(N,E2,E2n), 625 comp_clauses(E1n,E2n,B1,B2,C,A). 626 627c_clauses(atom,L,_,_):- !, L = atom. 628c_clauses(number,L,_,_):- !, L = number. 629c_clauses(atomic,L,_,_):- !, L = atomic. 630c_clauses(_,L2,_,_):- 631 (L2 = atom ; L2 = number ; L2 = atomic),!, 632 fail. 633c_clauses(T1,T2,C,A):- 634 ( (member(T1:T2,A);member(T2:T1,A)) -> 635 true 636 ; type_equal(T1,T2,[T1:T2|A],C) 637 ). 638 639%*********************************************************************** 640%* 641%* predicate: find_variant_clause/4 642%* 643%* syntax: find_variant_clause(+CL,+Head,-CL1,-Clause) 644%* 645%* args: 646%* 647%* description: CL1 is CL - Clause, where the head argument of Head and 648%* of the head of Clause are variants 649%* 650%* example: 651%* 652%* peculiarities: none 653%* 654%* 655%* see also: 656%* 657%*********************************************************************** 658 659find_variant_clause([(H2:-B2)|R],H1,R,(H2:-B2)):- 660 arg(1,H1,E1),arg(1,H2,E2), 661 variant(E1,E2). 662find_variant_clause([C|R],H,[C|R1],C1):- 663 find_variant_clause(R,H,R1,C1). 664 665%*********************************************************************** 666%* 667%* predicate: def_literal/3 668%* 669%* syntax: def_literal(+Var,+Body,-Lit) 670%* 671%* args: 672%* 673%* description: Lit is the literal within Body that defines the type of 674%* Var 675%* 676%* example: def_literal(A,(atom(A),list(B)),atom(A)) 677%* 678%* peculiarities: none 679%* 680%* see also: 681%* 682%*********************************************************************** 683 684def_literal(X,(A,B),C):- !, 685 ( contains_var(X,A) -> 686 C = A 687 ; def_literal(X,B,C) 688 ). 689def_literal(X,A,A):- 690 contains_var(X,A),!. 691def_literal(X,_,all(X)). 692 693%********************************************************************************** 694%* 695%* predicate: type_sub/2 696%* 697%* syntax: type_sub(+Gen,+Spec) 698%* 699%* args: Gen, Spec: type names or intermediate type definitions 700%* t_int(H):- B (cf. type_of). 701%* 702%* description: succeeds if the type Gen is more general than 703%* the type Spec. 704%* 705%* example: 706%* 707%* peculiarities: none 708%* 709%********************************************************************************** 710 711 712type_sub(Gen,(H:-B)):- 713 type_sub1([(H:-B)],Gen,[]). 714type_sub(Gen,Spec):- 715 type_sub(Gen,Spec,[Gen:Spec]). 716 717 718 719%*********************************************************************** 720%* 721%* predicate: type_sub/3 722%* 723%* syntax: type_sub(+Gen,+Spec,+Ancestors) 724%* 725%* args: 726%* 727%* description: 728%* Ancestors contains the types that have been compared already in order to 729%* avoid infinite recursion 730%* 731%* example: 732%* 733%* peculiarities: none 734%* 735%* see also: 736%* 737%*********************************************************************** 738 739 740type_sub(all,_,_):- !. % all is the most general type 741type_sub(T1,all,_):- !, T1 = all. 742type_sub(T,T1,_):- T == T1,!. 743 744type_sub(atomic,T,_):- 745 !, ( T = atom 746 ; T = atomic 747 ; T = number 748 ; functor(HT,T,1), 749 setof((HT,B),ID^CL^(get_clause(ID,HT,B,CL,type)),TL), 750 all_t_in(TL,[atom,number,atomic]) 751 ). 752type_sub(atom,T,_):- 753 !, ( T = atom 754 ; functor(HT,T,1), 755 setof((HT,B),ID^CL^(get_clause(ID,HT,B,CL,type)),TL), 756 all_t_in(TL,[atom]) 757 ). 758type_sub(number,T,_):- 759 !, ( T = number 760 ; functor(HT,T,1), 761 setof((HT,B),ID^CL^(get_clause(ID,HT,B,CL,type)),TL), 762 all_t_in(TL,[number]) 763 ). 764 765type_sub(T,atomic,_):- 766 !, ( T = atomic 767 ; T = all 768 ; functor(HT,T,1), 769 setof((HT,B),ID^CL^(get_clause(ID,HT,B,CL,type)),TL), 770 all_t_in(TL,[atomic]) 771 ). 772type_sub(T,atom,_):- 773 !, ( T = atom 774 ; T = atomic 775 ; T = all 776 ; functor(HT,T,1), 777 setof((HT,B),ID^CL^(get_clause(ID,HT,B,CL,type)),TL), 778 all_t_in(TL,[atom,atomic]) 779 ). 780type_sub(T,number,_):- 781 !, ( T = number 782 ; T = atomic 783 ; T = all 784 ; functor(HT,T,1), 785 setof((HT,B),ID^CL^(get_clause(ID,HT,B,CL,type)),TL), 786 all_t_in(TL,[number,atomic]) 787 ). 788 789 790type_sub(TG,TS,A):- 791 functor(HTS,TS,1), 792 mysetof((HTS:- BS),ID^CL^(get_clause(ID,HTS,BS,CL,type)),CS), 793 type_sub1(CS,TG,A). 794 795%*********************************************************************** 796%* 797%* predicate: type_sub1/3 798%* 799%* syntax: type_sub1(+SpecClauses,+Gen,+Ancestors) 800%* 801%* args: 802%* 803%* description: 804%* for each clause C in SpecClauses defining the more specific type, 805%* there must be a clause defining Gen that is more general than C 806%* 807%* example: 808%* 809%* peculiarities: none 810%* 811%* see also: 812%* 813%*********************************************************************** 814 815type_sub1([],_,_). 816type_sub1([(H:-B)|R],(HG:-BG),A):- !, 817 type_sub1(R,(HG:-BG),A),!, 818 H =.. [_,Es], HG =.. [_,Es], 819 expand_to_type_def(BG,BG1), 820 is_type_definition((H:- B)), 821 test_type_def(B), 822 is_type_definition((HG:-BG1)), 823 test_type_def(BG1), 824 only_vars(Es,EsV), 825 type_sub2(EsV,BG1,B,A). 826type_sub1([(H:-B)|R],TG,A):- 827 type_sub1(R,TG,A),!, 828 H =.. [_,Es], HTG =.. [TG,Es], 829 get_clause(_,HTG,BG,_,type), 830 expand_to_type_def(BG,BG1), 831 is_type_definition((H:- B)), 832 test_type_def(B), 833 is_type_definition((HTG:-BG1)), 834 test_type_def(BG1), 835 only_vars(Es,EsV), 836 type_sub2(EsV,BG1,B,A). 837 838 839%*********************************************************************** 840%* 841%* predicate: type_sub2/4 842%* 843%* syntax: type_sub2(+Varlist,+Genbody,+Specbody,+Ancestors) 844%* 845%* args: 846%* 847%* description: 848%* tests for each variable V in Varlist whether the literal defining V in Genbody 849%* is of a more general type than the literal defining V in Specbody. 850%* 851%* example: 852%* 853%* peculiarities: none 854%* 855%* see also: 856%* 857%*********************************************************************** 858 859type_sub2([],_,_,_). 860type_sub2([X|R],BG1,B,A):- 861 type_sub2(R,BG1,B,A),!, 862 def_literal(X,BG1,LG), 863 def_literal(X,B,LS), 864 LS =.. [TS|_], LG =.. [TG|_], 865 ( member(TG:TS,A) -> 866 true 867 ; type_sub(TG,TS,[TG:TS|A]) 868 ). 869 870 871%*********************************************************************** 872%* 873%* predicate: expand_to_type_definition/2 874%* 875%* syntax: expand_to_type_definition(+Body,-Body1) 876%* 877%* args: 878%* 879%* description: 880%* transform Body to a valid type definition (i.e. each literal is of the 881%* form t(X), were t in atom,atomic,number,typex and X is simple), by expanding 882%* literals containing complex terms 883%* 884%* example: 885%* 886%* peculiarities: none 887%* 888%* see also: 889%* 890%*********************************************************************** 891 892expand_to_type_def((A,B),(A,B1)):- 893 simple_td(A), 894 expand_to_type_def(B,B1). 895expand_to_type_def((A,B),B1):- 896 \+(simple_td(A)), 897 get_clause(_,A,Lits,_,type), 898 append_body(Lits,B,B0), 899 expand_to_type_def(B0,B1). 900expand_to_type_def(A,A):- 901 simple_td(A). 902expand_to_type_def(A,A1):- 903 \+(A = (_,_)), \+(simple_td(A)), 904 get_clause(_,A,Lits,_,type), 905 expand_to_type_def(Lits,A1). 906 907%*********************************************************************** 908%* 909%* predicate: simple_td/1 910%* 911%* syntax: simple_td(+Lit) 912%* 913%* args: Lit is a literal within a type definition 914%* 915%* description: succeeds if Lit == true, or Lit = t(X), where X is atomic or 916%* a variable 917%* 918%* example: 919%* 920%* peculiarities: none 921%* 922%* see also: 923%* 924%*********************************************************************** 925 926simple_td(true):- !. 927simple_td(A):- A =.. [_,X],simple(X). 928 929%*********************************************************************** 930%* 931%* predicate: test_type_definition/1 932%* 933%* syntax: test_type_definition(Body) 934%* 935%* args: 936%* 937%* description: partially evaluates Body. 938%* Fails if body contains invalid ground literals 939%* with predicate symbol atom, number or atomic 940%* 941%* peculiarities: none 942%* 943%* see also: 944%* 945%*********************************************************************** 946 947test_type_def((A,B)):- !, 948 test_type_def(A), 949 test_type_def(B). 950test_type_def(A):- 951 A =.. [T,X], ground(X), 952 ( T =atom; T = atomic; T = number ),!, 953 call(A). 954test_type_def(_). 955 956 957%*********************************************************************** 958%* 959%* predicate: is_type_definition/1 960%* 961%* syntax: is_type_definition(+Clause) 962%* 963%* args: 964%* 965%* description: 966%* succeeds if Clause is a syntactically correct type definition, i.e. only 967%* atom, atomic, number and typex occur as unary predicate in the body, and 968%* every variable of Clause occurs once in the head and once in the body of Clause 969%* 970%* peculiarities: none 971%* 972%* see also: 973%* 974%*********************************************************************** 975 976is_type_definition((H:-B)):- 977 only_vars(H,Vars), 978 is_type_def(Vars,B). 979 980is_type_def([],_). 981is_type_def([X|R],B):- 982 def_literal(X,B,Lit),!, 983 Lit =.. [_,X1], 984 X == X1, 985 is_type_def(R,B). 986 987all_t_in([],_). 988all_t_in([(H,B)|R],L):- 989 H =.. [_,X], var(X), 990 B =.. [N,X], member(N,L), 991 all_t_in(R,L). 992 993 994%********************************************************************************** 995%* 996%* predicate: type_of/3 997%* 998%* syntax: type_of(+Var,+C,-Type) 999%* 1000%* args: 1001%* 1002%* description: C is a clause or a literal. Returns the most specific type of Var 1003%* within C. If Var does not occur in C or if it occurs at 1004%* positions with incompatible types, type_of returns fail. If Var 1005%* is a term that only partially matches the body of a type 1006%* definition, a intermediate type definition t_int(Var):- B is 1007%* returned 1008%* 1009%* example: 1010%* 1011%* pecularities: 1012%* 1013%********************************************************************************** 1014 1015type_of(V,(H:-B),Type):- !, 1016 type_of(V,H,Type1), 1017 type_of(V,B,Type2), 1018 compare_types(Type1,Type2,Type). 1019type_of(V,(A,B),Type):- !, 1020 type_of(V,A,Type1), 1021 type_of(V,B,Type2), 1022 compare_types(Type1,Type2,Type). 1023type_of(T,Pred,Type):- 1024 ( type_restriction(Pred,Plist) -> 1025 mysetof(Ts,(member(Ts,Plist),contains_var(T,Ts)),TsL), 1026 type_of1(TsL,T,Type) 1027 ; Type = all 1028 ). 1029type_of(_,true,all). 1030 1031type_of1([],_,all). 1032type_of1([Ts|R],T,Type):- !, 1033 type_of1(R,T,Type1), 1034 Ts =.. [Type0,T2], 1035 ( T2 == T -> 1036 compare_types(Type1,Type0,Type) 1037 ; get_clause(_,Ts,_,[_|CL],type), 1038 mysetof(Ts1,(member(Ts1:_,CL),contains_var(T,Ts1)),TsL), 1039 ( TsL = [] -> 1040 mysetof(Ts2,(member(Ts2,CL),shares_var(T,Ts2)),TsL1), 1041 H_int =.. [t_int,T], 1042 kb:body2list(B_int,TsL1), 1043 compare_types(Type1,(H_int:-B_int),Type) 1044 ; type_of1(TsL,T,Type2), 1045 compare_types(Type1,Type2,Type) 1046 ) 1047 ). 1048 1049 1050 1051%********************************************************************************** 1052%* 1053%* predicate: types_of/3 1054%* 1055%* syntax: types_of(+Varlist,+C,-Typelist) 1056%* 1057%* args: 1058%* 1059%* description: like type_of for each Var in Varlist. 1060%* Varlist = [V1,..,Vn] => Typelist = [V1:T1,..,Vn:Tn] 1061%* 1062%* example: 1063%* 1064%* peculiarities: 1065%* 1066%********************************************************************************** 1067 1068types_of([],_,[]). 1069types_of([V|R],C,[V:T|R1]):- 1070 type_of(V,C,T), 1071 types_of(R,C,R1). 1072 1073 1074%*********************************************************************** 1075%* 1076%* predicate: compare_types/3 1077%* 1078%* syntax: compare_types(+Type1,+Type2,-Type) 1079%* 1080%* args: Type1,Type2: types to be compared 1081%* Type: the most specific type among type1 and typ2 1082%* 1083%* description: returns the more specific type 1084%* 1085%* example: 1086%* 1087%* peculiarities: none 1088%* 1089%* see also: 1090%* 1091%*********************************************************************** 1092 1093compare_types(Type1,Type2,Type):- 1094 ( type_sub(Type1,Type2) -> 1095 Type = Type2 1096 ; ( type_sub(Type2,Type1) -> 1097 Type = Type1 1098 ; fail 1099 ) 1100 ). 1101 1102%*********************************************************************** 1103%* 1104%* predicate: define_type/0 1105%* 1106%* syntax: 1107%* 1108%* args: 1109%* 1110%* description: allows to define a type restriction for a predicate 1111%* 1112%* example: 1113%* 1114%* peculiarities: none 1115%* 1116%* see also: 1117%* 1118%*********************************************************************** 1119 1120define_type:- 1121 show_kb_types, 1122 read_type_restriction. 1123 1124read_type_restriction:- 1125 repeat, 1126 nl, write('Please enter name and arity of the predicate p/n: '), 1127 ( (read(P/N),atom(P),integer(N)) -> 1128 functor(F,P,N),F =.. [P|Args], 1129 read_type_restriction(Args,1,Alist), 1130 assert(type_restriction(F,Alist)) 1131 ; fail 1132 ). 1133 1134read_type_restriction([],_,[]). 1135read_type_restriction([V|R],N,[T|R1]):- 1136 repeat, 1137 nl, write('Please enter the type at argument position '),write(N),write(' : '), 1138 ( (read(TN),atom(TN)) -> 1139 ( ((H =.. [TN,_], get_clause(_,H,_,_,type)); 1140 member(TN,[atom,number,atomic])) -> 1141 T =.. [TN,V] 1142 ; read_type_definition(TN), 1143 T =.. [TN,V] 1144 ) 1145 ; fail 1146 ), 1147 N1 is N + 1, 1148 read_type_restriction(R,N1,R1). 1149 1150 1151%*********************************************************************** 1152%* 1153%* predicate: read_type_definition/1 1154%* 1155%* syntax: read_type_definition(+TN) 1156%* 1157%* args: TN.. name of a type 1158%* 1159%* description: allows to enter clauses defining the type TN 1160%* 1161%* example: 1162%* 1163%* peculiarities: none 1164%* 1165%* see also: 1166%* 1167%*********************************************************************** 1168 1169read_type_definition(TN):- 1170 nl, write('Type '),write(TN), write(' is undefined. Enter a definition (y/n)? '), 1171 read(A), 1172 ( A == y -> 1173 read_type_def(TN) 1174 ; ( A == n -> 1175 fail 1176 ; nl, write('Please enter y or n'), 1177 read_type_definition(TN) 1178 ) 1179 ). 1180 1181read_type_def(TN):- 1182 nl, write('Please enter the definition of '),write(TN), 1183 write(' in clausal form. Stop by entering stop.'),nl, 1184 repeat, 1185 read(A), 1186 ( ((A = (H:-_), H =.. [_,_]); (A =.. [_,_])) -> 1187 store_clause(A,_,type,_),nl, 1188 fail 1189 ; ( A == stop -> 1190 true 1191 ; nl, write('Please enter a clause or stop'),fail 1192 ) 1193 ). 1194 1195%*********************************************************************** 1196%* 1197%* predicate: verify_types/0 1198%* 1199%* syntax: 1200%* 1201%* args: 1202%* 1203%* description: checks for the type restrictions in the kb whether 1204%* the contain only defined or built-in types. If not, 1205%* the user is asked for replacing or defining the unknown 1206%* types. 1207%* 1208%* example: 1209%* 1210%* peculiarities: none 1211%* 1212%* see also: 1213%* 1214%*********************************************************************** 1215 1216verify_types:- 1217 findall((M,A),type_restriction(M,A),TSet), 1218 verify_types(TSet). 1219 1220verify_types([]). 1221verify_types([(M,A)|R]):- 1222 verify_types(R), 1223 verify_types(A,M,A). 1224 1225verify_types([],_,_). 1226verify_types([H|R],M,A):- 1227 verify_types(R,M,A), 1228 H =.. [T|_], 1229 findall((H1,B1),(H1 =.. [T,_],known(ID,H1,B1,CL,_,E), 1230 delete_clause(ID), 1231 assertz(kb:known(ID,H1,B1,CL,type,E))),Tlist), 1232 ( (Tlist \== [];member(T,[atom,number,atomic])) -> 1233 true 1234 ; nl, write('The type '),write(T),write(' is undefined in '), 1235 copy_term((M,A),(M1,A1)),numbervars((M1,A1),0,_), 1236 write(type_restriction(M1,A1)),nl, 1237 show_kb_types, 1238 repeat, 1239 nl, write('Do you want to replace '), write(T), write(' in '), 1240 write(type_restriction(M1,A1)),write(' (y/n)?'),nl, 1241 read(An), 1242 ( An == y -> 1243 retract(type_restriction(M,A)), 1244 repeat, 1245 nl, write('Enter the name of the type replacing '), write(T), write(': '), 1246 ( (read(T1),atom(T1)) -> 1247 H1 =.. [T1,_], 1248 ( get_clause(_,H1,_,_,_) -> 1249 vrt(A,T,T1,A2), 1250 assert(type_restriction(M,A2)) 1251 ; nl, write('The type '), write(T1),write(' is undefined.'), 1252 vrt1(T1) 1253 ) 1254 ; fail 1255 ) 1256 ; ( An == n -> 1257 nl,write('Then you have to define '),write(T), 1258 read_type_def(T) 1259 ; write('Please enter y or n'),fail 1260 ) 1261 ) ). 1262 1263vrt([],_,_,[]). 1264vrt([H|R],T,T1,[H1|R1]):- 1265 vrt(R,T,T1,R1), 1266 H =.. [T2,V], 1267 ( T2 == T -> 1268 H1 =.. [T1,V] 1269 ; H1 = H 1270 ). 1271 1272 1273vrt1(T1):- 1274 nl, write('Do you want to define it (y/n)? '), 1275 read(Bn), 1276 ( Bn == y -> 1277 read_type_def(T1) 1278 ; ( Bn == n -> 1279 fail 1280 ; write('Please enter y or n'), 1281 vrt1(T1) 1282 ) 1283 )