Cleaning up FStar/examples so that they all build cleanly into .checked files

[nikswamy]

We have been accumulating lots of code in examples, but there were two problems

• each sub directory was build separately, not necessarily producing .checked files etc.

• many directories contained examples that were old, no longer maintained etc., but these were intermingled with the other files.

This PR cleans up the the examples directory, with the following main changes:

0. I changed the behavior of fstar --dep so that if it is called with an empty list of F* files on the command line, it will scan the all the directories in the include path (without nesting) for all their F* files and then proceed to build a dependence graph over them.

1. We have a revised examples/Makefile which scans a given list of directories for all F* files, builds a dependence graph for them, and then builds all of them into examples/_cache/*.checked. There are a few special cases of examples that don't fit this pattern that are documented at the top of that Makefile.

2. I moved many examples that were no longer maintained but that could perhaps some day be restored into old/. For a few other examples that didn't meet this bar, I just removed them.

3. I moved examples/extraction to tests and examples/error-reporting/Test1.fst was folded into tests/error-messages

Some other points to note.

DM4F

The DM4F directory (with examples from Dijkstra Monads for Free) had been dropped from CI. I restored most of these examples and added them back, but there are a couple of regressions to note---we already report a deprecation warning on DM4F effect definitions, so I am just noting these points rather than trying to fix them now.

1. At one point, using reify/reflect, it used to be possible to enrich the type of an effectful function with its own reification, i.e., f : (x:t -> ST t' p q) could be turned via refine_st f into x:t -> ST t p (fun h0 x h1 -> q h0 x h1 /\ x,h1 == reify f h0). This no longer works and I had to assume refine_st to continue some of the examples.

2. Using effect templates with DM4F and .checked files leads to universe errors---so, I had to replace the instantiations of FStar.DM4F.ST.STATE_h h.

3. Projections of actions from DM4F effects across checked file boundaries fails, i.e., you cannot write STATE?.get and instead have to use an alias for it.

[nikswamy]

heads-up @gebner