Merge branch 'master' into autodiff

AnyDSL · Oct 21, 2022 · 639b8fd · 639b8fd
2 parents b1772d4 + 2a38a50
commit 639b8fd
Show file tree

Hide file tree

Showing 53 changed files with 135 additions and 131 deletions.
diff --git a/dialects/autodiff/autodiff.h b/dialects/autodiff/autodiff.h
@@ -10,7 +10,7 @@ inline const Def* op_autodiff(const Def* fun) {
     World& world = fun->world();
     // We rely on the normalized thorin convention that all arguments in functions are grouped.
     // `cn[[args], cont:=cn[returns]]`
-    return world.app(world.app(world.ax<autodiff>(), fun->type()), fun);
+    return world.app(world.app(world.ax<ad>(), fun->type()), fun);
 }
 
 inline const Def* op_zero(const Def* A) {

diff --git a/dialects/autodiff/autodiff.thorin b/dialects/autodiff/autodiff.thorin
@@ -11,23 +11,20 @@
 ///
 /// ## Types
 ///
-.ax %autodiff.tangent_type: * -> *, normalize_tangent_type;
+.ax %autodiff.Tangent: * -> *, normalize_Tangent;
 ///
 /// ## Operations
 ///
-/// ### %autodiff.autodiff
+/// ### %autodiff.ad
 /// 
 /// This axiom operates on functions and types.
 ///
 /// For function types the augmented type is computed: `(T -> U) => (T -> U × (U -> T))`
-.ax %autodiff.autodiff_type: * -> *, 
-    normalize_autodiff_type;
+.ax %autodiff.AD: * -> *, normalize_AD;
 /// On closed terms (functions, operators, ho arguments, registered axioms, etc.) the augmented term is returned.
 /// The augmented term `f'` returns the result together with the pullback.
 /// `autodiff f = f' = λ args. (f args, f*)` 
-.ax %autodiff.autodiff: Π [T: *] -> T -> 
-    %autodiff.autodiff_type T, 
-    normalize_autodiff;
+.ax %autodiff.ad: Π [T: *] -> T -> %autodiff.AD T, normalize_ad;
 ///
 /// ### %autodiff.zero
 /// 

diff --git a/dialects/autodiff/normalizers.cpp b/dialects/autodiff/normalizers.cpp
@@ -11,19 +11,19 @@ namespace thorin::autodiff {
 
 /// Currently this normalizer does nothin.
 /// TODO: Maybe we want to handle trivial lookup replacements here.
-const Def* normalize_autodiff(const Def* type, const Def* callee, const Def* arg, const Def* dbg) {
+const Def* normalize_ad(const Def* type, const Def* callee, const Def* arg, const Def* dbg) {
     auto& world = type->world();
     return world.raw_app(callee, arg, dbg);
 }
 
-const Def* normalize_autodiff_type(const Def* type, const Def* callee, const Def* arg, const Def* dbg) {
+const Def* normalize_AD(const Def* type, const Def* callee, const Def* arg, const Def* dbg) {
     auto& world = type->world();
     auto ad_ty  = autodiff_type_fun(arg);
     if (ad_ty) return ad_ty;
     return world.raw_app(callee, arg, dbg);
 }
 
-const Def* normalize_tangent_type(const Def*, const Def*, const Def* arg, const Def*) { return tangent_type_fun(arg); }
+const Def* normalize_Tangent(const Def*, const Def*, const Def* arg, const Def*) { return tangent_type_fun(arg); }
 
 /// Currently this normalizer does nothing.
 /// We usually want to keep zeros as long as possible to avoid unnecessary allocations.

diff --git a/dialects/autodiff/passes/autodiff_eval.cpp b/dialects/autodiff/passes/autodiff_eval.cpp
@@ -28,7 +28,7 @@ const Def* AutoDiffEval::derive(const Def* def) {
 }
 
 const Def* AutoDiffEval::rewrite(const Def* def) {
-    if (auto ad_app = match<autodiff>(def); ad_app) {
+    if (auto ad_app = match<ad>(def); ad_app) {
         // callee = autodiff T
         // arg = function of type T
         //   (or operator)

diff --git a/dialects/core/be/ll/ll.cpp b/dialects/core/be/ll/ll.cpp
@@ -497,13 +497,18 @@ std::string Emitter::emit_bb(BB& bb, const Def* def) {
         unreachable();
     } else if (def->isa<Bot>()) {
         return "undef";
-    } else if (auto bit = match<core::bit2>(def)) {
-        auto [a, b] = bit->args<2>([this](auto def) { return emit(def); });
-        auto t      = convert(bit->type());
-
-        auto neg = [&](std::string_view x) { return bb.assign(name + ".neg", "xor {} 0, {}", t, x); };
-
-        switch (bit.id()) {
+    } else if (auto bit1 = match<core::bit1>(def)) {
+        assert(bit1.id() == core::bit1::neg);
+        auto x = emit(bit1->arg());
+        auto t = convert(bit1->type());
+        return bb.assign(name, "xor {} -1, {}", t, x);
+    } else if (auto bit2 = match<core::bit2>(def)) {
+        auto [a, b] = bit2->args<2>([this](auto def) { return emit(def); });
+        auto t      = convert(bit2->type());
+
+        auto neg = [&](std::string_view x) { return bb.assign(name + ".neg", "xor {} -1, {}", t, x); };
+
+        switch (bit2.id()) {
             // clang-format off
             case core::bit2::_and: return bb.assign(name, "and {} {}, {}", t, a, b);
             case core::bit2:: _or: return bb.assign(name, "or  {} {}, {}", t, a, b);

diff --git a/dialects/core/normalizers.cpp b/dialects/core/normalizers.cpp
@@ -350,7 +350,7 @@ const Def* normalize_nop(const Def* type, const Def* callee, const Def* arg, con
         }
     }
 
-    return world.raw_app(callee, a, dbg);
+    return world.raw_app(callee, arg, dbg);
 }
 
 template<ncmp id>
@@ -379,7 +379,7 @@ const Def* normalize_ncmp(const Def* type, const Def* callee, const Def* arg, co
         }
     }
 
-    return world.raw_app(callee, a, dbg);
+    return world.raw_app(callee, arg, dbg);
 }
 
 template<rop id>

diff --git a/docs/langref.md b/docs/langref.md
@@ -138,9 +138,8 @@ The following tables comprise all production rules:
 | d           | `.pack` Sym ( `:` e<sub>type</sub> )? `,` e<sub>shape</sub> v? n  |            | nominal pack declaration         | thorin::Pack  |
 | d           | `.Sigma` Sym ( `:` e<sub>type</sub> )? `,` L<sub>arity</sub> v? n |            | nominal sigma declaration        | thorin::Sigma |
 | d           | `.def` Sym n                                                      |            | nominal definition               | nominals      |
-| v           | `,` `@` Sym \| `,` `@` `(` Sym `,` ... `,` Sym `)`                |            | nominal variable declaration     | nominals      |
 | n           | `;` \| o                                                          |            | nominal definition               | -             |
-| o           | `=` e `;`                                                         |            | operand of nominal definition    | -             |
+| o           | `=` de `;`                                                        |            | operand of nominal definition    | -             |
 | o           | `=` `{` e `,` ... `,` e  `}` `;`                                  | ✓          | operands of nominal definition   | -             |
 
 ### Patterns
@@ -162,18 +161,19 @@ For this reason there is no rule `b -> s (p, ..., p)`.
 
 | Nonterminal | Right-Hand Side                                                               | New Scope? | Comment                              | Thorin Class    |
 |-------------|-------------------------------------------------------------------------------|------------|--------------------------------------|-----------------|
+| de          | d\* e                                                                         |            | declaration expression               | -               |
 | e           | `.Univ`                                                                       |            | universise: type of a type level     | thorin::Univ    |
 | e           | `.Type` e                                                                     |            | type of level e                      | thorin::Type    |
 | e           | `*`                                                                           |            | alias for `.Type (0:.Univ)`          | thorin::Type    |
 | e           | `□`                                                                           |            | alias for `.Type (1:.Univ)`          | thorin::Type    |
 | e           | `.Nat`                                                                        |            | natural number                       | thorin::Nat     |
 | e           | `.Idx`                                                                        |            | builtin constant of type `.Nat -> *` | thorin::Idx     |
 | e           | `.Bool`                                                                       |            | alias for `.Idx 2`                   | thorin::Idx     |
-| e           | `{` e `}`                                                                     | ✓          | block                                | -               |
+| e           | `{` de `}`                                                                    | ✓          | block                                | -               |
 | e           | L `:` e<sub>type</sub>                                                        |            | literal                              | thorin::Lit     |
 | e           | `.ff`                                                                         |            | alias for `0_2`                      | thorin::Lit     |
 | e           | `.tt`                                                                         |            | alias for `1_2`                      | thorin::Lit     |
-| e           | ( `.bot` or `.top` ) ( `:` e<sub>type</sub> )?                                |            | bottom/top                           | thorin::TExt    |
+| e           | ( `.bot` \| `.top` ) ( `:` e<sub>type</sub> )?                                |            | bottom/top                           | thorin::TExt    |
 | e           | Sym                                                                           |            | identifier                           | -               |
 | e           | Ax                                                                            |            | use of an axiom                      | -               |
 | e           | e e                                                                           |            | application                          | thorin::App     |
@@ -187,7 +187,6 @@ For this reason there is no rule `b -> s (p, ..., p)`.
 | e           | `[` b `,` ... `,` b `]`                                                       | ✓          | sigma                                | thorin::Sigma   |
 | e           | `‹` i e<sub>shape</sub> `;` e<sub>body</sub>`›`                               | ✓          | pack                                 | thorin::Pack    |
 | e           | `«` i e<sub>shape</sub> `;` e<sub>body</sub>`»`                               | ✓          | array                                | thorin::Arr     |
-| e           | d e                                                                           |            | declaration                          | -               |
 
 An elided type of
 * a literal defaults to `.Nat`,

diff --git a/lit/autodiff/2out.thorin.disabled b/lit/autodiff/2out.thorin.disabled
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -24,7 +24,7 @@
         pb((1:I32,0:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [I32,.Cn[I32,I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [I32,.Cn[I32,I32]]) f;
     .let c = (42:I32);
     f_diff (c,ret_cont)
 };
diff --git a/lit/autodiff/autodiff_mult_in_call.thorin b/lit/autodiff/autodiff_mult_in_call.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -32,7 +32,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [[I32,I32],.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [[I32,I32],.Cn[I32]]) f;
 
     .let c = (42:I32,43:I32);
     f_diff (c,ret_cont)

diff --git a/lit/autodiff/autodiff_mult_in_call2.thorin b/lit/autodiff/autodiff_mult_in_call2.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -29,7 +29,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [[I32,I32],.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [[I32,I32],.Cn[I32]]) f;
 
     .let c = (42:I32,43:I32);
     f_diff (c,ret_cont)

diff --git a/lit/autodiff/autodiff_mult_in_call2_2.thorin b/lit/autodiff/autodiff_mult_in_call2_2.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -29,7 +29,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [[I32,I32],.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [[I32,I32],.Cn[I32]]) f;
 
     .let c = (42:I32,43:I32);
     f_diff (c,ret_cont)

diff --git a/lit/autodiff/autodiff_mult_in_call2_3.thorin b/lit/autodiff/autodiff_mult_in_call2_3.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -29,7 +29,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [[I32,I32],.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [[I32,I32],.Cn[I32]]) f;
 
     .let c = (42:I32,43:I32);
     f_diff (c,ret_cont)

diff --git a/lit/autodiff/autodiff_mult_in_call_cont.thorin b/lit/autodiff/autodiff_mult_in_call_cont.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -28,7 +28,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [[I32,I32],.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [[I32,I32],.Cn[I32]]) f;
 
     .let c = (42:I32,43:I32);
     f_diff (c,ret_cont)

diff --git a/lit/autodiff/call_autodiff.thorin b/lit/autodiff/call_autodiff.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -30,7 +30,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [I32,.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [I32,.Cn[I32]]) f;
     .let f_diff_cast = f_diff;
 
     .let c = (42:I32);

diff --git a/lit/autodiff/call_autodiff_cont.thorin b/lit/autodiff/call_autodiff_cont.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff  %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff  %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -34,7 +34,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [I32,.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [I32,.Cn[I32]]) f;
 
     .let c = (42:I32);
     f_diff (c,ret_cont)

diff --git a/lit/autodiff/general/2out.thorin b/lit/autodiff/general/2out.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;

diff --git a/lit/autodiff/general/42.thorin b/lit/autodiff/general/42.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;

diff --git a/lit/autodiff/general/add_tuple.thorin b/lit/autodiff/general/add_tuple.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import direct;

diff --git a/lit/autodiff/general/cps_inline.thorin b/lit/autodiff/general/cps_inline.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin %s --output-ll %t.ll -o - | FileCheck %s
 
 .import mem;
 .import core;

diff --git a/lit/autodiff/general/ds_inline.thorin b/lit/autodiff/general/ds_inline.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import mem;

diff --git a/lit/autodiff/general/invoke_ds.thorin b/lit/autodiff/general/invoke_ds.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import direct;

diff --git a/lit/autodiff/general/simple_real.thorin.disabled b/lit/autodiff/general/simple_real.thorin.disabled
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import autodiff;
 .import mem;

diff --git a/lit/autodiff/general/tangent_type_cast.thorin b/lit/autodiff/general/tangent_type_cast.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import mem;
@@ -14,13 +14,13 @@
 
 .cn .extern main [mem : %mem.M, argc : I32, argv : %mem.Ptr (%mem.Ptr (.Idx 256, 0:.Nat), 0:.Nat), return : .Cn [%mem.M, I32]] = {
 
-    .cn ret_cont r::[%autodiff.tangent_type I32] = {
-        .let r2=%core.bitcast (I32,(%autodiff.tangent_type I32)) r;
+    .cn ret_cont r::[%autodiff.Tangent I32] = {
+        .let r2=%core.bitcast (I32,(%autodiff.Tangent I32)) r;
         return (mem, r2)
     };
 
     .cn ret_wrap r::[I32] = {
-        .let r2=%core.bitcast ((%autodiff.tangent_type I32),I32) r;
+        .let r2=%core.bitcast ((%autodiff.Tangent I32),I32) r;
         ret_cont r2
     };
 

diff --git a/lit/autodiff/general/zero_tuple.thorin b/lit/autodiff/general/zero_tuple.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import direct;

diff --git a/lit/autodiff/id_autodiff.thorin b/lit/autodiff/id_autodiff.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -23,7 +23,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [I32,.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [I32,.Cn[I32]]) f;
     .let f_diff_cast = f_diff;
 
     .let c = (43:I32);

diff --git a/lit/autodiff/id_autodiff_info_out.thorin b/lit/autodiff/id_autodiff_info_out.thorin
@@ -1,5 +1,5 @@
 // RUN: rm -f %t.ll ; \
-// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll --output-thorin - | FileCheck %s
+// RUN: %thorin -d direct -d autodiff %s --output-ll %t.ll -o - | FileCheck %s
 
 .import core;
 .import autodiff;
@@ -23,7 +23,7 @@
         pb((1:I32),pb_ret_cont)
     };
 
-    .let f_diff = %autodiff.autodiff (.Cn [I32,.Cn[I32]]) f;
+    .let f_diff = %autodiff.ad (.Cn [I32,.Cn[I32]]) f;
     .let f_diff_cast = f_diff;
 
     .let c = (43:I32);