Refactor/pi syntax

.github/workflows/linux.yml

@@ -51,7 +51,7 @@ jobs:
           sudo ln -s ${{github.workspace}}/bin/FileCheck-x86_64-ubuntu /usr/bin/FileCheck
           sudo chmod +x /usr/bin/FileCheck
           # sudo python -m pip install --upgrade pip
-          sudo pip install lit psutil --break-system-packages
+          sudo pip install lit psutil # --break-system-packages
 
       - name: Setup ccache
         uses: Chocobo1/setup-ccache-action@v1

docs/langref.md

@@ -38,7 +38,7 @@ Both tokens are identified as `⊥`.
 | ------------------------------- | ------------------------------------------- | ------------------------- |
 | `(` `)` `[` `]` `{` `}`         |                                             | delimiters                |
 | `‹` `›` `«` `»`                 | `<<` `>>` `<` `>`                           | UTF-8 delimiters          |
-| `→` `⊥` `⊤` `★` `□` `λ` `Π`     | `->` `.bot` `.top` `*` `.lm` <tt>\|~\|</tt> | further UTF-8 tokens      |
+| `→` `⊥` `⊤` `★` `□` `λ`         | `->` `.bot` `.top` `*` `.lm`                | further UTF-8 tokens      |
 | `=` `,` `;` `.` `#` `:` `%` `@` |                                             | further tokens            |
 | `<eof>`                         |                                             | marks the end of the file |
 
@@ -62,7 +62,6 @@ In addition the following keywords are _terminals_:
 | `.cn`     | [continuation](@ref mim::Lam) expression                  |
 | `.fn`     | [function](@ref mim::Lam) expression                      |
 | `.lm`     | [lambda](@ref mim::Lam) expression                        |
-| `.Pi`     | [Pi](@ref mim::Pi) declaration                            |
 | `.Sigma`  | [Sigma](@ref mim::Sigma) declaration                      |
 | `.extern` | marks function as external                                |
 | `.ins`    | mim::Insert expression                                    |
@@ -177,7 +176,6 @@ The following tables comprise all production rules:
 | d   | `.lam` n (`.`? p)+ (`:` e<sub>codom</sub>)? ( `=` d\* e)? `;`                                                                                     | lambda declaration<sup>s</sup>       | [Lam](@ref mim::Lam)                 |
 | d   | `.con` n (`.`? p)+ ( `=` d\* e)? `;`                                                                                                              | continuation declaration<sup>s</sup> | [Lam](@ref mim::Lam)                 |
 | d   | `.fun` n (`.`? p)+ (`:` e<sub>ret</sub>)? ( `=` d\* e)? `;`                                                                                       | function declaration<sup>s</sup>     | [Lam](@ref mim::Lam)                 |
-| d   | `.Pi` n (`:` e<sub>type</sub>)? (`=` e)? `;`                                                                                                      | Pi declaration                       | [Pi](@ref mim::Pi)                   |
 | d   | `.Sigma` n (`:` e<sub>type</sub> )? (`,` L<sub>arity</sub>)? (`=` b<sub>[ ]</sub>)? `;`                                                           | sigma declaration                    | [Sigma](@ref mim::Sigma)             |
 | d   | `.ax` A `:` e<sub>type</sub> (`(` sa `,` ... `,` sa `)`)? <br> (`,` 𝖨<sub>normalizer</sub>)? (`,` L<sub>curry</sub>)? (`,` L<sub>trip</sub>)? `;` | axiom                                | [Axiom](@ref mim::Axiom)             |
 | n   | 𝖨 \| A                                                                                                                                            | identifier or annex name             | `fe::Sym`/[Annex](@ref mim::Annex)   |
@@ -238,7 +236,7 @@ This will bind
 Here is another example:
 
 ```rust
-Π.Tas::[T: *, as: .Nat][%mem.M, %mem.Ptr Tas] → [%mem.M, T]
+{T: *, as: .Nat}::Tas [%mem.M, %mem.Ptr Tas] → [%mem.M, T]
 ```
 
 #### Rebind
@@ -324,35 +322,15 @@ Expressions nesting is disambiguated according to the following precedence table
 | 2     | e `#` e  | extract                                        | left-to-right |
 | 3     | e e      | application                                    | left-to-right |
 | 3     | e `@` e  | application making implicit arguments explicit | left-to-right |
-| 4     | `Π` b    | domain of a dependent function type            | -             |
-| 5     | e `→` e  | function type                                  | right-to-left |
-
-@note The domain of a dependent function type binds slightly stronger than `→`.
-This has the effect that
-
-```rust
-Π T: * → T → T
-```
-
-has the expected binding like this:
-
-```rust
-(Π T: *) → (T → T)
-```
-
-Otherwise, `→` would be consumed by the domain:
-
-```rust
-Π T: (* → (T → T)) ↯
-```
+| 4     | e `→` e  | function type                                  | right-to-left |
 
 ## Summary: Functions & Types
 
 The following table summarizes the different tokens used for functions declarations, expressions, and types:
 
 | Declaration | Expression     | Type                    |
 | ----------- | -------------- | ----------------------- |
-| `.lam`      | `.lm` <br> `λ` | <tt>\|~\|</tt> <br> `Π` |
+| `.lam`      | `.lm` <br> `λ` | `->` |
 | `.con`      | `.cn`          | `.Cn`                   |
 | `.fun`      | `.fn`          | `.Fn`                   |
 
@@ -394,9 +372,9 @@ f .Nat ((23, 42), .cn res: .Nat = use(res))
 Finally, the following function types are all equivalent and denote the type of `f` above.
 
 ```rust
- Π  [T:*][[T, T], T → ⊥] → ⊥
-.Cn [T:*][[T, T], .Cn T]
-.Fn [T:*] [T, T] → T
+    [T:*] [[T, T], T → ⊥] → ⊥
+.Cn [T:*] [[T, T], .Cn T]
+.Fn [T:*]  [T, T] → T
 ```
 
 ## Scoping
@@ -410,27 +388,6 @@ The symbol `_` is special and never binds to an entity.
 For this reason, `_` can be bound over and over again within the same scope (without effect).
 Hence, using the symbol `_` will always result in a scoping error.
 
-### Pis
-
-@note **Only**
-
-```rust
-Π x: e → e
-```
-
-introduces a new scope whereas
-
-```rust
-x: e → e
-```
-
-is a syntax error.
-If the variable name of a Pi's domain is elided and the domain is a sigma, its elements will be imported into the Pi's scope to make these elements available in the Pi's codomain:
-
-```rust
-Π [T: *, U: *] → [T, U]
-```
-
 ### Annex
 
 Annex names are special and live in a global namespace.
@@ -445,12 +402,12 @@ In the following example, `i` refers to the first element `i` of `X` and **not**
 
 ```rust
 .let i = 1_2;
-Π X: [i: .Nat, j: .Nat] → f X#i;
+[i: .Nat, j: .Nat]::X → f X#i;
 ```
 
 Use parentheses to refer to the `.let`-bounded `i`:
 
 ```rust
 .let i = 1_2;
-Π X: [i: .Nat, j: .Nat] → f X#(i);
+[i: .Nat, j: .Nat]::X → f X#(i);
 ```

gtest/lexer.cpp

@@ -16,7 +16,7 @@ TEST(Lexer, Toks) {
     Driver driver;
     auto& w  = driver.world();
     auto ast = AST(w);
-    std::istringstream is("{ } ( ) [ ] ‹ › « » : , . .lam λ Π 23₀₁₂₃₄₅₆₇₈₉");
+    std::istringstream is("{ } ( ) [ ] ‹ › « » : , . .lam λ   23₀₁₂₃₄₅₆₇₈₉");
     Lexer lexer(ast, is);
 
     EXPECT_TRUE(lexer.lex().isa(Tok::Tag::D_brace_l));
@@ -34,7 +34,6 @@ TEST(Lexer, Toks) {
     EXPECT_TRUE(lexer.lex().isa(Tok::Tag::T_dot));
     EXPECT_TRUE(lexer.lex().isa(Tok::Tag::K_lam));
     EXPECT_TRUE(lexer.lex().isa(Tok::Tag::T_lm));
-    EXPECT_TRUE(lexer.lex().isa(Tok::Tag::T_Pi));
     auto tok = lexer.lex();
     EXPECT_TRUE(tok.isa(Tok::Tag::L_i));
     EXPECT_TRUE(lexer.lex().isa(Tok::Tag::EoF));

include/mim/ast/ast.h

@@ -7,9 +7,10 @@
 #include <fe/assert.h>
 #include <fe/cast.h>
 
-#include "mim/ast/tok.h"
 #include "mim/driver.h"
 
+#include "mim/ast/tok.h"
+
 namespace mim::ast {
 
 class LamDecl;
@@ -421,17 +422,20 @@ class ArrowExpr : public Expr {
     const Expr* codom() const { return codom_.get(); }
 
     void bind(Scopes&) const override;
+    Ref emit_decl(Emitter&, Ref type) const override;
+    void emit_body(Emitter&, Ref decl) const override;
     std::ostream& stream(Tab&, std::ostream&) const override;
 
 private:
     Ref emit_(Emitter&) const override;
 
     Ptr<Expr> dom_;
     Ptr<Expr> codom_;
+    mutable Pi* decl_ = nullptr;
 };
 
 /// One of:
-/// * `Π   dom_0 ... dom_n-1 -> codom`
+/// * `    dom_0 ... dom_n-1 -> codom`
 /// * `.Cn dom_0 ... dom_n-1`
 /// * `.Fn dom_0 ... dom_n-1 -> codom`
 class PiExpr : public Expr {

include/mim/ast/lexer.h

@@ -1,7 +1,5 @@
 #pragma once
 
-#include <optional>
-
 #include <absl/container/flat_hash_map.h>
 #include <fe/lexer.h>
 
@@ -23,7 +21,6 @@ class Lexer : public fe::Lexer<3, Lexer> {
 
     AST& ast() { return ast_; }
     const fs::path* path() const { return loc_.path; }
-    Loc loc() const { return loc_; }
     Tok lex();
 
 private:
@@ -41,9 +38,8 @@ class Lexer : public fe::Lexer<3, Lexer> {
         return res;
     }
 
-    Tok tok(Tok::Tag tag) { return {loc(), tag}; }
+    Tok tok(Tok::Tag tag) { return {loc_, tag}; }
     Sym sym();
-    Loc cache_trailing_dot();
     bool lex_id();
     char8_t lex_char();
     std::optional<Tok> parse_lit();
@@ -60,7 +56,6 @@ class Lexer : public fe::Lexer<3, Lexer> {
     std::ostream* md_;
     bool out_ = true;
     fe::SymMap<Tok::Tag> keywords_;
-    std::optional<Tok> cache_ = std::nullopt;
 
     friend class fe::Lexer<3, Lexer>;
 };

include/mim/ast/parser.h

@@ -87,7 +87,7 @@ class Parser : public fe::Parser<Tok, Tok::Tag, Look_Ahead, Parser> {
     Ptr<Expr> parse_extremum_expr();
     Ptr<Expr> parse_type_expr();
     Ptr<Expr> parse_ret_expr();
-    Ptr<Expr> parse_pi_expr();
+    Ptr<Expr> parse_pi_expr(Ptr<Ptrn>&& = nullptr);
     Ptr<Expr> parse_lam_expr();
     Ptr<Expr> parse_sigma_expr();
     Ptr<Expr> parse_tuple_expr();

include/mim/ast/tok.h

@@ -78,7 +78,6 @@ constexpr auto Num_Keys = size_t(0) MIM_KEY(CODE);
     m(D_quote_l,    "«")               \
     m(D_quote_r,    "»")               \
     /* further tokens */               \
-    m(T_Pi,         "Π")               \
     m(T_arrow,      "→")               \
     m(T_assign,     "=")               \
     m(T_at,         "@")               \
@@ -96,7 +95,7 @@ constexpr auto Num_Keys = size_t(0) MIM_KEY(CODE);
     m(T_semicolon,  ";")               \
     m(T_star,       "*")               \
 
-#define MIM_SUBST(m)                \
+#define MIM_SUBST(m)                   \
     m(".lm",     T_lm   )              \
     m(".bot",    T_bot  )              \
     m(".top",    T_top  )              \

include/mim/plug/direct/pass/ds2cps.h

@@ -1,14 +1,15 @@
 #pragma once
 
 #include <mim/def.h>
+
 #include <mim/pass/pass.h>
 
 namespace mim::plug::direct {
 
 /// Converts direct style function to cps functions.
 /// To do so, for each (non-type-level) ds function a corresponding cps function is created:
 /// ```
-/// f:     Π a: A -> B
+/// f:     [a: A] -> B
 /// f_cps: .Cn [a: A, .Cn B]
 /// ```
 /// Only the type signature of the function is changed and the body is wrapped in the newly added return continuation.

include/mim/plug/matrix/matrix.h

@@ -1,15 +1,16 @@
 #pragma once
 
-#include <mim/pass/pipelinebuilder.h>
 #include <mim/world.h>
 
+#include <mim/pass/pipelinebuilder.h>
+
 #include "mim/plug/matrix/autogen.h"
 
 namespace mim::plug::matrix {
 
 #define INTERNAL_PREFIX "internal_mapRed_"
 
-/// %mat.zero: Π [n: .Nat, S: «n; .Nat», m: .Nat] -> %mat.Mat (n,S,(.Idx m));
+/// %mat.zero: [n: .Nat, S: «n; .Nat», m: .Nat] -> %mat.Mat (n,S,(.Idx m));
 inline const Def* zero_int(World& w, Ref n, Ref S, Ref mem, nat_t m) {
     // TODO: use mim definition by name
     return w.app(w.annex<matrix::constMat>(), {n, S, w.type_idx(m), mem, w.lit_idx(m, 0)});

lit/annex.mim

@@ -4,7 +4,7 @@
 
 .let %annex.Vec3.xyz = [x: %math.F64, y: %math.F64, z: %math.F64];
 .let %annex.Vec3.rgb = [r: %math.F64, g: %math.F64, w: %math.F64];
-.rec %annex.Vec3.rec: □ = Π %annex.Vec3.xyz -> %annex.Vec3.rec;
+.rec %annex.Vec3.rec: □ = %annex.Vec3.xyz -> %annex.Vec3.rec;
 .let %annex.Vec3.zero = 0;
 
 // CHECK: zero = 0x8f3c66400000003

lit/beta_equiv.mim

@@ -4,7 +4,7 @@
 .plugin mem;
 
 .rec Num = [T: *, add: [T, T] -> T];
-.lam my_add .(pe: «2; .Nat») (a b: %math.F pe): %math.F pe = %math.arith.add 0 (a, b);
+.lam my_add {pe: «2; .Nat»} (a b: %math.F pe): %math.F pe = %math.arith.add 0 (a, b);
 
 .let F64 = (%math.F64, my_add @%math.f64);
 .ax %bug.Arr: Num -> *;

lit/direct/ds2cps_ax_cps2ds_dependent_short.mim.disabled

@@ -3,7 +3,7 @@
 
 /*
 Current issue:
-:4294967295: error: 'Π n_167425: .Nat → .infer (<nullptr>)' used as a type but is in fact a term
+:4294967295: error: '[n_167425: .Nat] → .infer (<nullptr>)' used as a type but is in fact a term
 
 Issue:
 https://github.com/AnyDSL/MimIR/issues/95

lit/direct/mut_dom_bug.mim

@@ -3,7 +3,7 @@
 
 .lam ForBody [n: .Nat] = [%mem.M, .Idx n] -> %mem.M;
 
-.lam For .[n: .Nat] [start: .Idx n, end: .Idx n] [mem: %mem.M] [it: ForBody n]: %mem.M =
+.lam For {n: .Nat} (start: .Idx n, end: .Idx n) (mem: %mem.M) (it: ForBody n): %mem.M =
     .lam loop [mem: %mem.M, i: .Idx n] @(%core.pe.known i) : [%mem.M, .Idx n] =
         .let `mem = it (mem, i);
 

lit/error/unsupported_rec.mim

@@ -1,3 +1,3 @@
 // RUN: (! %mim %s 2>&1) | FileCheck %s
-.rec S = {.Nat};
+.rec S = .Nat;
 // CHECK: error: unsupported expression

lit/fib.mim

@@ -5,7 +5,7 @@
 
 .plugin core;
 
-.con seq .(A: *) (n: .Nat) (body: .Cn [.Cn A][A]) (exit: .Cn A) (acc: A)@.tt =
+.con seq {A: *} (n: .Nat) (body: .Cn [.Cn A][A]) (exit: .Cn A) (acc: A)@.tt =
     head(0, acc)
     .where
         .con head (i: .Nat, acc: A)@%core.pe.known n =

lit/fun.mim

@@ -21,9 +21,9 @@
 .let g2 = .cn (T: *)((x y: T), return: .Cn T)       = return x;
 .let g3 = .fn (T: *) (x y: T)                       = return x;
 
-.let F1 = Π [T:*][T, T][T -> ⊥] -> ⊥;
-.let F2 =.Cn[T:*][T, T][.Cn T];
-.let F3 =.Fn[T:*][T, T] -> T;
+.let F1 =    [T:*] [T, T] [T -> ⊥] -> ⊥;
+.let F2 =.Cn [T:*] [T, T] [.Cn T];
+.let F3 =.Fn [T:*] [T, T] -> T;
 
 .fun bar(cond: .Bool): .Nat =
     .con t() =

lit/group.mim

@@ -1,4 +1,4 @@
 // RUN: %mim %s -o -
 .lam f(a b: .Nat, x: «a; .Nat»): .Bool = .ff;
 .ax %foo.F: [p e: .Nat] -> *;
-.ax %foo.bar: Π .[p e: .Nat]::pe [.Nat] [a b: %foo.F pe] -> %foo.F (p, e);
+.ax %foo.bar: {p e: .Nat}::pe [.Nat] [a b: %foo.F pe] -> %foo.F (p, e);

lit/let_ptrn.mim

@@ -1,6 +1,6 @@
 // RUN: %mim %s -o -
 .ax %foo.F: * -> *;
-.ax %foo.f: |~| T: * -> .Nat -> %foo.F T;
+.ax %foo.f: [T: *] -> .Nat -> %foo.F T;
 
 .fun .extern f(
         T: *,

lit/rec_pi.mim

@@ -6,7 +6,7 @@
 .ax %phase.phase2: []            -> %phase.Phase;
 .ax %phase.phase3: [.Nat, .Bool] -> %phase.Phase;
 
-.rec PiPeline: * = |~| %phase.Phase -> PiPeline; // got the pun? XD
+.rec PiPeline: * = %phase.Phase -> PiPeline; // got the pun? XD
 
 .ax %phase.pipe: PiPeline;
 

lit/recursive_uniform_bug.mim

@@ -2,5 +2,5 @@
 .let Triple = [T: *, U: *, V: *];
 
 .ax %bug.Box: Triple -> *;
-.ax %bug.test: Π [n: .Nat] [Ss: «n; Triple», X: Triple] -> %bug.Box X;
+.ax %bug.test: [n: .Nat] [Ss: «n; Triple», X: Triple] -> %bug.Box X;
 .lam l3 [S: Triple]: %bug.Box S = %bug.test 3 ((S, S, S), S);

lit/restructre_free_var.mim

@@ -3,15 +3,15 @@
 
 .plugin core;
 
-.ax %foo.Mat: Π [n: .Nat, S: «n; .Nat», T: *] -> *;
+.ax %foo.Mat: [n: .Nat, S: «n; .Nat», T: *] -> *;
 
 .ax %foo.map_reduce:
     // out shape depends on in shape but is complex
-    Π [n: .Nat, S: «n; .Nat», T: *, // out shape
-        m: .Nat,                    // number of inputs
-        NI: «m; .Nat»,              // input dimensions
-        TI: «m; *»,                 // input types
-        SI: «i:m; «NI#i; .Nat»»     // input shapes
+    [n: .Nat, S: «n; .Nat», T: *, // out shape
+     m: .Nat,                    // number of inputs
+     NI: «m; .Nat»,              // input dimensions
+     TI: «m; *»,                 // input types
+     SI: «i:m; «NI#i; .Nat»»     // input shapes
     ] ->
     // for completeness sake
     // main arguments