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 <janmasrovira@gmail.com>

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,7 +22,8 @@ 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
@@ -28,19 +31,24 @@ instance CanonicalProjection CoreReadOptions Eval.CoreEvalOptions where
     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,6 +5,7 @@ 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
 
@@ -12,7 +13,6 @@ 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

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

@@ -3,6 +3,7 @@ module Juvix.Compiler.Core.Data.InfoTableBuilder where
 import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Extra.Base
+import Juvix.Compiler.Core.Info.NameInfo
 import Juvix.Compiler.Core.Language
 
 data InfoTableBuilder m a where
@@ -149,7 +150,7 @@ declareInductiveBuiltins ::
   Sem r ()
 declareInductiveBuiltins indName blt ctrs = do
   sym <- freshSymbol
-  let ty = mkTypeConstr' sym []
+  let ty = mkTypeConstr (setInfoName indName mempty) sym []
       constrs = builtinConstrs sym ty ctrs
   registerInductive
     indName
@@ -184,7 +185,7 @@ declareIOBuiltins =
 declareBoolBuiltins :: (Member InfoTableBuilder r) => Sem r ()
 declareBoolBuiltins =
   declareInductiveBuiltins
-    "bool"
+    "Bool"
     (Just (BuiltinTypeInductive BuiltinBool))
     [ (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue),
       (BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse)
@@ -195,7 +196,7 @@ declareNatBuiltins = do
   tagZero <- freshTag
   tagSuc <- freshTag
   declareInductiveBuiltins
-    "nat"
+    "Nat"
     (Just (BuiltinTypeInductive BuiltinNat))
     [ (tagZero, "zero", id, Just BuiltinNatZero),
       (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)

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

@@ -15,6 +15,7 @@ data TransformationId
   | ComputeTypeInfo
   | MatchToCase
   | EtaExpandApps
+  | DisambiguateNames
   deriving stock (Data, Bounded, Enum)
 
 data PipelineId

src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs

@@ -79,6 +79,7 @@ transformationText = \case
   ConvertBuiltinTypes -> strConvertBuiltinTypes
   ComputeTypeInfo -> strComputeTypeInfo
   UnrollRecursion -> strUnrollRecursion
+  DisambiguateNames -> strDisambiguateNames
 
 parsePipeline :: MonadParsec e Text m => m PipelineId
 parsePipeline = choice [symbol (pipelineText t) $> t | t <- allElements]
@@ -133,3 +134,6 @@ strComputeTypeInfo = "compute-type-info"
 
 strUnrollRecursion :: Text
 strUnrollRecursion = "unroll-recursion"
+
+strDisambiguateNames :: Text
+strDisambiguateNames = "disambiguate-names"

src/Juvix/Compiler/Core/Extra/SubstEnv.hs

@@ -1,18 +0,0 @@
--- | This module contains `substEnv`. This function is used in the pretty
--- printer. So it is convenient to have it isolated so that when debugging other
--- functions in Core.Utils we can use `ppTrace`
-module Juvix.Compiler.Core.Extra.SubstEnv where
-
-import Juvix.Compiler.Core.Extra.Recursors
-import Juvix.Compiler.Core.Language
-
--- | substitution of all free variables for values in an environment
-substEnv :: Env -> Node -> Node
-substEnv env
-  | null env = id
-  | otherwise = umapN go
-  where
-    go k n = case n of
-      NVar (Var _ idx)
-        | idx >= k -> env !! (idx - k)
-      _ -> n

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -6,7 +6,7 @@ module Juvix.Compiler.Core.Extra.Utils
     module Juvix.Compiler.Core.Extra.Equality,
     module Juvix.Compiler.Core.Extra.Recursors.Fold.Named,
     module Juvix.Compiler.Core.Extra.Recursors.Map.Named,
-    module Juvix.Compiler.Core.Extra.SubstEnv,
+    module Juvix.Compiler.Core.Extra.Utils.Base,
   )
 where
 
@@ -21,7 +21,7 @@ import Juvix.Compiler.Core.Extra.Info
 import Juvix.Compiler.Core.Extra.Recursors
 import Juvix.Compiler.Core.Extra.Recursors.Fold.Named
 import Juvix.Compiler.Core.Extra.Recursors.Map.Named
-import Juvix.Compiler.Core.Extra.SubstEnv
+import Juvix.Compiler.Core.Extra.Utils.Base
 import Juvix.Compiler.Core.Language
 
 isClosed :: Node -> Bool
@@ -33,14 +33,6 @@ freeVarsSorted n = Set.fromList (n ^.. freeVars)
 freeVarsSet :: Node -> HashSet Var
 freeVarsSet n = HashSet.fromList (n ^.. freeVars)
 
-freeVars :: SimpleFold Node Var
-freeVars f = ufoldNA reassemble go
-  where
-    go k = \case
-      NVar var@(Var _ idx)
-        | idx >= k -> NVar <$> f (shiftVar (-k) var)
-      n -> pure n
-
 getIdents :: Node -> HashSet Ident
 getIdents n = HashSet.fromList (n ^.. nodeIdents)
 
@@ -51,16 +43,6 @@ nodeIdents f = ufoldA reassemble go
       NIdt i -> NIdt <$> f i
       n -> pure n
 
-countFreeVarOccurrences :: Index -> Node -> Int
-countFreeVarOccurrences idx = gatherN go 0
-  where
-    go k acc = \case
-      NVar (Var _ idx') | idx' == idx + k -> acc + 1
-      _ -> acc
-
-shiftVar :: Index -> Var -> Var
-shiftVar m = over varIndex (+ m)
-
 -- | increase all free variable indices by a given value
 shift :: Index -> Node -> Node
 shift 0 = id

src/Juvix/Compiler/Core/Extra/Utils/Base.hs

@@ -0,0 +1,39 @@
+-- | The functions from this module are used in the pretty
+-- printer. So it is convenient to have them isolated so that when debugging other
+-- functions in Core.Utils we can use `ppTrace`
+module Juvix.Compiler.Core.Extra.Utils.Base where
+
+import Juvix.Compiler.Core.Extra.Base
+import Juvix.Compiler.Core.Extra.Recursors
+import Juvix.Compiler.Core.Language
+
+-- | substitution of all free variables for values in an environment
+substEnv :: Env -> Node -> Node
+substEnv env
+  | null env = id
+  | otherwise = umapN go
+  where
+    go k n = case n of
+      NVar (Var _ idx)
+        | idx >= k -> env !! (idx - k)
+      _ -> n
+
+freeVars :: SimpleFold Node Var
+freeVars f = ufoldNA reassemble go
+  where
+    go k = \case
+      NVar var@Var {..}
+        | _varIndex >= k -> NVar <$> f (shiftVar (-k) var)
+      n -> pure n
+
+shiftVar :: Index -> Var -> Var
+shiftVar m = over varIndex (+ m)
+
+freeVarOccurrences :: Index -> SimpleFold Node Var
+freeVarOccurrences idx = freeVars . filtered ((== idx) . (^. varIndex))
+
+countFreeVarOccurrences :: Index -> Node -> Int
+countFreeVarOccurrences idx n = length (n ^.. freeVarOccurrences idx)
+
+varOccurs :: Index -> Node -> Bool
+varOccurs idx = has (freeVarOccurrences idx)

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -12,7 +12,7 @@ import Juvix.Compiler.Core.Data.BinderList as BL
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Stripped
 import Juvix.Compiler.Core.Extra.Base
-import Juvix.Compiler.Core.Extra.SubstEnv
+import Juvix.Compiler.Core.Extra.Utils.Base
 import Juvix.Compiler.Core.Info.NameInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Language.Stripped qualified as Stripped
@@ -61,16 +61,22 @@ instance PrettyCode Tag where
 
 instance PrettyCode Primitive where
   ppCode = \case
-    PrimInteger _ -> return $ annotate (AnnKind KNameInductive) (pretty ("int" :: String))
-    PrimBool _ -> return $ annotate (AnnKind KNameInductive) (pretty ("bool" :: String))
-    PrimString -> return $ annotate (AnnKind KNameInductive) (pretty ("string" :: String))
+    PrimInteger _ -> return $ annotate (AnnKind KNameInductive) (pretty ("Int" :: String))
+    PrimBool _ -> return $ annotate (AnnKind KNameInductive) (pretty ("Bool" :: String))
+    PrimString -> return $ annotate (AnnKind KNameInductive) (pretty ("String" :: String))
 
 ppName :: NameKind -> Text -> Sem r (Doc Ann)
 ppName kind name = return $ annotate (AnnKind kind) (pretty name)
 
+ppIdentName :: Member (Reader Options) r => Text -> Symbol -> Sem r (Doc Ann)
+ppIdentName name sym = do
+  showIds <- asks (^. optShowIdentIds)
+  let name' = if showIds then name <> "!" <> prettyText sym else name
+  ppName KNameFunction name'
+
 ppCodeVar' :: (Member (Reader Options) r) => Text -> Var' i -> Sem r (Doc Ann)
 ppCodeVar' name v = do
-  let name' = annotate (AnnKind KNameLocal) (pretty name)
+  name' <- ppName KNameLocal name
   showDeBruijn <- asks (^. optShowDeBruijnIndices)
   if showDeBruijn || name == ""
     then return $ name' <> kwDeBruijnVar <> pretty (v ^. varIndex)
@@ -154,6 +160,18 @@ ppWithType d = \case
     ty' <- ppCode ty
     return $ parens (d <+> kwColon <+> ty')
 
+ppNameTyped :: NameKind -> Text -> Maybe (Doc Ann) -> Sem r (Doc Ann)
+ppNameTyped kn name mty = do
+  n <- ppName kn name
+  case mty of
+    Nothing -> return n
+    Just ty -> return $ parens (n <+> kwColon <+> ty)
+
+ppType :: Member (Reader Options) r => Type -> Sem r (Maybe (Doc Ann))
+ppType = \case
+  NDyn {} -> return Nothing
+  ty -> Just <$> ppCode ty
+
 ppTypeAnnot :: Member (Reader Options) r => Type -> Sem r (Doc Ann)
 ppTypeAnnot = \case
   NDyn {} ->
@@ -174,8 +192,8 @@ ppCodeLet' name mty lt = do
           mempty
   return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <+> b'
 
-ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [Text] -> Case' i bi a ty -> Sem r (Doc Ann)
-ppCodeCase' branchBinderNames branchTagNames Case {..} =
+ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [[Maybe (Doc Ann)]] -> [Text] -> Case' i bi a ty -> Sem r (Doc Ann)
+ppCodeCase' branchBinderNames branchBinderTypes branchTagNames Case {..} =
   case _caseBranches of
     [CaseBranch _ (BuiltinTag TagTrue) _ _ br1, CaseBranch _ (BuiltinTag TagTrue) _ _ br2] -> do
       br1' <- ppCode br1
@@ -189,7 +207,7 @@ ppCodeCase' branchBinderNames branchTagNames Case {..} =
       return $ kwIf <+> v <+> kwThen <+> br1' <+> kwElse <+> br2'
     _ -> do
       let branchBodies = map (^. caseBranchBody) _caseBranches
-      bns <- mapM (mapM (ppName KNameLocal)) branchBinderNames
+      bns <- zipWithM (zipWithM (ppNameTyped KNameLocal)) branchBinderNames branchBinderTypes
       cns <- mapM (ppName KNameConstructor) branchTagNames
       v <- ppCode _caseValue
       bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies
@@ -274,7 +292,7 @@ instance PrettyCode LetRec where
                   concatWith (\a b -> a <> kwSemicolon <> line <> b) $
                     zipWithExact (\b val -> b <+> kwAssign <+> val) (toList bs) (toList vs)
             nss = enclose kwSquareL kwSquareR (concatWith (<+>) names)
-         in kwLetRec <> nss <> line <> bss <> line <> kwIn <> line <> b'
+         in kwLetRec <> nss <> line <> bss <> kwSemicolon <> line <> kwIn <> line <> b'
     where
       getName :: Binder -> Sem r (Doc Ann)
       getName i = ppName KNameLocal (i ^. binderName)
@@ -285,9 +303,9 @@ instance PrettyCode Node where
     NVar x ->
       let name = getInfoName (x ^. varInfo)
        in ppCodeVar' name x
-    NIdt x ->
+    NIdt x -> do
       let name = getInfoName (x ^. identInfo)
-       in ppName KNameLocal name
+       in ppIdentName name (x ^. identSymbol)
     NCst x -> ppCode x
     NApp x -> ppCode x
     NBlt x -> ppCode x
@@ -306,17 +324,18 @@ instance PrettyCode Node where
       return (lam <+> b)
     NLet x -> ppCode x
     NRec l -> ppCode l
-    NCase x@Case {..} ->
+    NCase x@Case {..} -> do
       let branchBinderNames = map (\CaseBranch {..} -> map (^. binderName) _caseBranchBinders) _caseBranches
           branchTagNames = map (\CaseBranch {..} -> getInfoName _caseBranchInfo) _caseBranches
-       in ppCodeCase' branchBinderNames branchTagNames x
+      branchBinderTypes <- mapM (\CaseBranch {..} -> mapM (ppType . (^. binderType)) _caseBranchBinders) _caseBranches
+      ppCodeCase' branchBinderNames branchBinderTypes branchTagNames x
     NMatch Match {..} -> do
       let branchPatterns = map (^. matchBranchPatterns) _matchBranches
           branchBodies = map (^. matchBranchBody) _matchBranches
       pats <- mapM ppPatterns branchPatterns
       vs <- mapM ppCode _matchValues
       vs' <- zipWithM ppWithType (toList vs) (toList _matchValueTypes)
-      bs <- sequence $ zipWithExact (\ps br -> ppCode br >>= \br' -> return $ ps <+> kwMapsto <+> br') pats branchBodies
+      bs <- sequence $ zipWithExact (\ps br -> ppCode br >>= \br' -> return $ ps <+> kwAssign <+> br') pats branchBodies
       let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs
       rty <- ppTypeAnnot _matchReturnType
       return $ kwMatch <+> hsep (punctuate comma vs') <+> kwWith <> rty <+> bss
@@ -325,7 +344,7 @@ instance PrettyCode Node where
     NPrim TypePrim {..} -> ppCode _typePrimPrimitive
     NTyp TypeConstr {..} -> do
       args' <- mapM (ppRightExpression appFixity) _typeConstrArgs
-      n' <- ppName KNameConstructor (getInfoName _typeConstrInfo)
+      n' <- ppName KNameInductive (getInfoName _typeConstrInfo)
       return $ foldl' (<+>) n' args'
     NDyn {} -> return kwDynamic
     Closure env l@Lambda {} ->
@@ -334,16 +353,16 @@ instance PrettyCode Node where
 instance PrettyCode Pi where
   ppCode Pi {..} =
     let piType = _piBinder ^. binderType
-     in case _piBinder ^. binderName of
-          "?" -> do
-            ty <- ppLeftExpression funFixity piType
-            b <- ppRightExpression funFixity _piBody
-            return $ ty <+> kwArrow <+> b
-          name -> do
-            n <- ppName KNameLocal name
-            ty <- ppCode piType
-            b <- ppCode _piBody
-            return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
+     in if
+            | varOccurs 0 _piBody -> do
+                n <- ppName KNameLocal (_piBinder ^. binderName)
+                ty <- ppCode piType
+                b <- ppCode _piBody
+                return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
+            | otherwise -> do
+                ty <- ppLeftExpression funFixity piType
+                b <- ppRightExpression funFixity _piBody
+                return $ ty <+> kwArrow <+> b
 
 instance PrettyCode (Univ' i) where
   ppCode Univ {..} =
@@ -371,6 +390,11 @@ instance PrettyCode Stripped.Type where
     Stripped.TyApp x -> ppCode x
     Stripped.TyFun x -> ppCode x
 
+ppTypeStripped :: Member (Reader Options) r => Stripped.Type -> Sem r (Maybe (Doc Ann))
+ppTypeStripped = \case
+  Stripped.TyDynamic -> return Nothing
+  ty -> Just <$> ppCode ty
+
 instance PrettyCode Stripped.Node where
   ppCode = \case
     Stripped.NVar x ->
@@ -378,7 +402,7 @@ instance PrettyCode Stripped.Node where
        in ppCodeVar' name x
     Stripped.NIdt x ->
       let name = x ^. (identInfo . Stripped.identInfoName)
-       in ppName KNameLocal name
+       in ppIdentName name (x ^. identSymbol)
     Stripped.NCst x -> ppCode x
     Stripped.NApp x -> ppCode x
     Stripped.NBlt x -> ppCode x
@@ -389,10 +413,11 @@ instance PrettyCode Stripped.Node where
       let name = x ^. (letItem . letItemBinder . binderName)
           ty = x ^. (letItem . letItemBinder . binderType)
        in ppCode ty >>= \tty -> ppCodeLet' name (Just tty) x
-    Stripped.NCase x@Stripped.Case {..} ->
+    Stripped.NCase x@Stripped.Case {..} -> do
       let branchBinderNames = map (map (^. binderName) . (^. caseBranchBinders)) _caseBranches
           branchTagNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoConstrName)) _caseBranches
-       in ppCodeCase' branchBinderNames branchTagNames x
+      branchBinderTypes <- mapM (\CaseBranch {..} -> mapM (ppTypeStripped . (^. binderType)) _caseBranchBinders) _caseBranches
+      ppCodeCase' branchBinderNames branchBinderTypes branchTagNames x
     Stripped.NIf x -> ppCode x
 
 instance PrettyCode ConstructorInfo where
@@ -406,36 +431,62 @@ instance PrettyCode InfoTable where
   ppCode :: forall r. (Member (Reader Options) r) => InfoTable -> Sem r (Doc Ann)
   ppCode tbl = do
     tys <- ppInductives (toList (tbl ^. infoInductives))
+    sigs <- ppSigs (toList (tbl ^. infoIdentifiers))
     ctx' <- ppContext (tbl ^. identContext)
-    return ("-- Types" <> line <> tys <> line <> "-- Identifiers" <> line <> ctx' <> line)
+    main <- maybe (return "") (\s -> (<> line) . (line <>) <$> ppName KNameFunction (fromJust (HashMap.lookup s (tbl ^. infoIdentifiers)) ^. identifierName)) (tbl ^. infoMain)
+    return (tys <> line <> line <> sigs <> line <> ctx' <> line <> main)
     where
+      ppSig :: Symbol -> Sem r (Maybe (Doc Ann))
+      ppSig s = do
+        showIds <- asks (^. optShowIdentIds)
+        let mname :: Text
+            mname = tbl ^. infoIdentifiers . at s . _Just . identifierName
+            mname' = if showIds then (\nm -> nm <> "!" <> prettyText s) mname else mname
+        sym' <- ppName KNameFunction mname'
+        let -- the identifier may be missing if we have filtered out some
+            -- identifiers for printing purposes
+            mii = HashMap.lookup s (tbl ^. infoIdentifiers)
+        case mii of
+          Nothing -> return Nothing
+          Just ii -> do
+            let ty = ii ^. identifierType
+            ty' <- ppCode ty
+            let tydoc
+                  | isDynamic ty = mempty
+                  | otherwise = space <> colon <+> ty'
+                blt = if isJust (ii ^. identifierBuiltin) then (Str.builtin <+> mempty) else mempty
+            return (Just (blt <> kwDef <+> sym' <> tydoc))
+
+      ppSigs :: [IdentifierInfo] -> Sem r (Doc Ann)
+      ppSigs idents = do
+        pp <- mapM (\ii -> ppSig (ii ^. identifierSymbol)) idents
+        return $ foldr (\p acc -> p <> kwSemicolon <> line <> acc) "" (catMaybes pp)
+
       ppContext :: IdentContext -> Sem r (Doc Ann)
       ppContext ctx = do
         defs <- mapM (uncurry ppDef) (HashMap.toList ctx)
-        return (vsep defs)
+        return (vsep (catMaybes defs))
         where
-          ppDef :: Symbol -> Node -> Sem r (Doc Ann)
+          ppDef :: Symbol -> Node -> Sem r (Maybe (Doc Ann))
           ppDef s n = do
-            let mname :: Text
-                mname = tbl ^. infoIdentifiers . at s . _Just . identifierName
-                mname' = (\nm -> nm <> "!" <> prettyText s) mname
-            sym' <- ppName KNameLocal mname'
-            body' <- ppCode n
-            let ii = fromJust $ HashMap.lookup s (tbl ^. infoIdentifiers)
-                ty = ii ^. identifierType
-            ty' <- ppCode ty
-            let tydoc = if isDynamic ty then mempty else space <> colon <+> ty'
-            return (kwDef <+> sym' <> tydoc <+> kwAssign <+> nest 2 body')
+            msig <- ppSig s
+            case msig of
+              Just sig -> do
+                body' <- ppCode n
+                return (Just (sig <+> kwAssign <+> nest' body' <> kwSemicolon))
+              Nothing ->
+                return Nothing
+
       ppInductives :: [InductiveInfo] -> Sem r (Doc Ann)
       ppInductives inds = do
-        inds' <- mapM ppInductive inds
+        inds' <- mapM ppInductive (filter (isNothing . (^. inductiveBuiltin)) inds)
         return (vsep inds')
         where
           ppInductive :: InductiveInfo -> Sem r (Doc Ann)
           ppInductive ii = do
             name <- ppName KNameInductive (ii ^. inductiveName)
             ctrs <- mapM (fmap (<> semi) . ppCode) (ii ^. inductiveConstructors)
-            return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line))
+            return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line) <> kwSemicolon)
 
 instance PrettyCode Stripped.ArgumentInfo where
   ppCode :: (Member (Reader Options) r) => Stripped.ArgumentInfo -> Sem r (Doc Ann)

src/Juvix/Compiler/Core/Pretty/Options.hs

@@ -3,8 +3,7 @@ module Juvix.Compiler.Core.Pretty.Options where
 import Juvix.Prelude
 
 data Options = Options
-  { _optIndent :: Int,
-    _optShowNameIds :: Bool,
+  { _optShowIdentIds :: Bool,
     _optShowDeBruijnIndices :: Bool
   }
 
@@ -13,21 +12,19 @@ makeLenses ''Options
 defaultOptions :: Options
 defaultOptions =
   Options
-    { _optIndent = 2,
-      _optShowNameIds = False,
+    { _optShowIdentIds = False,
       _optShowDeBruijnIndices = False
     }
 
 traceOptions :: Options
 traceOptions =
   Options
-    { _optIndent = 2,
-      _optShowNameIds = False,
+    { _optShowIdentIds = False,
       _optShowDeBruijnIndices = True
     }
 
 fromGenericOptions :: GenericOptions -> Options
-fromGenericOptions GenericOptions {..} = set optShowNameIds _showNameIds defaultOptions
+fromGenericOptions _ = defaultOptions
 
 instance CanonicalProjection GenericOptions Options where
-  project = fromGenericOptions
+  project _ = defaultOptions

src/Juvix/Compiler/Core/Transformation.hs

@@ -12,6 +12,7 @@ import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation.ComputeTypeInfo
 import Juvix.Compiler.Core.Transformation.ConvertBuiltinTypes
+import Juvix.Compiler.Core.Transformation.DisambiguateNames
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Transformation.Identity
 import Juvix.Compiler.Core.Transformation.LambdaLetRecLifting
@@ -39,3 +40,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
       UnrollRecursion -> unrollRecursion
       MatchToCase -> matchToCase
       EtaExpandApps -> etaExpansionApps
+      DisambiguateNames -> disambiguateNames

src/Juvix/Compiler/Core/Transformation/DisambiguateNames.hs

@@ -0,0 +1,87 @@
+module Juvix.Compiler.Core.Transformation.DisambiguateNames where
+
+import Data.HashSet qualified as HashSet
+import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
+import Juvix.Compiler.Core.Data.BinderList qualified as BL
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.NameInfo (setInfoName)
+import Juvix.Compiler.Core.Transformation.Base
+
+disambiguateNodeNames :: InfoTable -> Node -> Node
+disambiguateNodeNames tab = dmapL go
+  where
+    go :: BinderList Binder -> Node -> Node
+    go bl node = case node of
+      NVar Var {..} ->
+        mkVar (setInfoName (BL.lookup _varIndex bl ^. binderName) _varInfo) _varIndex
+      NIdt Ident {..} ->
+        mkIdent (setInfoName (identName tab _identSymbol) _identInfo) _identSymbol
+      NLam lam ->
+        NLam (over lambdaBinder (over binderName (disambiguate bl)) lam)
+      NLet lt ->
+        NLet (over letItem (over letItemBinder (over binderName (disambiguate bl))) lt)
+      NRec lt ->
+        NRec
+          ( set
+              letRecValues
+              ( NonEmpty.fromList $
+                  zipWithExact
+                    (set letItemBinder)
+                    (disambiguateBinders bl (map (^. letItemBinder) vs))
+                    vs
+              )
+              lt
+          )
+        where
+          vs = toList (lt ^. letRecValues)
+      NCase c ->
+        NCase (over caseBranches (map (over caseBranchBinders (disambiguateBinders bl))) c)
+      NMatch m ->
+        NMatch (over matchBranches (map (over matchBranchPatterns (NonEmpty.fromList . snd . disambiguatePatterns bl . toList))) m)
+      NTyp TypeConstr {..} ->
+        mkTypeConstr (setInfoName (typeName tab _typeConstrSymbol) _typeConstrInfo) _typeConstrSymbol _typeConstrArgs
+      NPi pi
+        | varOccurs 0 (pi ^. piBody) ->
+            NPi (over piBinder (over binderName (disambiguate bl)) pi)
+      _ -> node
+
+    disambiguateBinders :: BinderList Binder -> [Binder] -> [Binder]
+    disambiguateBinders bl = \case
+      [] -> []
+      b : bs' -> b' : disambiguateBinders (BL.cons b' bl) bs'
+        where
+          b' = over binderName (disambiguate bl) b
+
+    disambiguatePatterns :: BinderList Binder -> [Pattern] -> (BinderList Binder, [Pattern])
+    disambiguatePatterns bl = \case
+      [] -> (bl, [])
+      pat : pats' -> case pat of
+        PatWildcard {} -> second (pat :) (disambiguatePatterns bl pats')
+        PatBinder pb -> second (PatBinder pb' :) (disambiguatePatterns bl' pats')
+          where
+            b' = over binderName (disambiguate bl) (pb ^. patternBinder)
+            (bl', p') = disambiguatePatterns (BL.cons b' bl) [pb ^. patternBinderPattern]
+            pb' = set patternBinderPattern (List.head p') (set patternBinder b' pb)
+        PatConstr c -> second (pat' :) (disambiguatePatterns bl' pats')
+          where
+            (bl', args') = disambiguatePatterns bl (c ^. patternConstrArgs)
+            pat' = PatConstr $ set patternConstrArgs args' c
+
+    disambiguate :: BinderList Binder -> Text -> Text
+    disambiguate bl name =
+      if
+          | name == "?" || name == "" || name == "_" ->
+              disambiguate bl "_X"
+          | elem name (map (^. binderName) (toList bl))
+              || HashSet.member name names ->
+              disambiguate bl (prime name)
+          | otherwise ->
+              name
+
+    names :: HashSet Text
+    names = identNames tab
+
+disambiguateNames :: InfoTable -> InfoTable
+disambiguateNames tab =
+  mapAllNodes (disambiguateNodeNames tab) tab

src/Juvix/Compiler/Core/Transformation/NatToInt.hs

@@ -130,8 +130,33 @@ convertNode tab = convert [] 0
             Just BuiltinNatEq -> f (\info x y -> mkBuiltinApp info OpEq [x, y])
             _ -> node
 
+filterNatBuiltins :: InfoTable -> InfoTable
+filterNatBuiltins tab =
+  let tab' =
+        over
+          infoIdentifiers
+          (HashMap.filter (isNotNatBuiltin . (^. identifierBuiltin)))
+          tab
+   in over
+        identMap
+        ( HashMap.filter
+            ( \case
+                IdentFun s -> HashMap.member s (tab' ^. infoIdentifiers)
+                _ -> True
+            )
+        )
+        $ over
+          identContext
+          (HashMap.filterWithKey (\s _ -> HashMap.member s (tab' ^. infoIdentifiers)))
+          tab'
+  where
+    isNotNatBuiltin :: Maybe BuiltinFunction -> Bool
+    isNotNatBuiltin = \case
+      Just b -> not (isNatBuiltin b)
+      Nothing -> True
+
 natToInt :: InfoTable -> InfoTable
-natToInt tab = mapT (const (convertNode tab')) tab'
+natToInt tab = filterNatBuiltins $ mapAllNodes (convertNode tab') tab'
   where
     tab' =
       case tab ^. infoIntToNat of

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -16,6 +16,7 @@ import Juvix.Compiler.Internal.Extra qualified as Internal
 import Juvix.Compiler.Internal.Translation.Extra qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped
 import Juvix.Data.Loc qualified as Loc
+import Juvix.Data.PPOutput
 import Juvix.Extra.Strings qualified as Str
 
 -- Translation of a Name into the identifier index used in the Core InfoTable
@@ -33,7 +34,7 @@ setupIntToNat sym tab =
     ii =
       IdentifierInfo
         { _identifierSymbol = sym,
-          _identifierName = "intToNat",
+          _identifierName = freshIdentName tab "intToNat",
           _identifierLocation = Nothing,
           _identifierArgsNum = 1,
           _identifierArgsInfo =
@@ -44,7 +45,7 @@ setupIntToNat sym tab =
                   _argumentIsImplicit = Explicit
                 }
             ],
-          _identifierType = mkPi' mkTypeInteger' mkTypeInteger',
+          _identifierType = mkPi' mkTypeInteger' targetType,
           _identifierIsExported = False,
           _identifierBuiltin = Nothing
         }
@@ -59,9 +60,11 @@ setupIntToNat sym tab =
               (mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
         _ ->
           mkLambda' mkTypeInteger' $ mkVar' 0
+    targetType = maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Nat" mempty) s []) natSymM
     tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
     tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
     boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
+    natSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinNat
 
 fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
 fromInternal i = do
@@ -273,7 +276,7 @@ goFunctionDefIden (f, sym) = do
   funTy <- runReader initIndexTable (goType (f ^. Internal.funDefType))
   let info =
         IdentifierInfo
-          { _identifierName = f ^. Internal.funDefName . nameText,
+          { _identifierName = normalizeBuiltinName (f ^. Internal.funDefBuiltin) (f ^. Internal.funDefName . nameText),
             _identifierLocation = Just $ f ^. Internal.funDefName . nameLoc,
             _identifierSymbol = sym,
             _identifierType = funTy,
@@ -284,9 +287,22 @@ goFunctionDefIden (f, sym) = do
             _identifierIsExported = False,
             _identifierBuiltin = f ^. Internal.funDefBuiltin
           }
-  registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info
-  when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym)
-  return funTy
+  case f ^. Internal.funDefBuiltin of
+    Just b
+      | isIgnoredBuiltin b ->
+          return funTy
+    _ -> do
+      registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info
+      when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym)
+      return funTy
+  where
+    normalizeBuiltinName :: Maybe BuiltinFunction -> Text -> Text
+    normalizeBuiltinName blt name = case blt of
+      Just b | isNatBuiltin b -> show (pretty b)
+      _ -> case name of
+        ">" -> Str.natGt
+        ">=" -> Str.natGe
+        _ -> name
 
 goFunctionDef ::
   forall r.
@@ -295,7 +311,7 @@ goFunctionDef ::
   Sem r ()
 goFunctionDef ((f, sym), ty) = do
   mbody <- case f ^. Internal.funDefBuiltin of
-    Just Internal.BuiltinBoolIf -> return Nothing
+    Just b | isIgnoredBuiltin b -> return Nothing
     Just _ -> Just <$> runReader initIndexTable (mkFunBody ty f)
     Nothing -> Just <$> runReader initIndexTable (mkFunBody ty f)
   forM_ mbody (registerIdentNode sym)
@@ -490,7 +506,7 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinIOSequence -> return ()
       Internal.BuiltinIOReadline -> return ()
       Internal.BuiltinString -> registerInductiveAxiom (Just BuiltinString) []
-      Internal.BuiltinIO -> registerInductiveAxiom Nothing builtinIOConstrs
+      Internal.BuiltinIO -> registerInductiveAxiom (Just BuiltinIO) builtinIOConstrs
       Internal.BuiltinTrace -> return ()
       Internal.BuiltinFail -> return ()
       Internal.BuiltinStringConcat -> return ()
@@ -501,11 +517,12 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
     registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
     registerInductiveAxiom ax ctrs = do
       sym <- freshSymbol
-      let ty = mkTypeConstr' sym []
+      let name = a ^. Internal.axiomName . nameText
+          ty = mkTypeConstr (setInfoName name mempty) sym []
           ctrs' = builtinConstrs sym ty ctrs
           info =
             InductiveInfo
-              { _inductiveName = a ^. Internal.axiomName . nameText,
+              { _inductiveName = name,
                 _inductiveLocation = Just $ a ^. Internal.axiomName . nameLoc,
                 _inductiveSymbol = sym,
                 _inductiveKind = mkSmallUniv,
@@ -525,7 +542,9 @@ goAxiomDef ::
 goAxiomDef a = do
   boolSym <- getBoolSymbol
   natSym <- getNatSymbol
-  case a ^. Internal.axiomBuiltin >>= builtinBody boolSym natSym of
+  tab <- getInfoTable
+  let natName = fromJust (HashMap.lookup natSym (tab ^. infoInductives)) ^. inductiveName
+  case a ^. Internal.axiomBuiltin >>= builtinBody boolSym natSym natName of
     Just body -> do
       sym <- freshSymbol
       ty <- axiomType'
@@ -546,9 +565,9 @@ goAxiomDef a = do
       setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
     Nothing -> return ()
   where
-    builtinBody :: Symbol -> Symbol -> Internal.BuiltinAxiom -> Maybe Node
-    builtinBody boolSym natSym = \case
-      Internal.BuiltinNatPrint -> Just $ writeLambda (mkTypeConstr' natSym [])
+    builtinBody :: Symbol -> Symbol -> Text -> Internal.BuiltinAxiom -> Maybe Node
+    builtinBody boolSym natSym natName = \case
+      Internal.BuiltinNatPrint -> Just $ writeLambda (mkTypeConstr (setInfoName natName mempty) natSym [])
       Internal.BuiltinStringPrint -> Just $ writeLambda mkTypeString'
       Internal.BuiltinBoolPrint -> Just $ writeLambda mkTypeBool'
       Internal.BuiltinIOSequence -> Nothing
@@ -583,7 +602,7 @@ goAxiomDef a = do
               )
           )
       Internal.BuiltinNatToString ->
-        Just (mkLambda' (mkTypeConstr' natSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
+        Just (mkLambda' (mkTypeConstr (setInfoName natName mempty) natSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
       Internal.BuiltinString -> Nothing
       Internal.BuiltinIO -> Nothing
       Internal.BuiltinTrace -> Nothing
@@ -886,7 +905,7 @@ goApplication a = do
                 mkApps'
                   ( mkConstr'
                       (BuiltinTag TagBind)
-                      [arg1, mkLambda' (mkTypeConstr' ioSym []) (shift 1 arg2)]
+                      [arg1, mkLambda' (mkTypeConstr (setInfoName Str.io mempty) ioSym []) (shift 1 arg2)]
                   )
                   xs
             _ -> error "internal to core: >> must be called with 2 arguments"

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

@@ -18,6 +18,7 @@ import Juvix.Compiler.Core.Info.NameInfo as NameInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Translation.FromSource.Lexer
+import Juvix.Extra.Strings qualified as Str
 import Juvix.Parser.Error
 import Text.Megaparsec qualified as P
 
@@ -50,7 +51,7 @@ setupMainFunction tab node =
     sym = tab ^. infoNextSymbol
     info =
       IdentifierInfo
-        { _identifierName = "main",
+        { _identifierName = freshIdentName tab "main",
           _identifierLocation = Nothing,
           _identifierSymbol = sym,
           _identifierArgsNum = 0,
@@ -95,9 +96,26 @@ statementBuiltin = do
   kw kwBuiltin
   sym <- statementDef
   ii <- lift $ getIdentifierInfo sym
-  case ii ^. identifierName of
-    "plus" -> lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatPlus}
-    _ -> parseFailure off "unrecorgnized builtin definition"
+  if
+      | ii ^. identifierName == Str.natPlus ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatPlus}
+      | ii ^. identifierName == Str.natSub ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatSub}
+      | ii ^. identifierName == Str.natMul ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatMul}
+      | ii ^. identifierName == Str.natDiv ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatDiv}
+      | ii ^. identifierName == Str.natMod ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatMod}
+      | ii ^. identifierName == Str.natUDiv ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatUDiv}
+      | ii ^. identifierName == Str.natLe ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatLe}
+      | ii ^. identifierName == Str.natLt ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatLt}
+      | ii ^. identifierName == Str.natEq ->
+          lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatEq}
+      | otherwise -> parseFailure off "unrecorgnized builtin definition"
 
 statementDef ::
   (Member InfoTableBuilder r) =>
@@ -113,8 +131,11 @@ statementDef = do
         sym
         (parseFailure off ("duplicate definition of: " ++ fromText txt))
       tab <- lift getInfoTable
+      mty <- optional typeAnnotation
       let fi = fromMaybe impossible $ HashMap.lookup sym (tab ^. infoIdentifiers)
-          ty = fi ^. identifierType
+          ty = fromMaybe (fi ^. identifierType) mty
+      unless (isDynamic (fi ^. identifierType) || ty == fi ^. identifierType) $
+        parseFailure off ("type signature doesn't match earlier definition")
       parseDefinition sym ty
       return sym
     Just IdentInd {} ->
@@ -511,6 +532,7 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwMinus $> OpIntSub)
       <|> (kw kwDiv $> OpIntDiv)
       <|> (kw kwMul $> OpIntMul)
+      <|> (kw kwMod $> OpIntMod)
       <|> (kw kwShow $> OpShow)
       <|> (kw kwStrConcat $> OpStrConcat)
       <|> (kw kwStrToInt $> OpStrToInt)
@@ -579,6 +601,28 @@ parseLocalName = parseWildcardName <|> parseIdentName
     parseIdentName :: ParsecS r (Text, Location)
     parseIdentName = identifierL
 
+parseLocalBinder ::
+  forall r.
+  (Member InfoTableBuilder r) =>
+  Index ->
+  HashMap Text Level ->
+  ParsecS r ((Text, Location), Type)
+parseLocalBinder varsNum vars = parseBinder <|> parseName
+  where
+    parseBinder :: ParsecS r ((Text, Location), Type)
+    parseBinder = do
+      lparen
+      n <- parseLocalName
+      kw kwColon
+      ty <- expr varsNum vars
+      rparen
+      return (n, ty)
+
+    parseName :: ParsecS r ((Text, Location), Type)
+    parseName = do
+      n <- parseLocalName
+      return (n, mkDynamic')
+
 exprPi ::
   (Member InfoTableBuilder r) =>
   Index ->
@@ -624,13 +668,14 @@ exprLetrecOne ::
 exprLetrecOne varsNum vars = do
   kw kwLetRec
   (name, loc) <- parseLocalName
+  mty <- optional (kw kwColon >> expr varsNum vars)
   kw kwAssign
   let vars' = HashMap.insert name varsNum vars
   value <- bracedExpr (varsNum + 1) vars'
   kw kwIn
   body <- bracedExpr (varsNum + 1) vars'
   let item :: LetItem
-      item = LetItem (Binder name (Just loc) mkDynamic') value
+      item = LetItem (Binder name (Just loc) (fromMaybe mkDynamic' mty)) value
   return $ mkLetRec mempty (pure item) body
 
 exprLetrecMany ::
@@ -644,7 +689,7 @@ exprLetrecMany varsNum vars = do
   when (null defNames) $
     parseFailure off "expected at least one identifier name in letrec signature"
   let (vars', varsNum') = foldl' (\(vs, k) txt -> (HashMap.insert txt k vs, k + 1)) (vars, varsNum) defNames
-  defs <- letrecDefs defNames varsNum' vars'
+  defs <- letrecDefs defNames varsNum vars varsNum' vars'
   kw kwIn
   body <- bracedExpr varsNum' vars'
   return $ mkLetRec mempty defs body
@@ -658,14 +703,16 @@ letrecDefs ::
   NonEmpty Text ->
   Index ->
   HashMap Text Level ->
+  Index ->
+  HashMap Text Level ->
   ParsecS r (NonEmpty LetItem)
-letrecDefs names varsNum vars = forM names letrecItem
+letrecDefs names varsNum0 vars0 varsNum vars = forM names letrecItem
   where
     letrecItem :: Text -> ParsecS r LetItem
     letrecItem n = do
       off <- P.getOffset
       (txt, i) <- identifierL
-      mty <- optional (typeAnnot varsNum vars)
+      mty <- optional (typeAnnot varsNum0 vars0)
       when (n /= txt) $
         parseFailure off "identifier name doesn't match letrec signature"
       kw kwAssign
@@ -765,6 +812,20 @@ caseDefaultBranch varsNum vars = do
   kw kwAssign
   bracedExpr varsNum vars
 
+parseCaseBranchBinders ::
+  (Member InfoTableBuilder r) =>
+  Index ->
+  HashMap Text Level ->
+  ParsecS r [((Text, Location), Type)]
+parseCaseBranchBinders varsNum vars = do
+  mb <- optional (parseLocalBinder varsNum vars)
+  case mb of
+    Just b@((name, _), _) ->
+      (b :)
+        <$> parseCaseBranchBinders (varsNum + 1) (HashMap.insert name varsNum vars)
+    Nothing ->
+      return []
+
 caseMatchingBranch ::
   (Member InfoTableBuilder r) =>
   Index ->
@@ -780,8 +841,8 @@ caseMatchingBranch varsNum vars = do
     Just IdentInd {} ->
       parseFailure off ("not a constructor: " ++ fromText txt)
     Just (IdentConstr tag) -> do
-      ns :: [(Text, Location)] <- P.many parseLocalName
-      let bindersNum = length ns
+      bs :: [((Text, Location), Type)] <- parseCaseBranchBinders varsNum vars
+      let bindersNum = length bs
       ci <- lift $ getConstructorInfo tag
       when
         (ci ^. constructorArgsNum /= bindersNum)
@@ -790,14 +851,20 @@ caseMatchingBranch varsNum vars = do
       let vars' =
             fst $
               foldl'
-                ( \(vs, k) (name, _) ->
+                ( \(vs, k) ((name, _), _) ->
                     (HashMap.insert name k vs, k + 1)
                 )
                 (vars, varsNum)
-                ns
+                bs
       br <- bracedExpr (varsNum + bindersNum) vars'
       let info = setInfoName (ci ^. constructorName) mempty
-          binders = zipWith (\(name, loc) -> Binder name (Just loc)) ns (typeArgs (ci ^. constructorType) ++ repeat mkDynamic')
+          binders =
+            zipWith
+              ( \((name, loc), ty) ty' ->
+                  Binder name (Just loc) (if isDynamic ty then ty' else ty)
+              )
+              bs
+              (typeArgs (ci ^. constructorType) ++ repeat mkDynamic')
       return $ CaseBranch info tag binders bindersNum br
     Nothing ->
       parseFailure off ("undeclared identifier: " ++ fromText txt)
@@ -976,8 +1043,8 @@ exprNamed varsNum vars = do
   off <- P.getOffset
   (txt, i) <- identifierL
   case txt of
-    "int" -> return mkTypeInteger'
-    "string" -> return mkTypeString'
+    "Int" -> return mkTypeInteger'
+    "String" -> return mkTypeString'
     _ ->
       case HashMap.lookup txt vars of
         Just k -> do

src/Juvix/Compiler/Pipeline/ExpressionContext.hs

@@ -9,6 +9,7 @@ import Juvix.Compiler.Concrete.Language qualified as C
 import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper
 import Juvix.Compiler.Core qualified as Core
 import Juvix.Compiler.Core.Data.InfoTableBuilder
+import Juvix.Compiler.Core.Extra.Base (mkDynamic')
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Transformation
 import Juvix.Compiler.Internal qualified as Internal
@@ -61,6 +62,21 @@ runTransformations :: [TransformationId] -> InfoTable -> Node -> (InfoTable, Nod
 runTransformations ts tab n = snd $ run $ runInfoTableBuilder tab $ do
   sym <- freshSymbol
   registerIdentNode sym n
+  -- `n` will get filtered out by the transformations unless it has a
+  -- corresponding entry in `infoIdentifiers`
+  let name = freshIdentName tab "_repl"
+      ii =
+        IdentifierInfo
+          { _identifierName = name,
+            _identifierSymbol = sym,
+            _identifierLocation = Nothing,
+            _identifierArgsNum = 0,
+            _identifierArgsInfo = [],
+            _identifierType = mkDynamic',
+            _identifierIsExported = False,
+            _identifierBuiltin = Nothing
+          }
+  registerIdent name ii
   tab' <- applyTransformations ts <$> getInfoTable
   let node' = lookupDefault impossible sym (tab' ^. identContext)
   return (tab', node')

src/Juvix/Extra/Strings.hs

@@ -149,6 +149,12 @@ natLt = "nat-lt"
 natEq :: (IsString s) => s
 natEq = "nat-eq"
 
+natGt :: (IsString s) => s
+natGt = "nat-gt"
+
+natGe :: (IsString s) => s
+natGe = "nat-ge"
+
 boolIf :: (IsString s) => s
 boolIf = "bool-if"
 
@@ -165,7 +171,7 @@ type_ :: (IsString s) => s
 type_ = "Type"
 
 any :: (IsString s) => s
-any = "any"
+any = "Any"
 
 questionMark :: (IsString s) => s
 questionMark = "?"

src/Juvix/Prelude/Base.hs

@@ -130,6 +130,7 @@ import Data.Singletons.TH (genSingletons, promoteOrdInstances, singOrdInstances)
 import Data.Stream (Stream)
 import Data.String
 import Data.Text (Text, pack, strip, unpack)
+import Data.Text qualified as Text
 import Data.Text.Encoding
 import Data.Text.IO
 import Data.Traversable
@@ -177,6 +178,7 @@ import System.IO hiding
     writeFile,
   )
 import System.IO.Error
+import Text.Read qualified as Text
 import Text.Show (Show)
 import Text.Show qualified as Show
 import Prelude (Double)
@@ -201,6 +203,22 @@ toUpperFirst :: String -> String
 toUpperFirst [] = []
 toUpperFirst (x : xs) = Char.toUpper x : xs
 
+--------------------------------------------------------------------------------
+-- Text
+--------------------------------------------------------------------------------
+
+prime :: Text -> Text
+prime "" = "_X"
+prime "?" = "_X"
+prime name = case Text.splitOn "'" name of
+  [name', ""] -> name' <> "'0"
+  [name', num] -> name' <> "'" <> maybe (num <> "'") (show . (+ 1)) (Text.readMaybe (unpack num) :: Maybe Word)
+  _ -> name <> "'"
+
+freshName :: HashSet Text -> Text -> Text
+freshName names name | HashSet.member name names = freshName names (prime name)
+freshName _ name = name
+
 --------------------------------------------------------------------------------
 -- Foldable
 --------------------------------------------------------------------------------

test/Core.hs

@@ -4,7 +4,8 @@ import Base
 import Core.Asm qualified as Asm
 import Core.Compile qualified as Compile
 import Core.Eval qualified as Eval
+import Core.Print qualified as Print
 import Core.Transformation qualified as Transformation
 
 allTests :: TestTree
-allTests = testGroup "JuvixCore tests" [Eval.allTests, Transformation.allTests, Asm.allTests, Compile.allTests]
+allTests = testGroup "JuvixCore tests" [Eval.allTests, Print.allTests, Transformation.allTests, Asm.allTests, Compile.allTests]

test/Core/Print.hs

@@ -0,0 +1,7 @@
+module Core.Print where
+
+import Base
+import Core.Print.Positive qualified as P
+
+allTests :: TestTree
+allTests = testGroup "JuvixCore print" [P.allTests]

test/Core/Print/Base.hs

@@ -0,0 +1,54 @@
+module Core.Print.Base where
+
+import Base
+import Core.Eval.Base
+import Core.Eval.Positive qualified as Eval
+import Data.Text.IO qualified as TIO
+import Juvix.Compiler.Core.Pipeline
+import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNames)
+import Juvix.Compiler.Core.Translation.FromSource
+
+newtype Test = Test
+  { _testEval :: Eval.PosTest
+  }
+
+fromTest :: Test -> TestTree
+fromTest = mkTest . toTestDescr
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/Core/positive/")
+
+toTestDescr :: Test -> TestDescr
+toTestDescr Test {..} =
+  let Eval.PosTest {..} = _testEval
+      tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+      expected' = tRoot <//> _expectedFile
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ corePrintAssertion file' expected'
+        }
+
+corePrintAssertion ::
+  Path Abs File ->
+  Path Abs File ->
+  (String -> IO ()) ->
+  Assertion
+corePrintAssertion mainFile expectedFile step = do
+  step "Parse"
+  r <- parseFile mainFile
+  case r of
+    Left err -> assertFailure (show (pretty err))
+    Right (_, Nothing) -> do
+      step "Empty program: compare expected and actual program output"
+      expected <- TIO.readFile (toFilePath expectedFile)
+      assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) "" expected
+    Right (tabIni, Just node) -> do
+      let tab = disambiguateNames (setupMainFunction tabIni node)
+      step "Print and parse back"
+      let r' = runParserMain mainFile emptyInfoTable (ppPrint tab)
+      case r' of
+        Left err -> assertFailure (show (pretty err))
+        Right tab' -> coreEvalAssertion' tab' mainFile expectedFile step

test/Core/Print/Positive.hs

@@ -0,0 +1,15 @@
+module Core.Print.Positive where
+
+import Base
+import Core.Eval.Positive qualified as Eval
+import Core.Print.Base
+
+allTests :: TestTree
+allTests = testGroup "JuvixCore print tests" (map liftTest Eval.tests)
+
+liftTest :: Eval.PosTest -> TestTree
+liftTest _testEval =
+  fromTest
+    Test
+      { _testEval
+      }

tests/Core/positive/test007.jvc

@@ -2,7 +2,7 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 def hd := \x case x of { cons x' _ := x' };

tests/Core/positive/test012.jvc

@@ -7,7 +7,7 @@ type tree : Type {
   leaf : tree;
 };
 
-def gen : int -> tree := \n
+def gen : Int -> tree := \n
   if n = 0 then
     leaf
   else if n % 3 = 0 then

tests/Core/positive/test023.jvc

@@ -2,7 +2,7 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 def head := \l case l of { cons h _ := h };

tests/Core/positive/test024.jvc

@@ -2,7 +2,7 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 def writeLn := \x write x >> write "\n";

tests/Core/positive/test028.jvc

@@ -2,7 +2,7 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 def hd := \l case l of { cons x _ := x };

tests/Core/positive/test029.jvc

@@ -1,7 +1,7 @@
 -- Church numerals
 
 type Pair {
-  pair : any -> any -> Pair;
+  pair : Any -> Any -> Pair;
 };
 
 def fst := \p case p of { pair x _ := x };

tests/Core/positive/test030.jvc

@@ -6,16 +6,16 @@ type Unit {
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 type Stream {
-  scons : any -> (Unit -> Stream) -> Stream;
+  scons : Any -> (Unit -> Stream) -> Stream;
 };
 
 def force : (Unit -> Stream) -> Stream := \f f unit;
 
-def filter : (any -> bool) -> (Unit -> Stream) -> Unit -> Stream := \p \s \_
+def filter : (Any -> Bool) -> (Unit -> Stream) -> Unit -> Stream := \p \s \_
   case force s of {
     scons h t :=
       if p h then
@@ -24,7 +24,7 @@ def filter : (any -> bool) -> (Unit -> Stream) -> Unit -> Stream := \p \s \_
         force (filter p t)
   };
 
-def take : int -> (Unit -> Stream) -> list := \n \s
+def take : Int -> (Unit -> Stream) -> list := \n \s
   if n = 0 then
     nil
   else
@@ -32,14 +32,14 @@ def take : int -> (Unit -> Stream) -> list := \n \s
       scons h t := cons h (take (n - 1) t)
     };
 
-def nth : int -> (Unit -> Stream) -> any := \n \s
+def nth : Int -> (Unit -> Stream) -> Any := \n \s
   case force s of {
     scons h t := if n = 0 then h else nth (n - 1) t
   };
 
-def numbers : int -> Unit -> Stream := \n \_ scons n (numbers (n + 1));
+def numbers : Int -> Unit -> Stream := \n \_ scons n (numbers (n + 1));
 
-def indivisible : int -> int -> bool := \n \x if x % n = 0 then false else true;
+def indivisible : Int -> Int -> Bool := \n \x if x % n = 0 then false else true;
 def eratostenes : (Unit -> Stream) -> Unit -> Stream := \s \_
   case force s of {
     scons n t :=

tests/Core/positive/test033.jvc

@@ -2,7 +2,7 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 def mklst := \n if n = 0 then nil else cons n (mklst (n - 1));

tests/Core/positive/test034.jvc

@@ -10,7 +10,7 @@ def const := \x \y x;
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 trace (const 0 (trace "!" 1)) (

tests/Core/positive/test035.jvc

@@ -2,11 +2,11 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 type product {
-  pair : any -> any -> product;
+  pair : Any -> Any -> product;
 };
 
 def length := \xs case xs of {

tests/Core/positive/test039.jvc

@@ -1,7 +1,7 @@
 -- eta-expansion of builtins and constructors
 
 type stream {
-  cons : any -> any -> stream;
+  cons : Any -> Any -> stream;
 };
 
 def f := \g g 2;

tests/Core/positive/test041.jvc

@@ -1,7 +1,7 @@
 -- match
 
 type list {
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
   nil : list;
 };
 

tests/Core/positive/test042.jvc

@@ -11,4 +11,4 @@ def hd : Π A : Type, list A → A := λ(A : Type) λl case l of { cons _ x _ :=
 
 def tl : Π A : Type, list A → list A := λ(A : Type) λl case l of { cons _ _ y := y };
 
-hd int (tl int (id (list int) (cons int 1 (cons int 2 (nil int)))))
+hd Int (tl Int (id (list Int) (cons Int 1 (cons Int 2 (nil Int)))))

tests/Core/positive/test043.jvc

@@ -2,10 +2,10 @@
 
 def fun := λ(A : Type) λ(x : A) let f := λ(h : A → A) h (h x) in f (λ(y : A) x);
 
-def fun' : Π T : Type → Type, Π X : Type, Π A : Type, any :=
+def fun' : Π T : Type → Type, Π X : Type, Π A : Type, Any :=
   λ(T : Type → Type) λ(_ : Type) λ(A : Type) λ(B : T A) λ(x : B)
   let f := λ(g : B → B) g (g x) in
   let h := λ(b : B) λ(a : A) a * b - b in
   f (λ(y : B) h y x);
 
-fun int 2 + fun' (λ(A : Type) A) bool int int 3
+fun Int 2 + fun' (λ(A : Type) A) Bool Int Int 3

tests/Core/positive/test044.jvc

@@ -1,17 +1,17 @@
 -- eta-expansion
 
-def compose : (int -> int) -> (int -> int) -> int -> int := \f \g \x f (g x);
+def compose : (Int -> Int) -> (Int -> Int) -> Int -> Int := \f \g \x f (g x);
 
-def expand : any -> int -> any := \f \x f;
+def expand : Any -> Int -> Any := \f \x f;
 
-def f : int -> int := (+) 1;
+def f : Int -> Int := (+) 1;
 
-def g : int -> int -> int := \z compose f (\x x - z);
+def g : Int -> Int -> Int := \z compose f (\x x - z);
 
-def h : int -> int := compose f (g 3);
+def h : Int -> Int := compose f (g 3);
 
-def j : int -> int -> int := g;
+def j : Int -> Int -> Int := g;
 
-def k : int -> int -> any -> int := expand j;
+def k : Int -> Int -> Any -> Int := expand j;
 
 h 13 + j 2 3 + k 9 4 7

tests/Core/positive/test045.jvc

@@ -21,6 +21,6 @@ def g := λ(A : Type) λ(xs : list A) λ(B : Type) λ(ys : list B) case xs of {
   nil _ := 0;
 };
 
-def main := g int (cons int 2 (nil int)) int (cons int 3 (nil int)) * f int 1 int (hd int (tl int (id (list int) (cons int 1 (cons int 2 (nil int))))));
+def main := g Int (cons Int 2 (nil Int)) Int (cons Int 3 (nil Int)) * f Int 1 Int (hd Int (tl Int (id (list Int) (cons Int 1 (cons Int 2 (nil Int))))));
 
 main

tests/Core/positive/test046.jvc

@@ -2,7 +2,7 @@
 
 type list {
   nil : list;
-  cons : any -> list -> list;
+  cons : Any -> list -> list;
 };
 
 def f := \l (case l of { cons x _ := x; nil := \x x } ) (let y := \x x in (let z := \x x in case l of { cons _ _ := \x x } z) y) 7;

tests/Core/positive/test047.jvc

@@ -1,8 +1,8 @@
 -- builtin natural numbers
 
-builtin def plus := \x \y case x of {
+builtin def nat-plus := \x \y case x of {
   zero := y;
-  suc x' := suc (plus x' y);
+  suc x' := suc (nat-plus x' y);
 };
 
 def from_int := \n if n = 0 then zero else suc (from_int (n - 1));
@@ -31,8 +31,8 @@ def f := \x case x of {
 def writeLn := \x write x >> write "\n";
 
 def main :=
-  writeLn (to_int (if even (from_int 124) then plus (suc zero) (suc (suc zero)) else zero)) >>
-  writeLn (to_int (plus (from_int 126) (from_int 10))) >>
+  writeLn (to_int (if even (from_int 124) then nat-plus (suc zero) (suc (suc zero)) else zero)) >>
+  writeLn (to_int (nat-plus (from_int 126) (from_int 10))) >>
   writeLn (f (from_int 65));
 
 main

tests/Core/positive/test049.jvc

@@ -6,10 +6,10 @@ type Boxed {
 
 def g : Π A : Type, A → Boxed A → A → A := λ(A : Type) λ(a : A) λ(_ : Boxed A) λ(a' : A) a;
 
-def f : Π A : Type, int → int → Boxed A → int → A → A :=
-    λ(A : Type) λ(n : int) λ(m : int) λ(b : Boxed A) λ(k : int) λ(a' : A)
+def f : Π A : Type, Int → Int → Boxed A → Int → A → A :=
+    λ(A : Type) λ(n : Int) λ(m : Int) λ(b : Boxed A) λ(k : Int) λ(a' : A)
         case b of {
-            Box _ a := (λ(_ : int) g A a b a') (n + m + k);
+            Box _ a := (λ(_ : Int) g A a b a') (n + m + k);
         };
 
-f int 0 1 (Box int 1) 2 3
+f Int 0 1 (Box Int 1) 2 3

tests/Core/positive/test050.jvc

@@ -6,17 +6,17 @@ def czero : Π A : Type, (A → A) → A → A :=
 def csuc : (Π A : Type, (A → A) → A → A) → Π A : Type, (A → A) → A → A :=
   λ(n : Π A : Type, (A → A) → A → A) λ(A : Type) λ(f : A → A) λ(x : A) f (n A f x);
 
-def num : nat → Π A : Type, (A → A) → A → A :=
-  λ(n : nat) match n : nat with : Π A : Type, (A → A) → A → A {
+def num : Nat → Π A : Type, (A → A) → A → A :=
+  λ(n : Nat) match n : Nat with : Π A : Type, (A → A) → A → A {
     zero := czero;
-    suc (n : nat) := csuc (num n);
+    suc (n : Nat) := csuc (num n);
   };
 
-def toNat : (Π A : Type, (A → A) → A → A) → nat :=
-  λ(n : Π A : Type, (A → A) → A → A) n nat suc zero;
+def toNat : (Π A : Type, (A → A) → A → A) → Nat :=
+  λ(n : Π A : Type, (A → A) → A → A) n Nat suc zero;
 
-def toInt : nat → int :=
-  λ(n : nat) case n of {
+def toInt : Nat → Int :=
+  λ(n : Nat) case n of {
     zero := 0;
     suc n := toInt n + 1;
   };

tests/Core/positive/test051.jvc

@@ -4,9 +4,9 @@ type Box {
     box : Π A : Type, A → Box A;
 };
 
-def f : Box (Π A : Type, A → A) → int := \(x : Box (Π A : Type, A → A))
-    match x : Box (Π A : Type, A → A) with : int {
-        box _ (g : Π A : Type, A → A) : Box (Π A : Type, A → A)  := g int 1;
+def f : Box (Π A : Type, A → A) → Int := \(x : Box (Π A : Type, A → A))
+    match x : Box (Π A : Type, A → A) with : Int {
+        box _ (g : Π A : Type, A → A) : Box (Π A : Type, A → A)  := g Int 1;
     };
 
 f (box (Π A : Type, A → A) \(A : Type) \(x : A) x)

tests/Core/positive/test052.jvc

@@ -12,4 +12,4 @@ def foldl : Π A : Type, Π B : Type, (B → A → B) → B → List A → B :=
         cons _ (h : A) (hs : List A) := foldl A B f (f b h) hs
     };
 
-foldl int int (+) 0 (cons int 1 (cons int 2 (cons int 3 (nil int))))
+foldl Int Int (+) 0 (cons Int 1 (cons Int 2 (cons Int 3 (nil Int))))

tests/Core/positive/test053.jvc

@@ -3,10 +3,10 @@ type Box {
     mkBox : Π A : Type, A → Box A;
 };
 
-def tt : Π A : Type, (int → A) → Box A → int :=
-    λ(A : Type) λ(f : int → A) λ(l : Box A)
-    match (l : Box A) with : int {
+def tt : Π A : Type, (Int → A) → Box A → Int :=
+    λ(A : Type) λ(f : Int → A) λ(l : Box A)
+    match (l : Box A) with : Int {
         mkBox _ _ := f 33
     };
 
-tt int ((+) 2) (mkBox int 1)
+tt Int ((+) 2) (mkBox Int 1)

tests/Core/positive/test054.jvc

@@ -5,18 +5,18 @@ type List {
   nil : Π A : Type, List A;
 };
 
-def lgen : int → List int := \(n : int)
-    if n = 0 then nil int else cons int n (lgen (n - 1));
+def lgen : Int → List Int := \(n : Int)
+    if n = 0 then nil Int else cons Int n (lgen (n - 1));
 
-def sum2 : List int → List int := \(x : List int) {
-  match x : List int with : List int {
-    cons _ x y@(cons _ z _) := cons int (x + z) (sum2 y);
+def sum2 : List Int → List Int := \(x : List Int) {
+  match x : List Int with : List Int {
+    cons _ x y@(cons _ z _) := cons Int (x + z) (sum2 y);
     _ := x
   }
 };
 
-def sum : List int → int := \(x : List int) {
-  match x : List int with : int {
+def sum : List Int → Int := \(x : List Int) {
+  match x : List Int with : Int {
     cons _ x y := x + sum y;
     _ := 0
   }
@@ -27,8 +27,8 @@ type Tree {
   node : Π A : Type, Tree A -> Tree A -> Tree A;
 };
 
-def gen : int → Tree int := \(n : int)
-    if n <= 0 then leaf int 1 else node int (gen (n - 2)) (gen (n - 1));
+def gen : Int → Tree Int := \(n : Int)
+    if n <= 0 then leaf Int 1 else node Int (gen (n - 2)) (gen (n - 1));
 
 def g : Π A : Type, Tree A → Tree A := \(A : Type) \(t : Tree A) {
   match t : Tree A with : Tree A {
@@ -38,12 +38,12 @@ def g : Π A : Type, Tree A → Tree A := \(A : Type) \(t : Tree A) {
   }
 };
 
-def f : Tree int → int := \(t : Tree int) match t : Tree int with : int {
-  leaf _ (x : int) := x;
-  node _ (l : Tree int) r :=
-    match (g int l : Tree int), (g int r : Tree int) with : int {
+def f : Tree Int → Int := \(t : Tree Int) match t : Tree Int with : Int {
+  leaf _ (x : Int) := x;
+  node _ (l : Tree Int) r :=
+    match (g Int l : Tree Int), (g Int r : Tree Int) with : Int {
       leaf _ _, leaf _ _ := 0 - 6;
-      node (A : Type) (l : Tree A) (r : Tree int), leaf _ _ := ((f l + f r) * 2) % 20000;
+      node (A : Type) (l : Tree A) (r : Tree Int), leaf _ _ := ((f l + f r) * 2) % 20000;
       node (A : Type) (l1 : Tree A) (r1 : Tree A), node (B : Type) (l2 : Tree A) (r2 : Tree B) := ((f l1 + f r1) * (f l2 + f r2)) % 20000;
       _, node _ l r := ((f l + f r) * (0 - 3)) % 20000;
     }

tests/Core/positive/test055.jvc

@@ -4,7 +4,7 @@ type Box {
     box : Π T : Type, Π A : T, A → A → Box A;
 };
 
-def f : Box int → int := \(x : Box int) case x of { box _ _ a b := b - a };
-def g : (int → int → Box int) → Box int := \(f : int → int → Box int) f 2 3;
+def f : Box Int → Int := \(x : Box Int) case x of { box _ _ a b := b - a };
+def g : (Int → Int → Box Int) → Box Int := \(f : Int → Int → Box Int) f 2 3;
 
-f (g (box Type int))
+f (g (box Type Int))

tests/Core/positive/test056.jvc

@@ -18,8 +18,7 @@ def g : Π A : Type, A → A := \(A : Type) \(x : A)
     in
     h A (unbox A b);
 
-letrec[A f]
-    A : Type := int;
-    f : A → int := \(x : A) x;
+letrec A : Type := Int in
+letrec f : A → Int := \(x : A) x
 in
-g int (f 4)
+g Int (f 4)

tests/Core/positive/test057.jvc

@@ -1,10 +1,10 @@
 -- type synonyms
 
 def T : Type := Type;
-def I : Type := int;
+def I : Type := Int;
 
 def id : Π A : T, A → A := \(A : T) \(x : A) x;
 
 def id' : I → I := \(x : I) id I x;
 
-id int 4 + id' 1
+id Int 4 + id' 1

tests/Core/positive/test058.jvc

@@ -1,8 +1,8 @@
 -- lifting and partial application
 
-def f : (int -> int -> int) -> int := \(h : int -> int -> int) h 1 2;
-def g : int -> int := \(x : int) x;
+def f : (Int -> Int -> Int) -> Int := \(h : Int -> Int -> Int) h 1 2;
+def g : Int -> Int := \(x : Int) x;
 
-let h : int -> int -> int := \(x : int) g
+let h : Int -> Int -> Int := \(x : Int) g
 in
 f h + h 2 3