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:- use_module(library(compound_expand)).   51:- reexport(library(assertions_op)).   52:- use_module(library(extend_args)).   53:- use_module(library(apply)).   54:- use_module(library(pairs)).   55:- use_module(library(extra_messages), []).   56:- use_module(library(filepos_line)).   57:- use_module(library(lists)).   58:- use_module(library(list_sequence)).   59:- use_module(library(neck)).   60:- use_module(library(termpos)).   61:- use_module(library(prolog_codewalk), []).

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:

  :- det callable.

is equivalent to:

  :- true prop callable/1 is det

but can be confused with:

:- true prop det(callable)
:- true prop det(X) :: callable(X).

in any case this is syntax sugar so we can always write the long version of the assertion to avoid ambiguities

*/

   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.
 asr_head(?Asr, ?Head) is det
Extract the Head for a given assertion identifier. Note that the first and second arguments of the Assertion identifier should contain the module and the head respectively.
  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).
 asr_aprop(+Asr, +Key, ?Prop, -From)
Extensible accessor to assertion properties, ideal to have different views of assertions, to extend the assertions or to create ancillary assertions (see module 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(?, 0, +, +),
  163       aprop_asr(?, 0, +, +).  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, -HPos, -CmpPos, -CPos, -SPos, -GPos, -ComPos)
Extract the different sections from the Body of an assertion. Note that this is expanded during compilation to contain extra arguments with the term locations for each section of the assertion from:
  decompose_assertion_body(+Body, +Pos, -Head, -Compat, -Call, -Succ, -Glob, Comment)

SWI-Extensions with respect to the Ciao Assertion Language:

  225:- add_termpos(decompose_assertion_body(+, -, -, -, -)).  226:- add_termpos(decompose_assertion_body(+, -, -, -, -, -)).  227:- add_termpos(decompose_assertion_body(+, -, -, -, -, -, -)).  228
  229% ----------------------- AB C  D    E- -AB--C-----D-----E----- %CDE
  230decompose_assertion_body((AB:C=>D  + E), AB, C,    D,    E   ) :- valid_cp(C). %111
  231decompose_assertion_body((AB:C=>D is E), AB, C,    D,    E   ) :- valid_cp(C). %111
  232decompose_assertion_body((AB:C=>D     ), AB, C,    D,    true) :- valid_cp(C). %110
  233decompose_assertion_body((AB:C     + E), AB, C,    true, E   ) :- valid_cp(C). %101
  234decompose_assertion_body((AB:C    is E), AB, C,    true, E   ) :- valid_cp(C). %101
  235decompose_assertion_body((AB:C        ), AB, C,    true, true) :- valid_cp(C). %100
  236decompose_assertion_body((AB  =>D  + E), AB, true, D,    E   ). %011
  237decompose_assertion_body((AB  =>D is E), AB, true, D,    E   ). %011
  238decompose_assertion_body((AB  =>D     ), AB, true, D,    true). %010
  239decompose_assertion_body((AB       + E), AB, true, true, E   ). %001
  240decompose_assertion_body((AB      is E), AB, true, true, E   ). %001
  241decompose_assertion_body((AB          ), AB, true, true, true). %000
  242
  243decompose_assertion_body((BO#F), A, B, C, D, E, F ) :- decompose_assertion_body(BO, A, B, C, D, E).
  244decompose_assertion_body(BO,     A, B, C, D, E, "") :- decompose_assertion_body(BO, A, B, C, D, E).
  245
  246decompose_assertion_body((A::BO), A, B,    C, D, E) :- decompose_assertion_body(BO, B, C, D, E).
  247decompose_assertion_body(BO,      A, true, C, D, E) :- decompose_assertion_body(BO, A, C, D, E).
  248
  249valid_cp(C) :- \+ invalid_cp(C).
  250
  251invalid_cp(_/_).
 validate_body_sections(+Type:assrt_type, -Compat:list(pair), -Calls:list(pair), -Success:list(pair), -Global:list(pair), -MustBeEmpty:list(pair), -MustNotBeEmpty:list(pair)) is det
Unifies MustBeEmpty with a list of sections that must be empty, and MustNotBeEmpty with a list of sections that must not be empty. The elements of both lists are pairs like Section-List, where section could be compatibility, preconditions, postconditions or global.
  260validate_body_sections(pred,     _,  _,     _,  _, [], []).
  261validate_body_sections(prop,     _,  _,     _,  _, [], []).
  262validate_body_sections(calls,   Cp, Ca,    Su, Gl,
  263                       [compatibility-Cp, postconditions-Su, globalprops-Gl],
  264                       [preconditions-Ca]).
  265validate_body_sections(success, Cp,  _,    Su, Gl,
  266                       [compatibility-Cp, globalprops-Gl],
  267                       [postconditions-Su]).
  268validate_body_sections(comp,    Cp,  _,    Su, Gl,
  269                       [compatibiltiy-Cp, postconditions-Su],
  270                       [globalprops-Gl]).
 assrt_type(Type)
The type of assertion, could have the following values:

calls - Specifies the properties at call time.

success - Specifies the properties on success, but only for external calls.

comp - Assertion type comp, specifies computational or global properties.

prop - States that the predicate is a property

pred - Union of calls, success and comp assertion types

  286assrt_type(Type) :-
  287    validate_body_sections(Type, _, _, _, _, _, _),
  288    neck.
 assrt_status(Status)
The status of an assertion. Be careful, since they are not compatible with those found in Ciao-Prolog. Could have the following values:

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).

To be done
- : The next are intended to be used internally, once the system be able to infer new assertions:

right: inferred by the static analysis trust: Ciao-Prolog like, provided by the user fail: false, inferred by the static analyss.

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