|
1 |
| -/** Predicates from [*Indexing dif/2*](https://arxiv.org/abs/1607.01590). |
| 1 | +:- module(reif, |
| 2 | + [if_/3, |
| 3 | + cond_t/3, |
| 4 | + (=)/3, |
| 5 | + dif/3, |
| 6 | + (',')/3, |
| 7 | + (;)/3, |
| 8 | + memberd_t/3, |
| 9 | + tmember/2, |
| 10 | + tmember_t/3, |
| 11 | + tfilter/3, |
| 12 | + tpartition/4 |
| 13 | +% |
| 14 | + ], [hidden(true)]). |
| 15 | +% |
| 16 | +% |
| 17 | +% |
2 | 18 |
|
3 |
| -Example: |
| 19 | +/** <module> Reified if, reification library v3 |
4 | 20 |
|
5 |
| -``` |
6 |
| -?- tfilter(=(a), [X,Y], Es). |
7 |
| - X = a, Y = a, Es = "aa" |
8 |
| -; X = a, Es = "a", dif:dif(a,Y) |
9 |
| -; Y = a, Es = "a", dif:dif(a,X) |
10 |
| -; Es = [], dif:dif(a,X), dif:dif(a,Y). |
11 |
| -``` |
| 21 | +@author Ulrich Neumerkel |
| 22 | +see Indexing dif/2 |
| 23 | +U. Neumerkel and S. Kral. https://arxiv.org/abs/1607.01590 [cs.PL]. July 2016. |
12 | 24 | */
|
13 | 25 |
|
14 |
| -:- module(reif, [if_/3, (=)/3, (',')/3, (;)/3, cond_t/3, dif/3, |
15 |
| - memberd_t/3, tfilter/3, tmember/2, tmember_t/3, |
16 |
| - tpartition/4]). |
17 | 26 |
|
18 |
| -:- use_module(library(dif)). |
| 27 | +:- meta_predicate |
| 28 | + if_(1, 0, 0), |
| 29 | + cond_t(1, 0, ?), |
| 30 | + tfilter(2, ?, ?), |
| 31 | + tpartition(2, ?, ?, ?), |
| 32 | + ','(1, 1, ?), |
| 33 | + ;(1, 1, ?), |
| 34 | + tmember(2, ?), |
| 35 | + tmember_t(2, ?, ?). |
19 | 36 |
|
20 |
| -:- meta_predicate(if_(1, 0, 0)). |
| 37 | +:- op(900, fy, [$]). |
21 | 38 |
|
22 |
| -if_(If_1, Then_0, Else_0) :- |
23 |
| - call(If_1, T), |
24 |
| - ( T == true -> call(Then_0) |
25 |
| - ; T == false -> call(Else_0) |
26 |
| - ; nonvar(T) -> throw(error(type_error(boolean, T), _)) |
27 |
| - ; throw(error(instantiation_error, _)) |
28 |
| - ). |
| 39 | +% uwnportray(T) :- write_term(T,[quoted(true)]),nl. |
29 | 40 |
|
30 |
| -=(X, Y, T) :- |
31 |
| - ( X == Y -> T = true |
32 |
| - ; X \= Y -> T = false |
33 |
| - ; T = true, X = Y |
34 |
| - ; T = false, dif(X, Y) |
35 |
| - ). |
| 41 | +uwnportray(T) :- portray_clause(T). % Item#539 |
36 | 42 |
|
37 |
| -dif(X, Y, T) :- |
38 |
| - =(X, Y, NT), |
39 |
| - non(NT, T). |
| 43 | +$(X) :- uwnportray(call-X),X,uwnportray(exit-X). |
| 44 | +$(C,V1) :- |
| 45 | + $call(C,V1). |
| 46 | +$(C,V1,V2) :- |
| 47 | + $call(C,V1,V2). |
| 48 | +$(C,V1,V2,V3) :- |
| 49 | + $call(C,V1,V2,V3). |
| 50 | +$(C,V1,V2,V3,V4) :- |
| 51 | + $call(C,V1,V2,V3,V4). |
| 52 | +$(C,V1,V2,V3,V4,V5) :- |
| 53 | + $call(C,V1,V2,V3,V4,V5). |
| 54 | +$(C,V1,V2,V3,V4,V5,V6) :- |
| 55 | + $call(C,V1,V2,V3,V4,V5,V6). |
| 56 | +$(C,V1,V2,V3,V4,V5,V6,V7) :- |
| 57 | + $call(C,V1,V2,V3,V4,V5,V6,V7). |
40 | 58 |
|
41 |
| -non(true, false). |
42 |
| -non(false, true). |
| 59 | +goal_expanded(MG_0, MGx_0) :- |
| 60 | + var(MG_0), |
| 61 | + !, |
| 62 | + MG_0 = MGx_0. |
| 63 | +goal_expanded(call(MG_1, X), MGx_0) :- |
| 64 | + MG_1 = M:G_1, atom(M), callable(G_1), G_1 \= (_:_), |
| 65 | + functor_(G_1, G_0, X), |
| 66 | + \+ predicate_property(M:G_0, (meta_predicate _)), |
| 67 | + !, |
| 68 | + MGx_0 = M:G_0. |
| 69 | +goal_expanded(call(G_0), Gx_0) :- |
| 70 | + acyclic_term(G_0), |
| 71 | + nonvar(G_0), |
| 72 | + % more conditions |
| 73 | + !, |
| 74 | + G_0 = Gx_0. |
| 75 | +goal_expanded(MG_0, MG_0). |
43 | 76 |
|
44 |
| -:- meta_predicate(tfilter(2, ?, ?)). |
45 | 77 |
|
46 |
| -tfilter(_, [], []). |
47 |
| -tfilter(C_2, [E|Es], Fs0) :- |
48 |
| - if_(call(C_2, E), Fs0 = [E|Fs], Fs0 = Fs), |
49 |
| - tfilter(C_2, Es, Fs). |
| 78 | +functor_(T, TA, A) :- |
| 79 | + functor(T, F, N0), |
| 80 | + N1 is N0+1, |
| 81 | + functor(TA, F, N1), |
| 82 | + arg(N1, TA, A), |
| 83 | + sameargs(N0, T, TA). |
| 84 | + |
| 85 | +sameargs(N0, S, T) :- |
| 86 | + N0 > 0, |
| 87 | + N1 is N0-1, |
| 88 | + arg(N0, S, A), |
| 89 | + arg(N0, T, A), |
| 90 | + sameargs(N1, S, T). |
| 91 | +sameargs(0, _, _). |
| 92 | + |
| 93 | + |
| 94 | +/* |
| 95 | + no !s that cut outside. |
| 96 | + no variables in place of goals |
| 97 | + no malformed goals like integers |
| 98 | +*/ |
| 99 | + |
| 100 | + |
| 101 | +/* 2do: unqualified If_1: error |
| 102 | +*/ |
| 103 | + |
| 104 | +% |
| 105 | +goal_expansion(if_(If_1, Then_0, Else_0), _L0, _M, G_0, []) :- |
| 106 | + ugoal_expansion(if_(If_1, Then_0, Else_0), G_0). |
50 | 107 |
|
51 |
| -:- meta_predicate(tpartition(2, ?, ?, ?)). |
| 108 | +% |
| 109 | +% |
| 110 | +% |
| 111 | +% |
| 112 | +% |
| 113 | +% |
| 114 | +% |
| 115 | +% |
| 116 | +% |
| 117 | +% |
| 118 | +% |
| 119 | +ugoal_expansion(if_(If_1, Then_0, Else_0), Goal_0) :- |
| 120 | + subsumes_term(M:(X=Y), If_1), |
| 121 | + M:(X=Y) = If_1, |
| 122 | + atom(M), |
| 123 | + ( M == reif -> true ; predicate_property(M: =(_,_,_),imported_from(reif)) ), |
| 124 | + goal_expanded(call(Then_0), Thenx_0), |
| 125 | + goal_expanded(call(Else_0), Elsex_0), |
| 126 | + !, |
| 127 | + Goal_0 = |
| 128 | + ( X \= Y -> Elsex_0 |
| 129 | + ; X == Y -> Thenx_0 |
| 130 | + ; X = Y, Thenx_0 |
| 131 | + ; dif(X,Y), Elsex_0 |
| 132 | + ). |
| 133 | +% if_((A_1;B_1), Then_0, Else_0) |
| 134 | +% => if_(A_1, Then_0, if_(B_1, Then_0, Else_0)) |
| 135 | +ugoal_expansion(if_(If_1, Then_0, Else_0), Goal) :- |
| 136 | + subsumes_term(M:(A_1;B_1), If_1), |
| 137 | + M:(A_1;B_1) = If_1, |
| 138 | + atom(M), |
| 139 | + ( M == reif -> true ; predicate_property(M:;(_,_,_),imported_from(reif)) ), |
| 140 | + !, |
| 141 | + Goal = if_(A_1, Then_0, if_(B_1, Then_0, Else_0)). |
| 142 | +ugoal_expansion(if_(If_1, Then_0, Else_0), Goal_0) :- |
| 143 | + subsumes_term(M:(A_1,B_1), If_1), |
| 144 | + M:(A_1,B_1) = If_1, |
| 145 | + atom(M), |
| 146 | + ( M == reif -> true ; predicate_property(M:','(_,_,_),imported_from(reif)) ), |
| 147 | + !, |
| 148 | + Goal_0 = if_(A_1, if_(B_1, Then_0, Else_0), Else_0). |
| 149 | +ugoal_expansion(if_(If_1, Then_0, Else_0), Goal_0) :- |
| 150 | + goal_expanded(call(If_1, T), Ifx_0), |
| 151 | + goal_expanded(call(Then_0), Thenx_0), |
| 152 | + goal_expanded(call(Else_0), Elsex_0), |
| 153 | + Goal_0 = |
| 154 | + ( Ifx_0, |
| 155 | + ( T == true -> Thenx_0 |
| 156 | + ; T == false -> Elsex_0 |
| 157 | + ; nonvar(T) -> throw(error(type_error(boolean,T), |
| 158 | + type_error(call(If_1,T),2,boolean,T))) |
| 159 | + ; throw(error(instantiation_error, |
| 160 | + instantiation_error(call(If_1,T),2))) |
| 161 | + ) |
| 162 | + ). |
| 163 | +% |
| 164 | +% |
| 165 | +% |
| 166 | +% |
| 167 | +% |
| 168 | +% |
| 169 | +% |
| 170 | +% |
| 171 | +% |
| 172 | +% |
| 173 | +% |
| 174 | +% |
| 175 | +% |
| 176 | +% |
| 177 | +% |
| 178 | +% |
| 179 | +% |
| 180 | +% |
| 181 | +% |
| 182 | +% |
| 183 | +% |
| 184 | +% |
| 185 | +% |
| 186 | +% |
| 187 | +% |
| 188 | +% |
| 189 | +% |
| 190 | +% |
| 191 | +% |
| 192 | +% |
| 193 | +% |
| 194 | +% |
| 195 | +% |
| 196 | +% |
| 197 | +% |
| 198 | +% |
| 199 | +% |
| 200 | +% |
| 201 | +% |
| 202 | +% |
| 203 | +% |
| 204 | +% |
| 205 | +% |
| 206 | +% |
| 207 | +% |
| 208 | +% |
| 209 | +% |
| 210 | +% |
| 211 | +% |
| 212 | +% |
| 213 | +% |
| 214 | +% |
| 215 | +% |
| 216 | +% |
| 217 | +% |
| 218 | +% |
| 219 | + |
| 220 | +if_(If_1, Then_0, Else_0) :- |
| 221 | + call(If_1, T), |
| 222 | + ( T == true -> Then_0 |
| 223 | + ; T == false -> Else_0 |
| 224 | + ; nonvar(T) -> throw(error(type_error(boolean,T), |
| 225 | + type_error(call(If_1,T),2,boolean,T))) |
| 226 | + ; throw(error(instantiation_error,instantiation_error(call(If_1,T),2))) |
| 227 | + ). |
| 228 | + |
| 229 | + |
| 230 | +tfilter(C_2, Es, Fs) :- |
| 231 | + i_tfilter(Es, C_2, Fs). |
| 232 | + |
| 233 | +i_tfilter([], _, []). |
| 234 | +i_tfilter([E|Es], C_2, Fs0) :- |
| 235 | + if_(call(C_2, E), Fs0 = [E|Fs], Fs0 = Fs), |
| 236 | + i_tfilter(Es, C_2, Fs). |
52 | 237 |
|
53 | 238 | tpartition(P_2, Xs, Ts, Fs) :-
|
54 | 239 | i_tpartition(Xs, P_2, Ts, Fs).
|
|
60 | 245 | , ( Fs0 = [X|Fs], Ts0 = Ts ) ),
|
61 | 246 | i_tpartition(Xs, P_2, Ts, Fs).
|
62 | 247 |
|
63 |
| -:- meta_predicate(','(1, 1, ?)). |
| 248 | +=(X, Y, T) :- |
| 249 | + ( X == Y -> T = true |
| 250 | + ; X \= Y -> T = false |
| 251 | + ; T = true, X = Y |
| 252 | + ; T = false, |
| 253 | + dif(X, Y) |
| 254 | + ). |
64 | 255 |
|
65 |
| -','(A_1, B_1, T) :- |
66 |
| - if_(A_1, call(B_1, T), T = false). |
| 256 | +dif(X, Y, T) :- |
| 257 | + =(X, Y, NT), |
| 258 | + non(NT, T). |
67 | 259 |
|
68 |
| -:- meta_predicate(';'(1, 1, ?)). |
| 260 | +non(true, false). |
| 261 | +non(false, true). |
69 | 262 |
|
70 |
| -';'(A_1, B_1, T) :- |
71 |
| - if_(A_1, T = true, call(B_1, T)). |
| 263 | +','(A_1, B_1, T) :- |
| 264 | + if_(A_1, call(B_1, T), T = false). |
72 | 265 |
|
73 |
| -:- meta_predicate(cond_t(1, 0, ?)). |
| 266 | +;(A_1, B_1, T) :- |
| 267 | + if_(A_1, T = true, call(B_1, T)). |
74 | 268 |
|
75 | 269 | cond_t(If_1, Then_0, T) :-
|
76 | 270 | if_(If_1, ( Then_0, T = true ), T = false ).
|
|
82 | 276 | i_memberd_t([X|Xs], E, T) :-
|
83 | 277 | if_( X = E, T = true, i_memberd_t(Xs, E, T) ).
|
84 | 278 |
|
85 |
| -:- meta_predicate(tmember(2, ?)). |
86 |
| - |
87 | 279 | tmember(P_2, [X|Xs]) :-
|
88 | 280 | if_( call(P_2, X), true, tmember(P_2, Xs) ).
|
89 | 281 |
|
90 |
| -:- meta_predicate(tmember_t(2, ?, ?)). |
91 |
| - |
92 | 282 | tmember_t(_P_2, [], false).
|
93 | 283 | tmember_t(P_2, [X|Xs], T) :-
|
94 | 284 | if_( call(P_2, X), T = true, tmember_t(P_2, Xs, T) ).
|
0 commit comments