ProofPrinter.hpp

/*
 
Copyright © 2023-26 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 PROOFPRINTER_HPP
#define PROOFPRINTER_HPP
 
#include<iostream>
#include<fstream>
#include<filesystem>
 
#include "Stack.hpp"
#include "TableauProof.hpp"
 
using std::filesystem::path;
 
using ProofLine = pair<string, vector<size_t>>;
using ProofType = vector<ProofLine>;
 
void show_internal_proof(const ProofType&);
 
class ProofPrinter {
private:
  Stack* p;
  string make_LaTeX_state(StackItem*) const;
  string make_LaTeX_subtree(StackItem*) const;
  string make_LaTeX_start(const path&, const path&, const string&) const;
  string make_LaTeX_end() const;
public:
  ProofPrinter() : p(nullptr) {};
  ProofPrinter(Stack* _p) : p(_p) {};
  inline void set_proof(Stack* _p) { p = _p; }
  inline void clear() { p = nullptr; }
  void make_LaTeX(const path&, const path&, const string&);
  void make_LaTeX_connection_tableau(const path&, const path&, const string&, 
                                     Matrix*, VariableIndex*, TermIndex*);
  void make_graphviz_connection_tableau(const path&, const path&,
                                     Matrix*, VariableIndex*, TermIndex*);
  void make_Prolog(const path&);
  void show_Prolog();
  pair<string, unordered_set<string>> make_tptp(Matrix*, VariableIndex*, TermIndex*);
  vector<pair<string, vector<size_t>>> make_internal() const;
};
 
#endif