Automatic formatting.

.githooks/pre-commit

@@ -0,0 +1,13 @@
+#!/bin/bash
+set -e
+
+filesToFormat=$(
+  git --no-pager diff --name-status --no-color --cached | \
+    awk '$1 != "D" && $2 ~ /\.hs/ {print $NF}'
+)
+
+for path in $filesToFormat
+do
+  ormolu --mode inplace $path
+  git add $path
+done;

README.md

@@ -34,3 +34,11 @@ $ direnv allow
 
 from the root directory, `nix develop` will be automatically invoked each time
 a change is detected in `flake.nix` or you return to the directory.
+
+## Formatting
+
+Link in `.githooks` by running:
+
+```bash
+$ git config --local core.hooksPath .githooks/
+```

flake.nix

@@ -25,6 +25,7 @@
             # https://www.reddit.com/r/Nix/comments/jyczts/nixshell_locale_issue/
             pkgs.glibcLocales
             pkgs.haskellPackages.cabal-install
+            pkgs.haskellPackages.ormolu
             pkgs.haskellPackages.tasty-discover
           ];
         };

initial-encoding/app/Main.hs

@@ -2,16 +2,15 @@
 
 module Main where
 
-import qualified Options.Applicative as O
-import qualified Text.Megaparsec as M
-
 import Data.Text (Text)
 import Data.Text.IO (hGetContents)
 import Options.Applicative ((<**>))
+import qualified Options.Applicative as O
 import Parser.Initial
 import Parser.Utils
 import System.Environment (getArgs)
-import System.IO (IOMode(ReadMode), openFile)
+import System.IO (IOMode (ReadMode), openFile)
+import qualified Text.Megaparsec as M
 
 -- ========================================
 -- Arguments
@@ -20,7 +19,8 @@ import System.IO (IOMode(ReadMode), openFile)
 data Args = Args {argsFileName :: !FilePath, argsMethod :: !Text}
 
 args :: O.Parser Args
-args = Args
+args =
+  Args
     <$> O.strArgument
       ( O.metavar "FILENAME" <> O.help "The file we want to parse."
       )
@@ -30,7 +30,8 @@ args = Args
           <> O.metavar "METHOD"
           <> O.showDefault
           <> O.value "naive"
-     <> O.help "The parse strategy we want to try. Should be one of 'naive', \
+          <> O.help
+            "The parse strategy we want to try. Should be one of 'naive', \
             \'single', 'strict', or 'gadt'."
       )
 
@@ -56,7 +57,9 @@ run args = do
 main :: IO ()
 main = run =<< O.execParser opts
   where
-  opts = O.info (args <**> O.helper)
+    opts =
+      O.info
+        (args <**> O.helper)
         ( O.fullDesc
             <> O.progDesc "Different parsing strategies using initial encoding"
             <> O.header "Initial encoding parsing"

initial-encoding/src/Parser/Initial.hs

@@ -6,30 +6,30 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 
 module Parser.Initial
-( Expr(..)
-, GExpr(..)
-, Result(..)
-, Wrapper(..)
-, eval
-, parseGadt
-, parseNaive
-, parseSingle
-, parseStrict
-, toResult
-) where
-
-import qualified Control.Monad.Combinators.Expr as E
-import qualified Text.Megaparsec as M
+  ( Expr (..),
+    GExpr (..),
+    Result (..),
+    Wrapper (..),
+    eval,
+    parseGadt,
+    parseNaive,
+    parseSingle,
+    parseStrict,
+    toResult,
+  )
+where
 
 import Control.Applicative ((<|>))
-import Control.DeepSeq (NFData(..), deepseq)
+import Control.DeepSeq (NFData (..), deepseq)
 import Control.Monad (join)
+import qualified Control.Monad.Combinators.Expr as E
 import Control.Monad.Except (MonadError, throwError)
 import Data.Bifunctor (bimap, first)
 import Data.Functor (void)
 import Data.Maybe (isJust)
 import Data.Text (Text, pack, unpack)
 import Parser.Utils
+import qualified Text.Megaparsec as M
 
 -- ========================================
 -- ADT
@@ -85,9 +85,11 @@ toResult (EOr lhs rhs) = do
 parseNaive :: Parser Result
 parseNaive = expr >>= either (fail . unpack) pure . toResult
   where
-  expr = E.makeExprParser term
-    [ [binary "+" EAdd, binary "-" ESub]
-    , [binary "&&" EAnd, binary "||" EOr]
+    expr =
+      E.makeExprParser
+        term
+        [ [binary "+" EAdd, binary "-" ESub],
+          [binary "&&" EAnd, binary "||" EOr]
         ]
 
     binary name f = E.InfixL (f <$ symbol name)
@@ -101,9 +103,11 @@ parseNaive = expr >>= either (fail . unpack) pure . toResult
 parseSingle :: Parser Result
 parseSingle = expr >>= either (fail . unpack) pure
   where
-  expr = E.makeExprParser term
-    [ [binary "+"  asInt  EInt  EAdd, binary "-"  asInt  EInt  ESub]
-    , [binary "&&" asBool EBool EAnd, binary "||" asBool EBool EOr ]
+    expr =
+      E.makeExprParser
+        term
+        [ [binary "+" asInt EInt EAdd, binary "-" asInt EInt ESub],
+          [binary "&&" asBool EBool EAnd, binary "||" asBool EBool EOr]
         ]
 
     binary name cast f bin = E.InfixL do
@@ -135,13 +139,13 @@ parseStrict = term >>= expr
         Just OpOr -> nest t asBool EBool EOr
         _ -> pure t
 
-  nest
-    :: forall a
-     . Result
-    -> (Result -> Either Text a)
-    -> (a -> Expr)
-    -> (Expr -> Expr -> Expr)
-    -> Parser Result
+    nest ::
+      forall a.
+      Result ->
+      (Result -> Either Text a) ->
+      (a -> Expr) ->
+      (Expr -> Expr -> Expr) ->
+      Parser Result
     nest t cast f bin = do
       t' <- term
       a <- either (fail . unpack) pure do
@@ -152,8 +156,9 @@ parseStrict = term >>= expr
 
     term = do
       p <- M.option Nothing $ Just <$> symbol "("
-    if isJust p then (term >>= expr) <* symbol ")" else
-      RInt <$> integer <|> RBool <$> boolean
+      if isJust p
+        then (term >>= expr) <* symbol ")"
+        else RInt <$> integer <|> RBool <$> boolean
 
 -- ========================================
 -- GADTs
@@ -178,13 +183,13 @@ eval (GAnd lhs rhs) = eval lhs && eval rhs
 eval (GOr lhs rhs) = eval lhs || eval rhs
 
 asInt' :: GExpr a -> Either Text (GExpr Integer)
-asInt' a@(GInt _  ) = pure a
+asInt' a@(GInt _) = pure a
 asInt' a@(GAdd _ _) = pure a
 asInt' a@(GSub _ _) = pure a
 asInt' _ = Left "Expected an integer type."
 
 asBool' :: GExpr a -> Either Text (GExpr Bool)
-asBool' a@(GBool _  ) = pure a
+asBool' a@(GBool _) = pure a
 asBool' a@(GAnd _ _) = pure a
 asBool' a@(GOr _ _) = pure a
 asBool' _ = Left "Expected a boolean type."
@@ -201,14 +206,14 @@ parseGadt = term >>= expr
         Just OpOr -> nest t asBool' GBool GOr
         _ -> pure t
 
-  nest
-    :: forall b
-     . Show b
-    => Wrapper
-    -> (forall a. GExpr a -> Either Text (GExpr b))
-    -> (b -> GExpr b)
-    -> (GExpr b -> GExpr b -> GExpr b)
-    -> Parser Wrapper
+    nest ::
+      forall b.
+      Show b =>
+      Wrapper ->
+      (forall a. GExpr a -> Either Text (GExpr b)) ->
+      (b -> GExpr b) ->
+      (GExpr b -> GExpr b -> GExpr b) ->
+      Parser Wrapper
     nest (Wrapper t) cast f bin = do
       Wrapper t' <- term
       case (cast t, cast t') of
@@ -220,5 +225,6 @@ parseGadt = term >>= expr
 
     term = do
       p <- M.option Nothing $ Just <$> symbol "("
-    if isJust p then (term >>= expr) <* symbol ")" else
-      Wrapper . GInt <$> integer <|> Wrapper . GBool <$> boolean
+      if isJust p
+        then (term >>= expr) <* symbol ")"
+        else Wrapper . GInt <$> integer <|> Wrapper . GBool <$> boolean

initial-encoding/test/Test/Parser/InitialTest.hs

@@ -4,17 +4,17 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Test.Parser.InitialTest
-( spec_parser,
-) where
-
-import qualified Text.Megaparsec as M
+  ( spec_parser,
+  )
+where
 
 import Data.Bifunctor (first)
-import Data.Functor.Identity (Identity(..))
+import Data.Functor.Identity (Identity (..))
 import Data.Text (Text, pack)
 import Parser.Initial
 import Parser.Utils (Parser, allEqual, runParser)
 import Test.Hspec (Expectation, Spec, describe, it, shouldBe)
+import qualified Text.Megaparsec as M
 
 -- ========================================
 -- Utility
@@ -30,11 +30,12 @@ convert (GOr  lhs rhs) = EOr  (convert lhs) (convert rhs)
 
 runParsers :: Text -> [Either Text Result]
 runParsers input =
-  [ runParser parseNaive
-  , runParser parseSingle
-  , runParser parseStrict
-  , runGadt
-  ] <*> [input]
+  [ runParser parseNaive,
+    runParser parseSingle,
+    runParser parseStrict,
+    runGadt
+  ]
+    <*> [input]
   where
     runGadt i = do
       Wrapper res <- runParser parseGadt i
@@ -84,7 +85,9 @@ spec_parser = do
       shouldParse "false || false" (RBool False)
   describe "invalid types" do
     it "mismatch" do
-      shouldNotParse "true && 1"
+      shouldNotParse
+        "true && 1"
         "1:10:\n  |\n1 | true && 1\n  |          ^\nCould not cast boolean.\n"
-      shouldNotParse "1 + true"
+      shouldNotParse
+        "1 + true"
         "1:9:\n  |\n1 | 1 + true\n  |         ^\nCould not cast integer.\n"

leibniz-proof/app/Main.hs

@@ -3,20 +3,22 @@
 
 module Main where
 
-import Data.Eq.Type ((:=)(..), refl)
+import Data.Eq.Type (refl, (:=) (..))
 
 newtype F1 t b a = F1 {runF1 :: t := (a -> b)}
+
 newtype F2 t a b = F2 {runF2 :: t := (a -> b)}
 
-functionEquality
-  :: forall a1 a2 b1 b2
-   . a1 := a2
-  -> b1 := b2
-  -> (a1 -> b1) := (a2 -> b2)
+functionEquality ::
+  forall a1 a2 b1 b2.
+  a1 := a2 ->
+  b1 := b2 ->
+  (a1 -> b1) := (a2 -> b2)
 functionEquality
   (Refl s1) -- s1 :: forall c. c a1 -> c a2
   (Refl s2) -- s2 :: forall c. c b1 -> c b2
-  = runF2    -- (a1 -> b1) := (a2 -> b2)
+    =
+    runF2 -- (a1 -> b1) := (a2 -> b2)
       . s2 -- F2 (a1 -> b1) a2 b2
       . F2 -- F2 (a1 -> b1) a2 b1
       . runF1 -- (a1 -> b1) := (a2 -> b1)

parser-utils/src/Parser/Utils.hs

@@ -2,28 +2,28 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Parser.Utils
-( Op(..)
-, Parser
-, ParserT
-, allEqual
-, boolean
-, integer
-, lexeme
-, ops
-, parens
-, runParser
-, space
-, symbol
-) where
-
-import qualified Text.Megaparsec as M
-import qualified Text.Megaparsec.Char as MC
-import qualified Text.Megaparsec.Char.Lexer as ML
+  ( Op (..),
+    Parser,
+    ParserT,
+    allEqual,
+    boolean,
+    integer,
+    lexeme,
+    ops,
+    parens,
+    runParser,
+    space,
+    symbol,
+  )
+where
 
 import Control.Applicative ((<|>))
 import Data.Functor (($>))
 import Data.Text (Text, pack)
 import Data.Void (Void)
+import qualified Text.Megaparsec as M
+import qualified Text.Megaparsec.Char as MC
+import qualified Text.Megaparsec.Char.Lexer as ML
 
 -- ========================================
 -- Parsing
@@ -66,11 +66,12 @@ instance Show Op where
   show OpOr = "||"
 
 ops :: forall m. ParserT m Op
-ops = M.choice
-  [ symbol "+"  $> OpAdd
-  , symbol "-"  $> OpSub
-  , symbol "&&" $> OpAnd
-  , symbol "||" $> OpOr
+ops =
+  M.choice
+    [ symbol "+" $> OpAdd,
+      symbol "-" $> OpSub,
+      symbol "&&" $> OpAnd,
+      symbol "||" $> OpOr
     ]
 
 runParser :: forall a. Parser a -> Text -> Either Text a
@@ -86,4 +87,4 @@ allEqual :: forall a. Eq a => [a] -> Bool
 allEqual [] = True
 allEqual [x] = True
 allEqual [x, y] = x == y
-allEqual (x:y:xs) = x == y && allEqual (y : xs)
+allEqual (x : y : xs) = x == y && allEqual (y : xs)

tagless-final/app/Main.hs

@@ -3,15 +3,14 @@
 
 module Main where
 
-import qualified Options.Applicative as O
-
 import Data.Text (Text)
 import Data.Text.IO (hGetContents)
 import Options.Applicative ((<**>))
+import qualified Options.Applicative as O
 import Parser.Final
 import Parser.Utils
 import System.Environment (getArgs)
-import System.IO (IOMode(ReadMode), openFile)
+import System.IO (IOMode (ReadMode), openFile)
 
 -- ========================================
 -- Arguments
@@ -20,7 +19,8 @@ import System.IO (IOMode(ReadMode), openFile)
 data Args = Args {argsFileName :: !FilePath, argsMethod :: !Text}
 
 args :: O.Parser Args
-args = Args
+args =
+  Args
     <$> O.strArgument
       ( O.metavar "FILENAME" <> O.help "The file we want to parse."
       )
@@ -30,7 +30,8 @@ args = Args
           <> O.metavar "METHOD"
           <> O.showDefault
           <> O.value "single"
-     <> O.help "The parse strategy we want to try. Should be one of 'single' \
+          <> O.help
+            "The parse strategy we want to try. Should be one of 'single' \
             \or 'strict'."
       )
 
@@ -59,7 +60,9 @@ run args = do
 main :: IO ()
 main = run =<< O.execParser opts
   where
-  opts = O.info (args <**> O.helper)
+    opts =
+      O.info
+        (args <**> O.helper)
         ( O.fullDesc
             <> O.progDesc "Different parsing strategies using initial encoding"
             <> O.header "Initial encoding parsing"

tagless-final/src/Parser/Final.hs

@@ -11,32 +11,32 @@
 {-# LANGUAGE ViewPatterns #-}
 
 module Parser.Final
-( Dynamic(..)
-, Eval(..)
-, SQ(..)
-, Symantics(..)
-, TQ(..)
-, TextSymantics(..)
-, Typeable(..)
-, fromDyn
-, parseSingle
-, parseStrict
-, toDyn
-, runBoth'
-) where
-
-import qualified Control.Monad.Combinators.Expr as E
-import qualified Data.Eq.Type as EQ
-import qualified Text.Megaparsec as M
+  ( Dynamic (..),
+    Eval (..),
+    SQ (..),
+    Symantics (..),
+    TQ (..),
+    TextSymantics (..),
+    Typeable (..),
+    fromDyn,
+    parseSingle,
+    parseStrict,
+    toDyn,
+    runBoth',
+  )
+where
 
 import Control.Applicative ((<|>))
-import Control.DeepSeq (NFData(..), deepseq)
+import Control.DeepSeq (NFData (..), deepseq)
 import Control.Monad.Combinators (sepBy)
+import qualified Control.Monad.Combinators.Expr as E
 import Data.Eq.Type ((:=))
+import qualified Data.Eq.Type as EQ
 import Data.Functor (void)
 import Data.Maybe (isJust)
 import Data.Text (Text, drop, dropEnd, pack, unpack)
 import Parser.Utils
+import qualified Text.Megaparsec as M
 import Prelude hiding (drop)
 
 -- ========================================
@@ -141,14 +141,14 @@ fromDyn (Dynamic t e) = case t of
     r' <- r
     pure $ EQ.coerce (EQ.lift r') e
 
-asDyn
-  :: forall repr a
-   . TextSymantics repr
-  => IsDynamic a
-  => (repr a -> repr a -> repr a)
-  -> Dynamic repr
-  -> Dynamic repr
-  -> Maybe (Dynamic repr)
+asDyn ::
+  forall repr a.
+  TextSymantics repr =>
+  IsDynamic a =>
+  (repr a -> repr a -> repr a) ->
+  Dynamic repr ->
+  Dynamic repr ->
+  Maybe (Dynamic repr)
 asDyn bin lhs rhs = do
   lhs' <- fromDyn lhs
   rhs' <- fromDyn rhs
@@ -163,9 +163,11 @@ parseSingle = expr >>= either offsetFail pure
   where
     offsetFail (offset, msg) = M.setOffset offset >> fail msg
 
-  expr = E.makeExprParser term
-    [ [binary "+" eAdd, binary "-" eSub]
-    , [binary "&&" eAnd, binary "||" eOr]
+    expr =
+      E.makeExprParser
+        term
+        [ [binary "+" eAdd, binary "-" eSub],
+          [binary "&&" eAnd, binary "||" eOr]
         ]
 
     binary name bin = E.InfixL do
@@ -190,11 +192,11 @@ instance (NFData t) => NFData (Eval t) where
 instance NFData (Dynamic Eval) where
   rnf (Dynamic _ e) = e `seq` ()
 
-parseStrict
-  :: forall repr
-   . NFData (Dynamic repr)
-  => TextSymantics repr
-  => Parser (Dynamic repr)
+parseStrict ::
+  forall repr.
+  NFData (Dynamic repr) =>
+  TextSymantics repr =>
+  Parser (Dynamic repr)
 parseStrict = term >>= expr
   where
     expr :: Dynamic repr -> Parser (Dynamic repr)
@@ -207,13 +209,13 @@ parseStrict = term >>= expr
         Just OpOr -> nest t eOr OpOr
         _ -> pure t
 
-  nest
-    :: forall a
-     . IsDynamic a
-    => Dynamic repr
-    -> (repr a -> repr a -> repr a)
-    -> Op
-    -> Parser (Dynamic repr)
+    nest ::
+      forall a.
+      IsDynamic a =>
+      Dynamic repr ->
+      (repr a -> repr a -> repr a) ->
+      Op ->
+      Parser (Dynamic repr)
     nest t bin op = do
       t' <- term
       case asDyn bin t t' of
@@ -223,8 +225,9 @@ parseStrict = term >>= expr
     term :: Parser (Dynamic repr)
     term = do
       p <- M.option Nothing $ Just <$> symbol "("
-    if isJust p then (term >>= expr) <* symbol ")" else
-      toDyn <$> integer <|> toDyn <$> boolean
+      if isJust p
+        then (term >>= expr) <* symbol ")"
+        else toDyn <$> integer <|> toDyn <$> boolean
 
 -- ========================================
 -- Pretty print
@@ -317,8 +320,10 @@ pPrint' d = case fromDyn @MSQ @Integer d of
 
 data SCopy repr1 repr2 a = SCopy (repr1 a) (repr2 a)
 
-instance (Symantics repr1, Symantics repr2)
-  => Symantics (SCopy repr1 repr2) where
+instance
+  (Symantics repr1, Symantics repr2) =>
+  Symantics (SCopy repr1 repr2)
+  where
   eInt e = SCopy (eInt e) (eInt e)
   eBool e = SCopy (eBool e) (eBool e)
   eAdd (SCopy a1 a2) (SCopy b1 b2) = SCopy (eAdd a1 b1) (eAdd a2 b2)
@@ -326,32 +331,34 @@ instance (Symantics repr1, Symantics repr2)
   eAnd (SCopy a1 a2) (SCopy b1 b2) = SCopy (eAnd a1 b1) (eAnd a2 b2)
   eOr (SCopy a1 a2) (SCopy b1 b2) = SCopy (eOr a1 b1) (eOr a2 b2)
 
-instance (MulSymantics repr1, MulSymantics repr2)
-  => MulSymantics (SCopy repr1 repr2) where
+instance
+  (MulSymantics repr1, MulSymantics repr2) =>
+  MulSymantics (SCopy repr1 repr2)
+  where
   eMul (SCopy a1 a2) (SCopy b1 b2) = SCopy (eMul a1 b1) (eMul a2 b2)
 
-runEval'
-  :: forall repr
-   . Dynamic (SCopy Eval repr)
-  -> Maybe (Result, Dynamic repr)
+runEval' ::
+  forall repr.
+  Dynamic (SCopy Eval repr) ->
+  Maybe (Result, Dynamic repr)
 runEval' d = case fromDyn d :: Maybe (SCopy Eval repr Integer) of
   Just (SCopy (Eval a) r) -> pure (RInt a, Dynamic pInt r)
   Nothing -> case fromDyn d :: Maybe (SCopy Eval repr Bool) of
     Just (SCopy (Eval a) r) -> pure (RBool a, Dynamic pBool r)
     Nothing -> Nothing
 
-runPPrint'
-  :: forall repr
-   . Dynamic (SCopy PPrint repr)
-  -> Maybe (Text, Dynamic repr)
+runPPrint' ::
+  forall repr.
+  Dynamic (SCopy PPrint repr) ->
+  Maybe (Text, Dynamic repr)
 runPPrint' d = case fromDyn d :: Maybe (SCopy PPrint repr Text) of
   Just (SCopy (PPrint a) r) -> pure (a, Dynamic pText r)
   Nothing -> Nothing
 
-runBoth'
-  :: forall repr
-   . Dynamic (SCopy Eval (SCopy PPrint repr))
-  -> Maybe (Result, Text, Dynamic repr)
+runBoth' ::
+  forall repr.
+  Dynamic (SCopy Eval (SCopy PPrint repr)) ->
+  Maybe (Result, Text, Dynamic repr)
 runBoth' d = do
   (r, d') <- runEval' d
   (p, d'') <- runPPrint' d'

tagless-final/test/Test/Parser/FinalTest.hs

@@ -5,8 +5,9 @@
 {-# LANGUAGE TypeApplications #-}
 
 module Test.Parser.FinalTest
-( spec_parser,
-) where
+  ( spec_parser,
+  )
+where
 
 import Data.Text (Text)
 import Parser.Final
@@ -78,7 +79,9 @@ spec_parser = do
       shouldParse "false || false" (toDyn False)
   describe "invalid types" do
     it "mismatch" do
-      shouldNotParse "true && 1"
+      shouldNotParse
+        "true && 1"
         "1:9:\n  |\n1 | true && 1\n  |         ^\nInvalid operands for `&&`\n"
-      shouldNotParse "1 + true"
+      shouldNotParse
+        "1 + true"
         "1:5:\n  |\n1 | 1 + true\n  |     ^\nInvalid operands for `+`\n"