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