Opening scopes at top level
When targetting WhyML from other languages, we would like to use scopes
to help manage the namespaces for the produced code. In particular, it is desirable to produce a forest of nested scopes which contain modules or other declarations at the leaves. Currently, this is not possible as module
s must be the top-level constructs of a WhyML file (implicit or explicit).
This restriction which prevents scopes from being at the top-level and thus containing modules seems unnecessary.
As a concrete example of what I would like to do:
scope MyScope
module Mod1
type t
end
scope OtherScope
(* optional, allow implicit modules inside scopes *)
let x () : bool = body
end
end
This code currently raises an error stating "Trying to open a module inside a module" due to the implicit module opened by Why3.