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.  Equivalent to goal(0, P).
  482
  483:- true prop goal/1.
  484goal(Pred) :- goal(0, Pred).
  485
  486%!  goal(N, :P)
  487%
  488%   P is a defined predicate with N extra arguments. goal/2 is not
  489%   meta_predicate, since P is already module qualificated due to the definition
  490%   of meta arguments in the predicate using this property.
  491
  492:- true prop goal/2.
  493goal(N, Pred) :-
  494    nnegint(N),
  495    ( cv_module(M)
  496    ->Goal = M:Pred
  497    ; Goal = Pred
  498    ),
  499    static_strip_module(Goal, user, H, C),
  500    goal_2(C:H, N).
  501
  502goal_2(M:Pred, N) :-
  503    var(Pred),
  504    !,
  505    checkprop_goal(
  506        ( ( var(M)
  507          ->current_module(CM),
  508            current_predicate(CM:F/A),
  509            M=CM
  510          ; current_module(M),
  511            current_predicate(M:F/A)
  512          ),
  513          A >= N,
  514          A1 is A - N,
  515          functor(Pred, F, A1)
  516        )).
  517goal_2(M:Pred, N) :-
  518    callable(Pred),
  519    functor(Pred, F, A1),
  520    A is A1 + N,
  521    ( var(M)
  522    ->checkprop_goal(
  523          ( current_module(CM),
  524            current_predicate(CM:F/A),
  525            M=CM
  526          ))
  527    ; current_module(M),
  528      current_predicate(M:F/A)
  529    ).
  530
  531:- true prop mod_qual/1.
  532:- meta_predicate mod_qual(:).  533mod_qual(M:V) :-
  534    static_strip_module(V, M, _, CM),
  535    current_module(CM).
  536
  537:- true prop mod_qual/2.
  538:- meta_predicate mod_qual(1, :).  539mod_qual(T, M:V) :-
  540    static_strip_module(V, M, C, CM),
  541    current_module(CM),
  542    with_cv_module(type(T, C), CM).
  543
  544:- type operator_specifier/1.
  545
  546operator_specifier(fy).
  547operator_specifier(fx).
  548operator_specifier(yfx).
  549operator_specifier(xfy).
  550operator_specifier(xfx).
  551operator_specifier(yf).
  552operator_specifier(xf).
  553
  554% Note: options as defined by the type opts/1 are a subset of the supported
  555% options, since it can only handle atomic/unique keys related to single values
  556
  557:- type opt/1.
  558
  559opt(A=B) :-
  560    atm(A),
  561    term(B).
  562opt(A-B) :-
  563    atm(A),
  564    term(B).
  565opt(AB) :-
  566    nonvar(AB),
  567    !,
  568    AB =.. [_, _].
  569
  570:- type opt_eq/1.
  571
  572opt_eq(A=B) :-
  573    atm(A),
  574    term(B).
  575
  576opt_eq(Opt, Opts, [Opt|Opts]) :-
  577    opt_eq(Opt),
  578    \+ member(Opt, Opts).
  579
  580:- type dict/1.
  581
  582dict(D) :-
  583    nonvar(D),
  584    !,
  585    is_dict(D).
  586dict(D) :-
  587    atm(T),
  588    foldl(opt_eq, _, [], O),
  589    dict_create(D, T, O).
  590
  591:- type opts/1.
  592
  593opts(L) :- list(opt, L).
  594opts(D) :- dict(D).
  595
  596:- type metaopts(1, :opts).
  597:- meta_predicate metaopts(1, :).  598
  599metaopts(IsMeta, MOpts) :-
  600    goal(1, IsMeta),
  601    mod_qual(opts, MOpts)