[Agda] Hoogle for Agda?

[Guillaume Allais]

Hi Phil,

There's a *very basic* search functionality which you can invoke
from emacs using C-c C-z. You can then input a space-separated
list of identifiers and strings and Agda will return all the
identifiers which:
- are in scope in the current module
- contain in their type *all* of the identifiers mentioned
- contain as substring *all* of the mentioned strings

For instance, using a fairly recent version of the stdlib, from
the module containing:

===========================================
open import Data.Nat
open import Data.Nat.Properties
===========================================

C-c C-z RET _+_ _*_ RET

will return

===========================================
Definitions about _+_, _*_
  *-+-isCommutativeSemiring
          : .Algebra.Structures.IsCommutativeSemiring
            .Agda.Builtin.Equality._≡_ _+_ _*_ 0 1
  *-cancelˡ-≡
          : {i j : ℕ} (k : ℕ) →
            i + k * i .Agda.Builtin.Equality.≡ j + k * j →
            i .Agda.Builtin.Equality.≡ j
  *-distrib-+
          : (.Agda.Builtin.Equality._≡_
             .Algebra.FunctionProperties.DistributesOver _*_)
            _+_
  *-distribʳ-+
          : (.Agda.Builtin.Equality._≡_
             .Algebra.FunctionProperties.DistributesOverʳ _*_)
            _+_
  *-distribˡ-+
          : (.Agda.Builtin.Equality._≡_
             .Algebra.FunctionProperties.DistributesOverˡ _*_)
            _+_
  +-*-suc : (m n : ℕ) → m * suc n .Agda.Builtin.Equality.≡ m + m * n
  ^-distribˡ-+-*
          : (m n p : ℕ) →
            (m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)
  distribʳ-*-+
          : (.Agda.Builtin.Equality._≡_
             .Algebra.FunctionProperties.DistributesOverʳ _*_)
            _+_
  im≡jm+n⇒[i∸j]m≡n
          : (i j m n : ℕ) →
            i * m .Agda.Builtin.Equality.≡ j * m + n →
            (i ∸ j) * m .Agda.Builtin.Equality.≡ n
  isCommutativeSemiring
          : .Algebra.Structures.IsCommutativeSemiring
            .Agda.Builtin.Equality._≡_ _+_ _*_ 0 1
===========================================

and C-c C-z RET _+_ _*_ "distr" RET
will filter definitions which are not about distributivity:

===========================================
Definitions about _+_, _*_, "distr"
  *-distrib-+
   : (.Agda.Builtin.Equality._≡_
      .Algebra.FunctionProperties.DistributesOver _*_)
     _+_
  *-distribʳ-+
   : (.Agda.Builtin.Equality._≡_
      .Algebra.FunctionProperties.DistributesOverʳ _*_)
     _+_
  *-distribˡ-+
   : (.Agda.Builtin.Equality._≡_
      .Algebra.FunctionProperties.DistributesOverˡ _*_)
     _+_
  ^-distribˡ-+-*
   : (m n p : ℕ) →
     (m ^ (n + p)) .Agda.Builtin.Equality.≡ (m ^ n) * (m ^ p)
  distribʳ-*-+
   : (.Agda.Builtin.Equality._≡_
      .Algebra.FunctionProperties.DistributesOverʳ _*_)
     _+_
===========================================

This search function respect the normalisation modifiers (that
is the (C-u)* you can type before most commands) and will search
types according to the normalisation level you've requested (and
print results accordingly).

Cheers,
--
gallais


On 15/02/18 16:52, Philip Wadler wrote:
> Is there anything like Hoogle for Agda? It would save newbies like me
> a *lot* of time. Cheers, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/0e943795/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/0e943795/attachment.sig>