9using namespace std::literals;
15 if (
auto i = augmented.find(def); i != augmented.end())
return i->second;
16 augmented[def] =
augment_(def, f, f_diff);
17 return augmented[def];
21 if (
auto i = derived.find(def); i != derived.end())
return i->second;
34 auto arg =
rewrite(ad_app->arg());
40 assert(0 &&
"not implemented");
44 return RWPhase::rewrite_imm_App(app);
55 auto deriv = world().mut_lam(deriv_ty)->set(lam->sym().str() +
"_deriv");
63 auto [arg_ty, ret_pi] = lam->type()->doms<2>();
64 auto deriv_all_args = deriv->var();
65 const Def* deriv_arg = deriv->
var(0uz)->
set(
"arg");
73 partial_pullback[deriv_arg] = arg_id_pb;
75 auto ret_var = deriv->var(1);
77 partial_pullback[ret_var] = ret_pb;
79 shadow_pullback[deriv_all_args] = world().tuple({arg_id_pb, ret_pb});
84 augmented[def] = deriv;
85 augmented[lam->var()] = deriv->var();
98 auto new_body =
augment(lam->body(), lam, deriv);
99 deriv->set(
true, new_body);
110 partial_pullback[lit] = pb;
115 assert(augmented.count(var));
116 auto aug_var = augmented[var];
117 assert(partial_pullback.count(aug_var));
125 if (augmented.count(lam)) {
130 return augmented[lam];
143 auto cont_dom = lam->
type()->
dom();
146 auto aug_lam = world().mut_con({aug_dom, pb_ty})->set(
"aug_"s + lam->
sym().str());
147 auto aug_var = aug_lam->var((
nat_t)0);
148 augmented[lam->
var()] = aug_var;
149 augmented[lam] = aug_lam;
150 derived[lam] = aug_lam;
151 auto pb = aug_lam->var(1);
152 partial_pullback[aug_var] = pb;
156 aug_lam->set(lam->
filter(), new_body);
159 partial_pullback[aug_lam] = lam_pb;
166 auto aug_lam =
derive(lam);
173 auto index = ext->
index();
176 auto aug_index =
augment(index, f, f_diff);
179 if (shadow_pullback.count(aug_tuple)) {
180 auto shadow_tuple_pb = shadow_pullback[aug_tuple];
181 pb = world().extract(shadow_tuple_pb, aug_index);
188 assert(partial_pullback.count(aug_tuple));
189 auto tuple_pb = partial_pullback[aug_tuple];
191 auto pb_fun = world().mut_lam(pb_ty)->set(
"extract_pb");
192 auto pb_tangent = pb_fun->var(0uz)->set(
"s");
193 auto tuple_tan = world().insert(world().call<zero>(aug_tuple->type()), aug_index, pb_tangent)->set(
"tup_s");
194 pb_fun->app(
true, tuple_pb, {tuple_tan, pb_fun->var(1) });
198 auto aug_ext = world().extract(aug_tuple, aug_index);
199 partial_pullback[aug_ext] = pb;
206 auto aug_ops = tup->
projs([&](
const Def* op) ->
const Def* {
return augment(op, f, f_diff); });
207 auto aug_tup = world().tuple(aug_ops);
209 auto pbs =
DefVec(
Defs(aug_ops), [&](
const Def* op) {
return partial_pullback[op]; });
211 auto shadow_pb = world().tuple(pbs);
212 shadow_pullback[aug_tup] = shadow_pb;
220 auto pb = world().mut_lam(pb_ty)->set(
"tup_pb");
222 auto pb_tangent = pb->var(0uz)->set(
"tup_s");
225 pbs.size(), [&](
nat_t i) { return world().app(cps::op_cps2ds_dep(pbs[i]), world().extract(pb_tangent, i)); });
226 pb->app(
true, pb->var(1),
229 partial_pullback[aug_tup] = pb;
235 auto arity = pack->
arity();
236 auto body = pack->
body();
238 auto aug_arity =
augment_(arity, f, f_diff);
239 auto aug_body =
augment(body, f, f_diff);
241 auto aug_pack = world().pack(aug_arity, aug_body);
243 assert(partial_pullback[aug_body] &&
"pack pullback should exists");
245 auto body_pb = partial_pullback[aug_body];
246 auto pb_pack = world().pack(aug_arity, body_pb);
247 shadow_pullback[aug_pack] = pb_pack;
250 auto pb = world().mut_lam(pb_type)->set(
"pack_pb");
253 auto app_pb = world().mut_pack(world().arr(aug_arity, f_arg_ty_diff));
260 auto sumup = world().app(world().
annex<sum>(), {aug_arity, f_arg_ty_diff});
262 pb->app(
true, pb->var(1), world().app(sumup, app_pb));
264 partial_pullback[aug_pack] = pb;
270 auto callee = app->
callee();
271 auto arg = app->
arg();
273 auto aug_arg =
augment(arg, f, f_diff);
274 auto aug_callee =
augment(callee, f, f_diff);
280 if (app->
type()->isa<
Pi>()) {
281 auto aug_app = world().app(aug_callee, aug_arg);
295 auto arg_pb = partial_pullback[aug_arg];
296 auto aug_app = world().app(aug_callee, {aug_arg, arg_pb});
302 auto aug_app = world().app(aug_callee, aug_arg);
305 auto [aug_res, fun_pb] = aug_app->projs<2>();
308 auto arg_pb = partial_pullback[aug_arg];
313 partial_pullback[aug_res] = res_pb;
327 auto g_deriv = aug_callee;
329 auto [real_aug_args, aug_cont] = aug_arg->projs<2>();
330 auto e_pb = partial_pullback[real_aug_args];
333 auto ret_g_deriv_ty = g_deriv->type()->as<
Pi>()->dom(1);
334 auto c1_ty = ret_g_deriv_ty->as<
Pi>();
335 auto c1 = world().mut_lam(c1_ty)->
set(
"c1");
337 auto r_pb = c1->
var(1);
338 c1->app(
true, aug_cont, {res,
compose_cn(e_pb, r_pb)});
340 auto aug_app = world().app(aug_callee, {real_aug_args, c1});
345 assert(
false &&
"should not be reached");
351 if (
auto app = def->isa<
App>()) {
353 }
else if (
auto ext = def->isa<
Extract>()) {
355 }
else if (
auto var = def->isa<
Var>()) {
359 }
else if (
auto lam = def->isa<
Lam>()) {
360 log().e(
"cannot augment an immutable Lam: {}", lam);
361 assert(
false &&
"can not handle non-mutable lambdas");
362 }
else if (
auto lit = def->isa<
Lit>()) {
364 }
else if (
auto tup = def->isa<
Tuple>()) {
366 }
else if (
auto pack = def->isa<
Pack>()) {
369 }
else if (
auto ax = def->isa<
Axm>()) {
370 auto diff_name = ax->sym().str();
371 fe::find_and_replace(diff_name,
".",
"_");
372 diff_name =
"autodiff.diff." + diff_name;
378 log().e(
"no derivative `{}`; expected type: {}", diff_name, expected_type);
379 assert(
false &&
"unhandled axm");
388 log().e(
"cannot augment {} node {}: {}", def->
node_name(), def, def->
type());
389 assert(
false &&
"augment not implemented on this def");
const Def * callee() const
static auto isa(const Def *def)
Def * set(size_t i, const Def *)
Successively set from left to right.
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
std::string_view node_name() const
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
const Def * var(nat_t a, nat_t i) noexcept
auto projs(F f) const
Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (other...
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
const Def * arity() const
Number of elements available to Extract / Insert (may be dynamic).
const Def * filter() const
static const Lam * isa_basicblock(const Def *d)
A (possibly paramterized) Tuple.
const fe::Log & log() const
A dependent function type.
static const Pi * isa_cn(const Def *d)
static const Pi * isa_basicblock(const Def *d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
Pi * set(const Def *dom, const Def *codom)
bool is_bootstrapping() const
Returns whether we are currently bootstrapping (rewriting annexes).
World & old_world()
Get old Defs from here.
virtual const Def * rewrite(const Def *)
Data constructor for a Sigma.
A variable introduced by a binder (mutable).
const Def * annex(Sym sym)
Lookup annex by Sym.
const Def * augment_app(const App *, Lam *, Lam *)
const Def * augment_extract(const Extract *, Lam *, Lam *)
const Def * augment_lit(const Lit *, Lam *, Lam *)
const Def * rewrite_imm_App(const App *) final
Detect autodiff calls.
const Def * derive(const Def *)
Acts on toplevel autodiff on closed terms:
const Def * augment_lam(Lam *, Lam *, Lam *)
const Def * augment_tuple(const Tuple *, Lam *, Lam *)
const Def * augment_var(const Var *, Lam *, Lam *)
helper functions for augment
const Def * augment(const Def *, Lam *, Lam *)
Applies to (open) expressions in a functional context.
const Def * augment_pack(const Pack *pack, Lam *f, Lam *f_diff)
const Def * derive_(const Def *)
Additionally to the derivation, the pullback is registered and the maps are initialized.
const Def * augment_(const Def *, Lam *, Lam *)
Rewrites the given definition in a lambda environment.
const Pi * autodiff_type_fun_pi(const Pi *)
const Def * op_sum(const Def *T, Defs)
const Def * autodiff_type_fun(const Def *)
const Def * tangent_type_fun(const Def *)
const Def * zero_pullback(const Def *E, const Def *A)
const Def * id_pullback(const Def *)
const Pi * pullback_type(const Def *E, const Def *A)
computes pb type E* -> A* E - type of the expression (return type for a function) A - type of the arg...
const Def * op_cps2ds_dep(const Def *k)
fe::View< const Def * > Defs
fe::Vector< const Def * > DefVec
const Def * compose_cn(const Def *f, const Def *g)
The high level view is: