Instance search keeps reproving the same goals, which take time because of the way we currently compose structures, so we have to repeatedly reconstruct them.
Solution: specialize structures more, e.g., don't declare ktree notation for Kleisli itree, but make it a definition of its own. Derive the various instances with some copy-paste boilerplate.
A more long-term solution would be to implement caching in type class search. Our constraints are Haskell-like, so they're not too wild (we shouldn't have to worry about existential variables). Universe polymorphism might become a problem though. In any case, it's a lot of work.
The proof of Imp2AsmCorrectness.seq_asm_correct provides a small (enough for debugging) but still noticeably slow rewrite (0.2s) (there are probably many others earlier...).
In particular, looking at rewrite app_asm_correct line 455.
Instance search keeps reproving the same goals, which take time because of the way we currently compose structures, so we have to repeatedly reconstruct them.
Solution: specialize structures more, e.g., don't declare
ktree
notation forKleisli itree
, but make it a definition of its own. Derive the various instances with some copy-paste boilerplate.A more long-term solution would be to implement caching in type class search. Our constraints are Haskell-like, so they're not too wild (we shouldn't have to worry about existential variables). Universe polymorphism might become a problem though. In any case, it's a lot of work.
The proof of
Imp2AsmCorrectness.seq_asm_correct
provides a small (enough for debugging) but still noticeably slow rewrite (0.2s) (there are probably many others earlier...).In particular, looking at
rewrite app_asm_correct
line 455.https://github.com/DeepSpec/InteractionTrees/blob/f140f0bb9677876e95cc716e10224d27eb7ef6ce/tutorial/Imp2AsmCorrectness.v#L455
The goal looks like this:
And we're rewriting using
That spawns the ridiculous tree search summarized below, but basically, the same goals keep on reappearing.
Proper
-ness of the contextsubpure swap >>> _
, which is solved by properness ofcat
(>>>
)...This also requires reflexivity of equivalence of arrows
eq2
(to ensure here thatsubpure swap
is "proper")eq2
is anEquivalence
(...)Properness of
cat
solved bycategory_proper_cat
, requiringsub (ktree E)
is aCategory
, requiringktree E
is aCategory
, requiringitree E
is a lawful monad (MonadLaws
,EqMProps
)Proper
-ness of the context_ >>> subpure (id_ (B + C)))
, which basically spawns the same search (...)Proper
-ness ofloop
, requiringeq2
is anEquivalence
(...)sub (ktree E)
is aCategory
(...)sub (ktree E)
is anIterative
category, which in turn requireseq2
is anEquivalence
(fourth time!) (...)ktree E
is aCategory
(fourth time!) (...)ktree E
has aCoproduct
, requiring again thatitree E
is a monad, for at least the fifth time (others hidden inCategory
constraints)(Related to #83)