json_stream.h

Go to the documentation of this file.

/*******************************************************************\
 
Module:
 
Author: Peter Schrammel
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_JSON_STREAM_H
#define CPROVER_UTIL_JSON_STREAM_H
 
#include <iosfwd>
#include <memory>
 
#include "json.h"
#include "invariant.h"
 
class json_stream_objectt;
class json_stream_arrayt;
 
class json_streamt
{
public:
  void close()
  {
    if(open)
    {
      output_child_stream();
      output_finalizer();
      open = false;
    }
  }
 
  virtual ~json_streamt() = default;
 
protected:
  json_streamt(std::ostream &_out, unsigned _indent)
    : open(true), out(_out), indent(_indent), first(true), child_stream(nullptr)
  {
  }
 
  bool open;
  std::ostream &out;
  unsigned indent;
 
  bool first;
 
  typedef std::map<std::string, jsont> objectt;
  objectt object;
 
  std::unique_ptr<json_streamt> child_stream;
  json_stream_arrayt &create_child_stream_array();
  json_stream_objectt &create_child_stream_object();
 
  void output_delimiter();
 
  // To be overridden by derived classes:
  virtual void output_child_stream() = 0;
  virtual void output_finalizer() = 0;
};
 
class json_stream_arrayt : public json_streamt
{
public:
  explicit json_stream_arrayt(std::ostream &out, unsigned indent = 0);
 
  ~json_stream_arrayt() override
  {
    close();
  }
 
  void push_back(const jsont &json)
  {
    PRECONDITION(open);
    // To ensure consistency of the output, we flush and
    // close the current child stream before printing the given element.
    output_child_stream();
    output_delimiter();
    json.output_rec(out, indent + 1);
  }
 
  jsont &push_back()
  {
    PRECONDITION(open);
    // To ensure consistency of the output, we flush and
    // close the current child stream before adding the given element.
    output_child_stream();
    // We store the new element in the object map.
    return object["array_element"];
  }
 
  json_stream_objectt &push_back_stream_object();
  json_stream_arrayt &push_back_stream_array();
 
protected:
  void output_child_stream() override;
  void output_finalizer() override;
};
 
class json_stream_objectt : public json_streamt
{
public:
  explicit json_stream_objectt(std::ostream &out, unsigned indent = 0);
 
  jsont &operator[](const std::string &key)
  {
    return object[key];
  }
 
  ~json_stream_objectt() override
  {
    close();
  }
 
  const jsont &operator[](const std::string &key) const
  {
    objectt::const_iterator it = object.find(key);
    if(it == object.end())
      return jsont::null_json_object;
    else
      return it->second;
  }
 
  void push_back(const std::string &key, const jsont &json)
  {
    PRECONDITION(open);
    // Check the key is not already due to be output later:
    PRECONDITION(!object.count(key));
    // To ensure consistency of the output, we flush and
    // close the current child stream before printing the given element.
    output_child_stream();
    output_delimiter();
    jsont::output_key(out, key);
    json.output_rec(out, indent + 1);
  }
 
  json_stream_objectt &push_back_stream_object(const std::string &key);
  json_stream_arrayt &push_back_stream_array(const std::string &key);
 
protected:
  void output_child_stream() override;
  void output_finalizer() override;
};
 
#endif // CPROVER_UTIL_JSON_STREAM_H