cps.h

Go to the documentation of this file.

#pragma once
 
#include <mim/rewrite.h>
#include <mim/world.h>
 
#include "mim/plug/cps/autogen.h"
 
namespace mim::plug::cps {
 
/// @name cps.cps2ds_dep
/// ```
/// let k: Cn [t: T, Cn U t] = ...;
/// let f: [t: T] → U = cps.cps2ds_dep (lm (t': T): * = [t → t']U) k;
/// ```
///@{
inline const Def* op_cps2ds_dep(const Def* k) {
    auto& w     = k->world();
    auto K      = Pi::isa_cn(k->type());
    auto [T, R] = K->doms<2>();
    auto U      = Pi::isa_cn(R)->dom();
    auto l      = w.mut_lam(T, w.type())->set("Uf");
    auto body   = U;
 
    // U only refers to `var#0`; the second component is a placeholder that is never projected.
    if (auto [dom, var] = K->dom()->isa_binder<Sigma>(); dom)
        body = VarRewriter(var, w.tuple({l->var(), w.tuple()})).rewrite(U);
    l->set(true, body);
 
    return w.app(w.app(w.app(w.annex<cps::cps2ds_dep>(), T), l), k);
}
///@}
 
} // namespace mim::plug::cps