Add the JuvixCore framework and its evaluator (#1421)

app/App.hs

@@ -11,6 +11,7 @@ import System.Console.ANSI qualified as Ansi
 data App m a where
   ExitMsg :: ExitCode -> Text -> App m ()
   ExitJuvixError :: JuvixError -> App m a
+  PrintJuvixError :: JuvixError -> App m ()
   ReadGlobalOptions :: App m GlobalOptions
   RenderStdOut :: (HasAnsiBackend a, HasTextBackend a) => a -> App m ()
   RunPipelineEither :: Sem PipelineEff a -> App m (Either JuvixError a)
@@ -31,11 +32,16 @@ runAppIO g = interpret $ \case
   Say t
     | g ^. globalOnlyErrors -> return ()
     | otherwise -> embed (putStrLn t)
+  PrintJuvixError e -> do
+    printErr e
   ExitJuvixError e -> do
-    (embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors)) (g ^. globalOnlyErrors)) e
+    printErr e
     embed exitFailure
   ExitMsg exitCode t -> embed (putStrLn t >> exitWith exitCode)
   Raw b -> embed (ByteString.putStr b)
+  where
+    printErr e =
+      (embed . hPutStrLn stderr . Error.render (not (g ^. globalNoColors)) (g ^. globalOnlyErrors)) e
 
 runPipeline :: Member App r => Sem PipelineEff a -> Sem r a
 runPipeline p = do

app/Commands/Dev.hs

@@ -1,5 +1,6 @@
 module Commands.Dev
   ( module Commands.Dev,
+    module Commands.Dev.Core,
     module Commands.Dev.Internal,
     module Commands.Dev.Parse,
     module Commands.Dev.Scope,
@@ -8,6 +9,7 @@ module Commands.Dev
   )
 where
 
+import Commands.Dev.Core
 import Commands.Dev.Doc
 import Commands.Dev.Internal
 import Commands.Dev.Parse
@@ -21,6 +23,7 @@ data InternalCommand
   = DisplayRoot
   | Highlight HighlightOptions
   | Internal MicroCommand
+  | Core CoreCommand
   | MiniC
   | MiniHaskell
   | MonoJuvix
@@ -39,6 +42,7 @@ parseInternalCommand =
     ( mconcat
         [ commandHighlight,
           commandInternal,
+          commandCore,
           commandMiniC,
           commandMiniHaskell,
           commandMonoJuvix,
@@ -96,6 +100,13 @@ commandInternal =
       (Internal <$> parseMicroCommand)
       (progDesc "Subcommands related to Internal")
 
+commandCore :: Mod CommandFields InternalCommand
+commandCore =
+  command "core" $
+    info
+      (Core <$> parseCoreCommand)
+      (progDesc "Subcommands related to JuvixCore")
+
 commandMiniHaskell :: Mod CommandFields InternalCommand
 commandMiniHaskell =
   command "minihaskell" $

app/Commands/Dev/Core.hs

@@ -0,0 +1,69 @@
+module Commands.Dev.Core where
+
+import Juvix.Prelude hiding (Doc)
+import Options.Applicative
+
+data CoreCommand
+  = Repl CoreReplOptions
+  | Eval CoreEvalOptions
+
+newtype CoreReplOptions = CoreReplOptions
+  { _coreReplShowDeBruijn :: Bool
+  }
+
+newtype CoreEvalOptions = CoreEvalOptions
+  { _coreEvalNoIO :: Bool
+  }
+
+makeLenses ''CoreReplOptions
+makeLenses ''CoreEvalOptions
+
+defaultCoreEvalOptions :: CoreEvalOptions
+defaultCoreEvalOptions =
+  CoreEvalOptions
+    { _coreEvalNoIO = False
+    }
+
+parseCoreCommand :: Parser CoreCommand
+parseCoreCommand =
+  hsubparser $
+    mconcat
+      [ commandRepl,
+        commandEval
+      ]
+  where
+    commandRepl :: Mod CommandFields CoreCommand
+    commandRepl = command "repl" replInfo
+
+    commandEval :: Mod CommandFields CoreCommand
+    commandEval = command "eval" evalInfo
+
+    replInfo :: ParserInfo CoreCommand
+    replInfo =
+      info
+        (Repl <$> parseCoreReplOptions)
+        (progDesc "Start an interactive session of the JuvixCore evaluator")
+
+    evalInfo :: ParserInfo CoreCommand
+    evalInfo =
+      info
+        (Eval <$> parseCoreEvalOptions)
+        (progDesc "Evaluate a JuvixCore file and pretty print the result")
+
+parseCoreEvalOptions :: Parser CoreEvalOptions
+parseCoreEvalOptions = do
+  _coreEvalNoIO <-
+    switch
+      ( long "no-io"
+          <> help "Don't interpret the IO effects"
+      )
+  pure CoreEvalOptions {..}
+
+parseCoreReplOptions :: Parser CoreReplOptions
+parseCoreReplOptions = do
+  _coreReplShowDeBruijn <-
+    switch
+      ( long "show-de-bruijn"
+          <> help "Show variable de Bruijn indices"
+      )
+  pure CoreReplOptions {..}

app/Main.hs

@@ -23,6 +23,15 @@ import Juvix.Compiler.Concrete.Data.InfoTable qualified as Scoper
 import Juvix.Compiler.Concrete.Pretty qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
 import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
+import Juvix.Compiler.Core.Data.InfoTable qualified as Core
+import Juvix.Compiler.Core.Error qualified as Core
+import Juvix.Compiler.Core.Evaluator qualified as Core
+import Juvix.Compiler.Core.Extra.Base qualified as Core
+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.Translation.FromSource qualified as Core
 import Juvix.Compiler.Internal.Pretty qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination qualified as Termination
@@ -39,6 +48,7 @@ import Juvix.Prelude.Pretty hiding (Doc)
 import Options.Applicative
 import System.Environment (getProgName)
 import System.Process qualified as Process
+import Text.Megaparsec.Pos qualified as M
 import Text.Show.Pretty hiding (Html)
 
 findRoot :: CommandGlobalOptions -> IO (FilePath, Package)
@@ -103,6 +113,7 @@ runCommand cmdWithOpts = do
   (root, pkg) <- embed (findRoot cmdWithOpts)
   case cmd of
     (Dev DisplayRoot) -> say (pack root)
+    (Dev (Core cmd')) -> runCoreCommand globalOpts cmd'
     _ -> do
       -- Other commands require an entry point:
       case getEntryPoint root pkg globalOpts of
@@ -264,6 +275,147 @@ runCommand cmdWithOpts = do
                                 printSuccessExit (n <> " Terminates with order " <> show (toList k))
                 _ -> impossible
 
+runCoreCommand :: Members '[Embed IO, App] r => GlobalOptions -> CoreCommand -> Sem r ()
+runCoreCommand globalOpts = \case
+  Repl opts -> do
+    embed showReplWelcome
+    runRepl opts Core.emptyInfoTable
+  Eval opts ->
+    case globalOpts ^. globalInputFiles of
+      [] -> printFailureExit "Provide a JuvixCore file to run this command\nUse --help to see all the options"
+      files -> mapM_ (evalFile opts) files
+  where
+    runRepl ::
+      forall r.
+      Members '[Embed IO, App] r =>
+      CoreReplOptions ->
+      Core.InfoTable ->
+      Sem r ()
+    runRepl opts tab = do
+      embed (putStr "> ")
+      embed (hFlush stdout)
+      done <- embed isEOF
+      unless done $ do
+        s <- embed getLine
+        case fromText (strip s) of
+          ":q" -> return ()
+          ":h" -> do
+            embed showReplHelp
+            runRepl opts tab
+          ':' : 'p' : ' ' : s' ->
+            case Core.parseText tab (fromString s') of
+              Left err -> do
+                printJuvixError (JuvixError err)
+                runRepl opts tab
+              Right (tab', Just node) -> do
+                renderStdOut (Core.ppOutDefault node)
+                embed (putStrLn "")
+                runRepl opts tab'
+              Right (tab', Nothing) ->
+                runRepl opts tab'
+          ':' : 'e' : ' ' : s' ->
+            case Core.parseText tab (fromString s') of
+              Left err -> do
+                printJuvixError (JuvixError err)
+                runRepl opts tab
+              Right (tab', Just node) ->
+                replEval True tab' node
+              Right (tab', Nothing) ->
+                runRepl opts tab'
+          ':' : 'l' : ' ' : f -> do
+            s' <- embed (readFile f)
+            case Core.runParser "" f Core.emptyInfoTable s' of
+              Left err -> do
+                printJuvixError (JuvixError err)
+                runRepl opts tab
+              Right (tab', Just node) ->
+                replEval False tab' node
+              Right (tab', Nothing) ->
+                runRepl opts tab'
+          ":r" ->
+            runRepl opts Core.emptyInfoTable
+          _ ->
+            case Core.parseText tab s of
+              Left err -> do
+                printJuvixError (JuvixError err)
+                runRepl opts tab
+              Right (tab', Just node) ->
+                replEval False tab' node
+              Right (tab', Nothing) ->
+                runRepl opts tab'
+      where
+        replEval :: Bool -> Core.InfoTable -> Core.Node -> Sem r ()
+        replEval noIO tab' node = do
+          r <- doEval noIO defaultLoc tab' node
+          case r of
+            Left err -> do
+              printJuvixError (JuvixError err)
+              runRepl opts tab'
+            Right node'
+              | Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
+                  runRepl opts tab'
+            Right node' -> do
+              renderStdOut (Core.ppOut docOpts node')
+              embed (putStrLn "")
+              runRepl opts tab'
+          where
+            defaultLoc = singletonInterval (mkLoc "stdin" 0 (M.initialPos "stdin"))
+            docOpts = set Core.optShowDeBruijnIndices (opts ^. coreReplShowDeBruijn) Core.defaultOptions
+
+    showReplWelcome :: IO ()
+    showReplWelcome = do
+      putStrLn "JuvixCore REPL"
+      putStrLn ""
+      putStrLn "Type \":h\" for help."
+      putStrLn ""
+
+    showReplHelp :: IO ()
+    showReplHelp = do
+      putStrLn ""
+      putStrLn "JuvixCore REPL"
+      putStrLn ""
+      putStrLn "Type in a JuvixCore program to evaluate."
+      putStrLn ""
+      putStrLn "Available commands:"
+      putStrLn ":p expr               Pretty print \"expr\"."
+      putStrLn ":e expr               Evaluate \"expr\" without interpreting IO actions."
+      putStrLn ":l file               Load and evaluate \"file\". Resets REPL state."
+      putStrLn ":r                    Reset REPL state."
+      putStrLn ":q                    Quit."
+      putStrLn ":h                    Display this help message."
+      putStrLn ""
+
+    evalFile :: Members '[Embed IO, App] r => CoreEvalOptions -> FilePath -> Sem r ()
+    evalFile opts f = do
+      s <- embed (readFile f)
+      case Core.runParser "" f Core.emptyInfoTable s of
+        Left err -> exitJuvixError (JuvixError err)
+        Right (tab, Just node) -> do
+          r <- doEval (opts ^. coreEvalNoIO) defaultLoc tab node
+          case r of
+            Left err -> exitJuvixError (JuvixError err)
+            Right node'
+              | Info.member Info.kNoDisplayInfo (Core.getInfo node') ->
+                  return ()
+            Right node' -> do
+              renderStdOut (Core.ppOutDefault node')
+              embed (putStrLn "")
+        Right (_, Nothing) -> return ()
+      where
+        defaultLoc = singletonInterval (mkLoc f 0 (M.initialPos f))
+
+    doEval ::
+      Members '[Embed IO, App] r =>
+      Bool ->
+      Interval ->
+      Core.InfoTable ->
+      Core.Node ->
+      Sem r (Either Core.CoreError Core.Node)
+    doEval noIO loc tab node =
+      if noIO
+        then embed $ Core.catchEvalError loc (Core.eval (tab ^. Core.identContext) [] node)
+        else embed $ Core.catchEvalErrorIO loc (Core.evalIO (tab ^. Core.identContext) [] node)
+
 showHelpText :: ParserPrefs -> IO ()
 showHelpText p = do
   progn <- getProgName

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs

@@ -13,8 +13,8 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Language qualified as L
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error.Pretty
-import Juvix.Compiler.Concrete.Translation.FromSource.Error qualified as Parser
 import Juvix.Data.CodeAnn
+import Juvix.Parser.Error qualified as Parser
 import Juvix.Prelude
 
 data MultipleDeclarations = MultipleDeclarations

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

@@ -2,7 +2,7 @@ module Juvix.Compiler.Concrete.Translation.FromSource
   ( module Juvix.Compiler.Concrete.Translation.FromSource,
     module Juvix.Compiler.Concrete.Translation.FromSource.Data.Context,
     module Juvix.Compiler.Concrete.Data.ParsedInfoTable,
-    module Juvix.Compiler.Concrete.Translation.FromSource.Error,
+    module Juvix.Parser.Error,
   )
 where
 
@@ -14,9 +14,9 @@ import Juvix.Compiler.Concrete.Extra (MonadParsec (takeWhile1P))
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context
-import Juvix.Compiler.Concrete.Translation.FromSource.Error
 import Juvix.Compiler.Concrete.Translation.FromSource.Lexer hiding (symbol)
 import Juvix.Compiler.Pipeline.EntryPoint
+import Juvix.Parser.Error
 import Juvix.Prelude
 import Juvix.Prelude.Pretty (Pretty, prettyText)
 

src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs

@@ -1,39 +1,21 @@
-module Juvix.Compiler.Concrete.Translation.FromSource.Lexer where
+module Juvix.Compiler.Concrete.Translation.FromSource.Lexer
+  ( module Juvix.Compiler.Concrete.Translation.FromSource.Lexer,
+    module Juvix.Parser.Lexer,
+  )
+where
 
 import Data.Text qualified as Text
 import GHC.Unicode
 import Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder
-import Juvix.Compiler.Concrete.Extra hiding (Pos, space)
+import Juvix.Compiler.Concrete.Extra hiding (Pos, space, string')
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Extra.Strings qualified as Str
+import Juvix.Parser.Lexer
 import Juvix.Prelude
 import Text.Megaparsec.Char.Lexer qualified as L
 
 type OperatorSym = Text
 
-type ParsecS r = ParsecT Void Text (Sem r)
-
-newtype ParserParams = ParserParams
-  { _parserParamsRoot :: FilePath
-  }
-
-makeLenses ''ParserParams
-
-space :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
-space = L.space space1 lineComment block
-  where
-    skipLineComment :: ParsecS r ()
-    skipLineComment = do
-      notFollowedBy (P.chunk Str.judocStart)
-      void (P.chunk "--")
-      void (P.takeWhileP Nothing (/= '\n'))
-
-    lineComment :: ParsecS r ()
-    lineComment = comment_ skipLineComment
-
-    block :: ParsecS r ()
-    block = comment_ (L.skipBlockComment "{-" "-}")
-
 comment :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
 comment c = do
   (a, i) <- interval c
@@ -43,6 +25,9 @@ comment c = do
 comment_ :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r ()
 comment_ = void . comment
 
+space :: forall r. Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
+space = space' True comment_
+
 lexeme :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r a -> ParsecS r a
 lexeme = L.lexeme space
 
@@ -62,13 +47,7 @@ identifierL :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (
 identifierL = lexeme bareIdentifier
 
 integer :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Integer, Interval)
-integer = do
-  minus <- optional (char '-')
-  (nat, i) <- decimal
-  let nat' = case minus of
-        Nothing -> nat
-        _ -> (-nat)
-  return (nat', i)
+integer = integer' decimal
 
 bracedString :: forall e m. MonadParsec e Text m => m Text
 bracedString =
@@ -86,9 +65,7 @@ bracedString =
       char '}'
 
 string :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Text, Interval)
-string =
-  lexemeInterval $
-    pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
+string = lexemeInterval string'
 
 judocExampleStart :: ParsecS r ()
 judocExampleStart = P.chunk Str.judocExample >> hspace
@@ -99,51 +76,14 @@ judocStart = P.chunk Str.judocStart >> hspace
 judocEmptyLine :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r ()
 judocEmptyLine = lexeme (void (P.try (judocStart >> P.newline)))
 
-curLoc :: Member (Reader ParserParams) r => ParsecS r Loc
-curLoc = do
-  sp <- getSourcePos
-  offset <- getOffset
-  root <- lift (asks (^. parserParamsRoot))
-  return (mkLoc root offset sp)
-
-interval :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (a, Interval)
-interval ma = do
-  start <- curLoc
-  res <- ma
-  end <- curLoc
-  return (res, mkInterval start end)
-
-withLoc :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (WithLoc a)
-withLoc ma = do
-  (a, i) <- interval ma
-  return (WithLoc i a)
-
 keyword :: Members '[Reader ParserParams, InfoTableBuilder] r => Text -> ParsecS r ()
 keyword kw = do
-  l <- P.try $ do
-    i <- snd <$> interval (P.chunk kw)
-    notFollowedBy (satisfy validTailChar)
-    space
-    return i
+  l <- keywordL' space kw
   lift (registerKeyword l)
 
 -- | Same as @identifier@ but does not consume space after it.
 bareIdentifier :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r (Text, Interval)
-bareIdentifier = interval $ do
-  notFollowedBy (choice allKeywords)
-  h <- P.satisfy validFirstChar
-  t <- P.takeWhileP Nothing validTailChar
-  return (Text.cons h t)
-
-validTailChar :: Char -> Bool
-validTailChar c =
-  isAlphaNum c || validFirstChar c
-
-reservedSymbols :: [Char]
-reservedSymbols = "\";(){}[].≔λ\\"
-
-validFirstChar :: Char -> Bool
-validFirstChar c = not $ isNumber c || isSpace c || (c `elem` reservedSymbols)
+bareIdentifier = interval $ rawIdentifier allKeywords
 
 dot :: forall e m. MonadParsec e Text m => m Char
 dot = P.char '.'

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

@@ -0,0 +1,45 @@
+module Juvix.Compiler.Core.Data.BinderList where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.List qualified as List
+import Juvix.Compiler.Core.Language.Base
+
+data BinderList a = BinderList
+  { _blLength :: Int,
+    _blMap :: HashMap Index a
+  }
+
+makeLenses ''BinderList
+
+fromList :: [a] -> BinderList a
+fromList l = BinderList (List.length l) (HashMap.fromList (zip [0 ..] l))
+
+toList :: BinderList a -> [a]
+toList bl =
+  List.map snd $
+    sortBy (\x y -> compare (fst y) (fst x)) $
+      HashMap.toList (bl ^. blMap)
+
+empty :: BinderList a
+empty = BinderList 0 mempty
+
+length :: BinderList a -> Int
+length = (^. blLength)
+
+lookup :: Index -> BinderList a -> a
+lookup idx bl =
+  fromMaybe
+    (error "invalid binder lookup")
+    (HashMap.lookup (bl ^. blLength - 1 - idx) (bl ^. blMap))
+
+extend :: a -> BinderList a -> BinderList a
+extend a bl =
+  BinderList
+    (bl ^. blLength + 1)
+    (HashMap.insert (bl ^. blLength) a (bl ^. blMap))
+
+map :: (a -> b) -> BinderList a -> BinderList b
+map f bl = bl {_blMap = HashMap.map f (bl ^. blMap)}
+
+prepend :: [a] -> BinderList a -> BinderList a
+prepend l bl = foldr extend bl l

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

@@ -0,0 +1,78 @@
+module Juvix.Compiler.Core.Data.InfoTable where
+
+import Juvix.Compiler.Core.Language
+
+type IdentContext = HashMap Symbol Node
+
+data InfoTable = InfoTable
+  { _identContext :: IdentContext,
+    -- `_identMap` is needed only for REPL
+    _identMap :: HashMap Text (Either Symbol Tag),
+    _infoMain :: Maybe Symbol,
+    _infoIdents :: HashMap Symbol IdentInfo,
+    _infoInductives :: HashMap Name InductiveInfo,
+    _infoConstructors :: HashMap Tag ConstructorInfo,
+    _infoAxioms :: HashMap Name AxiomInfo
+  }
+
+emptyInfoTable :: InfoTable
+emptyInfoTable =
+  InfoTable
+    { _identContext = mempty,
+      _identMap = mempty,
+      _infoMain = Nothing,
+      _infoIdents = mempty,
+      _infoInductives = mempty,
+      _infoConstructors = mempty,
+      _infoAxioms = mempty
+    }
+
+data IdentInfo = IdentInfo
+  { _identName :: Name,
+    _identSymbol :: Symbol,
+    _identType :: Type,
+    -- _identArgsNum will be used often enough to justify avoiding recomputation
+    _identArgsNum :: Int,
+    _identArgsInfo :: [ArgumentInfo],
+    _identIsExported :: Bool
+  }
+
+data ArgumentInfo = ArgumentInfo
+  { _argumentName :: Name,
+    _argumentType :: Type,
+    _argumentIsImplicit :: Bool
+  }
+
+data InductiveInfo = InductiveInfo
+  { _inductiveName :: Name,
+    _inductiveKind :: Type,
+    _inductiveConstructors :: [ConstructorInfo],
+    _inductiveParams :: [ParameterInfo],
+    _inductivePositive :: Bool
+  }
+
+data ConstructorInfo = ConstructorInfo
+  { _constructorName :: Name,
+    _constructorTag :: Tag,
+    _constructorType :: Type,
+    _constructorArgsNum :: Int
+  }
+
+data ParameterInfo = ParameterInfo
+  { _paramName :: Name,
+    _paramKind :: Type,
+    _paramIsImplicit :: Bool
+  }
+
+data AxiomInfo = AxiomInfo
+  { _axiomName :: Name,
+    _axiomType :: Type
+  }
+
+makeLenses ''InfoTable
+makeLenses ''IdentInfo
+makeLenses ''ArgumentInfo
+makeLenses ''InductiveInfo
+makeLenses ''ConstructorInfo
+makeLenses ''ParameterInfo
+makeLenses ''AxiomInfo

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

@@ -0,0 +1,83 @@
+module Juvix.Compiler.Core.Data.InfoTableBuilder where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Language
+
+data InfoTableBuilder m a where
+  FreshSymbol :: InfoTableBuilder m Symbol
+  FreshTag :: InfoTableBuilder m Tag
+  RegisterIdent :: IdentInfo -> InfoTableBuilder m ()
+  RegisterConstructor :: ConstructorInfo -> InfoTableBuilder m ()
+  RegisterIdentNode :: Symbol -> Node -> InfoTableBuilder m ()
+  SetIdentArgsInfo :: Symbol -> [ArgumentInfo] -> InfoTableBuilder m ()
+  GetIdent :: Text -> InfoTableBuilder m (Maybe (Either Symbol Tag))
+  GetInfoTable :: InfoTableBuilder m InfoTable
+
+makeSem ''InfoTableBuilder
+
+hasIdent :: Member InfoTableBuilder r => Text -> Sem r Bool
+hasIdent txt = do
+  i <- getIdent txt
+  case i of
+    Just _ -> return True
+    Nothing -> return False
+
+getConstructorInfo :: Member InfoTableBuilder r => Tag -> Sem r ConstructorInfo
+getConstructorInfo tag = do
+  tab <- getInfoTable
+  return $ fromJust (HashMap.lookup tag (tab ^. infoConstructors))
+
+checkSymbolDefined :: Member InfoTableBuilder r => Symbol -> Sem r Bool
+checkSymbolDefined sym = do
+  tab <- getInfoTable
+  return $ HashMap.member sym (tab ^. identContext)
+
+data BuilderState = BuilderState
+  { _stateNextSymbol :: Word,
+    _stateNextUserTag :: Word,
+    _stateInfoTable :: InfoTable
+  }
+
+makeLenses ''BuilderState
+
+initBuilderState :: InfoTable -> BuilderState
+initBuilderState tab =
+  BuilderState
+    { _stateNextSymbol = fromIntegral $ HashMap.size (tab ^. infoIdents),
+      _stateNextUserTag = fromIntegral $ HashMap.size (tab ^. infoConstructors),
+      _stateInfoTable = tab
+    }
+
+runInfoTableBuilder :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
+runInfoTableBuilder tab =
+  fmap (first (^. stateInfoTable))
+    . runState (initBuilderState tab)
+    . reinterpret interp
+  where
+    interp :: InfoTableBuilder m a -> Sem (State BuilderState : r) a
+    interp = \case
+      FreshSymbol -> do
+        modify' (over stateNextSymbol (+ 1))
+        s <- get
+        return (s ^. stateNextSymbol - 1)
+      FreshTag -> do
+        modify' (over stateNextUserTag (+ 1))
+        s <- get
+        return (UserTag (s ^. stateNextUserTag - 1))
+      RegisterIdent ii -> do
+        modify' (over stateInfoTable (over infoIdents (HashMap.insert (ii ^. identSymbol) ii)))
+        modify' (over stateInfoTable (over identMap (HashMap.insert (ii ^. (identName . nameText)) (Left (ii ^. identSymbol)))))
+      RegisterConstructor ci -> do
+        modify' (over stateInfoTable (over infoConstructors (HashMap.insert (ci ^. constructorTag) ci)))
+        modify' (over stateInfoTable (over identMap (HashMap.insert (ci ^. (constructorName . nameText)) (Right (ci ^. constructorTag)))))
+      RegisterIdentNode sym node ->
+        modify' (over stateInfoTable (over identContext (HashMap.insert sym node)))
+      SetIdentArgsInfo sym argsInfo -> do
+        modify' (over stateInfoTable (over infoIdents (HashMap.adjust (set identArgsInfo argsInfo) sym)))
+        modify' (over stateInfoTable (over infoIdents (HashMap.adjust (set identArgsNum (length argsInfo)) sym)))
+      GetIdent txt -> do
+        s <- get
+        return $ HashMap.lookup txt (s ^. (stateInfoTable . identMap))
+      GetInfoTable ->
+        get <&> (^. stateInfoTable)

src/Juvix/Compiler/Core/Error.hs

@@ -0,0 +1,30 @@
+module Juvix.Compiler.Core.Error where
+
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Pretty
+
+data CoreError = CoreError
+  { _coreErrorMsg :: Text,
+    _coreErrorNode :: Maybe Node,
+    _coreErrorLoc :: Location
+  }
+
+makeLenses ''CoreError
+
+instance ToGenericError CoreError where
+  genericError e =
+    GenericError
+      { _genericErrorLoc = i,
+        _genericErrorMessage = AnsiText $ pretty @_ @AnsiStyle e,
+        _genericErrorIntervals = [i]
+      }
+    where
+      i = getLoc e
+
+instance Pretty CoreError where
+  pretty (CoreError {..}) = case _coreErrorNode of
+    Just node -> pretty _coreErrorMsg <> colon <> space <> pretty (ppTrace node)
+    Nothing -> pretty _coreErrorMsg
+
+instance HasLoc CoreError where
+  getLoc (CoreError {..}) = _coreErrorLoc

src/Juvix/Compiler/Core/Evaluator.hs

@@ -0,0 +1,175 @@
+{-# LANGUAGE BangPatterns #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Avoid restricted extensions" #-}
+{-# HLINT ignore "Avoid restricted flags" #-}
+
+module Juvix.Compiler.Core.Evaluator where
+
+import Control.Exception qualified as Exception
+import Data.HashMap.Strict qualified as HashMap
+import Debug.Trace qualified as Debug
+import GHC.Show as S
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Error
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NoDisplayInfo
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Pretty
+
+data EvalError = EvalError
+  { _evalErrorMsg :: !Text,
+    _evalErrorNode :: !(Maybe Node)
+  }
+
+makeLenses ''EvalError
+
+instance Show EvalError where
+  show :: EvalError -> String
+  show (EvalError {..}) =
+    "evaluation error: "
+      ++ fromText _evalErrorMsg
+      ++ case _evalErrorNode of
+        Nothing -> ""
+        Just node -> ": " ++ fromText (ppTrace node)
+
+-- We definitely do _not_ want to wrap the evaluator in an exception monad / the
+-- polysemy effects! This would almost double the execution time (whether an
+-- error occurred needs to be checked at every point). Evaluation errors should
+-- not happen for well-typed input (except perhaps division by zero), so it is
+-- reasonable to catch them only at the CLI toplevel and just exit when they
+-- occur. Use `catchEvalError` to catch evaluation errors in the IO monad.
+
+instance Exception.Exception EvalError
+
+-- `eval ctx env n` evalues a node `n` whose all free variables point into
+-- `env`. All nodes in `ctx` must be closed. All nodes in `env` must be values.
+-- Invariant for values v: eval ctx env v = v
+eval :: IdentContext -> Env -> Node -> Node
+eval !ctx !env0 = convertRuntimeNodes . eval' env0
+  where
+    evalError :: Text -> Node -> a
+    evalError !msg !node = Exception.throw (EvalError msg (Just node))
+
+    eval' :: Env -> Node -> Node
+    eval' !env !n = case n of
+      Var _ idx -> env !! idx
+      Ident _ sym -> eval' [] (lookupContext n sym)
+      Constant {} -> n
+      App i l r ->
+        case eval' env l of
+          Closure _ env' b -> let !v = eval' env r in eval' (v : env') b
+          v -> evalError "invalid application" (App i v (substEnv env r))
+      BuiltinApp _ op args -> applyBuiltin n env op args
+      Constr i tag args -> Constr i tag (map (eval' env) args)
+      Lambda i b -> Closure i env b
+      Let _ v b -> let !v' = eval' env v in eval' (v' : env) b
+      Case i v bs def ->
+        case eval' env v of
+          Constr _ tag args -> branch n env args tag def bs
+          v' -> evalError "matching on non-data" (substEnv env (Case i v' bs def))
+      Pi {} -> substEnv env n
+      Univ {} -> n
+      TypeConstr i sym args -> TypeConstr i sym (map (eval' env) args)
+      Closure {} -> n
+
+    branch :: Node -> Env -> [Node] -> Tag -> Maybe Node -> [CaseBranch] -> Node
+    branch n !env !args !tag !def = \case
+      (CaseBranch tag' _ b) : _ | tag' == tag -> eval' (revAppend args env) b
+      _ : bs' -> branch n env args tag def bs'
+      [] -> case def of
+        Just b -> eval' env b
+        Nothing -> evalError "no matching case branch" (substEnv env n)
+
+    applyBuiltin :: Node -> Env -> BuiltinOp -> [Node] -> Node
+    applyBuiltin _ env OpIntAdd [l, r] = nodeFromInteger (integerFromNode (eval' env l) + integerFromNode (eval' env r))
+    applyBuiltin _ env OpIntSub [l, r] = nodeFromInteger (integerFromNode (eval' env l) - integerFromNode (eval' env r))
+    applyBuiltin _ env OpIntMul [l, r] = nodeFromInteger (integerFromNode (eval' env l) * integerFromNode (eval' env r))
+    applyBuiltin n env OpIntDiv [l, r] =
+      case integerFromNode (eval' env r) of
+        0 -> evalError "division by zero" (substEnv env n)
+        k -> nodeFromInteger (div (integerFromNode (eval' env l)) k)
+    applyBuiltin n env OpIntMod [l, r] =
+      case integerFromNode (eval' env r) of
+        0 -> evalError "division by zero" (substEnv env n)
+        k -> nodeFromInteger (mod (integerFromNode (eval' env l)) k)
+    applyBuiltin _ env OpIntLt [l, r] = nodeFromBool (integerFromNode (eval' env l) < integerFromNode (eval' env r))
+    applyBuiltin _ env OpIntLe [l, r] = nodeFromBool (integerFromNode (eval' env l) <= integerFromNode (eval' env r))
+    applyBuiltin _ env OpEq [l, r] = nodeFromBool (eval' env l == eval' env r)
+    applyBuiltin _ env OpTrace [msg, x] = Debug.trace (printNode (eval' env msg)) (eval' env x)
+    applyBuiltin _ env OpFail [msg] =
+      Exception.throw (EvalError (fromString ("failure: " ++ printNode (eval' env msg))) Nothing)
+    applyBuiltin n env _ _ = evalError "invalid builtin application" (substEnv env n)
+
+    nodeFromInteger :: Integer -> Node
+    nodeFromInteger !int = Constant Info.empty (ConstInteger int)
+
+    nodeFromBool :: Bool -> Node
+    nodeFromBool True = Constr Info.empty (BuiltinTag TagTrue) []
+    nodeFromBool False = Constr Info.empty (BuiltinTag TagFalse) []
+
+    integerFromNode :: Node -> Integer
+    integerFromNode = \case
+      Constant _ (ConstInteger int) -> int
+      v -> evalError "not an integer" v
+
+    printNode :: Node -> String
+    printNode = \case
+      Constant _ (ConstString s) -> fromText s
+      v -> fromText $ ppPrint v
+
+    lookupContext :: Node -> Symbol -> Node
+    lookupContext n sym =
+      case HashMap.lookup sym ctx of
+        Just n' -> n'
+        Nothing -> evalError "symbol not defined" n
+
+-- Evaluate `node` and interpret the builtin IO actions.
+hEvalIO :: Handle -> Handle -> IdentContext -> Env -> Node -> IO Node
+hEvalIO hin hout ctx env node =
+  let node' = eval ctx env node
+   in case node' of
+        Constr _ (BuiltinTag TagReturn) [x] ->
+          return x
+        Constr _ (BuiltinTag TagBind) [x, f] -> do
+          x' <- hEvalIO hin hout ctx env x
+          hEvalIO hin hout ctx env (App Info.empty f x')
+        Constr _ (BuiltinTag TagWrite) [Constant _ (ConstString s)] -> do
+          hPutStr hout s
+          return unitNode
+        Constr _ (BuiltinTag TagWrite) [arg] -> do
+          hPutStr hout (ppPrint arg)
+          return unitNode
+        Constr _ (BuiltinTag TagReadLn) [] -> do
+          hFlush hout
+          Constant Info.empty . ConstString <$> hGetLine hin
+        _ ->
+          return node'
+  where
+    unitNode = Constr (Info.singleton (NoDisplayInfo ())) (BuiltinTag TagTrue) []
+
+evalIO :: IdentContext -> Env -> Node -> IO Node
+evalIO = hEvalIO stdin stdout
+
+-- Catch EvalError and convert it to CoreError. Needs a default location in case
+-- no location is available in EvalError.
+catchEvalError :: Location -> a -> IO (Either CoreError a)
+catchEvalError loc a =
+  Exception.catch
+    (Exception.evaluate a <&> Right)
+    (\(ex :: EvalError) -> return (Left (toCoreError loc ex)))
+
+catchEvalErrorIO :: Location -> IO a -> IO (Either CoreError a)
+catchEvalErrorIO loc ma =
+  Exception.catch
+    (Exception.evaluate ma >>= \ma' -> ma' <&> Right)
+    (\(ex :: EvalError) -> return (Left (toCoreError loc ex)))
+
+toCoreError :: Location -> EvalError -> CoreError
+toCoreError loc (EvalError {..}) =
+  CoreError
+    { _coreErrorMsg = mappend "evaluation error: " _evalErrorMsg,
+      _coreErrorNode = _evalErrorNode,
+      _coreErrorLoc = fromMaybe loc (lookupLocation =<< _evalErrorNode)
+    }

src/Juvix/Compiler/Core/Extra.hs

@@ -0,0 +1,98 @@
+module Juvix.Compiler.Core.Extra
+  ( module Juvix.Compiler.Core.Extra,
+    module Juvix.Compiler.Core.Extra.Base,
+    module Juvix.Compiler.Core.Extra.Recursors,
+    module Juvix.Compiler.Core.Extra.Info,
+  )
+where
+
+import Data.HashSet qualified as HashSet
+import Juvix.Compiler.Core.Extra.Base
+import Juvix.Compiler.Core.Extra.Info
+import Juvix.Compiler.Core.Extra.Recursors
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Language
+
+-- `isClosed` may short-circuit evaluation due to the use of `&&`, so it's not
+-- entirely reducible to `getFreeVars` in terms of computation time.
+isClosed :: Node -> Bool
+isClosed = ufoldN (&&) go
+  where
+    go :: Index -> Node -> Bool
+    go k = \case
+      Var _ idx | idx >= k -> False
+      _ -> True
+
+getFreeVars :: Node -> HashSet Index
+getFreeVars = gatherN go HashSet.empty
+  where
+    go :: Index -> HashSet Index -> Node -> HashSet Index
+    go k acc = \case
+      Var _ idx | idx >= k -> HashSet.insert (idx - k) acc
+      _ -> acc
+
+getIdents :: Node -> HashSet Symbol
+getIdents = gather go HashSet.empty
+  where
+    go :: HashSet Symbol -> Node -> HashSet Symbol
+    go acc = \case
+      Ident _ sym -> HashSet.insert sym acc
+      _ -> acc
+
+countFreeVarOccurrences :: Index -> Node -> Int
+countFreeVarOccurrences idx = gatherN go 0
+  where
+    go k acc = \case
+      Var _ idx' | idx' == idx + k -> acc + 1
+      _ -> acc
+
+-- increase all free variable indices by a given value
+shift :: Index -> Node -> Node
+shift 0 = id
+shift m = umapN go
+  where
+    go k n = case n of
+      Var i idx | idx >= k -> Var i (idx + m)
+      _ -> n
+
+-- substitute a term t for the free variable with de Bruijn index 0, avoiding
+-- variable capture
+subst :: Node -> Node -> Node
+subst t = umapN go
+  where
+    go k n = case n of
+      Var _ idx | idx == k -> shift k t
+      _ -> n
+
+-- reduce all beta redexes present in a term and the ones created immediately
+-- downwards (i.e., a "beta-development")
+developBeta :: Node -> Node
+developBeta = umap go
+  where
+    go :: Node -> Node
+    go n = case n of
+      App _ (Lambda _ body) arg -> subst arg body
+      _ -> n
+
+etaExpand :: Int -> Node -> Node
+etaExpand 0 n = n
+etaExpand k n = mkLambdas k (mkApp (shift k n) (map (Var Info.empty) (reverse [0 .. k - 1])))
+
+-- substitution of all free variables for values in an environment
+substEnv :: Env -> Node -> Node
+substEnv env = if null env then id else umapN go
+  where
+    go k n = case n of
+      Var _ idx | idx >= k -> env !! (idx - k)
+      _ -> n
+
+convertClosures :: Node -> Node
+convertClosures = umap go
+  where
+    go :: Node -> Node
+    go n = case n of
+      Closure i env b -> substEnv env (Lambda i b)
+      _ -> n
+
+convertRuntimeNodes :: Node -> Node
+convertRuntimeNodes = convertClosures

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

@@ -0,0 +1,180 @@
+module Juvix.Compiler.Core.Extra.Base where
+
+import Data.Functor.Identity
+import Data.List qualified as List
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.BinderInfo
+import Juvix.Compiler.Core.Language
+
+{------------------------------------------------------------------------}
+{- functions on Type -}
+
+-- unfold a type into the target and the arguments (left-to-right)
+unfoldType' :: Type -> (Type, [(Info, Type)])
+unfoldType' ty = case ty of
+  Pi i l r -> let (tgt, args) = unfoldType' r in (tgt, (i, l) : args)
+  _ -> (ty, [])
+
+{------------------------------------------------------------------------}
+{- functions on Node -}
+
+mkIf :: Info -> Node -> Node -> Node -> Node
+mkIf i v b1 b2 = Case i v [CaseBranch (BuiltinTag TagTrue) 0 b1] (Just b2)
+
+mkApp' :: Node -> [(Info, Node)] -> Node
+mkApp' = foldl' (\acc (i, n) -> App i acc n)
+
+mkApp :: Node -> [Node] -> Node
+mkApp = foldl' (App Info.empty)
+
+unfoldApp' :: Node -> (Node, [(Info, Node)])
+unfoldApp' = go []
+  where
+    go :: [(Info, Node)] -> Node -> (Node, [(Info, Node)])
+    go acc n = case n of
+      App i l r -> go ((i, r) : acc) l
+      _ -> (n, acc)
+
+unfoldApp :: Node -> (Node, [Node])
+unfoldApp = second (map snd) . unfoldApp'
+
+mkLambdas' :: [Info] -> Node -> Node
+mkLambdas' is n = foldr Lambda n is
+
+mkLambdas :: Int -> Node -> Node
+mkLambdas k = mkLambdas' (replicate k Info.empty)
+
+unfoldLambdas' :: Node -> ([Info], Node)
+unfoldLambdas' = go []
+  where
+    go :: [Info] -> Node -> ([Info], Node)
+    go acc n = case n of
+      Lambda i b -> go (i : acc) b
+      _ -> (acc, n)
+
+unfoldLambdas :: Node -> (Int, Node)
+unfoldLambdas = first length . unfoldLambdas'
+
+-- `NodeDetails` is a convenience datatype which provides the most commonly needed
+-- information about a node in a generic fashion.
+data NodeDetails = NodeDetails
+  { -- `nodeInfo` is the info associated with the node,
+    _nodeInfo :: Info,
+    -- `nodeChildren` are the children, in a fixed order, i.e., the immediate
+    -- recursive subnodes
+    _nodeChildren :: [Node],
+    -- `nodeChildBindersNum` is the number of binders introduced for each child
+    -- in the parent node. Same length and order as in `nodeChildren`.
+    _nodeChildBindersNum :: [Int],
+    -- `nodeChildBindersInfo` is information about binders for each child, if
+    -- present. Same length and order as in `nodeChildren`.
+    _nodeChildBindersInfo :: [Maybe [BinderInfo]],
+    -- `nodeReassemble` reassembles the node from the info and the children
+    -- (which should be in the same fixed order as in the `nodeChildren`
+    -- component).
+    _nodeReassemble :: Info -> [Node] -> Node
+  }
+
+makeLenses ''NodeDetails
+
+-- Destruct a node into NodeDetails. This is an ugly internal function used to
+-- implement more high-level accessors and recursors.
+destruct :: Node -> NodeDetails
+destruct = \case
+  Var i idx -> NodeDetails i [] [] [] (\i' _ -> Var i' idx)
+  Ident i sym -> NodeDetails i [] [] [] (\i' _ -> Ident i' sym)
+  Constant i c -> NodeDetails i [] [] [] (\i' _ -> Constant i' c)
+  App i l r -> NodeDetails i [l, r] [0, 0] [Nothing, Nothing] (\i' args' -> App i' (hd args') (args' !! 1))
+  BuiltinApp i op args -> NodeDetails i args (map (const 0) args) (map (const Nothing) args) (`BuiltinApp` op)
+  Constr i tag args -> NodeDetails i args (map (const 0) args) (map (const Nothing) args) (`Constr` tag)
+  Lambda i b -> NodeDetails i [b] [1] [fetchBinderInfo i] (\i' args' -> Lambda i' (hd args'))
+  Let i v b -> NodeDetails i [v, b] [0, 1] [Nothing, fetchBinderInfo i] (\i' args' -> Let i' (hd args') (args' !! 1))
+  Case i v bs Nothing ->
+    NodeDetails
+      i
+      (v : map (\(CaseBranch _ _ br) -> br) bs)
+      (0 : map (\(CaseBranch _ k _) -> k) bs)
+      (Nothing : fetchCaseBinderInfo i (replicate (length bs) Nothing))
+      ( \i' args' ->
+          Case
+            i'
+            (hd args')
+            ( zipWithExact
+                (\(CaseBranch tag k _) br' -> CaseBranch tag k br')
+                bs
+                (tl args')
+            )
+            Nothing
+      )
+  Case i v bs (Just def) ->
+    NodeDetails
+      i
+      (v : def : map (\(CaseBranch _ _ br) -> br) bs)
+      (0 : 0 : map (\(CaseBranch _ k _) -> k) bs)
+      (Nothing : Nothing : fetchCaseBinderInfo i (replicate (length bs) Nothing))
+      ( \i' args' ->
+          Case
+            i'
+            (hd args')
+            ( zipWithExact
+                (\(CaseBranch tag k _) br' -> CaseBranch tag k br')
+                bs
+                (tl (tl args'))
+            )
+            (Just (hd (tl args')))
+      )
+  Pi i ty b ->
+    NodeDetails i [ty, b] [0, 1] [Nothing, fetchBinderInfo i] (\i' args' -> Pi i' (hd args') (args' !! 1))
+  Univ i l ->
+    NodeDetails i [] [] [] (\i' _ -> Univ i' l)
+  TypeConstr i sym args ->
+    NodeDetails i args (map (const 0) args) (map (const Nothing) args) (`TypeConstr` sym)
+  Closure i env b ->
+    NodeDetails
+      i
+      (b : env)
+      (1 : map (const 0) env)
+      (fetchBinderInfo i : map (const Nothing) env)
+      (\i' args' -> Closure i' (tl args') (hd args'))
+  where
+    fetchBinderInfo :: Info -> Maybe [BinderInfo]
+    fetchBinderInfo i = case Info.lookup kBinderInfo i of
+      Just bi -> Just [bi]
+      Nothing -> Nothing
+
+    fetchCaseBinderInfo :: Info -> [Maybe [BinderInfo]] -> [Maybe [BinderInfo]]
+    fetchCaseBinderInfo i d = case Info.lookup kCaseBinderInfo i of
+      Just cbi -> map Just (cbi ^. infoBranchBinders)
+      Nothing -> d
+
+    hd :: [a] -> a
+    hd = List.head
+
+    tl :: [a] -> [a]
+    tl = List.tail
+
+children :: Node -> [Node]
+children = (^. nodeChildren) . destruct
+
+-- children together with the number of binders
+bchildren :: Node -> [(Int, Node)]
+bchildren n =
+  let ni = destruct n
+   in zipExact (ni ^. nodeChildBindersNum) (ni ^. nodeChildren)
+
+-- shallow children: not under binders
+schildren :: Node -> [Node]
+schildren = map snd . filter (\p -> fst p == 0) . bchildren
+
+getInfo :: Node -> Info
+getInfo = (^. nodeInfo) . destruct
+
+modifyInfoM :: Applicative m => (Info -> m Info) -> Node -> m Node
+modifyInfoM f n =
+  let ni = destruct n
+   in do
+        i' <- f (ni ^. nodeInfo)
+        return ((ni ^. nodeReassemble) i' (ni ^. nodeChildren))
+
+modifyInfo :: (Info -> Info) -> Node -> Node
+modifyInfo f n = runIdentity $ modifyInfoM (pure . f) n

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

@@ -0,0 +1,22 @@
+module Juvix.Compiler.Core.Extra.Info where
+
+import Juvix.Compiler.Core.Extra.Base
+import Juvix.Compiler.Core.Extra.Recursors
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.LocationInfo
+import Juvix.Compiler.Core.Info.NameInfo
+import Juvix.Compiler.Core.Language
+
+mapInfo :: (Info -> Info) -> Node -> Node
+mapInfo f = umap (modifyInfo f)
+
+removeInfo :: IsInfo i => Key i -> Node -> Node
+removeInfo k = mapInfo (Info.delete k)
+
+lookupLocation :: Node -> Maybe Location
+lookupLocation node =
+  case Info.lookup kLocationInfo (getInfo node) of
+    Just li -> Just (li ^. infoLocation)
+    Nothing -> case Info.lookup kNameInfo (getInfo node) of
+      Just ni -> Just $ ni ^. (infoName . nameLoc)
+      Nothing -> Nothing

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

@@ -0,0 +1,180 @@
+module Juvix.Compiler.Core.Extra.Recursors
+  ( module Juvix.Compiler.Core.Extra.Recursors,
+    BinderList,
+  )
+where
+
+import Data.Functor.Identity
+import Juvix.Compiler.Core.Data.BinderList (BinderList)
+import Juvix.Compiler.Core.Data.BinderList qualified as BL
+import Juvix.Compiler.Core.Extra.Base
+import Juvix.Compiler.Core.Info.BinderInfo
+import Juvix.Compiler.Core.Language
+
+{---------------------------------------------------------------------------------}
+{- General recursors on Node  -}
+
+-- a collector collects information top-down on a single path in the program
+-- tree
+data Collector a c = Collector
+  { _cEmpty :: c,
+    _cCollect :: a -> c -> c
+  }
+
+makeLenses ''Collector
+
+unitCollector :: Collector a ()
+unitCollector = Collector () (\_ _ -> ())
+
+binderInfoCollector :: Collector (Int, Maybe [BinderInfo]) (BinderList (Maybe BinderInfo))
+binderInfoCollector =
+  Collector
+    BL.empty
+    (\(k, bi) c -> if k == 0 then c else BL.prepend (map Just (fromJust bi)) c)
+
+binderNumCollector :: Collector (Int, Maybe [BinderInfo]) Index
+binderNumCollector = Collector 0 (\(k, _) c -> c + k)
+
+-- `umapG` maps the nodes bottom-up, i.e., when invoking the mapper function the
+-- recursive subnodes have already been mapped
+umapG ::
+  forall c m.
+  Monad m =>
+  Collector (Int, Maybe [BinderInfo]) c ->
+  (c -> Node -> m Node) ->
+  Node ->
+  m Node
+umapG coll f = go (coll ^. cEmpty)
+  where
+    go :: c -> Node -> m Node
+    go c n =
+      let ni = destruct n
+       in do
+            ns <-
+              sequence $
+                zipWith3Exact
+                  (\n' k bis -> go ((coll ^. cCollect) (k, bis) c) n')
+                  (ni ^. nodeChildren)
+                  (ni ^. nodeChildBindersNum)
+                  (ni ^. nodeChildBindersInfo)
+            f c ((ni ^. nodeReassemble) (ni ^. nodeInfo) ns)
+
+umapM :: Monad m => (Node -> m Node) -> Node -> m Node
+umapM f = umapG unitCollector (const f)
+
+umapMB :: Monad m => (BinderList (Maybe BinderInfo) -> Node -> m Node) -> Node -> m Node
+umapMB f = umapG binderInfoCollector f
+
+umapMN :: Monad m => (Index -> Node -> m Node) -> Node -> m Node
+umapMN f = umapG binderNumCollector f
+
+umap :: (Node -> Node) -> Node -> Node
+umap f n = runIdentity $ umapM (return . f) n
+
+umapB :: (BinderList (Maybe BinderInfo) -> Node -> Node) -> Node -> Node
+umapB f n = runIdentity $ umapMB (\is -> return . f is) n
+
+umapN :: (Index -> Node -> Node) -> Node -> Node
+umapN f n = runIdentity $ umapMN (\idx -> return . f idx) n
+
+-- `dmapG` maps the nodes top-down
+dmapG ::
+  forall c m.
+  Monad m =>
+  Collector (Int, Maybe [BinderInfo]) c ->
+  (c -> Node -> m Node) ->
+  Node ->
+  m Node
+dmapG coll f = go (coll ^. cEmpty)
+  where
+    go :: c -> Node -> m Node
+    go c n = do
+      n' <- f c n
+      let ni = destruct n'
+      ns <-
+        sequence $
+          zipWith3Exact
+            (\n'' k bis -> go ((coll ^. cCollect) (k, bis) c) n'')
+            (ni ^. nodeChildren)
+            (ni ^. nodeChildBindersNum)
+            (ni ^. nodeChildBindersInfo)
+      return ((ni ^. nodeReassemble) (ni ^. nodeInfo) ns)
+
+dmapM :: Monad m => (Node -> m Node) -> Node -> m Node
+dmapM f = dmapG unitCollector (const f)
+
+dmapMB :: Monad m => (BinderList (Maybe BinderInfo) -> Node -> m Node) -> Node -> m Node
+dmapMB f = dmapG binderInfoCollector f
+
+dmapMN :: Monad m => (Index -> Node -> m Node) -> Node -> m Node
+dmapMN f = dmapG binderNumCollector f
+
+dmap :: (Node -> Node) -> Node -> Node
+dmap f n = runIdentity $ dmapM (return . f) n
+
+dmapB :: (BinderList (Maybe BinderInfo) -> Node -> Node) -> Node -> Node
+dmapB f n = runIdentity $ dmapMB (\is -> return . f is) n
+
+dmapN :: (Index -> Node -> Node) -> Node -> Node
+dmapN f n = runIdentity $ dmapMN (\idx -> return . f idx) n
+
+-- `ufoldG` folds the tree bottom-up. The `uplus` argument combines the values -
+-- it should be commutative and associative.
+ufoldG ::
+  forall c a m.
+  Monad m =>
+  Collector (Int, Maybe [BinderInfo]) c ->
+  (a -> a -> a) ->
+  (c -> Node -> m a) ->
+  Node ->
+  m a
+ufoldG coll uplus f = go (coll ^. cEmpty)
+  where
+    go :: c -> Node -> m a
+    go c n = foldr (liftM2 uplus) (f c n) mas
+      where
+        ni :: NodeDetails
+        ni = destruct n
+        mas :: [m a]
+        mas =
+          zipWith3Exact
+            (\n' k bis -> go ((coll ^. cCollect) (k, bis) c) n')
+            (ni ^. nodeChildren)
+            (ni ^. nodeChildBindersNum)
+            (ni ^. nodeChildBindersInfo)
+
+ufoldM :: Monad m => (a -> a -> a) -> (Node -> m a) -> Node -> m a
+ufoldM uplus f = ufoldG unitCollector uplus (const f)
+
+ufoldMB :: Monad m => (a -> a -> a) -> (BinderList (Maybe BinderInfo) -> Node -> m a) -> Node -> m a
+ufoldMB uplus f = ufoldG binderInfoCollector uplus f
+
+ufoldMN :: Monad m => (a -> a -> a) -> (Index -> Node -> m a) -> Node -> m a
+ufoldMN uplus f = ufoldG binderNumCollector uplus f
+
+ufold :: (a -> a -> a) -> (Node -> a) -> Node -> a
+ufold uplus f n = runIdentity $ ufoldM uplus (return . f) n
+
+ufoldB :: (a -> a -> a) -> (BinderList (Maybe BinderInfo) -> Node -> a) -> Node -> a
+ufoldB uplus f n = runIdentity $ ufoldMB uplus (\is -> return . f is) n
+
+ufoldN :: (a -> a -> a) -> (Index -> Node -> a) -> Node -> a
+ufoldN uplus f n = runIdentity $ ufoldMN uplus (\idx -> return . f idx) n
+
+walk :: Monad m => (Node -> m ()) -> Node -> m ()
+walk = ufoldM mappend
+
+walkB :: Monad m => (BinderList (Maybe BinderInfo) -> Node -> m ()) -> Node -> m ()
+walkB = ufoldMB mappend
+
+walkN :: Monad m => (Index -> Node -> m ()) -> Node -> m ()
+walkN = ufoldMN mappend
+
+gather :: (a -> Node -> a) -> a -> Node -> a
+gather f acc n = run $ execState acc (walk (\n' -> modify' (`f` n')) n)
+
+gatherB :: (BinderList (Maybe BinderInfo) -> a -> Node -> a) -> a -> Node -> a
+gatherB f acc n = run $ execState acc (walkB (\is n' -> modify' (\a -> f is a n')) n)
+
+gatherN :: (Index -> a -> Node -> a) -> a -> Node -> a
+gatherN f acc n = run $ execState acc (walkN (\idx n' -> modify' (\a -> f idx a n')) n)

src/Juvix/Compiler/Core/Info.hs

@@ -0,0 +1,81 @@
+module Juvix.Compiler.Core.Info where
+
+{-
+  This file defines Infos stored in JuvixCore Nodes. The Info data structure
+  maps an info type to an info of that type.
+-}
+
+import Data.Dynamic
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Prelude
+
+class Typeable a => IsInfo a
+
+newtype Info = Info
+  { _infoMap :: HashMap TypeRep Dynamic
+  }
+
+type Key = Proxy
+
+makeLenses ''Info
+
+empty :: Info
+empty = Info HashMap.empty
+
+singleton :: forall a. IsInfo a => a -> Info
+singleton a = Juvix.Compiler.Core.Info.insert a Juvix.Compiler.Core.Info.empty
+
+member :: forall a. IsInfo a => Key a -> Info -> Bool
+member k i = HashMap.member (typeRep k) (i ^. infoMap)
+
+lookup :: IsInfo a => Key a -> Info -> Maybe a
+lookup k i = case HashMap.lookup (typeRep k) (i ^. infoMap) of
+  Just a -> Just $ fromDyn a impossible
+  Nothing -> Nothing
+
+lookupDefault :: IsInfo a => a -> Info -> a
+lookupDefault a i =
+  fromDyn (HashMap.lookupDefault (toDyn a) (typeOf a) (i ^. infoMap)) impossible
+
+lookup' :: IsInfo a => Key a -> Info -> a
+lookup' k i = fromMaybe impossible (Juvix.Compiler.Core.Info.lookup k i)
+
+(!) :: IsInfo a => Key a -> Info -> a
+(!) = lookup'
+
+insert :: IsInfo a => a -> Info -> Info
+insert a i = Info (HashMap.insert (typeOf a) (toDyn a) (i ^. infoMap))
+
+insertWith :: IsInfo a => (a -> a -> a) -> a -> Info -> Info
+insertWith f a i = Info (HashMap.insertWith f' (typeOf a) (toDyn a) (i ^. infoMap))
+  where
+    f' x1 x2 = toDyn (f (fromDyn x1 impossible) (fromDyn x2 impossible))
+
+delete :: IsInfo a => Key a -> Info -> Info
+delete k i = Info (HashMap.delete (typeRep k) (i ^. infoMap))
+
+adjust :: forall a. IsInfo a => (a -> a) -> Info -> Info
+adjust f i =
+  Info $
+    HashMap.adjust
+      (\x -> toDyn $ f $ fromDyn x impossible)
+      (typeRep (Proxy :: Proxy a))
+      (i ^. infoMap)
+
+update :: forall a. IsInfo a => (a -> Maybe a) -> Info -> Info
+update f i = Info (HashMap.update f' (typeRep (Proxy :: Proxy a)) (i ^. infoMap))
+  where
+    f' x = case f (fromDyn x impossible) of
+      Just y -> Just (toDyn y)
+      Nothing -> Nothing
+
+alter :: forall a. IsInfo a => (Maybe a -> Maybe a) -> Info -> Info
+alter f i = Info (HashMap.alter f' (typeRep (Proxy :: Proxy a)) (i ^. infoMap))
+  where
+    f' x = case y of
+      Just y' -> Just (toDyn y')
+      Nothing -> Nothing
+      where
+        y = case x of
+          Just x' -> f (fromDyn x' impossible)
+          Nothing -> f Nothing

src/Juvix/Compiler/Core/Info/BinderInfo.hs

@@ -0,0 +1,25 @@
+module Juvix.Compiler.Core.Info.BinderInfo where
+
+import Juvix.Compiler.Core.Language
+
+data BinderInfo = BinderInfo
+  { _infoName :: Name,
+    _infoType :: Type
+  }
+
+instance IsInfo BinderInfo
+
+kBinderInfo :: Key BinderInfo
+kBinderInfo = Proxy
+
+newtype CaseBinderInfo = CaseBinderInfo
+  { _infoBranchBinders :: [[BinderInfo]]
+  }
+
+instance IsInfo CaseBinderInfo
+
+kCaseBinderInfo :: Key CaseBinderInfo
+kCaseBinderInfo = Proxy
+
+makeLenses ''BinderInfo
+makeLenses ''CaseBinderInfo

src/Juvix/Compiler/Core/Info/BranchInfo.hs

@@ -0,0 +1,24 @@
+module Juvix.Compiler.Core.Info.BranchInfo where
+
+import Juvix.Compiler.Core.Language.Base
+
+newtype BranchInfo = BranchInfo
+  { _infoTagName :: Name
+  }
+
+instance IsInfo BranchInfo
+
+kBranchInfo :: Key BranchInfo
+kBranchInfo = Proxy
+
+newtype CaseBranchInfo = CaseBranchInfo
+  { _infoBranches :: [BranchInfo]
+  }
+
+instance IsInfo CaseBranchInfo
+
+kCaseBranchInfo :: Key CaseBranchInfo
+kCaseBranchInfo = Proxy
+
+makeLenses ''BranchInfo
+makeLenses ''CaseBranchInfo

src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs

@@ -0,0 +1,47 @@
+module Juvix.Compiler.Core.Info.FreeVarsInfo where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Language
+
+newtype FreeVarsInfo = FreeVarsInfo
+  { -- map free variables to the number of their occurrences
+    _infoFreeVars :: HashMap Index Int
+  }
+
+instance IsInfo FreeVarsInfo
+
+kFreeVarsInfo :: Key FreeVarsInfo
+kFreeVarsInfo = Proxy
+
+makeLenses ''FreeVarsInfo
+
+computeFreeVarsInfo :: Node -> Node
+computeFreeVarsInfo = umapN go
+  where
+    go :: Index -> Node -> Node
+    go k n = case n of
+      Var i idx | idx >= k -> Var (Info.insert fvi i) idx
+        where
+          fvi = FreeVarsInfo (HashMap.singleton (idx - k) 1)
+      _ -> modifyInfo (Info.insert fvi) n
+        where
+          fvi =
+            FreeVarsInfo $
+              foldr
+                ( \(m, n') acc ->
+                    HashMap.unionWith (+) acc $
+                      HashMap.mapKeys (\j -> j - m) $
+                        HashMap.filterWithKey
+                          (\j _ -> j < m)
+                          (getFreeVarsInfo n' ^. infoFreeVars)
+                )
+                mempty
+                (bchildren n)
+
+getFreeVarsInfo :: Node -> FreeVarsInfo
+getFreeVarsInfo = fromJust . Info.lookup kFreeVarsInfo . getInfo
+
+freeVarOccurrences :: Index -> Node -> Int
+freeVarOccurrences idx n = fromMaybe 0 (HashMap.lookup idx (getFreeVarsInfo n ^. infoFreeVars))

src/Juvix/Compiler/Core/Info/IdentInfo.hs

@@ -0,0 +1,41 @@
+module Juvix.Compiler.Core.Info.IdentInfo where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Language
+
+newtype IdentInfo = IdentInfo
+  { -- map symbols to the number of their occurrences
+    _infoIdents :: HashMap Symbol Int
+  }
+
+instance IsInfo IdentInfo
+
+kIdentInfo :: Key IdentInfo
+kIdentInfo = Proxy
+
+makeLenses ''IdentInfo
+
+computeIdentInfo :: Node -> Node
+computeIdentInfo = umap go
+  where
+    go :: Node -> Node
+    go n = case n of
+      Ident i sym -> Ident (Info.insert fvi i) sym
+        where
+          fvi = IdentInfo (HashMap.singleton sym 1)
+      _ -> modifyInfo (Info.insert fvi) n
+        where
+          fvi =
+            IdentInfo $
+              foldr
+                (HashMap.unionWith (+) . (^. infoIdents) . getIdentInfo)
+                mempty
+                (children n)
+
+getIdentInfo :: Node -> IdentInfo
+getIdentInfo = Info.lookupDefault (IdentInfo mempty) . getInfo
+
+identOccurrences :: Symbol -> Node -> Int
+identOccurrences sym = fromMaybe 0 . HashMap.lookup sym . (^. infoIdents) . getIdentInfo

src/Juvix/Compiler/Core/Info/LocationInfo.hs

@@ -0,0 +1,12 @@
+module Juvix.Compiler.Core.Info.LocationInfo where
+
+import Juvix.Compiler.Core.Language.Base
+
+newtype LocationInfo = LocationInfo {_infoLocation :: Location}
+
+instance IsInfo LocationInfo
+
+kLocationInfo :: Key LocationInfo
+kLocationInfo = Proxy
+
+makeLenses ''LocationInfo

src/Juvix/Compiler/Core/Info/NameInfo.hs

@@ -0,0 +1,12 @@
+module Juvix.Compiler.Core.Info.NameInfo where
+
+import Juvix.Compiler.Core.Language.Base
+
+newtype NameInfo = NameInfo {_infoName :: Name}
+
+instance IsInfo NameInfo
+
+kNameInfo :: Key NameInfo
+kNameInfo = Proxy
+
+makeLenses ''NameInfo

src/Juvix/Compiler/Core/Info/NoDisplayInfo.hs

@@ -0,0 +1,10 @@
+module Juvix.Compiler.Core.Info.NoDisplayInfo where
+
+import Juvix.Compiler.Core.Language.Base
+
+newtype NoDisplayInfo = NoDisplayInfo ()
+
+instance IsInfo NoDisplayInfo
+
+kNoDisplayInfo :: Key NoDisplayInfo
+kNoDisplayInfo = Proxy

src/Juvix/Compiler/Core/Info/TypeInfo.hs

@@ -0,0 +1,12 @@
+module Juvix.Compiler.Core.Info.TypeInfo where
+
+import Juvix.Compiler.Core.Language
+
+newtype TypeInfo = TypeInfo {_infoType :: Type}
+
+instance IsInfo TypeInfo
+
+kTypeInfo :: Key TypeInfo
+kTypeInfo = Proxy
+
+makeLenses ''TypeInfo

src/Juvix/Compiler/Core/Language.hs

@@ -0,0 +1,147 @@
+{-# OPTIONS_GHC -Wno-partial-fields #-}
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+
+{-# HLINT ignore "Avoid restricted flags" #-}
+
+module Juvix.Compiler.Core.Language
+  ( module Juvix.Compiler.Core.Language,
+    module Juvix.Compiler.Core.Language.Base,
+  )
+where
+
+{-
+  This file defines the tree representation of JuvixCore (Node datatype).
+-}
+
+import Juvix.Compiler.Core.Language.Base
+
+{---------------------------------------------------------------------------------}
+{- Program tree datatype -}
+
+-- `Node` is the type of nodes in the program tree. The nodes themselves
+-- contain only runtime-relevant information. Runtime-irrelevant annotations
+-- (including all type information) are stored in the infos associated with each
+-- node.
+data Node
+  = -- De Bruijn index of a locally bound variable.
+    Var {_varInfo :: !Info, _varIndex :: !Index}
+  | -- Global identifier of a function (with corresponding `Node` in the global
+    -- context).
+    Ident {_identInfo :: !Info, _identSymbol :: !Symbol}
+  | Constant {_constantInfo :: !Info, _constantValue :: !ConstantValue}
+  | App {_appInfo :: !Info, _appLeft :: !Node, _appRight :: !Node}
+  | -- A builtin application. A builtin has no corresponding Node. It is treated
+    -- specially by the evaluator and the code generator. For example, basic
+    -- arithmetic operations go into `Builtin`. The number of arguments supplied
+    -- must be equal to the number of arguments expected by the builtin
+    -- operation (this simplifies evaluation and code generation). If you need
+    -- partial application, eta-expand with lambdas, e.g., eta-expand `(+) 2` to
+    -- `\x -> (+) 2 x`. See Transformation/Eta.hs.
+    BuiltinApp {_builtinInfo :: !Info, _builtinOp :: !BuiltinOp, _builtinArgs :: ![Node]}
+  | -- A data constructor application. The number of arguments supplied must be
+    -- equal to the number of arguments expected by the constructor.
+    Constr
+      { _constrInfo :: !Info,
+        _constrTag :: !Tag,
+        _constrArgs :: ![Node]
+      }
+  | Lambda {_lambdaInfo :: !Info, _lambdaBody :: !Node}
+  | -- `let x := value in body` is not reducible to lambda + application for the purposes
+    -- of ML-polymorphic / dependent type checking or code generation!
+    Let {_letInfo :: !Info, _letValue :: !Node, _letBody :: !Node}
+  | -- One-level case matching on the tag of a data constructor: `Case value
+    -- branches default`. `Case` is lazy: only the selected branch is evaluated.
+    Case
+      { _caseInfo :: !Info,
+        _caseValue :: !Node,
+        _caseBranches :: ![CaseBranch],
+        _caseDefault :: !(Maybe Node)
+      }
+  | -- Dependent Pi-type. Compilation-time only. Pi implicitly introduces a binder
+    -- in the body, exactly like Lambda. So `Pi info ty body` is `Pi x : ty .
+    -- body` in more familiar notation, but references to `x` in `body` are via de
+    -- Bruijn index. For example, Pi A : Type . A -> A translates to (omitting
+    -- Infos): Pi (Univ level) (Pi (Var 0) (Var 1)).
+    Pi {_piInfo :: !Info, _piType :: !Type, _piBody :: !Type}
+  | -- Universe. Compilation-time only.
+    Univ {_univInfo :: !Info, _univLevel :: !Int}
+  | -- Type constructor application. Compilation-time only.
+    TypeConstr {_typeConstrInfo :: !Info, _typeConstrSymbol :: !Symbol, _typeConstrArgs :: ![Type]}
+  | -- Evaluation only: `Closure env body`
+    Closure
+      { _closureInfo :: !Info,
+        _closureEnv :: !Env,
+        _closureBody :: !Node
+      }
+
+-- Other things we might need in the future:
+-- - laziness annotations (converting these to closure/thunk creation should be
+--   done further down the pipeline)
+
+data ConstantValue
+  = ConstInteger !Integer
+  | ConstString !Text
+  deriving stock (Eq)
+
+-- Other things we might need in the future:
+-- - ConstFloat
+
+-- `CaseBranch tag argsNum branch`
+-- - `argsNum` is the number of arguments of the constructor tagged with `tag`,
+--   equal to the number of implicit binders above `branch`
+data CaseBranch = CaseBranch {_caseTag :: !Tag, _caseBindersNum :: !Int, _caseBranch :: !Node}
+  deriving stock (Eq)
+
+-- A node (term) is closed if it has no free variables, i.e., no de Bruijn
+-- indices pointing outside the term.
+
+-- Values are closed nodes of the following kinds:
+-- - Constant
+-- - Constr if all arguments are values
+-- - Closure
+--
+-- Whether something is a value matters only for the evaluation semantics. It
+-- doesn't matter much outside the evaluator.
+
+-- All nodes in an environment must be values.
+type Env = [Node]
+
+type Type = Node
+
+instance HasAtomicity Node where
+  atomicity = \case
+    Var {} -> Atom
+    Ident {} -> Atom
+    Constant {} -> Atom
+    App {} -> Aggregate appFixity
+    BuiltinApp {..} | null _builtinArgs -> Atom
+    BuiltinApp {} -> Aggregate lambdaFixity
+    Constr {..} | null _constrArgs -> Atom
+    Constr {} -> Aggregate lambdaFixity
+    Lambda {} -> Aggregate lambdaFixity
+    Let {} -> Aggregate lambdaFixity
+    Case {} -> Aggregate lambdaFixity
+    Pi {} -> Aggregate lambdaFixity
+    Univ {} -> Atom
+    TypeConstr {} -> Aggregate appFixity
+    Closure {} -> Aggregate lambdaFixity
+
+lambdaFixity :: Fixity
+lambdaFixity = Fixity (PrecNat 0) (Unary AssocPostfix)
+
+instance Eq Node where
+  (==) :: Node -> Node -> Bool
+  Var _ idx1 == Var _ idx2 = idx1 == idx2
+  Ident _ sym1 == Ident _ sym2 = sym1 == sym2
+  Constant _ v1 == Constant _ v2 = v1 == v2
+  App _ l1 r1 == App _ l2 r2 = l1 == l2 && r1 == r2
+  BuiltinApp _ op1 args1 == BuiltinApp _ op2 args2 = op1 == op2 && args1 == args2
+  Constr _ tag1 args1 == Constr _ tag2 args2 = tag1 == tag2 && args1 == args2
+  Lambda _ b1 == Lambda _ b2 = b1 == b2
+  Let _ v1 b1 == Let _ v2 b2 = v1 == v2 && b1 == b2
+  Case _ v1 bs1 def1 == Case _ v2 bs2 def2 = v1 == v2 && bs1 == bs2 && def1 == def2
+  Pi _ ty1 b1 == Pi _ ty2 b2 = ty1 == ty2 && b1 == b2
+  Univ _ l1 == Univ _ l2 = l1 == l2
+  TypeConstr _ sym1 args1 == TypeConstr _ sym2 args2 = sym1 == sym2 && args1 == args2
+  Closure _ env1 b1 == Closure _ env2 b2 = env1 == env2 && b1 == b2
+  _ == _ = False

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

@@ -0,0 +1,35 @@
+module Juvix.Compiler.Core.Language.Base
+  ( Info,
+    Key,
+    IsInfo,
+    module Juvix.Compiler.Core.Language.Builtins,
+    module Juvix.Prelude,
+    module Juvix.Compiler.Abstract.Data.Name,
+    Location,
+    Symbol,
+    Tag (..),
+    Index,
+  )
+where
+
+import Juvix.Compiler.Abstract.Data.Name
+import Juvix.Compiler.Core.Info (Info, IsInfo, Key)
+import Juvix.Compiler.Core.Language.Builtins
+import Juvix.Prelude
+
+type Location = Interval
+
+-- Consecutive symbol IDs for reachable user functions.
+type Symbol = Word
+
+-- Tag of a constructor, uniquely identifying it. Tag values are consecutive and
+-- separate from symbol IDs. We might need fixed special tags in Core for common
+-- "builtin" constructors, e.g., unit, nat, lists, pairs, so that the code
+-- generator can treat them specially.
+data Tag = BuiltinTag BuiltinDataTag | UserTag Word
+  deriving stock (Eq, Generic)
+
+instance Hashable Tag
+
+-- de Bruijn index
+type Index = Int

src/Juvix/Compiler/Core/Language/Builtins.hs

@@ -0,0 +1,52 @@
+module Juvix.Compiler.Core.Language.Builtins where
+
+import Juvix.Prelude
+
+-- Builtin operations which the evaluator and the code generator treat
+-- specially and non-uniformly.
+data BuiltinOp
+  = OpIntAdd
+  | OpIntSub
+  | OpIntMul
+  | OpIntDiv
+  | OpIntMod
+  | OpIntLt
+  | OpIntLe
+  | OpEq
+  | OpTrace
+  | OpFail
+  deriving stock (Eq)
+
+-- Builtin data tags
+data BuiltinDataTag
+  = TagTrue
+  | TagFalse
+  | TagReturn
+  | TagBind
+  | TagWrite
+  | TagReadLn
+  deriving stock (Eq, Generic)
+
+instance Hashable BuiltinDataTag
+
+builtinOpArgsNum :: BuiltinOp -> Int
+builtinOpArgsNum = \case
+  OpIntAdd -> 2
+  OpIntSub -> 2
+  OpIntMul -> 2
+  OpIntDiv -> 2
+  OpIntMod -> 2
+  OpIntLt -> 2
+  OpIntLe -> 2
+  OpEq -> 2
+  OpTrace -> 2
+  OpFail -> 1
+
+builtinConstrArgsNum :: BuiltinDataTag -> Int
+builtinConstrArgsNum = \case
+  TagTrue -> 0
+  TagFalse -> 0
+  TagReturn -> 1
+  TagBind -> 2
+  TagWrite -> 1
+  TagReadLn -> 0

src/Juvix/Compiler/Core/Pretty.hs

@@ -0,0 +1,25 @@
+module Juvix.Compiler.Core.Pretty
+  ( module Juvix.Compiler.Core.Pretty,
+    module Juvix.Compiler.Core.Pretty.Base,
+    module Juvix.Compiler.Core.Pretty.Options,
+    module Juvix.Data.PPOutput,
+  )
+where
+
+import Juvix.Compiler.Core.Pretty.Base
+import Juvix.Compiler.Core.Pretty.Options
+import Juvix.Data.PPOutput
+import Juvix.Prelude
+import Prettyprinter.Render.Terminal qualified as Ansi
+
+ppOutDefault :: PrettyCode c => c -> AnsiText
+ppOutDefault = AnsiText . PPOutput . doc defaultOptions
+
+ppOut :: PrettyCode c => Options -> c -> AnsiText
+ppOut o = AnsiText . PPOutput . doc o
+
+ppTrace :: PrettyCode c => c -> Text
+ppTrace = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc defaultOptions
+
+ppPrint :: PrettyCode c => c -> Text
+ppPrint = show . ppOutDefault

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

@@ -0,0 +1,255 @@
+module Juvix.Compiler.Core.Pretty.Base
+  ( module Juvix.Compiler.Core.Pretty.Base,
+    module Juvix.Data.CodeAnn,
+    module Juvix.Compiler.Core.Pretty.Options,
+  )
+where
+
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.BinderInfo as BinderInfo
+import Juvix.Compiler.Core.Info.BranchInfo as BranchInfo
+import Juvix.Compiler.Core.Info.NameInfo as NameInfo
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Pretty.Options
+import Juvix.Data.CodeAnn
+import Juvix.Extra.Strings qualified as Str
+
+doc :: PrettyCode c => Options -> c -> Doc Ann
+doc opts =
+  run
+    . runReader opts
+    . ppCode
+
+class PrettyCode c where
+  ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
+
+runPrettyCode :: PrettyCode c => Options -> c -> Doc Ann
+runPrettyCode opts = run . runReader opts . ppCode
+
+instance PrettyCode NameId where
+  ppCode (NameId k) = return (pretty k)
+
+instance PrettyCode Name where
+  ppCode n = do
+    showNameId <- asks (^. optShowNameIds)
+    return (prettyName showNameId n)
+
+instance PrettyCode BuiltinOp where
+  ppCode = \case
+    OpIntAdd -> return kwPlus
+    OpIntSub -> return kwMinus
+    OpIntMul -> return kwMul
+    OpIntDiv -> return kwDiv
+    OpIntMod -> return kwMod
+    OpIntLt -> return kwLess
+    OpIntLe -> return kwLessEquals
+    OpEq -> return kwEquals
+    OpTrace -> return kwTrace
+    OpFail -> return kwFail
+
+instance PrettyCode BuiltinDataTag where
+  ppCode = \case
+    TagTrue -> return $ annotate (AnnKind KNameConstructor) (pretty ("true" :: String))
+    TagFalse -> return $ annotate (AnnKind KNameConstructor) (pretty ("false" :: String))
+    TagReturn -> return $ annotate (AnnKind KNameConstructor) (pretty ("return" :: String))
+    TagBind -> return $ annotate (AnnKind KNameConstructor) (pretty ("bind" :: String))
+    TagWrite -> return $ annotate (AnnKind KNameConstructor) (pretty ("write" :: String))
+    TagReadLn -> return $ annotate (AnnKind KNameConstructor) (pretty ("readLn" :: String))
+
+instance PrettyCode Tag where
+  ppCode = \case
+    BuiltinTag tag -> ppCode tag
+    UserTag tag -> return $ kwUnnamedConstr <> pretty tag
+
+instance PrettyCode Node where
+  ppCode node = case node of
+    Var {..} ->
+      case Info.lookup kNameInfo _varInfo of
+        Just ni -> do
+          showDeBruijn <- asks (^. optShowDeBruijnIndices)
+          n <- ppCode (ni ^. NameInfo.infoName)
+          if showDeBruijn
+            then return $ n <> kwDeBruijnVar <> pretty _varIndex
+            else return n
+        Nothing -> return $ kwDeBruijnVar <> pretty _varIndex
+    Ident {..} ->
+      case Info.lookup kNameInfo _identInfo of
+        Just ni -> ppCode (ni ^. NameInfo.infoName)
+        Nothing -> return $ kwUnnamedIdent <> pretty _identSymbol
+    Constant _ (ConstInteger int) ->
+      return $ annotate AnnLiteralInteger (pretty int)
+    Constant _ (ConstString txt) ->
+      return $ annotate AnnLiteralString (pretty (show txt :: String))
+    App {..} -> do
+      l' <- ppLeftExpression appFixity _appLeft
+      r' <- ppRightExpression appFixity _appRight
+      return $ l' <+> r'
+    BuiltinApp {..} -> do
+      args' <- mapM (ppRightExpression appFixity) _builtinArgs
+      op' <- ppCode _builtinOp
+      return $ foldl' (<+>) op' args'
+    Constr {..} -> do
+      args' <- mapM (ppRightExpression appFixity) _constrArgs
+      n' <-
+        case Info.lookup kNameInfo _constrInfo of
+          Just ni -> ppCode (ni ^. NameInfo.infoName)
+          Nothing -> ppCode _constrTag
+      return $ foldl' (<+>) n' args'
+    Lambda {} -> do
+      let (infos, body) = unfoldLambdas' node
+      pplams <- mapM ppLam infos
+      b <- ppCode body
+      return $ foldl' (flip (<+>)) b pplams
+      where
+        ppLam :: Member (Reader Options) r => Info -> Sem r (Doc Ann)
+        ppLam i =
+          case Info.lookup kBinderInfo i of
+            Just bi -> do
+              n <- ppCode (bi ^. BinderInfo.infoName)
+              return $ kwLambda <> n
+            Nothing -> return $ kwLambda <> kwQuestion
+    Let {..} -> do
+      n' <-
+        case Info.lookup kBinderInfo _letInfo of
+          Just bi -> ppCode (bi ^. BinderInfo.infoName)
+          Nothing -> return kwQuestion
+      v' <- ppCode _letValue
+      b' <- ppCode _letBody
+      return $ kwLet <+> n' <+> kwAssign <+> v' <+> kwIn <+> b'
+    Case {..} -> do
+      bns <-
+        case Info.lookup kCaseBinderInfo _caseInfo of
+          Just ci -> mapM (mapM (ppCode . (^. BinderInfo.infoName))) (ci ^. infoBranchBinders)
+          Nothing -> mapM (\(CaseBranch _ n _) -> replicateM n (return kwQuestion)) _caseBranches
+      cns <-
+        case Info.lookup kCaseBranchInfo _caseInfo of
+          Just ci -> mapM (ppCode . (^. BranchInfo.infoTagName)) (ci ^. infoBranches)
+          Nothing -> mapM (\(CaseBranch tag _ _) -> ppCode tag) _caseBranches
+      let bs = map (\(CaseBranch _ _ br) -> br) _caseBranches
+      v <- ppCode _caseValue
+      bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwMapsto <+> br') cns bns bs
+      bs'' <-
+        case _caseDefault of
+          Just def -> do
+            d' <- ppCode def
+            return $ bs' ++ [kwDefault <+> kwMapsto <+> d']
+          Nothing -> return bs'
+      let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs''
+      return $ kwCase <+> v <+> kwOf <+> bss
+    Pi {..} ->
+      case Info.lookup kBinderInfo _piInfo of
+        Just bi -> do
+          n <- ppCode (bi ^. BinderInfo.infoName)
+          b <- ppCode _piBody
+          return $ kwLambda <> n <+> b
+        Nothing -> do
+          b <- ppCode _piBody
+          return $ kwLambda <> kwQuestion <+> b
+    Univ {..} ->
+      return $ kwType <+> pretty _univLevel
+    TypeConstr {..} -> do
+      args' <- mapM (ppRightExpression appFixity) _typeConstrArgs
+      n' <-
+        case Info.lookup kNameInfo _typeConstrInfo of
+          Just ni -> ppCode (ni ^. NameInfo.infoName)
+          Nothing -> return $ kwUnnamedIdent <> pretty _typeConstrSymbol
+      return $ foldl' (<+>) n' args'
+    Closure {..} ->
+      ppCode (substEnv _closureEnv (Lambda _closureInfo _closureBody))
+
+instance PrettyCode a => PrettyCode (NonEmpty a) where
+  ppCode x = do
+    cs <- mapM ppCode (toList x)
+    return $ encloseSep "(" ")" ", " cs
+
+{--------------------------------------------------------------------------------}
+{- helper functions -}
+
+parensIf :: Bool -> Doc Ann -> Doc Ann
+parensIf t = if t then parens else id
+
+ppPostExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppPostExpression = ppLRExpression isPostfixAssoc
+
+ppRightExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppRightExpression = ppLRExpression isRightAssoc
+
+ppLeftExpression ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppLeftExpression = ppLRExpression isLeftAssoc
+
+ppLRExpression ::
+  (HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
+  (Fixity -> Bool) ->
+  Fixity ->
+  a ->
+  Sem r (Doc Ann)
+ppLRExpression associates fixlr e =
+  parensIf (atomParens associates (atomicity e) fixlr)
+    <$> ppCode e
+
+{--------------------------------------------------------------------------------}
+{- keywords -}
+
+kwDeBruijnVar :: Doc Ann
+kwDeBruijnVar = keyword Str.deBruijnVar
+
+kwUnnamedIdent :: Doc Ann
+kwUnnamedIdent = keyword Str.exclamation
+
+kwUnnamedConstr :: Doc Ann
+kwUnnamedConstr = keyword Str.exclamation
+
+kwQuestion :: Doc Ann
+kwQuestion = keyword Str.questionMark
+
+kwLess :: Doc Ann
+kwLess = keyword Str.less
+
+kwLessEquals :: Doc Ann
+kwLessEquals = keyword Str.lessEqual
+
+kwPlus :: Doc Ann
+kwPlus = keyword Str.plus
+
+kwMinus :: Doc Ann
+kwMinus = keyword Str.minus
+
+kwMul :: Doc Ann
+kwMul = keyword Str.mul
+
+kwDiv :: Doc Ann
+kwDiv = keyword Str.div
+
+kwMod :: Doc Ann
+kwMod = keyword Str.mod
+
+kwCase :: Doc Ann
+kwCase = keyword Str.case_
+
+kwOf :: Doc Ann
+kwOf = keyword Str.of_
+
+kwDefault :: Doc Ann
+kwDefault = keyword Str.underscore
+
+kwPi :: Doc Ann
+kwPi = keyword Str.pi_
+
+kwTrace :: Doc Ann
+kwTrace = keyword Str.trace_
+
+kwFail :: Doc Ann
+kwFail = keyword Str.fail_

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

@@ -0,0 +1,19 @@
+module Juvix.Compiler.Core.Pretty.Options where
+
+import Juvix.Prelude
+
+data Options = Options
+  { _optIndent :: Int,
+    _optShowNameIds :: Bool,
+    _optShowDeBruijnIndices :: Bool
+  }
+
+defaultOptions :: Options
+defaultOptions =
+  Options
+    { _optIndent = 2,
+      _optShowNameIds = False,
+      _optShowDeBruijnIndices = False
+    }
+
+makeLenses ''Options

src/Juvix/Compiler/Core/Transformation.hs

@@ -0,0 +1,10 @@
+module Juvix.Compiler.Core.Transformation
+  ( module Juvix.Compiler.Core.Transformation.Base,
+    module Juvix.Compiler.Core.Transformation.Eta,
+    module Juvix.Compiler.Core.Transformation.LambdaLifting,
+  )
+where
+
+import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.Eta
+import Juvix.Compiler.Core.Transformation.LambdaLifting

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

@@ -0,0 +1,22 @@
+module Juvix.Compiler.Core.Transformation.Base
+  ( module Juvix.Compiler.Core.Transformation.Base,
+    module Juvix.Compiler.Core.Data.InfoTable,
+    module Juvix.Compiler.Core.Language,
+  )
+where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Data.InfoTableBuilder
+import Juvix.Compiler.Core.Language
+
+type Transformation = InfoTable -> InfoTable
+
+mapT :: (Node -> Node) -> InfoTable -> InfoTable
+mapT f tab = tab {_identContext = HashMap.map f (tab ^. identContext)}
+
+mapT' :: (Node -> Sem (InfoTableBuilder ': r) Node) -> InfoTable -> Sem r InfoTable
+mapT' f tab = fmap fst $ runInfoTableBuilder tab $ do
+  mapM_
+    (\(k, v) -> f v >>= registerIdentNode k)
+    (HashMap.toList (tab ^. identContext))

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

@@ -0,0 +1,55 @@
+module Juvix.Compiler.Core.Transformation.Eta
+  ( module Juvix.Compiler.Core.Transformation.Eta,
+    module Juvix.Compiler.Core.Transformation.Base,
+  )
+where
+
+import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+
+etaExpandBuiltins :: Node -> Node
+etaExpandBuiltins = umap go
+  where
+    go :: Node -> Node
+    go n = case n of
+      BuiltinApp {..}
+        | builtinOpArgsNum _builtinOp > length _builtinArgs ->
+            etaExpand (builtinOpArgsNum _builtinOp - length _builtinArgs) n
+      _ -> n
+
+etaExpandConstrs :: (Tag -> Int) -> Node -> Node
+etaExpandConstrs argsNum = umap go
+  where
+    go :: Node -> Node
+    go n = case n of
+      Constr {..}
+        | k > length _constrArgs ->
+            etaExpand (k - length _constrArgs) n
+        where
+          k = argsNum _constrTag
+      _ -> n
+
+squashApps :: Node -> Node
+squashApps = dmap go
+  where
+    go :: Node -> Node
+    go n =
+      let (l, args) = unfoldApp n
+       in case l of
+            Constr i tag args' -> Constr i tag (args' ++ args)
+            BuiltinApp i op args' -> BuiltinApp i op (args' ++ args)
+            _ -> n
+
+etaExpandApps :: InfoTable -> Node -> Node
+etaExpandApps tab =
+  squashApps . etaExpandConstrs constrArgsNum . etaExpandBuiltins . squashApps
+  where
+    constrArgsNum :: Tag -> Int
+    constrArgsNum tag =
+      case HashMap.lookup tag (tab ^. infoConstructors) of
+        Just ci -> ci ^. constructorArgsNum
+        Nothing -> 0
+
+etaExpansionApps :: Transformation
+etaExpansionApps tab = mapT (etaExpandApps tab) tab

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

@@ -0,0 +1,16 @@
+module Juvix.Compiler.Core.Transformation.LambdaLifting
+  ( module Juvix.Compiler.Core.Transformation.LambdaLifting,
+    module Juvix.Compiler.Core.Transformation.Base,
+  )
+where
+
+import Juvix.Compiler.Core.Data.InfoTableBuilder
+import Juvix.Compiler.Core.Transformation.Base
+
+lambdaLiftNode :: Member InfoTableBuilder r => Node -> Sem r Node
+lambdaLiftNode _ = do
+  void freshSymbol
+  error "not yet implemented"
+
+lambdaLifting :: Transformation
+lambdaLifting = run . mapT' lambdaLiftNode

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

@@ -0,0 +1,664 @@
+module Juvix.Compiler.Core.Translation.FromSource
+  ( module Juvix.Compiler.Core.Translation.FromSource,
+    module Juvix.Parser.Error,
+  )
+where
+
+import Control.Monad.Trans.Class (lift)
+import Data.HashMap.Strict qualified as HashMap
+import Data.List qualified as List
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Data.InfoTableBuilder
+import Juvix.Compiler.Core.Extra.Base
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.BinderInfo as BinderInfo
+import Juvix.Compiler.Core.Info.BranchInfo as BranchInfo
+import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
+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.Parser.Error
+import Text.Megaparsec qualified as P
+
+parseText :: InfoTable -> Text -> Either ParserError (InfoTable, Maybe Node)
+parseText = runParser "" ""
+
+-- Note: only new symbols and tags that are not in the InfoTable already will be
+-- generated during parsing, but nameIds are generated starting from 0
+-- regardless of the names already in the InfoTable
+runParser :: FilePath -> FilePath -> InfoTable -> Text -> Either ParserError (InfoTable, Maybe Node)
+runParser root fileName tab input =
+  case run $
+    runInfoTableBuilder tab $
+      runReader params $
+        runNameIdGen $
+          P.runParserT parseToplevel fileName input of
+    (_, Left err) -> Left (ParserError err)
+    (tbl, Right r) -> Right (tbl, r)
+  where
+    params =
+      ParserParams
+        { _parserParamsRoot = root
+        }
+
+starType :: Type
+starType = Pi Info.empty (Univ Info.empty 0) (Var Info.empty 0)
+
+freshName ::
+  Members '[InfoTableBuilder, NameIdGen] r =>
+  NameKind ->
+  Text ->
+  Interval ->
+  Sem r Name
+freshName kind txt i = do
+  nid <- freshNameId
+  return $
+    Name
+      { _nameText = txt,
+        _nameId = nid,
+        _nameKind = kind,
+        _namePretty = txt,
+        _nameLoc = i
+      }
+
+declareBuiltinConstr ::
+  Members '[InfoTableBuilder, NameIdGen] r =>
+  BuiltinDataTag ->
+  Text ->
+  Interval ->
+  Sem r ()
+declareBuiltinConstr btag nameTxt i = do
+  name <- freshName KNameConstructor nameTxt i
+  registerConstructor
+    ( ConstructorInfo
+        { _constructorName = name,
+          _constructorTag = BuiltinTag btag,
+          _constructorType = starType,
+          _constructorArgsNum = builtinConstrArgsNum btag
+        }
+    )
+
+guardSymbolNotDefined ::
+  Member InfoTableBuilder r =>
+  Symbol ->
+  ParsecS r () ->
+  ParsecS r ()
+guardSymbolNotDefined sym err = do
+  b <- lift $ checkSymbolDefined sym
+  when b err
+
+declareBuiltins :: Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r => ParsecS r ()
+declareBuiltins = do
+  loc <- curLoc
+  let i = mkInterval loc loc
+  lift $ declareBuiltinConstr TagTrue "true" i
+  lift $ declareBuiltinConstr TagFalse "false" i
+  lift $ declareBuiltinConstr TagReturn "return" i
+  lift $ declareBuiltinConstr TagBind "bind" i
+  lift $ declareBuiltinConstr TagWrite "write" i
+  lift $ declareBuiltinConstr TagReadLn "readLn" i
+
+parseToplevel ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r (Maybe Node)
+parseToplevel = do
+  declareBuiltins
+  space
+  P.endBy statement kwSemicolon
+  r <- optional expression
+  P.eof
+  return r
+
+statement ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r ()
+statement = statementDef <|> statementConstr
+
+statementDef ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r ()
+statementDef = do
+  kwDef
+  off <- P.getOffset
+  (txt, i) <- identifierL
+  r <- lift (getIdent txt)
+  case r of
+    Just (Left sym) -> do
+      guardSymbolNotDefined
+        sym
+        (parseFailure off ("duplicate definition of: " ++ fromText txt))
+      parseDefinition sym
+    Just (Right {}) ->
+      parseFailure off ("duplicate identifier: " ++ fromText txt)
+    Nothing -> do
+      sym <- lift freshSymbol
+      name <- lift $ freshName KNameFunction txt i
+      let info =
+            IdentInfo
+              { _identName = name,
+                _identSymbol = sym,
+                _identType = starType,
+                _identArgsNum = 0,
+                _identArgsInfo = [],
+                _identIsExported = False
+              }
+      lift $ registerIdent info
+      void $ optional (parseDefinition sym)
+
+parseDefinition ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Symbol ->
+  ParsecS r ()
+parseDefinition sym = do
+  kwAssignment
+  node <- expression
+  lift $ registerIdentNode sym node
+  let (is, _) = unfoldLambdas' node
+  lift $ setIdentArgsInfo sym (map toArgumentInfo is)
+  where
+    toArgumentInfo :: Info -> ArgumentInfo
+    toArgumentInfo i =
+      case Info.lookup kBinderInfo i of
+        Just bi ->
+          ArgumentInfo
+            { _argumentName = bi ^. BinderInfo.infoName,
+              _argumentType = bi ^. BinderInfo.infoType,
+              _argumentIsImplicit = False
+            }
+        Nothing -> error "missing binder info"
+
+statementConstr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r ()
+statementConstr = do
+  kwConstr
+  off <- P.getOffset
+  (txt, i) <- identifierL
+  (argsNum, _) <- number 0 128
+  dupl <- lift (hasIdent txt)
+  when
+    dupl
+    (parseFailure off ("duplicate identifier: " ++ fromText txt))
+  tag <- lift freshTag
+  name <- lift $ freshName KNameConstructor txt i
+  let info =
+        ConstructorInfo
+          { _constructorName = name,
+            _constructorTag = tag,
+            _constructorType = starType,
+            _constructorArgsNum = argsNum
+          }
+  lift $ registerConstructor info
+
+expression ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r Node
+expression = do
+  node <- expr 0 mempty
+  tab <- lift getInfoTable
+  return $ etaExpandApps tab node
+
+expr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  -- current de Bruijn index, i.e., the number of binders upwards
+  Index ->
+  -- reverse de Bruijn indices
+  HashMap Text Index ->
+  ParsecS r Node
+expr varsNum vars = ioExpr varsNum vars
+
+ioExpr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+ioExpr varsNum vars = cmpExpr varsNum vars >>= ioExpr' varsNum vars
+
+ioExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+ioExpr' varsNum vars node = do
+  bindExpr' varsNum vars node
+    <|> seqExpr' varsNum vars node
+    <|> return node
+
+bindExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+bindExpr' varsNum vars node = do
+  kwBind
+  node' <- cmpExpr varsNum vars
+  ioExpr' varsNum vars (Constr Info.empty (BuiltinTag TagBind) [node, node'])
+
+seqExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+seqExpr' varsNum vars node = do
+  ((), i) <- interval kwSeq
+  node' <- cmpExpr (varsNum + 1) vars
+  name <- lift $ freshName KNameLocal "_" i
+  ioExpr' varsNum vars $
+    Constr
+      Info.empty
+      (BuiltinTag TagBind)
+      [node, Lambda (Info.singleton (BinderInfo name starType)) node']
+
+cmpExpr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+cmpExpr varsNum vars = arithExpr varsNum vars >>= cmpExpr' varsNum vars
+
+cmpExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+cmpExpr' varsNum vars node =
+  eqExpr' varsNum vars node
+    <|> ltExpr' varsNum vars node
+    <|> leExpr' varsNum vars node
+    <|> gtExpr' varsNum vars node
+    <|> geExpr' varsNum vars node
+    <|> return node
+
+eqExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+eqExpr' varsNum vars node = do
+  kwEq
+  node' <- arithExpr varsNum vars
+  return $ BuiltinApp Info.empty OpEq [node, node']
+
+ltExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+ltExpr' varsNum vars node = do
+  kwLt
+  node' <- arithExpr varsNum vars
+  return $ BuiltinApp Info.empty OpIntLt [node, node']
+
+leExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+leExpr' varsNum vars node = do
+  kwLe
+  node' <- arithExpr varsNum vars
+  return $ BuiltinApp Info.empty OpIntLe [node, node']
+
+gtExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+gtExpr' varsNum vars node = do
+  kwGt
+  node' <- arithExpr varsNum vars
+  return $ BuiltinApp Info.empty OpIntLt [node', node]
+
+geExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+geExpr' varsNum vars node = do
+  kwGe
+  node' <- arithExpr varsNum vars
+  return $ BuiltinApp Info.empty OpIntLe [node', node]
+
+arithExpr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+arithExpr varsNum vars = factorExpr varsNum vars >>= arithExpr' varsNum vars
+
+arithExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+arithExpr' varsNum vars node =
+  plusExpr' varsNum vars node
+    <|> minusExpr' varsNum vars node
+    <|> return node
+
+plusExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+plusExpr' varsNum vars node = do
+  kwPlus
+  node' <- factorExpr varsNum vars
+  arithExpr' varsNum vars (BuiltinApp Info.empty OpIntAdd [node, node'])
+
+minusExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+minusExpr' varsNum vars node = do
+  kwMinus
+  node' <- factorExpr varsNum vars
+  arithExpr' varsNum vars (BuiltinApp Info.empty OpIntSub [node, node'])
+
+factorExpr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+factorExpr varsNum vars = appExpr varsNum vars >>= factorExpr' varsNum vars
+
+factorExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+factorExpr' varsNum vars node =
+  mulExpr' varsNum vars node
+    <|> divExpr' varsNum vars node
+    <|> modExpr' varsNum vars node
+    <|> return node
+
+mulExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+mulExpr' varsNum vars node = do
+  kwMul
+  node' <- appExpr varsNum vars
+  factorExpr' varsNum vars (BuiltinApp Info.empty OpIntMul [node, node'])
+
+divExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+divExpr' varsNum vars node = do
+  kwDiv
+  node' <- appExpr varsNum vars
+  factorExpr' varsNum vars (BuiltinApp Info.empty OpIntDiv [node, node'])
+
+modExpr' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  Node ->
+  ParsecS r Node
+modExpr' varsNum vars node = do
+  kwMod
+  node' <- appExpr varsNum vars
+  factorExpr' varsNum vars (BuiltinApp Info.empty OpIntMod [node, node'])
+
+appExpr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+appExpr varsNum vars = builtinAppExpr varsNum vars <|> atoms varsNum vars
+
+builtinAppExpr ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+builtinAppExpr varsNum vars = do
+  op <-
+    (kwEq >> return OpEq)
+      <|> (kwLt >> return OpIntLt)
+      <|> (kwLe >> return OpIntLe)
+      <|> (kwPlus >> return OpIntAdd)
+      <|> (kwMinus >> return OpIntSub)
+      <|> (kwDiv >> return OpIntDiv)
+      <|> (kwMul >> return OpIntMul)
+      <|> (kwTrace >> return OpTrace)
+      <|> (kwFail >> return OpFail)
+  args <- P.many (atom varsNum vars)
+  return $ BuiltinApp Info.empty op args
+
+atoms ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+atoms varsNum vars = do
+  es <- P.some (atom varsNum vars)
+  return $ mkApp (List.head es) (List.tail es)
+
+atom ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+atom varsNum vars =
+  exprNamed varsNum vars
+    <|> exprConstInt
+    <|> exprConstString
+    <|> exprLambda varsNum vars
+    <|> exprLet varsNum vars
+    <|> exprCase varsNum vars
+    <|> exprIf varsNum vars
+    <|> parens (expr varsNum vars)
+    <|> braces (expr varsNum vars)
+
+exprNamed ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprNamed varsNum vars = do
+  off <- P.getOffset
+  (txt, i) <- identifierL
+  case HashMap.lookup txt vars of
+    Just k -> do
+      name <- lift $ freshName KNameLocal txt i
+      return $ Var (Info.singleton (NameInfo name)) (varsNum - k - 1)
+    Nothing -> do
+      r <- lift (getIdent txt)
+      case r of
+        Just (Left sym) -> do
+          name <- lift $ freshName KNameFunction txt i
+          return $ Ident (Info.singleton (NameInfo name)) sym
+        Just (Right tag) -> do
+          name <- lift $ freshName KNameConstructor txt i
+          return $ Constr (Info.singleton (NameInfo name)) tag []
+        Nothing ->
+          parseFailure off ("undeclared identifier: " ++ fromText txt)
+
+exprConstInt ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r Node
+exprConstInt = P.try $ do
+  (n, i) <- integer
+  return $ Constant (Info.singleton (LocationInfo i)) (ConstInteger n)
+
+exprConstString ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r Node
+exprConstString = P.try $ do
+  (s, i) <- string
+  return $ Constant (Info.singleton (LocationInfo i)) (ConstString s)
+
+parseLocalName ::
+  forall r.
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  ParsecS r Name
+parseLocalName = parseWildcardName <|> parseIdentName
+  where
+    parseWildcardName :: ParsecS r Name
+    parseWildcardName = do
+      ((), i) <- interval kwWildcard
+      lift $ freshName KNameLocal "_" i
+
+    parseIdentName :: ParsecS r Name
+    parseIdentName = do
+      (txt, i) <- identifierL
+      lift $ freshName KNameLocal txt i
+
+exprLambda ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprLambda varsNum vars = do
+  kwLambda
+  name <- parseLocalName
+  let vars' = HashMap.insert (name ^. nameText) varsNum vars
+  body <- expr (varsNum + 1) vars'
+  return $ Lambda (Info.singleton (BinderInfo name starType)) body
+
+exprLet ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprLet varsNum vars = do
+  kwLet
+  name <- parseLocalName
+  kwAssignment
+  value <- expr varsNum vars
+  kwIn
+  let vars' = HashMap.insert (name ^. nameText) varsNum vars
+  body <- expr (varsNum + 1) vars'
+  return $ Let (Info.singleton (BinderInfo name starType)) value body
+
+exprCase ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprCase varsNum vars = do
+  off <- P.getOffset
+  kwCase
+  value <- expr varsNum vars
+  kwOf
+  braces (exprCase' off value varsNum vars)
+    <|> exprCase' off value varsNum vars
+
+exprCase' ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Int ->
+  Node ->
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprCase' off value varsNum vars = do
+  bs <- P.sepEndBy (caseBranch varsNum vars) kwSemicolon
+  let bs' = map fromLeft' $ filter isLeft bs
+  let bss = map fst bs'
+  let bsns = map snd bs'
+  let def' = map fromRight' $ filter isRight bs
+  let bi = CaseBinderInfo $ map (map (`BinderInfo` starType)) bsns
+  bri <-
+    CaseBranchInfo
+      <$> mapM
+        ( \(CaseBranch tag _ _) -> do
+            ci <- lift $ getConstructorInfo tag
+            return $ BranchInfo (ci ^. constructorName)
+        )
+        bss
+  let info = Info.insert bri (Info.singleton bi)
+  case def' of
+    [def] ->
+      return $ Case info value bss (Just def)
+    [] ->
+      return $ Case info value bss Nothing
+    _ ->
+      parseFailure off "multiple default branches"
+
+caseBranch ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r (Either (CaseBranch, [Name]) Node)
+caseBranch varsNum vars =
+  (defaultBranch varsNum vars <&> Right)
+    <|> (matchingBranch varsNum vars <&> Left)
+
+defaultBranch ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+defaultBranch varsNum vars = do
+  kwWildcard
+  kwMapsTo
+  expr varsNum vars
+
+matchingBranch ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r (CaseBranch, [Name])
+matchingBranch varsNum vars = do
+  off <- P.getOffset
+  txt <- identifier
+  r <- lift (getIdent txt)
+  case r of
+    Just (Left {}) ->
+      parseFailure off ("not a constructor: " ++ fromText txt)
+    Just (Right tag) -> do
+      ns <- P.many parseLocalName
+      let bindersNum = length ns
+      ci <- lift $ getConstructorInfo tag
+      when
+        (ci ^. constructorArgsNum /= bindersNum)
+        (parseFailure off "wrong number of constructor arguments")
+      kwMapsTo
+      let vars' =
+            fst $
+              foldl'
+                ( \(vs, k) name ->
+                    (HashMap.insert (name ^. nameText) k vs, k + 1)
+                )
+                (vars, varsNum)
+                ns
+      br <- expr (varsNum + bindersNum) vars'
+      return (CaseBranch tag bindersNum br, ns)
+    Nothing ->
+      parseFailure off ("undeclared identifier: " ++ fromText txt)
+
+exprIf ::
+  Members '[Reader ParserParams, InfoTableBuilder, NameIdGen] r =>
+  Index ->
+  HashMap Text Index ->
+  ParsecS r Node
+exprIf varsNum vars = do
+  kwIf
+  value <- expr varsNum vars
+  kwThen
+  br1 <- expr varsNum vars
+  kwElse
+  br2 <- expr varsNum vars
+  return $ mkIf Info.empty value br1 br2

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

@@ -0,0 +1,196 @@
+module Juvix.Compiler.Core.Translation.FromSource.Lexer
+  ( module Juvix.Compiler.Core.Translation.FromSource.Lexer,
+    module Juvix.Parser.Lexer,
+  )
+where
+
+import Juvix.Extra.Strings qualified as Str
+import Juvix.Parser.Lexer
+import Juvix.Prelude
+import Text.Megaparsec as P hiding (sepBy1, sepEndBy1, some)
+import Text.Megaparsec.Char.Lexer qualified as L
+
+space :: ParsecS r ()
+space = space' False void
+
+lexeme :: ParsecS r a -> ParsecS r a
+lexeme = L.lexeme space
+
+lexemeInterval :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (a, Interval)
+lexemeInterval = lexeme . interval
+
+symbol :: Text -> ParsecS r ()
+symbol = void . L.symbol space
+
+decimal :: (Member (Reader ParserParams) r, Num n) => ParsecS r (n, Interval)
+decimal = lexemeInterval L.decimal
+
+integer :: Member (Reader ParserParams) r => ParsecS r (Integer, Interval)
+integer = integer' decimal
+
+number :: Member (Reader ParserParams) r => Int -> Int -> ParsecS r (Int, Interval)
+number = number' integer
+
+string :: Member (Reader ParserParams) r => ParsecS r (Text, Interval)
+string = lexemeInterval string'
+
+keyword :: Text -> ParsecS r ()
+keyword = keyword' space
+
+rawKeyword :: Text -> ParsecS r ()
+rawKeyword = rawKeyword' space
+
+identifier :: ParsecS r Text
+identifier = lexeme bareIdentifier
+
+identifierL :: Member (Reader ParserParams) r => ParsecS r (Text, Interval)
+identifierL = lexemeInterval bareIdentifier
+
+-- | Same as @identifier@ but does not consume space after it.
+bareIdentifier :: ParsecS r Text
+bareIdentifier = rawIdentifier allKeywords
+
+allKeywords :: [ParsecS r ()]
+allKeywords =
+  [ kwAssignment,
+    kwColon,
+    kwLambda,
+    kwLet,
+    kwIn,
+    kwConstr,
+    kwCase,
+    kwOf,
+    kwIf,
+    kwThen,
+    kwElse,
+    kwDef,
+    kwMapsTo,
+    kwRightArrow,
+    kwSemicolon,
+    kwWildcard,
+    kwPlus,
+    kwMinus,
+    kwMul,
+    kwDiv,
+    kwMod,
+    kwEq,
+    kwLt,
+    kwLe,
+    kwGt,
+    kwGe,
+    kwBind,
+    kwSeq,
+    kwTrace,
+    kwFail
+  ]
+
+lbrace :: ParsecS r ()
+lbrace = symbol "{"
+
+rbrace :: ParsecS r ()
+rbrace = symbol "}"
+
+lparen :: ParsecS r ()
+lparen = symbol "("
+
+rparen :: ParsecS r ()
+rparen = symbol ")"
+
+parens :: ParsecS r a -> ParsecS r a
+parens = between lparen rparen
+
+braces :: ParsecS r a -> ParsecS r a
+braces = between (symbol "{") (symbol "}")
+
+kwAssignment :: ParsecS r ()
+kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii
+
+kwColon :: ParsecS r ()
+kwColon = keyword Str.colon
+
+kwInductive :: ParsecS r ()
+kwInductive = keyword Str.inductive
+
+kwLambda :: ParsecS r ()
+kwLambda = rawKeyword Str.lambdaUnicode <|> rawKeyword Str.lambdaAscii
+
+kwLet :: ParsecS r ()
+kwLet = keyword Str.let_
+
+kwIn :: ParsecS r ()
+kwIn = keyword Str.in_
+
+kwConstr :: ParsecS r ()
+kwConstr = keyword Str.constr
+
+kwCase :: ParsecS r ()
+kwCase = keyword Str.case_
+
+kwOf :: ParsecS r ()
+kwOf = keyword Str.of_
+
+kwIf :: ParsecS r ()
+kwIf = keyword Str.if_
+
+kwThen :: ParsecS r ()
+kwThen = keyword Str.then_
+
+kwElse :: ParsecS r ()
+kwElse = keyword Str.else_
+
+kwDef :: ParsecS r ()
+kwDef = keyword Str.def
+
+kwMapsTo :: ParsecS r ()
+kwMapsTo = keyword Str.mapstoUnicode <|> keyword Str.mapstoAscii
+
+kwRightArrow :: ParsecS r ()
+kwRightArrow = keyword Str.toUnicode <|> keyword Str.toAscii
+
+kwSemicolon :: ParsecS r ()
+kwSemicolon = keyword Str.semicolon
+
+kwWildcard :: ParsecS r ()
+kwWildcard = keyword Str.underscore
+
+kwPlus :: ParsecS r ()
+kwPlus = keyword Str.plus
+
+kwMinus :: ParsecS r ()
+kwMinus = keyword Str.minus
+
+kwMul :: ParsecS r ()
+kwMul = keyword Str.mul
+
+kwDiv :: ParsecS r ()
+kwDiv = keyword Str.div
+
+kwMod :: ParsecS r ()
+kwMod = keyword Str.mod
+
+kwEq :: ParsecS r ()
+kwEq = keyword Str.equal
+
+kwLt :: ParsecS r ()
+kwLt = keyword Str.less
+
+kwLe :: ParsecS r ()
+kwLe = keyword Str.lessEqual
+
+kwGt :: ParsecS r ()
+kwGt = keyword Str.greater
+
+kwGe :: ParsecS r ()
+kwGe = keyword Str.greaterEqual
+
+kwBind :: ParsecS r ()
+kwBind = keyword Str.bind
+
+kwSeq :: ParsecS r ()
+kwSeq = keyword Str.seq_
+
+kwTrace :: ParsecS r ()
+kwTrace = keyword Str.trace_
+
+kwFail :: ParsecS r ()
+kwFail = keyword Str.fail_

src/Juvix/Extra/Strings.hs

@@ -41,6 +41,9 @@ function = "function"
 constructor :: IsString s => s
 constructor = "constructor"
 
+constr :: IsString s => s
+constr = "constr"
+
 topModule :: IsString s => s
 topModule = "top module"
 
@@ -128,9 +131,39 @@ pipe = "|"
 equal :: IsString s => s
 equal = "="
 
+less :: IsString s => s
+less = "<"
+
+lessEqual :: IsString s => s
+lessEqual = "<="
+
+greater :: IsString s => s
+greater = ">"
+
+greaterEqual :: IsString s => s
+greaterEqual = ">="
+
+bind :: IsString s => s
+bind = ">>="
+
+seq_ :: IsString s => s
+seq_ = ">>"
+
+trace_ :: IsString s => s
+trace_ = "trace"
+
+fail_ :: IsString s => s
+fail_ = "fail"
+
 data_ :: IsString s => s
 data_ = "data"
 
+deBruijnVar :: IsString s => s
+deBruijnVar = "$"
+
+exclamation :: IsString s => s
+exclamation = "!"
+
 lambdaUnicode :: IsString s => s
 lambdaUnicode = "λ"
 
@@ -227,6 +260,9 @@ sizeof = "sizeof"
 true_ :: IsString s => s
 true_ = "true"
 
+false_ :: IsString s => s
+false_ = "false"
+
 tag :: IsString s => s
 tag = "tag"
 
@@ -242,6 +278,60 @@ putStrLn_ = "putStrLn"
 debug_ :: IsString s => s
 debug_ = "debug"
 
+plus :: IsString s => s
+plus = "+"
+
+minus :: IsString s => s
+minus = "-"
+
+mul :: IsString s => s
+mul = "*"
+
+div :: IsString s => s
+div = "/"
+
+mod :: IsString s => s
+mod = "%"
+
+if_ :: IsString s => s
+if_ = "if"
+
+then_ :: IsString s => s
+then_ = "then"
+
+else_ :: IsString s => s
+else_ = "else"
+
+pi_ :: IsString s => s
+pi_ = "pi"
+
+def :: IsString s => s
+def = "def"
+
+zero :: IsString s => s
+zero = "0"
+
+succ :: IsString s => s
+succ = "S"
+
+unit :: IsString s => s
+unit = "unit"
+
+nil :: IsString s => s
+nil = "nil"
+
+cons :: IsString s => s
+cons = "cons"
+
+pair :: IsString s => s
+pair = "pair"
+
+case_ :: IsString s => s
+case_ = "case"
+
+of_ :: IsString s => s
+of_ = "of"
+
 juvixFunctionT :: IsString s => s
 juvixFunctionT = "juvix_function_t"
 

src/Juvix/Parser/Error.hs

@@ -1,9 +1,9 @@
-module Juvix.Compiler.Concrete.Translation.FromSource.Error where
+module Juvix.Parser.Error where
 
-import Juvix.Compiler.Concrete.Extra (errorOffset)
 import Juvix.Prelude
 import Juvix.Prelude.Pretty
 import Text.Megaparsec qualified as M
+import Text.Megaparsec.Error (errorOffset)
 
 newtype ParserError = ParserError
   { _parseError :: M.ParseErrorBundle Text Void

src/Juvix/Parser/Lexer.hs

@@ -0,0 +1,121 @@
+module Juvix.Parser.Lexer where
+
+{-
+
+This module contains lexing functions common to all parsers in the pipeline
+(Juvix, JuvixCore, JuvixAsm).
+
+-}
+
+import Control.Monad.Trans.Class (lift)
+import Data.Set qualified as Set
+import Data.Text qualified as Text
+import GHC.Unicode
+import Juvix.Extra.Strings qualified as Str
+import Juvix.Prelude
+import Text.Megaparsec as P hiding (sepBy1, sepEndBy1, some)
+import Text.Megaparsec.Char hiding (space)
+import Text.Megaparsec.Char.Lexer qualified as L
+
+type ParsecS r = ParsecT Void Text (Sem r)
+
+newtype ParserParams = ParserParams
+  { _parserParamsRoot :: FilePath
+  }
+
+makeLenses ''ParserParams
+
+parseFailure :: Int -> String -> ParsecS r a
+parseFailure off str = P.parseError $ P.FancyError off (Set.singleton (P.ErrorFail str))
+
+space' :: forall r. Bool -> (forall a. ParsecS r a -> ParsecS r ()) -> ParsecS r ()
+space' judoc comment_ = L.space space1 lineComment block
+  where
+    lineComment :: ParsecS r ()
+    lineComment = comment_ $ do
+      when
+        judoc
+        (notFollowedBy (P.chunk Str.judocStart))
+      void (P.chunk "--")
+      void (P.takeWhileP Nothing (/= '\n'))
+
+    block :: ParsecS r ()
+    block = comment_ (L.skipBlockComment "{-" "-}")
+
+integer' :: ParsecS r (Integer, Interval) -> ParsecS r (Integer, Interval)
+integer' dec = do
+  minus <- optional (char '-')
+  (nat, i) <- dec
+  let nat' = case minus of
+        Nothing -> nat
+        _ -> (-nat)
+  return (nat', i)
+
+number' :: ParsecS r (Integer, Interval) -> Int -> Int -> ParsecS r (Int, Interval)
+number' int mn mx = do
+  off <- getOffset
+  (n, i) <- int
+  when
+    (n < fromIntegral mn || n > fromIntegral mx)
+    (parseFailure off ("number out of bounds: " ++ show n))
+  return (fromInteger n, i)
+
+string' :: ParsecS r Text
+string' = pack <$> (char '"' >> manyTill L.charLiteral (char '"'))
+
+keyword' :: ParsecS r () -> Text -> ParsecS r ()
+keyword' spc kw = do
+  P.try $ do
+    P.chunk kw
+    notFollowedBy (satisfy validTailChar)
+    spc
+
+keywordL' :: Member (Reader ParserParams) r => ParsecS r () -> Text -> ParsecS r Interval
+keywordL' spc kw = do
+  P.try $ do
+    i <- snd <$> interval (P.chunk kw)
+    notFollowedBy (satisfy validTailChar)
+    spc
+    return i
+
+rawKeyword' :: ParsecS r () -> Text -> ParsecS r ()
+rawKeyword' spc kw = do
+  P.try $ do
+    void (P.chunk kw)
+    spc
+
+rawIdentifier :: [ParsecS r ()] -> ParsecS r Text
+rawIdentifier allKeywords = do
+  notFollowedBy (choice allKeywords)
+  h <- P.satisfy validFirstChar
+  t <- P.takeWhileP Nothing validTailChar
+  return (Text.cons h t)
+
+validTailChar :: Char -> Bool
+validTailChar c =
+  isAlphaNum c || validFirstChar c
+
+reservedSymbols :: [Char]
+reservedSymbols = "\";(){}[].≔λ\\"
+
+validFirstChar :: Char -> Bool
+validFirstChar c = not $ isNumber c || isSpace c || (c `elem` reservedSymbols)
+
+curLoc :: Member (Reader ParserParams) r => ParsecS r Loc
+curLoc = do
+  sp <- getSourcePos
+  offset <- getOffset
+  root <- lift (asks (^. parserParamsRoot))
+  return (mkLoc root offset sp)
+
+interval :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (a, Interval)
+interval ma = do
+  start <- curLoc
+  res <- ma
+  end <- curLoc
+  return (res, mkInterval start end)
+
+withLoc :: Member (Reader ParserParams) r => ParsecS r a -> ParsecS r (WithLoc a)
+withLoc ma = do
+  (a, i) <- interval ma
+  return (WithLoc i a)

src/Juvix/Prelude/Base.hs

@@ -218,6 +218,14 @@ tableNestedInsert ::
   HashMap k1 (HashMap k2 a)
 tableNestedInsert k1 k2 = tableInsert (HashMap.singleton k2) (HashMap.insert k2) k1
 
+--------------------------------------------------------------------------------
+-- List
+--------------------------------------------------------------------------------
+
+revAppend :: [a] -> [a] -> [a]
+revAppend [] ys = ys
+revAppend (x : xs) ys = revAppend xs (x : ys)
+
 --------------------------------------------------------------------------------
 -- NonEmpty
 --------------------------------------------------------------------------------

test/Core.hs

@@ -0,0 +1,8 @@
+module Core where
+
+import Base
+import Core.Negative qualified as N
+import Core.Positive qualified as P
+
+allTests :: TestTree
+allTests = testGroup "JuvixCore tests" [P.allTests, N.allTests]

test/Core/Base.hs

@@ -0,0 +1,82 @@
+module Core.Base where
+
+import Base
+import Data.Text.IO qualified as TIO
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Error
+import Juvix.Compiler.Core.Evaluator
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NoDisplayInfo
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Pretty
+import Juvix.Compiler.Core.Translation.FromSource
+import System.IO.Extra (withTempDir)
+import Text.Megaparsec.Pos qualified as M
+
+coreEvalAssertion :: FilePath -> FilePath -> (String -> IO ()) -> Assertion
+coreEvalAssertion mainFile expectedFile step = do
+  step "Parse"
+  r <- parseFile mainFile
+  case r of
+    Left err -> assertFailure (show (pretty err))
+    Right (_, Nothing) -> do
+      step "Compare expected and actual program output"
+      expected <- TIO.readFile expectedFile
+      assertEqDiff ("Check: EVAL output = " <> expectedFile) "" expected
+    Right (tab, Just node) -> do
+      withTempDir
+        ( \dirPath -> do
+            let outputFile = dirPath </> "out.out"
+            hout <- openFile outputFile WriteMode
+            step "Evaluate"
+            r' <- doEval mainFile hout tab node
+            case r' of
+              Left err -> do
+                hClose hout
+                assertFailure (show (pretty err))
+              Right value -> do
+                unless
+                  (Info.member kNoDisplayInfo (getInfo value))
+                  (hPutStrLn hout (ppPrint value))
+                hClose hout
+                actualOutput <- TIO.readFile outputFile
+                step "Compare expected and actual program output"
+                expected <- TIO.readFile expectedFile
+                assertEqDiff ("Check: EVAL output = " <> expectedFile) actualOutput expected
+        )
+
+coreEvalErrorAssertion :: FilePath -> (String -> IO ()) -> Assertion
+coreEvalErrorAssertion mainFile step = do
+  step "Parse"
+  r <- parseFile mainFile
+  case r of
+    Left _ -> assertBool "" True
+    Right (_, Nothing) -> assertFailure "no error"
+    Right (tab, Just node) -> do
+      withTempDir
+        ( \dirPath -> do
+            let outputFile = dirPath </> "out.out"
+            hout <- openFile outputFile WriteMode
+            step "Evaluate"
+            r' <- doEval mainFile hout tab node
+            case r' of
+              Left _ -> assertBool "" True
+              Right _ -> assertFailure "no error"
+        )
+
+parseFile :: FilePath -> IO (Either ParserError (InfoTable, Maybe Node))
+parseFile f = do
+  s <- readFile f
+  return $ runParser "" f emptyInfoTable s
+
+doEval ::
+  FilePath ->
+  Handle ->
+  InfoTable ->
+  Node ->
+  IO (Either CoreError Node)
+doEval f hout tab node =
+  catchEvalErrorIO defaultLoc (hEvalIO stdin hout (tab ^. identContext) [] node)
+  where
+    defaultLoc = singletonInterval (mkLoc f 0 (M.initialPos f))

test/Core/Negative.hs

@@ -0,0 +1,68 @@
+module Core.Negative where
+
+import Base
+import Core.Base
+
+data NegTest = NegTest
+  { _name :: String,
+    _relDir :: FilePath,
+    _file :: FilePath
+  }
+
+root :: FilePath
+root = "tests/Core/negative"
+
+testDescr :: NegTest -> TestDescr
+testDescr NegTest {..} =
+  let tRoot = root </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ coreEvalErrorAssertion _file
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "JuvixCore negative tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [NegTest]
+tests =
+  [ NegTest
+      "Division by zero"
+      "."
+      "test001.jvc",
+    NegTest
+      "Arithmetic operations on non-numbers"
+      "."
+      "test002.jvc",
+    NegTest
+      "Matching on non-data"
+      "."
+      "test003.jvc",
+    NegTest
+      "If on non-boolean"
+      "."
+      "test004.jvc",
+    NegTest
+      "No matching case branch"
+      "."
+      "test005.jvc",
+    NegTest
+      "Invalid application"
+      "."
+      "test006.jvc",
+    NegTest
+      "Invalid builtin application"
+      "."
+      "test007.jvc",
+    NegTest
+      "Undefined symbol"
+      "."
+      "test008.jvc",
+    NegTest
+      "Erroneous Church numerals"
+      "."
+      "test009.jvc"
+  ]

test/Core/Positive.hs

@@ -0,0 +1,228 @@
+module Core.Positive where
+
+import Base
+import Core.Base
+
+data PosTest = PosTest
+  { _name :: String,
+    _relDir :: FilePath,
+    _file :: FilePath,
+    _expectedFile :: FilePath
+  }
+
+root :: FilePath
+root = "tests/Core/positive"
+
+testDescr :: PosTest -> TestDescr
+testDescr PosTest {..} =
+  let tRoot = root </> _relDir
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ coreEvalAssertion _file _expectedFile
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "JuvixCore positive tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [PosTest]
+tests =
+  [ PosTest
+      "Arithmetic operators"
+      "."
+      "test001.jvc"
+      "out/test001.out",
+    PosTest
+      "Arithmetic operators inside lambdas"
+      "."
+      "test002.jvc"
+      "out/test002.out",
+    PosTest
+      "Empty program with comments"
+      "."
+      "test003.jvc"
+      "out/test003.out",
+    PosTest
+      "IO builtins"
+      "."
+      "test004.jvc"
+      "out/test004.out",
+    PosTest
+      "Higher-order functions"
+      "."
+      "test005.jvc"
+      "out/test005.out",
+    PosTest
+      "If-then-else"
+      "."
+      "test006.jvc"
+      "out/test006.out",
+    PosTest
+      "Case"
+      "."
+      "test007.jvc"
+      "out/test007.out",
+    PosTest
+      "Recursion"
+      "."
+      "test008.jvc"
+      "out/test008.out",
+    PosTest
+      "Tail recursion"
+      "."
+      "test009.jvc"
+      "out/test009.out",
+    PosTest
+      "Let"
+      "."
+      "test010.jvc"
+      "out/test010.out",
+    PosTest
+      "Tail recursion: Fibonacci numbers in linear time"
+      "."
+      "test011.jvc"
+      "out/test011.out",
+    PosTest
+      "Trees"
+      "."
+      "test012.jvc"
+      "out/test012.out",
+    PosTest
+      "Functions returning functions with variable capture"
+      "."
+      "test013.jvc"
+      "out/test013.out",
+    PosTest
+      "Arithmetic"
+      "."
+      "test014.jvc"
+      "out/test014.out",
+    PosTest
+      "Local functions with free variables"
+      "."
+      "test015.jvc"
+      "out/test015.out",
+    PosTest
+      "Recursion through higher-order functions"
+      "."
+      "test016.jvc"
+      "out/test016.out",
+    PosTest
+      "Tail recursion through higher-order functions"
+      "."
+      "test017.jvc"
+      "out/test017.out",
+    PosTest
+      "Higher-order functions and recursion"
+      "."
+      "test018.jvc"
+      "out/test018.out",
+    PosTest
+      "Self-application"
+      "."
+      "test019.jvc"
+      "out/test019.out",
+    PosTest
+      "Recursive functions: McCarthy's 91 function, subtraction by increments"
+      "."
+      "test020.jvc"
+      "out/test020.out",
+    PosTest
+      "Higher-order recursive functions"
+      "."
+      "test021.jvc"
+      "out/test021.out",
+    PosTest
+      "Fast exponentiation"
+      "."
+      "test022.jvc"
+      "out/test022.out",
+    PosTest
+      "Lists"
+      "."
+      "test023.jvc"
+      "out/test023.out",
+    PosTest
+      "Structural equality"
+      "."
+      "test024.jvc"
+      "out/test024.out",
+    PosTest
+      "Mutual recursion"
+      "."
+      "test025.jvc"
+      "out/test025.out",
+    PosTest
+      "Nested 'case', 'let' and 'if' with variable capture"
+      "."
+      "test026.jvc"
+      "out/test026.out",
+    PosTest
+      "Euclid's algorithm"
+      "."
+      "test027.jvc"
+      "out/test027.out",
+    PosTest
+      "Functional queues"
+      "."
+      "test028.jvc"
+      "out/test028.out",
+    PosTest
+      "Church numerals"
+      "."
+      "test029.jvc"
+      "out/test029.out",
+    PosTest
+      "Streams without memoization"
+      "."
+      "test030.jvc"
+      "out/test030.out",
+    PosTest
+      "Ackermann function"
+      "."
+      "test031.jvc"
+      "out/test031.out",
+    PosTest
+      "Ackermann function (higher-order definition)"
+      "."
+      "test032.jvc"
+      "out/test032.out",
+    PosTest
+      "Nested lists"
+      "."
+      "test033.jvc"
+      "out/test033.out",
+    {-    PosTest
+          "Evaluation order"
+          "."
+          "test034.jvc"
+          "out/test034.out", -}
+    PosTest
+      "Merge sort"
+      "."
+      "test035.jvc"
+      "out/test035.out",
+    PosTest
+      "Big numbers"
+      "."
+      "test036.jvc"
+      "out/test036.out",
+    PosTest
+      "Global variables"
+      "."
+      "test037.jvc"
+      "out/test037.out",
+    PosTest
+      "Global variables and forward declarations"
+      "."
+      "test038.jvc"
+      "out/test038.out",
+    PosTest
+      "Eta-expansion of builtins and constructors"
+      "."
+      "test039.jvc"
+      "out/test039.out"
+  ]

test/Main.hs

@@ -3,6 +3,7 @@ module Main (main) where
 import Arity qualified
 import BackendC qualified
 import Base
+import Core qualified
 import MonoJuvix qualified
 import Reachability qualified
 import Scope qualified
@@ -13,7 +14,9 @@ slowTests :: TestTree
 slowTests =
   testGroup
     "Juvix slow tests"
-    [BackendC.allTests]
+    [ BackendC.allTests,
+      Core.allTests
+    ]
 
 fastTests :: TestTree
 fastTests =

tests/Core/benchmark/out/test001.out

@@ -0,0 +1,6 @@
+50005000
+5000050000
+500000500000
+50000005000000
+5000000050000000
+500000000500000000

tests/Core/benchmark/out/test003.out

@@ -0,0 +1,5 @@
+50005000
+5000050000
+500000500000
+50000005000000
+5000000050000000

tests/Core/benchmark/out/test004.out

@@ -0,0 +1,4 @@
+541
+7919
+104729
+224737

tests/Core/benchmark/test001.jvc

@@ -0,0 +1,13 @@
+-- tail recursion
+
+def sum' := \x \acc if x = 0 then acc else sum' (x - 1) (x + acc);
+def sum := \x sum' x 0;
+
+def writeLn := \x write x >> write "\n";
+
+writeLn (sum 10000) >>
+writeLn (sum 100000) >>
+writeLn (sum 1000000) >>
+writeLn (sum 10000000) >>
+writeLn (sum 100000000) >>
+writeLn (sum 1000000000)

tests/Core/benchmark/test002.jvc

@@ -0,0 +1,13 @@
+-- tail recursion: compute n-th Fibonacci number in O(n)
+
+def fib' := \n \x \y if n = 0 then x else fib' (n - 1) y (x + y);
+def fib := \n fib' n 0 1;
+
+def writeLn := \x write x >> write "\n";
+
+writeLn (fib 10) >>
+writeLn (fib 100) >>
+writeLn (fib 1000) >>
+writeLn (fib 10000) >>
+writeLn (fib 100000) >>
+writeLn (fib 1000000)

tests/Core/benchmark/test003.jvc

@@ -0,0 +1,13 @@
+-- tail recursion through higher-order functions
+
+def sumb := \f \x \acc if x = 0 then acc else f (x - 1) acc;
+def sum' := \x \acc sumb sum' x (x + acc);
+def sum := \x sum' x 0;
+
+def writeLn := \x write x >> write "\n";
+
+writeLn (sum 10000) >>
+writeLn (sum 100000) >>
+writeLn (sum 1000000) >>
+writeLn (sum 10000000) >>
+writeLn (sum 100000000)

tests/Core/benchmark/test004.jvc

@@ -0,0 +1,37 @@
+-- streams without memoization
+
+constr nil 0;
+constr cons 2;
+
+def force := \f f nil;
+
+def filter := \p \s \_
+  case force s of {
+    cons h t ->
+      if p h then
+        cons h (filter p t)
+      else
+        force (filter p t)
+  };
+
+def nth := \n \s
+  case force s of {
+    cons h t -> if n = 1 then h else nth (n - 1) t
+  };
+
+def numbers := \n \_ cons n (numbers (n + 1));
+
+def indivisible := \n \x if x % n = 0 then false else true;
+def eratostenes := \s \_
+  case force s of {
+    cons n t ->
+      cons n (eratostenes (filter (indivisible n) t))
+  };
+def primes := eratostenes (numbers 2);
+
+def writeLn := \x write x >> write "\n";
+
+writeLn (nth 100 primes) >>
+writeLn (nth 1000 primes) >>
+writeLn (nth 10000 primes) >>
+writeLn (nth 20000 primes)

tests/Core/negative/test001.jvc

@@ -0,0 +1,5 @@
+-- division by zero
+
+def f := \x 2 / x;
+
+f 0

tests/Core/negative/test002.jvc

@@ -0,0 +1,5 @@
+-- arithmetic operations on non-numbers
+
+def y := 3 + \x x;
+
+y

tests/Core/negative/test003.jvc

@@ -0,0 +1,3 @@
+-- matching on non-data
+
+case \x x of nil -> nil

tests/Core/negative/test004.jvc

@@ -0,0 +1,3 @@
+-- if on non-boolean
+
+if 2 then 1 else 0

tests/Core/negative/test005.jvc

@@ -0,0 +1,7 @@
+-- no matching case branch
+
+constr cons 2;
+
+case cons 1 2 of {
+  nil -> true
+}

tests/Core/negative/test006.jvc

@@ -0,0 +1,3 @@
+-- invalid application
+
+(if true then 1 else 2) 3

tests/Core/negative/test007.jvc

@@ -0,0 +1,3 @@
+-- invalid builtin application
+
+(+ 2 3 4)

tests/Core/negative/test008.jvc

@@ -0,0 +1,5 @@
+-- undefined symbol
+
+def f;
+
+f

tests/Core/negative/test009.jvc

@@ -0,0 +1,34 @@
+-- erroneous Church numerals
+
+constr pair 2;
+
+def fst := \p case p of { pair x _ -> x };
+def snd := \p case p of { pair _ x -> x };
+
+def compose := \f \g \x f (g x);
+
+def zero := \f \x x;
+
+def num := \n
+  if n = 0 then
+    zero
+  else
+    \f compose f (num (n - 1) f);
+
+def succ := \n \f compose f n; -- wrong
+
+def isZero := \n n (\_ false) true;
+
+def pred := \n
+  fst (
+    n (\x
+        if isZero (snd x) then
+          pair (fst x) (succ (snd x))
+        else
+          pair (succ (fst x)) (succ (snd x)))
+      (pair zero zero)
+  );
+
+def toInt := \n n (+ 1) 0;
+
+toInt (pred (num 7))

tests/Core/positive/out/test001.out

@@ -0,0 +1 @@
+11

tests/Core/positive/out/test002.out

@@ -0,0 +1 @@
+11

tests/Core/positive/out/test004.out

@@ -0,0 +1,2 @@
+12345
+12345

tests/Core/positive/out/test005.out

@@ -0,0 +1 @@
+6

tests/Core/positive/out/test006.out

@@ -0,0 +1 @@
+2

tests/Core/positive/out/test007.out

@@ -0,0 +1,7 @@
+false
+true
+0
+cons 1 nil
+1
+cons 1 (cons 2 nil)
+cons 1 (cons 2 nil)

tests/Core/positive/out/test008.out

@@ -0,0 +1 @@
+50005000

tests/Core/positive/out/test009.out

@@ -0,0 +1,5 @@
+50005000
+5000050000
+120
+3628800
+93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000

tests/Core/positive/out/test010.out

@@ -0,0 +1 @@
+40

tests/Core/positive/out/test011.out

@@ -0,0 +1,3 @@
+55
+354224848179261915075
+43466557686937456435688527675040625802564660517371780402481729089536555417949051890403879840079255169295922593080322634775209689623239873322471161642996440906533187938298969649928516003704476137795166849228875

tests/Core/positive/out/test012.out

@@ -0,0 +1,5 @@
+13200200200
+21320020020013200200200
+3213200200200132002002002132002002001320020020021320020020013200200200
+13213200200200132002002002132002002001320020020021320020020013200200200
+21321320020020013200200200213200200200132002002002132002002001320020020013213200200200132002002002132002002001320020020021320020020013200200200

tests/Core/positive/out/test013.out

@@ -0,0 +1,4 @@
+1
+0
+2
+5

tests/Core/positive/out/test014.out

@@ -0,0 +1,4 @@
+7
+17
+37
+-29

tests/Core/positive/out/test015.out

@@ -0,0 +1,6 @@
+600
+25
+30
+45
+55
+16

tests/Core/positive/out/test016.out

@@ -0,0 +1 @@
+55

tests/Core/positive/out/test017.out

@@ -0,0 +1,2 @@
+50005000
+5000050000

tests/Core/positive/out/test018.out

@@ -0,0 +1 @@
+11

tests/Core/positive/out/test019.out

@@ -0,0 +1 @@
+7

tests/Core/positive/out/test020.out

@@ -0,0 +1,9 @@
+91
+91
+91
+91
+100
+6
+6
+400
+4000

tests/Core/positive/out/test021.out

@@ -0,0 +1,24 @@
+6
+4
+7
+9
+40
+6
+3
+7
+9
+30
+6
+2
+7
+9
+20
+6
+1
+7
+9
+10
+6
+0
+7
+end

tests/Core/positive/out/test022.out

@@ -0,0 +1,3 @@
+8
+2187
+476837158203125

tests/Core/positive/out/test023.out

@@ -0,0 +1,10 @@
+cons 10 (cons 9 (cons 8 (cons 7 (cons 6 (cons 5 (cons 4 (cons 3 (cons 2 (cons 1 nil)))))))))
+cons 1 (cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 (cons 10 nil)))))))))
+cons 10 (cons 9 (cons 8 (cons 7 (cons 6 nil))))
+cons 0 (cons 1 (cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 nil)))))))))
+50005000
+5000050000
+50005000
+5000050000
+50005000
+5000050000

tests/Core/positive/out/test024.out

@@ -0,0 +1,8 @@
+true
+false
+true
+false
+false
+true
+false
+true

tests/Core/positive/out/test025.out

@@ -0,0 +1,2 @@
+120
+3628800

tests/Core/positive/out/test026.out

@@ -0,0 +1,6 @@
+-12096
+-1448007509520
+5510602057585725
+-85667472308246220
+527851146861989286336
+-441596546382859135501706333021475

tests/Core/positive/out/test027.out

@@ -0,0 +1,5 @@
+14
+70
+1
+1
+1

tests/Core/positive/out/test028.out

@@ -0,0 +1 @@
+cons 1 (cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 (cons 10 (cons 11 (cons 12 (cons 13 (cons 14 (cons 15 (cons 16 (cons 17 (cons 18 (cons 19 (cons 20 (cons 21 (cons 22 (cons 23 (cons 24 (cons 25 (cons 26 (cons 27 (cons 28 (cons 29 (cons 30 (cons 31 (cons 32 (cons 33 (cons 34 (cons 35 (cons 36 (cons 37 (cons 38 (cons 39 (cons 40 (cons 41 (cons 42 (cons 43 (cons 44 (cons 45 (cons 46 (cons 47 (cons 48 (cons 49 (cons 50 (cons 51 (cons 52 (cons 53 (cons 54 (cons 55 (cons 56 (cons 57 (cons 58 (cons 59 (cons 60 (cons 61 (cons 62 (cons 63 (cons 64 (cons 65 (cons 66 (cons 67 (cons 68 (cons 69 (cons 70 (cons 71 (cons 72 (cons 73 (cons 74 (cons 75 (cons 76 (cons 77 (cons 78 (cons 79 (cons 80 (cons 81 (cons 82 (cons 83 (cons 84 (cons 85 (cons 86 (cons 87 (cons 88 (cons 89 (cons 90 (cons 91 (cons 92 (cons 93 (cons 94 (cons 95 (cons 96 (cons 97 (cons 98 (cons 99 (cons 100 nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

tests/Core/positive/out/test029.out

@@ -0,0 +1,7 @@
+7
+21
+6
+5
+8
+13
+21

tests/Core/positive/out/test030.out

@@ -0,0 +1,3 @@
+cons 2 (cons 3 (cons 5 (cons 7 (cons 11 (cons 13 (cons 17 (cons 19 (cons 23 (cons 29 nil)))))))))
+547
+1229

tests/Core/positive/out/test031.out

@@ -0,0 +1,6 @@
+8
+9
+15
+17
+29
+1021

tests/Core/positive/out/test032.out

@@ -0,0 +1,4 @@
+10
+21
+2187
+1021

tests/Core/positive/out/test033.out

@@ -0,0 +1,2 @@
+cons (cons 4 (cons 3 (cons 2 (cons 1 nil)))) (cons (cons 3 (cons 2 (cons 1 nil))) (cons (cons 2 (cons 1 nil)) (cons (cons 1 nil) nil)))
+cons 4 (cons 3 (cons 2 (cons 1 (cons 3 (cons 2 (cons 1 (cons 2 (cons 1 (cons 1 nil)))))))))

tests/Core/positive/out/test034.out

@@ -0,0 +1,20 @@
+1
+2
+3
+6
+1
+0
+1
+0
+1
+0
+1
+0
+1
+0
+9
+7
+2
+8
+3
+6

tests/Core/positive/out/test035.out

@@ -0,0 +1,3 @@
+cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 (cons 10 (cons 11 nil)))))))))
+cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 (cons 10 (cons 11 nil)))))))))
+cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 (cons 10 (cons 11 nil)))))))))

tests/Core/positive/out/test037.out

@@ -0,0 +1 @@
+77