Support compilation to Anoma compatible functions

app/Commands/Compile.hs

@@ -28,6 +28,7 @@ runCommand opts@CompileOptions {..} = do
     TargetAsm -> Compile.runAsmPipeline arg
     TargetReg -> Compile.runRegPipeline arg
     TargetNockma -> Compile.runNockmaPipeline arg
+    TargetAnoma -> Compile.runAnomaPipeline arg
 
 writeCoreFile :: (Members '[EmbedIO, App, TaggedLock] r) => Compile.PipelineArg -> Sem r ()
 writeCoreFile [email protected] {..} = do

app/Commands/Dev/Asm/Compile.hs

@@ -58,6 +58,7 @@ runCommand opts = do
       TargetNative64 -> return Backend.TargetCNative64
       TargetReg -> return Backend.TargetReg
       TargetNockma -> err "Nockma"
+      TargetAnoma -> err "Anoma"
       TargetTree -> err "JuvixTree"
       TargetGeb -> err "GEB"
       TargetVampIR -> err "VampIR"

app/Commands/Dev/Core/Compile.hs

@@ -22,6 +22,7 @@ runCommand opts = do
     TargetReg -> runRegPipeline arg
     TargetTree -> runTreePipeline arg
     TargetNockma -> runNockmaPipeline arg
+    TargetAnoma -> runAnomaPipeline arg
   where
     getFile :: Sem r (Path Abs File)
     getFile = getMainFile (opts ^. compileInputFile)

app/Commands/Dev/Core/Compile/Base.hs

@@ -9,6 +9,7 @@ import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Backend.Geb qualified as Geb
 import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
 import Juvix.Compiler.Core.Data.Module qualified as Core
+import Juvix.Compiler.Core.Data.TransformationId qualified as Core
 import Juvix.Compiler.Nockma.Pretty qualified as Nockma
 import Juvix.Compiler.Reg.Pretty qualified as Reg
 import Juvix.Compiler.Tree.Pretty qualified as Tree
@@ -43,6 +44,7 @@ getEntry PipelineArg {..} = do
       TargetReg -> Backend.TargetReg
       TargetTree -> Backend.TargetTree
       TargetNockma -> Backend.TargetNockma
+      TargetAnoma -> Backend.TargetAnoma
 
     defaultOptLevel :: Int
     defaultOptLevel
@@ -135,7 +137,7 @@ runTreePipeline pa@PipelineArg {..} = do
   r <-
     runReader entryPoint
       . runError @JuvixError
-      . coreToTree
+      . coreToTree Core.Identity
       $ _pipelineArgModule
   tab' <- getRight r
   let code = Tree.ppPrint tab' tab'
@@ -153,3 +155,16 @@ runNockmaPipeline pa@PipelineArg {..} = do
   tab' <- getRight r
   let code = Nockma.ppSerialize tab'
   writeFileEnsureLn nockmaFile code
+
+runAnomaPipeline :: (Members '[Embed IO, App, TaggedLock] r) => PipelineArg -> Sem r ()
+runAnomaPipeline pa@PipelineArg {..} = do
+  entryPoint <- getEntry pa
+  nockmaFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  r <-
+    runReader entryPoint
+      . runError @JuvixError
+      . coreToAnoma
+      $ _pipelineArgModule
+  tab' <- getRight r
+  let code = Nockma.ppSerialize tab'
+  writeFileEnsureLn nockmaFile code

app/Commands/Dev/Core/Strip.hs

@@ -15,7 +15,7 @@ runCommand opts = do
   let r =
         run $
           runReader (project gopts) $
-            runError @JuvixError (Core.toStripped' (Core.moduleFromInfoTable tab) :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.Module)
+            runError @JuvixError (Core.toStripped' Core.Identity (Core.moduleFromInfoTable tab) :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.Module)
   tab' <- getRight $ mapLeft JuvixError $ mapRight (Stripped.fromCore . Core.computeCombinedInfoTable) r
   unless (project opts ^. coreStripNoPrint) $ do
     renderStdOut (Core.ppOut opts tab')

app/Commands/Dev/Nockma/Repl.hs

@@ -11,6 +11,7 @@ import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty
 import Juvix.Compiler.Nockma.Pretty qualified as Nockma
 import Juvix.Compiler.Nockma.Translation.FromSource (parseProgramFile, parseReplStatement, parseReplText, parseText)
+import Juvix.Compiler.Nockma.Translation.FromSource qualified as Nockma
 import Juvix.Parser.Error
 import Juvix.Prelude qualified as Prelude
 import System.Console.Haskeline
@@ -85,7 +86,8 @@ options =
     ("set-stack", setStack),
     ("load", loadFile . Prelude.absFile),
     ("reload", const reloadFile),
-    ("dir", direction')
+    ("dir", direction'),
+    ("help", const printHelpTxt)
   ]
 
 banner :: Repline.MultiLine -> Repl String
@@ -169,12 +171,22 @@ replAction =
       }
 
 runCommand :: forall r. (Members '[EmbedIO, App] r) => NockmaReplOptions -> Sem r ()
-runCommand _ = embed . (`State.evalStateT` iniState) $ replAction
+runCommand opts = do
+  mt :: Maybe (Term Natural) <- mapM iniStack (opts ^. nockmaReplOptionsStackFile)
+  embed . (`State.evalStateT` (iniState mt)) $ replAction
   where
-    iniState :: ReplState
-    iniState =
+    iniStack :: AppPath File -> Sem r (Term Natural)
+    iniStack af = do
+      afile <- fromAppPathFile af
+      parsedTerm <- Nockma.parseTermFile afile
+      case parsedTerm of
+        Left err -> exitJuvixError (JuvixError err)
+        Right t -> return t
+
+    iniState :: Maybe (Term Natural) -> ReplState
+    iniState mt =
       ReplState
-        { _replStateStack = Nothing,
+        { _replStateStack = mt,
           _replStateProgram = Nothing,
           _replStateLoadedFile = Nothing
         }

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

@@ -7,6 +7,8 @@ newtype NockmaReplOptions = NockmaReplOptions
   }
   deriving stock (Data)
 
+makeLenses ''NockmaReplOptions
+
 parseNockmaReplOptions :: Parser NockmaReplOptions
 parseNockmaReplOptions = do
   _nockmaReplOptionsStackFile <- optional (parseInputFile FileExtNockma)

app/Commands/Dev/Tree/Compile.hs

@@ -21,6 +21,7 @@ runCommand opts = do
     TargetReg -> runRegPipeline arg
     TargetTree -> return ()
     TargetNockma -> runNockmaPipeline arg
+    TargetAnoma -> runAnomaPipeline arg
   where
     getFile :: Sem r (Path Abs File)
     getFile = getMainFile (opts ^. compileInputFile)

app/Commands/Dev/Tree/Compile/Base.hs

@@ -39,6 +39,7 @@ getEntry PipelineArg {..} = do
       TargetReg -> Backend.TargetReg
       TargetTree -> Backend.TargetTree
       TargetNockma -> Backend.TargetNockma
+      TargetAnoma -> Backend.TargetAnoma
 
     defaultOptLevel :: Int
     defaultOptLevel
@@ -111,3 +112,16 @@ runNockmaPipeline pa@PipelineArg {..} = do
   tab' <- getRight r
   let code = Nockma.ppSerialize tab'
   writeFileEnsureLn nockmaFile code
+
+runAnomaPipeline :: (Members '[Embed IO, App, TaggedLock] r) => PipelineArg -> Sem r ()
+runAnomaPipeline pa@PipelineArg {..} = do
+  entryPoint <- getEntry pa
+  nockmaFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  r <-
+    runReader entryPoint
+      . runError @JuvixError
+      . treeToAnoma
+      $ _pipelineArgTable
+  tab' <- getRight r
+  let code = Nockma.ppSerialize tab'
+  writeFileEnsureLn nockmaFile code

app/Commands/Extra/Compile.hs

@@ -36,6 +36,7 @@ runCompile inputFile o = do
     TargetReg -> return (Right ())
     TargetTree -> return (Right ())
     TargetNockma -> return (Right ())
+    TargetAnoma -> return (Right ())
 
 prepareRuntime :: forall r. (Members '[App, EmbedIO] r) => Path Abs Dir -> CompileOptions -> Sem r ()
 prepareRuntime buildDir o = do
@@ -54,6 +55,7 @@ prepareRuntime buildDir o = do
     TargetReg -> return ()
     TargetTree -> return ()
     TargetNockma -> return ()
+    TargetAnoma -> return ()
   where
     wasiReleaseRuntime :: BS.ByteString
     wasiReleaseRuntime = $(FE.makeRelativeToProject "runtime/_build.wasm32-wasi/libjuvix.a" >>= FE.embedFile)
@@ -117,6 +119,8 @@ outputFile opts inputFile =
           replaceExtension' juvixTreeFileExt baseOutputFile
         TargetNockma ->
           replaceExtension' nockmaFileExt baseOutputFile
+        TargetAnoma ->
+          replaceExtension' nockmaFileExt baseOutputFile
 
 clangNativeCompile ::
   forall r.

app/Commands/Extra/Compile/Options.hs

@@ -14,6 +14,7 @@ data CompileTarget
   | TargetReg
   | TargetTree
   | TargetNockma
+  | TargetAnoma
   deriving stock (Eq, Data, Bounded, Enum)
 
 instance Show CompileTarget where
@@ -27,6 +28,7 @@ instance Show CompileTarget where
     TargetReg -> "reg"
     TargetTree -> "tree"
     TargetNockma -> "nockma"
+    TargetAnoma -> "anoma"
 
 data CompileOptions = CompileOptions
   { _compileDebug :: Bool,

src/Juvix/Compiler/Backend.hs

@@ -13,6 +13,7 @@ data Target
   | TargetReg
   | TargetTree
   | TargetNockma
+  | TargetAnoma
   deriving stock (Data, Eq, Show)
 
 data Limits = Limits
@@ -94,6 +95,8 @@ getLimits tgt debug = case tgt of
     defaultLimits
   TargetNockma ->
     defaultLimits
+  TargetAnoma ->
+    defaultLimits
 
 defaultLimits :: Limits
 defaultLimits =

src/Juvix/Compiler/Core/Data.hs

@@ -2,9 +2,11 @@ module Juvix.Compiler.Core.Data
   ( module Juvix.Compiler.Core.Data.InfoTable,
     module Juvix.Compiler.Core.Data.InfoTableBuilder,
     module Juvix.Compiler.Core.Data.Module,
+    module Juvix.Compiler.Core.Data.TransformationId,
   )
 where
 
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Data.Module
+import Juvix.Compiler.Core.Data.TransformationId

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

@@ -24,6 +24,7 @@ data TransformationId
   | CheckGeb
   | CheckExec
   | CheckVampIR
+  | CheckAnoma
   | Normalize
   | LetFolding
   | LambdaFolding
@@ -51,6 +52,7 @@ data PipelineId
   | PipelineGeb
   | PipelineVampIR
   | PipelineStripped
+  | PipelineExec
   deriving stock (Data, Bounded, Enum)
 
 type TransformationLikeId = TransformationLikeId' TransformationId PipelineId
@@ -67,9 +69,9 @@ toNormalizeTransformations = [CombineInfoTables, LetRecLifting, LetFolding, Unro
 toVampIRTransformations :: [TransformationId]
 toVampIRTransformations = [CombineInfoTables, FilterUnreachable, CheckVampIR, LetRecLifting, OptPhaseVampIR, UnrollRecursion, Normalize, LetHoisting]
 
-toStrippedTransformations :: [TransformationId]
-toStrippedTransformations =
-  [CombineInfoTables, FilterUnreachable, CheckExec, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps, RemoveTypeArgs]
+toStrippedTransformations :: TransformationId -> [TransformationId]
+toStrippedTransformations checkId =
+  [CombineInfoTables, FilterUnreachable, checkId, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps, RemoveTypeArgs]
 
 toGebTransformations :: [TransformationId]
 toGebTransformations = [CombineInfoTables, FilterUnreachable, CheckGeb, LetRecLifting, OptPhaseGeb, UnrollRecursion, FoldTypeSynonyms, ComputeTypeInfo]
@@ -96,6 +98,7 @@ instance TransformationId' TransformationId where
     CheckGeb -> strCheckGeb
     CheckExec -> strCheckExec
     CheckVampIR -> strCheckVampIR
+    CheckAnoma -> strCheckAnoma
     Normalize -> strNormalize
     LetFolding -> strLetFolding
     LambdaFolding -> strLambdaFolding
@@ -124,11 +127,13 @@ instance PipelineId' TransformationId PipelineId where
     PipelineGeb -> strGebPipeline
     PipelineVampIR -> strVampIRPipeline
     PipelineStripped -> strStrippedPipeline
+    PipelineExec -> strExecPipeline
 
   pipeline :: PipelineId -> [TransformationId]
   pipeline = \case
     PipelineStored -> toStoredTransformations
     PipelineNormalize -> toNormalizeTransformations
     PipelineGeb -> toGebTransformations
     PipelineVampIR -> toVampIRTransformations
-    PipelineStripped -> toStrippedTransformations
+    PipelineStripped -> toStrippedTransformations Identity
+    PipelineExec -> toStrippedTransformations CheckExec

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

@@ -20,6 +20,9 @@ strVampIRPipeline = "pipeline-vampir"
 strStrippedPipeline :: Text
 strStrippedPipeline = "pipeline-stripped"
 
+strExecPipeline :: Text
+strExecPipeline = "pipeline-exec"
+
 strLifting :: Text
 strLifting = "lifting"
 
@@ -77,6 +80,9 @@ strCheckExec = "check-exec"
 strCheckVampIR :: Text
 strCheckVampIR = "check-vampir"
 
+strCheckAnoma :: Text
+strCheckAnoma = "check-anoma"
+
 strNormalize :: Text
 strNormalize = "normalize"
 

src/Juvix/Compiler/Core/Pipeline.hs

@@ -21,11 +21,11 @@ toStored = mapReader fromEntryPoint . applyTransformations toStoredTransformatio
 
 -- | Perform transformations on stored Core necessary before the translation to
 -- Core.Stripped
-toStripped' :: (Members '[Error JuvixError, Reader CoreOptions] r) => Module -> Sem r Module
-toStripped' = applyTransformations toStrippedTransformations
+toStripped' :: (Members '[Error JuvixError, Reader CoreOptions] r) => TransformationId -> Module -> Sem r Module
+toStripped' checkId = applyTransformations (toStrippedTransformations checkId)
 
-toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
-toStripped = mapReader fromEntryPoint . applyTransformations toStrippedTransformations
+toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => TransformationId -> Module -> Sem r Module
+toStripped checkId = mapReader fromEntryPoint . applyTransformations (toStrippedTransformations checkId)
 
 -- | Perform transformations on stored Core necessary before the translation to GEB
 toGeb' :: (Members '[Error JuvixError, Reader CoreOptions] r) => Module -> Sem r Module

src/Juvix/Compiler/Core/Transformation.hs

@@ -13,6 +13,7 @@ import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.Check.Anoma
 import Juvix.Compiler.Core.Transformation.Check.Exec
 import Juvix.Compiler.Core.Transformation.Check.Geb
 import Juvix.Compiler.Core.Transformation.Check.VampIR
@@ -75,6 +76,7 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
       CheckGeb -> mapError (JuvixError @CoreError) . checkGeb
       CheckExec -> mapError (JuvixError @CoreError) . checkExec
       CheckVampIR -> mapError (JuvixError @CoreError) . checkVampIR
+      CheckAnoma -> mapError (JuvixError @CoreError) . checkAnoma
       Normalize -> return . normalize
       LetFolding -> return . letFolding
       LambdaFolding -> return . lambdaFolding

src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs

@@ -0,0 +1,13 @@
+module Juvix.Compiler.Core.Transformation.Check.Anoma where
+
+import Juvix.Compiler.Core.Error
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.Check.Base
+
+checkAnoma :: forall r. (Member (Error CoreError) r) => Module -> Sem r Module
+checkAnoma md = do
+  checkMainExists md
+  checkNoAxioms md
+  mapAllNodesM checkNoIO md
+  mapAllNodesM (checkBuiltins' [OpStrConcat, OpStrToInt, OpShow] [PrimString]) md

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

@@ -70,6 +70,22 @@ checkBuiltins allowUntypedFail = dmapRM go
           _ -> return $ Recur node
       _ -> return $ Recur node
 
+checkBuiltins' :: forall r. (Member (Error CoreError) r) => [BuiltinOp] -> [Primitive] -> Node -> Sem r Node
+checkBuiltins' unsupportedOps unsupportedTypes = dmapRM go
+  where
+    go :: Node -> Sem r Recur
+    go node = case node of
+      NPrim TypePrim {..}
+        | _typePrimPrimitive `elem` unsupportedTypes ->
+            throw $ unsupportedError "type" node (getInfoLocation _typePrimInfo)
+      NBlt BuiltinApp {..}
+        | _builtinAppOp `elem` unsupportedOps ->
+            throw $ unsupportedError "operation" node (getInfoLocation _builtinAppInfo)
+        | otherwise -> case _builtinAppOp of
+            OpFail -> return $ End node
+            _ -> return $ Recur node
+      _ -> return $ Recur node
+
 -- | Checks that the root of the node is not `Bottom`. Currently the only way we
 -- create `Bottom` is when translating axioms that are not builtin. Hence it is
 -- enough to check the root only.

src/Juvix/Compiler/Nockma/EvalCompiled.hs

@@ -3,14 +3,8 @@ module Juvix.Compiler.Nockma.EvalCompiled where
 import Juvix.Compiler.Nockma.Evaluator
 import Juvix.Compiler.Nockma.Language
 import Juvix.Compiler.Nockma.Pretty (ppTrace)
-import Juvix.Compiler.Nockma.Translation.FromTree
 import Juvix.Prelude
 
-compileAndRunNock' :: (Members '[Reader EvalOptions, Output (Term Natural)] r) => CompilerOptions -> ConstructorInfos -> [CompilerFunction] -> CompilerFunction -> Sem r (Term Natural)
-compileAndRunNock' opts constrs funs mainfun =
-  let Cell nockSubject t = runCompilerWith opts constrs funs mainfun
-   in evalCompiledNock' nockSubject t
-
 evalCompiledNock' :: (Members '[Reader EvalOptions, Output (Term Natural)] r) => Term Natural -> Term Natural -> Sem r (Term Natural)
 evalCompiledNock' stack mainTerm = do
   evalT <-

src/Juvix/Compiler/Nockma/Language.hs

@@ -247,6 +247,9 @@ nockBool = \case
   True -> nockTrue
   False -> nockFalse
 
+nockNil' :: Term Natural
+nockNil' = TermAtom nockNil
+
 data NockNaturalNaturalError
   = NaturalInvalidPath (Atom Natural)
   | NaturalInvalidOp (Atom Natural)