Uncase removal pass

[DCupello1]

This transformation focuses on transforming uncase expressions into explicit projection functions.

This is achieved through the following steps:

• The uncase expressions are collected and placed in a map (as a first pass). This is a map from id
  to a list of mixops.
• When encountering a user defined type definition, we lookup in the map and generate
  the projection functions accordingly for each mixop in the list. If there is more than one case,
  the projection function returns the case tuple wrapped in an optional type.
• When encountering an uncase expression, we just simply make the appropriate transformation
  to a function call.

This pass works with/without dependent types. It will simply add the dependent type parameters
to the projection function whenver necessary.

As an example,
given the following type:

syntax foo =
  | A v
  | B c v

where A and B are case constructors, and v c are types.

Assume we have uncase expressions somewhere in our script (with x being a variable of type foo):
(x!A).0 and (x!B).1

This is transformed into:

syntax foo =
  | A v
  | B c v

def $proj_foo_0(x : foo) : (v)?
  def $proj_foo_0{var : v}(A(var)) = ?(var)
  def $proj_foo_0{var : foo}(var) = ?()

def $proj_foo_1(x : foo) : (c, v)?
  def $proj_foo_0{v_c : c, v_v : v}(B(v_c, v_v)) = ?((v_c, v_v))
  def $proj_foo_0{var : foo}(var) = ?()

with uncase expressions being transformed into:
(the($proj_foo_0(x))).0 and (the($proj_foo_1(x))).1

Names were specifically chosen here for simplicity.

This pass is an attempt to make uncase semantics more general, even though its use case is only limited to single case types.

[DCupello1]

I am assuming the CI is using version 4.10-4.12 ? Will note that for the future.

(Maybe 5.0 given it states in the README to get ocaml 5.0 or higher)

[DCupello1]

@rossberg: would you know why the CI would stack overflow? I have ran the tests locally and they seem to be fine.

[rossberg]

I have no idea in particular, but usually that's because some algorithm ends up in an infinite loop.

[rossberg]

FWIW, sometimes not all tests are run properly unless you do a make clean.

[DCupello1]

I have no idea in particular, but usually that's because some algorithm ends up in an infinite loop.

Hmm thats what I thought initially, it might just be that I didn't make clean. I'll rerun the tests locally and see.

[nomeata]

Names were specifically chosen here for simplicity.

Doesn't have to be now, but probably it'll improve our lives down the road if the name includes the name of the construction that's being projected out

[DCupello1]

Names were specifically chosen here for simplicity.

Doesn't have to be now, but probably it'll improve our lives down the road if the name includes the name of the construction that's being projected out

Fair enough, though for the sake of this PR and #195 I'll change it in a future PR.

Though in the cases that it is actually used on at the moment, the constructors are empty strings. But who knows how this will be used later.

[nomeata]

Though in the cases that it is actually used on at the moment, the constructors are empty strings.

Ah ok, I wasn’t aware of that. What’s the source syntax for that? What comes after the !?

[DCupello1]

An example of this is:

syntax uN = 
  | `%`{i : nat}(i : nat)

Which has source syntax as:

syntax uN(N) hint(desc "unsigned integer") hint(show u#%) =
  0 | ... | $nat$(2^N-1)

After the ! it would just be %. Example: i!%_uN.0 (the _uN is the type, not the constructor itself)

[nomeata]

Thanks!

[rossberg]

Perhaps the simplest example of an anonymous constructor being generated would be something like

syntax u8 = nat  -- if nat < 256

[DCupello1]

@nomeata I guess you can review this one then! Would you like me to fix the merge conflicts first though?

[nomeata]

Not needed, I can look at the diff. But I need to point out that I am fundamentally not a good reviewer, because I am usually too optimistic and too trusting…

[nomeata]

Looks good enough to me

[nomeata]

Have you considered not writing this code, and instead add a partial annotation when there is more than one case, and leave the opt-transformation to the totality pass?

[DCupello1]

Haven't considered it, (or maybe I have, and I can't remember). It would make it cleaner yes.

Only issue with adding a partial annotation is making more dependencies between passes, which we kind of want to avoid, as there are already many dependencies.

[nomeata]

I think dependencies are ok where they compose nicely or avoid duplicating logic. But it's not a lot of code, so fine as is indeed.

[DCupello1]

Makes sense. I'll leave it for now, and once we have a bigger picture on all the dependencies, I'll look into improving this.

[nomeata]

Just a nit, but (unless you go via the partial hint anyways), can you if has_one_case earlier, and indent, so that those bindings that are only relevant in the then-case are really only in the the then case?

let make_func …
  let …
  if has_one_case then
    let …
    DecD …
  else
    let …
    DecD …

[DCupello1]

Fair enough! I'll modify this while fixing the merge conflicts