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(typeprops,
   36          [list/1, list/2, tlist/2, nlist/1, nlist/2, goal/2, nnegint/1, pair/1,
   37           flt/1, nnegflt/1, posflt/1, num/1, nnegnum/1, posnum/1, atm/1, gnd/1,
   38           any/1, gndstr/1, str/1, struct/1, term/1, char/1, atmel/1, keypair/1,
   39           sequence/2, negint/1, operator_specifier/1, character_code/1, goal/1,
   40           mod_qual/1, mod_qual/2, keylist/1, predname/1, constant/1, linear/1,
   41           arithexpression/1, int/1, rat/1, posint/1
   42          ]).   43
   44:- use_module(library(arithmetic)).   45:- use_module(library(neck)).   46:- use_module(library(assertions)).   47:- use_module(library(metaprops)).   48:- use_module(library(apply)).   49:- use_module(library(static_strip_module)).   50:- init_expansors.   51
   52%!  int(Int)
   53%
   54%   The type of integers
   55
   56:- type int/1.
   57
   58int(X) :-
   59    nonvar(X),
   60    !,
   61    integer(X).
   62int(X) :-
   63    checkprop_goal(
   64        ( between(0, inf, N),
   65          give_sign(N, X)
   66        )).
   67
   68:- type posint/1.
   69
   70posint(X) :-
   71    nonvar(X),
   72    !,
   73    integer(X),
   74    X > 0.
   75posint(X) :-
   76    checkprop_goal(curr_posint(X)).
   77
   78curr_posint(N) :- between(1, inf, N).
   79
   80:- type negint/1.
   81
   82negint(X) :-
   83    nonvar(X),
   84    !,
   85    integer(X),
   86    X < 0.
   87negint(X) :-
   88    checkprop_goal(
   89        ( curr_posint(N),
   90          X is -N
   91        )).
   92
   93give_sign(0, 0) :- !.
   94give_sign(P, P).
   95give_sign(P, N) :- N is -P.
   96
   97:- type nnegint/1.
 nnegint(X)
The type of non negative integers, i.e., natural numbers (including zero)
  103nnegint(X) :-
  104    nonvar(X),
  105    !,
  106    integer(X),
  107    X >= 0.
  108nnegint(N) :-
  109    checkprop_goal(between(0, inf, N)).
  110
  111:- type flt/1.
 flt(X)
Floating point numbers
  117flt(X) :-
  118    nonvar(X),
  119    !,
  120    float(X).
  121flt(F) :-
  122    checkprop_goal(
  123        ( nnegfltgen(Q),
  124          give_sign(Q, F)
  125        )).
  126
  127:- type nnegflt/1.
  128
  129nnegflt(X) :-
  130    nonvar(X),
  131    !,
  132    float(X),
  133    X >= 0.
  134nnegflt(Q) :-
  135    checkprop_goal(nnegfltgen(Q)).
  136
  137nnegfltgen(Q) :-
  138    nnegint(X),
  139    intfrac1(X, Q).
  140
  141intfrac1(X, Q) :-
  142    ( Q is 1.0*X
  143    ; frac(X, Q)
  144    ).
  145
  146:- type posflt/1.
  147
  148posflt(X) :-
  149    nonvar(X),
  150    !,
  151    float(X),
  152    X > 0.
  153posflt(Q) :-
  154    checkprop_goal(
  155        ( curr_posint(X),
  156          intfrac1(X, Q)
  157        )).
  158
  159:- type rat/1.
  160
  161rat(X) :-
  162    rational(X),
  163    !.
  164rat(X) :-
  165    checkprop_goal(
  166        ( int(A),
  167          int(B),
  168          X is A rdiv B
  169        )).
  170
  171:- type num/1.
 num(X)
Numbers
  177num(X) :-
  178    nonvar(X),
  179    !,
  180    number(X).
  181num(F) :-
  182    checkprop_goal(
  183        ( nnegnumgen(Q),
  184          give_sign(Q, F)
  185        )).
  186
  187:- type nnegnum/1.
  188
  189nnegnum(X) :-
  190    nonvar(X),
  191    !,
  192    number(X),
  193    X >= 0.
  194nnegnum(Q) :-
  195    checkprop_goal(nnegnumgen(Q)).
  196
  197nnegnumgen(Q) :-
  198    nnegint(X),
  199    intfrac2(X, Q).
  200
  201:- type posnum/1.
  202
  203posnum(X) :-
  204    nonvar(X), !,
  205    number(X),
  206    X > 0.
  207posnum(Q) :-
  208    checkprop_goal(
  209        ( curr_posint(X),
  210          intfrac2(X, Q)
  211        )).
  212
  213intfrac2(X, Q) :-
  214    ( Q is X
  215    ; Q is 1.0*X
  216    ; frac(X, R),
  217      ( Q is R
  218      ; Q is 1.0*R
  219      )
  220    ).
  221
  222frac(X, Q) :-
  223    between(2, X, Y),
  224    1 =:= gcd(X, Y),
  225    ( Q is X rdiv Y
  226    ; Q is Y rdiv X
  227    ).
  228
  229:- type atm/1.
 atm(A)
An atom
  235atm(T) :-
  236    nonvar(T),
  237    !,
  238    atom(T).
  239atm(A) :-
  240    checkprop_goal(
  241        ( list(character_code, L),
  242          atom_codes(A, L)
  243        )).
  244
  245:- type atmel/1.
 atmel(A)
An atom or an empty list
  251atmel([]).
  252atmel(A) :- atm(A).
  253
  254:- type str/1.
 str(S)
A string
  260str(T) :-
  261    nonvar(T),
  262    !,
  263    string(T).
  264str(S) :-
  265    checkprop_goal(
  266        ( list(character_code, L),
  267          string_codes(S, L)
  268        )).
  269
  270%!  character_code(I)
  271%
  272%   An integer which is a character code
  273
  274:- type character_code/1.
  275
  276character_code(I) :-
  277    between(0, 255, I),
  278    neck.
  279
  280%!  constant(C)
  281%
  282%   An atomic term (an atom, string or a number)
  283
  284:- type constant/1.
  285
  286constant([]).
  287constant(T) :- atm(T).
  288constant(T) :- num(T).
  289constant(T) :- str(T).
  290
  291:- type predname/1.
 predname(PI)
A predicate indicator
  297predname(P/A) :-
  298    atm(P),
  299    nnegint(A).
  300
  301:- type term/1.
 term(Term)
Any term
  307term(_).
  308
  309:- type list/1.
 list(List)
List is a list
  315list([]).
  316list([_|L]) :- list(L).
  317
  318%!  list(:Type, List:list)
  319%
  320%    List is a list of Type
  321
  322:- type list(1, list).
  323:- meta_predicate list(1, ?).  324
  325list(Type, List) :- list_(List, Type).
  326
  327:- prop list_/2.
  328list_([], _).
  329list_([E|L], T) :-
  330    type(T, E),
  331    list_(L, T).
  332
  333:- type pair/1.
  334pair(_-_).
  335
  336:- type keypair/1.
  337keypair(_-_).
  338
  339:- type keylist/1.
  340keylist(KL) :- list(keypair, KL).
  341
  342%!  tlist(T, L)
  343%
  344%   L is a list or a value of T's
  345
  346:- type tlist/2.
  347:- meta_predicate tlist(1, ?).  348
  349tlist(T, L) :- list(T, L).
  350tlist(T, E) :- type(T, E).
  351
  352%!  nlist(T, NL)
  353%
  354%   A nested list of T's
  355
  356:- type nlist/2.
  357:- meta_predicate nlist(1, ?).  358
  359nlist(T, X) :- type(T, X).
  360nlist(T, L) :- list(nlist(T), L).
  361
  362%!  nlist(NL)
  363%
  364%   A nested list
  365
  366:- type nlist/1.
  367:- meta_predicate nlist(1, ?).  368
  369nlist(T) :- term(T).
  370nlist(L) :- list(nlist, L).
  371
  372/* Note: this definition could lead to il-formed lists, like [a|b], that is why
  373 * we prefer the definition above
  374
  375nlist(Type, NList) :- nlist_(NList, Type).
  376
  377nlist_([], _).
  378nlist_([X|Xs], T) :-
  379        nlist_(X, T),
  380        nlist_(Xs, T).
  381nlist_(X, T) :-
  382        type(T, X).
  383*/
  384
  385:- type char/1.
  386char(A) :- atm(A). % size(A)=1
  387
  388:- type any/1.
  389any(_).
  390
  391:- type linear/1.
 linear(LT)
A linear term, i.e. all variables occurs only once.
  396linear(T) :-
  397    term_variables(T, Vars),
  398    maplist(occurrs_one(T), Vars).
  399
  400occurrs_one(T, Var) :- occurrences_of_var(Var, T, 1).
  401
  402%!  sequence(:T, S)
  403%
  404%   S is a sequence of T's
  405
  406:- type sequence/2.
  407
  408:- meta_predicate sequence(1, ?).  409
  410sequence(T, S) :- sequence_(T, S).
  411
  412sequence_(E, T) :- type(E, T).
  413sequence_((E, S), T) :-
  414        type(E, T),
  415        sequence_(S, T).
  416
  417:- type struct/1 # "A compound term".
  418
  419% TBD: Proper generator
  420struct([_|_]):- !.
  421struct(T) :- functor(T, _, A), A>0. % compound(T).
  422
  423:- type gnd/1 # "A ground term".
  424
  425% TBD: Proper generator
  426gnd([]) :- !.
  427gnd(T) :-
  428    term_variables(T, Vars),
  429    list(gnd, Vars).
  430
  431:- type arithexpression/1.
  432
  433%!  arithexpression(Expr)
  434
  435%   An arithmetic expression
  436
  437:- type gndstr/1.
  438
  439gndstr(A) :- gnd(A), struct(A).
  440
  441arithexpression(X) :- number(X), !. % Optimization
  442arithexpression(X) :- num(X).
  443arithexpression(X) :-
  444    callable(X),
  445    curr_arithmetic_function(X),
  446    X =.. [_|Args],
  447    list(arithexpression, Args).
  448
  449curr_arithmetic_function(X) :- current_arithmetic_function(X).
  450curr_arithmetic_function(X) :- arithmetic:evaluable(X, _Module).
  451
  452% BUG: if the trace has all the ports active, we can not use ';'/2 in goal/2
  453% and some variables becomes uninstantiated. That is an SWI-Prolog bug but I
  454% don't have time to isolate it --EMM
  455
  456%!  goal(:P)
  457%
  458%   P is a defined predicate
  459
  460:- true prop goal/1.
  461:- meta_predicate goal(0).  462goal(Pred) :- goal(0, Pred).
  463    % current_predicate(_, M:G).
  464
  465%!  goal(N, :P)
  466%
  467%   P is a defined predicate with N extra arguments
  468
  469:- true prop goal/2.
  470:- meta_predicate goal(+, :).  471goal(N, Pred) :-
  472    nnegint(N),
  473    goal_2(Pred, N).
  474
  475goal_2(M:Pred, N) :-
  476    var(Pred),
  477    !,
  478    checkprop_goal(
  479        ( ( var(M)
  480          ->current_module(CM),
  481            current_predicate(CM:F/A),
  482            M=CM
  483          ; current_module(M),
  484            current_predicate(M:F/A)
  485          ),
  486          A >= N,
  487          A1 is A - N,
  488          functor(Pred, F, A1)
  489        )).
  490goal_2(M:Pred, N) :-
  491    callable(Pred),
  492    functor(Pred, F, A1),
  493    A is A1 + N,
  494    ( var(M)
  495    ->checkprop_goal(
  496          ( current_module(CM),
  497            current_predicate(CM:F/A),
  498            M=CM
  499          ))
  500    ; current_module(M),
  501      current_predicate(M:F/A)
  502    ).
  503
  504:- true prop mod_qual/1.
  505:- meta_predicate mod_qual(:).  506mod_qual(M:V) :-
  507    static_strip_module(V, M, _, CM),
  508    current_module(CM).
  509
  510:- true prop mod_qual/2.
  511:- meta_predicate mod_qual(1, :).  512mod_qual(T, M:V) :-
  513    static_strip_module(V, M, C, CM),
  514    current_module(CM),
  515    with_cv_module(type(T, C), CM).
  516
  517:- type operator_specifier/1.
  518
  519operator_specifier(fy).
  520operator_specifier(fx).
  521operator_specifier(yfx).
  522operator_specifier(xfy).
  523operator_specifier(xfx).
  524operator_specifier(yf).
  525operator_specifier(xf)