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
   51%!  int(Int)
   52%
   53%   The type of integers
   54
   55:- type int/1.
   56
   57int(X) :-
   58    nonvar(X), !,
   59    integer(X).
   60int(X) :-
   61    between(0, inf, N),
   62    give_sign(N, X).
   63
   64:- type posint/1.
   65
   66posint(X) :-
   67    nonvar(X), !,
   68    integer(X),
   69    X > 0.
   70posint(X) :- curr_posint(X).
   71
   72curr_posint(N) :- between(1, inf, N).
   73
   74:- type negint/1.
   75
   76negint(X) :-
   77    nonvar(X),
   78    !,
   79    integer(X),
   80    X < 0.
   81negint(X) :-
   82    curr_posint(N),
   83    X is -N.
   84
   85give_sign(0, 0) :- !.
   86give_sign(P, P).
   87give_sign(P, N) :- N is -P.
   88
   89:- type nnegint/1.
 nnegint(X)
The type of non negative integers, i.e., natural numbers (including zero)
   95nnegint(X) :-
   96    nonvar(X), !,
   97    integer(X),
   98    X >= 0.
   99nnegint(N) :-
  100    between(0, inf, N).
  101
  102:- type flt/1.
 flt(X)
Floating point numbers
  108flt(X) :-
  109    nonvar(X), !,
  110    float(X).
  111flt(F) :-
  112    nnegfltgen(Q),
  113    give_sign(Q, F).
  114
  115:- type nnegflt/1.
  116
  117nnegflt(X) :-
  118    nonvar(X), !,
  119    float(X),
  120    X >= 0.
  121nnegflt(Q) :-
  122    nnegfltgen(Q).
  123
  124nnegfltgen(Q) :-
  125    nnegint(X),
  126    intfrac1(X, Q).
  127
  128intfrac1(X, Q) :-
  129    ( Q is 1.0*X
  130    ; frac(X, Q)
  131    ).
  132
  133:- type posflt/1.
  134
  135posflt(X) :-
  136    nonvar(X), !,
  137    float(X),
  138    X > 0.
  139posflt(Q) :-
  140    curr_posint(X),
  141    intfrac1(X, Q).
  142
  143:- type rat/1.
  144
  145rat(X) :-
  146    rational(X),
  147    !.
  148rat(X) :-
  149    int(A),
  150    int(B),
  151    X is A rdiv B.
  152
  153real(X) :- number(X).
  154
  155:- type num/1.
 num(X)
Numbers
  161num(X) :-
  162    nonvar(X),
  163    !,
  164    real(X).
  165num(F) :-
  166    nnegnumgen(Q),
  167    give_sign(Q, F).
  168
  169:- type nnegnum/1.
  170
  171nnegnum(X) :-
  172    nonvar(X),
  173    !,
  174    real(X),
  175    X >= 0.
  176nnegnum(Q) :-
  177    nnegnumgen(Q).
  178
  179nnegnumgen(Q) :-
  180    nnegint(X),
  181    intfrac2(X, Q).
  182
  183:- type posnum/1.
  184
  185posnum(X) :-
  186    nonvar(X), !,
  187    number(X),
  188    X > 0.
  189posnum(Q) :-
  190    curr_posint(X),
  191    intfrac2(X, Q).
  192
  193intfrac2(X, Q) :-
  194    ( Q is X
  195    ; Q is 1.0*X
  196    ; frac(X, R),
  197      ( Q is R
  198      ; Q is 1.0*R
  199      )
  200    ).
  201
  202frac(X, Q) :-
  203    between(2, X, Y),
  204    1 =:= gcd(X, Y),
  205    ( Q is X rdiv Y
  206    ; Q is Y rdiv X
  207    ).
  208
  209:- type atm/1.
 atm(A)
An atom
  215atm(T) :- nonvar(T), !, atom(T).
  216atm(A) :-
  217    list(character_code, L),
  218    atom_codes(A, L).
  219
  220:- type atmel/1.
 atmel(A)
An atom or an empty list
  226atmel([]).
  227atmel(A) :- atm(A).
  228
  229:- type str/1.
 str(S)
A string
  235str(T) :- nonvar(T), !, string(T).
  236str(S) :-
  237    list(character_code, L),
  238    string_codes(S, L).
  239
  240%!  character_code(I)
  241%
  242%   An integer which is a character code
  243
  244:- type character_code/1.
  245
  246character_code(I) :-
  247    between(0, 255, I),
  248    neck.
  249
  250
  251%!  constant(C)
  252%
  253%   An atomic term (an atom, string or a number)
  254
  255:- type constant/1.
  256
  257constant([]).
  258constant(T) :- atm(T).
  259constant(T) :- num(T).
  260constant(T) :- str(T).
  261
  262:- type predname/1.
 predname(PI)
A predicate indicator
  268predname(P/A) :-
  269    atm(P),
  270    nnegint(A).
  271
  272:- type term/1.
 term(Term)
Any term
  278term(_).
  279
  280:- type list/1.
 list(List)
List is a list
  286list([]).
  287list([_|L]) :- list(L).
  288
  289%!  list(:Type, List:list)
  290%
  291%    List is a list of Type
  292
  293:- type list(1, list).
  294:- meta_predicate list(1, ?).  295
  296list(Type, List) :- list_(List, Type).
  297
  298:- prop list_/2.
  299list_([], _).
  300list_([E|L], T) :-
  301    type(T, E),
  302    list_(L, T).
  303
  304:- type pair/1.
  305pair(_-_).
  306
  307:- type keypair/1.
  308keypair(_-_).
  309
  310:- type keylist/1.
  311keylist(KL) :- list(keypair, KL).
  312
  313%!  tlist(T, L)
  314%
  315%   L is a list or a value of T's
  316
  317:- type tlist/2.
  318:- meta_predicate tlist(1, ?).  319
  320tlist(T, L) :- list(T, L).
  321tlist(T, E) :- type(T, E).
  322
  323%!  nlist(T, NL)
  324%
  325%   A nested list of T's
  326
  327:- type nlist/2.
  328:- meta_predicate nlist(1, ?).  329
  330nlist(T, X) :- type(T, X).
  331nlist(T, L) :- list(nlist(T), L).
  332
  333%!  nlist(NL)
  334%
  335%   A nested list
  336
  337:- type nlist/1.
  338:- meta_predicate nlist(1, ?).  339
  340nlist(T) :- term(T).
  341nlist(L) :- list(nlist, L).
  342
  343/* Note: this definition could lead to il-formed lists, like [a|b], that is why
  344 * we prefer the definition above
  345
  346nlist(Type, NList) :- nlist_(NList, Type).
  347
  348nlist_([], _).
  349nlist_([X|Xs], T) :-
  350        nlist_(X, T),
  351        nlist_(Xs, T).
  352nlist_(X, T) :-
  353        type(T, X).
  354*/
  355
  356:- type char/1.
  357char(A) :- atm(A). % size(A)=1
  358
  359:- type any/1.
  360any(_).
  361
  362:- type linear/1.
 linear(LT)
A linear term, i.e. all variables occurs only once.
  367linear(T) :-
  368    term_variables(T, Vars),
  369    maplist(occurrs_one(T), Vars).
  370
  371occurrs_one(T, Var) :- occurrences_of_var(Var, T, 1).
  372
  373%!  sequence(:T, S)
  374%
  375%   S is a sequence of T's
  376
  377:- type sequence/2.
  378
  379:- meta_predicate sequence(1, ?).  380
  381sequence(T, S) :- sequence_(T, S).
  382
  383sequence_(E, T) :- type(E, T).
  384sequence_((E, S), T) :-
  385        type(E, T),
  386        sequence_(S, T).
  387
  388:- type struct/1 # "A compound term".
  389
  390% TBD: Proper generator
  391struct([_|_]):- !.
  392struct(T) :- functor(T, _, A), A>0. % compound(T).
  393
  394:- type gnd/1 # "A ground term".
  395
  396% TBD: Proper generator
  397gnd([]) :- !.
  398gnd(T) :-
  399    term_variables(T, Vars),
  400    maplist(gnd, Vars).
  401
  402:- type arithexpression/1.
  403
  404%!  arithexpression(Expr)
  405
  406%   An arithmetic expression
  407
  408:- type gndstr/1.
  409
  410gndstr(A) :- gnd(A), struct(A).
  411
  412arithexpression(X) :- number(X), !. % Optimization
  413arithexpression(X) :- num(X).
  414arithexpression(X) :-
  415    callable(X),
  416    curr_arithmetic_function(X),
  417    X =.. [_|Args],
  418    maplist(arithexpression, Args).
  419
  420curr_arithmetic_function(X) :- current_arithmetic_function(X).
  421curr_arithmetic_function(X) :- arithmetic:evaluable(X, _Module).
  422
  423% BUG: if the trace have all the ports active, we can not use ';'/2 in goal/2
  424% and some variables becomes uninstantiated. That is an SWI-Prolog bug but I
  425% don't have time to isolate it --EMM
  426
  427%!  goal(:P)
  428%
  429%   P is a defined predicate
  430
  431:- true prop goal/1.
  432:- meta_predicate goal(0).  433goal(Pred) :- goal(0, Pred).
  434    % current_predicate(_, M:G).
  435
  436%!  goal(N, :P)
  437%
  438%   P is a defined predicate with N extra arguments
  439
  440:- true prop goal/2.
  441:- meta_predicate goal(?, :).  442goal(N, Pred) :-
  443    nnegint(N),
  444    goal_2(Pred, N).
  445
  446goal_2(M:Pred, N) :-
  447    var(Pred), !,
  448    ( var(M)
  449    ->current_module(CM),
  450      current_predicate(CM:F/A),
  451      M=CM
  452    ; current_module(M),
  453      current_predicate(M:F/A)
  454    ),
  455    A >= N,
  456    A1 is A - N,
  457    functor(Pred, F, A1).
  458goal_2(M:Pred, N) :-
  459    functor(Pred, F, A1),
  460    A is A1 + N,
  461    ( var(M)
  462    ->current_module(CM),
  463      current_predicate(CM:F/A),
  464      M=CM
  465    ; current_module(M),
  466      current_predicate(M:F/A)
  467    ).
  468
  469:- true prop mod_qual/1.
  470mod_qual(M:V) :-
  471    static_strip_module(V, M, _, CM),
  472    current_module(CM).
  473
  474:- true prop mod_qual/2.
  475:- meta_predicate mod_qual(:, ?).  476mod_qual(T, M:V) :-
  477    static_strip_module(V, M, C, CM),
  478    current_module(CM),
  479    type(T, C).
  480
  481:- type operator_specifier/1.
  482
  483operator_specifier(fy).
  484operator_specifier(fx).
  485operator_specifier(yfx).
  486operator_specifier(xfy).
  487operator_specifier(xfx).
  488operator_specifier(yf).
  489operator_specifier(xf)