Support for limited extraction of indexed effects

[aseemr]

The PR adds limited support for extraction of indexed effects. See this wiki page for details:

https://github.com/FStarLang/FStar/wiki/Indexed-effects#reification-and-extraction

and https://github.com/FStarLang/FStar/tree/_aseem_indexed_effects_extraction/examples/layeredeffects/extraction for some examples.

[mtzguido]

Hi Aseem, I tried this out a bit. It fails for me when extracting examples/layeredeffects/LL.fst, though it's not demanded by the Makefile but maybe that's just a typo?

$ ./bin/fstar.exe examples/layeredeffects/LL.fst --codegen OCaml
Extracted module FStar.Pervasives.Native
Extracted module FStar.Monotonic.Pure
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("This should not happen (should have been handled at Tm_abs level for effect LL.EXN)")

Removing the inline_for_extraction_ qualifier on get_flt_stexnmakes it work. Looking at the code I'm confused on whether reification is triggered by areify(orreify___E`), or by the meta monadics.. is it a mix? Could it always just be the Meta_monadic nodes?

[aseemr]

Thanks for testing Guido, much appreciated!

This reify___M thing was quite ugly and the root cause of this failure. The issue is, with reify___M and reify is that we have to match on both everywhere we want to check for reify.

The reason I had added reify___M in the first place was that, in the smtencoding when we get reify e, I wanted to not encode this when e has an indexed effect. But the term itself does not have the effect of e, so reify___M as an assume val was trying to emulate it.

I have now removed this reify___M altogether, adding an option lident to reify syntax which is filled by the typechecker. And then checked in smtencoding. If this option is not set, then to be safe, we encode reify e abstractly (and in fact Bug2641.fst relies on it being abstract).

With this change, LL also works. It had a double reify, and normalizer was getting stuck.

I also added DM4F_layered5 which is also double layered. Added these two to the CI.