[TOC]

We use the following notation:

Mim files are UTF-8 encoded and lexed from left to right.

@note The maximal munch strategy resolves any ambiguities in the lexical rules below. For Example, <<< is lexed as << and <.

The actual terminals are specified in the following tables.

The grammatical rules will directly reference these primary terminals. Secondary terminals are ASCII-only tokens that represent the same lexical element as its corresponding primary token. For example, the lexer doesn't care, if you use ⊥ or .bot. Both tokens are identified as ⊥.

In addition you can use ⟨, ⟩, ⟪, and ⟫ as an alternative for ‹, ›, «, and ».

In addition the following keywords are terminals:

All keywords start with a . to prevent name clashes with identifiers.

The following terminals comprise more complicated patterns:

The previous table resorts to the following definitions as shorthand:

So, sym refers to the shorthand rule while 𝖨 refers to the terminal that is identical to sym. However, the terminal A also uses the shorthand rule sym.

In addition, the following comments are available:

• /* ... */: multi-line comment
• //: single-line comment
• ///: single-line comment for Markdown [output](@ref cli):
  • Single-line /// xxx comments will put xxx directly into the Markdown output. You can put an optional space after the /// that will be elided in the Markdown output.
  • Everything else will be put verbatim within a fenced code block.

Mim's grammar is defined as a context-free grammar that consists of the terminals defined above as well as the nonterminals and productions defined below. The start symbol is "m" (module).

The follwing tables summarizes the main nonterminals:

The following tables comprise all production rules:

@note An elided type of a .Pi or Sigma declaration defaults to *.

Patterns allow you to decompose a value into its components like in Standard ML or other functional languages.

There are

• p: parenthesis-style patterns (()-style), and
• b: bracket-style patterns ([]-style) .

The main difference is that

• (a, b, c) means (a: ?, b: ?, c: ?) whereas
• [a, b, c] means [_: a, _: c, _: d] while
• (a: A, b: B, c: C) is the same as [a: A, b: B, C: C].

You can switch from a ()-style pattern to a []-pattern but not vice versa. For this reason there is no rule for a ()-[]-pattern.

Tuple patterns allow for groups:

• (a b c: Nat, d e: Bool) means (a: Nat, b: Nat, c: Nat, d: Bool, e: Bool).
• [a b c: Nat, d e: Bool] means [a: Nat, b: Nat, c: Nat, d: Bool, e: Bool].

You can wrap a pattern into an alias pattern:

let (a, b, c) as abc = (1, 2, 3);

This will bind

• a to 1,
• b to 2,
• c to 3, and
• abc to (1, 2, 3).

Here is another example:

{T: *, a: Nat} as Ts → [%mem.M, %mem.Ptr Ts] → [%mem.M, T]

A let and ret expression allows you to rebind the same name to a different value. This is particularly useful, when dealing with memory:

let (mem, ptr) = %mem.alloc (I32, 0) mem;
let mem        = %mem.store (mem, ptr, 23:I32);
let (mem, val) = %mem.load (mem, ptr);

@note An elided type of

• a literal defaults to Nat,
• a bottom/top defaults to *.

Expressions nesting is disambiguated according to the following precedence table (from strongest to weakest binding):

The following table summarizes the different tokens used for functions declarations, expressions, and types:

The following function declarations are all equivalent:

lam f(T: *)((x y: T), return: T → ⊥)@(ff): ⊥ = return x;
con f(T: *)((x y: T), return: Cn T)          = return x;
fun f(T: *) (x y: T): T                       = return x;

Note that all partial evaluation filters default to tt except for con/cn/fun/fn.

The following function expressions are all equivalent. What is more, since they are bound by a let declaration, they have the exact same effect as the function declarations above:

let f =  λ (T: *) ((x y: T), return: T → ⊥)@(ff): ⊥ = return x;
let f = lm (T: *) ((x y: T), return: T → ⊥)      : ⊥ = return x;
let f = cn (T: *) ((x y: T), return: Cn T)          = return x;
let f = fn (T: *)  (x y: T): T                       = return x;

The following expressions for applying f are also equivalent:

f Nat ((23, 42), cn res: Nat = use(res))
ret res = f Nat $ (23, 42); use(res)

Finally, the following function types are all equivalent and denote the type of f above.

[T: *] →    [[T, T], T → ⊥] → ⊥
[T: *] → Cn [[T, T], Cn T]
[T: *] → Fn  [T, T] → T

Mim uses lexical scoping where all names live within the same namespace - with a few exceptions noted below. @note The grammar tables above also indiciate which constructs open new scopes (and close them again) with this^s annotation in the Comments column.

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.

Annex names are special and live in a global namespace.

Named elements of mutable sigmas are available for extracts/inserts.

@note These names take precedence over the usual scope. In the following example, i refers to the first element i of X and not to the i introduced via let:

let i = 1_2;
[i: Nat, j: Nat]::X → f X#i;

Use parentheses to refer to the let-bounded i:

let i = 1_2;
[i: Nat, j: Nat]::X → f X#(i);