N⋆ v3: complete breaking change?

[Mesabloo]

It's that time of the year, thinking about re-designing N⋆ (again).

As of now, N⋆ lacks flexibility:

• adding a new platform requires changing a lot of things inside the compiler
• while trying to be generic, the instruction set may not work great on some platforms (e.g. x86)
• all platforms do not have the same number of registers, and we currently only limit those to r0 until r5 (whereas there are more than 16 registers on amd64)

But here are some challenges:

• we need to be able to extend the current typechecker while adding new instructions
• parsing mainly becomes handling macros
• how to handle code generation
• optimizations through type- and context-aware rewrite rules?
• the grammar for types and labels is fixed, but do we want users to also change those?

[Mesabloo]

A very quick idea we could consider for N⋆ is this (key points are in bold):

• We need to have a way to add instructions (either terminal -- jumps --, or not)
• For each added instruction, there needs to be types pre- and post-conditions (typing rules, really)
  • How do we handle ad-hoc “polymorphism”? e.g. specifying two mov/2 instructions able to be typed differently depending on their arguments (this is common in the current design of N⋆, where mv has 2 or 3 different typing rules)
• Multiple (or zero) rewrite rules can be attached to a specific instruction for optimization purposes
• Allow describing how to encode a specific instruction in machine code (might also be a VM bytecode at this point, tho it would be harder to generate a specific format)

For each of these points, we could create file “sections” (in a specific interface file), something along those lines:

# x86.nsti

%registers 6;;
# Indicate there are only 6 registers named `%r0` to `%r5` for the X86 architecture

%instructions {
  # `mov` takes 2 arguments, where `src` must have type `τ` and the continuation is neither `src` nor `dst`
  mov/2 | src dst := ( Γ; Δ; Ξ; χ; σ; ε ⊢ src : τ
                     & src /= ε
                     & dst /= ε
                     ) => (Γ; Δ; Ξ; χ; σ; ε ⊢ Γ; Δ; Ξ; χ ∖ dst, dst : τ; σ; ε);;
                     
  # No syntax errors: only type errors (clearer)
  # In this case, we should have pattern matched on `dst` to only allow registers as the destination operand
  #   but for the sake of being a simple example, we did not        
  #
  # This also lacks an alternative ASCII syntax, but this is not the main problem at all      
}

%rewrite {
  mov/2 | src dst := ignore;;
  # Completely optimize away any `mov/2` from the source code, before generating machine code
}

let registerNumber 
    | (reg 0) := 2
    | (reg 1) := 3
    | (reg 2) := 0
    # ...
    ;;
# We can also embed micro helper functions which can be used throughout the sections (mostly `%rewrite` and `%generate`)

%generate {
  # move from register `src` to register `dst`
  mov/2 | (reg src) (reg dst) := [ 0x10, 0x20, registerNumber src, 0x30, registerNumber dst ];; 
                                    # Not actual valid x86 machine code
}

[Mesabloo]

Very much looks like a “complete” compiler generator for an assembly language!

[Mesabloo]

We may also embed a very simple Prolog to write typechecking rules, for simpler use.
We still need some builtins so as to access environments or have predicates for some rules (e.g. call where we need to filter our banged registers).

[Mesabloo]

This is in fact not that great of an idea.

First of all, this makes N⋆ hard to maintain: 3 languages instead of 1, each having completely different evaluation strategies.
Second of all, the burden of having to maintain that many languages is not worth the few extensibility advantages it “offers”.
And finally, errors will basically be trash going for something like this. While N⋆ is not really meant to be used by people directly (this is particularly a compiler backend), this is still required to facilitate debugging.

Therefore, this will not happen. N⋆ stays the way it has been and will be extended with new features (see e.g. #59 and #47) or new targets (see #57 and #37).