Currently, the only non-singleton data structure for which literal constants can be provided is the
list type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data structures. So it would be worth having an input syntax for expressing literals for such structures and propagating these constants as far as possible in the system. A few questions to answer:
- What is the syntax? The OCaml syntax
[| ... ; ... |]might be fine.
- What is the type of such a literal? Should it have a fixed type (e.g.
seq 'a)? Or should its type depend on the context so that one can use this syntax to input program arrays?
- How should it be translated to provers that do not support such literals? Using
epsilon s. length s = ... /\ s = ... /\ ...might be both effective and cheap implementation-wise.