[Agda] Hoogle for Agda?

[Philip Wadler]

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 <liamoc at 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 (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 listAgda at lists.chalmers.sehttps://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/20180215/8583fcb2/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180215/8583fcb2/attachment-0001.ksh>