Variable Class Reference

Basic representation of variables. More...

#include <Variable.hpp>

Collaboration diagram for Variable:

Public Member Functions
	Variable (const Variable &)=delete
	Explicitly disallow copying as this is a very bad idea.
	Variable (const Variable &&)=delete
Variable &	operator= (const Variable &)=delete
Variable &	operator= (const Variable &&)=delete
ID	get_id () const
	Self-explanatory access function.
string	get_name () const
	Self-explanatory access function.
string	to_string (bool=false) const
	Convert to a (coloured) string.
bool	is_subbed () const
	Is this variable currently substituted?
Term *	get_subbed_term () const
	Get the current substitution, or nullptr.
void	remove_substitution ()
	Self-explanatory, but be careful!
void	substitute (Term *t)
	Self-explanatory, but be careful!
bool	subbed_is_function () const
	Is the variable now a function, taking substitution into account?
bool	subbed_is_variable () const
	Is the variable still in fact a variable, taking substitution into account?
Variable *	subbed_variable () const
	If the variable is unsubbed then return "this"; otherwise a pointer to the variable at the end of a chain of substitutions of variables for variables.
bool	contains_variable (Variable *) const
	Does the substitution turn the variable into something that includes the variable passed?
Function *	get_subbed_f () const
	If there is a chain of substitutions ending in a function, find that function.
Arity	get_subbed_arity () const
	If there is a chain of substitutions ending in a function, find that function's arity.
Term *	skip_leading_variables () const
	It may be that there is a chain of substitutions attached to this variable: skip the leading ones.
string	make_LaTeX (bool=false) const
	Convert the Variable to a useable LaTeX representation.

Private Member Functions
	Variable ()
	Constructors: you can only construct un-substituted variables.
	Variable (ID new_id)
	Variable (ID new_id, const string &new_name)

Private Attributes
ID	id
string	name
Term *	substitution

Friends
class	VariableIndex
ostream &	operator<< (ostream &, const Variable &)
	This is mainly for debugging. If you want actual representations then use Variable::to_string or similar.

Detailed Description

Basic representation of variables.

This way of treating variables makes substitution and the removal thereof extremely easy. BUT, you have to be somewhat careful, because once substituted you may no longer have a variable.

A Variable has an id and a name. Substitution is by way of setting the substitution pointer from nullptr to the address of a Term.

Some of the implementation is in Term.cpp in order to allow the compiler to do things in the right order.

You should never try to construct one of these yourself. Only do it by way of the VariableIndex.

Definition at line 58 of file Variable.hpp.

Constructor & Destructor Documentation

Variable() [1/4]

Variable::Variable ( )

inlineprivate

Constructors: you can only construct un-substituted variables.

These are private because in order to enforce sharing the only place you should ever construct one is in the VariableIndex, which is a friend.

Definition at line 71 of file Variable.hpp.

: id(0), name(), substitution(nullptr) {}

Variable() [2/4]

Variable::Variable ( ID new_id )

inlineprivate

Definition at line 72 of file Variable.hpp.

: id(new_id), name(), substitution(nullptr) {}

Variable() [3/4]

Variable::Variable ( ID new_id, const string & new_name )

inlineprivate

Definition at line 73 of file Variable.hpp.

    : id(new_id), name(new_name), substitution(nullptr) {}

Variable() [4/4]

Variable::Variable ( const Variable & )

delete

Explicitly disallow copying as this is a very bad idea.

You should never have to do this, and by explicitly disallowing it we help the compiler to find our errors for us.

Member Function Documentation

contains_variable()

bool Variable::contains_variable

(

Variable *

v2

)

const

Does the substitution turn the variable into something that includes the variable passed?

Note that this acts on the eventual term, so if you look for something that has itself been subbed then the answer is "no".

Parameters

v2	Pointer to Variable to search for.

Definition at line 363 of file Term.cpp.

                                                   {
    if (substitution == nullptr)
        return this==v2;
    else
        return substitution->contains_variable(v2);
}

get_id()

ID Variable::get_id ( ) const

inline

Self-explanatory access function.

Definition at line 90 of file Variable.hpp.

{ return id; }

get_name()

string Variable::get_name ( ) const

inline

Self-explanatory access function.

Only return the variable name – do not follow substitutions.

Definition at line 96 of file Variable.hpp.

{ return name; }

get_subbed_arity()

Arity Variable::get_subbed_arity

(

)

const

If there is a chain of substitutions ending in a function, find that function's arity.

Definition at line 379 of file Term.cpp.

                                       {
    if (substitution == nullptr) {
        cerr << "There is no arity to be found..." << endl;
        return 0;
    }
    else
        return substitution->get_subbed_arity();
}

get_subbed_f()

Function * Variable::get_subbed_f

(

)

const

If there is a chain of substitutions ending in a function, find that function.

Definition at line 370 of file Term.cpp.

                                       {
    if (substitution == nullptr) {
        cerr << "There is no function name to be found..." << endl;
        return nullptr;
    }
    else
        return substitution->get_subbed_f();
}

get_subbed_term()

Term * Variable::get_subbed_term ( ) const

inline

Get the current substitution, or nullptr.

Definition at line 110 of file Variable.hpp.

{ return substitution; }

is_subbed()

bool Variable::is_subbed ( ) const

inline

Is this variable currently substituted?

Definition at line 106 of file Variable.hpp.

{ return (substitution != nullptr); }

make_LaTeX()

string Variable::make_LaTeX

(

bool

subbed = false

)

const

Convert the Variable to a useable LaTeX representation.

Note that this makes a limited attempt to deal with all situations. Anonymous variables will work fine, but if your named variables have symbols that need an escape or similar it may not work as expected.

Assumes that the output will be typeset in math mode. Parameter implements substitutions if true.

Parameters

subbed

Include effect of substitution if true.

Definition at line 329 of file Term.cpp.

                                             {
 if (subbed && substitution != nullptr)
   return substitution->make_LaTeX(subbed);
 else {
   string s ("\\text{");
   s += latex_escape_characters(name);
   s += "}";
   return s;
 }
}

remove_substitution()

void Variable::remove_substitution ( )

inline

Self-explanatory, but be careful!

As long as your Term* pointers are only generated by the TermIndex, then you don't have to worry about memory allocation or de-allocation.

If you did a "new Term" anywhere yourself then you must live with the consequences.

Definition at line 121 of file Variable.hpp.

{ substitution = nullptr; }

skip_leading_variables()

Term * Variable::skip_leading_variables

(

)

const

It may be that there is a chain of substitutions attached to this variable: skip the leading ones.

When doing unification we actually want a pointer either to the final variable in a chain or to the first term that's a function. This returns it.

Definition at line 388 of file Term.cpp.

                                             {
  if (substitution != nullptr) {
    return substitution->skip_leading_variables();
  }
  cerr << "Stop it! You're trying to skip something inappropriate!" << endl;
  return nullptr;
}

subbed_is_function()

bool Variable::subbed_is_function

(

)

const

Is the variable now a function, taking substitution into account?

Note that this it false if the variable is unsubstituted.

Definition at line 340 of file Term.cpp.

                                        {
    if (substitution == nullptr)
        return false;
    else
        return substitution->subbed_is_function();
}

subbed_is_variable()

bool Variable::subbed_is_variable

(

)

const

Is the variable still in fact a variable, taking substitution into account?

Note that this it true if the variable is unsubstituted.

Definition at line 347 of file Term.cpp.

                                        {
    if (substitution == nullptr)
        return true;
    else
        return substitution->subbed_is_variable();
}

subbed_variable()

Variable * Variable::subbed_variable

(

)

const

If the variable is unsubbed then return "this"; otherwise a pointer to the variable at the end of a chain of substitutions of variables for variables.

You should probably only call this if you know the substitution is a chain of variables. (Otherwise you're getting a nullptr and an error message.)

Definition at line 354 of file Term.cpp.

                                          {
    if (substitution == nullptr) {
        Variable* p = const_cast<Variable*>(this);
        return p;
    }
    else
        return substitution->subbed_variable();
}

substitute()

void Variable::substitute ( Term * t )

inline

Self-explanatory, but be careful!

See the documentation for remove_substitution.

Parameters

t	Pointer to Term to substitute.

Definition at line 129 of file Variable.hpp.

{ substitution = t; }

to_string()

string Variable::to_string

(

bool

subbed = false

)

const

Convert to a (coloured) string.

Parameters

subbed

Include effect of substitution if true.

Definition at line 319 of file Term.cpp.

                                            {
  colour_string::ColourString cs(params::use_colours);
  string s = cs(name).lblue();
  if (subbed && substitution != nullptr) {
    s += unicode_symbols::LogSym::subbed;
    s += substitution->to_string(subbed);
  }
  return s;
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const Variable & v )

friend

This is mainly for debugging. If you want actual representations then use Variable::to_string or similar.

Definition at line 33 of file Variable.cpp.

                                                     {
    out << "Var: " << setw(params::output_width) << v.name
        <<" ID: " << setw(params::output_width) << v.id;
    if (v.substitution != nullptr)
        out << " Subbed";
    return out;
}

VariableIndex

friend class VariableIndex

friend

Definition at line 199 of file Variable.hpp.

Member Data Documentation

id

ID Variable::id

private

Definition at line 60 of file Variable.hpp.

name

string Variable::name

private

Definition at line 61 of file Variable.hpp.

substitution

Term* Variable::substitution

private

Definition at line 62 of file Variable.hpp.

---

The documentation for this class was generated from the following files:

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/terms/Variable.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/terms/Term.cpp