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 )