1:- module(onepointfour_basics_checks,
2 [
3 check_that/2
4 ,check_that/3
5 ,check_that/4
6 ,check_that/5
7 ,check_that/6
8 ,check_that/7
9 ]). 10
11:- use_module(library(yall)). 12:- use_module(library(apply)). 13:- use_module(library(apply_macros)). 14:- use_module(library('onepointfour_basics/dict_settings.pl')). 15:- use_module(library('onepointfour_basics/checks/print_error_message.pl')). 16:- use_module(library('onepointfour_basics/checks/throwers.pl')). 17:- use_module(library('onepointfour_basics/checks/wellformed.pl')). 18
42
43
60
71
74
75check_that(X,[]) :-
76 !,
77 check_that_1(X,[],_,_{}).
78check_that(X,[C|Cs]) :-
79 !,
80 check_that_1(X,[C|Cs],_,_{}).
81
84
85check_that(X,C1) :-
86 !,
87 check_that_1(X,[C1],_,_{}).
88
91
92check_that(X,[],Tuned) :-
93 \+ is_dict(Tuned),
94 !,
95 check_that_1(X,[],Tuned,_{}).
96check_that(X,[C|Cs],Tuned) :-
97 \+ is_dict(Tuned),
98 !,
99 check_that_1(X,[C|Cs],Tuned,_{}).
100check_that(X,[],SettingsDict) :-
101 is_dict(SettingsDict),
102 !,
103 check_that_1(X,[],_,SettingsDict).
104check_that(X,[C|Cs],SettingsDict) :-
105 is_dict(SettingsDict),
106 !,
107 check_that_1(X,[C|Cs],_,SettingsDict).
108
110
111check_that(X,C1,C2) :-
112 not_soft_hard(C2),
113 \+ is_dict(C2),
114 !,
115 check_that_1(X,[C1,C2],_,_{}).
116check_that(X,C1,Tuned) :-
117 soft_hard(Tuned),
118 !,
119 check_that_1(X,[C1],Tuned,_{}).
120check_that(X,C1,SettingsDict) :-
121 is_dict(SettingsDict),
122 !,
123 check_that_1(X,[C1],_,SettingsDict).
124check_that(A1,A2,A3) :-
125 throw_2(unmatched_call,"no matching check_that/3",check_that(A1,A2,A3)).
126
128
129check_that(X,C1,C2,C3) :-
130 not_soft_hard(C3),
131 \+ is_dict(C3),
132 !,
133 check_that_1(X,[C1,C2,C3],_,_{}).
134check_that(X,C1,C2,Tuned) :-
135 soft_hard(Tuned),
136 !,
137 check_that_1(X,[C1,C2],Tuned,_{}).
138check_that(X,C1,C2,SettingsDict) :-
139 is_dict(SettingsDict),
140 !,
141 check_that_1(X,[C1,C2],_,SettingsDict).
142check_that(A1,A2,A3,A4) :-
143 throw_2(unmatched_call,"no matching check_that/4",check_that(A1,A2,A3,A4)).
144
146
147check_that(X,C1,C2,C3,C4) :-
148 not_soft_hard(C4),
149 \+ is_dict(C4),
150 !,
151 check_that_1(X,[C1,C2,C3,C4],_,_{}).
152check_that(X,C1,C2,C3,Tuned) :-
153 soft_hard(Tuned),
154 !,
155 check_that_1(X,[C1,C2,C3],Tuned,_{}).
156check_that(X,C1,C2,C3,SettingsDict) :-
157 is_dict(SettingsDict),
158 !,
159 check_that_1(X,[C1,C2,C3],_,SettingsDict).
160check_that(A1,A2,A3,A4,A5) :-
161 throw_2(unmatched_call,"no matching check_that/5",check_that(A1,A2,A3,A4,A5)).
162
164
165check_that(X,C1,C2,C3,C4,C5) :-
166 not_soft_hard(C5),
167 \+ is_dict(C5),
168 !,
169 check_that_1(X,[C1,C2,C3,C4,C5],_,_{}).
170check_that(X,C1,C2,C3,C4,Tuned) :-
171 soft_hard(Tuned),
172 !,
173 check_that_1(X,[C1,C2,C3,C4],Tuned,_{}).
174check_that(X,C1,C2,C3,C4,SettingsDict) :-
175 is_dict(SettingsDict),
176 !,
177 check_that_1(X,[C1,C2,C3,C4],_,SettingsDict).
178check_that(A1,A2,A3,A4,A5,A6) :-
179 throw_2(unmatched_call,"no matching check_that/6",check_that(A1,A2,A3,A4,A5,A6)).
180
182
183check_that(X,C1,C2,C3,C4,C5,C6) :-
184 not_soft_hard(C6),
185 \+ is_dict(C6),
186 !,
187 check_that_1(X,[C1,C2,C3,C4,C5,C6],_,_{}).
188check_that(X,C1,C2,C3,C4,C5,Tuned) :-
189 soft_hard(Tuned),
190 !,
191 check_that_1(X,[C1,C2,C3,C4,C5],Tuned,_{}).
192check_that(X,C1,C2,C3,C4,C5,SettingsDict) :-
193 is_dict(SettingsDict),
194 !,
195 check_that_1(X,[C1,C2,C3,C4,C5],_,SettingsDict).
196check_that(A1,A2,A3,A4,A5,A6,A7) :-
197 throw_2(unmatched_call,"no matching check_that/7",check_that(A1,A2,A3,A4,A5,A6,A7)).
198
200
201get_tuned(SettingsDict,Tuned) :-
202 default_tuned(DefaultTuned),
203 get_setting(SettingsDict,tuned,Tuned,DefaultTuned),
204 (soft_hard(Tuned)
205 ->
206 true
207 ;
208 throw_2(domain,"Expected either 'hard' or 'soft' as value of key 'tuned' in the settings dict",Tuned)).
209
210not_soft_hard(P) :- P \== soft, P \== hard.
211soft_hard(P) :- P == soft; P == hard.
212
213 216
229
230default_tuned(hard).
231wellformed_check.
232
233check_that_1(X,Conditions,Tuned,SettingsDict) :-
234 235 236 237 238 (
239 wellformed_check
240 ->
241 no_var_in_list_or_throw(Conditions),
242 wellformed_conds_or_throw(Conditions,X)
243 ;
244 true
245 ),
246 tag_var(Tuned,TaggedTunedFromArg),
247 tag_tuned_from_dict(SettingsDict,TaggedTunedFromDict),
248 determine_tuned(TaggedTunedFromArg,TaggedTunedFromDict,Tuned2),
249 !,
250 check_that_2(Conditions,X,Tuned2,SettingsDict).
251
252determine_tuned(var(_FromArg) , var(_FromDict) , Default) :-
253 default_tuned(Default).
254determine_tuned(var(_FromArg) , nonvar(hard) , hard).
255determine_tuned(var(_FromArg) , nonvar(soft) , soft).
256determine_tuned(var(_FromArg) , nonvar(X) , Default) :-
257 default_tuned(Default),
258 format(user_error,"Unknown 'tuned' value from settings dict: ~q. Choosing default: ~q.~n",[X,Default]).
259determine_tuned(nonvar(hard) , _ , hard).
260determine_tuned(nonvar(soft) , _ , soft).
261determine_tuned(nonvar(X) , _ , Default) :-
262 default_tuned(Default),
263 format(user_error,"Unknown 'tuned' value from argument: ~q. Choosing default: ~q.~n",[X,Default]).
264
265tag_var(X,var(X)) :- var(X),!.
266tag_var(X,nonvar(X)).
267
268tag_tuned_from_dict(SettingsDict,Tagged) :-
269 assertion(is_dict(SettingsDict)),
270 (get_dict(tuned,SettingsDict,InDict)
271 ->
272 tag_var(InDict,Tagged)
273 ;
274 Tagged=var(_)).
275
276no_var_in_list_or_throw(Conditions) :-
277 no_var_in_list(Conditions)
278 ->
279 true
280 ;
281 throw_2(syntax,"unbound variable in conditions list",Conditions).
282
283no_var_in_list([C|More]) :-
284 nonvar(C),
285 no_var_in_list(More).
286no_var_in_list([]).
287
303
304check_that_2([Condition|More],X,Tuned,Dict) :-
305 assertion(member(Tuned,[hard,soft])),
306 exists_cond_or_throw(Condition), 307 check_that_3(Condition,X,Tuned,Outcome,Dict), 308 !, 309 outcome_branching(Outcome,Condition,More,X,Tuned,Dict). 310check_that_2([],_,_,_).
311
312outcome_branching(break,_,_,_,_,_) :- !.
313outcome_branching(done,_,_,_,_,_) :- !.
314outcome_branching(fail,_,_,_,_,_) :- !,fail.
315outcome_branching(next,_,More,X,Tuned,Dict) :- !,check_that_2(More,X,Tuned,Dict).
316outcome_branching(Outcome,Condition,_,_,_,_) :- throw_2(unknown_outcome,"bug: condition yields unknown outcome",[Condition,Outcome]).
317
318check_that_3(break(Check),X,_Tuned,Outcome,Dict) :-
319 eval(Check,X,soft,hard,Dict) 320 ->
321 Outcome = break
322 ;
323 Outcome = next.
324check_that_3(smooth(Check),X,_Tuned,Outcome,Dict) :-
325 eval(Check,X,soft,soft,Dict) 326 ->
327 Outcome = next
328 ;
329 Outcome = fail.
330check_that_3(soft(Check),X,_Tuned,Outcome,Dict) :-
331 eval(Check,X,soft,hard,Dict) 332 ->
333 Outcome = next
334 ;
335 Outcome = fail.
336check_that_3(tuned(Check),X,Tuned,Outcome,Dict) :-
337 eval(Check,X,Tuned,hard,Dict) 338 ->
339 Outcome = next
340 ;
341 Outcome = fail.
342check_that_3(hard(Check),X,_,Outcome,Dict) :-
343 eval(Check,X,hard,hard,Dict) 344 ->
345 Outcome = next
346 ;
347 throw_2(hard_check_fails,"a 'hard' check should throw but instead just fails",Check).
348check_that_3([],_,_,_,done,_).
349
354
355precondition_X_must_be_instantiated(X,Context,Tuned,Dict) :-
356 nonvar(X)
357 ->
358 true
359 ;
360 throw_or_fail(instantiation,X,Tuned,be("instantiated",Context),Dict).
361
362precondition_X_must_be_list(X,Context,Tuned,Dict) :-
363 is_proper_list(X)
364 ->
365 true
366 ;
367 throw_or_fail(type,X,Tuned,be("List",Context),Dict).
368
369precondition_X_must_be_dict(X,Context,Tuned,Dict) :-
370 is_dict(X)
371 ->
372 true
373 ;
374 throw_or_fail(type,X,Tuned,be("Dict",Context),Dict).
375
378
379precondition_X_must_be_atomic(X,Context,Tuned,Dict) :-
380 atomic(X)
381 ->
382 true
383 ;
384 throw_or_fail(type,X,Tuned,be("atomic",Context),Dict).
385
387
388precondition_X_must_be_instantiated_enough_to_decide_whether_cyclic(X,Tuned,Dict) :-
389 var(X),
390 !,
391 throw_or_fail(instantiation,X,Tuned,be("nonvar","Can't say anything about cyclic-ness."),Dict).
392precondition_X_must_be_instantiated_enough_to_decide_whether_cyclic(X,Tuned,Dict) :-
393 \+ground(X),
394 acyclic_term(X),
395 !,
396 throw_or_fail(instantiation,X,Tuned,be("nonground and cyclic","Can't say anything about cyclic-ness."),Dict).
397precondition_X_must_be_instantiated_enough_to_decide_whether_cyclic(_,_,_).
398
404
405just_an_inty(X,Tuned,TP,Dict) :-
406 precondition_X_must_be_instantiated(X,"inty",TP,Dict),
407 ((integer(X);inty_float(X))
408 ->
409 true
410 ;
411 throw_or_fail(type(int_or_float),X,Tuned,"inty",Dict)).
412
418
419inty_float(X) :-
420 float(X),
421 X =\= -1.0Inf,
422 X =\= +1.0Inf,
423 round(X)=:=X.
424
428
429is_proper_list(L) :-
430 is_list(L).
431
436
437eval(true,_,_,_,_).
438eval(false,_,_,_,_).
439eval(fail,_,_,_,_).
440
441eval(var,X,Tuned,_TP,Dict) :-
442 var(X)
443 ->
444 true
445 ;
446 throw_or_fail(uninstantiation,X,Tuned,"var",Dict).
447
448eval(nonvar,X,Tuned,_TP,Dict) :-
449 nonvar(X)
450 ->
451 true
452 ;
453 throw_or_fail(instantiation,X,Tuned,"nonvar",Dict).
454
455eval(ground,X,Tuned,_TP,Dict) :-
456 ground(X)
457 ->
458 true
459 ;
460 throw_or_fail(domain,X,Tuned,"ground",Dict).
461
462eval(nonground,X,Tuned,_TP,Dict) :-
463 \+ground(X)
464 ->
465 true
466 ;
467 throw_or_fail(domain,X,Tuned,"nonground",Dict).
468
469eval(atom,X,Tuned,TP,Dict) :-
470 precondition_X_must_be_instantiated(X,"atom",TP,Dict),
471 (atom(X)
472 ->
473 true
474 ;
475 throw_or_fail(type,X,Tuned,"atom",Dict)).
476
477eval(symbol,X,Tuned,TP,Dict) :-
478 eval(atom,X,Tuned,TP,Dict).
479
480eval(atomic,X,Tuned,TP,Dict) :-
481 precondition_X_must_be_instantiated(X,"atomic",TP,Dict),
482 (atomic(X)
483 ->
484 true
485 ;
486 throw_or_fail(type,X,Tuned,"atomic",Dict)).
487
488eval(constant,X,Tuned,TP,Dict) :-
489 eval(atomic,X,Tuned,TP,Dict).
490
491eval(compound,X,Tuned,TP,Dict) :-
492 precondition_X_must_be_instantiated(X,"compound",TP,Dict),
493 (compound(X)
494 ->
495 true
496 ;
497 throw_or_fail(type,X,Tuned,"compound",Dict)).
498
499eval(boolean,X,Tuned,TP,Dict) :-
500 eval(atom,X,Tuned,TP,Dict),
501 ((X==true;X==false)
502 ->
503 true
504 ;
505 throw_or_fail(domain,X,Tuned,"boolean",Dict)).
506
507eval(pair,X,Tuned,TP,Dict) :-
508 eval(compound,X,Tuned,TP,Dict),
509 (X = -(_,_)
510 ->
511 true
512 ;
513 throw_or_fail(domain,X,Tuned,"pair",Dict)).
514
515eval(string,X,Tuned,TP,Dict) :-
516 precondition_X_must_be_instantiated(X,"string",TP,Dict),
517 (string(X)
518 ->
519 true
520 ;
521 throw_or_fail(type,X,Tuned,"string",Dict)).
522
523eval(stringy,X,Tuned,TP,Dict) :-
524 precondition_X_must_be_instantiated(X,"stringy",TP,Dict),
525 ((atom(X);string(X))
526 ->
527 true
528 ;
529 throw_or_fail(type,X,Tuned,"stringy",Dict)).
530
531eval(nonempty_stringy,X,Tuned,TP,Dict) :-
532 eval(stringy,X,Tuned,TP,Dict),
533 ((X\=='',X\== "")
534 ->
535 true
536 ;
537 throw_or_fail(domain,X,Tuned,"nonempty stringy",Dict)).
538
539eval(char,X,Tuned,TP,Dict) :-
540 eval(atom,X,Tuned,TP,Dict),
541 542 543 (atom_length(X,1)
544 ->
545 true
546 ;
547 throw_or_fail(domain,X,Tuned,"char",Dict)).
548
549eval(code,X,Tuned,TP,Dict) :-
550 eval(integer,X,Tuned,TP,Dict),
551 ((0=<X,X=<0x10FFFF)
552 ->
553 true
554 ;
555 throw_or_fail(domain,X,Tuned,"code",Dict)).
556
557eval(chary,X,Tuned,TP,Dict) :-
558 precondition_X_must_be_instantiated(X,"chary",TP,Dict),
559 (integer(X)
560 ->
561 ((0=<X,X=<0x10FFFF)
562 ->
563 true
564 ;
565 throw_or_fail(domain,X,Tuned,"code",Dict))
566 ;
567 atom(X)
568 ->
569 (atom_length(X,1)
570 ->
571 true
572 ;
573 throw_or_fail(domain,X,Tuned,"char",Dict))
574 ;
575 throw_or_fail(type,X,Tuned,"chary",Dict)).
576
577eval(number,X,Tuned,TP,Dict) :-
578 precondition_X_must_be_instantiated(X,"number",TP,Dict),
579 (number(X)
580 ->
581 true
582 ;
583 throw_or_fail(type,X,Tuned,"number",Dict)).
584
585eval(float,X,Tuned,TP,Dict) :-
586 precondition_X_must_be_instantiated(X,"float",TP,Dict),
587 (float(X)
588 ->
589 true
590 ;
591 throw_or_fail(type,X,Tuned,"float",Dict)).
592
593eval(int,X,Tuned,TP,Dict) :-
594 precondition_X_must_be_instantiated(X,"integer",TP,Dict),
595 (integer(X)
596 ->
597 true
598 ;
599 throw_or_fail(type,X,Tuned,"integer",Dict)).
600
601eval(integer,X,Tuned,TP,Dict) :-
602 eval(int,X,Tuned,TP,Dict).
603
604eval(rational,X,Tuned,TP,Dict) :-
605 precondition_X_must_be_instantiated(X,"rational",TP,Dict),
606 (rational(X)
607 ->
608 true
609 ;
610 throw_or_fail(type,X,Tuned,"rational",Dict)).
611
612eval(nonint_rational,X,Tuned,TP,Dict) :-
613 precondition_X_must_be_instantiated(X,"nonint_rational",TP,Dict),
614 (rational(X)
615 ->
616 true
617 ;
618 throw_or_fail(type,X,Tuned,"nonint_rational",Dict)),
619 (integer(X)
620 ->
621 throw_or_fail(domain,X,Tuned,"nonint_rational",Dict)
622 ;
623 true).
624
625eval(proper_rational,X,Tuned,TP,Dict) :-
626 eval(nonint_rational,X,Tuned,TP,Dict).
627
628eval(negnum,X,Tuned,TP,Dict) :-
629 eval(number,X,Tuned,TP,Dict),
630 ((X < 0)
631 ->
632 true
633 ;
634 throw_or_fail(domain,X,Tuned,"strictly negative number",Dict)).
635
636eval(negnumber,X,Tuned,TP,Dict) :-
637 eval(negnum,X,Tuned,TP,Dict).
638
639eval(posnum,X,Tuned,TP,Dict) :-
640 eval(number,X,Tuned,TP,Dict),
641 ((X > 0)
642 ->
643 true
644 ;
645 throw_or_fail(domain,X,Tuned,"strictly positive number",Dict)).
646
647eval(posnumber,X,Tuned,TP,Dict) :-
648 eval(posnum,X,Tuned,TP,Dict).
649
650eval(neg0num,X,Tuned,TP,Dict) :-
651 eval(number,X,Tuned,TP,Dict),
652 ((X =< 0)
653 ->
654 true
655 ;
656 throw_or_fail(domain,X,Tuned,"number that is =< 0",Dict)).
657
658eval(neg0number,X,Tuned,TP,Dict) :-
659 eval(neg0num,X,Tuned,TP,Dict).
660
661eval(pos0num,X,Tuned,TP,Dict) :-
662 eval(number,X,Tuned,TP,Dict),
663 ((X >= 0)
664 ->
665 true
666 ;
667 throw_or_fail(domain,X,Tuned,"number that is >= 0",Dict)).
668
669eval(pos0number,X,Tuned,TP,Dict) :-
670 eval(pos0num,X,Tuned,TP,Dict).
671
672eval(non0num,X,Tuned,TP,Dict) :-
673 eval(number,X,Tuned,TP,Dict),
674 ((X =\= 0)
675 ->
676 true
677 ;
678 throw_or_fail(domain,X,Tuned,"number that is not 0",Dict)).
679
680eval(non0number,X,Tuned,TP,Dict) :-
681 eval(non0num,X,Tuned,TP,Dict).
682
683eval(float_not_nan,X,Tuned,TP,Dict) :-
684 eval(float,X,Tuned,TP,Dict),
685 ((NaN is nan,X \== NaN) 686 ->
687 true
688 ;
689 throw_or_fail(domain,X,Tuned,"float that is not NaN",Dict)).
690
691eval(float_not_inf,X,Tuned,TP,Dict) :-
692 eval(float,X,Tuned,TP,Dict),
693 ((X =\= -1.0Inf,X =\= +1.0Inf)
694 ->
695 true
696 ;
697 throw_or_fail(domain,X,Tuned,"float that is not positive or negative infinity",Dict)).
698
699eval(float_not_neginf,X,Tuned,TP,Dict) :-
700 eval(float,X,Tuned,TP,Dict),
701 ((X =\= -1.0Inf)
702 ->
703 true
704 ;
705 throw_or_fail(domain,X,Tuned,"float that is not negative infinity",Dict)).
706
707eval(float_not_posinf,X,Tuned,TP,Dict) :-
708 eval(float,X,Tuned,TP,Dict),
709 ((X =\= +1.0Inf)
710 ->
711 true
712 ;
713 throw_or_fail(domain,X,Tuned,"float that is not positive infinity",Dict)).
714
715eval(negint,X,Tuned,TP,Dict) :-
716 eval(int,X,Tuned,TP,Dict),
717 ((X<0)
718 ->
719 true
720 ;
721 throw_or_fail(domain,X,Tuned,"strictly negative integer",Dict)).
722
723eval(negative_integer,X,Tuned,TP,Dict) :-
724 eval(negint,X,Tuned,TP,Dict).
725
726eval(posint,X,Tuned,TP,Dict) :-
727 eval(int,X,Tuned,TP,Dict),
728 ((X>0)
729 ->
730 true
731 ;
732 throw_or_fail(domain,X,Tuned,"strictly positive integer",Dict)).
733
734eval(positive_integer,X,Tuned,TP,Dict) :-
735 eval(posint,X,Tuned,TP,Dict).
736
737eval(neg0int,X,Tuned,TP,Dict) :-
738 eval(int,X,Tuned,TP,Dict),
739 ((X =< 0)
740 ->
741 true
742 ;
743 throw_or_fail(domain,X,Tuned,"integer that is =< 0",Dict)).
744
745eval(pos0int,X,Tuned,TP,Dict) :-
746 eval(int,X,Tuned,TP,Dict),
747 ((X >= 0)
748 ->
749 true
750 ;
751 throw_or_fail(domain,X,Tuned,"integer that is >= 0",Dict)).
752
753eval(nonneg,X,Tuned,TP,Dict) :-
754 eval(pos0int,X,Tuned,TP,Dict).
755
756eval(inty,X,Tuned,TP,Dict) :-
757 just_an_inty(X,Tuned,TP,Dict).
758
759eval(neginty,X,Tuned,TP,Dict) :-
760 eval(inty,X,Tuned,TP,Dict),
761 (((integer(X),X<0);(float(X),X<0.0))
762 ->
763 true
764 ;
765 throw_or_fail(domain,X,Tuned,"strictly negative inty",Dict)).
766
767eval(posinty,X,Tuned,TP,Dict) :-
768 eval(inty,X,Tuned,TP,Dict),
769 (((integer(X),X>0);(float(X),X>0.0))
770 ->
771 true
772 ;
773 throw_or_fail(domain,X,Tuned,"strictly positive inty",Dict)).
774
775eval(neg0inty,X,Tuned,TP,Dict) :-
776 eval(inty,X,Tuned,TP,Dict),
777 (((integer(X),X=<0);(float(X),X=<0.0))
778 ->
779 true
780 ;
781 throw_or_fail(domain,X,Tuned,"inty that is =< 0",Dict)).
782
783eval(pos0inty,X,Tuned,TP,Dict) :-
784 eval(inty,X,Tuned,TP,Dict),
785 (((integer(X),X>=0);(float(X),X>=0.0))
786 ->
787 true
788 ;
789 throw_or_fail(domain,X,Tuned,"inty that is >= 0",Dict)).
790
791eval(negfloat,X,Tuned,TP,Dict) :-
792 eval(float_not_nan,X,Tuned,TP,Dict),
793 (X<0.0
794 ->
795 true
796 ;
797 throw_or_fail(domain,X,Tuned,"strictly negative float",Dict)).
798
799eval(posfloat,X,Tuned,TP,Dict) :-
800 eval(float_not_nan,X,Tuned,TP,Dict),
801 (X>0.0
802 ->
803 true
804 ;
805 throw_or_fail(domain,X,Tuned,"strictly positive float",Dict)).
806
807eval(neg0float,X,Tuned,TP,Dict) :-
808 eval(float_not_nan,X,Tuned,TP,Dict),
809 (X=<0.0
810 ->
811 true
812 ;
813 throw_or_fail(domain,X,Tuned,"float that is =< 0",Dict)).
814
815eval(pos0float,X,Tuned,TP,Dict) :-
816 eval(float_not_nan,X,Tuned,TP,Dict),
817 (X>=0.0
818 ->
819 true
820 ;
821 throw_or_fail(domain,X,Tuned,"float that is >= 0",Dict)).
822
823eval(list,X,Tuned,TP,Dict) :-
824 precondition_X_must_be_instantiated(X,"list",TP,Dict),
825 (is_proper_list(X)
826 ->
827 true
828 ;
829 throw_or_fail(type,X,Tuned,"proper list",Dict)).
830
831eval(proper_list,X,Tuned,TP,Dict) :-
832 eval(list,X,Tuned,TP,Dict).
833
834eval(nonempty_list,X,Tuned,TP,Dict) :-
835 eval(list,X,Tuned,TP,Dict),
836 (X \== []
837 ->
838 true
839 ;
840 throw_or_fail(domain,X,Tuned,"proper nonempty list",Dict)).
841
842eval(dict,X,Tuned,TP,Dict) :-
843 precondition_X_must_be_instantiated(X,"dict",TP,Dict),
844 (is_dict(X)
845 ->
846 true
847 ;
848 throw_or_fail(type,X,Tuned,"dict",Dict)).
849
850eval(stringy_typeid,X,Tuned,TP,Dict) :-
851 eval(atom,X,Tuned,TP,Dict),
852 ((X==atom;X==string)
853 ->
854 true
855 ;
856 throw_or_fail(domain,X,Tuned,"stringy_typeid",Dict)).
857
858eval(chary_typeid,X,Tuned,TP,Dict) :-
859 eval(atom,X,Tuned,TP,Dict),
860 ((X==char;X==code)
861 ->
862 true
863 ;
864 throw_or_fail(domain,X,Tuned,"chary_typeid",Dict)).
865
866eval(char_list,X,Tuned,TP,Dict) :-
867 precondition_X_must_be_instantiated(X,"char_list",TP,Dict),
868 precondition_X_must_be_list(X,"char_list",Tuned,Dict), 869 forall(member(MX,X),eval(char,MX,Tuned,TP,Dict)). 870
871eval(chars,X,Tuned,TP,Dict) :-
872 eval(char_list,X,Tuned,TP,Dict).
873
874eval(code_list,X,Tuned,TP,Dict) :-
875 precondition_X_must_be_instantiated(X,"code_list",TP,Dict),
876 precondition_X_must_be_list(X,"code_list",Tuned,Dict), 877 forall(member(MX,X),eval(code,MX,Tuned,TP,Dict)). 878
879eval(codes,X,Tuned,TP,Dict) :-
880 eval(code_list,X,Tuned,TP,Dict).
881
882eval(chary_list,X,Tuned,TP,Dict) :-
883 precondition_X_must_be_instantiated(X,"chary_list",TP,Dict),
884 precondition_X_must_be_list(X,"chary_list",Tuned,Dict), 885 eval(forany([chars,codes]),X,Tuned,TP,Dict). 886 887
888eval(charys,X,Tuned,TP,Dict) :-
889 eval(chary_list,X,Tuned,TP,Dict).
890
893
894eval(member([]),X,Tuned,TP,Dict) :-
895 eval_member_with_list([],X,Tuned,TP,Dict).
896eval(member([E|Es]),X,Tuned,TP,Dict) :-
897 !,
898 eval_member_with_list([E|Es],X,Tuned,TP,Dict).
899eval(member(E),X,Tuned,TP,Dict) :-
900 eval_member_with_list([E],X,Tuned,TP,Dict).
901eval(member(E1,E2),X,Tuned,TP,Dict) :-
902 eval_member_with_list([E1,E2],X,Tuned,TP,Dict).
903eval(member(E1,E2,E3),X,Tuned,TP,Dict) :-
904 eval_member_with_list([E1,E2,E3],X,Tuned,TP,Dict).
905eval(member(E1,E2,E3,E4),X,Tuned,TP,Dict) :-
906 eval_member_with_list([E1,E2,E3,E4],X,Tuned,TP,Dict).
907eval(member(E1,E2,E3,E4,E5),X,Tuned,TP,Dict) :-
908 eval_member_with_list([E1,E2,E3,E4,E5],X,Tuned,TP,Dict).
909eval(member(E1,E2,E3,E4,E5,E6),X,Tuned,TP,Dict) :-
910 eval_member_with_list([E1,E2,E3,E4,E5,E6],X,Tuned,TP,Dict).
911eval(member(E1,E2,E3,E4,E5,E6,E7),X,Tuned,TP,Dict) :-
912 eval_member_with_list([E1,E2,E3,E4,E5,E6,E7],X,Tuned,TP,Dict).
913
914eval(dict_has_key(Key),X,Tuned,TP,Dict) :-
915 precondition_X_must_be_instantiated(X,"dict-has-key",TP,Dict),
916 precondition_X_must_be_dict(X,"dict-has-key",TP,Dict),
917 precondition_X_must_be_instantiated(Key,"dict-has-key",TP,Dict),
918 precondition_X_must_be_atomic(Key,"dict-has-key",TP,Dict),
919 (get_dict(Key,X,_)
920 ->
921 true
922 ;
923 throw_or_fail(domain,[dict-X,key-Key],Tuned,"dict-has-key",Dict)). 924
925eval(random(Probability),_,Tuned,_,_) :-
926 maybe(Probability) 927 ->
928 true
929 ;
930 throw_or_fail_for_case_random(Tuned).
931
932eval(fail(Msg),X,Tuned,_TP,Dict) :-
933 throw_or_fail(explicit_fail,X,Tuned,Msg,Dict).
934
935eval(unifies(Z),X,_,_,_) :-
936 \+ \+ (Z = X).
937
938eval(acyclic_now,X,Tuned,_,Dict) :-
939 acyclic_term(X) 940 ->
941 true
942 ;
943 throw_or_fail(domain,X,Tuned,"acyclic_now",Dict). 944
945eval(cyclic_now,X,Tuned,_,Dict) :-
946 cyclic_term(X) 947 ->
948 true
949 ;
950 throw_or_fail(domain,X,Tuned,"cyclic_now",Dict). 951
952eval(acyclic_forever,X,Tuned,_,Dict) :-
953 (ground(X),acyclic_term(X)) 954 ->
955 true
956 ;
957 throw_or_fail(domain,X,Tuned,"acyclic_forever",Dict). 958
959eval(cyclic,X,Tuned,TP,Dict) :-
960 precondition_X_must_be_instantiated_enough_to_decide_whether_cyclic(X,TP,Dict),
961 (cyclic_term(X)
962 ->
963 true
964 ;
965 throw_or_fail(domain,X,Tuned,"cyclic",Dict)). 966
967eval(stream,X,Tuned,TP,Dict) :-
968 precondition_X_must_be_instantiated(X,"stream",TP,Dict),
969 (atom(X)
970 ->
971 (is_stream(X)
972 ->
973 true
974 ;
975 throw_or_fail(domain,X,Tuned,"atom-naming-a-stream",Dict))
976 ;
977 atomic(X)
978 ->
979 (is_stream(X)
980 ->
981 true
982 ;
983 throw_or_fail(domain,X,Tuned,"atomic-designating-a-stream",Dict))
984 ;
985 throw_or_fail(type,X,Tuned,"atom-or-atomic",Dict)).
986
990
991eval(forall(ListOfChecks),X,Tuned,TP,Dict) :-
992 forall_forall_loop(ListOfChecks,X,Tuned,TP,Dict) 993 ->
994 true
995 ;
996 throw_or_fail(forall,checks(ListOfChecks)-item(X),Tuned,"all of the checks succeed for the item",Dict).
997
998eval(forany(ListOfChecks),X,Tuned,TP,Dict) :-
999 forany_forall_loop(ListOfChecks,X,TP,Dict) 1000 ->
1001 true
1002 ;
1003 throw_or_fail(forany,checks(ListOfChecks)-item(X),Tuned,"at least one of the checks succeeds for the item",Dict).
1004
1005eval(fornone(ListOfChecks),X,Tuned,TP,Dict) :-
1006 fornone_forall_loop(ListOfChecks,X,TP,Dict) 1007 ->
1008 true
1009 ;
1010 throw_or_fail(fornone,checks(ListOfChecks)-item(X),Tuned,"none of the checks succeeds for the item",Dict).
1011
1019
1020eval(passall(Check),ListOfX,Tuned,TP,Dict) :-
1021 passall_forall_loop(Check,ListOfX,Tuned,TP,Dict) 1022 ->
1023 true
1024 ;
1025 throw_or_fail(passall,check(Check)-items(ListOfX),Tuned,"all of the items pass the check",Dict).
1026
1027eval(passany(Check),ListOfX,Tuned,TP,Dict) :-
1028 passany_forall_loop(Check,ListOfX,TP,Dict) 1029 ->
1030 true
1031 ;
1032 throw_or_fail(passany,check(Check)-items(ListOfX),Tuned,"at least one of the items passes the check",Dict).
1033
1034eval(passnone(Check),ListOfX,Tuned,TP,Dict) :-
1035 passnone_forall_loop(Check,ListOfX,TP,Dict) 1036 ->
1037 true
1038 ;
1039 throw_or_fail(passnone,check(Check)-items(ListOfX),Tuned,"none of the items passes the check",Dict).
1040
1044
1045eval_member_with_list(ListOfValues,X,Tuned,TP,Dict) :-
1046 precondition_X_must_be_instantiated(X,"list_membership",TP,Dict),
1047 precondition_X_must_be_list(ListOfValues,"list_membership",TP,Dict), 1048 ((\+ \+ member(X,ListOfValues)) 1049 ->
1050 true
1051 ;
1052 throw_or_fail(domain,X,Tuned,"list_membership",Dict)).
1053
1057
1058forall_forall_loop(ListOfChecks,X,Tuned,TP,Dict) :-
1059 1060 1061 1062 eval(proper_list,ListOfChecks,hard,hard,Dict),
1063 forall( 1064 member(Check,ListOfChecks),
1065 eval(Check,X,Tuned,TP,Dict)).
1066
1067forany_forall_loop(ListOfChecks,X,TP,Dict) :-
1068 eval(proper_list,ListOfChecks,hard,hard,Dict),
1069 \+forall( 1070 member(Check,ListOfChecks),
1071 \+eval(Check,X,soft,TP,Dict)). 1072
1073fornone_forall_loop(ListOfChecks,X,TP,Dict) :-
1074 eval(proper_list,ListOfChecks,hard,hard,Dict),
1075 (ListOfChecks == []) 1076 ->
1077 false
1078 ;
1079 forall(
1080 member(Check,ListOfChecks),
1081 \+eval(Check,X,soft,TP,Dict)). 1082
1083passall_forall_loop(Check,ListOfX,Tuned,TP,Dict) :-
1084 1085 1086 1087 eval(proper_list,ListOfX,hard,hard,Dict),
1088 forall( 1089 member(X,ListOfX),
1090 eval(Check,X,Tuned,TP,Dict)).
1091
1092passany_forall_loop(Check,ListOfX,TP,Dict) :-
1093 eval(proper_list,ListOfX,hard,hard,Dict),
1094 \+forall( 1095 member(X,ListOfX),
1096 \+eval(Check,X,soft,TP,Dict)). 1097
1098passnone_forall_loop(Check,ListOfX,TP,Dict) :-
1099 eval(proper_list,ListOfX,hard,hard,Dict),
1100 (ListOfX == []) 1101 ->
1102 false
1103 ;
1104 forall(
1105 member(X,ListOfX),
1106 \+eval(Check,X,soft,TP,Dict)).
A replacement for must/2
check_that/3 and friends: a replacement for the must_be/2 predicate of Prolog. must_be/2 is used to check preconditions on predicate entry, but is not very flexible. Can we improve on that?
The homepage for this module is at
https://github.com/dtonhofer/prolog_code/blob/main/unpacked/onepointfour_basics/README_checks.md
*/