-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathpredef.pl
More file actions
223 lines (190 loc) · 8.94 KB
/
Copy pathpredef.pl
File metadata and controls
223 lines (190 loc) · 8.94 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
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
% Copyright (C) 2026 Fred Mesnard <frederic.mesnard@gmail.com>
%
% This file is part of Prolog-mode-analysis.
%
% Prolog-mode-analysis is free software: you can redistribute it and/or
% modify it under the terms of the GNU Lesser General Public License as
% published by the Free Software Foundation, either version 3 of the
% License, or (at your option) any later version.
%
% Prolog-mode-analysis is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
% Lesser General Public License for more details.
%
% You should have received a copy of the GNU Lesser General Public
% License along with this program. If not, see
% <https://www.gnu.org/licenses/>.
:- module(predef,[predef_nat_bool_tc/4,predef/1,predef_iso/1,predef_include/1]).
:- dynamic(predef_include/4).
predef_nat_bool_tc(Predef,Eqns,BoolTerm,TermCond) :-
predef0(Predef,Cs,Bool,TermCond),!,
BoolTerm=Bool,Eqns=Cs.
predef_nat_bool_tc(X,_,_,_) :-
throw(analyzer_exception(predef,unknown_predef(X))).
predef(At) :-
nonvar(At),
functor(At,P,N),
functor(AtP,P,N),
predef0(AtP,_,_,_),!.
predef(At) :-
var(At),
predef0(At,_,_,_).
% predef which are included have priority
predef0(At,N,B,T) :- predef_include(At,N,B,T),!.
predef0(At,N,B,T) :- predef_iso(At,N,B,T).
predef_iso(A) :- predef_iso(A,_,_,_),!.
predef_include(A) :- predef_include(A,_,_,_),!.
% predef_include(Predef, Cs, Bool, TermCond)
predef_include(tab(N), [N=0], N, N). % requires N ground
predef_include(name(X,Y), [X=0,Y>=0], X*Y, X+Y). % like atom_codes/2
predef_include(get(C), [C=0], C, 1). % like get_code/1
predef_include(length(L,N), [L>=0,N=0], N, L+N). % N ground, L not necessarily
% predef_iso(AtPredefProlog,ContraintesEquivNum,ContraintesEquivBool,CondTerm)
% nb: the args of At are always variables, except for '$bool'/1 and '$num'/1
%---------------------------------------------------------------------------------
% Prolog: The Standard, Deransart et al., Springer, p. 261
%----------------------------------------------------------
% all solutions
predef_iso( setof(_,_G,_L), [],1,1). % ((G,false);true)
predef_iso( findall(_,_,_), [],1,1).
predef_iso( bagof(_,_,_), [],1,1).
% arithmetic comparison & evaluation
predef_iso( X is Y, [X=0],X*Y,1).
predef_iso( X > Y, [],X*Y,1).
predef_iso( X >= Y, [],X*Y,1).
predef_iso( X < Y, [],X*Y,1).
predef_iso( X =< Y, [],X*Y,1).
predef_iso( X =:=Y, [],X*Y,1).
predef_iso( X =\=Y, [],X*Y,1).
% atomic term processing
predef_iso( atom_chars(X,Y), [X=0,Y>=0],X*Y,1).
predef_iso( atom_codes(X,Y), [X=0,Y>=0],X*Y,1).
predef_iso( atom_concat(X,Y,Z), [X=0,Y=0,Z=0],X*Y*Z,1).
predef_iso( atom_length(X,L), [X=0,L>=0],X*L,1).
predef_iso( char_code(Char,Code), [Char=0,Code=0],Char*Code,1).
predef_iso( number_chars(N,Chars), [N=0,Chars>=1],N*Chars,1).
predef_iso( number_codes(N,Codes), [N=0,Codes>=1],N*Codes,1).
predef_iso( sub_atom(A,I,J,K,B), [A=0,B=0,I=0,J=0,K=0],A*B*I*J*K,1).
% byte input/output
predef_iso( get_byte(B), [B=0],B,1).
predef_iso( get_byte(SA,B), [B=0],SA*B,1).
predef_iso( peek_byte(C), [C=0],C,1).
predef_iso( peek_byte(SA,B), [B=0],SA*B,1).
predef_iso( put_byte(B), [B=0],B,1).
predef_iso( put_byte(SA,B), [B=0],SA*B,1).
% char input/output
predef_iso( get_char(C), [C=0],C,1).
predef_iso( get_char(SA,C), [C=0],SA*C,1).
predef_iso( get_code(C), [C=0],C,1).
predef_iso( get_code(SA,C), [C=0],SA*C,1).
predef_iso( peek_char(C), [C=0],C,1).
predef_iso( peek_char(SA,C), [C=0],SA*C,1).
predef_iso( peek_code(C), [C=0],C,1).
predef_iso( peek_code(SA,C), [C=0],SA*C,1).
predef_iso( put_char(C), [C=0],C,1).
predef_iso( put_char(SA,C), [C=0],SA*C,1).
predef_iso( put_code(C), [C=0],C,1).
predef_iso( put_code(SA,C), [C=0],SA*C,1).
predef_iso( nl, [],1,1).
predef_iso( nl(SA), [],SA,1).
% clause retrieval & information
predef_iso( clause(_,_), [],1,1).
predef_iso( current_predicate(PI), [PI=1],PI,1).
% clause creation & destruction
predef_iso( abolish(PI), [],PI,1).
predef_iso( asserta(_), [],1,1).
predef_iso( assertz(_), [],1,1).
predef_iso( retract(_), [],1,1).
% flag updates
predef_iso( current_prolog_flag(_,_), [],1,1).
predef_iso( set_prolog_flag(_,_), [],1,1).
% logic & control
predef_iso( !, [0=0],1,1).
predef_iso( true, [],1,1).
predef_iso( fail, [0=1],0,1).
predef_iso( repeat, [],1,0).
predef_iso( call(_), [],1,1).
predef_iso( \+(_), [],1,1).
predef_iso( halt, [0=1],0,1).
predef_iso( halt(_), [0=1],0,1).
predef_iso( once(_), [],1,0).
predef_iso( ','(_,_), [],1,0).
predef_iso( ';'(_,_), [],1,0).
predef_iso( '->'(_,_), [],1,0).
predef_iso( catch(_,_,_), [],1,0).
predef_iso( throw(_), [0=1],0,0).
% stream selection & control
predef_iso( at_end_of_stream, [],1,1).
predef_iso( at_end_of_stream(_), [],1,1).
predef_iso( close(_), [],1,1).
predef_iso( current_input(_), [],1,1).
predef_iso( current_input(_,_), [],1,1).
predef_iso( flush_output, [],1,1).
predef_iso( flush_output(_), [],1,1).
predef_iso( open(_,_,_), [],1,1).
predef_iso( open(_,_,_,_), [],1,1).
predef_iso( set_input(_), [],1,1).
predef_iso( set_output(_), [],1,1).
predef_iso( set_stream_position(_,_), [],1,1).
predef_iso( stream_property(_,_), [],1,1).
% term comparison
predef_iso( X == Y, [X=Y],(X=:=Y),1).
predef_iso( _ \== _, [],1,1).
predef_iso( _ @< _, [],1,1).
predef_iso( _ @=< _, [],1,1).
predef_iso( _ @> _, [],1,1).
predef_iso( _ @>= _, [],1,1).
% term creation & decomposition
predef_iso( functor(_T,F,N), [F=0,N=0],F*N,1).
predef_iso( arg(N,T,A), [N=0,T >= A+1, A>=0],N*(T =< A),1).
%predef_iso( X =.. Y, [N+X>=Y,Y >=X+1,X>=0],(X =:= Y),1) :- current_prolog_flag(max_arity,N).
predef_iso( X =.. Y, [Y >=0,X>=0],(X =:= Y),1).
predef_iso( copy_term(_X,_Y), [],1,1).
% term unification
predef_iso( X = Y, [X=Y],(X=:=Y),1).
%predef_iso( '\='(_,_), [],1,1). % otherwise a bug on =
predef_iso(unify_with_occurs_check(X,Y), [X=Y],(X=:=Y),1).
% term testing
predef_iso( var(_), [],1,1).
predef_iso( nonvar(_), [],1,1).
predef_iso( compound(X), [X >= 1],1,1).
predef_iso( atomic(X), [X = 0],X,1).
predef_iso( atom(X), [X = 0],X,1).
predef_iso( number(X), [X = 0],X,1).
predef_iso( float(X), [X = 0],X,1).
predef_iso( integer(X), [X = 0],X,1).
% term input/ouput
predef_iso( char_conversion(X,Y), [X=0,Y=0],X*Y,1).
predef_iso( current_char_conversion(X,Y), [X=0,Y=0],X*Y,1).
predef_iso( current_op(_,_,_), [X=0,Y=0,Z=0],X*Y*Z,1).
predef_iso( op(_,_,_), [],1,1).
predef_iso( read(_), [],1,1).
predef_iso( read(_,_), [],1,1).
predef_iso( read_term(_), [],1,1).
predef_iso( read_term(_,_), [],1,1).
predef_iso( write(_), [],1,1).
predef_iso( write(_,_), [],1,1).
predef_iso( write_canonical(_), [],1,1).
predef_iso( write_canonical(_,_), [],1,1).
predef_iso( write_term(_,_), [],1,1).
predef_iso( write_term(_,_,_), [],1,1).
predef_iso( writeq(_), [],1,1).
predef_iso( writeq(_,_), [],1,1).
% Flags (Prolog: The Standard, p. 215--219)
predef_iso(current_prolog_flag(X,Y), [X=0,Y=0],X*Y,1).
predef_iso(set_prolog_flag(X,Y), [X=0,Y=0],X*Y,1).
% Directives (should not appear inside clauses, but this is not checked)
predef_iso(discontiguous(_PI), _,_,_).
predef_iso(dynamic(_PI), _,_,_).
predef_iso(multifile(_PI), _,_,_).
predef_iso(ensure_loaded(_Ptext), _,_,_).
predef_iso(include(_Ptext), _,_,_).
predef_iso(initialization(_G), _,_,_).
%------------------------------------------------------------------------
% internal to the analyzer
predef_iso( '$bool'(X), [],X,1).
predef_iso( '$num'(X), X,1,1).
predef_iso( '$term_cond'(TC), [],1,TC).
predef_iso( '$constraint'(_), [],1,1).
%------------------------------------------------------------------------