[Agda] Hoogle for Agda?
Liam O'Connor
liamoc at cse.unsw.edu.au
Fri Feb 16 01:00:25 CET 2018
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 (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 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
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180216/58066906/attachment-0001.html>
More information about the Agda
mailing list