Add support for arbitrary input for prompts

[danmatichuk]

Currently the only input that the verifier supports is choosing from a list of options. This has a number of drawbacks that are already apparent (i.e. when selecting addresses for sync/desync points), and would make it difficult to provide the necessary input for providing additional constraints to counter-examples.

As an interim solution pending a better protocol between the front and backend, we can simply add a command to the TTY that takes a string as input and is parsed in the context of the current prompt. The most straightforward solution is to have these always parsed as JSON objects into some simple AST datatype that is then interpreted by the prompt.

[jim-carciofini]

This sounds like a good interim solution.

[danmatichuk]

WIP: #423

[lcasburn]

From @danmatichuk:

• Done: Initial implementation of core functions for trace tree datatype holding structured logging & menu options
• Next steps
  • Test API is sensible by adapting one of the existing menus to accept text input that exercises end-to-end capability. For example, change menu where you define an address for sync/desync point so that users can manually type addresses.
  • Update script interface to support this feature, allowing regression suite updates

[lcasburn]

From @danmatichuk

• Done: Implemented menu for selecting the sync/desync to accept address string
• Today: Add command in repl to use the new input mechanism
• Next: Update script interface to support this feature, allowing regression suite updates

[danmatichuk]

I've now updated the scripting backend to be agnostic of whether or not a given input element is a menu selection or parsed input. e.g. a script step > foo will both provide "foo" as input or select a choice matching the text "foo" from a list of options, which is just determined contextually. At the cost of some ambiguity, this makes it easier to update the existing menus without needing to do any updates to the test scripts.

This is mostly working, except for some strange differences in behavior when running the verifier through pate.sh vs. cabal test. My current hypothesis is that this is some kind of race condition/data contention issue, since the input is provided asynchronously to the verifier.