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