new MINT module and polymorphic sort support

[dwightguth]

Essentially, the design is as follows:

• Instantiations of parametric sorts must be explicitly declared in order to be used in the frontend.
• natural numbers are implicitly sorts, but they have no productions and simply serve as placeholders for actual natural numbers
• sort inference picks the correct parameters for the widths based on the declared subsort relations, which are over parametrized sorts, not sort heads.
• the kore generated has a concrete width for all axioms that use MINT symbols, and that width is a sort with a nat attribute specifying the width in bits that it corresponds to.
• the MINT module has been substantially refactored in order to bring it stylistically into alignment with the rest of the frontend.

Code passes all tests and seems to generate the right kore when I inspect it manually, but the backend isn't implemented yet so we can't actually run anything or build an llvm backend interpreter yet. That will come in a pr to the backend next.

[ttuegel]

This parameterization should be fine for the Haskell backend, but what will Width be instantiated with in practice?

[dwightguth]

For reference, here is a subset of a K definition I wrote for testing purposes that uses the MINT module:

module TEST
  imports MINT

  syntax MInt{8}
  syntax Number ::= Int | MInt{8}

  syntax AExp ::= Number
                | AExp "+" AExp [strict]

  syntax KResult ::= MInt{8}

  rule I:Int => Int2Signed(I)::MInt{8}

  rule I + J => I +MInt J

endmodule

In this case the frontend treats 8 like a sort, but the kore generation will generate a sort declaration containing an attribute annotating the sort with its corresponding bitwidth, which the backend will understand. This is basically just a workaround until we reach the point where we can have natural numbers as parameters of sorts.

[ehildenb]

This is a pretty huge change, is there a reasonable way to separate it out into 2 or 3 PRs? Would make reviewing it easier.

[radumereuta]

Encoding null with some sort of information seems odd to me.

[dwightguth]

this is already to a certain extent how the sort injection pass deals with there not being an expected sort. We could probably make it an optional instead, but it really doesn't get a lot better by doing so. I'm going to leave this as is and someone can refactor the whole thing later if they want to.

[dwightguth]

@ehildenb we could probably break out the changes to the AST and the parser from the changes to kore generation, but it wouldn't make the first of those two PRs very much smaller and then we wouldn't have any test for it. Do you still want me to? I'm not sure it's going to be possible to separate the changes to the parser from the changes to the AST, because they very much go hand in hand.

[dwightguth]

With that being said, if you look at the commits one at a time, it should give you a pretty good idea of the evolution of changes required; I can try to refactor the history some so that it's more concise before you do that if you want though.

[ttuegel]

Generated Kore looks good to me!

[yzhang90]

I only reviewed ModuleToKore.java and it looks good to me.