12using namespace std::literals;
34 auto& world = A->
world();
36 auto id_pb = world.mut_lam(arg_pb_ty)->set(
"id_pb");
37 auto id_pb_scalar = id_pb->var(2, 0)->set(
"s");
38 id_pb->app(
true, id_pb->var(2, 1),
45 auto& world = A->
world();
48 auto pb = world.mut_lam(pb_ty)->set(
"zero_pb");
49 pb->app(
true, pb->var(2, 1), world.call<
zero>(A_tangent));
62 auto& world = E->
world();
65 auto pb_ty = world.cn({tang_ret, world.cn(tang_arg)});
72 auto& world = arg->
world();
75 if (!aug_arg || !aug_ret)
return nullptr;
80 auto deriv_ty = world.cn({aug_arg, world.cn({aug_ret, pb_ty})});
86 auto& world = pi->
world();
90 auto ret = pi->
codom();
93 if (!aug_arg)
return nullptr;
95 if (!aug_ret)
return nullptr;
96 return world.pi(aug_arg, aug_ret);
100 auto [arg, ret_pi] = pi->
doms<2>();
101 auto ret = ret_pi->as<
Pi>()->dom();
108 auto& world = ty->
world();
113 if (ty == world.type_nat())
return ty;
114 if (
auto arr = ty->isa<
Arr>()) {
115 auto shape = arr->shape();
116 auto body = arr->body();
118 if (!body_ad)
return nullptr;
119 return world.arr(shape, body_ad);
121 if (
auto sig = ty->isa<
Sigma>()) {
123 auto ops =
DefVec(sig->ops(), [&](
const Def* op) { return autodiff_type_fun(op); });
124 if (std::ranges::contains(ops,
nullptr))
return nullptr;
125 return world.sigma(ops);
129 world.log().w(
"not differentiable: {}", ty);
136 auto& world = T->
world();
137 if (
auto arr = T->isa<
Arr>()) {
138 auto shape = arr->shape();
139 auto body = arr->body();
140 auto inner_zero = world.app(world.annex<
zero>(), body);
141 auto zero_arr = world.pack(shape, inner_zero);
145 auto zero = world.lit(T, 0)->set(
"zero");
147 }
else if (
auto sig = T->isa<
Sigma>()) {
148 auto ops =
DefVec(sig->ops(), [&](
const Def* op) { return world.app(world.annex<zero>(), op); });
149 return world.tuple(ops);
156 auto& world = T->
world();
157 return world.
app(world.app(world.annex<
sum>(), {world.lit_nat(defs.size()), T}), defs);
static void reg_phases(Flags2Phases &phases)
A (possibly paramterized) Array.
static auto isa(const Def *def)
World & world() const noexcept
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
static void hook(Flags2Phases &phases)
A dependent function type.
auto doms(Projector auto f) const noexcept
static const Pi * isa_cn(const Def *d)
const Def * codom() const
const Def * app(const Def *callee, const Def *arg)
The automatic differentiation Plugin
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 * zero_def(const Def *T)
const Def * tangent_type_fun(const Def *)
const Def * zero_pullback(const Def *E, const Def *A)
const Def * id_pullback(const Def *)
void register_normalizers(Normalizers &normalizers)
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...
fe::View< const Def * > Defs
fe::Vector< const Def * > DefVec
ankerl::unordered_dense::map< flags_t, std::function< std::unique_ptr< Phase >(World &)> > Flags2Phases
Maps an axiom of a Phase to a function that creates one.
#define MIM_REPL(__phases, __annex,...)
#define MIM_PLUGIN_ENTRY(p)
Defines a Plugin's entry point; the body fills in the plugin handed to it, as in MIM_PLUGIN_ENTRY(dem...