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(apply)).   45:- use_module(library(arithmetic)).   46:- use_module(library(occurs)).   47:- use_module(library(neck)).   48:- use_module(library(assertions)).   49:- use_module(library(metaprops)).   50:- use_module(library(static_strip_module)).   51:- init_expansors.   52
   53%!  int(Int)
   54%
   55%   The type of integers
   56
   57:- type int/1.
   58
   59int(X) :-
   60    nonvar(X),
   61    !,
   62    integer(X).
   63int(X) :-
   64    checkprop_goal(
   65        ( between(0, inf, N),
   66          give_sign(N, X)
   67        )).
   68
   69:- type posint/1.
   70
   71posint(X) :-
   72    nonvar(X),
   73    !,
   74    integer(X),
   75    X > 0.
   76posint(X) :-
   77    checkprop_goal(curr_posint(X)).
   78
   79curr_posint(N) :- between(1, inf, N).
   80
   81:- type negint/1.
   82
   83negint(X) :-
   84    nonvar(X),
   85    !,
   86    integer(X),
   87    X < 0.
   88negint(X) :-
   89    checkprop_goal(
   90        ( curr_posint(N),
   91          X is -N
   92        )).
   93
   94give_sign(0, 0) :- !.
   95give_sign(P, P).
   96give_sign(P, N) :- N is -P.
   97
   98:- type nnegint/1.

 nnegint(X)

The type of non negative integers, i.e., natural numbers (including zero)

  104nnegint(X) :-
  105    nonvar(X),
  106    !,
  107    integer(X),
  108    X >= 0.
  109nnegint(N) :-
  110    checkprop_goal(between(0, inf, N)).
  111
  112:- type flt/1.

 flt(X)

Floating point numbers

  118flt(X) :-
  119    nonvar(X),
  120    !,
  121    float(X).
  122flt(F) :-
  123    checkprop_goal(
  124        ( nnegfltgen(Q),
  125          give_sign(Q, F)
  126        )).
  127
  128:- type nnegflt/1.
  129
  130nnegflt(X) :-
  131    nonvar(X),
  132    !,
  133    float(X),
  134    X >= 0.
  135nnegflt(Q) :-
  136    checkprop_goal(nnegfltgen(Q)).
  137
  138nnegfltgen(Q) :-
  139    nnegint(X),
  140    intfrac1(X, Q).
  141
  142intfrac1(X, Q) :-
  143    ( Q is 1.0*X
  144    ; frac(X, Q)
  145    ).
  146
  147:- type posflt/1.
  148
  149posflt(X) :-
  150    nonvar(X),
  151    !,
  152    float(X),
  153    X > 0.
  154posflt(Q) :-
  155    checkprop_goal(
  156        ( curr_posint(X),
  157          intfrac1(X, Q)
  158        )).
  159
  160:- type rat/1.
  161
  162rat(X) :-
  163    rational(X),
  164    !.
  165rat(X) :-
  166    checkprop_goal(
  167        ( int(A),
  168          int(B),
  169          X is A rdiv B
  170        )).
  171
  172:- type num/1.

 num(X)

Numbers

  178num(X) :-
  179    nonvar(X),
  180    !,
  181    number(X).
  182num(F) :-
  183    checkprop_goal(
  184        ( nnegnumgen(Q),
  185          give_sign(Q, F)
  186        )).
  187
  188:- type nnegnum/1.
  189
  190nnegnum(X) :-
  191    nonvar(X),
  192    !,
  193    number(X),
  194    X >= 0.
  195nnegnum(Q) :-
  196    checkprop_goal(nnegnumgen(Q)).
  197
  198nnegnumgen(Q) :-
  199    nnegint(X),
  200    intfrac2(X, Q).
  201
  202:- type posnum/1.
  203
  204posnum(X) :-
  205    nonvar(X), !,
  206    number(X),
  207    X > 0.
  208posnum(Q) :-
  209    checkprop_goal(
  210        ( curr_posint(X),
  211          intfrac2(X, Q)
  212        )).
  213
  214intfrac2(X, Q) :-
  215    ( Q is X
  216    ; Q is 1.0*X
  217    ; frac(X, R),
  218      ( Q is R
  219      ; Q is 1.0*R
  220      )
  221    ).
  222
  223frac(X, Q) :-
  224    between(2, X, Y),
  225    1 =:= gcd(X, Y),
  226    ( Q is X rdiv Y
  227    ; Q is Y rdiv X
  228    ).
  229
  230:- type atm/1.

 atm(A)

An atom

  236atm(T) :-
  237    nonvar(T),
  238    !,
  239    atom(T).
  240atm(A) :-
  241    checkprop_goal(
  242        ( list(character_code, L),
  243          atom_codes(A, L)
  244        )).
  245
  246:- type atmel/1.

 atmel(A)

An atom or an empty list

  252atmel([]).
  253atmel(A) :- atm(A).
  254
  255:- type str/1.

 str(S)

A string

  261str(T) :-
  262    nonvar(T),
  263    !,
  264    string(T).
  265str(S) :-
  266    checkprop_goal(
  267        ( list(character_code, L),
  268          string_codes(S, L)
  269        )).
  270
  271%!  character_code(I)
  272%
  273%   An integer which is a character code
  274
  275:- type character_code/1.
  276
  277character_code(I) :-
  278    between(0, 255, I),
  279    neck.
  280
  281%!  constant(C)
  282%
  283%   An atomic term (an atom, string or a number)
  284
  285:- type constant/1.
  286
  287constant([]).
  288constant(T) :- atm(T).
  289constant(T) :- num(T).
  290constant(T) :- str(T).
  291
  292:- type predname/1.

 predname(PI)

A predicate indicator

  298predname(P/A) :-
  299    atm(P),
  300    nnegint(A).
  301
  302:- type term/1.

 term(Term)

Any term

  308term(_).
  309
  310:- type list/1.

 list(List)

List is a list

  316list([]).
  317list([_|L]) :- list(L).
  318
  319%!  list(:Type, List:list)
  320%
  321%    List is a list of Type
  322
  323:- type list(1, list).
  324:- meta_predicate list(1, ?).  325
  326list(Type, List) :- list_(List, Type).
  327
  328:- prop list_/2.
  329list_([], _).
  330list_([E|L], T) :-
  331    type(T, E),
  332    list_(L, T).
  333
  334:- type pair/1.
  335pair(_-_).
  336
  337:- type keypair/1.
  338keypair(_-_).
  339
  340:- type keylist/1.
  341keylist(KL) :- list(keypair, KL).
  342
  343%!  tlist(T, L)
  344%
  345%   L is a list or a value of T's
  346
  347:- type tlist/2.
  348:- meta_predicate tlist(1, ?).  349
  350tlist(T, L) :- list(T, L).
  351tlist(T, E) :- type(T, E).
  352
  353%!  nlist(T, NL)
  354%
  355%   A nested list of T's
  356
  357:- type nlist/2.
  358:- meta_predicate nlist(1, ?).  359
  360nlist(T, X) :- type(T, X).
  361nlist(T, L) :- list(nlist(T), L).
  362
  363%!  nlist(NL)
  364%
  365%   A nested list
  366
  367:- type nlist/1.
  368:- meta_predicate nlist(1, ?).  369
  370nlist(T) :- term(T).
  371nlist(L) :- list(nlist, L).
  372
  373/* Note: this definition could lead to il-formed lists, like [a|b], that is why
  374 * we prefer the definition above
  375
  376nlist(Type, NList) :- nlist_(NList, Type).
  377
  378nlist_([], _).
  379nlist_([X|Xs], T) :-
  380        nlist_(X, T),
  381        nlist_(Xs, T).
  382nlist_(X, T) :-
  383        type(T, X).
  384*/
  385
  386:- type char/1.
  387char(A) :- atm(A). % size(A)=1
  388
  389:- type any/1.
  390any(_).
  391
  392:- type linear/1.

 linear(LT)

A linear term, i.e. all variables occurs only once.

  397linear(T) :-
  398    term_variables(T, Vars),
  399    maplist(occurrs_one(T), Vars).
  400
  401occurrs_one(T, Var) :- occurrences_of_var(Var, T, 1).
  402
  403%!  sequence(:T, S)
  404%
  405%   S is a sequence of T's
  406
  407:- type sequence/2.
  408
  409:- meta_predicate sequence(1, ?).  410
  411sequence(T, S) :- sequence_(T, S).
  412
  413sequence_(E, T) :- type(E, T).
  414sequence_((E, S), T) :-
  415        type(E, T),
  416        sequence_(S, T).
  417
  418:- type struct/1 # "A compound term".
  419
  420% TBD: Proper generator
  421struct([_|_]):- !.
  422struct(T) :- functor(T, _, A), A>0. % compound(T).
  423
  424:- type gnd/1 # "A ground term".
  425
  426% TBD: Proper generator
  427gnd([]) :- !.
  428gnd(T) :-
  429    term_variables(T, Vars),
  430    list(gnd, Vars).
  431
  432:- type arithexpression/1.
  433
  434%!  arithexpression(Expr)
  435
  436%   An arithmetic expression
  437
  438:- type gndstr/1.
  439
  440gndstr(A) :- gnd(A), struct(A).
  441
  442arithexpression(X) :- number(X), !. % Optimization
  443arithexpression(X) :- num(X).
  444arithexpression(X) :-
  445    callable(X),
  446    curr_arithmetic_function(X),
  447    X =.. [_|Args],
  448    list(arithexpression, Args).
  449
  450curr_arithmetic_function(X) :- current_arithmetic_function(X).
  451curr_arithmetic_function(X) :- arithmetic:evaluable(X, _Module).
  452
  453% BUG: if the trace has all the ports active, we can not use ';'/2 in goal/2
  454% and some variables becomes uninstantiated. That is an SWI-Prolog bug but I
  455% don't have time to isolate it --EMM
  456
  457%!  goal(:P)
  458%
  459%   P is a defined predicate
  460
  461:- true prop goal/1.
  462:- meta_predicate goal(0).  463goal(Pred) :- goal(0, Pred).
  464    % current_predicate(_, M:G).
  465
  466%!  goal(N, :P)
  467%
  468%   P is a defined predicate with N extra arguments
  469
  470:- true prop goal/2.
  471:- meta_predicate goal(+, :).  472goal(N, Pred) :-
  473    nnegint(N),
  474    goal_2(Pred, N).
  475
  476goal_2(M:Pred, N) :-
  477    var(Pred),
  478    !,
  479    checkprop_goal(
  480        ( ( var(M)
  481          ->current_module(CM),
  482            current_predicate(CM:F/A),
  483            M=CM
  484          ; current_module(M),
  485            current_predicate(M:F/A)
  486          ),
  487          A >= N,
  488          A1 is A - N,
  489          functor(Pred, F, A1)
  490        )).
  491goal_2(M:Pred, N) :-
  492    callable(Pred),
  493    functor(Pred, F, A1),
  494    A is A1 + N,
  495    ( var(M)
  496    ->checkprop_goal(
  497          ( current_module(CM),
  498            current_predicate(CM:F/A),
  499            M=CM
  500          ))
  501    ; current_module(M),
  502      current_predicate(M:F/A)
  503    ).
  504
  505:- true prop mod_qual/1.
  506:- meta_predicate mod_qual(:).  507mod_qual(M:V) :-
  508    static_strip_module(V, M, _, CM),
  509    current_module(CM).
  510
  511:- true prop mod_qual/2.
  512:- meta_predicate mod_qual(1, :).  513mod_qual(T, M:V) :-
  514    static_strip_module(V, M, C, CM),
  515    current_module(CM),
  516    with_cv_module(type(T, C), CM).
  517
  518:- type operator_specifier/1.
  519
  520operator_specifier(fy).
  521operator_specifier(fx).
  522operator_specifier(yfx).
  523operator_specifier(xfy).
  524operator_specifier(xfx).
  525operator_specifier(yf).
  526operator_specifier(xf)