4ever2
commented
2 months ago @mattam82 could you please elaborate a bit on what these changes to the valid masks are?
This PR breaks all our extraction examples in https://github.com/AU-COBRA/coq-elm-extraction and https://github.com/AU-COBRA/coq-rust-extraction when both the do_trim_ctor_masks and check_valid_masks flags are set to true in dearg_transform.
Those examples worked before and it is not clear to me if it is a bug or that is the expected behaviour after this PR.
spitters
This finally updates the typed extraction correctness proof, including the dearging optimization, allowing it to use efficent environment representations. We additionally prove that it preserves wellformedness and fixpoint eta-expansion, so it can be integrated in all existing pipelines. We generalize a bit the correctness theorem so that we have a simulation for all terms (it used to be restricted to constants that evaluate to constructors). This mainly required adding a bit more of invariants on valid masks in the environment. The transformation is partial in the sense that if the environment analysis does not produce valid masks for dearging, we will just use the identity transformation, to fit in the total erasure pipelines we have for now. The new commands "MetaCoq (Bypass) Typed Erase" run the extracted verified extraction in OCaml.