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   )