program.hh

#pragma once
 
#include <clingo/input/statement.hh>
 
#include <clingo/core/logger.hh>
 
#include <clingo/util/enum.hh>
#include <clingo/util/ordered_map.hh>
#include <clingo/util/ordered_set.hh>
 
namespace CppClingo::Input {
 
 
enum class ProjectionMode : uint8_t {
    disabled = 0,  
    anonymous = 1, 
    pure = 2,      
};
 
struct RewriteOptions {
    ProjectionMode project_mode = ProjectionMode::pure;
    bool project_anonymous = false;
};
 
using ConstMap = Util::ordered_map<SharedString, std::pair<StmConst, SharedSymbol>>;
 
using ParamUnmap = Util::ordered_map<SharedString, SharedString>;
 
struct ProgramPart {
    StmProgram part;
    StmVec stms;
    SymbolVec facts;
};
using ProgramPartVec = std::vector<ProgramPart>;
 
class UnprocessedProgram {
  public:
    void add(SymbolStore &store, Stm stm);
 
    void clear();
 
    [[nodiscard]] auto empty() const -> bool;
 
    void mark(SymbolCollector &gc) const;
 
    void join(UnprocessedProgram const &other);
 
    [[nodiscard]] auto parts() const -> ProgramPartVec const & { return parts_; }
    [[nodiscard]] auto meta_stms() const -> StmVec const & { return meta_stms_; }
  private:
    ProgramPartVec parts_;
    StmVec meta_stms_;
};
 
enum class ComponentType : uint8_t {
    positive = 1,    
    single_pass = 2, 
};
CLINGO_ENABLE_BITSET_ENUM(ComponentType);
 
struct Component {
    std::vector<Stm const *> stms;
    Util::unordered_set<std::tuple<String, size_t, bool>> depend;
    Util::ordered_map<Term const *, Util::ordered_set<Term const *>> incomplete;
    ComponentType type;
};
 
using Components = std::vector<std::vector<Component>>;
 
class DependencyBuilder {
  public:
    virtual ~DependencyBuilder() = default;
    void param(ProgramParam const &param) { do_param(param); }
    void meta(std::vector<Stm> const &stms) { do_meta(stms); }
    void fact(std::vector<Symbol> const &facts) { do_fact(facts); }
    [[nodiscard]] auto components(Components const &comps) -> bool { return do_components(comps); }
 
  private:
    virtual void do_param(ProgramParam const &param) = 0;
    virtual void do_meta(std::vector<Stm> const &stms) = 0;
    virtual void do_fact(SymbolVec const &facts) = 0;
    [[nodiscard]] virtual auto do_components(Components const &comps) -> bool = 0;
};
 
class Program {
  public:
    Program(RewriteOptions opts) : opts_{opts} {}
    void join(Logger &log, SymbolStore &store, UnprocessedProgram const &prg);
    template <class F> void visit_stms(SymbolStore &store, F fun) const {
        for (auto const &stm : script_stms_) {
            fun(stm);
        }
        if (default_parts_) {
            fun(*default_parts_);
        }
        for (auto const &stm : defined_stms_) {
            fun(stm);
        }
        for (auto const &[id, sym] : const_map_) {
            fun(Stm{StmConst{sym.first.loc(), sym.first.type(), sym.first.name(),
                             TermSymbol{location(sym.first.value()), *sym.second}}});
        }
        for (auto const &stm : thy_stms_) {
            fun(stm);
        }
        for (auto const &stm : meta_stms_) {
            fun(stm);
        }
        for (auto const &[sig, part] : parts_) {
            auto pum = param_map_(store, part);
            auto loc = part.part.loc();
            auto ids = SharedStringArray{pum.begin(), pum.end(), [](auto const &x) { return *x.second; }};
            fun(StmProgram{loc, *sig.first, std::move(ids)});
            for (auto const &fact : part.facts) {
                fun(Stm{StmRule{loc, HdLitSimple{LitSymbolic{loc, Sign::none, TermSymbol{loc, fact}}}, BdLitArray{}}});
            }
            for (auto const &stm : part.stms) {
                if (auto unmapped = unmap_(store, pum, stm); unmapped) {
                    fun(std::move(unmapped).value());
                } else {
                    fun(stm);
                }
            }
        }
    }
    auto meta_stms() -> StmVec const & { return meta_stms_; }
 
    [[nodiscard]] auto analyze(SymbolStore &store, ProgramParamVec const &params, DependencyBuilder &bld) const -> bool;
 
    void mark(SymbolCollector &gc) const;
 
    void check(Logger &log);
 
    [[nodiscard]] auto theory_directives() const -> TheorySigVec;
 
    [[nodiscard]] auto const_map() const -> ConstMap const & { return const_map_; };
 
    void mark_sig(Input::Sig const &sig);
 
    [[nodiscard]] auto default_parts() -> std::optional<StmParts> & { return default_parts_; }
 
  private:
    using Signature = std::pair<SharedString, size_t>;
    using PartMap = Util::ordered_map<Signature, ProgramPart>;
 
    [[nodiscard]] static auto param_map_(SymbolStore &store, ProgramPart const &part) -> ParamUnmap;
    [[nodiscard]] static auto unmap_(SymbolStore &store, ParamUnmap const &pum, Stm const &stm) -> std::optional<Stm>;
 
    RewriteOptions opts_;
    StmVec meta_stms_;
    std::vector<StmScript> script_stms_;
    std::vector<StmDefined> defined_stms_;
    std::vector<StmTheory> thy_stms_;
    std::optional<StmParts> default_parts_;
    PartMap parts_;
    ConstMap const_map_;
    SharedSigSet provide_;
    Util::ordered_map<SharedSig, Location> depend_;
    size_t depend_offset_ = 0;
};
 
 
} // namespace CppClingo::Input