Syntax and semantics of name modifiers (v5.1, WIP)

[favonia]

• [ ] pattens.
• [ ] implement the blind application.
• [ ] equip import with the new syntax.
• [ ] check unused subpatterns.

• [ ] enable the most powerful ML version.

(The issue description contains the latest syntax.)

The full import syntax is

["public"] "import" path [modifier]+ arguments

and the full syntax of name modifiers is:

modifier := "[" act "]" -- see below for the meaning of "[]".

act :=
  | "<:" ML function of type
    subpattern:bool -> path-> [`Match of (path * [`Hidden | `Shown] * [`Public | `Private] option) list | `NoMatch | `Err]
    ":>"
  | "*" -- match p with [] -> `NoMatch | _ -> `Match [l, `Shown, None]
  | id
    /-
      if p = [id] then
        `Match [p, `Shown, None]
      else if subpattern then
        `NoMatch
      else
        `Match [p, `Hidden, None]
    -/
  | [path0] "->" [tag] [path1]
    /-
      if p = Option.default [] path0 then
        `Match [Option.default [] path1, `Shown, tag]
      else if subpattern then
        `NoMatch
      else
        `Match [p, `Shown, None]
    -/
  | "!" act -- match act ~subpattern p with `Match l -> `Match (map (`Shown <-> `Hidden) l) | `NoMatch -> `NoMatch | `Err -> `Err
  | tag act -- match act ~subpattern p with `Match l -> `Match (map (None -> Some tag) l) | `NoMatch -> `NoMatch | `Err -> `Err
  | act0 "|" act1
    /-
      match act0 ~subpattern p, act1 ~subpattern p with
      | `Err, _ | _, `Err -> `Err
      | `NoMatch, `NoMatch -> `NoMatch
      | `NoMatch, `Match l | `Match l, `NoMatch ->
        let l = filter `Shown l in if l = [] then `NoMatch else `Match l
      | `Match l0, `Match1 l1 when consistent l0 l1 -> `Match (union l0 l1)
      | _ -> `Err

      consistency = for each resulting path, the [`Public | `Private] option parts match.
      union = `Shown | `Hidden -> `Shown
    -/
  | act0 "&" act1
    /-
      match act0 ~subpattern p, do act1 ~subpattern p with
      | `Err, _ | _, `Err -> `Err
      | `NoMatch, `NoMatch -> `NoMatch
      | `NoMatch, `Match l | `Match l, `NoMatch ->
        let l = filter `Hidden l in if l = [] then `NoMatch else `Match l
      | `Match l0, `Match1 l1 when consistent l0 l1 -> `Match l0
      | _ -> `Err

      consistency = for each resulting path, the [`Public | `Private] option parts match.
      union = `Shown | `Hidden -> `Hidden
    -/
  | act0 "." act1 -- vertical concatenation of actions
    /-
      union_match ~subpattern p @@ fun p0 p1 -> -- p = p0 @ p1
      match act0 ~subpattern:true p0, act1 ~subpattern:true p1 with
      | `Err, _ -> | _, `Err -> `Err
      | `NoMatch, _ | _, `NoMatch -> `NoMatch
      | `Match l0, `Match1 l1 -> `Match (concat l0 l1)
    -/
  | act0 ";" act1 -- horizontal concatenation of actions
    /-
      join (act0 ~subpattern) (act1 ~subpattern) p
    -/
  | "[" act "]" -- act ~subpattern:false p

---

Comparison with Agda:

open import A.B -- ignore A.B for comparison

import A.B

open import A.B using (x; y) -- ignore A.B for comparison

import A.B [x | y]

open import A.B renaming (x to y) -- ignore A.B for comparison

import A.B [x -> y]

open import A.B hiding (x; y) -- ignore A.B for comparison

import A.B [! x & ! y]
import A.B [! (x | y)]

import A.B as C

import A.B [-> C]

import A.B as C using (x; y; z)

import A.B [x | y | z; -> C]

import A.B as C renaming (x to y)

import A.B [x -> y; -> C]

import A.B as C renaming (x to y; z to w)

import A.B [x -> y | z -> w; -> C]

import A.B as C hiding (x; y)

import A.B [!x & !y; -> C]
import A.B [! (x | y); -> C]

Something that Agda can't do:

import A.B [C.x -> x]

[favonia]

The trolling but otherwise very clear import syntax:

import x.y [ -> none] -- imports nothing
import x.y [x -> private x] -- imports everything (default)
import x.y [x -> public x] -- same as "public import"
import x.y ["z" | "y" as z -> public z | "op2" -> private "op1" | _ -> none]

EDIT: This comment is outdated

[jonsterling]

omg this would be so great to have!!!

[jonsterling]

@favonia As powerful as the notation you are suggesting is, I think it might be clearer to our users if we did something a bit more simple-minded and less powerful, maybe along the lines of what is supported in Agda.

[jonsterling]

(BTW I'm still open to some very powerful version like you suggest)

[favonia]

Well, we can support the less powerful syntax and compile it down to the ultimate syntax. To me, it is never clear what Agda would do if I simultaneous use and hide and/or rename something. (In fact, I just discovered that the documentation was outdated!)

How about this dumb version?

import x.y [ -> hidden ] -- import nothing
public import x.y [ -> hidden ] -- (same as above)
import x.y [ ] -- import everything (default)
import x.y -- (same as above)
public import x.y [ -> private ] -- (same as above)
import x.y [ -> public ] -- import and re-export everything
public import x.y [ ] -- (same as above)
public import x.y -- (same as above)
import x.y [ z | y -> public | op2 -> public op1 | -> hidden ] -- import and re-export z and y, import and re-export op2 as op1, and hide everything else
import x.y [ z | y -> hidden ] -- import everything except z or y
import x.y [ z | y -> hidden | -> public ] -- import and re-export everything except z or y

The defult tag is private for import or public for public import. Anything not mentioned by the case analysis is implicitly treated as the default tag says.

The full version distinguish meta-variables from names, which means

import x.y ⦉ write your own ML function of type "string list -> string list tag list" ⦊

The restriction is that this needs to be injective except for hidden.

[favonia]

The full syntax of name modifiers is:

<: ML function :>

or

"[" (cases divided by "|") "]"

A case is one of the following:

pattern -> [tag] [name path]
pattern -> hidden

and a tag is either "public" or "private". A pattern is (in terms of grammar):

atomic_pattern := name | name DOT atomic_pattern | "(" pattern ")"
pattern := | [atomic_pattern] "|" pattern

The pattern is executed by the longest-prefix matching.

[favonia]

This design based on transformers on individual names is misguided. It seems better to define transformers on the entire trees so that we could detect useless imports, etc. For example, importing an non-existing item should be an error, but in this design such an error could not be detected.