Allow local modules to be forward referenced

[janmasrovira]

This pr makes a number of changes to the Scoper. The most important change is that local modules can be forward referenced. Below I list all the changes.

• Closes The rules for where blocks of mutually recursive definitions end are unclear and confusing #3032

Referencing local modules

Local modules can now be forward referenced. However, there is one restriction:

1. When forward referencing a local module. The symbols that come from an open public are not yet in scope, so they can't be referenced. E.g.

   -- at this point, P.p is in scope, but P.m is not
   
   module P;
     axiom p : Type;
   
     open M public;
   end;
   
   -- at this point, both P.p and P.m are in scope
   
   module M;
     axiom m : Type;
   end;
   

Forward reference passed an import, open or module statement

The following example was not allowed but now it is.

axiom A : B;
import M;
module S;
end;
axiom B : Type;

Changes in operators and iteratos

The semantics of operator and iterator definitions have changed slightly. Before, when the scoper found syntax operator , pair, it would remember in the state that when the , symbol is defined in the current syntax block, it should have the fixity pair. These had some implications.

1. It was not possible to reassign/overwrite a fixity.
2. The , symbol in the syntax operator , pair is not highlighted and it doesn't support going to definition.
3. We required special checks to throw an error when we had duplicate operator/iterator definitions. We also had a check for when a symbol used in an operator/iterator statement was not defined in the same syntax block.

The new behaviour is as follows.

1. When the scoper finds syntax operator , pair, the symbol , is scoped using the regular scoping rules - so , must be in scope. Then, the scoper modifies the fixity for , in the current scope.
2. It is now possible to overwrite the fixity of a symbol. So this would be possible.

syntax operator , pair;
p1 : Pair Nat Nat := 1, 2;
syntax operator , none;
p2 : Pair Nat Nat := , 1 2;

6. It is now possible to have qualified names in syntax/iterator definitions. E.g. syntax operator Pair., pair.

Because of point 1) we might encounter some breaking changes.

1. syntax operator mkpair none;
   syntax alias mkpair := ,;
   

   This is now invalid because mkpair is not in scope in the syntax operator
   statement, because aliases cannot be forward referenced.
2. A syntax operator op fix will now throw an ambiguity error if op is both defined in this module and imported from somewhere else.

Qualified fixities

It is now possible to reference fixities using qualified names. E.g.

syntax operator , Fixities.pair;

Pending tasks

• Add positive test for local module forward referencing.
• Add positive test for fixity overwriting.
• Add positive test for qualified fixity.
• Add positive test for qualified operator.
• Add negative tests for local module forward referencing restrictions.
• Fix printing of operators in Core.
• Cleanup the code.

[paulcadman]

Q: What needs to change in https://github.com/anoma/nspec to be compatible with this PR?

[janmasrovira]

Q: What needs to change in https://github.com/anoma/nspec to be compatible with this PR?

• I've made a pr (https://github.com/anoma/nspec/pull/327).

The only relevant change related to this pr is tiny:
.