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
• [x] Rescue Vec out from under the Reflection module
• [x] Separate reflection primitives and reflection helpers
• [ ] Developer documentation in all the reflection modules
• [ ] Idiom-syntax, Do-syntax, Alt-syntax for Maybe
• [x] Move <$> from Idiom-syntax to (e.g.) Map-syntax
• [x] Proper fixities for _>>=, _=<<_
• [x] 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???