View source with raw comments or as raw

    1/*  Part of SWI-Prolog
    2
    3    Author:        Jan Wielemaker
    4    E-mail:        J.Wielemaker@vu.nl
    5    WWW:           http://www.swi-prolog.org
    6    Copyright (c)  2011-2016, VU University Amsterdam
    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(varnumbers,
   36          [ numbervars/1,                       % +Term
   37            varnumbers/2,                       % +Term, -Copy
   38            max_var_number/3,                   % +Term, +Start, -Max
   39            varnumbers/3,                       % +Term, +No, -Copy
   40            varnumbers_names/3                  % +Term, -Copy, -VariableNames
   41          ]).   42:- use_module(library(error)).   43:- use_module(library(assoc)).   44:- use_module(library(apply)).

Utilities for numbered terms

This library provides the inverse functionality of the built-in numbervars/3. Note that this library suffers from the known issues that '$VAR'(X) is a normal Prolog term and, -unlike the built-in numbervars-, the inverse predicates do not process cyclic terms. The following predicate is true for any acyclic term that contains no '$VAR'(X), integer(X) terms and no constraint variables:

always_true(X) :-
      copy_term(X, X2),
      numbervars(X),
      varnumbers(X, Copy),
      Copy =@= X2.

See also: - numbervars/4, =@=/2 (variant/2).
Compatibility: -
This library was introduced by Quintus and available in many related implementations, although not with exactly the same set of predicates. */

numbervars(+Term) is det

Number variables in Term using $VAR(N). Equivalent to numbervars(Term, 0, _).

See also: - numbervars/3, numbervars/4

   76numbervars(Term) :-
   77    numbervars(Term, 0, _).

varnumbers(+Term, -Copy) is det: Inverse of numbervars/1. Equivalent to varnumbers(Term, 0, Copy).

   84varnumbers(Term, Copy) :-
   85    varnumbers(Term, 0, Copy).

varnumbers(+Term, +Start, -Copy) is det

Inverse of numbervars/3. True when Copy is a copy of Term with all variables numbered >= Start consistently replaced by fresh variables. Variables in Term are shared with Copy rather than replaced by fresh variables.

Errors: - domain_error(acyclic_term, Term) if Term is cyclic.
Compatibility: - Quintus, SICStus. Not in YAP version of this library

   97varnumbers(Term, Min, Copy) :-
   98    must_be(acyclic, Term),
   99    MaxStart is Min-1,
  100    max_var_number(Term, MaxStart, Max),
  101    NVars is Max-MaxStart,
  102    (   NVars == 0
  103    ->  Copy = Term
  104    ;   roundup_next_power_two(NVars, Len),
  105        functor(Vars, v, Len),
  106        varnumbers(Term, MaxStart, Vars, Copy)
  107    ).
  108
  109varnumbers(Var, _, _, Copy) :-
  110    var(Var),
  111    !,
  112    Copy = Var.
  113varnumbers(Var, _, _, Copy) :-
  114    atomic(Var),
  115    !,
  116    Copy = Var.
  117varnumbers('$VAR'(I), Min, Vars, Copy) :-
  118    integer(I),
  119    I > Min,
  120    !,
  121    Index is I-Min,
  122    arg(Index, Vars, Copy).
  123varnumbers(Term, Min, Vars, Copy) :-
  124    functor(Term, Name, Arity),
  125    functor(Copy, Name, Arity),
  126    varnumbers_args(1, Arity, Term, Min, Vars, Copy).
  127
  128varnumbers_args(I, Arity, Term, Min, Vars, Copy) :-
  129    I =< Arity,
  130    !,
  131    arg(I, Term, AT),
  132    arg(I, Copy, CT),
  133    varnumbers(AT, Min, Vars, CT),
  134    I2 is I + 1,
  135    varnumbers_args(I2, Arity, Term, Min, Vars, Copy).
  136varnumbers_args(_, _, _, _, _, _).

roundup_next_power_two(+Int, -NextPower) is det: NextPower is I**2, such that NextPower >= Int.

  142roundup_next_power_two(1, 1) :- !.
  143roundup_next_power_two(N, L) :-
  144    L is 1<<(msb(N-1)+1).

max_var_number(+Term, +Start, -Max) is det

True when Max is the max of Start and the highest numbered $VAR(N) term.

author: - Vitor Santos Costa
Compatibility: - YAP

  154max_var_number(V, Max, Max) :-
  155    var(V),
  156    !.
  157max_var_number('$VAR'(I), Max0, Max) :-
  158    integer(I),
  159    !,
  160    Max is max(I,Max0).
  161max_var_number(S, Max0, Max) :-
  162    functor(S, _, Ar),
  163    max_var_numberl(Ar, S, Max0, Max).
  164
  165max_var_numberl(0, _, Max, Max) :- !.
  166max_var_numberl(I, T, Max0, Max) :-
  167    arg(I, T, Arg),
  168    I2 is I-1,
  169    max_var_number(Arg, Max0, Max1),
  170    max_var_numberl(I2, T, Max1, Max).

varnumbers_names(+Term, -Copy, -VariableNames) is det

If Term is a term with numbered and named variables using the reserved term '$VAR'(X), Copy is a copy of Term where each '$VAR'(X) is consistently replaced by a fresh variable and Bindings is a list X = Var, relating the X terms with the variable it is mapped to.

See also: - numbervars/3, varnumbers/3, read_term/3 using the variable_names option.

  183varnumbers_names(Term, Copy, Bindings) :-
  184    must_be(acyclic, Term),
  185    empty_assoc(Named),
  186    varnumbers_names(Term, Named, BindingAssoc, Copy),
  187    assoc_to_list(BindingAssoc, BindingPairs),
  188    maplist(pair_equals, BindingPairs, Bindings).
  189
  190pair_equals(N-V, N=V).
  191
  192varnumbers_names(Var, Bindings, Bindings, Copy) :-
  193    var(Var),
  194    !,
  195    Copy = Var.
  196varnumbers_names(Var, Bindings, Bindings, Copy) :-
  197    atomic(Var),
  198    !,
  199    Copy = Var.
  200varnumbers_names('$VAR'(Name), Bindings0, Bindings, Copy) :-
  201    !,
  202    (   get_assoc(Name, Bindings0, Copy)
  203    ->  Bindings = Bindings0
  204    ;   put_assoc(Name, Bindings0, Copy, Bindings)
  205    ).
  206varnumbers_names(Term, Bindings0, Bindings, Copy) :-
  207    functor(Term, Name, Arity),
  208    functor(Copy, Name, Arity),
  209    varnumbers_names_args(1, Arity, Term, Bindings0, Bindings, Copy).
  210
  211varnumbers_names_args(I, Arity, Term, Bindings0, Bindings, Copy) :-
  212    I =< Arity,
  213    !,
  214    arg(I, Term, AT),
  215    arg(I, Copy, CT),
  216    varnumbers_names(AT, Bindings0, Bindings1, CT),
  217    I2 is I + 1,
  218    varnumbers_names_args(I2, Arity, Term, Bindings1, Bindings, Copy).
  219varnumbers_names_args(_, _, _, Bindings, Bindings, _)