[Agda] Hoogle for Agda?

[Liam O'Connor]

The agda standard library has a makefile entry for an “Everything.agda” that includes.. well… everything in the standard library.

You can build that file, and it should suit your purposes. (It has a listing here http://www.cse.chalmers.se/~nad/listings/lib/Everything.html)

Regards,
Liam

On 16 February 2018 at 3:19:04 am, Philip Wadler (wadler at inf.ed.ac.uk) wrote:

Thanks!

What would help enormously is if I could do the same thing, *searching the entire standard library*. This basically requires someone to put together a huge import list and put it in a file (preferably available with the standard library). Has anyone done so, or could this be whipped together quickly?

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/

On 15 February 2018 at 14:01, Guillaume Allais <guillaume.allais at ens-lyon.org> wrote:
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


_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda


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/20180216/285be1aa/attachment.html>