[Agda] Hoogle for Agda?
Philip Wadler
wadler at inf.ed.ac.uk
Thu Feb 15 20:25:07 CET 2018
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/
On 15 February 2018 at 17:07, Philip Wadler <wadler at 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 <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/f3967662/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/f3967662/attachment-0001.ksh>
More information about the Agda
mailing list