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_arg_comp(N, Head, CompArgL, ArgPosL, PosL, BCp, PCp) :- 467 cleanup_parentheses(PCp, CompPos), 468 combine_arg_comp_(N, Head, CompArgL, ArgPosL, PosL, BCp, CompPos). 469 470combine_arg(Comp, Arg, Comp:Arg). 471 472combine_pos(CPos, APos, term_position(_, _, _, _, [CPos, APos])). 473 474combine_arg_comp_(_, Head, CompArgL, ArgPosL, PosL, CompL, list_position(_, _, CompPosL, _)) :- 475 is_list(CompL), 476 !, 477 Head =.. [_|ArgL], 478 maplist(combine_arg, CompL, ArgL, CompArgL), 479 maplist(combine_pos, CompPosL, ArgPosL, PosL). 480combine_arg_comp_(N, Head, CompArgL, ArgPosL, PosL, BCp, Pos) :- 481 combine_arg_comp_(N, Head, [], CompArgL, ArgPosL, [], PosL, BCp, Pos). 482 483combine_arg_comp_(N1, Head, CompArgL1, CompArgL, [APos|ArgPosL], PosL1, PosL, (H * Comp), term_position(_, _, _, _, [TCp, CPos])) :- 484 arg(N1, Head, Arg), 485 !, 486 succ(N, N1), 487 cleanup_parentheses(TCp, TPos), 488 combine_arg(Comp, Arg, CompArg), 489 combine_pos(CPos, APos, Pos), 490 combine_arg_comp_(N, Head, [CompArg|CompArgL1], CompArgL, ArgPosL, [Pos|PosL1], PosL, H, TPos). 491combine_arg_comp_(1, Head, CompArgL, [CompArg|CompArgL], [APos], PosL, [Pos|PosL], Comp, CPos) :- 492 arg(1, Head, Arg), 493 combine_arg(Comp, Arg, CompArg), 494 combine_pos(CPos, APos, Pos). 495 496% EMM: Support for grouped properties 497 498merge_props(BCp1, _, BCp, PCp, BCp, PCp) :- strip_module(BCp1, _, true). 499merge_props(BCp, PCp, BCp2, _, BCp, PCp) :- strip_module(BCp2, _, true). 500merge_props(BCp1, PCp1, BCp2, PCp2, (BCp1, BCp2), term_position(_, _, _, _, [PCp1, PCp2])). 501 502decompose_assertion_head_body(B, P1, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 503 cleanup_parentheses(P1, P), 504 decompose_assertion_head_body_(B, P, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 505 506decompose_assertion_head_body_(Var, _, _, _, _, _, _, _, _, _) :- 507 var(Var), 508 !, 509 fail. 510decompose_assertion_head_body_((B1, B2), M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 511 !, 512 ( decompose_assertion_head_body(B1, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 513 ; decompose_assertion_head_body(B2, M, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) 514 ). 515decompose_assertion_head_body_([B1|B2], M, 516 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_(M:Body, CM, Pred, BCp, Cp, Ca, Su, Gl, Co, RPos) :- 522 atom(M), 523 callable(Body), 524 !, 525 % Switching the body context does not implies switching the context of the 526 % compatibility properties, that is why CM should be preserved in the 527 % compatibility section: 528 decompose_assertion_head_body(Body, M, Pred, CM:BCp, Cp, Ca, Su, Gl, Co, RPos). 529decompose_assertion_head_body_([], _, _, _, _, _, _, _, _, _) :- 530 !, 531 fail. 532decompose_assertion_head_body_(Body, BPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 533 is_decl_global(Body, M), 534 Body =.. [F, Head|GArgL], 535 nonvar(Head), 536 !, 537 ( nonvar(BPos) 538 ->BPos = term_position(_, _, FF, FT, [HPos|PArgL]), 539 NPos = term_position(_, _, _, _, [HPos, term_position(_, _, FF, FT, [PArgL])]) 540 ; true 541 ), 542 BGl =.. [F|GArgL], 543 decompose_assertion_head_body(Head + BGl, NPos, M, Pred, BCp, PCp, Cp, Ca, Su, Gl, Co, CoPos, RPos). 544decompose_assertion_head_body_(Body, BPos, M, Pred, BCp2, PCp2, Cp, Ca, Su, Gl, Co, CoPos, RPos) :- 545 ( once(decompose_assertion_body(Body, BPos, BH1, PH1, BCp1, PCp1, 546 BCa, PCa, BSu, PSu, BGl, PGl, BCo, PCo)), 547 Body \= BH1 548 ->propdef(BGl, PGl, M, Gl, Gl1), 549 once(merge_props(BCp1, PCp1, BCp2, PCp2, BCp, PCp)), 550 decompose_assertion_head_body(BH1, PH1, M, Pred, BCp, PCp, Cp, Ca1, Su1, Gl1, BCo1, PCo1, RPos), 551 apropdef(Pred, M, BCa, PCa, Ca, Ca1), 552 apropdef(Pred, M, BSu, PSu, Su, Su1), 553 once(merge_comments(BCo1, PCo1, BCo, PCo, Co, CoPos)) 554 ; decompose_assertion_head(Body, BPos, M, Pred, BCp2, PCp2, BCp, PCp, Cp1, Ca, Su, Gl, RPos), 555 apropdef(Pred, M, BCp, PCp, Cp, Cp1), 556 Co = "" 557 ). 558 559decompose_assertion_head(Head, PPos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos) :- 560 cleanup_parentheses(PPos, Pos), 561 decompose_assertion_head_(Head, Pos, M, Pred, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, HPos). 562 563decompose_assertion_head_(M:H, _, P, BCp1, BCp, Cp, Ca, Su, Gl, RP) :- 564 atom(M), 565 !, 566 decompose_assertion_head(H, M, P, BCp1, BCp, Cp, Ca, Su, Gl, RP). 567decompose_assertion_head_(F/A, HPos, M, P, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 568 !, 569 atom(F), 570 integer(A), 571 functor(Head, F, A), 572 ( nonvar(HPos) 573 ->HPos = term_position(From, To, _, _, [FPos, _]), 574 ( nonvar(FPos) 575 ->arg(1, FPos, FFrom), 576 arg(2, FPos, FTo) 577 ; true 578 ) 579 ; true 580 ), 581 decompose_assertion_head_(Head, term_position(From, To, FFrom, FTo, _), M, P, BCp1, PCp1, BCp, PCp, Cp, Ca, Su, Gl, Pos). 582decompose_assertion_head_(Head, HPos, M, M:Pred, BCp1, PCp1, BCp, _, Cp, Ca, Su, Gl, Pos) :- 583 compound(Head), 584 once(( BCp1 = CM:BCp2, 585 PCp1 = term_position(_, _, _, _, [_, PCp2]) 586 ; BCp1 = BCp2, 587 PCp1 = PCp2, 588 CM = M 589 )), 590 BCp2 \= true, 591 functor(Head, F, A), 592 combine_arg_comp(A, Head, CompArgL, ArgPosL, PosL, BCp2, PCp2), 593 !, 594 NHead =.. [F|CompArgL], 595 ( nonvar(HPos) 596 ->HPos = term_position(From, To, FFrom, FTo, ArgPosL) 597 ; true 598 ), 599 Pos = term_position(From, To, FFrom, FTo, PosL), 600 functor(Pred, F, A), 601 BCp = true, 602 decompose_args(PosL, 1, NHead, CM, Pred, Cp, Ca, Su, Gl). 603decompose_assertion_head_(Head, Pos, M, M:Pred, BCp, PCp, BCp, PCp, Cp, Ca, Su, Gl, Pos) :- 604 compound(Head), 605 !, 606 functor(Head, F, A), 607 functor(Pred, F, A), 608 ignore(Pos = term_position(_, _, _, _, PosL)), 609 decompose_args(PosL, 1, Head, M, Pred, Cp, Ca, Su, Gl). 610decompose_assertion_head_(Head, Pos, M, M:Head, BCp, PCp, BCp, PCp, [], [], [], [], Pos) :- 611 atom(Head). 612 613decompose_args([Pos|PosL], N1, Head, M, Pred, Cp1, Ca1, Su1, Gl1) :- 614 arg(N1, Head, HArg), 615 !, 616 resolve_types_modes(HArg, Pos, M, PArg, Cp1, Ca1, Su1, Gl1, Cp2, Ca2, Su2, Gl2), 617 arg(N1, Pred, PArg), 618 succ(N1, N), 619 decompose_args(PosL, N, Head, M, Pred, Cp2, Ca2, Su2, Gl2). 620decompose_args([], _, _, _, _, [], [], [], []). 621 622:- add_termpos(resolve_types_modes_(+,?,?,?,?,?,?,?,?,?,?)). 623:- add_termpos(do_modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 624:- add_termpos(modedef(+,?,?,-,?,?,?,?,?,?,?,?,?,?)). 625:- add_termpos(do_propdef(+,?,?,?,?)). 626:- add_termpos(hpropdef(?,+,?,?,?)). 627 628resolve_types_modes(A, _, _, A, Cp, Ca, Su, Gl, Cp, Ca, Su, Gl) :- var(A), !. 629resolve_types_modes(A1, PPos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 630 cleanup_parentheses(PPos, Pos), 631 resolve_types_modes_(A1, Pos, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl). 632 633resolve_types_modes_(A1:T, term_position(_, _, _, _, [PA1, PT]), M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 634 do_propdef(T, PT, M, A, Pr1, Pr2), 635 cleanup_parentheses(PA1, PA11), 636 do_modedef(A1, PA11, M, A, A2, PA2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 637 !, 638 do_propdef(A2, PA2, M, A, Pr2, Pr). 639resolve_types_modes_(A1, M, A, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl) :- 640 do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 641 do_propdef(A2, M, A, Pr1, Pr). 642 643do_propdef(A, _, A, Cp, Cp) :- var(A), !. 644do_propdef(A1, M, A, Cp1, Cp) :- 645 hpropdef(M, A1, A, Cp1, Cp). 646 647do_modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 648 nonvar(A1), 649 modedef(A1, M, A, A2, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 650 !. 651do_modedef(A1, APos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 652 atom(A1), 653 A3 =.. [A1, A], 654 ( var(APos) -> true ; APos = From-To, Pos = term_position(From, To, From, To, [To-To]) ), 655 modedef(A3, Pos, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 656 !. 657do_modedef(A1, From-To, M, A, A2, PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr) :- 658 integer(A1), 659 ( A1 >= 0 660 ->A3 = goal_in(A1, A) 661 ; A4 is -A1, 662 A3 = goal_go(A4, A) 663 ), 664 modedef(A3, term_position(From, To, From, From, [From-From, From-To]), M, A, A2, 665 PA1, Cp1, Ca1, Su1, Gl1, Cp, Ca, Su, Gl, Pr1, Pr), 666 !. 667do_modedef(A1, PA1, _, _, A1, PA1, Cp1, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp1, Cp). 668 669:- add_termpos(put_prop(+,?,?,?)). 670 671put_prop(_, Pos, Prop) --> [Prop-Pos]. 672 673% NOTE: In M. A. Covington 2009 paper, mode (=) was defined as input that may be 674% var on entry, but in this implementation is different in the sense that is 675% used to say that an input argument doesn't determine the output of the 676% predicate, in practice that means that the program could be refactorized to 677% avoid such input by placing in its body the method that determines its 678% value. For instance, in: 679% 680% :- true pred p(+,-). 681% :- true pred q(+,-). 682% :- true pred r(+,=,-). 683% p(A, B) :- q(A, X), r(A, X, B), ... . 684% q(A, A). 685% r(A, X, B) :- t(A, X, B), ... . 686 687% we can annotate r/3 as r(+,=,-) since the next refactoring over r/3 ---> r'/2 688% doesn't change the semantic of p/2: 689% 690% p(A, B) :- r'(A, B). 691% r'(A, B) :- q(A, X), t(A, X, B). 692 693% In practice this can be used by an optimizer that remembers tabled values of 694% r/3, knowing that we don't need to record the value of the second argument. 695 696:- add_termpos(cond_prop(+,?,?,?,?)). 697cond_prop(A, M, Prop, Pr1, Pr2) :- 698 ( var(A), var(Pr2) 699 ->put_prop(A, M:Prop, Pr1, Pr2) 700 ; Pr1 = Pr2 701 ). % A bit confuse hack, Pr1 comes instantiated to optimize the expression 702 703% Support for modes are hard-wired here: 704% ISO Modes 705modedef(-A, M, B, A, Cp, Ca2, Su1, Gl, Cp, Ca, Su, Gl, Su1, Su) :- put_prop(A, M:var(B), Ca2, Ca). 706modedef(+A, M, B, A, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- cond_prop(A, M, nonvar(B), Ca1, Ca2). 707modedef(>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 708modedef(?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 709% Less restrictive - uses further instantiated: 710% modedef(-(A), _, A, B, Pos, PA, Cp, Ca, Su1, [(globprops:fi(B))-Pos|Gl], Cp, Ca, Su, Gl, Su1, Su) :- Pos = term_position(_, _, _, _, [PA]). 711modedef(@A, _, B, A, Cp1, Ca, Su, Gl1, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, globprops:nfi(B), Gl1, Gl). % Not furher instantiated 712modedef(=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). 713 714% PlDoc (SWI) Modes 715modedef(:A1, Pos, M, B, A, PA, Cp, Ca1, Su, Gl, Cp, Ca, Su, Gl, Ca2, Ca) :- 716 Pos = term_position(From, To, FFrom, FTo, [PA1]), 717 % The first part of this check is not redundant if we forgot the meta_predicate declaration 718 ( var(A1), 719 var(Ca2) 720 ->put_prop(A, Pos, M:mod_qual(B), Ca1, Ca2), 721 A1 = A, 722 PA = PA1 723 ; Ca1 = Ca2, 724 A = M:mod_qual(A1, B), 725 PA = term_position(From, To, FFrom, FTo, [PA1, From-From]) 726 ). 727modedef(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). 728modedef(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). 729modedef(!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) 730% Ciao Modes: 731modedef(in(A), M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:gnd(B), Ca2, Ca1). 732modedef(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). 733modedef(go(A), M, B, A, Cp1, Ca, Su2, Gl, Cp, Ca, Su, Gl, Cp1, Cp) :- put_prop(A, M:gnd(B), Su2, Su). 734% Additional Modes (See Coding Guidelines for Prolog, Michael A. Covington, 2009): 735modedef(*A, M, B, A, Cp, Ca2, Su, Gl, Cp, Ca, Su, Gl, Ca1, Ca) :- put_prop(A, M:gnd(B), Ca2, Ca1). 736modedef(/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 737 738% nfi == not_further_inst 739% nsh == not_shared 740 741:- multifile prolog:error_message/3. 742 743prologerror_message(assertion(il_formed_assertion, Term)) --> 744 [ 'Il formed assertion, check term ~w'-[Term]]. 745 746hpropdef(M, A1, PA1, A, Cp1, Cp) :- 747 term_variables(A1, V), 748 ( member(X, V), 749 X==A 750 ->Cp1 = [(M:A1)-PA1|Cp] 751 ; aprops_arg(A1, M, A, PA1, Cp1, Cp) 752 ). 753 754apropdef_2(0, _, _, _, _) --> !, {fail}. 755apropdef_2(N, Head, M, A, PPos) --> 756 {cleanup_parentheses(PPos, Pos)}, 757 !, 758 apropdef_3(N, Head, M, A, Pos). 759 760apropdef_3(_, Head, M, AL, list_position(_, _, PosL, _)) --> 761 {is_list(AL)}, 762 !, 763 {Head =.. [_|VL]}, 764 foldl(hpropdef(M), AL, PosL, VL). 765apropdef_3(N, Head, M, A, Pos) --> 766 apropdef_4(N, Head, M, A, Pos). 767 768apropdef_4(N1, Head, M, (P * A), term_position(_, _, _, _, [PPos, APos])) --> 769 {arg(N1, Head, V)}, 770 !, 771 {succ(N, N1)}, 772 {cleanup_parentheses(PPos, Pos)}, 773 apropdef_4(N, Head, M, P, Pos), 774 hpropdef(M, A, APos, V). 775apropdef_4(1, Head, M, A, APos) --> 776 {arg(1, Head, V)}, 777 hpropdef(M, A, APos, V). 778 779apropdef(Var, _, _, _) --> {var(Var), !, fail}. 780apropdef(_:Head, M, A, APos) --> 781 {functor(Head, _, N)}, 782 apropdef_2(N, Head, M, A, APos), 783 !. 784apropdef(_, M, A, APos) --> propdef(A, APos, M). 785 786propdef(A, APos, M) --> props_args(A, M, push, APos). 787 788push(A, M, Pos) --> [(M:A)-Pos]. 789 790aprops_arg(A, M, V, PPos) --> 791 {cleanup_parentheses(PPos, Pos)}, 792 aprops_arg_(A, M, V, Pos). 793 794aprops_arg_({A}, M, V, brace_term_position(_, _, Pos)) --> !, aprops_args(A, M, V, Pos). 795aprops_arg_(A, M, V, Pos) --> aprops_args(A, M, V, Pos). 796 797aprops_args(A, M, V, Pos) --> props_args(A, M, prop_arg(V), Pos). 798 799:- meta_predicate props_args(, , , , , ). 800 801props_args(true, _, _, _) --> !, []. 802props_args(A, M, V, PPos) --> 803 {cleanup_parentheses(PPos, Pos)}, 804 !, 805 props_args_(A, M, V, Pos). 806 807props_args_((A, B), M, V, term_position(_, _, _, _, [PA, PB])) --> 808 !, 809 props_args(A, M, V, PA), 810 props_args(B, M, V, PB). 811props_args_((A; B), M, V, Pos) --> 812 !, 813 { Pos = term_position(_, _, _, _, [PA, PB]), 814 props_args(A, M, V, PA, P1, []), 815 pairs_keys(P1, ML1), 816 maplist(cleanup_mod(M), ML1, L1), 817 list_sequence(L1, C1), 818 props_args(B, M, V, PB, P2, []), 819 pairs_keys(P2, ML2), 820 maplist(cleanup_mod(M), ML2, L2), 821 list_sequence(L2, C2) 822 }, 823 [(M:(C1;C2))-Pos]. 824props_args_(M:A, _, V, term_position(_, _, _, _, [_, PA])) --> 825 {atom(M)}, 826 !, 827 props_args(A, M, V, PA). 828props_args_(A, M, V, Pos) --> call(V, A, M, Pos). 829 830cleanup_mod(M, M:C, C) :- !. 831cleanup_mod(_, MC, MC). 832 833prop_arg(V, A, M, Pos) --> 834 {add_arg(V, A, P, Pos, PPos)}, 835 [(M:P)-PPos]. 836 837expand_assertion_helper(Match, a(Match, Record, Pos), Record, Pos). 838 839expand_assertion(M, Dict, Decl, PPos, Records, RPos) :- 840 cleanup_parentheses(PPos, Pos), 841 !, 842 expand_assertion_(M, Dict, Decl, Pos, Records, RPos). 843 844expand_assertion_(_, Dict, M:Decl, term_position(_, _, _, _, [_, DPos]), 845 Records, RPos) :- 846 atom(M), 847 !, 848 expand_assertion(M, Dict, Decl, DPos, Records, RPos). 849expand_assertion_(M, Dict, doc(Key, Doc), 850 term_position(From, To, FFrom, FTo, [KPos, DPos]), 851 assertions:doc_db(Key, M, Doc, Dict), 852 term_position(0, 0, 0, 0, 853 [0-0, 854 term_position(From, To, FFrom, FTo, 855 [KPos, 0-0, DPos, 0-0 ])])) :- !. 856% Note: We MUST save the full location (File, HPos), because later we will not 857% have access to source_location/2, and this will fails for further created 858% clauses --EMM 859expand_assertion_(CM, Dict, Assertions, APos, Records, RPos) :- 860 Match=(Assertions-Dict), 861 findall(a(Match, Clause, HPos), 862 assertion_record_each(CM, Dict, Assertions, APos, Clause, HPos), 863 ARecords), 864 ARecords \= [], 865 maplist(expand_assertion_helper(Match), ARecords, Records, RPos).
file(File, Line, Pos, _), instead of the term
'$source_location'(File,Line):Clause
875assertion_record_each(CM, Dict, Assertions, APos, Clause, TermPos) :-
876 ignore(source_location(File, Line1)),
877 ( nonvar(File)
878 ->Loc = file(File, Line, Pos, _),
879 ( var(APos)
880 ->Line = Line1,
881 Pos = -1
882 ; true
883 )
884 ; true
885 ),
886 current_decomposed_assertion(Assertions, APos, CM, M:Head, Status, Type, CpL, CaL, SuL, GlL, Co, CoPos, HPos),
887 with_mutex('get_sequence_and_inc/1', get_sequence_and_inc(Count)),
888 term_variables(t(Co, CpL, CaL, SuL, GlL), ShareL),
889 atom_number(AIdx, Count),
890 Asr =.. [AIdx, M, Head|ShareL], % Asr also contains variable bindings. By
891 % convention, M is in the 1st position and
892 % Head in the 2nd, to facilitate work
893 ( Clause = assertions:asr_head_prop(Asr, M, Head, Status, Type, Dict, CM, Loc),
894 SubPos = HPos,
895 ( nonvar(SubPos)
896 ->arg(1, SubPos, From),
897 arg(2, SubPos, To),
898 TermPos = term_position(From, To, From, To,
899 [SubPos, 0-0, 0-0, 0-0, _, _, _])
900 ; true
901 )
902 ; Co \= "",
903 Clause = assertions:asr_comm(Asr, Co, Loc),
904 SubPos = CoPos,
905 ( nonvar(SubPos)
906 ->arg(1, SubPos, From),
907 arg(2, SubPos, To),
908 TermPos = term_position(From, To, From, To, [_, SubPos, _])
909 ; true
910 )
911 ; ( Clause = assertions:AClause,
912 member(AClause-PrL,
913 [asr_comp(Asr, PM, Pr, Loc)-CpL,
914 asr_call(Asr, PM, Pr, Loc)-CaL,
915 asr_succ(Asr, PM, Pr, Loc)-SuL
916 ]),
917 member(MPr-SubPos, PrL),
918 strip_module(MPr, PM, Pr)
919 ; Clause = assertions:asr_glob(Asr, PM, Pr, Loc),
920 member(MGl-GPos, GlL),
921 strip_module(MGl, PM, Gl),
922 add_arg(_, Gl, Pr, GPos, SubPos)
923 ;
924 once(( member(MGl-GPos, GlL),
925 member(Gl, [declaration, declaration(_)]),
926 strip_module(MGl, PM, Gl),
927 add_arg(_, Gl, Pr, GPos, _),
928 predicate_property(PM:Pr, implementation_module(metaprops)),
929 functor(Head, Op, 1)
930 )),
931 Clause = (:- '$export_ops'([op(1125, fy, Op)], PM, File))
932 ; member(MGl-_, GlL),
933 member(Gl, [declaration,
934 declaration(_),
935 global,
936 global(_)]),
937 strip_module(MGl, PM, Gl),
938 add_arg(_, Gl, Pr, _, _),
939 predicate_property(PM:Pr, implementation_module(metaprops))
940 ->functor(Head, Fn, N),
941 ( \+ predicate_property(M:Head, meta_predicate(_)),
942 functor(Meta, Fn, N),
943 Meta =.. [_|ArgL],
944 once(append(ArgL1, [0], ArgL)),
945 maplist(=(?), ArgL1),
946 Clause = (:- meta_predicate Meta)
947 )
948 ),
949 ( nonvar(SubPos)
950 ->arg(1, SubPos, From),
951 arg(2, SubPos, To),
952 TermPos = term_position(From, To, From, To, [_, 0-0, SubPos, _])
953 ; true
954 )
955 ),
956 ( var(Pos),
957 nonvar(File)
958 ->( nonvar(SubPos),
959 integer(From)
960 ->filepos_line(File, From, Line, Pos)
961 ; Line = Line1,
962 Pos = -1
963 )
964 ; true
965 ).972expand_assertion(Decl, DPos, Records, RPos) :- 973 '$current_source_module'(M), 974 expand_assertion(M, Dict, Decl, DPos, Records, RPos), 975 % Dict Must be assigned after expand_assertion/6 to avoid performance 976 % issues --EMM 977 ( nb_current('$variable_names', Dict) 978 ->true 979 ; Dict = [] 980 ). 981 982:- dynamic sequence/1. 983sequence(1). 984 985get_sequence_and_inc(S) :- 986 retract(sequence(S)), 987 succ(S, S2), 988 assertz(sequence(S2)). 989 990% ---------------------------------------------------------------------------- 991 992term_expansion_decl(Decl, PPos, Records, RPos) :- 993 nonvar(PPos), 994 PPos = parentheses_term_position(_, _, Pos), 995 !, 996 term_expansion_decl(Decl, Pos, Records, RPos). 997term_expansion_decl(Decl, PPos, Records, RPos) :- 998 ( nonvar(PPos) 999 ->PPos = term_position(_, _, _, _, [DPos]) 1000 ; true 1001 ), 1002 expand_assertion(Decl, DPos, Records, RPos). 1003 1004term_expansion((:- Decl), DPos, Records, RPos) :- 1005 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
*/