1:- module(assrt_lib, [assertion_read/9,
    2		      assertion_body/7,
    3		      comps_to_goal/3,
    4		      comps_to_goal/4,
    5		      assertion_records/4,
    6		      a_fake_body/5,
    7		      assertion_db/11,
    8		      assrt_lib_tr/4]).    9
   10:- use_module(library(lists)).   11:- use_module(library(assertions_op)).   12
   13:- expects_dialect(swi).   14
   15% :- ml(160).
   16
   17% Assertion reader for SWI-Prolog
   18
   19:- multifile
   20    assrt_lib:assertion_head/7,
   21    assrt_lib:doc_db/4,
   22    assrt_lib:nodirective_error_hook/1.   23
   24% :- volatile
   25%     assrt_lib:assertion_head/7,
   26%     assrt_lib:doc_db/4.
   27
   28add_arg(H, M:G0, M:G) :- !,
   29    add_arg(H, G0, G).
   30add_arg(H, G0, G) :-
   31    ( nonvar(G0)
   32    ->G0 =.. [F|L],
   33      G  =.. [F,H|L]
   34    ; G  =.. [F,H|L],
   35      G0 =.. [F|L]
   36    ).
   37
   38list_conj([],     true).
   39list_conj([E|EL], CL) :-
   40    list_conj_2(EL, E, CL).
   41
   42list_conj_2([E|L], E0, (E0, S)) :- list_conj_2(L, E, S).
   43list_conj_2([], E, E).
   44
   45% conj_list(V) --> {var(V)}, !, [V].
   46% conj_list((A, B)) --> !,
   47%     conj_list(A),
   48%     conj_list(B).
   49% conj_list(A) --> [A].
   50
   51a_fake_body(CompL, CallL, SuccL, GlobL0, (call(Comp), call(Call), call(Succ), call(Glob))) :-
   52    list_conj(CompL, Comp),
   53    list_conj(CallL, Call),
   54    list_conj(SuccL, Succ),
   55    ( nonvar(Glob)
   56    ->list_conj(GlobL, Glob),
   57      maplist(add_arg(_), GlobL0, GlobL)
   58    ; maplist(add_arg(_), GlobL0, GlobL),
   59      list_conj(GlobL, Glob)
   60    ).
   61
   62% Note: assertion_db/11 encapsulates the nasty call to clause/2.
   63%
   64assertion_db(Head, M, Status, Type, Comp, Call, Succ, Glob, Comm, Dict, Pos) :-
   65    clause(assertion_head(Head, M, Status, Type, Comm, Dict, Pos), _:FBody),
   66    once(a_fake_body(Comp, Call, Succ, Glob, FBody)).
   67
   68filepos_line(File, CharPos, Line, LinePos) :-
   69    setup_call_cleanup('$push_input_context'(filepos),
   70		       prolog_codewalk:filepos_line(File, CharPos, Line, LinePos),
   71		       '$pop_input_context').
   72
   73% For compatibility with Ciao Libraries
   74assertion_read(Head, M, Status, Type, Body, Dict, File, Line0, Line1) :-
   75    clause(assrt_lib:assertion_head(Head, M, Status, Type, Comm, Dict, Loc), _:FBody, Ref),
   76    once(a_fake_body(Comp, Call, Succ, Glob0, FBody)),
   77    maplist(add_arg(Head), Glob0, Glob),
   78    assertion_body(Head, Comp, Call, Succ, Glob, Comm, Body),
   79    ( nonvar(Loc),
   80      ( Loc = file_term_position(File, Pos),
   81	nonvar(Pos),
   82	arg(1, Pos, From),
   83	arg(2, Pos, To),
   84	integer(From),
   85	integer(To)
   86      ->filepos_line(File, From, Line0, _),
   87	filepos_line(File, To,   Line1, _)
   88      ; Loc = file(File, Line0, -1, _),
   89	Line1 = Line0
   90      )
   91    ->true
   92    ; clause_property(Ref, file(File)),
   93      clause_property(Ref, line_count(Line0 )),
   94      Line1 = Line0
   95    ).
   96
   97% ---------------------------------------------------------------------------
   98% :- pred normalize_assertion_body(B,F,NB)
   99%    # "@var{NB} is a normalized assertion body corresponding to the
  100%      unnomalized assertion body @var{B}.".
  101% ---------------------------------------------------------------------------
  102
  103% MH: Added new assertions for transition. Marked as %N
  104% MH: No comments allowed now in basic assertions (difficult to document).
  105% EM: SWI-Like notation, usage of is/2 instead of +/2.
  106% EM: valid_cp/1 solves ambiguity of :/2 with module qualification
  107% --------------------------- A  B   C     D  E -- FormatId ------------------------------- %ABCDE
  108normalize_assertion_body((PD::DP:CP=>AP  + GP#CO), p, PD, DP,   CP,   AP,   GP,   CO) :- !. %11111%N
  109normalize_assertion_body((PD::DP:CP=>AP is GP#CO), p, PD, DP,   CP,   AP,   GP,   CO) :- !. %11111%N
  110normalize_assertion_body((PD::DP:CP=>AP  + GP   ), p, PD, DP,   CP,   AP,   GP,   "") :- !. %11110
  111normalize_assertion_body((PD::DP:CP=>AP is GP   ), p, PD, DP,   CP,   AP,   GP,   "") :- !. %11110
  112normalize_assertion_body((PD::DP:CP=>AP      #CO), p, PD, DP,   CP,   AP,   true, CO) :- !. %11101%N%N
  113normalize_assertion_body((PD::DP:CP=>AP         ), p, PD, DP,   CP,   AP,   true, "") :- !. %11100
  114normalize_assertion_body((PD::DP:CP      + GP#CO), p, PD, DP,   CP,   true, GP,   CO) :- !. %11011%N
  115normalize_assertion_body((PD::DP:CP     is GP#CO), p, PD, DP,   CP,   true, GP,   CO) :- !. %11011%N
  116normalize_assertion_body((PD::DP:CP      + GP   ), p, PD, DP,   CP,   true, GP,   "") :- !. %11010
  117normalize_assertion_body((PD::DP:CP     is GP   ), p, PD, DP,   CP,   true, GP,   "") :- !. %11010
  118normalize_assertion_body((PD::DP:CP          #CO), p, PD, DP,   CP,   true, true, CO) :- !. %11001%N
  119normalize_assertion_body((PD::DP:CP             ), p, PD, DP,   CP,   true, true, "") :- !. %11000
  120normalize_assertion_body((PD::DP   =>AP  + GP#CO), p, PD, DP,   true, AP,   GP,   CO) :- !. %10111%N
  121normalize_assertion_body((PD::DP   =>AP is GP#CO), p, PD, DP,   true, AP,   GP,   CO) :- !. %10111%N
  122normalize_assertion_body((PD::DP   =>AP  + GP   ), p, PD, DP,   true, AP,   GP,   "") :- !. %10110
  123normalize_assertion_body((PD::DP   =>AP is GP   ), p, PD, DP,   true, AP,   GP,   "") :- !. %10110
  124normalize_assertion_body((PD::DP   =>AP      #CO), p, PD, DP,   true, AP,   true, CO) :- !. %10101%N
  125normalize_assertion_body((PD::DP   =>AP         ), p, PD, DP,   true, AP,   true, "") :- !. %10100
  126normalize_assertion_body((PD::DP         + GP#CO), p, PD, DP,   true, true, GP,   CO) :- !. %10011%N
  127normalize_assertion_body((PD::DP        is GP#CO), p, PD, DP,   true, true, GP,   CO) :- !. %10011%N
  128normalize_assertion_body((PD::DP         + GP   ), p, PD, DP,   true, true, GP,   "") :- !. %10010
  129normalize_assertion_body((PD::DP        is GP   ), p, PD, DP,   true, true, GP,   "") :- !. %10010
  130normalize_assertion_body((PD::DP             #CO), d, PD, DP,   true, true, true, CO) :- !. %10001%N
  131normalize_assertion_body((PD::DP                ), d, PD, DP,   true, true, true, "") :- !. %10000
  132normalize_assertion_body((PD    :CP=>AP  + GP#CO), p, PD, true, CP,   AP,   GP,   CO) :- valid_cp(CP), !. %01111%N
  133normalize_assertion_body((PD    :CP=>AP is GP#CO), p, PD, true, CP,   AP,   GP,   CO) :- valid_cp(CP), !. %01111%N
  134normalize_assertion_body((PD    :CP=>AP  + GP   ), p, PD, true, CP,   AP,   GP,   "") :- valid_cp(CP), !. %01110
  135normalize_assertion_body((PD    :CP=>AP is GP   ), p, PD, true, CP,   AP,   GP,   "") :- valid_cp(CP), !. %01110
  136normalize_assertion_body((PD    :CP=>AP      #CO), s, PD, true, CP,   AP,   true, CO) :- valid_cp(CP), !. %01101%N
  137normalize_assertion_body((PD    :CP=>AP         ), s, PD, true, CP,   AP,   true, "") :- valid_cp(CP), !. %01100
  138normalize_assertion_body((PD    :CP      + GP#CO), g, PD, true, CP,   true, GP,   CO) :- valid_cp(CP), !. %01011%N
  139normalize_assertion_body((PD    :CP     is GP#CO), g, PD, true, CP,   true, GP,   CO) :- valid_cp(CP), !. %01011%N
  140normalize_assertion_body((PD    :CP      + GP   ), g, PD, true, CP,   true, GP,   "") :- valid_cp(CP), !. %01010
  141normalize_assertion_body((PD    :CP     is GP   ), g, PD, true, CP,   true, GP,   "") :- valid_cp(CP), !. %01010
  142normalize_assertion_body((PD    :CP          #CO), c, PD, true, CP,   true, true, CO) :- valid_cp(CP), !. %01001%N
  143normalize_assertion_body((PD    :CP             ), c, PD, true, CP,   true, true, "") :- valid_cp(CP), !. %01000
  144normalize_assertion_body((PD       =>AP  + GP#CO), p, PD, true, true, AP,   GP,   CO) :- !. %00111%N
  145normalize_assertion_body((PD       =>AP is GP#CO), p, PD, true, true, AP,   GP,   CO) :- !. %00111%N
  146normalize_assertion_body((PD       =>AP  + GP   ), p, PD, true, true, AP,   GP,   "") :- !. %00110
  147normalize_assertion_body((PD       =>AP is GP   ), p, PD, true, true, AP,   GP,   "") :- !. %00110
  148normalize_assertion_body((PD       =>AP      #CO), s, PD, true, true, AP,   true, CO) :- !. %00101%N
  149normalize_assertion_body((PD       =>AP         ), s, PD, true, true, AP,   true, "") :- !. %00100
  150normalize_assertion_body((PD             + GP#CO), g, PD, true, true, true, GP,   CO) :- !. %00011%N
  151normalize_assertion_body((PD            is GP#CO), g, PD, true, true, true, GP,   CO) :- !. %00011%N
  152normalize_assertion_body((PD             + GP   ), g, PD, true, true, true, GP,   "") :- !. %00010
  153normalize_assertion_body((PD            is GP   ), g, PD, true, true, true, GP,   "") :- !. %00010
  154normalize_assertion_body((BO                 #CO), P, PD, DP,   CP,   AP,   GP,   CO) :-
  155    normalize_assertion_body(BO, P, PD, DP, CP, AP, GP, ""), !. %00001%N
  156normalize_assertion_body((PD                 #CO), p, PD, true, true, true, true, CO) :- !. %00001%N
  157normalize_assertion_body((PD                    ), t, (PD                    ), true, true, true, true, ""). %00000
  158%% ---------------------------------------------------------------------------------------- %% ----
  159
  160fix_format_global(p, p).
  161fix_format_global(d, p).
  162fix_format_global(s, p).
  163fix_format_global(g, g).
  164fix_format_global(c, g).
  165fix_format_global(t, g).
  166
  167valid_cp(CP) :- \+ invalid_cp(CP).
  168
  169invalid_cp(_/_).
  170
  171assertion_body(Pred,Compat,Call,Succ,Comp,Comm,
  172	       (Pred::Compat:Call=>Succ+Comp#Comm)).
  173
  174assrt_type(pred).
  175assrt_type(prop).
  176assrt_type(decl).
  177assrt_type(func).
  178assrt_type(calls).
  179assrt_type(success).
  180assrt_type(comp).
  181assrt_type(entry).
  182assrt_type(exit).
  183assrt_type(test).
  184assrt_type(texec).
  185assrt_type(modedef).
  186
  187assrt_status(true).
  188assrt_status(false).
  189assrt_status(check).
  190assrt_status(checked).
  191assrt_status(trust).
  192assrt_status(trace).
  193assrt_status(debug).
  194
  195% ---------------------------------------------------------------------------
  196% :- pred default_assrt_status(+assrt_type,-assrt_status)
  197% # "Defines the status to be used for a given assertion type, if an
  198%    assertion status is not specified explicitly.".
  199% ---------------------------------------------------------------------------
  200
  201default_assrt_status(entry,   true) :- !. % ???
  202default_assrt_status(modedef, true) :- !. % ???
  203default_assrt_status(X,       check) :-
  204    assrt_type(X),
  205    !.
  206
  207normalize_status_and_type(Assertions, APos, AssrtStatus, AssrtType, UBody, BPos) :-
  208    normalize_status_and_type_1(Assertions, APos, AssrtStatus, AssrtType, UBody, BPos),
  209    status_and_type(AssrtStatus, AssrtType).
  210
  211normalize_status_and_type_1(Assertions, term_position(_, _, _, _, [BPos]),
  212			  _, AssrtType, UBody, BPos) :-
  213    Assertions =.. [AssrtType, UBody].
  214normalize_status_and_type_1(Assertions, term_position(_, _, _, _, [_, BPos]),
  215			  AssrtStatus, AssrtType, UBody, BPos) :-
  216    Assertions =.. [AssrtType, AssrtStatus, UBody].
  217
  218status_and_type(AssrtStatus, AssrtType) :-
  219    assrt_type(AssrtType),
  220    ( default_assrt_status(AssrtType, AssrtStatus)
  221    ; assrt_status(AssrtStatus)
  222    ).
  223
  224term_expansion(generate_nodirective_error, Clauses) :-
  225    expand_nodirective_error(Clauses).
  226
  227expand_nodirective_error(Clauses) :-
  228    findall((:- export(Type/Arity)),
  229	    ( assrt_type(Type),
  230	      member(Arity, [1, 2])
  231	    ), Clauses, ClauseT),
  232    findall((Assr :- Body),
  233	    ( assrt_type(Type),
  234	      normalize_status_and_type_1(Assr, _, Status, Type, _, _),
  235	      functor(Assr, Type, Arity),
  236	      Body0 = ignore(assrt_lib:nodirective_error_hook(Assr)),
  237	      ( Arity = 1
  238	      ->Body = Body0
  239	      ; Body = (assrt_lib:assrt_status(Status), Body0 )
  240	      )
  241	    ),
  242	    ClauseT).
  243
  244% To Avoid attempts to execute asertions (must be declarations):
  245generate_nodirective_error.
 ---------------------------------------------------------------------------
:- pred assertion_format(AssrtType, Code) :: assrt_type * assrt_format_code # "@var{Code} describes an admissible format in which assertions of the class @var{AssrtType} can be written.". % ---------------------------------------------------------------------------
  253% Admissible assertion formats:
  254assertion_format(pred, X) :- assrt_format_code(X).
  255assertion_format(decl, X) :- assrt_format_code(X). % ?
  256assertion_format(prop, X) :- assrt_format_code(X).
  257assertion_format(test, X) :- assrt_format_code(X). % For unit-test -- EMM
  258% Obsolete: delete eventually...
  259% assertion_format(type,    t).
  260% Not needed any more...
  261% assertion_format(type,    g). %% Added for now to put typedef there...
  262% assertion_format(compat,  d). %% Not using these as basic any more?!
  263assertion_format(calls,   c).
  264assertion_format(success, s).
  265% Entry for unit-test -- EMM
  266assertion_format(texec, g).
  267assertion_format(texec, c).
  268% DTM: New assertion type
  269assertion_format(exit, s).
  270assertion_format(comp, g).
  271% These to become obsolete?
  272assertion_format(entry, c).
  273assertion_format(entry, t).
  274
  275% Not an assertion any more, but a status instead
  276% assertion_format(trust,   X) :- assrt_format_code(X).
  277assertion_format(modedef, X) :- assrt_format_code(X).
  278
  279% :- prop assrt_format_code(X) + regtype
  280%    # "@var{X} is a designator for an assertion format.".
  281
  282assrt_format_code(p).
  283assrt_format_code(d).
  284assrt_format_code(c).
  285assrt_format_code(s).
  286assrt_format_code(g).
  287assrt_format_code(t).
  288
  289% EMM: Support for grouped global properties
  290
  291current_body(M:BodyS, _, term_position(_, _, _, _, [_, PosS]), Body, BPos, Gl0, Gl) :-
  292    atom(M), !,
  293    current_body(BodyS, M, PosS, Body, BPos, Gl0, Gl).
  294current_body(BodyS + PGl, M, term_position(_, _, _, _, [PosS, _]),
  295	     Body, BPos, Gl0, Gl) :- !,
  296    propdef(PGl, M, Gl0, Gl1),
  297    current_body(BodyS, M, PosS, Body, BPos, Gl1, Gl).
  298current_body(BodyS is PGl#Co, M,
  299	     term_position(From, To, _, _,
  300			   [PosS, term_position(_, _, FFrom, FTo, [_, PosCo])]),
  301	     Body, BPos, Gl0, Gl) :- !,
  302    propdef(PGl, M, Gl0, Gl1),
  303    current_body(BodyS#Co, M, term_position(From, To, FFrom, FTo, [PosS, PosCo]),
  304		 Body, BPos, Gl1, Gl).
  305current_body(BodyS is PGl, M, term_position(_, _, _, _, [PosS, _]),
  306	     Body, BPos, Gl0, Gl) :- !,
  307    propdef(PGl, M, Gl0, Gl1),
  308    current_body(BodyS, M, PosS, Body, BPos, Gl1, Gl).
  309current_body(BodyS, M, PosS, Body, BPos, Gl0, Gl) :-
  310    ( body_member(BodyS, PosS, Lit, LPos)
  311    *->
  312      current_body(Lit, M, LPos, Body, BPos, Gl0, Gl)
  313    ; Body = M:BodyS,
  314      Gl = Gl0,
  315      BPos = PosS
  316    ).
  317
  318body_member(Body, _, _, _) :-
  319    var(Body), !, fail.
  320body_member([], _, _, _) :- !, fail.
  321body_member([A|B], list_position(From, To, [APos|EPos], TPos), Lit, LPos) :- !,
  322    ( Lit=A, LPos=APos
  323    ; Lit=B, LPos=list_position(From, To, EPos, TPos)
  324    ).
  325body_member((A, B), term_position(_, _, _, _, [APos, BPos]), Lit, LPos) :- !,
  326    ( Lit=A, LPos=APos
  327    ; Lit=B, LPos=BPos
  328    ).
  329
  330normalize_assertions(Assertions  + PGl, M, term_position(_, _, _, _, [APos, _]),
  331		     Pred, Status, Type, Cp, Ca, Su, Gl, Co, RPos) :- !,
  332    propdef(PGl, M, Gl, Gl0),
  333    normalize_assertions(Assertions, M, APos, Pred, Status, Type, Cp, Ca, Su, Gl0, Co, RPos).
  334normalize_assertions(Assertions is PGl, M, term_position(_, _, _, _, [APos, _]),
  335		     Pred, Status, Type, Cp, Ca, Su, Gl, Co, RPos) :- !,
  336    propdef(PGl, M, Gl, Gl0),
  337    normalize_assertions(Assertions, M, APos, Pred, Status, Type, Cp, Ca, Su, Gl0, Co, RPos).
  338normalize_assertions(Assertions, M, APos, Pred, Status, Type, Cp, Ca, Su, Gl, Co, RPos) :-
  339    once(normalize_status_and_type(Assertions, APos, Status, Type, BodyS, PosS)),
  340    current_body(BodyS, M, PosS, BM:Body, BPos, Gl, Gl0),
  341    normalize_assertion_head_body(Body, BM, BPos, Pred, Format, Cp, Ca, Su, Gl0, Co, RPos),
  342    (Gl \= [] -> fix_format_global(Format, GFormat) ; GFormat = Format),
  343    assertion_format(Type, GFormat).
  344
  345/*
  346normalize_assertion(Assr, Pred, Status, Type, Cp, Ca, Su, Gl, Co) :-
  347    once(normalize_status_and_type(Assr, Status, Type, Body)),
  348    normalize_assertion_head_body(Body, M, Pred, Format, Cp, Ca, Su, Gl, Co),
  349    assertion_format(Type, Format).
  350*/
  351
  352:- use_module(library(prolog_codewalk), []).  353
  354normalize_assertion_head_body(Body, M, BPos, Pred, Format, Cp, Ca, Su, Gl, Co, RPos) :-
  355    normalize_assertion_body(Body, Format, Head, PCp, PCa, PSu, PGl, Co),
  356    ignore(prolog_codewalk:subterm_pos(Head, Body, BPos, HPos)),
  357    normalize_assertion_head(Head, M, HPos, Pred, Cp0, Ca0, Su0, Gl0, RPos),
  358    apropdef(Pred, M, PCp, Cp, Cp0),
  359    apropdef(Pred, M, PCa, Ca, Ca0),
  360    apropdef(Pred, M, PSu, Su, Su0),
  361    propdef(PGl, M, Gl, Gl0).
  362
  363normalize_assertion_head((H1,H2), M, term_position(_, _, _, _, [P1, P2]),
  364			 P, Cp, Ca, Su, Gl, RP) :- !,
  365    ( normalize_assertion_head(H1, M, P1, P, Cp, Ca, Su, Gl, RP)
  366    ; normalize_assertion_head(H2, M, P2, P, Cp, Ca, Su, Gl, RP)
  367    ).
  368normalize_assertion_head([H1|H2], M, list_position(From, To, [P1|E], TP),
  369			 P, Cp, Ca, Su, Gl, RP) :- !,
  370    ( normalize_assertion_head(H1, M, P1, P, Cp, Ca, Su, Gl, RP)
  371    ; normalize_assertion_head(H2, M, list_position(From, To, E, TP),
  372			       P, Cp, Ca, Su, Gl, RP)
  373    ).
  374normalize_assertion_head(M:H, _, term_position(_, _, _, _, [_, HP]),
  375			 P, Cp, Ca, Su, Gl, RP) :-
  376    atom(M), !,
  377    normalize_assertion_head(H, M, HP, P, Cp, Ca, Su, Gl, RP).
  378normalize_assertion_head(F/A, M, Pos, M:Pred, [], [], [], [], Pos) :- !,
  379    functor(Pred, F, A).
  380normalize_assertion_head(Head, M, Pos, M:Pred, Cp, Ca, Su, Gl, Pos) :-
  381    compound(Head),
  382    !,
  383    functor(Head, F, A),
  384    functor(Pred, F, A),
  385    normalize_args(1, Head, M, Pred, Cp, Ca, Su, Gl).
  386normalize_assertion_head(Head, M, Pos, M:Head, [], [], [], [], Pos) :-
  387    atom(Head).
  388
  389normalize_args(N0, Head, M, Pred, Cp0, Ca0, Su0, Gl0) :-
  390    arg(N0, Head, HArg),
  391    !,
  392    arg(N0, Pred, PArg),
  393    resolve_types_modes(HArg, M, PArg, Cp0, Ca0, Su0, Gl0, Cp1, Ca1, Su1, Gl1),
  394    N is N0 + 1,
  395    normalize_args(N, Head, M, Pred, Cp1, Ca1, Su1, Gl1).
  396normalize_args(_, _, _, _, [], [], [], []).
  397
  398resolve_types_modes(A,    _, A, Cp,  Ca,  Su,  Gl,  Cp, Ca, Su, Gl) :- var(A), !.
  399resolve_types_modes(A0:T, M, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl) :-
  400    do_propdef(T, M, A, Pr0, Pr1),
  401    do_modedef(A0, A1, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl, Pr0, Pr),
  402    !,
  403    do_propdef(A1, M, A, Pr1, Pr).
  404resolve_types_modes(A0, M, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl) :-
  405    do_modedef(A0, A1, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl, Pr0, Pr),
  406    do_propdef(A1, M, A, Pr0, Pr).
  407
  408do_propdef(A,  _, A, Cp,  Cp) :- var(A), !.
  409do_propdef(A1, M, A, Cp1, Cp) :-
  410    hpropdef(A1, M, A, Cp1, Cp).
  411
  412do_modedef(A0, A1, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl, Pr0, Pr) :-
  413    nonvar(A0),
  414    modedef(A0, A1, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl, Pr0, Pr),
  415    !.
  416do_modedef(A0, A1, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl, Pr0, Pr) :-
  417    atom(A0),
  418    A2 =.. [A0, A],
  419    modedef(A2, A1, A, Cp0, Ca0, Su0, Gl0, Cp, Ca, Su, Gl, Pr0, Pr),
  420    !.
  421do_modedef(A0, A0, _, Cp0, Ca, Su, Gl, Cp, Ca, Su, Gl, Cp0, Cp).
  422
  423% Support for modes are hard-wired here:
  424% ISO Modes
  425modedef(+(A),   A, B, Cp,                Ca0,  Su,         Gl,  Cp, Ca, Su, Gl, Ca1, Ca) :-
  426    (var(A), var(Ca1) -> Ca0 = [nonvar(B)|Ca1] ; Ca0 = Ca1). % A bit confuse hack, Ca1 come instantiated to optimize the expression
  427modedef(-(A),   A, B, Cp,        [var(B)|Ca],  Su0,        Gl,  Cp, Ca, Su, Gl, Su0, Su).
  428modedef(?(A),   A, _, Cp0,               Ca,   Su,         Gl,  Cp, Ca, Su, Gl, Cp0, Cp).
  429modedef(@(A),   A, B, Cp0,               Ca,   Su, [nfi(B)|Gl], Cp, Ca, Su, Gl, Cp0, Cp).
  430% PlDoc (SWI) Modes
  431modedef(':'(A), A, B, Cp,   [callable(B)|Ca0], Su, Gl, Cp, Ca, Su, Gl, Ca0, Ca).
  432modedef('!'(A), A, B, Cp0,  [compound(B)|Ca],  Su, Gl, Cp, Ca, Su, Gl, Cp0, Cp). % May be modified using setarg/3 or nb_setarg/3 (mutable)
  433% Ciao Modes:
  434modedef(in(A),  A, B, Cp,     [ground(B)|Ca0],            Su,          Gl,  Cp, Ca, Su, Gl, Ca0, Ca).
  435modedef(out(A), A, B, Cp,        [var(B)|Ca],  [ground(B)|Su0],        Gl,  Cp, Ca, Su, Gl, Su0, Su).
  436modedef(go(A),  A, B, Cp0, Ca,                 [ground(B)|Su],         Gl,  Cp, Ca, Su, Gl, Cp0, Cp).
  437% Additional Modes (See Coding Guidelines for Prolog, Michael A. Covington, 2009):
  438modedef('*'(A), A, B, Cp,     [ground(B)|Ca0],            Su,          Gl,  Cp, Ca, Su, Gl, Ca0, Ca).
  439modedef('='(A), A, B, Cp0,               Ca,              Su,  [nfi(B)|Gl], Cp, Ca, Su, Gl, Cp0, Cp). % The state of A is preserved
  440modedef('/'(A), A, B, Cp,        [var(B)|Ca],             Su0, [nsh(B)|Gl], Cp, Ca, Su, Gl, Su0, Su). % Like '-' but also A don't share with any other argument
  441modedef('>'(A), A, _, Cp, Ca,                             Su0,         Gl,  Cp, Ca, Su, Gl, Su0, Su). % Like output but A might be nonvar on entry
  442
  443				% nfi == not_further_inst
  444				% nsh == not_shared
  445
  446:- multifile prolog:error_message/3.  447
  448prolog:error_message(assertion(il_formed_assertion, Term)) -->
  449    [ 'Il formed assertion, check term ~w'-[Term]].
  450
  451hpropdef(A0, M, A, Cp0, Cp) :-
  452    term_variables(A0, V),
  453    ( member(X, V), X==A ->
  454      Cp0 = [M:A0|Cp]
  455    ; aprops_arg(A0, M, A, Cp0, Cp)
  456    ).
  457
  458apropdef_2(0, _, _, _) --> !, {fail}.
  459apropdef_2(1, Head, M, A) -->
  460    {arg(1, Head, V)},
  461    !,
  462    hpropdef(A, M, V).
  463apropdef_2(N0, Head, M, (P * A)) -->
  464    {arg(N0, Head, V)},
  465    !,
  466    {N is N0 - 1},
  467    apropdef_2(N, Head, M, P),
  468    hpropdef(A, M, V).
  469
  470apropdef(_:Head, M, A) -->
  471    {functor(Head, _, N)},
  472    apropdef_2(N, Head, M, A), !.
  473apropdef(_, M, A) --> propdef(A, M).
  474
  475propdef(A, M) --> props_args(A, M, push).
  476
  477push(A, M) --> [M:A].
  478
  479aprops_arg('{}'(A), M, V) --> !, aprops_args(A, M, V).
  480aprops_arg(A,       M, V) -->    aprops_args(A, M, V).
  481
  482aprops_args(A, M, V) --> props_args(A, M, prop_arg(V)).
  483
  484:- meta_predicate props_args(?, ?, 4, ?, ?).  485
  486props_args(true,   _, _) --> !, [].
  487props_args((A, B), M, V) --> !,
  488    props_args(A, M, V),
  489    props_args(B, M, V).
  490props_args((A; B), M, V) --> !,
  491    {props_args(A, M, V, P1, [])},
  492    {props_args(B, M, V, P2, [])},
  493    [(P1;P2)].
  494props_args(M:A, _, V) -->
  495    {atom(M)}, !,
  496    props_args(A, M, V).
  497props_args(A, M, V) --> call(V, A, M).
  498
  499% add_module(M, P, M:P).
  500
  501prop_arg(V, A, M) -->
  502    {add_arg(V, M:A, P)},
  503    [P].
  504
  505comp_to_goal_assrt(M:Comp, M:Body0, Body) :- !,
  506	comp_to_goal_assrt(Comp, Body0, Body).
  507comp_to_goal_assrt(Comp, Body0, Body) :-
  508	Comp  =.. [PropName, _|Args],
  509	Body0 =.. [PropName, Body|Args].
  510
  511:- pred comps_to_goal/3 #
  512	"This predicate allows to compound a list of global properties in to
  513	sucessive meta-calls".
  514
  515comps_to_goal(Comp) -->
  516	comps_to_goal(Comp, comp_to_goal_assrt).
  517
  518:- pred comps_to_goal/3 # "This predicate allows to compound a list of
  519	global properties in to successive meta-calls, but in the
  520	third argument you can use your own selector.".
  521
  522:- test comps_to_goal(Comp, Goal, Pred) :
  523	(
  524	    Comp = [not_fails(p(A)), is_det(p(A)), exception(p(A), exc)],
  525	    Pred = p(A)
  526	) =>
  527	(
  528	    Goal = not_fails(is_det(exception(p(A),exc)))
  529	).
  530
  531:- meta_predicate comps_to_goal(?, 3, ?, ?).  532comps_to_goal([],             _) --> [].
  533comps_to_goal([Check|Checks], Goal) -->
  534    comps_to_goal2(Checks, Check, Goal).
  535
  536:- meta_predicate comps_to_goal2(?, ?, 3, ?, ?).  537comps_to_goal2([], Check, Goal) -->
  538    call(Goal, Check).
  539comps_to_goal2([Check|Checks], Check0, Goal) -->
  540    call(Goal, Check0),
  541    comps_to_goal2(Checks, Check, Goal).
  542
  543assrt_lib_tr((:- Decl), Records, M, Dict) :-
  544    assertion_records(M, Dict, Decl, _, Records, _).
  545
  546assertion_records_helper(Match, a(Match, Record, Pos), Record, Pos).
  547
  548assertion_records(_, Dict, M:Decl, term_position(_, _, _, _, [_, DPos]),
  549		  Records, RPos) :-
  550    atom(M), !,
  551    assertion_records(M, Dict, Decl, DPos, Records, RPos).
  552assertion_records(M, Dict, doc(Key, Doc),
  553		  term_position(From, To, FFrom, FTo, [KPos, DPos]),
  554		  assrt_lib:doc_db(Key, M, Doc, Dict),
  555		  term_position(0, 0, 0, 0,
  556				[0-0,
  557				 term_position(From, To, FFrom, FTo,
  558					       [KPos, 0-0, DPos, 0-0 ])])) :- !.
  559% Note: We MUST save the full location (File, HPos), because later we will not
  560% have access to source_location/2, and it will fails for further created
  561% clauses --EMM
  562assertion_records(CM, Dict, Assertions, APos, Records, RPos) :-
  563    Match=(Assertions-Dict),
  564    Clause0 = (assrt_lib:assertion_head(Head, M, Status, Type, Co, Dict, Loc) :- FBody),
  565    ( source_location(File, Line0 )
  566    ->Clause = ('$source_location'(File, Line):Clause0 )
  567    ; Clause = Clause0
  568    ),
  569    findall(a(Match, Clause, HPos),
  570	    ( normalize_assertions(Assertions, CM, APos, M:Head, Status,
  571				   Type, Cp0, Ca0, Su0, Gl0, Co, HPos),
  572	      ( nonvar(File),
  573		nonvar(HPos),
  574		arg(1, HPos, HFrom),
  575		integer(HFrom)
  576	      ->Loc = file_term_position(File, HPos),
  577		filepos_line(File, HFrom, Line, _)
  578	      ; ( nonvar(File),
  579		  nonvar(Line0 )
  580		->Loc = file(File, Line0, -1, _)
  581		; true
  582		),
  583		Line = Line0
  584	      ),
  585	      once(maplist(maplist(compact_module_call(M)),
  586			   [Cp0, Ca0, Su0, Gl0 ],
  587			   [Cp,  Ca,  Su,  Gl])),
  588	      a_fake_body(Cp, Ca, Su, Gl, FBody)
  589	    ),
  590	    ARecords),
  591    ARecords \= [], % Is a valid assertion if it defines at least one Record
  592    maplist(assertion_records_helper(Match), ARecords, Records, RPos).
  593
  594:- public compact_module_call/3.  595compact_module_call(M, M:C, C) :- !.
  596compact_module_call(M, (A0;B0), (A;B)) :- !,
  597    maplist(compact_module_call(M), A0, A),
  598    maplist(compact_module_call(M), B0, B).
  599compact_module_call(_, C, C).
  600
  601:- use_module(library(dialect/ciao), []).  602
  603ciao:declaration_hook(Decl, Records) :-
  604    assertion_records(Decl, _, Records, _).
  605
  606assertion_records(Decl, DPos, Records, RPos) :-
  607    '$set_source_module'(M, M),
  608    assertion_records(M, Dict, Decl, DPos, Records, RPos),
  610    
  611    ciao:get_dictionary((:- Decl), M, Dict)