rewrite.h

Go to the documentation of this file.

#pragma once
 
#include <ranges>
 
#include "mim/world.h"
 
namespace mim {
 
/// Recurseivly rebuilds part of a program **into** the provided World w.r.t.\ Rewriter::map.
/// This World may be different than the World we started with.
class Rewriter {
public:
    Rewriter(World& world)
        : world_(world) {
        push(); // create root map
    }
    Rewriter(World& world) {…}
 
    World& world() { return world_; }
 
    /// @name Stack of Maps
    ///@{
    virtual void push() { old2news_.emplace_back(Def2Def{}); }
    virtual void pop() { old2news_.pop_back(); }
 
    /// Map @p old_def to @p new_def and returns @p new_def.
    /// @returns `new_def`
    const Def* map(const Def* old_def, const Def* new_def) { return old2news_.back()[old_def] = new_def; }
 
    /// Lookup `old_def` by searching in reverse through the stack of maps.
    /// @returns `nullptr` if nothing was found.
    const Def* lookup(const Def* old_def) {
        for (const auto& old2new : old2news_ | std::views::reverse)
            if (auto i = old2new.find(old_def); i != old2new.end()) return i->second;
        return nullptr;
    }
    const Def* lookup(const Def* old_def) {…}
 
    /// @name rewrite
    /// Recursively rewrite old Def%s.
    ///@{
    virtual const Def* rewrite(const Def*);
    virtual const Def* dispatch(const Def*);
 
    virtual const Def* rewrite_imm(const Def*);
    virtual const Def* rewrite_mut(Def*);
 
    virtual const Def* rewrite_arr(const Arr* arr) { return rewrite_seq(arr); }
    virtual const Def* rewrite_pack(const Pack* pack) { return rewrite_seq(pack); }
    virtual const Def* rewrite_seq(const Seq*);
    virtual const Def* rewrite_extract(const Extract*);
    virtual const Def* rewrite_hole(Hole*);
    ///@}
 
private:
    World& world_;
    std::deque<Def2Def> old2news_;
};
class Rewriter {…};
 
class VarRewriter : public Rewriter {
public:
    VarRewriter(World& world)
        : Rewriter(world) {}
    VarRewriter(World& world) {…}
 
    VarRewriter(const Var* var, const Def* arg)
        : Rewriter(arg->world()) {
        add(var, arg);
    }
    VarRewriter(const Var* var, const Def* arg) {…}
 
    void add(const Var* var, const Def* arg) {
        map(var, arg);
        vars_.emplace_back(var);
    }
    void add(const Var* var, const Def* arg) {…}
 
    void push() final {
        Rewriter::push();
        vars_.emplace_back(Vars());
    }
    void push() final {…}
 
    void pop() final {
        vars_.pop_back();
        Rewriter::pop();
    }
    void pop() final {…}
 
    const Def* rewrite(const Def* old_def) final {
        if (old_def->isa<Univ>()) return world().univ();
        if (auto new_def = lookup(old_def)) return new_def;
        if (descend(old_def)) return Rewriter::dispatch(old_def);
        // return map(mut, mut);
        return old_def;
    }
    const Def* rewrite(const Def* old_def) final {…}
 
    bool descend(const Def* old_def) {
        if (auto imm = old_def->isa_imm()) {
            if (imm->has_dep(Dep::Hole)) return true;
            if (imm->local_vars().empty() && imm->local_muts().empty()) return false; // safe to skip
        }
 
        for (const auto& vars : vars_ | std::views::reverse)
            if (vars.has_intersection(old_def->free_vars())) return true;
 
        return false;
    }
    bool descend(const Def* old_def) {…}
 
    const Def* rewrite_mut(Def* mut) final {
        if (auto var = mut->has_var()) {
            auto& vars = vars_.back();
            vars       = world().vars().insert(vars, var);
        }
 
        return Rewriter::rewrite_mut(mut);
    }
    const Def* rewrite_mut(Def* mut) final {…}
 
private:
    Vector<Vars> vars_;
};
class VarRewriter : public Rewriter {…};
 
} // namespace mim