Apply formatting and linting

.gitignore

@@ -7,3 +7,7 @@ docs/build/
 *.hi
 *.o
 
+# For nix users
+.direnv/**
+.envrc
+result

Makefile

@@ -1,5 +1,29 @@
 .PHONY : install agda repl libHtml test testHtml golden docs
-FILES = $(shell find src -type f)
+
+
+usage:
+	@echo "usage: make <command>"
+	@echo
+	@echo "Available commands:"
+	@echo ""
+	# Code
+	@echo "    install                -- Installs agda2hs in the user's ~/.cabal/bin"
+	@echo "    agda                   -- Installs Agda itself"
+	@echo "    repl                   -- Starts a cabal repl"
+	@echo "    libHtml                -- generates HTML documentation for the agda2hs library"
+    # Formatting
+	@echo "    format                 -- Formats .hs, .cabal, .nix files"
+	@echo "    format_check           -- Check formatting of .hs, .cabal, .nix files"
+	@echo "    format_haskell         -- Formats .hs files"
+	@echo "    format_check_haskell   -- Check formatting of .hs files"
+	@echo "    format_nix             -- Formats .nix files"
+	@echo "    format_check_nix       -- Check formatting of .nix files"
+	@echo "    format_cabal           -- Formats .cabal files"
+	@echo "    format_check_cabal     -- Check formatting of .cabal files"
+	@echo "    lint                   -- Auto-refactors code"
+	@echo "    lint_check             -- Run code linting"
+	@echo ""
+	# Documentation (haskell)
 
 install :
 	cabal install --overwrite-policy=always
@@ -14,6 +38,8 @@ libHtml :
 	cabal run agda2hs -- --html lib/Haskell/Prelude.agda
 	cp html/Haskell.Prelude.html html/index.html
 
+FILES = $(shell find src -type f)
+
 test/agda2hs : $(FILES)
 	cabal install agda2hs --overwrite-policy=always --installdir=test --install-method=copy
 
@@ -28,3 +54,60 @@ golden :
 
 docs :
 	make -C docs html
+
+
+################################################################################
+# Fromatting and linting
+FIND_EXCLUDE_PATH := -not -path './dist-*/*'
+
+FIND_HASKELL_SOURCES := find -name '*.hs' $(FIND_EXCLUDE_PATH)
+FIND_NIX_SOURCES := find -name '*.nix' $(FIND_EXCLUDE_PATH)
+FIND_CABAL_SOURCES := find -name '*.cabal' $(FIND_EXCLUDE_PATH)
+
+# Runs as command on all results of the `find` call at one.
+# e.g.
+#   foo found_file_1 found_file_2
+find_exec_all_fn = $(1) -exec $(2) {} +
+
+# Runs a command on all results of the `find` call one-by-one
+# e.g.
+#   foo found_file_1
+#   foo found_file_2
+find_exec_one_by_one_fn = $(1) | xargs -i $(2) {}
+
+.PHONY: format
+format: format_haskell format_nix format_cabal
+format_check : format_check_haskell format_check_nix format_check_cabal
+
+# Run stylish-haskell of .hs files
+.PHONY: format_haskell
+format_haskell:
+	$(call find_exec_all_fn, $(FIND_HASKELL_SOURCES), fourmolu -c -m inplace)
+
+# Run nixpkgs-fmt of .nix files
+.PHONY: format_nix
+format_nix:
+	$(call find_exec_all_fn, $(FIND_NIX_SOURCES), nixpkgs-fmt)
+
+.PHONY: format_check_nix
+format_check_nix:
+	$(call find_exec_all_fn, $(FIND_NIX_SOURCES), nixpkgs-fmt --check)
+
+# Run cabal-fmt of .cabal files
+.PHONY: format_cabal
+format_cabal:
+	$(call find_exec_all_fn, $(FIND_CABAL_SOURCES), cabal-fmt -i)
+
+.PHONY: format_check_cabal
+format_check_cabal:
+	$(call find_exec_all_fn, $(FIND_CABAL_SOURCES), cabal-fmt --check)
+
+# Apply hlint suggestions
+.PHONY: lint
+lint:
+	$(call find_exec_one_by_one_fn, $(FIND_HASKELL_SOURCES), hlint -j --refactor --refactor-options="-i")
+
+# Check hlint suggestions
+.PHONY: lint_check
+lint_check:
+	$(call find_exec_all_fn, $(FIND_HASKELL_SOURCES), hlint -j)

README.md

@@ -24,6 +24,17 @@ agda2hs was introduced in the Haskell Symposium '22 paper [Reasonable Agda is
 Correct Haskell: Writing Verified Haskell using
 agda2hs](https://jesper.sikanda.be/files/reasonable-agda-is-correct-haskell.pdf).
 
+## Development Setup
+
+Use the `make` command (with no arguments) to see a `Usage` message. 
+The commands make use of the following tools (all provided in the Nix development shell):
+
+- `cabal-fmt`: a cabal file formatter
+- `nixpkgs-fmt`: a nix file formatter
+- `hlint`: a haskell source code linter
+- `apply-refact`: a utility that ties in with `hlint` to perform automatic refactorings
+- `fourmolu`: a haskell source code formatter
+
 ## Future work
 
 Currently agda2hs is under active development, please take a look at

agda2hs.cabal

@@ -1,89 +1,104 @@
-cabal-version:       2.2
-name:                agda2hs
-version:             1.3
-license:             BSD-3-Clause
-license-file:        LICENSE
-author:              Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
-maintainer:          [email protected]
-copyright:           2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
-category:            Language, Compiler
-build-type:          Simple
-synopsis:            Compiling Agda code to readable Haskell.
+cabal-version:   2.2
+name:            agda2hs
+version:         1.3
+license:         BSD-3-Clause
+license-file:    LICENSE
+author:
+  Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
+
+maintainer:      [email protected]
+copyright:
+  2023 Ulf Norell, Jesper Cockx, Orestis Melkonian, Sára Juhošová, James Chapman, Lucas Escot, Henry Blanchette
+
+category:        Language, Compiler
+build-type:      Simple
+synopsis:        Compiling Agda code to readable Haskell.
 description:
   Produces verified and readable Haskell code by extracting it from a
   (lightly annotated) Agda program.
   The tool is implemented as an Agda backend, which means that `agda2hs` is a
   fully functional Agda compiler.
 
-extra-doc-files:    CHANGELOG.md
-                    README.md
+extra-doc-files:
+  CHANGELOG.md
+  README.md
 
 source-repository head
   type:     git
   location: https://github.com/agda/agda2hs.git
 
 flag smuggler2
-  description: Rewrite sources to cleanup imports, and create explicit exports
+  description:
+    Rewrite sources to cleanup imports, and create explicit exports
+
   default:     False
   manual:      True
 
 common smuggler-options
   if flag(smuggler2)
-    ghc-options: -fplugin=Smuggler2.Plugin
-                 -fplugin-opt=Smuggler2.Plugin:MinimiseImports
-                 -fplugin-opt=Smuggler2.Plugin:NoExportProcessing
-    build-depends: smuggler2 >= 0.3 && < 0.4
+    ghc-options:
+      -fplugin=Smuggler2.Plugin
+      -fplugin-opt=Smuggler2.Plugin:MinimiseImports
+      -fplugin-opt=Smuggler2.Plugin:NoExportProcessing
+
+    build-depends: smuggler2 >=0.3 && <0.4
 
 executable agda2hs
-  import:              smuggler-options
-  hs-source-dirs:      src
-  main-is:             Main.hs
-  other-modules:       Agda2Hs.AgdaUtils,
-                       Agda2Hs.Compile,
-                       Agda2Hs.Compile.ClassInstance,
-                       Agda2Hs.Compile.Data,
-                       Agda2Hs.Compile.Function,
-                       Agda2Hs.Compile.Imports,
-                       Agda2Hs.Compile.Name,
-                       Agda2Hs.Compile.Postulate,
-                       Agda2Hs.Compile.Record,
-                       Agda2Hs.Compile.Term,
-                       Agda2Hs.Compile.Type,
-                       Agda2Hs.Compile.TypeDefinition,
-                       Agda2Hs.Compile.Types,
-                       Agda2Hs.Compile.Utils,
-                       Agda2Hs.Compile.Var,
-                       Agda2Hs.Config,
-                       Agda2Hs.HsUtils,
-                       Agda2Hs.Pragma,
-                       Agda2Hs.Render,
-                       AgdaInternals,
-                       Paths_agda2hs
-  autogen-modules:     Paths_agda2hs
-  build-depends:       base                 >= 4.13    && < 4.20,
-                       Agda                 >= 2.6.4   && < 2.6.5,
-                       bytestring           >= 0.11.5  && < 0.13,
-                       containers           >= 0.6     && < 0.8,
-                       unordered-containers >= 0.2.19  && < 0.3,
-                       mtl                  >= 2.2     && < 2.3 || >= 2.3.1,
-                       transformers         >= 0.6     && < 0.7,
-                       monad-control        >= 1.0     && < 1.1,
-                       directory            >= 1.2.6.2 && < 1.4,
-                       filepath             >= 1.4.1.0 && < 1.5,
-                       haskell-src-exts     >= 1.23    && < 1.25,
-                       syb                  >= 0.7.2   && < 0.8,
-                       text                 >= 2.0.2   && < 2.2,
-                       deepseq              >= 1.4.4   && < 1.6,
-                       yaml                 >= 0.11    && < 0.12,
-                       aeson                >= 2.2     && < 2.3,
-  default-language:    Haskell2010
-  default-extensions:  LambdaCase
-                       RecordWildCards
-                       FlexibleContexts
-                       MultiWayIf
-                       TupleSections
-                       ScopedTypeVariables
-                       ViewPatterns
-                       NamedFieldPuns
-                       PatternSynonyms
-  ghc-options:         -Werror -rtsopts
+  import:             smuggler-options
+  hs-source-dirs:     src
+  main-is:            Main.hs
+  other-modules:
+    Agda2Hs.AgdaUtils
+    Agda2Hs.Compile
+    Agda2Hs.Compile.ClassInstance
+    Agda2Hs.Compile.Data
+    Agda2Hs.Compile.Function
+    Agda2Hs.Compile.Imports
+    Agda2Hs.Compile.Name
+    Agda2Hs.Compile.Postulate
+    Agda2Hs.Compile.Record
+    Agda2Hs.Compile.Term
+    Agda2Hs.Compile.Type
+    Agda2Hs.Compile.TypeDefinition
+    Agda2Hs.Compile.Types
+    Agda2Hs.Compile.Utils
+    Agda2Hs.Compile.Var
+    Agda2Hs.Config
+    Agda2Hs.HsUtils
+    Agda2Hs.Pragma
+    Agda2Hs.Render
+    AgdaInternals
+    Paths_agda2hs
+
+  autogen-modules:    Paths_agda2hs
+  build-depends:
+    , aeson                 >=2.2     && <2.3
+    , Agda                  >=2.6.4   && <2.6.5
+    , base                  >=4.13    && <4.20
+    , bytestring            >=0.11.5  && <0.13
+    , containers            >=0.6     && <0.8
+    , deepseq               >=1.4.4   && <1.6
+    , directory             >=1.2.6.2 && <1.4
+    , filepath              >=1.4.1.0 && <1.5
+    , haskell-src-exts      >=1.23    && <1.25
+    , monad-control         >=1.0     && <1.1
+    , mtl                   >=2.2     && <2.3   || >=2.3.1
+    , syb                   >=0.7.2   && <0.8
+    , text                  >=2.0.2   && <2.2
+    , transformers          >=0.6     && <0.7
+    , unordered-containers  >=0.2.19  && <0.3
+    , yaml                  >=0.11    && <0.12
+
+  default-language:   Haskell2010
+  default-extensions:
+    FlexibleContexts
+    LambdaCase
+    MultiWayIf
+    NamedFieldPuns
+    PatternSynonyms
+    RecordWildCards
+    ScopedTypeVariables
+    TupleSections
+    ViewPatterns
+
+  ghc-options:        -Werror -rtsopts

agda2hs.nix

@@ -1,29 +1,33 @@
-{stdenv, lib, self, agda2hs, runCommandNoCC, makeWrapper, writeText, mkShell, ghcWithPackages}:
+{ stdenv, lib, self, agda2hs, runCommandNoCC, makeWrapper, writeText, mkShell, ghcWithPackages }:
 with lib.strings;
 let
-  withPackages' = {
-      pkgs,
-      ghc ? ghcWithPackages (p: with p; [ ieee754 ])
-  }: let
-    pkgs' = if builtins.isList pkgs then pkgs else pkgs self;
-    library-file = writeText "libraries" ''
-      ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')}
-    '';
-    pname = "agda2hsWithPackages";
-    version = agda2hs.version;
-  in runCommandNoCC "${pname}-${version}" {
-    inherit pname version;
-    nativeBuildInputs = [ makeWrapper ];
-    passthru.unwrapped = agda2hs;
-  } ''
-    mkdir -p $out/bin
-    makeWrapper ${agda2hs}/bin/agda2hs $out/bin/agda2hs \
-      --add-flags "--with-compiler=${ghc}/bin/ghc" \
-      --add-flags "--library-file=${library-file}" \
-      --add-flags "--local-interfaces"
+  withPackages' =
+    { pkgs
+    , ghc ? ghcWithPackages (p: with p; [ ieee754 ])
+    }:
+    let
+      pkgs' = if builtins.isList pkgs then pkgs else pkgs self;
+      library-file = writeText "libraries" ''
+        ${(concatMapStringsSep "\n" (p: "${p}/${p.libraryFile}") pkgs')}
+      '';
+      pname = "agda2hsWithPackages";
+      version = agda2hs.version;
+    in
+    runCommandNoCC "${pname}-${version}"
+      {
+        inherit pname version;
+        nativeBuildInputs = [ makeWrapper ];
+        passthru.unwrapped = agda2hs;
+      } ''
+      mkdir -p $out/bin
+      makeWrapper ${agda2hs}/bin/agda2hs $out/bin/agda2hs \
+        --add-flags "--with-compiler=${ghc}/bin/ghc" \
+        --add-flags "--library-file=${library-file}" \
+        --add-flags "--local-interfaces"
     ''; # Local interfaces has been added for now: See https://github.com/agda/agda/issues/4526
   withPackages = arg: if builtins.isAttrs arg then withPackages' arg else withPackages' { pkgs = arg; };
-in {
+in
+{
   inherit withPackages;
-  agda2hs = withPackages [];
+  agda2hs = withPackages [ ];
 }