Apply formatting

fizruk · Jun 20, 2024 · f41ad16 · f41ad16
1 parent 7367092
commit f41ad16
Show file tree

Hide file tree

Showing 6 changed files with 37 additions and 35 deletions.
diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/Convert.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/Convert.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE LambdaCase      #-}
 {-# OPTIONS_GHC -fno-warn-type-defaults      #-}
+{-# LANGUAGE LambdaCase      #-}
 {-# LANGUAGE TemplateHaskell #-}
 module Control.Monad.Free.Foil.TH.Convert where
 
@@ -77,11 +77,11 @@ mkConvertToSig termT nameT scopeT patternT = do
         where
           x = mkName "x"
           isVarP VarP{} = True
-          isVarP _ = False
+          isVarP _      = False
           pats =
             [ case type_ of
                 PeelConT typeName _ | typeName == nameT -> VarP x
-                _ -> WildP
+                _                                       -> WildP
             | (_bang, type_) <- types ]
       NormalC conName types -> mkClause conName conName' types
         where
@@ -205,9 +205,9 @@ mkGetPatternBinder nameT patternT = do
     mkClause :: Name -> [BangType] -> Q [Clause]
     mkClause conName types = do
       body <- case concat vars of
-        [] -> [e| Nothing |]
+        []       -> [e| Nothing |]
         [Just y] -> [e| Just $y |]
-        _ -> [e| error "complex patterns are not supported" |]
+        _        -> [e| error "complex patterns are not supported" |]
       return [ Clause [ConP conName [] pats] (NormalB body) [] ]
       where
         x = mkName "x"
@@ -259,7 +259,7 @@ mkGetScopedTerm termT scopeT = do
     mkClause conName types = do
       body <- case concat vars of
         [y] -> [e| $y |]
-        _ -> [e| error "complex patterns are not supported" |]
+        _   -> [e| error "complex patterns are not supported" |]
       return [ Clause [ConP conName [] pats] (NormalB body) [] ]
       where
         x = mkName "x"

diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs
@@ -5,7 +5,7 @@
 {-# LANGUAGE ViewPatterns    #-}
 module Control.Monad.Free.Foil.TH.PatternSynonyms where
 
-import Control.Monad (forM_)
+import           Control.Monad              (forM_)
 import qualified Control.Monad.Foil         as Foil
 import           Control.Monad.Foil.TH.Util
 import           Control.Monad.Free.Foil

diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs
@@ -1,7 +1,7 @@
-{-# LANGUAGE LambdaCase      #-}
 {-# OPTIONS_GHC -fno-warn-type-defaults      #-}
-{-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE LambdaCase      #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns    #-}
 module Control.Monad.Free.Foil.TH.ZipMatch where
 
 import           Language.Haskell.TH

diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FoilTH.hs
@@ -1,10 +1,9 @@
--- {-# OPTIONS_GHC -ddump-splices #-}
+{-# LANGUAGE DataKinds                  #-}
 {-# LANGUAGE DerivingStrategies         #-}
-{-# LANGUAGE KindSignatures         #-}
-{-# LANGUAGE DataKinds         #-}
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE InstanceSigs               #-}
+{-# LANGUAGE KindSignatures             #-}
 {-# LANGUAGE LambdaCase                 #-}
 {-# LANGUAGE LiberalTypeSynonyms        #-}
 {-# LANGUAGE OverloadedStrings          #-}
@@ -40,13 +39,13 @@ module Language.LambdaPi.Impl.FoilTH where
 
 import           Control.Monad.Foil
 import           Control.Monad.Foil.TH
-import qualified Language.LambdaPi.Syntax.Abs as Raw
-import qualified Language.LambdaPi.Syntax.Print as Raw
-import qualified Language.LambdaPi.Syntax.Par as Raw
+import qualified Data.Map                        as Map
+import qualified Language.LambdaPi.Syntax.Abs    as Raw
 import qualified Language.LambdaPi.Syntax.Layout as Raw
-import qualified Language.LambdaPi.Syntax.Lex as Raw
-import System.Exit (exitFailure)
-import qualified Data.Map as Map
+import qualified Language.LambdaPi.Syntax.Lex    as Raw
+import qualified Language.LambdaPi.Syntax.Par    as Raw
+import qualified Language.LambdaPi.Syntax.Print  as Raw
+import           System.Exit                     (exitFailure)
 
 -- * Generated code
 
@@ -122,11 +121,11 @@ whnf scope = \case
   FoilFirst loc t ->
     case whnf scope t of
       FoilPair _loc l _r -> whnf scope l
-      t'         -> FoilFirst loc t'
+      t'                 -> FoilFirst loc t'
   FoilSecond loc t ->
     case whnf scope t of
       FoilPair _loc _l r -> whnf scope r
-      t'         -> FoilSecond loc t'
+      t'                 -> FoilSecond loc t'
   t -> t
 
 -- ** Interpreter

diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoil.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE DataKinds         #-}
-{-# LANGUAGE DeriveTraversable     #-}
+{-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs             #-}
 {-# LANGUAGE LambdaCase        #-}
@@ -31,8 +31,8 @@ module Language.LambdaPi.Impl.FreeFoil where
 
 import qualified Control.Monad.Foil              as Foil
 import           Control.Monad.Free.Foil
-import           Data.Bifunctor.TH
 import           Data.Bifunctor.Sum
+import           Data.Bifunctor.TH
 import           Data.Map                        (Map)
 import qualified Data.Map                        as Map
 import           Data.String                     (IsString (..))

diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
@@ -1,6 +1,6 @@
+{-# LANGUAGE DataKinds         #-}
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures    #-}
 {-# LANGUAGE LambdaCase        #-}
 {-# LANGUAGE PatternSynonyms   #-}
@@ -29,19 +29,19 @@
 -- so only wildcard patterns and variable patterns are handled in this implementation.
 module Language.LambdaPi.Impl.FreeFoilTH where
 
-import System.Exit (exitFailure)
-import Data.String (IsString(..))
-import qualified Control.Monad.Foil           as Foil
+import qualified Control.Monad.Foil              as Foil
 import           Control.Monad.Free.Foil
 import           Control.Monad.Free.Foil.TH
 import           Data.Bifunctor.TH
-import           Data.Map                     (Map)
-import qualified Data.Map as Map
-import qualified Language.LambdaPi.Syntax.Abs as Raw
-import qualified Language.LambdaPi.Syntax.Par as Raw
-import qualified Language.LambdaPi.Syntax.Lex as Raw
+import           Data.Map                        (Map)
+import qualified Data.Map                        as Map
+import           Data.String                     (IsString (..))
+import qualified Language.LambdaPi.Syntax.Abs    as Raw
 import qualified Language.LambdaPi.Syntax.Layout as Raw
-import qualified Language.LambdaPi.Syntax.Print as Raw
+import qualified Language.LambdaPi.Syntax.Lex    as Raw
+import qualified Language.LambdaPi.Syntax.Par    as Raw
+import qualified Language.LambdaPi.Syntax.Print  as Raw
+import           System.Exit                     (exitFailure)
 
 -- $setup
 -- >>> :set -XOverloadedStrings
@@ -104,7 +104,7 @@ fromTerm' = convertFromAST
 -- λ x0 . λ x1 . λ x2 . x2
 instance IsString (AST (Term'Sig Raw.BNFC'Position) Foil.VoidS) where
   fromString input = case Raw.pTerm (Raw.tokens input) of
-    Left err -> error ("could not parse λΠ-term: " <> input <> "\n  " <> err)
+    Left err   -> error ("could not parse λΠ-term: " <> input <> "\n  " <> err)
     Right term -> toTerm'Closed term
 
 -- | Pretty-print scope-safe terms via raw representation.
@@ -153,13 +153,16 @@ whnf scope = \case
   First loc t ->
     case whnf scope t of
       Pair _loc l _r -> whnf scope l
-      t' -> First loc t'
+      t'             -> First loc t'
   Second loc t ->
     case whnf scope t of
       Pair _loc _l r -> whnf scope r
-      t' -> Second loc t'
+      t'             -> Second loc t'
   t -> t
 
+-- ** Type checking
+
+
 -- ** λΠ-interpreter
 
 -- | Interpret a λΠ command.