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, _)