diff --git a/app/Commands/Compile.hs b/app/Commands/Compile.hs index 1d6cb9cf79..c8abf22137 100644 --- a/app/Commands/Compile.hs +++ b/app/Commands/Compile.hs @@ -10,7 +10,6 @@ import Commands.Compile.Cairo qualified as Cairo import Commands.Compile.Native qualified as Native import Commands.Compile.Options import Commands.Compile.RiscZeroRust qualified as RiscZeroRust -import Commands.Compile.Vampir qualified as Vampir import Commands.Compile.Wasi qualified as Wasi runCommand :: (Members AppEffects r) => CompileCommand -> Sem r () @@ -19,5 +18,4 @@ runCommand = \case Wasi opts -> Wasi.runCommand opts Anoma opts -> Anoma.runCommand opts Cairo opts -> Cairo.runCommand opts - Vampir opts -> Vampir.runCommand opts RiscZeroRust opts -> RiscZeroRust.runCommand opts diff --git a/app/Commands/Compile/Options.hs b/app/Commands/Compile/Options.hs index da7936f024..2b791c6894 100644 --- a/app/Commands/Compile/Options.hs +++ b/app/Commands/Compile/Options.hs @@ -7,7 +7,6 @@ import Commands.Compile.Anoma.Options import Commands.Compile.Cairo.Options import Commands.Compile.Native.Options import Commands.Compile.RiscZeroRust.Options -import Commands.Compile.Vampir.Options import Commands.Compile.Wasi.Options import Commands.Extra.NewCompile import CommonOptions @@ -16,7 +15,6 @@ import Juvix.Config qualified as Config data CompileCommand = Native (NativeOptions 'InputMain) | Wasi (WasiOptions 'InputMain) - | Vampir (VampirOptions 'InputMain) | Anoma (AnomaOptions 'InputMain) | Cairo (CairoOptions 'InputMain) | RiscZeroRust (RiscZeroRustOptions 'InputMain) @@ -27,8 +25,7 @@ parseCompileCommand = commandTargetsHelper supportedTargets supportedTargets :: [(CompileTarget, Parser CompileCommand)] supportedTargets = - [ (AppTargetVampIR, Vampir <$> parseVampir), - (AppTargetAnoma, Anoma <$> parseAnoma), + [ (AppTargetAnoma, Anoma <$> parseAnoma), (AppTargetCairo, Cairo <$> parseCairo), (AppTargetNative64, Native <$> parseNative) ] diff --git a/app/Commands/Dev/DevCompile.hs b/app/Commands/Dev/DevCompile.hs index 117274b475..6fb6d0e177 100644 --- a/app/Commands/Dev/DevCompile.hs +++ b/app/Commands/Dev/DevCompile.hs @@ -9,6 +9,7 @@ import Commands.Dev.DevCompile.Options import Commands.Dev.DevCompile.Reg qualified as Reg import Commands.Dev.DevCompile.Rust qualified as Rust import Commands.Dev.DevCompile.Tree qualified as Tree +import Commands.Dev.DevCompile.Vampir qualified as Vampir runCommand :: (Members AppEffects r) => DevCompileCommand -> Sem r () runCommand = \case @@ -19,3 +20,4 @@ runCommand = \case Casm opts -> Casm.runCommand opts Rust opts -> Rust.runCommand opts NativeRust opts -> NativeRust.runCommand opts + Vampir opts -> Vampir.runCommand opts diff --git a/app/Commands/Dev/DevCompile/Options.hs b/app/Commands/Dev/DevCompile/Options.hs index 884cd94a46..ad16e2f244 100644 --- a/app/Commands/Dev/DevCompile/Options.hs +++ b/app/Commands/Dev/DevCompile/Options.hs @@ -7,6 +7,7 @@ import Commands.Dev.DevCompile.NativeRust.Options import Commands.Dev.DevCompile.Reg.Options import Commands.Dev.DevCompile.Rust.Options import Commands.Dev.DevCompile.Tree.Options +import Commands.Dev.DevCompile.Vampir.Options import CommonOptions import Juvix.Config qualified as Config @@ -18,6 +19,7 @@ data DevCompileCommand | Casm (CasmOptions 'InputMain) | Rust (RustOptions 'InputMain) | NativeRust (NativeRustOptions 'InputMain) + | Vampir (VampirOptions 'InputMain) deriving stock (Data) parseDevCompileCommand :: Parser DevCompileCommand @@ -28,7 +30,8 @@ parseDevCompileCommand = commandReg, commandTree, commandCasm, - commandAsm + commandAsm, + commandVampir ] <> [commandRust | Config.config ^. Config.configRust] <> [commandNativeRust | Config.config ^. Config.configRust] @@ -82,3 +85,10 @@ commandNativeRust = info (NativeRust <$> parseNativeRust) (progDesc "Compile to native executable through Rust") + +commandVampir :: Mod CommandFields DevCompileCommand +commandVampir = + command "vampir" $ + info + (Vampir <$> parseVampir) + (progDesc "Compile to VampIR") diff --git a/app/Commands/Compile/Vampir.hs b/app/Commands/Dev/DevCompile/Vampir.hs similarity index 89% rename from app/Commands/Compile/Vampir.hs rename to app/Commands/Dev/DevCompile/Vampir.hs index 4a08e45aa6..5855ff8685 100644 --- a/app/Commands/Compile/Vampir.hs +++ b/app/Commands/Dev/DevCompile/Vampir.hs @@ -1,7 +1,7 @@ -module Commands.Compile.Vampir where +module Commands.Dev.DevCompile.Vampir where import Commands.Base -import Commands.Compile.Vampir.Options +import Commands.Dev.DevCompile.Vampir.Options import Commands.Extra.NewCompile import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR diff --git a/app/Commands/Compile/Vampir/Options.hs b/app/Commands/Dev/DevCompile/Vampir/Options.hs similarity index 90% rename from app/Commands/Compile/Vampir/Options.hs rename to app/Commands/Dev/DevCompile/Vampir/Options.hs index 9b18b5b5f1..3645225bd9 100644 --- a/app/Commands/Compile/Vampir/Options.hs +++ b/app/Commands/Dev/DevCompile/Vampir/Options.hs @@ -1,7 +1,7 @@ {-# LANGUAGE UndecidableInstances #-} -module Commands.Compile.Vampir.Options - ( module Commands.Compile.Vampir.Options, +module Commands.Dev.DevCompile.Vampir.Options + ( module Commands.Dev.DevCompile.Vampir.Options, module Commands.Compile.CommonOptions, ) where diff --git a/test/Core/VampIR/Positive.hs b/test/Core/VampIR/Positive.hs index aa9d33f184..025a878c04 100644 --- a/test/Core/VampIR/Positive.hs +++ b/test/Core/VampIR/Positive.hs @@ -15,5 +15,5 @@ toTestDescr = Normalize.toTestDescr' (const (coreVampIRAssertion (toStoredTransf allTests :: TestTree allTests = testGroup - "JuvixCore VampIR positive tests" + "JuvixCore VampIR pipeline positive tests" (map (mkTest . toTestDescr) Normalize.tests) diff --git a/test/Main.hs b/test/Main.hs index e54d98a302..6f7dd375ab 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -25,7 +25,6 @@ import Scope qualified import Termination qualified import Tree qualified import Typecheck qualified -import VampIR qualified slowTests :: IO TestTree slowTests = @@ -42,7 +41,6 @@ slowTests = return Compilation.allTests, return Examples.allTests, Casm.allTests, - VampIR.allTests, return Anoma.allTests, return Repl.allTests ] diff --git a/test/VampIR.hs b/test/VampIR.hs deleted file mode 100644 index 826d584304..0000000000 --- a/test/VampIR.hs +++ /dev/null @@ -1,18 +0,0 @@ -module VampIR where - -import Base -import VampIR.Compilation.Negative qualified as Negative -import VampIR.Compilation.Positive qualified as CompilationPositive -import VampIR.Core.Base -import VampIR.Core.Positive qualified as CorePositive - -allTests :: IO TestTree -allTests = - withPrecondition precondition - . return - $ testGroup - "VampIR tests" - [ CorePositive.allTests, - CompilationPositive.allTests, - Negative.allTests - ] diff --git a/test/VampIR/Compilation/Base.hs b/test/VampIR/Compilation/Base.hs deleted file mode 100644 index f4bbd2328a..0000000000 --- a/test/VampIR/Compilation/Base.hs +++ /dev/null @@ -1,32 +0,0 @@ -module VampIR.Compilation.Base where - -import Base -import Core.VampIR.Base (coreVampIRAssertion') -import Juvix.Compiler.Core -import VampIR.Core.Base (VampirBackend (..), vampirAssertion') - -vampirCompileAssertion :: Path Abs Dir -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion -vampirCompileAssertion root' mainFile dataFile step = do - step "Translate to JuvixCore" - entryPoint <- testDefaultEntryPointIO root' mainFile - PipelineResult {..} <- snd <$> testRunIO entryPoint upToStoredCore - let tab = computeCombinedInfoTable (_pipelineResult ^. coreResultModule) - coreVampIRAssertion' tab toVampIRTransformations mainFile dataFile step - vampirAssertion' entryPoint VampirHalo2 tab dataFile step - -vampirCompileErrorAssertion :: - Path Abs Dir -> - Path Abs File -> - (String -> IO ()) -> - Assertion -vampirCompileErrorAssertion root' mainFile step = do - step "Translate to JuvixCore" - entryPoint <- testDefaultEntryPointIO root' mainFile - r <- testRunIOEither entryPoint upToStoredCore - case r of - Left _ -> return () - Right res -> - let m = snd res ^. pipelineResult . coreResultModule - in case run $ runReader entryPoint $ runError @JuvixError $ toVampIR m of - Left _ -> return () - Right _ -> assertFailure "no error" diff --git a/test/VampIR/Compilation/Negative.hs b/test/VampIR/Compilation/Negative.hs deleted file mode 100644 index d190945479..0000000000 --- a/test/VampIR/Compilation/Negative.hs +++ /dev/null @@ -1,37 +0,0 @@ -module VampIR.Compilation.Negative where - -import Base -import VampIR.Compilation.Base - -data NegTest = NegTest - { _name :: String, - _relDir :: Path Rel Dir, - _file :: Path Rel File - } - -root :: Path Abs Dir -root = relToProject $(mkRelDir "tests/VampIR/negative") - -testDescr :: NegTest -> TestDescr -testDescr NegTest {..} = - let tRoot = root _relDir - file' = tRoot _file - in TestDescr - { _testName = _name, - _testRoot = tRoot, - _testAssertion = Steps $ vampirCompileErrorAssertion tRoot file' - } - -allTests :: TestTree -allTests = - testGroup - "Juvix to VampIR compilation negative tests" - (map (mkTest . testDescr) tests) - -tests :: [NegTest] -tests = - [ NegTest - "Test001: Missing comma" - $(mkRelDir ".") - $(mkRelFile "test001.juvix") - ] diff --git a/test/VampIR/Compilation/Positive.hs b/test/VampIR/Compilation/Positive.hs deleted file mode 100644 index 8543214630..0000000000 --- a/test/VampIR/Compilation/Positive.hs +++ /dev/null @@ -1,162 +0,0 @@ -module VampIR.Compilation.Positive where - -import Base -import VampIR.Compilation.Base - -data PosTest = PosTest - { _name :: String, - _dir :: Path Abs Dir, - _file :: Path Abs File, - _dataFile :: Path Abs File - } - -makeLenses ''PosTest - -fromTest :: PosTest -> TestTree -fromTest = mkTest . toTestDescr - -root :: Path Abs Dir -root = relToProject $(mkRelDir "tests/VampIR/positive/Compilation") - -toTestDescr :: PosTest -> TestDescr -toTestDescr PosTest {..} = - let tRoot = _dir - file' = _file - data' = _dataFile - in TestDescr - { _testName = _name, - _testRoot = tRoot, - _testAssertion = Steps $ vampirCompileAssertion _dir file' data' - } - -allTests :: TestTree -allTests = - testGroup - "Juvix to VampIR compilation positive tests" - (map (mkTest . toTestDescr) tests) - -posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest -posTest _name rdir rfile routfile = - let _dir = root rdir - _file = _dir rfile - _dataFile = root routfile - in PosTest {..} - -tests :: [PosTest] -tests = - [ posTest - "Test001: not function" - $(mkRelDir ".") - $(mkRelFile "test001.juvix") - $(mkRelFile "data/test001.json"), - posTest - "Test002: pattern matching" - $(mkRelDir ".") - $(mkRelFile "test002.juvix") - $(mkRelFile "data/test002.json"), - posTest - "Test003: inductive types" - $(mkRelDir ".") - $(mkRelFile "test003.juvix") - $(mkRelFile "data/test003.json"), - posTest - "Test004: arithmetic" - $(mkRelDir ".") - $(mkRelFile "test004.juvix") - $(mkRelFile "data/test004.json"), - posTest - "Test005: single-constructor inductive types" - $(mkRelDir ".") - $(mkRelFile "test005.juvix") - $(mkRelFile "data/test005.json"), - posTest - "Test006: higher-order inductive types" - $(mkRelDir ".") - $(mkRelFile "test006.juvix") - $(mkRelFile "data/test006.json"), - posTest - "Test007: let" - $(mkRelDir ".") - $(mkRelFile "test007.juvix") - $(mkRelFile "data/test007.json"), - posTest - "Test008: functions returning functions with variable capture" - $(mkRelDir ".") - $(mkRelFile "test008.juvix") - $(mkRelFile "data/test008.json"), - posTest - "Test009: applications with lets and cases in function position" - $(mkRelDir ".") - $(mkRelFile "test009.juvix") - $(mkRelFile "data/test009.json"), - posTest - "Test010: mid-square hashing (unrolled)" - $(mkRelDir ".") - $(mkRelFile "test010.juvix") - $(mkRelFile "data/test010.json"), - posTest - "Test011: recursion" - $(mkRelDir ".") - $(mkRelFile "test011.juvix") - $(mkRelFile "data/test011.json"), - posTest - "Test012: tail recursion" - $(mkRelDir ".") - $(mkRelFile "test012.juvix") - $(mkRelFile "data/test012.json"), - posTest - "Test013: tail recursion: Fibonacci numbers in linear time" - $(mkRelDir ".") - $(mkRelFile "test013.juvix") - $(mkRelFile "data/test013.json"), - posTest - "Test014: recursion through higher-order functions" - $(mkRelDir ".") - $(mkRelFile "test014.juvix") - $(mkRelFile "data/test014.json"), - posTest - "Test015: tail recursion through higher-order functions" - $(mkRelDir ".") - $(mkRelFile "test015.juvix") - $(mkRelFile "data/test015.json"), - posTest - "Test016: higher-order functions" - $(mkRelDir ".") - $(mkRelFile "test016.juvix") - $(mkRelFile "data/test016.json"), - posTest - "Test017: mutual recursion" - $(mkRelDir ".") - $(mkRelFile "test017.juvix") - $(mkRelFile "data/test017.json"), - posTest - "Test018: mid-square hashing" - $(mkRelDir ".") - $(mkRelFile "test018.juvix") - $(mkRelFile "data/test018.json"), - posTest - "Test019: polymorphism" - $(mkRelDir ".") - $(mkRelFile "test019.juvix") - $(mkRelFile "data/test019.json"), - posTest - "Test020: boolean target" - $(mkRelDir ".") - $(mkRelFile "test020.juvix") - $(mkRelFile "data/test020.json"), - posTest - "Test021: fast exponentiation (exponential unrolling)" - $(mkRelDir ".") - $(mkRelFile "test021.juvix") - $(mkRelFile "data/test021.json"), - posTest - "Test022: fast exponentiation" - $(mkRelDir ".") - $(mkRelFile "test022.juvix") - $(mkRelFile "data/test022.json"), - posTest - "Test023: permutative conversions" - $(mkRelDir ".") - $(mkRelFile "test023.juvix") - $(mkRelFile "data/test023.json") - ] diff --git a/test/VampIR/Core/Base.hs b/test/VampIR/Core/Base.hs deleted file mode 100644 index afb73b424a..0000000000 --- a/test/VampIR/Core/Base.hs +++ /dev/null @@ -1,133 +0,0 @@ -module VampIR.Core.Base where - -import Base -import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR -import Juvix.Compiler.Core -import Juvix.Prelude.Pretty -import System.Process qualified as P - -data VampirBackend = VampirHalo2 | VampirPlonk - -vampirAssertion :: VampirBackend -> Path Abs Dir -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion -vampirAssertion backend root mainFile dataFile step = do - step "Parse" - s <- readFile mainFile - case runParserMain mainFile defaultModuleId mempty s of - Left err -> assertFailure (show err) - Right tab -> do - entryPoint <- testDefaultEntryPointIO root mainFile - vampirAssertion' entryPoint backend tab dataFile step - -precondition :: Assertion -precondition = do - assertCmdExists $(mkRelFile "vamp-ir") - -vampirAssertion' :: EntryPoint -> VampirBackend -> InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion -vampirAssertion' entryPoint backend tab dataFile step = do - withTempDir' - ( \dirPath -> do - step "Translate to VampIR" - let vampirFile = dirPath $(mkRelFile "program.pir") - case run (runReader entryPoint (runError @JuvixError (coreToVampIR (moduleFromInfoTable tab)))) of - Left err -> assertFailure (prettyString (fromJuvixError @GenericError err)) - Right VampIR.Result {..} -> do - writeFileEnsureLn vampirFile _resultCode - - vampirSetupArgs backend dirPath step - - step "VampIR compile" - P.callProcess "vamp-ir" (compileArgs vampirFile dirPath backend) - step "VampIR prove" - P.callProcess "vamp-ir" (proveArgs dataFile dirPath backend) - step "VampIR verify" - P.callProcess "vamp-ir" (verifyArgs dirPath backend) - ) - -vampirSetupArgs :: VampirBackend -> Path Abs Dir -> (String -> IO ()) -> Assertion -vampirSetupArgs VampirHalo2 _ _ = return () -vampirSetupArgs VampirPlonk dirPath step = do - step "VampIR setup parameters" - P.callProcess "vamp-ir" setupParamsArgs - where - setupParamsArgs = - [ "-q", - "plonk", - "setup", - "-m", - "9", - "-o", - toFilePath (dirPath $(mkRelFile "params.pp")) - ] - -compileArgs :: Path Abs File -> Path Abs Dir -> VampirBackend -> [String] -compileArgs inputFile dirPath = \case - VampirHalo2 -> - [ "-q", - "halo2", - "compile", - "-s", - toFilePath inputFile, - "-o", - toFilePath (dirPath $(mkRelFile "circuit.halo2")) - ] - VampirPlonk -> - [ "-q", - "plonk", - "compile", - "-u", - toFilePath (dirPath $(mkRelFile "params.pp")), - "-s", - toFilePath inputFile, - "-o", - toFilePath (dirPath $(mkRelFile "circuit.plonk")) - ] - -proveArgs :: Path Abs File -> Path Abs Dir -> VampirBackend -> [String] -proveArgs dataFile dirPath = \case - VampirHalo2 -> - [ "-q", - "halo2", - "prove", - "-c", - toFilePath (dirPath $(mkRelFile "circuit.halo2")), - "-o", - toFilePath (dirPath $(mkRelFile "proof.halo2")), - "-i", - toFilePath dataFile - ] - VampirPlonk -> - [ "-q", - "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 -> VampirBackend -> [String] -verifyArgs dirPath = \case - VampirHalo2 -> - [ "-q", - "halo2", - "verify", - "-c", - toFilePath (dirPath $(mkRelFile "circuit.halo2")), - "-p", - toFilePath (dirPath $(mkRelFile "proof.halo2")) - ] - VampirPlonk -> - [ "-q", - "plonk", - "verify", - "-u", - toFilePath (dirPath $(mkRelFile "params.pp")), - "-c", - toFilePath (dirPath $(mkRelFile "circuit.plonk")), - "-p", - toFilePath (dirPath $(mkRelFile "proof.plonk")) - ] diff --git a/test/VampIR/Core/Positive.hs b/test/VampIR/Core/Positive.hs deleted file mode 100644 index 386c2ef41f..0000000000 --- a/test/VampIR/Core/Positive.hs +++ /dev/null @@ -1,57 +0,0 @@ -module VampIR.Core.Positive where - -import Base -import Core.Normalize.Positive (PosTest (..)) -import Core.Normalize.Positive qualified as Normalize -import VampIR.Core.Base - -fromTest :: PosTest -> TestTree -fromTest = mkTest . toTestDescr - -toTestDescr :: PosTest -> TestDescr -toTestDescr = Normalize.toTestDescr' (vampirAssertion VampirHalo2) - -toPlonkTestDescr :: PosTest -> TestDescr -toPlonkTestDescr = Normalize.toTestDescr' (vampirAssertion VampirPlonk) - -allTests :: TestTree -allTests = - testGroup - "Core to VampIR translation positive tests" - ( map (mkTest . toPlonkTestDescr . (over Normalize.name (++ " (plonk)"))) tests - ++ map - (mkTest . toTestDescr) - ( tests - ++ ( Normalize.filterOutTests - ( -- VampIR stack overflow - [ "Test020: functional queues", - "Test026: letrec" - ] - ++ - -- recursion takes too long - [ "Test014: recursion", - "Test015: tail recursion", - "Test016: tail recursion: Fibonacci numbers in linear time", - "Test017: recursion through higher-order functions", - "Test018: tail recursion through higher-order functions", - "Test022: mutual recursion" - ] - ) - Normalize.tests - ) - ) - ) - -tests :: [PosTest] -tests = - [ PosTest - "Test001" - $(mkRelDir "translation") - $(mkRelFile "test001.jvc") - $(mkRelFile "data/test001.json"), - PosTest - "Test002" - $(mkRelDir "translation") - $(mkRelFile "test002.jvc") - $(mkRelFile "data/test002.json") - ] diff --git a/tests/smoke/Commands/compile.smoke.yaml b/tests/smoke/Commands/compile.smoke.yaml index 71247bcf6d..88aa15868d 100644 --- a/tests/smoke/Commands/compile.smoke.yaml +++ b/tests/smoke/Commands/compile.smoke.yaml @@ -162,34 +162,6 @@ tests: stdin: "[call [L [replace [RL [quote 0]] [@ S]]]]" exit-status: 0 - - name: target-vampir - command: - shell: - - bash - script: | - temp=$(mktemp -d) - trap 'rm -rf -- "$temp"' EXIT - testdir=$PWD/tests/VampIR/positive/Compilation - cd $temp - juvix --log-level error compile vampir $testdir/test001.juvix - grep -q 'VampIR runtime for Juvix (safe version)' test001.pir - stdout: "" - exit-status: 0 - - - name: target-varmpir-unsafe - command: - shell: - - bash - script: | - temp=$(mktemp -d) - trap 'rm -rf -- "$temp"' EXIT - testdir=$PWD/tests/VampIR/positive/Compilation - cd $temp - juvix --log-level error compile vampir $testdir/test001.juvix --unsafe - grep -q 'VampIR runtime for Juvix (unsafe version)' test001.pir - stdout: "" - exit-status: 0 - - name: input-file-does-not-exist command: - juvix