Skip to content

Commit 70e68f7

Browse files
hurufuhurufu
committed
Copy reif.pl from the link specified in the paper
This is a direct copy from http://www.complang.tuwien.ac.at/ulrich/Prolog-inedit/sicstus/reif.pl
1 parent be7bed3 commit 70e68f7

File tree

1 file changed

+179
-131
lines changed

1 file changed

+179
-131
lines changed

‎src/lib/reif.pl

Lines changed: 179 additions & 131 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,60 @@
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+
%
218

3-
Example:
19+
/** <module> Reified if, reification library v3
420
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.
1224
*/
1325

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]).
1726

18-
:- use_module(library(dif)).
19-
20-
% TODO: Remove when fully debugged
21-
:- use_module(library(debug)).
22-
:- use_module(library(format)).
23-
:- op(750, xfy, =>).
24-
:- op(950, fy, +).
25-
%+(A) :- call(A).
26-
+(_).
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, ?, ?).
36+
37+
:- op(900, fy, [$]).
38+
39+
% uwnportray(T) :- write_term(T,[quoted(true)]),nl.
40+
41+
uwnportray(T) :- portray_clause(T). % Item#539
42+
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).
2758

2859
goal_expanded(MG_0, MGx_0) :-
2960
var(MG_0),
@@ -44,14 +75,6 @@
4475
goal_expanded(MG_0, MG_0).
4576

4677

47-
%% functor_(+T, ?TA, ?A).
48-
%
49-
% `TA` is `T` extended with additional parameter `A`
50-
%
51-
% ```
52-
% ?- functor_(a(b), X, c).
53-
% X = a(b,c).
54-
% ```
5578
functor_(T, TA, A) :-
5679
functor(T, F, N0),
5780
N1 is N0+1,
@@ -68,129 +91,149 @@
6891
sameargs(0, _, _).
6992

7093

71-
/* FIXME: What does this ↓ comment from the source mean? Is it a list of features, "to do" items or guidelines? */
7294
/*
7395
no !s that cut outside.
7496
no variables in place of goals
7597
no malformed goals like integers
7698
*/
7799

78100

79-
/* FIXME: How can I reproduce this? ↓ */
80101
/* 2do: unqualified If_1: error
81102
*/
82103

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).
83107

84-
user:goal_expansion(if_(If_1, Then_0, Else_0), G_0) :-
85-
ugoal_expansion(if_(If_1, Then_0, Else_0), G_0),
86-
% Dump expanded goals to the console for inspection.
87-
% TODO: Remove when fully debugged
88-
+ portray_clause((if_(If_1,Then_0,Else_0) => G_0)).
89-
90-
91-
%% ugoal_expansion(if_(+If_1, ?Then_0, ?Else_0), -Goal_0).
92108
%
93-
% Performance of if_/3 heavily relies on call/N, this predicates tries to unwrap
94-
% some terms for improved speed.
95109
%
96-
% Expansion rules:
97110
%
98-
% if_(A=B,Then_0,Else_0)
99-
% => if equality of A and B is satisfiable then expanded `Then_0`, otherwise
100-
% expanded `Else_0`.
101111
%
102-
% if_((A_1;B_1), Then_0, Else_0)
103-
% => if_(A_1, Then_0, if_(B_1, Then_0, Else_0))
104112
%
105-
% if_((A_1,B_1), Then_0, Else_0)
106-
% => if_(A_1, if_(B_1, Then_0, Else_0), Else_0).
107113
%
108-
% Otherwise it simply expands If_1, Then_0 and Else_0 using goal_expanded/2.
109-
% Read it's documentation to find out how it operates.
110114
%
111-
% TODO: Remove code duplication
115+
%
116+
%
117+
%
118+
%
112119
ugoal_expansion(if_(If_1, Then_0, Else_0), Goal_0) :-
113-
nonvar(If_1), If_1 = (X = Y),
114-
goal_expanded(call(Then_0), Thenx_0),
115-
goal_expanded(call(Else_0), Elsex_0),
116-
!,
117-
+ write('% =\n'),
118-
Goal_0 =
119-
( X \= Y -> Elsex_0
120-
; X == Y -> Thenx_0
121-
; X = Y, Thenx_0
122-
; dif(X,Y), Elsex_0
123-
).
124-
ugoal_expansion(if_(If_1, Then_0, Else_0), Goal) :-
125-
nonvar(If_1), If_1 = dif(X, Y),
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)) ),
126124
goal_expanded(call(Then_0), Thenx_0),
127125
goal_expanded(call(Else_0), Elsex_0),
128126
!,
129-
+ write('% ≠\n'),
130-
Goal =
131-
( X \= Y -> Thenx_0
132-
; X == Y -> Elsex_0
133-
; X = Y, Elsex_0
134-
; dif(X,Y), Thenx_0
127+
Goal_0 =
128+
( X \= Y -> Elsex_0
129+
; X == Y -> Thenx_0
130+
; X = Y, Thenx_0
131+
; dif(X,Y), Elsex_0
135132
).
133+
% if_((A_1;B_1), Then_0, Else_0)
134+
% => if_(A_1, Then_0, if_(B_1, Then_0, Else_0))
136135
ugoal_expansion(if_(If_1, Then_0, Else_0), Goal) :-
137-
subsumes_term((A_1;B_1), If_1),
138-
(A_1;B_1) = If_1,
139-
!,
140-
+ write('% ;\n'),
141-
Goal = if_(A_1, Then_0, if_(B_1, Then_0, Else_0)).
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)).
142142
ugoal_expansion(if_(If_1, Then_0, Else_0), Goal_0) :-
143-
subsumes_term((A_1,B_1), If_1),
144-
(A_1,B_1) = If_1,
145-
!,
146-
+ write('% ,\n'),
147-
Goal_0 = if_(A_1, if_(B_1, Then_0, Else_0), Else_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).
148149
ugoal_expansion(if_(If_1, Then_0, Else_0), Goal_0) :-
149-
+ write('% _\n'),
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-
; throw(error(instantiation_error,_))
159-
)
160-
).
161-
162-
:- meta_predicate(if_(1, 0, 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+
%
163219

164220
if_(If_1, Then_0, Else_0) :-
165-
call(If_1, T),
166-
( T == true -> call(Then_0)
167-
; T == false -> call(Else_0)
168-
; nonvar(T) -> throw(error(type_error(boolean, T), _))
169-
; throw(error(instantiation_error, _))
170-
).
171-
172-
=(X, Y, T) :-
173-
( X == Y -> T = true
174-
; X \= Y -> T = false
175-
; T = true, X = Y
176-
; T = false, dif(X, Y)
177-
).
178-
179-
dif(X, Y, T) :-
180-
=(X, Y, NT),
181-
non(NT, T).
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+
).
182228

183-
non(true, false).
184-
non(false, true).
185229

186-
:- meta_predicate(tfilter(2, ?, ?)).
230+
tfilter(C_2, Es, Fs) :-
231+
i_tfilter(Es, C_2, Fs).
187232

188-
tfilter(_, [], []).
189-
tfilter(C_2, [E|Es], Fs0) :-
233+
i_tfilter([], _, []).
234+
i_tfilter([E|Es], C_2, Fs0) :-
190235
if_(call(C_2, E), Fs0 = [E|Fs], Fs0 = Fs),
191-
tfilter(C_2, Es, Fs).
192-
193-
:- meta_predicate(tpartition(2, ?, ?, ?)).
236+
i_tfilter(Es, C_2, Fs).
194237

195238
tpartition(P_2, Xs, Ts, Fs) :-
196239
i_tpartition(Xs, P_2, Ts, Fs).
@@ -202,17 +245,26 @@
202245
, ( Fs0 = [X|Fs], Ts0 = Ts ) ),
203246
i_tpartition(Xs, P_2, Ts, Fs).
204247

205-
:- 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+
).
206255

207-
','(A_1, B_1, T) :-
208-
if_(A_1, call(B_1, T), T = false).
256+
dif(X, Y, T) :-
257+
=(X, Y, NT),
258+
non(NT, T).
209259

210-
:- meta_predicate(';'(1, 1, ?)).
260+
non(true, false).
261+
non(false, true).
211262

212-
';'(A_1, B_1, T) :-
213-
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).
214265

215-
:- meta_predicate(cond_t(1, 0, ?)).
266+
;(A_1, B_1, T) :-
267+
if_(A_1, T = true, call(B_1, T)).
216268

217269
cond_t(If_1, Then_0, T) :-
218270
if_(If_1, ( Then_0, T = true ), T = false ).
@@ -224,13 +276,9 @@
224276
i_memberd_t([X|Xs], E, T) :-
225277
if_( X = E, T = true, i_memberd_t(Xs, E, T) ).
226278

227-
:- meta_predicate(tmember(2, ?)).
228-
229279
tmember(P_2, [X|Xs]) :-
230280
if_( call(P_2, X), true, tmember(P_2, Xs) ).
231281

232-
:- meta_predicate(tmember_t(2, ?, ?)).
233-
234282
tmember_t(_P_2, [], false).
235283
tmember_t(P_2, [X|Xs], T) :-
236284
if_( call(P_2, X), T = true, tmember_t(P_2, Xs, T) ).

0 commit comments

Comments
 (0)