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)).
  45
  46/** <module> Utilities for numbered terms
  47
  48This  library  provides  the  inverse   functionality  of  the  built-in
  49numbervars/3. Note that this library suffers  from the known issues that
  50'$VAR'(X) is a normal Prolog term and, -unlike the built-in numbervars-,
  51the inverse predicates do _not_  process   cyclic  terms.  The following
  52predicate is true for  any  acyclic   term  that  contains no '$VAR'(X),
  53integer(X) terms and no constraint variables:
  54
  55  ==
  56  always_true(X) :-
  57        copy_term(X, X2),
  58        numbervars(X),
  59        varnumbers(X, Copy),
  60        Copy =@= X2.
  61  ==
  62
  63@see    numbervars/4, =@=/2 (variant/2).
  64@compat This library was introduced by Quintus and available in
  65        many related implementations, although not with exactly the
  66        same set of predicates.
  67*/
  68
  69%!  numbervars(+Term) is det.
  70%
  71%   Number  variables  in  Term   using    $VAR(N).   Equivalent  to
  72%   numbervars(Term, 0, _).
  73%
  74%   @see numbervars/3, numbervars/4
  75
  76numbervars(Term) :-
  77    numbervars(Term, 0, _).
  78
  79%!  varnumbers(+Term, -Copy) is det.
  80%
  81%   Inverse  of  numbervars/1.  Equivalent  to  varnumbers(Term,  0,
  82%   Copy).
  83
  84varnumbers(Term, Copy) :-
  85    varnumbers(Term, 0, Copy).
  86
  87%!  varnumbers(+Term, +Start, -Copy) is det.
  88%
  89%   Inverse of numbervars/3. True when Copy is   a copy of Term with
  90%   all variables numbered >= Start   consistently replaced by fresh
  91%   variables. Variables in Term are _shared_  with Copy rather than
  92%   replaced by fresh variables.
  93%
  94%   @error domain_error(acyclic_term, Term) if Term is cyclic.
  95%   @compat Quintus, SICStus.  Not in YAP version of this library
  96
  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(_, _, _, _, _, _).
 137
 138%!  roundup_next_power_two(+Int, -NextPower) is det.
 139%
 140%   NextPower is I**2, such that NextPower >= Int.
 141
 142roundup_next_power_two(1, 1) :- !.
 143roundup_next_power_two(N, L) :-
 144    L is 1<<(msb(N-1)+1).
 145
 146%!  max_var_number(+Term, +Start, -Max) is det.
 147%
 148%   True when Max is the  max  of   Start  and  the highest numbered
 149%   $VAR(N) term.
 150%
 151%   @author Vitor Santos Costa
 152%   @compat YAP
 153
 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).
 171
 172%!  varnumbers_names(+Term, -Copy, -VariableNames) is det.
 173%
 174%   If Term is a term with numbered   and  named variables using the
 175%   reserved term '$VAR'(X), Copy  is  a   copy  of  Term where each
 176%   '$VAR'(X) is consistently  replaced  by   a  fresh  variable and
 177%   Bindings is a list `X = Var`,   relating  the `X` terms with the
 178%   variable it is mapped to.
 179%
 180%   @see numbervars/3, varnumbers/3, read_term/3 using the
 181%   `variable_names` option.
 182
 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, _).