Big list of wants: better (meta)programming facilities

[plt-amy]

Just a really big list of requests for an eventual refactoring of the "bootstrap" code (some parts of 1Lab, some parts of Data).

• Proper separation between the data structures and their properties for:
  • List
  • Bool
  • Fin
• Rescue Vec out from under the Reflection module
• Separate reflection primitives and reflection helpers
• Developer documentation in all the reflection modules
• Idiom-syntax, Do-syntax, Alt-syntax for Maybe
• Move <$> from Idiom-syntax to (e.g.) Map-syntax
• Proper fixities for _>>=, _=<<_
• Map-syntax instance for Arg
• Missing "generic" combinators:
  • Idiom-syntax: <*, *>
  • <$
  • Traverse-syntax (traverse, sequence)
  • Fold-syntax (nondet, choice/asum/msum)
• Combinator to abstract away instance search
• Generic term traversals?
• More convenient List ErrorPart combinators?
  • Wrap TC in a reader-style monad to carry around the logging prefix for the current tactic?

[plt-amy]

• Syntax for small lists (must ponder: also for small vectors)
• Range syntax for lists of naturals
• Maybe have Dec-eq/Dec-ord classes???