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(neck)). 58:- use_module(library(termpos)). 59:- use_module(library(lists)). 60:- use_module(library(list_sequence)). 61:- use_module(library(prolog_codewalk), []). 62:- init_expansors.
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 232% WARNING: Next is ambiguous if AB is a module-qualification, use [Module:Head] => D to deambiguate 233decompose_assertion_body((AB:C=>D ), AB, C, D, true) :- valid_cp(C). %110 234decompose_assertion_body((AB:C + E), AB, C, true, E ) :- valid_cp(C). %101 235decompose_assertion_body((AB:C is E), AB, C, true, E ) :- valid_cp(C). %101 236decompose_assertion_body((AB:C ), AB, C, true, true) :- valid_cp(C). %100 237decompose_assertion_body((AB =>D + E), AB, true, D, E ). %011 238decompose_assertion_body((AB =>D is E), AB, true, D, E ). %011 239decompose_assertion_body((AB =>D ), AB, true, D, true). %010 240decompose_assertion_body((AB + E), AB, true, true, E ). %001 241decompose_assertion_body((AB is E), AB, true, true, E ). %001 242decompose_assertion_body((AB ), AB, true, true, true). %000 243 244decompose_assertion_body((BO#F), A, B, C, D, E, F ) :- decompose_assertion_body(BO, A, B, C, D, E). 245decompose_assertion_body(BO, A, B, C, D, E, "") :- decompose_assertion_body(BO, A, B, C, D, E). 246 247decompose_assertion_body((A::BO), A, B, C, D, E) :- decompose_assertion_body(BO, B, C, D, E). 248decompose_assertion_body(BO, A, true, C, D, E) :- decompose_assertion_body(BO, A, C, D, E). 249 250valid_cp(C) :- \+ invalid_cp(C). 251 252invalid_cp(_/_).
261validate_body_sections(pred, _, _, _, _, [], []). 262validate_body_sections(prop, _, _, _, _, [], []). 263validate_body_sections(calls, Cp, Ca, Su, Gl, 264 [compatibility-Cp, postconditions-Su, globalprops-Gl], 265 [preconditions-Ca]). 266validate_body_sections(success, Cp, _, Su, Gl, 267 [compatibility-Cp, globalprops-Gl], 268 [postconditions-Su]). 269validate_body_sections(comp, Cp, _, Su, Gl, 270 [compatibiltiy-Cp, postconditions-Su], 271 [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
287assrt_type(Type) :-
288 validate_body_sections(Type, _, _, _, _, _, _),
289 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).
318assrt_status(check). 319assrt_status(true). 320assrt_status(false). 321assrt_status(debug). 322assrt_status(static). 323 324:- add_termpos(decompose_status_and_type_1(+,?,?,-)). 325:- add_termpos(decompose_status_and_type(+,?,?,-)). 326 327decompose_status_and_type_1(Assertions, check, AssrtType, UBody) :- 328 assrt_type(AssrtType), 329 Assertions =.. [AssrtType, UBody], 330 neck. 331decompose_status_and_type_1(Assertions, AssrtStatus, AssrtType, UBody) :- 332 assrt_type(AssrtType), 333 Assertions =.. [AssrtType, AssrtStatus, UBody], 334 neck. 335 336decompose_status_and_type(Assertions, APos, AssrtStatus, AssrtType, UBody, BPos) :- 337 cleanup_parentheses(APos, Pos), 338 decompose_status_and_type_1(Assertions, Pos, AssrtStatus, AssrtType, UBody, BPos), 339 assrt_status(AssrtStatus). 340 341cleanup_parentheses(Pos1, Pos) :- 342 nonvar(Pos1), 343 Pos1 = parentheses_term_position(_, _, Pos2), 344 !, 345 cleanup_parentheses(Pos2, Pos). 346cleanup_parentheses(Pos, Pos). 347 348% To Avoid attempts to execute asertions (must be declarations): 349 350:- assrt_type(Type), 351 member(Arity, [1, 2]), 352 neck, 353 export(Type/Arity). 354 355Assr :- 356 decompose_status_and_type_1(Assr, _, Status, Type, _, _), 357 functor(Assr, Type, Arity), 358 Body1 = ignore(nodirective_error_hook(Assr)), 359 ( Arity = 1 360 ->Body = Body1 361 ; Body = (assrt_status(Status), Body1) 362 ), 363 neck, 364 . 365 366is_decl_global(Head, M) :- 367 is_decl_global(Head, _, _, M). 368 369is_decl_global(Head, Status, Type, M) :- 370 forall(Head = HM:_, (var(HM);atom(HM))), 371 prop_asr(head, M:Head, _, Asr), 372 ( ( prop_asr(glob, metaprops:declaration(Status, _), _, Asr) 373 ; Status = true, 374 prop_asr(glob, metaprops:declaration(_), _, Asr) 375 ) 376 ->( prop_asr(glob, metaprops:global(Type, _), _, Asr) 377 ; Type = (pred) 378 ) 379 ; ( prop_asr(glob, metaprops:global(Type, _), _, Asr) 380 ; Type = (pred), 381 prop_asr(glob, metaprops:global(_), _, Asr) 382 ), 383 Status = true 384 ), 385 !. 386 387:- add_termpos(current_decomposed_assertion(+,?,?,?,?,?,?,?,?,-,?)). 388:- add_termpos(current_decomposed_assertion_1(+,?,?,?,-,?,?,-,?)). 389:- add_termpos(current_decomposed_assertion_2(+,?,?,?,-,?,?,-,?)). 390:- add_termpos(propdef(+,?,?,?)). 391:- add_termpos(merge_comments(-,-,+)). 392:- add_termpos(decompose_assertion_head_body(+,?,?,+,?,?,?,?,-,?)). 393:- add_termpos(decompose_assertion_head_body_(+,?,?,+,?,?,?,?,-,?)). 394:- add_termpos(decompose_assertion_head(+,?,?,+,-,?,?,?,?,?)). 395:- add_termpos(decompose_assertion_head_(+,?,?,+,-,?,?,?,?,?)). 396 397merge_comments("", C, C). 398merge_comments(C, "", C). 399merge_comments(C1, C2, [C1, C2]). 400 401current_decomposed_assertion(Assertions, PPos, M, Pred, Status, Type, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 402 current_decomposed_assertion_1(Assertions, PPos, M, Status, Type, BodyS, BSPos, Gl, Gl2, Co, CoPos, RPos), 403 decompose_assertion_head_body(BodyS, BSPos, M, Pred, true, _, Cp, Ca, Su, Gl2, Co, CoPos, RPos), 404 validate_body_sections(Type, Cp, Ca, Su, Gl, MustBeEmpty, MustNotBeEmpty), 405 maplist(report_must_be_empty(Type), MustBeEmpty), 406 maplist(report_must_not_be_empty(Type, RPos), MustNotBeEmpty). 407 408current_decomposed_assertion_1(Assertions, PPos, M, Status, Type, BodyS, BSPos, Gl1, Gl, Co, CoPos, RPos) :- 409 cleanup_parentheses(PPos, APos), 410 current_decomposed_assertion_2(Assertions, APos, M, Status, Type, BodyS, BSPos, Gl1, Gl, Co, CoPos, RPos). 411 412current_decomposed_assertion_2(AssertionsBGl, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 413 member(AssertionsBGl, [Assertions + BGl, 414 Assertions is BGl]), 415 necki, 416 propdef(BGl, M, Gl1, Gl2), 417 current_decomposed_assertion_1(Assertions, M, Status, Type, BodyS, Gl2, Gl, Co, RPos). 418current_decomposed_assertion_2(Assertions # Co2, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 419 !, 420 current_decomposed_assertion_1(Assertions, M, Status, Type, BodyS, Gl1, Gl, Co1, RPos), 421 once(merge_comments(Co1, Co2, Co)). 422current_decomposed_assertion_2(Assertions, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) :- 423 ( is_decl_global(Assertions, DStatus, DType, M) 424 ->once(decompose_status_and_type_1(Term, DStatus, DType, Assertions)), 425 current_decomposed_assertion_2(Term, M, Status, Type, BodyS, Gl1, Gl, Co, RPos) 426 ; decompose_status_and_type(Assertions, Status, Type, BodyS), 427 Gl = Gl1 428 ). 429 430report_must_be_empty(Type, Section-Props) :- 431 maplist(report_must_be_empty(Type, Section), Props). 432 433termpos_location(Pos, Loc) :- 434 ignore(source_location(File, Line)), 435 ( nonvar(File) 436 ->( nonvar(Pos) 437 ->Loc = file_term_position(File, Pos) 438 ; nonvar(Line) 439 ->Loc = file(File, Line, -1, _) 440 ; true 441 ) 442 ; true 443 ). 444 445report_must_be_empty(Type, Section, Prop-Pos) :- 446 termpos_location(Pos, Loc), 447 print_message( 448 warning, 449 at_location( 450 Loc, 451 format("In '~w' assertion, '~w' section, '~w' will be ignored", 452 [Type, Section, Prop]))). 453 454report_must_not_be_empty(Type, Pos, Section-Prop) :- 455 ( Prop = [] 456 ->termpos_location(Pos, Loc), 457 print_message( 458 warning, 459 at_location( 460 Loc, 461 format("In '~w' assertion, missing properties in '~w' section", 462 [Type, Section]))) 463 ; true 464 ). 465 466combine_pi_comp(N, Head, PosL1, PosL, BCp, PCp) :- 467 cleanup_parentheses(PCp, Pos), 468 combine_pi_comp_(N, Head, PosL1, PosL, BCp, Pos). 469 470combine_pi_comp_(N1, Head, PosL1, PosL, (H * P), term_position(_, _, _, _, [TPos, Pos])) :- 471 arg(N1, Head, P), 472 !, 473 succ(N, N1), 474 combine_pi_comp(N, Head, [Pos|PosL1], PosL, H, TPos). 475combine_pi_comp_(N, Head, PosL, [Pos|PosL], P, Pos) :- 476 arg(N, Head, P). 477 478% EMM: Support for grouped properties 479 480merge_props(BCp1, _, BCp, PCp, BCp, PCp) :- strip_module(BCp1, _, true). 481merge_props(BCp, PCp, BCp2, _, BCp, PCp) :- strip_module(BCp2, _, true). 482merge_props(BCp1, PCp1, BCp2, PCp2, (BCp1, BCp2), term_position(_, _, _, _, [PCp1, PCp2])). 483 484decompose_assertion_head_body(B, P1, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 485 cleanup_parentheses(P1, P), 486 decompose_assertion_head_body_(B, P, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 487 488decompose_assertion_head_body_(Var, _, _, _, _, _, _, _, _, _) :- 489 var(Var), 490 !, 491 fail. 492decompose_assertion_head_body_((B1, B2), M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 493 !, 494 ( decompose_assertion_head_body(B1, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 495 ; decompose_assertion_head_body(B2, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 496 ). 497decompose_assertion_head_body_([B1|B2], M, 498 Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 499 !, 500 ( decompose_assertion_head_body(B1, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 501 ; decompose_assertion_head_body(B2, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 502 ). 503decompose_assertion_head_body_(M:Body, CM, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 504 atom(M), 505 callable(Body), 506 !, 507 % Switching the body context does not implies switching the context of the 508 % compatibility properties, that is why CM should be preserved in the 509 % compatibility section: 510 decompose_assertion_head_body(Body, M, Pred, CM:BCp, Cp, Ca, Su, Gl, Co, RPos). 511decompose_assertion_head_body_([], _, _, _, _, _, _, _, _, _) :- 512 !, 513 fail. 514decompose_assertion_head_body_(Body, BPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 515 is_decl_global(Body, M), 516 Body =.. [F, Head|GArgL], 517 nonvar(Head), 518 !, 519 ( nonvar(BPos) 520 ->BPos = term_position(_, _, FF, FT, [HPos|PArgL]), 521 NPos = term_position(_, _, _, _, [HPos, term_position(_, _, FF, FT, [PArgL])]) 522 ; true 523 ), 524 BGl =.. [F|GArgL], 525 decompose_assertion_head_body(Head + BGl, NPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 526decompose_assertion_head_body_(Body, BPos, M, Pred, BCp2, PCp2, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 527 ( once(decompose_assertion_body(Body, BPos, BH1, PH1, BCp1, PCp1, 528 BCa, PCa, BSu, PSu, BGl, PGl, BCo, PCo)), 529 Body \= BH1 530 ->propdef(BGl, PGl, M, Gl, Gl1), 531 once(merge_props(BCp1, PCp1, BCp2, PCp2, BCp, PCp)), 532 decompose_assertion_head_body(BH1, PH1, M, Pred, BCp, PCp, Cp, Ca1, Su1, Gl1, BCo1, PCo1, RPos), 533 apropdef(Pred, M, BCa, PCa, Ca, Ca1), 534 apropdef(Pred, M, BSu, PSu, Su, Su1), 535 once(merge_comments(BCo1, PCo1, BCo, PCo, Co, CoPos)) 536 ; decompose_assertion_head(Body, BPos, M, Pred, BCp2, PCp2, BCp, PCp, Cp1, Ca, Su, Gl, RPos), 537 apropdef(Pred, M, BCp, PCp, Cp, Cp1), 538 Co = "" 539 ). 540 541decompose_assertion_head(Head, PPos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos) :- 542 cleanup_parentheses(PPos, Pos), 543 decompose_assertion_head_(Head, Pos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos). 544 545decompose_assertion_head_(M:H, _, P, BCp1, BCp, Cp, Ca, Su, Gl, RP) :- 546 atom(M), 547 !, 548 decompose_assertion_head(H, M, P, BCp1, BCp, Cp, Ca, Su, Gl, RP). 549decompose_assertion_head_(F/A, HPos, M, M:Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 550 !, 551 atom(F), 552 integer(A), 553 functor(Head, F, A), 554 ( once(( BCp1 = CM:BCp2, 555 PCp1 = term_position(_, _, _, _, [_, PCp2]) 556 ; BCp1 = BCp2, 557 PCp1 = PCp2, 558 CM = M 559 )), 560 BCp2 \= true, 561 combine_pi_comp(A, Head, [], PosL, BCp2, PCp2) 562 ->( nonvar(HPos) 563 ->HPos = term_position(From, To, _, _, [FPos, APos]), 564 ( nonvar(FPos) 565 ->arg(1, FPos, FFrom), 566 arg(2, FPos, FTo) 567 ; true 568 ) 569 ; true 570 ), 571 decompose_assertion_head_(Head, term_position(From, To, FFrom, FTo, PosL), CM, 572 CM:Pred, true, APos, BCp, PCp, Cp, Ca, Su, Gl, Pos) 573 ; Pred = Head, 574 Cp = [], 575 Ca = [], 576 Su = [], 577 Gl = [], 578 HPos = Pos, 579 BCp = BCp1, 580 PCp = PCp1 581 ). 582decompose_assertion_head_(Head, Pos, M, M:Pred, BCp, PCp, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 583 compound(Head), 584 !, 585 functor(Head, F, A), 586 functor(Pred, F, A), 587 ignore(Pos = term_position(_, _, _, _, PosL)), 588 decompose_args(PosL, 1, Head, M, Pred, Cp, Ca, Su, Gl). 589decompose_assertion_head_(Head, Pos, M, M:Head, BCp, PCp, BCp, PCp, [], [], [], [], Pos) :- 590 atom(Head). 591 592decompose_args([Pos|PosL], N1, Head, M, Pred, Cp1, Ca1, Su1, Gl1) :- 593 arg(N1, Head, HArg), 594 !, 595 resolve_types_modes(HArg, Pos, M, PArg, Cp1, Ca1, Su1, Gl1, Cp2, Ca2, Su2, Gl2), 596 arg(N1, Pred, PArg), 597 succ(N1, N), 598 decompose_args(PosL, N, Head, M, Pred, Cp2, Ca2, Su2, Gl2). 599decompose_args([], _, _, _, _, [], [], [], []). 600 601:- add_termpos(resolve_types_modes_(+,?,?,?,?,?,?,?,?,?,?)). 602:- add_termpos(do_modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 603:- add_termpos(modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 604:- add_termpos(do_propdef(+,?,?,?,?)). 605:- add_termpos(hpropdef(+,?,?,?,?)). 606 607resolve_types_modes(A, _, _, A, Cp, Ca, Su, Gl, Cp, Ca, Su, Gl) :- var(A), !. 608resolve_types_modes(A1, PPos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 609 cleanup_parentheses(PPos, Pos), 610 resolve_types_modes_(A1, Pos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl). 611 612resolve_types_modes_(A1:T, term_position(_, _, _, _, [PA1, PT]), M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 613 do_propdef(T, PT, M, A, Pr1, Pr2), 614 cleanup_parentheses(PA1, PA11), 615 do_modedef(A1, PA11, M, A, A2, PA2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 616 !, 617 do_propdef(A2, PA2, M, A, Pr2, Pr). 618resolve_types_modes_(A1, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 619 do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 620 do_propdef(A2, M, A, Pr1, Pr). 621 622do_propdef(A, _, A, Cp, Cp) :- var(A), !. 623do_propdef(A1, M, A, Cp1, Cp) :- 624 hpropdef(A1, M, A, Cp1, Cp). 625 626do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 627 nonvar(A1), 628 modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 629 !. 630do_modedef(A1, APos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 631 atom(A1), 632 A3 =.. [A1, A], 633 ( var(APos) -> true ; APos = From-To, Pos = term_position(From, To, From, To, [To-To]) ), 634 modedef(A3, Pos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 635 !. 636do_modedef(A1, From-To, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 637 integer(A1), 638 ( A1 >= 0 639 ->A3 = goal_in(A1, A) 640 ; A4 is -A1, 641 A3 = goal_go(A4, A) 642 ), 643 modedef(A3, term_position(From, To, From, From, [From-From, From-To]), M, A, A2, 644 PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 645 !. 646do_modedef(A1, PA1, _, _, A1, PA1, Cp1, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp). 647 648:- add_termpos(put_prop(+,?,?,?)). 649 650put_prop(_, Pos, Prop) --> [Prop-Pos]. 651 652% Support for modes are hard-wired here: 653% ISO Modes 654modedef(+A, M, B, A, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- 655 ( var(A), var(Ca2) 656 ->put_prop(A, M:nonvar(B), Ca1, Ca2) 657 ; Ca1 = Ca2 658 ). % A bit confuse hack, Ca1 comes instantiated to optimize the expression 659modedef(-A, M, B, A, Cp, Ca2, Su1, Gl, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, M:var(B), Ca2, Ca). 660% Less restrictive - uses further instantiated: 661% modedef(-(A), _, A, B, Pos, PA, Cp, Ca, Su1, [(globprops:fi(B))-Pos|Gl], Cp, Ca, Su, Gl, Su1, Su) :- Pos = term_position(_, _, _, _, [PA]). 662modedef(?A, _, _, A, Cp1, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp). 663modedef(@(A), _, B, A, Cp1, Ca, Su, Gl1, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, globprops:nfi(B), Gl1, Gl). 664% PlDoc (SWI) Modes 665modedef(:A1, Pos, M, B, A, PA, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- 666 Pos = term_position(From, To, FFrom, FTo, [PA1]), 667 % The first part of this check is not redundant if we forgot the meta_predicate declaration 668 ( var(A1), 669 var(Ca2) 670 ->put_prop(A, Pos, M:mod_qual(B), Ca1, Ca2), 671 A1 = A, 672 PA = PA1 673 ; Ca1 = Ca2, 674 A = M:mod_qual(A1, B), 675 PA = term_position(From, To, FFrom, FTo, [PA1, From-From]) 676 ). 677modedef(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). 678modedef(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). 679modedef(!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) 680% Ciao Modes: 681modedef(in(A), M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:ground(B), Ca2, Ca1). 682modedef(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). 683modedef(go(A), M, B, A, Cp1, Ca, Su2, Gl, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, M:gnd(B), Su2, Su). 684% Additional Modes (See Coding Guidelines for Prolog, Michael A. Covington, 2009): 685modedef(*A, M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:ground(B), Ca2, Ca1). 686modedef(=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 687modedef(/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 688modedef(>A, _, _, A, Cp, Ca, Su1, Gl, Cp, Ca, Su, Gl, Su1, Su). % Like output but A might be nonvar on entry 689 690% nfi == not_further_inst 691% nsh == not_shared 692 693:- multifile prolog:error_message/3. 694 695prologerror_message(assertion(il_formed_assertion, Term)) --> 696 [ 'Il formed assertion, check term ~w'-[Term]]. 697 698hpropdef(A1, PA1, M, A, Cp1, Cp) :- 699 term_variables(A1, V), 700 ( member(X, V), X==A -> 701 Cp1 = [(M:A1)-PA1|Cp] 702 ; aprops_arg(A1, M, A, PA1, Cp1, Cp) 703 ). 704 705apropdef_2(0, _, _, _, _) --> !, {fail}. 706apropdef_2(N, Head, M, A, PPos) --> 707 {cleanup_parentheses(PPos, Pos)}, 708 !, 709 apropdef_2_(N, Head, M, A, Pos). 710 711apropdef_2_(1, Head, M, A, APos) --> 712 {arg(1, Head, V)}, 713 !, 714 hpropdef(A, APos, M, V). 715apropdef_2_(N1, Head, M, (P * A), term_position(_, _, _, _, [PPos, APos])) --> 716 {arg(N1, Head, V)}, 717 !, 718 {succ(N, N1)}, 719 apropdef_2(N, Head, M, P, PPos), 720 hpropdef(A, APos, M, V). 721 722apropdef(Var, _, _, _) --> {var(Var), !, fail}. 723apropdef(_:Head, M, A, APos) --> 724 {functor(Head, _, N)}, 725 apropdef_2(N, Head, M, A, APos), 726 !. 727apropdef(_, M, A, APos) --> propdef(A, APos, M). 728 729propdef(A, APos, M) --> props_args(A, M, push, APos). 730 731push(A, M, Pos) --> [(M:A)-Pos]. 732 733aprops_arg(A, M, V, PPos) --> 734 {cleanup_parentheses(PPos, Pos)}, 735 aprops_arg_(A, M, V, Pos). 736 737aprops_arg_({A}, M, V, brace_term_position(_, _, Pos)) --> !, aprops_args(A, M, V, Pos). 738aprops_arg_(A, M, V, Pos) --> aprops_args(A, M, V, Pos). 739 740aprops_args(A, M, V, Pos) --> props_args(A, M, prop_arg(V), Pos). 741 742:- meta_predicate props_args(, , , , , ). 743 744props_args(true, _, _, _) --> !, []. 745props_args(A, M, V, PPos) --> 746 {cleanup_parentheses(PPos, Pos)}, 747 !, 748 props_args_(A, M, V, Pos). 749 750props_args_((A, B), M, V, term_position(_, _, _, _, [PA, PB])) --> 751 !, 752 props_args(A, M, V, PA), 753 props_args(B, M, V, PB). 754props_args_((A; B), M, V, Pos) --> 755 !, 756 { Pos = term_position(_, _, _, _, [PA, PB]), 757 props_args(A, M, V, PA, P1, []), 758 pairs_keys(P1, ML1), 759 maplist(cleanup_mod(M), ML1, L1), 760 list_sequence(L1, C1), 761 props_args(B, M, V, PB, P2, []), 762 pairs_keys(P2, ML2), 763 maplist(cleanup_mod(M), ML2, L2), 764 list_sequence(L2, C2) 765 }, 766 [(M:(C1;C2))-Pos]. 767props_args_(M:A, _, V, term_position(_, _, _, _, [_, PA])) --> 768 {atom(M)}, 769 !, 770 props_args(A, M, V, PA). 771props_args_(A, M, V, Pos) --> call(V, A, M, Pos). 772 773cleanup_mod(M, M:C, C) :- !. 774cleanup_mod(_, MC, MC). 775 776prop_arg(V, A, M, Pos) --> 777 {add_arg(V, A, P, Pos, PPos)}, 778 [(M:P)-PPos]. 779 780expand_assertion_helper(Match, a(Match, Record, Pos), Record, Pos). 781 782expand_assertion(M, Dict, Decl, PPos, Records, RPos) :- 783 cleanup_parentheses(PPos, Pos), 784 !, 785 expand_assertion_(M, Dict, Decl, Pos, Records, RPos). 786 787expand_assertion_(_, Dict, M:Decl, term_position(_, _, _, _, [_, DPos]), 788 Records, RPos) :- 789 atom(M), 790 !, 791 expand_assertion(M, Dict, Decl, DPos, Records, RPos). 792expand_assertion_(M, Dict, doc(Key, Doc), 793 term_position(From, To, FFrom, FTo, [KPos, DPos]), 794 assertions:doc_db(Key, M, Doc, Dict), 795 term_position(0, 0, 0, 0, 796 [0-0, 797 term_position(From, To, FFrom, FTo, 798 [KPos, 0-0, DPos, 0-0 ])])) :- !. 799% Note: We MUST save the full location (File, HPos), because later we will not 800% have access to source_location/2, and this will fails for further created 801% clauses --EMM 802expand_assertion_(CM, Dict, Assertions, APos, Records, RPos) :- 803 Match=(Assertions-Dict), 804 findall(a(Match, Clause, HPos), 805 assertion_record_each(CM, Dict, Assertions, APos, Clause, HPos), 806 ARecords), 807 ARecords \= [], 808 maplist(expand_assertion_helper(Match), ARecords, Records, RPos).
file(File, Line, Pos, _), instead of the term
'$source_location'(File,Line):Clause
818assertion_record_each(CM, Dict, Assertions, APos, Clause, TermPos) :-
819 ignore(source_location(File, Line1)),
820 ( nonvar(File)
821 ->Loc = file(File, Line, Pos, _),
822 ( var(APos)
823 ->Line = Line1,
824 Pos = -1
825 ; true
826 )
827 ; true
828 ),
829 current_decomposed_assertion(Assertions, APos, CM, M:Head, Status, Type, CpL, CaL, SuL, GlL, Co, CoPos, HPos),
830 with_mutex('get_sequence_and_inc/1', get_sequence_and_inc(Count)),
831 term_variables(t(Co, CpL, CaL, SuL, GlL), ShareL),
832 atom_number(AIdx, Count),
833 Asr =.. [AIdx, M, Head|ShareL], % Asr also contains variable bindings. By
834 % convention, M is in the 1st position and
835 % Head in the 2nd, to facilitate work
836 ( Clause = assertions:asr_head_prop(Asr, M, Head, Status, Type, Dict, CM, Loc),
837 SubPos = HPos,
838 ( nonvar(SubPos)
839 ->arg(1, SubPos, From),
840 arg(2, SubPos, To),
841 TermPos = term_position(From, To, From, To,
842 [SubPos, 0-0, 0-0, 0-0, _, _, _])
843 ; true
844 )
845 ; Co \= "",
846 Clause = assertions:asr_comm(Asr, Co, Loc),
847 SubPos = CoPos,
848 ( nonvar(SubPos)
849 ->arg(1, SubPos, From),
850 arg(2, SubPos, To),
851 TermPos = term_position(From, To, From, To, [_, SubPos, _])
852 ; true
853 )
854 ; ( Clause = assertions:AClause,
855 member(AClause-PrL,
856 [asr_comp(Asr, PM, Pr, Loc)-CpL,
857 asr_call(Asr, PM, Pr, Loc)-CaL,
858 asr_succ(Asr, PM, Pr, Loc)-SuL
859 ]),
860 member(MPr-SubPos, PrL),
861 strip_module(MPr, PM, Pr)
862 ; Clause = assertions:asr_glob(Asr, PM, Pr, Loc),
863 member(MGl-GPos, GlL),
864 strip_module(MGl, PM, Gl),
865 add_arg(_, Gl, Pr, GPos, SubPos)
866 ;
867 once(( member(MGl-GPos, GlL),
868 member(Gl, [declaration, declaration(_)]),
869 strip_module(MGl, PM, Gl),
870 add_arg(_, Gl, Pr, GPos, _),
871 predicate_property(PM:Pr, implementation_module(metaprops)),
872 functor(Head, Op, 1)
873 )),
874 Clause = (:- '$export_ops'([op(1125, fy, Op)], PM, File))
875 ; member(MGl-_, GlL),
876 member(Gl, [declaration,
877 declaration(_),
878 global,
879 global(_)]),
880 strip_module(MGl, PM, Gl),
881 add_arg(_, Gl, Pr, _, _),
882 predicate_property(PM:Pr, implementation_module(metaprops))
883 ->functor(Head, Fn, N),
884 ( \+ predicate_property(M:Head, meta_predicate(_)),
885 functor(Meta, Fn, N),
886 Meta =.. [_|ArgL],
887 once(append(ArgL1, [0], ArgL)),
888 maplist(=(?), ArgL1),
889 Clause = (:- meta_predicate Meta)
890 )
891 ),
892 ( nonvar(SubPos)
893 ->arg(1, SubPos, From),
894 arg(2, SubPos, To),
895 TermPos = term_position(From, To, From, To, [_, 0-0, SubPos, _])
896 ; true
897 )
898 ),
899 ( var(Pos),
900 nonvar(File)
901 ->( nonvar(SubPos),
902 integer(From)
903 ->filepos_line(File, From, Line, Pos)
904 ; Line = Line1,
905 Pos = -1
906 )
907 ; true
908 ).915expand_assertion(Decl, DPos, Records, RPos) :- 916 '$current_source_module'(M), 917 expand_assertion(M, Dict, Decl, DPos, Records, RPos), 918 % Dict Must be assigned after expand_assertion/6 to avoid performance 919 % issues --EMM 920 ( nb_current('$variable_names', Dict) 921 ->true 922 ; Dict = [] 923 ). 924 925:- dynamic sequence/1. 926sequence(1). 927 928get_sequence_and_inc(S) :- 929 retract(sequence(S)), 930 succ(S, S2), 931 assertz(sequence(S2)). 932 933% ---------------------------------------------------------------------------- 934 935term_expansion_decl(Decl, PPos, Records, RPos) :- 936 nonvar(PPos), 937 PPos = parentheses_term_position(_, _, Pos), 938 !, 939 term_expansion_decl(Decl, Pos, Records, RPos). 940term_expansion_decl(Decl, PPos, Records, RPos) :- 941 ( nonvar(PPos) 942 ->PPos = term_position(_, _, _, _, [DPos]) 943 ; true 944 ), 945 expand_assertion(Decl, DPos, Records, RPos). 946 947term_expansion((:- Decl), DPos, Records, RPos) :- 948 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
*/