[ fix #370 ] add locate command, data-files in cabal config

CHANGELOG.md

@@ -13,6 +13,7 @@ Changes to agda2hs:
 - Non-erased implicit arguments and instance arguments are now compiled to regular arguments in Haskell
 - Non-erased module parameters are now compiled to regular arguments in Haskell
 - Rank-N Haskell types are now supported
+- Added `agda2hs locate` command printing the path to the agda2hs prelude `.agda-lib` file
 
 Additions to the agda2hs Prelude:
 - New module `Haskell.Extra.Dec` for working with decidability proofs (compiled to `Bool`)

agda2hs.cabal

@@ -1,4 +1,4 @@
-cabal-version:       2.2
+cabal-version:       2.4
 name:                agda2hs
 version:             1.3
 license:             BSD-3-Clause
@@ -18,6 +18,9 @@ description:
 extra-doc-files:    CHANGELOG.md
                     README.md
 
+data-files: agda2hs.agda-lib
+            lib/**/*.agda
+
 source-repository head
   type:     git
   location: https://github.com/agda/agda2hs.git

docs/source/introduction.md

@@ -15,7 +15,29 @@
   - you can navigate the library in [HTML format](https://agda.github.io/agda2hs/lib/),
     along with a comprehensive [test suite](https://agda.github.io/agda2hs/test/)
 
-### Installation
+### Installation with Cabal
+
+agda2hs is released [on Hackage](https://hackage.haskell.org/package/agda2hs),
+and can be installed with Cabal:
+
+```sh
+cabal install agda2hs
+```
+
+Once installed, the agda2hs prelude bundled with agda2hs
+can be registered in the Agda config using the `agda2hs locate` command:
+
+```sh
+agda2hs locate >> ~/.agda/libaries
+```
+
+Optionally, the agda2hs prelude can also be added as a default global import:
+
+```sh
+echo agda2hs >> ~/.agda/defaults
+```
+
+### Manual installation
 
 Let `DIR` be the directory in which you start running these shell commands.
 ```sh

src/Main.hs

@@ -21,7 +21,7 @@ import Agda2Hs.Config ( checkConfig )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Render
 
-import Paths_agda2hs ( version )
+import Paths_agda2hs ( version, getDataFileName )
 
 
 -- | Agda2Hs default config
@@ -87,8 +87,15 @@ isInteractive = do
   return $ not $ null i
 
 main = do
-  -- Issue #201: disable backend when run in interactive mode
-  isInt <- isInteractive
-  if isInt
-    then runAgda [Backend backend{isEnabled = const False}]
-    else runAgda [Backend backend]
+  args <- getArgs
+
+  -- Issue #370: `agda2hs locate` will print out the path to the prelude agda-lib file
+  if args == ["locate"] then
+    putStrLn =<< getDataFileName "agda2hs.agda-lib"
+  else do
+    -- Issue #201: disable backend when run in interactive mode
+    isInt <- isInteractive
+
+    if isInt
+      then runAgda [Backend backend{isEnabled = const False}]
+      else runAgda [Backend backend]