34
35:- module(typeprops,
36 [list/1, list/2, tlist/2, nlist/1, nlist/2, goal/2, nnegint/1, pair/1,
37 flt/1, nnegflt/1, posflt/1, num/1, nnegnum/1, posnum/1, atm/1, gnd/1,
38 any/1, gndstr/1, str/1, struct/1, term/1, char/1, atmel/1, keypair/1,
39 sequence/2, negint/1, operator_specifier/1, character_code/1, goal/1,
40 mod_qual/1, mod_qual/2, keylist/1, predname/1, constant/1, linear/1,
41 arithexpression/1, int/1, rat/1, posint/1
42 ]). 43
44:- use_module(library(apply)). 45:- use_module(library(arithmetic)). 46:- use_module(library(occurs)). 47:- use_module(library(neck)). 48:- use_module(library(assertions)). 49:- use_module(library(metaprops)). 50:- use_module(library(static_strip_module)). 51:- init_expansors. 52
53%! int(Int)
54%
55% The type of integers
56
57:- type int/1.
58
59int(X) :-
60 nonvar(X),
61 !,
62 integer(X).
63int(X) :-
64 checkprop_goal(
65 ( between(0, inf, N),
66 give_sign(N, X)
67 )).
68
69:- type posint/1.
70
71posint(X) :-
72 nonvar(X),
73 !,
74 integer(X),
75 X > 0.
76posint(X) :-
77 checkprop_goal(curr_posint(X)).
78
79curr_posint(N) :- between(1, inf, N).
80
81:- type negint/1.
82
83negint(X) :-
84 nonvar(X),
85 !,
86 integer(X),
87 X < 0.
88negint(X) :-
89 checkprop_goal(
90 ( curr_posint(N),
91 X is -N
92 )).
93
94give_sign(0, 0) :- !.
95give_sign(P, P).
96give_sign(P, N) :- N is -P.
97
98:- type nnegint/1.
104nnegint(X) :-
105 nonvar(X),
106 !,
107 integer(X),
108 X >= 0.
109nnegint(N) :-
110 checkprop_goal(between(0, inf, N)).
111
112:- type flt/1.
118flt(X) :-
119 nonvar(X),
120 !,
121 float(X).
122flt(F) :-
123 checkprop_goal(
124 ( nnegfltgen(Q),
125 give_sign(Q, F)
126 )).
127
128:- type nnegflt/1.
129
130nnegflt(X) :-
131 nonvar(X),
132 !,
133 float(X),
134 X >= 0.
135nnegflt(Q) :-
136 checkprop_goal(nnegfltgen(Q)).
137
138nnegfltgen(Q) :-
139 nnegint(X),
140 intfrac1(X, Q).
141
142intfrac1(X, Q) :-
143 ( Q is 1.0*X
144 ; frac(X, Q)
145 ).
146
147:- type posflt/1.
148
149posflt(X) :-
150 nonvar(X),
151 !,
152 float(X),
153 X > 0.
154posflt(Q) :-
155 checkprop_goal(
156 ( curr_posint(X),
157 intfrac1(X, Q)
158 )).
159
160:- type rat/1.
161
162rat(X) :-
163 rational(X),
164 !.
165rat(X) :-
166 checkprop_goal(
167 ( int(A),
168 int(B),
169 X is A rdiv B
170 )).
171
172:- type num/1.
178num(X) :-
179 nonvar(X),
180 !,
181 number(X).
182num(F) :-
183 checkprop_goal(
184 ( nnegnumgen(Q),
185 give_sign(Q, F)
186 )).
187
188:- type nnegnum/1.
189
190nnegnum(X) :-
191 nonvar(X),
192 !,
193 number(X),
194 X >= 0.
195nnegnum(Q) :-
196 checkprop_goal(nnegnumgen(Q)).
197
198nnegnumgen(Q) :-
199 nnegint(X),
200 intfrac2(X, Q).
201
202:- type posnum/1.
203
204posnum(X) :-
205 nonvar(X), !,
206 number(X),
207 X > 0.
208posnum(Q) :-
209 checkprop_goal(
210 ( curr_posint(X),
211 intfrac2(X, Q)
212 )).
213
214intfrac2(X, Q) :-
215 ( Q is X
216 ; Q is 1.0*X
217 ; frac(X, R),
218 ( Q is R
219 ; Q is 1.0*R
220 )
221 ).
222
223frac(X, Q) :-
224 between(2, X, Y),
225 1 =:= gcd(X, Y),
226 ( Q is X rdiv Y
227 ; Q is Y rdiv X
228 ).
229
230:- type atm/1.
236atm(T) :-
237 nonvar(T),
238 !,
239 atom(T).
240atm(A) :-
241 checkprop_goal(
242 ( list(character_code, L),
243 atom_codes(A, L)
244 )).
245
246:- type atmel/1.
252atmel([]).
253atmel(A) :- atm(A).
254
255:- type str/1.
261str(T) :-
262 nonvar(T),
263 !,
264 string(T).
265str(S) :-
266 checkprop_goal(
267 ( list(character_code, L),
268 string_codes(S, L)
269 )).
270
271%! character_code(I)
272%
273% An integer which is a character code
274
275:- type character_code/1.
276
277character_code(I) :-
278 between(0, 255, I),
279 neck.
280
281%! constant(C)
282%
283% An atomic term (an atom, string or a number)
284
285:- type constant/1.
286
287constant([]).
288constant(T) :- atm(T).
289constant(T) :- num(T).
290constant(T) :- str(T).
291
292:- type predname/1.
298predname(P/A) :-
299 atm(P),
300 nnegint(A).
301
302:- type term/1.
308term(_).
309
310:- type list/1.
316list([]).
317list([_|L]) :- list(L).
318
319%! list(:Type, List:list)
320%
321% List is a list of Type
322
323:- type list(1, list).
324:- meta_predicate list(1, ?). 325
326list(Type, List) :- list_(List, Type).
327
328:- prop list_/2.
329list_([], _).
330list_([E|L], T) :-
331 type(T, E),
332 list_(L, T).
333
334:- type pair/1.
335pair(_-_).
336
337:- type keypair/1.
338keypair(_-_).
339
340:- type keylist/1.
341keylist(KL) :- list(keypair, KL).
342
343%! tlist(T, L)
344%
345% L is a list or a value of T's
346
347:- type tlist/2.
348:- meta_predicate tlist(1, ?). 349
350tlist(T, L) :- list(T, L).
351tlist(T, E) :- type(T, E).
352
353%! nlist(T, NL)
354%
355% A nested list of T's
356
357:- type nlist/2.
358:- meta_predicate nlist(1, ?). 359
360nlist(T, X) :- type(T, X).
361nlist(T, L) :- list(nlist(T), L).
362
363%! nlist(NL)
364%
365% A nested list
366
367:- type nlist/1.
368:- meta_predicate nlist(1, ?). 369
370nlist(T) :- term(T).
371nlist(L) :- list(nlist, L).
372
373/* Note: this definition could lead to il-formed lists, like [a|b], that is why
374 * we prefer the definition above
375
376nlist(Type, NList) :- nlist_(NList, Type).
377
378nlist_([], _).
379nlist_([X|Xs], T) :-
380 nlist_(X, T),
381 nlist_(Xs, T).
382nlist_(X, T) :-
383 type(T, X).
384*/
385
386:- type char/1.
387char(A) :- atm(A). % size(A)=1
388
389:- type any/1.
390any(_).
391
392:- type linear/1.
397linear(T) :-
398 term_variables(T, Vars),
399 maplist(occurrs_one(T), Vars).
400
401occurrs_one(T, Var) :- occurrences_of_var(Var, T, 1).
402
403%! sequence(:T, S)
404%
405% S is a sequence of T's
406
407:- type sequence/2.
408
409:- meta_predicate sequence(1, ?). 410
411sequence(T, S) :- sequence_(T, S).
412
413sequence_(E, T) :- type(E, T).
414sequence_((E, S), T) :-
415 type(E, T),
416 sequence_(S, T).
417
418:- type struct/1 # "A compound term".
419
421struct([_|_]):- !.
422struct(T) :- functor(T, _, A), A>0. % compound(T).
423
424:- type gnd/1 # "A ground term".
425
427gnd([]) :- !.
428gnd(T) :-
429 term_variables(T, Vars),
430 list(gnd, Vars).
431
432:- type arithexpression/1.
433
434%! arithexpression(Expr)
435
436% An arithmetic expression
437
438:- type gndstr/1.
439
440gndstr(A) :- gnd(A), struct(A).
441
442arithexpression(X) :- number(X), !. 443arithexpression(X) :- num(X).
444arithexpression(X) :-
445 callable(X),
446 curr_arithmetic_function(X),
447 X =.. [_|Args],
448 list(arithexpression, Args).
449
450curr_arithmetic_function(X) :- current_arithmetic_function(X).
451curr_arithmetic_function(X) :- arithmetic:evaluable(X, _Module).
452
453% BUG: if the trace has all the ports active, we can not use ';'/2 in goal/2
454% and some variables becomes uninstantiated. That is an SWI-Prolog bug but I
455% don't have time to isolate it --EMM
456
457%! goal(:P)
458%
459% P is a defined predicate
460
461:- true prop goal/1.
462:- meta_predicate goal(0). 463goal(Pred) :- goal(0, Pred).
464 % current_predicate(_, M:G).
465
466%! goal(N, :P)
467%
468% P is a defined predicate with N extra arguments
469
470:- true prop goal/2.
471:- meta_predicate goal(+, :). 472goal(N, Pred) :-
473 nnegint(N),
474 goal_2(Pred, N).
475
476goal_2(M:Pred, N) :-
477 var(Pred),
478 !,
479 checkprop_goal(
480 ( ( var(M)
481 ->current_module(CM),
482 current_predicate(CM:F/A),
483 M=CM
484 ; current_module(M),
485 current_predicate(M:F/A)
486 ),
487 A >= N,
488 A1 is A - N,
489 functor(Pred, F, A1)
490 )).
491goal_2(M:Pred, N) :-
492 callable(Pred),
493 functor(Pred, F, A1),
494 A is A1 + N,
495 ( var(M)
496 ->checkprop_goal(
497 ( current_module(CM),
498 current_predicate(CM:F/A),
499 M=CM
500 ))
501 ; current_module(M),
502 current_predicate(M:F/A)
503 ).
504
505:- true prop mod_qual/1.
506:- meta_predicate mod_qual(:). 507mod_qual(M:V) :-
508 static_strip_module(V, M, _, CM),
509 current_module(CM).
510
511:- true prop mod_qual/2.
512:- meta_predicate mod_qual(1, :). 513mod_qual(T, M:V) :-
514 static_strip_module(V, M, C, CM),
515 current_module(CM),
516 with_cv_module(type(T, C), CM).
517
518:- type operator_specifier/1.
519
520operator_specifier(fy).
521operator_specifier(fx).
522operator_specifier(yfx).
523operator_specifier(xfy).
524operator_specifier(xfx).
525operator_specifier(yf).
526operator_specifier(xf)