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:- autoload(library(apply),[maplist/3]).   43:- autoload(library(assoc),
   44	    [empty_assoc/1,assoc_to_list/2,get_assoc/3,put_assoc/4]).   45:- autoload(library(error),[must_be/2]).

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

   78numbervars(Term) :-
   79    numbervars(Term, 0, _).

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

   86varnumbers(Term, Copy) :-
   87    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

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

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

  144roundup_next_power_two(1, 1) :- !.
  145roundup_next_power_two(N, L) :-
  146    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

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

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