anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-08 08:39:26 +03:00
Code Issues Projects Releases Wiki Activity
6bfe727a0e
juvix/tests/positive/Symbols.juvix

37 lines
549 B
Plaintext
Raw Normal View History

Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
module Symbols;
Modify `open import` syntax (#2098)
2023-05-17 12:08:48 +03:00
import Stdlib.Data.Nat open;
Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
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
╘⑽╛ : Nat;
╘⑽╛ := suc 9;
Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
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
-- no - function!?
- : Nat -> Nat -> Nat;
- := (+);
Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
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
（-） : Nat -> Nat -> Nat;
（-） := (-);
Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
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
（*） : Nat -> Nat -> Nat;
（*） := (*);
Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
Add `syntax` keyword (#2107) * Closes #2007
2023-05-22 13:50:07 +03:00
syntax infixl 6 －;
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
－ : Nat -> Nat -> Nat;
－ := （-）;
Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
Add `syntax` keyword (#2107) * Closes #2007
2023-05-22 13:50:07 +03:00
syntax infixl 7 ·;
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
· : Nat -> Nat -> Nat;
· := （*）;
Widens the accepted symbol list (#1385) * Changed the valid symbols from inclusvie to exclusive * Add test using the new valid symbols
2022-07-18 14:32:43 +03:00
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
（0） : Nat;
（0） := ╘⑽╛ － ╘⑽╛ · zero;
Improve error message for confusing ':=' with '=' (#1715) Closes #1483 The error now points to the offending `=`, works correctly with multi-line clauses, and explains exactly what's wrong. E.g. for ```agda f : Nat → Nat → Nat; f zero x = x; ``` we get ``` | 6 | f zero x = x; | ^ expected ":=" instead of "=" ``` A minor disadvantage of the proposed solution is that now it's impossible to use `=` without parentheses as a top variable name in a pattern, e.g. ``` f zero = := =; ``` gives an error. However, if one really wants to name a variable `=`, it is enough just to enclose it in parentheses: ```agda f : Nat → Nat → Nat; f zero (=) := =; f (suc n) (=) := f n =; ``` I believe this slight non-uniformity is well worth the increased usability due to a better error message. Confusing `:=` with `=` is very common. Using `=` as a variable name in a top pattern is rare. Co-authored-by: janmasrovira <janmasrovira@gmail.com>
2023-01-11 18:43:16 +03:00
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
主功能 : Nat;
主功能 := （0）;
Improve error message for confusing ':=' with '=' (#1715) Closes #1483 The error now points to the offending `=`, works correctly with multi-line clauses, and explains exactly what's wrong. E.g. for ```agda f : Nat → Nat → Nat; f zero x = x; ``` we get ``` | 6 | f zero x = x; | ^ expected ":=" instead of "=" ``` A minor disadvantage of the proposed solution is that now it's impossible to use `=` without parentheses as a top variable name in a pattern, e.g. ``` f zero = := =; ``` gives an error. However, if one really wants to name a variable `=`, it is enough just to enclose it in parentheses: ```agda f : Nat → Nat → Nat; f zero (=) := =; f (suc n) (=) := f n =; ``` I believe this slight non-uniformity is well worth the increased usability due to a better error message. Confusing `:=` with `=` is very common. Using `=` as a variable name in a top pattern is rare. Co-authored-by: janmasrovira <janmasrovira@gmail.com>
2023-01-11 18:43:16 +03:00
Fix: format juvix files in test/positive (#1978) This PR fixes a formatting issue that drops blank lines between axiom declarations. It goes after: - #1980 - Closes https://github.com/anoma/juvix/issues/1986
2023-04-12 11:07:01 +03:00
axiom = : Type;
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
K : Nat → Nat → Nat;
K =a@zero (=) := =a · =;
K =a@(suc =) == := = · ==;
Reference in New Issue Copy Permalink