Asm optimization - Githubissues

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq

MIT License

199 stars 50 forks source link

Closed Zdancewic closed 5 years ago

Zdancewic commented 5 years ago

With this commit, there are only a few minor admits left in the AsmOptimization branch.

tutorial/Label.v has an admitted lemma
we should add some parameterized typeclass instances for Reflexive, Transitive, Symmetric, and Equivalence relations (see AsmOptimization.v)
the file theories/Events/MapDefaultFacts.v has two missing lemmas that should follow straightforwardly from ext-lib

I think that we should merges this and then prepare to release a new version of ITrees on opam.

bollu commented 5 years ago

From what I understand, this pas models general peephole-style optimisations, correct?

Lysxia commented 5 years ago

That is indeed the case.

Zdancewic commented 5 years ago

I just fixed the Label finite set isomorphism. Gil is working on generalizing the eutt stuff to account for the parameterized typeclasses.