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/5, 46 prop_asr/8, 47 current_decomposed_assertion_1/12, 48 decompose_assertion_head_body/13]). 49 50:- discontiguous '$exported_op'/3. 51:- reexport(library(compound_expand)). 52:- reexport(library(assertions_op)). 53:- use_module(library(extend_args)). 54:- use_module(library(apply)). 55:- use_module(library(pairs)). 56:- use_module(library(extra_messages), []). 57:- use_module(library(filepos_line)). 58:- use_module(library(neck)). 59:- use_module(library(termpos)). 60:- use_module(library(lists)). 61:- use_module(library(list_sequence)). 62:- use_module(library(prolog_codewalk), []). 63:- after(neck). 64:- init_expansors.
92:- multifile 93 asr_head_prop/8, 94 asr_comm/3, 95 asr_glob/4, 96 asr_comp/4, 97 asr_call/4, 98 asr_succ/4, 99 doc_db/4, 100 nodirective_error_hook/1. 101 102% asr_* declared dynamic to facilitate cleaning 103:- dynamic 104 asr_head_prop/8, 105 asr_comm/3, 106 asr_glob/4, 107 asr_comp/4, 108 asr_call/4, 109 asr_succ/4, 110 doc_db/4, 111 nodirective_error_hook/1. 112 113% These predicates are intended not to be called directly by user-applications: 114 115:- public 116 asr_comm/3, 117 asr_comp/4, 118 asr_call/4, 119 asr_succ/4, 120 asr_glob/4.
128asr_head(Asr, M:Head) :- 129 ( nonvar(Asr) 130 ->arg(1, Asr, M), 131 arg(2, Asr, Head) 132 ; true 133 ). 134 135curr_prop_asr(head, M:P, From, Asr) :- asr_head_prop(Asr, M, P, _, _, _, _, From). 136curr_prop_asr(stat, P, From, Asr) :- asr_head_prop(Asr, _, _, P, _, _, _, From). 137curr_prop_asr(type, P, From, Asr) :- asr_head_prop(Asr, _, _, _, P, _, _, From). 138curr_prop_asr(dict, D, From, Asr) :- asr_head_prop(Asr, _, _, _, _, D, _, From). 139curr_prop_asr(comm, C, From, Asr) :- asr_comm(Asr, C, From). 140curr_prop_asr(comp, M:P, From, Asr) :- asr_comp(Asr, M, P, From). 141curr_prop_asr(call, M:P, From, Asr) :- asr_call(Asr, M, P, From). 142curr_prop_asr(succ, M:P, From, Asr) :- asr_succ(Asr, M, P, From). 143curr_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.153:- multifile asr_aprop/4. 154 155prop_asr(H, M, Stat, Type, Dict, IM, From, Asr) :- 156 asr_head_prop(Asr, C, H, Stat, Type, Dict, _, From), 157 predicate_property(C:H, implementation_module(IM)), 158 match_modules(H, M, IM). 159 160match_modules(_, M, M) :- !. 161match_modules(H, M, IM) :- predicate_property(M:H, implementation_module(IM)). 162 163:- meta_predicate 164 prop_asr(, , , ), 165 prop_asr(, , , , ), 166 aprop_asr(, , , ). 167 168prop_asr(Key, M:P, From, Asr) :- 169 prop_asr(Key, M:P, _, From, Asr). 170 171prop_asr(Key, M:P, C, From, Asr) :- 172 curr_prop_asr(Key, C:P, From, Asr), 173 predicate_property(C:P, implementation_module(IM)), 174 match_modules(P, M, IM). 175 176aprop_asr(Key, M:P, From, Asr) :- 177 asr_aprop(Asr, Key, C:P, From), 178 predicate_property(C:P, implementation_module(IM)), 179 match_modules(P, M, IM). 180 181add_arg(_, G1, G2, _, _) :- 182 var(G1), 183 var(G2), 184 !, 185 assertion(fail), 186 fail. 187add_arg(H, G1, G2, PPos1, PPos2) :- 188 \+ ( var(PPos1), 189 var(PPos2) 190 ), 191 PPos1 = parentheses_term_position(From, To, Pos1), 192 PPos2 = parentheses_term_position(From, To, Pos2), 193 !, 194 add_arg(H, G1, G2, Pos1, Pos2). 195add_arg(H, M:G1, M:G2, 196 term_position(From, To, FFrom, FTo, [MPos, Pos1]), 197 term_position(From, To, FFrom, FTo, [MPos, Pos2])) :- 198 !, 199 add_arg(H, G1, G2, Pos1, Pos2). 200add_arg(H, G1, G2, Pos1, Pos2) :- 201 ( var(Pos1) 202 ->true 203 ; ( Pos1 = term_position(From, To, FFrom, FTo, PosL1) 204 ->( nonvar(PosL1) 205 ->append(PosL1, [0-0 ], PosL) 206 ; true 207 ) 208 ; Pos1 = From-To 209 ->FFrom = From, 210 FTo = To, 211 PosL = [0-0 ] 212 ), 213 Pos2 = term_position(From, To, FFrom, FTo, PosL) 214 ), 215 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:
231:- add_termpos(decompose_assertion_body(+, -, -, -, -)). 232:- add_termpos(decompose_assertion_body(+, -, -, -, -, -)). 233:- add_termpos(decompose_assertion_body(+, -, -, -, -, -, -)). 234 235% ----------------------- AB C D E- -AB--C-----D-----E----- %CDE 236decompose_assertion_body((AB:C=>D + E), AB, C, D, E ) :- valid_cp(C). %111 237decompose_assertion_body((AB:C=>D is E), AB, C, D, E ) :- valid_cp(C). %111 238% WARNING: Next is ambiguous if AB is a module-qualification, use [Module:Head] => D to deambiguate 239decompose_assertion_body((AB:C=>D ), AB, C, D, true) :- valid_cp(C). %110 240decompose_assertion_body((AB:C + E), AB, C, true, E ) :- valid_cp(C). %101 241decompose_assertion_body((AB:C is E), AB, C, true, E ) :- valid_cp(C). %101 242decompose_assertion_body((AB:C ), AB, C, true, true) :- valid_cp(C). %100 243decompose_assertion_body((AB =>D + E), AB, true, D, E ). %011 244decompose_assertion_body((AB =>D is E), AB, true, D, E ). %011 245decompose_assertion_body((AB =>D ), AB, true, D, true). %010 246decompose_assertion_body((AB + E), AB, true, true, E ). %001 247decompose_assertion_body((AB is E), AB, true, true, E ). %001 248decompose_assertion_body((AB ), AB, true, true, true). %000 249 250decompose_assertion_body((BO#F), A, B, C, D, E, F ) :- decompose_assertion_body(BO, A, B, C, D, E). 251decompose_assertion_body(BO, A, B, C, D, E, "") :- decompose_assertion_body(BO, A, B, C, D, E). 252 253decompose_assertion_body((A::BO), A, B, C, D, E) :- decompose_assertion_body(BO, B, C, D, E). 254decompose_assertion_body(BO, A, true, C, D, E) :- decompose_assertion_body(BO, A, C, D, E). 255 256valid_cp(C) :- \+ invalid_cp(C). 257 258invalid_cp(_/_).
267validate_body_sections(pred, _, _, _, _, [], []). 268validate_body_sections(prop, _, _, _, _, [], []). 269validate_body_sections(calls, Cp, Ca, Su, Gl, 270 [compatibility-Cp, postconditions-Su, globalprops-Gl], 271 [preconditions-Ca]). 272validate_body_sections(success, Cp, _, Su, Gl, 273 [compatibility-Cp, globalprops-Gl], 274 [postconditions-Su]). 275validate_body_sections(comp, Cp, _, Su, Gl, 276 [compatibiltiy-Cp, postconditions-Su], 277 [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
293assrt_type(Type) :-
294 validate_body_sections(Type, _, _, _, _, _, _),
295 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).
324assrt_status(check). 325assrt_status(true). 326assrt_status(false). 327assrt_status(debug). 328assrt_status(static). 329 330:- add_termpos(decompose_status_and_type_1(+,?,?,-)). 331:- add_termpos(decompose_status_and_type(+,?,?,-)). 332 333decompose_status_and_type_1(Assertions, check, AssrtType, UBody) :- 334 assrt_type(AssrtType), 335 Assertions =.. [AssrtType, UBody], 336 neck. 337decompose_status_and_type_1(Assertions, AssrtStatus, AssrtType, UBody) :- 338 assrt_type(AssrtType), 339 Assertions =.. [AssrtType, AssrtStatus, UBody], 340 neck. 341 342decompose_status_and_type(Assertions, APos, AssrtStatus, AssrtType, UBody, BPos) :- 343 cleanup_parentheses(APos, Pos), 344 decompose_status_and_type_1(Assertions, Pos, AssrtStatus, AssrtType, UBody, BPos), 345 assrt_status(AssrtStatus). 346 347cleanup_parentheses(Pos1, Pos) :- 348 nonvar(Pos1), 349 Pos1 = parentheses_term_position(_, _, Pos2), 350 !, 351 cleanup_parentheses(Pos2, Pos). 352cleanup_parentheses(Pos, Pos). 353 354% To Avoid attempts to execute asertions (must be declarations): 355 356:- assrt_type(Type), 357 member(Arity, [1, 2]), 358 neck, 359 export(Type/Arity). 360 361Assr :- 362 decompose_status_and_type_1(Assr, _, Status, Type, _, _), 363 functor(Assr, Type, Arity), 364 Body1 = ignore(nodirective_error_hook(Assr)), 365 ( Arity = 1 366 ->Body = Body1 367 ; Body = (assrt_status(Status), Body1) 368 ), 369 neck, 370 . 371 372is_decl_global(Head, M) :- 373 is_decl_global(Head, _, _, M). 374 375is_decl_global(Head, Status, Type, M) :- 376 forall(Head = HM:_, (var(HM);atom(HM))), 377 prop_asr(head, M:Head, _, Asr), 378 ( ( prop_asr(glob, metaprops:declaration(Status, _), _, Asr) 379 ; Status = true, 380 prop_asr(glob, metaprops:declaration(_), _, Asr) 381 ) 382 ->( prop_asr(glob, metaprops:global(Type, _), _, Asr) 383 ; Type = (pred) 384 ) 385 ; ( prop_asr(glob, metaprops:global(Type, _), _, Asr) 386 ; Type = (pred), 387 prop_asr(glob, metaprops:global(_), _, Asr) 388 ), 389 Status = true 390 ), 391 !. 392 393:- add_termpos(current_decomposed_assertion(+,?,?,?,?,?,?,?,?,-,?)). 394:- add_termpos(current_decomposed_assertion_1(+,?,?,?,-,?,?,-,?)). 395:- add_termpos(current_decomposed_assertion_2(+,?,?,?,-,?,?,-,?)). 396:- add_termpos(propdef(+,?,?,?)). 397:- add_termpos(merge_comments(-,-,+)). 398:- add_termpos(decompose_assertion_head_body(+,?,?,+,?,?,?,?,-,?)). 399:- add_termpos(decompose_assertion_head_body_(+,?,?,+,?,?,?,?,-,?)). 400:- add_termpos(decompose_assertion_head(+,?,?,+,-,?,?,?,?,?)). 401:- add_termpos(decompose_assertion_head_(+,?,?,+,-,?,?,?,?,?)). 402 403merge_comments("", C, C). 404merge_comments(C, "", C). 405merge_comments(C1, C2, [C1, C2]). 406 407current_decomposed_assertion(Assertions, PPos, M, Pred, Status, Type, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 408 current_decomposed_assertion_1(Assertions, PPos, M, Status, Type, BodyS, BSPos, Gl, Gl2, Co, CoPos, RPos), 409 decompose_assertion_head_body(BodyS, BSPos, M, Pred, true, _, Cp, Ca, Su, Gl2, Co, CoPos, RPos), 410 validate_body_sections(Type, Cp, Ca, Su, Gl, MustBeEmpty, MustNotBeEmpty), 411 maplist(report_must_be_empty(Type), MustBeEmpty), 412 maplist(report_must_not_be_empty(Type, RPos), MustNotBeEmpty). 413 414current_decomposed_assertion_1(Assertions, PPos, M, Status, Type, BodyS, BSPos, Gl1, Gl, Co, CoPos, RPos) :- 415 cleanup_parentheses(PPos, APos), 416 current_decomposed_assertion_2(Assertions, APos, M, Status, Type, BodyS, BSPos, Gl1, Gl, Co, CoPos, RPos). 417 418current_decomposed_assertion_2(AssertionsBGl, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 419 member(AssertionsBGl, [Assertions + BGl, 420 Assertions is BGl]), 421 necki, 422 propdef(BGl, M, Gl1, Gl2), 423 current_decomposed_assertion_1(Assertions, M, Status, Type, BodyS, Gl2, Gl, Co, RPos). 424current_decomposed_assertion_2(Assertions # Co2, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 425 !, 426 current_decomposed_assertion_1(Assertions, M, Status, Type, BodyS, Gl1, Gl, Co1, RPos), 427 once(merge_comments(Co1, Co2, Co)). 428current_decomposed_assertion_2(Assertions, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 429 ( is_decl_global(Assertions, DStatus, DType, M) 430 ->once(decompose_status_and_type_1(Term, DStatus, DType, Assertions)), 431 current_decomposed_assertion_2(Term, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) 432 ; decompose_status_and_type(Assertions, Status, Type, BodyS), 433 Gl = Gl1 434 ). 435 436report_must_be_empty(Type, Section-Props) :- 437 maplist(report_must_be_empty(Type, Section), Props). 438 439termpos_location(Pos, Loc) :- 440 ignore(source_location(File, Line)), 441 ( nonvar(File) 442 ->( nonvar(Pos) 443 ->Loc = file_term_position(File, Pos) 444 ; nonvar(Line) 445 ->Loc = file(File, Line, -1, _) 446 ; true 447 ) 448 ; true 449 ). 450 451report_must_be_empty(Type, Section, Prop-Pos) :- 452 termpos_location(Pos, Loc), 453 print_message( 454 warning, 455 at_location( 456 Loc, 457 format("In '~w' assertion, '~w' section, '~w' will be ignored", 458 [Type, Section, Prop]))). 459 460report_must_not_be_empty(Type, Pos, Section-Prop) :- 461 ( Prop = [] 462 ->termpos_location(Pos, Loc), 463 print_message( 464 warning, 465 at_location( 466 Loc, 467 format("In '~w' assertion, missing properties in '~w' section", 468 [Type, Section]))) 469 ; true 470 ). 471 472combine_arg_comp(N, Head, CompArgL, ArgPosL, PosL, BCp, PCp) :- 473 cleanup_parentheses(PCp, CompPos), 474 combine_arg_comp_(N, Head, CompArgL, ArgPosL, PosL, BCp, CompPos). 475 476combine_arg(Comp, Arg, Comp:Arg). 477 478combine_pos(CPos, APos, term_position(_, _, _, _, [CPos, APos])). 479 480combine_arg_comp_(_, Head, CompArgL, ArgPosL, PosL, CompL, list_position(_, _, CompPosL, _)) :- 481 is_list(CompL), 482 !, 483 Head =.. [_|ArgL], 484 maplist(combine_arg, CompL, ArgL, CompArgL), 485 maplist(combine_pos, CompPosL, ArgPosL, PosL). 486combine_arg_comp_(N, Head, CompArgL, ArgPosL, PosL, BCp, Pos) :- 487 combine_arg_comp_(N, Head, [], CompArgL, ArgPosL, [], PosL, BCp, Pos). 488 489combine_arg_comp_(N1, Head, CompArgL1, CompArgL, [APos|ArgPosL], PosL1, PosL, (H * Comp), term_position(_, _, _, _, [TCp, CPos])) :- 490 arg(N1, Head, Arg), 491 !, 492 succ(N, N1), 493 cleanup_parentheses(TCp, TPos), 494 combine_arg(Comp, Arg, CompArg), 495 combine_pos(CPos, APos, Pos), 496 combine_arg_comp_(N, Head, [CompArg|CompArgL1], CompArgL, ArgPosL, [Pos|PosL1], PosL, H, TPos). 497combine_arg_comp_(1, Head, CompArgL, [CompArg|CompArgL], [APos], PosL, [Pos|PosL], Comp, CPos) :- 498 arg(1, Head, Arg), 499 combine_arg(Comp, Arg, CompArg), 500 combine_pos(CPos, APos, Pos). 501 502% EMM: Support for grouped properties 503 504merge_props(BCp1, _, BCp, PCp, BCp, PCp) :- strip_module(BCp1, _, true). 505merge_props(BCp, PCp, BCp2, _, BCp, PCp) :- strip_module(BCp2, _, true). 506merge_props(BCp1, PCp1, BCp2, PCp2, (BCp1, BCp2), term_position(_, _, _, _, [PCp1, PCp2])). 507 508decompose_assertion_head_body(B, P1, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 509 cleanup_parentheses(P1, P), 510 decompose_assertion_head_body_(B, P, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 511 512decompose_assertion_head_body_(Var, _, _, _, _, _, _, _, _, _) :- 513 var(Var), 514 !, 515 fail. 516decompose_assertion_head_body_((B1, B2), M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 517 !, 518 ( decompose_assertion_head_body(B1, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 519 ; decompose_assertion_head_body(B2, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 520 ). 521decompose_assertion_head_body_([B1|B2], M, 522 Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 523 !, 524 ( decompose_assertion_head_body(B1, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 525 ; decompose_assertion_head_body(B2, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 526 ). 527decompose_assertion_head_body_(M:Body, CM, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 528 atom(M), 529 callable(Body), 530 !, 531 % Switching the body context does not implies switching the context of the 532 % compatibility properties, that is why CM should be preserved in the 533 % compatibility section: 534 decompose_assertion_head_body(Body, M, Pred, CM:BCp, Cp, Ca, Su, Gl, Co, RPos). 535decompose_assertion_head_body_([], _, _, _, _, _, _, _, _, _) :- 536 !, 537 fail. 538decompose_assertion_head_body_(Body, BPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 539 is_decl_global(Body, M), 540 Body =.. [F, Head|GArgL], 541 nonvar(Head), 542 !, 543 ( nonvar(BPos) 544 ->BPos = term_position(_, _, FF, FT, [HPos|PArgL]), 545 NPos = term_position(_, _, _, _, [HPos, term_position(_, _, FF, FT, [PArgL])]) 546 ; true 547 ), 548 BGl =.. [F|GArgL], 549 decompose_assertion_head_body(Head + BGl, NPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 550decompose_assertion_head_body_(Body, BPos, M, Pred, BCp2, PCp2, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 551 ( once(decompose_assertion_body(Body, BPos, BH1, PH1, BCp1, PCp1, 552 BCa, PCa, BSu, PSu, BGl, PGl, BCo, PCo)), 553 Body \= BH1 554 ->propdef(BGl, PGl, M, Gl, Gl1), 555 once(merge_props(BCp1, PCp1, BCp2, PCp2, BCp, PCp)), 556 decompose_assertion_head_body(BH1, PH1, M, Pred, BCp, PCp, Cp, Ca1, Su1, Gl1, BCo1, PCo1, RPos), 557 apropdef(Pred, M, BCa, PCa, Ca, Ca1), 558 apropdef(Pred, M, BSu, PSu, Su, Su1), 559 once(merge_comments(BCo1, PCo1, BCo, PCo, Co, CoPos)) 560 ; decompose_assertion_head(Body, BPos, M, Pred, BCp2, PCp2, BCp, PCp, Cp1, Ca, Su, Gl, RPos), 561 apropdef(Pred, M, BCp, PCp, Cp, Cp1), 562 Co = "" 563 ). 564 565decompose_assertion_head(Head, PPos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos) :- 566 cleanup_parentheses(PPos, Pos), 567 decompose_assertion_head_(Head, Pos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos). 568 569decompose_assertion_head_(M:H, _, P, BCp1, BCp, Cp, Ca, Su, Gl, RP) :- 570 atom(M), 571 !, 572 decompose_assertion_head(H, M, P, BCp1, BCp, Cp, Ca, Su, Gl, RP). 573decompose_assertion_head_(F/A, HPos, M, P, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 574 !, 575 atom(F), 576 integer(A), 577 functor(Head, F, A), 578 ( nonvar(HPos) 579 ->HPos = term_position(From, To, _, _, [FPos, _]), 580 ( nonvar(FPos) 581 ->arg(1, FPos, FFrom), 582 arg(2, FPos, FTo) 583 ; true 584 ) 585 ; true 586 ), 587 decompose_assertion_head_(Head, term_position(From, To, FFrom, FTo, _), M, P, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, Pos). 588decompose_assertion_head_(Head, HPos, M, M:Pred, BCp1, PCp1, BCp, _, Cp, Ca, Su, Gl, Pos) :- 589 compound(Head), 590 once(( BCp1 = CM:BCp2, 591 PCp1 = term_position(_, _, _, _, [_, PCp2]) 592 ; BCp1 = BCp2, 593 PCp1 = PCp2, 594 CM = M 595 )), 596 BCp2 \= true, 597 functor(Head, F, A), 598 combine_arg_comp(A, Head, CompArgL, ArgPosL, PosL, BCp2, PCp2), 599 !, 600 NHead =.. [F|CompArgL], 601 ( nonvar(HPos) 602 ->HPos = term_position(From, To, FFrom, FTo, ArgPosL) 603 ; true 604 ), 605 Pos = term_position(From, To, FFrom, FTo, PosL), 606 functor(Pred, F, A), 607 BCp = true, 608 decompose_args(PosL, 1, NHead, CM, Pred, Cp, Ca, Su, Gl). 609decompose_assertion_head_(Head, Pos, M, M:Pred, BCp, PCp, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 610 compound(Head), 611 !, 612 functor(Head, F, A), 613 functor(Pred, F, A), 614 ignore(Pos = term_position(_, _, _, _, PosL)), 615 decompose_args(PosL, 1, Head, M, Pred, Cp, Ca, Su, Gl). 616decompose_assertion_head_(Head, Pos, M, M:Head, BCp, PCp, BCp, PCp, [], [], [], [], Pos) :- 617 atom(Head). 618 619decompose_args([Pos|PosL], N1, Head, M, Pred, Cp1, Ca1, Su1, Gl1) :- 620 arg(N1, Head, HArg), 621 !, 622 resolve_types_modes(HArg, Pos, M, PArg, Cp1, Ca1, Su1, Gl1, Cp2, Ca2, Su2, Gl2), 623 arg(N1, Pred, PArg), 624 succ(N1, N), 625 decompose_args(PosL, N, Head, M, Pred, Cp2, Ca2, Su2, Gl2). 626decompose_args([], _, _, _, _, [], [], [], []). 627 628:- add_termpos(resolve_types_modes_(+,?,?,?,?,?,?,?,?,?,?)). 629:- add_termpos(do_modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 630:- add_termpos(modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 631:- add_termpos(do_propdef(+,?,?,?,?)). 632:- add_termpos(hpropdef(?,+,?,?,?)). 633 634resolve_types_modes(A, _, _, A, Cp, Ca, Su, Gl, Cp, Ca, Su, Gl) :- var(A), !. 635resolve_types_modes(A1, PPos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 636 cleanup_parentheses(PPos, Pos), 637 resolve_types_modes_(A1, Pos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl). 638 639resolve_types_modes_(A1:T, term_position(_, _, _, _, [PA1, PT]), M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 640 do_propdef(T, PT, M, A, Pr1, Pr2), 641 cleanup_parentheses(PA1, PA11), 642 do_modedef(A1, PA11, M, A, A2, PA2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 643 !, 644 do_propdef(A2, PA2, M, A, Pr2, Pr). 645resolve_types_modes_(A1, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 646 do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 647 do_propdef(A2, M, A, Pr1, Pr). 648 649do_propdef(A, _, A, Cp, Cp) :- var(A), !. 650do_propdef(A1, M, A, Cp1, Cp) :- 651 hpropdef(M, A1, A, Cp1, Cp). 652 653do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 654 nonvar(A1), 655 modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 656 !. 657do_modedef(A1, APos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 658 atom(A1), 659 A3 =.. [A1, A], 660 ( var(APos) -> true ; APos = From-To, Pos = term_position(From, To, From, To, [To-To]) ), 661 modedef(A3, Pos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 662 !. 663do_modedef(A1, From-To, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 664 integer(A1), 665 ( A1 >= 0 666 ->A3 = goal_in(A1, A) 667 ; A4 is -A1, 668 A3 = goal_go(A4, A) 669 ), 670 modedef(A3, term_position(From, To, From, From, [From-From, From-To]), M, A, A2, 671 PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 672 !. 673do_modedef(A1, PA1, _, _, A1, PA1, Cp1, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp). 674 675:- add_termpos(put_prop(+,?,?,?)). 676 677put_prop(_, Pos, Prop) --> [Prop-Pos]. 678 679% NOTE: In M. A. Covington 2009 paper, mode (=) was defined as input that may be 680% var on entry, but in this implementation is different in the sense that is 681% used to say that an input argument doesn't determine the output of the 682% predicate, in practice that means that the program could be refactorized to 683% avoid such input by placing in its body the method that determines its 684% value. For instance, in: 685% 686% :- true pred p(+,-). 687% :- true pred q(+,-). 688% :- true pred r(+,=,-). 689% p(A, B) :- q(A, X), r(A, X, B), ... . 690% q(A, A). 691% r(A, X, B) :- t(A, X, B), ... . 692 693% we can annotate r/3 as r(+,=,-) since the next refactoring over r/3 ---> r'/2 694% doesn't change the semantic of p/2: 695% 696% p(A, B) :- r'(A, B). 697% r'(A, B) :- q(A, X), t(A, X, B). 698 699% In practice this can be used by an optimizer that remembers tabled values of 700% r/3, knowing that we don't need to record the value of the second argument. 701 702:- add_termpos(cond_prop(+,?,?,?,?)). 703cond_prop(A, M, Prop, Pr1, Pr2) :- 704 ( var(A), var(Pr2) 705 ->put_prop(A, M:Prop, Pr1, Pr2) 706 ; Pr1 = Pr2 707 ). % A bit confuse hack, Pr1 comes instantiated to optimize the expression 708 709% Support for modes are hard-wired here: 710% ISO Modes 711modedef(-A, M, B, A, Cp, Ca2, Su1, Gl, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, M:var(B), Ca2, Ca). 712modedef(+A, M, B, A, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- cond_prop(A, M, nonvar(B), Ca1, Ca2). 713modedef(>A, M, B, A, Cp, Ca, Su1, Gl, Cp, Ca, Su, Gl, Su2, Su) :- cond_prop(A, M, nonvar(B), Su1, Su2). % Like - but A might be nonvar on entry 714modedef(?A, M, B, A, Cp2, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp) :- cond_prop(A, M, any( B), Cp2, Cp1). % Mode not specified. Added any/1 to track usage of this one 715% Less restrictive - uses further instantiated: 716% modedef(-(A), _, A, B, Pos, PA, Cp, Ca, Su1, [(globprops:fi(B))-Pos|Gl], Cp, Ca, Su, Gl, Su1, Su) :- Pos = term_position(_, _, _, _, [PA]). 717modedef(@A, _, B, A, Cp1, Ca, Su, Gl1, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, globprops:nfi(B), Gl1, Gl). % Not furher instantiated 718modedef(=A, _, B, A, Cp1, Ca, Su, Gl1, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, globprops:mve(B), Gl1, Gl). % Dependent input argument, may be var on entry (mve). 719 720% PlDoc (SWI) Modes 721modedef(:A1, Pos, M, B, A, PA, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- 722 Pos = term_position(From, To, FFrom, FTo, [PA1]), 723 % The first part of this check is not redundant if we forgot the meta_predicate declaration 724 ( var(A1), 725 var(Ca2) 726 ->put_prop(A, Pos, M:mod_qual(B), Ca1, Ca2), 727 A1 = A, 728 PA = PA1 729 ; Ca1 = Ca2, 730 A = M:mod_qual(A1, B), 731 PA = term_position(From, To, FFrom, FTo, [PA1, From-From]) 732 ). 733modedef(goal_in(N,A), M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:goal(N,B), Ca2, Ca1). 734modedef(goal_go(N,A), M, B, A, Cp, Ca, Su2, Gl, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, M:goal(N,B), Su2, Su1). 735modedef(!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) 736% Ciao Modes: 737modedef(in(A), M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:gnd(B), Ca2, Ca1). 738modedef(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). 739modedef(go(A), M, B, A, Cp1, Ca, Su2, Gl, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, M:gnd(B), Su2, Su). 740% Additional Modes (See Coding Guidelines for Prolog, Michael A. Covington, 2009): 741modedef(*A, M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:gnd(B), Ca2, Ca1). 742modedef(/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 743 744% nfi == not_further_inst 745% nsh == not_shared 746 747:- multifile prolog:error_message/3. 748 749prologerror_message(assertion(il_formed_assertion, Term)) --> 750 [ 'Il formed assertion, check term ~w'-[Term]]. 751 752hpropdef(M, A1, PA1, A, Cp1, Cp) :- 753 term_variables(A1, V), 754 ( member(X, V), 755 X==A 756 ->Cp1 = [(M:A1)-PA1|Cp] 757 ; aprops_arg(A1, M, A, PA1, Cp1, Cp) 758 ). 759 760apropdef_2(0, _, _, _, _) --> !, {fail}. 761apropdef_2(N, Head, M, A, PPos) --> 762 {cleanup_parentheses(PPos, Pos)}, 763 !, 764 apropdef_3(N, Head, M, A, Pos). 765 766apropdef_3(_, Head, M, AL, list_position(_, _, PosL, _)) --> 767 {is_list(AL)}, 768 !, 769 {Head =.. [_|VL]}, 770 foldl(hpropdef(M), AL, PosL, VL). 771apropdef_3(N, Head, M, A, Pos) --> 772 apropdef_4(N, Head, M, A, Pos). 773 774apropdef_4(N1, Head, M, (P * A), term_position(_, _, _, _, [PPos, APos])) --> 775 {arg(N1, Head, V)}, 776 !, 777 {succ(N, N1)}, 778 {cleanup_parentheses(PPos, Pos)}, 779 apropdef_4(N, Head, M, P, Pos), 780 hpropdef(M, A, APos, V). 781apropdef_4(1, Head, M, A, APos) --> 782 {arg(1, Head, V)}, 783 hpropdef(M, A, APos, V). 784 785apropdef(Var, _, _, _) --> {var(Var), !, fail}. 786apropdef(_:Head, M, A, APos) --> 787 {functor(Head, _, N)}, 788 apropdef_2(N, Head, M, A, APos), 789 !. 790apropdef(_, M, A, APos) --> propdef(A, APos, M). 791 792propdef(A, APos, M) --> props_args(A, M, push, APos). 793 794push(A, M, Pos) --> [(M:A)-Pos]. 795 796aprops_arg(A, M, V, PPos) --> 797 {cleanup_parentheses(PPos, Pos)}, 798 aprops_arg_(A, M, V, Pos). 799 800aprops_arg_({A}, M, V, brace_term_position(_, _, Pos)) --> !, aprops_args(A, M, V, Pos). 801aprops_arg_(A, M, V, Pos) --> aprops_args(A, M, V, Pos). 802 803aprops_args(A, M, V, Pos) --> props_args(A, M, prop_arg(V), Pos). 804 805:- meta_predicate props_args(, , , , , ). 806 807props_args(true, _, _, _) --> !, []. 808props_args(A, M, V, PPos) --> 809 {cleanup_parentheses(PPos, Pos)}, 810 !, 811 props_args_(A, M, V, Pos). 812 813props_args_((A, B), M, V, term_position(_, _, _, _, [PA, PB])) --> 814 !, 815 props_args(A, M, V, PA), 816 props_args(B, M, V, PB). 817props_args_((A; B), M, V, Pos) --> 818 !, 819 { Pos = term_position(_, _, _, _, [PA, PB]), 820 props_args(A, M, V, PA, P1, []), 821 pairs_keys(P1, ML1), 822 maplist(cleanup_mod(M), ML1, L1), 823 list_sequence(L1, C1), 824 props_args(B, M, V, PB, P2, []), 825 pairs_keys(P2, ML2), 826 maplist(cleanup_mod(M), ML2, L2), 827 list_sequence(L2, C2) 828 }, 829 [(M:(C1;C2))-Pos]. 830props_args_(M:A, _, V, term_position(_, _, _, _, [_, PA])) --> 831 {atom(M)}, 832 !, 833 props_args(A, M, V, PA). 834props_args_(A, M, V, Pos) --> call(V, A, M, Pos). 835 836cleanup_mod(M, M:C, C) :- !. 837cleanup_mod(_, MC, MC). 838 839prop_arg(V, A, M, Pos) --> 840 {add_arg(V, A, P, Pos, PPos)}, 841 [(M:P)-PPos]. 842 843expand_assertion_helper(Match, a(Match, Record, Pos), Record, Pos). 844 845expand_assertion(M, Dict, Decl, PPos, Records, RPos) :- 846 cleanup_parentheses(PPos, Pos), 847 !, 848 expand_assertion_(M, Dict, Decl, Pos, Records, RPos). 849 850expand_assertion_(_, Dict, M:Decl, term_position(_, _, _, _, [_, DPos]), 851 Records, RPos) :- 852 atom(M), 853 !, 854 expand_assertion(M, Dict, Decl, DPos, Records, RPos). 855expand_assertion_(M, Dict, doc(Key, Doc), 856 term_position(From, To, FFrom, FTo, [KPos, DPos]), 857 assertions:doc_db(Key, M, Doc, Dict), 858 term_position(0, 0, 0, 0, 859 [0-0, 860 term_position(From, To, FFrom, FTo, 861 [KPos, 0-0, DPos, 0-0 ])])) :- !. 862% Note: We MUST save the full location (File, HPos), because later we will not 863% have access to source_location/2, and this will fails for further created 864% clauses --EMM 865expand_assertion_(CM, Dict, Assertions, APos, Records, RPos) :- 866 Match=(Assertions-Dict), 867 findall(a(Match, Clause, HPos), 868 assertion_record_each(CM, Dict, Assertions, APos, Clause, HPos), 869 ARecords), 870 ARecords \= [], 871 maplist(expand_assertion_helper(Match), ARecords, Records, RPos).
file(File, Line, Pos, _), instead of the term
'$source_location'(File,Line):Clause
881assertion_record_each(CM, Dict, Assertions, APos, Clause, TermPos) :-
882 ignore(source_location(File, Line1)),
883 ( nonvar(File)
884 ->Loc = file(File, Line, Pos, _),
885 ( var(APos)
886 ->Line = Line1,
887 Pos = -1
888 ; true
889 )
890 ; true
891 ),
892 current_decomposed_assertion(Assertions, APos, CM, M:Head, Status, Type, CpL, CaL, SuL, GlL, Co, CoPos, HPos),
893 with_mutex('get_sequence_and_inc/1', get_sequence_and_inc(Count)),
894 term_variables(t(Co, CpL, CaL, SuL, GlL), ShareL),
895 atom_number(AIdx, Count),
896 Asr =.. [AIdx, M, Head|ShareL], % Asr also contains variable bindings. By
897 % convention, M is in the 1st position and
898 % Head in the 2nd, to facilitate work
899 ( Clause = assertions:asr_head_prop(Asr, M, Head, Status, Type, Dict, CM, Loc),
900 SubPos = HPos,
901 ( nonvar(SubPos)
902 ->arg(1, SubPos, From),
903 arg(2, SubPos, To),
904 TermPos = term_position(From, To, From, To,
905 [SubPos, 0-0, 0-0, 0-0, _, _, _])
906 ; true
907 )
908 ; Co \= "",
909 Clause = assertions:asr_comm(Asr, Co, Loc),
910 SubPos = CoPos,
911 ( nonvar(SubPos)
912 ->arg(1, SubPos, From),
913 arg(2, SubPos, To),
914 TermPos = term_position(From, To, From, To, [_, SubPos, _])
915 ; true
916 )
917 ; ( Clause = assertions:AClause,
918 member(AClause-PrL,
919 [asr_comp(Asr, PM, Pr, Loc)-CpL,
920 asr_call(Asr, PM, Pr, Loc)-CaL,
921 asr_succ(Asr, PM, Pr, Loc)-SuL
922 ]),
923 member(MPr-SubPos, PrL),
924 strip_module(MPr, PM, Pr)
925 ; Clause = assertions:asr_glob(Asr, PM, Pr, Loc),
926 member(MGl-GPos, GlL),
927 strip_module(MGl, PM, Gl),
928 add_arg(_, Gl, Pr, GPos, SubPos)
929 ;
930 once(( member(MGl-GPos, GlL),
931 member(Gl, [declaration, declaration(_)]),
932 strip_module(MGl, PM, Gl),
933 add_arg(_, Gl, Pr, GPos, _),
934 predicate_property(PM:Pr, implementation_module(metaprops)),
935 functor(Head, Op, 1)
936 )),
937 Clause = (:- '$export_ops'([op(1125, fy, Op)], PM, File))
938 ; member(MGl-_, GlL),
939 member(Gl, [declaration,
940 declaration(_),
941 global,
942 global(_)]),
943 strip_module(MGl, PM, Gl),
944 add_arg(_, Gl, Pr, _, _),
945 predicate_property(PM:Pr, implementation_module(metaprops))
946 ->functor(Head, Fn, N),
947 ( \+ predicate_property(M:Head, meta_predicate(_)),
948 functor(Meta, Fn, N),
949 Meta =.. [_|ArgL],
950 once(append(ArgL1, [0], ArgL)),
951 maplist(=(?), ArgL1),
952 Clause = (:- meta_predicate Meta)
953 )
954 ),
955 ( nonvar(SubPos)
956 ->arg(1, SubPos, From),
957 arg(2, SubPos, To),
958 TermPos = term_position(From, To, From, To, [_, 0-0, SubPos, _])
959 ; true
960 )
961 ),
962 ( var(Pos),
963 nonvar(File)
964 ->( nonvar(SubPos),
965 integer(From)
966 ->filepos_line(File, From, Line, Pos)
967 ; Line = Line1,
968 Pos = -1
969 )
970 ; true
971 ).978expand_assertion(Decl, DPos, Records, RPos) :- 979 '$current_source_module'(M), 980 expand_assertion(M, Dict, Decl, DPos, Records, RPos), 981 % Dict Must be assigned after expand_assertion/6 to avoid performance 982 % issues --EMM 983 ( nb_current('$variable_names', Dict) 984 ->true 985 ; Dict = [] 986 ). 987 988:- dynamic sequence/1. 989sequence(1). 990 991get_sequence_and_inc(S) :- 992 retract(sequence(S)), 993 succ(S, S2), 994 assertz(sequence(S2)). 995 996% ---------------------------------------------------------------------------- 997 998term_expansion_decl(Decl, PPos, Records, RPos) :- 999 nonvar(PPos), 1000 PPos = parentheses_term_position(_, _, Pos), 1001 !, 1002 term_expansion_decl(Decl, Pos, Records, RPos). 1003term_expansion_decl(Decl, PPos, Records, RPos) :- 1004 ( nonvar(PPos) 1005 ->PPos = term_position(_, _, _, _, [DPos]) 1006 ; true 1007 ), 1008 expand_assertion(Decl, DPos, Records, RPos). 1009 1010term_expansion((:- Decl), DPos, Records, RPos) :- 1011 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
*/