Discussion:
Hoogle for Agda?
(too old to reply)
Philip Wadler
2018-02-15 15:52:09 UTC
Permalink
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/
Guillaume Allais
2018-02-15 16:01:51 UTC
Permalink
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
Post by Philip Wadler
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
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-02-15 16:18:08 UTC
Permalink
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 <
Post by 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
- 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
===========================================
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
===========================================
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
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
https://lists.chalmers.se/mailman/listinfo/agda
Liam O'Connor
2018-02-15 16:23:59 UTC
Permalink
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 (***@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 <***@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
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda


_______________________________________________
Agda mailing list
***@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
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-02-15 19:07:22 UTC
Permalink
Thank you! Everything sounds like everything I need!

I got the standard library from here:

git clone https://github.com/agda/agda-stdlib.git ~/agda-stdlib

This version does not have a file called Everything. It has no Makefile
that I can spot. It does contain a file called GenerateEverything.hs, but
it doesn't work for me:

bruichladdich$ ghci GenerateEverything.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( GenerateEverything.hs, interpreted )
Could not find module ‘System.FilePath.Find’
Perhaps you meant
System.FilePath.Windows (from filepath-1.4.1.2)
System.FilePath (from filepath-1.4.1.2)
System.FilePath.Posix (from filepath-1.4.1.2)
Use -v to see a list of the files searched for.
|
9 | import System.FilePath.Find
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
What are my other options? Could someone simply add Everything.agda to
https://github.com/agda/agda-stdlib.git, and then I could pull it?

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 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
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 <
Post by 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
- 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
===========================================
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
===========================================
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
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
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
https://lists.chalmers.se/mailman/listinfo/agda
Philip Wadler
2018-02-15 19:25:07 UTC
Permalink
OK, I've made it work. I used copy and paste from

http://www.cse.chalmers.se/~nad/listings/lib/Everything.html

and then changed all occurrences of "import" to "open import", and then
using ^C ^Z does indeed work. It produces a large and difficult to read
listing (because it finds many entries with huge types), but is much better
than what I had previously (which was to guess where to look).

Thank you to all for your help. If someone did produce Hoogle for Agda, it
would be a huge boon. 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/
Post by Philip Wadler
Thank you! Everything sounds like everything I need!
git clone https://github.com/agda/agda-stdlib.git ~/agda-stdlib
This version does not have a file called Everything. It has no Makefile
that I can spot. It does contain a file called GenerateEverything.hs, but
bruichladdich$ ghci GenerateEverything.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( GenerateEverything.hs, interpreted )
Could not find module ‘System.FilePath.Find’
Perhaps you meant
System.FilePath.Windows (from filepath-1.4.1.2)
System.FilePath (from filepath-1.4.1.2)
System.FilePath.Posix (from filepath-1.4.1.2)
Use -v to see a list of the files searched for.
|
9 | import System.FilePath.Find
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
What are my other options? Could someone simply add Everything.agda to
https://github.com/agda/agda-stdlib.git, and then I could pull it?
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 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
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 <
Post by 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
- 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
===========================================
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
===========================================
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
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
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
https://lists.chalmers.se/mailman/listinfo/agda
Liam O'Connor
2018-02-16 00:00:25 UTC
Permalink
Hi Phil,

Sorry, the Makefile is called GNUmakefile. it’s here, for future reference:

https://github.com/agda/agda-stdlib/blob/master/GNUmakefile

I think, if you have GNU make, “make Everything.agda” should work.

L
On 16 February 2018 at 6:08:18 am, Philip Wadler (***@inf.ed.ac.uk) wrote:

Thank you! Everything sounds like everything I need!

I got the standard library from here:

  git clone https://github.com/agda/agda-stdlib.git ~/agda-stdlib

This version does not have a file called Everything. It has no Makefile that I can spot. It does contain a file called GenerateEverything.hs, but it doesn't work for me:

bruichladdich$ ghci GenerateEverything.hs 
GHCi, version 8.2.2: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( GenerateEverything.hs, interpreted )
GenerateEverything.hs:9:1: error:
    Could not find module ‘System.FilePath.Find’
    Perhaps you meant
      System.FilePath.Windows (from filepath-1.4.1.2)
      System.FilePath (from filepath-1.4.1.2)
      System.FilePath.Posix (from filepath-1.4.1.2)
    Use -v to see a list of the files searched for.
  |
9 | import System.FilePath.Find
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude> 

What are my other options? Could someone simply add Everything.agda to https://github.com/agda/agda-stdlib.git, and then I could pull it?

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:23, Liam O'Connor <***@cse.unsw.edu.au> wrote:

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 (***@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 <***@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
***@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda


_______________________________________________
Agda mailing list
***@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
***@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.
Philip Wadler
2018-02-16 13:06:27 UTC
Permalink
Thanks!

There is a long run, ending with:

cabal exec -- GenerateEverything
cabal: The program 'GenerateEverything' is required but it could not be
found.
make: *** [Everything.agda] Error 1
bruichladdich$ ls
AllNonAsciiChars.hs Setup.hs
CHANGELOG.md dist
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
README.md
bruichladdich$

Which is mysterious, since as you can see, GenerateEverything.hs is
present. Complete run below, in case you want details. Fortunately, I have
a version copied from the html page cited earlier, which works well enough
for now. An easy way to fix the problem for the future is to check
Everything.agda into the repository, rather than leaving each user to
generate it for theirself. Cheers, -- P


bruichladdich$ cd ~/agda-stdlib/
bruichladdich$ ls
AllNonAsciiChars.hs README.md
CHANGELOG.md Setup.hs
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
bruichladdich$ git pull
remote: Counting objects: 17, done.
remote: Compressing objects: 100% (3/3), done.
remote: Total 17 (delta 13), reused 17 (delta 13), pack-reused 0
Unpacking objects: 100% (17/17), done.
From https://github.com/agda/agda-stdlib
a68ee7e0..157497a5 master -> origin/master
81b74c8a..d8ae867e gh-pages -> origin/gh-pages
Updating a68ee7e0..157497a5
Fast-forward
CHANGELOG.md | 25 ++++++++++++-------------
src/Data/Table.agda | 6 +++---
src/Data/Table/Base.agda | 10 +++++-----
src/Data/Table/Properties.agda | 31 ++++++++++++++++---------------
src/Data/Table/Relation/Equality.agda | 4 ++--
5 files changed, 38 insertions(+), 38 deletions(-)
bruichladdich$ ls
AllNonAsciiChars.hs README.md
CHANGELOG.md Setup.hs
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
bruichladdich$ make Everything.agda
cabal clean && cabal install
cleaning...
Warning: --root-cmd is no longer supported, see
https://github.com/haskell/cabal/issues/3353 (if you didn't type --root-cmd,
comment out root-cmd in your ~/.cabal/config file)
Warning: The package list for 'hackage.haskell.org' is 63 days old.
Run 'cabal update' to get the latest list of available packages.
Resolving dependencies...
Downloading unix-compat-0.5.0.1...
Configuring unix-compat-0.5.0.1...
Preprocessing library for unix-compat-0.5.0.1..
Building library for unix-compat-0.5.0.1..
[1 of 8] Compiling System.PosixCompat.Files (
dist/build/System/PosixCompat/Files.hs,
dist/build/System/PosixCompat/Files.o )
[2 of 8] Compiling System.PosixCompat.Temp (
src/System/PosixCompat/Temp.hs, dist/build/System/PosixCompat/Temp.o )
[3 of 8] Compiling System.PosixCompat.Time (
src/System/PosixCompat/Time.hs, dist/build/System/PosixCompat/Time.o )
[4 of 8] Compiling System.PosixCompat.Types (
src/System/PosixCompat/Types.hs, dist/build/System/PosixCompat/Types.o )
[5 of 8] Compiling System.PosixCompat.Extensions (
dist/build/System/PosixCompat/Extensions.hs,
dist/build/System/PosixCompat/Extensions.o )
[6 of 8] Compiling System.PosixCompat.Unistd (
src/System/PosixCompat/Unistd.hs, dist/build/System/PosixCompat/Unistd.o )
[7 of 8] Compiling System.PosixCompat.User (
dist/build/System/PosixCompat/User.hs, dist/build/System/PosixCompat/User.o
)
[8 of 8] Compiling System.PosixCompat ( src/System/PosixCompat.hs,
dist/build/System/PosixCompat.o )
[1 of 8] Compiling System.PosixCompat.Files (
dist/build/System/PosixCompat/Files.hs,
dist/build/System/PosixCompat/Files.p_o )
[2 of 8] Compiling System.PosixCompat.Temp (
src/System/PosixCompat/Temp.hs, dist/build/System/PosixCompat/Temp.p_o )
[3 of 8] Compiling System.PosixCompat.Time (
src/System/PosixCompat/Time.hs, dist/build/System/PosixCompat/Time.p_o )
[4 of 8] Compiling System.PosixCompat.Types (
src/System/PosixCompat/Types.hs, dist/build/System/PosixCompat/Types.p_o )
[5 of 8] Compiling System.PosixCompat.Extensions (
dist/build/System/PosixCompat/Extensions.hs,
dist/build/System/PosixCompat/Extensions.p_o )
[6 of 8] Compiling System.PosixCompat.Unistd (
src/System/PosixCompat/Unistd.hs, dist/build/System/PosixCompat/Unistd.p_o )
[7 of 8] Compiling System.PosixCompat.User (
dist/build/System/PosixCompat/User.hs,
dist/build/System/PosixCompat/User.p_o )
[8 of 8] Compiling System.PosixCompat ( src/System/PosixCompat.hs,
dist/build/System/PosixCompat.p_o )
Preprocessing library for unix-compat-0.5.0.1..
Running Haddock on library for unix-compat-0.5.0.1..
Haddock coverage:
99% ( 77 / 78) in 'System.PosixCompat.Files'
Missing documentation for:
PathVar
100% ( 2 / 2) in 'System.PosixCompat.Temp'
100% ( 2 / 2) in 'System.PosixCompat.Time'
100% ( 2 / 2) in 'System.PosixCompat.Types'
71% ( 5 / 7) in 'System.PosixCompat.Extensions'
Missing documentation for:
CMajor (src/System/PosixCompat/Extensions.hsc:23)
CMinor (src/System/PosixCompat/Extensions.hsc:24)
75% ( 6 / 8) in 'System.PosixCompat.Unistd'
Missing documentation for:
SystemID
getSystemID
91% ( 21 / 23) in 'System.PosixCompat.User'
Missing documentation for:
GroupEntry
UserEntry
100% ( 8 / 8) in 'System.PosixCompat'
Documentation created: dist/doc/html/unix-compat/index.html
Installing library in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/unix-compat-0.5.0.1/lib
Installed unix-compat-0.5.0.1
Downloading filemanip-0.3.6.3...
Configuring filemanip-0.3.6.3...
Preprocessing library for filemanip-0.3.6.3..
Building library for filemanip-0.3.6.3..
[1 of 4] Compiling System.FilePath.GlobPattern (
System/FilePath/GlobPattern.hs, dist/build/System/FilePath/GlobPattern.o )

System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]
This binding for ‘g’ shadows the existing binding
bound at System/FilePath/GlobPattern.hs:148:24
|
149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs
| ^
[2 of 4] Compiling System.FilePath.Glob ( System/FilePath/Glob.hs,
dist/build/System/FilePath/Glob.o )
[3 of 4] Compiling System.FilePath.Find ( System/FilePath/Find.hs,
dist/build/System/FilePath/Find.o )

System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
227 | where visit path depth st =
| ^^^^^

System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
231 | traverse dir depth dirSt = do
| ^^^^^^^^

System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
231 | traverse dir depth dirSt = do
| ^^^^^

System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
238 | filterPath path depth st result =
| ^^^^^

System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
274 | where visit state path depth st =
| ^^^^^

System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
274 | where visit state path depth st =
| ^^^^

System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
274 | where visit state path depth st =
| ^^^^^

System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^^^^

System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^

System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^

System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:279:18
|
282 | in state' `seq` flip foldM state' (\state name ->
| ^^^^^

System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
284 | let path = dir </> name
| ^^^^
[4 of 4] Compiling System.FilePath.Manip ( System/FilePath/Manip.hs,
dist/build/System/FilePath/Manip.o )
[1 of 4] Compiling System.FilePath.GlobPattern (
System/FilePath/GlobPattern.hs, dist/build/System/FilePath/GlobPattern.p_o )

System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]
This binding for ‘g’ shadows the existing binding
bound at System/FilePath/GlobPattern.hs:148:24
|
149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs
| ^
[2 of 4] Compiling System.FilePath.Glob ( System/FilePath/Glob.hs,
dist/build/System/FilePath/Glob.p_o )
[3 of 4] Compiling System.FilePath.Find ( System/FilePath/Find.hs,
dist/build/System/FilePath/Find.p_o )

System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
227 | where visit path depth st =
| ^^^^^

System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
231 | traverse dir depth dirSt = do
| ^^^^^^^^

System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
231 | traverse dir depth dirSt = do
| ^^^^^

System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
238 | filterPath path depth st result =
| ^^^^^

System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
274 | where visit state path depth st =
| ^^^^^

System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
274 | where visit state path depth st =
| ^^^^

System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
274 | where visit state path depth st =
| ^^^^^

System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^^^^

System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^

System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^

System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:279:18
|
282 | in state' `seq` flip foldM state' (\state name ->
| ^^^^^

System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
284 | let path = dir </> name
| ^^^^
[4 of 4] Compiling System.FilePath.Manip ( System/FilePath/Manip.hs,
dist/build/System/FilePath/Manip.p_o )
Preprocessing library for filemanip-0.3.6.3..
Running Haddock on library for filemanip-0.3.6.3..
Haddock coverage:

System/FilePath/GlobPattern.hs:149:22: warning: [-Wname-shadowing]
This binding for ‘g’ shadows the existing binding
bound at System/FilePath/GlobPattern.hs:148:24
|
149 | where matchGroup g = matchTerms (MatchLiteral g : ts) cs
| ^
100% ( 7 / 7) in 'System.FilePath.GlobPattern'
100% ( 2 / 2) in 'System.FilePath.Glob'

System/FilePath/Find.hs:227:20: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
227 | where visit path depth st =
| ^^^^^

System/FilePath/Find.hs:231:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
231 | traverse dir depth dirSt = do
| ^^^^^^^^

System/FilePath/Find.hs:231:22: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
231 | traverse dir depth dirSt = do
| ^^^^^

System/FilePath/Find.hs:238:25: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
238 | filterPath path depth st result =
| ^^^^^

System/FilePath/Find.hs:274:15: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
274 | where visit state path depth st =
| ^^^^^

System/FilePath/Find.hs:274:21: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
274 | where visit state path depth st =
| ^^^^

System/FilePath/Find.hs:274:26: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
274 | where visit state path depth st =
| ^^^^^

System/FilePath/Find.hs:279:9: warning: [-Wname-shadowing]
This binding for ‘traverse’ shadows the existing binding
imported from ‘Prelude’ at System/FilePath/Find.hs:39:8-27
(and originally defined in ‘Data.Traversable’)
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^^^^

System/FilePath/Find.hs:279:18: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:271:38
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^

System/FilePath/Find.hs:279:28: warning: [-Wname-shadowing]
This binding for ‘depth’ shadows the existing binding
defined at System/FilePath/Find.hs:195:1
|
279 | traverse state dir depth dirSt = handle (errHandler dir
state) $
| ^^^^^

System/FilePath/Find.hs:282:53: warning: [-Wname-shadowing]
This binding for ‘state’ shadows the existing binding
bound at System/FilePath/Find.hs:279:18
|
282 | in state' `seq` flip foldM state' (\state name ->
| ^^^^^

System/FilePath/Find.hs:284:25: warning: [-Wname-shadowing]
This binding for ‘path’ shadows the existing binding
bound at System/FilePath/Find.hs:271:44
|
284 | let path = dir </> name
| ^^^^
65% ( 41 / 63) in 'System.FilePath.Find'
Missing documentation for:
FileType (System/FilePath/Find.hs:394)
FilterPredicate (System/FilePath/Find.hs:202)
RecursionPredicate (System/FilePath/Find.hs:203)
deviceID (System/FilePath/Find.hs:439)
fileID (System/FilePath/Find.hs:442)
fileOwner (System/FilePath/Find.hs:445)
fileGroup (System/FilePath/Find.hs:448)
fileSize (System/FilePath/Find.hs:451)
linkCount (System/FilePath/Find.hs:454)
specialDeviceID (System/FilePath/Find.hs:457)
fileMode (System/FilePath/Find.hs:460)
accessTime (System/FilePath/Find.hs:478)
modificationTime (System/FilePath/Find.hs:481)
statusChangeTime (System/FilePath/Find.hs:484)
==? (System/FilePath/Find.hs:527)
/=? (System/FilePath/Find.hs:531)
? (System/FilePath/Find.hs:535)
<? (System/FilePath/Find.hs:539)
=? (System/FilePath/Find.hs:543)
<=? (System/FilePath/Find.hs:547)
&&? (System/FilePath/Find.hs:557)
||? (System/FilePath/Find.hs:561)
100% ( 6 / 6) in 'System.FilePath.Manip'
Documentation created: dist/doc/html/filemanip/index.html
Installing library in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/filemanip-0.3.6.3/lib
Installed filemanip-0.3.6.3
Configuring lib-0.14...
Preprocessing executable 'GenerateEverything' for lib-0.14..
Building executable 'GenerateEverything' for lib-0.14..
[1 of 1] Compiling Main ( GenerateEverything.hs,
dist/build/GenerateEverything/GenerateEverything-tmp/Main.o )
Linking dist/build/GenerateEverything/GenerateEverything ...
Preprocessing executable 'AllNonAsciiChars' for lib-0.14..
Building executable 'AllNonAsciiChars' for lib-0.14..
[1 of 1] Compiling Main ( AllNonAsciiChars.hs,
dist/build/AllNonAsciiChars/AllNonAsciiChars-tmp/Main.o )
Linking dist/build/AllNonAsciiChars/AllNonAsciiChars ...
Warning: No documentation was generated as this package does not contain a
library. Perhaps you want to use the --executables, --tests, --benchmarks or
--foreign-libraries flags.
Installing executable GenerateEverything in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin
Warning: The directory
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin is not in the
system
search path.
Installing executable AllNonAsciiChars in
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin
Warning: The directory
/Users/wadler/Library/Haskell/ghc-8.2.2/lib/lib-0.14/bin is not in the
system
search path.
Installed lib-0.14
Updating documentation index /Users/wadler/Library/Haskell/doc/index.html
cabal exec -- GenerateEverything
cabal: The program 'GenerateEverything' is required but it could not be
found.
make: *** [Everything.agda] Error 1
bruichladdich$ ls
AllNonAsciiChars.hs Setup.hs
CHANGELOG.md dist
GNUmakefile index.agda
GenerateEverything.hs index.sh
HACKING.md lib.cabal
Header notes
LICENCE publish-listings.sh
README src
README.agda standard-library.agda-lib
README.md
bruichladdich$

. \ 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/
Hi Phil,
https://github.com/agda/agda-stdlib/blob/master/GNUmakefile
I think, if you have GNU make, “make Everything.agda” should work.
L
Thank you! Everything sounds like everything I need!
git clone https://github.com/agda/agda-stdlib.git ~/agda-stdlib
This version does not have a file called Everything. It has no Makefile
that I can spot. It does contain a file called GenerateEverything.hs, but
bruichladdich$ ghci GenerateEverything.hs
GHCi, version 8.2.2: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( GenerateEverything.hs, interpreted )
Could not find module ‘System.FilePath.Find’
Perhaps you meant
System.FilePath.Windows (from filepath-1.4.1.2)
System.FilePath (from filepath-1.4.1.2)
System.FilePath.Posix (from filepath-1.4.1.2)
Use -v to see a list of the files searched for.
|
9 | import System.FilePath.Find
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude>
What are my other options? Could someone simply add Everything.agda to
https://github.com/agda/agda-stdlib.git, and then I could pull it?
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 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
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 <
Post by 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
- 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
===========================================
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
===========================================
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
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
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
https://lists.chalmers.se/mailman/listinfo/agda
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
Andrés Sicard-Ramírez
2018-02-16 13:36:13 UTC
Permalink
Post by Philip Wadler
cabal exec -- GenerateEverything
cabal: The program 'GenerateEverything' is required but it could not be
Download the version of the standard library supported by your version
of Agda from

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary


Then (I downloaded version 0.14 supported by Agda 2.5.3) the following commands

$ tar xvf agda-stdlib-0.14.tar.gz
$ cd agda-stdlib-0.14
$ make Everything.agda

generate the `Everything.agda` file.

--
Andrés
La información contenida en este correo electrónico está dirigida únicamente a su destinatario y puede contener información confidencial, material privilegiado o información protegida por derecho de autor. Está prohibida cualquier copia, utilización, indebida retención, modificación, difusión, distribución o reproducción total o parcial. Si usted recibe este mensaje por error, por favor contacte al remitente y elimínelo. La información aquí contenida es responsabilidad exclusiva de su remitente por lo tanto la Universidad EAFIT no se hace responsable de lo que el mensaje contenga. The information contained in this email is addressed to its recipient only and may contain confidential information, privileged material or information protected by copyright. Its prohibited any copy, use, improper retention, modification, dissemination, distribution or total or partial reproduction. If you receive this message by error, please contact the sender and delete it. The information contained herein is the sole responsibility of the sender therefore Universidad EAFIT is not responsible for what the message contains.
John Leo
2018-02-15 16:27:03 UTC
Permalink
I recall a bachelors or masters student at Chalmers was working on such a
project, but I’m not sure what became of it.

John
Post by Philip Wadler
Is there anything like Hoogle for Agda? It would save newbies like me a
*lot* of time. Cheers, -- P
--
John
Loading...