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 19/* MIT License Follows (https://opensource.org/licenses/MIT) 20 21 Copyright 2021 David Tonhofer <ronerycoder@gluino.name> 22 23 Permission is hereby granted, free of charge, to any person obtaining 24 a copy of this software and associated documentation files 25 (the "Software"), to deal in the Software without restriction, 26 including without limitation the rights to use, copy, modify, merge, 27 publish, distribute, sublicense, and/or sell copies of the Software, 28 and to permit persons to whom the Software is furnished to do so, 29 subject to the following conditions: 30 31 The above copyright notice and this permission notice shall be 32 included in all copies or substantial portions of the Software. 33 34 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, 35 EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 36 MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. 37 IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY 38 CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, 39 TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE 40 SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. 41*/ 42 43 44/* pldoc ==================================================================== */

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

58% Various ways of calling check_that/N, which we distinguish (and unify into a call to 59% check_that_1) by examining the arguments. 60 61% The default stance for "tuned" is "hard", i.e. check failure will cause exceptions rather than just failure. 62% As specific name for the value can be given via the SettingsDict, with key 'name'. This name will be inserted 63% into a generated error message, otherwise the messages in exceptions will be relatively generic. 64% If Conditions is not a list, it is transformed into a list first. 65% Conditions marked "tuned" in the conditions list are influence by the parameter "Tuned": 66% - hard means that condition failure leads to an exception 67% - soft means that condition failure leads to just failure 68% Whether one or the other is preferred depends on the caller's context. 69% The behaviour can be specifically influenced by testing certain subdoamins first, using "break(var)" 70% to unconditionally accept var et.c 71 72% 2 arguments 73% old school: conditions in a list 74 75check_that(X,[]) :- 76 !, 77 check_that_1(X,[],_,_{}). 78check_that(X,[C|Cs]) :- 79 !, 80 check_that_1(X,[C|Cs],_,_{}). 81 82% 2 arguments 83% new school: conditions not in a list 84 85check_that(X,C1) :- 86 !, 87 check_that_1(X,[C1],_,_{}). 88 89% 3 arguments 90% old school: conditions in a list 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 109% 3 arguments, conditions not in a list (ambiguous) 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 127% 4 arguments, conditions not in a list (ambiguous) 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 145% 5 arguments, conditions not in a list (ambiguous) 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 163% 6 arguments, conditions not in a list (ambiguous) 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 181% 7 arguments, conditions not in a list (ambiguous) 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 199% helpers for the above 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 /********************************************* 214 * What lies beneath the exported predicates * 215 *********************************************/ 216 217% --- 218% Two-step process: 219% 1) Verify the syntactic correctness of all conditions. 220% Throw if there is a problems with the syntax. 221% TODO: That should be done during compilation, i.e. using term expansion, because 222% checking the syntax once instead of at every call should really be enough! 223% 2) Evaluate the check tagged by the condition.. 224% 225% For the syntax checks, the code tries to tell the caller _why_ there is a problem, 226% instead of just "failing" with zero information left, so it's a bit unidiomatic, 227% Prolog needs something to handle that more elegantly. 228% --- 229 230default_tuned(hard). 231wellformed_check. 232 233check_that_1(X,Conditions,Tuned,SettingsDict) :- 234 % 235 % ***** TODO: a global variable that says whether this should be called or not **** 236 % ***** (it makes a *fat* difference in performance, but tells the programmer about errors) **** 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 288% --- 289% check_that_2(Conditions,TermToCheck,Tuned,SettingsDict) 290% 291% One we have passed the basic syntactic/well-formedness checks of 292% check_that_1/4, we can proceed to evaluate the checks in-order. 293% Generally this means unpacking the compound term of the check and 294% calling eval/4. 295% 296% In case we find an unknown check, we throw ISO type error in the 297% penultimate clause. If check_that_1/4 indeed performed 298% well-formedness checks, this actually can't happen. 299% 300% The "SettingsDict" may carry: 301% - The name of the TermToCheck for insertion into error messages, under 'name' 302% --- 303 304check_that_2([Condition|More],X,Tuned,Dict) :- 305 assertion(member(Tuned,[hard,soft])), 306 exists_cond_or_throw(Condition), % always succeeds if the syntax check was passed 307 check_that_3(Condition,X,Tuned,Outcome,Dict), % needs no internal cut 308 !, % no need to go back on success 309 outcome_branching(Outcome,Condition,More,X,Tuned,Dict). % recurses 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) % fail for eval, throw for precondition 320 -> 321 Outcome = break 322 ; 323 Outcome = next. 324check_that_3(smooth(Check),X,_Tuned,Outcome,Dict) :- 325 eval(Check,X,soft,soft,Dict) % fail for eval, fail for precondition 326 -> 327 Outcome = next 328 ; 329 Outcome = fail. 330check_that_3(soft(Check),X,_Tuned,Outcome,Dict) :- 331 eval(Check,X,soft,hard,Dict) % fail for eval, throw for precondition 332 -> 333 Outcome = next 334 ; 335 Outcome = fail. 336check_that_3(tuned(Check),X,Tuned,Outcome,Dict) :- 337 eval(Check,X,Tuned,hard,Dict) % tuned for eval, throw for precondition 338 -> 339 Outcome = next 340 ; 341 Outcome = fail. 342check_that_3(hard(Check),X,_,Outcome,Dict) :- 343 eval(Check,X,hard,hard,Dict) % throw for eval, throw for precondition 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 350% --- 351% Special precondition checks: we want to unconditionally throw if X does not have enough 352% information for a meaningful answer, i.e. if we encounter an "instantiation error" 353% --- 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 376% special case precondition: atomic (used to assess dict key) 377% TODO: should really be "integer or atom" 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 386% special case precondition: X must be instantiated enough to positively say whether it is cyclic 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 399% ---- 400% The "type test" for inty terms: accepts an integer 401% or a float that represents an integer. Anything else 402% causes failure to type error. 403% --- 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 413% --- 414% Accept a float that represents an integer 415% round(X)=:=X fails for NaN because NaN =/= NaN, so there is no 416% need to test for NaN separately. 417% --- 418 419inty_float(X) :- 420 float(X), 421 X =\= -1.0Inf, 422 X =\= +1.0Inf, 423 round(X)=:=X. 424 425% --- 426% This one just exists to make code clearer 427% --- 428 429is_proper_list(L) :- 430 is_list(L). 431 432% --- 433% eval(Check,TermToCheck,Tuned,PreconditionTuned,Dict) 434% This predicate needs no internal cuts as a unique decision is taken on arg 1 435% --- 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 % Note that we need to test atom/1 first because atom_length/2 transforms-to-atom! 542 % atom_length/2 may be too wasteful to test for a precise length (?) 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) % arithmetic comparison would fail 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), % Dual traversal, but one is in C, so this may be faster than "unifying" to a single traversal. 869 forall(member(MX,X),eval(char,MX,Tuned,TP,Dict)). % TODO: Open up to get at the index 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), % Dual traversal, but one is in C, so this may be faster than "unifying" to a single traversal. 877 forall(member(MX,X),eval(code,MX,Tuned,TP,Dict)). % TODO: Open up to get at the index 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), % Dual traversal, but one is in C, so this may be faster than "unifying" to a single traversal. 885 eval(forany([chars,codes]),X,Tuned,TP,Dict). % TODO: Open up to get at the index and get better error messages 886 % Simple, but the error is confusing for "check_that([a,2],hard(chary_list))" for example and does not give the index 887 888eval(charys,X,Tuned,TP,Dict) :- 889 eval(chary_list,X,Tuned,TP,Dict). 890 891% These exist so that one does not need to explicity bracket the arguments of member/N, 892% which increases legibility 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)). % domain error sounds right here for "key not in dict" 924 925eval(random(Probability),_,Tuned,_,_) :- 926 maybe(Probability) % throws type error on value not in [0.0,1.0] 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) % never throws 940 -> 941 true 942 ; 943 throw_or_fail(domain,X,Tuned,"acyclic_now",Dict). % is domain right here? 944 945eval(cyclic_now,X,Tuned,_,Dict) :- 946 cyclic_term(X) % never throws 947 -> 948 true 949 ; 950 throw_or_fail(domain,X,Tuned,"cyclic_now",Dict). % is domain right here? 951 952eval(acyclic_forever,X,Tuned,_,Dict) :- 953 (ground(X),acyclic_term(X)) % never throws 954 -> 955 true 956 ; 957 throw_or_fail(domain,X,Tuned,"acyclic_forever",Dict). % is domain right here? 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)). % is domain right here? 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 987% --- 988% eval with forall/forany/fornone 989% --- 990 991eval(forall(ListOfChecks),X,Tuned,TP,Dict) :- 992 forall_forall_loop(ListOfChecks,X,Tuned,TP,Dict) % Tuned is passed 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) % Tuned is not upheld, can only fail 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) % Tuned is not upheld, can only fail 1007 -> 1008 true 1009 ; 1010 throw_or_fail(fornone,checks(ListOfChecks)-item(X),Tuned,"none of the checks succeeds for the item",Dict). 1011 1012% --- 1013% eval with passall/passany/passnone 1014% TODO: - We give not precise indicates which X failed the check how (i..e no index) 1015% - Also, passany and passnone do not give any information about what went wrong at 1016% all as they fail the individual checks and then throw a generic exception 1017% Is fixing both of these worth the complexity? 1018% --- 1019 1020eval(passall(Check),ListOfX,Tuned,TP,Dict) :- 1021 passall_forall_loop(Check,ListOfX,Tuned,TP,Dict) % Tuned is passed; thrown exception informs about problem 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) % Tuned is not upheld, can only fail 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) % Tuned is not upheld, can only fail 1036 -> 1037 true 1038 ; 1039 throw_or_fail(passnone,check(Check)-items(ListOfX),Tuned,"none of the items passes the check",Dict). 1040 1041% --- 1042% eval for the special case of "membership in explicitly given list" 1043% --- 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), % predicate name is confusing here: it is not X but ListOfValues which must be a list! 1048 ((\+ \+ member(X,ListOfValues)) % Use \+ \+ to roll back any accidental bindings 1049 -> 1050 true 1051 ; 1052 throw_or_fail(domain,X,Tuned,"list_membership",Dict)). 1053 1054% --- 1055% More helpers 1056% --- 1057 1058forall_forall_loop(ListOfChecks,X,Tuned,TP,Dict) :- 1059 % TODO: There is no need to do this if the well-formedness check 1060 % is on, but it must be done either there or here otherwise the forall 1061 % call will succeed on non-list (similarly, in forany/fornone) 1062 eval(proper_list,ListOfChecks,hard,hard,Dict), 1063 forall( % success of ListOfChecks is empty 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( % failure if ListOfChecks is empty 1070 member(Check,ListOfChecks), 1071 \+eval(Check,X,soft,TP,Dict)). % disable throwing 1072 1073fornone_forall_loop(ListOfChecks,X,TP,Dict) :- 1074 eval(proper_list,ListOfChecks,hard,hard,Dict), 1075 (ListOfChecks == []) % force failure if ListOfChecks is empty 1076 -> 1077 false 1078 ; 1079 forall( 1080 member(Check,ListOfChecks), 1081 \+eval(Check,X,soft,TP,Dict)). % disable throwing 1082 1083passall_forall_loop(Check,ListOfX,Tuned,TP,Dict) :- 1084 % TODO: There is no need to do this if the well-formedness check 1085 % is on, but it must be done either there or here otherwise the forall 1086 % call will succeed on non-list 1087 eval(proper_list,ListOfX,hard,hard,Dict), 1088 forall( % success if ListOfX is empty 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( % failure if ListOfX is empty 1095 member(X,ListOfX), 1096 \+eval(Check,X,soft,TP,Dict)). % disable throwing 1097 1098passnone_forall_loop(Check,ListOfX,TP,Dict) :- 1099 eval(proper_list,ListOfX,hard,hard,Dict), 1100 (ListOfX == []) % force failure if ListOfX is empty 1101 -> 1102 false 1103 ; 1104 forall( 1105 member(X,ListOfX), 1106 \+eval(Check,X,soft,TP,Dict)). % disable throwing