typeprops.pl

    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, flt/1,
   37            gndstr/1, posflt/1, num/1, nnegnum/1, posnum/1, atm/1, gnd/1, any/1,
   38            int/1, nnegflt/1, str/1, term/1, char/1, atmel/1, keypair/1, pair/1,
   39            struct/1, constant/1, operator_specifier/1, character_code/1, rat/1,
   40            mod_qual/1, mod_qual/2, keylist/1, predname/1, sequence/2, linear/1,
   41            negint/1, posint/1, dict/1, atmstr/1, opts/1, metaopts/2, goal/1,
   42            arithexpression/1
   43          ]).   44
   45:- use_module(library(apply)).   46:- use_module(library(arithmetic)).   47:- use_module(library(occurs)).   48:- use_module(library(neck)).   49:- use_module(library(assertions)).   50:- use_module(library(metaprops)).   51:- use_module(library(static_strip_module)).   52:- init_expansors.   53
   54%!  int(Int)
   55%
   56%   The type of integers
   57
   58:- type int/1.
   59
   60int(X) :-
   61    nonvar(X),
   62    !,
   63    integer(X).
   64int(X) :-
   65    checkprop_goal(
   66        ( between(0, inf, N),
   67          give_sign(N, X)
   68        )).
   69
   70:- type posint/1.
   71
   72posint(X) :-
   73    nonvar(X),
   74    !,
   75    integer(X),
   76    X > 0.
   77posint(X) :-
   78    checkprop_goal(curr_posint(X)).
   79
   80curr_posint(N) :- between(1, inf, N).
   81
   82:- type negint/1.
   83
   84negint(X) :-
   85    nonvar(X),
   86    !,
   87    integer(X),
   88    X < 0.
   89negint(X) :-
   90    checkprop_goal(
   91        ( curr_posint(N),
   92          X is -N
   93        )).
   94
   95give_sign(0, 0) :- !.
   96give_sign(P, P).
   97give_sign(P, N) :- N is -P.
   98
   99:- type nnegint/1.

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

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

flt(X): Floating point numbers

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

num(X): Numbers

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

atm(A): An atom

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

atmel(A): An atom or an empty list

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

str(S): A string

  262str(T) :-
  263    nonvar(T),
  264    !,
  265    string(T).
  266str(S) :-
  267    checkprop_goal(
  268        ( list(character_code, L),
  269          string_codes(S, L)
  270        )).
  271
  272%!  character_code(I)
  273%
  274%   An integer which is a character code
  275
  276:- type character_code/1.
  277
  278character_code(I) :-
  279    between(0, 255, I),
  280    neck.
  281
  282:- type atmstr/1.

atmel(A): An atom or string

  288atmstr(T) :-
  289    nonvar(T),
  290    !,
  291    once(( atom(A)
  292         ; string(A)
  293         )).
  294atmstr(S) :-
  295    checkprop_goal(
  296        ( list(character_code, L),
  297          ( string_codes(S, L)
  298          ; atom_codes(S, L)
  299          )
  300        )).
  301    
  302
  303%!  constant(C)
  304%
  305%   An atomic term (an atom, string or a number)
  306
  307:- type constant/1.
  308
  309constant([]).
  310constant(T) :- atm(T).
  311constant(T) :- num(T).
  312constant(T) :- str(T).
  313
  314:- type predname/1.

predname(PI): A predicate indicator

  320predname(P/A) :-
  321    atm(P),
  322    nnegint(A).
  323
  324:- type term/1.

term(Term): Any term

  330term(_).
  331
  332:- type list/1.

list(List): List is a list

  338list([]).
  339list([_|L]) :- list(L).
  340
  341%!  list(:Type, List:list)
  342%
  343%    List is a list of Type
  344
  345:- type list(1, list).
  346:- meta_predicate list(1, ?).  347
  348list(Type, List) :- list_(List, Type).
  349
  350:- type list_/2.
  351list_([], _).
  352list_([E|L], T) :-
  353    type(T, E),
  354    list_(L, T).
  355
  356:- type pair/1.
  357pair(_-_).
  358
  359:- type keypair/1.
  360keypair(_-_).
  361
  362:- type keylist/1.
  363keylist(KL) :- list(keypair, KL).
  364
  365%!  tlist(T, L)
  366%
  367%   L is a list or a value of T's
  368
  369:- type tlist/2.
  370:- meta_predicate tlist(1, ?).  371
  372tlist(T, L) :- list(T, L).
  373tlist(T, E) :- type(T, E).
  374
  375%!  nlist(T, NL)
  376%
  377%   A nested list of T's
  378
  379:- type nlist/2.
  380:- meta_predicate nlist(1, ?).  381
  382nlist(T, X) :- type(T, X).
  383nlist(T, L) :- list(nlist(T), L).
  384
  385%!  nlist(NL)
  386%
  387%   A nested list
  388
  389:- type nlist/1.
  390:- meta_predicate nlist(1, ?).  391
  392nlist(T) :- term(T).
  393nlist(L) :- list(nlist, L).
  394
  395/* Note: this definition could lead to il-formed lists, like [a|b], that is why
  396 * we prefer the definition above
  397
  398nlist(Type, NList) :- nlist_(NList, Type).
  399
  400nlist_([], _).
  401nlist_([X|Xs], T) :-
  402        nlist_(X, T),
  403        nlist_(Xs, T).
  404nlist_(X, T) :-
  405        type(T, X).
  406*/
  407
  408:- type char/1.
  409char(A) :- atm(A). % size(A)=1
  410
  411:- type any/1.
  412any(_).
  413
  414:- type linear/1.

linear(LT): A linear term, i.e. all variables occurs only once.

  419linear(T) :-
  420    term_variables(T, Vars),
  421    maplist(occurrs_one(T), Vars).
  422
  423occurrs_one(T, Var) :- occurrences_of_var(Var, T, 1).
  424
  425%!  sequence(:T, S)
  426%
  427%   S is a sequence of T's
  428
  429:- type sequence/2.
  430
  431:- meta_predicate sequence(1, ?).  432
  433sequence(T, S) :- sequence_(T, S).
  434
  435sequence_(E, T) :- type(E, T).
  436sequence_((E, S), T) :-
  437        type(E, T),
  438        sequence_(S, T).
  439
  440:- type struct/1 # "A compound term".
  441
  442% TBD: Proper generator
  443struct([_|_]):- !.
  444struct(T) :- functor(T, _, A), A>0. % compound(T).
  445
  446:- type gnd/1 # "A ground term".
  447
  448% TBD: Proper generator
  449gnd([]) :- !.
  450gnd(T) :-
  451    term_variables(T, Vars),
  452    list(gnd, Vars).
  453
  454:- type arithexpression/1.
  455
  456%!  arithexpression(Expr)
  457
  458%   An arithmetic expression
  459
  460:- type gndstr/1.
  461
  462gndstr(A) :- gnd(A), struct(A).
  463
  464arithexpression(X) :- number(X), !. % Optimization
  465arithexpression(X) :- num(X).
  466arithexpression(X) :-
  467    callable(X),
  468    curr_arithmetic_function(X),
  469    X =.. [_|Args],
  470    list(arithexpression, Args).
  471
  472curr_arithmetic_function(X) :- current_arithmetic_function(X).
  473curr_arithmetic_function(X) :- arithmetic:evaluable(X, _Module).
  474
  475% BUG: if the trace has all the ports active, we can not use ';'/2 in goal/2
  476% and some variables becomes uninstantiated. That is an SWI-Prolog bug but I
  477% don't have time to isolate it --EMM
  478
  479%!  goal(:P)
  480%
  481%   P is a defined predicate
  482
  483:- true prop goal/1.
  484:- meta_predicate goal(0).  485goal(Pred) :- goal(0, Pred).
  486    % current_predicate(_, M:G).
  487
  488%!  goal(N, :P)
  489%
  490%   P is a defined predicate with N extra arguments
  491
  492:- true prop goal/2.
  493:- meta_predicate goal(+, :).  494goal(N, Pred) :-
  495    nnegint(N),
  496    goal_2(Pred, N).
  497
  498goal_2(M:Pred, N) :-
  499    var(Pred),
  500    !,
  501    checkprop_goal(
  502        ( ( var(M)
  503          ->current_module(CM),
  504            current_predicate(CM:F/A),
  505            M=CM
  506          ; current_module(M),
  507            current_predicate(M:F/A)
  508          ),
  509          A >= N,
  510          A1 is A - N,
  511          functor(Pred, F, A1)
  512        )).
  513goal_2(M:Pred, N) :-
  514    callable(Pred),
  515    functor(Pred, F, A1),
  516    A is A1 + N,
  517    ( var(M)
  518    ->checkprop_goal(
  519          ( current_module(CM),
  520            current_predicate(CM:F/A),
  521            M=CM
  522          ))
  523    ; current_module(M),
  524      current_predicate(M:F/A)
  525    ).
  526
  527:- true prop mod_qual/1.
  528:- meta_predicate mod_qual(:).  529mod_qual(M:V) :-
  530    static_strip_module(V, M, _, CM),
  531    current_module(CM).
  532
  533:- true prop mod_qual/2.
  534:- meta_predicate mod_qual(1, :).  535mod_qual(T, M:V) :-
  536    static_strip_module(V, M, C, CM),
  537    current_module(CM),
  538    with_cv_module(type(T, C), CM).
  539
  540:- type operator_specifier/1.
  541
  542operator_specifier(fy).
  543operator_specifier(fx).
  544operator_specifier(yfx).
  545operator_specifier(xfy).
  546operator_specifier(xfx).
  547operator_specifier(yf).
  548operator_specifier(xf).
  549
  550% Note: options as defined by the type opts/1 are a subset of the supported
  551% options, since it can only handle atomic/unique keys related to single values
  552
  553:- type opt/1.
  554
  555opt(A=B) :-
  556    atm(A),
  557    term(B).
  558opt(A-B) :-
  559    atm(A),
  560    term(B).
  561opt(AB) :-
  562    nonvar(AB),
  563    !,
  564    AB =.. [_, _].
  565
  566:- type opt_eq/1.
  567
  568opt_eq(A=B) :-
  569    atm(A),
  570    term(B).
  571
  572opt_eq(Opt, Opts, [Opt|Opts]) :-
  573    opt_eq(Opt),
  574    \+ member(Opt, Opts).
  575
  576:- type dict/1.
  577
  578dict(D) :-
  579    nonvar(D),
  580    !,
  581    is_dict(D).
  582dict(D) :-
  583    atm(T),
  584    foldl(opt_eq, _, [], O),
  585    dict_create(D, T, O).
  586
  587:- type opts/1.
  588
  589opts(L) :- list(opt, L).
  590opts(D) :- dict(D).
  591
  592:- type metaopts(1, :opts).
  593:- meta_predicate metaopts(1, :).  594
  595metaopts(IsMeta, MOpts) :-
  596    goal(1, IsMeta),
  597    mod_qual(opts, MOpts)