juvix/tests/positive/Imports/A.juvix

module A;

module M;
  module N;
    infix 3 t;
    type T :=
      | t : T;
  end;

  infixr 2 +;
  axiom
  + : Type → Type → Type;
end;

import M;

f : M.N.T;
f (_ M.N.t _) := Type M.+ Type M.+ M.MType;
[tests] add support for mocked file system in scope checker. Useful for multi file tests 2022-02-18 19:48:21 +03:00			`module A;`
Add `juvix format` command (#1886) This PR adds `juvix format` that can be used to format either a single Juvix file or all files in a Juvix project. ## Usage ``` $ juvix format --help Usage: juvix format JUVIX_FILE_OR_PROJECT [--check] [--in-place] Format a Juvix file or Juvix project When the command is run with an unformatted file it prints the reformatted source to standard output. When the command is run with a project directory it prints a list of unformatted files in the project. Available options: JUVIX_FILE_OR_PROJECT Path to a .juvix file or to a directory containing a Juvix project. --check Do not print reformatted sources or unformatted file paths to standard output. --in-place Do not print reformatted sources to standard output. Overwrite the target's contents with the formatted version if the formatted version differs from the original content. -h,--help Show this help text ``` ## Location of main implementation The implementation is split into two components: * The src API: `format` and `formatProject` https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Formatter.hs * The CLI interface: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/app/Commands/Format.hs ## in-place uses polysemy Resource effect The `--in-place` option makes a backup of the target file and restores it if there's an error during processing to avoid data loss. The implementation of this uses the polysemy [Resource effect](https://hackage.haskell.org/package/polysemy-1.9.0.0/docs/Polysemy-Resource.html). The recommended way to interpret the resource effect is to use `resourceToIOFinal` which makes it necessary to change the effects interpretation in main to use `Final IO`: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/app/Main.hs#L15 ## Format input is `FilePath` The format options uses `FilePath` instead of `AppFile f` for the input file/directory used by other commands. This is because we cannot determine if the input string is a file or directory in the CLI parser (we require IO). I discussed some ideas with @janmasrovira on how to improve this in a way that would also solve other issues with CLI input file/parsing but I want to defer this to a separate PR as this one is already quite large. One consequence of Format using `FilePath` as the input option is that the code that changes the working directory to the root of the project containing the CLI input file is changed to work with `FilePath`: https://github.com/anoma/juvix/blob/f715ef6a531f63c40ac3f629dd9cfea7e867507a/app/TopCommand/Options.hs#L33 ## New dependencies This PR adds new dependencies on `temporary` and `polysemy-zoo`. `temporary` is used for `emptySystemTempFile` in the implementation of the TempFile interpreter for IO: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Data/Effect/Files/IO.hs#L49 `polysemy-zoo` is used for the `Fresh` effect and `absorbMonadThrow` in the implementation of the pure TempFile interpreter: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Data/Effect/Files/Pure.hs#L91 NB: The pure TempFile interpreter is not used, but it seemed a good idea to include it while it's fresh in my mind. * Closes https://github.com/anoma/juvix/issues/1777 --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no> 2023-03-29 16:51:04 +03:00
			`module M;`
[tests] add support for mocked file system in scope checker. Useful for multi file tests 2022-02-18 19:48:21 +03:00			`module N;`
Add `juvix format` command (#1886) This PR adds `juvix format` that can be used to format either a single Juvix file or all files in a Juvix project. ## Usage ``` $ juvix format --help Usage: juvix format JUVIX_FILE_OR_PROJECT [--check] [--in-place] Format a Juvix file or Juvix project When the command is run with an unformatted file it prints the reformatted source to standard output. When the command is run with a project directory it prints a list of unformatted files in the project. Available options: JUVIX_FILE_OR_PROJECT Path to a .juvix file or to a directory containing a Juvix project. --check Do not print reformatted sources or unformatted file paths to standard output. --in-place Do not print reformatted sources to standard output. Overwrite the target's contents with the formatted version if the formatted version differs from the original content. -h,--help Show this help text ``` ## Location of main implementation The implementation is split into two components: * The src API: `format` and `formatProject` https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Formatter.hs * The CLI interface: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/app/Commands/Format.hs ## in-place uses polysemy Resource effect The `--in-place` option makes a backup of the target file and restores it if there's an error during processing to avoid data loss. The implementation of this uses the polysemy [Resource effect](https://hackage.haskell.org/package/polysemy-1.9.0.0/docs/Polysemy-Resource.html). The recommended way to interpret the resource effect is to use `resourceToIOFinal` which makes it necessary to change the effects interpretation in main to use `Final IO`: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/app/Main.hs#L15 ## Format input is `FilePath` The format options uses `FilePath` instead of `AppFile f` for the input file/directory used by other commands. This is because we cannot determine if the input string is a file or directory in the CLI parser (we require IO). I discussed some ideas with @janmasrovira on how to improve this in a way that would also solve other issues with CLI input file/parsing but I want to defer this to a separate PR as this one is already quite large. One consequence of Format using `FilePath` as the input option is that the code that changes the working directory to the root of the project containing the CLI input file is changed to work with `FilePath`: https://github.com/anoma/juvix/blob/f715ef6a531f63c40ac3f629dd9cfea7e867507a/app/TopCommand/Options.hs#L33 ## New dependencies This PR adds new dependencies on `temporary` and `polysemy-zoo`. `temporary` is used for `emptySystemTempFile` in the implementation of the TempFile interpreter for IO: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Data/Effect/Files/IO.hs#L49 `polysemy-zoo` is used for the `Fresh` effect and `absorbMonadThrow` in the implementation of the pure TempFile interpreter: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Data/Effect/Files/Pure.hs#L91 NB: The pure TempFile interpreter is not used, but it seemed a good idea to include it while it's fresh in my mind. * Closes https://github.com/anoma/juvix/issues/1777 --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no> 2023-03-29 16:51:04 +03:00			`infix 3 t;`
			`type T :=`
			`\| t : T;`
			`end;`

Keep regular comments in html output (#1766) - Fixes #1723 - It refactors parsing/scoping so that the scoper does not need to read files or parse any module. Instead, the parser takes care of parsing all the imported modules transitively. 2023-01-27 15:24:28 +03:00			`infixr 2 +;`
Fix: pprint positive kw for data types (#1980) As the title says. - I found this bug while formatting the examples found in the tests folder. - In addition to printing the missing positive' keyword for data types, the code also prints certain keyword annotations onto separate lines, the ones that act as attributes to their term. While this is a matter of personal preference, I find that it makes it easier to comment and uncomment individual annotations. 2023-04-05 17:40:46 +03:00			`axiom`
			`+ : Type → Type → Type;`
[ pre-commit ] Add support and hooks 2022-04-04 18:44:08 +03:00			`end;`
Add `juvix format` command (#1886) This PR adds `juvix format` that can be used to format either a single Juvix file or all files in a Juvix project. ## Usage ``` $ juvix format --help Usage: juvix format JUVIX_FILE_OR_PROJECT [--check] [--in-place] Format a Juvix file or Juvix project When the command is run with an unformatted file it prints the reformatted source to standard output. When the command is run with a project directory it prints a list of unformatted files in the project. Available options: JUVIX_FILE_OR_PROJECT Path to a .juvix file or to a directory containing a Juvix project. --check Do not print reformatted sources or unformatted file paths to standard output. --in-place Do not print reformatted sources to standard output. Overwrite the target's contents with the formatted version if the formatted version differs from the original content. -h,--help Show this help text ``` ## Location of main implementation The implementation is split into two components: * The src API: `format` and `formatProject` https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Formatter.hs * The CLI interface: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/app/Commands/Format.hs ## in-place uses polysemy Resource effect The `--in-place` option makes a backup of the target file and restores it if there's an error during processing to avoid data loss. The implementation of this uses the polysemy [Resource effect](https://hackage.haskell.org/package/polysemy-1.9.0.0/docs/Polysemy-Resource.html). The recommended way to interpret the resource effect is to use `resourceToIOFinal` which makes it necessary to change the effects interpretation in main to use `Final IO`: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/app/Main.hs#L15 ## Format input is `FilePath` The format options uses `FilePath` instead of `AppFile f` for the input file/directory used by other commands. This is because we cannot determine if the input string is a file or directory in the CLI parser (we require IO). I discussed some ideas with @janmasrovira on how to improve this in a way that would also solve other issues with CLI input file/parsing but I want to defer this to a separate PR as this one is already quite large. One consequence of Format using `FilePath` as the input option is that the code that changes the working directory to the root of the project containing the CLI input file is changed to work with `FilePath`: https://github.com/anoma/juvix/blob/f715ef6a531f63c40ac3f629dd9cfea7e867507a/app/TopCommand/Options.hs#L33 ## New dependencies This PR adds new dependencies on `temporary` and `polysemy-zoo`. `temporary` is used for `emptySystemTempFile` in the implementation of the TempFile interpreter for IO: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Data/Effect/Files/IO.hs#L49 `polysemy-zoo` is used for the `Fresh` effect and `absorbMonadThrow` in the implementation of the pure TempFile interpreter: https://github.com/anoma/juvix/blob/73952ba15c90f33919c75426cf62ae7e83fd3225/src/Juvix/Data/Effect/Files/Pure.hs#L91 NB: The pure TempFile interpreter is not used, but it seemed a good idea to include it while it's fresh in my mind. * Closes https://github.com/anoma/juvix/issues/1777 --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no> 2023-03-29 16:51:04 +03:00
			`import M;`

			`f : M.N.T;`
			`f (_ M.N.t _) := Type M.+ Type M.+ M.MType;`