1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-19 21:01:48 +03:00
juvix/test/Compilation/Base.hs

57 lines
1.8 KiB
Haskell
Raw Normal View History

module Compilation.Base where
import Base
import Core.Compile.Base
Add compilation of complex pattern matching to case (#1824) This PR adds the `match-to-case` Core transformation. This transforms pattern matching nodes to a sequence of case and let nodes. ## High level description Each branch of the match is compiled to a lambda. In the combined match Each branch of the match is compiled to a lambda. These lambdas are combined in nested lets and each lambda is called in turn as each branch gets checked. The lambda corresponding to the first branch gets called first, if the pattern match in the branch fails, the lambda corresponding to the next branch is called and so on. If no branches match then a lambda is called which returns a fail node. Conceptually: <table> <tr> <td> Core </td> <td> Transformed </td> </tr> <tr> <td> ``` match v1 .. vn { b1 b2 ... bk } ``` </td> <td> ``` λ let c0 := λ FAIL in let ck := λ {...} in ... let c1 := λ {...} in c1 v1 ... vn ``` </td> </tr> </table> The patterns on each branch are compiled to either let bindings (pattern binders) or case expressions (constructor patterns). Auxillary bindings are added in the case of nested constructor patterns. The default branch in each case expression has a call to the lambda corresponding to the next branch of the match. This is because the default branch is reached if the pattern match fails. <table> <tr> <td> Pattern match </td> <td> Transformed </td> </tr> <tr> <td> ``` suc (suc n) ↦ n ``` </td> <td> ``` case ?$0 of { suc arg_8 := case ?$0 of { suc n := let n := ?$0 in n$0; _ := ?$2 ?$1 }; _ := ?$1 ?$0 } ``` </td> </tr> </table> The body of each branch is wrapped in let bindings so that the indicies of bound variables in the body point to the correct variables in the compiled expression. This is necessary because the auxiliary bindings added for nested constructor patterns will cause the original indicies to be offset. Finally, the free variables in the match branch body need to be shifted by all the bindings we've added as part of the compilation. ## Examples ### Single wildcard <table> <tr> <td> Juvix </td> <td> Core </td> <td> Transformed Core </td> </tr> <tr> <td> ``` f : Nat -> Nat; f _ := 1; ``` </td> <td> ``` λ? match ?$0 with { _ω309 ↦ ? 1 } ``` </td> <td> ``` λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? let _ω309 := ?$0 in let _ω309 := ?$0 in 1 in ?$0 ?$2 ``` </td> </tr> </table> ### Single binder <table> <tr> <td> Juvix </td> <td> Core </td> <td> Transformed Core </td> </tr> <tr> <td> ``` f : Nat -> Nat; f n := n; ``` </td> <td> ``` λ? match ?$0 with { n ↦ n$0 } ``` </td> <td> ``` λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? let n := ?$0 in let n := ?$0 in n$0 in ?$0 ?$2 ``` </td> </tr> </table> ### Single Constructor <table> <tr> <td> Juvix </td> <td> Core </td> <td> Transformed Core </td> </tr> <tr> <td> ``` f : Nat -> Nat; f (suc n) := n; ``` </td> <td> ``` λ? match ?$0 with { suc n ↦ n$0 } ``` </td> <td> ``` λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of { suc n := let n := ?$0 in let n := ?$0 in n$0; _ := ?$1 ?$0 } in ?$0 ?$2 ``` </td> </tr> </table> ### Nested Constructor <table> <tr> <td> Juvix </td> <td> Core </td> <td> Transformed Core </td> </tr> <tr> <td> ``` f : Nat -> Nat; f (suc (suc n)) := n; ``` </td> <td> ``` λ? match ?$0 with { suc (suc n) ↦ n$0 } ``` </td> <td> ``` λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of { suc arg_8 := case ?$0 of { suc n := let n := ?$0 in let n := ?$0 in n$0; _ := ?$2 ?$1 }; _ := ?$1 ?$0 } in ?$0 ?$2 ``` </td> </tr> </table> ### Multiple Branches <table> <tr> <td> Juvix </td> <td> Core </td> <td> Transformed Core </td> </tr> <tr> <td> ``` f : Nat -> Nat; f (suc n) := n; f zero := 0; ``` </td> <td> ``` λ? match ?$0 with { suc n ↦ n$0; zero ↦ ? 0 } ``` </td> <td> ``` λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of { zero := ? 0; _ := ?$1 ?$0 } in let ? := λ? case ?$0 of { suc n := let n := ?$0 in let n := ?$0 in n$0; _ := ?$1 ?$0 } in ?$0 ?$3 ``` </td> </tr> </table> ### Nested case with captured variable <table> <tr> <td> Juvix </td> <td> Core </td> <td> Transformed Core </td> </tr> <tr> <td> ``` f : Nat -> Nat -> Nat; f n m := case m | suc k := n + k; ``` </td> <td> ``` f = λ? λ? match ?$1, ?$0 with { n, m ↦ match m$0 with { suc k ↦ + n$2 k$0 } } ``` </td> <td> ``` λ? λ? let ? := λ? λ? fail "Non-exhaustive patterns" in let ? := λ? λ? let n := ?$1 in let m := ?$1 in let n := ?$1 in let m := ?$1 in let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of { suc k := let k := ?$0 in let k := ?$0 in + n$6 k$0; _ := ?$1 ?$0 } in ?$0 m$2 in ?$0 ?$3 ?$2 ``` </td> </tr> </table> ## Testing The `tests/Compilation/positive` tests are run up to the Core evaluator with `match-to-case` and `nat-to-int` transformations on Core turned on. --------- Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
2023-02-15 13:30:12 +03:00
import Core.Eval.Base
import Juvix.Compiler.Core qualified as Core
data CompileAssertionMode
= EvalOnly
| -- | Specify text to be sent to stdin of the process under test
CompileOnly Text
| EvalAndCompile
compileAssertion ::
Run test suite in parallel (#2507) ## Overview This PR makes the compiler pipeline thread-safe so that the test suite can be run in parallel. This is achieved by: * Removing use of `{get, set, with}CurrentDir` functions. * Adding locking around shared file resources like the the global-project and internal build directory. NB: **Locking is disabled for the main compiler target**, as it is single threaded they are not required. ## Run test suite in parallel To run the test suite in parallel you must add `--ta '+RTS -N -RTS'` to your stack test arguments. For example: ``` stack test --fast --ta '+RTS -N -RTS' ``` The `-N` instructs the Haskell runtime to choose the number of threads to use based on how many processors there are on your machine. You can use `-Nn` to see the number of threads to `n`. These flags are already [set in the Makefile](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/Makefile#L26) when you or CI uses `stack test`. ## Locking The Haskell package [filelock](https://hackage.haskell.org/package/filelock) is used for locking. File locks are used instead of MVars because Juvix code does not control when new threads are created, they are created by the test suite. This means that MVars created by Juvix code will have no effect, because they are created independently on each test-suite thread. Additionally the resources we're locking live on the filesystem and so can be conveniently tagged by path. ### FileLock The filelock library is wrapped in a FileLock effect: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/Base.hs#L6-L8 There is an [IO interpreter](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/IO.hs#L8) that uses filelock and an [no-op interpreter](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/Permissive.hs#L7) that just runs actions unconditionally. ### TaggedLock To make the file locks simpler to use a TaggedLock effect is introduced: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/TaggedLock/Base.hs#L5-L11 And convenience function: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/TaggedLock.hs#L28 This allows an action to be locked, tagged by a directory that may or may not exist. For example in the following code, an action is performed on a directory `root` that may delete the directory before repopulating the files. So the lockfile cannot be stored in the `root` itself. https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Extra/Files.hs#L55-L60 ## Pipeline As noted above, we only use locking in the test suite. The main app target pipeline is single threaded and so locking is unnecessary. So the interpretation of locks is parameterised so that locking can be disabled https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Compiler/Pipeline/Run.hs#L64
2023-11-16 18:19:52 +03:00
Path Abs Dir ->
Int ->
CompileAssertionMode ->
Path Abs File ->
Path Abs File ->
(String -> IO ()) ->
Assertion
compileAssertion = compileAssertionEntry id
compileAssertionEntry ::
(EntryPoint -> EntryPoint) ->
Path Abs Dir ->
Int ->
CompileAssertionMode ->
Path Abs File ->
Path Abs File ->
(String -> IO ()) ->
Assertion
compileAssertionEntry adjustEntry root' optLevel mode mainFile expectedFile step = do
step "Translate to JuvixCore"
entryPoint <- adjustEntry <$> testDefaultEntryPointIO root' mainFile
PipelineResult {..} <- snd <$> testRunIO entryPoint upToStoredCore
let tab' = Core.computeCombinedInfoTable (_pipelineResult ^. Core.coreResultModule)
evalAssertion = coreEvalAssertion' EvalModePlain tab' mainFile expectedFile step
compileAssertion' stdinText = coreCompileAssertion' optLevel tab' mainFile expectedFile stdinText step
case mode of
EvalOnly -> evalAssertion
CompileOnly stdinText -> compileAssertion' stdinText
EvalAndCompile -> evalAssertion >> compileAssertion' ""
compileErrorAssertion ::
Run test suite in parallel (#2507) ## Overview This PR makes the compiler pipeline thread-safe so that the test suite can be run in parallel. This is achieved by: * Removing use of `{get, set, with}CurrentDir` functions. * Adding locking around shared file resources like the the global-project and internal build directory. NB: **Locking is disabled for the main compiler target**, as it is single threaded they are not required. ## Run test suite in parallel To run the test suite in parallel you must add `--ta '+RTS -N -RTS'` to your stack test arguments. For example: ``` stack test --fast --ta '+RTS -N -RTS' ``` The `-N` instructs the Haskell runtime to choose the number of threads to use based on how many processors there are on your machine. You can use `-Nn` to see the number of threads to `n`. These flags are already [set in the Makefile](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/Makefile#L26) when you or CI uses `stack test`. ## Locking The Haskell package [filelock](https://hackage.haskell.org/package/filelock) is used for locking. File locks are used instead of MVars because Juvix code does not control when new threads are created, they are created by the test suite. This means that MVars created by Juvix code will have no effect, because they are created independently on each test-suite thread. Additionally the resources we're locking live on the filesystem and so can be conveniently tagged by path. ### FileLock The filelock library is wrapped in a FileLock effect: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/Base.hs#L6-L8 There is an [IO interpreter](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/IO.hs#L8) that uses filelock and an [no-op interpreter](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/Permissive.hs#L7) that just runs actions unconditionally. ### TaggedLock To make the file locks simpler to use a TaggedLock effect is introduced: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/TaggedLock/Base.hs#L5-L11 And convenience function: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/TaggedLock.hs#L28 This allows an action to be locked, tagged by a directory that may or may not exist. For example in the following code, an action is performed on a directory `root` that may delete the directory before repopulating the files. So the lockfile cannot be stored in the `root` itself. https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Extra/Files.hs#L55-L60 ## Pipeline As noted above, we only use locking in the test suite. The main app target pipeline is single threaded and so locking is unnecessary. So the interpretation of locks is parameterised so that locking can be disabled https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Compiler/Pipeline/Run.hs#L64
2023-11-16 18:19:52 +03:00
Path Abs Dir ->
Path Abs File ->
(String -> IO ()) ->
Assertion
Run test suite in parallel (#2507) ## Overview This PR makes the compiler pipeline thread-safe so that the test suite can be run in parallel. This is achieved by: * Removing use of `{get, set, with}CurrentDir` functions. * Adding locking around shared file resources like the the global-project and internal build directory. NB: **Locking is disabled for the main compiler target**, as it is single threaded they are not required. ## Run test suite in parallel To run the test suite in parallel you must add `--ta '+RTS -N -RTS'` to your stack test arguments. For example: ``` stack test --fast --ta '+RTS -N -RTS' ``` The `-N` instructs the Haskell runtime to choose the number of threads to use based on how many processors there are on your machine. You can use `-Nn` to see the number of threads to `n`. These flags are already [set in the Makefile](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/Makefile#L26) when you or CI uses `stack test`. ## Locking The Haskell package [filelock](https://hackage.haskell.org/package/filelock) is used for locking. File locks are used instead of MVars because Juvix code does not control when new threads are created, they are created by the test suite. This means that MVars created by Juvix code will have no effect, because they are created independently on each test-suite thread. Additionally the resources we're locking live on the filesystem and so can be conveniently tagged by path. ### FileLock The filelock library is wrapped in a FileLock effect: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/Base.hs#L6-L8 There is an [IO interpreter](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/IO.hs#L8) that uses filelock and an [no-op interpreter](https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/FileLock/Permissive.hs#L7) that just runs actions unconditionally. ### TaggedLock To make the file locks simpler to use a TaggedLock effect is introduced: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/TaggedLock/Base.hs#L5-L11 And convenience function: https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Data/Effect/TaggedLock.hs#L28 This allows an action to be locked, tagged by a directory that may or may not exist. For example in the following code, an action is performed on a directory `root` that may delete the directory before repopulating the files. So the lockfile cannot be stored in the `root` itself. https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Extra/Files.hs#L55-L60 ## Pipeline As noted above, we only use locking in the test suite. The main app target pipeline is single threaded and so locking is unnecessary. So the interpretation of locks is parameterised so that locking can be disabled https://github.com/anoma/juvix/blob/e6dca22cfdcff936add5e7134f9c6f20416504a5/src/Juvix/Compiler/Pipeline/Run.hs#L64
2023-11-16 18:19:52 +03:00
compileErrorAssertion root' mainFile step = do
step "Translate to JuvixCore"
entryPoint <- testDefaultEntryPointIO root' mainFile
PipelineResult {..} <- snd <$> testRunIO entryPoint upToCore
case run $ runReader Core.defaultCoreOptions $ runError @JuvixError $ Core.toStored' (_pipelineResult ^. Core.coreResultModule) >>= Core.toStripped' of
Left _ -> assertBool "" True
Right _ -> assertFailure "no error"