Next: , Previous: univ, Up: Top   [Contents]


93 varset

%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%--------------------------------------------------%
% Copyright (C) 1993-2000,2002-2007, 2009-2011 The University of Melbourne.
% This file may only be copied under the terms of the GNU Library General
% Public License - see the file COPYING.LIB in the Mercury distribution.
%--------------------------------------------------%
%
% File: varset.m.
% Main author: fjh.
% Stability: low.
%
% This file provides facilities for manipulating collections of
% variables and terms.
% It provides the 'varset' ADT. A varset is a set of variables.
% (These variables are object-level variables, and are represented
% as ground terms, so it might help to think of them as "variable ids"
% rather than variables.)
% Associated with each variable there can be both a name and a value
% (binding).
%
% There may be some design flaws in the relationship between varset.m, and
% term.m.  Once we have implemented unique modes and destructive assignment, we
% will need to rethink the design;  we may end up modifying these modules
% considerably, or we may end up making new single-threaded versions of these
% modules.
%
%--------------------------------------------------%
%--------------------------------------------------%

:- module varset.
:- interface.

:- import_module assoc_list.
:- import_module list.
:- import_module map.
:- import_module maybe.
:- import_module set.
:- import_module term.

%--------------------------------------------------%

:- type varset(T).

:- type varset  ==  varset(generic).

%--------------------------------------------------%

    % Construct an empty varset.
    %
:- func init = varset(T).
:- pred init(varset(T)::out) is det.

    % Check whether a varset is empty.
    %
:- pred is_empty(varset(T)::in) is semidet.

%--------------------------------------------------%

    % Create a new variable.
    %
:- pred new_var(var(T)::out, varset(T)::in, varset(T)::out) is det.

    % Create a new named variable.
    %
:- pred new_named_var(string::in, var(T)::out,
    varset(T)::in, varset(T)::out) is det.

    % Create a new named variable with a unique (w.r.t. the
    % varset) number appended to the name.
    %
:- pred new_uniquely_named_var(string::in, var(T)::out,
    varset(T)::in, varset(T)::out) is det.

    % Create a new variable, and maybe give it a name.
    %
:- pred new_maybe_named_var(maybe(string)::in, var(T)::out,
    varset(T)::in, varset(T)::out) is det.

    % Create multiple new variables.
    %
:- pred new_vars(int::in, list(var(T))::out,
    varset(T)::in, varset(T)::out) is det.

%--------------------------------------------------%

    % Delete the name and value for a variable.
    %
:- func delete_var(varset(T), var(T)) = varset(T).
:- pred delete_var(var(T)::in, varset(T)::in, varset(T)::out) is det.

    % Delete the names and values for a list of variables.
    %
:- func delete_vars(varset(T), list(var(T))) = varset(T).
:- pred delete_vars(list(var(T))::in, varset(T)::in, varset(T)::out)
    is det.

    % Delete the names and values for a sorted list of variables.
    % (If the list is not sorted, the result will be either an abort
    % or incorrect output.)
    %
:- func delete_sorted_vars(varset(T), list(var(T))) = varset(T).
:- pred delete_sorted_vars(list(var(T))::in,
    varset(T)::in, varset(T)::out) is det.

%--------------------------------------------------%

    % Return a list of all the variables in a varset.
    %
:- func vars(varset(T)) = list(var(T)).
:- pred vars(varset(T)::in, list(var(T))::out) is det.

%--------------------------------------------------%

    % Set the name of a variable.
    %
:- func name_var(varset(T), var(T), string) = varset(T).
:- pred name_var(var(T)::in, string::in,
    varset(T)::in, varset(T)::out) is det.

    % Lookup the name of a variable;
    % If it doesn't have one, create on using V_ as a prefix.
    %
:- func lookup_name(varset(T), var(T)) = string.
:- pred lookup_name(varset(T)::in, var(T)::in, string::out) is det.

    % Lookup the name of a variable;
    % if it doesn't have one, create one using the specified prefix.
    %
:- func lookup_name(varset(T), var(T), string) = string.
:- pred lookup_name(varset(T)::in, var(T)::in, string::in, string::out)
    is det.

    % Lookup the name of a variable;
    % fail if it doesn't have one.
    %
:- pred search_name(varset(T)::in, var(T)::in, string::out) is semidet.

%--------------------------------------------------%

    % Bind a value to a variable.
    % This will overwrite any existing binding.
    %
:- func bind_var(varset(T), var(T), term(T)) = varset(T).
:- pred bind_var(var(T)::in, term(T)::in,
    varset(T)::in, varset(T)::out) is det.

    % Bind a set of terms to a set of variables.
    %
:- func bind_vars(varset(T), substitution(T)) = varset(T).
:- pred bind_vars(substitution(T)::in,
    varset(T)::in, varset(T)::out) is det.

    % Lookup the value of a variable.
    %
:- pred search_var(varset(T)::in, var(T)::in, term(T)::out) is semidet.

%--------------------------------------------------%

    % Get the bindings for all the bound variables.
    %
:- func lookup_vars(varset(T)) = substitution(T).
:- pred lookup_vars(varset(T)::in, substitution(T)::out) is det.

    % Get the bindings for all the bound variables.
    %
:- func get_bindings(varset(T)) = substitution(T).
:- pred get_bindings(varset(T)::in, substitution(T)::out) is det.

    % Set the bindings for all the bound variables.
    %
:- func set_bindings(varset(T), substitution(T)) = varset(T).
:- pred set_bindings(varset(T)::in, substitution(T)::in,
    varset(T)::out) is det.

%--------------------------------------------------%

    % Combine two different varsets, renaming apart:
    % merge_renaming(VarSet0, NewVarSet, VarSet, Subst) is true
    % iff VarSet is the varset that results from joining a suitably renamed
    % version of NewVarSet to VarSet0. (Any bindings in NewVarSet are ignored.)
    % Renaming will map each variable in NewVarSet to the corresponding
    % fresh variable in VarSet.
    %
:- pred merge_renaming(varset(T)::in, varset(T)::in, varset(T)::out,
    renaming(T)::out) is det.

    % Same as merge_renaming, except that the names of variables
    % in NewVarSet are not included in the final varset.
    % This is useful if create_name_var_map needs to be used
    % on the resulting varset.
    %
:- pred merge_renaming_without_names(varset(T)::in,
    varset(T)::in, varset(T)::out, renaming(T)::out) is det.

    % Does the same job as merge_renaming, but returns the renaming
    % as a general substitution in which all the terms in the range happen
    % to be variables.
    %
    % Consider using merge_renaming instead.
    %
:- pred merge_subst(varset(T)::in, varset(T)::in, varset(T)::out,
    substitution(T)::out) is det.
:- pragma obsolete(merge_subst/4).

    % Same as merge_subst, except that the names of variables
    % in NewVarSet are not included in the final varset.
    % This is useful if create_name_var_map needs to be used
    % on the resulting varset.
    %
    % Consider using merge_renaming_without_names instead.
    %
:- pred merge_subst_without_names(varset(T)::in,
    varset(T)::in, varset(T)::out, substitution(T)::out) is det.
:- pragma obsolete(merge_subst_without_names/4).

    % merge(VarSet0, NewVarSet, Terms0, VarSet, Terms):
    %
    % As merge_renaming, except instead of returning the renaming,
    % this predicate applies it to the given list of terms.
    %
:- pred merge(varset(T)::in, varset(T)::in, list(term(T))::in,
    varset(T)::out, list(term(T))::out) is det.

    % Same as merge, except that the names of variables
    % in NewVarSet are not included in the final varset.
    % This is useful if create_name_var_map needs to be used
    % on the resulting varset.
    %
:- pred merge_without_names(varset(T)::in, varset(T)::in,
    list(term(T))::in, varset(T)::out, list(term(T))::out) is det.

%--------------------------------------------------%

    % Create a map from names to variables.
    % Each name is mapped to only one variable, even if a name is
    % shared by more than one variable. Therefore this predicate
    % is only really useful if it is already known that no two
    % variables share the same name.
    %
:- func create_name_var_map(varset(T)) = map(string, var(T)).
:- pred create_name_var_map(varset(T)::in, map(string, var(T))::out)
    is det.

    % Return an association list giving the name of each variable.
    % Every variable has an entry in the returned association list,
    % even if it shares its name with another variable.
    %
:- func var_name_list(varset(T)) = assoc_list(var(T), string).
:- pred var_name_list(varset(T)::in, assoc_list(var(T), string)::out)
    is det.

    % Given a list of variable and varset in which some variables have
    % no name but some other variables may have the same name,
    % return another varset in which every variable has a unique name.
    % If necessary, names will have suffixes added on the end;
    % the second argument gives the suffix to use.
    %
:- func ensure_unique_names(list(var(T)), string, varset(T))
    = varset(T).
:- pred ensure_unique_names(list(var(T))::in,
    string::in, varset(T)::in, varset(T)::out) is det.

%--------------------------------------------------%

    % Given a varset and a set of variables, remove the names
    % and values of any other variables stored in the varset.
    %
:- func select(varset(T), set(var(T))) = varset(T).
:- pred select(set(var(T))::in, varset(T)::in, varset(T)::out) is det.

    % Given a varset and a list of variables, construct a new varset
    % containing one variable for each one in the list (and no others).
    % Also return a substitution mapping the selected variables in the
    % original varset into variables in the new varset. The relative
    % ordering of variables in the original varset is maintained.
    %
:- pred squash(varset(T)::in, list(var(T))::in,
    varset(T)::out, renaming(T)::out) is det.

    % Coerce the types of the variables in a varset.
    %
:- func coerce(varset(T)) = varset(U).
:- pred coerce(varset(T)::in, varset(U)::out) is det.

%--------------------------------------------------%
%--------------------------------------------------%


Next: , Previous: univ, Up: Top   [Contents]