1/* Part of Assertion Reader for SWI-Prolog 2 3 Author: Edison Mera 4 E-mail: efmera@gmail.com 5 WWW: https://github.com/edisonm/assertions 6 Copyright (C): 2017, Process Design Center, Breda, The Netherlands. 7 All rights reserved. 8 9 Redistribution and use in source and binary forms, with or without 10 modification, are permitted provided that the following conditions 11 are met: 12 13 1. Redistributions of source code must retain the above copyright 14 notice, this list of conditions and the following disclaimer. 15 16 2. Redistributions in binary form must reproduce the above copyright 17 notice, this list of conditions and the following disclaimer in 18 the documentation and/or other materials provided with the 19 distribution. 20 21 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 22 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 23 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 24 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 25 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 26 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 27 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 28 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 29 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 30 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 31 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 32 POSSIBILITY OF SUCH DAMAGE. 33*/ 34 35:- module(assertions, 36 [asr_head/2, 37 assrt_type/1, 38 assrt_status/1, 39 expand_assertion/4, 40 asr_head_prop/8, 41 curr_prop_asr/4, 42 asr_aprop/4, 43 aprop_asr/4, 44 prop_asr/4, 45 prop_asr/7, 46 current_decomposed_assertion_1/12, 47 decompose_assertion_head_body/13]). 48 49:- discontiguous '$exported_op'/3. 50:- reexport(library(compound_expand)). 51:- reexport(library(assertions_op)). 52:- use_module(library(extend_args)). 53:- use_module(library(apply)). 54:- use_module(library(pairs)). 55:- use_module(library(extra_messages), []). 56:- use_module(library(filepos_line)). 57:- use_module(library(lists)). 58:- use_module(library(list_sequence)). 59:- use_module(library(neck)). 60:- use_module(library(termpos)). 61:- use_module(library(prolog_codewalk), []).
90:- multifile 91 asr_head_prop/8, 92 asr_comm/3, 93 asr_glob/4, 94 asr_comp/4, 95 asr_call/4, 96 asr_succ/4, 97 doc_db/4, 98 nodirective_error_hook/1. 99 100% asr_* declared dynamic to facilitate cleaning 101:- dynamic 102 asr_head_prop/8, 103 asr_comm/3, 104 asr_glob/4, 105 asr_comp/4, 106 asr_call/4, 107 asr_succ/4, 108 doc_db/4, 109 nodirective_error_hook/1. 110 111% These predicates are intended not to be called directly by user-applications: 112 113:- public 114 asr_comm/3, 115 asr_comp/4, 116 asr_call/4, 117 asr_succ/4, 118 asr_glob/4.
126asr_head(Asr, M:Head) :- 127 ( nonvar(Asr) 128 ->arg(1, Asr, M), 129 arg(2, Asr, Head) 130 ; true 131 ). 132 133curr_prop_asr(head, M:P, From, Asr) :- asr_head_prop(Asr, M, P, _, _, _, _, From). 134curr_prop_asr(stat, P, From, Asr) :- asr_head_prop(Asr, _, _, P, _, _, _, From). 135curr_prop_asr(type, P, From, Asr) :- asr_head_prop(Asr, _, _, _, P, _, _, From). 136curr_prop_asr(dict, D, From, Asr) :- asr_head_prop(Asr, _, _, _, _, D, _, From). 137curr_prop_asr(comm, C, From, Asr) :- asr_comm(Asr, C, From). 138curr_prop_asr(comp, M:P, From, Asr) :- asr_comp(Asr, M, P, From). 139curr_prop_asr(call, M:P, From, Asr) :- asr_call(Asr, M, P, From). 140curr_prop_asr(succ, M:P, From, Asr) :- asr_succ(Asr, M, P, From). 141curr_prop_asr(glob, M:P, From, Asr) :- asr_glob(Asr, M, P, From).
assrt_meta.pl for an example). The first argument is wrapped to
facilitate indexing. Note that it is recommended that multiple clauses of
this predicate be mutually exclusive.151:- multifile asr_aprop/4. 152 153prop_asr(H, M, Stat, Type, Dict, From, Asr) :- 154 asr_head_prop(Asr, C, H, Stat, Type, Dict, _, From), 155 predicate_property(C:H, implementation_module(IM)), 156 match_modules(H, M, IM). 157 158match_modules(_, M, M) :- !. 159match_modules(H, M, IM) :- predicate_property(M:H, implementation_module(IM)). 160 161:- meta_predicate 162 prop_asr(, , , ), 163 aprop_asr(, , , ). 164 165prop_asr(Key, M:P, From, Asr) :- 166 curr_prop_asr(Key, C:P, From, Asr), 167 predicate_property(C:P, implementation_module(IM)), 168 match_modules(P, M, IM). 169 170aprop_asr(Key, M:P, From, Asr) :- 171 asr_aprop(Asr, Key, C:P, From), 172 predicate_property(C:P, implementation_module(IM)), 173 match_modules(P, M, IM). 174 175add_arg(_, G1, G2, _, _) :- 176 var(G1), 177 var(G2), 178 !, 179 assertion(fail), 180 fail. 181add_arg(H, G1, G2, PPos1, PPos2) :- 182 \+ ( var(PPos1), 183 var(PPos2) 184 ), 185 PPos1 = parentheses_term_position(From, To, Pos1), 186 PPos2 = parentheses_term_position(From, To, Pos2), 187 !, 188 add_arg(H, G1, G2, Pos1, Pos2). 189add_arg(H, M:G1, M:G2, 190 term_position(From, To, FFrom, FTo, [MPos, Pos1]), 191 term_position(From, To, FFrom, FTo, [MPos, Pos2])) :- 192 !, 193 add_arg(H, G1, G2, Pos1, Pos2). 194add_arg(H, G1, G2, Pos1, Pos2) :- 195 ( var(Pos1) 196 ->true 197 ; ( Pos1 = term_position(From, To, FFrom, FTo, PosL1) 198 ->( nonvar(PosL1) 199 ->append(PosL1, [0-0 ], PosL) 200 ; true 201 ) 202 ; Pos1 = From-To 203 ->FFrom = From, 204 FTo = To, 205 PosL = [0-0 ] 206 ), 207 Pos2 = term_position(From, To, FFrom, FTo, PosL) 208 ), 209 extend_args(G1, [H], G2).
decompose_assertion_body(+Body, +Pos, -Head, -Compat, -Call, -Succ, -Glob, Comment)
SWI-Extensions with respect to the Ciao Assertion Language:
225:- add_termpos(decompose_assertion_body(+, -, -, -, -)). 226:- add_termpos(decompose_assertion_body(+, -, -, -, -, -)). 227:- add_termpos(decompose_assertion_body(+, -, -, -, -, -, -)). 228 229% ----------------------- AB C D E- -AB--C-----D-----E----- %CDE 230decompose_assertion_body((AB:C=>D + E), AB, C, D, E ) :- valid_cp(C). %111 231decompose_assertion_body((AB:C=>D is E), AB, C, D, E ) :- valid_cp(C). %111 232decompose_assertion_body((AB:C=>D ), AB, C, D, true) :- valid_cp(C). %110 233decompose_assertion_body((AB:C + E), AB, C, true, E ) :- valid_cp(C). %101 234decompose_assertion_body((AB:C is E), AB, C, true, E ) :- valid_cp(C). %101 235decompose_assertion_body((AB:C ), AB, C, true, true) :- valid_cp(C). %100 236decompose_assertion_body((AB =>D + E), AB, true, D, E ). %011 237decompose_assertion_body((AB =>D is E), AB, true, D, E ). %011 238decompose_assertion_body((AB =>D ), AB, true, D, true). %010 239decompose_assertion_body((AB + E), AB, true, true, E ). %001 240decompose_assertion_body((AB is E), AB, true, true, E ). %001 241decompose_assertion_body((AB ), AB, true, true, true). %000 242 243decompose_assertion_body((BO#F), A, B, C, D, E, F ) :- decompose_assertion_body(BO, A, B, C, D, E). 244decompose_assertion_body(BO, A, B, C, D, E, "") :- decompose_assertion_body(BO, A, B, C, D, E). 245 246decompose_assertion_body((A::BO), A, B, C, D, E) :- decompose_assertion_body(BO, B, C, D, E). 247decompose_assertion_body(BO, A, true, C, D, E) :- decompose_assertion_body(BO, A, C, D, E). 248 249valid_cp(C) :- \+ invalid_cp(C). 250 251invalid_cp(_/_).
260validate_body_sections(pred, _, _, _, _, [], []). 261validate_body_sections(prop, _, _, _, _, [], []). 262validate_body_sections(calls, Cp, Ca, Su, Gl, 263 [compatibility-Cp, postconditions-Su, globalprops-Gl], 264 [preconditions-Ca]). 265validate_body_sections(success, Cp, _, Su, Gl, 266 [compatibility-Cp, globalprops-Gl], 267 [postconditions-Su]). 268validate_body_sections(comp, Cp, _, Su, Gl, 269 [compatibiltiy-Cp, postconditions-Su], 270 [globalprops-Gl]).
calls - Specifies the properties at call time.
success - Specifies the properties on success, but only for external calls.
comp - Assertion type comp, specifies computational or global properties.
prop - States that the predicate is a property
pred - Union of calls, success and comp assertion types
286assrt_type(Type) :-
287 validate_body_sections(Type, _, _, _, _, _, _),
288 neck.check - Assertion should be checked statically or with the rtcheck tracer (default)
true - Assertion is true, provided by the user
false - Assertion is false, provided by the user (not implemented yet)
debug - Assertion should be checked only at development time
static - Assertion is always instrumented in the code via a wrapper, in other words, it is considered part of the implementation.
@note: For static, such instrumentation can be removed only if a static analysis prove it is always true (not implemented yet).
317assrt_status(check). 318assrt_status(true). 319assrt_status(false). 320assrt_status(debug). 321assrt_status(static). 322 323:- add_termpos(decompose_status_and_type_1(+,?,?,-)). 324:- add_termpos(decompose_status_and_type(+,?,?,-)). 325 326decompose_status_and_type_1(Assertions, check, AssrtType, UBody) :- 327 assrt_type(AssrtType), 328 Assertions =.. [AssrtType, UBody], 329 neck. 330decompose_status_and_type_1(Assertions, AssrtStatus, AssrtType, UBody) :- 331 assrt_type(AssrtType), 332 Assertions =.. [AssrtType, AssrtStatus, UBody], 333 neck. 334 335decompose_status_and_type(Assertions, APos, AssrtStatus, AssrtType, UBody, BPos) :- 336 cleanup_parentheses(APos, Pos), 337 decompose_status_and_type_1(Assertions, Pos, AssrtStatus, AssrtType, UBody, BPos), 338 assrt_status(AssrtStatus). 339 340cleanup_parentheses(Pos1, Pos) :- 341 nonvar(Pos1), 342 Pos1 = parentheses_term_position(_, _, Pos2), 343 !, 344 cleanup_parentheses(Pos2, Pos). 345cleanup_parentheses(Pos, Pos). 346 347% To Avoid attempts to execute asertions (must be declarations): 348 349:- assrt_type(Type), 350 member(Arity, [1, 2]), 351 neck, 352 export(Type/Arity). 353 354Assr :- 355 decompose_status_and_type_1(Assr, _, Status, Type, _, _), 356 functor(Assr, Type, Arity), 357 Body1 = ignore(nodirective_error_hook(Assr)), 358 ( Arity = 1 359 ->Body = Body1 360 ; Body = (assrt_status(Status), Body1) 361 ), 362 neck, 363 . 364 365is_decl_global(Head, M) :- 366 is_decl_global(Head, _, _, M). 367 368is_decl_global(Head, Status, Type, M) :- 369 forall(Head = HM:_, (var(HM);atom(HM))), 370 prop_asr(head, M:Head, _, Asr), 371 ( ( prop_asr(glob, metaprops:declaration(Status, _), _, Asr) 372 ; Status = true, 373 prop_asr(glob, metaprops:declaration(_), _, Asr) 374 ) 375 ->( prop_asr(glob, metaprops:global(Type, _), _, Asr) 376 ; Type = (pred) 377 ) 378 ; ( prop_asr(glob, metaprops:global(Type, _), _, Asr) 379 ; Type = (pred), 380 prop_asr(glob, metaprops:global(_), _, Asr) 381 ), 382 Status = true 383 ), 384 !. 385 386:- multifile current_decomposed_assertion_2/9. % prevent false positive warning 387 388:- add_termpos(current_decomposed_assertion(+,?,?,?,?,?,?,?,?,-,?)). 389:- add_termpos(current_decomposed_assertion_1(+,?,?,?,-,?,?,-,?)). 390:- add_termpos(current_decomposed_assertion_2(+,?,?,?,-,?,?,-,?)). 391:- add_termpos(propdef(+,?,?,?)). 392:- add_termpos(merge_comments(-,-,+)). 393:- add_termpos(decompose_assertion_head_body(+,?,?,+,?,?,?,?,-,?)). 394:- add_termpos(decompose_assertion_head_body_(+,?,?,+,?,?,?,?,-,?)). 395:- add_termpos(decompose_assertion_head(+,?,?,+,-,?,?,?,?,?)). 396:- add_termpos(decompose_assertion_head_(+,?,?,+,-,?,?,?,?,?)). 397 398merge_comments("", C, C). 399merge_comments(C, "", C). 400merge_comments(C1, C2, [C1, C2]). 401 402current_decomposed_assertion(Assertions, PPos, M, Pred, Status, Type, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 403 current_decomposed_assertion_1(Assertions, PPos, M, Status, Type, BodyS, BSPos, Gl, Gl2, Co, CoPos, RPos), 404 decompose_assertion_head_body(BodyS, BSPos, M, Pred, true, _, Cp, Ca, Su, Gl2, Co, CoPos, RPos), 405 validate_body_sections(Type, Cp, Ca, Su, Gl, MustBeEmpty, MustNotBeEmpty), 406 maplist(report_must_be_empty(Type), MustBeEmpty), 407 maplist(report_must_not_be_empty(Type, RPos), MustNotBeEmpty). 408 409current_decomposed_assertion_1(Assertions, PPos, M, Status, Type, BodyS, BSPos, Gl1, Gl, Co, CoPos, RPos) :- 410 cleanup_parentheses(PPos, APos), 411 current_decomposed_assertion_2(Assertions, APos, M, Status, Type, BodyS, BSPos, Gl1, Gl, Co, CoPos, RPos). 412 413current_decomposed_assertion_2(AssertionsBGl, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 414 member(AssertionsBGl, [Assertions + BGl, 415 Assertions is BGl]), 416 necki, 417 propdef(BGl, M, Gl1, Gl2), 418 current_decomposed_assertion_1(Assertions, M, Status, Type, BodyS, Gl2, Gl, Co, RPos). 419current_decomposed_assertion_2(Assertions # Co2, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 420 !, 421 current_decomposed_assertion_1(Assertions, M, Status, Type, BodyS, Gl1, Gl, Co1, RPos), 422 once(merge_comments(Co1, Co2, Co)). 423current_decomposed_assertion_2(Assertions, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 424 ( is_decl_global(Assertions, DStatus, DType, M) 425 ->once(decompose_status_and_type_1(Term, DStatus, DType, Assertions)), 426 current_decomposed_assertion_2(Term, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) 427 ; decompose_status_and_type(Assertions, Status, Type, BodyS), 428 Gl = Gl1 429 ). 430 431report_must_be_empty(Type, Section-Props) :- 432 maplist(report_must_be_empty(Type, Section), Props). 433 434termpos_location(Pos, Loc) :- 435 ignore(source_location(File, Line)), 436 ( nonvar(File) 437 ->( nonvar(Pos) 438 ->Loc = file_term_position(File, Pos) 439 ; nonvar(Line) 440 ->Loc = file(File, Line, -1, _) 441 ; true 442 ) 443 ; true 444 ). 445 446report_must_be_empty(Type, Section, Prop-Pos) :- 447 termpos_location(Pos, Loc), 448 print_message( 449 warning, 450 at_location( 451 Loc, 452 format("In '~w' assertion, '~w' section, '~w' will be ignored", 453 [Type, Section, Prop]))). 454 455report_must_not_be_empty(Type, Pos, Section-Prop) :- 456 ( Prop = [] 457 ->termpos_location(Pos, Loc), 458 print_message( 459 warning, 460 at_location( 461 Loc, 462 format("In '~w' assertion, missing properties in '~w' section", 463 [Type, Section]))) 464 ; true 465 ). 466 467combine_pi_comp(N, Head, PosL1, PosL, BCp, PCp) :- 468 cleanup_parentheses(PCp, Pos), 469 combine_pi_comp_(N, Head, PosL1, PosL, BCp, Pos). 470 471combine_pi_comp_(N1, Head, PosL1, PosL, (H * P), term_position(_, _, _, _, [TPos, Pos])) :- 472 arg(N1, Head, P), 473 !, 474 succ(N, N1), 475 combine_pi_comp(N, Head, [Pos|PosL1], PosL, H, TPos). 476combine_pi_comp_(N, Head, PosL, [Pos|PosL], P, Pos) :- 477 arg(N, Head, P). 478 479% EMM: Support for grouped properties 480 481merge_props(BCp1, _, BCp, PCp, BCp, PCp) :- strip_module(BCp1, _, true). 482merge_props(BCp, PCp, BCp2, _, BCp, PCp) :- strip_module(BCp2, _, true). 483merge_props(BCp1, PCp1, BCp2, PCp2, (BCp1, BCp2), term_position(_, _, _, _, [PCp1, PCp2])). 484 485decompose_assertion_head_body(B, P1, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 486 cleanup_parentheses(P1, P), 487 decompose_assertion_head_body_(B, P, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 488 489decompose_assertion_head_body_(Var, _, _, _, _, _, _, _, _, _) :- 490 var(Var), 491 !, 492 fail. 493decompose_assertion_head_body_((B1, B2), M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 494 !, 495 ( decompose_assertion_head_body(B1, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 496 ; decompose_assertion_head_body(B2, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 497 ). 498decompose_assertion_head_body_([B1|B2], M, 499 Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 500 !, 501 ( decompose_assertion_head_body(B1, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 502 ; decompose_assertion_head_body(B2, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 503 ). 504decompose_assertion_head_body_(M:Body, CM, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 505 atom(M), 506 callable(Body), 507 !, 508 % Switching the body context does not implies switching the context of the 509 % compatibility properties, that is why CM should be preserved in the 510 % compatibility section: 511 decompose_assertion_head_body(Body, M, Pred, CM:BCp, Cp, Ca, Su, Gl, Co, RPos). 512decompose_assertion_head_body_([], _, _, _, _, _, _, _, _, _) :- 513 !, 514 fail. 515decompose_assertion_head_body_(Body, BPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 516 is_decl_global(Body, M), 517 Body =.. [F, Head|GArgL], 518 nonvar(Head), 519 !, 520 ( nonvar(BPos) 521 ->BPos = term_position(_, _, FF, FT, [HPos|PArgL]), 522 NPos = term_position(_, _, _, _, [HPos, term_position(_, _, FF, FT, [PArgL])]) 523 ; true 524 ), 525 BGl =.. [F|GArgL], 526 decompose_assertion_head_body(Head + BGl, NPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 527decompose_assertion_head_body_(Body, BPos, M, Pred, BCp2, PCp2, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 528 ( once(decompose_assertion_body(Body, BPos, BH1, PH1, BCp1, PCp1, 529 BCa, PCa, BSu, PSu, BGl, PGl, BCo, PCo)), 530 Body \= BH1 531 ->propdef(BGl, PGl, M, Gl, Gl1), 532 once(merge_props(BCp1, PCp1, BCp2, PCp2, BCp, PCp)), 533 decompose_assertion_head_body(BH1, PH1, M, Pred, BCp, PCp, Cp, Ca1, Su1, Gl1, BCo1, PCo1, RPos), 534 apropdef(Pred, M, BCa, PCa, Ca, Ca1), 535 apropdef(Pred, M, BSu, PSu, Su, Su1), 536 once(merge_comments(BCo1, PCo1, BCo, PCo, Co, CoPos)) 537 ; decompose_assertion_head(Body, BPos, M, Pred, BCp2, PCp2, BCp, PCp, Cp1, Ca, Su, Gl, RPos), 538 apropdef(Pred, M, BCp, PCp, Cp, Cp1), 539 Co = "" 540 ). 541 542decompose_assertion_head(Head, PPos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos) :- 543 cleanup_parentheses(PPos, Pos), 544 decompose_assertion_head_(Head, Pos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos). 545 546decompose_assertion_head_(M:H, _, P, BCp1, BCp, Cp, Ca, Su, Gl, RP) :- 547 atom(M), 548 !, 549 decompose_assertion_head(H, M, P, BCp1, BCp, Cp, Ca, Su, Gl, RP). 550decompose_assertion_head_(F/A, HPos, M, M:Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 551 !, 552 atom(F), 553 integer(A), 554 functor(Head, F, A), 555 ( once(( BCp1 = CM:BCp2, 556 PCp1 = term_position(_, _, _, _, [_, PCp2]) 557 ; BCp1 = BCp2, 558 PCp1 = PCp2, 559 CM = M 560 )), 561 BCp2 \= true, 562 combine_pi_comp(A, Head, [], PosL, BCp2, PCp2) 563 ->( nonvar(HPos) 564 ->HPos = term_position(From, To, _, _, [FPos, APos]), 565 ( nonvar(FPos) 566 ->arg(1, FPos, FFrom), 567 arg(2, FPos, FTo) 568 ; true 569 ) 570 ; true 571 ), 572 decompose_assertion_head_(Head, term_position(From, To, FFrom, FTo, PosL), CM, 573 CM:Pred, true, APos, BCp, PCp, Cp, Ca, Su, Gl, Pos) 574 ; Pred = Head, 575 Cp = [], 576 Ca = [], 577 Su = [], 578 Gl = [], 579 HPos = Pos, 580 BCp = BCp1, 581 PCp = PCp1 582 ). 583decompose_assertion_head_(Head, Pos, M, M:Pred, BCp, PCp, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 584 compound(Head), 585 !, 586 functor(Head, F, A), 587 functor(Pred, F, A), 588 Pos = term_position(_, _, _, _, PosL), 589 decompose_args(PosL, 1, Head, M, Pred, Cp, Ca, Su, Gl). 590decompose_assertion_head_(Head, Pos, M, M:Head, BCp, PCp, BCp, PCp, [], [], [], [], Pos) :- 591 atom(Head). 592 593decompose_args([Pos|PosL], N1, Head, M, Pred, Cp1, Ca1, Su1, Gl1) :- 594 arg(N1, Head, HArg), 595 !, 596 resolve_types_modes(HArg, Pos, M, PArg, Cp1, Ca1, Su1, Gl1, Cp2, Ca2, Su2, Gl2), 597 arg(N1, Pred, PArg), 598 succ(N1, N), 599 decompose_args(PosL, N, Head, M, Pred, Cp2, Ca2, Su2, Gl2). 600decompose_args([], _, _, _, _, [], [], [], []). 601 602:- add_termpos(resolve_types_modes_(+,?,?,?,?,?,?,?,?,?,?)). 603:- add_termpos(do_modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 604:- add_termpos(modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 605:- add_termpos(do_propdef(+,?,?,?,?)). 606:- add_termpos(hpropdef(+,?,?,?,?)). 607 608resolve_types_modes(A, _, _, A, Cp, Ca, Su, Gl, Cp, Ca, Su, Gl) :- var(A), !. 609resolve_types_modes(A1, PPos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 610 cleanup_parentheses(PPos, Pos), 611 resolve_types_modes_(A1, Pos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl). 612 613resolve_types_modes_(A1:T, term_position(_, _, _, _, [PA1, PT]), M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 614 do_propdef(T, PT, M, A, Pr1, Pr2), 615 cleanup_parentheses(PA1, PA11), 616 do_modedef(A1, PA11, M, A, A2, PA2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 617 !, 618 do_propdef(A2, PA2, M, A, Pr2, Pr). 619resolve_types_modes_(A1, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 620 do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 621 do_propdef(A2, M, A, Pr1, Pr). 622 623do_propdef(A, _, A, Cp, Cp) :- var(A), !. 624do_propdef(A1, M, A, Cp1, Cp) :- 625 hpropdef(A1, M, A, Cp1, Cp). 626 627do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 628 nonvar(A1), 629 modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 630 !. 631do_modedef(A1, APos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 632 atom(A1), 633 A3 =.. [A1, A], 634 ( var(APos) -> true ; APos = From-To, Pos = term_position(From, To, From, To, [To-To]) ), 635 modedef(A3, Pos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 636 !. 637do_modedef(A1, From-To, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 638 integer(A1), 639 ( A1 >= 0 640 ->A3 = goal_in(A1, A) 641 ; A4 is -A1, 642 A3 = goal_go(A4, A) 643 ), 644 modedef(A3, term_position(From, To, From, From, [From-From, From-To]), M, A, A2, 645 PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 646 !. 647do_modedef(A1, PA1, _, _, A1, PA1, Cp1, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp). 648 649:- add_termpos(put_prop(+,?,?,?)). 650 651put_prop(_, Pos, Prop) --> [Prop-Pos]. 652 653% Support for modes are hard-wired here: 654% ISO Modes 655modedef(+A, M, B, A, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- 656 ( var(A), var(Ca2) 657 ->put_prop(A, M:nonvar(B), Ca1, Ca2) 658 ; Ca1 = Ca2 659 ). % A bit confuse hack, Ca1 comes instantiated to optimize the expression 660modedef(-A, M, B, A, Cp, Ca2, Su1, Gl, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, M:var(B), Ca2, Ca). 661% Less restrictive - uses further instantiated: 662% modedef(-(A), _, A, B, Pos, PA, Cp, Ca, Su1, [(globprops:fi(B))-Pos|Gl], Cp, Ca, Su, Gl, Su1, Su) :- Pos = term_position(_, _, _, _, [PA]). 663modedef(?A, _, _, A, Cp1, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp). 664modedef(@(A), _, B, A, Cp1, Ca, Su, Gl1, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, globprops:nfi(B), Gl1, Gl). 665% PlDoc (SWI) Modes 666modedef(:A1, Pos, M, B, A, PA, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- 667 Pos = term_position(From, To, FFrom, FTo, [PA1]), 668 % The first part of this check is not redundant if we forgot the meta_predicate declaration 669 ( var(A1), 670 var(Ca2) 671 ->put_prop(A, Pos, M:mod_qual(B), Ca1, Ca2), 672 A1 = A, 673 PA = PA1 674 ; Ca1 = Ca2, 675 A = M:mod_qual(A1, B), 676 PA = term_position(From, To, FFrom, FTo, [PA1, From-From]) 677 ). 678modedef(goal_in(N,A), _, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, typeprops:goal(N,B), Ca2, Ca1). 679modedef(goal_go(N,A), _, B, A, Cp, Ca, Su2, Gl, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, typeprops:goal(N,B), Su2, Su1). 680modedef(!A, M, B, A, Cp1, Ca2, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, M:compound(B), Ca2, Ca). % May be modified using setarg/3 or nb_setarg/3 (mutable) 681% Ciao Modes: 682modedef(in(A), M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:ground(B), Ca2, Ca1). 683modedef(out(A), M, B, A, Cp, Ca2, Su2, Gl, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, M:var(B), Ca2, Ca), put_prop(A, M:gnd(B), Su2, Su1). 684modedef(go(A), M, B, A, Cp1, Ca, Su2, Gl, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, M:gnd(B), Su2, Su). 685% Additional Modes (See Coding Guidelines for Prolog, Michael A. Covington, 2009): 686modedef(*A, M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:ground(B), Ca2, Ca1). 687modedef(=A, _, B, A, Cp1, Ca, Su, Gl1, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, globprops:nfi(B), Gl1, Gl). % The state of A is preserved 688modedef(/A, M, B, A, Cp, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, M:var(B), Ca1, Ca), put_prop(A, globprops:nsh(B), Gl1, Gl). % Like '-' but also A don't share with any other argument 689modedef(>A, _, _, A, Cp, Ca, Su1, Gl, Cp, Ca, Su, Gl, Su1, Su). % Like output but A might be nonvar on entry 690 691% nfi == not_further_inst 692% nsh == not_shared 693 694:- multifile prolog:error_message/3. 695 696prologerror_message(assertion(il_formed_assertion, Term)) --> 697 [ 'Il formed assertion, check term ~w'-[Term]]. 698 699hpropdef(A1, PA1, M, A, Cp1, Cp) :- 700 term_variables(A1, V), 701 ( member(X, V), X==A -> 702 Cp1 = [(M:A1)-PA1|Cp] 703 ; aprops_arg(A1, M, A, PA1, Cp1, Cp) 704 ). 705 706apropdef_2(0, _, _, _, _) --> !, {fail}. 707apropdef_2(N, Head, M, A, PPos) --> 708 {cleanup_parentheses(PPos, Pos)}, 709 !, 710 apropdef_2_(N, Head, M, A, Pos). 711 712apropdef_2_(1, Head, M, A, APos) --> 713 {arg(1, Head, V)}, 714 !, 715 hpropdef(A, APos, M, V). 716apropdef_2_(N1, Head, M, (P * A), term_position(_, _, _, _, [PPos, APos])) --> 717 {arg(N1, Head, V)}, 718 !, 719 {succ(N, N1)}, 720 apropdef_2(N, Head, M, P, PPos), 721 hpropdef(A, APos, M, V). 722 723apropdef(Var, _, _, _) --> {var(Var), !, fail}. 724apropdef(_:Head, M, A, APos) --> 725 {functor(Head, _, N)}, 726 apropdef_2(N, Head, M, A, APos), 727 !. 728apropdef(_, M, A, APos) --> propdef(A, APos, M). 729 730propdef(A, APos, M) --> props_args(A, M, push, APos). 731 732push(A, M, Pos) --> [(M:A)-Pos]. 733 734aprops_arg(A, M, V, PPos) --> 735 {cleanup_parentheses(PPos, Pos)}, 736 aprops_arg_(A, M, V, Pos). 737 738aprops_arg_({A}, M, V, brace_term_position(_, _, Pos)) --> !, aprops_args(A, M, V, Pos). 739aprops_arg_(A, M, V, Pos) --> aprops_args(A, M, V, Pos). 740 741aprops_args(A, M, V, Pos) --> props_args(A, M, prop_arg(V), Pos). 742 743:- meta_predicate props_args(, , , , , ). 744 745props_args(true, _, _, _) --> !, []. 746props_args(A, M, V, PPos) --> 747 {cleanup_parentheses(PPos, Pos)}, 748 !, 749 props_args_(A, M, V, Pos). 750 751props_args_((A, B), M, V, term_position(_, _, _, _, [PA, PB])) --> 752 !, 753 props_args(A, M, V, PA), 754 props_args(B, M, V, PB). 755props_args_((A; B), M, V, Pos) --> 756 !, 757 { Pos = term_position(_, _, _, _, [PA, PB]), 758 props_args(A, M, V, PA, P1, []), 759 pairs_keys(P1, ML1), 760 maplist(cleanup_mod(M), ML1, L1), 761 list_sequence(L1, C1), 762 props_args(B, M, V, PB, P2, []), 763 pairs_keys(P2, ML2), 764 maplist(cleanup_mod(M), ML2, L2), 765 list_sequence(L2, C2) 766 }, 767 [(M:(C1;C2))-Pos]. 768props_args_(M:A, _, V, term_position(_, _, _, _, [_, PA])) --> 769 {atom(M)}, 770 !, 771 props_args(A, M, V, PA). 772props_args_(A, M, V, Pos) --> call(V, A, M, Pos). 773 774cleanup_mod(M, M:C, C) :- !. 775cleanup_mod(_, MC, MC). 776 777prop_arg(V, A, M, Pos) --> 778 {add_arg(V, A, P, Pos, PPos)}, 779 [(M:P)-PPos]. 780 781expand_assertion_helper(Match, a(Match, Record, Pos), Record, Pos). 782 783expand_assertion(M, Dict, Decl, PPos, Records, RPos) :- 784 cleanup_parentheses(PPos, Pos), 785 !, 786 expand_assertion_(M, Dict, Decl, Pos, Records, RPos). 787 788expand_assertion_(_, Dict, M:Decl, term_position(_, _, _, _, [_, DPos]), 789 Records, RPos) :- 790 atom(M), 791 !, 792 expand_assertion(M, Dict, Decl, DPos, Records, RPos). 793expand_assertion_(M, Dict, doc(Key, Doc), 794 term_position(From, To, FFrom, FTo, [KPos, DPos]), 795 assertions:doc_db(Key, M, Doc, Dict), 796 term_position(0, 0, 0, 0, 797 [0-0, 798 term_position(From, To, FFrom, FTo, 799 [KPos, 0-0, DPos, 0-0 ])])) :- !. 800% Note: We MUST save the full location (File, HPos), because later we will not 801% have access to source_location/2, and this will fails for further created 802% clauses --EMM 803expand_assertion_(CM, Dict, Assertions, APos, Records, RPos) :- 804 Match=(Assertions-Dict), 805 findall(a(Match, Clause, HPos), 806 assertion_record_each(CM, Dict, Assertions, APos, Clause, HPos), 807 ARecords), 808 ARecords \= [], 809 maplist(expand_assertion_helper(Match), ARecords, Records, RPos).
file(File, Line, Pos, _), instead of the term
'$source_location'(File,Line):Clause
819assertion_record_each(CM, Dict, Assertions, APos, Clause, TermPos) :-
820 ignore(source_location(File, Line1)),
821 ( nonvar(File)
822 ->Loc = file(File, Line, Pos, _),
823 ( var(APos)
824 ->Line = Line1,
825 Pos = -1
826 ; true
827 )
828 ; true
829 ),
830 current_decomposed_assertion(Assertions, APos, CM, M:Head, Status, Type, CpL, CaL, SuL, GlL, Co, CoPos, HPos),
831 with_mutex('get_sequence_and_inc/1', get_sequence_and_inc(Count)),
832 term_variables(t(Co, CpL, CaL, SuL, GlL), ShareL),
833 atom_number(AIdx, Count),
834 Asr =.. [AIdx, M, Head|ShareL], % Asr also contains variable bindings. By
835 % convention, M is in the 1st position and
836 % Head in the 2nd, to facilitate work
837 ( Clause = assertions:asr_head_prop(Asr, M, Head, Status, Type, Dict, CM, Loc),
838 SubPos = HPos,
839 ( nonvar(SubPos)
840 ->arg(1, SubPos, From),
841 arg(2, SubPos, To),
842 TermPos = term_position(From, To, From, To,
843 [SubPos, 0-0, 0-0, 0-0, _, _, _])
844 ; true
845 )
846 ; Co \= "",
847 Clause = assertions:asr_comm(Asr, Co, Loc),
848 SubPos = CoPos,
849 ( nonvar(SubPos)
850 ->arg(1, SubPos, From),
851 arg(2, SubPos, To),
852 TermPos = term_position(From, To, From, To, [_, SubPos, _])
853 ; true
854 )
855 ; ( Clause = assertions:AClause,
856 member(AClause-PrL,
857 [asr_comp(Asr, PM, Pr, Loc)-CpL,
858 asr_call(Asr, PM, Pr, Loc)-CaL,
859 asr_succ(Asr, PM, Pr, Loc)-SuL
860 ]),
861 member(MPr-SubPos, PrL),
862 strip_module(MPr, PM, Pr)
863 ; Clause = assertions:asr_glob(Asr, PM, Pr, Loc),
864 member(MGl-GPos, GlL),
865 strip_module(MGl, PM, Gl),
866 add_arg(_, Gl, Pr, GPos, SubPos)
867 ;
868 once(( member(MGl-GPos, GlL),
869 member(Gl, [declaration, declaration(_)]),
870 strip_module(MGl, PM, Gl),
871 add_arg(_, Gl, Pr, GPos, _),
872 predicate_property(PM:Pr, implementation_module(metaprops)),
873 functor(Head, Op, 1)
874 )),
875 Clause = (:- '$export_ops'([op(1125, fy, Op)], PM, File))
876 ; member(MGl-_, GlL),
877 member(Gl, [declaration,
878 declaration(_),
879 global,
880 global(_)]),
881 strip_module(MGl, PM, Gl),
882 add_arg(_, Gl, Pr, _, _),
883 predicate_property(PM:Pr, implementation_module(metaprops))
884 ->functor(Head, Fn, N),
885 ( \+ predicate_property(M:Head, meta_predicate(_)),
886 functor(Meta, Fn, N),
887 Meta =.. [_|ArgL],
888 once(append(ArgL1, [0], ArgL)),
889 maplist(=(?), ArgL1),
890 Clause = (:- meta_predicate Meta)
891 )
892 ),
893 ( nonvar(SubPos)
894 ->arg(1, SubPos, From),
895 arg(2, SubPos, To),
896 TermPos = term_position(From, To, From, To, [_, 0-0, SubPos, _])
897 ; true
898 )
899 ),
900 ( var(Pos),
901 nonvar(File)
902 ->( nonvar(SubPos),
903 integer(From)
904 ->filepos_line(File, From, Line, Pos)
905 ; Line = Line1,
906 Pos = -1
907 )
908 ; true
909 ).916expand_assertion(Decl, DPos, Records, RPos) :- 917 '$current_source_module'(M), 918 expand_assertion(M, Dict, Decl, DPos, Records, RPos), 919 % Dict Must be assigned after expand_assertion/6 to avoid performance 920 % issues --EMM 921 ( nb_current('$variable_names', Dict) 922 ->true 923 ; Dict = [] 924 ). 925 926:- dynamic sequence/1. 927sequence(1). 928 929get_sequence_and_inc(S) :- 930 retract(sequence(S)), 931 succ(S, S2), 932 assertz(sequence(S2)). 933 934% ---------------------------------------------------------------------------- 935 936term_expansion_decl(Decl, PPos, Records, RPos) :- 937 nonvar(PPos), 938 PPos = parentheses_term_position(_, _, Pos), 939 !, 940 term_expansion_decl(Decl, Pos, Records, RPos). 941term_expansion_decl(Decl, PPos, Records, RPos) :- 942 ( nonvar(PPos) 943 ->PPos = term_position(_, _, _, _, [DPos]) 944 ; true 945 ), 946 expand_assertion(Decl, DPos, Records, RPos). 947 948term_expansion((:- Decl), DPos, Records, RPos) :- 949 term_expansion_decl(Decl, DPos, Records, RPos)
Assertion reader for SWI-Prolog
@note: asr_* declared multifile to allow extensibility. At this point you extend concrete assertions (not abstractions or fake ones, since they will be collected by the run-time checker, for instance)
@note: Next syntax is ambiguous, but shorter:
is equivalent to:
but can be confused with:
in any case this is syntax sugar so we can always write the long version of the assertion to avoid ambiguities
*/