Feature/infer5

[leissa]

Type Inference 2: Electric Boogaloo

Okay, lots of changes here and there are still plenty of loose ends but at some point I wanted to merge into master before the changes are getting out of hands. Here is a list of the most important ones:

Curried Functions

These are now working as expected:

.lam f (i: .Nat)(j: .Nat) -> .Nat = /*...*/;
.con g (T: *)(x: T) = /*...*/;
.let k: .Cn [T: *][T, T] = /*...*/;

Note, that all curried parameter groups are in direct style even for .con/.cn/.Cn. Here, only the last parameter makes up the continuation.

Implicits and Type Inference

You can now mark a parameter group as implicit with a dot like this:

.ax %mem.load:  Π.Tas::[T: *, .Nat][%mem.M, %mem.Ptr Tas] -> [%mem.M, T], normalize_load;
.ax %core.wrap(add, sub, mul, shl): Π.[s: .Nat][.Nat][«2; .Idx s»] -> .Idx s, normalize_wrap;
.con .extern internal_diff_core_icmp_xYgLE !.(s: .Nat)!(ab::(a b: .Idx s), ret: .Cn[.Idx 2, .Cn[.Idx 2, .Cn«2; .Idx s»]]) =
    ret (%core.icmp.sle ab, .cn ![.Idx 2, pb_ret: .Cn«2; .Idx s»] = pb_ret ‹2; 0:(.Idx s)›);

The argument will be automatically inferred by Thorin:

.let acci = %core.wrap.add 0 (i, acc);

From the C++ API you can now use World::call/World::dcall like this:

w.dcall(dbg, core::wrap::add, mode, Defs{ldef, rdef});
w.call(core::wrap:: add, mode, Defs{ldef, rdef});

I ported core, mem, and math to make use of implicits and removed the now superfluous boilerplate from the dialect headers.

We had some discussions in Discord about the syntax for . and !. For now, I kept it like this because the other idea for using | just looked really odd to me but we can still change this.

In order to make this work, I'm using a class Ref that automatically looks through Infers. We have to use these Ref things even more aggressively, but for now I didn't want to have the diff going completely nuts.

The IR keeps track of implicits with the help of Def::meta. This can now be a nested pair that mirrors the curried type and indicates where to place an Infer.

Right now, the type inference will be triggered as soon as a function with implicit arguments is fully invoked. More complex things, won't work for now, but I will work on that in the future.

UMax/UInc

The type level doesn't have to be a constant anymore and can be adjusted with the umax/uinc operators. This is important for type inference and may be interesting for future universe polymorphism.

Minor Changes

• Improved Def::dep & friends
• Disabled Windows Debug workflow as MSVC Linker is going bonkers again :(
• Removed this clumsy error handler in favor of just emitting an error.

Impala

Impala branch here.