Direct translation from normalized JuvixCore to VampIR (#2086)

* Closes #2034.
* Adds the `vampir` target to the `compile` command.
* Adds two tests which are not yet enabled because `vamp-ir` is not
available in the CI (these and more tests will be enabled in #2103).

app/Commands/Compile.hs

@@ -23,6 +23,7 @@ runCommand opts@CompileOptions {..} = do
     TargetNative64 -> Compile.runCPipeline arg
     TargetWasm32Wasi -> Compile.runCPipeline arg
     TargetGeb -> Compile.runGebPipeline arg
+    TargetVampIR -> Compile.runVampIRPipeline arg
     TargetCore -> writeCoreFile arg
     TargetAsm -> Compile.runAsmPipeline arg
 

app/Commands/Dev/Asm/Compile.hs

@@ -40,6 +40,7 @@ runCommand opts = do
       TargetWasm32Wasi -> return Backend.TargetCWasm32Wasi
       TargetNative64 -> return Backend.TargetCNative64
       TargetGeb -> exitMsg (ExitFailure 1) "error: GEB target not supported for JuvixAsm"
+      TargetVampIR -> exitMsg (ExitFailure 1) "error: VampIR target not supported for JuvixAsm"
       TargetCore -> exitMsg (ExitFailure 1) "error: JuvixCore target not supported for JuvixAsm"
       TargetAsm -> exitMsg (ExitFailure 1) "error: JuvixAsm target not supported for JuvixAsm"
 

app/Commands/Dev/Core/Compile.hs

@@ -16,6 +16,7 @@ runCommand opts = do
     TargetWasm32Wasi -> runCPipeline arg
     TargetNative64 -> runCPipeline arg
     TargetGeb -> runGebPipeline arg
+    TargetVampIR -> runVampIRPipeline arg
     TargetCore -> return ()
     TargetAsm -> runAsmPipeline arg
   where

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

@@ -8,6 +8,7 @@ import Juvix.Compiler.Asm.Pretty qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 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.InfoTable qualified as Core
 import System.FilePath (takeBaseName)
 
@@ -33,6 +34,7 @@ getEntry PipelineArg {..} = do
       TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
       TargetNative64 -> Backend.TargetCNative64
       TargetGeb -> Backend.TargetGeb
+      TargetVampIR -> Backend.TargetVampIR
       TargetCore -> Backend.TargetCore
       TargetAsm -> Backend.TargetAsm
 
@@ -79,6 +81,17 @@ runGebPipeline pa@PipelineArg {..} = do
   Geb.Result {..} <- getRight (run (runReader entryPoint (runError (coreToGeb spec _pipelineArgInfoTable :: Sem '[Error JuvixError, Reader EntryPoint] Geb.Result))))
   embed $ TIO.writeFile (toFilePath gebFile) _resultCode
 
+runVampIRPipeline ::
+  forall r.
+  (Members '[Embed IO, App] r) =>
+  PipelineArg ->
+  Sem r ()
+runVampIRPipeline pa@PipelineArg {..} = do
+  entryPoint <- getEntry pa
+  vampirFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
+  VampIR.Result {..} <- getRight (run (runReader entryPoint (runError (coreToVampIR _pipelineArgInfoTable :: Sem '[Error JuvixError, Reader EntryPoint] VampIR.Result))))
+  embed $ TIO.writeFile (toFilePath vampirFile) _resultCode
+
 runAsmPipeline :: (Members '[Embed IO, App] r) => PipelineArg -> Sem r ()
 runAsmPipeline pa@PipelineArg {..} = do
   entryPoint <- getEntry pa

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

@@ -16,6 +16,7 @@ coreSupportedTargets =
     [ TargetWasm32Wasi,
       TargetNative64,
       TargetGeb,
+      TargetVampIR,
       TargetAsm
     ]
 

app/Commands/Dev/Core/Options.hs

@@ -105,4 +105,4 @@ parseCoreCommand =
     compileInfo =
       info
         (CoreCompile <$> parseCoreCompileOptions)
-        (progDesc "Compile a JuvixCore file to native code, WebAssembly or GEB")
+        (progDesc "Compile a JuvixCore file to native code, WebAssembly, GEB or VampIR")

app/Commands/Extra/Compile.hs

@@ -30,6 +30,7 @@ runCompile inputFile o = do
     TargetWasm32Wasi -> runError (clangWasmWasiCompile inputFile o)
     TargetNative64 -> runError (clangNativeCompile inputFile o)
     TargetGeb -> return $ Right ()
+    TargetVampIR -> return $ Right ()
     TargetCore -> return $ Right ()
     TargetAsm -> return $ Right ()
 
@@ -42,6 +43,7 @@ prepareRuntime buildDir o = do
     TargetNative64 | o ^. compileDebug -> writeRuntime nativeDebugRuntime
     TargetNative64 -> writeRuntime nativeReleaseRuntime
     TargetGeb -> return ()
+    TargetVampIR -> return ()
     TargetCore -> return ()
     TargetAsm -> return ()
   where
@@ -98,6 +100,8 @@ outputFile opts inputFile =
           if
               | opts ^. compileTerm -> replaceExtension' ".geb" inputFile
               | otherwise -> replaceExtension' ".lisp" baseOutputFile
+        TargetVampIR ->
+          replaceExtension' ".pir" baseOutputFile
         TargetCore ->
           replaceExtension' ".jvc" baseOutputFile
         TargetAsm ->

app/Commands/Extra/Compile/Options.hs

@@ -8,6 +8,7 @@ data CompileTarget
   = TargetWasm32Wasi
   | TargetNative64
   | TargetGeb
+  | TargetVampIR
   | TargetCore
   | TargetAsm
   deriving stock (Eq, Data, Bounded, Enum)
@@ -17,6 +18,7 @@ instance Show CompileTarget where
     TargetWasm32Wasi -> "wasm32-wasi"
     TargetNative64 -> "native"
     TargetGeb -> "geb"
+    TargetVampIR -> "vampir"
     TargetCore -> "core"
     TargetAsm -> "asm"
 

cntlines.sh

@@ -1,28 +1,34 @@
 #!/bin/bash
 
-RUNTIME=`find runtime/src/ -name '*.c' -or -name '*.h' | xargs wc -l | tail -1 | tr -d ' toal'`
+function count() {
+    cloc $1 | grep 'SUM:' | awk '{print $5}'
+}
 
-BACKENDC=`find src/Juvix/Compiler/Backend/C/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-GEB=`find src/Juvix/Compiler/Backend/Geb/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-REG=`find src/Juvix/Compiler/Reg/ -name '*.hs' -print | xargs wc -l | tail -1 | tr -d ' toal'`
-ASM=`find src/Juvix/Compiler/Asm/ -name '*.hs' -print | xargs wc -l | tail -1 | tr -d ' toal'`
-CORE=`find src/Juvix/Compiler/Core/ -name '*.hs' -print | xargs wc -l | tail -1 | tr -d ' toal'`
+RUNTIME=$(count runtime/src)
 
-CONCRETE=`find src/Juvix/Compiler/Concrete/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-ABSTRACT=`find src/Juvix/Compiler/Abstract/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-INTERNAL=`find src/Juvix/Compiler/Internal/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-BUILTINS=`find src/Juvix/Compiler/Builtins/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-PIPELINE=`find src/Juvix/Compiler/Pipeline/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
+BACKENDC=$(count src/Juvix/Compiler/Backend/C/)
+GEB=$(count src/Juvix/Compiler/Backend/Geb/)
+VAMPIR=$(count src/Juvix/Compiler/Backend/VampIR/)
+REG=$(count src/Juvix/Compiler/Reg/)
+ASM=$(count src/Juvix/Compiler/Asm/)
+CORE=$(count src/Juvix/Compiler/Core/)
 
-APP=`find app/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-HTML=`find src/Juvix/Compiler/Backend/Html/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-EXTRA=`find src/Juvix/Extra/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-DATA=`find src/Juvix/Data/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
-PRELUDE=`find src/Juvix/Prelude/ -name '*.hs' | xargs wc -l | tail -1 | tr -d ' toal'`
+CONCRETE=$(count src/Juvix/Compiler/Concrete/)
+ABSTRACT=$(count src/Juvix/Compiler/Abstract/)
+INTERNAL=$(count src/Juvix/Compiler/Internal/)
+BUILTINS=$(count src/Juvix/Compiler/Builtins/)
+PIPELINE=$(count src/Juvix/Compiler/Pipeline/)
+
+APP=$(count app/)
+HTML=$(count src/Juvix/Compiler/Backend/Html/)
+EXTRA=$(count src/Juvix/Extra/)
+DATA=$(count src/Juvix/Data/)
+PRELUDE=$(count src/Juvix/Prelude/)
 
 FRONT=$((CONCRETE + ABSTRACT + INTERNAL + BUILTINS + PIPELINE))
-BACK=$((BACKENDC + GEB + REG + ASM + CORE))
+BACK=$((BACKENDC + GEB + VAMPIR + REG + ASM + CORE))
 OTHER=$((APP + HTML + EXTRA + DATA + PRELUDE))
+TESTS=$(count test/)
 
 echo "Front end: $FRONT LOC"
 echo "   Concrete: $CONCRETE LOC"
@@ -31,8 +37,9 @@ echo "   Internal: $INTERNAL LOC"
 echo "   Builtins: $BUILTINS LOC"
 echo "   Pipeline: $PIPELINE LOC"
 echo "Middle and back end: $BACK LOC"
-echo "   C backend: $BACKENDC LOC"
+echo "   VampIR backend: $VAMPIR LOC"
 echo "   GEB backend: $GEB LOC"
+echo "   C backend: $BACKENDC LOC"
 echo "   JuvixReg: $REG LOC"
 echo "   JuvixAsm: $ASM LOC"
 echo "   JuvixCore: $CORE LOC"
@@ -43,3 +50,4 @@ echo "   Html: $HTML LOC"
 echo "   Extra: $EXTRA LOC"
 echo "   Data: $DATA LOC"
 echo "   Prelude: $PRELUDE LOC"
+echo "Tests: $TESTS LOC"

src/Juvix/Compiler/Backend.hs

@@ -7,6 +7,7 @@ data Target
   = TargetCWasm32Wasi
   | TargetCNative64
   | TargetGeb
+  | TargetVampIR
   | TargetCore
   | TargetAsm
   deriving stock (Data, Eq, Show)
@@ -62,6 +63,8 @@ getLimits tgt debug = case tgt of
       }
   TargetGeb ->
     defaultLimits
+  TargetVampIR ->
+    defaultLimits
   TargetCore ->
     defaultLimits
   TargetAsm ->

src/Juvix/Compiler/Backend/Geb/Pretty/Keywords.hs

@@ -4,34 +4,6 @@ import Juvix.Compiler.Backend.Geb.Language
 import Juvix.Data.CodeAnn
 import Juvix.Extra.Strings qualified as Str
 
-keywords :: [Doc Ann]
-keywords =
-  [ kwInitial,
-    kwTerminal,
-    kwProd,
-    kwCoprod,
-    kwHom,
-    kwInteger,
-    kwEq,
-    kwLt,
-    kwAbsurd,
-    kwUnit,
-    kwLeft,
-    kwRight,
-    kwFst,
-    kwSnd,
-    kwPair,
-    kwLamb,
-    kwApp,
-    kwVar,
-    kwAdd,
-    kwSub,
-    kwMul,
-    kwDiv,
-    kwMod,
-    kwFail
-  ]
-
 kwAbsurd :: Doc Ann
 kwAbsurd = keyword Str.gebAbsurd
 

src/Juvix/Compiler/Backend/VampIR/Language.hs

@@ -0,0 +1,81 @@
+module Juvix.Compiler.Backend.VampIR.Language
+  ( module Juvix.Compiler.Backend.VampIR.Language,
+    module Juvix.Prelude,
+  )
+where
+
+import Juvix.Prelude
+
+newtype Var = Var
+  { _varName :: Text
+  }
+
+data OpCode
+  = OpAdd
+  | OpSub
+  | OpMul
+  | OpDiv
+  | OpMod
+  | OpEq
+  | OpLt
+  | OpLe
+
+data Binop = Binop
+  { _binopOp :: OpCode,
+    _binopLeft :: Expression,
+    _binopRight :: Expression
+  }
+
+data IfThenElse = IfThenElse
+  { _ifThenElseCondition :: Expression,
+    _ifThenElseBranchTrue :: Expression,
+    _ifThenElseBranchFalse :: Expression
+  }
+
+data Expression
+  = ExpressionVar Var
+  | ExpressionConstant Integer
+  | ExpressionBinop Binop
+  | ExpressionIfThenElse IfThenElse
+  | ExpressionFail
+
+data LocalDef = LocalDef
+  { _localDefName :: Text,
+    _localDefValue :: Expression
+  }
+
+data Function = Function
+  { _functionName :: Text,
+    _functionArguments :: [Text],
+    _functionLocalDefs :: [LocalDef],
+    _functionExpression :: Expression
+  }
+
+newtype Program = Program
+  { _programFunctions :: [Function]
+  }
+
+makeLenses ''Var
+makeLenses ''Binop
+makeLenses ''IfThenElse
+makeLenses ''Expression
+makeLenses ''LocalDef
+makeLenses ''Function
+makeLenses ''Program
+
+instance HasAtomicity Var where
+  atomicity _ = Atom
+
+instance HasAtomicity Binop where
+  atomicity _ = Aggregate appFixity
+
+instance HasAtomicity IfThenElse where
+  atomicity _ = Aggregate appFixity
+
+instance HasAtomicity Expression where
+  atomicity = \case
+    ExpressionVar x -> atomicity x
+    ExpressionConstant {} -> Atom
+    ExpressionBinop x -> atomicity x
+    ExpressionIfThenElse x -> atomicity x
+    ExpressionFail -> Atom

src/Juvix/Compiler/Backend/VampIR/Pretty.hs

@@ -0,0 +1,28 @@
+module Juvix.Compiler.Backend.VampIR.Pretty
+  ( module Juvix.Compiler.Backend.VampIR.Pretty,
+    module Juvix.Compiler.Backend.VampIR.Pretty.Base,
+    module Juvix.Compiler.Backend.VampIR.Pretty.Options,
+    module Juvix.Data.PPOutput,
+  )
+where
+
+import Juvix.Compiler.Backend.VampIR.Language
+import Juvix.Compiler.Backend.VampIR.Pretty.Base
+import Juvix.Compiler.Backend.VampIR.Pretty.Options
+import Juvix.Data.PPOutput
+import Prettyprinter.Render.Terminal qualified as Ansi
+
+ppOutDefault :: PrettyCode c => c -> AnsiText
+ppOutDefault = AnsiText . PPOutput . doc defaultOptions
+
+ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText
+ppOut o = AnsiText . PPOutput . doc (project o)
+
+ppTrace' :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> Text
+ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts)
+
+ppTrace :: PrettyCode c => c -> Text
+ppTrace = ppTrace' traceOptions
+
+ppPrint :: PrettyCode c => c -> Text
+ppPrint = show . ppOutDefault

src/Juvix/Compiler/Backend/VampIR/Pretty/Base.hs

@@ -0,0 +1,142 @@
+module Juvix.Compiler.Backend.VampIR.Pretty.Base where
+
+import Juvix.Compiler.Backend.VampIR.Language
+import Juvix.Compiler.Backend.VampIR.Pretty.Keywords
+import Juvix.Compiler.Backend.VampIR.Pretty.Options
+import Juvix.Data.CodeAnn
+import Juvix.Data.NameKind
+
+class PrettyCode c where
+  ppCode :: Member (Reader Options) r => c -> Sem r (Doc Ann)
+
+doc :: PrettyCode c => Options -> c -> Doc Ann
+doc opts x =
+  run $
+    runReader opts $
+      ppCode x
+
+ppName :: NameKind -> Text -> Sem r (Doc Ann)
+ppName k n = return $ annotate (AnnKind k) (pretty n)
+
+instance PrettyCode Var where
+  ppCode Var {..} = ppName KNameLocal _varName
+
+instance PrettyCode OpCode where
+  ppCode = \case
+    OpAdd -> return kwAdd
+    OpSub -> return kwSub
+    OpMul -> return kwMul
+    OpDiv -> return kwDiv
+    OpMod -> return kwMod
+    OpEq -> return kwEqual
+    OpLt -> return kwLessThan
+    OpLe -> return kwLessOrEqual
+
+instance PrettyCode Binop where
+  ppCode Binop {..} = do
+    op <- ppCode _binopOp
+    l <- ppArg _binopLeft
+    r <- ppArg _binopRight
+    return $ op <+> l <+> r
+
+instance PrettyCode IfThenElse where
+  ppCode IfThenElse {..} = do
+    c <- ppArg _ifThenElseCondition
+    l <- ppArg _ifThenElseBranchTrue
+    r <- ppArg _ifThenElseBranchFalse
+    return $ kwIf <+> c <+> l <+> r
+
+instance PrettyCode Expression where
+  ppCode = \case
+    ExpressionVar x -> ppCode x
+    ExpressionConstant i -> return $ annotate AnnLiteralInteger (pretty i)
+    ExpressionBinop x -> ppCode x
+    ExpressionIfThenElse x -> ppCode x
+    ExpressionFail -> return $ annotate AnnLiteralInteger "0"
+
+instance PrettyCode LocalDef where
+  ppCode LocalDef {..} = do
+    n <- ppName KNameLocal _localDefName
+    v <- ppCode _localDefValue
+    return $ kwDef <+> n <+> kwEq <+> v <> semi <> line
+
+instance PrettyCode Function where
+  ppCode Function {..} = do
+    n <- ppName KNameFunction _functionName
+    args <- mapM (ppName KNameLocal) _functionArguments
+    defs <- mapM ppCode _functionLocalDefs
+    e <- ppCode _functionExpression
+    return $ kwDef <+> hsep (n : args) <+> kwEq <+> bracesIndent (vsep defs <> line <> e) <> semi
+
+ppEquation :: Function -> Sem r (Doc Ann)
+ppEquation Function {..} = do
+  let n = length _functionArguments
+      args = if n == 1 then ["in"] else map (\k -> "in" <> show k) [1 .. n]
+  fn <- ppName KNameFunction _functionName
+  return $ fn <+> hsep args <+> kwEq <+> "out" <> semi
+
+instance PrettyCode Program where
+  ppCode Program {..} = do
+    fns <- mapM ppCode _programFunctions
+    eqns <- mapM ppEquation _programFunctions
+    return $ vsep vampIRDefs <> line <> line <> vsep fns <> line <> line <> vsep eqns
+
+--------------------------------------------------------------------------------
+-- VampIR definitions
+--------------------------------------------------------------------------------
+
+vampIRDefs :: [Doc Ann]
+vampIRDefs =
+  [ "def add x y = x + y;",
+    "def sub x y = x - y;",
+    "def mul x y = x * y;",
+    "def isZero x = {def xi = fresh (1 | x); x * (1 - xi * x) = 0; 1 - xi * x};",
+    "def equal x y = isZero (x - y);",
+    "def bool x = {x * (x - 1) = 0; x};",
+    "def range32 a = {def a0 = bool (fresh ((a \\ 1) % 2)); def a1 = bool (fresh ((a \\ 2) % 2)); def a2 = bool (fresh ((a \\ 4) % 2)); def a3 = bool (fresh ((a \\ 8) % 2)); def a4 = bool (fresh ((a \\ 16) % 2)); def a5 = bool (fresh ((a \\ 32) % 2)); def a6 = bool (fresh ((a \\ 64) % 2)); def a7 = bool (fresh ((a \\ 128) % 2)); def a8 = bool (fresh ((a \\ 256) % 2)); def a9 = bool (fresh ((a \\ 512) % 2)); def a10 = bool (fresh ((a \\ 1024) % 2)); def a11 = bool (fresh ((a \\ 2048) % 2)); def a12 = bool (fresh ((a \\ 4096) % 2)); def a13 = bool (fresh ((a \\ 8192) % 2)); def a14 = bool (fresh ((a \\ 16384) % 2)); def a15 = bool (fresh ((a \\ 32768) % 2)); def a16 = bool (fresh ((a \\ 65536) % 2)); def a17 = bool (fresh ((a \\ 131072) % 2)); def a18 = bool (fresh ((a \\ 262144) % 2)); def a19 = bool (fresh ((a \\ 524288) % 2)); def a20 = bool (fresh ((a \\ 1048576) % 2)); def a21 = bool (fresh ((a \\ 2097152) % 2)); def a22 = bool (fresh ((a \\ 4194304) % 2)); def a23 = bool (fresh ((a \\ 8388608) % 2)); def a24 = bool (fresh ((a \\ 16777216) % 2)); def a25 = bool (fresh ((a \\ 33554432) % 2)); def a26 = bool (fresh ((a \\ 67108864) % 2)); def a27 = bool (fresh ((a \\ 134217728) % 2)); def a28 = bool (fresh ((a \\ 268435456) % 2)); def a29 = bool (fresh ((a \\ 536870912) % 2)); def a30 = bool (fresh ((a \\ 1073741824) % 2)); def a31 = bool (fresh ((a \\ 2147483648) % 2)); a = ((((((((((((((((((((((((((((((a0 + (2 * a1)) + (4 * a2)) + (8 * a3)) + (16 * a4)) + (32 * a5)) + (64 * a6)) + (128 * a7)) + (256 * a8)) + (512 * a9)) + (1024 * a10)) + (2048 * a11)) + (4096 * a12)) + (8192 * a13)) + (16384 * a14)) + (32768 * a15)) + (65536 * a16)) + (131072 * a17)) + (262144 * a18)) + (524288 * a19)) + (1048576 * a20)) + (2097152 * a21)) + (4194304 * a22)) + (8388608 * a23)) + (16777216 * a24)) + (33554432 * a25)) + (67108864 * a26)) + (134217728 * a27)) + (268435456 * a28)) + (536870912 * a29)) + (1073741824 * a30)) + (2147483648 * a31); (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, ())};",
+    "def intrange32 a = {range32 (a + 2147483648)};",
+    "def negative32 a = {def (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, ()) = intrange32 a; a31};",
+    "def isNegative x = negative32 x;",
+    "def lessThan x y = isNegative (x - y);",
+    "def lessOrEqual x y = lessThan x (y + 1);",
+    "def divRem a b = {def q = fresh (a\\b); def r = fresh (a%b); isNegative r = 0; lessThan r b = 1; a = b * q + r; (q, r) };",
+    "def fst (x, y) = x;",
+    "def snd (x, y) = y;",
+    "def div x y = fst (divRem x y);",
+    "def rem x y = snd (divRem x y);",
+    "def if b x y = b * x + (1 - b) * y;"
+  ]
+
+--------------------------------------------------------------------------------
+-- helper functions
+--------------------------------------------------------------------------------
+
+ppArg ::
+  (PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
+  a ->
+  Sem r (Doc Ann)
+ppArg = ppRightExpression appFixity
+
+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

src/Juvix/Compiler/Backend/VampIR/Pretty/Keywords.hs

@@ -0,0 +1,38 @@
+module Juvix.Compiler.Backend.VampIR.Pretty.Keywords where
+
+import Juvix.Compiler.Backend.VampIR.Language
+import Juvix.Data.CodeAnn
+import Juvix.Extra.Strings qualified as Str
+
+kwDef :: Doc Ann
+kwDef = keyword Str.vampirDef
+
+kwEq :: Doc Ann
+kwEq = keyword Str.vampirEq
+
+kwAdd :: Doc Ann
+kwAdd = keyword Str.vampirAdd
+
+kwSub :: Doc Ann
+kwSub = keyword Str.vampirSub
+
+kwMul :: Doc Ann
+kwMul = keyword Str.vampirMul
+
+kwDiv :: Doc Ann
+kwDiv = keyword Str.vampirDiv
+
+kwMod :: Doc Ann
+kwMod = keyword Str.vampirMod
+
+kwEqual :: Doc Ann
+kwEqual = keyword Str.vampirEqual
+
+kwLessThan :: Doc Ann
+kwLessThan = keyword Str.vampirLessThan
+
+kwLessOrEqual :: Doc Ann
+kwLessOrEqual = keyword Str.vampirLessOrEqual
+
+kwIf :: Doc Ann
+kwIf = keyword Str.vampirIf

src/Juvix/Compiler/Backend/VampIR/Pretty/Options.hs

@@ -0,0 +1,21 @@
+module Juvix.Compiler.Backend.VampIR.Pretty.Options where
+
+import Juvix.Prelude
+
+-- no fields for now, but make it easier to add options in the future I don't
+-- remove this datatype entirely
+data Options = Options
+
+makeLenses ''Options
+
+defaultOptions :: Options
+defaultOptions = Options
+
+traceOptions :: Options
+traceOptions = defaultOptions
+
+fromGenericOptions :: GenericOptions -> Options
+fromGenericOptions _ = defaultOptions
+
+instance CanonicalProjection GenericOptions Options where
+  project = fromGenericOptions

src/Juvix/Compiler/Backend/VampIR/Translation.hs

@@ -0,0 +1,18 @@
+module Juvix.Compiler.Backend.VampIR.Translation
+  ( module Juvix.Compiler.Backend.VampIR.Translation,
+    module Juvix.Compiler.Backend.VampIR.Translation.FromCore,
+  )
+where
+
+import Juvix.Compiler.Backend.VampIR.Language
+import Juvix.Compiler.Backend.VampIR.Pretty
+import Juvix.Compiler.Backend.VampIR.Translation.FromCore
+
+newtype Result = Result
+  { _resultCode :: Text
+  }
+
+toResult :: Program -> Result
+toResult p = Result $ ppPrint p
+
+makeLenses ''Result

src/Juvix/Compiler/Backend/VampIR/Translation/FromCore.hs

@@ -0,0 +1,97 @@
+module Juvix.Compiler.Backend.VampIR.Translation.FromCore where
+
+import Data.Text qualified as T
+import Juvix.Compiler.Backend.VampIR.Language as VampIR
+import Juvix.Compiler.Core.Data.InfoTable
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info.NameInfo (getInfoName)
+import Juvix.Compiler.Core.Language as Core
+import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNodeNames')
+
+fromCore :: InfoTable -> Program
+fromCore tab = fromCoreNode $ lookupIdentifierNode tab (fromJust (tab ^. infoMain))
+
+fromCoreNode :: Node -> Program
+fromCoreNode node =
+  let (lams, body) = unfoldLambdas (disambiguateNodeNames' disambiguate emptyInfoTable node)
+      (defs, expr) = convertLets body
+   in Program
+        { _programFunctions =
+            [ Function
+                { _functionName = "main",
+                  _functionArguments = map (^. lambdaLhsBinder . binderName) lams,
+                  _functionLocalDefs = defs,
+                  _functionExpression = expr
+                }
+            ]
+        }
+  where
+    isValidChar :: Char -> Bool
+    isValidChar c = c == '_' || ((isLetter c || isDigit c) && isAscii c)
+
+    mkName :: Text -> Text
+    mkName ident = "var_" <> T.filter isValidChar ident
+
+    disambiguate :: BinderList Binder -> Text -> Text
+    disambiguate bl name = mkName name <> "_" <> show (length bl)
+
+    convertLets :: Core.Node -> ([LocalDef], Expression)
+    convertLets = \case
+      NLet Let {..} ->
+        let (defs, expr) = convertLets _letBody
+            def =
+              LocalDef
+                { _localDefName = _letItem ^. letItemBinder . binderName,
+                  _localDefValue = convertExpr (_letItem ^. letItemValue)
+                }
+         in (def : defs, expr)
+      nd ->
+        ([], convertExpr nd)
+
+    convertExpr :: Core.Node -> Expression
+    convertExpr = \case
+      NVar x -> goVar x
+      NCst x -> goConstant x
+      NBlt x -> goBuiltinApp x
+      NCtr x -> goConstructor x
+      NCase c -> goCase c
+      _ -> impossible
+
+    goVar :: Core.Var -> Expression
+    goVar Core.Var {..} = ExpressionVar $ VampIR.Var (getInfoName _varInfo)
+
+    goConstant :: Constant -> Expression
+    goConstant Constant {..} = case _constantValue of
+      ConstInteger i -> ExpressionConstant i
+      _ -> impossible
+
+    goBuiltinApp :: BuiltinApp -> Expression
+    goBuiltinApp BuiltinApp {..} = case _builtinAppArgs of
+      [l, r] ->
+        ExpressionBinop (Binop op (convertExpr l) (convertExpr r))
+        where
+          op = case _builtinAppOp of
+            OpIntAdd -> OpAdd
+            OpIntSub -> OpSub
+            OpIntMul -> OpMul
+            OpIntDiv -> OpDiv
+            OpIntMod -> OpMod
+            OpIntLt -> OpLt
+            OpIntLe -> OpLe
+            Core.OpEq -> VampIR.OpEq
+            _ -> impossible
+      _ -> case _builtinAppOp of
+        OpFail -> ExpressionFail
+        _ -> impossible
+
+    goConstructor :: Constr -> Expression
+    goConstructor Constr {..} = case _constrTag of
+      BuiltinTag TagTrue -> ExpressionConstant 1
+      BuiltinTag TagFalse -> ExpressionConstant 0
+      _ -> impossible
+
+    goCase :: Case -> Expression
+    goCase c = translateCase translateIf impossible c
+      where
+        translateIf :: Node -> Node -> Node -> Expression
+        translateIf val br1 br2 = ExpressionIfThenElse $ IfThenElse (convertExpr val) (convertExpr br1) (convertExpr br2)

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

@@ -36,6 +36,7 @@ data PipelineId
   = PipelineEval
   | PipelineNormalize
   | PipelineGeb
+  | PipelineVampIR
   | PipelineStripped
   deriving stock (Data, Bounded, Enum)
 
@@ -81,4 +82,5 @@ pipeline = \case
   PipelineEval -> toEvalTransformations
   PipelineNormalize -> toNormalizeTransformations
   PipelineGeb -> toGebTransformations
+  PipelineVampIR -> toVampIRTransformations
   PipelineStripped -> toStrippedTransformations

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

@@ -53,6 +53,7 @@ pipelineText = \case
   PipelineEval -> strEvalPipeline
   PipelineNormalize -> strNormalizePipeline
   PipelineGeb -> strGebPipeline
+  PipelineVampIR -> strVampIRPipeline
   PipelineStripped -> strStrippedPipeline
 
 transformationLikeText :: TransformationLikeId -> Text
@@ -111,6 +112,9 @@ strNormalizePipeline = "pipeline-normalize"
 strGebPipeline :: Text
 strGebPipeline = "pipeline-geb"
 
+strVampIRPipeline :: Text
+strVampIRPipeline = "pipeline-vampir"
+
 strStrippedPipeline :: Text
 strStrippedPipeline = "pipeline-stripped"
 

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

@@ -291,6 +291,27 @@ builtinOpArgTypes = \case
   OpTrace -> [mkDynamic']
   OpFail -> [mkTypeString']
 
+translateCase :: (Node -> Node -> Node -> a) -> a -> Case -> a
+translateCase translateIf dflt Case {..} = case _caseBranches of
+  [br@CaseBranch {..}]
+    | _caseBranchTag == BuiltinTag TagTrue ->
+        translateIf _caseValue (br ^. caseBranchBody) (fromMaybe branchFailure _caseDefault)
+  [br@CaseBranch {..}]
+    | _caseBranchTag == BuiltinTag TagFalse ->
+        translateIf _caseValue (fromMaybe branchFailure _caseDefault) (br ^. caseBranchBody)
+  [br1, br2]
+    | br1 ^. caseBranchTag == BuiltinTag TagTrue
+        && br2 ^. caseBranchTag == BuiltinTag TagFalse ->
+        translateIf _caseValue (br1 ^. caseBranchBody) (br2 ^. caseBranchBody)
+    | br1 ^. caseBranchTag == BuiltinTag TagFalse
+        && br2 ^. caseBranchTag == BuiltinTag TagTrue ->
+        translateIf _caseValue (br2 ^. caseBranchBody) (br1 ^. caseBranchBody)
+  _ ->
+    dflt
+  where
+    branchFailure :: Node
+    branchFailure = mkBuiltinApp' OpFail [mkConstant' (ConstString "illegal `if` branch")]
+
 checkDepth :: Int -> Node -> Bool
 checkDepth 0 _ = False
 checkDepth d node = all (checkDepth (d - 1)) (childrenNodes node)

src/Juvix/Compiler/Core/Pipeline.hs

@@ -33,3 +33,10 @@ toGeb' = applyTransformations toGebTransformations
 
 toGeb :: Members '[Error JuvixError, Reader EntryPoint] r => InfoTable -> Sem r InfoTable
 toGeb = mapReader fromEntryPoint . applyTransformations toGebTransformations
+
+-- | Perform transformations on Core necessary before the translation to VampIR
+toVampIR' :: Members '[Error JuvixError, Reader CoreOptions] r => InfoTable -> Sem r InfoTable
+toVampIR' = applyTransformations toVampIRTransformations
+
+toVampIR :: Members '[Error JuvixError, Reader EntryPoint] r => InfoTable -> Sem r InfoTable
+toVampIR = mapReader fromEntryPoint . applyTransformations toVampIRTransformations

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

@@ -7,8 +7,8 @@ import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info.NameInfo (setInfoName)
 import Juvix.Compiler.Core.Transformation.Base
 
-disambiguateNodeNames :: InfoTable -> Node -> Node
-disambiguateNodeNames tab = dmapL go
+disambiguateNodeNames' :: (BinderList Binder -> Text -> Text) -> InfoTable -> Node -> Node
+disambiguateNodeNames' disambiguate tab = dmapL go
   where
     go :: BinderList Binder -> Node -> Node
     go bl node = case node of
@@ -66,6 +66,9 @@ disambiguateNodeNames tab = dmapL go
             (bl', args') = disambiguatePatterns (BL.cons b' bl) (c ^. patternConstrArgs)
             pat' = PatConstr $ set patternConstrBinder b' $ set patternConstrArgs args' c
 
+disambiguateNodeNames :: InfoTable -> Node -> Node
+disambiguateNodeNames tab = disambiguateNodeNames' disambiguate tab
+  where
     disambiguate :: BinderList Binder -> Text -> Text
     disambiguate bl name =
       if

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -135,26 +135,14 @@ translateNode node = case node of
       )
       (translateNode (_letItem ^. letItemValue))
       (translateNode _letBody)
-  NCase Case {..} -> case _caseBranches of
-    [br@CaseBranch {..}]
-      | _caseBranchTag == BuiltinTag TagTrue ->
-          translateIf _caseValue (br ^. caseBranchBody) (fromMaybe branchFailure _caseDefault)
-    [br@CaseBranch {..}]
-      | _caseBranchTag == BuiltinTag TagFalse ->
-          translateIf _caseValue (fromMaybe branchFailure _caseDefault) (br ^. caseBranchBody)
-    [br1, br2]
-      | br1 ^. caseBranchTag == BuiltinTag TagTrue
-          && br2 ^. caseBranchTag == BuiltinTag TagFalse ->
-          translateIf _caseValue (br1 ^. caseBranchBody) (br2 ^. caseBranchBody)
-      | br1 ^. caseBranchTag == BuiltinTag TagFalse
-          && br2 ^. caseBranchTag == BuiltinTag TagTrue ->
-          translateIf _caseValue (br2 ^. caseBranchBody) (br1 ^. caseBranchBody)
-    _ ->
-      Stripped.mkCase
-        _caseInductive
-        (translateNode _caseValue)
-        (map translateCaseBranch _caseBranches)
-        (fmap translateNode _caseDefault)
+  NCase c@Case {..} -> translateCase translateIf dflt c
+    where
+      dflt =
+        Stripped.mkCase
+          _caseInductive
+          (translateNode _caseValue)
+          (map translateCaseBranch _caseBranches)
+          (fmap translateNode _caseDefault)
   _
     | isType node ->
         Stripped.mkConstr (Stripped.ConstrInfo "()" Nothing Stripped.TyDynamic) (BuiltinTag TagTrue) []
@@ -167,9 +155,6 @@ translateNode node = case node of
     translateIf :: Node -> Node -> Node -> Stripped.Node
     translateIf val br1 br2 = Stripped.mkIf (translateNode val) (translateNode br1) (translateNode br2)
 
-    branchFailure :: Node
-    branchFailure = mkBuiltinApp' OpFail [mkConstant' (ConstString "illegal `if` branch")]
-
     translateCaseBranch :: CaseBranch -> Stripped.CaseBranch
     translateCaseBranch CaseBranch {..}
       | _caseBranchTag == BuiltinTag TagTrue || _caseBranchTag == BuiltinTag TagFalse =

src/Juvix/Compiler/Pipeline.hs

@@ -14,6 +14,7 @@ import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm
 import Juvix.Compiler.Backend qualified as Backend
 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.Builtins
 import Juvix.Compiler.Concrete.Data.Highlight.Input
 import Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder.BuilderState qualified as Concrete
@@ -139,6 +140,9 @@ regToMiniC tab = do
 coreToGeb :: Members '[Error JuvixError, Reader EntryPoint] r => Geb.ResultSpec -> Core.InfoTable -> Sem r Geb.Result
 coreToGeb spec = Core.toGeb >=> return . uncurry (Geb.toResult spec) . Geb.fromCore
 
+coreToVampIR :: Members '[Error JuvixError, Reader EntryPoint] r => Core.InfoTable -> Sem r VampIR.Result
+coreToVampIR = Core.toVampIR >=> return . VampIR.toResult . VampIR.fromCore
+
 asmToMiniC' :: Members '[Error JuvixError, Reader Asm.Options] r => Asm.InfoTable -> Sem r C.MiniCResult
 asmToMiniC' = mapError (JuvixError @Asm.AsmError) . Asm.toReg' >=> regToMiniC' . Reg.fromAsm
 
@@ -147,6 +151,9 @@ regToMiniC' tab = do
   e <- ask
   return $ C.fromReg (e ^. Asm.optLimits) tab
 
+coreToVampIR' :: Members '[Error JuvixError, Reader Core.CoreOptions] r => Core.InfoTable -> Sem r VampIR.Result
+coreToVampIR' = Core.toVampIR' >=> return . VampIR.toResult . VampIR.fromCore
+
 --------------------------------------------------------------------------------
 -- Run pipeline
 --------------------------------------------------------------------------------

src/Juvix/Extra/Strings.hs

@@ -613,3 +613,36 @@ gebTyped = "typed"
 
 juvixDotOrg :: (IsString s) => s
 juvixDotOrg = "https://juvix.org"
+
+vampirDef :: IsString s => s
+vampirDef = "def"
+
+vampirEq :: IsString s => s
+vampirEq = "="
+
+vampirAdd :: IsString s => s
+vampirAdd = "add"
+
+vampirSub :: IsString s => s
+vampirSub = "sub"
+
+vampirMul :: IsString s => s
+vampirMul = "mul"
+
+vampirDiv :: IsString s => s
+vampirDiv = "div"
+
+vampirMod :: IsString s => s
+vampirMod = "rem"
+
+vampirEqual :: IsString s => s
+vampirEqual = "equal"
+
+vampirLessThan :: IsString s => s
+vampirLessThan = "lessThan"
+
+vampirLessOrEqual :: IsString s => s
+vampirLessOrEqual = "lessOrEqual"
+
+vampirIf :: IsString s => s
+vampirIf = "if"

test/VampIR.hs

@@ -0,0 +1,7 @@
+module VampIR where
+
+import Base
+import VampIR.Core.Positive qualified as PT
+
+allTests :: TestTree
+allTests = testGroup "VampIR tests" [PT.allTests]

test/VampIR/Core/Base.hs

@@ -0,0 +1,89 @@
+module VampIR.Core.Base where
+
+import Base
+import Data.Text.IO qualified as TIO
+import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
+import Juvix.Compiler.Core
+import Juvix.Prelude.Pretty
+import System.Process qualified as P
+
+vampirAssertion :: Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
+vampirAssertion mainFile dataFile step = do
+  step "Parse"
+  s <- readFile (toFilePath mainFile)
+  case runParserMain mainFile emptyInfoTable s of
+    Left err -> assertFailure (show err)
+    Right tab -> do
+      withTempDir'
+        ( \dirPath -> do
+            step "Translate to VampIR"
+            let vampirFile = dirPath <//> $(mkRelFile "program.pir")
+            case run (runReader defaultCoreOptions (runError @JuvixError (coreToVampIR' tab))) of
+              Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
+              Right VampIR.Result {..} -> do
+                TIO.writeFile (toFilePath vampirFile) _resultCode
+                vampirAssertion' vampirFile dataFile step
+        )
+
+vampirAssertion' :: Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
+vampirAssertion' inputFile dataFile step = do
+  step "Check vamp-ir on path"
+  assertCmdExists $(mkRelFile "vamp-ir")
+
+  withTempDir'
+    ( \dirPath -> do
+        step "VampIR setup parameters"
+        P.callProcess "vamp-ir" (setupParamsArgs dirPath)
+        step "VampIR compile"
+        P.callProcess "vamp-ir" (compileArgs inputFile dirPath)
+        step "VampIR prove"
+        P.callProcess "vamp-ir" (proveArgs dataFile dirPath)
+        step "VampIR verify"
+        P.callProcess "vamp-ir" (verifyArgs dirPath)
+    )
+
+setupParamsArgs :: Path Abs Dir -> [String]
+setupParamsArgs dirPath =
+  [ "plonk",
+    "setup",
+    "-o",
+    toFilePath (dirPath <//> $(mkRelFile "params.pp"))
+  ]
+
+compileArgs :: Path Abs File -> Path Abs Dir -> [String]
+compileArgs inputFile dirPath =
+  [ "plonk",
+    "compile",
+    "-u",
+    toFilePath (dirPath <//> $(mkRelFile "params.pp")),
+    "-s",
+    toFilePath inputFile,
+    "-o",
+    toFilePath (dirPath <//> $(mkRelFile "circuit.plonk"))
+  ]
+
+proveArgs :: Path Abs File -> Path Abs Dir -> [String]
+proveArgs dataFile dirPath =
+  [ "plonk",
+    "prove",
+    "-u",
+    toFilePath (dirPath <//> $(mkRelFile "params.pp")),
+    "-c",
+    toFilePath (dirPath <//> $(mkRelFile "circuit.plonk")),
+    "-o",
+    toFilePath (dirPath <//> $(mkRelFile "proof.plonk")),
+    "-i",
+    toFilePath dataFile
+  ]
+
+verifyArgs :: Path Abs Dir -> [String]
+verifyArgs dirPath =
+  [ "plonk",
+    "verify",
+    "-u",
+    toFilePath (dirPath <//> $(mkRelFile "params.pp")),
+    "-c",
+    toFilePath (dirPath <//> $(mkRelFile "circuit.plonk")),
+    "-p",
+    toFilePath (dirPath <//> $(mkRelFile "proof.plonk"))
+  ]

test/VampIR/Core/Positive.hs

@@ -0,0 +1,47 @@
+module VampIR.Core.Positive where
+
+import Base
+import VampIR.Core.Base
+
+data PosTest = PosTest
+  { _name :: String,
+    _relDir :: Path Rel Dir,
+    _file :: Path Rel File,
+    _dataFile :: Path Rel File
+  }
+
+makeLenses ''PosTest
+
+root :: Path Abs Dir
+root = relToProject $(mkRelDir "tests/VampIR/positive/translation")
+
+testDescr :: PosTest -> TestDescr
+testDescr PosTest {..} =
+  let tRoot = root <//> _relDir
+      file' = tRoot <//> _file
+      data' = tRoot <//> _dataFile
+   in TestDescr
+        { _testName = _name,
+          _testRoot = tRoot,
+          _testAssertion = Steps $ vampirAssertion file' data'
+        }
+
+allTests :: TestTree
+allTests =
+  testGroup
+    "VampIR translation positive tests"
+    (map (mkTest . testDescr) tests)
+
+tests :: [PosTest]
+tests =
+  [ PosTest
+      "Test001"
+      $(mkRelDir ".")
+      $(mkRelFile "test001.jvc")
+      $(mkRelFile "data/test001.json"),
+    PosTest
+      "Test002"
+      $(mkRelDir ".")
+      $(mkRelFile "test002.jvc")
+      $(mkRelFile "data/test002.json")
+  ]

tests/VampIR/positive/translation/data/test001.json

@@ -0,0 +1,4 @@
+{
+    "in": "3",
+    "out": "45"
+}

tests/VampIR/positive/translation/data/test002.json

@@ -0,0 +1,5 @@
+{
+    "in1": "3",
+    "in2": "4",
+    "out": "7"
+}

tests/VampIR/positive/translation/test001.jvc

@@ -0,0 +1,2 @@
+
+\(x : Int) let y := 2 * x in if x = 0 then 1 else x + 7 * y

tests/VampIR/positive/translation/test002.jvc

@@ -0,0 +1,2 @@
+
+\(x : Int) \(y : Int) if (if x = y then false else true) then x + y else 0