Print JuvixCore correctly (#1875)

Print JuvixCore InfoTable in such a way that it can be parsed back by
the JuvixCore parser.

* Depends on PR #1832 
* Depends on PR #1862 
* Closes #1841 
* Adds "JuvixCore print" tests which read the files from
Core/positive/*.jvc, print them, read them back and check if the
evaluation results are preserved.

---------

Co-authored-by: Jan Mas Rovira <[email protected]>

app/Commands/Compile.hs

@@ -6,7 +6,9 @@ import Commands.Dev.Core.Compile.Base qualified as Compile
 import Commands.Extra.Compile qualified as Compile
 import Data.Text.IO qualified as TIO
 import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Core.Pipeline qualified as Core
 import Juvix.Compiler.Core.Pretty qualified as Core
+import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
 
 runCommand :: (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
 runCommand opts@CompileOptions {..} = do
@@ -28,4 +30,5 @@ runCommand opts@CompileOptions {..} = do
 writeCoreFile :: (Members '[Embed IO, App] r) => Compile.PipelineArg -> Sem r ()
 writeCoreFile Compile.PipelineArg {..} = do
   coreFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
-  embed $ TIO.writeFile (toFilePath coreFile) (show $ Core.ppOut Core.defaultOptions {Core._optShowDeBruijnIndices = True} _pipelineArgInfoTable)
+  let tab = Core.toEval _pipelineArgInfoTable
+  embed $ TIO.writeFile (toFilePath coreFile) (show $ Core.ppOutDefault (Core.disambiguateNames tab))

app/Commands/Dev/Core/Eval/Options.hs

@@ -7,7 +7,9 @@ import Juvix.Compiler.Core.Pretty.Options qualified as Core
 data CoreEvalOptions = CoreEvalOptions
   { _coreEvalNoIO :: Bool,
     _coreEvalInputFile :: AppPath File,
-    _coreEvalShowDeBruijn :: Bool
+    _coreEvalShowDeBruijn :: Bool,
+    _coreEvalShowIdentIds :: Bool,
+    _coreEvalNoDisambiguate :: Bool
   }
   deriving stock (Data)
 
@@ -16,14 +18,16 @@ makeLenses ''CoreEvalOptions
 instance CanonicalProjection CoreEvalOptions Core.Options where
   project c =
     Core.defaultOptions
-      { Core._optShowDeBruijnIndices = c ^. coreEvalShowDeBruijn
+      { Core._optShowDeBruijnIndices = c ^. coreEvalShowDeBruijn,
+        Core._optShowIdentIds = c ^. coreEvalShowIdentIds
       }
 
 instance CanonicalProjection CoreEvalOptions Eval.EvalOptions where
   project c =
     Eval.EvalOptions
       { _evalInputFile = c ^. coreEvalInputFile,
-        _evalNoIO = c ^. coreEvalNoIO
+        _evalNoIO = c ^. coreEvalNoIO,
+        _evalNoDisambiguate = c ^. coreEvalNoDisambiguate
       }
 
 parseCoreEvalOptions :: Parser CoreEvalOptions
@@ -34,5 +38,7 @@ parseCoreEvalOptions = do
           <> help "Don't interpret the IO effects"
       )
   _coreEvalShowDeBruijn <- optDeBruijn
+  _coreEvalShowIdentIds <- optIdentIds
+  _coreEvalNoDisambiguate <- optNoDisambiguate
   _coreEvalInputFile <- parseInputJuvixCoreFile
   pure CoreEvalOptions {..}

app/Commands/Dev/Core/FromConcrete.hs

@@ -6,17 +6,20 @@ import Evaluator
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Core.Transformation qualified as Core
+import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNames)
 import Juvix.Compiler.Core.Translation
 
 runCommand :: forall r. Members '[Embed IO, App] r => CoreFromConcreteOptions -> Sem r ()
 runCommand localOpts = do
   tab <- (^. coreResultTable) <$> runPipeline (localOpts ^. coreFromConcreteInputFile) upToCore
   path :: Path Abs File <- someBaseToAbs' (localOpts ^. coreFromConcreteInputFile . pathPath)
-  let tab' :: InfoTable = Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
+  let tab0 :: InfoTable = Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
+      tab' :: InfoTable = if localOpts ^. coreFromConcreteNoDisambiguate then tab0 else disambiguateNames tab0
 
       inInputModule :: IdentifierInfo -> Bool
-      inInputModule _ | not (localOpts ^. coreFromConcreteFilter) = True
-      inInputModule x = (== Just path) . (^? identifierLocation . _Just . intervalFile) $ x
+      inInputModule x
+        | localOpts ^. coreFromConcreteFilter = (== Just path) . (^? identifierLocation . _Just . intervalFile) $ x
+        | otherwise = True
 
       mainIdens :: [IdentifierInfo] =
         sortOn
@@ -34,17 +37,20 @@ runCommand localOpts = do
         find (^. identifierName . to (== s)) mainIdens
 
       goPrint :: Sem r ()
-      goPrint = forM_ nodes printNode
+      goPrint = case localOpts ^. coreFromConcreteSymbolName of
+        Just {} -> printNode (fromMaybe err (getDef selInfo))
+        Nothing -> renderStdOut (Core.ppOut localOpts printTab)
         where
+          printTab :: InfoTable
+          printTab
+            | localOpts ^. coreFromConcreteFilter = filterByFile path tab'
+            | otherwise = tab'
           printNode :: (Text, Core.Node) -> Sem r ()
           printNode (name, node) = do
             renderStdOut (name <> " = ")
             renderStdOut (Core.ppOut localOpts node)
             newline
             newline
-          nodes :: [(Text, Core.Node)]
-            | isJust (localOpts ^. coreFromConcreteSymbolName) = [fromMaybe err (getDef selInfo)]
-            | otherwise = mapMaybe (getDef . Just) mainIdens
 
       goEval :: Sem r ()
       goEval = evalAndPrint localOpts tab' evalNode

app/Commands/Dev/Core/FromConcrete/Options.hs

@@ -8,6 +8,8 @@ import Juvix.Compiler.Core.Pretty.Options qualified as Core
 data CoreFromConcreteOptions = CoreFromConcreteOptions
   { _coreFromConcreteTransformations :: [TransformationId],
     _coreFromConcreteShowDeBruijn :: Bool,
+    _coreFromConcreteShowIdentIds :: Bool,
+    _coreFromConcreteNoDisambiguate :: Bool,
     _coreFromConcreteFilter :: Bool,
     _coreFromConcreteNoIO :: Bool,
     _coreFromConcreteEval :: Bool,
@@ -21,24 +23,24 @@ makeLenses ''CoreFromConcreteOptions
 instance CanonicalProjection CoreFromConcreteOptions Core.Options where
   project c =
     Core.defaultOptions
-      { Core._optShowDeBruijnIndices = c ^. coreFromConcreteShowDeBruijn
+      { Core._optShowDeBruijnIndices = c ^. coreFromConcreteShowDeBruijn,
+        Core._optShowIdentIds = c ^. coreFromConcreteShowIdentIds
       }
 
 instance CanonicalProjection CoreFromConcreteOptions Eval.EvalOptions where
   project c =
     Eval.EvalOptions
       { _evalInputFile = c ^. coreFromConcreteInputFile,
-        _evalNoIO = c ^. coreFromConcreteNoIO
+        _evalNoIO = c ^. coreFromConcreteNoIO,
+        _evalNoDisambiguate = c ^. coreFromConcreteNoDisambiguate
       }
 
 parseCoreFromConcreteOptions :: Parser CoreFromConcreteOptions
 parseCoreFromConcreteOptions = do
   _coreFromConcreteTransformations <- optTransformationIds
-  _coreFromConcreteShowDeBruijn <-
-    switch
-      ( long "show-de-bruijn"
-          <> help "Show variable de Bruijn indices"
-      )
+  _coreFromConcreteShowDeBruijn <- optDeBruijn
+  _coreFromConcreteShowIdentIds <- optIdentIds
+  _coreFromConcreteNoDisambiguate <- optNoDisambiguate
   _coreFromConcreteFilter <-
     switch
       ( long "filter"

app/Commands/Dev/Core/Read.hs

@@ -6,6 +6,7 @@ import Evaluator qualified as Eval
 import Juvix.Compiler.Core.Pretty qualified as Core
 import Juvix.Compiler.Core.Scoper qualified as Scoper
 import Juvix.Compiler.Core.Transformation qualified as Core
+import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
 import Juvix.Compiler.Core.Translation.FromSource qualified as Core
 
 runCommand ::
@@ -21,7 +22,8 @@ runCommand opts = do
   inputFile :: Path Abs File <- someBaseToAbs' sinputFile
   s' <- embed . readFile . toFilePath $ inputFile
   tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
-  let tab' = Core.applyTransformations (project opts ^. coreReadTransformations) tab
+  let tab0 = Core.applyTransformations (project opts ^. coreReadTransformations) tab
+      tab' = if project opts ^. coreReadNoDisambiguate then tab0 else Core.disambiguateNames tab0
   embed (Scoper.scopeTrace tab')
   unless (project opts ^. coreReadNoPrint) $ do
     renderStdOut (Core.ppOut opts tab')

app/Commands/Dev/Core/Read/Options.hs

@@ -9,6 +9,8 @@ import Juvix.Compiler.Core.Pretty.Options qualified as Core
 data CoreReadOptions = CoreReadOptions
   { _coreReadTransformations :: [TransformationId],
     _coreReadShowDeBruijn :: Bool,
+    _coreReadShowIdentIds :: Bool,
+    _coreReadNoDisambiguate :: Bool,
     _coreReadEval :: Bool,
     _coreReadNoPrint :: Bool,
     _coreReadInputFile :: AppPath File
@@ -20,27 +22,33 @@ makeLenses ''CoreReadOptions
 instance CanonicalProjection CoreReadOptions Core.Options where
   project c =
     Core.defaultOptions
-      { Core._optShowDeBruijnIndices = c ^. coreReadShowDeBruijn
+      { Core._optShowDeBruijnIndices = c ^. coreReadShowDeBruijn,
+        Core._optShowIdentIds = c ^. coreReadShowIdentIds
       }
 
 instance CanonicalProjection CoreReadOptions Eval.CoreEvalOptions where
   project c =
     Eval.CoreEvalOptions
       { _coreEvalNoIO = False,
         _coreEvalInputFile = c ^. coreReadInputFile,
-        _coreEvalShowDeBruijn = c ^. coreReadShowDeBruijn
+        _coreEvalShowDeBruijn = c ^. coreReadShowDeBruijn,
+        _coreEvalShowIdentIds = c ^. coreReadShowIdentIds,
+        _coreEvalNoDisambiguate = c ^. coreReadNoDisambiguate
       }
 
 instance CanonicalProjection CoreReadOptions Evaluator.EvalOptions where
   project x =
     Evaluator.EvalOptions
       { _evalNoIO = False,
+        _evalNoDisambiguate = x ^. coreReadNoDisambiguate,
         _evalInputFile = x ^. coreReadInputFile
       }
 
 parseCoreReadOptions :: Parser CoreReadOptions
 parseCoreReadOptions = do
   _coreReadShowDeBruijn <- optDeBruijn
+  _coreReadShowIdentIds <- optIdentIds
+  _coreReadNoDisambiguate <- optNoDisambiguate
   _coreReadNoPrint <-
     switch
       ( long "no-print"

app/Commands/Dev/Core/Repl/Options.hs

@@ -3,8 +3,9 @@ module Commands.Dev.Core.Repl.Options where
 import CommonOptions
 import Juvix.Compiler.Core.Pretty.Options qualified as Core
 
-newtype CoreReplOptions = CoreReplOptions
-  { _coreReplShowDeBruijn :: Bool
+data CoreReplOptions = CoreReplOptions
+  { _coreReplShowDeBruijn :: Bool,
+    _coreReplShowIdentIds :: Bool
   }
   deriving stock (Data)
 
@@ -13,10 +14,12 @@ makeLenses ''CoreReplOptions
 instance CanonicalProjection CoreReplOptions Core.Options where
   project c =
     Core.defaultOptions
-      { Core._optShowDeBruijnIndices = c ^. coreReplShowDeBruijn
+      { Core._optShowDeBruijnIndices = c ^. coreReplShowDeBruijn,
+        Core._optShowIdentIds = c ^. coreReplShowIdentIds
       }
 
 parseCoreReplOptions :: Parser CoreReplOptions
 parseCoreReplOptions = do
   _coreReplShowDeBruijn <- optDeBruijn
+  _coreReplShowIdentIds <- optIdentIds
   pure CoreReplOptions {..}

app/Commands/Eval/Options.hs

@@ -24,7 +24,8 @@ instance CanonicalProjection EvalOptions Eval.EvalOptions where
   project c =
     Eval.EvalOptions
       { _evalInputFile = c ^. evalInputFile,
-        _evalNoIO = c ^. evalNoIO
+        _evalNoIO = c ^. evalNoIO,
+        _evalNoDisambiguate = False
       }
 
 parseEvalOptions :: Parser EvalOptions

app/CommonOptions.hs

@@ -234,6 +234,20 @@ optDeBruijn =
         <> help "Show variable de Bruijn indices"
     )
 
+optIdentIds :: Parser Bool
+optIdentIds =
+  switch
+    ( long "show-ident-ids"
+        <> help "Show identifier IDs"
+    )
+
+optNoDisambiguate :: Parser Bool
+optNoDisambiguate =
+  switch
+    ( long "no-disambiguate"
+        <> help "Don't disambiguate the names of bound variables"
+    )
+
 optTransformationIds :: Parser [TransformationId]
 optTransformationIds =
   option

app/Evaluator.hs

@@ -10,10 +10,12 @@ import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo qualified as Info
 import Juvix.Compiler.Core.Language qualified as Core
 import Juvix.Compiler.Core.Pretty qualified as Core
+import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
 
 data EvalOptions = EvalOptions
   { _evalInputFile :: AppPath File,
-    _evalNoIO :: Bool
+    _evalNoIO :: Bool,
+    _evalNoDisambiguate :: Bool
   }
 
 makeLenses ''EvalOptions
@@ -54,8 +56,10 @@ evalAndPrint opts tab node = do
       | Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
           return ()
     Right node' -> do
-      renderStdOut (Core.ppOut opts node')
+      renderStdOut (Core.ppOut opts node'')
       embed (putStrLn "")
+      where
+        node'' = if project opts ^. evalNoDisambiguate then node' else Core.disambiguateNodeNames tab node'
   where
     defaultLoc :: Sem r Interval
     defaultLoc = singletonInterval . mkInitialLoc <$> someBaseToAbs' f

src/Juvix/Compiler/Asm/Translation/FromSource.hs

@@ -32,7 +32,7 @@ createBuiltinConstr ::
   BuiltinDataTag ->
   Text ->
   Type ->
-  Interval ->
+  Location ->
   ConstructorInfo
 createBuiltinConstr sym btag name ty i =
   let n = builtinConstrArgsNum btag

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -143,3 +143,19 @@ builtinTypeToPrim :: BuiltinType -> BuiltinPrim
 builtinTypeToPrim = \case
   BuiltinTypeInductive b -> BuiltinsInductive b
   BuiltinTypeAxiom b -> BuiltinsAxiom b
+
+isNatBuiltin :: BuiltinFunction -> Bool
+isNatBuiltin = \case
+  BuiltinNatPlus -> True
+  BuiltinNatSub -> True
+  BuiltinNatMul -> True
+  BuiltinNatUDiv -> True
+  BuiltinNatDiv -> True
+  BuiltinNatMod -> True
+  BuiltinNatLe -> True
+  BuiltinNatLt -> True
+  BuiltinNatEq -> True
+  _ -> False
+
+isIgnoredBuiltin :: BuiltinFunction -> Bool
+isIgnoredBuiltin = not . isNatBuiltin

src/Juvix/Compiler/Core/Data/InfoTable.hs

@@ -5,14 +5,14 @@ module Juvix.Compiler.Core.Data.InfoTable
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Concrete.Data.Builtins
 import Juvix.Compiler.Core.Language
 
 type IdentContext = HashMap Symbol Node
 
 data InfoTable = InfoTable
   { _identContext :: IdentContext,
-    -- `_identMap` is needed only for REPL
     _identMap :: HashMap Text IdentKind,
     _infoMain :: Maybe Symbol,
     _infoIdentifiers :: HashMap Symbol IdentifierInfo,
@@ -138,3 +138,31 @@ lookupBuiltinFunction tab b = (HashMap.!) (tab ^. infoIdentifiers) . funSym <$>
     funSym = \case
       IdentFun s -> s
       _ -> error "core infotable: expected function identifier"
+
+identName :: InfoTable -> Symbol -> Text
+identName tab sym = fromJust (HashMap.lookup sym (tab ^. infoIdentifiers)) ^. identifierName
+
+typeName :: InfoTable -> Symbol -> Text
+typeName tab sym = fromJust (HashMap.lookup sym (tab ^. infoInductives)) ^. inductiveName
+
+identNames :: InfoTable -> HashSet Text
+identNames tab =
+  HashSet.fromList $
+    map (^. identifierName) (HashMap.elems (tab ^. infoIdentifiers))
+      ++ map (^. constructorName) (HashMap.elems (tab ^. infoConstructors))
+      ++ map (^. inductiveName) (HashMap.elems (tab ^. infoInductives))
+
+freshIdentName :: InfoTable -> Text -> Text
+freshIdentName tab = freshName (identNames tab)
+
+filterByFile :: Path Abs File -> InfoTable -> InfoTable
+filterByFile f t =
+  t
+    { _infoIdentifiers = HashMap.filter (^. identifierLocation . to matchesLocation) (t ^. infoIdentifiers),
+      _infoAxioms = HashMap.filter (^. axiomLocation . to matchesLocation) (t ^. infoAxioms),
+      _infoConstructors = HashMap.filter (^. constructorLocation . to matchesLocation) (t ^. infoConstructors),
+      _infoInductives = HashMap.filter (^. inductiveLocation . to matchesLocation) (t ^. infoInductives)
+    }
+  where
+    matchesLocation :: Maybe Location -> Bool
+    matchesLocation l = l ^? _Just . intervalFile == Just f