Finite map notations

This adds some ad-hoc notations for maps up to size 13, e.g. {[ k1 := a1 ; k2 := a2 ]} for (<[k2 := a2]>{[k1 := a1]}). 13 seems to be enough for many useful cases.

For future reference if notations for larger sets are needed, this is the script I used:

#!/bin/python3

n = 13
# indent by two spaces
indent = "  "


def generate(n):
  # Header
  out = "Notation \"{[ " 

  # notation itself
  for i in range(1, n+1):
    if i > 1:
      out += " ; "
    out += "k" + str(i) + " := a" + str(i)
  out += " ]}\" := \n" 

  # translation of notation
  line = indent + "("
  for i in range(1, n):
    if i > 1:
      line += " $ "
    if len(line) > 70:
      out += line + "\n"
      line = indent + indent 
    line += "<[ k" + str(i) + " := a" + str(i) + " ]>"
  # singleton element
  line += "{[ k" + str(n) + " := a" + str(n) + " ]}"
  line += ")\n" 
  out += line

  out += indent + "(at level 1, format\n"

  # format printing
  line = indent + "\"{[ '[hv' "
  for i in range(1, n+1):
    if i > 1:
      # extra space for printing
      line += " ; ']'  '/' "
    # if len(line) > 70:
      # out += line + "\"\n"
      # line = indent + indent + "\""
    line += "'[' k" + str(i) + "  :=  a" + str(i)
  line += " ']' ']' ]}\")"
  out += line

  out += " : stdpp_scope."
  return out

for i in range(2, n+1):
  print(generate(i))

Thanks for the MR. While this is a lot of boilerplate, I think it's very useful, and I don't know a good way to avoid it.

Some comments/questions:

• {[ k1 := a1 ; k2 := a2 ]} is defined as (<[k2 := a2]>{[k1 := a1]}) I would expect that the definition goes into the same direction as the notation, so start with k2 and insert k1 into that.
• I would write the RHSs using the $ notation for application, that saves a lot of parentheses.
• Are we sure that just level 1 is sufficient? It would be good to have some parsing and pretty printing tests.

added 2 commits

• 3c6ba319 - incorporate suggested changes
• da5eead3 - add small test that map notations can be parsed

Compare with previous version

added 1 commit

• f6ff930c - operators in notation tests

Compare with previous version

added 1 commit

• 9f798640 - format notation; printing tests

Compare with previous version

added 1 commit

• 2d6ae3d0 - better imports in notation test

Compare with previous version

This MR is ready as far as I am concerned. I leave it to @jung to check if the setup of the tests is correct.

added 1 commit

• b499714c - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

added 2 commits

• 65fbdb40 - change printing to horizontal-else-vertical
• 10636cdd - Merge branch 'map-notations' of gitlab.mpi-sws.org:lgaeher/stdpp into map-notations

Compare with previous version

changed the description

LGTM.

resolved all threads