1% MODULE td_basic EXPORTS
    2:- module( td_basic,
    3	   [ distribute_vars/3,
    4	     vars_of_type/3,
    5	     enumerate_t/3,
    6             append_body/3 ]).    7
    8% IMPORTS
    9:- use_module(home(argument_types),
   10                   [type_sub/2]).   11
   12% METAPREDICATES
   13% none
   14
   15
   16%***********************************************************************
   17%*	
   18%* module: td_basic.pl        					
   19%*									
   20%* author:  I.Stahl    		                    date:12/92			
   21%*									
   22%* changed:								
   23%*									
   24%* description:	basics for top-down induction
   25%*									
   26%* see also:	
   27%*									
   28%***********************************************************************
   29
   30
   31
   32%***********************************************************************
   33%*									
   34%* predicate:	append_body/3								
   35%*									
   36%* syntax: append_body(+Clause,+Literal,-Clause1)
   37%*									
   38%* args: Clause,Clause1.. Prolog clauses
   39%*									
   40%* description:	adds Literal to the end of the body of Clause
   41%*									
   42%* example:								
   43%*									
   44%* peculiarities:	none						
   45%*									
   46%* see also:								
   47%*									
   48%***********************************************************************
   49
   50append_body((H:-true),B,(H:-B)):- !.
   51append_body((H:-B),C,(H:-B1)):- 
   52  !, append_body(B,C,B1).
   53append_body((A,B),C,(A,D)):-
   54  !, append_body(B,C,D).
   55append_body(A,B,(A,B)).
   56
   57
   58%***********************************************************************
   59%*
   60%* predicate: distribute_vars/3	
   61%*
   62%* syntax: distribute_vars(+PVars,+Terms,-DVars) 
   63%*		 	
   64%* args:  PVars = [X:Tx|R]: terms X with types Tx in the new literal P    
   65%*        Terms: all terms with their types in the clause C to be refined 
   66%*   
   67%*        DVars = [X:Vx,...]: for each X in PVars a list of all type-matching
   68%*               variables Vx in Terms + an additional new variable    
   69%*
   70%* description: computes DVars 
   71%*
   72%* example:          
   73%*	
   74%* peculiarities:	none						
   75%*									
   76%* see also:								
   77%*									
   78%***********************************************************************
   79
   80distribute_vars([],_,[]).
   81distribute_vars([X:Tx|R],V,[X:Vx|R1]):-
   82   distribute_vars(R,V,R1),
   83   vars_of_type(V,Tx,Vx).
   84
   85
   86%***********************************************************************
   87%*
   88%* predicate: vars_of_type/3	
   89%*
   90%* syntax: vars_of_type(+Terms,+Ty,-R2) 
   91%*		 	
   92%* args:  Terms= [X:Tx|_]: terms X with types Tx in the clause C to be refined
   93%*        Ty: type Ty of an argument of the new literal  
   94%*        R2: a list of all terms in C matching  type Ty         
   95%*	
   96%* description: adds a term X of Terms to R2 if type Ty subsumes type 
   97%*          of X or vice versa
   98%*          and one new term (last element in R2) 
   99%*
  100%* example:         
  101%*	
  102%* peculiarities:	none						
  103%*									
  104%* see also:								
  105%*									
  106%***********************************************************************
  107
  108vars_of_type([],_,[_]).
  109vars_of_type([X:Tx|R],Ty,R2):-
  110   vars_of_type(R,Ty,R1),
  111   (   (type_sub(Ty,Tx);type_sub(Tx,Ty)) ->
  112       R2 = [X|R1]
  113   ;   R2 = R1
  114   ).
  115
  116
  117%***********************************************************************
  118%*
  119%* predicate: enumerate_t/3	
  120%*
  121%* syntax: enumerate_t(+DVars,+PL,-PL2)
  122%*		 	
  123%* args:   DVars = [X:Vx,...]: all variables X in the new literal    
  124%*               with their type-matching variables in C 
  125%*         PL:  initial predicate list 
  126%*
  127%*         PL2:  predicate list 
  128%*	
  129%* description: computes predicates P where variables in Vx are unified to X in P  
  130%*
  131%* example:        
  132%*	
  133%* peculiarities:	none						
  134%*									
  135%* see also:								
  136%*
  137%***********************************************************************
  138
  139enumerate_t([],PL,PL).
  140enumerate_t([X:Vx|R],PL,PL2):-
  141   enumerate_t(R,PL,PL1),
  142   et(Vx,X,PL1,PL2).
  143
  144
  145%***********************************************************************
  146%*
  147%* predicate: et/4	
  148%*
  149%* syntax: et(+Vx,+X,+PL,-PL3)
  150%*		 	
  151%* args:   Vx: a list of variables to be unified with X 	
  152%*         X:  a term of P to be unified by a variable of Vx 
  153%*         PL:  initial predicate list
  154%*
  155%*         PL3:  predicate list
  156%*
  157%* example:
  158%*	
  159%* peculiarities:	none						
  160%*									
  161%* see also:								
  162%*									
  163%***********************************************************************
  164
  165et([],_,_,[]).
  166et([Y|R],X,PL,PL3):-
  167   et(R,X,PL,PL1),
  168   etx(PL,X,Y,PL2),
  169   append(PL2,PL1,PL3).
  170
  171
  172%***********************************************************************
  173%*
  174%* predicate: etx/4	
  175%*
  176%* syntax: etx(PL,X,Y,R2)                     					
  177%*		 	
  178%* args:   PL: literals of P	
  179%*         X:  a term of P to be unified by Y 
  180%*         Y:  a term of the clause C to be unfied with X  
  181%*
  182%*         R2:  predicate list  where X and Y are unified 
  183%*
  184%* description: (if Y is not in args(P) then ) "unify" X and Y. This is
  185%*     done by copying P and replacing X by Y. 
  186%*
  187%* example:        
  188%*	
  189%* peculiarities:	none						
  190%*									
  191%* see also:								
  192%*
  193%***********************************************************************
  194
  195etx([],_,_,[]).
  196etx([P|R],X,Y,R2):-
  197   etx(R,X,Y,R1),
  198   functor(P,F,N),
  199   functor(P1,F,N),
  200   etx1(N,P,P1,X,Y),
  201   R2 = [P1|R1].
  202
  203
  204
  205%***********************************************************************
  206%*
  207%* predicate: etx1/5	
  208%*
  209%* syntax: etx1(+N,+P,-P1,+X,+Y)                     					
  210%*		 	
  211%* args:  N: arity of literal P 
  212%*        P: literal to be added
  213%*        X: variable to be replaced by Y
  214%*        Y: variable
  215%*	
  216%* description: replaces X by Y in the copy P1 of P 
  217%*
  218%* example:        
  219%*	
  220%* peculiarities:	none						
  221%*									
  222%* see also:								
  223%*									
  224%***********************************************************************
  225
  226etx1(0,_,_,_,_):- !.
  227etx1(N,P,P1,X,Y):-
  228   N1 is N - 1,
  229   etx1(N1,P,P1,X,Y),
  230   arg(N,P,Pn),
  231   (   Pn == X ->
  232       arg(N,P1,Y)
  233   ;   arg(N,P1,Pn)
  234   )