Variable.hpp

/*
 
Copyright © 2023-24 Sean Holden. All rights reserved.
 
*/
/*
 
This file is part of Connect++.
 
Connect++ is free software: you can redistribute it and/or modify it 
under the terms of the GNU General Public License as published by the 
Free Software Foundation, either version 3 of the License, or (at your 
option) any later version.
 
Connect++ is distributed in the hope that it will be useful, but WITHOUT 
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for 
more details.
 
You should have received a copy of the GNU General Public License along 
with Connect++. If not, see <https://www.gnu.org/licenses/>. 
 
*/
 
#ifndef VARIABLE_HPP
#define VARIABLE_HPP
 
#include<iostream>
#include<iomanip>
#include<string>
#include<vector>
 
#include "LaTeXUtilities.hpp"
#include "Function.hpp"
 
class Term;
 
using std::string;
using std::ostream;
 
class Variable {
private:
    ID id;
    string name;
    Term* substitution;
    Variable() : id(0), name(), substitution(nullptr) {}
    Variable(ID new_id) : id(new_id), name(), substitution(nullptr) {}
    Variable(ID new_id, const string& new_name)
    : id(new_id), name(new_name), substitution(nullptr) {}
public:
    friend class VariableIndex;
    Variable(const Variable&) = delete;
    Variable(const Variable&&) = delete;
    Variable& operator=(const Variable&) = delete;
    Variable& operator=(const Variable&&) = delete;
    //----------------------------------------------------------------------
    inline ID get_id() const { return id; }
    //----------------------------------------------------------------------
    inline string get_name() const { return name; }
    //----------------------------------------------------------------------
    string to_string(bool = false) const;
    //----------------------------------------------------------------------
    inline bool is_subbed() const { return (substitution != nullptr); }
    //----------------------------------------------------------------------
    inline Term* get_subbed_term() const { return substitution; }
    //----------------------------------------------------------------------
    inline void remove_substitution() { substitution = nullptr; }
    //----------------------------------------------------------------------
    inline void substitute(Term* t) { substitution = t; }
    //----------------------------------------------------------------------
    bool subbed_is_function() const;
    //----------------------------------------------------------------------
    bool subbed_is_variable() const;
    //----------------------------------------------------------------------
    Variable* subbed_variable() const;
    //----------------------------------------------------------------------
    bool contains_variable(Variable*) const;
    //----------------------------------------------------------------------
    Function* get_subbed_f() const;
    //----------------------------------------------------------------------
    Arity get_subbed_arity() const;
    //----------------------------------------------------------------------
    Term* skip_leading_variables() const;
    //----------------------------------------------------------------------
    string make_LaTeX(bool = false) const;
    //----------------------------------------------------------------------
 
    friend ostream& operator<<(ostream&, const Variable&);
};
 
#endif