wip: working on #126 and #117

dialects/clos/clos.cpp

@@ -20,6 +20,37 @@
 
 namespace thorin::clos {
 
+template<bool type>
+size_t env_idx(const Def* def) {
+    size_t n = def->num_projs();
+    if (n == 0) return 0;
+    auto first = def->proj(n, 0_s);
+    if ((type && match<mem::M>(first)) || (!type && match<mem::M>(first->type()))) return 1;
+    return 0;
+}
+
+template<bool type>
+const Def* env_insert(const Def* def, const Def* env) {
+    auto& w  = env->world();
+    size_t n = def->num_projs();
+    size_t x = env_idx<type>(def);
+
+    DefArray new_ops(n + 1);
+    for (size_t i = 0, j = 0; i != n + 1; ++i) new_ops[i] = i == x ? env : def->proj(n, j++);
+
+    return type ? w.sigma(new_ops) : w.tuple(new_ops);
+}
+
+Sigma* pi2clos(const Pi* pi) {
+    auto& world  = pi->world();
+    auto sigma   = world.nom_sigma(world.type(), 3, world.dbg("Clos"))->set(0, world.type());
+    auto env_t   = sigma->var(0_s);
+    auto new_dom = env_insert<true>(pi->dom(), env_t);
+    sigma->set(1, world.pi(new_dom, pi->codom()));
+    sigma->set(2, env_t);
+    return sigma;
+}
+
 /*
  * ClosLit
  */
@@ -99,7 +130,8 @@ const Sigma* isa_clos_type(const Def* def) {
     return (pi && pi->is_cn() && pi->num_ops() > 1_u64 && pi->dom(Clos_Env_Param) == var) ? sig : nullptr;
 }
 
-Sigma* clos_type(const Pi* pi) { return ctype(pi->world(), pi->doms(), nullptr)->as_nom<Sigma>(); }
+Sigma* clos_type(const Pi* pi) { return pi2clos(pi); }
+    //return ctype(pi->world(), pi->doms(), nullptr)->as_nom<Sigma>(); }
 
 const Pi* clos_type_to_pi(const Def* ct, const Def* new_env_type) {
     assert(isa_clos_type(ct));

dialects/clos/clos.h

@@ -48,9 +48,7 @@ class ClosLit {
     ///@}
 
     operator bool() const { return def_ != nullptr; }
-
     operator const Tuple*() { return def_; }
-
     const Tuple* operator->() {
         assert(def_);
         return def_;
@@ -163,6 +161,11 @@ inline const Def* clos_remove_env(const Def* tup_or_sig) {
 inline const Def* clos_sub_env(const Def* tup_or_sig, const Def* new_env) {
     return tup_or_sig->refine(Clos_Env_Param, new_env);
 }
+
+size_t env_idx(const Def*);
+const Def* env_insert(const Def* def, const Def* env);
+
+
 ///@}
 
 } // namespace thorin::clos

dialects/clos/phase/clos_conv.h

@@ -19,7 +19,7 @@ class FreeDefAna {
     FreeDefAna(World& world)
         : world_(world)
         , cur_pass_id(1)
-        , lam2nodes_(){};
+        , lam2nodes_() {}
 
     /// FreeDefAna::run will compute free defs (FD) that appear in @p lam%s body.
     /// Nominal Def%s are only considered free if they are annotated with Clos::freeBB or

thorin/def.cpp

@@ -380,7 +380,7 @@ const Def* Def::proj(nat_t a, nat_t i, const Def* dbg) const {
 
     World& w = world();
 
-    if (isa<Tuple>() || isa<Sigma>()) {
+    if (isa<Tuple, Sigma>()) {
         return op(i);
     } else if (auto arr = isa<Arr>()) {
         if (arr->arity()->isa<Top>()) return arr->body();