Move agda2hs.agda-lib into lib directory and rename to base.agda-lib

.github/workflows/ci.yml

@@ -8,7 +8,7 @@ on:
       - 'lib/**'
       - 'src/**'
       - 'test/**'
-      - 'agda2hs.agda-lib'
+      - 'lib/base/base.agda-lib'
       - 'agda2hs.cabal'
       - 'cabal.project'
       - 'Makefile'

.github/workflows/nix-ci.yml

@@ -8,7 +8,7 @@ on:
       - 'lib/**'
       - 'src/**'
       - 'test/**'
-      - 'agda2hs.agda-lib'
+      - 'lib/base/base.agda-lib'
       - 'agda2hs.cabal'
       - 'cabal.project'
       - 'Makefile'
@@ -24,12 +24,12 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        derivation: [agda2hs, agda2hs-lib]
+        derivation: [agda2hs, base-lib]
         include:
           - pretty: "Compile agda2hs"
             derivation: agda2hs
           - pretty: "Typecheck with Agda"
-            derivation: agda2hs-lib
+            derivation: base-lib
     steps:
     - uses: actions/checkout@v3
     - uses: cachix/install-nix-action@v22

Makefile

@@ -11,7 +11,7 @@ repl :
 	cabal repl # e.g. `:set args -itest -otest/build test/AllTests.agda ... main ... :r ... main`
 
 libHtml :
-	cabal run agda2hs -- --html lib/Haskell/Prelude.agda
+	cabal run agda2hs -- --html --include-path lib/base lib/base/Haskell/Prelude.agda
 	cp html/Haskell.Prelude.html html/index.html
 
 test/agda2hs : $(FILES)

agda2hs.cabal

@@ -18,8 +18,9 @@ description:
 extra-doc-files:    CHANGELOG.md
                     README.md
 
-data-files: agda2hs.agda-lib
-            lib/**/*.agda
+data-files:
+    lib/base/base.agda-lib
+    lib/base/**/*.agda
 
 source-repository head
   type:     git

docs/source/introduction.md

@@ -9,9 +9,9 @@
 - [Agda programming language](https://github.com/agda/agda)
   - version >= 2.6.4 && < 2.6.5
 - [Agda standard library](https://github.com/agda/agda-stdlib)
-- Agda library `agda2hs`
+- Agda library `base`
   - this Agda library is included in the `agda2hs` repository; see
-    [`agda2hs.agda-lib`](https://github.com/agda/agda2hs/blob/master/agda2hs.agda-lib)
+    [`base.agda-lib`](https://github.com/agda/agda2hs/blob/master/lib/base/base.agda-lib)
   - 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/)
 
@@ -31,10 +31,10 @@ can be registered in the Agda config using the `agda2hs locate` command:
 agda2hs locate >> ~/.agda/libraries
 ```
 
-Optionally, the agda2hs prelude can also be added as a default global import:
+Optionally, the `base.agda-lib` library can also be added as a default global import:
 
 ```sh
-echo agda2hs >> ~/.agda/defaults
+echo base >> ~/.agda/defaults
 ```
 
 ### Manual installation
@@ -48,10 +48,10 @@ git clone [email protected]:agda/agda2hs.git
 cd agda2hs
 cabal install
 
-# register the agda2hs Agda library
-echo $(pwd)/agda2hs.agda-lib >> ~/.agda/libraries
-# register the agda2hs Agda library as a default
-echo agda2hs >> ~/.agda/defaults
+# register the base Agda library
+echo $(pwd)/lib/base/base.agda-lib >> ~/.agda/libraries
+# register the base Agda library as a default
+echo base >> ~/.agda/defaults
 ```
 
 ### Running `agda2hs`

lib/base/base.agda-lib

@@ -0,0 +1,8 @@
+-- This library
+-- * mirrors the Haskell `base` package
+-- * is intertwined with `agda2hs`
+
+name: base
+depend:
+include: .
+flags: -W noUnsupportedIndexedMatch --erasure

nix/default.nix

@@ -5,19 +5,19 @@
 let
   lib = import ./lib.nix { inherit pkgs; };
   version = "1.3";
-  agdalib = pkgs.agdaPackages.mkDerivation {
-    pname = "agda2hs";
+  base-lib = pkgs.agdaPackages.mkDerivation {
+    pname = "base";
     meta = { };
     version = version;
     preBuild = ''
       echo "{-# OPTIONS --sized-types #-}" > Everything.agda
       echo "module Everything where" >> Everything.agda
-      find lib -name '*.agda' | sed -e 's/lib\///;s/\//./g;s/\.agda$//;s/^/import /' >> Everything.agda
+      find . -name '*.agda' ! -name 'Everything.agda' | sed -e 's/.\///;s/\//./g;s/\.agda$//;s/^/import /' >> Everything.agda
     '';
-    src = ../.;
+    src = ../lib/base;
   };
 in
 {
   inherit (lib) agda2hs;
-  agda2hs-lib = agdalib;
+  base-lib = base-lib;
 }

test/agda2hs-test.agda-lib

@@ -1,4 +1,4 @@
 name: agda2hs-test
 depend:
-include: . ../lib
+include: . ../lib/base/
 flags: --sized-types --erasure