diff --git a/app/Commands/Dev/DevCompile.hs b/app/Commands/Dev/DevCompile.hs index 40f28876ed..dd5da1471d 100644 --- a/app/Commands/Dev/DevCompile.hs +++ b/app/Commands/Dev/DevCompile.hs @@ -4,8 +4,10 @@ import Commands.Base import Commands.Dev.DevCompile.Asm qualified as Asm import Commands.Dev.DevCompile.Casm qualified as Casm import Commands.Dev.DevCompile.Core qualified as Core +import Commands.Dev.DevCompile.NativeRust qualified as NativeRust 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 runCommand :: (Members '[App, EmbedIO, TaggedLock] r) => DevCompileCommand -> Sem r () @@ -15,3 +17,5 @@ runCommand = \case Asm opts -> Asm.runCommand opts Tree opts -> Tree.runCommand opts Casm opts -> Casm.runCommand opts + Rust opts -> Rust.runCommand opts + NativeRust opts -> NativeRust.runCommand opts diff --git a/app/Commands/Dev/DevCompile/NativeRust.hs b/app/Commands/Dev/DevCompile/NativeRust.hs new file mode 100644 index 0000000000..21c126c866 --- /dev/null +++ b/app/Commands/Dev/DevCompile/NativeRust.hs @@ -0,0 +1,75 @@ +module Commands.Dev.DevCompile.NativeRust where + +import Commands.Base +import Commands.Dev.DevCompile.NativeRust.Options +import Commands.Extra.Rust +import Data.ByteString qualified as BS +import Data.FileEmbed qualified as FE +import Juvix.Compiler.Backend.Rust.Data.Result + +runCommand :: + (Members '[App, EmbedIO, TaggedLock] r) => + NativeRustOptions 'InputMain -> + Sem r () +runCommand opts = do + let opts' = opts ^. nativeRustCompileCommonOptions + inputFile = opts' ^. compileInputFile + moutputFile = opts' ^. compileOutputFile + mainFile <- getMainFile inputFile + Result {..} <- runPipeline opts inputFile upToRust + rustFile <- inputRustFile mainFile + writeFileEnsureLn rustFile _resultRustCode + buildDir <- askBuildDir + ensureDir buildDir + prepareRuntime + outputFile <- nativeOutputFile mainFile moutputFile + let args = + RustArgs + { _rustDebug = opts' ^. compileDebug, + _rustInputFile = rustFile, + _rustOutputFile = outputFile, + _rustOptimizationLevel = fmap (min 3 . (+ 1)) (opts' ^. compileOptimizationLevel) + } + rustCompile args + where + prepareRuntime :: + forall s. + (Members '[App, EmbedIO] s) => + Sem s () + prepareRuntime = writeRuntime runtime + where + runtime :: BS.ByteString + runtime + | opts ^. nativeRustCompileCommonOptions . compileDebug = rustDebugRuntime + | otherwise = rustReleaseRuntime + where + rustReleaseRuntime :: BS.ByteString + rustReleaseRuntime = $(FE.makeRelativeToProject "runtime/rust/target/release/libjuvix.rlib" >>= FE.embedFile) + + rustDebugRuntime :: BS.ByteString + rustDebugRuntime = $(FE.makeRelativeToProject "runtime/rust/target/debug/libjuvix.rlib" >>= FE.embedFile) + +inputRustFile :: (Members '[App, EmbedIO] r) => Path Abs File -> Sem r (Path Abs File) +inputRustFile inputFileCompile = do + buildDir <- askBuildDir + ensureDir buildDir + return (buildDir replaceExtension' ".rs" (filename inputFileCompile)) + +nativeOutputFile :: forall r. (Member App r) => Path Abs File -> Maybe (AppPath File) -> Sem r (Path Abs File) +nativeOutputFile inputFile moutputFile = + case moutputFile of + Just f -> fromAppFile f + Nothing -> do + invokeDir <- askInvokeDir + let baseOutputFile = invokeDir filename inputFile + return $ removeExtension' baseOutputFile + +writeRuntime :: + forall r. + (Members '[App, EmbedIO] r) => + BS.ByteString -> + Sem r () +writeRuntime runtime = do + buildDir <- askBuildDir + liftIO $ + BS.writeFile (toFilePath (buildDir $(mkRelFile "libjuvix.rlib"))) runtime diff --git a/app/Commands/Dev/DevCompile/NativeRust/Options.hs b/app/Commands/Dev/DevCompile/NativeRust/Options.hs new file mode 100644 index 0000000000..28598003d3 --- /dev/null +++ b/app/Commands/Dev/DevCompile/NativeRust/Options.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE UndecidableInstances #-} + +module Commands.Dev.DevCompile.NativeRust.Options + ( module Commands.Dev.DevCompile.NativeRust.Options, + module Commands.Compile.CommonOptions, + ) +where + +import Commands.Compile.CommonOptions +import CommonOptions + +data NativeRustOptions (k :: InputKind) = NativeRustOptions + { _nativeRustCompileCommonOptions :: CompileCommonOptions k + } + +deriving stock instance (Typeable k, Data (InputFileType k)) => Data (NativeRustOptions k) + +makeLenses ''NativeRustOptions + +parseNativeRust :: (SingI k) => Parser (NativeRustOptions k) +parseNativeRust = do + _nativeRustCompileCommonOptions <- parseCompileCommonOptions + pure NativeRustOptions {..} + +instance EntryPointOptions (NativeRustOptions k) where + applyOptions opts = + set entryPointTarget (Just TargetRust) + . applyOptions (opts ^. nativeRustCompileCommonOptions) diff --git a/app/Commands/Dev/DevCompile/Options.hs b/app/Commands/Dev/DevCompile/Options.hs index ca3688f6ef..8b24a33abb 100644 --- a/app/Commands/Dev/DevCompile/Options.hs +++ b/app/Commands/Dev/DevCompile/Options.hs @@ -3,7 +3,9 @@ module Commands.Dev.DevCompile.Options where import Commands.Dev.DevCompile.Asm.Options import Commands.Dev.DevCompile.Casm.Options import Commands.Dev.DevCompile.Core.Options +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 CommonOptions @@ -13,6 +15,8 @@ data DevCompileCommand | Reg (RegOptions 'InputMain) | Tree (TreeOptions 'InputMain) | Casm (CasmOptions 'InputMain) + | Rust (RustOptions 'InputMain) + | NativeRust (NativeRustOptions 'InputMain) deriving stock (Data) parseDevCompileCommand :: Parser DevCompileCommand @@ -23,7 +27,9 @@ parseDevCompileCommand = commandReg, commandTree, commandCasm, - commandAsm + commandAsm, + commandRust, + commandNativeRust ] ) @@ -61,3 +67,17 @@ commandAsm = info (Asm <$> parseAsm) (progDesc "Compile to Juvix ASM") + +commandRust :: Mod CommandFields DevCompileCommand +commandRust = + command "rust" $ + info + (Rust <$> parseRust) + (progDesc "Compile to Rust") + +commandNativeRust :: Mod CommandFields DevCompileCommand +commandNativeRust = + command "native-rust" $ + info + (NativeRust <$> parseNativeRust) + (progDesc "Compile to native executable through Rust") diff --git a/app/Commands/Dev/DevCompile/Rust.hs b/app/Commands/Dev/DevCompile/Rust.hs new file mode 100644 index 0000000000..1c27b2210a --- /dev/null +++ b/app/Commands/Dev/DevCompile/Rust.hs @@ -0,0 +1,17 @@ +module Commands.Dev.DevCompile.Rust where + +import Commands.Base +import Commands.Dev.DevCompile.Rust.Options +import Commands.Extra.NewCompile +import Juvix.Compiler.Backend.Rust.Data.Result + +runCommand :: + (Members '[App, EmbedIO, TaggedLock] r) => + RustOptions 'InputMain -> + Sem r () +runCommand opts = do + let inputFile = opts ^. rustCompileCommonOptions . compileInputFile + moutputFile = opts ^. rustCompileCommonOptions . compileOutputFile + outFile :: Path Abs File <- getOutputFile FileExtRust inputFile moutputFile + Result {..} <- runPipeline opts inputFile upToRust + writeFileEnsureLn outFile _resultRustCode diff --git a/app/Commands/Dev/DevCompile/Rust/Options.hs b/app/Commands/Dev/DevCompile/Rust/Options.hs new file mode 100644 index 0000000000..d7712bbda4 --- /dev/null +++ b/app/Commands/Dev/DevCompile/Rust/Options.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE UndecidableInstances #-} + +module Commands.Dev.DevCompile.Rust.Options + ( module Commands.Dev.DevCompile.Rust.Options, + module Commands.Compile.CommonOptions, + ) +where + +import Commands.Compile.CommonOptions +import CommonOptions + +data RustOptions (k :: InputKind) = RustOptions + { _rustCompileCommonOptions :: CompileCommonOptions k + } + +deriving stock instance (Typeable k, Data (InputFileType k)) => Data (RustOptions k) + +makeLenses ''RustOptions + +parseRust :: (SingI k) => Parser (RustOptions k) +parseRust = do + _rustCompileCommonOptions <- parseCompileCommonOptions + pure RustOptions {..} + +instance EntryPointOptions (RustOptions k) where + applyOptions opts = + set entryPointTarget (Just TargetRust) + . applyOptions (opts ^. rustCompileCommonOptions) diff --git a/app/Commands/Extra/Rust.hs b/app/Commands/Extra/Rust.hs new file mode 100644 index 0000000000..bb17664b42 --- /dev/null +++ b/app/Commands/Extra/Rust.hs @@ -0,0 +1,87 @@ +module Commands.Extra.Rust where + +import Commands.Base +import System.Process qualified as P + +data RustArgs = RustArgs + { _rustDebug :: Bool, + _rustInputFile :: Path Abs File, + _rustOutputFile :: Path Abs File, + _rustOptimizationLevel :: Maybe Int + } + +makeLenses ''RustArgs + +rustCompile :: + forall r. + (Members '[App, EmbedIO] r) => + RustArgs -> + Sem r () +rustCompile args = do + getRustcCliArgs args >>= runRustc + +getRustcCliArgs :: (Members '[App, EmbedIO] r) => RustArgs -> Sem r [String] +getRustcCliArgs args = do + buildDir <- askBuildDir + return (nativeArgs buildDir args) + +nativeArgs :: Path Abs Dir -> RustArgs -> [String] +nativeArgs buildDir args@RustArgs {..} = + commonArgs buildDir args ++ extraArgs + where + extraArgs :: [String] + extraArgs = run . execAccumList $ do + addOptimizationOption args + addArg (toFilePath _rustInputFile) + +addOptimizationOption :: (Member (Accum String) r) => RustArgs -> Sem r () +addOptimizationOption args = do + addArg "-C" + addArg $ "opt-level=" <> show (maybe defaultOptLevel (max 1) (args ^. rustOptimizationLevel)) + where + defaultOptLevel :: Int + defaultOptLevel + | args ^. rustDebug = debugRustOptimizationLevel + | otherwise = defaultRustOptimizationLevel + +debugRustOptimizationLevel :: Int +debugRustOptimizationLevel = 1 + +defaultRustOptimizationLevel :: Int +defaultRustOptimizationLevel = 3 + +addArg :: (Member (Accum String) r) => String -> Sem r () +addArg = accum + +commonArgs :: Path Abs Dir -> RustArgs -> [String] +commonArgs buildDir RustArgs {..} = run . execAccumList $ do + when _rustDebug $ do + addArg "-g" + addArg "-C" + addArg "debug-assertions=true" + addArg "-C" + addArg "overflow-checks=true" + addArg "-o" + addArg (toFilePath _rustOutputFile) + addArg ("-L") + addArg (toFilePath buildDir) + +runRustc :: + forall r. + (Members '[App, EmbedIO] r) => + [String] -> + Sem r () +runRustc args = do + cp <- rustcBinPath + (exitCode, _, err) <- liftIO (P.readProcessWithExitCode cp args "") + case exitCode of + ExitSuccess -> return () + _ -> exitFailMsg (pack err) + where + rustcBinPath :: Sem r String + rustcBinPath = do + p <- findExecutable $(mkRelFile "rustc") + maybe (exitFailMsg rustcNotFoundErr) (return . toFilePath) p + + rustcNotFoundErr :: Text + rustcNotFoundErr = "Error: The rustc executable was not found. Please install the Rust compiler" diff --git a/cntlines.sh b/cntlines.sh index bd1e078c68..1fc6e8ab16 100755 --- a/cntlines.sh +++ b/cntlines.sh @@ -17,6 +17,7 @@ RUNTIME_CASM=$(count_ext '*.casm' runtime/casm) RUNTIME=$((RUNTIME_C+RUNTIME_RUST+RUNTIME_VAMPIR+RUNTIME_JVT+RUNTIME_CASM)) BACKENDC=$(count src/Juvix/Compiler/Backend/C/) +BACKENDRUST=$(count src/Juvix/Compiler/Backend/Rust/) CAIRO=$(count src/Juvix/Compiler/Backend/Cairo/) GEB=$(count src/Juvix/Compiler/Backend/Geb/) VAMPIR=$(count src/Juvix/Compiler/Backend/VampIR/) @@ -40,7 +41,7 @@ PRELUDE=$(count src/Juvix/Prelude/) STORE=$(count src/Juvix/Compiler/Store/) FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE)) -BACK=$((BACKENDC + GEB + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO)) +BACK=$((BACKENDC + BACKENDRUST + GEB + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO)) OTHER=$((APP + STORE + HTML + EXTRA + DATA + PRELUDE)) TESTS=$(count test/) @@ -55,6 +56,7 @@ echo "Middle and back end: $BACK LOC" echo " VampIR backend: $VAMPIR LOC" echo " GEB backend: $GEB LOC" echo " C backend: $BACKENDC LOC" +echo " Rust backend: $BACKENDRUST LOC" echo " Cairo backend: $((CASM + CAIRO)) LOC" echo " Nockma backend: $NOCK LOC" echo " JuvixReg: $REG LOC" diff --git a/package.yaml b/package.yaml index b5f01c776a..5ac93c1d9d 100644 --- a/package.yaml +++ b/package.yaml @@ -38,6 +38,7 @@ extra-source-files: - include/package-base/**/*.juvix - runtime/c/include/**/*.h - runtime/c/**/*.a + - runtime/rust/target/**/*.rlib - runtime/tree/*.jvt - runtime/vampir/*.pir - runtime/casm/*.casm diff --git a/runtime/Makefile b/runtime/Makefile index fc99daaab7..07e20e8659 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -10,7 +10,7 @@ juvix_c: .PHONY: juvix_rust juvix_rust: - cd rust && cargo build --release + cd rust && cargo build && cargo build --release .PHONY: clean clean: diff --git a/runtime/rust/src/apply.rs b/runtime/rust/src/apply.rs index e367550ee2..d18c17a3cf 100644 --- a/runtime/rust/src/apply.rs +++ b/runtime/rust/src/apply.rs @@ -29,11 +29,11 @@ impl Memory { #[macro_export] macro_rules! tapply { - ($lab:lifetime, $program:ident, $mem:ident, $fid:ident, $args:ident, $cl0:expr, $cargs0:expr) => { + ($lab:lifetime, $program:ident, $mem:ident, $fid:ident, $args:ident, $cl0:expr, $cargs0:expr) => {{ let mut cl = $cl0; let mut cargs = $cargs0; loop { - match $mem.apply( cl, &cargs) { + match $mem.apply(cl, &cargs) { apply::AppResult::Call(fid1, args1) => { $fid = fid1; $args = args1; @@ -46,7 +46,7 @@ macro_rules! tapply { } } } - }; + }} } #[macro_export] diff --git a/runtime/rust/src/closure.rs b/runtime/rust/src/closure.rs index 328132afbe..4d2ff20a2f 100644 --- a/runtime/rust/src/closure.rs +++ b/runtime/rust/src/closure.rs @@ -30,8 +30,8 @@ impl Memory { p } - // Assigns stored closure args plus the provided closure args (`cargs`) to the - // argument space (`args`). Returns the function id to call. + // Returns the function id to call and the full arguments for closure call: + // stored closure args plus the provided closure args (`cargs`). pub fn call_closure(self: &Memory, cl: Word, cargs: &[Word]) -> (Word, Vec) { let mut args = Vec::from(self.get_closure_args(cl)); args.extend(cargs); diff --git a/runtime/rust/src/defs.rs b/runtime/rust/src/defs.rs index f6d8ded99c..ca1d475c63 100644 --- a/runtime/rust/src/defs.rs +++ b/runtime/rust/src/defs.rs @@ -12,6 +12,11 @@ pub type SmallInt = i32; pub const INITIAL_STACK_CAPACITY: usize = 10 * 1024; pub const INITIAL_MEMORY_CAPACITY: usize = 10 * 1024; +pub const BOOL_FALSE: Word = 0; +pub const BOOL_TRUE: Word = 1; +pub const OBJ_UNIT: Word = 0; +pub const OBJ_VOID: Word = 0; + pub fn word_to_usize(s: Word) -> usize { s as usize } diff --git a/runtime/rust/src/equality.rs b/runtime/rust/src/equality.rs index cce7c53fc3..7986feb99f 100644 --- a/runtime/rust/src/equality.rs +++ b/runtime/rust/src/equality.rs @@ -4,6 +4,6 @@ use super::defs::*; // Check for equality. The implementation is incorrect for complex objects, but // complex objects are not compared in Juvix with built-in equality for now. -pub fn juvix_equal(x: Word, y: Word) -> bool { - x == y +pub fn juvix_equal(x: Word, y: Word) -> Word { + bool_to_word(x == y) } diff --git a/runtime/rust/src/lib.rs b/runtime/rust/src/lib.rs index 40e8753ffc..f1222f11c3 100644 --- a/runtime/rust/src/lib.rs +++ b/runtime/rust/src/lib.rs @@ -49,7 +49,7 @@ mod tests { continue; } FUN_ITFIB_GO => { - if juvix_equal(args[0], make_smallint(0)) { + if word_to_bool(juvix_equal(args[0], make_smallint(0))) { break args[1]; } else { args = vec![ @@ -122,19 +122,19 @@ mod tests { vec![id, id, id, id, id, id, id, id, id, id, id, make_smallint(1)] ); let tmp1 = smallint_add(x, y); - break smallint_add(tmp1, z); + return smallint_add(tmp1, z); } FUN_S => { let xz = apply!(program_sk, mem, args[0], vec![args[2]]); let yz = apply!(program_sk, mem, args[1], vec![args[2]]); - tapply!('program, program_sk, mem, fid, args, xz, vec![yz]); + tapply!('program, program_sk, mem, fid, args, xz, vec![yz]) } FUN_K => { - break args[0]; + return args[0]; } FUN_I => { let k = mem.alloc_closure(FUN_K, &[], 2); - break mem.alloc_closure(FUN_S, &[k, k], 1); + return mem.alloc_closure(FUN_S, &[k, k], 1); } _ => panic!("unknown function id"), } diff --git a/src/Juvix/Compiler/Backend.hs b/src/Juvix/Compiler/Backend.hs index 94d92c268a..dfc6c4be20 100644 --- a/src/Juvix/Compiler/Backend.hs +++ b/src/Juvix/Compiler/Backend.hs @@ -12,6 +12,7 @@ data Target | TargetAsm | TargetReg | TargetTree + | TargetRust | TargetAnoma | TargetCairo deriving stock (Data, Eq, Show) @@ -110,6 +111,21 @@ getLimits tgt debug = case tgt of _limitsBuiltinUIDsNum = 8, _limitsSpecialisedApply = 3 } + TargetRust -> + Limits + { _limitsMaxConstrs = fromIntegral (maxBound :: Int32), + _limitsMaxConstrArgs = fromIntegral (maxBound :: Int32), + _limitsMaxFunctionArgs = fromIntegral (maxBound :: Int32), + _limitsMaxLocalVars = 2048, + _limitsMaxClosureSize = fromIntegral (maxBound :: Int32), + _limitsClosureHeadSize = 3, + _limitsMaxStringSize = 0, + _limitsMaxStackDelta = 0, + _limitsMaxFunctionAlloc = 0, + _limitsDispatchStackSize = 0, + _limitsBuiltinUIDsNum = 0, + _limitsSpecialisedApply = 0 + } defaultLimits :: Limits defaultLimits = diff --git a/src/Juvix/Compiler/Backend/Rust/Data/Result.hs b/src/Juvix/Compiler/Backend/Rust/Data/Result.hs new file mode 100644 index 0000000000..377119db5d --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Data/Result.hs @@ -0,0 +1,9 @@ +module Juvix.Compiler.Backend.Rust.Data.Result where + +import Juvix.Prelude + +newtype Result = Result + { _resultRustCode :: Text + } + +makeLenses ''Result diff --git a/src/Juvix/Compiler/Backend/Rust/Language.hs b/src/Juvix/Compiler/Backend/Rust/Language.hs new file mode 100644 index 0000000000..12fa287508 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Language.hs @@ -0,0 +1,135 @@ +module Juvix.Compiler.Backend.Rust.Language where + +import Juvix.Prelude + +data Program = Program + { _programFunctions :: [Function] + } + +data Type + = Word + | VecOfWord + | Memory + +data IsMut + = Mut + | NotMut + +data FunctionArgument = FunctionArgument + { _functionArgumentMutable :: IsMut, + _functionArgumentName :: Text, + _functionArgumentType :: Type + } + +data Function = Function + { _functionName :: Text, + _functionArguments :: [FunctionArgument], + _functionReturnType :: Maybe Type, + _functionBody :: [Statement], + _functionAttributes :: Maybe Text + } + +data Statement + = StatementLet Let + | StatementConst ConstDecl + | StatementAssignment Assignment + | StatementIf If + | StatementMatch Match + | StatementLoop Loop + | StatementContinue + | StatementReturn Return + | StatementExpression Expression + +data Let = Let + { _letVariable :: Text, + _letType :: Maybe Type, + _letMutable :: IsMut, + _letInitializer :: Maybe Expression + } + +data ConstDecl = ConstDecl + { _constVariable :: Text, + _constType :: Type, + _constValue :: Expression + } + +data Assignment = Assignment + { _assignmentVariable :: Text, + _assignmentValue :: Expression + } + +data If = If + { _ifValue :: Expression, + _ifBranchTrue :: [Statement], + _ifBranchFalse :: [Statement] + } + +data MatchBranch = MatchBranch + { -- Nothing indicates the wildcard + _matchBranchPattern :: Maybe Expression, + _matchBranchBody :: [Statement] + } + +data Match = Match + { _matchValue :: Expression, + _matchBranches :: [MatchBranch] + } + +data Loop = Loop + { _loopLabel :: Maybe Text, + _loopBody :: [Statement] + } + +data Return = Return + { _returnValue :: Maybe Expression + } + +data Expression + = ExprVar Var + | ExprCall Call + | ExprVec Vec + | ExprArray Array + | ExprLiteral Literal + | ExprBlock Block + | ExprVerbatim Text + +data Var = Var + { _varName :: Text + } + +data Call = Call + { _callFunction :: Text, + _callArgs :: [Expression] + } + +data Vec = Vec + { _vecArgs :: [Expression] + } + +data Array = Array + { _arrayArgs :: [Expression] + } + +data Block = Block + { _blockBody :: [Statement] + } + +data Literal + = LitInteger Integer + | LitString Text + +makeLenses ''FunctionArgument +makeLenses ''Function +makeLenses ''Let +makeLenses ''ConstDecl +makeLenses ''Assignment +makeLenses ''MatchBranch +makeLenses ''Match +makeLenses ''Loop +makeLenses ''Return +makeLenses ''Var +makeLenses ''Call +makeLenses ''Vec +makeLenses ''Array +makeLenses ''Block +makeLenses ''Program diff --git a/src/Juvix/Compiler/Backend/Rust/Pretty.hs b/src/Juvix/Compiler/Backend/Rust/Pretty.hs new file mode 100644 index 0000000000..660d69fafa --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Pretty.hs @@ -0,0 +1,28 @@ +module Juvix.Compiler.Backend.Rust.Pretty + ( module Juvix.Compiler.Backend.Rust.Pretty, + module Juvix.Compiler.Backend.Rust.Pretty.Base, + module Juvix.Compiler.Backend.Rust.Pretty.Options, + module Juvix.Data.PPOutput, + ) +where + +import Juvix.Compiler.Backend.Rust.Pretty.Base +import Juvix.Compiler.Backend.Rust.Pretty.Options +import Juvix.Data.PPOutput +import Juvix.Prelude +import Prettyprinter.Render.Terminal qualified as Ansi + +ppOutDefault :: (PrettyCode c) => c -> AnsiText +ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions + +ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText +ppOut o = mkAnsiText . 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 diff --git a/src/Juvix/Compiler/Backend/Rust/Pretty/Base.hs b/src/Juvix/Compiler/Backend/Rust/Pretty/Base.hs new file mode 100644 index 0000000000..5ff4ff1baf --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Pretty/Base.hs @@ -0,0 +1,190 @@ +module Juvix.Compiler.Backend.Rust.Pretty.Base where + +import Juvix.Compiler.Backend.Rust.Language +import Juvix.Compiler.Backend.Rust.Pretty.Keywords +import Juvix.Compiler.Backend.Rust.Pretty.Options +import Juvix.Data.CodeAnn +import Juvix.Prelude + +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 + +ampersand :: Doc Ann +ampersand = "&" + +hashsym :: Doc Ann +hashsym = "#" + +ppName :: NameKind -> Text -> Sem r (Doc Ann) +ppName k n = return $ annotate (AnnKind k) (pretty n) + +ppMut :: IsMut -> Sem r (Maybe (Doc Ann)) +ppMut = \case + Mut -> return $ Just kwMut + NotMut -> return Nothing + +ppAttrs :: Maybe Text -> Sem r (Doc Ann) +ppAttrs = \case + Just attrs -> return $ hashsym <> brackets (pretty attrs) <> line + Nothing -> return mempty + +ppBlock :: (Member (Reader Options) r) => [Statement] -> Sem r (Doc Ann) +ppBlock stmts = do + stmts' <- mapM ppCode stmts + let stmts'' = punctuate semi stmts' + return $ oneLineOrNextBraces (vsep stmts'') + +instance PrettyCode Type where + ppCode = \case + Word -> return kwWord + VecOfWord -> return $ kwVector <> angles kwWord + Memory -> return $ ampersand <> kwMut <+> kwMemory + +instance PrettyCode FunctionArgument where + ppCode FunctionArgument {..} = do + ty <- ppCode _functionArgumentType + n <- ppName KNameLocal _functionArgumentName + mut <- ppMut _functionArgumentMutable + return $ mut n <> colon <+> ty + +instance PrettyCode Function where + ppCode Function {..} = do + attrs <- ppAttrs _functionAttributes + name <- ppName KNameFunction _functionName + args <- mapM ppCode _functionArguments + rty <- maybe (return Nothing) (ppCode >=> return . Just . ("->" <+>)) _functionReturnType + body <- ppBlock _functionBody + let args' = punctuate comma args + return $ attrs <> kwFn <+> name <> parens (hsep args') <+> rty body <> line + +instance PrettyCode Statement where + ppCode = \case + StatementLet x -> ppCode x + StatementConst x -> ppCode x + StatementAssignment x -> ppCode x + StatementIf x -> ppCode x + StatementMatch x -> ppCode x + StatementLoop x -> ppCode x + StatementContinue -> return kwContinue + StatementReturn x -> ppCode x + StatementExpression x -> ppCode x + +instance PrettyCode Let where + ppCode Let {..} = do + name <- ppName KNameLocal _letVariable + ty <- maybe (return Nothing) (ppCode >=> return . Just) _letType + mut <- ppMut _letMutable + ini <- maybe (return Nothing) (ppCode >=> return . Just) _letInitializer + let ini' = fmap ("=" <+>) ini + ty' = fmap (colon <+>) ty + return $ kwLet <+> mut (name <>? ty' <+?> ini') + +instance PrettyCode ConstDecl where + ppCode ConstDecl {..} = do + name <- ppName KNameLocal _constVariable + ty <- ppCode _constType + val <- ppCode _constValue + return $ kwConst <+> name <> colon <+> ty <+> "=" <+> val + +instance PrettyCode Assignment where + ppCode Assignment {..} = do + name <- ppName KNameLocal _assignmentVariable + val <- ppCode _assignmentValue + return $ name <+> "=" <+> val + +instance PrettyCode If where + ppCode If {..} = do + val <- ppCode _ifValue + br1 <- ppBlock _ifBranchTrue + br2 <- ppBlock _ifBranchFalse + return $ kwIf <+> val <+> br1 <+> kwElse <+> br2 + +instance PrettyCode MatchBranch where + ppCode MatchBranch {..} = do + pat <- case _matchBranchPattern of + Just p -> ppCode p + Nothing -> return "_" + body <- ppBlock _matchBranchBody + return $ pat <+> "=>" <+> body + +instance PrettyCode Match where + ppCode Match {..} = do + val <- ppCode _matchValue + brs <- mapM ppCode _matchBranches + return $ kwMatch <+> val <+> oneLineOrNextBraces (vsep brs) + +instance PrettyCode Loop where + ppCode Loop {..} = do + let lab = fmap ((<> colon) . pretty) _loopLabel + body <- ppBlock _loopBody + return $ lab kwLoop <+> body + +instance PrettyCode Return where + ppCode Return {..} = do + val <- maybe (return Nothing) (ppCode >=> return . Just) _returnValue + return $ kwReturn <+?> val + +instance PrettyCode Expression where + ppCode = \case + ExprVar x -> ppCode x + ExprCall x -> ppCode x + ExprVec x -> ppCode x + ExprArray x -> ppCode x + ExprLiteral x -> ppCode x + ExprBlock x -> ppCode x + ExprVerbatim x -> return $ pretty x + +instance PrettyCode Var where + ppCode Var {..} = ppName KNameLocal _varName + +instance PrettyCode Call where + ppCode Call {..} = do + name <- ppName KNameFunction _callFunction + args <- mapM ppCode _callArgs + return $ name <> parens (hsep (punctuate comma args)) + +instance PrettyCode Vec where + ppCode Vec {..} = do + args <- mapM ppCode _vecArgs + return $ kwVec <> brackets (hsep (punctuate comma args)) + +instance PrettyCode Array where + ppCode Array {..} = do + args <- mapM ppCode _arrayArgs + return $ ampersand <> brackets (hsep (punctuate comma args)) + +instance PrettyCode Literal where + ppCode = \case + LitInteger i -> return $ annotate AnnLiteralInteger (pretty i) + LitString s -> return $ annotate AnnLiteralString (show s) + +instance PrettyCode Block where + ppCode Block {..} = ppBlock _blockBody + +instance PrettyCode Program where + ppCode Program {..} = do + funs <- mapM ppCode _programFunctions + return $ pretty prelude <> line <> vsep funs + where + prelude :: Text + prelude = + "extern crate juvix;\n\ + \\n\ + \#[allow(unused_imports)]\n\ + \use juvix::defs::*;\n\ + \#[allow(unused_imports)]\n\ + \use juvix::apply;\n\ + \#[allow(unused_imports)]\n\ + \use juvix::tapply;\n\ + \#[allow(unused_imports)]\n\ + \use juvix::equality::*;\n\ + \#[allow(unused_imports)]\n\ + \use juvix::integer::*;\n\ + \#[allow(unused_imports)]\n\ + \use juvix::memory::*;\n" diff --git a/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs b/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs new file mode 100644 index 0000000000..2a308704df --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Pretty/Keywords.hs @@ -0,0 +1,43 @@ +module Juvix.Compiler.Backend.Rust.Pretty.Keywords where + +import Juvix.Data.CodeAnn +import Juvix.Extra.Strings qualified as Str + +kwFn :: Doc Ann +kwFn = keyword Str.rustFn + +kwIf :: Doc Ann +kwIf = keyword Str.rustIf + +kwElse :: Doc Ann +kwElse = keyword Str.rustElse + +kwMatch :: Doc Ann +kwMatch = keyword Str.rustMatch + +kwLoop :: Doc Ann +kwLoop = keyword Str.rustLoop + +kwConst :: Doc Ann +kwConst = keyword Str.rustConst + +kwMut :: Doc Ann +kwMut = keyword Str.rustMut + +kwVec :: Doc Ann +kwVec = keyword Str.rustVec + +kwVector :: Doc Ann +kwVector = keyword Str.rustVector + +kwWord :: Doc Ann +kwWord = keyword Str.rustWord + +kwMemory :: Doc Ann +kwMemory = keyword Str.rustMemory + +kwContinue :: Doc Ann +kwContinue = keyword Str.rustContinue + +kwReturn :: Doc Ann +kwReturn = keyword Str.rustReturn diff --git a/src/Juvix/Compiler/Backend/Rust/Pretty/Options.hs b/src/Juvix/Compiler/Backend/Rust/Pretty/Options.hs new file mode 100644 index 0000000000..784671f852 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Pretty/Options.hs @@ -0,0 +1,21 @@ +module Juvix.Compiler.Backend.Rust.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 diff --git a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs new file mode 100644 index 0000000000..39b67471ab --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg.hs @@ -0,0 +1,396 @@ +module Juvix.Compiler.Backend.Rust.Translation.FromReg + ( module Juvix.Compiler.Backend.Rust.Translation.FromReg, + module Juvix.Compiler.Backend.Rust.Data.Result, + ) +where + +import Data.HashMap.Strict qualified as HashMap +import Juvix.Compiler.Backend +import Juvix.Compiler.Backend.Rust.Data.Result +import Juvix.Compiler.Backend.Rust.Data.Result as Rust +import Juvix.Compiler.Backend.Rust.Language as Rust +import Juvix.Compiler.Backend.Rust.Pretty as Rust +import Juvix.Compiler.Backend.Rust.Translation.FromReg.Base +import Juvix.Compiler.Reg.Data.InfoTable qualified as Reg +import Juvix.Compiler.Reg.Extra.Info qualified as Reg +import Juvix.Compiler.Reg.Language qualified as Reg +import Juvix.Prelude + +fromReg :: Limits -> Reg.InfoTable -> Rust.Result +fromReg lims tab = + Rust.Result $ Rust.ppPrint $ Program [programFunction, mainFunction] + where + info :: Reg.ExtraInfo + info = Reg.computeExtraInfo lims tab + + mainFunid :: Int + mainFunid = getFUID info $ fromJust $ tab ^. Reg.infoMainFunction + + mainFunction :: Function + mainFunction = + Function + { _functionName = "main", + _functionAttributes = Nothing, + _functionArguments = [], + _functionReturnType = Nothing, + _functionBody = + [ stmtLet NotMut "result" (mkCall "program" [ExprVerbatim "&mut Memory::new()", mkInteger mainFunid, mkVec []]), + StatementExpression (mkCall "println!" [mkString "{}", mkVar "result"]), + StatementReturn (Return Nothing) + ] + } + + programFunction :: Function + programFunction = + Function + { _functionName = "program", + _functionAttributes = Just "allow(unused_mut, unused)", + _functionArguments = + [ FunctionArgument NotMut "mem" Memory, + FunctionArgument Mut "funid" Word, + FunctionArgument Mut "args" VecOfWord + ], + _functionReturnType = Just Word, + _functionBody = programBody + } + + programBody :: [Statement] + programBody = funConstDecls ++ juvixFunctions + + funConstDecls :: [Statement] + funConstDecls = map mkFunConstDecl funs + where + mkFunConstDecl :: Reg.FunctionInfo -> Statement + mkFunConstDecl funInfo = + StatementConst $ + ConstDecl + { _constVariable = getFunctionIdent info (funInfo ^. Reg.functionSymbol), + _constType = Word, + _constValue = mkInteger (getFUID info (funInfo ^. Reg.functionSymbol)) + } + + juvixFunctions :: [Statement] + juvixFunctions = + [ StatementLoop $ + Loop + { _loopLabel = Just "'program", + _loopBody = + [ StatementMatch $ + Match + { _matchValue = mkVar "funid", + _matchBranches = map (fromRegFunction info) funs ++ [errBranch] + } + ] + } + ] + where + errBranch = + MatchBranch + { _matchBranchPattern = Nothing, + _matchBranchBody = [StatementExpression $ mkCall "panic!" [mkString "unknown function"]] + } + + funs :: [Reg.FunctionInfo] + funs = HashMap.elems (tab ^. Reg.infoFunctions) + +fromRegFunction :: Reg.ExtraInfo -> Reg.FunctionInfo -> MatchBranch +fromRegFunction info funInfo = + MatchBranch + { _matchBranchPattern = Just $ mkVar $ getFunctionIdent info (funInfo ^. Reg.functionSymbol), + _matchBranchBody = varDecls ++ fromRegCode info (funInfo ^. Reg.functionCode) + } + where + varsNum :: Int + varsNum = getLocalVarsNum info (funInfo ^. Reg.functionSymbol) + + varDecls :: [Statement] + varDecls = map (\n -> stmtDecl Mut ("var_" <> show n) Word) [0 .. varsNum - 1] + +fromRegCode :: Reg.ExtraInfo -> Reg.Code -> [Statement] +fromRegCode info = concatMap (fromRegInstr info) + +fromRegInstr :: Reg.ExtraInfo -> Reg.Instruction -> [Statement] +fromRegInstr info = \case + Reg.Nop -> + [] + Reg.Binop x -> + [fromBinaryOp x] + Reg.Unop x -> + [fromUnaryOp x] + Reg.Cairo {} -> + unsupported "Cairo builtin" + Reg.Assign Reg.InstrAssign {..} -> + stmtsAssign (mkVarRef _instrAssignResult) (fromValue _instrAssignValue) + Reg.Trace {} -> + unsupported "trace" + Reg.Dump -> + unsupported "dump" + Reg.Failure {} -> + unsupported "fail" + Reg.Prealloc {} -> + [] + Reg.Alloc x -> + fromAlloc x + Reg.AllocClosure x -> + fromAllocClosure x + Reg.ExtendClosure x -> + fromExtendClosure x + Reg.TailCall x -> + fromTailCall x + Reg.Call x -> + fromCall x + Reg.TailCallClosures x -> + fromTailCallClosures x + Reg.CallClosures x -> + fromCallClosures x + Reg.Return x -> + fromReturn x + Reg.Branch x -> + fromBranch x + Reg.Case x -> + fromCase x + Reg.Block Reg.InstrBlock {..} -> + fromRegCode info _instrBlockCode + where + unsupported :: Text -> a + unsupported x = error ("unsupported: " <> x) + + fromBinaryOp :: Reg.InstrBinop -> Statement + fromBinaryOp Reg.InstrBinop {..} = + stmtAssign + (mkVarRef _instrBinopResult) + ( mkCall + (getBinaryOpName _instrBinopOpcode) + [fromValue _instrBinopArg1, fromValue _instrBinopArg2] + ) + + getBinaryOpName :: Reg.BinaryOp -> Text + getBinaryOpName = \case + Reg.OpIntAdd -> "smallint_add" + Reg.OpIntSub -> "smallint_sub" + Reg.OpIntMul -> "smallint_mul" + Reg.OpIntDiv -> "smallint_div" + Reg.OpIntMod -> "smallint_mod" + Reg.OpIntLt -> "smallint_lt" + Reg.OpIntLe -> "smallint_le" + Reg.OpEq -> "juvix_equal" + Reg.OpStrConcat -> unsupported "strings" + Reg.OpFieldAdd -> unsupported "field type" + Reg.OpFieldSub -> unsupported "field type" + Reg.OpFieldMul -> unsupported "field type" + Reg.OpFieldDiv -> unsupported "field type" + + fromUnaryOp :: Reg.InstrUnop -> Statement + fromUnaryOp Reg.InstrUnop {..} = case _instrUnopOpcode of + Reg.OpShow -> unsupported "strings" + Reg.OpStrToInt -> unsupported "strings" + Reg.OpArgsNum -> + stmtAssign + (mkVarRef _instrUnopResult) + (mkCall "mem.get_closure_largs" [fromValue _instrUnopArg]) + Reg.OpFieldToInt -> unsupported "field type" + Reg.OpIntToField -> unsupported "field type" + + mkVarRef :: Reg.VarRef -> Text + mkVarRef Reg.VarRef {..} = case _varRefGroup of + Reg.VarGroupArgs -> "args[" <> show _varRefIndex <> "]" + Reg.VarGroupLocal -> "var_" <> show _varRefIndex + + fromVarRef :: Reg.VarRef -> Expression + fromVarRef = mkVar . mkVarRef + + fromValue :: Reg.Value -> Expression + fromValue = \case + Reg.ValConst c -> fromConst c + Reg.CRef Reg.ConstrField {..} -> + case _constrFieldMemRep of + Reg.MemRepConstr -> + mkCall + "mem.get_constr_arg" + [fromVarRef _constrFieldRef, mkInteger _constrFieldIndex] + Reg.MemRepTag -> + unsupported "MemRepTag" + Reg.MemRepTuple -> + unsupported "MemRepTuple" + Reg.MemRepUnit -> + unsupported "MemRepUnit" + Reg.MemRepUnpacked {} -> + fromVarRef _constrFieldRef + Reg.VRef x -> fromVarRef x + + fromConst :: Reg.Constant -> Expression + fromConst = \case + Reg.ConstInt x -> mkCall "make_smallint" [mkInteger x] + Reg.ConstField {} -> impossible + Reg.ConstBool True -> mkVar "BOOL_TRUE" + Reg.ConstBool False -> mkVar "BOOL_FALSE" + Reg.ConstString {} -> unsupported "strings" + Reg.ConstUnit -> mkVar "OBJ_UNIT" + Reg.ConstVoid -> mkVar "OBJ_VOID" + + fromAlloc :: Reg.InstrAlloc -> [Statement] + fromAlloc Reg.InstrAlloc {..} = + case _instrAllocMemRep of + Reg.MemRepConstr -> + stmtsAssign + (mkVarRef _instrAllocResult) + ( mkCall + "mem.alloc_constr" + [ mkInteger (getUID info _instrAllocTag), + mkArray (map fromValue _instrAllocArgs) + ] + ) + Reg.MemRepTag -> + unsupported "MemRepTag" + Reg.MemRepTuple -> + unsupported "MemRepTuple" + Reg.MemRepUnit -> + unsupported "MemRepUnit" + Reg.MemRepUnpacked {} -> + unsupported "MemRepUnpacked" + + fromAllocClosure :: Reg.InstrAllocClosure -> [Statement] + fromAllocClosure Reg.InstrAllocClosure {..} = + stmtsAssign + (mkVarRef _instrAllocClosureResult) + ( mkCall + "mem.alloc_closure" + [ mkVar (getFunctionIdent info _instrAllocClosureSymbol), + mkArray (map fromValue _instrAllocClosureArgs), + mkInteger (_instrAllocClosureExpectedArgsNum - length _instrAllocClosureArgs) + ] + ) + + fromExtendClosure :: Reg.InstrExtendClosure -> [Statement] + fromExtendClosure Reg.InstrExtendClosure {..} = + stmtsAssign + (mkVarRef _instrExtendClosureResult) + ( mkCall + "mem.extend_closure" + [ fromVarRef _instrExtendClosureValue, + mkArray (map fromValue _instrExtendClosureArgs) + ] + ) + + fromCall :: Reg.InstrCall -> [Statement] + fromCall Reg.InstrCall {..} = + case _instrCallType of + Reg.CallFun sym -> + stmtsAssign + (mkVarRef _instrCallResult) + ( mkCall + "program" + [mkVar "mem", mkVar (getFunctionIdent info sym), mkVec (map fromValue _instrCallArgs)] + ) + Reg.CallClosure vr -> + stmtsBlock + [ stmtLet Mut "cargs" (mkVec (map fromValue _instrCallArgs)), + stmtLet NotMut "(cfunid, args)" (mkCall "mem.call_closure" [fromVarRef vr, mkVar "&cargs"]), + stmtAssign + (mkVarRef _instrCallResult) + ( mkCall + "program" + [mkVar "mem", mkVar "cfunid", mkVar "args"] + ) + ] + + fromTailCall :: Reg.InstrTailCall -> [Statement] + fromTailCall Reg.InstrTailCall {..} = + case _instrTailCallType of + Reg.CallFun sym -> + [ stmtAssign "args" (mkVec (map fromValue _instrTailCallArgs)), + stmtAssign "funid" (mkVar (getFunctionIdent info sym)), + StatementContinue + ] + Reg.CallClosure vr -> + [ stmtAssign + "funid" + ( mkCall + "mem.call_closure" + [fromVarRef vr, mkArray ((map fromValue _instrTailCallArgs))] + ), + StatementContinue + ] + + fromCallClosures :: Reg.InstrCallClosures -> [Statement] + fromCallClosures Reg.InstrCallClosures {..} = + stmtsAssign + (mkVarRef _instrCallClosuresResult) + ( mkCall + "apply!" + [ mkVar "program", + mkVar "mem", + fromVarRef _instrCallClosuresValue, + mkVec (map fromValue _instrCallClosuresArgs) + ] + ) + + fromTailCallClosures :: Reg.InstrTailCallClosures -> [Statement] + fromTailCallClosures Reg.InstrTailCallClosures {..} = + [ StatementExpression $ + mkCall + "tapply!" + [ mkVar "'program", + mkVar "program", + mkVar "mem", + mkVar "funid", + mkVar "args", + fromVarRef _instrTailCallClosuresValue, + mkVec (map fromValue _instrTailCallClosuresArgs) + ] + ] + + fromBranch :: Reg.InstrBranch -> [Statement] + fromBranch Reg.InstrBranch {..} = + stmtsIf (mkCall "word_to_bool" [fromValue _instrBranchValue]) br1 br2 + where + br1 = fromRegCode info _instrBranchTrue + br2 = fromRegCode info _instrBranchFalse + + fromCase :: Reg.InstrCase -> [Statement] + fromCase Reg.InstrCase {..} = do + case _instrCaseIndRep of + Reg.IndRepStandard -> + [ StatementMatch $ + Match + { _matchValue = mkCall "mem.get_constr_tag" [fromValue _instrCaseValue], + _matchBranches = brs' + } + ] + Reg.IndRepEnum -> + error "unsupported constructor representation" + Reg.IndRepEnumRecord -> + error "unsupported constructor representation" + Reg.IndRepEnumMaybe {} -> + error "unsupported constructor representation" + Reg.IndRepRecord -> + error "unsupported constructor representation" + Reg.IndRepUnit -> + error "unsupported constructor representation" + Reg.IndRepNewtype {} -> + error "unsupported constructor representation" + Reg.IndRepMixed -> + error "unsupported constructor representation" + where + brs = map fromCaseBranch _instrCaseBranches + def = case _instrCaseDefault of + Nothing -> Nothing + Just c -> Just $ fromRegCode info c + brs' = + brs + ++ [ MatchBranch + { _matchBranchPattern = Nothing, + _matchBranchBody = fromMaybe [StatementExpression $ mkCall "panic!" [mkString "match failure"]] def + } + ] + + fromCaseBranch :: Reg.CaseBranch -> MatchBranch + fromCaseBranch Reg.CaseBranch {..} = + MatchBranch + { _matchBranchPattern = Just $ mkInteger (getUID info _caseBranchTag), + _matchBranchBody = fromRegCode info _caseBranchCode + } + + fromReturn :: Reg.InstrReturn -> [Statement] + fromReturn Reg.InstrReturn {..} = + [StatementReturn $ Return $ Just $ fromValue _instrReturnValue] diff --git a/src/Juvix/Compiler/Backend/Rust/Translation/FromReg/Base.hs b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg/Base.hs new file mode 100644 index 0000000000..7adcf6ad97 --- /dev/null +++ b/src/Juvix/Compiler/Backend/Rust/Translation/FromReg/Base.hs @@ -0,0 +1,100 @@ +module Juvix.Compiler.Backend.Rust.Translation.FromReg.Base where + +import Data.HashMap.Strict qualified as HashMap +import Data.Text qualified as T +import Juvix.Compiler.Backend.Rust.Language +import Juvix.Compiler.Reg.Data.InfoTable qualified as Reg +import Juvix.Compiler.Reg.Extra.Info qualified as Reg +import Juvix.Compiler.Reg.Language qualified as Reg +import Juvix.Prelude + +mkRustIdent :: Text -> Text +mkRustIdent ident = T.filter isValidIdentChar ident + +getFunctionName :: Reg.ExtraInfo -> Reg.Symbol -> Text +getFunctionName info sym = ((info ^. Reg.extraInfoTable . Reg.infoFunctions) HashMap.! sym) ^. Reg.functionName + +getBuiltinUID :: Reg.BuiltinDataTag -> Int +getBuiltinUID = \case + Reg.TagFalse -> impossible + Reg.TagTrue -> impossible + Reg.TagReturn -> impossible + Reg.TagBind -> impossible + Reg.TagWrite -> impossible + Reg.TagReadLn -> impossible + +getUID :: Reg.ExtraInfo -> Reg.Tag -> Int +getUID info tag = case tag of + Reg.BuiltinTag builtin -> getBuiltinUID builtin + Reg.UserTag {} -> fromJust $ HashMap.lookup tag (info ^. Reg.extraInfoCIDs) + +getFUID :: Reg.ExtraInfo -> Reg.Symbol -> Int +getFUID info sym = fromJust $ HashMap.lookup sym (info ^. Reg.extraInfoFUIDs) + +getStringId :: Reg.ExtraInfo -> Text -> Int +getStringId info txt = fromJust $ HashMap.lookup txt (info ^. Reg.extraInfoStringMap) + +getMaxStackHeight :: Reg.ExtraInfo -> Reg.Symbol -> Int +getMaxStackHeight info sym = fromJust $ HashMap.lookup sym (info ^. Reg.extraInfoMaxStackHeight) + +getLocalVarsNum :: Reg.ExtraInfo -> Reg.Symbol -> Int +getLocalVarsNum info sym = fromJust $ HashMap.lookup sym (info ^. Reg.extraInfoLocalVarsNum) + +getFunctionIdent :: Reg.ExtraInfo -> Reg.Symbol -> Text +getFunctionIdent info sym = mkRustIdent $ "JUVIX_FUNCTION_" <> T.toUpper (getFunctionName info sym) <> "_" <> show (getFUID info sym) + +stmtAssign :: Text -> Expression -> Statement +stmtAssign result value = StatementAssignment $ Assignment result value + +stmtsAssign :: Text -> Expression -> [Statement] +stmtsAssign result value = [stmtAssign result value] + +stmtsCall :: Text -> [Expression] -> [Statement] +stmtsCall fun args = [StatementExpression $ mkCall fun args] + +stmtsBlock :: [Statement] -> [Statement] +stmtsBlock stmts = [StatementExpression (ExprBlock (Block stmts))] + +stmtLet :: IsMut -> Text -> Expression -> Statement +stmtLet isMut result value = + StatementLet $ + Let + { _letMutable = isMut, + _letVariable = result, + _letType = Nothing, + _letInitializer = Just value + } + +stmtDecl :: IsMut -> Text -> Type -> Statement +stmtDecl isMut var ty = + StatementLet $ + Let + { _letMutable = isMut, + _letVariable = var, + _letType = Just ty, + _letInitializer = Nothing + } + +stmtIf :: Expression -> [Statement] -> [Statement] -> Statement +stmtIf v br1 br2 = StatementIf $ If v br1 br2 + +stmtsIf :: Expression -> [Statement] -> [Statement] -> [Statement] +stmtsIf v br1 br2 = [stmtIf v br1 br2] + +mkCall :: Text -> [Expression] -> Expression +mkCall fun args = ExprCall $ Call fun args + +mkInteger :: (Integral a) => a -> Expression +mkInteger i = ExprLiteral $ LitInteger (fromIntegral i) + +mkString :: Text -> Expression +mkString s = ExprLiteral $ LitString s + +mkVar :: Text -> Expression +mkVar = ExprVar . Var + +mkArray :: [Expression] -> Expression +mkArray = ExprArray . Array + +mkVec :: [Expression] -> Expression +mkVec = ExprVec . Vec diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index c7b60ccedc..a073931ca3 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs @@ -23,6 +23,7 @@ data TransformationId | CombineInfoTables | CheckGeb | CheckExec + | CheckRust | CheckVampIR | CheckAnoma | CheckCairo @@ -103,6 +104,7 @@ instance TransformationId' TransformationId where CombineInfoTables -> strCombineInfoTables CheckGeb -> strCheckGeb CheckExec -> strCheckExec + CheckRust -> strCheckRust CheckVampIR -> strCheckVampIR CheckAnoma -> strCheckAnoma CheckCairo -> strCheckCairo diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs index 35b5a45590..b6be5dc47e 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs @@ -77,6 +77,9 @@ strCheckGeb = "check-geb" strCheckExec :: Text strCheckExec = "check-exec" +strCheckRust :: Text +strCheckRust = "check-rust" + strCheckVampIR :: Text strCheckVampIR = "check-vampir" diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index 10c82c2dee..ba160116b1 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/src/Juvix/Compiler/Core/Transformation.hs @@ -17,6 +17,7 @@ import Juvix.Compiler.Core.Transformation.Check.Anoma import Juvix.Compiler.Core.Transformation.Check.Cairo import Juvix.Compiler.Core.Transformation.Check.Exec import Juvix.Compiler.Core.Transformation.Check.Geb +import Juvix.Compiler.Core.Transformation.Check.Rust import Juvix.Compiler.Core.Transformation.Check.VampIR import Juvix.Compiler.Core.Transformation.CombineInfoTables (combineInfoTables) import Juvix.Compiler.Core.Transformation.ComputeTypeInfo @@ -81,6 +82,7 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts CombineInfoTables -> return . combineInfoTables CheckGeb -> mapError (JuvixError @CoreError) . checkGeb CheckExec -> mapError (JuvixError @CoreError) . checkExec + CheckRust -> mapError (JuvixError @CoreError) . checkRust CheckVampIR -> mapError (JuvixError @CoreError) . checkVampIR CheckAnoma -> mapError (JuvixError @CoreError) . checkAnoma CheckCairo -> mapError (JuvixError @CoreError) . checkCairo diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs index 1898ffab49..953a57a9be 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs @@ -162,3 +162,36 @@ checkMainExists md = _coreErrorNode = Nothing, _coreErrorLoc = defaultLoc } + +checkMainTypeExec :: (Member (Error CoreError) r) => Module -> Sem r () +checkMainTypeExec md = + case md ^. moduleInfoTable . infoMain of + Nothing -> + throw + CoreError + { _coreErrorMsg = ppOutput "no `main` function", + _coreErrorNode = Nothing, + _coreErrorLoc = defaultLoc + } + Just sym -> + case ii ^. identifierType of + NPi {} -> + throw + CoreError + { _coreErrorMsg = ppOutput "`main` cannot have a function type for this target", + _coreErrorNode = Nothing, + _coreErrorLoc = loc + } + ty + | isTypeConstr md ty -> + throw + CoreError + { _coreErrorMsg = ppOutput "`main` cannot be a type for this target", + _coreErrorNode = Nothing, + _coreErrorLoc = loc + } + _ -> + return () + where + ii = lookupIdentifierInfo md sym + loc = fromMaybe defaultLoc (ii ^. identifierLocation) diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs b/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs index 0c3b0cffb7..f11b3265aa 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs +++ b/src/Juvix/Compiler/Core/Transformation/Check/Exec.hs @@ -4,44 +4,10 @@ import Juvix.Compiler.Core.Error import Juvix.Compiler.Core.Extra import Juvix.Compiler.Core.Transformation.Base import Juvix.Compiler.Core.Transformation.Check.Base -import Juvix.Data.PPOutput checkExec :: forall r. (Member (Error CoreError) r) => Module -> Sem r Module checkExec md = do checkNoAxioms md checkMainExists md - checkMainType + checkMainTypeExec md mapAllNodesM (checkBuiltins' (builtinsCairo ++ builtinsAnoma) []) md - where - checkMainType :: Sem r () - checkMainType = - case md ^. moduleInfoTable . infoMain of - Nothing -> - throw - CoreError - { _coreErrorMsg = ppOutput "no `main` function", - _coreErrorNode = Nothing, - _coreErrorLoc = defaultLoc - } - Just sym -> - case ii ^. identifierType of - NPi {} -> - throw - CoreError - { _coreErrorMsg = ppOutput "`main` cannot have a function type for this target", - _coreErrorNode = Nothing, - _coreErrorLoc = loc - } - ty - | isTypeConstr md ty -> - throw - CoreError - { _coreErrorMsg = ppOutput "`main` cannot be a type for this target", - _coreErrorNode = Nothing, - _coreErrorLoc = loc - } - _ -> - return () - where - ii = lookupIdentifierInfo md sym - loc = fromMaybe defaultLoc (ii ^. identifierLocation) diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Rust.hs b/src/Juvix/Compiler/Core/Transformation/Check/Rust.hs new file mode 100644 index 0000000000..36ba3ac8d3 --- /dev/null +++ b/src/Juvix/Compiler/Core/Transformation/Check/Rust.hs @@ -0,0 +1,14 @@ +module Juvix.Compiler.Core.Transformation.Check.Rust where + +import Juvix.Compiler.Core.Error +import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Transformation.Base +import Juvix.Compiler.Core.Transformation.Check.Base + +checkRust :: forall r. (Member (Error CoreError) r) => Module -> Sem r Module +checkRust md = do + checkNoAxioms md + checkMainExists md + checkMainTypeExec md + mapAllNodesM checkNoIO md + mapAllNodesM (checkBuiltins False) md diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 2bcc1a6aac..7b5d73a4d3 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/src/Juvix/Compiler/Pipeline.hs @@ -16,6 +16,7 @@ import Juvix.Compiler.Backend qualified as Backend import Juvix.Compiler.Backend.C qualified as C import Juvix.Compiler.Backend.Cairo qualified as Cairo import Juvix.Compiler.Backend.Geb qualified as Geb +import Juvix.Compiler.Backend.Rust.Translation.FromReg qualified as Rust import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR import Juvix.Compiler.Casm.Data.Builtins qualified as Casm import Juvix.Compiler.Casm.Data.Result qualified as Casm @@ -158,6 +159,11 @@ upToAnoma :: Sem r NockmaTree.AnomaResult upToAnoma = upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToAnoma _coreResultModule +upToRust :: + (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, PathResolver] r) => + Sem r Rust.Result +upToRust = upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToRust _coreResultModule + upToCoreTypecheck :: (Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError, PathResolver] r) => Sem r Core.CoreResult @@ -191,6 +197,9 @@ storedCoreToReg = storedCoreToAsm >=> asmToReg storedCoreToMiniC :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r C.MiniCResult storedCoreToMiniC = storedCoreToAsm >=> asmToMiniC +storedCoreToRust :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Rust.Result +storedCoreToRust = storedCoreToTree Core.CheckRust >=> treeToReg >=> regToRust + storedCoreToCasm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Casm.Result storedCoreToCasm = local (set entryPointFieldSize cairoFieldSize) . storedCoreToTree Core.CheckCairo >=> treeToCasm @@ -283,6 +292,12 @@ regToMiniC tab = do e <- ask return $ C.fromReg (Backend.getLimits (getEntryPointTarget e) (e ^. entryPointDebug)) tab' +regToRust :: (Member (Reader EntryPoint) r) => Reg.InfoTable -> Sem r Rust.Result +regToRust tab = do + tab' <- Reg.toRust tab + e <- ask + return $ Rust.fromReg (Backend.getLimits (getEntryPointTarget e) (e ^. entryPointDebug)) tab' + regToCasm :: Reg.InfoTable -> Sem r Casm.Result regToCasm = Reg.toCasm >=> return . Casm.fromReg diff --git a/src/Juvix/Compiler/Reg/Data/TransformationId.hs b/src/Juvix/Compiler/Reg/Data/TransformationId.hs index 30c7148ecd..89b690b779 100644 --- a/src/Juvix/Compiler/Reg/Data/TransformationId.hs +++ b/src/Juvix/Compiler/Reg/Data/TransformationId.hs @@ -14,6 +14,7 @@ data TransformationId data PipelineId = PipelineCasm | PipelineC + | PipelineRust deriving stock (Data, Bounded, Enum) type TransformationLikeId = TransformationLikeId' TransformationId PipelineId @@ -21,6 +22,9 @@ type TransformationLikeId = TransformationLikeId' TransformationId PipelineId toCTransformations :: [TransformationId] toCTransformations = [Cleanup] +toRustTransformations :: [TransformationId] +toRustTransformations = [Cleanup] + toCasmTransformations :: [TransformationId] toCasmTransformations = [Cleanup, SSA] @@ -36,9 +40,11 @@ instance PipelineId' TransformationId PipelineId where pipelineText :: PipelineId -> Text pipelineText = \case PipelineC -> strCPipeline + PipelineRust -> strRustPipeline PipelineCasm -> strCasmPipeline pipeline :: PipelineId -> [TransformationId] pipeline = \case PipelineC -> toCTransformations + PipelineRust -> toRustTransformations PipelineCasm -> toCasmTransformations diff --git a/src/Juvix/Compiler/Reg/Data/TransformationId/Strings.hs b/src/Juvix/Compiler/Reg/Data/TransformationId/Strings.hs index 4d0ae8c182..a38e22620a 100644 --- a/src/Juvix/Compiler/Reg/Data/TransformationId/Strings.hs +++ b/src/Juvix/Compiler/Reg/Data/TransformationId/Strings.hs @@ -5,6 +5,9 @@ import Juvix.Prelude strCPipeline :: Text strCPipeline = "pipeline-c" +strRustPipeline :: Text +strRustPipeline = "pipeline-rust" + strCasmPipeline :: Text strCasmPipeline = "pipeline-casm" diff --git a/src/Juvix/Compiler/Reg/Pipeline.hs b/src/Juvix/Compiler/Reg/Pipeline.hs index cde5f45780..43eee4a079 100644 --- a/src/Juvix/Compiler/Reg/Pipeline.hs +++ b/src/Juvix/Compiler/Reg/Pipeline.hs @@ -14,6 +14,10 @@ import Juvix.Compiler.Reg.Translation.Blocks.FromReg qualified as Blocks toC :: InfoTable -> Sem r InfoTable toC = applyTransformations toCTransformations +-- | Perform transformations on JuvixReg necessary before the translation to Rust +toRust :: InfoTable -> Sem r InfoTable +toRust = applyTransformations toRustTransformations + -- | Perform transformations on JuvixReg necessary before the translation to -- Cairo assembly toCasm :: InfoTable -> Sem r Blocks.InfoTable diff --git a/src/Juvix/Data/FileExt.hs b/src/Juvix/Data/FileExt.hs index dda274981f..353ec822ba 100644 --- a/src/Juvix/Data/FileExt.hs +++ b/src/Juvix/Data/FileExt.hs @@ -22,6 +22,7 @@ data FileExt | FileExtPlonk | FileExtHalo | FileExtLisp + | FileExtRust | FileExtC | FileExtMarkdown | FileExtHtml @@ -85,6 +86,9 @@ markdownFileExt = ".md" cFileExt :: (IsString a) => a cFileExt = ".c" +rustFileExt :: (IsString a) => a +rustFileExt = ".rs" + cssFileExt :: (IsString a) => a cssFileExt = ".css" @@ -110,6 +114,7 @@ fileExtToIsString = \case FileExtPlonk -> plonkFileExt FileExtHalo -> haloFileExt FileExtLisp -> lispFileExt + FileExtRust -> rustFileExt FileExtC -> cFileExt FileExtMarkdown -> markdownFileExt FileExtHtml -> htmlFileExt @@ -135,6 +140,7 @@ toMetavar = \case FileExtPlonk -> "PLONK_FILE" FileExtHalo -> "HALO_FILE" FileExtLisp -> "LISP_FILE" + FileExtRust -> "RUST_FILE" FileExtC -> "C_FILE" FileExtMarkdown -> "MARKDOWN_FILE" FileExtHtml -> "HTML_FILE" @@ -194,6 +200,9 @@ isLispFile = (== Just lispFileExt) . fileExtension isMarkdownFile :: Path b File -> Bool isMarkdownFile = (== Just markdownFileExt) . fileExtension +isRustFile :: Path b File -> Bool +isRustFile = (== Just rustFileExt) . fileExtension + isCFile :: Path b File -> Bool isCFile = (== Just cFileExt) . fileExtension @@ -221,6 +230,7 @@ toFileExt p | isPlonkFile p = Just FileExtPlonk | isHaloFile p = Just FileExtHalo | isLispFile p = Just FileExtLisp + | isRustFile p = Just FileExtRust | isCFile p = Just FileExtC | isMarkdownFile p = Just FileExtMarkdown | isHtmlFile p = Just FileExtHtml diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 4347536591..57284e46f2 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -1054,3 +1054,45 @@ cairoEcPoint = "ec_point" cairoMkEcPoint :: (IsString s) => s cairoMkEcPoint = "mkEcPoint" + +rustFn :: (IsString s) => s +rustFn = "fn" + +rustIf :: (IsString s) => s +rustIf = "if" + +rustElse :: (IsString s) => s +rustElse = "else" + +rustMatch :: (IsString s) => s +rustMatch = "match" + +rustLoop :: (IsString s) => s +rustLoop = "loop" + +rustLet :: (IsString s) => s +rustLet = "let" + +rustConst :: (IsString s) => s +rustConst = "const" + +rustMut :: (IsString s) => s +rustMut = "mut" + +rustVec :: (IsString s) => s +rustVec = "vec!" + +rustVector :: (IsString s) => s +rustVector = "Vec" + +rustWord :: (IsString s) => s +rustWord = "Word" + +rustMemory :: (IsString s) => s +rustMemory = "Memory" + +rustContinue :: (IsString s) => s +rustContinue = "continue" + +rustReturn :: (IsString s) => s +rustReturn = "return" diff --git a/test/Base.hs b/test/Base.hs index ea0a0c61ff..293fa23b17 100644 --- a/test/Base.hs +++ b/test/Base.hs @@ -21,6 +21,7 @@ import Juvix.Data.Effect.TaggedLock import Juvix.Extra.Paths hiding (rootBuildDir) import Juvix.Prelude hiding (assert) import Juvix.Prelude.Env +import System.Process qualified as P import Test.Tasty import Test.Tasty.HUnit hiding (assertFailure) import Test.Tasty.HUnit qualified as HUnit @@ -114,3 +115,36 @@ testRunIOEitherTermination entry = assertFailure :: (MonadIO m) => String -> m a assertFailure = liftIO . HUnit.assertFailure + +-- | The same as `P.readProcess` but instead of inheriting `stderr` redirects it +-- to the child's `stdout`. +readProcess :: FilePath -> [String] -> Text -> IO Text +readProcess = readProcessCwd' Nothing + +readProcessCwd :: FilePath -> FilePath -> [String] -> Text -> IO Text +readProcessCwd cwd = readProcessCwd' (Just cwd) + +readProcessCwd' :: Maybe FilePath -> FilePath -> [String] -> Text -> IO Text +readProcessCwd' mcwd cmd args stdinText = + withTempDir' + ( \dirPath -> do + (_, hin) <- openTempFile dirPath "stdin" + (_, hout) <- openTempFile dirPath "stdout" + hPutStr hin stdinText + hSeek hin AbsoluteSeek 0 + (_, _, _, ph) <- + P.createProcess_ + "readProcess" + (P.proc cmd args) + { P.std_in = P.UseHandle hin, + P.std_out = P.UseHandle hout, + P.std_err = P.UseHandle hout, + P.cwd = mcwd + } + P.waitForProcess ph + hSeek hout AbsoluteSeek 0 + r <- hGetContents hout + hClose hin + hClose hout + return r + ) diff --git a/test/Casm/Run/Base.hs b/test/Casm/Run/Base.hs index fa56192b12..3266885e09 100644 --- a/test/Casm/Run/Base.hs +++ b/test/Casm/Run/Base.hs @@ -12,12 +12,11 @@ import Juvix.Compiler.Casm.Validate import Juvix.Data.Field import Juvix.Data.PPOutput import Juvix.Parser.Error -import Runtime.Base qualified as R casmRunVM' :: Path Abs Dir -> Path Abs File -> Maybe (Path Abs File) -> IO Text casmRunVM' dirPath outputFile inputFile = do let args = maybe [] (\f -> ["--program_input", toFilePath f]) inputFile - R.readProcessCwd (toFilePath dirPath) "run_cairo_vm.sh" (toFilePath outputFile : args) "" + readProcessCwd (toFilePath dirPath) "run_cairo_vm.sh" (toFilePath outputFile : args) "" casmRunVM :: LabelInfo -> Code -> [Builtin] -> Maybe (Path Abs File) -> Path Abs File -> (String -> IO ()) -> Assertion casmRunVM labi instrs blts inputFile expectedFile step = do diff --git a/test/Main.hs b/test/Main.hs index e8e54aa308..b9cf5d2b08 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -19,6 +19,7 @@ import Reg qualified import Repl qualified import Resolver qualified import Runtime qualified +import Rust qualified import Scope qualified import Termination qualified import Tree qualified @@ -38,6 +39,7 @@ slowTests = Internal.allTests, Compilation.allTests, Examples.allTests, + Rust.allTests, Casm.allTests, VampIR.allTests, Anoma.allTests, diff --git a/test/Runtime/Base.hs b/test/Runtime/Base.hs index 867565443b..db8cb706a9 100644 --- a/test/Runtime/Base.hs +++ b/test/Runtime/Base.hs @@ -23,39 +23,6 @@ clangCompile mkClangArgs inputFile outputFile execute step = execute outputFile' ) --- | The same as `P.readProcess` but instead of inheriting `stderr` redirects it --- to the child's `stdout`. -readProcess :: FilePath -> [String] -> Text -> IO Text -readProcess = readProcessCwd' Nothing - -readProcessCwd :: FilePath -> FilePath -> [String] -> Text -> IO Text -readProcessCwd cwd = readProcessCwd' (Just cwd) - -readProcessCwd' :: Maybe FilePath -> FilePath -> [String] -> Text -> IO Text -readProcessCwd' mcwd cmd args stdinText = - withTempDir' - ( \dirPath -> do - (_, hin) <- openTempFile dirPath "stdin" - (_, hout) <- openTempFile dirPath "stdout" - hPutStr hin stdinText - hSeek hin AbsoluteSeek 0 - (_, _, _, ph) <- - P.createProcess_ - "readProcess" - (P.proc cmd args) - { P.std_in = P.UseHandle hin, - P.std_out = P.UseHandle hout, - P.std_err = P.UseHandle hout, - P.cwd = mcwd - } - P.waitForProcess ph - hSeek hout AbsoluteSeek 0 - r <- hGetContents hout - hClose hin - hClose hout - return r - ) - clangAssertion :: Int -> Path Abs File -> Path Abs File -> Text -> ((String -> IO ()) -> Assertion) clangAssertion optLevel inputFile expectedFile stdinText step = do step "Check clang and wasmer are on path" diff --git a/test/Rust.hs b/test/Rust.hs new file mode 100644 index 0000000000..65f7c95ef9 --- /dev/null +++ b/test/Rust.hs @@ -0,0 +1,7 @@ +module Rust where + +import Base +import Rust.Compilation qualified as Compilation + +allTests :: TestTree +allTests = testGroup "Juvix to Rust tests" [Compilation.allTests] diff --git a/test/Rust/Compilation.hs b/test/Rust/Compilation.hs new file mode 100644 index 0000000000..59064cba33 --- /dev/null +++ b/test/Rust/Compilation.hs @@ -0,0 +1,7 @@ +module Rust.Compilation where + +import Base +import Rust.Compilation.Positive qualified as P + +allTests :: TestTree +allTests = testGroup "Juvix to native Rust compilation tests" [P.allTests, P.allTestsNoOptimize] diff --git a/test/Rust/Compilation/Base.hs b/test/Rust/Compilation/Base.hs new file mode 100644 index 0000000000..b479033e62 --- /dev/null +++ b/test/Rust/Compilation/Base.hs @@ -0,0 +1,81 @@ +module Rust.Compilation.Base where + +import Base +import Data.FileEmbed +import Juvix.Compiler.Backend.Rust.Data.Result +import Juvix.Compiler.Backend.Rust.Pretty +import Juvix.Compiler.Core qualified as Core +import System.Process qualified as P + +compileAssertion :: + Path Abs Dir -> + Int -> + Path Abs File -> + Path Abs File -> + (String -> IO ()) -> + Assertion +compileAssertion root' optLevel mainFile expectedFile step = do + step "Translate to JuvixCore" + entryPoint <- testDefaultEntryPointIO root' mainFile + PipelineResult {..} <- snd <$> testRunIO entryPoint upToStoredCore + step "Translate to Rust" + case run $ runError @JuvixError $ runReader entryPoint $ storedCoreToRust (_pipelineResult ^. Core.coreResultModule) of + Left err -> assertFailure (prettyString (fromJuvixError @GenericError err)) + Right Result {..} -> do + withTempDir' + ( \dirPath -> do + let inputFile = dirPath $(mkRelFile "Program.rs") + writeFileEnsureLn inputFile _resultRustCode + + step "Check rustc is on path" + assertCmdExists $(mkRelFile "rustc") + + expected <- readFile expectedFile + + let executeNative :: Path Abs File -> IO Text + executeNative outputFile = readProcess (toFilePath outputFile) [] "" + + step "Compile Rust to native code" + actualNative <- rustcCompile (nativeArgs optLevel) inputFile $(mkRelFile "Program") executeNative step + step "Compare expected and actual program output" + assertEqDiffText ("check: native output = " <> toFilePath expectedFile) actualNative expected + ) + +rustcCompile :: + (Path Abs File -> Path Abs File -> [String]) -> + Path Abs File -> + Path Rel File -> + (Path Abs File -> IO Text) -> + (String -> IO ()) -> + IO Text +rustcCompile mkRustcArgs inputFile outputFile execute step = + withTempDir' + ( \dirPath -> do + let outputFile' = dirPath outputFile + step "Rust compilation" + P.callProcess + "rustc" + (mkRustcArgs outputFile' inputFile) + step "Execution" + execute outputFile' + ) + +nativeArgs :: Int -> Path Abs File -> Path Abs File -> [String] +nativeArgs optLevel outputFile inputFile = + [ "-o", + toFilePath outputFile, + "-C", + "opt-level=" + <> show optLevel, + "-L", + juvixLibraryDir, + toFilePath inputFile + ] + where + juvixLibraryDir :: FilePath + juvixLibraryDir = + if + | optLevel > 0 -> + $(makeRelativeToProject "runtime/rust/target/release" >>= strToExp) + | otherwise -> + $(makeRelativeToProject "runtime/rust/target/debug" >>= strToExp) diff --git a/test/Rust/Compilation/Positive.hs b/test/Rust/Compilation/Positive.hs new file mode 100644 index 0000000000..05d4e38fa7 --- /dev/null +++ b/test/Rust/Compilation/Positive.hs @@ -0,0 +1,348 @@ +module Rust.Compilation.Positive where + +import Base +import Data.HashSet qualified as HashSet +import Rust.Compilation.Base + +data PosTest = PosTest + { _name :: String, + _dir :: Path Abs Dir, + _file :: Path Abs File, + _expectedFile :: Path Abs File + } + +makeLenses ''PosTest + +root :: Path Abs Dir +root = relToProject $(mkRelDir "tests/Rust/Compilation/positive/") + +toTestDescr :: Int -> PosTest -> TestDescr +toTestDescr optLevel PosTest {..} = + let tRoot = _dir + file' = _file + expected' = _expectedFile + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Steps $ compileAssertion _dir optLevel file' expected' + } + +allTests :: TestTree +allTests = + testGroup + "Juvix to native Rust positive tests" + (map (mkTest . toTestDescr 3) tests) + +allTestsNoOptimize :: TestTree +allTestsNoOptimize = + testGroup + "Juvix to native Rust positive tests (no optimization)" + (map (mkTest . toTestDescr 0) 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 + _expectedFile = root routfile + in PosTest {..} + +isIgnored :: PosTest -> Bool +isIgnored t = HashSet.member (t ^. name) ignored + +ignored :: HashSet String +ignored = + HashSet.fromList + [ -- strings not supported (Partial trait) + "Test026: Functional queues" + ] + +tests :: [PosTest] +tests = + filter + (not . isIgnored) + [ posTest + "Test001: Arithmetic operators" + $(mkRelDir ".") + $(mkRelFile "test001.juvix") + $(mkRelFile "out/test001.out"), + posTest + "Test002: Arithmetic operators inside lambdas" + $(mkRelDir ".") + $(mkRelFile "test002.juvix") + $(mkRelFile "out/test002.out"), + posTest + "Test003: Integer arithmetic" + $(mkRelDir ".") + $(mkRelFile "test003.juvix") + $(mkRelFile "out/test003.out"), + posTest + "Test005: Higher-order functions" + $(mkRelDir ".") + $(mkRelFile "test005.juvix") + $(mkRelFile "out/test005.out"), + posTest + "Test006: If-then-else and lazy boolean operators" + $(mkRelDir ".") + $(mkRelFile "test006.juvix") + $(mkRelFile "out/test006.out"), + posTest + "Test007: Pattern matching and lambda-case" + $(mkRelDir ".") + $(mkRelFile "test007.juvix") + $(mkRelFile "out/test007.out"), + posTest + "Test008: Recursion" + $(mkRelDir ".") + $(mkRelFile "test008.juvix") + $(mkRelFile "out/test008.out"), + posTest + "Test009: Tail recursion" + $(mkRelDir ".") + $(mkRelFile "test009.juvix") + $(mkRelFile "out/test009.out"), + posTest + "Test010: Let" + $(mkRelDir ".") + $(mkRelFile "test010.juvix") + $(mkRelFile "out/test010.out"), + posTest + "Test013: Functions returning functions with variable capture" + $(mkRelDir ".") + $(mkRelFile "test013.juvix") + $(mkRelFile "out/test013.out"), + posTest + "Test014: Arithmetic" + $(mkRelDir ".") + $(mkRelFile "test014.juvix") + $(mkRelFile "out/test014.out"), + posTest + "Test015: Local functions with free variables" + $(mkRelDir ".") + $(mkRelFile "test015.juvix") + $(mkRelFile "out/test015.out"), + posTest + "Test016: Recursion through higher-order functions" + $(mkRelDir ".") + $(mkRelFile "test016.juvix") + $(mkRelFile "out/test016.out"), + posTest + "Test017: Tail recursion through higher-order functions" + $(mkRelDir ".") + $(mkRelFile "test017.juvix") + $(mkRelFile "out/test017.out"), + posTest + "Test018: Higher-order functions and recursion" + $(mkRelDir ".") + $(mkRelFile "test018.juvix") + $(mkRelFile "out/test018.out"), + posTest + "Test019: Self-application" + $(mkRelDir ".") + $(mkRelFile "test019.juvix") + $(mkRelFile "out/test019.out"), + posTest + "Test020: Recursive functions: McCarthy's 91 function, subtraction by increments" + $(mkRelDir ".") + $(mkRelFile "test020.juvix") + $(mkRelFile "out/test020.out"), + posTest + "Test021: Fast exponentiation" + $(mkRelDir ".") + $(mkRelFile "test021.juvix") + $(mkRelFile "out/test021.out"), + posTest + "Test022: Lists" + $(mkRelDir ".") + $(mkRelFile "test022.juvix") + $(mkRelFile "out/test022.out"), + posTest + "Test023: Mutual recursion" + $(mkRelDir ".") + $(mkRelFile "test023.juvix") + $(mkRelFile "out/test023.out"), + posTest + "Test024: Nested binders with variable capture" + $(mkRelDir ".") + $(mkRelFile "test024.juvix") + $(mkRelFile "out/test024.out"), + posTest + "Test025: Euclid's algorithm" + $(mkRelDir ".") + $(mkRelFile "test025.juvix") + $(mkRelFile "out/test025.out"), + posTest + "Test026: Functional queues" + $(mkRelDir ".") + $(mkRelFile "test026.juvix") + $(mkRelFile "out/test026.out"), + posTest + "Test028: Streams without memoization" + $(mkRelDir ".") + $(mkRelFile "test028.juvix") + $(mkRelFile "out/test028.out"), + posTest + "Test029: Ackermann function" + $(mkRelDir ".") + $(mkRelFile "test029.juvix") + $(mkRelFile "out/test029.out"), + posTest + "Test030: Ackermann function (higher-order definition)" + $(mkRelDir ".") + $(mkRelFile "test030.juvix") + $(mkRelFile "out/test030.out"), + posTest + "Test032: Merge sort" + $(mkRelDir ".") + $(mkRelFile "test032.juvix") + $(mkRelFile "out/test032.out"), + posTest + "Test033: Eta-expansion of builtins and constructors" + $(mkRelDir ".") + $(mkRelFile "test033.juvix") + $(mkRelFile "out/test033.out"), + posTest + "Test034: Recursive let" + $(mkRelDir ".") + $(mkRelFile "test034.juvix") + $(mkRelFile "out/test034.out"), + posTest + "Test035: Pattern matching" + $(mkRelDir ".") + $(mkRelFile "test035.juvix") + $(mkRelFile "out/test035.out"), + posTest + "Test036: Eta-expansion" + $(mkRelDir ".") + $(mkRelFile "test036.juvix") + $(mkRelFile "out/test036.out"), + posTest + "Test037: Applications with lets and cases in function position" + $(mkRelDir ".") + $(mkRelFile "test037.juvix") + $(mkRelFile "out/test037.out"), + posTest + "Test038: Simple case expression" + $(mkRelDir ".") + $(mkRelFile "test038.juvix") + $(mkRelFile "out/test038.out"), + posTest + "Test039: Mutually recursive let expression" + $(mkRelDir ".") + $(mkRelFile "test039.juvix") + $(mkRelFile "out/test039.out"), + posTest + "Test040: Pattern matching nullary constructor" + $(mkRelDir ".") + $(mkRelFile "test040.juvix") + $(mkRelFile "out/test040.out"), + posTest + "Test045: Implicit builtin bool" + $(mkRelDir ".") + $(mkRelFile "test045.juvix") + $(mkRelFile "out/test045.out"), + posTest + "Test046: Polymorphic type arguments" + $(mkRelDir ".") + $(mkRelFile "test046.juvix") + $(mkRelFile "out/test046.out"), + posTest + "Test047: Local Modules" + $(mkRelDir ".") + $(mkRelFile "test047.juvix") + $(mkRelFile "out/test047.out"), + posTest + "Test050: Pattern matching with integers" + $(mkRelDir ".") + $(mkRelFile "test050.juvix") + $(mkRelFile "out/test050.out"), + posTest + "Test053: Inlining" + $(mkRelDir ".") + $(mkRelFile "test053.juvix") + $(mkRelFile "out/test053.out"), + posTest + "Test054: Iterators" + $(mkRelDir ".") + $(mkRelFile "test054.juvix") + $(mkRelFile "out/test054.out"), + posTest + "Test056: Argument specialization" + $(mkRelDir ".") + $(mkRelFile "test056.juvix") + $(mkRelFile "out/test056.out"), + posTest + "Test057: Case folding" + $(mkRelDir ".") + $(mkRelFile "test057.juvix") + $(mkRelFile "out/test057.out"), + posTest + "Test058: Ranges" + $(mkRelDir ".") + $(mkRelFile "test058.juvix") + $(mkRelFile "out/test058.out"), + posTest + "Test059: Builtin list" + $(mkRelDir ".") + $(mkRelFile "test059.juvix") + $(mkRelFile "out/test059.out"), + posTest + "Test060: Record update" + $(mkRelDir ".") + $(mkRelFile "test060.juvix") + $(mkRelFile "out/test060.out"), + posTest + "Test062: Overapplication" + $(mkRelDir ".") + $(mkRelFile "test062.juvix") + $(mkRelFile "out/test062.out"), + posTest + "Test064: Constant folding" + $(mkRelDir ".") + $(mkRelFile "test064.juvix") + $(mkRelFile "out/test064.out"), + posTest + "Test065: Arithmetic simplification" + $(mkRelDir ".") + $(mkRelFile "test065.juvix") + $(mkRelFile "out/test065.out"), + posTest + "Test066: Import function with a function call in default argument" + $(mkRelDir "test066") + $(mkRelFile "M.juvix") + $(mkRelFile "out/test066.out"), + posTest + "Test067: Dependent default values inserted during translation FromConcrete" + $(mkRelDir ".") + $(mkRelFile "test067.juvix") + $(mkRelFile "out/test067.out"), + posTest + "Test068: Dependent default values inserted in the arity checker" + $(mkRelDir ".") + $(mkRelFile "test068.juvix") + $(mkRelFile "out/test068.out"), + posTest + "Test069: Dependent default values for Ord trait" + $(mkRelDir ".") + $(mkRelFile "test069.juvix") + $(mkRelFile "out/test069.out"), + posTest + "Test070: Nested default values and named arguments" + $(mkRelDir ".") + $(mkRelFile "test070.juvix") + $(mkRelFile "out/test070.out"), + posTest + "Test071: Named application (Ord instance with default cmp)" + $(mkRelDir ".") + $(mkRelFile "test071.juvix") + $(mkRelFile "out/test071.out"), + posTest + "Test072: Monad transformers (ReaderT + StateT + Identity)" + $(mkRelDir "test072") + $(mkRelFile "ReaderT.juvix") + $(mkRelFile "out/test072.out"), + posTest + "Test073: Import and use a syntax alias" + $(mkRelDir "test073") + $(mkRelFile "test073.juvix") + $(mkRelFile "out/test073.out") + ] diff --git a/tests/Rust/Compilation/positive/out/test001.out b/tests/Rust/Compilation/positive/out/test001.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test001.out @@ -0,0 +1 @@ +11 diff --git a/tests/Rust/Compilation/positive/out/test002.out b/tests/Rust/Compilation/positive/out/test002.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test002.out @@ -0,0 +1 @@ +11 diff --git a/tests/Rust/Compilation/positive/out/test003.out b/tests/Rust/Compilation/positive/out/test003.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test003.out @@ -0,0 +1 @@ +11 diff --git a/tests/Rust/Compilation/positive/out/test005.out b/tests/Rust/Compilation/positive/out/test005.out new file mode 100644 index 0000000000..1e8b314962 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test005.out @@ -0,0 +1 @@ +6 diff --git a/tests/Rust/Compilation/positive/out/test006.out b/tests/Rust/Compilation/positive/out/test006.out new file mode 100644 index 0000000000..00750edc07 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test006.out @@ -0,0 +1 @@ +3 diff --git a/tests/Rust/Compilation/positive/out/test007.out b/tests/Rust/Compilation/positive/out/test007.out new file mode 100644 index 0000000000..1e8b314962 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test007.out @@ -0,0 +1 @@ +6 diff --git a/tests/Rust/Compilation/positive/out/test008.out b/tests/Rust/Compilation/positive/out/test008.out new file mode 100644 index 0000000000..b9d569380c --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test008.out @@ -0,0 +1 @@ +50005000 diff --git a/tests/Rust/Compilation/positive/out/test009.out b/tests/Rust/Compilation/positive/out/test009.out new file mode 100644 index 0000000000..094058575c --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test009.out @@ -0,0 +1 @@ +532635520 diff --git a/tests/Rust/Compilation/positive/out/test010.out b/tests/Rust/Compilation/positive/out/test010.out new file mode 100644 index 0000000000..f5c89552bd --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test010.out @@ -0,0 +1 @@ +32 diff --git a/tests/Rust/Compilation/positive/out/test013.out b/tests/Rust/Compilation/positive/out/test013.out new file mode 100644 index 0000000000..45a4fb75db --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test013.out @@ -0,0 +1 @@ +8 diff --git a/tests/Rust/Compilation/positive/out/test014.out b/tests/Rust/Compilation/positive/out/test014.out new file mode 100644 index 0000000000..cd5b025272 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test014.out @@ -0,0 +1 @@ +92 diff --git a/tests/Rust/Compilation/positive/out/test015.out b/tests/Rust/Compilation/positive/out/test015.out new file mode 100644 index 0000000000..a01f8275a7 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test015.out @@ -0,0 +1 @@ +771 diff --git a/tests/Rust/Compilation/positive/out/test016.out b/tests/Rust/Compilation/positive/out/test016.out new file mode 100644 index 0000000000..c3f407c095 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test016.out @@ -0,0 +1 @@ +55 diff --git a/tests/Rust/Compilation/positive/out/test017.out b/tests/Rust/Compilation/positive/out/test017.out new file mode 100644 index 0000000000..b9d569380c --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test017.out @@ -0,0 +1 @@ +50005000 diff --git a/tests/Rust/Compilation/positive/out/test018.out b/tests/Rust/Compilation/positive/out/test018.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test018.out @@ -0,0 +1 @@ +11 diff --git a/tests/Rust/Compilation/positive/out/test019.out b/tests/Rust/Compilation/positive/out/test019.out new file mode 100644 index 0000000000..7f8f011eb7 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test019.out @@ -0,0 +1 @@ +7 diff --git a/tests/Rust/Compilation/positive/out/test020.out b/tests/Rust/Compilation/positive/out/test020.out new file mode 100644 index 0000000000..c4fa141442 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test020.out @@ -0,0 +1 @@ +4876 diff --git a/tests/Rust/Compilation/positive/out/test021.out b/tests/Rust/Compilation/positive/out/test021.out new file mode 100644 index 0000000000..607874b4cd --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test021.out @@ -0,0 +1 @@ +80320 diff --git a/tests/Rust/Compilation/positive/out/test022.out b/tests/Rust/Compilation/positive/out/test022.out new file mode 100644 index 0000000000..3fb224413e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test022.out @@ -0,0 +1 @@ +100010000 diff --git a/tests/Rust/Compilation/positive/out/test023.out b/tests/Rust/Compilation/positive/out/test023.out new file mode 100644 index 0000000000..1fa666edc5 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test023.out @@ -0,0 +1 @@ +6386010 diff --git a/tests/Rust/Compilation/positive/out/test024.out b/tests/Rust/Compilation/positive/out/test024.out new file mode 100644 index 0000000000..f7bd8cc287 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test024.out @@ -0,0 +1 @@ +6688 diff --git a/tests/Rust/Compilation/positive/out/test025.out b/tests/Rust/Compilation/positive/out/test025.out new file mode 100644 index 0000000000..84df3526d8 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test025.out @@ -0,0 +1 @@ +87 diff --git a/tests/Rust/Compilation/positive/out/test026.out b/tests/Rust/Compilation/positive/out/test026.out new file mode 100644 index 0000000000..c3ac783e70 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test026.out @@ -0,0 +1 @@ +5050 diff --git a/tests/Rust/Compilation/positive/out/test028.out b/tests/Rust/Compilation/positive/out/test028.out new file mode 100644 index 0000000000..a8629432ce --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test028.out @@ -0,0 +1 @@ +2040 diff --git a/tests/Rust/Compilation/positive/out/test029.out b/tests/Rust/Compilation/positive/out/test029.out new file mode 100644 index 0000000000..8e14edce9c --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test029.out @@ -0,0 +1 @@ +78 diff --git a/tests/Rust/Compilation/positive/out/test030.out b/tests/Rust/Compilation/positive/out/test030.out new file mode 100644 index 0000000000..40c4a2ca34 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test030.out @@ -0,0 +1 @@ +2247 diff --git a/tests/Rust/Compilation/positive/out/test032.out b/tests/Rust/Compilation/positive/out/test032.out new file mode 100644 index 0000000000..6bb2f98fb0 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test032.out @@ -0,0 +1 @@ +195 diff --git a/tests/Rust/Compilation/positive/out/test033.out b/tests/Rust/Compilation/positive/out/test033.out new file mode 100644 index 0000000000..e85087affd --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test033.out @@ -0,0 +1 @@ +31 diff --git a/tests/Rust/Compilation/positive/out/test034.out b/tests/Rust/Compilation/positive/out/test034.out new file mode 100644 index 0000000000..ee5a2becbf --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test034.out @@ -0,0 +1 @@ +501527 diff --git a/tests/Rust/Compilation/positive/out/test035.out b/tests/Rust/Compilation/positive/out/test035.out new file mode 100644 index 0000000000..e61273a900 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test035.out @@ -0,0 +1 @@ +34422 diff --git a/tests/Rust/Compilation/positive/out/test036.out b/tests/Rust/Compilation/positive/out/test036.out new file mode 100644 index 0000000000..3c032078a4 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test036.out @@ -0,0 +1 @@ +18 diff --git a/tests/Rust/Compilation/positive/out/test037.out b/tests/Rust/Compilation/positive/out/test037.out new file mode 100644 index 0000000000..ec635144f6 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test037.out @@ -0,0 +1 @@ +9 diff --git a/tests/Rust/Compilation/positive/out/test038.out b/tests/Rust/Compilation/positive/out/test038.out new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test038.out @@ -0,0 +1 @@ +1 diff --git a/tests/Rust/Compilation/positive/out/test039.out b/tests/Rust/Compilation/positive/out/test039.out new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test039.out @@ -0,0 +1 @@ +1 diff --git a/tests/Rust/Compilation/positive/out/test040.out b/tests/Rust/Compilation/positive/out/test040.out new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test040.out @@ -0,0 +1 @@ +1 diff --git a/tests/Rust/Compilation/positive/out/test045.out b/tests/Rust/Compilation/positive/out/test045.out new file mode 100644 index 0000000000..b8626c4cff --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test045.out @@ -0,0 +1 @@ +4 diff --git a/tests/Rust/Compilation/positive/out/test046.out b/tests/Rust/Compilation/positive/out/test046.out new file mode 100644 index 0000000000..7f8f011eb7 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test046.out @@ -0,0 +1 @@ +7 diff --git a/tests/Rust/Compilation/positive/out/test047.out b/tests/Rust/Compilation/positive/out/test047.out new file mode 100644 index 0000000000..e250077b11 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test047.out @@ -0,0 +1 @@ +660 diff --git a/tests/Rust/Compilation/positive/out/test050.out b/tests/Rust/Compilation/positive/out/test050.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test050.out @@ -0,0 +1 @@ +11 diff --git a/tests/Rust/Compilation/positive/out/test053.out b/tests/Rust/Compilation/positive/out/test053.out new file mode 100644 index 0000000000..aabe6ec390 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test053.out @@ -0,0 +1 @@ +21 diff --git a/tests/Rust/Compilation/positive/out/test054.out b/tests/Rust/Compilation/positive/out/test054.out new file mode 100644 index 0000000000..6c412452bc --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test054.out @@ -0,0 +1 @@ +189 diff --git a/tests/Rust/Compilation/positive/out/test056.out b/tests/Rust/Compilation/positive/out/test056.out new file mode 100644 index 0000000000..b5489e5e51 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test056.out @@ -0,0 +1 @@ +69 diff --git a/tests/Rust/Compilation/positive/out/test057.out b/tests/Rust/Compilation/positive/out/test057.out new file mode 100644 index 0000000000..45a4fb75db --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test057.out @@ -0,0 +1 @@ +8 diff --git a/tests/Rust/Compilation/positive/out/test058.out b/tests/Rust/Compilation/positive/out/test058.out new file mode 100644 index 0000000000..8a1c3eb605 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test058.out @@ -0,0 +1 @@ +7550 diff --git a/tests/Rust/Compilation/positive/out/test059.out b/tests/Rust/Compilation/positive/out/test059.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test059.out @@ -0,0 +1 @@ +11 diff --git a/tests/Rust/Compilation/positive/out/test060.out b/tests/Rust/Compilation/positive/out/test060.out new file mode 100644 index 0000000000..d81cc0710e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test060.out @@ -0,0 +1 @@ +42 diff --git a/tests/Rust/Compilation/positive/out/test062.out b/tests/Rust/Compilation/positive/out/test062.out new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test062.out @@ -0,0 +1 @@ +1 diff --git a/tests/Rust/Compilation/positive/out/test064.out b/tests/Rust/Compilation/positive/out/test064.out new file mode 100644 index 0000000000..81b5c5d06c --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test064.out @@ -0,0 +1 @@ +37 diff --git a/tests/Rust/Compilation/positive/out/test065.out b/tests/Rust/Compilation/positive/out/test065.out new file mode 100644 index 0000000000..d81cc0710e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test065.out @@ -0,0 +1 @@ +42 diff --git a/tests/Rust/Compilation/positive/out/test066.out b/tests/Rust/Compilation/positive/out/test066.out new file mode 100644 index 0000000000..573541ac97 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test066.out @@ -0,0 +1 @@ +0 diff --git a/tests/Rust/Compilation/positive/out/test067.out b/tests/Rust/Compilation/positive/out/test067.out new file mode 100644 index 0000000000..64bb6b746d --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test067.out @@ -0,0 +1 @@ +30 diff --git a/tests/Rust/Compilation/positive/out/test068.out b/tests/Rust/Compilation/positive/out/test068.out new file mode 100644 index 0000000000..64bb6b746d --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test068.out @@ -0,0 +1 @@ +30 diff --git a/tests/Rust/Compilation/positive/out/test069.out b/tests/Rust/Compilation/positive/out/test069.out new file mode 100644 index 0000000000..d00491fd7e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test069.out @@ -0,0 +1 @@ +1 diff --git a/tests/Rust/Compilation/positive/out/test070.out b/tests/Rust/Compilation/positive/out/test070.out new file mode 100644 index 0000000000..e9bae3d88e --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test070.out @@ -0,0 +1 @@ +1463 diff --git a/tests/Rust/Compilation/positive/out/test071.out b/tests/Rust/Compilation/positive/out/test071.out new file mode 100644 index 0000000000..9030a57f28 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test071.out @@ -0,0 +1 @@ +1528 diff --git a/tests/Rust/Compilation/positive/out/test072.out b/tests/Rust/Compilation/positive/out/test072.out new file mode 100644 index 0000000000..f599e28b8a --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test072.out @@ -0,0 +1 @@ +10 diff --git a/tests/Rust/Compilation/positive/out/test073.out b/tests/Rust/Compilation/positive/out/test073.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test073.out @@ -0,0 +1 @@ +11 diff --git a/tests/Rust/Compilation/positive/out/test074.out b/tests/Rust/Compilation/positive/out/test074.out new file mode 100644 index 0000000000..eb3e83f932 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test074.out @@ -0,0 +1 @@ +-1085550836599839364109196834928521031686932164599479009991927616840761606155 diff --git a/tests/Rust/Compilation/positive/out/test075.out b/tests/Rust/Compilation/positive/out/test075.out new file mode 100644 index 0000000000..b2823ee522 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test075.out @@ -0,0 +1 @@ +1725896553192394782543714999351211125700806599592244002323760583399227747069 diff --git a/tests/Rust/Compilation/positive/out/test076.out b/tests/Rust/Compilation/positive/out/test076.out new file mode 100644 index 0000000000..2c8ff669b5 --- /dev/null +++ b/tests/Rust/Compilation/positive/out/test076.out @@ -0,0 +1 @@ +-239707713998411894939692760394344630800925432259393396371649456207189656012 diff --git a/tests/Rust/Compilation/positive/test001.juvix b/tests/Rust/Compilation/positive/test001.juvix new file mode 100644 index 0000000000..c52a9268c9 --- /dev/null +++ b/tests/Rust/Compilation/positive/test001.juvix @@ -0,0 +1,5 @@ +module test001; + +import Stdlib.Prelude open; + +main : Nat := 5 + 2 * 3; diff --git a/tests/Rust/Compilation/positive/test002.juvix b/tests/Rust/Compilation/positive/test002.juvix new file mode 100644 index 0000000000..59485b0ea2 --- /dev/null +++ b/tests/Rust/Compilation/positive/test002.juvix @@ -0,0 +1,5 @@ +module test002; + +import Stdlib.Prelude open; + +main : Nat := \ {x y z := z + x * y} 2 3 5; diff --git a/tests/Rust/Compilation/positive/test003.juvix b/tests/Rust/Compilation/positive/test003.juvix new file mode 100644 index 0000000000..535c119129 --- /dev/null +++ b/tests/Rust/Compilation/positive/test003.juvix @@ -0,0 +1,14 @@ +-- Integer arithmetic +module test003; + +{- + +Multiline comment + +{- nested comments work -} + +-} + +import Stdlib.Prelude open; + +main : Nat := mod 3 2 + div 18 4 + mod 18 4 + div 16 4 + mod 16 4; diff --git a/tests/Rust/Compilation/positive/test005.juvix b/tests/Rust/Compilation/positive/test005.juvix new file mode 100644 index 0000000000..4747cdbde3 --- /dev/null +++ b/tests/Rust/Compilation/positive/test005.juvix @@ -0,0 +1,19 @@ +-- Higher-order functions +module test005; + +import Stdlib.Prelude open; + +S {A B C} (x : A → B → C) (y : A → B) (z : A) : C := + x z (y z); + +K {A B} (x : A) (_ : B) : A := x; + +I {A} : A → A := S K (K {_} {Bool}); + +main : Nat := + I 1 + + I I 1 + + I (I 1) + + I I I 1 + + I (I I) I (I I I) 1 + + I I I (I I I (I I)) I (I I) I I I 1; diff --git a/tests/Rust/Compilation/positive/test006.juvix b/tests/Rust/Compilation/positive/test006.juvix new file mode 100644 index 0000000000..2032d091a4 --- /dev/null +++ b/tests/Rust/Compilation/positive/test006.juvix @@ -0,0 +1,13 @@ +-- if-then-else and lazy boolean operators +module test006; + +import Stdlib.Prelude open; + +terminating +loop : Nat := loop; + +main : Nat := + if (3 > 0) 1 loop + + if (2 < 1) loop (if (7 >= 8) loop 1) + + if (2 > 0 || loop == 0) 1 0 + + if (2 < 0 && loop == 0) 1 0; diff --git a/tests/Rust/Compilation/positive/test007.juvix b/tests/Rust/Compilation/positive/test007.juvix new file mode 100644 index 0000000000..998b804c07 --- /dev/null +++ b/tests/Rust/Compilation/positive/test007.juvix @@ -0,0 +1,20 @@ +-- pattern matching and lambda-case +module test007; + +import Stdlib.Prelude open; + +map' {A B} (f : A → B) : List A → List B := + \ { + | nil := nil + | (h :: t) := f h :: map' f t + }; + +lst : List Nat := 0 :: 1 :: nil; + +main : Nat := + if (null lst) 1 0 + + if (null (nil {Nat})) 1 0 + + head 1 lst + + head 0 (tail lst) + + head 0 (tail (map ((+) 1) lst)) + + head 0 (tail (map' ((+) 1) lst)); diff --git a/tests/Rust/Compilation/positive/test008.juvix b/tests/Rust/Compilation/positive/test008.juvix new file mode 100644 index 0000000000..11290705be --- /dev/null +++ b/tests/Rust/Compilation/positive/test008.juvix @@ -0,0 +1,10 @@ +-- recursion +module test008; + +import Stdlib.Prelude open; + +sum : Nat → Nat + | zero := 0 + | (suc x) := suc x + sum x; + +main : Nat := sum 10000; diff --git a/tests/Rust/Compilation/positive/test009.juvix b/tests/Rust/Compilation/positive/test009.juvix new file mode 100644 index 0000000000..7f5600e9de --- /dev/null +++ b/tests/Rust/Compilation/positive/test009.juvix @@ -0,0 +1,18 @@ +-- tail recursion +module test009; + +import Stdlib.Prelude open; + +sum' (acc : Nat) : Nat → Nat + | zero := acc + | (suc x) := sum' (suc x + acc) x; + +sum : Nat → Nat := sum' 0; + +fact' (acc : Nat) : Nat → Nat + | zero := acc + | (suc x) := fact' (acc * suc x) x; + +fact : Nat → Nat := fact' 1; + +main : Nat := sum 10000 + fact 5 + fact 10 + fact 12; diff --git a/tests/Rust/Compilation/positive/test010.juvix b/tests/Rust/Compilation/positive/test010.juvix new file mode 100644 index 0000000000..63f91b3997 --- /dev/null +++ b/tests/Rust/Compilation/positive/test010.juvix @@ -0,0 +1,22 @@ +-- let +module test010; + +import Stdlib.Prelude open; + +main : Nat := + let + x : Nat := 1; + in let + x1 : + Nat := + x + + let + x2 : Nat := 2; + in x2; + in let + x3 : Nat := x1 * x1; + in let + y : Nat := x3 + 2; + in let + z : Nat := x3 + y; + in x + y + z; diff --git a/tests/Rust/Compilation/positive/test013.juvix b/tests/Rust/Compilation/positive/test013.juvix new file mode 100644 index 0000000000..b0d63c9a81 --- /dev/null +++ b/tests/Rust/Compilation/positive/test013.juvix @@ -0,0 +1,16 @@ +-- functions returning functions with variable capture +module test013; + +import Stdlib.Prelude open; + +f : Nat → Nat → Nat + | x := + if + (x == 6) + λ {_ := 0} + (if + (x == 5) + λ {_ := 1} + (if (x == 10) λ {_ := λ {x := x} 2} λ {x := x})); + +main : Nat := f 5 6 + f 6 5 + f 10 5 + f 11 5; diff --git a/tests/Rust/Compilation/positive/test014.juvix b/tests/Rust/Compilation/positive/test014.juvix new file mode 100644 index 0000000000..0ad36179ab --- /dev/null +++ b/tests/Rust/Compilation/positive/test014.juvix @@ -0,0 +1,36 @@ +-- arithmetic +module test014; + +import Stdlib.Prelude open; + +f (x y : Nat) : Nat := x + y; + +g (x y : Nat) : Nat := sub (x + 21) (y * 7); + +h (f : Nat → Nat → Nat) (y z : Nat) : Nat := f y y * z; + +x : Nat := 5; + +y : Nat := 17; + +func (x : Nat) : Nat := x + 4; + +z : Nat := 0; + +vx : Nat := 30; + +vy : Nat := 7; + +main : Nat := + func (div y x) + + -- 17 div 5 + 4 = 7 + (y + + x * z) + + -- 17 + (vx + + vy * (z + 1)) + + -- 37 + f + (h g 2 3) + 4; +-- (g 2 2) * 3 + 4 = (2+21-2*7)*3 + 4 = 9*3 + 4 = 27+4 = 31 diff --git a/tests/Rust/Compilation/positive/test015.juvix b/tests/Rust/Compilation/positive/test015.juvix new file mode 100644 index 0000000000..6c6486d628 --- /dev/null +++ b/tests/Rust/Compilation/positive/test015.juvix @@ -0,0 +1,43 @@ +-- local functions with free variables +module test015; + +import Stdlib.Prelude open; + +terminating +f : Nat → Nat → Nat + | x := + let + g (y : Nat) : Nat := x + y; + in if + (x == 0) + (f 10) + (if (x < 10) λ {y := g (f (sub x 1) y)} g); + +g (x : Nat) (h : Nat → Nat) : Nat := x + h x; + +terminating +h : Nat → Nat + | zero := 0 + | (suc x) := g x h; + +main : Nat := + f 100 500 + + -- 600 + f + 5 + 0 + + -- 25 + f + 5 + 5 + + -- 30 + h + 10 + + -- 45 + g + 10 + h + + -- 55 + g + 3 + (f 10); diff --git a/tests/Rust/Compilation/positive/test016.juvix b/tests/Rust/Compilation/positive/test016.juvix new file mode 100644 index 0000000000..dc6af79858 --- /dev/null +++ b/tests/Rust/Compilation/positive/test016.juvix @@ -0,0 +1,14 @@ +-- recursion through higher-order functions +module test016; + +import Stdlib.Prelude open; + +g (f : Nat → Nat) : Nat → Nat + | zero := 0 + | (suc x) := f x; + +terminating +f (x : Nat) : Nat := x + g f x; + +main : Nat := f 10; +-- 55 diff --git a/tests/Rust/Compilation/positive/test017.juvix b/tests/Rust/Compilation/positive/test017.juvix new file mode 100644 index 0000000000..3e9d8a7b3d --- /dev/null +++ b/tests/Rust/Compilation/positive/test017.juvix @@ -0,0 +1,15 @@ +-- tail recursion through higher-order functions +module test017; + +import Stdlib.Prelude open; + +sumb (acc : Nat) (f : Nat → Nat → Nat) : Nat → Nat + | zero := acc + | (suc x) := f acc x; + +terminating +sum' (acc x : Nat) : Nat := sumb (x + acc) sum' x; + +sum : Nat → Nat := sum' 0; + +main : Nat := sum 10000; diff --git a/tests/Rust/Compilation/positive/test018.juvix b/tests/Rust/Compilation/positive/test018.juvix new file mode 100644 index 0000000000..081f17492c --- /dev/null +++ b/tests/Rust/Compilation/positive/test018.juvix @@ -0,0 +1,16 @@ +-- higher-order functions & recursion +module test018; + +import Stdlib.Prelude open; + +f : (Nat → Nat) → Nat + | g := g 5; + +h : Nat → Nat → Nat + | x z := x + z; + +u : Nat → Nat + | x := f (h 4) + x; + +main : Nat := u 2; + diff --git a/tests/Rust/Compilation/positive/test019.juvix b/tests/Rust/Compilation/positive/test019.juvix new file mode 100644 index 0000000000..2f8313399f --- /dev/null +++ b/tests/Rust/Compilation/positive/test019.juvix @@ -0,0 +1,11 @@ +-- self-application +module test019; + +import Stdlib.Prelude open; + +-- change this to a lambda once we have type annotations for lambdas +app : ({A : Type} → A → A) → {A : Type} → A → A + | x := x x; + +main : Nat := app id (3 + 4); + diff --git a/tests/Rust/Compilation/positive/test020.juvix b/tests/Rust/Compilation/positive/test020.juvix new file mode 100644 index 0000000000..4cd552d220 --- /dev/null +++ b/tests/Rust/Compilation/positive/test020.juvix @@ -0,0 +1,25 @@ +-- recursive functions +module test020; + +import Stdlib.Prelude open; + +-- McCarthy's 91 function +terminating +f91 : Nat → Nat + | n := if (n > 100) (sub n 10) (f91 (f91 (n + 11))); + +-- subtraction by increments +terminating +subp : Nat → Nat → Nat + | i j := if (i == j) 0 (subp i (j + 1) + 1); + +main : Nat := + f91 101 + + f91 95 + + f91 16 + + f91 5 + + subp 101 1 + + subp 11 5 + + subp 10 4 + + subp 1000 600 + + subp 10000 6000; diff --git a/tests/Rust/Compilation/positive/test021.juvix b/tests/Rust/Compilation/positive/test021.juvix new file mode 100644 index 0000000000..5d178f2db4 --- /dev/null +++ b/tests/Rust/Compilation/positive/test021.juvix @@ -0,0 +1,16 @@ +-- fast exponentiation +module test021; + +import Stdlib.Prelude open; + +terminating +power' : Nat → Nat → Nat → Nat + | acc a b := + if + | b == 0 := acc + | mod b 2 == 0 := power' acc (a * a) (div b 2) + | else := power' (acc * a) (a * a) (div b 2); + +power : Nat → Nat → Nat := power' 1; + +main : Nat := power 2 3 + power 3 7 + power 5 7; diff --git a/tests/Rust/Compilation/positive/test022.juvix b/tests/Rust/Compilation/positive/test022.juvix new file mode 100644 index 0000000000..adafdf5b46 --- /dev/null +++ b/tests/Rust/Compilation/positive/test022.juvix @@ -0,0 +1,16 @@ +-- lists +module test022; + +import Stdlib.Prelude open; + +gen : Nat → List Nat + | zero := nil + | n@(suc m) := n :: gen m; + +sum : Nat → Nat + | n := foldl (+) 0 (gen n); + +sum' : Nat → Nat + | n := foldr (+) 0 (gen n); + +main : Nat := sum 10000 + sum' 10000; diff --git a/tests/Rust/Compilation/positive/test023.juvix b/tests/Rust/Compilation/positive/test023.juvix new file mode 100644 index 0000000000..26cb5429ab --- /dev/null +++ b/tests/Rust/Compilation/positive/test023.juvix @@ -0,0 +1,19 @@ +-- mutual recursion +module test023; + +import Stdlib.Prelude open; + +terminating +f : Nat → Nat + + | x := if (x < 1) 1 (2 * x + g (sub x 1)); + +terminating +g : Nat → Nat + | x := if (x < 1) 1 (x + h (sub x 1)); + +terminating +h : Nat → Nat + | x := if (x < 1) 1 (x * f (sub x 1)); + +main : Nat := f 5 + f 10 + f 20; diff --git a/tests/Rust/Compilation/positive/test024.juvix b/tests/Rust/Compilation/positive/test024.juvix new file mode 100644 index 0000000000..83d3acdda3 --- /dev/null +++ b/tests/Rust/Compilation/positive/test024.juvix @@ -0,0 +1,46 @@ +-- nested binders with variable capture +module test024; + +import Stdlib.Prelude open; + +type Tree := + | leaf : Tree + | node : Tree → Tree → Tree; + +gen : Nat → Tree + | zero := leaf + | (suc zero) := node leaf leaf + | (suc (suc n')) := node (gen n') (gen (suc n')); + +g : Tree → Tree + + | leaf := leaf + | (node l r) := if (isNode l) r (node r l); + +terminating +f : Tree → Nat + | leaf := 1 + | (node l' r') := + let + l : Tree := g l'; + r : Tree := g r'; + terminating + a : + Nat := + case l of + | leaf := 1 + | node l r := f l + f r; + terminating + b : + Nat := + case r of + | node l r := f l + f r + | _ := 2; + in a * b; + +isNode : Tree → Bool + | (node _ _) := true + | leaf := false; + +main : Nat := f (gen 10); + diff --git a/tests/Rust/Compilation/positive/test025.juvix b/tests/Rust/Compilation/positive/test025.juvix new file mode 100644 index 0000000000..ceb84cd312 --- /dev/null +++ b/tests/Rust/Compilation/positive/test025.juvix @@ -0,0 +1,16 @@ +-- Euclid's algorithm +module test025; + +import Stdlib.Prelude open; + +terminating +gcd : Nat → Nat → Nat + | a b := + if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a)); + +main : Nat := + gcd (3 * 7 * 2) (7 * 2 * 11) + + gcd (3 * 7 * 2 * 11 * 5) (7 * 2 * 5) + + gcd 3 7 + + gcd 7 3 + + gcd (11 * 7 * 3) (2 * 5 * 13); diff --git a/tests/Rust/Compilation/positive/test026.juvix b/tests/Rust/Compilation/positive/test026.juvix new file mode 100644 index 0000000000..f3cc2b1a6c --- /dev/null +++ b/tests/Rust/Compilation/positive/test026.juvix @@ -0,0 +1,56 @@ +-- functional queues +module test026; + +import Stdlib.Prelude open; + +type Queue (A : Type) := queue : List A → List A → Queue A; + +qfst : {A : Type} → Queue A → List A + | (queue x _) := x; + +qsnd : {A : Type} → Queue A → List A + | (queue _ x) := x; + +front {{Partial}} : {A : Type} → Queue A → A + | q := phead (qfst q); + +pop_front : {A : Type} → Queue A → Queue A + | {A} q := + let + q' : Queue A := queue (tail (qfst q)) (qsnd q); + in case qfst q' of + | nil := queue (reverse (qsnd q')) nil + | _ := q'; + +push_back : {A : Type} → Queue A → A → Queue A + | q x := + case qfst q of + | nil := queue (x :: nil) (qsnd q) + | q' := queue q' (x :: qsnd q); + +is_empty : {A : Type} → Queue A → Bool + | q := + case qfst q of + | nil := + case qsnd q of { + | nil := true + | _ := false + } + | _ := false; + +empty : {A : Type} → Queue A := queue nil nil; + +terminating +g {{Partial}} : List Nat → Queue Nat → List Nat + | acc q := + if (is_empty q) acc (g (front q :: acc) (pop_front q)); + +f {{Partial}} : Nat → Queue Nat → List Nat + | zero q := g nil q + | n@(suc n') q := f n' (push_back q n); + +sum : List Nat → Nat + | nil := 0 + | (h :: t) := h + sum t; + +main : Nat := sum (runPartial λ {{{_}} := f 100 empty}); diff --git a/tests/Rust/Compilation/positive/test028.juvix b/tests/Rust/Compilation/positive/test028.juvix new file mode 100644 index 0000000000..c014a3a584 --- /dev/null +++ b/tests/Rust/Compilation/positive/test028.juvix @@ -0,0 +1,46 @@ +-- streams without memoization +module test028; + +import Stdlib.Prelude open; + +type Stream := cons : Nat → (Unit → Stream) → Stream; + +force : (Unit → Stream) → Stream + | f := f unit; + +terminating +sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream + | p s unit := + case force s of {cons h t := + if (p h) (cons h (sfilter p t)) (force (sfilter p t))}; + +shead : Stream → Nat + | (cons h _) := h; + +stail : Stream → Unit → Stream + | (cons _ t) := t; + +snth : Nat → (Unit → Stream) → Nat + | zero s := shead (force s) + | (suc n) s := snth n (stail (force s)); + +terminating +numbers : Nat → Unit → Stream + | n unit := cons n (numbers (suc n)); + +indivisible : Nat → Nat → Bool + | n x := not (mod x n == 0); + +terminating +eratostenes : (Unit → Stream) → Unit → Stream + | s unit := + case force s of {cons n t := + cons n (eratostenes (sfilter (indivisible n) t))}; + +primes : Unit → Stream := eratostenes (numbers 2); + +main : Nat := + snth 10 primes + + snth 50 primes + + snth 100 primes + + snth 200 primes; diff --git a/tests/Rust/Compilation/positive/test029.juvix b/tests/Rust/Compilation/positive/test029.juvix new file mode 100644 index 0000000000..43cd0299ef --- /dev/null +++ b/tests/Rust/Compilation/positive/test029.juvix @@ -0,0 +1,16 @@ +-- Ackermann function +module test029; + +import Stdlib.Prelude open; + +ack : Nat → Nat → Nat + | zero n := n + 1 + | (suc m) zero := ack m 1 + | (suc m) (suc n) := ack m (ack (suc m) n); + +main : Nat := + ack 0 7 + + ack 1 7 + + ack 1 13 + + ack 2 7 + + ack 2 13; diff --git a/tests/Rust/Compilation/positive/test030.juvix b/tests/Rust/Compilation/positive/test030.juvix new file mode 100644 index 0000000000..b5434b9b29 --- /dev/null +++ b/tests/Rust/Compilation/positive/test030.juvix @@ -0,0 +1,23 @@ +-- Ackermann function (higher-order definition) +module test030; + +import Stdlib.Prelude open hiding {iterate}; + +iterate : {A : Type} → (A → A) → Nat → A → A + -- clauses with differing number of patterns not yet supported + -- iterate f zero x := x; + | f zero := id + | f (suc n) := f ∘ iterate f n; + +plus : Nat → Nat → Nat := iterate suc; + +mult : Nat → Nat → Nat + | m n := iterate (plus n) m 0; + +exp : Nat → Nat → Nat + | m n := iterate (mult m) n 1; + +ackermann : Nat → Nat → Nat + | m := iterate λ {f n := iterate f (suc n) 1} m suc; + +main : Nat := plus 3 7 + mult 3 7 + exp 3 7 + ackermann 2 13; diff --git a/tests/Rust/Compilation/positive/test032.juvix b/tests/Rust/Compilation/positive/test032.juvix new file mode 100644 index 0000000000..eb6fe52591 --- /dev/null +++ b/tests/Rust/Compilation/positive/test032.juvix @@ -0,0 +1,58 @@ +-- merge sort +module test032; + +import Stdlib.Prelude open; + +split : {A : Type} → Nat → List A → List A × List A + | zero xs := nil, xs + | (suc n) nil := nil, nil + | (suc n) (x :: xs) := + case split n xs of {l1, l2 := x :: l1, l2}; + +terminating +merge' : List Nat → List Nat → List Nat + | nil ys := ys + | xs nil := xs + | xs@(x :: xs') ys@(y :: ys') := + if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys'); + +terminating +sort : List Nat → List Nat + | xs := + let + n : Nat := length xs; + in if + (n <= 1) + xs + case split (div n 2) xs of {l1, l2 := + merge' (sort l1) (sort l2)}; + +terminating +uniq : List Nat → List Nat + | nil := nil + | (x :: nil) := x :: nil + | (x :: xs@(x' :: _)) := + if (x == x') (uniq xs) (x :: uniq xs); + +gen : List Nat → Nat → (Nat → Nat) → List Nat + | acc zero f := acc + | acc (suc n) f := gen (f (suc n) :: acc) n f; + +gen2 : List (List Nat) → Nat → Nat → List (List Nat) + | acc m zero := acc + | acc m (suc n) := + gen2 (gen nil m ((+) (suc n)) :: acc) m n; + +printListNatLn : List Nat → IO + | nil := printStringLn "nil" + | (x :: xs) := + printNat x >> printString " :: " >> printListNatLn xs; + +sum : List Nat → Nat + | nil := 0 + | (h :: t) := h + sum t; + +main : Nat := + sum (take 10 (uniq (sort (flatten (gen2 nil 6 40))))) + + sum (take 10 (uniq (sort (flatten (gen2 nil 9 80))))) + + sum (take 10 (uniq (sort (flatten (gen2 nil 6 80))))); diff --git a/tests/Rust/Compilation/positive/test033.juvix b/tests/Rust/Compilation/positive/test033.juvix new file mode 100644 index 0000000000..e2be0043f6 --- /dev/null +++ b/tests/Rust/Compilation/positive/test033.juvix @@ -0,0 +1,35 @@ +-- eta-expansion of builtins and constructors +module test033; + +import Stdlib.Prelude open; + +f : (Nat → Nat) → Nat + | g := g 2; + +f' : Nat → Nat + | x := f ((+) x); + +g : (Nat → Nat × Nat) → Nat × Nat + | f := f 2; + +g' : Nat → Nat × Nat + | x := g ((,) x); + +f1' : Nat → Nat → Nat + | x y := f ((+) (div x y)); + +g1' : Nat → Nat → Nat × Nat + | x y := g ((,) (div x y)); + +h : (Nat → Nat → Nat × Nat) → Nat × Nat + | f := f 1 2; + +main : Nat := + f' 7 + + fst (g' 7) + + snd (g' 7) + + f1' 7 2 + + fst (g1' 7 2) + + snd (g1' 7 2) + + fst (h (,)) + + snd (h (,)); diff --git a/tests/Rust/Compilation/positive/test034.juvix b/tests/Rust/Compilation/positive/test034.juvix new file mode 100644 index 0000000000..6cfd93686b --- /dev/null +++ b/tests/Rust/Compilation/positive/test034.juvix @@ -0,0 +1,25 @@ +-- recursive let +module test034; + +import Stdlib.Prelude open; + +sum : Nat → Nat := + let + sum' : Nat → Nat := + λ { + zero := zero + | (suc n) := suc n + sum' n + }; + in sum'; + +mutrec : Nat := + let + terminating + f (x : Nat) : Nat := if (x < 1) 1 (g (sub x 1) + 2 * x); + terminating + g (x : Nat) : Nat := if (x < 1) 1 (x + h (sub x 1)); + terminating + h (x : Nat) : Nat := if (x < 1) 1 (x * f (sub x 1)); + in f 5 + f 10 + g 5 + h 5; + +main : Nat := sum 1000 + mutrec; diff --git a/tests/Rust/Compilation/positive/test035.juvix b/tests/Rust/Compilation/positive/test035.juvix new file mode 100644 index 0000000000..75a9d3ffe9 --- /dev/null +++ b/tests/Rust/Compilation/positive/test035.juvix @@ -0,0 +1,58 @@ +-- pattern matching +module test035; + +import Stdlib.Prelude open; + +lgen : Nat → List Nat + | zero := nil + | (suc n) := suc n :: lgen n; + +sum2 : List Nat → List Nat + | (x :: y :: xs) := x + y :: sum2 (y :: xs) + | xs := xs; + +type Tree := + | leaf : Tree + | node : Tree -> Tree -> Tree; + +gen : Nat → Tree + | zero := leaf + | (suc zero) := node leaf leaf + | (suc (suc n)) := node (gen n) (gen (suc n)); + +terminating +f : Tree → Nat + | leaf := 1 + | (node l r) := + case g l, g r of { + | leaf, leaf := 3 + | node l r, leaf := mod ((f l + f r) * 2) 20000 + | node l1 r1, node l2 r2 := + mod ((f l1 + f r1) * (f l2 + f r2)) 20000 + | _, node l r := mod (f l + f r) 20000 + }; + +g : Tree → Tree + | leaf := leaf + | (node (node _ _) r) := r + | (node l r) := node r l; + +h : Nat -> Nat + | (suc (suc (suc (suc n)))) := n + | _ := 0; + +printListNatLn : List Nat → IO + | nil := printStringLn "nil" + | (x :: xs) := + printNat x >> printString " :: " >> printListNatLn xs; + +main : Nat := + head 0 (sum2 (lgen 5)) + + f (gen 10) + + f (gen 15) + + f (gen 16) + + f (gen 17) + + f (gen 18) + + f (gen 20) + + h 5 + + h 3; diff --git a/tests/Rust/Compilation/positive/test036.juvix b/tests/Rust/Compilation/positive/test036.juvix new file mode 100644 index 0000000000..540f26bed5 --- /dev/null +++ b/tests/Rust/Compilation/positive/test036.juvix @@ -0,0 +1,24 @@ +-- eta-expansion +module test036; + +import Stdlib.Prelude open; + +expand : {A : Type} → A → Nat → A + | f x := f; + +f : Nat → Nat := suc; + +g : Nat → Nat → Nat + | z := f ∘ flip sub z; + +g' : Nat → Nat → Nat + | z := f ∘ λ {x := sub x z}; + +h : Nat → Nat := f ∘ g 3; + +j : Nat → Nat → Nat := g'; + +k : Nat → Nat → Nat → Nat := expand j; + +main : Nat := h 13 + j 2 3 + k 9 4 7; + diff --git a/tests/Rust/Compilation/positive/test037.juvix b/tests/Rust/Compilation/positive/test037.juvix new file mode 100644 index 0000000000..92ba7034d5 --- /dev/null +++ b/tests/Rust/Compilation/positive/test037.juvix @@ -0,0 +1,23 @@ +-- Applications with lets and cases in function position +module test037; + +import Stdlib.Prelude open; + +f (l : List ((Nat → Nat) → Nat → Nat)) : Nat := + case l of { + | x :: _ := x + | nil := id + } + (let + y : Nat → Nat := id; + in (let + z : (Nat → Nat) → Nat → Nat := id; + in case l of { + | _ :: _ := id + | _ := id + } + z) + y) + 7; + +main : Nat := f (λ {| x y := x y + 2} :: nil); diff --git a/tests/Rust/Compilation/positive/test038.juvix b/tests/Rust/Compilation/positive/test038.juvix new file mode 100644 index 0000000000..56d57bbe39 --- /dev/null +++ b/tests/Rust/Compilation/positive/test038.juvix @@ -0,0 +1,11 @@ +-- Simple case expression +module test038; + +import Stdlib.Prelude open; + +main : Nat := + case 1, 2 of { + | suc _, zero := 0 + | suc _, suc x := x + | _ := 19 + }; diff --git a/tests/Rust/Compilation/positive/test039.juvix b/tests/Rust/Compilation/positive/test039.juvix new file mode 100644 index 0000000000..76d471bd28 --- /dev/null +++ b/tests/Rust/Compilation/positive/test039.juvix @@ -0,0 +1,17 @@ +-- Mutually recursive let expressions +module test039; + +import Stdlib.Prelude open; + +main : Nat := + let + Ty : Type := Nat; + odd : _ + | zero := false + | (suc n) := not (even n); + unused : _ := 123; + even : _ + | zero := true + | (suc n) := not (odd n); + plusOne (n : Ty) : Ty := n + 1; + in if (odd (plusOne 13)) 1 0 + if (even (plusOne 12)) 1 0; diff --git a/tests/Rust/Compilation/positive/test040.juvix b/tests/Rust/Compilation/positive/test040.juvix new file mode 100644 index 0000000000..2d5fb89f25 --- /dev/null +++ b/tests/Rust/Compilation/positive/test040.juvix @@ -0,0 +1,17 @@ +-- pattern matching nullary constructor +module test040; + +import Stdlib.System.IO open; +import Stdlib.Data.Bool open; +import Stdlib.Data.Nat open; + +type Unit := + | unit : Unit; + +type Foo (A : Type) := + | foo : Unit -> A -> Foo A; + +f : {A : Type} -> Foo A -> A + | (foo unit a) := a; + +main : Nat := if (f (foo unit true)) 1 0; diff --git a/tests/Rust/Compilation/positive/test045.juvix b/tests/Rust/Compilation/positive/test045.juvix new file mode 100644 index 0000000000..2768de61de --- /dev/null +++ b/tests/Rust/Compilation/positive/test045.juvix @@ -0,0 +1,19 @@ +-- implicit builtin bool +-- Builtin nat requires builtin bool when translated to integers, because +-- matching is translated to comparison operators and cases on booleans. +module test045; + +builtin nat +type Nat := + | zero : Nat + | suc : Nat → Nat; + +syntax fixity additive := binary {assoc := left}; + +syntax operator + additive; + ++ : Nat → Nat → Nat + | zero b := b + | (suc a) b := suc (a + b); + +main : Nat := suc zero + suc (suc (suc zero)); diff --git a/tests/Rust/Compilation/positive/test046.juvix b/tests/Rust/Compilation/positive/test046.juvix new file mode 100644 index 0000000000..ff692742fd --- /dev/null +++ b/tests/Rust/Compilation/positive/test046.juvix @@ -0,0 +1,17 @@ +-- polymorphic type arguments +module test046; + +import Stdlib.Data.Nat open; +import Stdlib.Function open; + +Ty : Type := {B : Type} -> B -> B; + +id' : Ty + | {_} x := x; + +-- In PR https://github.com/anoma/juvix/pull/2545 we had to slightly modify +-- the `fun` definition. The previous version is kept here as a comment. +-- fun : {A : Type} → A → Ty := id λ {_ := id'}; +fun {A : Type} : A → Ty := id { _ -> {C : Type} → C → C } λ {_ := id'}; + +main : Nat := fun 5 {Nat} 7; diff --git a/tests/Rust/Compilation/positive/test047.juvix b/tests/Rust/Compilation/positive/test047.juvix new file mode 100644 index 0000000000..90ee620a67 --- /dev/null +++ b/tests/Rust/Compilation/positive/test047.juvix @@ -0,0 +1,43 @@ +-- local modules +module test047; + +import Stdlib.Prelude open; + +module Local; + t : Nat := 2; + + module Nested; + t : Nat := 3; + + -- module shadowing + module Nested; + t : Nat := 5; + end; + + module Nested2; + t : Nat := 7; + + -- module shadowing + module Nested; + t : Nat := 11; + end; + end; + end; +end; + +open Local; + +module Public; + open Nested public; +end; + +tt : Nat := t; + +x : Nat := + t + * Local.t + * Local.Nested.t + * Nested.Nested2.Nested.t + * Public.Nested.t; + +main : Nat := x; diff --git a/tests/Rust/Compilation/positive/test050.juvix b/tests/Rust/Compilation/positive/test050.juvix new file mode 100644 index 0000000000..0543155f0a --- /dev/null +++ b/tests/Rust/Compilation/positive/test050.juvix @@ -0,0 +1,11 @@ +-- Pattern matching with integers +module test050; + +import Stdlib.Prelude open; + +f : Int -> Int + | (negSuc zero) := ofNat 0 + | (negSuc m@(suc n)) := ofNat n + ofNat m + | (ofNat n) := neg (ofNat n - ofNat 7); + +main : Int := f -10 - f 1 + f -1; diff --git a/tests/Rust/Compilation/positive/test053.juvix b/tests/Rust/Compilation/positive/test053.juvix new file mode 100644 index 0000000000..ef4dbfc0f5 --- /dev/null +++ b/tests/Rust/Compilation/positive/test053.juvix @@ -0,0 +1,36 @@ +-- Inlining +module test053; + +import Stdlib.Prelude open; + +{-# inline: 2 #-} +mycompose : {A B C : Type} -> (B -> C) -> (A -> B) -> A -> C + | f g x := f (g x); + +{-# inline: true #-} +myconst : {A B : Type} -> A -> B -> A + | x _ := x; + +{-# inline: 1 #-} +myflip : {A B C : Type} -> (A -> B -> C) -> B -> A -> C + | f b a := f a b; + +rumpa : {A : Type} -> (A -> A) -> A -> A + | {A} f a := + let + {-# inline: 1 #-} + go : Nat -> A -> A + | zero a := a + | (suc _) a := f a; + + {-# inline: false #-} + h (g : A -> A) : A := g a; + in h (go 10); + +main : Nat := + let + f : Nat -> Nat := mycompose λ {x := x + 1} λ {x := x * 2}; + g : Nat -> Nat -> Nat := myflip myconst; + {-# inline: false #-} + myid : Nat -> Nat := λ {x := x}; + in myid (f 3 + g 7 9 + rumpa myid 5); diff --git a/tests/Rust/Compilation/positive/test054.juvix b/tests/Rust/Compilation/positive/test054.juvix new file mode 100644 index 0000000000..aae917428a --- /dev/null +++ b/tests/Rust/Compilation/positive/test054.juvix @@ -0,0 +1,59 @@ +-- Iterators +module test054; + +import Stdlib.Prelude open; + +syntax iterator myfor; +myfor : {A B : Type} → (A → B → A) → A → List B → A := + foldl {_} {_}; + +syntax iterator mymap {init := 0}; +mymap : {A B : Type} → (A → B) → List A → List B + | f nil := nil + | f (x :: xs) := f x :: mymap f xs; + +sum : List Nat → Nat + | xs := myfor (acc := 0) (x in xs) {acc + x}; + +sum' : List Nat → Nat + | xs := myfor λ {acc x := acc + x} 0 xs; + +lst : List Nat := 1 :: 2 :: 3 :: 4 :: 5 :: nil; + +syntax iterator myfor2 {init := 1; range := 2}; +myfor2 + : {A B C : Type} + → (A → B → C → A) + → A + → List B + → List C + → A + | f acc xs ys := + myfor (acc' := acc) (x in xs) + myfor (acc'' := acc') (y in ys) + f acc'' x y; + +syntax iterator myzip2 {init := 2; range := 2}; +myzip2 + : {A A' B C : Type} + → (A → A' → B → C → A × A') + → A + → A' + → List B + → List C + → A × A' + | f a b xs ys := + myfor (acc, acc' := a, b) (x, y in zip xs ys) + f acc acc' x y; + +main : Nat := + sum lst + + sum' lst + + fst (myfor (a, b := 0, 0) (x in lst) b + x, a) + + (myfor2 (acc := 0) (x in lst; y in 1 :: 2 :: nil) + acc + x + y) + + fst + (myzip2 (a := 0; b := 0) (x in lst; y in reverse lst) + a + x * y, b + y) + + myfor (a := 0) (x, y in mymap (x in lst) {x, x + 1}) + a + x * y; diff --git a/tests/Rust/Compilation/positive/test056.juvix b/tests/Rust/Compilation/positive/test056.juvix new file mode 100644 index 0000000000..2981ae3b5d --- /dev/null +++ b/tests/Rust/Compilation/positive/test056.juvix @@ -0,0 +1,71 @@ +-- argument specialization +module test056; + +import Stdlib.Prelude open; + +{-# specialize: [f] #-} +mymap {A B} (f : A -> B) : List A -> List B + | nil := nil + | (x :: xs) := f x :: mymap f xs; + +{-# specialize: [2, 5], inline: false #-} +myf + : {A B : Type} + -> A + -> (A -> A -> B) + -> A + -> B + -> Bool + -> B + | a0 f a b true := f a0 a + | a0 f a b false := b; + +{-# inline: false #-} +myf' + : {A B : Type} -> A -> (A -> A -> A -> B) -> A -> B -> B + | a0 f a b := myf a0 (f a0) a b true; + +sum : List Nat -> Nat + | xs := for (acc := 0) (x in xs) {x + acc}; + +funa : {A : Type} -> (A -> A) -> A -> A + | {A} f a := + let + {-# specialize-by: [f] #-} + go : Nat -> A + | zero := a + | (suc n) := f (go n); + in go 10; + +{-# specialize: true #-} +type Additive A := mkAdditive {add : A -> A -> A}; + +type Multiplicative A := + mkMultiplicative {mul : A -> A -> A}; + +addNat : Additive Nat := mkAdditive (+); + +{-# specialize: true #-} +mulNat : Multiplicative Nat := mkMultiplicative (*); + +{-# inline: false #-} +fadd {A} (a : Additive A) (x y : A) : A := + Additive.add a x y; + +{-# inline: false #-} +fmul {A} (m : Multiplicative A) (x y : A) : A := + Multiplicative.mul m x y; + +main : Nat := + sum (mymap λ {x := x + 3} (1 :: 2 :: 3 :: 4 :: nil)) + + sum + (flatten + (mymap + (mymap λ {x := x + 2}) + ((1 :: nil) :: (2 :: 3 :: nil) :: nil))) + + myf 3 (*) 2 5 true + + myf 1 (+) 2 0 false + + myf' 7 (const (+)) 2 0 + + funa ((+) 1) 5 + + fadd addNat 1 2 + + fmul mulNat 1 2; diff --git a/tests/Rust/Compilation/positive/test057.juvix b/tests/Rust/Compilation/positive/test057.juvix new file mode 100644 index 0000000000..27cb228a1a --- /dev/null +++ b/tests/Rust/Compilation/positive/test057.juvix @@ -0,0 +1,13 @@ +-- case folding +module test057; + +import Stdlib.Prelude open; + +myfun : {A : Type} -> (A -> A -> A) -> A -> List A -> A + | f x xs := + case x :: xs of + | nil := x + | y :: nil := y + | y :: z :: _ := f y z; + +main : Nat := myfun (+) 1 (7 :: 3 :: nil); diff --git a/tests/Rust/Compilation/positive/test058.juvix b/tests/Rust/Compilation/positive/test058.juvix new file mode 100644 index 0000000000..662cdcd3fd --- /dev/null +++ b/tests/Rust/Compilation/positive/test058.juvix @@ -0,0 +1,13 @@ +-- ranges +module test058; + +import Stdlib.Prelude open hiding {for}; +import Stdlib.Data.Range open; + +sum (x : Nat) : Nat := + for (acc := 0) (n in 1 to x) {acc + n}; + +sum' (x : Nat) : Nat := + for (acc := 0) (n in 1 to x step 2) {acc + n}; + +main : Nat := sum 100 + sum' 100; diff --git a/tests/Rust/Compilation/positive/test059.juvix b/tests/Rust/Compilation/positive/test059.juvix new file mode 100644 index 0000000000..03a5be832f --- /dev/null +++ b/tests/Rust/Compilation/positive/test059.juvix @@ -0,0 +1,15 @@ +-- builtin list +module test059; + +import Stdlib.Prelude open hiding {head}; + +mylist : List Nat := [1; 2; 3 + 1]; + +mylist2 : List (List Nat) := [[10]; [2]; 3 + 1 :: nil]; + +head : {a : Type} -> a -> List a -> a + | a [] := a + | a [x; _] := x + | _ (h :: _) := h; + +main : Nat := head 50 mylist + head 50 (head [] mylist2); diff --git a/tests/Rust/Compilation/positive/test060.juvix b/tests/Rust/Compilation/positive/test060.juvix new file mode 100644 index 0000000000..6e306a3948 --- /dev/null +++ b/tests/Rust/Compilation/positive/test060.juvix @@ -0,0 +1,48 @@ +-- record updates and record patterns +module test060; + +import Stdlib.Prelude open hiding {fst}; + +type Triple (A B C : Type) := + mkTriple { + fst : A; + snd : B; + thd : C + }; + +type Pair (A B : Type) := + mkPair { + fst : A; + snd : B + }; + +sum : Triple Nat Nat Nat → Nat + | mkTriple@{fst; snd; thd} := fst + snd + thd; + +mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool + | mkPair@{fst := mkPair@{fst; snd := nil}; + snd := zero :: _} := fst + | x := case x of {_ := false}; + +main : Nat := + let + p : Triple Nat Nat Nat := mkTriple 2 2 2; + p' : Triple Nat Nat Nat := + p@Triple{ + fst := fst + 1; + snd := snd * 3 + thd + fst + }; + f : Triple Nat Nat Nat -> Triple Nat Nat Nat := + (@Triple{fst := fst * 10}); + in sum $ if + (mf + mkPair@{ + fst := mkPair true nil; + snd := 0 :: nil + }) + (f p') + mkTriple@{ + fst := 0; + thd := 0; + snd := 0 + }; diff --git a/tests/Rust/Compilation/positive/test062.juvix b/tests/Rust/Compilation/positive/test062.juvix new file mode 100644 index 0000000000..bc3f65a0bb --- /dev/null +++ b/tests/Rust/Compilation/positive/test062.juvix @@ -0,0 +1,12 @@ +-- Overapplication +module test062; + +import Stdlib.Data.Nat open; + +{-# inline: false #-} +I {A} (x : A) : A := x; + +{-# inline: false #-} +I' {A} (x : A) : A := x; + +main : Nat := I' (I I I I 1); diff --git a/tests/Rust/Compilation/positive/test064.juvix b/tests/Rust/Compilation/positive/test064.juvix new file mode 100644 index 0000000000..c3674c2730 --- /dev/null +++ b/tests/Rust/Compilation/positive/test064.juvix @@ -0,0 +1,42 @@ +-- Constant folding +module test064; + +import Stdlib.Prelude open; +import Stdlib.Debug.Fail as Debug; + +{-# inline: false #-} +f (x y : Nat) : Nat := x + y; + +{-# inline: false #-} +g (x : Bool) : Bool := if x false true; + +{-# inline: false #-} +h (x : Bool) : Bool := if (g x) false true; + +{-# inline: false, eval: false #-} +j (x : Nat) : Nat := x + 0; + +sum : Nat -> Nat + | zero := 0 + | k@(suc n) := k + sum n; + +even : Nat -> Bool + | zero := true + | (suc n) := odd n; + +odd : Nat -> Bool + | zero := false + | (suc n) := even n; + +terminating +loop : Nat := loop; + +{-# inline: false #-} +even' : Nat -> Bool := even; + +main : Nat := + sum 3 + + case even' 6 || g true || h true of { + | true := if (g false) (f 1 2 + sum 7 + j 0) 0 + | false := f (3 + 4) (f 0 8) + loop + }; diff --git a/tests/Rust/Compilation/positive/test065.juvix b/tests/Rust/Compilation/positive/test065.juvix new file mode 100644 index 0000000000..29bc0b2fbb --- /dev/null +++ b/tests/Rust/Compilation/positive/test065.juvix @@ -0,0 +1,15 @@ +-- Arithmetic simplification +module test065; + +import Stdlib.Prelude open; + +{-# inline: false #-} +f (x : Int) : Int := + (x + fromNat 1 - fromNat 1) * fromNat 1 + + fromNat 0 * x + + (fromNat 10 + (x - fromNat 10)) + + (fromNat 10 + x - fromNat 10) + + (fromNat 11 + (fromNat 11 - x)) + + fromNat 1 * x * fromNat 0 * fromNat 1; + +main : Int := f (fromNat 10); diff --git a/tests/Rust/Compilation/positive/test066/M.juvix b/tests/Rust/Compilation/positive/test066/M.juvix new file mode 100644 index 0000000000..8d1f10f57c --- /dev/null +++ b/tests/Rust/Compilation/positive/test066/M.juvix @@ -0,0 +1,6 @@ +module M; + +import Stdlib.Prelude open; +import N open; + +main : Nat := f; diff --git a/tests/Rust/Compilation/positive/test066/N.juvix b/tests/Rust/Compilation/positive/test066/N.juvix new file mode 100644 index 0000000000..e23c0ca29e --- /dev/null +++ b/tests/Rust/Compilation/positive/test066/N.juvix @@ -0,0 +1,7 @@ +module N; + +import Stdlib.Prelude open; + +mkNat (n : Nat) : Nat := n; + +f {a : Nat := mkNat 0} : Nat := a; diff --git a/tests/Rust/Compilation/positive/test066/Package.juvix b/tests/Rust/Compilation/positive/test066/Package.juvix new file mode 100644 index 0000000000..5b60fc4da1 --- /dev/null +++ b/tests/Rust/Compilation/positive/test066/Package.juvix @@ -0,0 +1,5 @@ +module Package; + +import PackageDescription.Basic open; + +package : Package := basicPackage; diff --git a/tests/Rust/Compilation/positive/test067.juvix b/tests/Rust/Compilation/positive/test067.juvix new file mode 100644 index 0000000000..c9fb065f98 --- /dev/null +++ b/tests/Rust/Compilation/positive/test067.juvix @@ -0,0 +1,8 @@ +-- Default values inserted in the translation FromConcrete +module test067; + +import Stdlib.Data.Nat open; + +f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c; + +main : Nat := f {c := 5}; diff --git a/tests/Rust/Compilation/positive/test068.juvix b/tests/Rust/Compilation/positive/test068.juvix new file mode 100644 index 0000000000..44cc2b7ff6 --- /dev/null +++ b/tests/Rust/Compilation/positive/test068.juvix @@ -0,0 +1,9 @@ +-- Default values inserted in the arity checker +module test068; + +import Stdlib.Data.Nat open; + +f {a : Nat := 2} {b : Nat := 3} {c : Nat := 5} : Nat := + a * b * c; + +main : Nat := f; diff --git a/tests/Rust/Compilation/positive/test069.juvix b/tests/Rust/Compilation/positive/test069.juvix new file mode 100644 index 0000000000..ac9dda3abe --- /dev/null +++ b/tests/Rust/Compilation/positive/test069.juvix @@ -0,0 +1,31 @@ +-- Default values inserted in the arity checker +module test069; + +import Stdlib.Data.Nat open hiding {Ord; mkOrd}; +import Stdlib.Data.Nat.Ord as Ord; +import Stdlib.Data.Product as Ord; +import Stdlib.Data.Bool.Base open; +import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; + +trait +type Ord A := + mkOrd { + cmp : A -> A -> Ordering; + lt : A -> A -> Bool; + ge : A -> A -> Bool + }; + +mkOrdHelper + {A} + (cmp : A -> A -> Ordering) + {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}} + {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}} + : Ord A := + mkOrd cmp lt gt; + +ordNatNamed : Ord Nat := mkOrdHelper (cmp := Ord.compare); + +instance +ordNat : Ord Nat := mkOrdHelper Ord.compare; + +main : Nat := if (Ord.lt 1 2) 1 0; diff --git a/tests/Rust/Compilation/positive/test070.juvix b/tests/Rust/Compilation/positive/test070.juvix new file mode 100644 index 0000000000..171cf12e8b --- /dev/null +++ b/tests/Rust/Compilation/positive/test070.juvix @@ -0,0 +1,10 @@ +-- Nested named application with default values +module test070; + +import Stdlib.Data.Nat open; + +fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} + : Nat := a * b + c; + +main : Nat := + fun {a := fun; b := fun {b := 3} * fun {b := fun {2}}}; diff --git a/tests/Rust/Compilation/positive/test071.juvix b/tests/Rust/Compilation/positive/test071.juvix new file mode 100644 index 0000000000..84f4d5100e --- /dev/null +++ b/tests/Rust/Compilation/positive/test071.juvix @@ -0,0 +1,43 @@ +-- Named application +module test071; + +import Stdlib.Data.Nat open hiding {Ord; mkOrd}; +import Stdlib.Data.Nat.Ord as Ord; +import Stdlib.Data.Product as Ord; +import Stdlib.Data.Bool.Base open; +import Stdlib.Trait.Ord open using {Ordering; LT; EQ; GT; isLT; isGT}; + +trait +type Ord A := + mkOrd { + cmp : A -> A -> Ordering; + lt : A -> A -> Bool; + ge : A -> A -> Bool + }; + +mkOrdHelper + {A} + (cmp : A -> A -> Ordering) + {lt : A -> A -> Bool := λ {a b := isLT (cmp a b)}} + {gt : A -> A -> Bool := λ {a b := isGT (cmp a b)}} + : Ord A := + mkOrd cmp lt gt; + +instance +ordNat : Ord Nat := mkOrdHelper@{ + cmp (x y : Nat) : Ordering := Ord.compare x y +}; + +fun {a : Nat := 1} {b : Nat := a + 1} {c : Nat := b + a + 1} + : Nat := a * b + c; + +f {a : Nat := 2} {b : Nat := a + 1} {c : Nat} : Nat := a * b * c; + +g {a : Nat := 2} {b : Nat := a + 1} (c : Nat) : Nat := a * b * c; + +h {a : Nat := 2} (b c : Nat) {d : Nat := 3} : Nat := a * b + c * d; + +main : Nat := + fun@{a := fun; b := fun@{b := 3} * fun@{b := fun {2}}} + + f@{c := 5} + g@?{b := 4} 3 + if (Ord.lt 1 0) 1 0 + + h@?{b := 4} 1; diff --git a/tests/Rust/Compilation/positive/test072/Functor.juvix b/tests/Rust/Compilation/positive/test072/Functor.juvix new file mode 100644 index 0000000000..76f31dbb83 --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/Functor.juvix @@ -0,0 +1,10 @@ +module Functor; + +syntax fixity fmap := binary {assoc := left}; + +trait +type Functor (f : Type -> Type) := + mkFunctor { + syntax operator <$> fmap; + <$> : {A B : Type} -> (A -> B) -> f A -> f B + }; diff --git a/tests/Rust/Compilation/positive/test072/Identity.juvix b/tests/Rust/Compilation/positive/test072/Identity.juvix new file mode 100644 index 0000000000..1d84c8fad2 --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/Identity.juvix @@ -0,0 +1,25 @@ +module Identity; + +import Monad open; +import Functor open; + +type Identity (a : Type) := mkIdentity {runIdentity : a}; + +open Identity public; + +instance +Identity-Functor : Functor Identity := + mkFunctor@{ + <$> {A B : Type} (f : A -> B) : Identity A -> Identity B + | (mkIdentity a) := mkIdentity (f a) + }; + +instance +Identity-Monad : Monad Identity := + mkMonad@{ + functor := Identity-Functor; + return {A : Type} (a : A) : Identity A := mkIdentity a; + >>= {A B : Type} + : Identity A -> (A -> Identity B) -> Identity B + | (mkIdentity a) f := f a + }; diff --git a/tests/Rust/Compilation/positive/test072/Monad.juvix b/tests/Rust/Compilation/positive/test072/Monad.juvix new file mode 100644 index 0000000000..81a4dfb960 --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/Monad.juvix @@ -0,0 +1,21 @@ +module Monad; + +import Functor open; +import Stdlib.Data.Fixity open; + +syntax fixity bind := binary {assoc := left}; + +trait +type Monad (f : Type -> Type) := + mkMonad { + functor : Functor f; + return : {A : Type} -> A -> f A; + syntax operator >>= bind; + >>= : {A B : Type} -> f A -> (A -> f B) -> f B + }; + +open Monad public; + +syntax operator >> bind; +>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M + A) (y : M B) : M B := x >>= λ {_ := y}; diff --git a/tests/Rust/Compilation/positive/test072/MonadReader.juvix b/tests/Rust/Compilation/positive/test072/MonadReader.juvix new file mode 100644 index 0000000000..8aeda8fd8d --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/MonadReader.juvix @@ -0,0 +1,14 @@ +module MonadReader; + +import Monad open; +import Stdlib.Data.Unit open; + +trait +type MonadReader (S : Type) (M : Type -> Type) := + mkMonadReader { + monad : Monad M; + ask : M S; + reader : {A : Type} → (S → A) → M A + }; + +open MonadReader public; diff --git a/tests/Rust/Compilation/positive/test072/MonadState.juvix b/tests/Rust/Compilation/positive/test072/MonadState.juvix new file mode 100644 index 0000000000..fc9eb31de0 --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/MonadState.juvix @@ -0,0 +1,18 @@ +module MonadState; + +import Monad open; +import Stdlib.Data.Unit open; + +trait +type MonadState (S : Type) (M : Type -> Type) := + mkMonadState { + monad : Monad M; + get : M S; + put : S -> M Unit + }; + +open MonadState public; + +modify {S : Type} {M : Type → Type} {{Monad M}} {{MonadState + S + M}} (f : S → S) : M Unit := get >>= λ {s := put (f s)}; diff --git a/tests/Rust/Compilation/positive/test072/Package.juvix b/tests/Rust/Compilation/positive/test072/Package.juvix new file mode 100644 index 0000000000..d86c375987 --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/Package.juvix @@ -0,0 +1,5 @@ +module Package; + +import PackageDescription.V2 open; + +package : Package := defaultPackage {name := "monads"}; diff --git a/tests/Rust/Compilation/positive/test072/Reader.juvix b/tests/Rust/Compilation/positive/test072/Reader.juvix new file mode 100644 index 0000000000..7e89040ffd --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/Reader.juvix @@ -0,0 +1,28 @@ +module Reader; + +import Monad open; +import Functor open; +import Stdlib.Function open; + +type Reader (r a : Type) := mkReader {runReader : r -> a}; + +instance +Reader-Functor {R : Type} : Functor (Reader R) := + mkFunctor@{ + <$> {A B : Type} (f : A -> B) : Reader R A -> Reader R B + | (mkReader ra) := mkReader (f ∘ ra) + }; + +instance +Reader-Monad {R : Type} : Monad (Reader R) := + mkMonad@{ + functor := Reader-Functor; + return {A : Type} (a : A) : Reader R A := + mkReader (const a); + >>= {A B : Type} + : Reader R A -> (A -> Reader R B) -> Reader R B + | (mkReader ra) arb := + let + open Reader; + in mkReader λ {r := runReader (arb (ra r)) r} + }; diff --git a/tests/Rust/Compilation/positive/test072/ReaderT.juvix b/tests/Rust/Compilation/positive/test072/ReaderT.juvix new file mode 100644 index 0000000000..95d4d7d3dd --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/ReaderT.juvix @@ -0,0 +1,92 @@ +module ReaderT; + +import Monad open; +import Monad open using {module Monad as MMonad}; +import Functor open; +import Functor open using {module Functor as MFunctor}; + +type ReaderT (S : Type) (M : Type → Type) (A : Type) := + mkReaderT {runReaderT : S → M A}; + +runReader {S A : Type} {M : Type + → Type} (r : S) (m : ReaderT S M A) : M A := + ReaderT.runReaderT m r; + +instance +ReaderT-Functor {S : Type} {M : Type + → Type} {{func : Functor M}} : Functor (ReaderT S M) := + mkFunctor@{ + <$> {A B : Type} (f : A → B) + : ReaderT S M A → ReaderT S M B + | (mkReaderT g) := + -- NOTE we cannot use unqualified <$> or the scoper gets confused + let + open MFunctor; + in mkReaderT λ {s := λ {a := f a} MFunctor.<$> g s} + }; + +instance +ReaderT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}} + : Monad (ReaderT S M) := + mkMonad@{ + functor := + ReaderT-Functor@{ + func := MMonad.functor + }; + return {A : Type} (a : A) : ReaderT S M A := + mkReaderT λ {s := MMonad.return a}; + >>= {A B : Type} (x : ReaderT S M A) (f : A → ReaderT S M B) + : ReaderT S M B := + mkReaderT + λ {s := runReader s x MMonad.>>= λ {a := runReader s (f a)}} + }; + +import MonadReader open; +import Stdlib.Data.Unit open; +import Stdlib.Function open; + +instance +ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}} + : MonadReader S (ReaderT S M) := + mkMonadReader@{ + monad := ReaderT-Monad; + ask : ReaderT S M S := mkReaderT λ {s := MMonad.return s}; + reader {A : Type} (f : S → A) : ReaderT S M A := + mkReaderT (MMonad.return ∘ f) + }; + +import MonadState open; +import StateT open; +import Identity open; +import Stdlib.Data.Product open; + +liftReaderT {R A : Type} {M : Type → Type} (m : M A) + : ReaderT R M A := mkReaderT (const m); + +liftStateT {S A : Type} {M : Type → Type} {{Monad M}} (m : M + A) : StateT S M A := + mkStateT + λ {s := m MMonad.>>= λ {a := MMonad.return (a, s)}}; + +import Stdlib.Data.Nat open; + +askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat := + ask; + +monadic : ReaderT Nat (StateT Nat Identity) Nat := + askNat + >>= λ {n := + liftReaderT (modify λ {m := m * n}) >> liftReaderT get}; + +main : Nat := + runIdentity (evalState 2 (runReader 5 monadic)); + +-- FIXME fails instance termination +-- instance +-- StateT-MonadReader {R S : Type} {M : Type +-- → Type} {{mreader : MonadReader R M}} : MonadReader R (StateT S M) := +-- mkMonadReader@{ +-- monad := StateT-Monad@{mon := MonadReader.monad {{mreader}}}; +-- reader {A : Type} : (R → A) → StateT S M A := liftStateT ∘ MonadReader.reader; +-- ask : StateT S M R := liftStateT MonadReader.ask; +-- }; diff --git a/tests/Rust/Compilation/positive/test072/State.juvix b/tests/Rust/Compilation/positive/test072/State.juvix new file mode 100644 index 0000000000..2e7fadc124 --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/State.juvix @@ -0,0 +1,42 @@ +module State; + +import Monad open; +import Functor open; +import Stdlib.Data.Product open; + +type State (S A : Type) := mkState {runState : S -> A × S}; + +instance +State-Functor {S : Type} : Functor (State S) := + mkFunctor@{ + <$> {A B : Type} (f : A -> B) : State S A -> State S B + | (mkState S→A×S) := + mkState λ {s := case S→A×S s of {a, s := f a, s}} + }; + +instance +State-Monad {S : Type} : Monad (State S) := + mkMonad@{ + functor := State-Functor; + return {A : Type} (a : A) : State S A := + mkState λ {s := a, s}; + >>= {A B : Type} + : State S A -> (A -> State S B) -> State S B + | (mkState s→s×a) a→Ss×b := + mkState + λ {s := + case s→s×a s of { + a, s1 := case a→Ss×b a of {mkState s→s×b := s→s×b s1} + }} + }; + +import MonadState open; +import Stdlib.Data.Unit open; + +instance +State-MonadState {S : Type} : MonadState S (State S) := + mkMonadState@{ + monad := State-Monad; + get : State S S := mkState λ {s := s, s}; + put (s : S) : State S Unit := mkState λ {_ := unit, s} + }; diff --git a/tests/Rust/Compilation/positive/test072/StateT.juvix b/tests/Rust/Compilation/positive/test072/StateT.juvix new file mode 100644 index 0000000000..f804233f37 --- /dev/null +++ b/tests/Rust/Compilation/positive/test072/StateT.juvix @@ -0,0 +1,63 @@ +module StateT; + +import Monad open; +import Monad open using {module Monad as MMonad}; +import Functor open; +import Functor open using {module Functor as MFunctor}; +import Stdlib.Data.Product open; + +type StateT (S : Type) (M : Type → Type) (A : Type) := + mkStateT {runStateT : S → M (A × S)}; + +runState {S A : Type} {M : Type → Type} (s : S) (m : StateT + S + M + A) : M (A × S) := StateT.runStateT m s; + +evalState {S A : Type} {M : Type → Type} {{Functor + M}} (s : S) (m : StateT S M A) : M A := + fst Functor.<$> runState s m; + +instance +StateT-Functor {S : Type} {M : Type → Type} {{func : Functor + M}} : Functor (StateT S M) := + mkFunctor@{ + <$> {A B : Type} (f : A → B) : StateT S M A → StateT S M B + | (mkStateT S→M⟨A×S⟩) := + let + open MFunctor; + in mkStateT + λ {s := λ {(a, s') := f a, s'} MFunctor.<$> S→M⟨A×S⟩ s} + }; + +instance +StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}} + : Monad (StateT S M) := + mkMonad@{ + functor := + StateT-Functor@{ + func := MMonad.functor + }; + return {A : Type} (a : A) : StateT S M A := + mkStateT λ {s := MMonad.return (a, s)}; + >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B) + : StateT S M B := + mkStateT + λ {s := + StateT.runStateT x s + MMonad.>>= λ {(a, s') := StateT.runStateT (f a) s'}} + }; + +import MonadState open; +import Stdlib.Data.Unit open; + +instance +StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}} + : MonadState S (StateT S M) := + mkMonadState@{ + monad := StateT-Monad; + get : StateT S M S := + mkStateT λ {s := MMonad.return (s, s)}; + put (s : S) : StateT S M Unit := + mkStateT λ {_ := MMonad.return (unit, s)} + }; diff --git a/tests/Rust/Compilation/positive/test073/Package.juvix b/tests/Rust/Compilation/positive/test073/Package.juvix new file mode 100644 index 0000000000..905b22a801 --- /dev/null +++ b/tests/Rust/Compilation/positive/test073/Package.juvix @@ -0,0 +1,5 @@ +module Package; + +import PackageDescription.V2 open; + +package : Package := defaultPackage {name := "test073"}; diff --git a/tests/Rust/Compilation/positive/test073/SyntaxAlias.juvix b/tests/Rust/Compilation/positive/test073/SyntaxAlias.juvix new file mode 100644 index 0000000000..1231cd99fb --- /dev/null +++ b/tests/Rust/Compilation/positive/test073/SyntaxAlias.juvix @@ -0,0 +1,5 @@ +module SyntaxAlias; + +import Stdlib.Prelude open; + +syntax alias MyNat := Nat; diff --git a/tests/Rust/Compilation/positive/test073/test073.juvix b/tests/Rust/Compilation/positive/test073/test073.juvix new file mode 100644 index 0000000000..f314df5de7 --- /dev/null +++ b/tests/Rust/Compilation/positive/test073/test073.juvix @@ -0,0 +1,5 @@ +module test073; + +import SyntaxAlias open; + +main : MyNat := 11;