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