Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

remove type ascr from tuple #240

Draft
wants to merge 12 commits into
base: master
Choose a base branch
from
47 changes: 24 additions & 23 deletions cli/main.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -45,31 +45,32 @@ int main(int argc, char** argv) {
// clang-format off
auto cli = lyra::cli()
| lyra::help(show_help)
| lyra::opt(show_version )["-v"]["--version" ]("Display version info and exit.")
| lyra::opt(list_search_paths )["-l"]["--list-search-paths" ]("List search paths in order and exit.")
| lyra::opt(clang, "clang" )["-c"]["--clang" ]("Path to clang executable (default: '" THORIN_WHICH " clang').")
| lyra::opt(plugins, "plugin" )["-p"]["--plugin" ]("Dynamically load plugin.")
| lyra::opt(search_paths, "path" )["-P"]["--plugin-path" ]("Path to search for plugins.")
| lyra::opt(inc_verbose )["-V"]["--verbose" ]("Verbose mode. Multiple -V options increase the verbosity. The maximum is 4.").cardinality(0, 4)
| lyra::opt(opt, "level" )["-O"]["--optimize" ]("Optimization level (default: 2).")
| lyra::opt(output[Dot ], "file" ) ["--output-dot" ]("Emits the Thorin program as a graph using Graphviz' DOT language.")
| lyra::opt(output[H ], "file" ) ["--output-h" ]("Emits a header file to be used to interface with a plugin in C++.")
| lyra::opt(output[LL ], "file" ) ["--output-ll" ]("Compiles the Thorin program to LLVM.")
| lyra::opt(output[Md ], "file" ) ["--output-md" ]("Emits the input formatted as Markdown.")
| lyra::opt(output[Thorin], "file" )["-o"]["--output-thorin" ]("Emits the Thorin program again.")
| lyra::opt(flags.bootstrap ) ["--bootstrap" ]("Puts thorin into \"bootstrap mode\". This means a '.plugin' directive has the same effect as an '.import' and will not load a library. In addition, no standard plugins will be loaded.")
| lyra::opt(flags.dump_gid, "level" ) ["--dump-gid" ]("Dumps gid of inline expressions as a comment in output if <level> > 0. Use a <level> of 2 to also emit the gid of trivial defs.")
| lyra::opt(flags.dump_recursive ) ["--dump-recursive" ]("Dumps Thorin program with a simple recursive algorithm that is not readable again from Thorin but is less fragile and also works for broken Thorin programs.")
| lyra::opt(flags.aggressive_lam_spec) ["--aggr-lam-spec" ]("Overrides LamSpec behavior to follow recursive calls.")
| lyra::opt(show_version )["-v"]["--version" ]("Display version info and exit.")
| lyra::opt(list_search_paths )["-l"]["--list-search-paths" ]("List search paths in order and exit.")
| lyra::opt(clang, "clang" )["-c"]["--clang" ]("Path to clang executable (default: '" THORIN_WHICH " clang').")
| lyra::opt(plugins, "plugin" )["-p"]["--plugin" ]("Dynamically load plugin.")
| lyra::opt(search_paths, "path" )["-P"]["--plugin-path" ]("Path to search for plugins.")
| lyra::opt(inc_verbose )["-V"]["--verbose" ]("Verbose mode. Multiple -V options increase the verbosity. The maximum is 4.").cardinality(0, 4)
| lyra::opt(opt, "level" )["-O"]["--optimize" ]("Optimization level (default: 2).")
| lyra::opt(output[Dot ], "file" ) ["--output-dot" ]("Emits the Thorin program as a graph using Graphviz' DOT language.")
| lyra::opt(output[H ], "file" ) ["--output-h" ]("Emits a header file to be used to interface with a plugin in C++.")
| lyra::opt(output[LL ], "file" ) ["--output-ll" ]("Compiles the Thorin program to LLVM.")
| lyra::opt(output[Md ], "file" ) ["--output-md" ]("Emits the input formatted as Markdown.")
| lyra::opt(output[Thorin], "file" )["-o"]["--output-thorin" ]("Emits the Thorin program again.")
| lyra::opt(flags.bootstrap ) ["--bootstrap" ]("Puts thorin into \"bootstrap mode\". This means a '.plugin' directive has the same effect as an '.import' and will not load a library. In addition, no standard plugins will be loaded.")
| lyra::opt(flags.dump_gid, "level" ) ["--dump-gid" ]("Dumps gid of inline expressions as a comment in output if <level> > 0. Use a <level> of 2 to also emit the gid of trivial defs.")
| lyra::opt(flags.dump_recursive ) ["--dump-recursive" ]("Dumps Thorin program with a simple recursive algorithm that is not readable again from Thorin but is less fragile and also works for broken Thorin programs.")
| lyra::opt(flags.aggressive_lam_spec ) ["--aggr-lam-spec" ]("Overrides LamSpec behavior to follow recursive calls.")
| lyra::opt(flags.scalerize_threshold, "threshold") ["--scalerize-threshold" ]("Thorin will not scalerize tuples/packs/sigmas/arrays with a number of elements greater than or equal this threshold.")
#ifdef THORIN_ENABLE_CHECKS
| lyra::opt(breakpoints, "gid" )["-b"]["--break" ]("*Triggers breakpoint upon construction of node with global id <gid>. Useful when running in a debugger.")
| lyra::opt(flags.reeval_breakpoints ) ["--reeval-breakpoints" ]("*Triggers breakpoint even upon unfying a node that has already been built.")
| lyra::opt(flags.break_on_alpha_unequal) ["--break-on-alpha-unequal"]("*Triggers breakpoint as soon as two expressions turn out to be not alpha-equivalent.")
| lyra::opt(flags.break_on_error ) ["--break-on-error" ]("*Triggers breakpoint on ELOG.")
| lyra::opt(flags.break_on_warn ) ["--break-on-warn" ]("*Triggers breakpoint on WLOG.")
| lyra::opt(flags.trace_gids ) ["--trace-gids" ]("*Output gids during World::unify/insert.")
| lyra::opt(breakpoints, "gid" )["-b"]["--break" ]("*Triggers breakpoint upon construction of node with global id <gid>. Useful when running in a debugger.")
| lyra::opt(flags.reeval_breakpoints ) ["--reeval-breakpoints" ]("*Triggers breakpoint even upon unfying a node that has already been built.")
| lyra::opt(flags.break_on_alpha_unequal ) ["--break-on-alpha-unequal"]("*Triggers breakpoint as soon as two expressions turn out to be not alpha-equivalent.")
| lyra::opt(flags.break_on_error ) ["--break-on-error" ]("*Triggers breakpoint on ELOG.")
| lyra::opt(flags.break_on_warn ) ["--break-on-warn" ]("*Triggers breakpoint on WLOG.")
| lyra::opt(flags.trace_gids ) ["--trace-gids" ]("*Output gids during World::unify/insert.")
#endif
| lyra::arg(input, "file" ) ("Input file.")
| lyra::arg(input, "file" ) ("Input file.")
;
// clang-format on

Expand Down
53 changes: 35 additions & 18 deletions dialects/affine/passes/lower_for.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,26 @@

namespace thorin::affine {

namespace {

const Def* merge_s(World& w, Ref elem, Ref sigma, Ref mem) {
if (mem) {
auto elems = sigma->projs();
return merge_sigma(elem, elems);
}
return w.sigma({elem, sigma});
}

const Def* merge_t(World& w, Ref elem, Ref tuple, Ref mem) {
if (mem) {
auto elems = tuple->projs();
return merge_tuple(elem, elems);
}
return w.tuple({elem, tuple});
}

} // namespace

Ref LowerFor::rewrite(Ref def) {
if (auto i = rewritten_.find(def); i != rewritten_.end()) return i->second;

Expand All @@ -19,28 +39,25 @@ Ref LowerFor::rewrite(Ref def) {
auto exit_lam = exit->isa_mut<Lam>();
if (!body_lam || !exit_lam) return def;

auto init_types = init->type()->projs();
auto head_lam = world().mut_lam(world().cn(merge_sigma(begin->type(), init_types)))->set("head");
auto phis = head_lam->vars();
auto iter = phis.front();
auto acc = world().tuple(phis.skip_front());
auto mem_phi = mem::mem_var(head_lam);
auto bb_type = world().cn(mem_phi ? mem_phi->type() : world().sigma());
auto new_body = world().mut_lam(bb_type)->set("new_body");
auto new_exit = world().mut_lam(bb_type)->set("new_exit");
auto new_yield = world().mut_lam(world().cn(init->type()))->set("new_yield");
auto cmp = world().call(core::icmp::ul, Defs{iter, end});
auto new_iter = world().call(core::wrap::add, core::Mode::nusw, Defs{iter, step});

head_lam->branch(false, cmp, new_body, new_exit, mem_phi);

auto new_yield_vars = new_yield->vars();
new_yield->app(false, head_lam, merge_tuple(new_iter, new_yield_vars));
auto mem = mem::mem_def(init);
auto head_lam = world().mut_lam(world().cn(merge_s(world(), begin->type(), init->type(), mem)))->set("head");
auto phis = head_lam->vars();
auto iter = phis.front();
auto acc = world().tuple(phis.skip_front());
mem = mem::mem_var(head_lam);
auto bb_type = world().cn(mem ? mem->type() : world().sigma());
auto new_body = world().mut_lam(bb_type)->set("new_body");
auto new_exit = world().mut_lam(bb_type)->set("new_exit");
auto new_yield = world().mut_lam(world().cn(init->type()))->set("new_yield");
auto cmp = world().call(core::icmp::ul, Defs{iter, end});
auto new_iter = world().call(core::wrap::add, core::Mode::nusw, Defs{iter, step});

head_lam->branch(false, cmp, new_body, new_exit, mem);
new_yield->app(false, head_lam, merge_t(world(), new_iter, new_yield->var(), mem));
new_body->set(false, body->reduce(world().tuple({iter, acc, new_yield})).back());
new_exit->set(false, exit->reduce(acc).back());

return rewritten_[def] = world().app(head_lam, merge_tuple(begin, init->projs()));
return rewritten_[def] = world().app(head_lam, merge_t(world(), begin, init, mem));
}

return def;
Expand Down
4 changes: 2 additions & 2 deletions dialects/clos/clos.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -84,11 +84,11 @@ Ref clos_pack(Ref env, Ref lam, Ref ct) {
auto pi = lam->type()->as<Pi>();
assert(env->type() == pi->dom(Clos_Env_Param));
ct = (ct) ? ct : clos_type(w.cn(clos_remove_env(pi->dom())));
return w.tuple(ct, {env->type(), lam, env})->isa<Tuple>();
return w.tuple({env->type(), lam, env})->isa<Tuple>();
}

std::tuple<Ref, Ref, Ref> clos_unpack(Ref c) {
assert(c && isa_clos_type(c->type()));
assert(c); // && isa_clos_type(c->type()));
// auto& w = c->world();
// auto env_type = c->proj(0_u64);
// // auto pi = clos_type_to_pi(c->type(), env_type);
Expand Down
4 changes: 2 additions & 2 deletions dialects/clos/clos.thorin
Original file line number Diff line number Diff line change
Expand Up @@ -47,14 +47,14 @@
%compile.pass_phase (%compile.pass_list
eta_red
eta_exp
(%compile.scalerize_pass (eta_exp, %compile.scalerize_threshold))
(%compile.scalerize_pass eta_exp)
)
};
.let clos_opt2_phase = {
.let nullptr = %compile.nullptr_pass;
%compile.pass_phase (%compile.pass_list
nullptr
(%compile.scalerize_pass (nullptr, %compile.scalerize_threshold))
(%compile.scalerize_pass nullptr)
%clos.branch_clos_pass
(%mem.copy_prop_pass (nullptr, nullptr, .tt))
%clos.lower_typed_clos_prep_pass
Expand Down
11 changes: 1 addition & 10 deletions dialects/compile/compile.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -77,16 +77,7 @@ extern "C" THORIN_EXPORT thorin::Plugin thorin_get_plugin() {
register_pass<compile::internal_cleanup_pass, compile::InternalCleanup>(passes);

register_pass_with_arg<compile::eta_exp_pass, EtaExp, EtaRed>(passes);

passes[flags_t(Annex::Base<compile::scalerize_pass>)]
= [&](World& world, PipelineBuilder& builder, const Def* app) {
auto [eta_exp, scalerize_threshold] = app->as<App>()->args<2>();
auto ee = (EtaExp*)builder.pass(eta_exp);
auto threshold = scalerize_threshold->as<Lit>()->get();
world.DLOG("registering Scalerize with ee = {}, scalerize_threshold = {}", ee, threshold);
builder.add_pass<Scalerize>(app, ee, threshold);
};

register_pass_with_arg<compile::scalerize_pass, Scalerize, EtaExp>(passes);
register_pass_with_arg<compile::tail_rec_elim_pass, TailRecElim, EtaRed>(passes);
},
nullptr};
Expand Down
9 changes: 4 additions & 5 deletions dialects/compile/compile.thorin
Original file line number Diff line number Diff line change
Expand Up @@ -103,9 +103,8 @@
.ax %compile.eta_red_pass: %compile.Pass;
/// Eta expansion expects an instance of eta reduction as argument.
.ax %compile.eta_exp_pass: %compile.Pass -> %compile.Pass;
/// Scalerize expects an instance of eta expansion as argument and a threshold where scalarize should stop.
.ax %compile.scalerize_pass: [%compile.Pass, .Nat] -> %compile.Pass;
.let %compile.scalerize_threshold = 32;
/// Scalerize expects an instance of eta expansion as argument.
.ax %compile.scalerize_pass: %compile.Pass -> %compile.Pass;
/// Tail recursion elimination expects an instance of eta reduction as argument.
.ax %compile.tail_rec_elim_pass: %compile.Pass -> %compile.Pass;
.ax %compile.lam_spec_pass: %compile.Pass;
Expand All @@ -124,7 +123,7 @@
%compile.beta_red_pass
eta_red
eta_exp
(%compile.scalerize_pass (eta_exp, %compile.scalerize_threshold))
(%compile.scalerize_pass eta_exp)
(%compile.tail_rec_elim_pass eta_red)
};
.let optimization_phase = {
Expand All @@ -137,7 +136,7 @@
.let nullptr = %compile.nullptr_pass;
%compile.pipe
(%compile.single_pass_phase nullptr)
(%compile.single_pass_phase (%compile.scalerize_pass (nullptr, %compile.scalerize_threshold)))
(%compile.single_pass_phase (%compile.scalerize_pass nullptr))
(%compile.single_pass_phase %compile.eta_red_pass)
(%compile.single_pass_phase (%compile.tail_rec_elim_pass nullptr))
optimization_phase
Expand Down
16 changes: 9 additions & 7 deletions dialects/core/be/ll.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -347,11 +347,12 @@ void Emitter::emit_epilogue(Lam* lam) {
// each callees type should agree with the argument type (should be checked by type checking).
// Especially, the number of vars should be the number of arguments.
// TODO: does not hold for complex arguments that are not tuples.
assert(callee->num_vars() == app->num_args());
for (size_t i = 0, e = callee->num_vars(); i != e; ++i) {
assert(callee->num_tvars() == app->num_targs());
size_t n = callee->num_tvars();
for (size_t i = 0; i != n; ++i) {
// emits the arguments one by one (TODO: handle together like before)
if (auto arg = emit_unsafe(app->arg(i)); !arg.empty()) {
auto phi = callee->var(i);
if (auto arg = emit_unsafe(app->arg(n, i)); !arg.empty()) {
auto phi = callee->var(n, i);
assert(!match<mem::M>(phi->type()));
lam2bb_[callee].phis[phi].emplace_back(arg, id(lam, true));
locals_[phi] = id(phi);
Expand All @@ -373,9 +374,10 @@ void Emitter::emit_epilogue(Lam* lam) {
} else if (app->callee()->isa<Bot>()) {
return bb.tail("ret ; bottom: unreachable");
} else if (auto callee = Lam::isa_mut_basicblock(app->callee())) { // ordinary jump
for (size_t i = 0, e = callee->num_vars(); i != e; ++i) {
if (auto arg = emit_unsafe(app->arg(i)); !arg.empty()) {
auto phi = callee->var(i);
size_t n = callee->num_tvars();
for (size_t i = 0; i != n; ++i) {
if (auto arg = emit_unsafe(app->arg(n, i)); !arg.empty()) {
auto phi = callee->var(n, i);
assert(!match<mem::M>(phi->type()));
lam2bb_[callee].phis[phi].emplace_back(arg, id(lam, true));
locals_[phi] = id(phi);
Expand Down
3 changes: 2 additions & 1 deletion dialects/mem/mem.h
Original file line number Diff line number Diff line change
Expand Up @@ -33,13 +33,14 @@ inline const Pi* fn_mem(Ref domain, Ref codomain) {
/// Returns the (first) element of type mem::M from the given tuple.
inline Ref mem_def(Ref def) {
if (match<mem::M>(def->type())) return def;
if (def->type()->isa<Arr>()) return {}; // don't look into possibly gigantic arrays

if (def->num_projs() > 1) {
for (auto proj : def->projs())
if (auto mem = mem_def(proj)) return mem;
}

return nullptr;
return {};
}

/// Returns the memory argument of a function if it has one.
Expand Down
3 changes: 1 addition & 2 deletions dialects/mem/normalizers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,7 @@ Ref normalize_load(Ref type, Ref callee, Ref arg) {
if (ptr->isa<Bot>()) return world.tuple({mem, world.bot(type->as<Sigma>()->op(1))});

// loading an empty tuple can only result in an empty tuple
if (auto sigma = pointee->isa<Sigma>(); sigma && sigma->num_ops() == 0)
return world.tuple({mem, world.tuple(sigma->type(), {})});
if (auto sigma = pointee->isa<Sigma>(); sigma && sigma->num_ops() == 0) return world.tuple({mem, world.tuple()});

return world.raw_app(type, callee, {mem, ptr});
}
Expand Down
16 changes: 8 additions & 8 deletions dialects/mem/passes/fp/copy_prop.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Ref CopyProp::rewrite(Ref def) {
auto [app, var_lam] = isa_apped_mut_lam(def);
if (!isa_workable(var_lam) || (bb_only_ && Lam::isa_returning(var_lam))) return def;

auto n = app->num_args();
auto n = app->num_targs();
if (n == 0) return app;

auto [it, _] = lam2info_.emplace(var_lam, std::tuple(Lattices(n), (Lam*)nullptr, DefArray(n)));
Expand All @@ -28,20 +28,20 @@ Ref CopyProp::rewrite(Ref def) {
switch (lattice[i]) {
case Lattice::Dead: break;
case Lattice::Prop:
if (app->arg(i)->has_dep(Dep::Proxy)) {
if (app->arg(n, i)->has_dep(Dep::Proxy)) {
world().DLOG("found proxy within app: {}@{} - wait till proxy is gone", var_lam, app);
return app;
} else if (args[i] == nullptr) {
args[i] = app->arg(i);
} else if (args[i] != app->arg(i)) {
args[i] = app->arg(n, i);
} else if (args[i] != app->arg(n, i)) {
appxy_ops.emplace_back(world().lit_nat(i));
} else {
assert(args[i] == app->arg(i));
assert(args[i] == app->arg(n, i));
}
break;
case Lattice::Keep:
new_doms.emplace_back(var_lam->var(i)->type());
new_args.emplace_back(app->arg(i));
new_doms.emplace_back(var_lam->var(n, i)->type());
new_args.emplace_back(app->arg(n, i));
break;
default: unreachable();
}
Expand Down Expand Up @@ -71,7 +71,7 @@ Ref CopyProp::rewrite(Ref def) {
size_t j = 0;
DefArray new_vars(n, [&, prop_lam = prop_lam](size_t i) -> Ref {
switch (lattice[i]) {
case Lattice::Dead: return proxy(var_lam->var(i)->type(), {var_lam, world().lit_nat(i)}, Varxy);
case Lattice::Dead: return proxy(var_lam->var(n, i)->type(), {var_lam, world().lit_nat(i)}, Varxy);
case Lattice::Prop: return args[i];
case Lattice::Keep: return prop_lam->var(j++);
default: unreachable();
Expand Down
2 changes: 1 addition & 1 deletion dialects/mem/passes/fp/ssa_constr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ Ref SSAConstr::mem2phi(const App* app, Lam* mem_lam) {
auto traxy = proxy(phi_lam->var()->type(), traxy_ops, Traxy);

DefArray new_vars(num_mem_vars, [&](size_t i) { return traxy->proj(i); });
phi_lam->set(mem_lam->reduce(world().tuple(mem_lam->dom(), new_vars)));
phi_lam->set(mem_lam->reduce(world().tuple(new_vars)));
} else {
world().DLOG("reuse phi_lam '{}'", phi_lam);
}
Expand Down
Loading