From 13b133fb62dc476f6553e96f6265246d7ea15930 Mon Sep 17 00:00:00 2001
From: Nikolai Kudasov <nickolay.kudasov@gmail.com>
Date: Sat, 26 Oct 2024 20:03:39 +0300
Subject: [PATCH] Cleanup

---
 .../Control/Monad/Free/Foil/TH/MkFreeFoil.hs  |  6 ++--
 .../src/Language/LambdaPi/Impl/FreeFoilTH.hs  | 36 ++++++++++---------
 haskell/soas/soas.cabal                       |  1 +
 3 files changed, 23 insertions(+), 20 deletions(-)

diff --git a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs
index 128f1bb1..997fc01f 100644
--- a/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs
+++ b/haskell/free-foil/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs
@@ -475,8 +475,8 @@ toFreeFoilClauseFromBinding config termConfig@FreeFoilTermConfig{..} rawRetType
       ForallC _params _ctx con -> go con
       RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType)
 
-toFreeFoilClauseFromQualified :: Name -> FreeFoilConfig -> Type -> Con -> Q [Clause]
-toFreeFoilClauseFromQualified rawTypeName config rawRetType = go
+toFreeFoilClauseFromQualified :: FreeFoilConfig -> Type -> Con -> Q [Clause]
+toFreeFoilClauseFromQualified config rawRetType = go
   where
     go = \case
       GadtC conNames rawArgTypes rawRetType' -> concat <$> do
@@ -676,7 +676,7 @@ mkFreeFoilConversions config@FreeFoilConfig{..} = concat <$> sequence
           safeType = toFreeFoilType SortTerm config (VarT outerScope) (VarT innerScope) rawType
       addModFinalizer $ putDoc (DeclDoc funName)
         ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Convert from scope-safe to raw representation.")
-      clauses <- concat <$> mapM (toFreeFoilClauseFromQualified rawName config rawType) cons
+      clauses <- concat <$> mapM (toFreeFoilClauseFromQualified config rawType) cons
       return
         [ SigD funName (AppT (AppT ArrowT safeType) rawType)
         , FunD funName clauses
diff --git a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
index 3acabf45..01040b19 100644
--- a/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
+++ b/haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs
@@ -1,16 +1,16 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# LANGUAGE DataKinds         #-}
-{-# LANGUAGE TypeFamilies         #-}
-{-# LANGUAGE DeriveGeneric         #-}
-{-# LANGUAGE StandaloneDeriving         #-}
-{-# LANGUAGE DeriveTraversable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE GADTs             #-}
-{-# LANGUAGE KindSignatures    #-}
-{-# LANGUAGE LambdaCase        #-}
-{-# LANGUAGE PatternSynonyms   #-}
-{-# LANGUAGE RankNTypes        #-}
-{-# LANGUAGE TemplateHaskell   #-}
+{-# LANGUAGE DataKinds          #-}
+{-# LANGUAGE DeriveGeneric      #-}
+{-# LANGUAGE DeriveTraversable  #-}
+{-# LANGUAGE FlexibleInstances  #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE KindSignatures     #-}
+{-# LANGUAGE LambdaCase         #-}
+{-# LANGUAGE PatternSynonyms    #-}
+{-# LANGUAGE RankNTypes         #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell    #-}
+{-# LANGUAGE TypeFamilies       #-}
 -- | Free foil implementation of the \(\lambda\Pi\)-calculus (with pairs).
 --
 -- Free foil provides __general__ definitions or implementations for the following:
@@ -38,20 +38,20 @@ module Language.LambdaPi.Impl.FreeFoilTH where
 import qualified Control.Monad.Foil              as Foil
 import           Control.Monad.Foil.TH
 import           Control.Monad.Free.Foil
+import           Control.Monad.Free.Foil.Generic
 import           Control.Monad.Free.Foil.TH
 import           Data.Bifunctor.TH
 import           Data.Map                        (Map)
 import qualified Data.Map                        as Map
 import           Data.String                     (IsString (..))
+import           Generics.Kind.TH                (deriveGenericK)
+import qualified GHC.Generics                    as GHC
 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 qualified Language.LambdaPi.Syntax.Par    as Raw
 import qualified Language.LambdaPi.Syntax.Print  as Raw
 import           System.Exit                     (exitFailure)
-import Control.Monad.Free.Foil.Generic
-import Generics.Kind.TH (deriveGenericK)
-import qualified GHC.Generics as GHC
 
 
 -- $setup
@@ -138,9 +138,11 @@ fromTerm' :: Term' a n -> Raw.Term' a
 fromTerm' = convertFromAST
   convertFromTerm'Sig
   (Raw.Var (error "location missing"))
-  fromFoilPattern'
+  (fromFoilPattern' mkVarIdent)
   (Raw.AScopedTerm (error "location missing"))
-  (\n -> Raw.VarIdent ("x" ++ show n))
+  mkVarIdent
+  where
+    mkVarIdent n = Raw.VarIdent ("x" ++ show n)
 
 -- | Parse scope-safe terms via raw representation.
 --
diff --git a/haskell/soas/soas.cabal b/haskell/soas/soas.cabal
index 339027c4..9e5ffde8 100644
--- a/haskell/soas/soas.cabal
+++ b/haskell/soas/soas.cabal
@@ -35,6 +35,7 @@ custom-setup
 
 library
   exposed-modules:
+      Language.SOAS.FreeFoilConfig
       Language.SOAS.Impl
       Language.SOAS.Syntax.Abs
       Language.SOAS.Syntax.Lex