Syntax and semantics of namespaces

[favonia]

• [ ] enrich ResEnv to enable local opens and prefixing
• [ ] implement the keywords open and namespace, sharing the code with #449.

• [ ] implement the += shortcut.

  This is what I want:

0. A namespace M.O.P telescope has exactly three effects:

   • temporarily do open M.O.P and
   • prefix every definition and nested namespace inside and
   • restore the old name resolver and merge all new public definitions according to the syntax in #449 but the default case is -> public M.O.P instead of private *.

1. Concretely, all the following should be exactly the same:

   namespace x.y (c : bool) with
   def a : bool = tt
   namespace z.w (d : bool) with
   def b : bool = tt
   end [public *] -- implicit
   end

   namespace x.y (c : bool) with
   open x.y [private] -- implicit
   def a : bool = tt
   def z.w.b (d : bool) : bool = tt
   end

   def x.y.a (c : bool) : bool = tt
   def x.y.z.w.b (c : bool) (d : bool) : bool = tt

   namespace with
   def x.y.a (c : bool) : bool = tt
   def x.y.z.w.b (c : bool) (d : bool) : bool = tt
   end [x.y.z.w.b -> x.y.z.w.d] -- public by default

2. Blind batch applications after open: it seems to be convenient to blindly apply all functions imported by an open to the same set of arguments. This means a new function is defined for each imported name with the same set of argument. There is no restriction as long as the elaboration and type-checker (run independently on each application) are happy. The following two should be the same.

   namespace M += N.O.P [ x -> y ] a b c

   open N.O.P [ x -> public M.y | -> public M ] a b c

---

These are the current full syntax

[private] namespace [name path] [telescope] begin ... end [name modifiers] arguments

[private] namespace [name path] [telescope] += name path [name modifier] arguments

and the following two should be the same

[private] namespace [name path A] [telescope] += (name path B) [name modifier] arguments

[private] namespace [name path A] [telescope] begin
  public open (name path B) [name modifier] arguments
end

[favonia]

The copy-paste semantics for imports:

import a [name modifiers] arguments

should be effectively the same as

private namespace begin

-- compiled content of a.red (without running ML again)

end [name modifiers] arguments

[favonia]

Mostly implemented by https://github.com/RedPRL/yuujinchou.