add formatting to Makefile, flake.nix, README

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

flake.nix

@@ -4,14 +4,15 @@
   inputs.nixpkgs.url = github:NixOS/nixpkgs;
   inputs.flake-utils.url = github:numtide/flake-utils;
 
-  outputs = {self, nixpkgs, flake-utils}:
+  outputs = { self, nixpkgs, flake-utils }:
     flake-utils.lib.eachDefaultSystem (system:
       let
-        pkgs = import nixpkgs {inherit system;};
+        pkgs = import nixpkgs { inherit system; };
 
         agda2hs-lib = pkgs.agdaPackages.mkDerivation
-          { pname = "agda2hs";
-            meta = {};
+          {
+            pname = "agda2hs";
+            meta = { };
             version = "1.3";
             preBuild = ''
               echo "{-# OPTIONS --sized-types #-}" > Everything.agda
@@ -25,16 +26,17 @@
             name = "agda2hs";
             src = ./.;
             extraCabal2nixOptions = options; #"--jailbreak"
-        };
+          };
         # jailbreaking here because otherwise aeson has to be overridden and that triggers recompilation of a lot of dependencies
-        agda2hs-hs = pkgs.haskellPackages.callPackage (agda2hs-pkg "--jailbreak") {};
+        agda2hs-hs = pkgs.haskellPackages.callPackage (agda2hs-pkg "--jailbreak") { };
         agda2hs-expr = import ./agda2hs.nix;
         agda2hs = pkgs.callPackage agda2hs-expr {
-            inherit self;
-            agda2hs = agda2hs-hs;
-            inherit (pkgs.haskellPackages) ghcWithPackages;
-          };
-      in {
+          inherit self;
+          agda2hs = agda2hs-hs;
+          inherit (pkgs.haskellPackages) ghcWithPackages;
+        };
+      in
+      {
         packages = {
           inherit agda2hs-lib;
           inherit (agda2hs) agda2hs;
@@ -45,12 +47,19 @@
           inherit agda2hs-pkg agda2hs-hs agda2hs-expr;
         };
         devShells.default = pkgs.haskellPackages.shellFor {
-          packages = p: [agda2hs-hs];
+          withHoogle = true;
+          packages = p: [ agda2hs-hs ];
           buildInputs = with pkgs.haskellPackages; [
+            ghcid
             cabal-install
             cabal2nix
             haskell-language-server
             pkgs.agda
+            cabal-fmt # cabal formatter
+            pkgs.nixpkgs-fmt # nix formatter
+            hlint # linter for haskell code
+            apply-refact # automatic refactorings, ties in with hlint
+            fourmolu # formatter for haskell code
           ];
         };
       });

fourmolu.yaml

@@ -0,0 +1,8 @@
+indentation: 2
+comma-style: leading
+record-brace-space: true
+indent-wheres: true
+diff-friendly-import-export: true
+respectful: true
+haddock-style: multi-line
+newlines-between-decls: 1