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(metaprops,
   36          [(declaration)/1,
   37           (declaration)/2,
   38           (global)/1,
   39           (global)/2,
   40           (type)/1,
   41           (type)/2,
   42           check/1,
   43           check/2,
   44           compat/1,
   45           compat/2,
   46           false/1,
   47           false/2,
   48           instan/1,
   49           instan/2,
   50           last_prop_failure/1,
   51           pp_status/1,
   52           true/1,
   53           true/2,
   54           trust/1,
   55           trust/2
   56          ]).   57
   58:- use_module(library(compound_expand)).   59:- use_module(library(neck)).   60:- use_module(library(filepos_line)).   61:- use_module(library(assertions)).   62:- use_module(library(resolve_calln)).   63:- use_module(library(qualify_meta_goal)).   64:- use_module(library(compilation_module)).   65
   66:- true prop (type)/1 + (declaration(check), global(prop)) # "Defines a type.".
   67
   68type(Goal) :- call(Goal).
   69
   70:- true prop (global)/1 + (global(prop), declaration)
   71# "A property that is global, i.e., can appear after the + in the assertion.
   72and as meta predicates, meta_predicate F(0)".
   73
   74global(Goal) :- call(Goal).
   75
   76:- type assrt_type/1, assrt_status/1.
   77
   78:- global global(Prop, Goal) : (assrt_type(Prop), callable(Goal))
   79# "Like global/1, but allows to specify the default assertion type".
   80
   81global(_, Goal) :- call(Goal).
   82
   83:- true prop (declaration)/1 + (global(prop), declaration)
   84# "A property that is a declaration, i.e., an operator is added as op(1125, fx, F). Implies global/1".
   85
   86declaration(Goal) :- call(Goal).
   87
   88:- true prop declaration(Status, Goal) : (assrt_status(Status), callable(Goal)) + global(prop)
   89# "Like declaration/1, but allows to specify the default assertion status".
   90
   91declaration(_, Goal) :- call(Goal).
   92
   93:- true prop type(T, A)
   94# "~w is internally of type ~w, a predicate of arity 1 defined as a type/1."-[A, T].
   95:- meta_predicate type(1, ?).   96
   97type(T, A) :- call(T, A).
   98
   99
  100:- multifile
  101    unfold_calls:unfold_call_hook/4.  102
  103unfold_calls:unfold_call_hook(type(T, A), metaprops, M, M:call(T, A)).
  104
  105:- true prop compat(Prop)
  106# "Uses ~w as a compatibility property."-[Prop].
  107
  108:- meta_predicate compat(0 ).  109
  110compat(M:Goal) :-
  111    term_variables(Goal, VS),
  112    compat(M:Goal, VS).
  113
  114:- use_module(library(gcb)).  115:- use_module(library(list_sequence)).  116:- use_module(library(substitute)).  117:- use_module(library(clambda)).  118:- use_module(library(terms_share)).  119
  120:- thread_local
  121        '$last_prop_failure'/2.  122
  123generalize_term(STerm, Term, _) :-
  124    \+ terms_share(STerm, Term).
  125
  126neg(nonvar(A), var(A)).
  127neg(A==B,  A \== B).
  128neg(A =B,  A  \= B).
  129neg(A=:=B, A =\= B).
  130neg(A,     \+A).
  131
  132current_prop_failure((SG :- Body)) :-
  133    '$last_prop_failure'(Term, SubU),
  134    sort(SubU, Sub),
  135    greatest_common_binding(Term, Sub, ST, SSub, [[]], Unifier, []),
  136    substitute(generalize_term(SSub), ST, SG),
  137    maplist(\ A^NA^once(neg(A, NA)), SSub, NSub),
  138    foldl(simplify_unifier(SG-SSub), Unifier, LitL, NSub),
  139    LitL \= [],
  140    list_sequence(LitL, Body).
  141
  142simplify_unifier(Term, A=B) -->
  143    ( {occurrences_of_var(A, Term, 0 )}
  144    ->{A=B}
  145    ; [A=B]
  146    ).
  147
  148last_prop_failure(L) :-
  149    findall(E, once(current_prop_failure(E)), L),
  150    retractall('$last_prop_failure'(_, _)).
  151
  152asserta_prop_failure(T, S) :-
  153    once(retract('$last_prop_failure'(T, L))),
  154    asserta('$last_prop_failure'(T, [S|L])).
  155
  156cleanup_prop_failure(T, S) :-
  157    retractall('$last_prop_failure'(_, _)),
  158    asserta('$last_prop_failure'(T, S)).
  159
  160
  161compat(M:Goal, VarL) :-
  162    copy_term_nat(Goal-VarL, Term-VarTL), % get rid of corroutining while checking compatibility
  163    sort(VarTL, VS),
  164    cleanup_prop_failure(Term, []),
  165    prolog_current_choice(CP),
  166    compat(Term, data(VS, Term, CP), M).
  167
  168% this small interpreter will reduce the possibility of loops if the goal being
  169% checked is not linear, i.e., if it contains linked variables:
  170compat(Var, _, _) :- var(Var), !.
  171compat(M:Goal, D, _) :-
  172    !,
  173    compat(Goal, D, M).
  174compat(A, D, M) :-
  175    do_resolve_calln(A, B),
  176    !,
  177    compat(B, D, M).
  178compat((A, B), D, M) :-
  179    !,
  180    compat(A, D, M),
  181    compat(B, D, M).
  182compat(compat(A), D, M) :-
  183    !,
  184    compat(A, D, M).
  185compat((A->B; C), D, M) :-
  186    !,
  187    ( call(M:A)
  188    ->compat(B, D, M)
  189    ; compat(C, D, M)
  190    ),
  191    !.
  192compat((A->B), D, M) :-
  193    !,
  194    ( call(M:A)
  195    ->compat(B, D, M)
  196    ).
  197compat(!, data(_, _, CP), _) :-
  198    !,
  199    cut_from(CP).
  200compat(A, data(VarL, _, _), M) :-
  201    % This clause allows usage of simple test predicates as compatibility check
  202    compound(A),
  203    A \= (_;_),
  204    compatc(A, VarL, M),
  205    !.
  206compat(Term, D, M) :-
  207    D = data(_, T, _),
  208    asserta_prop_failure(T, Term),
  209    compat_1(Term, D, M),
  210    cleanup_prop_failure(T, []).
  211
  212% NOTE: The cut in compat_1 assume that is safe to do it.  That happens when the
  213% arguments of the Goal do not share with other parts of the check that could
  214% eventually lead the execution to a failure and backtrack.
  215
  216compat_1((A; B), D, M) :-
  217    ( compat(A, D, M)
  218    ; compat(B, D, M)
  219    ),
  220    !.
  221compat_1(A, D, M) :-
  222    ( is_prop(A, M)
  223    ->catch(compat_body(M:A, D),
  224            _,
  225            do_compat(M:A, D))
  226    ; do_compat(M:A, D)
  227    ),
  228    !.
  229
  230do_compat(Goal, data(VarL, _, _)) :-
  231    term_variables(VarL, VS),
  232    prolog_current_choice(CP),
  233    maplist(freeze_cut(CP), VS),
  234    Goal,
  235    maplist(del_freeze, VS).
  236
  237del_freeze(Var) :-
  238    ( attvar(Var)
  239    ->del_attr(Var, freeze)
  240    ; true
  241    ).
  242
  243is_prop(Head, M) :-
  244    prop_asr(Head, M, Stat, prop, _, _, _),
  245    memberchk(Stat, [check, true]).
  246
  247:- meta_predicate compat_body(0, +).  248
  249compat_body(MG1, data(V, T, _)) :-
  250    qualify_meta_goal(MG1, MG),
  251    prolog_current_choice(CP),
  252    clause(MG, Body, Ref),
  253    clause_property(Ref, module(CM)),
  254    compat(Body, data(V, T, CP), CM).
  255
  256:- use_module(library(safe_prolog_cut_to)).  257
  258cut_from(CP) :- catch(safe_prolog_cut_to(CP), _, true).
  259
  260freeze_cut(CP, V) :-
  261    freeze(V, catch(prolog_cut_to(CP), _, true)).
  262
  263compatc(H, VarL, M) :-
  264    functor(H, _, N),
  265    arg(N, H, A),
  266    ( var(A),
  267      ord_intersect(VarL, [A], [A])
  268    ; predicate_property(M:H, meta_predicate(Spec)),
  269      arg(N, Spec, Meta),
  270      '$expand':meta_arg(Meta),
  271      A = X:Y,
  272      ( ( var(X)
  273        ; current_module(X)
  274        )
  275      ->var(Y),
  276        ord_intersect(VarL, [Y], [Y])
  277      )
  278    ),
  279    !.
  280compatc(H, VarL, _) :-
  281    compatc_arg(H, A),
  282    (var(A)->ord_intersect(VarL, [A], [A]) ; true).
  283
  284compatc_arg(var(      A), A).
  285compatc_arg(nonvar(   A), A).
  286compatc_arg(term(     A), A).
  287compatc_arg(gnd(      A), A).
  288compatc_arg(ground(   A), A).
  289compatc_arg(nonground(A), A).
  290
  291freeze_fail(CP, Term, V, N) :-
  292    freeze(V, ( prolog_cut_to(CP),
  293                cleanup_prop_failure(Term, [nonvar(N), N==V]),
  294                fail
  295              )).
  296
  297:- global instan(Prop)
  298# "Uses Prop as an instantiation property. Verifies that execution of
  299   ~w does not produce bindings for the argument variables."-[Prop].
  300
  301:- meta_predicate instan(0).  302
  303instan(Goal) :-
  304    term_variables(Goal, VS),
  305    instan(Goal, VS).
  306
  307:- meta_predicate instan(0, +).  308
  309instan(Goal, VS) :-
  310    prolog_current_choice(CP),
  311    \+ \+ ( copy_term_nat(Goal-VS, Term-VN),
  312            maplist(freeze_fail(CP, Term), VS, VN),
  313            Goal
  314          ).
  315
  316pp_status(check).
  317pp_status(trust).
  318pp_status(true ).
  319pp_status(false).
  320
  321:-  pp_status(Status),
  322    ( Call =.. [Status, 0   ]
  323    ; Call =.. [Status, 0, +]
  324    ),
  325    neck,
  326    meta_predicate(Call).  327
  328Call :-
  329    pp_status(Status),
  330    ( Call =.. [Status, _]
  331    ; Call =.. [Status, _, _]
  332    ),
  333    neck.
  334
  335goal_expansion(Check, TermPos1, CheckLoc, TermPos) :-
  336    pp_status(Status),
  337    Check =.. [Status, Pred],
  338    CheckLoc =.. [Status, Pred, Loc],
  339    Loc = file(File, Line, Pos, _),
  340    necks,
  341    source_location(File, Line1),
  342    ( var(TermPos1)
  343    ->Line = Line1,
  344      Pos = -1,
  345      TermPos = TermPos1
  346    ; TermPos1 = term_position(From, To, FFrom, FTo, [APos]),
  347      integer(From),
  348      filepos_line(File, From, Line, Pos),
  349      TermPos  = term_position(From, To, FFrom, FTo, [APos, _])
  350    )