Redesign property generation & testing

[byorgey]

e.g. currently desugaring happens for every single test! There should be a desugaring pass that happens before tests are run. Desugaring can also include translating special properties into universally quantified ones for randomized testing (but keeping the special names around for printing results).

The way we are returning results from testing is also silly, we should cleanly separate the results from printing messages.

[byorgey]

This should happen as part of the Prop extension (#217). Properties will no longer be a separate syntactic category, but just terms of type Prop.

[byorgey]

Well, it didn't happen (at least not completely) as part of #217 . The next step is to just look through the code and make a plan for how to clean things up.

[byorgey]

Here is the current organization of code related to properties:

• Disco.Property has some utility functions for generating samples and inverting results.
• Disco.Value has code for pretty-printing test results (prettyTestResult, etc.). Those functions need to call Disco.Value.prettyValue, but otherwise there doesn't seem to be any particular reason for them to be there. They should probably move to their own module which imports Disco.Value. In fact, Disco.Property already imports Disco.Value.
• Disco.Interpret.CESK defines ensureProp, testProperty, runTest, + a few other related utility functions. They call CESK stuff (e.g. runTest calls eval which calls runCESK) and in turn CESK evaluation of e.g. holds will call testProperty.
• Disco.Interactive.Commands defines runAllTests, which currently returns Sem r Bool; want to change it to return a summary of results instead of a Bool. Also has handleTest which calls runTest.
  • Both the above mentioned use specific numbers of examples (50 and 100) which we ought to make configurable somehow.

Edit: this has likely changed since I wrote that comment. First task would be to just get a survey of how the code is currently organized.