Based on #1760

Currently the Regionality axis has three levels: global, regional and local. This PR generalizes it to natural numbers 0, 1, 2, ... where 0 means global, 1 means the top level, and so on. For example:

let local_ x = "hello"
let foo () = 
  let z = "foo" in 
  let local_ y = ref z in 
  ()

z is 0, y is 2. x would be 1, but it will be rejected because we force top-level to be global.

Moreover, Regionality is indexed as follows:

Regionality 1 = {0, 1}
Regionality 2 = {0, 1, 2}
...

The essential idea is that, by indexing, we can avoid talking about Regionality = 6 when we are only in 5 layers of nested regions. This is essential for some morphisms to have adjoints.

Note that the index starts at 1 instead of 0 - this is also essential for some morphisms to have adjoints. Intuitively, some adjunctions lose meanings if there is only "global" and no local to talk about.