Imported items in requires

[boyland]

In version 1.6.0a1, a module might want to refer to an existing module in the "requires" section. For example:

module set
requires
  
  abstract syntax e
  abstract judgment elem-equal: e = e

  syntax n = org.sasylf.util.Natural.n ::= 0 | 1+ n    
  judgment nat-eq = org.sasylf.util.Natural.equal : n = n

  abstract judgment toNat: e <-> n
  // ...

We need n so that we can refer to it in the toNat bijection, and we need the equality judgment so that we can refer to it in the abstract theorems that the bijection is actually a bijection.

This leads to two problems in 1.6.0a1

1. There was an error for nat-eq saying that it was neither abstract nor had rules. (NB: this error was happening when I ran the example in the PR but it went away in the actual release. Not sure why, it's easy to fix in any case.)
2. More seriously, in the module substitution, it's not possible to substitute in org.sasylf.util.Natural.n, one gets the error message

   Nonterminal type mismatch in module argument. Nonterminal nhas type n, but is expected to have type n because n is bound to n.

As I said, the first item is easy to fix. The second problem is much more serious,. (There is of course a typo in the error message "nhas" should be "n has"). I renamed the import of n in the using module to see which n was which. This got the updated message:

Nonterminal type mismatch in module argument. Nonterminal mhas type m, but is expected to have type n because n is bound to n.

At the initial level: the instantiation should permit substitution with a use of the same module (without parameters).

Thinking about the big picture, it would be better to update modules to have an "imports" section (or the like) before the requires for situations like this, since we don't want people to have to provide actual parameters when the nonterminal/judgment is not actually abstract. Or maybe we change parameterization to not require any corresponding actual for non-abstract things in "requires". (This would be a breaking change and would have to be decided upon before releasing 1.6.0 .)

[boyland]

A conservative resolution of this issue and Issue #137 would include:

• A new section of "imports" in a module to include module imports, including nonterminals and judgments imported.
• imports not allowed in "requires" but non-abstract judgments (and rules) allowed, and checked.