Add REPL option to apply Core transformations (#1796)

Core transformations apply to the whole InfoTable, the REPL needs to
apply Core transformations to the single node that it compiles from the
user input string.

The solution in this commit is to:

1. Compile the input string as before to obtain a Core Node.
2. Add this Node to a copy of the Core InfoTable for the loaded file.
3. Apply the (CLI specified) Core transformations to this InfoTable.
4. Extract the (now transformed) Node from the InfoTable.

We can think of a way to improve this, maybe when we tackle allowing the
user to make new definitions in the REPL.

As soon as compilation of pattern matching is complete we should enable
some (all?) Core transformations by default.

Example:

At the moment we get the following result in the REPL:

```
juvix repl
...
Stdlib.Prelude> 1 + 1
suc (suc zero)
```

After this commit we can turn on `nat-to-int` transformation:

```
juvix repl -t nat-to-int
Stdlib.Prelude> 1 + 1
2
```

* Part of #1531

app/Commands/Repl.hs

@@ -16,6 +16,7 @@ import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Info.NoDisplayInfo qualified as Info
 import Juvix.Compiler.Core.Language qualified as Core
 import Juvix.Compiler.Core.Pretty qualified as Core
+import Juvix.Compiler.Core.Transformation qualified as Core
 import Juvix.Compiler.Core.Translation.FromInternal.Data qualified as Core
 import Juvix.Compiler.Internal.Language qualified as Internal
 import Juvix.Compiler.Internal.Pretty qualified as Internal
@@ -170,14 +171,20 @@ runCommand opts = do
           defaultLoc = singletonInterval (mkInitialLoc replPath)
 
           compileThenEval :: ReplContext -> String -> Repl (Either JuvixError Core.Node)
-          compileThenEval ctx s = bindEither compileString eval
+          compileThenEval ctx s = bindEither (fmap transformNode' <$> compileString) eval
             where
               eval :: Core.Node -> Repl (Either JuvixError Core.Node)
               eval n =
                 liftIO $
                   mapLeft
                     (JuvixError @Core.CoreError)
-                    <$> doEvalIO False defaultLoc (ctx ^. replContextExpContext . contextCoreResult . Core.coreResultTable) n
+                    <$> doEvalIO False defaultLoc infoTable n
+
+              infoTable :: Core.InfoTable
+              infoTable = ctx ^. replContextExpContext . contextCoreResult . Core.coreResultTable
+
+              transformNode' :: Core.Node -> Core.Node
+              transformNode' = transformNode infoTable (opts ^. replTransformations)
 
               compileString :: Repl (Either JuvixError Core.Node)
               compileString = liftIO $ compileExpressionIO' ctx (strip (pack s))

app/Commands/Repl/Options.hs

@@ -2,11 +2,13 @@ module Commands.Repl.Options where
 
 import CommonOptions
 import Juvix.Compiler.Core.Pretty.Options qualified as Core
+import Juvix.Compiler.Core.Transformation
 
 data ReplOptions = ReplOptions
   { _replInputFile :: Maybe (AppPath File),
     _replShowDeBruijn :: Bool,
-    _replNoPrelude :: Bool
+    _replNoPrelude :: Bool,
+    _replTransformations :: [TransformationId]
   }
   deriving stock (Data)
 
@@ -20,6 +22,7 @@ instance CanonicalProjection ReplOptions Core.Options where
 
 parseRepl :: Parser ReplOptions
 parseRepl = do
+  _replTransformations <- optTransformationIds
   _replInputFile <- optional parseInputJuvixFile
   _replShowDeBruijn <-
     switch

src/Juvix/Compiler/Pipeline/ExpressionContext.hs

@@ -1,16 +1,19 @@
 module Juvix.Compiler.Pipeline.ExpressionContext where
 
+import Data.HashMap.Strict
 import Juvix.Compiler.Abstract.Translation qualified as Abstract
 import Juvix.Compiler.Concrete.Data.InfoTable qualified as Scoper
 import Juvix.Compiler.Concrete.Data.Scope qualified as S
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language qualified as C
 import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper
 import Juvix.Compiler.Core qualified as Core
+import Juvix.Compiler.Core.Data.InfoTableBuilder
+import Juvix.Compiler.Core.Language
+import Juvix.Compiler.Core.Transformation
 import Juvix.Compiler.Internal qualified as Internal
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as InternalTyped
-import Juvix.Prelude
 
 data ExpressionContext = ExpressionContext
   { _contextInternalTypedResult :: InternalTyped.InternalTypedResult,
@@ -53,3 +56,12 @@ mainModuleScope e = fromJust (moduleScope e (mainModuleTopPath e))
 
 mainModuleTopPath :: ExpressionContext -> C.TopModulePath
 mainModuleTopPath = (^. contextScoperResult . Scoper.mainModule . C.modulePath . S.nameConcrete)
+
+transformNode :: InfoTable -> [TransformationId] -> Node -> Node
+transformNode tab ts n = snd (run (runInfoTableBuilder tab transformNode'))
+  where
+    transformNode' :: Member InfoTableBuilder r => Sem r Node
+    transformNode' = do
+      sym <- freshSymbol
+      registerIdentNode sym n
+      lookupDefault impossible sym . (^. identContext) . applyTransformations ts <$> getInfoTable

tests/smoke/Commands/repl.smoke.yaml

@@ -243,4 +243,15 @@ tests:
     stderr:
       contains: |
         evaluation error: failure: Enough
-    exit-status: 0
+    exit-status: 0
+
+  - name: repl-nat-to-int-transform
+    command:
+      - juvix
+      - repl
+      - -t nat-to-int
+    stdin: "1 + 2"
+    stdout:
+      contains: |
+        3
+    exit-status: 0