From a7159620d87cc8503c2d419b7eeec17662816d63 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 26 Jun 2024 16:55:28 +0200
Subject: [PATCH 1/9] style

---
 src/Juvix/Compiler/Concrete/Print/Base.hs | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 2fd4c1587d..dea867b569 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -39,7 +39,9 @@ import Juvix.Prelude.Pretty qualified as P
 --- * the body of a `Top` iterator,
 --- * the else branch body of a `Top` if expression,
 --- * the last branch body of a `Top` case expresssion.
-data IsTop = Top | NotTop
+data IsTop
+  = Top
+  | NotTop
 
 type PrettyPrintingMaybe a = forall r. (Members '[ExactPrint, Reader Options] r) => a -> Maybe (Sem r ())
 
@@ -60,11 +62,10 @@ instance PrettyPrint KeywordRef where
   ppCode p =
     morphemeM
       (getLoc p)
-      ( annotated (C.kwTypeAnn (p ^. keywordRefKeyword . keywordType))
-          . noLoc
-          . pretty
-          $ p
-      )
+      . annotated (C.kwTypeAnn (p ^. keywordRefKeyword . keywordType))
+      . noLoc
+      . pretty
+      $ p
 
 docNoComments :: (PrettyPrint c) => Options -> c -> Doc Ann
 docNoComments = docHelper Nothing

From 154bc023d8b372f0b525a0739bf8578cbd9bdb74 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 26 Jun 2024 19:50:09 +0200
Subject: [PATCH 2/9] wip

---
 src/Juvix/Compiler/Concrete/Data/Rename.hs    | 96 +++++++++++++++++++
 .../FromSource/ParserResultBuilder.hs         |  9 ++
 src/Juvix/Parser/Lexer.hs                     |  9 +-
 src/Juvix/Prelude/Parsing.hs                  |  7 ++
 4 files changed, 118 insertions(+), 3 deletions(-)
 create mode 100644 src/Juvix/Compiler/Concrete/Data/Rename.hs

diff --git a/src/Juvix/Compiler/Concrete/Data/Rename.hs b/src/Juvix/Compiler/Concrete/Data/Rename.hs
new file mode 100644
index 0000000000..67b7660aad
--- /dev/null
+++ b/src/Juvix/Compiler/Concrete/Data/Rename.hs
@@ -0,0 +1,96 @@
+module Juvix.Compiler.Concrete.Data.Rename where
+
+import Data.Text qualified as Text
+import Juvix.Compiler.Concrete.Data.ScopedName
+import Juvix.Compiler.Concrete.Translation.FromSource.Lexer qualified as L
+import Juvix.Compiler.Concrete.Translation.FromSource.ParserResultBuilder (ParserResultBuilder, ignoreParserResultBuilder)
+import Juvix.Data.Keyword.All qualified as Kw
+import Juvix.Prelude.Base
+import Juvix.Prelude.Pretty
+import Juvix.Prelude.Parsing
+
+data RenameCondition = RenameCondition
+  { _renamePackageName :: Maybe Text,
+    _renameModulePath :: Maybe Text,
+    _renameOldName :: Text
+  }
+  deriving stock (Show, Eq, Ord, Generic, Data)
+
+data Rename = Rename
+  { _renameCondition :: RenameCondition,
+    _renameNewName :: Text
+  }
+  deriving stock (Show, Eq, Ord, Generic, Data)
+
+makeLenses ''Rename
+makeLenses ''RenameCondition
+
+instance Hashable RenameCondition
+
+instance Hashable Rename
+
+checkRenameCondition :: RenameCondition -> Name' n -> Bool
+checkRenameCondition RenameCondition {..} n =
+  checkEq _renameModulePath (modId ^. moduleIdPath)
+    && checkEq _renamePackageName (modId ^. moduleIdPackage)
+    && checkEq _renamePackageName (n ^. nameVerbatim)
+  where
+    modId :: ModuleId
+    modId = n ^. nameId . nameIdModuleId
+    checkEq :: Maybe Text -> Text -> Bool
+    checkEq mt1 t2 = case mt1 of
+      Nothing -> True
+      Just t1 -> t1 == t2
+
+instance Pretty RenameCondition where
+
+instance Pretty Rename where
+  pretty Rename {..} = undefined
+
+{--| Rename syntax:
+<packageName>:<modulePath>:<oldname> => <newname>
+
+Examples:
+stdlib:Stdlib.Function:if -> ite
+\*:Stdlib.Function:if -> ite
+
+note that the space before '->' is mandatory because - is not a reserved symbol.
+--}
+
+parseRename :: Text -> Either Text Rename
+parseRename = parseHelperSem parser (run . ignoreParserResultBuilder)
+  where
+    parser :: forall r. (Members '[ParserResultBuilder] r) => ParsecS r Rename
+    parser = do
+      L.whiteSpace
+      _renamePackageName <- stringHelper L.identifier
+      L.kw Kw.kwColon
+      _renameModulePath <- stringHelper pmodulePath
+      L.kw Kw.kwColon
+      _renameOldName <- L.identifier
+      L.kw Kw.kwMapsTo
+      _renameNewName <- L.identifier
+      eof
+      let _renameCondition =
+            RenameCondition
+              { _renamePackageName,
+                _renameModulePath,
+                _renameOldName
+              }
+      return
+        Rename
+          { _renameCondition,
+            _renameNewName
+          }
+      where
+        pmodulePath :: ParsecS r Text
+        pmodulePath =
+          Text.intercalate "."
+            . fmap fst
+            . toList
+            <$> L.dottedIdentifier
+
+        stringHelper :: ParsecS r Text -> ParsecS r (Maybe Text)
+        stringHelper p =
+          char '*' $> Nothing
+            <|> Just <$> p
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs
index 98ac443ada..ce8477caca 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs
+++ b/src/Juvix/Compiler/Concrete/Translation/FromSource/ParserResultBuilder.hs
@@ -75,6 +75,15 @@ execParserResultBuilder ::
   Sem r ParserState
 execParserResultBuilder s = fmap fst . runParserResultBuilder s
 
+ignoreParserResultBuilder ::
+  Sem (ParserResultBuilder ': r) a ->
+  Sem r a
+ignoreParserResultBuilder =
+  interpret $ \case
+    RegisterImport {} -> return ()
+    RegisterItem {} -> return ()
+    RegisterSpaceSpan {} -> return ()
+
 runParserResultBuilder ::
   (Member HighlightBuilder r) =>
   ParserState ->
diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs
index cffbf31ee1..fc3141053c 100644
--- a/src/Juvix/Parser/Lexer.hs
+++ b/src/Juvix/Parser/Lexer.hs
@@ -1,6 +1,10 @@
 -- | This module contains lexing functions common to all parsers in the pipeline
 -- (Juvix, JuvixCore, JuvixAsm).
-module Juvix.Parser.Lexer where
+module Juvix.Parser.Lexer
+  ( module Juvix.Parser.Lexer,
+    module Juvix.Prelude.Parsing,
+  )
+where
 
 import Data.HashSet qualified as HashSet
 import Data.Set qualified as Set
@@ -10,11 +14,10 @@ import Juvix.Compiler.Concrete.Data.Literal
 import Juvix.Data.Keyword
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude
+import Juvix.Prelude.Parsing (ParsecS)
 import Juvix.Prelude.Parsing as P hiding (hspace, space, space1)
 import Text.Megaparsec.Char.Lexer qualified as L
 
-type ParsecS r = ParsecT Void Text (Sem r)
-
 parseFailure :: Int -> String -> ParsecS r a
 parseFailure off str = P.parseError $ P.FancyError off (Set.singleton (P.ErrorFail str))
 
diff --git a/src/Juvix/Prelude/Parsing.hs b/src/Juvix/Prelude/Parsing.hs
index 3395b8b272..be1218a0f1 100644
--- a/src/Juvix/Prelude/Parsing.hs
+++ b/src/Juvix/Prelude/Parsing.hs
@@ -16,7 +16,14 @@ import Juvix.Prelude.Pretty
 import Text.Megaparsec hiding (sepBy1, sepEndBy1, some)
 import Text.Megaparsec.Char
 
+type ParsecS r = ParsecT Void Text (Sem r)
+
 parseHelper :: (TraversableStream txt, VisualStream txt) => Parsec Void txt a -> txt -> Either Text a
 parseHelper p t = case runParser p "<input>" t of
   Left (err :: ParseErrorBundle txt Void) -> Left (prettyText (errorBundlePretty err))
   Right r -> return r
+
+parseHelperSem :: ParsecS r a -> (forall x. Sem r x -> x) -> Text -> Either Text a
+parseHelperSem p runS t = case runS (runParserT p "<input>" t) of
+  Left (err :: ParseErrorBundle txt Void) -> Left (prettyText (errorBundlePretty err))
+  Right r -> return r

From 0a7c38750823c5ce9ece319500cd83eb68271736 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 26 Jun 2024 20:00:46 +0200
Subject: [PATCH 3/9] parse and pretty

---
 src/Juvix/Compiler/Concrete/Data/Rename.hs | 38 +++++++++++++++++-----
 1 file changed, 29 insertions(+), 9 deletions(-)

diff --git a/src/Juvix/Compiler/Concrete/Data/Rename.hs b/src/Juvix/Compiler/Concrete/Data/Rename.hs
index 67b7660aad..f6b8bc61aa 100644
--- a/src/Juvix/Compiler/Concrete/Data/Rename.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Rename.hs
@@ -5,9 +5,10 @@ import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Compiler.Concrete.Translation.FromSource.Lexer qualified as L
 import Juvix.Compiler.Concrete.Translation.FromSource.ParserResultBuilder (ParserResultBuilder, ignoreParserResultBuilder)
 import Juvix.Data.Keyword.All qualified as Kw
+import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude.Base
-import Juvix.Prelude.Pretty
 import Juvix.Prelude.Parsing
+import Juvix.Prelude.Pretty
 
 data RenameCondition = RenameCondition
   { _renamePackageName :: Maybe Text,
@@ -43,16 +44,30 @@ checkRenameCondition RenameCondition {..} n =
       Just t1 -> t1 == t2
 
 instance Pretty RenameCondition where
+  pretty RenameCondition {..} =
+    helper _renamePackageName
+      <> pretty Kw.delimSemicolon
+      <> helper _renameModulePath
+      <> pretty Kw.delimSemicolon
+      <> pretty _renameOldName
+    where
+      helper :: Maybe Text -> Doc a
+      helper = maybe Str.underscore pretty
 
 instance Pretty Rename where
-  pretty Rename {..} = undefined
+  pretty Rename {..} =
+    pretty _renameCondition
+      <> " "
+      <> pretty Kw.kwMapsTo
+      <> " "
+      <> pretty _renameNewName
 
 {--| Rename syntax:
-<packageName>:<modulePath>:<oldname> => <newname>
+<packageName>;<modulePath>;<oldname> -> <newname>
 
 Examples:
-stdlib:Stdlib.Function:if -> ite
-\*:Stdlib.Function:if -> ite
+stdlib;Stdlib.Function;if -> ite
+_;Stdlib.Function;if -> ite
 
 note that the space before '->' is mandatory because - is not a reserved symbol.
 --}
@@ -64,9 +79,9 @@ parseRename = parseHelperSem parser (run . ignoreParserResultBuilder)
     parser = do
       L.whiteSpace
       _renamePackageName <- stringHelper L.identifier
-      L.kw Kw.kwColon
+      L.kw Kw.delimSemicolon
       _renameModulePath <- stringHelper pmodulePath
-      L.kw Kw.kwColon
+      L.kw Kw.delimSemicolon
       _renameOldName <- L.identifier
       L.kw Kw.kwMapsTo
       _renameNewName <- L.identifier
@@ -85,12 +100,17 @@ parseRename = parseHelperSem parser (run . ignoreParserResultBuilder)
       where
         pmodulePath :: ParsecS r Text
         pmodulePath =
-          Text.intercalate "."
+          Text.intercalate Str.dot
             . fmap fst
             . toList
             <$> L.dottedIdentifier
 
         stringHelper :: ParsecS r Text -> ParsecS r (Maybe Text)
         stringHelper p =
-          char '*' $> Nothing
+          chunk Str.underscore $> Nothing
             <|> Just <$> p
+
+tt :: Text -> IO ()
+tt t = case parseRename t of
+  Left err -> putStrLn err
+  Right x -> putStrLn (prettyText x)

From 99938fb1e68824808e51b995c951e99603036397 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 26 Jun 2024 20:02:32 +0200
Subject: [PATCH 4/9] add comment

---
 src/Juvix/Compiler/Concrete/Data/Rename.hs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/Juvix/Compiler/Concrete/Data/Rename.hs b/src/Juvix/Compiler/Concrete/Data/Rename.hs
index f6b8bc61aa..8b7f54a936 100644
--- a/src/Juvix/Compiler/Concrete/Data/Rename.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Rename.hs
@@ -70,6 +70,9 @@ stdlib;Stdlib.Function;if -> ite
 _;Stdlib.Function;if -> ite
 
 note that the space before '->' is mandatory because - is not a reserved symbol.
+
+It should be that:
+forall r :: Rename. parseRename (prettyText r) == r
 --}
 
 parseRename :: Text -> Either Text Rename

From 5c1a536cb4e5e5210956f4404001430854df70b9 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 26 Jun 2024 21:54:56 +0200
Subject: [PATCH 5/9] sync

---
 app/Commands/Format/Options.hs                |  9 ++++++++-
 app/CommonOptions.hs                          | 16 ++++++++++++++++
 src/Juvix/Compiler/Concrete/Pretty/Options.hs | 10 +++++++++-
 3 files changed, 33 insertions(+), 2 deletions(-)

diff --git a/app/Commands/Format/Options.hs b/app/Commands/Format/Options.hs
index 65729e4c3b..646f237177 100644
--- a/app/Commands/Format/Options.hs
+++ b/app/Commands/Format/Options.hs
@@ -1,9 +1,15 @@
-module Commands.Format.Options where
+module Commands.Format.Options
+  ( module Commands.Format.Options,
+    module Juvix.Compiler.Concrete.Data.Rename,
+  )
+where
 
 import CommonOptions
+import Juvix.Compiler.Concrete.Data.Rename
 
 data FormatOptions = FormatOptions
   { _formatInput :: Maybe (AppPath FileOrDir),
+    _formatRename :: Maybe Rename,
     _formatCheck :: Bool,
     _formatInPlace :: Bool
   }
@@ -26,6 +32,7 @@ parseInputFileOrDir = do
 parseFormat :: Parser FormatOptions
 parseFormat = do
   _formatInput <- optional parseInputFileOrDir
+  _formatRename <- optional parseOptRename
   _formatCheck <-
     switch
       ( long "check"
diff --git a/app/CommonOptions.hs b/app/CommonOptions.hs
index e1f1c33003..a720ae5752 100644
--- a/app/CommonOptions.hs
+++ b/app/CommonOptions.hs
@@ -11,6 +11,7 @@ import Control.Exception qualified as GHC
 import Data.List.NonEmpty qualified as NonEmpty
 import GHC.Conc
 import Juvix.Compiler.Casm.Data.TransformationId.Parser qualified as Casm
+import Juvix.Compiler.Concrete.Data.Rename
 import Juvix.Compiler.Concrete.Translation.ImportScanner
 import Juvix.Compiler.Core.Data.TransformationId.Parser qualified as Core
 import Juvix.Compiler.Pipeline.EntryPoint
@@ -101,6 +102,15 @@ parseGenericInputFile = do
       )
   pure AppPath {_pathIsInput = True, ..}
 
+parseOptRename :: Parser Rename
+parseOptRename =
+  option
+    renameOpt
+    ( long "dev-rename"
+        <> metavar "RENAME_SPEC"
+        <> help "Rename an identifier while formatting"
+    )
+
 parseGenericOutputFile :: Parser (AppPath File)
 parseGenericOutputFile = do
   _pathPath <-
@@ -136,6 +146,12 @@ somePreFileOrDirOpt = mkPrepath <$> str
 somePreFileOpt :: ReadM (Prepath File)
 somePreFileOpt = mkPrepath <$> str
 
+renameOpt :: ReadM Rename
+renameOpt = eitherReader aux
+  where
+    aux :: String -> Either String Rename
+    aux = mapLeft unpack . parseRename . pack
+
 someFileOpt :: ReadM (SomeBase File)
 someFileOpt = eitherReader aux
   where
diff --git a/src/Juvix/Compiler/Concrete/Pretty/Options.hs b/src/Juvix/Compiler/Concrete/Pretty/Options.hs
index 4ed4f99ec1..760782e633 100644
--- a/src/Juvix/Compiler/Concrete/Pretty/Options.hs
+++ b/src/Juvix/Compiler/Concrete/Pretty/Options.hs
@@ -1,10 +1,16 @@
-module Juvix.Compiler.Concrete.Pretty.Options where
+module Juvix.Compiler.Concrete.Pretty.Options
+  ( module Juvix.Compiler.Concrete.Pretty.Options,
+    module Juvix.Compiler.Concrete.Data.Rename,
+  )
+where
 
+import Juvix.Compiler.Concrete.Data.Rename
 import Juvix.Prelude
 
 data Options = Options
   { _optShowNameIds :: Bool,
     _optInJudocBlock :: Bool,
+    _optRenames :: [Rename],
     _optPrintPragmas :: Bool
   }
 
@@ -13,6 +19,7 @@ defaultOptions =
   Options
     { _optShowNameIds = False,
       _optInJudocBlock = False,
+      _optRenames = [],
       _optPrintPragmas = True
     }
 
@@ -21,6 +28,7 @@ traceOptions =
   Options
     { _optShowNameIds = True,
       _optInJudocBlock = False,
+      _optRenames = [],
       _optPrintPragmas = True
     }
 

From 747af716bb72b62719fbf6f25b1bdf0b38c66119 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 26 Jun 2024 23:18:41 +0200
Subject: [PATCH 6/9] apply rename in pretty printer

---
 app/Commands/Format.hs                     |  7 ++++++-
 src/Juvix/Compiler/Concrete/Data/Rename.hs |  8 +++++++-
 src/Juvix/Compiler/Concrete/Print/Base.hs  | 11 ++++++++---
 src/Juvix/Formatter.hs                     | 10 +++++++---
 4 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/app/Commands/Format.hs b/app/Commands/Format.hs
index d40fef91e7..cfbd1ad1e4 100644
--- a/app/Commands/Format.hs
+++ b/app/Commands/Format.hs
@@ -5,6 +5,7 @@ import Commands.Format.Options
 import Data.Text qualified as Text
 import Juvix.Compiler.Pipeline.Driver (processModule)
 import Juvix.Compiler.Pipeline.Loader.PathResolver.ImportTree.Base
+import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Pipeline.ModuleInfoCache
 import Juvix.Compiler.Store.Language (ModuleInfo)
 import Juvix.Formatter
@@ -69,7 +70,11 @@ runCommand :: forall r. (Members '[EmbedIO, App, TaggedLock, Files] r) => Format
 runCommand opts = do
   target <- targetFromOptions opts
   runOutputSem (renderFormattedOutput target opts) . runScopeFileApp $ do
-    res <- case target of
+    let printOpts =
+          defaultOptions
+            { _optRenames = maybe [] pure (opts ^. formatRename)
+            }
+    res <- runReader printOpts $ case target of
       TargetFile p -> format p
       TargetProject -> formatProject
       TargetStdin -> do
diff --git a/src/Juvix/Compiler/Concrete/Data/Rename.hs b/src/Juvix/Compiler/Concrete/Data/Rename.hs
index 8b7f54a936..43acc7cb48 100644
--- a/src/Juvix/Compiler/Concrete/Data/Rename.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Rename.hs
@@ -30,14 +30,20 @@ instance Hashable RenameCondition
 
 instance Hashable Rename
 
+applyRename :: Name' n -> Rename -> Maybe Text
+applyRename n r
+  | checkRenameCondition (r ^. renameCondition) n = Just (r ^. renameNewName)
+  | otherwise = Nothing
+
 checkRenameCondition :: RenameCondition -> Name' n -> Bool
 checkRenameCondition RenameCondition {..} n =
   checkEq _renameModulePath (modId ^. moduleIdPath)
     && checkEq _renamePackageName (modId ^. moduleIdPackage)
-    && checkEq _renamePackageName (n ^. nameVerbatim)
+    && checkEq (Just _renameOldName) (n ^. nameVerbatim)
   where
     modId :: ModuleId
     modId = n ^. nameId . nameIdModuleId
+
     checkEq :: Maybe Text -> Text -> Bool
     checkEq mt1 t2 = case mt1 of
       Nothing -> True
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index dea867b569..26769bb314 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -28,7 +28,7 @@ import Juvix.Data.Keyword.All qualified as Kw
 import Juvix.Data.NameKind
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude hiding ((<+>), (<+?>), (<?+>), (?<>))
-import Juvix.Prelude.Pretty (annotate, pretty)
+import Juvix.Prelude.Pretty (annotate, pretty, prettyText)
 import Juvix.Prelude.Pretty qualified as P
 
 --- An expression is `Top` if it is:
@@ -468,8 +468,13 @@ instance PrettyPrint TopModulePath where
 
 instance (PrettyPrint n) => PrettyPrint (S.Name' n) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => S.Name' n -> Sem r ()
-  ppCode S.Name' {..} = do
-    let nameConcrete' = region (C.annotateKind _nameKind) (ppCode _nameConcrete)
+  ppCode sn@S.Name' {..} = do
+    renames <- asks (^. optRenames)
+    -- TODO qualified names are not currently handled properly
+    let renameText :: Maybe (Doc Ann) = pretty <$> firstJust (applyRename sn) renames
+        nameConcrete' =
+          region (C.annotateKind _nameKind) $
+            maybe (ppCode _nameConcrete) noLoc renameText
     annSRef (withNameIdSuffix _nameId nameConcrete')
     where
       annSRef :: Sem r () -> Sem r ()
diff --git a/src/Juvix/Formatter.hs b/src/Juvix/Formatter.hs
index 08b973b547..f5bcb20b20 100644
--- a/src/Juvix/Formatter.hs
+++ b/src/Juvix/Formatter.hs
@@ -5,6 +5,7 @@ module Juvix.Formatter where
 import Juvix.Compiler.Concrete.Data.Highlight.Input (ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Print (ppOutDefault)
+import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping (ScoperResult, getModuleId, scopeCheck)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource (ParserResult, fromSource)
@@ -67,7 +68,7 @@ instance Monoid FormatResult where
 -- contents of the file.
 format ::
   forall r.
-  (Members '[ScopeEff, Files, Output FormattedFileInfo] r) =>
+  (Members '[ScopeEff, Reader Options, Files, Output FormattedFileInfo] r) =>
   Path Abs File ->
   Sem r FormatResult
 format p = do
@@ -154,7 +155,7 @@ formatPath p = do
 
 formatStdin ::
   forall r.
-  (Members '[Reader EntryPoint, ScopeEff, Files, Output FormattedFileInfo] r) =>
+  (Members '[Reader EntryPoint, Reader Options, ScopeEff, Files, Output FormattedFileInfo] r) =>
   Sem r FormatResult
 formatStdin = do
   entry <- ask
@@ -189,7 +190,10 @@ formatResultSourceCode filepath src = do
 formatScoperResult' ::
   Bool -> Text -> Scoper.ScoperResult -> Text
 formatScoperResult' forceFormat original sres =
-  run . runReader original $ formatScoperResult forceFormat sres
+  run
+    . runReader original
+    . runReader defaultOptions
+    $ formatScoperResult forceFormat sres
 
 formatScoperResult ::
   (Members '[Reader OriginalSource] r) =>

From bd9eac533b5907ef6e7e997c00941755789757c0 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 1 Jul 2024 18:15:40 +0200
Subject: [PATCH 7/9] fix rebase

---
 app/Commands/Format.hs                     |  2 +-
 src/Juvix/Compiler/Concrete/Data/Rename.hs | 21 ++++++++++-----------
 src/Juvix/Compiler/Concrete/Print/Base.hs  |  2 +-
 src/Juvix/Formatter.hs                     |  2 +-
 4 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/app/Commands/Format.hs b/app/Commands/Format.hs
index cfbd1ad1e4..7b8ea3cdd0 100644
--- a/app/Commands/Format.hs
+++ b/app/Commands/Format.hs
@@ -3,9 +3,9 @@ module Commands.Format where
 import Commands.Base
 import Commands.Format.Options
 import Data.Text qualified as Text
+import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Pipeline.Driver (processModule)
 import Juvix.Compiler.Pipeline.Loader.PathResolver.ImportTree.Base
-import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Compiler.Pipeline.ModuleInfoCache
 import Juvix.Compiler.Store.Language (ModuleInfo)
 import Juvix.Formatter
diff --git a/src/Juvix/Compiler/Concrete/Data/Rename.hs b/src/Juvix/Compiler/Concrete/Data/Rename.hs
index 43acc7cb48..60f1eb0276 100644
--- a/src/Juvix/Compiler/Concrete/Data/Rename.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Rename.hs
@@ -1,10 +1,10 @@
 module Juvix.Compiler.Concrete.Data.Rename where
 
-import Data.Text qualified as Text
 import Juvix.Compiler.Concrete.Data.ScopedName
 import Juvix.Compiler.Concrete.Translation.FromSource.Lexer qualified as L
 import Juvix.Compiler.Concrete.Translation.FromSource.ParserResultBuilder (ParserResultBuilder, ignoreParserResultBuilder)
 import Juvix.Data.Keyword.All qualified as Kw
+import Juvix.Data.TopModulePathKey
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude.Base
 import Juvix.Prelude.Parsing
@@ -12,7 +12,7 @@ import Juvix.Prelude.Pretty
 
 data RenameCondition = RenameCondition
   { _renamePackageName :: Maybe Text,
-    _renameModulePath :: Maybe Text,
+    _renameModulePath :: Maybe TopModulePathKey,
     _renameOldName :: Text
   }
   deriving stock (Show, Eq, Ord, Generic, Data)
@@ -44,7 +44,7 @@ checkRenameCondition RenameCondition {..} n =
     modId :: ModuleId
     modId = n ^. nameId . nameIdModuleId
 
-    checkEq :: Maybe Text -> Text -> Bool
+    checkEq :: (Eq a) => Maybe a -> a -> Bool
     checkEq mt1 t2 = case mt1 of
       Nothing -> True
       Just t1 -> t1 == t2
@@ -57,7 +57,7 @@ instance Pretty RenameCondition where
       <> pretty Kw.delimSemicolon
       <> pretty _renameOldName
     where
-      helper :: Maybe Text -> Doc a
+      helper :: (Pretty str) => Maybe str -> Doc a
       helper = maybe Str.underscore pretty
 
 instance Pretty Rename where
@@ -87,9 +87,9 @@ parseRename = parseHelperSem parser (run . ignoreParserResultBuilder)
     parser :: forall r. (Members '[ParserResultBuilder] r) => ParsecS r Rename
     parser = do
       L.whiteSpace
-      _renamePackageName <- stringHelper L.identifier
+      _renamePackageName <- optionalHelper L.identifier
       L.kw Kw.delimSemicolon
-      _renameModulePath <- stringHelper pmodulePath
+      _renameModulePath <- optionalHelper pmodulePath
       L.kw Kw.delimSemicolon
       _renameOldName <- L.identifier
       L.kw Kw.kwMapsTo
@@ -107,15 +107,14 @@ parseRename = parseHelperSem parser (run . ignoreParserResultBuilder)
             _renameNewName
           }
       where
-        pmodulePath :: ParsecS r Text
+        pmodulePath :: ParsecS r TopModulePathKey
         pmodulePath =
-          Text.intercalate Str.dot
+          nonEmptyToTopModulePathKey
             . fmap fst
-            . toList
             <$> L.dottedIdentifier
 
-        stringHelper :: ParsecS r Text -> ParsecS r (Maybe Text)
-        stringHelper p =
+        optionalHelper :: ParsecS r a -> ParsecS r (Maybe a)
+        optionalHelper p =
           chunk Str.underscore $> Nothing
             <|> Just <$> p
 
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index 26769bb314..50335aae02 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -28,7 +28,7 @@ import Juvix.Data.Keyword.All qualified as Kw
 import Juvix.Data.NameKind
 import Juvix.Extra.Strings qualified as Str
 import Juvix.Prelude hiding ((<+>), (<+?>), (<?+>), (?<>))
-import Juvix.Prelude.Pretty (annotate, pretty, prettyText)
+import Juvix.Prelude.Pretty (annotate, pretty)
 import Juvix.Prelude.Pretty qualified as P
 
 --- An expression is `Top` if it is:
diff --git a/src/Juvix/Formatter.hs b/src/Juvix/Formatter.hs
index f5bcb20b20..a1248e262b 100644
--- a/src/Juvix/Formatter.hs
+++ b/src/Juvix/Formatter.hs
@@ -4,8 +4,8 @@ module Juvix.Formatter where
 
 import Juvix.Compiler.Concrete.Data.Highlight.Input (ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Language
-import Juvix.Compiler.Concrete.Print (ppOutDefault)
 import Juvix.Compiler.Concrete.Pretty.Options
+import Juvix.Compiler.Concrete.Print (ppOutDefault)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping (ScoperResult, getModuleId, scopeCheck)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource (ParserResult, fromSource)

From efff3643dd85b186ae4a196dd241cbdb80c4cb12 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 1 Jul 2024 18:28:22 +0200
Subject: [PATCH 8/9] pass options correctly

---
 app/Commands/Format.hs |  2 +-
 src/Juvix/Formatter.hs | 10 ++++++----
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/app/Commands/Format.hs b/app/Commands/Format.hs
index 7b8ea3cdd0..465786d23d 100644
--- a/app/Commands/Format.hs
+++ b/app/Commands/Format.hs
@@ -52,7 +52,7 @@ targetFromOptions opts = do
 -- | Formats the project on the root
 formatProject ::
   forall r.
-  (Members '[App, EmbedIO, TaggedLock, Files, Output FormattedFileInfo] r) =>
+  (Members '[App, EmbedIO, Reader Options, TaggedLock, Files, Output FormattedFileInfo] r) =>
   Sem r FormatResult
 formatProject = runPipelineOptions . runPipelineSetup $ do
   pkg <- askPackage
diff --git a/src/Juvix/Formatter.hs b/src/Juvix/Formatter.hs
index a1248e262b..b0dbd48084 100644
--- a/src/Juvix/Formatter.hs
+++ b/src/Juvix/Formatter.hs
@@ -5,7 +5,7 @@ module Juvix.Formatter where
 import Juvix.Compiler.Concrete.Data.Highlight.Input (ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Pretty.Options
-import Juvix.Compiler.Concrete.Print (ppOutDefault)
+import Juvix.Compiler.Concrete.Print (ppOut)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping (ScoperResult, getModuleId, scopeCheck)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource (ParserResult, fromSource)
@@ -109,6 +109,7 @@ formatModuleInfo ::
   ( Members
       '[ PathResolver,
          Error JuvixError,
+         Reader Options,
          Files,
          Reader Package
        ]
@@ -146,7 +147,7 @@ formatModuleInfo node moduleInfo =
         forcesField sourceCodeOriginal
 
 formatPath ::
-  (Members '[Reader OriginalSource, ScopeEff] r) =>
+  (Members '[Reader Options, Reader OriginalSource, ScopeEff] r) =>
   Path Abs File ->
   Sem r Text
 formatPath p = do
@@ -196,13 +197,14 @@ formatScoperResult' forceFormat original sres =
     $ formatScoperResult forceFormat sres
 
 formatScoperResult ::
-  (Members '[Reader OriginalSource] r) =>
+  (Members '[Reader Options, Reader OriginalSource] r) =>
   Bool ->
   Scoper.ScoperResult ->
   Sem r Text
 formatScoperResult forceFormat res = do
+  opts :: Options <- ask
   let comments = Scoper.getScoperResultComments res
-      formattedTxt = toPlainTextTrim (ppOutDefault comments (res ^. Scoper.resultModule))
+      formattedTxt = toPlainTextTrim (ppOut opts comments (res ^. Scoper.resultModule))
   runFailDefault formattedTxt $ do
     pragmas <- failMaybe (res ^. Scoper.mainModule . modulePragmas)
     PragmaFormat {..} <- failMaybe (pragmas ^. withLocParam . withSourceValue . pragmasFormat)

From 95027d15da75cd47de8d8872eda703bb51db3b5e Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Mon, 1 Jul 2024 19:05:06 +0200
Subject: [PATCH 9/9] add reader

---
 test/Formatter/Positive.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test/Formatter/Positive.hs b/test/Formatter/Positive.hs
index b5f5a77228..778142dabe 100644
--- a/test/Formatter/Positive.hs
+++ b/test/Formatter/Positive.hs
@@ -1,6 +1,7 @@
 module Formatter.Positive where
 
 import Base
+import Juvix.Compiler.Concrete.Pretty.Options
 import Juvix.Formatter
 import Scope.Positive qualified
 import Scope.Positive qualified as Scope
@@ -26,6 +27,7 @@ makeFormatTest' Scope.PosTest {..} =
                 . runError
                 . runOutputList @FormattedFileInfo
                 . runScopeEffIO tRoot
+                . runReader defaultOptions
                 . runFilesIO
                 $ format file'
             case d of