From 1eadbc4f810698f4de873703cd5bb549f0fcc996 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Tue, 14 Mar 2023 17:22:32 +0100 Subject: [PATCH] Remove the old C backend (#1862) * Depends on PR #1832 * Closes #1799 * Removes Backend.C.Translation.FromInternal * Removes `foreign` and `compile` blocks * Removes unused test files * Removes the old C runtime * Removes other dead code --- app/Commands/Dev/MiniC/Options.hs | 15 - c-runtime/anoma/anoma.h | 30 - c-runtime/builtins/bool.h | 21 - c-runtime/builtins/io.h | 10 - c-runtime/builtins/juvix_string.h | 6 - c-runtime/builtins/nat.h | 36 - c-runtime/standalone/c-runtime.h | 221 ----- c-runtime/walloc/walloc.c | 466 --------- c-runtime/wasi-libc/c-runtime.h | 129 --- c-runtime/wasi-standalone/c-runtime.h | 294 ------ docs/org/examples/README.org | 7 - .../backend-specific/minic-hello-world.org | 44 - .../validity-predicates/PolyFungibleToken.org | 304 ------ docs/org/reference/language/compileblocks.org | 65 -- docs/org/reference/language/foreign.org | 30 - docs/org/tutorials/learn.org | 2 +- .../ValidityPredicates/Anoma/Base.hs | 16 - .../ValidityPredicates/Anoma/Base.juvix | 82 -- .../ValidityPredicates/Data/Int.juvix | 19 - .../ValidityPredicates/Data/Int/Ops.juvix | 56 -- .../SimpleFungibleToken.juvix | 52 - .../milestone/ValidityPredicates/Tests.juvix | 36 - .../milestone/ValidityPredicates/juvix.yaml | 2 - package.yaml | 2 - src/Juvix/Compiler/Abstract/Data/InfoTable.hs | 7 +- .../Abstract/Extra/DependencyBuilder.hs | 1 - src/Juvix/Compiler/Abstract/Language.hs | 3 +- .../Abstract/Translation/FromConcrete.hs | 2 - src/Juvix/Compiler/Backend/C/Data/Base.hs | 340 ------- .../Compiler/Backend/C/Data/BuiltinTable.hs | 55 -- src/Juvix/Compiler/Backend/C/Data/CNames.hs | 168 ---- src/Juvix/Compiler/Backend/C/Data/Closure.hs | 290 ------ src/Juvix/Compiler/Backend/C/Data/Types.hs | 39 - .../Compiler/Backend/C/Extra/Serialization.hs | 46 +- src/Juvix/Compiler/Backend/C/Language.hs | 158 --- src/Juvix/Compiler/Backend/C/Translation.hs | 6 +- .../Backend/C/Translation/FromInternal.hs | 921 ------------------ .../Compiler/Backend/C/Translation/FromReg.hs | 3 - src/Juvix/Compiler/Concrete/Data/InfoTable.hs | 13 +- .../Concrete/Data/InfoTableBuilder.hs | 15 - src/Juvix/Compiler/Concrete/Data/Scope.hs | 6 +- src/Juvix/Compiler/Concrete/Keywords.hs | 12 - src/Juvix/Compiler/Concrete/Language.hs | 22 - src/Juvix/Compiler/Concrete/Pretty/Base.hs | 37 - src/Juvix/Compiler/Concrete/Print/Base.hs | 39 - .../FromParsed/Analysis/Scoping.hs | 96 -- .../FromParsed/Analysis/Scoping/Error.hs | 8 - .../Analysis/Scoping/Error/Types.hs | 105 -- .../Concrete/Translation/FromSource.hs | 38 - src/Juvix/Compiler/Core/Extra/Utils.hs | 10 - src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs | 48 - src/Juvix/Compiler/Core/Info/IdentInfo.hs | 41 - src/Juvix/Compiler/Core/Keywords.hs | 1 - .../Compiler/Core/Translation/FromInternal.hs | 1 - src/Juvix/Compiler/Internal/Language.hs | 1 - src/Juvix/Compiler/Internal/Pretty/Base.hs | 24 - .../Internal/Translation/FromAbstract.hs | 1 - .../Analysis/ArityChecking/Checker.hs | 1 - .../FromInternal/Analysis/Reachability.hs | 1 - .../Analysis/TypeChecking/Checker.hs | 1 - src/Juvix/Compiler/Pipeline.hs | 6 - src/Juvix/Data.hs | 6 +- src/Juvix/Data/Backends.hs | 21 - src/Juvix/Data/CodeAnn.hs | 27 - src/Juvix/Data/ForeignBlock.hs | 15 - src/Juvix/Data/Keyword/All.hs | 28 +- src/Juvix/Extra/Strings.hs | 108 -- test/Reachability/Positive.hs | 1 - test/Scope/Negative.hs | 28 - test/Scope/Positive.hs | 4 - test/Typecheck/Positive.hs | 8 - tests/Core/positive/lambda-lifting/test1.jvc | 1 - tests/Core/positive/lambda-lifting/test1.out | 3 - tests/Core/positive/lambda-lifting/test2.jvc | 1 - tests/Core/positive/lambda-lifting/test2.out | 6 - tests/Core/positive/lambda-lifting/test3.jvc | 3 - tests/Core/positive/lambda-lifting/test3.out | 6 - .../MultipleCompileBlockSameName.juvix | 13 - .../MultipleCompileRuleSameBackend.juvix | 11 - .../CompileBlocks/Sample/Definitions.juvix | 12 - .../WrongKindExpressionCompileBlock.juvix | 10 - .../WrongLocationCompileBlock.juvix | 9 - tests/negative/CompileBlocks/juvix.yaml | 0 tests/positive/Axiom.juvix | 3 - tests/positive/Foreign.juvix | 37 - tests/positive/FullExamples/Anoma.hs | 16 - .../MonoSimpleFungibleToken.juvix | 310 ------ .../SimpleFungibleTokenImplicit.juvix | 310 ------ tests/positive/FullExamples/juvix.yaml | 0 .../positive/MiniC/AlwaysValidVP/Input.juvix | 38 - .../MiniC/AlwaysValidVP/expected.golden | 1 - tests/positive/MiniC/AlwaysValidVP/input.js | 7 - tests/positive/MiniC/AlwaysValidVP/juvix.yaml | 0 .../positive/MiniC/AxiomNoCompile/Input.juvix | 13 - .../MiniC/AxiomNoCompile/expected.golden | 1 - .../positive/MiniC/AxiomNoCompile/juvix.yaml | 0 tests/positive/MiniC/Builtins/Input.juvix | 65 -- tests/positive/MiniC/Builtins/expected.golden | 8 - tests/positive/MiniC/Builtins/juvix.yaml | 0 .../positive/MiniC/BuiltinsStdlib/Input.juvix | 21 - .../MiniC/BuiltinsStdlib/expected.golden | 9 - .../positive/MiniC/BuiltinsStdlib/juvix.yaml | 0 tests/positive/MiniC/ClosureEnv/Data | 1 - tests/positive/MiniC/ClosureEnv/Input.juvix | 107 -- .../positive/MiniC/ClosureEnv/Prelude.mjuvix | 1 - .../positive/MiniC/ClosureEnv/expected.golden | 8 - tests/positive/MiniC/ClosureEnv/juvix.yaml | 0 tests/positive/MiniC/ClosureNoEnv/Data | 1 - tests/positive/MiniC/ClosureNoEnv/Input.juvix | 84 -- .../MiniC/ClosureNoEnv/Prelude.mjuvix | 1 - .../MiniC/ClosureNoEnv/expected.golden | 4 - tests/positive/MiniC/ClosureNoEnv/juvix.yaml | 0 tests/positive/MiniC/ExportName/Input.juvix | 8 - .../positive/MiniC/ExportName/expected.golden | 1 - tests/positive/MiniC/ExportName/juvix.yaml | 0 .../positive/MiniC/ExportNameArgs/Input.juvix | 8 - .../MiniC/ExportNameArgs/expected.golden | 1 - .../positive/MiniC/ExportNameArgs/juvix.yaml | 0 tests/positive/MiniC/HelloWorld/Input.juvix | 25 - .../positive/MiniC/HelloWorld/expected.golden | 1 - tests/positive/MiniC/HelloWorld/juvix.yaml | 0 tests/positive/MiniC/HigherOrder/Input.juvix | 142 --- .../MiniC/HigherOrder/expected.golden | 1 - tests/positive/MiniC/HigherOrder/juvix.yaml | 0 .../MiniC/ImportExportName/Input.juvix | 10 - .../MiniC/ImportExportName/expected.golden | 1 - .../positive/MiniC/ImportExportName/input.js | 35 - .../MiniC/ImportExportName/juvix.yaml | 0 tests/positive/MiniC/Lib/Data/Bool.juvix | 17 - tests/positive/MiniC/Lib/Data/IO.juvix | 41 - tests/positive/MiniC/Lib/Data/Int.juvix | 28 - tests/positive/MiniC/Lib/Data/Nat.juvix | 33 - tests/positive/MiniC/Lib/Data/Pair.juvix | 10 - tests/positive/MiniC/Lib/Data/String.juvix | 10 - tests/positive/MiniC/Lib/Prelude.juvix | 15 - tests/positive/MiniC/Lib/minijuvix.yaml | 0 .../MiniC/MultiModules/Data/Bool.juvix | 17 - .../positive/MiniC/MultiModules/Data/IO.juvix | 41 - .../MiniC/MultiModules/Data/Int.juvix | 38 - .../MiniC/MultiModules/Data/Nat.juvix | 33 - .../MiniC/MultiModules/Data/Pair.juvix | 10 - .../MiniC/MultiModules/Data/String.juvix | 10 - tests/positive/MiniC/MultiModules/Input.juvix | 29 - .../positive/MiniC/MultiModules/Prelude.juvix | 15 - .../MiniC/MultiModules/expected.golden | 1 - tests/positive/MiniC/MultiModules/juvix.yaml | 0 .../MiniC/MutuallyRecursive/Data/Bool.juvix | 17 - .../MiniC/MutuallyRecursive/Data/IO.juvix | 41 - .../MiniC/MutuallyRecursive/Data/Int.juvix | 49 - .../MiniC/MutuallyRecursive/Data/Nat.juvix | 33 - .../MiniC/MutuallyRecursive/Data/Pair.juvix | 10 - .../MiniC/MutuallyRecursive/Data/String.juvix | 10 - .../MiniC/MutuallyRecursive/Input.juvix | 32 - .../MiniC/MutuallyRecursive/Prelude.juvix | 15 - .../MiniC/MutuallyRecursive/expected.golden | 6 - .../MiniC/MutuallyRecursive/juvix.yaml | 0 tests/positive/MiniC/Nat/Input.juvix | 177 ---- tests/positive/MiniC/Nat/expected.golden | 5 - tests/positive/MiniC/Nat/juvix.yaml | 0 tests/positive/MiniC/NestedList/Data | 1 - tests/positive/MiniC/NestedList/Input.juvix | 19 - .../positive/MiniC/NestedList/Prelude.mjuvix | 1 - .../positive/MiniC/NestedList/expected.golden | 1 - tests/positive/MiniC/NestedList/juvix.yaml | 0 .../MiniC/PolymorphicAxioms/Input.juvix | 25 - .../MiniC/PolymorphicAxioms/expected.golden | 0 .../MiniC/PolymorphicAxioms/juvix.yaml | 0 .../MiniC/PolymorphicTarget/Input.juvix | 30 - .../MiniC/PolymorphicTarget/expected.golden | 0 .../MiniC/PolymorphicTarget/juvix.yaml | 0 tests/positive/MiniC/Polymorphism/Input.juvix | 87 -- .../MiniC/Polymorphism/expected.golden | 2 - tests/positive/MiniC/Polymorphism/juvix.yaml | 0 .../MiniC/PolymorphismHoles/Input.juvix | 87 -- .../MiniC/PolymorphismHoles/expected.golden | 1 - .../MiniC/PolymorphismHoles/juvix.yaml | 0 .../SimpleFungibleTokenImplicit/Input.juvix | 359 ------- .../expected.golden | 1 - .../SimpleFungibleTokenImplicit/juvix.yaml | 0 tests/positive/MiniC/StdlibImport/Input.juvix | 11 - .../MiniC/StdlibImport/expected.golden | 1 - tests/positive/MiniC/StdlibImport/juvix.yaml | 0 tests/smoke/Commands/html.smoke.yaml | 128 +-- 183 files changed, 22 insertions(+), 7586 deletions(-) delete mode 100644 app/Commands/Dev/MiniC/Options.hs delete mode 100644 c-runtime/anoma/anoma.h delete mode 100644 c-runtime/builtins/bool.h delete mode 100644 c-runtime/builtins/io.h delete mode 100644 c-runtime/builtins/juvix_string.h delete mode 100644 c-runtime/builtins/nat.h delete mode 100644 c-runtime/standalone/c-runtime.h delete mode 100644 c-runtime/walloc/walloc.c delete mode 100644 c-runtime/wasi-libc/c-runtime.h delete mode 100644 c-runtime/wasi-standalone/c-runtime.h delete mode 100755 docs/org/examples/backend-specific/minic-hello-world.org delete mode 100644 docs/org/examples/validity-predicates/PolyFungibleToken.org delete mode 100644 docs/org/reference/language/compileblocks.org delete mode 100644 docs/org/reference/language/foreign.org delete mode 100644 examples/milestone/ValidityPredicates/Anoma/Base.hs delete mode 100644 examples/milestone/ValidityPredicates/Anoma/Base.juvix delete mode 100644 examples/milestone/ValidityPredicates/Data/Int.juvix delete mode 100644 examples/milestone/ValidityPredicates/Data/Int/Ops.juvix delete mode 100644 examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix delete mode 100644 examples/milestone/ValidityPredicates/Tests.juvix delete mode 100644 examples/milestone/ValidityPredicates/juvix.yaml delete mode 100644 src/Juvix/Compiler/Backend/C/Data/Base.hs delete mode 100644 src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs delete mode 100644 src/Juvix/Compiler/Backend/C/Data/CNames.hs delete mode 100644 src/Juvix/Compiler/Backend/C/Data/Closure.hs delete mode 100644 src/Juvix/Compiler/Backend/C/Translation/FromInternal.hs delete mode 100644 src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs delete mode 100644 src/Juvix/Compiler/Core/Info/IdentInfo.hs delete mode 100644 src/Juvix/Data/Backends.hs delete mode 100644 src/Juvix/Data/ForeignBlock.hs delete mode 100644 tests/Core/positive/lambda-lifting/test1.jvc delete mode 100644 tests/Core/positive/lambda-lifting/test1.out delete mode 100644 tests/Core/positive/lambda-lifting/test2.jvc delete mode 100644 tests/Core/positive/lambda-lifting/test2.out delete mode 100644 tests/Core/positive/lambda-lifting/test3.jvc delete mode 100644 tests/Core/positive/lambda-lifting/test3.out delete mode 100644 tests/negative/CompileBlocks/MultipleCompileBlockSameName.juvix delete mode 100644 tests/negative/CompileBlocks/MultipleCompileRuleSameBackend.juvix delete mode 100644 tests/negative/CompileBlocks/Sample/Definitions.juvix delete mode 100644 tests/negative/CompileBlocks/WrongKindExpressionCompileBlock.juvix delete mode 100644 tests/negative/CompileBlocks/WrongLocationCompileBlock.juvix delete mode 100644 tests/negative/CompileBlocks/juvix.yaml delete mode 100644 tests/positive/Foreign.juvix delete mode 100644 tests/positive/FullExamples/Anoma.hs delete mode 100644 tests/positive/FullExamples/MonoSimpleFungibleToken.juvix delete mode 100644 tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix delete mode 100644 tests/positive/FullExamples/juvix.yaml delete mode 100644 tests/positive/MiniC/AlwaysValidVP/Input.juvix delete mode 100644 tests/positive/MiniC/AlwaysValidVP/expected.golden delete mode 100644 tests/positive/MiniC/AlwaysValidVP/input.js delete mode 100644 tests/positive/MiniC/AlwaysValidVP/juvix.yaml delete mode 100644 tests/positive/MiniC/AxiomNoCompile/Input.juvix delete mode 100644 tests/positive/MiniC/AxiomNoCompile/expected.golden delete mode 100644 tests/positive/MiniC/AxiomNoCompile/juvix.yaml delete mode 100644 tests/positive/MiniC/Builtins/Input.juvix delete mode 100644 tests/positive/MiniC/Builtins/expected.golden delete mode 100644 tests/positive/MiniC/Builtins/juvix.yaml delete mode 100644 tests/positive/MiniC/BuiltinsStdlib/Input.juvix delete mode 100644 tests/positive/MiniC/BuiltinsStdlib/expected.golden delete mode 100644 tests/positive/MiniC/BuiltinsStdlib/juvix.yaml delete mode 120000 tests/positive/MiniC/ClosureEnv/Data delete mode 100644 tests/positive/MiniC/ClosureEnv/Input.juvix delete mode 120000 tests/positive/MiniC/ClosureEnv/Prelude.mjuvix delete mode 100644 tests/positive/MiniC/ClosureEnv/expected.golden delete mode 100644 tests/positive/MiniC/ClosureEnv/juvix.yaml delete mode 120000 tests/positive/MiniC/ClosureNoEnv/Data delete mode 100644 tests/positive/MiniC/ClosureNoEnv/Input.juvix delete mode 120000 tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix delete mode 100644 tests/positive/MiniC/ClosureNoEnv/expected.golden delete mode 100644 tests/positive/MiniC/ClosureNoEnv/juvix.yaml delete mode 100644 tests/positive/MiniC/ExportName/Input.juvix delete mode 100644 tests/positive/MiniC/ExportName/expected.golden delete mode 100644 tests/positive/MiniC/ExportName/juvix.yaml delete mode 100644 tests/positive/MiniC/ExportNameArgs/Input.juvix delete mode 100644 tests/positive/MiniC/ExportNameArgs/expected.golden delete mode 100644 tests/positive/MiniC/ExportNameArgs/juvix.yaml delete mode 100644 tests/positive/MiniC/HelloWorld/Input.juvix delete mode 100644 tests/positive/MiniC/HelloWorld/expected.golden delete mode 100644 tests/positive/MiniC/HelloWorld/juvix.yaml delete mode 100644 tests/positive/MiniC/HigherOrder/Input.juvix delete mode 100644 tests/positive/MiniC/HigherOrder/expected.golden delete mode 100644 tests/positive/MiniC/HigherOrder/juvix.yaml delete mode 100644 tests/positive/MiniC/ImportExportName/Input.juvix delete mode 100644 tests/positive/MiniC/ImportExportName/expected.golden delete mode 100644 tests/positive/MiniC/ImportExportName/input.js delete mode 100644 tests/positive/MiniC/ImportExportName/juvix.yaml delete mode 100644 tests/positive/MiniC/Lib/Data/Bool.juvix delete mode 100644 tests/positive/MiniC/Lib/Data/IO.juvix delete mode 100644 tests/positive/MiniC/Lib/Data/Int.juvix delete mode 100644 tests/positive/MiniC/Lib/Data/Nat.juvix delete mode 100644 tests/positive/MiniC/Lib/Data/Pair.juvix delete mode 100644 tests/positive/MiniC/Lib/Data/String.juvix delete mode 100644 tests/positive/MiniC/Lib/Prelude.juvix delete mode 100644 tests/positive/MiniC/Lib/minijuvix.yaml delete mode 100644 tests/positive/MiniC/MultiModules/Data/Bool.juvix delete mode 100644 tests/positive/MiniC/MultiModules/Data/IO.juvix delete mode 100644 tests/positive/MiniC/MultiModules/Data/Int.juvix delete mode 100644 tests/positive/MiniC/MultiModules/Data/Nat.juvix delete mode 100644 tests/positive/MiniC/MultiModules/Data/Pair.juvix delete mode 100644 tests/positive/MiniC/MultiModules/Data/String.juvix delete mode 100644 tests/positive/MiniC/MultiModules/Input.juvix delete mode 100644 tests/positive/MiniC/MultiModules/Prelude.juvix delete mode 100644 tests/positive/MiniC/MultiModules/expected.golden delete mode 100644 tests/positive/MiniC/MultiModules/juvix.yaml delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Data/IO.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Data/String.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Input.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/Prelude.juvix delete mode 100644 tests/positive/MiniC/MutuallyRecursive/expected.golden delete mode 100644 tests/positive/MiniC/MutuallyRecursive/juvix.yaml delete mode 100644 tests/positive/MiniC/Nat/Input.juvix delete mode 100644 tests/positive/MiniC/Nat/expected.golden delete mode 100644 tests/positive/MiniC/Nat/juvix.yaml delete mode 120000 tests/positive/MiniC/NestedList/Data delete mode 100644 tests/positive/MiniC/NestedList/Input.juvix delete mode 120000 tests/positive/MiniC/NestedList/Prelude.mjuvix delete mode 100644 tests/positive/MiniC/NestedList/expected.golden delete mode 100644 tests/positive/MiniC/NestedList/juvix.yaml delete mode 100644 tests/positive/MiniC/PolymorphicAxioms/Input.juvix delete mode 100644 tests/positive/MiniC/PolymorphicAxioms/expected.golden delete mode 100644 tests/positive/MiniC/PolymorphicAxioms/juvix.yaml delete mode 100644 tests/positive/MiniC/PolymorphicTarget/Input.juvix delete mode 100644 tests/positive/MiniC/PolymorphicTarget/expected.golden delete mode 100644 tests/positive/MiniC/PolymorphicTarget/juvix.yaml delete mode 100644 tests/positive/MiniC/Polymorphism/Input.juvix delete mode 100644 tests/positive/MiniC/Polymorphism/expected.golden delete mode 100644 tests/positive/MiniC/Polymorphism/juvix.yaml delete mode 100644 tests/positive/MiniC/PolymorphismHoles/Input.juvix delete mode 100644 tests/positive/MiniC/PolymorphismHoles/expected.golden delete mode 100644 tests/positive/MiniC/PolymorphismHoles/juvix.yaml delete mode 100644 tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix delete mode 100644 tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden delete mode 100644 tests/positive/MiniC/SimpleFungibleTokenImplicit/juvix.yaml delete mode 100644 tests/positive/MiniC/StdlibImport/Input.juvix delete mode 100644 tests/positive/MiniC/StdlibImport/expected.golden delete mode 100644 tests/positive/MiniC/StdlibImport/juvix.yaml diff --git a/app/Commands/Dev/MiniC/Options.hs b/app/Commands/Dev/MiniC/Options.hs deleted file mode 100644 index f2e4b92e6c..0000000000 --- a/app/Commands/Dev/MiniC/Options.hs +++ /dev/null @@ -1,15 +0,0 @@ -module Commands.Dev.MiniC.Options where - -import CommonOptions - -newtype MiniCOptions = MiniCOptions - { _miniCInputFile :: AppPath File - } - deriving stock (Data) - -makeLenses ''MiniCOptions - -parseMiniC :: Parser MiniCOptions -parseMiniC = do - _miniCInputFile <- parseInputJuvixFile - pure MiniCOptions {..} diff --git a/c-runtime/anoma/anoma.h b/c-runtime/anoma/anoma.h deleted file mode 100644 index 46d00e6fea..0000000000 --- a/c-runtime/anoma/anoma.h +++ /dev/null @@ -1,30 +0,0 @@ -#ifndef ANOMA_H_ -#define ANOMA_H_ - -#include "c-runtime.h" - -int readPre(const char *key) { - if (strcmp("change1-key", key)) { - return 100; - } else if (strcmp("change2-key", key)) { - return 90; - } else { - return -1; - } -} - -int readPost(const char *key) { - if (strcmp("change1-key", key)) { - return 90; - } else if (strcmp("change2-key", key)) { - return 100; - } else { - return -1; - } -} - -const char* isBalanceKey(const char* s1, const char* s2) { - return "owner-address"; -} - -#endif // ANOMA_H_ diff --git a/c-runtime/builtins/bool.h b/c-runtime/builtins/bool.h deleted file mode 100644 index 29c15ece4d..0000000000 --- a/c-runtime/builtins/bool.h +++ /dev/null @@ -1,21 +0,0 @@ -#ifndef BOOL_H_ -#define BOOL_H_ - -#include - -typedef bool prim_bool; - -#define prim_true true -#define prim_false false - -bool is_prim_true(prim_bool b) { return b == prim_true; } - -bool is_prim_false(prim_bool b) { return b == prim_false; } - -#define prim_if(b, ifThen, ifElse) (b ? ifThen : ifElse) - -#define prim_or(a, b) ((a) || (b)) - -#define prim_and(a, b) ((a) && (b)) - -#endif // BOOL_H_ diff --git a/c-runtime/builtins/io.h b/c-runtime/builtins/io.h deleted file mode 100644 index 7954bdee56..0000000000 --- a/c-runtime/builtins/io.h +++ /dev/null @@ -1,10 +0,0 @@ -#ifndef IO_H_ -#define IO_H_ - -typedef int prim_io; - -prim_io prim_sequence(prim_io a, prim_io b) { - return a + b; -} - -#endif // IO_H_ diff --git a/c-runtime/builtins/juvix_string.h b/c-runtime/builtins/juvix_string.h deleted file mode 100644 index ec9f197046..0000000000 --- a/c-runtime/builtins/juvix_string.h +++ /dev/null @@ -1,6 +0,0 @@ -#ifndef STRING_H_ -#define STRING_H_ - -typedef char* prim_string; - -#endif // STRING_H_ diff --git a/c-runtime/builtins/nat.h b/c-runtime/builtins/nat.h deleted file mode 100644 index 958e1b335e..0000000000 --- a/c-runtime/builtins/nat.h +++ /dev/null @@ -1,36 +0,0 @@ -#ifndef NAT_H_ -#define NAT_H_ - -#include - -typedef int prim_nat; - -#define prim_zero 0 - -prim_nat prim_suc(prim_nat n) { return n + 1; } - -bool is_prim_zero(prim_nat n) { return n == 0; } - -bool is_prim_suc(prim_nat n) { return n != 0; } - -prim_nat proj_ca0_prim_suc(prim_nat n) { return n - 1; } - -prim_nat prim_natplus(prim_nat a, prim_nat b) { return a + b; } - -prim_nat prim_natsub(prim_nat a, prim_nat b) { return a - b; } - -prim_nat prim_natmul(prim_nat a, prim_nat b) { return a * b; } - -prim_nat prim_natudiv(prim_nat a, prim_nat b) { return (a + b - 1) / b; } - -prim_nat prim_natdiv(prim_nat a, prim_nat b) { return a / b; } - -prim_nat prim_natmod(prim_nat a, prim_nat b) { return a % b; } - -bool prim_natle(prim_nat a, prim_nat b) { return a <= b; } - -bool prim_natlt(prim_nat a, prim_nat b) { return a < b; } - -bool prim_nateq(prim_nat a, prim_nat b) { return a == b; } - -#endif // NAT_H_ diff --git a/c-runtime/standalone/c-runtime.h b/c-runtime/standalone/c-runtime.h deleted file mode 100644 index dc3e9244e7..0000000000 --- a/c-runtime/standalone/c-runtime.h +++ /dev/null @@ -1,221 +0,0 @@ -#ifndef C_RUNTIME_H_ -#define C_RUNTIME_H_ - -#include "bool.h" -#include "nat.h" -#include "io.h" -#include "juvix_string.h" - -typedef __SIZE_TYPE__ size_t; -typedef __UINT8_TYPE__ uint8_t; -typedef __UINT16_TYPE__ uint16_t; -typedef __UINT32_TYPE__ uint32_t; -typedef __UINT64_TYPE__ uint64_t; -typedef __UINTPTR_TYPE__ uintptr_t; -typedef __INT64_TYPE__ int64_t; - -typedef struct juvix_function { - uintptr_t fun; -} juvix_function_t; - -/** - * Allocator - */ - -void *malloc(size_t size); -void free(void *p); - -void* memcpy(void *dest, const void *src, size_t n) { - char *csrc = (char*) src; - char *cdest = (char*) dest; - - for (int i=0; i < n; i++) { - cdest[i] = csrc[i]; - } - return dest; -} - -void* realloc(void *ptr, size_t n) { - void* newptr; - newptr = malloc(n); - memcpy(newptr, ptr, n); - free(ptr); - return newptr; -} - -/** - * stdlib.h - */ - -#define EXIT_FAILURE 1 - -_Noreturn void exit(int rval) { - __builtin_trap(); -} - -/** - * string.h - */ - -int strcmp(const char *s1, const char *s2) { - while (*s1) { - if (*s1 != *s2) { - break; - } - s1++; - s2++; - } - return *(const unsigned char*)s1 - *(const unsigned char*)s2; -} - -size_t strlen(const char *s) { - const char* p = s; - while(*p!='\0') { - ++p; - } - return p - s; -} - -/** - * Utilities - */ - -/** - * C++ version 0.4 char* style "itoa": - * Written by Lukás Chmela - * Released under GPLv3. - - */ -char* itoa(int value, char* result, int base) { - // check that the base if valid - if (base < 2 || base > 36) { *result = '\0'; return result; } - - char* ptr = result, *ptr1 = result, tmp_char; - int tmp_value; - - do { - tmp_value = value; - value /= base; - *ptr++ = "zyxwvutsrqponmlkjihgfedcba9876543210123456789abcdefghijklmnopqrstuvwxyz" [35 + (tmp_value - value * base)]; - } while ( value ); - - // Apply negative sign - if (tmp_value < 0) *ptr++ = '-'; - *ptr-- = '\0'; - while(ptr1 < ptr) { - tmp_char = *ptr; - *ptr--= *ptr1; - *ptr1++ = tmp_char; - } - return result; -} - -char* intToStr(int i) { - // int will occupy at least one char - size_t len = 1; - - // calculate the size of the digits - int n = i < 0 ? -i : i; - while (n >= 10) { - n /= 10; - len += 1; - } - - // add an extra char for the negative sign - if (i < 0) { - len += 1; - } - - char* buf = (char*)malloc(len + 1); - itoa(i, buf, 10); - return buf; -} - -int strToInt(char *str) -{ - int result; - int puiss; - - result = 0; - puiss = 1; - while (('-' == (*str)) || ((*str) == '+')) - { - if (*str == '-') - puiss = puiss * -1; - str++; - } - while ((*str >= '0') && (*str <= '9')) - { - result = (result * 10) + ((*str) - '0'); - str++; - } - return (result * puiss); -} - -prim_io prim_printNat(prim_nat n) { - exit(1); -} - -prim_io prim_printString(prim_string s) { - exit(1); -} - -prim_io prim_printBool(prim_bool b) { - exit(1); -} - -// Tries to parse str as a positive integer. -// Returns -1 if parsing fails. -int parsePositiveInt(char *str) { - int result = 0; - char* p = str; - size_t len = strlen(str); - while ((*str >= '0') && (*str <= '9')) - { - result = (result * 10) + ((*str) - '0'); - str++; - } - if (str - p != len) return -1; - return result; -} - - -char* concat(const char* s1, const char* s2) { - const size_t len1 = strlen(s1); - const size_t len2 = strlen(s2); - int i,j=0,count=0; - char* result = (char*)malloc(len1 + len2 + 1); - - for(i=0; i < len1; i++) { - result[i] = s1[i]; - count++; - } - - for(i=count; j < len2; i++) { - result[i] = s2[j]; - j++; - } - - result[len1 + len2] = '\0'; - return result; -} - -int debug(const char* str) { - return 0; -} - -prim_io prim_readline(juvix_function_t* f) { exit(1); } - -prim_string prim_natToString(prim_nat n) { return intToStr(n); } - -prim_nat prim_stringToNat(prim_string s) { return parsePositiveInt(s); } - -prim_string prim_stringConcat(prim_string s1, prim_string s2) { - return concat(s1, s2); -} - -prim_bool prim_stringEq(prim_string s1, prim_string s2) { - return strcmp(s1, s2) == 0; -} - -#endif // C_RUNTIME_H_ diff --git a/c-runtime/walloc/walloc.c b/c-runtime/walloc/walloc.c deleted file mode 100644 index 315d9e74ca..0000000000 --- a/c-runtime/walloc/walloc.c +++ /dev/null @@ -1,466 +0,0 @@ -// walloc.c: a small malloc implementation for use in WebAssembly targets -// Copyright (c) 2020 Igalia, S.L. -// -// Permission is hereby granted, free of charge, to any person obtaining a -// copy of this software and associated documentation files (the -// "Software"), to deal in the Software without restriction, including -// without limitation the rights to use, copy, modify, merge, publish, -// distribute, sublicense, and/or sell copies of the Software, and to -// permit persons to whom the Software is furnished to do so, subject to -// the following conditions: -// -// The above copyright notice and this permission notice shall be included -// in all copies or substantial portions of the Software. -// -// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS -// OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF -// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND -// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE -// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION -// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION -// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. - -typedef __SIZE_TYPE__ size_t; -typedef __UINTPTR_TYPE__ uintptr_t; -typedef __UINT8_TYPE__ uint8_t; - -#define NULL ((void *) 0) - -#define STATIC_ASSERT_EQ(a, b) _Static_assert((a) == (b), "eq") - -#ifndef NDEBUG -#define ASSERT(x) do { if (!(x)) __builtin_trap(); } while (0) -#else -#define ASSERT(x) do { } while (0) -#endif -#define ASSERT_EQ(a,b) ASSERT((a) == (b)) - -static inline size_t max(size_t a, size_t b) { - return a < b ? b : a; -} -static inline uintptr_t align(uintptr_t val, uintptr_t alignment) { - return (val + alignment - 1) & ~(alignment - 1); -} -#define ASSERT_ALIGNED(x, y) ASSERT((x) == align((x), y)) - -#define CHUNK_SIZE 256 -#define CHUNK_SIZE_LOG_2 8 -#define CHUNK_MASK (CHUNK_SIZE - 1) -STATIC_ASSERT_EQ(CHUNK_SIZE, 1 << CHUNK_SIZE_LOG_2); - -#define PAGE_SIZE 65536 -#define PAGE_SIZE_LOG_2 16 -#define PAGE_MASK (PAGE_SIZE - 1) -STATIC_ASSERT_EQ(PAGE_SIZE, 1 << PAGE_SIZE_LOG_2); - -#define CHUNKS_PER_PAGE 256 -STATIC_ASSERT_EQ(PAGE_SIZE, CHUNK_SIZE * CHUNKS_PER_PAGE); - -#define GRANULE_SIZE 8 -#define GRANULE_SIZE_LOG_2 3 -#define LARGE_OBJECT_THRESHOLD 256 -#define LARGE_OBJECT_GRANULE_THRESHOLD 32 - -STATIC_ASSERT_EQ(GRANULE_SIZE, 1 << GRANULE_SIZE_LOG_2); -STATIC_ASSERT_EQ(LARGE_OBJECT_THRESHOLD, - LARGE_OBJECT_GRANULE_THRESHOLD * GRANULE_SIZE); - -struct chunk { - char data[CHUNK_SIZE]; -}; - -// There are small object pages for allocations of these sizes. -#define FOR_EACH_SMALL_OBJECT_GRANULES(M) \ - M(1) M(2) M(3) M(4) M(5) M(6) M(8) M(10) M(16) M(32) - -enum chunk_kind { -#define DEFINE_SMALL_OBJECT_CHUNK_KIND(i) GRANULES_##i, - FOR_EACH_SMALL_OBJECT_GRANULES(DEFINE_SMALL_OBJECT_CHUNK_KIND) -#undef DEFINE_SMALL_OBJECT_CHUNK_KIND - - SMALL_OBJECT_CHUNK_KINDS, - FREE_LARGE_OBJECT = 254, - LARGE_OBJECT = 255 -}; - -static const uint8_t small_object_granule_sizes[] = -{ -#define SMALL_OBJECT_GRANULE_SIZE(i) i, - FOR_EACH_SMALL_OBJECT_GRANULES(SMALL_OBJECT_GRANULE_SIZE) -#undef SMALL_OBJECT_GRANULE_SIZE -}; - -static enum chunk_kind granules_to_chunk_kind(unsigned granules) { -#define TEST_GRANULE_SIZE(i) if (granules <= i) return GRANULES_##i; - FOR_EACH_SMALL_OBJECT_GRANULES(TEST_GRANULE_SIZE); -#undef TEST_GRANULE_SIZE - return LARGE_OBJECT; -} - -static unsigned chunk_kind_to_granules(enum chunk_kind kind) { - switch (kind) { -#define CHUNK_KIND_GRANULE_SIZE(i) case GRANULES_##i: return i; - FOR_EACH_SMALL_OBJECT_GRANULES(CHUNK_KIND_GRANULE_SIZE); -#undef CHUNK_KIND_GRANULE_SIZE - default: - return -1; - } -} - -// Given a pointer P returned by malloc(), we get a header pointer via -// P&~PAGE_MASK, and a chunk index via (P&PAGE_MASK)/CHUNKS_PER_PAGE. If -// chunk_kinds[chunk_idx] is [FREE_]LARGE_OBJECT, then the pointer is a large -// object, otherwise the kind indicates the size in granules of the objects in -// the chunk. -struct page_header { - uint8_t chunk_kinds[CHUNKS_PER_PAGE]; -}; - -struct page { - union { - struct page_header header; - struct chunk chunks[CHUNKS_PER_PAGE]; - }; -}; - -#define PAGE_HEADER_SIZE (sizeof (struct page_header)) -#define FIRST_ALLOCATABLE_CHUNK 1 -STATIC_ASSERT_EQ(PAGE_HEADER_SIZE, FIRST_ALLOCATABLE_CHUNK * CHUNK_SIZE); - -static struct page* get_page(void *ptr) { - return (struct page*) (char*) (((uintptr_t) ptr) & ~PAGE_MASK); -} -static unsigned get_chunk_index(void *ptr) { - return (((uintptr_t) ptr) & PAGE_MASK) / CHUNK_SIZE; -} - -struct freelist { - struct freelist *next; -}; - -struct large_object { - struct large_object *next; - size_t size; -}; - -#define LARGE_OBJECT_HEADER_SIZE (sizeof (struct large_object)) - -static inline void* get_large_object_payload(struct large_object *obj) { - return ((char*) obj) + LARGE_OBJECT_HEADER_SIZE; -} -static inline struct large_object* get_large_object(void *ptr) { - return (struct large_object*) (((char*) ptr) - LARGE_OBJECT_HEADER_SIZE); -} - -static struct freelist *small_object_freelists[SMALL_OBJECT_CHUNK_KINDS]; -static struct large_object *large_objects; - -extern void __heap_base; -static size_t walloc_heap_size; - -static struct page* -allocate_pages(size_t payload_size, size_t *n_allocated) { - size_t needed = payload_size + PAGE_HEADER_SIZE; - size_t heap_size = __builtin_wasm_memory_size(0) * PAGE_SIZE; - uintptr_t base = heap_size; - uintptr_t preallocated = 0, grow = 0; - - if (!walloc_heap_size) { - // We are allocating the initial pages, if any. We skip the first 64 kB, - // then take any additional space up to the memory size. - uintptr_t heap_base = align((uintptr_t)&__heap_base, PAGE_SIZE); - preallocated = heap_size - heap_base; // Preallocated pages. - walloc_heap_size = preallocated; - base -= preallocated; - } - - if (preallocated < needed) { - // Always grow the walloc heap at least by 50%. - grow = align(max(walloc_heap_size / 2, needed - preallocated), - PAGE_SIZE); - ASSERT(grow); - if (__builtin_wasm_memory_grow(0, grow >> PAGE_SIZE_LOG_2) == -1) { - return NULL; - } - walloc_heap_size += grow; - } - - struct page *ret = (struct page *)base; - size_t size = grow + preallocated; - ASSERT(size); - ASSERT_ALIGNED(size, PAGE_SIZE); - *n_allocated = size / PAGE_SIZE; - return ret; -} - -static char* -allocate_chunk(struct page *page, unsigned idx, enum chunk_kind kind) { - page->header.chunk_kinds[idx] = kind; - return page->chunks[idx].data; -} - -// It's possible for splitting to produce a large object of size 248 (256 minus -// the header size) -- i.e. spanning a single chunk. In that case, push the -// chunk back on the GRANULES_32 small object freelist. -static void maybe_repurpose_single_chunk_large_objects_head(void) { - if (large_objects->size < CHUNK_SIZE) { - unsigned idx = get_chunk_index(large_objects); - char *ptr = allocate_chunk(get_page(large_objects), idx, GRANULES_32); - large_objects = large_objects->next; - struct freelist* head = (struct freelist *)ptr; - head->next = small_object_freelists[GRANULES_32]; - small_object_freelists[GRANULES_32] = head; - } -} - -// If there have been any large-object frees since the last large object -// allocation, go through the freelist and merge any adjacent objects. -static int pending_large_object_compact = 0; -static struct large_object** -maybe_merge_free_large_object(struct large_object** prev) { - struct large_object *obj = *prev; - while (1) { - char *end = get_large_object_payload(obj) + obj->size; - ASSERT_ALIGNED((uintptr_t)end, CHUNK_SIZE); - unsigned chunk = get_chunk_index(end); - if (chunk < FIRST_ALLOCATABLE_CHUNK) { - // Merging can't create a large object that newly spans the header chunk. - // This check also catches the end-of-heap case. - return prev; - } - struct page *page = get_page(end); - if (page->header.chunk_kinds[chunk] != FREE_LARGE_OBJECT) { - return prev; - } - struct large_object *next = (struct large_object*) end; - - struct large_object **prev_prev = &large_objects, *walk = large_objects; - while (1) { - ASSERT(walk); - if (walk == next) { - obj->size += LARGE_OBJECT_HEADER_SIZE + walk->size; - *prev_prev = walk->next; - if (prev == &walk->next) { - prev = prev_prev; - } - break; - } - prev_prev = &walk->next; - walk = walk->next; - } - } -} -static void -maybe_compact_free_large_objects(void) { - if (pending_large_object_compact) { - pending_large_object_compact = 0; - struct large_object **prev = &large_objects; - while (*prev) { - prev = &(*maybe_merge_free_large_object(prev))->next; - } - } -} - -// Allocate a large object with enough space for SIZE payload bytes. Returns a -// large object with a header, aligned on a chunk boundary, whose payload size -// may be larger than SIZE, and whose total size (header included) is -// chunk-aligned. Either a suitable allocation is found in the large object -// freelist, or we ask the OS for some more pages and treat those pages as a -// large object. If the allocation fits in that large object and there's more -// than an aligned chunk's worth of data free at the end, the large object is -// split. -// -// The return value's corresponding chunk in the page as starting a large -// object. -static struct large_object* -allocate_large_object(size_t size) { - maybe_compact_free_large_objects(); - struct large_object *best = NULL, **best_prev = &large_objects; - size_t best_size = -1; - for (struct large_object **prev = &large_objects, *walk = large_objects; - walk; - prev = &walk->next, walk = walk->next) { - if (walk->size >= size && walk->size < best_size) { - best_size = walk->size; - best = walk; - best_prev = prev; - if (best_size + LARGE_OBJECT_HEADER_SIZE - == align(size + LARGE_OBJECT_HEADER_SIZE, CHUNK_SIZE)) - // Not going to do any better than this; just return it. - break; - } - } - - if (!best) { - // The large object freelist doesn't have an object big enough for this - // allocation. Allocate one or more pages from the OS, and treat that new - // sequence of pages as a fresh large object. It will be split if - // necessary. - size_t size_with_header = size + sizeof(struct large_object); - size_t n_allocated = 0; - struct page *page = allocate_pages(size_with_header, &n_allocated); - if (!page) { - return NULL; - } - char *ptr = allocate_chunk(page, FIRST_ALLOCATABLE_CHUNK, LARGE_OBJECT); - best = (struct large_object *)ptr; - size_t page_header = ptr - ((char*) page); - best->next = large_objects; - best->size = best_size = - n_allocated * PAGE_SIZE - page_header - LARGE_OBJECT_HEADER_SIZE; - ASSERT(best_size >= size_with_header); - } - - allocate_chunk(get_page(best), get_chunk_index(best), LARGE_OBJECT); - - struct large_object *next = best->next; - *best_prev = next; - - size_t tail_size = (best_size - size) & ~CHUNK_MASK; - if (tail_size) { - // The best-fitting object has 1 or more aligned chunks free after the - // requested allocation; split the tail off into a fresh aligned object. - struct page *start_page = get_page(best); - char *start = get_large_object_payload(best); - char *end = start + best_size; - - if (start_page == get_page(end - tail_size - 1)) { - // The allocation does not span a page boundary; yay. - ASSERT_ALIGNED((uintptr_t)end, CHUNK_SIZE); - } else if (size < PAGE_SIZE - LARGE_OBJECT_HEADER_SIZE - CHUNK_SIZE) { - // If the allocation itself smaller than a page, split off the head, then - // fall through to maybe split the tail. - ASSERT_ALIGNED((uintptr_t)end, PAGE_SIZE); - size_t first_page_size = PAGE_SIZE - (((uintptr_t)start) & PAGE_MASK); - struct large_object *head = best; - allocate_chunk(start_page, get_chunk_index(start), FREE_LARGE_OBJECT); - head->size = first_page_size; - head->next = large_objects; - large_objects = head; - - maybe_repurpose_single_chunk_large_objects_head(); - - struct page *next_page = start_page + 1; - char *ptr = allocate_chunk(next_page, FIRST_ALLOCATABLE_CHUNK, LARGE_OBJECT); - best = (struct large_object *) ptr; - best->size = best_size = best_size - first_page_size - CHUNK_SIZE - LARGE_OBJECT_HEADER_SIZE; - ASSERT(best_size >= size); - start = get_large_object_payload(best); - tail_size = (best_size - size) & ~CHUNK_MASK; - } else { - // A large object that spans more than one page will consume all of its - // tail pages. Therefore if the split traverses a page boundary, round up - // to page size. - ASSERT_ALIGNED((uintptr_t)end, PAGE_SIZE); - size_t first_page_size = PAGE_SIZE - (((uintptr_t)start) & PAGE_MASK); - size_t tail_pages_size = align(size - first_page_size, PAGE_SIZE); - size = first_page_size + tail_pages_size; - tail_size = best_size - size; - } - best->size -= tail_size; - - unsigned tail_idx = get_chunk_index(end - tail_size); - while (tail_idx < FIRST_ALLOCATABLE_CHUNK && tail_size) { - // We would be splitting in a page header; don't do that. - tail_size -= CHUNK_SIZE; - tail_idx++; - } - - if (tail_size) { - struct page *page = get_page(end - tail_size); - char *tail_ptr = allocate_chunk(page, tail_idx, FREE_LARGE_OBJECT); - struct large_object *tail = (struct large_object *) tail_ptr; - tail->next = large_objects; - tail->size = tail_size - LARGE_OBJECT_HEADER_SIZE; - ASSERT_ALIGNED((uintptr_t)(get_large_object_payload(tail) + tail->size), CHUNK_SIZE); - large_objects = tail; - - maybe_repurpose_single_chunk_large_objects_head(); - } - } - - ASSERT_ALIGNED((uintptr_t)(get_large_object_payload(best) + best->size), CHUNK_SIZE); - return best; -} - -static struct freelist* -obtain_small_objects(enum chunk_kind kind) { - struct freelist** whole_chunk_freelist = &small_object_freelists[GRANULES_32]; - void *chunk; - if (*whole_chunk_freelist) { - chunk = *whole_chunk_freelist; - *whole_chunk_freelist = (*whole_chunk_freelist)->next; - } else { - chunk = allocate_large_object(0); - if (!chunk) { - return NULL; - } - } - char *ptr = allocate_chunk(get_page(chunk), get_chunk_index(chunk), kind); - char *end = ptr + CHUNK_SIZE; - struct freelist *next = NULL; - size_t size = chunk_kind_to_granules(kind) * GRANULE_SIZE; - for (size_t i = size; i <= CHUNK_SIZE; i += size) { - struct freelist *head = (struct freelist*) (end - i); - head->next = next; - next = head; - } - return next; -} - -static inline size_t size_to_granules(size_t size) { - return (size + GRANULE_SIZE - 1) >> GRANULE_SIZE_LOG_2; -} -static struct freelist** get_small_object_freelist(enum chunk_kind kind) { - ASSERT(kind < SMALL_OBJECT_CHUNK_KINDS); - return &small_object_freelists[kind]; -} - -static void* -allocate_small(enum chunk_kind kind) { - struct freelist **loc = get_small_object_freelist(kind); - if (!*loc) { - struct freelist *freelist = obtain_small_objects(kind); - if (!freelist) { - return NULL; - } - *loc = freelist; - } - struct freelist *ret = *loc; - *loc = ret->next; - return (void *) ret; -} - -static void* -allocate_large(size_t size) { - struct large_object *obj = allocate_large_object(size); - return obj ? get_large_object_payload(obj) : NULL; -} - -void* -malloc(size_t size) { - size_t granules = size_to_granules(size); - enum chunk_kind kind = granules_to_chunk_kind(granules); - return (kind == LARGE_OBJECT) ? allocate_large(size) : allocate_small(kind); -} - -void -free(void *ptr) { - if (!ptr) return; - struct page *page = get_page(ptr); - unsigned chunk = get_chunk_index(ptr); - uint8_t kind = page->header.chunk_kinds[chunk]; - if (kind == LARGE_OBJECT) { - struct large_object *obj = get_large_object(ptr); - obj->next = large_objects; - large_objects = obj; - allocate_chunk(page, chunk, FREE_LARGE_OBJECT); - pending_large_object_compact = 1; - } else { - size_t granules = kind; - struct freelist **loc = get_small_object_freelist(granules); - struct freelist *obj = ptr; - obj->next = *loc; - *loc = obj; - } -} diff --git a/c-runtime/wasi-libc/c-runtime.h b/c-runtime/wasi-libc/c-runtime.h deleted file mode 100644 index cb4e3cfe6a..0000000000 --- a/c-runtime/wasi-libc/c-runtime.h +++ /dev/null @@ -1,129 +0,0 @@ -#ifndef C_RUNTIME_H_ -#define C_RUNTIME_H_ - -#include -#include -#include -#include - -#include "bool.h" -#include "nat.h" -#include "io.h" -#include "juvix_string.h" - -typedef struct juvix_function { - uintptr_t fun; -} juvix_function_t; - -char* intToStr(int i) { - int length = snprintf(NULL, 0, "%d", i); - char* str = (char*)malloc(length + 1); - snprintf(str, length + 1, "%d", i); - return str; -} - -char* concat(const char* s1, const char* s2) { - const size_t len1 = strlen(s1); - const size_t len2 = strlen(s2); - int i,j=0,count=0; - char* result = (char*)malloc(len1 + len2 + 1); - - for(i=0; i < len1; i++) { - result[i] = s1[i]; - count++; - } - - for(i=count; j < len2; i++) { - result[i] = s2[j]; - j++; - } - - result[len1 + len2] = '\0'; - return result; -} - -// Tries to parse str as a positive integer. -// Returns -1 if parsing fails. -int parsePositiveInt(char *str) { - int result = 0; - char* p = str; - size_t len = strlen(str); - while ((*str >= '0') && (*str <= '9')) - { - result = (result * 10) + ((*str) - '0'); - str++; - } - if (str - p != len) return -1; - return result; -} - -char* readline() { - int i = 0, bytesAlloced = 64; - char* buffer = (char*) malloc(bytesAlloced); - int bufferSize = bytesAlloced; - - for (;;++i) { - int ch; - - if (i == bufferSize - 1) { - bytesAlloced += bytesAlloced; - buffer = (char*) realloc(buffer, bytesAlloced); - bufferSize = bytesAlloced; - } - - ch = getchar(); - if (ch == -1) { - free(buffer); - return 0; - } - if (ch == '\n') break; - buffer[i] = ch; - } - - buffer[i] = '\0'; - return buffer; -} - -int putStr(const char* str) { - fputs(str, stdout); - return fflush(stdout); -} - -int putStrLn(const char* str) { - puts(str); - return fflush(stdout); -} - -int debug(const char* str) { - return putStrLn(str); -} - -prim_io prim_printNat(prim_nat n) { - return putStr(intToStr(n)); -} - -prim_io prim_printString(prim_string s) { - return putStr(s); -} - -prim_io prim_printBool(prim_bool b) { - return putStr(b ? "true" : "false"); -} - -prim_io prim_readline(juvix_function_t* f) { - return ((prim_io(*)(juvix_function_t*, prim_string))f->fun)(f, readline()); -} - -prim_string prim_natToString(prim_nat n) { return intToStr(n); } - -prim_nat prim_stringToNat(prim_string s) { return parsePositiveInt(s); } - -prim_string prim_stringConcat(prim_string s1, prim_string s2) { - return concat(s1, s2); -} - -prim_bool prim_stringEq(prim_string s1, prim_string s2) { - return strcmp(s1, s2) == 0; -} - -#endif // C_RUNTIME_H_ diff --git a/c-runtime/wasi-standalone/c-runtime.h b/c-runtime/wasi-standalone/c-runtime.h deleted file mode 100644 index a4257ed873..0000000000 --- a/c-runtime/wasi-standalone/c-runtime.h +++ /dev/null @@ -1,294 +0,0 @@ -#ifndef C_RUNTIME_H_ -#define C_RUNTIME_H_ - -#include "bool.h" -#include "nat.h" -#include "io.h" -#include "juvix_string.h" - -typedef __SIZE_TYPE__ size_t; -typedef __UINT8_TYPE__ uint8_t; -typedef __UINT16_TYPE__ uint16_t; -typedef __UINT32_TYPE__ uint32_t; -typedef __UINT64_TYPE__ uint64_t; -typedef __UINTPTR_TYPE__ uintptr_t; -typedef __INT64_TYPE__ int64_t; - -typedef struct juvix_function { - uintptr_t fun; -} juvix_function_t; - -/** - * Allocator - */ - -void *malloc(size_t size); -void free(void *p); - -void* memcpy(void *dest, const void *src, size_t n) { - char *csrc = (char*) src; - char *cdest = (char*) dest; - - for (int i=0; i < n; i++) { - cdest[i] = csrc[i]; - } - return dest; -} - -void* realloc(void *ptr, size_t n) { - void* newptr; - newptr = malloc(n); - memcpy(newptr, ptr, n); - free(ptr); - return newptr; -} - -/** - * WASI Definitions - */ - -typedef struct Ciovec { - uint8_t *buf; - uint32_t buf_len; -} Ciovec_t; - -uint16_t fd_write(uint32_t fd, Ciovec_t *iovs_ptr, uint32_t iovs_len, uint32_t *nwritten) - __attribute__(( - __import_module__("wasi_snapshot_preview1"), - __import_name__("fd_write"), - )); - -uint16_t fd_read(uint32_t fd, Ciovec_t *iovs_ptr, uint32_t iovs_len, uint32_t *read) - __attribute__(( - __import_module__("wasi_snapshot_preview1"), - __import_name__("fd_read"), - )); - -_Noreturn void proc_exit(uint32_t rval) - __attribute__(( - __import_module__("wasi_snapshot_preview1"), - __import_name__("proc_exit"), - )); - -/** - * stdlib.h - */ - -#define EXIT_FAILURE 1 - -_Noreturn void exit(int rval) { - proc_exit(rval); -} - -/** - * string.h - */ - -int strcmp(const char *s1, const char *s2) { - while (*s1) { - if (*s1 != *s2) { - break; - } - s1++; - s2++; - } - return *(const unsigned char*)s1 - *(const unsigned char*)s2; -} - -size_t strlen(const char *s) { - const char* p = s; - while(*p!='\0') { - ++p; - } - return p - s; -} - -/** - * Utilities - */ - -/** - * C++ version 0.4 char* style "itoa": - * Written by Lukás Chmela - * Released under GPLv3. - - */ -char* itoa(int value, char* result, int base) { - // check that the base if valid - if (base < 2 || base > 36) { *result = '\0'; return result; } - - char* ptr = result, *ptr1 = result, tmp_char; - int tmp_value; - - do { - tmp_value = value; - value /= base; - *ptr++ = "zyxwvutsrqponmlkjihgfedcba9876543210123456789abcdefghijklmnopqrstuvwxyz" [35 + (tmp_value - value * base)]; - } while ( value ); - - // Apply negative sign - if (tmp_value < 0) *ptr++ = '-'; - *ptr-- = '\0'; - while(ptr1 < ptr) { - tmp_char = *ptr; - *ptr--= *ptr1; - *ptr1++ = tmp_char; - } - return result; -} - -char* intToStr(int i) { - // int will occupy at least one char - size_t len = 1; - - // calculate the size of the digits - int n = i < 0 ? -i : i; - while (n >= 10) { - n /= 10; - len += 1; - } - - // add an extra char for the negative sign - if (i < 0) { - len += 1; - } - - char* buf = (char*)malloc(len + 1); - itoa(i, buf, 10); - return buf; -} - -int strToInt(char *str) -{ - int result; - int puiss; - - result = 0; - puiss = 1; - while (('-' == (*str)) || ((*str) == '+')) - { - if (*str == '-') - puiss = puiss * -1; - str++; - } - while ((*str >= '0') && (*str <= '9')) - { - result = (result * 10) + ((*str) - '0'); - str++; - } - return (result * puiss); -} - -int putStr(const char* str) { - size_t n = strlen(str); - Ciovec_t vec = {.buf = (uint8_t*)str, .buf_len=(uint32_t)n}; - return fd_write(1, &vec, 1, 0); -} - -int putStrLn(const char* str) { - return putStr(str) || putStr("\n"); -} - -int debug(const char* str) { - return putStrLn(str); -} - -prim_io prim_printNat(prim_nat n) { - return putStr(intToStr(n)); -} - -prim_io prim_printString(prim_string s) { - return putStr(s); -} - -prim_io prim_printBool(prim_bool b) { - return putStr(b ? "true" : "false"); -} - -// Tries to parse str as a positive integer. -// Returns -1 if parsing fails. -int parsePositiveInt(char *str) { - int result = 0; - char* p = str; - size_t len = strlen(str); - while ((*str >= '0') && (*str <= '9')) - { - result = (result * 10) + ((*str) - '0'); - str++; - } - if (str - p != len) return -1; - return result; -} - - -char* concat(const char* s1, const char* s2) { - const size_t len1 = strlen(s1); - const size_t len2 = strlen(s2); - int i,j=0,count=0; - char* result = (char*)malloc(len1 + len2 + 1); - - for(i=0; i < len1; i++) { - result[i] = s1[i]; - count++; - } - - for(i=count; j < len2; i++) { - result[i] = s2[j]; - j++; - } - - result[len1 + len2] = '\0'; - return result; -} - -int getchar() { - int ch; - Ciovec_t v = {.buf = (uint8_t*) &ch, .buf_len=1}; - if (fd_read(0, &v, 1, 0) != 0) return -1; - return ch; -} - -char* readline() { - int i = 0, bytesAlloced = 64; - char* buffer = (char*) malloc(bytesAlloced); - int bufferSize = bytesAlloced; - - for (;;++i) { - int ch; - - if (i == bufferSize - 1) { - bytesAlloced += bytesAlloced; - buffer = (char*) realloc(buffer, bytesAlloced); - bufferSize = bytesAlloced; - } - - ch = getchar(); - if (ch == -1) { - free(buffer); - return 0; - } - if (ch == '\n') break; - buffer[i] = ch; - } - - buffer[i] = '\0'; - return buffer; -} - -prim_io prim_readline(juvix_function_t* f) { - return ((prim_io(*)(juvix_function_t*, prim_string))f->fun)(f, readline()); -} - -prim_string prim_natToString(prim_nat n) { return intToStr(n); } - -prim_nat prim_stringToNat(prim_string s) { return parsePositiveInt(s); } - -prim_string prim_stringConcat(prim_string s1, prim_string s2) { - return concat(s1, s2); -} - -prim_bool prim_stringEq(prim_string s1, prim_string s2) { - return strcmp(s1, s2) == 0; -} - -#endif // C_RUNTIME_H_ diff --git a/docs/org/examples/README.org b/docs/org/examples/README.org index 8713b0483a..a2083e7014 100644 --- a/docs/org/examples/README.org +++ b/docs/org/examples/README.org @@ -8,13 +8,6 @@ The following links are clickable versions of their corresponding Juvix programs - [[https://docs.juvix.org/examples/html/PascalsTriangle/PascalsTriangle.html][PascalsTriangle.juvix]] - [[https://docs.juvix.org/examples/html/Collatz/Collatz.html][Collatz.juvix]] - [[https://docs.juvix.org/examples/html/TicTacToe/CLI/CLI.TicTacToe.html][TicTacToe.juvix]] -- [[https://docs.juvix.org/examples/html/ValidityPredicates/SimpleFungibleToken.html][SimpleFungibleToken.juvix]] The [[https://anoma.github.io/juvix-stdlib/][Juvix standard library]] contains common functions that can be used in Juvix programs. - -** Example Juvix Web apps - -The following links navigate to example Juvix programs running as Web apps: - -- [[https://docs.juvix.org/examples/webapp/TicTacToe/Web/][WebTicTacToe]] diff --git a/docs/org/examples/backend-specific/minic-hello-world.org b/docs/org/examples/backend-specific/minic-hello-world.org deleted file mode 100755 index cf07e594b2..0000000000 --- a/docs/org/examples/backend-specific/minic-hello-world.org +++ /dev/null @@ -1,44 +0,0 @@ -* Hello World - -In the following example a Juvix file is compiled using the C backend. - -#+begin_src --- tests/positive/MiniC/HelloWorld/Input.juvix -module Input; - -axiom String : Type; - -compile String { - c ↦ "char*"; -}; - -axiom Action : Type; - -compile Action { - c ↦ "int"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - c ↦ "putStrLn"; -}; - -main : Action; -main := put-str-ln "hello world!"; - -end; -#+end_src - - -The result is compiled to WASM using [[https://llvm.org][Clang]] and then executed using [[https://wasmer.io][wasmer]]. - -NB: Set the =WASI_SYSROOT_PATH= environment variable to the root of the WASI sysroot. See [[../../getting-started/dependencies.md][Installing dependencies]] for instructions on how to install the sysroot. - -#+begin_src shell -cd tests/positive/MiniC/HelloWorld -juvix compile Input.juvix -wasmer Input.wasm -#+end_src - -You should see the output: =hello world!= diff --git a/docs/org/examples/validity-predicates/PolyFungibleToken.org b/docs/org/examples/validity-predicates/PolyFungibleToken.org deleted file mode 100644 index 4f7f4d85eb..0000000000 --- a/docs/org/examples/validity-predicates/PolyFungibleToken.org +++ /dev/null @@ -1,304 +0,0 @@ -# Polymorphic simple fungible token - -#+begin_src --- tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix -module SimpleFungibleTokenImplicit; - -foreign ghc { - import Anoma -}; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -type Bool := - true : Bool - | false : Bool; - -infixr 2 ||; -|| : Bool → Bool → Bool; -|| false a := a; -|| true _ := true; - -infixr 3 &&; -&& : Bool → Bool → Bool; -&& false _ := false; -&& true a := a; - -if : {A : Type} → Bool → A → A → A; -if true a _ := a; -if false _ b := b; - --------------------------------------------------------------------------------- --- Backend Booleans --------------------------------------------------------------------------------- - -axiom BackendBool : Type; - -compile BackendBool { - ghc ↦ "Bool"; -}; - -axiom backend-true : BackendBool; -compile backend-true { - ghc ↦ "True"; -}; - -axiom backend-false : BackendBool; -compile backend-false { - ghc ↦ "False"; -}; - --------------------------------------------------------------------------------- --- Backend Bridge --------------------------------------------------------------------------------- - -foreign ghc { - bool :: Bool -> a -> a -> a - bool True x _ = x - bool False _ y = y -}; - -axiom bool : BackendBool → Bool → Bool → Bool; -compile bool { - ghc ↦ "bool"; -}; - -from-backend-bool : BackendBool → Bool; -from-backend-bool bb := bool bb true false; - --------------------------------------------------------------------------------- --- Functions --------------------------------------------------------------------------------- - -id : {A : Type} → A → A; -id a := a; - --------------------------------------------------------------------------------- --- Integers --------------------------------------------------------------------------------- - -axiom Int : Type; -compile Int { - ghc ↦ "Int"; -}; - -infix 4 <'; -axiom <' : Int → Int → BackendBool; -compile <' { - ghc ↦ "(<)"; -}; - -infix 4 <; -< : Int → Int → Bool; -< i1 i2 := from-backend-bool (i1 <' i2); - -axiom eqInt : Int → Int → BackendBool; -compile eqInt { - ghc ↦ "(==)"; -}; - -infix 4 ==Int; -==Int : Int → Int → Bool; -==Int i1 i2 := from-backend-bool (eqInt i1 i2); - -infixl 6 -; -axiom - : Int -> Int -> Int; -compile - { - ghc ↦ "(-)"; -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - ghc ↦ "(+)"; -}; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -axiom String : Type; -compile String { - ghc ↦ "[Char]"; -}; - -axiom eqString : String → String → BackendBool; -compile eqString { - ghc ↦ "(==)"; -}; - -infix 4 ==String; -==String : String → String → Bool; -==String s1 s2 := from-backend-bool (eqString s1 s2); - --------------------------------------------------------------------------------- --- Lists --------------------------------------------------------------------------------- - -infixr 5 ::; -type List (A : Type) := - nil : List A - | :: : A → List A → List A; - -elem : {A : Type} → (A → A → Bool) → A → List A → Bool; -elem _ _ nil := false; -elem eq s (x :: xs) := eq s x || elem eq s xs; - -foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil := z; -foldl f z (h :: hs) := foldl f (f z h) hs; - --------------------------------------------------------------------------------- --- Pair --------------------------------------------------------------------------------- - -infixr 4 ,; -infixr 2 ×; -type × (A : Type) (B : Type) := - , : A → B → A × B; - --------------------------------------------------------------------------------- --- Maybe --------------------------------------------------------------------------------- - -type Maybe (A : Type) := - nothing : Maybe A | - just : A → Maybe A; - -from-int : Int → Maybe Int; -from-int i := if (i < 0) nothing (just i); - -maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B; -maybe b _ nothing := b; -maybe _ f (just x) := f x; - -from-string : String → Maybe String; -from-string s := if (s ==String "") nothing (just s); - -pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; -pair-from-optionString := maybe (0 , false); - --------------------------------------------------------------------------------- --- Anoma --------------------------------------------------------------------------------- - -axiom readPre : String → Int; -compile readPre { - ghc ↦ "readPre"; -}; - -axiom readPost : String → Int; -compile readPost { - ghc ↦ "readPost"; -}; - -axiom isBalanceKey : String → String → String; -compile isBalanceKey { - ghc ↦ "isBalanceKey"; -}; - -read-pre : String → Maybe Int; -read-pre s := from-int (readPre s); - -read-post : String → Maybe Int; -read-post s := from-int (readPost s); - -is-balance-key : String → String → Maybe String; -is-balance-key token key := from-string (isBalanceKey token key); - -unwrap-default : Maybe Int → Int; -unwrap-default := maybe 0 id; - --------------------------------------------------------------------------------- --- Validity Predicate --------------------------------------------------------------------------------- - -change-from-key : String → Int; -change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); - -check-vp : List String → String → Int → String → Int × Bool; -check-vp verifiers key change owner := - if - (change-from-key key < 0) - -- make sure the spender approved the transaction - (change + (change-from-key key), elem (==String) owner verifiers) - (change + (change-from-key key), true); - -check-keys : String → List String → Int × Bool → String → Int × Bool; -check-keys token verifiers (change , is-success) key := - if - is-success - (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) - (0 , false); - -check-result : Int × Bool → Bool; -check-result (change , all-checked) := (change ==Int 0) && all-checked; - -vp : String → List String → List String → Bool; -vp token keys-changed verifiers := - check-result - (foldl - (check-keys token verifiers) - (0 , true) - keys-changed); - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; -compile Action { - ghc ↦ "IO ()"; -}; - -axiom putStr : String → Action; -compile putStr { - ghc ↦ "putStr"; -}; - -axiom putStrLn : String → Action; -compile putStrLn { - ghc ↦ "putStrLn"; -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; -compile >> { - ghc ↦ "(>>)"; -}; - -show-result : Bool → String; -show-result true := "OK"; -show-result false := "FAIL"; - --------------------------------------------------------------------------------- --- Testing VP --------------------------------------------------------------------------------- - -token : String; -token := "owner-token"; - -owner-address : String; -owner-address := "owner-address"; - -change1-key : String; -change1-key := "change1-key"; - -change2-key : String; -change2-key := "change2-key"; - -verifiers : List String; -verifiers := owner-address :: nil; - -keys-changed : List String; -keys-changed := change1-key :: change2-key :: nil; - -main : Action; -main := - (putStr "VP Status: ") - >> (putStrLn (show-result (vp token keys-changed verifiers))); - -end; -#+end_src diff --git a/docs/org/reference/language/compileblocks.org b/docs/org/reference/language/compileblocks.org deleted file mode 100644 index 9450d073cc..0000000000 --- a/docs/org/reference/language/compileblocks.org +++ /dev/null @@ -1,65 +0,0 @@ -* Compile blocks - -The compile keyword has two arguments: - -- A name of an expression to be compiled. -- A set of compilation rules using the format (=backend= -> =string=) - where the string is the text we inline. - -This is an example: - -#+begin_src haskell -$ cat tests/positive/HelloWorld -... -axiom Action : Type; -compile Action { - c -> "int"; -}; -... -#+end_src - -The following Juvix examples are NOT valid. - -- One can not repeat backend inside a =compile= block. - -#+begin_src haskell -... -axiom Action : Type; -compile Action { - c -> "int"; - c -> "int"; -- -}; -... -#+end_src - -- One name, one compile block, no more. - -#+begin_src haskell -... -axiom Action : Type; -compile Action { - c -> "int"; -}; -compile Action { - c -> "int"; -}; -... -#+end_src - -- A compile block must be in the same module as their name definition. - -#+begin_src haskell -$ cat A.juvix -... -axiom Action : Type; -... -#+end_src - -#+begin_src haskell -$ cat B.juvix -... -compile Action { - c -> "int"; -}; -... -#+end_src diff --git a/docs/org/reference/language/foreign.org b/docs/org/reference/language/foreign.org deleted file mode 100644 index 3dffab2f0d..0000000000 --- a/docs/org/reference/language/foreign.org +++ /dev/null @@ -1,30 +0,0 @@ -* Foreign blocks - -The =foreign= blocks give the developer the ability to introduce any piece of -code in the compiled file. In addition, every foreign block specifies the -backend's name that will include the given code in the body of the foreign -block. - -The following is an example taken from the Juvix standard library. - -#+begin_example -module Integers; -axiom Int : Type; -compile Int { c -> "int" }; - -foreign c { - bool lessThan(int l, int r) { - return l < r; - \} -}; - -type Bool := - true : Bool | - false : Bool; - -infix 4 <'; -axiom <' : Int -> Int -> Bool; -compile <' { - c -> "lessThan"; -}; -#+end_example diff --git a/docs/org/tutorials/learn.org b/docs/org/tutorials/learn.org index 6dea402822..dc9816ad04 100644 --- a/docs/org/tutorials/learn.org +++ b/docs/org/tutorials/learn.org @@ -347,7 +347,7 @@ The constructor =::= is declared as a right-associative infix operator with prio Now one can define the =map= function polymorphically: #+begin_example -map : {A : Type} -> {B : Type} -> (A -> B) -> List A -> List B; +map : {A B : Type} -> (A -> B) -> List A -> List B; map f nil := nil; map f (h :: hs) := f h :: map f hs; #+end_example diff --git a/examples/milestone/ValidityPredicates/Anoma/Base.hs b/examples/milestone/ValidityPredicates/Anoma/Base.hs deleted file mode 100644 index 26d4843a08..0000000000 --- a/examples/milestone/ValidityPredicates/Anoma/Base.hs +++ /dev/null @@ -1,16 +0,0 @@ -module Anoma.Base where - -import Prelude - -readPre :: String -> Int -readPre "change1-key" = 100 -readPre "change2-key" = 90 -readPre _ = -1 - -readPost :: String -> Int -readPost "change1-key" = 90 -readPost "change2-key" = 100 -readPost _ = -1 - -isBalanceKey :: String -> String -> String -isBalanceKey _ _ = "owner-address" diff --git a/examples/milestone/ValidityPredicates/Anoma/Base.juvix b/examples/milestone/ValidityPredicates/Anoma/Base.juvix deleted file mode 100644 index d74bf95f73..0000000000 --- a/examples/milestone/ValidityPredicates/Anoma/Base.juvix +++ /dev/null @@ -1,82 +0,0 @@ -module Anoma.Base; - foreign ghc { - import Anoma.Base - }; - - foreign c { - int readPre(const char *key) { - if (strcmp("change1-key", key)) { - return 100; - \} else if (strcmp("change2-key", key)) { - return 90; - \} else { - return -1; - \} - \} - - int readPost(const char *key) { - if (strcmp("change1-key", key)) { - return 90; - \} else if (strcmp("change2-key", key)) { - return 100; - \} else { - return -1; - \} - \} - - char* isBalanceKey(const char* s1, const char* s2) { - return "owner-address"; - \} - }; - - open import Stdlib.Prelude; - open import Data.Int; - open import Data.Int.Ops; - - import Stdlib.Data.String.Ord; - - from-int : Int → Maybe Int; - from-int i := if (i < Int_0) nothing (just i); - - from-string : String → Maybe String; - from-string s := - if (s Stdlib.Data.String.Ord.== "") nothing (just s); - - --- ----------------------------------------------------------------------------- - - -- Anoma - --- ----------------------------------------------------------------------------- - axiom readPre : String → Int; - - compile readPre { - c ↦ "readPre"; - ghc ↦ "readPre"; - }; - - axiom readPost : String → Int; - - compile readPost { - c ↦ "readPost"; - ghc ↦ "readPost"; - }; - - axiom isBalanceKey : String → String → String; - - compile isBalanceKey { - c ↦ "isBalanceKey"; - ghc ↦ "isBalanceKey"; - }; - - read-pre : String → Maybe Int; - read-pre s := from-int (readPre s); - - read-post : String → Maybe Int; - read-post s := from-int (readPost s); - - is-balance-key : String → String → Maybe String; - is-balance-key token key := - from-string (isBalanceKey token key); - - unwrap-default : Maybe Int → Int; - unwrap-default := maybe Int_0 id; -end; diff --git a/examples/milestone/ValidityPredicates/Data/Int.juvix b/examples/milestone/ValidityPredicates/Data/Int.juvix deleted file mode 100644 index 6738e93b2a..0000000000 --- a/examples/milestone/ValidityPredicates/Data/Int.juvix +++ /dev/null @@ -1,19 +0,0 @@ -module Data.Int; - axiom Int : Type; - - compile Int { - c ↦ "int"; - }; - - axiom Int_0 : Int; - - compile Int_0 { - c ↦ "0"; - }; - - axiom Int_1 : Int; - - compile Int_1 { - c ↦ "1"; - }; -end; diff --git a/examples/milestone/ValidityPredicates/Data/Int/Ops.juvix b/examples/milestone/ValidityPredicates/Data/Int/Ops.juvix deleted file mode 100644 index 52acf1d226..0000000000 --- a/examples/milestone/ValidityPredicates/Data/Int/Ops.juvix +++ /dev/null @@ -1,56 +0,0 @@ -module Data.Int.Ops; - open import Data.Int; - open import Stdlib.Data.Bool; - - foreign c { - bool lessThan(int l, int r) { - return l < r; - \} - - bool eqInt(int l, int r) { - return l == r; - \} - - int plus(int l, int r) { - return l + r; - \} - - int minus(int l, int r) { - return l - r; - \} - }; - - infix 4 <; - axiom < : Int → Int → Bool; - - compile < { - c ↦ "lessThan"; - }; - - axiom eqInt : Int → Int → Bool; - - compile eqInt { - c ↦ "eqInt"; - }; - - infix 4 ==; - axiom == : Int → Int → Bool; - - compile == { - c ↦ "eqInt"; - }; - - infixl 6 -; - axiom - : Int → Int → Int; - - compile - { - c ↦ "minus"; - }; - - infixl 6 +; - axiom + : Int → Int → Int; - - compile + { - c ↦ "plus"; - }; -end; diff --git a/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix b/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix deleted file mode 100644 index b9417ea7db..0000000000 --- a/examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix +++ /dev/null @@ -1,52 +0,0 @@ -module SimpleFungibleToken; - open import Anoma.Base; - open import Stdlib.Prelude; - - import Stdlib.Data.String.Ord; - - open import Data.Int; - - import Data.Int.Ops; - - -- Misc - pair-from-optionString : (String → Int × Bool) → Maybe - String → Int × Bool; - pair-from-optionString := maybe (Int_0, false); - - -- Validity Predicate - change-from-key : String → Int; - change-from-key key := - unwrap-default (read-post key) - Data.Int.Ops.- unwrap-default (read-pre key); - - check-vp : List String → String → Int → String → Int × Bool; - check-vp verifiers key change owner := - if - (change-from-key key Data.Int.Ops.< Int_0) - (change Data.Int.Ops.+ change-from-key key - , elem (Stdlib.Data.String.Ord.==) owner verifiers) - (change Data.Int.Ops.+ change-from-key key, true); - - -- make sure the spender approved the transaction - check-keys : String → List String → Int - × Bool → String → Int × Bool; - check-keys token verifiers (change , is-success) key := - if - is-success - (pair-from-optionString - (check-vp verifiers key change) - (is-balance-key token key)) - (Int_0, false); - - check-result : Int × Bool → Bool; - check-result (change , all-checked) := - change Data.Int.Ops.== Int_0 && all-checked; - - vp : String → List String → List String → Bool; - vp token keys-changed verifiers := - check-result - (foldl - (check-keys token verifiers) - (Int_0, true) - keys-changed); -end; diff --git a/examples/milestone/ValidityPredicates/Tests.juvix b/examples/milestone/ValidityPredicates/Tests.juvix deleted file mode 100644 index 5ad0d34f96..0000000000 --- a/examples/milestone/ValidityPredicates/Tests.juvix +++ /dev/null @@ -1,36 +0,0 @@ -module Tests; - open import Stdlib.Prelude; - open import SimpleFungibleToken; - - --- ----------------------------------------------------------------------------- - - -- Testing VP - --- ----------------------------------------------------------------------------- - token : String; - token := "owner-token"; - - owner-address : String; - owner-address := "owner-address"; - - change1-key : String; - change1-key := "change1-key"; - - change2-key : String; - change2-key := "change2-key"; - - verifiers : List String; - verifiers := owner-address :: nil; - - keys-changed : List String; - keys-changed := change1-key :: change2-key :: nil; - - show-result : Bool → String; - show-result true := "OK"; - show-result false := "FAIL"; - - main : IO; - main := - printString "VP Status: " - >> printStringLn - (show-result (vp token keys-changed verifiers)); -end; diff --git a/examples/milestone/ValidityPredicates/juvix.yaml b/examples/milestone/ValidityPredicates/juvix.yaml deleted file mode 100644 index 67134a4998..0000000000 --- a/examples/milestone/ValidityPredicates/juvix.yaml +++ /dev/null @@ -1,2 +0,0 @@ -name: ValidityPredicates -version: 0.1.0 diff --git a/package.yaml b/package.yaml index 248a30cf7a..9860868f4e 100644 --- a/package.yaml +++ b/package.yaml @@ -22,8 +22,6 @@ extra-source-files: - juvix-stdlib/**/*.juvix - runtime/include/**/*.h - runtime/**/*.a -- c-runtime/**/*.h -- c-runtime/walloc/walloc.c dependencies: - aeson == 2.0.* diff --git a/src/Juvix/Compiler/Abstract/Data/InfoTable.hs b/src/Juvix/Compiler/Abstract/Data/InfoTable.hs index a6a5f87e4f..9b66ee17b4 100644 --- a/src/Juvix/Compiler/Abstract/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Abstract/Data/InfoTable.hs @@ -1,7 +1,6 @@ module Juvix.Compiler.Abstract.Data.InfoTable where import Juvix.Compiler.Abstract.Language -import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Prelude newtype FunctionInfo = FunctionInfo @@ -26,8 +25,7 @@ data InfoTable = InfoTable { _infoConstructors :: HashMap ConstructorRef ConstructorInfo, _infoAxioms :: HashMap AxiomRef AxiomInfo, _infoInductives :: HashMap InductiveRef InductiveInfo, - _infoFunctions :: HashMap FunctionRef FunctionInfo, - _infoCompilationRules :: HashMap S.Symbol [BackendItem] + _infoFunctions :: HashMap FunctionRef FunctionInfo } emptyInfoTable :: InfoTable @@ -36,8 +34,7 @@ emptyInfoTable = { _infoConstructors = mempty, _infoAxioms = mempty, _infoInductives = mempty, - _infoFunctions = mempty, - _infoCompilationRules = mempty + _infoFunctions = mempty } makeLenses ''InfoTable diff --git a/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs index 80366a92e8..c85cb1fa80 100644 --- a/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs +++ b/src/Juvix/Compiler/Abstract/Extra/DependencyBuilder.hs @@ -88,7 +88,6 @@ goStatement modName = \case checkStartNode (ax ^. axiomName) addEdge (ax ^. axiomName) modName goExpression (ax ^. axiomName) (ax ^. axiomType) - StatementForeign {} -> return () StatementFunction f -> goTopFunctionDef modName f StatementImport m -> guardNotVisited (m ^. moduleName) (goModule m) StatementLocalModule m -> goLocalModule modName m diff --git a/src/Juvix/Compiler/Abstract/Language.hs b/src/Juvix/Compiler/Abstract/Language.hs index 4455bc4dff..f9a4de4862 100644 --- a/src/Juvix/Compiler/Abstract/Language.hs +++ b/src/Juvix/Compiler/Abstract/Language.hs @@ -14,7 +14,7 @@ where import Juvix.Compiler.Abstract.Data.Name import Juvix.Compiler.Concrete.Data.Builtins import Juvix.Compiler.Concrete.Data.Literal -import Juvix.Compiler.Concrete.Language (BackendItem, ForeignBlock (..), symbolLoc) +import Juvix.Compiler.Concrete.Language (symbolLoc) import Juvix.Data.Hole import Juvix.Data.IsImplicit import Juvix.Data.Universe @@ -43,7 +43,6 @@ data Statement = StatementInductive InductiveDef | StatementFunction FunctionDef | StatementImport TopModule - | StatementForeign ForeignBlock | StatementLocalModule LocalModule | StatementAxiom AxiomDef deriving stock (Eq, Show) diff --git a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs index 0e823532e8..f84d8534c8 100644 --- a/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs +++ b/src/Juvix/Compiler/Abstract/Translation/FromConcrete.hs @@ -147,11 +147,9 @@ goStatement (Indexed idx s) = StatementOperator {} -> return Nothing StatementOpenModule o -> goOpenModule o StatementInductive i -> Just . Abstract.StatementInductive <$> goInductive i - StatementForeign f -> return (Just (Abstract.StatementForeign f)) StatementModule f -> Just . Abstract.StatementLocalModule <$> goLocalModule f StatementTypeSignature {} -> return Nothing StatementFunctionClause {} -> return Nothing - StatementCompile {} -> return Nothing goOpenModule :: forall r. diff --git a/src/Juvix/Compiler/Backend/C/Data/Base.hs b/src/Juvix/Compiler/Backend/C/Data/Base.hs deleted file mode 100644 index c208363ddb..0000000000 --- a/src/Juvix/Compiler/Backend/C/Data/Base.hs +++ /dev/null @@ -1,340 +0,0 @@ -module Juvix.Compiler.Backend.C.Data.Base - ( module Juvix.Compiler.Backend.C.Data.Base, - module Juvix.Compiler.Backend.C.Data.Types, - module Juvix.Compiler.Backend.C.Data.CNames, - ) -where - -import Data.HashMap.Strict qualified as HashMap -import Data.Text qualified as T -import Juvix.Compiler.Backend.C.Data.BuiltinTable -import Juvix.Compiler.Backend.C.Data.CNames -import Juvix.Compiler.Backend.C.Data.Types -import Juvix.Compiler.Backend.C.Language -import Juvix.Compiler.Internal.Extra (mkPolyType') -import Juvix.Compiler.Internal.Extra qualified as Internal -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Internal -import Juvix.Extra.Strings qualified as Str -import Juvix.Prelude - -unsupported :: Text -> a -unsupported msg = error (msg <> " Internal to C: not yet supported") - --- The direct use of Internal.PolyType is safe here -unfoldFunType :: Internal.PolyType -> ([Internal.PolyType], Internal.PolyType) -unfoldFunType t = (map (Internal.PolyType . (^. Internal.paramType)) params, Internal.PolyType ret) - where - (params, ret) = Internal.unfoldFunType (t ^. Internal.unpolyType) - -unfoldPolyApp :: (Member (Reader Internal.TypesTable) r) => Internal.Application -> Sem r (Internal.Expression, [Internal.Expression]) -unfoldPolyApp a = - let (f, args) = Internal.unfoldApplication a - in case f of - Internal.ExpressionLiteral {} -> return (f, toList args) - Internal.ExpressionIden iden -> do - args' <- filterCompileTimeArgsOrPatterns (Internal.getName iden) (toList args) - return (f, args') - _ -> impossible - -filterCompileTimeArgsOrPatterns :: (Member (Reader Internal.TypesTable) r) => Internal.Name -> [a] -> Sem r [a] -filterCompileTimeArgsOrPatterns idenName lst = do - tab <- ask - return $ - map fst $ - filter (not . isUniverse . snd) $ - zip lst (map (^. Internal.paramType) (fst (Internal.unfoldFunType (ty tab)))) - where - ty = HashMap.lookupDefault impossible idenName - isUniverse :: Internal.Expression -> Bool - isUniverse = \case - (Internal.ExpressionUniverse {}) -> True - _ -> False - -mkName :: Internal.Name -> Text -mkName n = - adaptFirstLetter lexeme <> nameTextSuffix - where - lexeme - | T.null lexeme' = "v" - | otherwise = lexeme' - where - lexeme' = T.filter isValidChar (n ^. Internal.nameText) - isValidChar :: Char -> Bool - isValidChar c = isLetter c && isAscii c - adaptFirstLetter :: Text -> Text - adaptFirstLetter t = case T.uncons t of - Nothing -> impossible - Just (h, r) -> T.cons (capitalize h) r - where - capitalize :: Char -> Char - capitalize - | capital = toUpper - | otherwise = toLower - capital = case n ^. Internal.nameKind of - Internal.KNameConstructor -> True - Internal.KNameInductive -> True - Internal.KNameTopModule -> True - Internal.KNameLocalModule -> True - _ -> False - nameTextSuffix :: Text - nameTextSuffix = case n ^. Internal.nameKind of - Internal.KNameTopModule -> mempty - Internal.KNameFunction -> - if n ^. Internal.nameText == Str.main then mempty else idSuffix - _ -> idSuffix - idSuffix :: Text - idSuffix = "_" <> show (n ^. Internal.nameId . Internal.unNameId) - -goType :: forall r. (Member (Reader Internal.InfoTable) r) => Internal.PolyType -> Sem r CDeclType -goType t = case t ^. Internal.unpolyType of - Internal.ExpressionIden ti -> getInternalType ti - Internal.ExpressionFunction {} -> return declFunctionPtrType - Internal.ExpressionUniverse {} -> unsupported "TypeUniverse" - Internal.ExpressionApplication a -> goType (mkPolyType' (fst (Internal.unfoldApplication a))) - Internal.ExpressionLiteral {} -> impossible - Internal.ExpressionHole {} -> impossible - Internal.ExpressionSimpleLambda {} -> impossible - Internal.ExpressionLambda {} -> impossible - Internal.ExpressionLet {} -> impossible - Internal.ExpressionCase {} -> impossible - where - getInternalType :: Internal.Iden -> Sem r CDeclType - getInternalType = \case - Internal.IdenInductive mn -> getInductiveCType mn - Internal.IdenAxiom mn -> do - axiomName <- getAxiomCName mn - return - CDeclType - { _typeDeclType = DeclTypeDefType axiomName, - _typeIsPtr = False - } - Internal.IdenVar {} -> - return - CDeclType - { _typeDeclType = uIntPtrType, - _typeIsPtr = False - } - _ -> impossible - -typeToFunType :: (Member (Reader Internal.InfoTable) r) => Internal.PolyType -> Sem r CFunType -typeToFunType t = do - let (args, ret) = unfoldFunType t - _cFunArgTypes <- mapM goType args - _cFunReturnType <- goType ret - return CFunType {..} - -applyOnFunStatement :: - forall a. (Monoid a) => (Internal.FunctionDef -> a) -> Internal.Statement -> a -applyOnFunStatement f = \case - Internal.StatementFunction (Internal.MutualBlock x) -> mconcatMap f x - Internal.StatementForeign {} -> mempty - Internal.StatementAxiom {} -> mempty - Internal.StatementInductive {} -> mempty - Internal.StatementInclude i -> mconcat $ map (applyOnFunStatement f) (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements) - -getConstructorCName :: (Members '[Reader Internal.InfoTable] r) => Internal.Name -> Sem r Text -getConstructorCName n = do - ctorInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoConstructors) - return - ( case ctorInfo ^. Internal.constructorInfoBuiltin of - Just builtin -> fromJust (builtinConstructorName builtin) - Nothing -> mkName n - ) - -getAxiomCName :: (Members '[Reader Internal.InfoTable] r) => Internal.Name -> Sem r Text -getAxiomCName n = do - axiomInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoAxioms) - return - ( case axiomInfo ^. Internal.axiomInfoBuiltin of - Just builtin -> fromJust (builtinAxiomName builtin) - Nothing -> mkName n - ) - -getInductiveCName :: (Members '[Reader Internal.InfoTable] r) => Internal.Name -> Sem r (Bool, Text) -getInductiveCName n = do - inductiveInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoInductives) - return - ( case inductiveInfo ^. (Internal.inductiveInfoDef . Internal.inductiveBuiltin) of - Just builtin -> (False, fromJust (builtinInductiveName builtin)) - Nothing -> (True, asTypeDef (mkName n)) - ) - -getInductiveCType :: (Member (Reader Internal.InfoTable) r) => Internal.Name -> Sem r CDeclType -getInductiveCType n = do - (isPtr, name) <- getInductiveCName n - return - ( CDeclType - { _typeDeclType = DeclTypeDefType name, - _typeIsPtr = isPtr - } - ) - -typeOfConstructor :: (Member (Reader Internal.InfoTable) r) => Internal.Name -> Sem r CDeclType -typeOfConstructor name = do - info <- Internal.lookupConstructor name - getInductiveCType (info ^. Internal.constructorInfoInductive) - -getClausePatternArgs :: (Member (Reader Internal.TypesTable) r) => Internal.FunctionClause -> Sem r [Internal.PatternArg] -getClausePatternArgs c = - filterCompileTimeArgsOrPatterns - (c ^. Internal.clauseName) - (c ^. Internal.clausePatterns) - -getClausePatterns :: (Member (Reader Internal.TypesTable) r) => Internal.FunctionClause -> Sem r [Internal.Pattern] -getClausePatterns c = (^.. each . Internal.patternArgPattern) <$> getClausePatternArgs c - -functionInfoPatternsNum :: (Member (Reader Internal.TypesTable) r) => Internal.FunctionInfo -> Sem r Int -functionInfoPatternsNum fInfo = do - let c = head (fInfo ^. (Internal.functionInfoDef . Internal.funDefClauses)) - pats <- getClausePatternArgs c - return (length pats) - -buildPatternInfoTable :: forall r. (Members '[Reader Internal.InfoTable, Reader Internal.TypesTable] r) => [Internal.PolyType] -> Internal.FunctionClause -> Sem r PatternInfoTable -buildPatternInfoTable argTyps c = - PatternInfoTable . HashMap.fromList <$> patBindings - where - funArgBindings :: Sem r [(Expression, CFunType)] - funArgBindings = mapM (bimapM (return . ExpressionVar) typeToFunType) (zip funArgs argTyps) - - patArgBindings :: Sem r [(Internal.PatternArg, (Expression, CFunType))] - patArgBindings = do - pats <- getClausePatternArgs c - zip pats <$> funArgBindings - - patBindings :: Sem r [(Text, BindingInfo)] - patBindings = patArgBindings >>= concatMapM go - - go :: (Internal.PatternArg, (Expression, CFunType)) -> Sem r [(Text, BindingInfo)] - go p = do - r <- goPat p - return $ goName p ++ r - - goName :: (Internal.PatternArg, (Expression, CFunType)) -> [(Text, BindingInfo)] - goName (p, (exp, typ)) = case p ^. Internal.patternArgName of - Just n -> [(n ^. Internal.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})] - Nothing -> [] - - goPat :: (Internal.PatternArg, (Expression, CFunType)) -> Sem r [(Text, BindingInfo)] - goPat (p, (exp, typ)) = case p ^. Internal.patternArgPattern of - Internal.PatternVariable v -> - return - [(v ^. Internal.nameText, BindingInfo {_bindingInfoExpr = exp, _bindingInfoType = typ})] - Internal.PatternConstructorApp Internal.ConstructorApp {..} -> - goConstructorApp exp _constrAppConstructor _constrAppParameters - - goConstructorApp :: Expression -> Internal.Name -> [Internal.PatternArg] -> Sem r [(Text, BindingInfo)] - goConstructorApp exp constructorName ps = do - ctorInfo' <- ctorInfo - let ctorArgBindings :: Sem r [(Expression, CFunType)] = - mapM (bimapM asConstructor typeToFunType) (zip ctorArgs ctorInfo') - patternCtorArgBindings :: Sem r [(Internal.PatternArg, (Expression, CFunType))] = zip ps <$> ctorArgBindings - patternCtorArgBindings >>= concatMapM go - where - ctorInfo :: Sem r [Internal.PolyType] - ctorInfo = do - p' :: HashMap Internal.Name Internal.ConstructorInfo <- asks (^. Internal.infoConstructors) - let fInfo = HashMap.lookupDefault impossible constructorName p' - return $ map mkPolyType' (fInfo ^. Internal.constructorInfoArgs) - - asConstructor :: Text -> Sem r Expression - asConstructor ctorArg = do - name <- getConstructorCName constructorName - ty <- typeOfConstructor constructorName - return (functionCall (ExpressionVar (asProjName ctorArg name)) [castToType ty exp]) - -getType :: - (Members '[Reader Internal.InfoTable, Reader Internal.TypesTable, Reader PatternInfoTable] r) => - Internal.Iden -> - Sem r (CFunType, CArity) -getType = \case - Internal.IdenFunction n -> do - fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoFunctions) - funTyp <- typeToFunType (mkPolyType' (fInfo ^. (Internal.functionInfoDef . Internal.funDefType))) - nPatterns <- functionInfoPatternsNum fInfo - return (funTyp, nPatterns) - Internal.IdenConstructor n -> do - fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoConstructors) - argTypes <- mapM (goType . mkPolyType') (fInfo ^. Internal.constructorInfoArgs) - typ <- goType $ mkPolyType' (Internal.ExpressionIden (Internal.IdenInductive (fInfo ^. Internal.constructorInfoInductive))) - return - ( CFunType - { _cFunArgTypes = argTypes, - _cFunReturnType = typ - }, - length argTypes - ) - Internal.IdenAxiom n -> do - fInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoAxioms) - t <- typeToFunType (mkPolyType' (fInfo ^. Internal.axiomInfoType)) - return (t, length (t ^. cFunArgTypes)) - Internal.IdenVar n -> do - t <- (^. bindingInfoType) . HashMap.lookupDefault impossible (n ^. Internal.nameText) <$> asks (^. patternBindings) - return (t, length (t ^. cFunArgTypes)) - Internal.IdenInductive _ -> impossible - -namedArgs :: (Text -> Text) -> [CDeclType] -> [Declaration] -namedArgs prefix = zipWith namedCDecl argLabels - where - argLabels :: [Text] - argLabels = prefix . show <$> [0 :: Integer ..] - -namedDecl :: Text -> Bool -> DeclType -> Declaration -namedDecl n isPtr typ = - Declaration - { _declType = typ, - _declIsPtr = isPtr, - _declName = Just n, - _declInitializer = Nothing - } - -namedCDecl :: Text -> CDeclType -> Declaration -namedCDecl n CDeclType {..} = namedDecl n _typeIsPtr _typeDeclType - -declFunctionType :: DeclType -declFunctionType = DeclTypeDefType Str.juvixFunctionT - -declFunctionPtrType :: CDeclType -declFunctionPtrType = - CDeclType - { _typeDeclType = declFunctionType, - _typeIsPtr = True - } - -funPtrType :: CFunType -> CDeclType -funPtrType CFunType {..} = - CDeclType - { _typeDeclType = - DeclFunPtr - ( FunPtr - { _funPtrReturnType = _cFunReturnType ^. typeDeclType, - _funPtrIsPtr = _cFunReturnType ^. typeIsPtr, - _funPtrArgs = _cFunArgTypes - } - ), - _typeIsPtr = False - } - -mallocSizeOf :: Text -> Expression -mallocSizeOf typeName = - functionCall (ExpressionVar Str.malloc) [functionCall (ExpressionVar Str.sizeof) [ExpressionVar typeName]] - -functionCallCasted :: CFunType -> Expression -> [Expression] -> Expression -functionCallCasted fType fExpr args = - functionCall fExpr (zipWith castToType (fType ^. cFunArgTypes) args) - -juvixFunctionCall :: CFunType -> Expression -> [Expression] -> Expression -juvixFunctionCall funType funParam args = - functionCallCasted fTyp (castToType (funPtrType fTyp) (memberAccess Pointer funParam "fun")) (funParam : args) - where - fTyp :: CFunType - fTyp = funType {_cFunArgTypes = declFunctionPtrType : (funType ^. cFunArgTypes)} - -cFunTypeToFunSig :: Text -> CFunType -> FunctionSig -cFunTypeToFunSig name CFunType {..} = - FunctionSig - { _funcReturnType = _cFunReturnType ^. typeDeclType, - _funcIsPtr = _cFunReturnType ^. typeIsPtr, - _funcQualifier = None, - _funcName = name, - _funcArgs = namedArgs asFunArg _cFunArgTypes - } diff --git a/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs b/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs deleted file mode 100644 index d58b64ed6e..0000000000 --- a/src/Juvix/Compiler/Backend/C/Data/BuiltinTable.hs +++ /dev/null @@ -1,55 +0,0 @@ -module Juvix.Compiler.Backend.C.Data.BuiltinTable where - -import Juvix.Compiler.Backend.C.Data.CNames -import Juvix.Compiler.Concrete.Data.Builtins -import Juvix.Prelude - -builtinConstructorName :: BuiltinConstructor -> Maybe Text -builtinConstructorName = \case - BuiltinNatZero -> Just zero - BuiltinNatSuc -> Just suc - BuiltinBoolTrue -> Just true_ - BuiltinBoolFalse -> Just false_ - -builtinInductiveName :: BuiltinInductive -> Maybe Text -builtinInductiveName = \case - BuiltinNat -> Just nat - BuiltinBool -> Just bool_ - -builtinAxiomName :: BuiltinAxiom -> Maybe Text -builtinAxiomName = \case - BuiltinNatPrint -> Just printNat - BuiltinNatToString -> Just natToString - BuiltinIO -> Just io - BuiltinIOSequence -> Just ioseq - BuiltinIOReadline -> Just ioreadline - BuiltinString -> Just string_ - BuiltinStringPrint -> Just printString - BuiltinStringConcat -> Just stringConcat - BuiltinStringEq -> Just stringEq - BuiltinStringToNat -> Just stringToNat - BuiltinBoolPrint -> Just printBool - BuiltinTrace -> Just trace_ - BuiltinFail -> Just fail_ - -builtinFunctionName :: BuiltinFunction -> Maybe Text -builtinFunctionName = \case - BuiltinNatPlus -> Just natplus - BuiltinNatSub -> Just natsub - BuiltinNatMul -> Just natmul - BuiltinNatUDiv -> Just natudiv - BuiltinNatDiv -> Just natdiv - BuiltinNatMod -> Just natmod - BuiltinNatLe -> Just natle - BuiltinNatLt -> Just natlt - BuiltinNatEq -> Just nateq - BuiltinBoolIf -> Just boolif - BuiltinBoolOr -> Just boolor - BuiltinBoolAnd -> Just booland - -builtinName :: BuiltinPrim -> Maybe Text -builtinName = \case - BuiltinsInductive i -> builtinInductiveName i - BuiltinsConstructor i -> builtinConstructorName i - BuiltinsAxiom i -> builtinAxiomName i - BuiltinsFunction i -> builtinFunctionName i diff --git a/src/Juvix/Compiler/Backend/C/Data/CNames.hs b/src/Juvix/Compiler/Backend/C/Data/CNames.hs deleted file mode 100644 index 368d9c1a9d..0000000000 --- a/src/Juvix/Compiler/Backend/C/Data/CNames.hs +++ /dev/null @@ -1,168 +0,0 @@ -module Juvix.Compiler.Backend.C.Data.CNames where - -import Juvix.Prelude - -primPrefix :: Text -> Text -primPrefix = ("prim_" <>) - -zero :: Text -zero = primPrefix "zero" - -suc :: Text -suc = primPrefix "suc" - -printNat :: Text -printNat = primPrefix "printNat" - -natToString :: Text -natToString = primPrefix "natToString" - -printString :: Text -printString = primPrefix "printString" - -stringConcat :: Text -stringConcat = primPrefix "stringConcat" - -stringEq :: Text -stringEq = primPrefix "stringEq" - -stringToNat :: Text -stringToNat = primPrefix "stringToNat" - -io :: Text -io = primPrefix "io" - -string_ :: Text -string_ = primPrefix "string" - -nat :: Text -nat = primPrefix "nat" - -bool_ :: Text -bool_ = primPrefix "bool" - -true_ :: Text -true_ = primPrefix "true" - -false_ :: Text -false_ = primPrefix "false" - -printBool :: Text -printBool = primPrefix "printBool" - -int_ :: Text -int_ = "int" - -ioseq :: Text -ioseq = primPrefix "sequence" - -ioreadline :: Text -ioreadline = primPrefix "readline" - -natplus :: Text -natplus = primPrefix "natplus" - -natsub :: Text -natsub = primPrefix "natsub" - -natmul :: Text -natmul = primPrefix "natmul" - -natudiv :: Text -natudiv = primPrefix "natudiv" - -natdiv :: Text -natdiv = primPrefix "natdiv" - -natmod :: Text -natmod = primPrefix "natmod" - -natle :: Text -natle = primPrefix "natle" - -natlt :: Text -natlt = primPrefix "natlt" - -nateq :: Text -nateq = primPrefix "nateq" - -boolif :: Text -boolif = primPrefix "if" - -boolor :: Text -boolor = primPrefix "or" - -booland :: Text -booland = primPrefix "and" - -trace_ :: Text -trace_ = "trace" - -fail_ :: Text -fail_ = "fail" - -funField :: Text -funField = "fun" - -asStruct :: Text -> Text -asStruct n = n <> "_s" - -asTypeDef :: Text -> Text -asTypeDef n = n <> "_t" - -asTag :: Text -> Text -asTag n = n <> "_tag" - -asField :: Text -> Text -asField n = n <> "_field" - -asNullary :: Text -> Text -asNullary n = n <> "_nullary" - -asCast :: Text -> Text -asCast n = "as_" <> n - -asProjName :: Text -> Text -> Text -asProjName argName n = "proj_" <> argName <> "_" <> n - -asProj :: Int -> Text -> Text -asProj argIdx n = asProjName (asCtorArg (show argIdx)) n - -asIs :: Text -> Text -asIs n = "is_" <> n - -asNew :: Text -> Text -asNew n = "new_" <> n - -asFun :: Text -> Text -asFun n = n <> "_fun" - -asEval :: Text -> Text -asEval n = n <> "_eval" - -asApply :: Text -> Text -asApply n = n <> "_apply" - -asEnv :: Text -> Text -asEnv n = n <> "_env" - -asFunArg :: Text -> Text -asFunArg n = "fa" <> n - -asCtorArg :: Text -> Text -asCtorArg n = "ca" <> n - -asEnvArg :: Text -> Text -asEnvArg n = "ea" <> n - -mkArgs :: (Text -> Text) -> [Text] -mkArgs f = map (f . show) [0 :: Integer ..] - -funArgs :: [Text] -funArgs = mkArgs asFunArg - -ctorArgs :: [Text] -ctorArgs = mkArgs asCtorArg - -envArgs :: [Text] -envArgs = mkArgs asEnvArg diff --git a/src/Juvix/Compiler/Backend/C/Data/Closure.hs b/src/Juvix/Compiler/Backend/C/Data/Closure.hs deleted file mode 100644 index 2f4ed9f9c9..0000000000 --- a/src/Juvix/Compiler/Backend/C/Data/Closure.hs +++ /dev/null @@ -1,290 +0,0 @@ -module Juvix.Compiler.Backend.C.Data.Closure where - -import Juvix.Compiler.Backend.C.Data.Base -import Juvix.Compiler.Backend.C.Language -import Juvix.Compiler.Concrete.Data.Builtins (IsBuiltin (toBuiltinPrim)) -import Juvix.Compiler.Internal.Extra (mkPolyType') -import Juvix.Compiler.Internal.Extra qualified as Micro -import Juvix.Compiler.Internal.Translation.Extra qualified as Micro -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Micro -import Juvix.Prelude - -genClosures :: - forall r. - (Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r) => - Micro.Module -> - Sem r [CCode] -genClosures Micro.Module {..} = do - closureInfos <- concatMapM (applyOnFunStatement functionDefClosures) (_moduleBody ^. Micro.moduleStatements) - return (genCClosure =<< nub closureInfos) - -genCClosure :: ClosureInfo -> [CCode] -genCClosure c = - [ ExternalDecl (genClosureEnv c), - ExternalFunc (genClosureApply c), - ExternalFunc (genClosureEval c) - ] - -functionDefClosures :: - (Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r) => - Micro.FunctionDef -> - Sem r [ClosureInfo] -functionDefClosures Micro.FunctionDef {..} = - concatMapM (clauseClosures (fst (unfoldFunType (mkPolyType' _funDefType)))) (toList _funDefClauses) - -lookupBuiltinIden :: (Members '[Reader Micro.InfoTable] r) => Micro.Iden -> Sem r (Maybe Micro.BuiltinPrim) -lookupBuiltinIden = \case - Micro.IdenFunction f -> fmap toBuiltinPrim . (^. Micro.functionInfoDef . Micro.funDefBuiltin) <$> Micro.lookupFunction f - Micro.IdenConstructor c -> fmap toBuiltinPrim . (^. Micro.constructorInfoBuiltin) <$> Micro.lookupConstructor c - Micro.IdenAxiom a -> fmap toBuiltinPrim . (^. Micro.axiomInfoBuiltin) <$> Micro.lookupAxiom a - Micro.IdenVar {} -> return Nothing - Micro.IdenInductive {} -> impossible - -genClosureExpression :: - forall r. - (Members '[Reader Micro.InfoTable, Reader Micro.TypesTable, Reader PatternInfoTable] r) => - [Micro.PolyType] -> - Micro.Expression -> - Sem r [ClosureInfo] -genClosureExpression funArgTyps = \case - Micro.ExpressionLet {} -> error "To be implemented" - Micro.ExpressionIden i -> do - let rootFunMicroName = Micro.getName i - rootFunNameId = rootFunMicroName ^. Micro.nameId - rootFunName = mkName rootFunMicroName - builtin <- lookupBuiltinIden i - case i of - Micro.IdenVar {} -> return [] - _ -> do - (t, patterns) <- getType i - let argTyps = t ^. cFunArgTypes - if - | null argTyps -> return [] - | otherwise -> - return - [ ClosureInfo - { _closureNameId = rootFunNameId, - _closureRootName = rootFunName, - _closureBuiltin = builtin, - _closureMembers = [], - _closureFunType = t, - _closureCArity = patterns - } - ] - Micro.ExpressionApplication a -> exprApplication a - Micro.ExpressionLiteral {} -> return [] - Micro.ExpressionFunction {} -> impossible - Micro.ExpressionHole {} -> impossible - Micro.ExpressionUniverse {} -> impossible - Micro.ExpressionSimpleLambda {} -> impossible - Micro.ExpressionLambda {} -> impossible - Micro.ExpressionCase {} -> impossible - where - exprApplication :: Micro.Application -> Sem r [ClosureInfo] - exprApplication a = do - (f0, appArgs) <- Micro.unfoldPolyApplication a - if - | null appArgs -> genClosureExpression funArgTyps f0 - | otherwise -> case f0 of - Micro.ExpressionLiteral {} -> return [] - Micro.ExpressionIden f -> do - let rootFunMicroName = Micro.getName f - rootFunNameId = rootFunMicroName ^. Micro.nameId - rootFunName = mkName rootFunMicroName - builtin <- lookupBuiltinIden f - (fType, patterns) <- getType f - closureArgs <- concatMapM (genClosureExpression funArgTyps) (toList appArgs) - if - | length appArgs < length (fType ^. cFunArgTypes) -> - return - ( [ ClosureInfo - { _closureNameId = rootFunNameId, - _closureRootName = rootFunName, - _closureBuiltin = builtin, - _closureMembers = take (length appArgs) (fType ^. cFunArgTypes), - _closureFunType = fType, - _closureCArity = patterns - } - ] - <> closureArgs - ) - | otherwise -> return closureArgs - _ -> impossible - -genClosureEnv :: ClosureInfo -> Declaration -genClosureEnv c = - typeDefWrap - (asTypeDef name) - ( DeclStructUnion - ( StructUnion - { _structUnionTag = StructTag, - _structUnionName = Just name, - _structMembers = Just (funDecl : members) - } - ) - ) - where - name :: Text - name = asEnv (closureNamedId c) - funDecl :: Declaration - funDecl = namedDeclType funField uIntPtrType - members :: [Declaration] - members = uncurry cDeclToNamedDecl <$> zip envArgs (c ^. closureMembers) - -genClosureApplySig :: ClosureInfo -> FunctionSig -genClosureApplySig c = cFunTypeToFunSig (asApply (closureNamedId c)) applyFunType - where - nonEnvTyps :: [CDeclType] - nonEnvTyps = drop (length (c ^. closureMembers)) (c ^. closureFunType . cFunArgTypes) - allFunTyps :: [CDeclType] - allFunTyps = declFunctionPtrType : nonEnvTyps - applyFunType :: CFunType - applyFunType = (c ^. closureFunType) {_cFunArgTypes = allFunTyps} - -genClosureApply :: ClosureInfo -> Function -genClosureApply c = - let localName :: Text - localName = "env" - localFunName :: Text - localFunName = "f" - name :: Text - name = closureNamedId c - envName :: Text - envName = asTypeDef (asEnv name) - closureEnvArgs :: [Text] - closureEnvArgs = take (length (c ^. closureMembers)) envArgs - closureEnvAccess :: [Expression] - closureEnvAccess = memberAccess Pointer (ExpressionVar localName) <$> closureEnvArgs - args :: [Expression] - args = take (length (c ^. closureFunType . cFunArgTypes)) (closureEnvAccess <> drop 1 (ExpressionVar <$> funArgs)) - nPatterns :: Int - nPatterns = c ^. closureCArity - patternArgs :: [Expression] - patternArgs = take nPatterns args - funType :: CFunType - funType = - (c ^. closureFunType) - { _cFunArgTypes = drop nPatterns (c ^. closureFunType . cFunArgTypes) - } - localFunType :: CFunType - localFunType = - (c ^. closureFunType) - { _cFunArgTypes = take nPatterns (c ^. closureFunType . cFunArgTypes) - } - funName :: Expression - funName = ExpressionVar (c ^. closureRootName) - funCall :: Expression - funCall = - if - | null patternArgs -> funName - | otherwise -> functionCallCasted localFunType funName patternArgs - juvixFunCall :: [BodyItem] - juvixFunCall = - if - | nPatterns < length args -> - [ BodyDecl - ( Declaration - { _declType = declFunctionType, - _declIsPtr = True, - _declName = Just localFunName, - _declInitializer = Just (ExprInitializer funCall) - } - ), - BodyStatement . StatementReturn . Just $ juvixFunctionCall funType (ExpressionVar localFunName) (drop nPatterns args) - ] - | otherwise -> - [ BodyStatement . StatementReturn . Just $ - functionCallCasted (c ^. closureFunType) (ExpressionVar (closureRootFunction c)) args - ] - envArg :: BodyItem - envArg = - BodyDecl - ( Declaration - { _declType = DeclTypeDefType envName, - _declIsPtr = True, - _declName = Just localName, - _declInitializer = - Just $ - ExprInitializer - ( castToType - ( CDeclType - { _typeDeclType = DeclTypeDefType envName, - _typeIsPtr = True - } - ) - (ExpressionVar "fa0") - ) - } - ) - in Function - { _funcSig = genClosureApplySig c, - _funcBody = envArg : juvixFunCall - } - -genClosureEval :: ClosureInfo -> Function -genClosureEval c = - let localName :: Text - localName = "f" - name :: Text - name = closureNamedId c - envName :: Text - envName = asTypeDef (asEnv name) - envArgToFunArg :: [(Text, Text)] - envArgToFunArg = take (length (c ^. closureMembers)) (zip envArgs funArgs) - assignments :: [Assign] - assignments = mkAssign <$> envArgToFunArg - mkAssign :: (Text, Text) -> Assign - mkAssign (envArg, funArg) = - Assign - { _assignLeft = memberAccess Pointer (ExpressionVar localName) envArg, - _assignRight = ExpressionVar funArg - } - in Function - { _funcSig = - FunctionSig - { _funcReturnType = declFunctionType, - _funcIsPtr = True, - _funcQualifier = None, - _funcName = asEval name, - _funcArgs = namedArgs asFunArg (c ^. closureMembers) - }, - _funcBody = - [ BodyDecl - ( Declaration - { _declType = DeclTypeDefType envName, - _declIsPtr = True, - _declName = Just localName, - _declInitializer = Just $ ExprInitializer (mallocSizeOf envName) - } - ), - BodyStatement - ( StatementExpr - ( ExpressionAssign - ( Assign - { _assignLeft = memberAccess Pointer (ExpressionVar localName) funField, - _assignRight = - castToType - ( CDeclType - { _typeDeclType = uIntPtrType, - _typeIsPtr = False - } - ) - (ExpressionVar (asApply name)) - } - ) - ) - ) - ] - <> (BodyStatement . StatementExpr . ExpressionAssign <$> assignments) - <> [ returnStatement (castToType declFunctionPtrType (ExpressionVar localName)) - ] - } - -clauseClosures :: - (Members '[Reader Micro.InfoTable, Reader Micro.TypesTable] r) => - [Micro.PolyType] -> - Micro.FunctionClause -> - Sem r [ClosureInfo] -clauseClosures argTyps clause = do - bindings <- buildPatternInfoTable argTyps clause - runReader bindings (genClosureExpression argTyps (clause ^. Micro.clauseBody)) diff --git a/src/Juvix/Compiler/Backend/C/Data/Types.hs b/src/Juvix/Compiler/Backend/C/Data/Types.hs index 98cddfcd81..30b8f6564c 100644 --- a/src/Juvix/Compiler/Backend/C/Data/Types.hs +++ b/src/Juvix/Compiler/Backend/C/Data/Types.hs @@ -1,46 +1,7 @@ module Juvix.Compiler.Backend.C.Data.Types where -import Juvix.Compiler.Backend.C.Data.BuiltinTable -import Juvix.Compiler.Backend.C.Language -import Juvix.Compiler.Internal.Language qualified as Micro import Juvix.Prelude newtype MiniCResult = MiniCResult { _resultCCode :: Text } - -data BindingInfo = BindingInfo - { _bindingInfoExpr :: Expression, - _bindingInfoType :: CFunType - } - -newtype PatternInfoTable = PatternInfoTable - {_patternBindings :: HashMap Text BindingInfo} - -type CArity = Int - -data ClosureInfo = ClosureInfo - { _closureNameId :: Micro.NameId, - _closureRootName :: Text, - _closureBuiltin :: Maybe Micro.BuiltinPrim, - _closureMembers :: [CDeclType], - _closureFunType :: CFunType, - _closureCArity :: CArity - } - deriving stock (Show, Eq) - -closureNamedId :: ClosureInfo -> Text -closureNamedId ClosureInfo {..} = _closureRootName <> "_" <> show (length _closureMembers) - -makeLenses ''ClosureInfo -makeLenses ''MiniCResult -makeLenses ''PatternInfoTable -makeLenses ''BindingInfo - -closureRootFunction :: ClosureInfo -> Text -closureRootFunction c = case c ^. closureBuiltin of - Just b -> fromMaybe unsup (builtinName b) - where - unsup :: a - unsup = error ("unsupported builtin " <> show b) - Nothing -> c ^. closureRootName diff --git a/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs b/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs index 0bd6d68334..90433921fb 100644 --- a/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs +++ b/src/Juvix/Compiler/Backend/C/Extra/Serialization.hs @@ -2,7 +2,6 @@ module Juvix.Compiler.Backend.C.Extra.Serialization where import Codec.Binary.UTF8.String qualified as UTF8 import Juvix.Compiler.Backend.C.Language -import Juvix.Extra.Strings qualified as Str import Juvix.Prelude hiding (Binary, Unary) import Language.C qualified as C import Language.C.Data.Ident qualified as C @@ -28,18 +27,9 @@ prettyCpp = \case prettyDefine :: Text -> HP.Doc -> HP.Doc prettyDefine n body = "#define" HP.<+> prettyText n HP.<+> body -prettyAttribute :: Attribute -> HP.Doc -prettyAttribute = \case - ExportName n -> attr "export_name" n - ImportName n -> attr "import_name" n - where - attr :: Text -> Text -> HP.Doc - attr n v = "__attribute__" HP.<> HP.parens (HP.parens (prettyText n HP.<> HP.parens (HP.doubleQuotes (prettyText v)))) - prettyCCode :: CCode -> HP.Doc prettyCCode = \case ExternalDecl decl -> P.pretty (CDeclExt (mkCDecl decl)) - ExternalAttribute a -> prettyAttribute a ExternalFuncSig funSig -> P.pretty (CDeclExt (mkCFunSig funSig)) ExternalFunc fun -> P.pretty (CFDefExt (mkCFunDef fun)) ExternalMacro m -> prettyCpp m @@ -51,33 +41,8 @@ serialize = show . codeUnitDoc codeUnitDoc :: CCodeUnit -> HP.Doc codeUnitDoc c = HP.vcat (map prettyCCode (c ^. ccodeCode)) -goTypeDecl' :: CDeclType -> Declaration -goTypeDecl' CDeclType {..} = - Declaration - { _declType = _typeDeclType, - _declIsPtr = _typeIsPtr, - _declName = Nothing, - _declInitializer = Nothing - } - mkCDecl :: Declaration -> CDecl mkCDecl Declaration {..} = case _declType of - DeclFunPtr FunPtr {..} -> - CDecl - (mkDeclSpecifier _funPtrReturnType) - [(Just declr, Nothing, Nothing)] - C.undefNode - where - declr :: CDeclr - declr = CDeclr (mkIdent <$> _declName) derivedDeclr Nothing [] C.undefNode - derivedDeclr :: [CDerivedDeclr] - derivedDeclr = CPtrDeclr [] C.undefNode : (funDerDeclr <> ptrDeclr) - ptrDeclr :: [CDerivedDeclr] - ptrDeclr = [CPtrDeclr [] C.undefNode | _funPtrIsPtr] - funDerDeclr :: [CDerivedDeclr] - funDerDeclr = [CFunDeclr (Right (funArgs, False)) [] C.undefNode] - funArgs :: [CDecl] - funArgs = mkCDecl . goTypeDecl' <$> _funPtrArgs DeclArray Array {..} -> CDecl (CStorageSpec (CStatic C.undefNode) : mkDeclSpecifier _arrayType) @@ -99,7 +64,7 @@ mkCDecl Declaration {..} = case _declType of declrName :: CDeclr declrName = CDeclr (mkIdent <$> _declName) ptrDeclr Nothing [] C.undefNode ptrDeclr :: [CDerivedDeclarator C.NodeInfo] - ptrDeclr = [CPtrDeclr [] C.undefNode | _declIsPtr] + ptrDeclr = [] initializer :: Maybe CInit initializer = mkCInit <$> _declInitializer @@ -124,7 +89,7 @@ mkFunCommon FunctionSig {..} = (declSpec, declr) derivedDeclr :: [CDerivedDeclr] derivedDeclr = funDerDeclr <> ptrDeclr ptrDeclr :: [CDerivedDeclr] - ptrDeclr = [CPtrDeclr [] C.undefNode | _funcIsPtr] + ptrDeclr = [] funDerDeclr :: [CDerivedDeclr] funDerDeclr = [CFunDeclr (Right (funArgs, False)) [] C.undefNode] funArgs :: [CDecl] @@ -153,7 +118,6 @@ mkBlockItem = \case mkCExpr :: Expression -> CExpr mkCExpr = \case ExpressionAssign Assign {..} -> CAssign CAssignOp (mkCExpr _assignLeft) (mkCExpr _assignRight) C.undefNode - ExpressionCast Cast {..} -> CCast (mkCDecl _castDecl) (mkCExpr _castExpression) C.undefNode ExpressionCall Call {..} -> CCall (mkCExpr _callCallee) (mkCExpr <$> _callArgs) C.undefNode ExpressionLiteral l -> case l of LiteralInt i -> CConst (CIntConst (cInteger i) C.undefNode) @@ -164,8 +128,6 @@ mkCExpr = \case CBinary (mkBinaryOp _binaryOp) (mkCExpr _binaryLeft) (mkCExpr _binaryRight) C.undefNode ExpressionUnary Unary {..} -> CUnary (mkUnaryOp _unaryOp) (mkCExpr _unarySubject) C.undefNode - ExpressionMember MemberAccess {..} -> - CMember (mkCExpr _memberSubject) (mkIdent _memberField) (_memberOp == Pointer) C.undefNode ExpressionStatement stmt -> CStatExpr (mkCStat stmt) C.undefNode @@ -224,12 +186,8 @@ mkUnaryOp = \case mkDeclSpecifier :: DeclType -> [CDeclSpec] mkDeclSpecifier = \case DeclTypeDefType typeDefName -> mkTypeDefTypeSpec typeDefName - DeclTypeDef typ -> CStorageSpec (CTypedef C.undefNode) : mkDeclSpecifier typ DeclStructUnion StructUnion {..} -> mkStructUnionTypeSpec _structUnionTag _structUnionName _structMembers DeclEnum Enum {..} -> mkEnumSpec _enumName _enumMembers - DeclJuvixClosure -> mkTypeDefTypeSpec Str.juvixFunctionT - BoolType -> [CTypeSpec (CBoolType C.undefNode)] - DeclFunPtr {} -> [] DeclArray {} -> [] mkEnumSpec :: Maybe Text -> Maybe [Text] -> [CDeclSpec] diff --git a/src/Juvix/Compiler/Backend/C/Language.hs b/src/Juvix/Compiler/Backend/C/Language.hs index 6cab334e5b..ebd1eefdc1 100644 --- a/src/Juvix/Compiler/Backend/C/Language.hs +++ b/src/Juvix/Compiler/Backend/C/Language.hs @@ -9,7 +9,6 @@ newtype CCodeUnit = CCodeUnit data CCode = ExternalDecl Declaration | ExternalFunc Function - | ExternalAttribute Attribute | ExternalFuncSig FunctionSig | ExternalMacro Cpp | Verbatim Text @@ -35,7 +34,6 @@ data Define = Define data Declaration = Declaration { _declType :: DeclType, - _declIsPtr :: Bool, _declName :: Maybe Text, _declInitializer :: Maybe Initializer } @@ -59,7 +57,6 @@ data DesigInit = DesigInit data FunctionSig = FunctionSig { _funcReturnType :: DeclType, - _funcIsPtr :: Bool, _funcQualifier :: Qualifier, _funcName :: Text, _funcArgs :: [Declaration] @@ -79,12 +76,6 @@ data Qualifier | None deriving stock (Eq) --------------------------------------------------------------------------------- --- Attributes --------------------------------------------------------------------------------- - -data Attribute = ExportName Text | ImportName Text - -------------------------------------------------------------------------------- -- Types -------------------------------------------------------------------------------- @@ -92,12 +83,8 @@ data Attribute = ExportName Text | ImportName Text data DeclType = DeclTypeDefType Text | DeclStructUnion StructUnion - | DeclTypeDef DeclType | DeclEnum Enum - | DeclFunPtr FunPtr | DeclArray Array - | DeclJuvixClosure - | BoolType deriving stock (Show, Eq) data StructUnion = StructUnion @@ -118,47 +105,23 @@ data Enum = Enum } deriving stock (Show, Eq) -data FunPtr = FunPtr - { _funPtrReturnType :: DeclType, - _funPtrIsPtr :: Bool, - _funPtrArgs :: [CDeclType] - } - deriving stock (Show, Eq) - data Array = Array { _arrayType :: DeclType, _arraySize :: Integer } deriving stock (Show, Eq) -data CDeclType = CDeclType - { _typeDeclType :: DeclType, - _typeIsPtr :: Bool - } - deriving stock (Show, Eq) - -data CFunType = CFunType - { _cFunArgTypes :: [CDeclType], - _cFunReturnType :: CDeclType - } - deriving stock (Show, Eq) - -uIntPtrType :: DeclType -uIntPtrType = DeclTypeDefType "uintptr_t" - -------------------------------------------------------------------------------- -- Expressions -------------------------------------------------------------------------------- data Expression = ExpressionAssign Assign - | ExpressionCast Cast | ExpressionCall Call | ExpressionLiteral Literal | ExpressionVar Text | ExpressionBinary Binary | ExpressionUnary Unary - | ExpressionMember MemberAccess | -- We need the "statement expression" GCC/clang extension because the -- Language.C library does not provide any special syntax for macros and we -- want to produce stuff like: @@ -172,39 +135,6 @@ data Assign = Assign } deriving stock (Show, Eq) -data Cast = Cast - { _castDecl :: Declaration, - _castExpression :: Expression - } - deriving stock (Show, Eq) - -castToType :: CDeclType -> Expression -> Expression -castToType cDecl e = - ExpressionCast - ( Cast - { _castDecl = cDeclToDecl cDecl, - _castExpression = e - } - ) - -cDeclToNamedDecl :: Text -> CDeclType -> Declaration -cDeclToNamedDecl name CDeclType {..} = - Declaration - { _declType = _typeDeclType, - _declIsPtr = _typeIsPtr, - _declName = Just name, - _declInitializer = Nothing - } - -cDeclToDecl :: CDeclType -> Declaration -cDeclToDecl CDeclType {..} = - Declaration - { _declType = _typeDeclType, - _declIsPtr = _typeIsPtr, - _declName = Nothing, - _declInitializer = Nothing - } - data Call = Call { _callCallee :: Expression, _callArgs :: [Expression] @@ -244,18 +174,6 @@ data Unary = Unary } deriving stock (Show, Eq) -data MemberAccessOp - = Object - | Pointer - deriving stock (Show, Eq) - -data MemberAccess = MemberAccess - { _memberSubject :: Expression, - _memberField :: Text, - _memberOp :: MemberAccessOp - } - deriving stock (Show, Eq) - -------------------------------------------------------------------------------- -- Statements -------------------------------------------------------------------------------- @@ -328,83 +246,7 @@ integer x = ExpressionLiteral (LiteralInt (fromIntegral x)) string :: Text -> Expression string x = ExpressionLiteral (LiteralString x) -ptrType :: DeclType -> Text -> Declaration -ptrType typ n = - Declaration - { _declType = typ, - _declIsPtr = True, - _declName = Just n, - _declInitializer = Nothing - } - -typeDefType :: Text -> Text -> Declaration -typeDefType typName declName = - Declaration - { _declType = DeclTypeDefType typName, - _declIsPtr = False, - _declName = Just declName, - _declInitializer = Nothing - } - -namedDeclType :: Text -> DeclType -> Declaration -namedDeclType name typ = - Declaration - { _declType = typ, - _declIsPtr = False, - _declName = Just name, - _declInitializer = Nothing - } - -equals :: Expression -> Expression -> Expression -equals e1 e2 = - ExpressionBinary - ( Binary - { _binaryOp = Eq, - _binaryLeft = e1, - _binaryRight = e2 - } - ) - -memberAccess :: MemberAccessOp -> Expression -> Text -> Expression -memberAccess op e fieldName = - ExpressionMember - ( MemberAccess - { _memberSubject = e, - _memberField = fieldName, - _memberOp = op - } - ) - -staticInlineFunc :: DeclType -> Bool -> Text -> [Declaration] -> [BodyItem] -> Function -staticInlineFunc t isPtr name args body = - Function - { _funcSig = - FunctionSig - { _funcReturnType = t, - _funcIsPtr = isPtr, - _funcQualifier = StaticInline, - _funcName = name, - _funcArgs = args - }, - _funcBody = body - } - -typeDefWrap :: Text -> DeclType -> Declaration -typeDefWrap typeDefName typ = - Declaration - { _declType = DeclTypeDef typ, - _declIsPtr = False, - _declName = Just typeDefName, - _declInitializer = Nothing - } - -returnStatement :: Expression -> BodyItem -returnStatement e = - BodyStatement (StatementReturn (Just e)) - makeLenses ''CCodeUnit makeLenses ''Declaration -makeLenses ''CDeclType makeLenses ''FunctionSig makeLenses ''Function -makeLenses ''CFunType diff --git a/src/Juvix/Compiler/Backend/C/Translation.hs b/src/Juvix/Compiler/Backend/C/Translation.hs index 7c25096162..1113a8d814 100644 --- a/src/Juvix/Compiler/Backend/C/Translation.hs +++ b/src/Juvix/Compiler/Backend/C/Translation.hs @@ -1,8 +1,8 @@ module Juvix.Compiler.Backend.C.Translation - ( module Juvix.Compiler.Backend.C.Translation.FromInternal, - module Juvix.Compiler.Backend.C.Translation.FromReg, + ( module Juvix.Compiler.Backend.C.Translation.FromReg, + module Juvix.Compiler.Backend.C.Data.Types, ) where -import Juvix.Compiler.Backend.C.Translation.FromInternal +import Juvix.Compiler.Backend.C.Data.Types import Juvix.Compiler.Backend.C.Translation.FromReg diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromInternal.hs b/src/Juvix/Compiler/Backend/C/Translation/FromInternal.hs deleted file mode 100644 index 20de6cdd85..0000000000 --- a/src/Juvix/Compiler/Backend/C/Translation/FromInternal.hs +++ /dev/null @@ -1,921 +0,0 @@ -module Juvix.Compiler.Backend.C.Translation.FromInternal - ( module Juvix.Compiler.Backend.C.Translation.FromInternal, - module Juvix.Compiler.Backend.C.Data.Types, - ) -where - -import Data.HashMap.Strict qualified as HashMap -import Data.Text qualified as T -import Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context qualified as Abstract -import Juvix.Compiler.Backend.C.Data.Base -import Juvix.Compiler.Backend.C.Data.BuiltinTable -import Juvix.Compiler.Backend.C.Data.Closure -import Juvix.Compiler.Backend.C.Data.Types -import Juvix.Compiler.Backend.C.Extra.Serialization -import Juvix.Compiler.Backend.C.Language -import Juvix.Compiler.Builtins -import Juvix.Compiler.Concrete.Data.InfoTable qualified as Scoper -import Juvix.Compiler.Concrete.Data.ScopedName qualified as Scoper -import Juvix.Compiler.Concrete.Language qualified as C -import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper -import Juvix.Compiler.Internal.Data.InfoTable -import Juvix.Compiler.Internal.Extra (mkPolyType') -import Juvix.Compiler.Internal.Extra qualified as Internal -import Juvix.Compiler.Internal.Translation.Extra qualified as Trans -import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as Internal1 -import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed -import Juvix.Extra.Strings qualified as Str -import Juvix.Prelude hiding (Binary, Unary) - -type CompileInfoTable = HashMap Scoper.NameId Scoper.CompileInfo - -compileInfoTable :: Typed.InternalTypedResult -> CompileInfoTable -compileInfoTable r = - HashMap.mapKeys - (^. Scoper.nameId) - ( r - ^. Typed.resultInternalArityResult - . Internal1.resultInternalResult - . Internal.resultAbstract - . Abstract.resultScoper - . Scoper.resultScoperTable - . Scoper.infoCompilationRules - ) - -fromInternal :: - forall r. - (Member Builtins r) => - Typed.InternalTypedResult -> - Sem r MiniCResult -fromInternal i = MiniCResult . serialize <$> cunitResult - where - compileInfo :: CompileInfoTable - compileInfo = compileInfoTable i - - typesTable :: Typed.TypesTable - typesTable = i ^. Typed.resultIdenTypes - - cunitResult :: Sem r CCodeUnit - cunitResult = do - cmodules' <- cmodules - return - CCodeUnit - { _ccodeCode = cheader <> cmodules' - } - - cheader :: [CCode] - cheader = - map - ExternalMacro - [ CppIncludeSystem Str.stdbool, - CppIncludeFile Str.minicRuntime - ] - - cmodule :: Internal.Module -> Sem r [CCode] - cmodule m = do - let infoTable = buildTable1 m - let defs = - genStructDefs m - <> run (runReader compileInfo (runReader infoTable (genAxioms m))) - <> run (runReader infoTable (genCTypes m)) - <> run (runReader infoTable (runReader typesTable (genFunctionSigs m))) - <> run (runReader infoTable (runReader typesTable (genClosures m))) - funDefs <- runReader infoTable (runReader typesTable (genFunctionDefs m)) - return (defs <> funDefs) - - cmodules :: Sem r [CCode] - cmodules = concatMapM cmodule (toList (i ^. Typed.resultModules)) - -validWasmIdent :: Text -> Bool -validWasmIdent = T.all (\c -> c == '_' || isAlphaNum c) - -genStructDefs :: Internal.Module -> [CCode] -genStructDefs Internal.Module {..} = - concatMap go (_moduleBody ^. Internal.moduleStatements) - where - go :: Internal.Statement -> [CCode] - go = \case - Internal.StatementInductive d -> mkInductiveTypeDef d - Internal.StatementInclude i -> - concatMap go (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements) - _ -> [] - -genAxioms :: forall r. (Members '[Reader Internal.InfoTable, Reader CompileInfoTable] r) => Internal.Module -> Sem r [CCode] -genAxioms Internal.Module {..} = - concatMapM go (_moduleBody ^. Internal.moduleStatements) - where - go :: Internal.Statement -> Sem r [CCode] - go = \case - Internal.StatementInductive {} -> return [] - Internal.StatementAxiom d -> goAxiom d - Internal.StatementForeign {} -> return [] - Internal.StatementFunction {} -> return [] - Internal.StatementInclude i -> - concatMapM go (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements) - -genCTypes :: forall r. (Member (Reader Internal.InfoTable) r) => Internal.Module -> Sem r [CCode] -genCTypes Internal.Module {..} = - concatMapM go (_moduleBody ^. Internal.moduleStatements) - where - go :: Internal.Statement -> Sem r [CCode] - go = \case - Internal.StatementInductive d -> goInductiveDef d - Internal.StatementAxiom {} -> return [] - Internal.StatementForeign d -> return (goForeign d) - Internal.StatementFunction {} -> return [] - Internal.StatementInclude i -> - concatMapM go (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements) - -genFunctionSigs :: forall r. (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable] r) => Internal.Module -> Sem r [CCode] -genFunctionSigs Internal.Module {..} = - concatMapM (applyOnFunStatement genFunctionDef) (_moduleBody ^. Internal.moduleStatements) - where - genFunctionDef :: Internal.FunctionDef -> Sem r [CCode] - genFunctionDef d - | validWasmIdent nameText = (ExternalAttribute (ExportName nameText) :) <$> sig - | otherwise = sig - where - nameText :: Text - nameText = d ^. Internal.funDefName . Internal.nameText - - sig :: Sem r [CCode] - sig = genFunctionSig d - -genFunctionDefs :: - (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable, Builtins] r) => - Internal.Module -> - Sem r [CCode] -genFunctionDefs Internal.Module {..} = genFunctionDefsBody _moduleBody - -genFunctionDefsBody :: - (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable, Builtins] r) => - Internal.ModuleBody -> - Sem r [CCode] -genFunctionDefsBody Internal.ModuleBody {..} = - concatMapM (applyOnFunStatement goFunctionDef) _moduleStatements - -isNullary :: Text -> CFunType -> Bool -isNullary funName funType = null (funType ^. cFunArgTypes) && funName /= Str.main_ - -mkFunctionSig :: forall r. (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable] r) => Internal.FunctionDef -> Sem r FunctionSig -mkFunctionSig Internal.FunctionDef {..} = - cFunTypeToFunSig <$> funName <*> funType - where - baseFunType :: Sem r CFunType - baseFunType = typeToFunType (mkPolyType' _funDefType) - - funType :: Sem r CFunType - funType = do - -- Assumption: All clauses have the same number of patterns - pats <- getClausePatterns (head _funDefClauses) - let nPatterns = length pats - typ <- baseFunType - return - ( if nPatterns == length (typ ^. cFunArgTypes) - then typ - else - CFunType - { _cFunArgTypes = take nPatterns (typ ^. cFunArgTypes), - _cFunReturnType = declFunctionPtrType - } - ) - - funIsNullary :: Sem r Bool - funIsNullary = isNullary funcBasename <$> funType - - funcBasename :: Text - funcBasename = mkName _funDefName - - funName :: Sem r Text - funName = bool funcBasename (asNullary funcBasename) <$> funIsNullary - -genFunctionSig :: forall r. (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable] r) => Internal.FunctionDef -> Sem r [CCode] -genFunctionSig d@(Internal.FunctionDef {..}) = do - sig <- mkFunctionSig d - nullaryDefine' <- nullaryDefine - return - ( [ExternalFuncSig sig] - <> (ExternalMacro . CppDefineParens <$> toList nullaryDefine') - ) - where - baseFunType :: Sem r CFunType - baseFunType = typeToFunType (mkPolyType' _funDefType) - - funType :: Sem r CFunType - funType = do - pats <- getClausePatterns (head _funDefClauses) - let nPatterns = length pats - typ <- baseFunType - return - ( if nPatterns == length (typ ^. cFunArgTypes) - then typ - else - CFunType - { _cFunArgTypes = take nPatterns (typ ^. cFunArgTypes), - _cFunReturnType = declFunctionPtrType - } - ) - - funIsNullary :: Sem r Bool - funIsNullary = isNullary funcBasename <$> funType - - funcBasename :: Text - funcBasename = mkName _funDefName - - funName :: Sem r Text - funName = bool funcBasename (asNullary funcBasename) <$> funIsNullary - - nullaryDefine :: Sem r (Maybe Define) - nullaryDefine = do - n <- funName - bool - Nothing - ( Just $ - Define - { _defineName = funcBasename, - _defineBody = functionCall (ExpressionVar n) [] - } - ) - <$> funIsNullary - -goFunctionDef :: - (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable, Builtins] r) => - Internal.FunctionDef -> - Sem r [CCode] -goFunctionDef d@(Internal.FunctionDef {..}) - | isJust _funDefBuiltin = return [] - | otherwise = do - funSig <- mkFunctionSig d - fc <- mapM (goFunctionClause funSig (fst (unfoldFunType (mkPolyType' _funDefType)))) (toList _funDefClauses) - let bodySpec = fst <$> fc - let preDecls :: [Function] = snd =<< fc - return $ - (ExternalFunc <$> preDecls) - <> [ ExternalFunc $ - Function - { _funcSig = funSig, - _funcBody = maybeToList (BodyStatement <$> mkBody bodySpec) - } - ] - where - mkBody :: [(Maybe Expression, Statement)] -> Maybe Statement - mkBody cs = do - let lastBranch = const fallback . head <$> nonEmpty cs - foldr mkIf lastBranch cs - - mkIf :: (Maybe Expression, Statement) -> Maybe Statement -> Maybe Statement - mkIf (mcondition, thenBranch) elseBranch = case mcondition of - Nothing -> Just thenBranch - Just condition -> - Just - ( StatementIf - ( If - { _ifCondition = condition, - _ifThen = thenBranch, - _ifElse = elseBranch - } - ) - ) - - fallback :: Statement - fallback = - StatementCompound - [ StatementExpr - ( functionCall - (ExpressionVar Str.debug_) - [ ExpressionLiteral - ( LiteralString - ( "Error: Pattern match(es) are non-exhaustive in " - <> _funDefName - ^. Internal.nameText - ) - ) - ] - ), - StatementExpr - ( functionCall - (ExpressionVar Str.exit) - [ ExpressionVar Str.exitFailure_ - ] - ) - ] - -goFunctionClause :: - forall r. - (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable, Builtins] r) => - FunctionSig -> - [Internal.PolyType] -> - Internal.FunctionClause -> - Sem r ((Maybe Expression, Statement), [Function]) -goFunctionClause funSig argTyps clause = do - (stmt, decls) <- returnStmt - cond <- clauseCondition - return ((cond, stmt), decls) - where - conditions :: Sem r [Expression] - conditions = do - pats <- getClausePatterns clause - concat - <$> sequence - [ patternCondition (ExpressionVar arg) p - | (p, arg) <- zip pats funArgs - ] - - patternCondition :: Expression -> Internal.Pattern -> Sem r [Expression] - patternCondition arg = \case - Internal.PatternConstructorApp Internal.ConstructorApp {..} -> do - ctorName <- getConstructorCName _constrAppConstructor - ty <- typeOfConstructor _constrAppConstructor - - let isCtor :: Expression - isCtor = functionCall (ExpressionVar (asIs ctorName)) [castToType ty arg] - projCtor :: Text -> Expression - projCtor ctorArg = functionCall (ExpressionVar (asProjName ctorArg ctorName)) [castToType ty arg] - subConditions :: Sem r [Expression] - subConditions = - fmap - concat - ( zipWithM - patternCondition - (map projCtor ctorArgs) - (_constrAppParameters ^.. each . Internal.patternArgPattern) - ) - fmap (isCtor :) subConditions - Internal.PatternVariable {} -> return [] - - clauseCondition :: Sem r (Maybe Expression) - clauseCondition = fmap (foldr1 f) . nonEmpty <$> conditions - where - f :: Expression -> Expression -> Expression - f e1 e2 = - ExpressionBinary - ( Binary - { _binaryOp = And, - _binaryLeft = e1, - _binaryRight = e2 - } - ) - returnStmt :: Sem r (Statement, [Function]) - returnStmt = do - bindings <- buildPatternInfoTable argTyps clause - (decls :: [Function], clauseResult) <- runOutputList (runReader bindings (goExpression (clause ^. Internal.clauseBody))) - return (StatementReturn (Just (castClause clauseResult)), decls) - where - castClause clauseResult = - castToType (CDeclType {_typeDeclType = funSig ^. funcReturnType, _typeIsPtr = funSig ^. funcIsPtr}) clauseResult - -goExpression :: (Members '[Reader Internal.InfoTable, Reader Typed.TypesTable, Builtins, Reader PatternInfoTable] r) => Internal.Expression -> Sem r Expression -goExpression = \case - Internal.ExpressionIden i -> do - let rootFunInternalName = Internal.getName i - rootFunName = mkName rootFunInternalName - evalFunName = asEval (rootFunName <> "_0") - case i of - Internal.IdenVar {} -> goIden i - _ -> do - (t, _) <- getType i - let argTyps = t ^. cFunArgTypes - (if null argTyps then goIden i else return $ functionCall (ExpressionVar evalFunName) []) - Internal.ExpressionApplication a -> goApplication a - Internal.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l)) - Internal.ExpressionFunction {} -> impossible - Internal.ExpressionHole {} -> impossible - Internal.ExpressionUniverse {} -> impossible - Internal.ExpressionSimpleLambda {} -> impossible - Internal.ExpressionLambda {} -> impossible - Internal.ExpressionLet {} -> impossible - Internal.ExpressionCase {} -> impossible - -goIden :: (Members '[Reader PatternInfoTable, Builtins, Reader Internal.InfoTable] r) => Internal.Iden -> Sem r Expression -goIden = \case - Internal.IdenFunction n -> do - funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoFunctions) - let varName = case funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin of - Just builtin -> fromJust (builtinFunctionName builtin) - Nothing -> mkName n - return (ExpressionVar varName) - Internal.IdenConstructor n -> ExpressionVar <$> getConstructorCName n - Internal.IdenVar n -> - (^. bindingInfoExpr) . HashMap.lookupDefault impossible (n ^. Internal.nameText) <$> asks (^. patternBindings) - Internal.IdenAxiom n -> ExpressionVar <$> getAxiomCName n - Internal.IdenInductive {} -> impossible - -goApplication :: forall r. (Members '[Reader PatternInfoTable, Reader Typed.TypesTable, Builtins, Reader Internal.InfoTable] r) => Internal.Application -> Sem r Expression -goApplication a = do - (f, args0) <- Trans.unfoldPolyApplication a - if - | null args0 -> goExpression f - | otherwise -> case f of - Internal.ExpressionLiteral {} -> goExpression f - Internal.ExpressionIden iden -> do - fArgs <- toList <$> mapM goExpression args0 - case iden of - Internal.IdenVar n -> do - BindingInfo {..} <- HashMap.lookupDefault impossible (n ^. Internal.nameText) <$> asks (^. patternBindings) - return $ juvixFunctionCall _bindingInfoType _bindingInfoExpr fArgs - Internal.IdenFunction n -> do - info <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoFunctions) - nPatterns <- functionInfoPatternsNum info - (idenType, _) <- getType iden - let nArgTyps = length (idenType ^. cFunArgTypes) - if - | length fArgs < nArgTyps -> do - let name = mkName (Internal.getName iden) - evalName = asEval (name <> "_" <> show (length fArgs)) - return $ functionCallCasted idenType (ExpressionVar evalName) fArgs - | nPatterns < nArgTyps -> do - idenExp <- goIden iden - let callTyp = idenType {_cFunArgTypes = drop nPatterns (idenType ^. cFunArgTypes)} - patternArgs = take nPatterns fArgs - funCall = - (if null patternArgs then idenExp else functionCallCasted idenType idenExp patternArgs) - return $ juvixFunctionCall callTyp funCall (drop nPatterns fArgs) - | otherwise -> do - idenExp <- goIden iden - return $ functionCallCasted idenType idenExp fArgs - Internal.IdenConstructor n -> returnFunCall iden fArgs n - Internal.IdenAxiom n -> returnFunCall iden fArgs n - Internal.IdenInductive {} -> impossible - _ -> impossible - where - returnFunCall :: Internal.Iden -> [Expression] -> Internal.Name -> Sem r Expression - returnFunCall iden fArgs name = do - (idenType, _) <- getType iden - ( if length fArgs < length (idenType ^. cFunArgTypes) - then - ( do - let evalName = asEval (mkName name <> "_" <> show (length fArgs)) - return $ functionCallCasted idenType (ExpressionVar evalName) fArgs - ) - else - ( do - idenExp <- goIden iden - return $ functionCallCasted idenType idenExp fArgs - ) - ) - -goLiteral :: C.LiteralLoc -> Literal -goLiteral l = case l ^. C.withLocParam of - C.LitString s -> LiteralString s - C.LitInteger i -> LiteralInt i - -goAxiom :: - (Members [Reader Internal.InfoTable, Reader CompileInfoTable] r) => - Internal.AxiomDef -> - Sem r [CCode] -goAxiom a - | isJust (a ^. Internal.axiomBuiltin) = return [] - | otherwise = do - backend <- runFail (lookupBackends (axiomName ^. Internal.nameId) >>= firstBackendMatch) - case backend of - Nothing -> genFunctionDef a - Just defineBody -> - return - [ ExternalMacro - ( CppDefine - ( Define - { _defineName = defineName, - _defineBody = ExpressionVar defineBody - } - ) - ) - ] - where - axiomName :: Internal.Name - axiomName = a ^. Internal.axiomName - defineName :: Text - defineName = mkName axiomName - getCode :: BackendItem -> Maybe Text - getCode b = - guard (BackendC == b ^. backendItemBackend . withLocParam) - $> b - ^. backendItemCode - firstBackendMatch :: - (Member Fail r) => - [BackendItem] -> - Sem r Text - firstBackendMatch = failMaybe . firstJust getCode - lookupBackends :: - (Members '[Fail, Reader CompileInfoTable] r) => - NameId -> - Sem r [BackendItem] - lookupBackends f = ask >>= failMaybe . fmap (^. Scoper.compileInfoBackendItems) . HashMap.lookup f - genFunctionDef :: - forall r. - (Members [Reader Internal.InfoTable, Reader CompileInfoTable] r) => - Internal.AxiomDef -> - Sem r [CCode] - genFunctionDef d - | validWasmIdent nameText = (ExternalAttribute (ImportName (axiomName ^. Internal.nameText)) :) <$> sig - | otherwise = sig - where - nameText :: Text - nameText = axiomName ^. Internal.nameText - - sig :: Sem r [CCode] - sig = do - s <- cFunTypeToFunSig defineName <$> typeToFunType (mkPolyType' (d ^. Internal.axiomType)) - return [ExternalFuncSig s] - -goForeign :: ForeignBlock -> [CCode] -goForeign b = case b ^. foreignBackend . withLocParam of - BackendC -> [Verbatim (b ^. foreignCode)] - _ -> [] - -mkInductiveName :: Internal.InductiveDef -> Text -mkInductiveName i = mkName (i ^. Internal.inductiveName) - -mkInductiveConstructorNames :: Internal.InductiveDef -> [Text] -mkInductiveConstructorNames i = mkName . view Internal.inductiveConstructorName <$> i ^. Internal.inductiveConstructors - -mkInductiveTypeDef :: Internal.InductiveDef -> [CCode] -mkInductiveTypeDef i = - [ExternalDecl structTypeDef] - where - structTypeDef :: Declaration - structTypeDef = - typeDefWrap - (asTypeDef baseName) - ( DeclStructUnion - ( StructUnion - { _structUnionTag = StructTag, - _structUnionName = Just (asStruct baseName), - _structMembers = Nothing - } - ) - ) - - baseName :: Text - baseName = mkName (i ^. Internal.inductiveName) - -goInductiveDef :: (Members '[Reader Internal.InfoTable] r) => Internal.InductiveDef -> Sem r [CCode] -goInductiveDef i - | isJust (i ^. Internal.inductiveBuiltin) = return [] - | otherwise = do - ctorDefs <- concatMapM goInductiveConstructorDef (i ^. Internal.inductiveConstructors) - ctorNews <- concatMapM (goInductiveConstructorNew i) (i ^. Internal.inductiveConstructors) - projections <- concatMapM (goProjections inductiveTypeDef) (i ^. Internal.inductiveConstructors) - return - ( [ExternalDecl tagsType] - <> ctorDefs - <> [ExternalDecl inductiveDecl] - <> ctorNews - <> (ExternalFunc . isFunction <$> constructorNames) - <> (ExternalFunc . asFunction <$> constructorNames) - <> projections - ) - where - baseName :: Text - baseName = mkName (i ^. Internal.inductiveName) - - constructorNames :: [Text] - constructorNames = mkInductiveConstructorNames i - - tagsType :: Declaration - tagsType = - typeDefWrap - (asTag baseName) - ( DeclEnum - ( Enum - { _enumName = Nothing, - _enumMembers = Just (asTag <$> constructorNames) - } - ) - ) - - inductiveDecl :: Declaration - inductiveDecl = - Declaration - { _declType = inductiveStruct, - _declIsPtr = False, - _declName = Nothing, - _declInitializer = Nothing - } - - inductiveTypeDef :: DeclType - inductiveTypeDef = DeclTypeDefType (asTypeDef baseName) - - inductiveStruct :: DeclType - inductiveStruct = - DeclStructUnion - ( StructUnion - { _structUnionTag = StructTag, - _structUnionName = Just (asStruct baseName), - _structMembers = - Just - [ typeDefType (asTag baseName) Str.tag, - Declaration - { _declType = unionMembers, - _declIsPtr = False, - _declName = Just Str.data_, - _declInitializer = Nothing - } - ] - } - ) - - unionMembers :: DeclType - unionMembers = - DeclStructUnion - ( StructUnion - { _structUnionTag = UnionTag, - _structUnionName = Nothing, - _structMembers = Just (map (\ctorName -> typeDefType (asTypeDef ctorName) (asField ctorName)) constructorNames) - } - ) - - isFunction :: Text -> Function - isFunction ctorName = - Function - { _funcSig = - FunctionSig - { _funcReturnType = BoolType, - _funcIsPtr = False, - _funcQualifier = StaticInline, - _funcName = asIs ctorName, - _funcArgs = [ptrType inductiveTypeDef funcArg] - }, - _funcBody = - [ returnStatement - ( equals - (memberAccess Pointer (ExpressionVar funcArg) Str.tag) - (ExpressionVar (asTag ctorName)) - ) - ] - } - where - funcArg :: Text - funcArg = "a" - - asFunction :: Text -> Function - asFunction ctorName = - Function - { _funcSig = - FunctionSig - { _funcReturnType = DeclTypeDefType (asTypeDef ctorName), - _funcIsPtr = False, - _funcQualifier = StaticInline, - _funcName = asCast ctorName, - _funcArgs = [ptrType inductiveTypeDef funcArg] - }, - _funcBody = - [ returnStatement - (memberAccess Object (memberAccess Pointer (ExpressionVar funcArg) Str.data_) (asField ctorName)) - ] - } - where - funcArg :: Text - funcArg = "a" - -goInductiveConstructorNew :: - forall r. - (Members '[Reader Internal.InfoTable] r) => - Internal.InductiveDef -> - Internal.InductiveConstructorDef -> - Sem r [CCode] -goInductiveConstructorNew i ctor = ctorNewFun - where - ctorNewFun :: Sem r [CCode] - ctorNewFun = if null ctorParams then return ctorNewNullary else ctorNewNary - - baseName :: Text - baseName = mkName (ctor ^. Internal.inductiveConstructorName) - - inductiveName :: Text - inductiveName = mkInductiveName i - - ctorParams :: [Internal.PolyType] - ctorParams = map mkPolyType' (ctor ^. Internal.inductiveConstructorParameters) - - ctorNewNullary :: [CCode] - ctorNewNullary = - [ ExternalFunc $ - commonFunctionDeclr - (asNullary baseName) - [] - [ BodyDecl allocInductive, - BodyDecl (commonInitDecl (dataInit Str.true_)), - BodyStatement assignPtr, - returnStatement (ExpressionVar tmpPtrName) - ], - ExternalMacro - ( CppDefineParens - ( Define - { _defineName = baseName, - _defineBody = functionCall (ExpressionVar (asNullary baseName)) [] - } - ) - ) - ] - - ctorNewNary :: Sem r [CCode] - ctorNewNary = do - ctorDecls' <- ctorDecls - ctorStructInit' <- ctorStructInit - return - [ ExternalFunc $ - commonFunctionDeclr - baseName - ctorDecls' - [ BodyDecl allocInductive, - BodyDecl ctorStructInit', - BodyDecl (commonInitDecl (dataInit tmpCtorStructName)), - BodyStatement assignPtr, - returnStatement (ExpressionVar tmpPtrName) - ] - ] - where - ctorDecls :: Sem r [Declaration] - ctorDecls = inductiveCtorArgs ctor - - ctorInit :: Sem r [DesigInit] - -- TODO: _declName is never Nothing by construction, fix the types - ctorInit = map (f . fromJust . (^. declName)) <$> ctorDecls - - f :: Text -> DesigInit - f fieldName = - DesigInit - { _desigDesignator = fieldName, - _desigInitializer = ExprInitializer (ExpressionVar fieldName) - } - - ctorStructInit :: Sem r Declaration - ctorStructInit = do - ctorInit' <- ctorInit - return - Declaration - { _declType = DeclTypeDefType (asTypeDef baseName), - _declIsPtr = False, - _declName = Just tmpCtorStructName, - _declInitializer = Just (DesignatorInitializer ctorInit') - } - - commonFunctionDeclr :: Text -> [Declaration] -> [BodyItem] -> Function - commonFunctionDeclr name args body = - Function - { _funcSig = - FunctionSig - { _funcReturnType = DeclTypeDefType (asTypeDef inductiveName), - _funcIsPtr = True, - _funcQualifier = StaticInline, - _funcName = name, - _funcArgs = args - }, - _funcBody = body - } - - commonInitDecl :: Initializer -> Declaration - commonInitDecl di = - ( Declaration - { _declType = DeclTypeDefType (asTypeDef inductiveName), - _declIsPtr = False, - _declName = Just tmpStructName, - _declInitializer = - Just - ( DesignatorInitializer - [ DesigInit - { _desigDesignator = Str.tag, - _desigInitializer = ExprInitializer (ExpressionVar (asTag baseName)) - }, - DesigInit - { _desigDesignator = Str.data_, - _desigInitializer = di - } - ] - ) - } - ) - - tmpPtrName :: Text - tmpPtrName = "n" - - tmpStructName :: Text - tmpStructName = "m" - - tmpCtorStructName :: Text - tmpCtorStructName = "s" - - allocInductive :: Declaration - allocInductive = - ( Declaration - { _declType = DeclTypeDefType (asTypeDef inductiveName), - _declIsPtr = True, - _declName = Just tmpPtrName, - _declInitializer = Just (ExprInitializer (mallocSizeOf (asTypeDef inductiveName))) - } - ) - - dataInit :: Text -> Initializer - dataInit varName = - DesignatorInitializer - [ DesigInit - { _desigDesignator = asField baseName, - _desigInitializer = ExprInitializer (ExpressionVar varName) - } - ] - - assignPtr :: Statement - assignPtr = - StatementExpr - ( ExpressionAssign - ( Assign - { _assignLeft = - ExpressionUnary - ( Unary - { _unaryOp = Indirection, - _unarySubject = ExpressionVar tmpPtrName - } - ), - _assignRight = ExpressionVar tmpStructName - } - ) - ) - -inductiveCtorParams :: (Members '[Reader Internal.InfoTable] r) => Internal.InductiveConstructorDef -> Sem r [CDeclType] -inductiveCtorParams ctor = mapM (goType . mkPolyType') (ctor ^. Internal.inductiveConstructorParameters) - -inductiveCtorArgs :: (Members '[Reader Internal.InfoTable] r) => Internal.InductiveConstructorDef -> Sem r [Declaration] -inductiveCtorArgs ctor = namedArgs asCtorArg <$> inductiveCtorParams ctor - -inductiveCtorTypes :: (Members '[Reader Internal.InfoTable] r) => Internal.Name -> Sem r [CDeclType] -inductiveCtorTypes ctor = do - info <- Internal.lookupConstructor ctor - mapM (goType . mkPolyType') (snd (Internal.constructorArgTypes info)) - -goInductiveConstructorDef :: - forall r. - (Members '[Reader Internal.InfoTable] r) => - Internal.InductiveConstructorDef -> - Sem r [CCode] -goInductiveConstructorDef ctor = do - d <- ctorDecl - return [ExternalDecl d] - where - ctorDecl :: Sem r Declaration - ctorDecl = if null ctorParams then return ctorBool else ctorStruct - - baseName :: Text - baseName = mkName (ctor ^. Internal.inductiveConstructorName) - - ctorParams :: [Internal.PolyType] - ctorParams = map mkPolyType' (ctor ^. Internal.inductiveConstructorParameters) - - ctorBool :: Declaration - ctorBool = typeDefWrap (asTypeDef baseName) BoolType - - ctorStruct :: Sem r Declaration - ctorStruct = typeDefWrap (asTypeDef baseName) <$> struct - - struct :: Sem r DeclType - struct = do - args <- inductiveCtorArgs ctor - return - ( DeclStructUnion - ( StructUnion - { _structUnionTag = StructTag, - _structUnionName = Just (asStruct baseName), - _structMembers = Just args - } - ) - ) - -goProjections :: - (Members '[Reader Internal.InfoTable] r) => - DeclType -> - Internal.InductiveConstructorDef -> - Sem r [CCode] -goProjections inductiveTypeDef ctor = do - params <- inductiveCtorParams ctor - return (ExternalFunc <$> zipWith projFunction [0 ..] params) - where - baseName :: Text - baseName = mkName (ctor ^. Internal.inductiveConstructorName) - - localName :: Text - localName = "a" - - projFunction :: Int -> CDeclType -> Function - projFunction argIdx projTyp = - Function - { _funcSig = - FunctionSig - { _funcReturnType = projTyp ^. typeDeclType, - _funcIsPtr = projTyp ^. typeIsPtr, - _funcQualifier = StaticInline, - _funcName = asProj argIdx baseName, - _funcArgs = [namedDecl localName True inductiveTypeDef] - }, - _funcBody = - [ BodyStatement - ( StatementReturn - ( Just - ( memberAccess - Object - (functionCall (ExpressionVar (asCast baseName)) [ExpressionVar localName]) - (asCtorArg (show argIdx)) - ) - ) - ) - ] - } diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs index 41ed5510af..4e2a4f3029 100644 --- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs @@ -33,7 +33,6 @@ fromReg lims tab = { _arrayType = DeclTypeDefType "constr_info_t", _arraySize = fromIntegral (info ^. Reg.extraInfoConstrsNum) }, - _declIsPtr = False, _declName = Just "juvix_constr_info_array", _declInitializer = Just $ @@ -54,7 +53,6 @@ fromReg lims tab = { _arrayType = DeclTypeDefType "function_info_t", _arraySize = fromIntegral (info ^. Reg.extraInfoFunctionsNum) }, - _declIsPtr = False, _declName = Just "juvix_function_info_array", _declInitializer = Just $ @@ -76,7 +74,6 @@ fromReg lims tab = mainSig = FunctionSig { _funcReturnType = DeclTypeDefType "int", - _funcIsPtr = False, _funcQualifier = None, _funcName = "main", _funcArgs = [] diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs b/src/Juvix/Compiler/Concrete/Data/InfoTable.hs index 6d59d2c44c..465d0876c7 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTable.hs @@ -24,12 +24,6 @@ newtype InductiveInfo = InductiveInfo } deriving stock (Eq, Show) -data CompileInfo = CompileInfo - { _compileInfoBackendItems :: [BackendItem], - _compileInfoDefined :: Interval - } - deriving stock (Eq, Show) - data InfoTable = InfoTable { _infoConstructors :: HashMap ConstructorRef ConstructorInfo, _infoModules :: HashMap S.TopModulePath (Module 'Scoped 'ModuleTop), @@ -37,8 +31,7 @@ data InfoTable = InfoTable _infoInductives :: HashMap InductiveRef InductiveInfo, _infoFunctions :: HashMap FunctionRef FunctionInfo, _infoFunctionClauses :: HashMap S.Symbol (FunctionClause 'Scoped), - _infoNames :: [S.AName], - _infoCompilationRules :: HashMap S.Symbol CompileInfo + _infoNames :: [S.AName] } emptyInfoTable :: InfoTable @@ -50,8 +43,7 @@ emptyInfoTable = _infoInductives = mempty, _infoFunctions = mempty, _infoFunctionClauses = mempty, - _infoNames = mempty, - _infoCompilationRules = mempty + _infoNames = mempty } makeLenses ''InfoTable @@ -59,4 +51,3 @@ makeLenses ''InductiveInfo makeLenses ''ConstructorInfo makeLenses ''AxiomInfo makeLenses ''FunctionInfo -makeLenses ''CompileInfo diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs index e3f3051a50..a96c2ead00 100644 --- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs @@ -13,7 +13,6 @@ data InfoTableBuilder m a where RegisterFunction :: TypeSignature 'Scoped -> InfoTableBuilder m () RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m () RegisterName :: (HasLoc c) => S.Name' c -> InfoTableBuilder m () - RegisterCompile :: Compile 'Scoped -> InfoTableBuilder m () RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m () makeSem ''InfoTableBuilder @@ -42,12 +41,6 @@ registerAxiom' :: Sem r (AxiomDef 'Scoped) registerAxiom' a = registerAxiom a $> a -registerCompile' :: - (Member InfoTableBuilder r) => - Compile 'Scoped -> - Sem r (Compile 'Scoped) -registerCompile' c = registerCompile c $> c - registerFunctionClause' :: (Member InfoTableBuilder r) => FunctionClause 'Scoped -> @@ -60,14 +53,6 @@ toState = reinterpret $ \case let ref = AxiomRef' (S.unqualifiedSymbol (d ^. axiomName)) info = AxiomInfo {_axiomInfoType = d ^. axiomType} in modify (over infoAxioms (HashMap.insert ref info)) - RegisterCompile c -> - let symb = c ^. compileName - info = - CompileInfo - { _compileInfoBackendItems = c ^. compileBackendItems, - _compileInfoDefined = getLoc symb - } - in modify (over infoCompilationRules (HashMap.insert symb info)) RegisterConstructor c -> let ref = ConstructorRef' (S.unqualifiedSymbol (c ^. constructorName)) info = ConstructorInfo {_constructorInfoType = c ^. constructorType} diff --git a/src/Juvix/Compiler/Concrete/Data/Scope.hs b/src/Juvix/Compiler/Concrete/Data/Scope.hs index 56a563f908..37e49abf14 100644 --- a/src/Juvix/Compiler/Concrete/Data/Scope.hs +++ b/src/Juvix/Compiler/Concrete/Data/Scope.hs @@ -36,8 +36,7 @@ data Scope = Scope -- should map to itself. This is needed because we may query it with a -- symbol with a different location but we may want the location of the -- original symbol - _scopeLocalSymbols :: HashMap Symbol S.Symbol, - _scopeCompilationRules :: HashMap Symbol CompileInfo + _scopeLocalSymbols :: HashMap Symbol S.Symbol } deriving stock (Show) @@ -87,6 +86,5 @@ emptyScope absPath = { _scopePath = absPath, _scopeSymbols = mempty, _scopeTopModules = mempty, - _scopeLocalSymbols = mempty, - _scopeCompilationRules = mempty + _scopeLocalSymbols = mempty } diff --git a/src/Juvix/Compiler/Concrete/Keywords.hs b/src/Juvix/Compiler/Concrete/Keywords.hs index 6f98697cd7..c4ff9a42d7 100644 --- a/src/Juvix/Compiler/Concrete/Keywords.hs +++ b/src/Juvix/Compiler/Concrete/Keywords.hs @@ -10,20 +10,13 @@ import Juvix.Data.Keyword.All ( -- reserved -- extra - cBackend, - ghc, kwAssign, kwAt, kwAxiom, kwBuiltin, kwCase, kwColon, - kwColonOmega, - kwColonOne, - kwColonZero, - kwCompile, kwEnd, - kwForeign, kwHiding, kwHole, kwImport, @@ -61,12 +54,7 @@ allKeywords = kwAxiom, kwCase, kwColon, - kwColonOmega, - kwColonOne, - kwColonZero, - kwCompile, kwEnd, - kwForeign, kwHiding, kwHole, kwImport, diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs index b2830d911e..4b71851a1c 100644 --- a/src/Juvix/Compiler/Concrete/Language.hs +++ b/src/Juvix/Compiler/Concrete/Language.hs @@ -115,8 +115,6 @@ data Statement (s :: Stage) | StatementOpenModule (OpenModule s) | StatementFunctionClause (FunctionClause s) | StatementAxiom (AxiomDef s) - | StatementForeign ForeignBlock - | StatementCompile (Compile s) deriving stock instance ( Show (ImportType s), @@ -806,25 +804,6 @@ deriving stock instance (Show (ExpressionType s), Show (PatternParensType s)) => deriving stock instance (Ord (ExpressionType s), Ord (PatternParensType s)) => Ord (Case s) --------------------------------------------------------------------------------- --- Compile statements --------------------------------------------------------------------------------- - -data Compile s = Compile - { _compileKw :: KeywordRef, - _compileName :: SymbolType s, - _compileBackendItems :: [BackendItem] - } - -deriving stock instance - (Show (SymbolType s)) => Show (Compile s) - -deriving stock instance - (Ord (SymbolType s)) => Ord (Compile s) - -deriving stock instance - (Eq (SymbolType s)) => Eq (Compile s) - -------------------------------------------------------------------------------- -- Debugging statements -------------------------------------------------------------------------------- @@ -954,7 +933,6 @@ makeLenses ''OpenModule makeLenses ''PatternApp makeLenses ''PatternInfixApp makeLenses ''PatternPostfixApp -makeLenses ''Compile makeLenses ''Case makeLenses ''CaseBranch makeLenses ''PatternBinding diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index 275964ac61..5a559f0f8a 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -6,7 +6,6 @@ module Juvix.Compiler.Concrete.Pretty.Base where import Data.List.NonEmpty.Extra qualified as NonEmpty -import Data.Text qualified as T import Juvix.Compiler.Concrete.Data.ScopedName (AbsModulePath, IsConcrete (..)) import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Extra (unfoldApplication) @@ -66,8 +65,6 @@ groupStatements = reverse . map reverse . uncurry cons . foldl' aux ([], []) -- blank line g :: Statement s -> Statement s -> Bool g a b = case (a, b) of - (StatementForeign _, _) -> False - (StatementCompile _, _) -> False (StatementOperator _, StatementOperator _) -> True (StatementOperator o, s) -> definesSymbol (o ^. opSymbol) s (StatementImport _, StatementImport _) -> True @@ -132,40 +129,6 @@ instance (SingI s) => PrettyCode (Statement s) where StatementOpenModule o -> ppCode o StatementFunctionClause c -> ppCode c StatementAxiom a -> ppCode a - StatementForeign p -> ppCode p - StatementCompile c -> ppCode c - -instance PrettyCode Backend where - ppCode = \case - BackendGhc -> return kwGhc - BackendC -> return kwC - -instance (SingI s) => PrettyCode (Compile s) where - ppCode Compile {..} = do - compileName' <- ppSymbol _compileName - compileBackendItems' <- bracesIndent <$> ppBlock _compileBackendItems - return $ kwCompile <+> compileName' <+> compileBackendItems' - -instance PrettyCode ForeignBlock where - ppCode ForeignBlock {..} = do - _foreignBackend' <- ppCode _foreignBackend - return $ - kwForeign - <+> _foreignBackend' - <+> lbrace - <> line - <> pretty (escape _foreignCode) - <> line - <> rbrace - where - escape :: Text -> Text - escape = T.replace "}" "\\}" - -instance PrettyCode BackendItem where - ppCode BackendItem {..} = do - backend <- ppCode _backendItemBackend - return $ - backend <+> kwMapsto <+> ppStringLit _backendItemCode ppTopModulePath :: forall s r. diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 139170437b..601d1cbacb 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -6,7 +6,6 @@ module Juvix.Compiler.Concrete.Print.Base where import Data.List.NonEmpty.Extra qualified as NonEmpty -import Data.Text qualified as Text import Juvix.Compiler.Concrete.Data.ScopedName qualified as S import Juvix.Compiler.Concrete.Language import Juvix.Compiler.Concrete.Pretty.Base qualified as P @@ -336,42 +335,6 @@ instance PrettyPrint (InductiveDef 'Scoped) where ppConstructorBlock :: NonEmpty (InductiveConstructorDef 'Scoped) -> Sem r () ppConstructorBlock cs = vsep (ppCode <$> cs) -instance PrettyPrint (WithLoc Backend) where - ppCode = ppMorpheme - -instance PrettyPrint ForeignBlock where - ppCode ForeignBlock {..} = do - let _foreignBackend' = ppCode _foreignBackend - ppCode _foreignKw - <+> _foreignBackend' - <+> lbrace - <> line - <> noLoc (pretty (escape _foreignCode)) - <> line - <> rbrace - where - escape :: Text -> Text - escape = Text.replace "}" "\\}" - -instance PrettyPrint BackendItem where - ppCode BackendItem {..} = do - let backend' = ppCode _backendItemBackend - backend' - <+> noLoc P.kwMapsto - <+> noLoc (ppStringLit _backendItemCode) - -instance PrettyPrint (Compile 'Scoped) where - ppCode :: forall r. Members '[ExactPrint, Reader Options] r => Compile 'Scoped -> Sem r () - ppCode Compile {..} = do - let name' = ppCode _compileName - items' = ppBlock _compileBackendItems - ppCode _compileKw - <+> name' - <+> items' - where - ppBlock :: PrettyPrint c => [c] -> Sem r () - ppBlock = bracesIndent . vsep . map ((<> semicolon) . ppCode) - instance PrettyPrint (Statement 'Scoped) where ppCode = \case StatementOperator o -> ppCode o @@ -382,5 +345,3 @@ instance PrettyPrint (Statement 'Scoped) where StatementOpenModule o -> ppCode o StatementFunctionClause c -> ppCode c StatementAxiom a -> ppCode a - StatementForeign f -> ppCode f - StatementCompile c -> ppCode c diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs index 31763f03a7..2771e6ffde 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs @@ -815,100 +815,6 @@ checkAxiomDef AxiomDef {..} = do axiomDoc' <- withLocalScope (mapM checkJudoc _axiomDoc) registerAxiom' AxiomDef {_axiomName = axiomName', _axiomType = axiomType', _axiomDoc = axiomDoc', ..} -checkCompile :: - (Members '[InfoTableBuilder, Error ScoperError, State Scope, State ScoperState] r) => - Compile 'Parsed -> - Sem r (Compile 'Scoped) -checkCompile c@Compile {..} = do - scopedSym :: S.Symbol <- checkCompileName c - let sym :: Symbol = c ^. compileName - rules <- gets (^. scopeCompilationRules) - if - | Just info <- HashMap.lookup sym rules -> - throw - ( ErrMultipleCompileBlockSameName - ( MultipleCompileBlockSameName - { _multipleCompileBlockFirstDefined = info ^. compileInfoDefined, - _multipleCompileBlockSym = sym - } - ) - ) - | otherwise -> do - void (checkBackendItems sym _compileBackendItems mempty) - registerName (S.unqualifiedSymbol scopedSym) - modify - ( over - scopeCompilationRules - ( HashMap.insert - _compileName - ( CompileInfo - { _compileInfoBackendItems = _compileBackendItems, - _compileInfoDefined = getLoc scopedSym - } - ) - ) - ) - registerCompile' $ Compile {_compileName = scopedSym, ..} - -checkBackendItems :: - (Members '[Error ScoperError] r) => - Symbol -> - [BackendItem] -> - HashSet Backend -> - Sem r (HashSet Backend) -checkBackendItems _ [] bset = return bset -checkBackendItems sym (b : bs) bset = - let cBackend = b ^. backendItemBackend . withLocParam - in if - | HashSet.member cBackend bset -> - throw - ( ErrMultipleCompileRuleSameBackend - (MultipleCompileRuleSameBackend b sym) - ) - | otherwise -> checkBackendItems sym bs (HashSet.insert cBackend bset) - -checkCompileName :: - (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) => - Compile 'Parsed -> - Sem r S.Symbol -checkCompileName Compile {..} = do - let sym :: Symbol = _compileName - name :: Name = NameUnqualified sym - scope <- get - entries <- lookupQualifiedSymbol ([], sym) - case filter S.canBeCompiled entries of - [] -> case entries of - [] -> - throw - ( ErrSymNotInScope - ( NotInScope - { _notInScopeSymbol = sym, - _notInScopeScope = scope - } - ) - ) - (e : _) -> - throw - ( ErrWrongKindExpressionCompileBlock - ( WrongKindExpressionCompileBlock - { _wrongKindExpressionCompileBlockSym = sym, - _wrongKindExpressionCompileBlockEntry = e - } - ) - ) - [x] -> do - actualPath <- gets (^. scopePath) - let scoped = entryToSymbol x sym - expectedPath = scoped ^. S.nameDefinedIn - if - | actualPath == expectedPath -> return scoped - | otherwise -> - throw - ( ErrWrongLocationCompileBlock - (WrongLocationCompileBlock expectedPath name) - ) - xs -> throw (ErrAmbiguousSym (AmbiguousSym name xs)) - entryToSymbol :: SymbolEntry -> Symbol -> S.Symbol entryToSymbol sentry csym = set S.nameConcrete csym (symbolEntryToSName sentry) @@ -1241,8 +1147,6 @@ checkStatement s = topBindings $ case s of StatementOpenModule open -> StatementOpenModule <$> checkOpenModule open StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax - StatementForeign d -> return (StatementForeign d) - StatementCompile c -> StatementCompile <$> checkCompile c ------------------------------------------------------------------------------- -- Infix Expression diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs index 520f1bfe81..2f3e2345db 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs @@ -27,10 +27,6 @@ data ScoperError | ErrAmbiguousSym AmbiguousSym | ErrAmbiguousModuleSym AmbiguousModuleSym | ErrUnusedOperatorDef UnusedOperatorDef - | ErrWrongLocationCompileBlock WrongLocationCompileBlock - | ErrMultipleCompileBlockSameName MultipleCompileBlockSameName - | ErrMultipleCompileRuleSameBackend MultipleCompileRuleSameBackend - | ErrWrongKindExpressionCompileBlock WrongKindExpressionCompileBlock | ErrDoubleBracesPattern DoubleBracesPattern | ErrDoubleBinderPattern DoubleBinderPattern | ErrAliasBinderPattern AliasBinderPattern @@ -58,10 +54,6 @@ instance ToGenericError ScoperError where ErrAmbiguousModuleSym e -> genericError e ErrUnusedOperatorDef e -> genericError e ErrLacksFunctionClause e -> genericError e - ErrWrongLocationCompileBlock e -> genericError e - ErrMultipleCompileBlockSameName e -> genericError e - ErrMultipleCompileRuleSameBackend e -> genericError e - ErrWrongKindExpressionCompileBlock e -> genericError e ErrDoubleBracesPattern e -> genericError e ErrDoubleBinderPattern e -> genericError e ErrAliasBinderPattern e -> genericError e diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs index d3385a81a4..da1ce4668d 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs @@ -410,111 +410,6 @@ instance ToGenericError AmbiguousModuleSym where is = map getLoc _ambiguousModSymEntires msg = ambiguousMessage opts' _ambiguousModName _ambiguousModSymEntires -data WrongLocationCompileBlock = WrongLocationCompileBlock - { _wrongLocationCompileBlockExpectedModPath :: S.AbsModulePath, - _wrongLocationCompileBlockName :: Name - } - deriving stock (Show) - -instance ToGenericError WrongLocationCompileBlock where - genericError WrongLocationCompileBlock {..} = ask >>= generr - where - generr opts = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = prettyError msg, - _genericErrorIntervals = [i] - } - where - opts' = fromGenericOptions opts - name = _wrongLocationCompileBlockName - i = getLoc name - msg = - "The compilation rules for the symbol" - <+> ppCode opts' name - <+> "need to be defined in the module:" - <> line - <> ppCode opts' _wrongLocationCompileBlockExpectedModPath - -data MultipleCompileBlockSameName = MultipleCompileBlockSameName - { _multipleCompileBlockFirstDefined :: Interval, - _multipleCompileBlockSym :: Symbol - } - deriving stock (Show) - -instance ToGenericError MultipleCompileBlockSameName where - genericError MultipleCompileBlockSameName {..} = ask >>= generr - where - generr opts = - return - GenericError - { _genericErrorLoc = i2, - _genericErrorMessage = prettyError msg, - _genericErrorIntervals = [i1, i2] - } - where - opts' = fromGenericOptions opts - i1 = _multipleCompileBlockFirstDefined - i2 = getLoc _multipleCompileBlockSym - msg = - "Multiple compile blocks for the symbol" - <+> ppCode opts' _multipleCompileBlockSym - -data MultipleCompileRuleSameBackend = MultipleCompileRuleSameBackend - { _multipleCompileRuleSameBackendBackendItem :: BackendItem, - _multipleCompileRuleSameBackendSym :: Symbol - } - deriving stock (Show) - -instance ToGenericError MultipleCompileRuleSameBackend where - genericError MultipleCompileRuleSameBackend {..} = ask >>= generr - where - generr opts = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = prettyError msg, - _genericErrorIntervals = [i] - } - where - opts' = fromGenericOptions opts - backend = _multipleCompileRuleSameBackendBackendItem ^. backendItemBackend - name = _multipleCompileRuleSameBackendSym - i = getLoc _multipleCompileRuleSameBackendSym - msg = - "Multiple" - <+> ppCode opts' backend - <+> "compilation rules for the symbol" - <+> ppCode opts' name - <+> "at" - <+> pretty (getLoc name) - -data WrongKindExpressionCompileBlock = WrongKindExpressionCompileBlock - { _wrongKindExpressionCompileBlockSym :: Symbol, - _wrongKindExpressionCompileBlockEntry :: SymbolEntry - } - deriving stock (Show) - -instance ToGenericError WrongKindExpressionCompileBlock where - genericError WrongKindExpressionCompileBlock {..} = ask >>= generr - where - generr opts = - return - GenericError - { _genericErrorLoc = i, - _genericErrorMessage = prettyError msg, - _genericErrorIntervals = [i] - } - where - opts' = fromGenericOptions opts - i = getLoc _wrongKindExpressionCompileBlockSym - msg = - "Symbol" - <+> ppCode opts' _wrongKindExpressionCompileBlockSym - <+> "is not a constructor, inductive data type, axiom nor a function." - <> "Thus, it cannot have a compile rule." - infixErrorAux :: Doc Ann -> Doc Ann -> Doc Ann infixErrorAux kind pp = "Error while resolving infixities in the" diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 8917018a8c..ace4208c1a 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -158,10 +158,8 @@ statement = P.label "" $ do <|> (StatementOpenModule <$> openModule) <|> (StatementImport <$> import_) <|> (StatementInductive <$> inductiveDef Nothing) - <|> (StatementForeign <$> foreignBlock) <|> (StatementModule <$> moduleDef) <|> (StatementAxiom <$> axiomDef Nothing) - <|> (StatementCompile <$> compileBlock) <|> builtinStatement <|> ( either StatementTypeSignature StatementFunctionClause <$> auxTypeSigFunClause @@ -264,42 +262,6 @@ builtinStatement = do <|> (builtinFunction >>= fmap StatementTypeSignature . builtinTypeSig) <|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef) --------------------------------------------------------------------------------- --- Compile --------------------------------------------------------------------------------- - -compileBlock :: forall r. (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r (Compile 'Parsed) -compileBlock = do - _compileKw <- kw kwCompile - _compileName <- symbol - _compileBackendItems <- backends - return Compile {..} - where - backends = toList <$> braces (P.sepEndBy1 backendItem (kw kwSemicolon)) - backendItem :: ParsecS r BackendItem - backendItem = do - _backendItemBackend <- backend - kw kwMapsTo - _backendItemCode <- fst <$> string - return BackendItem {..} - --------------------------------------------------------------------------------- --- Foreign --------------------------------------------------------------------------------- - -backend :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (WithLoc Backend) -backend = - withLoc $ - kw ghc $> BackendGhc - <|> kw cBackend $> BackendC - -foreignBlock :: (Members '[InfoTableBuilder, JudocStash, NameIdGen] r) => ParsecS r ForeignBlock -foreignBlock = do - _foreignKw <- kw kwForeign - _foreignBackend <- backend - _foreignCode <- bracedString - return ForeignBlock {..} - -------------------------------------------------------------------------------- -- Operator syntax declaration -------------------------------------------------------------------------------- diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs index a7e76f25bb..c4e9ad0656 100644 --- a/src/Juvix/Compiler/Core/Extra/Utils.hs +++ b/src/Juvix/Compiler/Core/Extra/Utils.hs @@ -184,16 +184,6 @@ substDrop args argtys = where k = length args --- | reduce all beta redexes present in a term and the ones created immediately --- downwards (i.e., a "beta-development") -developBeta :: Node -> Node -developBeta = umap go - where - go :: Node -> Node - go n = case n of - NApp (App _ (NLam (Lambda {..})) arg) -> subst arg _lambdaBody - _ -> n - etaExpand :: [Type] -> Node -> Node etaExpand [] n = n etaExpand argtys n = diff --git a/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs b/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs deleted file mode 100644 index 101ae8d59f..0000000000 --- a/src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs +++ /dev/null @@ -1,48 +0,0 @@ -module Juvix.Compiler.Core.Info.FreeVarsInfo where - -import Data.HashMap.Strict qualified as HashMap -import Juvix.Compiler.Core.Extra -import Juvix.Compiler.Core.Info qualified as Info -import Juvix.Compiler.Core.Language - -newtype FreeVarsInfo = FreeVarsInfo - { -- map free variables to the number of their occurrences - _infoFreeVars :: HashMap Index Int - } - -instance IsInfo FreeVarsInfo - -kFreeVarsInfo :: Key FreeVarsInfo -kFreeVarsInfo = Proxy - -makeLenses ''FreeVarsInfo - -computeFreeVarsInfo :: Node -> Node -computeFreeVarsInfo = umapN go - where - go :: Index -> Node -> Node - go k n = case n of - NVar (Var i idx) | idx >= k -> mkVar (Info.insert fvi i) idx - where - fvi = FreeVarsInfo (HashMap.singleton (idx - k) 1) - _ -> modifyInfo (Info.insert fvi) n - where - fvi = - FreeVarsInfo $ - foldr - ( \n' acc -> - let m = n' ^. childBindersNum - in HashMap.unionWith (+) acc $ - HashMap.mapKeys (\j -> j - m) $ - HashMap.filterWithKey - (\j _ -> j < m) - (getFreeVarsInfo (n' ^. childNode) ^. infoFreeVars) - ) - mempty - (children n) - -getFreeVarsInfo :: Node -> FreeVarsInfo -getFreeVarsInfo = fromJust . Info.lookup kFreeVarsInfo . getInfo - -freeVarOccurrences :: Index -> Node -> Int -freeVarOccurrences idx n = fromMaybe 0 (HashMap.lookup idx (getFreeVarsInfo n ^. infoFreeVars)) diff --git a/src/Juvix/Compiler/Core/Info/IdentInfo.hs b/src/Juvix/Compiler/Core/Info/IdentInfo.hs deleted file mode 100644 index f9a50c849b..0000000000 --- a/src/Juvix/Compiler/Core/Info/IdentInfo.hs +++ /dev/null @@ -1,41 +0,0 @@ -module Juvix.Compiler.Core.Info.IdentInfo where - -import Data.HashMap.Strict qualified as HashMap -import Juvix.Compiler.Core.Extra -import Juvix.Compiler.Core.Info qualified as Info -import Juvix.Compiler.Core.Language - -newtype IdentInfo = IdentInfo - { -- map symbols to the number of their occurrences - _infoIdents :: HashMap Symbol Int - } - -instance IsInfo IdentInfo - -kIdentInfo :: Key IdentInfo -kIdentInfo = Proxy - -makeLenses ''IdentInfo - -computeIdentInfo :: Node -> Node -computeIdentInfo = umap go - where - go :: Node -> Node - go n = case n of - NIdt (Ident i sym) -> mkIdent (Info.insert fvi i) sym - where - fvi = IdentInfo (HashMap.singleton sym 1) - _ -> modifyInfo (Info.insert fvi) n - where - fvi = - IdentInfo $ - foldr - (HashMap.unionWith (+) . (^. infoIdents) . getIdentInfo) - mempty - (childrenNodes n) - -getIdentInfo :: Node -> IdentInfo -getIdentInfo = Info.lookupDefault (IdentInfo mempty) . getInfo - -identOccurrences :: Symbol -> Node -> Int -identOccurrences sym = fromMaybe 0 . HashMap.lookup sym . (^. infoIdents) . getIdentInfo diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs index 9c17f1149f..0255a14e05 100644 --- a/src/Juvix/Compiler/Core/Keywords.hs +++ b/src/Juvix/Compiler/Core/Keywords.hs @@ -14,7 +14,6 @@ import Juvix.Data.Keyword.All kwCase, kwColon, kwComma, - kwConstr, kwDef, kwDiv, kwElse, diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 4f8bcfcbfc..8ccfd6edcf 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -123,7 +123,6 @@ registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements) go = \case Internal.StatementInductive d -> goInductiveDef d Internal.StatementAxiom {} -> return () - Internal.StatementForeign {} -> return () Internal.StatementFunction {} -> return () Internal.StatementInclude i -> mapM_ go (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements) diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs index 01b80a8008..c0166520af 100644 --- a/src/Juvix/Compiler/Internal/Language.hs +++ b/src/Juvix/Compiler/Internal/Language.hs @@ -39,7 +39,6 @@ newtype ModuleBody = ModuleBody data Statement = StatementInductive InductiveDef | StatementFunction MutualBlock - | StatementForeign ForeignBlock | StatementAxiom AxiomDef | StatementInclude Include deriving stock (Data) diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index a78511b0f5..efcf6dbddf 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -113,12 +113,6 @@ instance PrettyCode Lambda where instance PrettyCode a => PrettyCode (WithLoc a) where ppCode = ppCode . (^. withLocParam) -instance PrettyCode BackendItem where - ppCode BackendItem {..} = do - backend <- ppCode _backendItemBackend - return $ - backend <+> kwMapsto <+> pretty _backendItemCode - instance PrettyCode FunctionParameter where ppCode FunctionParameter {..} = do case _paramName of @@ -200,23 +194,6 @@ instance PrettyCode FunctionClause where clauseBody' <- ppCode (c ^. clauseBody) return $ nest 2 (funName <+?> clausePatterns' <+> kwAssign <+> clauseBody') -instance PrettyCode Backend where - ppCode = \case - BackendGhc -> return kwGhc - BackendC -> return kwC - -instance PrettyCode ForeignBlock where - ppCode ForeignBlock {..} = do - _foreignBackend' <- ppCode _foreignBackend - return $ - kwForeign - <+> _foreignBackend' - <+> lbrace - <> line - <> pretty _foreignCode - <> line - <> rbrace - instance PrettyCode Include where ppCode i = do name' <- ppCode (i ^. includeModule . moduleName) @@ -234,7 +211,6 @@ instance PrettyCode MutualBlock where instance PrettyCode Statement where ppCode = \case - StatementForeign f -> ppCode f StatementFunction f -> ppCode f StatementInductive f -> ppCode f StatementAxiom f -> ppCode f diff --git a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs index 97c5d1dcd8..aa9b50f3cc 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromAbstract.hs @@ -148,7 +148,6 @@ goStatement :: Sem r (Maybe Statement) goStatement = \case Abstract.StatementAxiom d -> Just . StatementAxiom <$> goAxiomDef d - Abstract.StatementForeign f -> return (Just (StatementForeign f)) Abstract.StatementFunction {} -> return Nothing Abstract.StatementImport i -> fmap StatementInclude <$> goImport i Abstract.StatementLocalModule {} -> unsupported "local modules" diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs index 3985414f2b..ffdf87e9e1 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs @@ -49,7 +49,6 @@ checkStatement :: checkStatement s = case s of StatementFunction b -> StatementFunction <$> checkMutualBlock b StatementInclude i -> StatementInclude <$> checkInclude i - StatementForeign {} -> return s StatementInductive d -> StatementInductive <$> checkInductive d StatementAxiom a -> StatementAxiom <$> checkAxiom a diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs index 983cff27db..79ddf76724 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Reachability.hs @@ -31,7 +31,6 @@ goStatement :: (Member (Reader NameDependencyInfo) r) => Statement -> Sem r (May goStatement s = case s of StatementInductive i -> returnIfReachable (i ^. inductiveName) s StatementFunction (MutualBlock (f :| _)) -> returnIfReachable (f ^. funDefName) s -- note that any function is reachable iff all are reachable - StatementForeign {} -> return (Just s) StatementAxiom ax -> returnIfReachable (ax ^. axiomName) s StatementInclude i -> do m <- goModule (i ^. includeModule) diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs index 3d3a15be98..d4d80abeb7 100644 --- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs +++ b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs @@ -58,7 +58,6 @@ checkStatement :: Sem r Statement checkStatement s = case s of StatementFunction funs -> StatementFunction <$> runReader emptyLocalVars (checkMutualBlock funs) - StatementForeign {} -> return s StatementInductive ind -> StatementInductive <$> checkInductiveDef ind StatementInclude i -> StatementInclude <$> checkInclude i StatementAxiom ax -> do diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 5224a22e3d..a6e4890825 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/src/Juvix/Compiler/Pipeline.hs @@ -108,12 +108,6 @@ typecheck = >=> Internal.arityChecking >=> Internal.typeChecking -compile :: - (Members PipelineEff r) => - EntryPoint -> - Sem r C.MiniCResult -compile = typecheck >=> C.fromInternal - upToParsing :: (Members '[Reader EntryPoint, Files, Error JuvixError, NameIdGen, PathResolver] r) => Sem r Parser.ParserResult diff --git a/src/Juvix/Data.hs b/src/Juvix/Data.hs index fa782d377c..8a3a477653 100644 --- a/src/Juvix/Data.hs +++ b/src/Juvix/Data.hs @@ -1,9 +1,7 @@ module Juvix.Data - ( module Juvix.Data.Backends, - module Juvix.Data.Effect, + ( module Juvix.Data.Effect, module Juvix.Data.Error, module Juvix.Data.Fixity, - module Juvix.Data.ForeignBlock, module Juvix.Data.Hole, module Juvix.Data.IsImplicit, module Juvix.Data.Loc, @@ -19,13 +17,11 @@ module Juvix.Data ) where -import Juvix.Data.Backends import Juvix.Data.Comment import Juvix.Data.DependencyInfo import Juvix.Data.Effect import Juvix.Data.Error import Juvix.Data.Fixity -import Juvix.Data.ForeignBlock import Juvix.Data.Hole import Juvix.Data.Irrelevant import Juvix.Data.IsImplicit diff --git a/src/Juvix/Data/Backends.hs b/src/Juvix/Data/Backends.hs deleted file mode 100644 index fdc9349598..0000000000 --- a/src/Juvix/Data/Backends.hs +++ /dev/null @@ -1,21 +0,0 @@ -module Juvix.Data.Backends where - -import Juvix.Data.WithLoc -import Juvix.Prelude.Base - -data Backend - = BackendGhc - | BackendC - deriving stock (Show, Eq, Ord, Generic, Data) - -instance Hashable Backend - -data BackendItem = BackendItem - { _backendItemBackend :: WithLoc Backend, - _backendItemCode :: Text - } - deriving stock (Show, Ord, Eq, Generic, Data) - -instance Hashable BackendItem - -makeLenses ''BackendItem diff --git a/src/Juvix/Data/CodeAnn.hs b/src/Juvix/Data/CodeAnn.hs index c029e4231d..f0cb9e93ec 100644 --- a/src/Juvix/Data/CodeAnn.hs +++ b/src/Juvix/Data/CodeAnn.hs @@ -74,18 +74,6 @@ kwArrow = keyword Str.toUnicode kwMapsto :: Doc Ann kwMapsto = keyword Str.mapstoUnicode -kwForeign :: Doc Ann -kwForeign = keyword Str.foreign_ - -kwCompile :: Doc Ann -kwCompile = keyword Str.compile - -kwC :: Doc Ann -kwC = keyword Str.cBackend - -kwGhc :: Doc Ann -kwGhc = keyword Str.ghc - kwColon :: Doc Ann kwColon = keyword Str.colon @@ -128,15 +116,9 @@ kwEnd = keyword Str.end kwBuiltin :: Doc Ann kwBuiltin = keyword Str.builtin -kwNat :: Doc Ann -kwNat = keyword Str.nat - kwInductive :: Doc Ann kwInductive = keyword Str.inductive -kwArrowR :: Doc Ann -kwArrowR = keyword Str.toUnicode - kwLet :: Doc Ann kwLet = keyword Str.let_ @@ -158,15 +140,6 @@ kwInfixl = keyword Str.infixl_ kwInfix :: Doc Ann kwInfix = keyword Str.infix_ -kwColonZero :: Doc Ann -kwColonZero = keyword Str.colonZero - -kwColonOne :: Doc Ann -kwColonOne = keyword Str.colonOne - -kwColonOmega :: Doc Ann -kwColonOmega = keyword Str.colonOmegaUnicode - kwOpen :: Doc Ann kwOpen = keyword Str.open diff --git a/src/Juvix/Data/ForeignBlock.hs b/src/Juvix/Data/ForeignBlock.hs deleted file mode 100644 index a2764f0feb..0000000000 --- a/src/Juvix/Data/ForeignBlock.hs +++ /dev/null @@ -1,15 +0,0 @@ -module Juvix.Data.ForeignBlock where - -import Juvix.Data.Backends -import Juvix.Data.Keyword -import Juvix.Data.WithLoc -import Juvix.Prelude.Base - -data ForeignBlock = ForeignBlock - { _foreignKw :: KeywordRef, - _foreignBackend :: WithLoc Backend, - _foreignCode :: Text - } - deriving stock (Eq, Ord, Show, Data) - -makeLenses ''ForeignBlock diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs index e24b5c19fc..f2f4d01881 100644 --- a/src/Juvix/Data/Keyword/All.hs +++ b/src/Juvix/Data/Keyword/All.hs @@ -25,18 +25,6 @@ kwAxiom = asciiKw Str.axiom kwColon :: Keyword kwColon = asciiKw Str.colon -kwColonOmega :: Keyword -kwColonOmega = unicodeKw Str.colonOmegaAscii Str.colonOmegaUnicode - -kwColonOne :: Keyword -kwColonOne = asciiKw Str.colonOne - -kwColonZero :: Keyword -kwColonZero = asciiKw Str.colonZero - -kwCompile :: Keyword -kwCompile = asciiKw Str.compile - kwEnd :: Keyword kwEnd = asciiKw Str.end @@ -46,9 +34,6 @@ kwHiding = asciiKw Str.hiding kwImport :: Keyword kwImport = asciiKw Str.import_ -kwForeign :: Keyword -kwForeign = asciiKw Str.foreign_ - kwIn :: Keyword kwIn = asciiKw Str.in_ @@ -118,18 +103,9 @@ kwHole = asciiKw Str.underscore kwWildcard :: Keyword kwWildcard = asciiKw Str.underscore -ghc :: Keyword -ghc = asciiKw Str.ghc - -cBackend :: Keyword -cBackend = asciiKw Str.cBackend - kwLetRec :: Keyword kwLetRec = asciiKw Str.letrec_ -kwConstr :: Keyword -kwConstr = asciiKw Str.constr - kwCase :: Keyword kwCase = asciiKw Str.case_ @@ -221,10 +197,10 @@ kwFalse :: Keyword kwFalse = asciiKw Str.false_ kwArg :: Keyword -kwArg = asciiKw Str.arg_ +kwArg = asciiKw Str.arg kwTmp :: Keyword -kwTmp = asciiKw Str.tmp_ +kwTmp = asciiKw Str.tmp kwUnit :: Keyword kwUnit = asciiKw Str.unit diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index 00d925acd1..b4a0118a9b 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -44,9 +44,6 @@ variable = "variable" constructor :: (IsString s) => s constructor = "constructor" -constr :: (IsString s) => s -constr = "constr" - topModule :: (IsString s) => s topModule = "top module" @@ -68,9 +65,6 @@ open = "open" postfix :: (IsString s) => s postfix = "postfix" -print :: (IsString s) => s -print = "print" - let_ :: (IsString s) => s let_ = "let" @@ -110,9 +104,6 @@ stringToNat = "string-to-nat" bool_ :: (IsString s) => s bool_ = "bool" -boolean_ :: (IsString s) => s -boolean_ = "boolean" - boolPrint :: (IsString s) => s boolPrint = "bool-print" @@ -257,12 +248,6 @@ mapstoUnicode = "↦" mapstoAscii :: (IsString s) => s mapstoAscii = "->" -foreign_ :: (IsString s) => s -foreign_ = "foreign" - -compile :: (IsString s) => s -compile = "compile" - comma :: (IsString s) => s comma = "," @@ -281,27 +266,6 @@ dot = "." colon :: (IsString s) => s colon = ":" -colonSpace :: (IsString s) => s -colonSpace = ": " - -colonOmegaUnicode :: (IsString s) => s -colonOmegaUnicode = ":ω" - -colonOmegaAscii :: (IsString s) => s -colonOmegaAscii = ":any" - -colonOne :: (IsString s) => s -colonOne = ":1" - -colonZero :: (IsString s) => s -colonZero = ":0" - -ghc :: (IsString s) => s -ghc = "ghc" - -cBackend :: (IsString s) => s -cBackend = "c" - terminating :: (IsString s) => s terminating = "terminating" @@ -311,36 +275,9 @@ positive = "positive" waveArrow :: (IsString s) => s waveArrow = "↝" -stdlib :: (IsString s) => s -stdlib = "stdlib.h" - -stdbool :: (IsString s) => s -stdbool = "stdbool.h" - -stdio :: (IsString s) => s -stdio = "stdio.h" - main :: (IsString s) => s main = "main" -fprintf :: (IsString s) => s -fprintf = "fprintf" - -stderr_ :: (IsString s) => s -stderr_ = "stderr" - -exit :: (IsString s) => s -exit = "exit" - -exitFailure_ :: (IsString s) => s -exitFailure_ = "EXIT_FAILURE" - -malloc :: (IsString s) => s -malloc = "malloc" - -sizeof :: (IsString s) => s -sizeof = "sizeof" - true_ :: (IsString s) => s true_ = "true" @@ -350,27 +287,6 @@ false_ = "false" default_ :: (IsString s) => s default_ = "default" -arg_ :: (IsString s) => s -arg_ = "arg" - -tmp_ :: (IsString s) => s -tmp_ = "tmp" - -tag :: (IsString s) => s -tag = "tag" - -main_ :: (IsString s) => s -main_ = "main" - -minicRuntime :: (IsString s) => s -minicRuntime = "c-runtime.h" - -putStrLn_ :: (IsString s) => s -putStrLn_ = "putStrLn" - -debug_ :: (IsString s) => s -debug_ = "debug" - plus :: (IsString s) => s plus = "+" @@ -404,33 +320,15 @@ piUnicode = "Π" piAscii :: (IsString s) => s piAscii = "Pi" -pi_ :: (IsString s) => s -pi_ = "pi" - def :: (IsString s) => s def = "def" -zero :: (IsString s) => s -zero = "0" - -succ :: (IsString s) => s -succ = "S" - unit :: (IsString s) => s unit = "unit" void :: (IsString s) => s void = "void" -nil :: (IsString s) => s -nil = "nil" - -cons :: (IsString s) => s -cons = "cons" - -pair :: (IsString s) => s -pair = "pair" - case_ :: (IsString s) => s case_ = "case" @@ -449,9 +347,6 @@ with_ = "with" fun_ :: (IsString s) => s fun_ = "function" -fwd_ :: (IsString s) => s -fwd_ = "forward" - integer :: (IsString s) => s integer = "integer" @@ -632,8 +527,5 @@ gebInteger = "int" gebTyped :: IsString s => s gebTyped = "typed" -juvixFunctionT :: IsString s => s -juvixFunctionT = "juvix_function_t" - juvixDotOrg :: (IsString s) => s juvixDotOrg = "https://juvix.org" diff --git a/test/Reachability/Positive.hs b/test/Reachability/Positive.hs index 8850058286..a0a1bd4027 100644 --- a/test/Reachability/Positive.hs +++ b/test/Reachability/Positive.hs @@ -52,7 +52,6 @@ getNames m = concatMap getDeclName (m ^. (Internal.moduleBody . Internal.moduleS getDeclName = \case Internal.StatementInductive i -> [i ^. (Internal.inductiveName . Internal.nameText)] Internal.StatementFunction (Internal.MutualBlock f) -> map (^. Internal.funDefName . Internal.nameText) (toList f) - Internal.StatementForeign {} -> [] Internal.StatementAxiom ax -> [ax ^. (Internal.axiomName . Internal.nameText)] Internal.StatementInclude i -> getNames (i ^. Internal.includeModule) diff --git a/test/Scope/Negative.hs b/test/Scope/Negative.hs index 1b15c10403..c77d15ffb2 100644 --- a/test/Scope/Negative.hs +++ b/test/Scope/Negative.hs @@ -171,13 +171,6 @@ scoperErrorTests = $ \case ErrAmbiguousSym {} -> Nothing _ -> wrongError, - NegTest - "Wrong location of a compile block" - $(mkRelDir "CompileBlocks") - $(mkRelFile "WrongLocationCompileBlock.juvix") - $ \case - ErrWrongLocationCompileBlock {} -> Nothing - _ -> wrongError, NegTest "Implicit argument on the left of an application" $(mkRelDir ".") @@ -185,20 +178,6 @@ scoperErrorTests = $ \case ErrAppLeftImplicit {} -> Nothing _ -> wrongError, - NegTest - "Multiple compile blocks for the same name" - $(mkRelDir "CompileBlocks") - $(mkRelFile "MultipleCompileBlockSameName.juvix") - $ \case - ErrMultipleCompileBlockSameName {} -> Nothing - _ -> wrongError, - NegTest - "Multiple rules for a backend inside a compile block" - $(mkRelDir "CompileBlocks") - $(mkRelFile "MultipleCompileRuleSameBackend.juvix") - $ \case - ErrMultipleCompileRuleSameBackend {} -> Nothing - _ -> wrongError, NegTest "issue 230" $(mkRelDir "230") @@ -241,13 +220,6 @@ scoperErrorTests = $ \case ErrConstructorExpectedLeftApplication {} -> Nothing _ -> wrongError, - NegTest - "Compile block for a unsupported kind of expression" - $(mkRelDir "CompileBlocks") - $(mkRelFile "WrongKindExpressionCompileBlock.juvix") - $ \case - ErrWrongKindExpressionCompileBlock {} -> Nothing - _ -> wrongError, NegTest "A type parameter name occurs twice when declaring an inductive type" $(mkRelDir ".") diff --git a/test/Scope/Positive.hs b/test/Scope/Positive.hs index d980c6bc9d..aa2c9887fc 100644 --- a/test/Scope/Positive.hs +++ b/test/Scope/Positive.hs @@ -173,10 +173,6 @@ tests = "Axiom with backends" $(mkRelDir ".") $(mkRelFile "Axiom.juvix"), - PosTest - "Foreign block parsing" - $(mkRelDir ".") - $(mkRelFile "Foreign.juvix"), PosTest "Multiple modules non-ambiguous symbol - same file" $(mkRelDir "QualifiedSymbol") diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 5207a182d9..82f0b6fdc5 100644 --- a/test/Typecheck/Positive.hs +++ b/test/Typecheck/Positive.hs @@ -110,14 +110,6 @@ tests = "Literal Int matches any type" $(mkRelDir "Internal") $(mkRelFile "LiteralInt.juvix"), - posTest - "PolySimpleFungibleToken" - $(mkRelDir "FullExamples") - $(mkRelFile "SimpleFungibleTokenImplicit.juvix"), - posTest - "GHC backend MonoSimpleFungibleToken" - $(mkRelDir "FullExamples") - $(mkRelFile "MonoSimpleFungibleToken.juvix"), posTest "Axiom" $(mkRelDir ".") diff --git a/tests/Core/positive/lambda-lifting/test1.jvc b/tests/Core/positive/lambda-lifting/test1.jvc deleted file mode 100644 index 6fa6089eb6..0000000000 --- a/tests/Core/positive/lambda-lifting/test1.jvc +++ /dev/null @@ -1 +0,0 @@ -def t1 := \g \f f (\x \y \z g x); diff --git a/tests/Core/positive/lambda-lifting/test1.out b/tests/Core/positive/lambda-lifting/test1.out deleted file mode 100644 index c4d55f2392..0000000000 --- a/tests/Core/positive/lambda-lifting/test1.out +++ /dev/null @@ -1,3 +0,0 @@ --- IdentContext -def t1 := λg λf f$0 (!3 g$1) -def 3 := λg λx λy λz g$3 x$2 diff --git a/tests/Core/positive/lambda-lifting/test2.jvc b/tests/Core/positive/lambda-lifting/test2.jvc deleted file mode 100644 index 19dc730039..0000000000 --- a/tests/Core/positive/lambda-lifting/test2.jvc +++ /dev/null @@ -1 +0,0 @@ -def t2 := \r \s r (\x \y s y (\z z y x (\w w x) (\e y e x y))); diff --git a/tests/Core/positive/lambda-lifting/test2.out b/tests/Core/positive/lambda-lifting/test2.out deleted file mode 100644 index 6cd28653b0..0000000000 --- a/tests/Core/positive/lambda-lifting/test2.out +++ /dev/null @@ -1,6 +0,0 @@ --- IdentContext -def t2 := λr λs r$1 (!6 s$0) -def 3 := λx λw w$0 x$1 -def 4 := λy λx λe y$2 e$0 x$1 y$2 -def 5 := λy λx λz z$0 y$2 x$1 (!3 x$1) (!4 x$1 y$2) -def 6 := λs λx λy s$2 y$0 (!5 x$1 y$0) diff --git a/tests/Core/positive/lambda-lifting/test3.jvc b/tests/Core/positive/lambda-lifting/test3.jvc deleted file mode 100644 index 877379e065..0000000000 --- a/tests/Core/positive/lambda-lifting/test3.jvc +++ /dev/null @@ -1,3 +0,0 @@ -def const := \x \y x; -def id := \x x; -def t3 := \r \s const (\x x) (id (\x r)); diff --git a/tests/Core/positive/lambda-lifting/test3.out b/tests/Core/positive/lambda-lifting/test3.out deleted file mode 100644 index 9d10867b19..0000000000 --- a/tests/Core/positive/lambda-lifting/test3.out +++ /dev/null @@ -1,6 +0,0 @@ --- IdentContext -def const := λx λy x$1 -def id := λx x$0 -def t3 := λr λs const !5 (id (!6 r$1)) -def 5 := λx x$0 -def 6 := λr λx r$1 diff --git a/tests/negative/CompileBlocks/MultipleCompileBlockSameName.juvix b/tests/negative/CompileBlocks/MultipleCompileBlockSameName.juvix deleted file mode 100644 index 71be65a926..0000000000 --- a/tests/negative/CompileBlocks/MultipleCompileBlockSameName.juvix +++ /dev/null @@ -1,13 +0,0 @@ -module MultipleCompileBlockSameName; - -axiom A : Type; - -compile A { - ghc -> "Bool"; -}; - -compile A { - ghc -> "Bool"; -}; - -end; diff --git a/tests/negative/CompileBlocks/MultipleCompileRuleSameBackend.juvix b/tests/negative/CompileBlocks/MultipleCompileRuleSameBackend.juvix deleted file mode 100644 index ac36278171..0000000000 --- a/tests/negative/CompileBlocks/MultipleCompileRuleSameBackend.juvix +++ /dev/null @@ -1,11 +0,0 @@ -module MultipleCompileRuleSameBackend; - - -axiom A : Type; - -compile A { - ghc -> "Bool"; - ghc -> "Integer"; -}; - -end; diff --git a/tests/negative/CompileBlocks/Sample/Definitions.juvix b/tests/negative/CompileBlocks/Sample/Definitions.juvix deleted file mode 100644 index 6ebf0e48f3..0000000000 --- a/tests/negative/CompileBlocks/Sample/Definitions.juvix +++ /dev/null @@ -1,12 +0,0 @@ -module Sample.Definitions; - -axiom A : Type; - -type Nat := -zero : Nat | -suc : Nat -> Nat; - -f : A -> Nat; -f a := zero; - -end; diff --git a/tests/negative/CompileBlocks/WrongKindExpressionCompileBlock.juvix b/tests/negative/CompileBlocks/WrongKindExpressionCompileBlock.juvix deleted file mode 100644 index f2863326ff..0000000000 --- a/tests/negative/CompileBlocks/WrongKindExpressionCompileBlock.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module WrongKindExpressionCompileBlock; - -module A; -end; - -compile A { -ghc -> "X"; -}; - -end; diff --git a/tests/negative/CompileBlocks/WrongLocationCompileBlock.juvix b/tests/negative/CompileBlocks/WrongLocationCompileBlock.juvix deleted file mode 100644 index 7a893088a6..0000000000 --- a/tests/negative/CompileBlocks/WrongLocationCompileBlock.juvix +++ /dev/null @@ -1,9 +0,0 @@ -module WrongLocationCompileBlock; -import Sample.Definitions; -open Sample.Definitions; - -compile A { - ghc -> "Bool"; -}; - -end; diff --git a/tests/negative/CompileBlocks/juvix.yaml b/tests/negative/CompileBlocks/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/Axiom.juvix b/tests/positive/Axiom.juvix index e42edf0a38..d19300222b 100644 --- a/tests/positive/Axiom.juvix +++ b/tests/positive/Axiom.juvix @@ -1,8 +1,5 @@ module Axiom; axiom Action : Type; -compile Action { - ghc ↦ "IO ()"; -}; end; diff --git a/tests/positive/Foreign.juvix b/tests/positive/Foreign.juvix deleted file mode 100644 index 0708e6c7f3..0000000000 --- a/tests/positive/Foreign.juvix +++ /dev/null @@ -1,37 +0,0 @@ -module Foreign; - -foreign ghc {}; - -foreign ghc { import Foo.Bar }; - -foreign c { import Foo.Bar }; - -foreign ghc { import Foo.Bar - import Foo.Baz }; - -foreign ghc { - import Foo.Bar - import Foo.Baz }; - -foreign ghc { - import Foo.Bar - import Foo.Baz -}; - -foreign ghc { - import Foo.Bar - - import Foo.Baz -}; - -foreign ghc { - data Foo = Foo { _unFoo :: Int \} -- \\ test -}; - -foreign ghc { - data Foo = Foo { - _unFoo :: Int - \} -}; - -end; diff --git a/tests/positive/FullExamples/Anoma.hs b/tests/positive/FullExamples/Anoma.hs deleted file mode 100644 index fc4ae542d9..0000000000 --- a/tests/positive/FullExamples/Anoma.hs +++ /dev/null @@ -1,16 +0,0 @@ -module Anoma where - -import Prelude - -readPre :: String -> Int -readPre "change1-key" = 100 -readPre "change2-key" = 90 -readPre _ = -1 - -readPost :: String -> Int -readPost "change1-key" = 90 -readPost "change2-key" = 100 -readPost _ = -1 - -isBalanceKey :: String -> String -> String -isBalanceKey _ _ = "owner-address" diff --git a/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix b/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix deleted file mode 100644 index c9b4b0f662..0000000000 --- a/tests/positive/FullExamples/MonoSimpleFungibleToken.juvix +++ /dev/null @@ -1,310 +0,0 @@ -module MonoSimpleFungibleToken; - -foreign ghc { - import Anoma -}; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -type Bool := - true : Bool - | false : Bool; - -infixr 2 ||; -|| : Bool → Bool → Bool; -|| false a := a; -|| true _ := true; - -infixr 3 &&; -&& : Bool → Bool → Bool; -&& false _ := false; -&& true a := a; - --------------------------------------------------------------------------------- --- Backend Booleans --------------------------------------------------------------------------------- - -axiom BackendBool : Type; -compile BackendBool { - ghc ↦ "Bool"; -}; - -axiom backend-true : BackendBool; -compile backend-true { - ghc ↦ "True"; -}; - -axiom backend-false : BackendBool; -compile backend-false { - ghc ↦ "False"; -}; - --------------------------------------------------------------------------------- --- Backend Bridge --------------------------------------------------------------------------------- - -foreign ghc { - bool :: Bool -> a -> a -> a - bool True x _ = x - bool False _ y = y -}; - -axiom bool : BackendBool → Bool → Bool → Bool; -compile bool { - ghc ↦ "bool"; -}; - -from-backend-bool : BackendBool → Bool; -from-backend-bool bb := bool bb true false; - --------------------------------------------------------------------------------- --- Integers --------------------------------------------------------------------------------- - -axiom Int : Type; -compile Int { - ghc ↦ "Int"; -}; - -axiom Int_0 : Int; -compile Int_0 { - ghc ↦ "0"; -}; - -axiom lt : Int → Int → BackendBool; -compile lt { - ghc ↦ "(<)"; -}; - -infix 4 <; -< : Int → Int → Bool; -< i1 i2 := from-backend-bool (lt i1 i2); - -axiom eqInt : Int → Int → BackendBool; -compile eqInt { - ghc ↦ "(==)"; -}; - -infix 4 ==Int; -==Int : Int → Int → Bool; -==Int i1 i2 := from-backend-bool (eqInt i1 i2); - -infixl 6 -; -axiom - : Int -> Int -> Int; -compile - { - ghc ↦ "(-)"; -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - ghc ↦ "(+)"; -}; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -builtin string axiom String : Type; -compile String { - ghc ↦ "[Char]"; -}; - -axiom eqString : String → String → BackendBool; -compile eqString { - ghc ↦ "(==)"; -}; - -infix 4 ==String; -==String : String → String → Bool; -==String s1 s2 := from-backend-bool (eqString s1 s2); - --------------------------------------------------------------------------------- --- Lists --------------------------------------------------------------------------------- - -type ListString := - Nil : ListString | - Cons : String → ListString → ListString; - -elem : String → ListString → Bool; -elem s Nil := false; -elem s (Cons x xs) := (s ==String x) || elem s xs; - --------------------------------------------------------------------------------- --- Pair --------------------------------------------------------------------------------- - -type PairIntBool := - MakePair : Int → Bool → PairIntBool; - -if-pairIntBool : Bool → PairIntBool → PairIntBool → PairIntBool; -if-pairIntBool true x _ := x; -if-pairIntBool false _ y := y; - --------------------------------------------------------------------------------- --- Optionals --------------------------------------------------------------------------------- - -type OptionInt := - NothingInt : OptionInt | - JustInt : Int -> OptionInt; - -if-optionInt : Bool → OptionInt → OptionInt → OptionInt; -if-optionInt true x _ := x; -if-optionInt false _ y := y; - -from-int : Int → OptionInt; -from-int i := if-optionInt (i < Int_0) NothingInt (JustInt i); - -maybe-int : Int → OptionInt → Int; -maybe-int d NothingInt := d; -maybe-int _ (JustInt i) := i; - -type OptionString := - NothingString : OptionString | - JustString : String -> OptionString; - -if-optionString : Bool → OptionString → OptionString → OptionString; -if-optionString true x _ := x; -if-optionString false _ y := y; - -from-string : String → OptionString; -from-string s := if-optionString (s ==String "") NothingString (JustString s); - -pair-from-optionString : (String → PairIntBool) → OptionString → PairIntBool; -pair-from-optionString _ NothingString := MakePair Int_0 false; -pair-from-optionString f (JustString o) := f o; - --------------------------------------------------------------------------------- --- foldl --------------------------------------------------------------------------------- - -foldl : (PairIntBool → String → PairIntBool) → PairIntBool → ListString → PairIntBool; -foldl f z Nil := z; -foldl f z (Cons h hs) := foldl f (f z h) hs; - --------------------------------------------------------------------------------- --- Anoma --------------------------------------------------------------------------------- - -axiom readPre : String → Int; -compile readPre { - ghc ↦ "readPre"; -}; - -axiom readPost : String → Int; -compile readPost { - ghc ↦ "readPost"; -}; - -axiom isBalanceKey : String → String → String; -compile isBalanceKey { - ghc ↦ "isBalanceKey"; -}; - -read-pre : String → OptionInt; -read-pre s := from-int (readPre s); - -read-post : String → OptionInt; -read-post s := from-int (readPost s); - -is-balance-key : String → String → OptionString; -is-balance-key token key := from-string (isBalanceKey token key); - -unwrap-default : OptionInt → Int; -unwrap-default o := maybe-int Int_0 o; - --------------------------------------------------------------------------------- --- Validity Predicate --------------------------------------------------------------------------------- - -change-from-key : String → Int; -change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); - -check-vp : ListString → String → Int → String → PairIntBool; -check-vp verifiers key change owner := - if-pairIntBool - (change-from-key key < Int_0) - -- make sure the spender approved the transaction - (MakePair (change + (change-from-key key)) (elem owner verifiers)) - (MakePair (change + (change-from-key key)) true); - -check-keys : String → ListString → PairIntBool → String → PairIntBool; -check-keys token verifiers (MakePair change is-success) key := - if-pairIntBool - is-success - (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) - (MakePair Int_0 false); - -check-result : PairIntBool → Bool; -check-result (MakePair change all-checked) := (change ==Int Int_0) && all-checked; - -vp : String → ListString → ListString → Bool; -vp token keys-changed verifiers := - check-result - (foldl - (check-keys token verifiers) - (MakePair Int_0 true) - keys-changed); - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; -compile Action { - ghc ↦ "IO ()"; -}; - -axiom putStr : String → Action; -compile putStr { - ghc ↦ "putStr"; -}; - -axiom putStrLn : String → Action; -compile putStrLn { - ghc ↦ "putStrLn"; -}; - -infixl 1 >>; -axiom >> : Action → Action → Action ; - -compile >> { - ghc ↦ "(>>)"; -}; - -show-result : Bool → String; -show-result true := "OK"; -show-result false := "FAIL"; - --------------------------------------------------------------------------------- --- Testing VP --------------------------------------------------------------------------------- - -token : String; -token := "owner-token"; - -owner-address : String; -owner-address := "owner-address"; - -change1-key : String; -change1-key := "change1-key"; - -change2-key : String; -change2-key := "change2-key"; - -verifiers : ListString; -verifiers := Cons owner-address Nil; - -keys-changed : ListString; -keys-changed := Cons change1-key (Cons change2-key Nil); - -main : Action; -main := - (putStr "VP Status: ") - >> (putStrLn (show-result (vp token keys-changed verifiers))); - -end; diff --git a/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix b/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix deleted file mode 100644 index be9bebbce3..0000000000 --- a/tests/positive/FullExamples/SimpleFungibleTokenImplicit.juvix +++ /dev/null @@ -1,310 +0,0 @@ -module SimpleFungibleTokenImplicit; - -foreign ghc { - import Anoma -}; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -type Bool := - true : Bool - | false : Bool; - -infixr 2 ||; -|| : Bool → Bool → Bool; -|| false a := a; -|| true _ := true; - -infixr 3 &&; -&& : Bool → Bool → Bool; -&& false _ := false; -&& true a := a; - -if : {A : Type} → Bool → A → A → A; -if true a _ := a; -if false _ b := b; - --------------------------------------------------------------------------------- --- Backend Booleans --------------------------------------------------------------------------------- - -axiom BackendBool : Type; - -compile BackendBool { - ghc ↦ "Bool"; -}; - -axiom backend-true : BackendBool; -compile backend-true { - ghc ↦ "True"; -}; - -axiom backend-false : BackendBool; -compile backend-false { - ghc ↦ "False"; -}; - --------------------------------------------------------------------------------- --- Backend Bridge --------------------------------------------------------------------------------- - -foreign ghc { - bool :: Bool -> a -> a -> a - bool True x _ = x - bool False _ y = y -}; - -axiom bool : BackendBool → Bool → Bool → Bool; -compile bool { - ghc ↦ "bool"; -}; - -from-backend-bool : BackendBool → Bool; -from-backend-bool bb := bool bb true false; - --------------------------------------------------------------------------------- --- Functions --------------------------------------------------------------------------------- - -id : {A : Type} → A → A; -id a := a; - --------------------------------------------------------------------------------- --- Integers --------------------------------------------------------------------------------- - -axiom Int : Type; -compile Int { - ghc ↦ "Int"; -}; - - -axiom Int_0 : Int; -compile Int_0 { - c ↦ "0"; -}; - -axiom Int_1 : Int; -compile Int_1 { - c ↦ "1"; -}; - -infix 4 <'; -axiom <' : Int → Int → BackendBool; -compile <' { - ghc ↦ "(<)"; -}; - -infix 4 <; -< : Int → Int → Bool; -< i1 i2 := from-backend-bool (i1 <' i2); - -axiom eqInt : Int → Int → BackendBool; -compile eqInt { - ghc ↦ "(==)"; -}; - -infix 4 ==Int; -==Int : Int → Int → Bool; -==Int i1 i2 := from-backend-bool (eqInt i1 i2); - -infixl 6 -; -axiom - : Int -> Int -> Int; -compile - { - ghc ↦ "(-)"; -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - ghc ↦ "(+)"; -}; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -builtin string axiom String : Type; -compile String { - ghc ↦ "[Char]"; -}; - -axiom eqString : String → String → BackendBool; -compile eqString { - ghc ↦ "(==)"; -}; - -infix 4 ==String; -==String : String → String → Bool; -==String s1 s2 := from-backend-bool (eqString s1 s2); - --------------------------------------------------------------------------------- --- Lists --------------------------------------------------------------------------------- - -infixr 5 ::; -type List (A : Type) := - nil : List A - | :: : A → List A → List A; - -elem : {A : Type} → (A → A → Bool) → A → List A → Bool; -elem _ _ nil := false; -elem eq s (x :: xs) := eq s x || elem eq s xs; - -foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil := z; -foldl f z (h :: hs) := foldl f (f z h) hs; - --------------------------------------------------------------------------------- --- Pair --------------------------------------------------------------------------------- - -infixr 4 ,; -infixr 2 ×; -type × (A : Type) (B : Type) := - , : A → B → A × B; - --------------------------------------------------------------------------------- --- Maybe --------------------------------------------------------------------------------- - -type Maybe (A : Type) := - nothing : Maybe A | - just : A → Maybe A; - -from-int : Int → Maybe Int; -from-int i := if (i < Int_0) nothing (just i); - -maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B; -maybe b _ nothing := b; -maybe _ f (just x) := f x; - -from-string : String → Maybe String; -from-string s := if (s ==String "") nothing (just s); - -pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; -pair-from-optionString := maybe (Int_0, false); - --------------------------------------------------------------------------------- --- Anoma --------------------------------------------------------------------------------- - -axiom readPre : String → Int; -compile readPre { - ghc ↦ "readPre"; -}; - -axiom readPost : String → Int; -compile readPost { - ghc ↦ "readPost"; -}; - -axiom isBalanceKey : String → String → String; -compile isBalanceKey { - ghc ↦ "isBalanceKey"; -}; - -read-pre : String → Maybe Int; -read-pre s := from-int (readPre s); - -read-post : String → Maybe Int; -read-post s := from-int (readPost s); - -is-balance-key : String → String → Maybe String; -is-balance-key token key := from-string (isBalanceKey token key); - -unwrap-default : Maybe Int → Int; -unwrap-default := maybe Int_0 id; - --------------------------------------------------------------------------------- --- Validity Predicate --------------------------------------------------------------------------------- - -change-from-key : String → Int; -change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); - -check-vp : List String → String → Int → String → Int × Bool; -check-vp verifiers key change owner := - if - (change-from-key key < Int_0) - -- make sure the spender approved the transaction - (change + (change-from-key key), elem (==String) owner verifiers) - (change + (change-from-key key), true); - -check-keys : String → List String → Int × Bool → String → Int × Bool; -check-keys token verifiers (change, is-success) key := - if - is-success - (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) - (Int_0, false); - -check-result : Int × Bool → Bool; -check-result (change, all-checked) := (change ==Int Int_0) && all-checked; - -vp : String → List String → List String → Bool; -vp token keys-changed verifiers := - check-result - (foldl - (check-keys token verifiers) - (Int_0, true) - keys-changed); - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; -compile Action { - ghc ↦ "IO ()"; -}; - -axiom putStr : String → Action; -compile putStr { - ghc ↦ "putStr"; -}; - -axiom putStrLn : String → Action; -compile putStrLn { - ghc ↦ "putStrLn"; -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; -compile >> { - ghc ↦ "(>>)"; -}; - -show-result : Bool → String; -show-result true := "OK"; -show-result false := "FAIL"; - --------------------------------------------------------------------------------- --- Testing VP --------------------------------------------------------------------------------- - -token : String; -token := "owner-token"; - -owner-address : String; -owner-address := "owner-address"; - -change1-key : String; -change1-key := "change1-key"; - -change2-key : String; -change2-key := "change2-key"; - -verifiers : List String; -verifiers := owner-address :: nil; - -keys-changed : List String; -keys-changed := change1-key :: change2-key :: nil; - -main : Action; -main := - (putStr "VP Status: ") - >> (putStrLn (show-result (vp token keys-changed verifiers))); - -end; diff --git a/tests/positive/FullExamples/juvix.yaml b/tests/positive/FullExamples/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/AlwaysValidVP/Input.juvix b/tests/positive/MiniC/AlwaysValidVP/Input.juvix deleted file mode 100644 index 6058778ba4..0000000000 --- a/tests/positive/MiniC/AlwaysValidVP/Input.juvix +++ /dev/null @@ -1,38 +0,0 @@ -module Input; - -open import Stdlib.Prelude; - -axiom AnomaPtr : Type; -compile AnomaPtr { - c ↦ "uint64_t"; -}; - -axiom AnomaSize : Type; -compile AnomaSize { - c ↦ "uint64_t"; -}; - -axiom AnomaBool : Type; -compile AnomaBool { - c ↦ "uint64_t"; -}; - -axiom AnomaBool_true : AnomaBool; -compile AnomaBool_true { - c ↦ "1"; -}; - -axiom AnomaBool_false : AnomaBool; -compile AnomaBool_false { - c ↦ "0"; -}; - -encodeBool : Bool → AnomaBool; -encodeBool true := AnomaBool_true; -encodeBool false := AnomaBool_false; - ---- The module entrypoint callable by wasm runtime -_validate_tx : AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaPtr → AnomaSize → AnomaBool; -_validate_tx _ _ _ _ _ _ _ _ := encodeBool true; - -end; diff --git a/tests/positive/MiniC/AlwaysValidVP/expected.golden b/tests/positive/MiniC/AlwaysValidVP/expected.golden deleted file mode 100644 index 7a5a058e16..0000000000 --- a/tests/positive/MiniC/AlwaysValidVP/expected.golden +++ /dev/null @@ -1 +0,0 @@ -1n diff --git a/tests/positive/MiniC/AlwaysValidVP/input.js b/tests/positive/MiniC/AlwaysValidVP/input.js deleted file mode 100644 index 3b27c8243c..0000000000 --- a/tests/positive/MiniC/AlwaysValidVP/input.js +++ /dev/null @@ -1,7 +0,0 @@ -const fs = require('fs'); - -const wasmBuffer = fs.readFileSync("Input.wasm"); - -WebAssembly.instantiate(wasmBuffer, {}).then((wasmModule) => { - console.log(wasmModule.instance.exports._validate_tx(0n,0n,0n,0n,0n,0n,0n,0n)); -}); diff --git a/tests/positive/MiniC/AlwaysValidVP/juvix.yaml b/tests/positive/MiniC/AlwaysValidVP/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/AxiomNoCompile/Input.juvix b/tests/positive/MiniC/AxiomNoCompile/Input.juvix deleted file mode 100644 index 74b2ee3f9b..0000000000 --- a/tests/positive/MiniC/AxiomNoCompile/Input.juvix +++ /dev/null @@ -1,13 +0,0 @@ -module Input; - -open import Stdlib.Prelude; - -type Unit := - unit : Unit; - -axiom ignore : Unit -> Unit; - -main : IO; -main := printStringLn "Hello"; - -end; diff --git a/tests/positive/MiniC/AxiomNoCompile/expected.golden b/tests/positive/MiniC/AxiomNoCompile/expected.golden deleted file mode 100644 index e965047ad7..0000000000 --- a/tests/positive/MiniC/AxiomNoCompile/expected.golden +++ /dev/null @@ -1 +0,0 @@ -Hello diff --git a/tests/positive/MiniC/AxiomNoCompile/juvix.yaml b/tests/positive/MiniC/AxiomNoCompile/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/Builtins/Input.juvix b/tests/positive/MiniC/Builtins/Input.juvix deleted file mode 100644 index 0bd80c6abc..0000000000 --- a/tests/positive/MiniC/Builtins/Input.juvix +++ /dev/null @@ -1,65 +0,0 @@ -module Input; - -builtin bool -type Bool := - true : Bool - | false : Bool; - -builtin bool-if -if : {A : Type} → Bool → A → A → A; -if true t _ := t; -if false _ e := e; - -builtin nat -type ℕ := - zero : ℕ | - suc : ℕ → ℕ; - -boolToNat : Bool → ℕ; -boolToNat false := zero; -boolToNat true := suc zero; - -infixl 4 +; -builtin nat-plus -+ : ℕ → ℕ → ℕ; -+ zero x := x; -+ (suc a) b := suc (a + b); - -mult : ℕ → ℕ → ℕ; -mult zero _ := zero; -mult (suc n) m := m + (mult n m); - -plusOne : ℕ → ℕ; -plusOne := suc; - -someLiteral : _; -someLiteral := 123; - -infix 4 ==; -== : ℕ → ℕ → Bool; -== zero zero := true; -== (suc n) (suc m) := n == m; -== _ _ := false; - -builtin IO axiom IO : Type; -builtin string axiom String : Type; - -infixl 1 >>; -builtin IO-sequence axiom >> : IO → IO → IO; -builtin nat-print axiom printNat : ℕ → IO; -builtin string-print axiom printString : String → IO; - -printNatLn : ℕ -> IO; -printNatLn n := printNat n >> printString "\n"; - -main : IO; -main := printNatLn (boolToNat true) - >> printNatLn (boolToNat false) - >> printNatLn (mult 3 (2 + 2)) - >> printNatLn 2 - >> printNatLn (if (1 == 2) 100 200) - >> printNatLn (if (1 == 1) 300 400) - >> if (1 == 2) (printNatLn 500) (printNatLn 600) - >> if (1 == 1) (printNatLn 700) (printNatLn 800); - -end; diff --git a/tests/positive/MiniC/Builtins/expected.golden b/tests/positive/MiniC/Builtins/expected.golden deleted file mode 100644 index 894065390f..0000000000 --- a/tests/positive/MiniC/Builtins/expected.golden +++ /dev/null @@ -1,8 +0,0 @@ -1 -0 -12 -2 -200 -300 -600 -700 diff --git a/tests/positive/MiniC/Builtins/juvix.yaml b/tests/positive/MiniC/Builtins/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/BuiltinsStdlib/Input.juvix b/tests/positive/MiniC/BuiltinsStdlib/Input.juvix deleted file mode 100644 index a6cae8520a..0000000000 --- a/tests/positive/MiniC/BuiltinsStdlib/Input.juvix +++ /dev/null @@ -1,21 +0,0 @@ -module Input; - -open import Stdlib.Prelude; -open import Stdlib.Data.Nat.Ord; - -mult : Nat → Nat → Nat; -mult zero _ := zero; -mult (suc n) m := m + (mult n m); - -main : IO; -main := printStringLn "hello" - >> printBoolLn true - >> printBoolLn false - >> printNatLn (mult 3 (2 + 2)) - >> printNatLn 2 - >> printNatLn (if (1 == 2) 100 200) - >> printNatLn (if (1 == 1) 300 400) - >> if (1 == 2) (printNatLn 500) (printNatLn 600) - >> if (1 == 1) (printNatLn 700) (printNatLn 800); - -end; diff --git a/tests/positive/MiniC/BuiltinsStdlib/expected.golden b/tests/positive/MiniC/BuiltinsStdlib/expected.golden deleted file mode 100644 index 61bd05c744..0000000000 --- a/tests/positive/MiniC/BuiltinsStdlib/expected.golden +++ /dev/null @@ -1,9 +0,0 @@ -hello -true -false -12 -2 -200 -300 -600 -700 diff --git a/tests/positive/MiniC/BuiltinsStdlib/juvix.yaml b/tests/positive/MiniC/BuiltinsStdlib/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/ClosureEnv/Data b/tests/positive/MiniC/ClosureEnv/Data deleted file mode 120000 index 6e2a68d952..0000000000 --- a/tests/positive/MiniC/ClosureEnv/Data +++ /dev/null @@ -1 +0,0 @@ -../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureEnv/Input.juvix b/tests/positive/MiniC/ClosureEnv/Input.juvix deleted file mode 100644 index bffe4cc6c9..0000000000 --- a/tests/positive/MiniC/ClosureEnv/Input.juvix +++ /dev/null @@ -1,107 +0,0 @@ -module Input; - -open import Data.IO; -open import Data.String; - -axiom Int : Type; -compile Int { - c ↦ "int"; -}; - -axiom Int_0 : Int; -compile Int_0 { - c ↦ "0"; -}; - -axiom Int_1 : Int; -compile Int_1 { - c ↦ "1"; -}; - -axiom to-str : Int → String; - -compile to-str { - c ↦ "intToStr"; -}; - -foreign c { - int cplus(int l, int r) { - return l + r; - \} -}; - -axiom plus : Int → Int → Int; - -compile plus { - c ↦ "cplus"; -}; - -type Nat := - zero : Nat - | suc : Nat → Nat; - -nplus : Nat → Nat → Nat; -nplus zero n := n; -nplus (suc m) n := suc (nplus m n); - -nplus-to-int : Nat → Int; -nplus-to-int zero := Int_0; -nplus-to-int (suc n) := plus Int_1 (nplus-to-int n); - -nOne : Nat; -nOne := suc zero; - -nplusOne : Nat → Nat → Nat; -nplusOne n := nplus nOne; - -plusOneInt : Int → Int; -plusOneInt := plus Int_1; - -one : Int; -one := Int_1; - -two : Int; -two := plusOneInt one; - -three : Int; -three := plusOneInt two; - -plusXIgnore2 : Int → Int → Int → Int → Int; -plusXIgnore2 _ _ := plus; - -plusXIgnore : Int → Int → Int → Int; -plusXIgnore _ := plus; - -plusXIgnore22 : Int → Int → Int → Int → Int; -plusXIgnore22 _ := plusXIgnore; - -plusX : Int → Int → Int; -plusX := plus; - -plusXThree : Int → Int; -plusXThree := plusX three; - -plusOne : Int → Int; -plusOne := plus one; - -plusOneThenTwo : Int; -plusOneThenTwo := plusOne two; - -plusOneThenX : Int → Int; -plusOneThenX x := plusOne x; - -plusOneTwo : Int; -plusOneTwo := plus one two; - -main : Action; -main := put-str "plusOne one: " >> put-str-ln (to-str (plusOne one)) - >> put-str "plusOneThenTwo: " >> put-str-ln (to-str (plusOneThenTwo)) - >> put-str "plusOneThenX three: " >> put-str-ln (to-str (plusOneThenX three)) - >> put-str "plusOneTwo: " >> put-str-ln (to-str (plusOneTwo)) - >> put-str "plusX three three: " >> put-str-ln (to-str (plusX three three)) - >> put-str "plusXIgnore one three three: " >> put-str-ln (to-str (plusXIgnore one three three)) - >> put-str "plusXIgnore2 one one three three: " >> put-str-ln (to-str (plusXIgnore2 one one three three)) - >> put-str "plusXIgnore22 one one three two: " >> put-str-ln (to-str (plusXIgnore22 one one three two)) - - -end; diff --git a/tests/positive/MiniC/ClosureEnv/Prelude.mjuvix b/tests/positive/MiniC/ClosureEnv/Prelude.mjuvix deleted file mode 120000 index 8fde4860a9..0000000000 --- a/tests/positive/MiniC/ClosureEnv/Prelude.mjuvix +++ /dev/null @@ -1 +0,0 @@ -../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureEnv/expected.golden b/tests/positive/MiniC/ClosureEnv/expected.golden deleted file mode 100644 index 2fab3ac3d0..0000000000 --- a/tests/positive/MiniC/ClosureEnv/expected.golden +++ /dev/null @@ -1,8 +0,0 @@ -plusOne one: 2 -plusOneThenTwo: 3 -plusOneThenX three: 4 -plusOneTwo: 3 -plusX three three: 6 -plusXIgnore one three three: 6 -plusXIgnore2 one one three three: 6 -plusXIgnore22 one one three two: 5 diff --git a/tests/positive/MiniC/ClosureEnv/juvix.yaml b/tests/positive/MiniC/ClosureEnv/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/ClosureNoEnv/Data b/tests/positive/MiniC/ClosureNoEnv/Data deleted file mode 120000 index 6e2a68d952..0000000000 --- a/tests/positive/MiniC/ClosureNoEnv/Data +++ /dev/null @@ -1 +0,0 @@ -../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureNoEnv/Input.juvix b/tests/positive/MiniC/ClosureNoEnv/Input.juvix deleted file mode 100644 index d5deee2eb4..0000000000 --- a/tests/positive/MiniC/ClosureNoEnv/Input.juvix +++ /dev/null @@ -1,84 +0,0 @@ -module Input; - -open import Data.IO; -open import Data.String; - -axiom Int : Type; -compile Int { - c ↦ "int"; -}; - -axiom Int_0 : Int; -compile Int_0 { - c ↦ "0"; -}; - -axiom Int_1 : Int; -compile Int_1 { - c ↦ "1"; -}; - -axiom Int_2 : Int; -compile Int_2 { - c ↦ "2"; -}; - -axiom to-str : Int → String; - -compile to-str { - c ↦ "intToStr"; -}; - -foreign c { - int cplus(int l, int r) { - return l + r; - \} -}; - -axiom plus : Int → Int → Int; - -compile plus { - c ↦ "cplus"; -}; - -apply : (Int → Int → Int) → Int → Int → Int; -apply f a b := f a b; - -type Nat := - zero : Nat - | suc : Nat → Nat; - -plus-nat : Nat → Nat → Nat; -plus-nat zero n := n; -plus-nat (suc m) n := suc (plus-nat m n); - -apply-nat : (Nat → Nat) → Nat → Nat; -apply-nat f a := f a; - -apply-nat2 : (Nat → Nat → Nat) → Nat → Nat → Nat; -apply-nat2 f a b := f a b; - -nat-to-int : Nat → Int; -nat-to-int zero := Int_0; -nat-to-int (suc n) := plus Int_1 (nat-to-int n); - -one : Nat; -one := suc zero; - -nest-apply : ((Nat → Nat) → Nat → Nat) → (Nat → Nat) → Nat → Nat; -nest-apply f g x := f g x; - -two : Nat; -two := suc one; - -main : Action; -main := put-str "plus 1 2: " - >> put-str-ln (to-str (apply plus Int_1 Int_2)) - >> put-str "suc one: " - >> put-str-ln (to-str (nat-to-int (apply-nat suc one))) - >> put-str "plus-nat 1 2: " - >> put-str-ln (to-str (nat-to-int (apply-nat2 plus-nat one two))) - >> put-str "nest-apply apply-nat suc one: " - >> put-str-ln (to-str (nat-to-int (nest-apply apply-nat suc one))); - -end; diff --git a/tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix b/tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix deleted file mode 120000 index 8fde4860a9..0000000000 --- a/tests/positive/MiniC/ClosureNoEnv/Prelude.mjuvix +++ /dev/null @@ -1 +0,0 @@ -../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/ClosureNoEnv/expected.golden b/tests/positive/MiniC/ClosureNoEnv/expected.golden deleted file mode 100644 index 21b6d4fb24..0000000000 --- a/tests/positive/MiniC/ClosureNoEnv/expected.golden +++ /dev/null @@ -1,4 +0,0 @@ -plus 1 2: 3 -suc one: 2 -plus-nat 1 2: 3 -nest-apply apply-nat suc one: 2 diff --git a/tests/positive/MiniC/ClosureNoEnv/juvix.yaml b/tests/positive/MiniC/ClosureNoEnv/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/ExportName/Input.juvix b/tests/positive/MiniC/ExportName/Input.juvix deleted file mode 100644 index 259fb474ac..0000000000 --- a/tests/positive/MiniC/ExportName/Input.juvix +++ /dev/null @@ -1,8 +0,0 @@ -module Input; - -open import Stdlib.Prelude; - -fun : Nat; -fun := 6; - -end; diff --git a/tests/positive/MiniC/ExportName/expected.golden b/tests/positive/MiniC/ExportName/expected.golden deleted file mode 100644 index 1e8b314962..0000000000 --- a/tests/positive/MiniC/ExportName/expected.golden +++ /dev/null @@ -1 +0,0 @@ -6 diff --git a/tests/positive/MiniC/ExportName/juvix.yaml b/tests/positive/MiniC/ExportName/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/ExportNameArgs/Input.juvix b/tests/positive/MiniC/ExportNameArgs/Input.juvix deleted file mode 100644 index aed00f7934..0000000000 --- a/tests/positive/MiniC/ExportNameArgs/Input.juvix +++ /dev/null @@ -1,8 +0,0 @@ -module Input; - -open import Stdlib.Prelude; - -fun : Nat → Nat; -fun _ := 3; - -end; diff --git a/tests/positive/MiniC/ExportNameArgs/expected.golden b/tests/positive/MiniC/ExportNameArgs/expected.golden deleted file mode 100644 index 00750edc07..0000000000 --- a/tests/positive/MiniC/ExportNameArgs/expected.golden +++ /dev/null @@ -1 +0,0 @@ -3 diff --git a/tests/positive/MiniC/ExportNameArgs/juvix.yaml b/tests/positive/MiniC/ExportNameArgs/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/HelloWorld/Input.juvix b/tests/positive/MiniC/HelloWorld/Input.juvix deleted file mode 100644 index 623b4bbb1b..0000000000 --- a/tests/positive/MiniC/HelloWorld/Input.juvix +++ /dev/null @@ -1,25 +0,0 @@ -module Input; - -builtin string axiom String : Type; - -compile String { - c ↦ "char*"; -}; - -axiom Action : Type; - -compile Action { - c ↦ "int"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - ghc ↦ "putStrLn"; - c ↦ "putStrLn"; -}; - -main : Action; -main := put-str-ln "hello world!"; - -end; diff --git a/tests/positive/MiniC/HelloWorld/expected.golden b/tests/positive/MiniC/HelloWorld/expected.golden deleted file mode 100644 index a042389697..0000000000 --- a/tests/positive/MiniC/HelloWorld/expected.golden +++ /dev/null @@ -1 +0,0 @@ -hello world! diff --git a/tests/positive/MiniC/HelloWorld/juvix.yaml b/tests/positive/MiniC/HelloWorld/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/HigherOrder/Input.juvix b/tests/positive/MiniC/HigherOrder/Input.juvix deleted file mode 100644 index 0b032571de..0000000000 --- a/tests/positive/MiniC/HigherOrder/Input.juvix +++ /dev/null @@ -1,142 +0,0 @@ -module Input; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -builtin string axiom String : Type; - -compile String { - c ↦ "char*"; -}; - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; - -compile Action { - c ↦ "int"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; - -compile >> { - c ↦ "sequence"; -}; - -axiom put-str : String → Action; - -compile put-str { - c ↦ "putStr"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - c ↦ "putStrLn"; -}; - --------------------------------------------------------------------------------- --- Integers --------------------------------------------------------------------------------- - -axiom Int : Type; - -compile Int { - c ↦ "int"; -}; - -axiom Int_0 : Int; -compile Int_0 { - c ↦ "0"; -}; - -axiom Int_1 : Int; -compile Int_1 { - c ↦ "1"; -}; - -foreign c { - int plus(int l, int r) { - return l + r; - \} -}; - -infixl 6 +int; -axiom +int : Int -> Int -> Int; - -compile +int { - ghc ↦ "(+)"; - c ↦ "plus"; -}; - -axiom to-str : Int → String; - -compile to-str { - c ↦ "intToStr"; -}; - --------------------------------------------------------------------------------- --- Natural Numbers --------------------------------------------------------------------------------- - -type Nat := - zero : Nat - | suc : Nat → Nat; - -infixl 6 +; -+ : Nat → Nat → Nat; -+ zero n := n; -+ (suc m) n := suc (m + n); - -to-int : Nat → Int; -to-int zero := Int_0; -to-int (suc n) := Int_1 +int (to-int n); - -nat-to-str : Nat → String; -nat-to-str n := to-str (to-int n); - -one : Nat; -one := suc zero; - -two : Nat; -two := suc one; - -three : Nat; -three := suc two; - --------------------------------------------------------------------------------- --- Lists --------------------------------------------------------------------------------- - -type ListNat := - null : ListNat | - cons : Nat → ListNat → ListNat; - -foldl : (Nat → Nat → Nat) → Nat → ListNat → Nat; -foldl _ z null := z; -foldl f z (cons n hs) := foldl f (f z n) hs; - -l : ListNat; -l := cons one (cons two null); - -sum : ListNat → Nat; -sum l := foldl (+) zero l; - -sum-is-three : Action; -sum-is-three := put-str "list sum is: " - >> put-str-ln (nat-to-str (sum l)); - -main : Action; -main := sum-is-three - -end; diff --git a/tests/positive/MiniC/HigherOrder/expected.golden b/tests/positive/MiniC/HigherOrder/expected.golden deleted file mode 100644 index 2c23c1eccc..0000000000 --- a/tests/positive/MiniC/HigherOrder/expected.golden +++ /dev/null @@ -1 +0,0 @@ -list sum is: 3 diff --git a/tests/positive/MiniC/HigherOrder/juvix.yaml b/tests/positive/MiniC/HigherOrder/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/ImportExportName/Input.juvix b/tests/positive/MiniC/ImportExportName/Input.juvix deleted file mode 100644 index 6b5ab0beae..0000000000 --- a/tests/positive/MiniC/ImportExportName/Input.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module Input; - -open import Stdlib.Prelude; - -axiom hostDisplayString : String → IO; - -juvixRender : IO; -juvixRender := hostDisplayString "Hello World from Juvix!"; - -end; diff --git a/tests/positive/MiniC/ImportExportName/expected.golden b/tests/positive/MiniC/ImportExportName/expected.golden deleted file mode 100644 index 66283ea681..0000000000 --- a/tests/positive/MiniC/ImportExportName/expected.golden +++ /dev/null @@ -1 +0,0 @@ -Hello World from Juvix! diff --git a/tests/positive/MiniC/ImportExportName/input.js b/tests/positive/MiniC/ImportExportName/input.js deleted file mode 100644 index f0c3157fd0..0000000000 --- a/tests/positive/MiniC/ImportExportName/input.js +++ /dev/null @@ -1,35 +0,0 @@ -const fs = require('fs'); - -let wasmModule = null; - -function cstrlen(mem, ptr) { - let len = 0; - while (mem[ptr] != 0) { - len++; - ptr++; - } - return len; -} - -function ptrToCstr(ptr) { - const wasmMemory = wasmModule.instance.exports.memory.buffer; - const mem = new Uint8Array(wasmMemory); - const len = cstrlen(mem, ptr); - const bytes = new Uint8Array(wasmMemory, ptr, len); - return new TextDecoder().decode(bytes); -} - -function hostDisplayString(strPtr) { - const text = ptrToCstr(strPtr); - console.log(text); -} - -const wasmBuffer = fs.readFileSync("Input.wasm"); -WebAssembly.instantiate(wasmBuffer, { - env: { - hostDisplayString, - } -}).then((w) => { - wasmModule = w; - wasmModule.instance.exports.juvixRender(); -}); diff --git a/tests/positive/MiniC/ImportExportName/juvix.yaml b/tests/positive/MiniC/ImportExportName/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/Lib/Data/Bool.juvix b/tests/positive/MiniC/Lib/Data/Bool.juvix deleted file mode 100644 index 77a5fec3bb..0000000000 --- a/tests/positive/MiniC/Lib/Data/Bool.juvix +++ /dev/null @@ -1,17 +0,0 @@ -module Data.Bool; - -open import Data.String; - -type Bool := - true : Bool - | false : Bool; - -not : Bool → Bool; -not true := false; -not false := true; - -boolToStr : Bool → String; -boolToStr true := "true"; -boolToStr false := "false"; - -end; diff --git a/tests/positive/MiniC/Lib/Data/IO.juvix b/tests/positive/MiniC/Lib/Data/IO.juvix deleted file mode 100644 index c4d5372731..0000000000 --- a/tests/positive/MiniC/Lib/Data/IO.juvix +++ /dev/null @@ -1,41 +0,0 @@ -module Data.IO; - -import Data.String; -open Data.String; - -axiom Action : Type; - -compile Action { - ghc ↦ "IO ()"; - c ↦ "int"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; - -compile >> { - ghc ↦ "(>>)"; - c ↦ "sequence"; -}; - -axiom put-str : String → Action; - -compile put-str { - ghc ↦ "putStr"; - c ↦ "putStr"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - ghc ↦ "putStrLn"; - c ↦ "putStrLn"; -}; - -end; diff --git a/tests/positive/MiniC/Lib/Data/Int.juvix b/tests/positive/MiniC/Lib/Data/Int.juvix deleted file mode 100644 index 91becf5eda..0000000000 --- a/tests/positive/MiniC/Lib/Data/Int.juvix +++ /dev/null @@ -1,28 +0,0 @@ -module Data.Int; - -open import Data.String; - -axiom Int : Type; -compile Int { - c ↦ "int"; -}; - -axiom intToStr : Int → String; - -compile intToStr { - c ↦ "intToStr"; -}; - -foreign c { - int plus(int l, int r) { - return l + r; - \} -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - c ↦ "plus"; -}; - -end; diff --git a/tests/positive/MiniC/Lib/Data/Nat.juvix b/tests/positive/MiniC/Lib/Data/Nat.juvix deleted file mode 100644 index 538f0d0310..0000000000 --- a/tests/positive/MiniC/Lib/Data/Nat.juvix +++ /dev/null @@ -1,33 +0,0 @@ -module Data.Nat; - -open import Data.String; -open import Data.Int; - -type Nat := - zero : Nat - | suc : Nat → Nat; - -foreign c { - void* natInd(int n, void* zeroCtor, juvix_function_t* sucCtor) { - if (n <= 0) return zeroCtor; - return ((void* (*) (juvix_function_t*, void*))sucCtor->fun)(sucCtor, natInd(n - 1, zeroCtor, sucCtor)); - \} -}; - -axiom natInd : Int → Nat → (Nat → Nat) → Nat; - -compile natInd { - c ↦ "natInd"; -}; - -natToInt : Nat → Int; -natToInt zero := 0; -natToInt (suc n) := 1 + (natToInt n); - -natToStr : Nat → String; -natToStr n := intToStr (natToInt n); - -intToNat : Int → Nat; -intToNat x := natInd x zero suc; - -end; diff --git a/tests/positive/MiniC/Lib/Data/Pair.juvix b/tests/positive/MiniC/Lib/Data/Pair.juvix deleted file mode 100644 index ecb48dca1f..0000000000 --- a/tests/positive/MiniC/Lib/Data/Pair.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module Data.Pair; - -type Pair (A : Type) (B : Type) := - mkPair : A → B → Pair A B; - -fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) := a; - - -end; diff --git a/tests/positive/MiniC/Lib/Data/String.juvix b/tests/positive/MiniC/Lib/Data/String.juvix deleted file mode 100644 index 3c50dcac21..0000000000 --- a/tests/positive/MiniC/Lib/Data/String.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module Data.String; - -builtin string axiom String : Type; - -compile String { - ghc ↦ "[Char]"; - c ↦ "char*"; -}; - -end; diff --git a/tests/positive/MiniC/Lib/Prelude.juvix b/tests/positive/MiniC/Lib/Prelude.juvix deleted file mode 100644 index 17f55c867e..0000000000 --- a/tests/positive/MiniC/Lib/Prelude.juvix +++ /dev/null @@ -1,15 +0,0 @@ -module Prelude; - -open import Data.String public; - -open import Data.Bool public; - -open import Data.Int public; - -open import Data.Pair public; - -open import Data.IO public; - -open import Data.Nat public; - -end; diff --git a/tests/positive/MiniC/Lib/minijuvix.yaml b/tests/positive/MiniC/Lib/minijuvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/MultiModules/Data/Bool.juvix b/tests/positive/MiniC/MultiModules/Data/Bool.juvix deleted file mode 100644 index 77a5fec3bb..0000000000 --- a/tests/positive/MiniC/MultiModules/Data/Bool.juvix +++ /dev/null @@ -1,17 +0,0 @@ -module Data.Bool; - -open import Data.String; - -type Bool := - true : Bool - | false : Bool; - -not : Bool → Bool; -not true := false; -not false := true; - -boolToStr : Bool → String; -boolToStr true := "true"; -boolToStr false := "false"; - -end; diff --git a/tests/positive/MiniC/MultiModules/Data/IO.juvix b/tests/positive/MiniC/MultiModules/Data/IO.juvix deleted file mode 100644 index c4d5372731..0000000000 --- a/tests/positive/MiniC/MultiModules/Data/IO.juvix +++ /dev/null @@ -1,41 +0,0 @@ -module Data.IO; - -import Data.String; -open Data.String; - -axiom Action : Type; - -compile Action { - ghc ↦ "IO ()"; - c ↦ "int"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; - -compile >> { - ghc ↦ "(>>)"; - c ↦ "sequence"; -}; - -axiom put-str : String → Action; - -compile put-str { - ghc ↦ "putStr"; - c ↦ "putStr"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - ghc ↦ "putStrLn"; - c ↦ "putStrLn"; -}; - -end; diff --git a/tests/positive/MiniC/MultiModules/Data/Int.juvix b/tests/positive/MiniC/MultiModules/Data/Int.juvix deleted file mode 100644 index 1675b33978..0000000000 --- a/tests/positive/MiniC/MultiModules/Data/Int.juvix +++ /dev/null @@ -1,38 +0,0 @@ -module Data.Int; - -open import Data.String; - -axiom Int : Type; -compile Int { - c ↦ "int"; -}; - -axiom Int_0 : Int; -compile Int_0 { - c ↦ "0"; -}; - -axiom Int_1 : Int; -compile Int_1 { - c ↦ "1"; -}; - -axiom intToStr : Int → String; - -compile intToStr { - c ↦ "intToStr"; -}; - -foreign c { - int plus(int l, int r) { - return l + r; - \} -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - c ↦ "plus"; -}; - -end; diff --git a/tests/positive/MiniC/MultiModules/Data/Nat.juvix b/tests/positive/MiniC/MultiModules/Data/Nat.juvix deleted file mode 100644 index f7135d2a97..0000000000 --- a/tests/positive/MiniC/MultiModules/Data/Nat.juvix +++ /dev/null @@ -1,33 +0,0 @@ -module Data.Nat; - -open import Data.String; -open import Data.Int; - -type Nat := - zero : Nat - | suc : Nat → Nat; - -foreign c { - void* natInd(int n, void* zeroCtor, juvix_function_t* sucCtor) { - if (n <= 0) return zeroCtor; - return ((void* (*) (juvix_function_t*, void*))sucCtor->fun)(sucCtor, natInd(n - 1, zeroCtor, sucCtor)); - \} -}; - -axiom natInd : Int → Nat → (Nat → Nat) → Nat; - -compile natInd { - c ↦ "natInd"; -}; - -natToInt : Nat → Int; -natToInt zero := Int_0; -natToInt (suc n) := Int_1 + (natToInt n); - -natToStr : Nat → String; -natToStr n := intToStr (natToInt n); - -intToNat : Int → Nat; -intToNat x := natInd x zero suc; - -end; diff --git a/tests/positive/MiniC/MultiModules/Data/Pair.juvix b/tests/positive/MiniC/MultiModules/Data/Pair.juvix deleted file mode 100644 index ecb48dca1f..0000000000 --- a/tests/positive/MiniC/MultiModules/Data/Pair.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module Data.Pair; - -type Pair (A : Type) (B : Type) := - mkPair : A → B → Pair A B; - -fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) := a; - - -end; diff --git a/tests/positive/MiniC/MultiModules/Data/String.juvix b/tests/positive/MiniC/MultiModules/Data/String.juvix deleted file mode 100644 index 3c50dcac21..0000000000 --- a/tests/positive/MiniC/MultiModules/Data/String.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module Data.String; - -builtin string axiom String : Type; - -compile String { - ghc ↦ "[Char]"; - c ↦ "char*"; -}; - -end; diff --git a/tests/positive/MiniC/MultiModules/Input.juvix b/tests/positive/MiniC/MultiModules/Input.juvix deleted file mode 100644 index f6b90c606c..0000000000 --- a/tests/positive/MiniC/MultiModules/Input.juvix +++ /dev/null @@ -1,29 +0,0 @@ -module Input; - -open import Data.String; - -open import Data.Bool; - -open import Data.Pair; - -open import Data.IO; - --- Not needed but useful for testing -open import Prelude; - -bool-to-str : Bool → String; -bool-to-str true := "True"; -bool-to-str false := "False"; - --------------------------------------------------------------------------------- --- Main --------------------------------------------------------------------------------- - -fst-of-pair : Action; -fst-of-pair := (put-str "fst (True, False) = ") - >> put-str-ln (bool-to-str (fst Bool Bool (mkPair true false))); - -main : Action; -main := fst-of-pair; - -end; diff --git a/tests/positive/MiniC/MultiModules/Prelude.juvix b/tests/positive/MiniC/MultiModules/Prelude.juvix deleted file mode 100644 index 17f55c867e..0000000000 --- a/tests/positive/MiniC/MultiModules/Prelude.juvix +++ /dev/null @@ -1,15 +0,0 @@ -module Prelude; - -open import Data.String public; - -open import Data.Bool public; - -open import Data.Int public; - -open import Data.Pair public; - -open import Data.IO public; - -open import Data.Nat public; - -end; diff --git a/tests/positive/MiniC/MultiModules/expected.golden b/tests/positive/MiniC/MultiModules/expected.golden deleted file mode 100644 index 9ec6158aa2..0000000000 --- a/tests/positive/MiniC/MultiModules/expected.golden +++ /dev/null @@ -1 +0,0 @@ -fst (True, False) = True diff --git a/tests/positive/MiniC/MultiModules/juvix.yaml b/tests/positive/MiniC/MultiModules/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix deleted file mode 100644 index 77a5fec3bb..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Data/Bool.juvix +++ /dev/null @@ -1,17 +0,0 @@ -module Data.Bool; - -open import Data.String; - -type Bool := - true : Bool - | false : Bool; - -not : Bool → Bool; -not true := false; -not false := true; - -boolToStr : Bool → String; -boolToStr true := "true"; -boolToStr false := "false"; - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/IO.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/IO.juvix deleted file mode 100644 index c4d5372731..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Data/IO.juvix +++ /dev/null @@ -1,41 +0,0 @@ -module Data.IO; - -import Data.String; -open Data.String; - -axiom Action : Type; - -compile Action { - ghc ↦ "IO ()"; - c ↦ "int"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; - -compile >> { - ghc ↦ "(>>)"; - c ↦ "sequence"; -}; - -axiom put-str : String → Action; - -compile put-str { - ghc ↦ "putStr"; - c ↦ "putStr"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - ghc ↦ "putStrLn"; - c ↦ "putStrLn"; -}; - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix deleted file mode 100644 index 7d7774cebf..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Data/Int.juvix +++ /dev/null @@ -1,49 +0,0 @@ -module Data.Int; - -open import Data.String; - -axiom Int : Type; -compile Int { - c ↦ "int"; -}; - -axiom Int_0 : Int; -compile Int_0 { - c ↦ "0"; -}; - -axiom Int_1 : Int; -compile Int_1 { - c ↦ "1"; -}; - -axiom Int_4 : Int; -compile Int_4 { - c ↦ "4"; -}; - - -axiom Int_9 : Int; -compile Int_9 { - c ↦ "9"; -}; - -axiom intToStr : Int → String; - -compile intToStr { - c ↦ "intToStr"; -}; - -foreign c { - int plus(int l, int r) { - return l + r; - \} -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - c ↦ "plus"; -}; - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix deleted file mode 100644 index f7135d2a97..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Data/Nat.juvix +++ /dev/null @@ -1,33 +0,0 @@ -module Data.Nat; - -open import Data.String; -open import Data.Int; - -type Nat := - zero : Nat - | suc : Nat → Nat; - -foreign c { - void* natInd(int n, void* zeroCtor, juvix_function_t* sucCtor) { - if (n <= 0) return zeroCtor; - return ((void* (*) (juvix_function_t*, void*))sucCtor->fun)(sucCtor, natInd(n - 1, zeroCtor, sucCtor)); - \} -}; - -axiom natInd : Int → Nat → (Nat → Nat) → Nat; - -compile natInd { - c ↦ "natInd"; -}; - -natToInt : Nat → Int; -natToInt zero := Int_0; -natToInt (suc n) := Int_1 + (natToInt n); - -natToStr : Nat → String; -natToStr n := intToStr (natToInt n); - -intToNat : Int → Nat; -intToNat x := natInd x zero suc; - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix deleted file mode 100644 index ecb48dca1f..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Data/Pair.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module Data.Pair; - -type Pair (A : Type) (B : Type) := - mkPair : A → B → Pair A B; - -fst : (A : Type) → (B : Type) → Pair A B → A; -fst _ _ (mkPair a b) := a; - - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Data/String.juvix b/tests/positive/MiniC/MutuallyRecursive/Data/String.juvix deleted file mode 100644 index 3c50dcac21..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Data/String.juvix +++ /dev/null @@ -1,10 +0,0 @@ -module Data.String; - -builtin string axiom String : Type; - -compile String { - ghc ↦ "[Char]"; - c ↦ "char*"; -}; - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Input.juvix b/tests/positive/MiniC/MutuallyRecursive/Input.juvix deleted file mode 100644 index 2598611231..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Input.juvix +++ /dev/null @@ -1,32 +0,0 @@ -module Input; - -open import Prelude; - -odd : Nat → Bool; - -even : Nat → Bool; - -odd zero := false; -odd (suc n) := even n; - -even zero := true; -even (suc n) := odd n; - -check : (Nat → Bool) → Int → String; -check f x := boolToStr (f (intToNat x)); - -checkEven : Int → String; -checkEven := check even; - -checkOdd : Int → String; -checkOdd := check odd; - -main : Action; -main := put-str "even 1: " >> put-str-ln (checkEven Int_1) - >> put-str "even 4: " >> put-str-ln (checkEven Int_4) - >> put-str "even 9: " >> put-str-ln (checkEven Int_9) - >> put-str "odd 1: " >> put-str-ln (checkOdd Int_1) - >> put-str "odd 4: " >> put-str-ln (checkOdd Int_4) - >> put-str "odd 9: " >> put-str-ln (checkOdd Int_9) - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/Prelude.juvix b/tests/positive/MiniC/MutuallyRecursive/Prelude.juvix deleted file mode 100644 index 17f55c867e..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/Prelude.juvix +++ /dev/null @@ -1,15 +0,0 @@ -module Prelude; - -open import Data.String public; - -open import Data.Bool public; - -open import Data.Int public; - -open import Data.Pair public; - -open import Data.IO public; - -open import Data.Nat public; - -end; diff --git a/tests/positive/MiniC/MutuallyRecursive/expected.golden b/tests/positive/MiniC/MutuallyRecursive/expected.golden deleted file mode 100644 index 0394cc0413..0000000000 --- a/tests/positive/MiniC/MutuallyRecursive/expected.golden +++ /dev/null @@ -1,6 +0,0 @@ -even 1: false -even 4: true -even 9: false -odd 1: true -odd 4: false -odd 9: true diff --git a/tests/positive/MiniC/MutuallyRecursive/juvix.yaml b/tests/positive/MiniC/MutuallyRecursive/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/Nat/Input.juvix b/tests/positive/MiniC/Nat/Input.juvix deleted file mode 100644 index 87d8a06708..0000000000 --- a/tests/positive/MiniC/Nat/Input.juvix +++ /dev/null @@ -1,177 +0,0 @@ -module Input; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -type Bool := - true : Bool - | false : Bool; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -builtin string axiom String : Type; - -compile String { - ghc ↦ "[Char]"; - c ↦ "char*"; -}; - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; - -compile Action { - ghc ↦ "IO ()"; - c ↦ "int"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; - -compile >> { - ghc ↦ "(>>)"; - c ↦ "sequence"; -}; - -axiom put-str : String → Action; - -compile put-str { - ghc ↦ "putStr"; - c ↦ "putStr"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - ghc ↦ "putStrLn"; - c ↦ "putStrLn"; -}; - -bool-to-str : Bool → String; -bool-to-str true := "True"; -bool-to-str false := "False"; - --------------------------------------------------------------------------------- --- Integers --------------------------------------------------------------------------------- - -axiom Int : Type; -compile Int { - ghc ↦ "Int"; - c ↦ "int"; -}; - -axiom Int_0 : Int; -compile Int_0 { - c ↦ "0"; -}; - -axiom Int_1 : Int; -compile Int_1 { - c ↦ "1"; -}; - -foreign c { - int plus(int l, int r) { - return l + r; - \} -}; - -infixl 6 +int; -axiom +int : Int -> Int -> Int; - -compile +int { - ghc ↦ "(+)"; - c ↦ "plus"; -}; - -axiom to-str : Int → String; - -compile to-str { - ghc ↦ "show"; - c ↦ "intToStr"; -}; - --------------------------------------------------------------------------------- --- Natural Numbers --------------------------------------------------------------------------------- - -type Nat := - zero : Nat - | suc : Nat → Nat; - -infixl 6 +; -+ : Nat → Nat → Nat; -+ zero n := n; -+ (suc m) n := suc (m + n); - -is-even : Nat → Bool; -is-even zero := true; -is-even (suc (suc n)) := is-even n; -is-even _ := false; - -infix 4 ==Nat; -==Nat : Nat → Nat → Bool; -==Nat zero zero := true; -==Nat (suc n) (suc m) := n ==Nat m; -==Nat _ _ := false; - -to-int : Nat → Int; -to-int zero := Int_0; -to-int (suc n) := Int_1 +int (to-int n); - -nat-to-str : Nat → String; -nat-to-str n := to-str (to-int n); - -one : Nat; -one := suc zero; - -two : Nat; -two := suc one; - -three : Nat; -three := suc two; - --------------------------------------------------------------------------------- --- Main --------------------------------------------------------------------------------- - -three-plus-suc-one : Action; -three-plus-suc-one := (put-str "3 + (1 + 1) = ") - >> put-str-ln (nat-to-str (three + (suc one))); - -three-eq-suc-two : Action; -three-eq-suc-two := (put-str "3 == 1 + 2 : ") - >> put-str-ln (bool-to-str (three ==Nat (one + two))); - -three-neq-two : Action; -three-neq-two := (put-str "3 == 2 : ") - >> put-str-ln (bool-to-str (three ==Nat two)); - -three-is-not-even : Action; -three-is-not-even := (put-str "is-even 3 : ") - >> put-str-ln (bool-to-str (is-even three)); - -four-is-even : Action; -four-is-even := (put-str "is-even 4 : ") - >> put-str-ln (bool-to-str (is-even (suc three))); - -main : Action; -main := three-plus-suc-one - >> three-eq-suc-two - >> three-neq-two - >> three-is-not-even - >> four-is-even - -end; diff --git a/tests/positive/MiniC/Nat/expected.golden b/tests/positive/MiniC/Nat/expected.golden deleted file mode 100644 index 3af5a49eef..0000000000 --- a/tests/positive/MiniC/Nat/expected.golden +++ /dev/null @@ -1,5 +0,0 @@ -3 + (1 + 1) = 5 -3 == 1 + 2 : True -3 == 2 : False -is-even 3 : False -is-even 4 : True diff --git a/tests/positive/MiniC/Nat/juvix.yaml b/tests/positive/MiniC/Nat/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/NestedList/Data b/tests/positive/MiniC/NestedList/Data deleted file mode 120000 index 6e2a68d952..0000000000 --- a/tests/positive/MiniC/NestedList/Data +++ /dev/null @@ -1 +0,0 @@ -../Lib/Data \ No newline at end of file diff --git a/tests/positive/MiniC/NestedList/Input.juvix b/tests/positive/MiniC/NestedList/Input.juvix deleted file mode 100644 index 9d10a66bcb..0000000000 --- a/tests/positive/MiniC/NestedList/Input.juvix +++ /dev/null @@ -1,19 +0,0 @@ -module Input; - -open import Data.IO; - -infixr 5 ::; -type List (A : Type) := - nil : List A - | :: : A → List A → List A; - -type Foo := - a : Foo; - -l : List (List Foo) → List (List Foo); -l ((_ :: nil) :: nil) := nil :: nil; - -main : Action; -main := put-str-ln "no errors"; - -end; diff --git a/tests/positive/MiniC/NestedList/Prelude.mjuvix b/tests/positive/MiniC/NestedList/Prelude.mjuvix deleted file mode 120000 index 8fde4860a9..0000000000 --- a/tests/positive/MiniC/NestedList/Prelude.mjuvix +++ /dev/null @@ -1 +0,0 @@ -../Lib/Prelude.mjuvix \ No newline at end of file diff --git a/tests/positive/MiniC/NestedList/expected.golden b/tests/positive/MiniC/NestedList/expected.golden deleted file mode 100644 index 481748b612..0000000000 --- a/tests/positive/MiniC/NestedList/expected.golden +++ /dev/null @@ -1 +0,0 @@ -no errors diff --git a/tests/positive/MiniC/NestedList/juvix.yaml b/tests/positive/MiniC/NestedList/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/PolymorphicAxioms/Input.juvix b/tests/positive/MiniC/PolymorphicAxioms/Input.juvix deleted file mode 100644 index 99ac159e85..0000000000 --- a/tests/positive/MiniC/PolymorphicAxioms/Input.juvix +++ /dev/null @@ -1,25 +0,0 @@ -module Input; - -type Unit := - unit : Unit; - -axiom Action : Type; - -compile Action { - c ↦ "int"; -}; - -axiom ignore : {A : Type} -> A -> Action; - -compile ignore { - c ↦ "ignore"; -}; - -foreign c { - static int ignore(uintptr_t ptr) { return 0; \} -}; - -main : Action; -main := ignore unit; - -end; diff --git a/tests/positive/MiniC/PolymorphicAxioms/expected.golden b/tests/positive/MiniC/PolymorphicAxioms/expected.golden deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/PolymorphicAxioms/juvix.yaml b/tests/positive/MiniC/PolymorphicAxioms/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/PolymorphicTarget/Input.juvix b/tests/positive/MiniC/PolymorphicTarget/Input.juvix deleted file mode 100644 index 1bc2814c1e..0000000000 --- a/tests/positive/MiniC/PolymorphicTarget/Input.juvix +++ /dev/null @@ -1,30 +0,0 @@ -module Input; - -type Unit := - unit : Unit; - -terminating -loop : {A : Type} -> A; -loop := loop; - -const : {A : Type} -> A -> A -> A; -const x y := x; - -fail : Unit; -fail := const unit loop; - -axiom Action : Type; - -compile Action { - c ↦ "int"; -}; - -axiom Int_0 : Action; -compile Int_0 { - c ↦ "0"; -}; - -main : Action; -main := Int_0; - -end; diff --git a/tests/positive/MiniC/PolymorphicTarget/expected.golden b/tests/positive/MiniC/PolymorphicTarget/expected.golden deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/PolymorphicTarget/juvix.yaml b/tests/positive/MiniC/PolymorphicTarget/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/Polymorphism/Input.juvix b/tests/positive/MiniC/Polymorphism/Input.juvix deleted file mode 100644 index 567f701bb3..0000000000 --- a/tests/positive/MiniC/Polymorphism/Input.juvix +++ /dev/null @@ -1,87 +0,0 @@ -module Input; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -type Bool := - true : Bool - | false : Bool; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -builtin string axiom String : Type; - -compile String { - ghc ↦ "[Char]"; - c ↦ "char*"; -}; - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; - -compile Action { - ghc ↦ "IO ()"; - c ↦ "int"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; - -compile >> { - ghc ↦ "(>>)"; - c ↦ "sequence"; -}; - -axiom put-str : String → Action; - -compile put-str { - ghc ↦ "putStr"; - c ↦ "putStr"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - ghc ↦ "putStrLn"; - c ↦ "putStrLn"; -}; - -bool-to-str : Bool → String; -bool-to-str true := "True"; -bool-to-str false := "False"; - -infixr 2 ×; -infixr 4 ,; -type × (A : Type) (B : Type) := - , : A → B → A × B; - -fst : {A : Type} → {B : Type} → A × B → A; -fst (a, b) := a; - -id' : {A : Type} → A → A; -id' a := fst (a, a); - --------------------------------------------------------------------------------- --- Main --------------------------------------------------------------------------------- - -fst-of-pair : Action; -fst-of-pair := (put-str "fst (True, False) = ") - >> put-str-ln (bool-to-str (fst (true, false))); - -main : Action; -main := fst-of-pair >> put-str-ln (bool-to-str (id' false)); - -end; diff --git a/tests/positive/MiniC/Polymorphism/expected.golden b/tests/positive/MiniC/Polymorphism/expected.golden deleted file mode 100644 index 1dcc250891..0000000000 --- a/tests/positive/MiniC/Polymorphism/expected.golden +++ /dev/null @@ -1,2 +0,0 @@ -fst (True, False) = True -False diff --git a/tests/positive/MiniC/Polymorphism/juvix.yaml b/tests/positive/MiniC/Polymorphism/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/PolymorphismHoles/Input.juvix b/tests/positive/MiniC/PolymorphismHoles/Input.juvix deleted file mode 100644 index 00b3edaaeb..0000000000 --- a/tests/positive/MiniC/PolymorphismHoles/Input.juvix +++ /dev/null @@ -1,87 +0,0 @@ -module Input; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -type Bool := - true : Bool - | false : Bool; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -builtin string axiom String : Type; - -compile String { - ghc ↦ "[Char]"; - c ↦ "char*"; -}; - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; - -compile Action { - ghc ↦ "IO ()"; - c ↦ "int"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; - -compile >> { - ghc ↦ "(>>)"; - c ↦ "sequence"; -}; - -axiom put-str : String → Action; - -compile put-str { - ghc ↦ "putStr"; - c ↦ "putStr"; -}; - -axiom put-str-ln : String → Action; - -compile put-str-ln { - ghc ↦ "putStrLn"; - c ↦ "putStrLn"; -}; - -bool-to-str : Bool → String; -bool-to-str true := "True"; -bool-to-str false := "False"; - - --------------------------------------------------------------------------------- --- Pair --------------------------------------------------------------------------------- - -type Pair (A : Type) (B : Type) := - mkPair : A → B → Pair A B; - -fst : {A : Type} → {B : Type} → Pair A B → A; -fst (mkPair a b) := a; - --------------------------------------------------------------------------------- --- Main --------------------------------------------------------------------------------- - -fst-of-pair : Action; -fst-of-pair := (put-str "fst (True, False) = ") - >> put-str-ln (bool-to-str (fst (mkPair true false))); - -main : Action; -main := fst-of-pair; - -end; diff --git a/tests/positive/MiniC/PolymorphismHoles/expected.golden b/tests/positive/MiniC/PolymorphismHoles/expected.golden deleted file mode 100644 index 9ec6158aa2..0000000000 --- a/tests/positive/MiniC/PolymorphismHoles/expected.golden +++ /dev/null @@ -1 +0,0 @@ -fst (True, False) = True diff --git a/tests/positive/MiniC/PolymorphismHoles/juvix.yaml b/tests/positive/MiniC/PolymorphismHoles/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix b/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix deleted file mode 100644 index fc4b1fd5d1..0000000000 --- a/tests/positive/MiniC/SimpleFungibleTokenImplicit/Input.juvix +++ /dev/null @@ -1,359 +0,0 @@ -module Input; - -foreign c { - int readPre(const char *key) { - if (strcmp("change1-key", key)) { - return 100; - \} else if (strcmp("change2-key", key)) { - return 90; - \} else { - return -1; - \} - \} - - int readPost(const char *key) { - if (strcmp("change1-key", key)) { - return 90; - \} else if (strcmp("change2-key", key)) { - return 100; - \} else { - return -1; - \} - \} - - char* isBalanceKey(const char* s1, const char* s2) { - return "owner-address"; - \} -}; - --------------------------------------------------------------------------------- --- Booleans --------------------------------------------------------------------------------- - -type Bool := - true : Bool - | false : Bool; - -infixr 2 ||; -|| : Bool → Bool → Bool; -|| false a := a; -|| true _ := true; - -infixr 3 &&; -&& : Bool → Bool → Bool; -&& false _ := false; -&& true a := a; - -if : {A : Type} → Bool → A → A → A; -if true a _ := a; -if false _ b := b; - --------------------------------------------------------------------------------- --- Backend Booleans --------------------------------------------------------------------------------- - -axiom BackendBool : Type; -compile BackendBool { - c ↦ "bool"; -}; - -axiom backend-true : BackendBool; -compile backend-true { - c ↦ "true"; -}; - -axiom backend-false : BackendBool; -compile backend-false { - c ↦ "false"; -}; - --------------------------------------------------------------------------------- --- Backend Bridge --------------------------------------------------------------------------------- - -foreign c { - void* boolInd(bool b, void* a1, void* a2) { - return b ? a1 : a2; - \} -}; - -axiom bool : BackendBool → Bool → Bool → Bool; -compile bool { - c ↦ "boolInd"; -}; - -from-backend-bool : BackendBool → Bool; -from-backend-bool bb := bool bb true false; - --------------------------------------------------------------------------------- --- Functions --------------------------------------------------------------------------------- - -id : {A : Type} → A → A; -id a := a; - --------------------------------------------------------------------------------- --- Integers --------------------------------------------------------------------------------- - -axiom Int : Type; -axiom Int_0 : Int; - -compile Int { - c ↦ "int"; -}; - -compile Int_0 { - c ↦ "0"; -}; - -foreign c { - bool lessThan(int l, int r) { - return l < r; - \} - - bool eqInt(int l, int r) { - return l == r; - \} - - int plus(int l, int r) { - return l + r; - \} - - int minus(int l, int r) { - return l - r; - \} -}; - -infix 4 <'; -axiom <' : Int → Int → BackendBool; -compile <' { - c ↦ "lessThan"; -}; - -infix 4 <; -< : Int → Int → Bool; -< i1 i2 := from-backend-bool (i1 <' i2); - -isNegative : Int → Bool; -isNegative n := n < Int_0; - -axiom eqInt : Int → Int → BackendBool; -compile eqInt { - c ↦ "eqInt"; -}; - -infix 4 ==Int; -==Int : Int → Int → Bool; -==Int i1 i2 := from-backend-bool (eqInt i1 i2); - -infixl 6 -; -axiom - : Int -> Int -> Int; -compile - { - c ↦ "minus"; -}; - -infixl 6 +; -axiom + : Int -> Int -> Int; -compile + { - c ↦ "plus"; -}; - --------------------------------------------------------------------------------- --- Strings --------------------------------------------------------------------------------- - -builtin string axiom String : Type; -compile String { - c ↦ "char*"; -}; - -foreign c { - bool eqString(char* l, char* r) { - return strcmp(l, r) == 0; - \} -}; - -axiom eqString : String → String → BackendBool; -compile eqString { - c ↦ "eqString"; -}; - -infix 4 ==String; -==String : String → String → Bool; -==String s1 s2 := from-backend-bool (eqString s1 s2); - --------------------------------------------------------------------------------- --- Lists --------------------------------------------------------------------------------- - -infixr 5 ::; -type List (A : Type) := - nil : List A - | :: : A → List A → List A; - -elem : {A : Type} → (A → A → Bool) → A → List A → Bool; -elem _ _ nil := false; -elem eq s (x :: xs) := eq s x || elem eq s xs; - -foldl : {A : Type} → {B : Type} → (B → A → B) → B → List A → B; -foldl f z nil := z; -foldl f z (h :: hs) := foldl f (f z h) hs; - --------------------------------------------------------------------------------- --- Pair --------------------------------------------------------------------------------- - -infixr 4 ,; -infixr 2 ×; -type × (A : Type) (B : Type) := - , : A → B → A × B; - --------------------------------------------------------------------------------- --- Maybe --------------------------------------------------------------------------------- - -type Maybe (A : Type) := - nothing : Maybe A | - just : A → Maybe A; - -from-int : Int → Maybe Int; -from-int i := if (isNegative i) nothing (just i); - -maybe : {A : Type} → {B : Type} → B → (A → B) → Maybe A → B; -maybe b _ nothing := b; -maybe _ f (just x) := f x; - -from-string : String → Maybe String; -from-string s := if (s ==String "") nothing (just s); - -pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool; -pair-from-optionString := maybe (Int_0, false); - --------------------------------------------------------------------------------- --- Anoma --------------------------------------------------------------------------------- - -axiom readPre : String → Int; -compile readPre { - c ↦ "readPre"; -}; - -axiom readPost : String → Int; -compile readPost { - c ↦ "readPost"; -}; - -axiom isBalanceKey : String → String → String; -compile isBalanceKey { - c ↦ "isBalanceKey"; -}; - -read-pre : String → Maybe Int; -read-pre s := from-int (readPre s); - -read-post : String → Maybe Int; -read-post s := from-int (readPost s); - -is-balance-key : String → String → Maybe String; -is-balance-key token key := from-string (isBalanceKey token key); - -unwrap-default : Maybe Int → Int; -unwrap-default := maybe Int_0 id; - --------------------------------------------------------------------------------- --- Validity Predicate --------------------------------------------------------------------------------- - -change-from-key : String → Int; -change-from-key key := unwrap-default (read-post key) - unwrap-default (read-pre key); - -check-vp : List String → String → Int → String → Int × Bool; -check-vp verifiers key change owner := - if - (isNegative (change-from-key key)) - -- make sure the spender approved the transaction - (change + (change-from-key key), elem (==String) owner verifiers) - (change + (change-from-key key), true); - -check-keys : String → List String → Int × Bool → String → Int × Bool; -check-keys token verifiers (change, is-success) key := - if - is-success - (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key)) - (Int_0, false); - -check-result : Int × Bool → Bool; -check-result (change, all-checked) := (change ==Int Int_0) && all-checked; - -vp : String → List String → List String → Bool; -vp token keys-changed verifiers := - check-result - (foldl - (check-keys token verifiers) - (Int_0, true) - keys-changed); - --------------------------------------------------------------------------------- --- IO --------------------------------------------------------------------------------- - -axiom Action : Type; -compile Action { - c ↦ "int"; -}; - -axiom putStr : String → Action; -compile putStr { - c ↦ "putStr"; -}; - -axiom putStrLn : String → Action; -compile putStrLn { - c ↦ "putStrLn"; -}; - -foreign c { - int sequence(int a, int b) { - return a + b; - \} -}; - -infixl 1 >>; -axiom >> : Action → Action → Action; -compile >> { - c ↦ "sequence"; -}; - -show-result : Bool → String; -show-result true := "OK"; -show-result false := "FAIL"; - --------------------------------------------------------------------------------- --- Testing VP --------------------------------------------------------------------------------- - -token : String; -token := "owner-token"; - -owner-address : String; -owner-address := "owner-address"; - -change1-key : String; -change1-key := "change1-key"; - -change2-key : String; -change2-key := "change2-key"; - -verifiers : List String; -verifiers := owner-address :: nil; - -keys-changed : List String; -keys-changed := change1-key :: change2-key :: nil; - -main : Action; -main := - (putStr "VP Status: ") - >> (putStrLn (show-result (vp token keys-changed verifiers))); - -end; diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden b/tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden deleted file mode 100644 index 7440ad4fd8..0000000000 --- a/tests/positive/MiniC/SimpleFungibleTokenImplicit/expected.golden +++ /dev/null @@ -1 +0,0 @@ -VP Status: OK diff --git a/tests/positive/MiniC/SimpleFungibleTokenImplicit/juvix.yaml b/tests/positive/MiniC/SimpleFungibleTokenImplicit/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/positive/MiniC/StdlibImport/Input.juvix b/tests/positive/MiniC/StdlibImport/Input.juvix deleted file mode 100644 index faf8d37e20..0000000000 --- a/tests/positive/MiniC/StdlibImport/Input.juvix +++ /dev/null @@ -1,11 +0,0 @@ -module Input; - --- import from stdlib -open import Stdlib.Data.String; -open import Stdlib.Data.Nat; -open import Stdlib.System.IO; - -main : IO; -main := printNatLn (2 + 3); - -end; diff --git a/tests/positive/MiniC/StdlibImport/expected.golden b/tests/positive/MiniC/StdlibImport/expected.golden deleted file mode 100644 index 7ed6ff82de..0000000000 --- a/tests/positive/MiniC/StdlibImport/expected.golden +++ /dev/null @@ -1 +0,0 @@ -5 diff --git a/tests/positive/MiniC/StdlibImport/juvix.yaml b/tests/positive/MiniC/StdlibImport/juvix.yaml deleted file mode 100644 index e69de29bb2..0000000000 diff --git a/tests/smoke/Commands/html.smoke.yaml b/tests/smoke/Commands/html.smoke.yaml index 4a49e3d116..bb10af059b 100644 --- a/tests/smoke/Commands/html.smoke.yaml +++ b/tests/smoke/Commands/html.smoke.yaml @@ -6,9 +6,9 @@ tests: shell: - bash script: | - cd milestone/ValidityPredicates - juvix html SimpleFungibleToken.juvix --only-source - cat html/SimpleFungibleToken.html + cd milestone/HelloWorld + juvix html HelloWorld.juvix --only-source + cat html/HelloWorld.html stdout: contains: @@ -20,127 +20,11 @@ tests: - bash script: | rm -rf html - juvix html milestone/ValidityPredicates/SimpleFungibleToken.juvix --only-source --output-dir=html --non-recursive + juvix html milestone/HelloWorld/HelloWorld.juvix --only-source --output-dir=html --non-recursive [ -d html/assets ] - [ -f html/SimpleFungibleToken.html ] + [ -f html/HelloWorld.html ] stdout: matches: | Copying assets files to .* - Writing .*SimpleFungibleToken.html - exit-status: 0 - - - name: recursive-generation - command: - shell: - - bash - script: | - rm -rf html - juvix html milestone/ValidityPredicates/SimpleFungibleToken.juvix --only-source --output-dir=html - (ls html | wc -l) - cd html - [ -f Stdlib.Data.Ord.html ] - [ -f Stdlib.Data.String.html ] - [ -f Stdlib.Data.Nat.html ] - [ -f Stdlib.System.IO.html ] - [ -f Stdlib.Function.html ] - [ -f Stdlib.Data.List.html ] - [ -f Stdlib.Data.String.Ord.html ] - [ -f Stdlib.Data.Product.html ] - [ -f Data.Int.Ops.html ] - [ -f Stdlib.Data.Maybe.html ] - [ -f Data.Int.html ] - [ -f Stdlib.Data.Bool.html ] - [ -f Stdlib.Prelude.html ] - [ -f Anoma.Base.html ] - [ -f SimpleFungibleToken.html ] - [ -f assets/css/source-ayu-light.css ] - [ -f assets/css/source-nord.css ] - [ -f assets/images/tara-magicien.png ] - [ -f assets/images/tara-seating.svg ] - [ -f assets/images/tara-smiling.png ] - [ -f assets/images/tara-smiling.svg ] - [ -f assets/images/tara-teaching.png ] - [ -f assets/images/tara-teaching.svg ] - [ -f assets/js/highlight.js ] - [ -f assets/js/tex-chtml.js ] - stdout: - contains: | - SimpleFungibleToken.html - exit-status: 0 - - - - name: judoc-assets - command: - shell: - - bash - script: | - rm -rf html - juvix html milestone/ValidityPredicates/SimpleFungibleToken.juvix --output-dir=html - (ls html | wc -l) - cd html - [ -f Stdlib.Data.Ord.html ] - [ -f Stdlib.Data.String.html ] - [ -f Stdlib.Data.Nat.html ] - [ -f Stdlib.System.IO.html ] - [ -f Stdlib.Function.html ] - [ -f Stdlib.Data.List.html ] - [ -f Stdlib.Data.String.Ord.html ] - [ -f Stdlib.Data.Product.html ] - [ -f Data.Int.Ops.html ] - [ -f Stdlib.Data.Maybe.html ] - [ -f Data.Int.html ] - [ -f Stdlib.Data.Bool.html ] - [ -f Stdlib.Prelude.html ] - [ -f Anoma.Base.html ] - [ -f SimpleFungibleToken.html ] - [ -f assets/css/source-ayu-light.css ] - [ -f assets/css/source-nord.css ] - [ -f assets/css/linuwial.css ] - [ -f assets/images/tara-magicien.png ] - [ -f assets/images/tara-seating.svg ] - [ -f assets/images/tara-smiling.png ] - [ -f assets/images/tara-smiling.svg ] - [ -f assets/images/tara-teaching.png ] - [ -f assets/images/tara-teaching.svg ] - [ -f assets/js/highlight.js ] - [ -f assets/js/tex-chtml.js ] - stdout: - contains: | - SimpleFungibleToken.html - exit-status: 0 - - - name: non-recursive-generation - command: - shell: - - bash - script: | - rm -rf html - juvix html milestone/ValidityPredicates/SimpleFungibleToken.juvix --output-dir=html --non-recursive - (ls html | wc -l) - cd html - [ -d assets ] - [ -f SimpleFungibleToken.html ] - stdout: - matches: | - Copying assets files to .* - Writing .*SimpleFungibleToken.html - \s*4 - exit-status: 0 - - - name: non-recursive-generation-only-source - command: - shell: - - bash - script: | - rm -rf html - juvix html milestone/ValidityPredicates/SimpleFungibleToken.juvix --output-dir=html --non-recursive --only-source - (ls html | wc -l) - cd html - [ -d assets/ ] - [ -f SimpleFungibleToken.html ] - stdout: - matches: | - Copying assets files to .* - Writing .*SimpleFungibleToken.html - \s*2 + Writing .*HelloWorld.html exit-status: 0