Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/4594 below:

Improve the blocking primitive · Issue #4594 · agda/agda · GitHub

I tried to figure out why one of my tactics is slow. Here is an example run for one call to the tactic:

• The tactic is given the following term (well, this term is part of what you get if you reduce the goal type):

  Monad.Raw-monad._⟨$⟩_ {equivalence-relation⁺} {equality-with-J}
  {lzero} {lzero} {_52 h hyp xs} (_53 h hyp xs) {ℕ} {ℕ} suc
  (_59 h hyp xs)

  The tactic blocks on meta-variable _52.
• The tactic is given the following term:

  Monad.Raw-monad._⟨$⟩_ {equivalence-relation⁺} {equality-with-J}
  {lzero} {lzero} {λ v → _78 v} (_53 h hyp xs) {ℕ} {ℕ} suc
  (_59 h hyp xs)

  The tactic blocks on meta-variable _78. Note that _52 seems to have been η-expanded to λ v → _78 v.
• The tactic is given the following term:

  Monad.Raw-monad._⟨$⟩_ {equivalence-relation⁺} {equality-with-J}
  {lzero} {lzero} {Maybe {lzero}}
  (Maybe.raw-monad {equivalence-relation⁺} equality-with-J {lzero})
  {ℕ} {ℕ} suc (_59 h hyp xs)

  The tactic blocks on meta-variable _59. Note that this meta-variable was part of the first term mentioned above.
• Finally the tactic is given a term without meta-variables, and completes successfully.

It seems wasteful for the tactic to repeatedly reduce and traverse the input in this way. Some suggestions for improvement:

• Make it possible to block on a set (list) of meta-variables. The tactic could traverse the first term and block on three meta-variables, _52, _53 and _59. The tactic should not be restarted until all of these meta-variables have been solved.
• Make it possible to block "transitively", so that the tactic does not restart until the meta-variables have been solved, any meta-variables in the solutions have been solved, and so on.
• Make it possible to block until a specific term (like the goal type) does not contain any unsolved meta-variables (transitively).

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4