Question

How do I disambiguate module names in an example like this:

module util {
  const x: nat := 0
}

module java {
  module util {
    const y: nat := util.x
    method test() { assert y == 0; }
  }
}

Answer

There is no direct syntax to do what is wanted here. If you have control of the names, perhaps some renaming or moving the top-level util to be a sub-module of another module. If this structure cannot be changed, then the following somewhat ugly code is a work-around:

module util {
  const x: nat := 0
}

module util_ {
  import util
}

module java {
  module util {
    import util_
    const y: nat := util_.util.x
    method test() { assert y == 0; }
  }
}

There is discussion of defining syntax that names the top-level module, which would make an easy way to solve the above problem. See this issue.