anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-01 12:06:57 +03:00
Code Issues Projects Releases Wiki Activity
9bfe20e323
juvix/app/Commands/Repl.hs

662 lines
24 KiB
Haskell
Raw Normal View History

Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
{-# LANGUAGE QuasiQuotes #-}
module Commands.Repl where
Make format command's filepath optional (#2028) # Description No the filepath in the `juvix forma` command is n=made optional. However, in that case, the `--stdin` command is required. ### Implementation details ~For now, as a quick solution, I have introduce the "fake" path that is used for `fomat` command with stdin option.~ I needed to do a couple of big changes: * `format` command FILE is now optional, howvere, I check that in case of `Nothing` `--stdin` option should be present, otherwise it will fail * `entryPointModulePaths` is now `[]` instead of `NonEmpty` * `ScopeEff` now has `ScopeStdin` constructor as well, which would take the input from stdin instead of having path passed around * `RunPipelineNoFileEither` is added to the `App` with the bunch of `*Stdin` functions that doesn't require filepath argument to be passed Fixes #2008 ## Type of change - [x] New feature (non-breaking change which adds functionality) # Checklist: - [x] My code follows the style guidelines of this project - [x] I have made corresponding changes to the documentation - [x] My changes generate no new warnings - [x] I have added tests that prove my fix is effective or that my feature works: - [x] smoke tests --------- Co-authored-by: Paul Cadman <git@paulcadman.dev> Co-authored-by: janmasrovira <janmasrovira@gmail.com>
2023-04-27 18:33:08 +03:00
import Commands.Base hiding
( command,
)
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
import Commands.Repl.Base
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Commands.Repl.Options
import Control.Exception (throwIO)
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
import Control.Monad.Except qualified as Except
import Control.Monad.Reader qualified as Reader
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Control.Monad.State.Strict qualified as State
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
import Control.Monad.Trans.Class (lift)
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Data.String.Interpolate (i, __i)
import Evaluator
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
import Juvix.Compiler.Concrete.Data.InfoTable qualified as Scoped
Fix REPL state to include enough information to rerun the pipeline (#1911) Previously we were: * discarding the types table * discarding the name ids state after processing an expression in the REPL. For example evaluating: ``` let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10 ``` would loop in the REPL. We noticed that the `n` in `suc n` was being given type `Type` instead of `Nat`. This was because the name id given to n was incorrect, the REPL started using name ids from 0 again. We fixed this issue by storing information, including the types table and name ids state in the Artifacts data structure that is returned when we run the pipeline for the first time. This information is then used when we call functions to compile / type check REPL expressions. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-03-30 14:39:27 +03:00
import Juvix.Compiler.Concrete.Data.Scope (scopePath)
import Juvix.Compiler.Concrete.Data.ScopedName (absTopModulePath)
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
import Juvix.Compiler.Concrete.Data.ScopedName qualified as Scoped
import Juvix.Compiler.Concrete.Language qualified as Concrete
import Juvix.Compiler.Concrete.Pretty qualified as Concrete
Fix pipeline setup in the repl (#2046) This pr fixes a bug where the repl would crash if it had the implicit stdlib dependency and the .juvix-build/stdlib directory did not yet exist. This bug was not exposed in the smoke tests because the .juvix-build was never cleared. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-05-03 21:04:31 +03:00
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver (runPathResolver)
External package dependencies (#2272) This PR adds external git dependency support to the Juvix package format. ## New dependency Git item You can now add a `git` block to the dependencies list: ```yaml name: HelloWorld main: HelloWorld.juvix dependencies: - .juvix-build/stdlib - git: url: https://my.git.repo name: myGitRepo ref: main version: 0.1.0 ``` Git block required fields: * `url`: The URL of the git repository * `ref`: The git reference that should be checked out * `name`: The name for the dependency. This is used to name the directory of the clone, it is required. Perhaps we could come up with a way to automatically name the clone directory. Current ideas are to somehow encode the URL / ref combination or use a UUID. However there's some value in having the clone directory named in a friendly way. NB: * The values of the `name` fields must be unique among the git blocks in the dependencies list. ## Behaviour When dependencies for a package are registered, at the beginning of the compiler pipeline, all remote dependencies are processed: 1. If it doesn't already exist, the remote dependency is cloned to `.juvix-build/deps/$name` 2. `git fetch` is run in the clone 3. `git checkout` at the specified `ref` is run in the clone The clone is then processed by the PathResolver in the same way as path dependencies. NB: * Remote dependencies of transitive dependencies are also processed. * The `git fetch` step is required for the case where the remote is updated. In this case we want the user to be able to update the `ref` field. ## Errors 1. Missing fields in the Git dependency block are YAML parse errors 2. Duplicate `name` values in the dependencies list is an error thrown when the package file is processed 3. The `ref` doesn't exist in the clone or the clone directory is otherwise corrupt. An error with a suggestion to `juvix clean` is given. The package file path is used as the location in the error message. 4. Other `git` command errors (command not found, etc.), a more verbose error is given with the arguments that were passed to the git command. ## Future work 1. Add an offline mode 2. Add a lock file mechanism that resolves branch/tag git refs to commit hashes * closes https://github.com/anoma/juvix/issues/2083 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-09-01 14:37:06 +03:00
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver.Error
Fix REPL state to include enough information to rerun the pipeline (#1911) Previously we were: * discarding the types table * discarding the name ids state after processing an expression in the REPL. For example evaluating: ``` let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10 ``` would loop in the REPL. We noticed that the `n` in `suc n` was being given type `Type` instead of `Nat`. This was because the name id given to n was incorrect, the REPL started using name ids from 0 again. We fixed this issue by storing information, including the types table and name ids state in the Artifacts data structure that is returned when we run the pipeline for the first time. This information is then used when we call functions to compile / type check REPL expressions. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-03-30 14:39:27 +03:00
import Juvix.Compiler.Core qualified as Core
Pretty print JuvixCore values consistently with Juvix syntax (#1988) This PR implements pretty printing of evaluation results consistently with Juvix syntax. The printed values do not necessarily originate directly from the source code. All functions/lambdas are printed as `<fun>`. The same mechanism is used to implement pretty printing of unmatched pattern examples. Juvix REPL now uses the new value printing mechanism to display evaluation results. Typing `nil` in the REPL will now just display `nil`. The command `juvix dev repl` still prints raw JuvixCore terms. * Closes #1957 * Closes #1985
2023-04-12 13:52:40 +03:00
import Juvix.Compiler.Core.Extra.Value
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.NoDisplayInfo qualified as Info
import Juvix.Compiler.Core.Pretty qualified as Core
Add REPL option to apply Core transformations (#1796) Core transformations apply to the whole InfoTable, the REPL needs to apply Core transformations to the single node that it compiles from the user input string. The solution in this commit is to: 1. Compile the input string as before to obtain a Core Node. 2. Add this Node to a copy of the Core InfoTable for the loaded file. 3. Apply the (CLI specified) Core transformations to this InfoTable. 4. Extract the (now transformed) Node from the InfoTable. We can think of a way to improve this, maybe when we tackle allowing the user to make new definitions in the REPL. As soon as compilation of pattern matching is complete we should enable some (all?) Core transformations by default. Example: At the moment we get the following result in the REPL: ``` juvix repl ... Stdlib.Prelude> 1 + 1 suc (suc zero) ``` After this commit we can turn on `nat-to-int` transformation: ``` juvix repl -t nat-to-int Stdlib.Prelude> 1 + 1 2 ``` * Part of https://github.com/anoma/juvix/issues/1531
2023-02-01 16:00:06 +03:00
import Juvix.Compiler.Core.Transformation qualified as Core
Add juvix dev repl command (#1941) The new `juvix dev repl` command is a copy of the `juvix repl` with the addition of `--no-disambiguate` flag that is present on the `juvix dev core from-concrete` command. The `juvix repl` command now does not have the `--transforms`, `--show-de-bruijn` flags as these are only relevant for compiler developers. The eval transforms are always applied. By default `juvix dev repl` uses the eval transforms. You can override this by specifying the `-t` flag. Also we now run `disambiguateNames` transform on the info table in the `dev repl` (unless the `--no-disambiguate-names` flag is set). This is so the output of the `juvix dev repl` will match that of `juvix dev core from-concrete` and also so the output can be parsed by back the core parser. * Closes https://github.com/anoma/juvix/issues/1914
2023-03-31 01:57:44 +03:00
import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNames)
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Juvix.Compiler.Internal.Language qualified as Internal
import Juvix.Compiler.Internal.Pretty qualified as Internal
Use a Juvix source file to define a package (#2434) Depends on: * ~~https://github.com/anoma/juvix/pull/2459~~ * https://github.com/anoma/juvix/pull/2462 This PR is part of a series implementing: * https://github.com/anoma/juvix/issues/2336 This PR adds the package file loading function, including a file evaluation effect. It integrates this with the existing `readPackage` function and adds tests / smoke tests. ## Package.juvix format Instead of `juvix.yaml` (which is still supported currently) users can now place a `Package.juvix` file in the root of their project. The simplest `Package.juvix` file you can write is: ``` module Package; import PackageDescription open; package : Package := defaultPackage; ``` The [PackageDescription](https://github.com/anoma/juvix/blob/35b2f618f093895f32929ac0f2c0affcdab8d627/include/package/PackageDescription.juvix) module defines the `Package` type. Users can use "go-to definition" in their IDE from the Package file to see the documentation and definitions. Users may also import `Stdlib.Prelude` in their Package file. This is loaded from the global project. No other module imports are supported. Notes: * If a directory contains both `Package.juvix` and `juvix.yaml` then `Package.juvix` is used in preference. ## Default stdlib dependency The `Dependency` type has a constructor called `defaultStdlib`. This means that any project can use the compiler builtin standard library dependency. With `juvix.yaml` this dependency is only available when the `dependencies` field is unspecified. ``` module Package; import PackageDescription open; package : Package := defaultPackage { dependencies := [defaultStdlib] }; ``` ## Validation As well as the standard type checking validation that the Juvix compiler provides additional validation is made on the file. * The Package module must contain the identifier `package` and it must have type `Package` that's obtained from the global `PackageDescription` module. * Every dependency specified in the Package.juvix must be unique. * Closes https://github.com/anoma/juvix/issues/2336 ## Examples ### Package with name and version ``` module Package; import PackageDescription open; package : Package := defaultPackage {name := "a-package"; version := mkVersion 0 1 0}; ``` ### Package with GitHub dependency ``` module Package; import PackageDescription open; package : Package := defaultPackage {name := "a-package"; version := mkVersion 0 1 0; dependencies := [defaultStdlib; github (org := "anoma"; repo := "juvix-containers"; ref := "v0.7.1")]}; ``` ## Package with main and buildDir fields ``` module Package; import Stdlib.Prelude open; import PackageDescription open; package : Package := defaultPackage {name := "a-package"; version := mkVersion 0 1 0; dependencies := [defaultStdlib; github (org := "anoma"; repo := "juvix-containers"; ref := "v0.7.1")]; buildDir := just "/tmp/build"; main := just "HelloWorld.juvix" }; ```
2023-10-27 14:35:20 +03:00
import Juvix.Compiler.Pipeline.Package.Loader.Error
import Juvix.Compiler.Pipeline.Package.Loader.EvalEff.IO
Support module imports in Juvix REPL (#2029) This PR adds support for importing modules from within a Juvix project in the Juvix REPL. The imported module is checked (parsed, arity-checked, type-checked etc) as normal and added to the REPL session scope. Any errors during the checking phase is reported to the user. ### Notes: * You must load a file before using `import`. This is because the REPL needs to know which Juvix project is active. * You may only import modules from within the same Juvix project. ### Examples After launching `juvix repl`: #### `open import` ``` Stdlib.Prelude> open import Stdlib.Data.Int.Ord Stdlib.Prelude> 1 == 1 true ``` #### `import as` ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int Stdlib.Prelude> 1 Int.== 1 true ``` #### `import`then `open` ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int Stdlib.Prelude> open Int Stdlib.Prelude> 1 == 1 true ``` #### Line-terminating semicolons are ignored: ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int;;;;; Stdlib.Prelude> 1 Int.== 1 true ``` * Closes https://github.com/anoma/juvix/issues/1951 --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-05-08 13:23:15 +03:00
import Juvix.Compiler.Pipeline.Repl
Refactor EntryPoint, Package, Pipeline, Root packages (#2458) Depends on: * https://github.com/anoma/juvix/pull/2451 This PR is part of a series implementing: * https://github.com/anoma/juvix/issues/2336 In attempt to make the main PR: * https://github.com/anoma/juvix/pull/2434 easier to review. Changes in this PR refactor EntryPoint, Package, Pipeline, Root, splitting out the types into Base modules so that they can be imported and used in subsequent PRs with fewer dependencies to avoid package cycles.
2023-10-23 14:38:52 +03:00
import Juvix.Compiler.Pipeline.Run
Fix pipeline setup in the repl (#2046) This pr fixes a bug where the repl would crash if it had the implicit stdlib dependency and the .juvix-build/stdlib directory did not yet exist. This bug was not exposed in the smoke tests because the .juvix-build was never cleared. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-05-03 21:04:31 +03:00
import Juvix.Compiler.Pipeline.Setup (entrySetup)
External package dependencies (#2272) This PR adds external git dependency support to the Juvix package format. ## New dependency Git item You can now add a `git` block to the dependencies list: ```yaml name: HelloWorld main: HelloWorld.juvix dependencies: - .juvix-build/stdlib - git: url: https://my.git.repo name: myGitRepo ref: main version: 0.1.0 ``` Git block required fields: * `url`: The URL of the git repository * `ref`: The git reference that should be checked out * `name`: The name for the dependency. This is used to name the directory of the clone, it is required. Perhaps we could come up with a way to automatically name the clone directory. Current ideas are to somehow encode the URL / ref combination or use a UUID. However there's some value in having the clone directory named in a friendly way. NB: * The values of the `name` fields must be unique among the git blocks in the dependencies list. ## Behaviour When dependencies for a package are registered, at the beginning of the compiler pipeline, all remote dependencies are processed: 1. If it doesn't already exist, the remote dependency is cloned to `.juvix-build/deps/$name` 2. `git fetch` is run in the clone 3. `git checkout` at the specified `ref` is run in the clone The clone is then processed by the PathResolver in the same way as path dependencies. NB: * Remote dependencies of transitive dependencies are also processed. * The `git fetch` step is required for the case where the remote is updated. In this case we want the user to be able to update the `ref` field. ## Errors 1. Missing fields in the Git dependency block are YAML parse errors 2. Duplicate `name` values in the dependencies list is an error thrown when the package file is processed 3. The `ref` doesn't exist in the clone or the clone directory is otherwise corrupt. An error with a suggestion to `juvix clean` is given. The package file path is used as the location in the error message. 4. Other `git` command errors (command not found, etc.), a more verbose error is given with the arguments that were passed to the git command. ## Future work 1. Add an offline mode 2. Add a lock file mechanism that resolves branch/tag git refs to commit hashes * closes https://github.com/anoma/juvix/issues/2083 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-09-01 14:37:06 +03:00
import Juvix.Data.Effect.Git
import Juvix.Data.Effect.Process
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Juvix.Data.Error.GenericError qualified as Error
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
import Juvix.Data.NameKind
Compute new entrypoint root when loading a file in the REPL (#1615) * Add shelltests for `juvix repl` * repl: Compute entrypoint root when loading a file Previously the REPL would use app root (which could be the current directory or the project root of the initially loaded file). Thus files in a different project could not be loaded. The entrypoint root must be computed each time a new file is `:load`ed. Adds shell-tests for REPL commands * Move preludePath to Juvix.Extra.Paths
2022-11-10 14:26:38 +03:00
import Juvix.Extra.Paths
Add juvix global project under xdg directory and other improvements (#1963) Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 12:27:39 +03:00
import Juvix.Extra.Stdlib
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Juvix.Extra.Version
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
import Juvix.Prelude.Pretty
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
import Juvix.Prelude.Pretty qualified as P
import System.Console.ANSI qualified as Ansi
import System.Console.Haskeline
import System.Console.Repline
import System.Console.Repline qualified as Repline
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
printHelpTxt :: ReplOptions -> Repl ()
printHelpTxt opts = do
liftIO $ do
putStrLn normalCmds
let isDev = opts ^. replIsDev
when isDev (putStrLn devCmds)
where
normalCmds :: Text
normalCmds =
[__i|
Improvements to Juvix REPL (#1607) * REPL support reloading * Reformat :help and add :version command * repl: Display the currently loaded module in the banner * repl: Load the Prelude at launch unless --no-prelude or --no-stdlib are set
2022-11-07 20:43:30 +03:00
EXPRESSION Evaluate an expression in the context of the currently loaded module
:help Print help text and describe options
:load FILE Load a file into the REPL
:reload Reload the currently loaded file
:type EXPRESSION Infer the type of an expression
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
:def IDENTIFIER Print the definition of the identifier
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
:doc IDENTIFIER Print the documentation of the identifier
Improvements to Juvix REPL (#1607) * REPL support reloading * Reformat :help and add :version command * repl: Display the currently loaded module in the banner * repl: Load the Prelude at launch unless --no-prelude or --no-stdlib are set
2022-11-07 20:43:30 +03:00
:core EXPRESSION Translate the expression to JuvixCore
:multiline Start a multi-line input. Submit with <Ctrl-D>
:root Print the current project root
:version Display the Juvix version
:quit Exit the REPL
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
|]
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
devCmds :: Text
devCmds =
[__i|
:dev DEV CMD Command reserved for debugging
|]
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
replDefaultLoc :: Interval
replDefaultLoc = singletonInterval (mkInitialLoc replPath)
replFromJust :: Repl a -> Maybe a -> Repl a
replFromJust err = maybe err return
replFromEither :: Either JuvixError a -> Repl a
replFromEither = either (lift . Except.throwError) return
replGetContext :: Repl ReplContext
replGetContext = State.gets (^. replStateContext) >>= replFromJust noFileLoadedErr
replError :: AnsiText -> Repl a
replError msg =
lift
. Except.throwError
. JuvixError
$ GenericError
{ _genericErrorLoc = replDefaultLoc,
_genericErrorMessage = msg,
_genericErrorIntervals = [replDefaultLoc]
}
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
noFileLoadedErr :: Repl a
Add `Semigroup` instance for `AnsiText` (#2140) `AnsiText` is a type that represents some text that can be printed with `Ansi` formatting annotations, or as plain text. It is expected that it should have a `Semigroup` instance. This pr adds that. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-05-31 10:53:08 +03:00
noFileLoadedErr = replError (mkAnsiText @Text "No file loaded. Load a file using the `:load FILE` command.")
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
Update ci to use ormolu 0.5.3.0 and reformat project (#2313) Updates ormolu to 0.5.3.0 and formats the project
2023-08-25 19:37:23 +03:00
welcomeMsg :: (MonadIO m) => m ()
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
welcomeMsg = liftIO (putStrLn [i|Juvix REPL version #{versionTag}: https://juvix.org. Run :help for help|])
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
multilineCmd :: String
multilineCmd = "multiline"
quit :: String -> Repl ()
quit _ = liftIO (throwIO Interrupt)
loadEntryPoint :: EntryPoint -> Repl ()
loadEntryPoint ep = do
artif <- liftIO (corePipelineIO' ep)
let newCtx =
ReplContext
{ _replContextArtifacts = artif,
_replContextEntryPoint = ep
}
State.modify (set replStateContext (Just newCtx))
let epPath :: Maybe (Path Abs File) = ep ^? entryPointModulePaths . _head
whenJust epPath $ \path -> liftIO (putStrLn [i|OK loaded: #{toFilePath path}|])
reloadFile :: String -> Repl ()
reloadFile _ = replGetContext >>= loadEntryPoint . (^. replContextEntryPoint)
pSomeFile :: String -> Prepath File
pSomeFile = mkPrepath
loadFile :: Prepath File -> Repl ()
loadFile f = do
Do not filter unreachable symbols when compiling for REPL (#2172) Say we have a module that import/open the Prelude: Test.juvix ``` module Test; import Stdlib.Prelude open; ``` When the module is compiled, we have a step in the compiler pipeline which filters out unreachable symbols. For this module all symbols are filtered because the module contains no definitions. So if the module is loaded in the REPL, no symbols will be available to process through the evaluator. The REPL is a place to explore the symbols in the module so (like with Haskell's GHCi) it would be useful if all symbols were available in the REPL session. That's what this PR implements. * Closes https://github.com/anoma/juvix/issues/2159 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-06-05 18:52:52 +03:00
entryPoint <- getReplEntryPointFromPrepath f
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
loadEntryPoint entryPoint
loadDefaultPrelude :: Repl ()
loadDefaultPrelude = whenJustM defaultPreludeEntryPoint $ \e -> do
root <- Reader.asks (^. replRoots . rootsRootDir)
Add Internet effect (#2337)
2023-09-07 19:26:19 +03:00
let hasInternet = not (e ^. entryPointOffline)
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
-- The following is needed to ensure that the default location of the
-- standard library exists
void
. liftIO
. runM
Add Internet effect (#2337)
2023-09-07 19:26:19 +03:00
. evalInternet hasInternet
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
. runFilesIO
Use JuvixError instead of Text for errors in Package file loading (#2459) Depends on: * https://github.com/anoma/juvix/pull/2458 This PR is part of a series implementing: * https://github.com/anoma/juvix/issues/2336 In attempt to make the main PR: * https://github.com/anoma/juvix/pull/2434 easier to review. This PR introduces standard JuvixError handling for errors related to the loading of the juvix.yaml file. Before this PR errors were thrown as Text and then communicated to the user using the `error` function.
2023-10-23 21:01:36 +03:00
. runError @JuvixError
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
. runReader e
External package dependencies (#2272) This PR adds external git dependency support to the Juvix package format. ## New dependency Git item You can now add a `git` block to the dependencies list: ```yaml name: HelloWorld main: HelloWorld.juvix dependencies: - .juvix-build/stdlib - git: url: https://my.git.repo name: myGitRepo ref: main version: 0.1.0 ``` Git block required fields: * `url`: The URL of the git repository * `ref`: The git reference that should be checked out * `name`: The name for the dependency. This is used to name the directory of the clone, it is required. Perhaps we could come up with a way to automatically name the clone directory. Current ideas are to somehow encode the URL / ref combination or use a UUID. However there's some value in having the clone directory named in a friendly way. NB: * The values of the `name` fields must be unique among the git blocks in the dependencies list. ## Behaviour When dependencies for a package are registered, at the beginning of the compiler pipeline, all remote dependencies are processed: 1. If it doesn't already exist, the remote dependency is cloned to `.juvix-build/deps/$name` 2. `git fetch` is run in the clone 3. `git checkout` at the specified `ref` is run in the clone The clone is then processed by the PathResolver in the same way as path dependencies. NB: * Remote dependencies of transitive dependencies are also processed. * The `git fetch` step is required for the case where the remote is updated. In this case we want the user to be able to update the `ref` field. ## Errors 1. Missing fields in the Git dependency block are YAML parse errors 2. Duplicate `name` values in the dependencies list is an error thrown when the package file is processed 3. The `ref` doesn't exist in the clone or the clone directory is otherwise corrupt. An error with a suggestion to `juvix clean` is given. The package file path is used as the location in the error message. 4. Other `git` command errors (command not found, etc.), a more verbose error is given with the arguments that were passed to the git command. ## Future work 1. Add an offline mode 2. Add a lock file mechanism that resolves branch/tag git refs to commit hashes * closes https://github.com/anoma/juvix/issues/2083 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-09-01 14:37:06 +03:00
. runLogIO
. runProcessIO
. runError @GitProcessError
Add Internet effect (#2337)
2023-09-07 19:26:19 +03:00
. runGitProcess
External package dependencies (#2272) This PR adds external git dependency support to the Juvix package format. ## New dependency Git item You can now add a `git` block to the dependencies list: ```yaml name: HelloWorld main: HelloWorld.juvix dependencies: - .juvix-build/stdlib - git: url: https://my.git.repo name: myGitRepo ref: main version: 0.1.0 ``` Git block required fields: * `url`: The URL of the git repository * `ref`: The git reference that should be checked out * `name`: The name for the dependency. This is used to name the directory of the clone, it is required. Perhaps we could come up with a way to automatically name the clone directory. Current ideas are to somehow encode the URL / ref combination or use a UUID. However there's some value in having the clone directory named in a friendly way. NB: * The values of the `name` fields must be unique among the git blocks in the dependencies list. ## Behaviour When dependencies for a package are registered, at the beginning of the compiler pipeline, all remote dependencies are processed: 1. If it doesn't already exist, the remote dependency is cloned to `.juvix-build/deps/$name` 2. `git fetch` is run in the clone 3. `git checkout` at the specified `ref` is run in the clone The clone is then processed by the PathResolver in the same way as path dependencies. NB: * Remote dependencies of transitive dependencies are also processed. * The `git fetch` step is required for the case where the remote is updated. In this case we want the user to be able to update the `ref` field. ## Errors 1. Missing fields in the Git dependency block are YAML parse errors 2. Duplicate `name` values in the dependencies list is an error thrown when the package file is processed 3. The `ref` doesn't exist in the clone or the clone directory is otherwise corrupt. An error with a suggestion to `juvix clean` is given. The package file path is used as the location in the error message. 4. Other `git` command errors (command not found, etc.), a more verbose error is given with the arguments that were passed to the git command. ## Future work 1. Add an offline mode 2. Add a lock file mechanism that resolves branch/tag git refs to commit hashes * closes https://github.com/anoma/juvix/issues/2083 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-09-01 14:37:06 +03:00
. runError @DependencyError
Use a Juvix source file to define a package (#2434) Depends on: * ~~https://github.com/anoma/juvix/pull/2459~~ * https://github.com/anoma/juvix/pull/2462 This PR is part of a series implementing: * https://github.com/anoma/juvix/issues/2336 This PR adds the package file loading function, including a file evaluation effect. It integrates this with the existing `readPackage` function and adds tests / smoke tests. ## Package.juvix format Instead of `juvix.yaml` (which is still supported currently) users can now place a `Package.juvix` file in the root of their project. The simplest `Package.juvix` file you can write is: ``` module Package; import PackageDescription open; package : Package := defaultPackage; ``` The [PackageDescription](https://github.com/anoma/juvix/blob/35b2f618f093895f32929ac0f2c0affcdab8d627/include/package/PackageDescription.juvix) module defines the `Package` type. Users can use "go-to definition" in their IDE from the Package file to see the documentation and definitions. Users may also import `Stdlib.Prelude` in their Package file. This is loaded from the global project. No other module imports are supported. Notes: * If a directory contains both `Package.juvix` and `juvix.yaml` then `Package.juvix` is used in preference. ## Default stdlib dependency The `Dependency` type has a constructor called `defaultStdlib`. This means that any project can use the compiler builtin standard library dependency. With `juvix.yaml` this dependency is only available when the `dependencies` field is unspecified. ``` module Package; import PackageDescription open; package : Package := defaultPackage { dependencies := [defaultStdlib] }; ``` ## Validation As well as the standard type checking validation that the Juvix compiler provides additional validation is made on the file. * The Package module must contain the identifier `package` and it must have type `Package` that's obtained from the global `PackageDescription` module. * Every dependency specified in the Package.juvix must be unique. * Closes https://github.com/anoma/juvix/issues/2336 ## Examples ### Package with name and version ``` module Package; import PackageDescription open; package : Package := defaultPackage {name := "a-package"; version := mkVersion 0 1 0}; ``` ### Package with GitHub dependency ``` module Package; import PackageDescription open; package : Package := defaultPackage {name := "a-package"; version := mkVersion 0 1 0; dependencies := [defaultStdlib; github (org := "anoma"; repo := "juvix-containers"; ref := "v0.7.1")]}; ``` ## Package with main and buildDir fields ``` module Package; import Stdlib.Prelude open; import PackageDescription open; package : Package := defaultPackage {name := "a-package"; version := mkVersion 0 1 0; dependencies := [defaultStdlib; github (org := "anoma"; repo := "juvix-containers"; ref := "v0.7.1")]; buildDir := just "/tmp/build"; main := just "HelloWorld.juvix" }; ```
2023-10-27 14:35:20 +03:00
. runError @PackageLoaderError
. runEvalFileEffIO
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
. runPathResolver root
Add `juvix dependencies update` command (#2419) This PR adds a new command `juvix dependencies update` that fetches all dependencies in a project and updates the project lock file. Currently the only way to update the lock file is to delete it and generate a new one. ## CLI Docs ``` juvix dependencies --help Usage: juvix dependencies COMMAND Subcommands related to dependencies Available options: -h,--help Show this help text Available commands: update Fetch package dependencies and update the lock file ``` ## Example A project containing the following `juvix.yaml` ```yaml dependencies: - .juvix-build/stdlib/ - git: url: https://github.com/anoma/juvix-test ref: v0.6.0 name: test main: Example.juvix name: example version: 1.0.0 ``` compile to generate the lockfile: `juvix compile` ```yaml # This file was autogenerated by Juvix version 0.5.1. # Do not edit this file manually. dependencies: - path: .juvix-build/stdlib/ dependencies: [] - git: name: test ref: a94c61749678ff57556ee6e4cb1f8fbbddbc4ab1 url: https://github.com/anoma/juvix-test dependencies: - git: name: stdlib ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45 url: https://github.com/anoma/juvix-stdlib dependencies: [] ``` Now update the test dependency version: ```yaml - .juvix-build/stdlib/ - git: url: https://github.com/anoma/juvix-test ref: v0.6.1 name: test main: Example.juvix name: example version: 1.0.0 ``` And run `juvix dependencies update` Now the lockfile has updated to the hash of v0.6.1: ```yaml # This file was autogenerated by Juvix version 0.5.1. # Do not edit this file manually. dependencies: - path: .juvix-build/stdlib/ dependencies: [] - git: name: test ref: a7ac74cac0db92e0b5e349f279d797c3788cdfdd url: https://github.com/anoma/juvix-test dependencies: - git: name: stdlib ref: 4facf14d9b2d06b81ce1be1882aa9050f768cb45 url: https://github.com/anoma/juvix-stdlib dependencies: [] ``` --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-10-03 19:09:13 +03:00
$ entrySetup defaultDependenciesConfig
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
loadEntryPoint e
Do not filter unreachable symbols when compiling for REPL (#2172) Say we have a module that import/open the Prelude: Test.juvix ``` module Test; import Stdlib.Prelude open; ``` When the module is compiled, we have a step in the compiler pipeline which filters out unreachable symbols. For this module all symbols are filtered because the module contains no definitions. So if the module is loaded in the REPL, no symbols will be available to process through the evaluator. The REPL is a place to explore the symbols in the module so (like with Haskell's GHCi) it would be useful if all symbols were available in the REPL session. That's what this PR implements. * Closes https://github.com/anoma/juvix/issues/2159 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-06-05 18:52:52 +03:00
getReplEntryPoint :: (Roots -> a -> GlobalOptions -> IO EntryPoint) -> a -> Repl EntryPoint
getReplEntryPoint f inputFile = do
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
roots <- Reader.asks (^. replRoots)
gopts <- State.gets (^. replStateGlobalOptions)
Do not filter unreachable symbols when compiling for REPL (#2172) Say we have a module that import/open the Prelude: Test.juvix ``` module Test; import Stdlib.Prelude open; ``` When the module is compiled, we have a step in the compiler pipeline which filters out unreachable symbols. For this module all symbols are filtered because the module contains no definitions. So if the module is loaded in the REPL, no symbols will be available to process through the evaluator. The REPL is a place to explore the symbols in the module so (like with Haskell's GHCi) it would be useful if all symbols were available in the REPL session. That's what this PR implements. * Closes https://github.com/anoma/juvix/issues/2159 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-06-05 18:52:52 +03:00
liftIO (set entryPointSymbolPruningMode KeepAll <$> f roots inputFile gopts)
getReplEntryPointFromPrepath :: Prepath File -> Repl EntryPoint
getReplEntryPointFromPrepath = getReplEntryPoint entryPointFromGlobalOptionsPre
getReplEntryPointFromPath :: Path Abs File -> Repl EntryPoint
getReplEntryPointFromPath = getReplEntryPoint entryPointFromGlobalOptions
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
displayVersion :: String -> Repl ()
displayVersion _ = liftIO (putStrLn versionTag)
replCommand :: ReplOptions -> String -> Repl ()
replCommand opts input = catchAll $ do
ctx <- replGetContext
let tab = ctx ^. replContextArtifacts . artifactCoreTable
evalRes <- compileThenEval ctx input
whenJust evalRes $ \n ->
if
| Info.member Info.kNoDisplayInfo (Core.getInfo n) -> return ()
| opts ^. replPrintValues ->
renderOutLn (Core.ppOut opts (toValue tab n))
| otherwise -> renderOutLn (Core.ppOut opts n)
where
compileThenEval :: ReplContext -> String -> Repl (Maybe Core.Node)
compileThenEval ctx s = compileString >>= mapM eval
where
artif :: Artifacts
artif = ctx ^. replContextArtifacts
eval :: Core.Node -> Repl Core.Node
eval n = do
Do not filter unreachable symbols when compiling for REPL (#2172) Say we have a module that import/open the Prelude: Test.juvix ``` module Test; import Stdlib.Prelude open; ``` When the module is compiled, we have a step in the compiler pipeline which filters out unreachable symbols. For this module all symbols are filtered because the module contains no definitions. So if the module is loaded in the REPL, no symbols will be available to process through the evaluator. The REPL is a place to explore the symbols in the module so (like with Haskell's GHCi) it would be useful if all symbols were available in the REPL session. That's what this PR implements. * Closes https://github.com/anoma/juvix/issues/2159 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-06-05 18:52:52 +03:00
ep <- getReplEntryPointFromPrepath (mkPrepath (toFilePath replPath))
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
let shouldDisambiguate :: Bool
repl: Run disambiguateNames on result node (#1961) There were two bugs here: 1. The _replNoDisambiguate option was set to True for `juvix repl`. 2. The disambiguateNames pass was being applied after the result node had already been fetched from the infotable. * Closes https://github.com/anoma/juvix/issues/1958
2023-04-03 11:58:08 +03:00
shouldDisambiguate = not (opts ^. replNoDisambiguate)
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
(artif', n') <-
replFromEither
. run
. runReader ep
. runError @JuvixError
. runState artif
. runTransformations shouldDisambiguate (opts ^. replTransformations)
$ n
liftIO (doEvalIO' artif' n') >>= replFromEither
doEvalIO' :: Artifacts -> Core.Node -> IO (Either JuvixError Core.Node)
doEvalIO' artif' n =
mapLeft (JuvixError @Core.CoreError)
<$> doEvalIO False replDefaultLoc (artif' ^. artifactCoreTable) n
compileString :: Repl (Maybe Core.Node)
compileString = do
(artifacts, res) <- liftIO $ compileReplInputIO' ctx (strip (pack s))
res' <- replFromEither res
State.modify (over (replStateContext . _Just) (set replContextArtifacts artifacts))
return res'
core :: String -> Repl ()
core input = do
ctx <- replGetContext
opts <- Reader.asks (^. replOptions)
compileRes <- liftIO (compileReplInputIO' ctx (strip (pack input))) >>= replFromEither . snd
whenJust compileRes (renderOutLn . Core.ppOut opts)
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
dev :: String -> Repl ()
dev input = do
ctx <- replGetContext
if
| input == scoperStateCmd -> do
renderOutLn (Concrete.ppTrace (ctx ^. replContextArtifacts . artifactScoperState))
| otherwise ->
renderOutLn
( "Unrecognized command "
<> input
<> "\nAvailable commands: "
<> unwords cmds
)
where
cmds :: [String]
cmds = [scoperStateCmd]
scoperStateCmd :: String
scoperStateCmd = "scoperState"
Update ci to use ormolu 0.5.3.0 and reformat project (#2313) Updates ormolu to 0.5.3.0 and formats the project
2023-08-25 19:37:23 +03:00
ppConcrete :: (Concrete.PrettyPrint a) => a -> Repl AnsiText
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
ppConcrete a = do
gopts <- State.gets (^. replStateGlobalOptions)
let popts :: GenericOptions = project' gopts
return (Concrete.ppOut popts a)
Update ci to use ormolu 0.5.3.0 and reformat project (#2313) Updates ormolu to 0.5.3.0 and formats the project
2023-08-25 19:37:23 +03:00
printConcrete :: (Concrete.PrettyPrint a) => a -> Repl ()
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
printConcrete = ppConcrete >=> renderOut
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
Update ci to use ormolu 0.5.3.0 and reformat project (#2313) Updates ormolu to 0.5.3.0 and formats the project
2023-08-25 19:37:23 +03:00
printConcreteLn :: (Concrete.PrettyPrint a) => a -> Repl ()
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
printConcreteLn = ppConcrete >=> renderOutLn
replParseIdentifiers :: String -> Repl (NonEmpty Concrete.ScopedIden)
replParseIdentifiers input =
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
replExpressionUpToScopedAtoms (strip (pack input))
>>= getIdentifiers
where
getIdentifiers :: Concrete.ExpressionAtoms 'Concrete.Scoped -> Repl (NonEmpty Concrete.ScopedIden)
getIdentifiers as = mapM getIdentifier (as ^. Concrete.expressionAtoms)
where
getIdentifier :: Concrete.ExpressionAtom 'Concrete.Scoped -> Repl (Concrete.ScopedIden)
getIdentifier = \case
Concrete.AtomIdentifier a -> return a
Concrete.AtomParens p
| Concrete.ExpressionIdentifier a <- p -> return a
| Concrete.ExpressionParensIdentifier a <- p -> return a
_ -> err
where
err :: Repl a
Add `Semigroup` instance for `AnsiText` (#2140) `AnsiText` is a type that represents some text that can be printed with `Ansi` formatting annotations, or as plain text. It is expected that it should have a `Semigroup` instance. This pr adds that. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-05-31 10:53:08 +03:00
err = replError (mkAnsiText @Text ":def expects one or more identifiers")
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
printDocumentation :: String -> Repl ()
printDocumentation = replParseIdentifiers >=> printIdentifiers
where
printIdentifiers :: NonEmpty Concrete.ScopedIden -> Repl ()
printIdentifiers (d :| ds) = do
printIdentifier d
whenJust (nonEmpty ds) $ \ds' -> replNewline >> printIdentifiers ds'
where
getInfoTable :: Repl Scoped.InfoTable
getInfoTable = (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
printIdentifier :: Concrete.ScopedIden -> Repl ()
printIdentifier s = do
Aliasing (#2301) - Closes #2188. This pr introduces a new syntactical statement for defining aliases: ``` syntax alias newName := oldName; ``` where `oldName` can be any name in the expression namespace. Fixity and module aliases are not supported at the moment. - The `newName` does not inherit the fixity of `oldName`. We have agreed that the goal is to inherit the fixity of `oldName` except if `newName` has a fixity statement, but this will be done in a separate pr as it requires #2310.
2023-08-25 16:28:58 +03:00
let n = s ^. Concrete.scopedIdenFinal . Scoped.nameId
Separate modules namespace (#2257)
2023-07-26 10:59:50 +03:00
mdoc <- case getNameKind s of
KNameAxiom -> getDocAxiom n
KNameInductive -> getDocInductive n
KNameLocal -> return Nothing
KNameFunction -> getDocFunction n
KNameConstructor -> getDocConstructor n
KNameLocalModule -> impossible
KNameTopModule -> impossible
Aliasing (#2301) - Closes #2188. This pr introduces a new syntactical statement for defining aliases: ``` syntax alias newName := oldName; ``` where `oldName` can be any name in the expression namespace. Fixity and module aliases are not supported at the moment. - The `newName` does not inherit the fixity of `oldName`. We have agreed that the goal is to inherit the fixity of `oldName` except if `newName` has a fixity statement, but this will be done in a separate pr as it requires #2310.
2023-08-25 16:28:58 +03:00
KNameAlias -> impossible
User-friendly operator declaration syntax (#2270) * Closes #1964 Adds the possibility to define operator fixities. They live in a separate namespace. Standard library defines a few in `Stdlib.Data.Fixity`: ``` syntax fixity rapp {arity: binary, assoc: right}; syntax fixity lapp {arity: binary, assoc: left, same: rapp}; syntax fixity seq {arity: binary, assoc: left, above: [lapp]}; syntax fixity functor {arity: binary, assoc: right}; syntax fixity logical {arity: binary, assoc: right, above: [seq]}; syntax fixity comparison {arity: binary, assoc: none, above: [logical]}; syntax fixity pair {arity: binary, assoc: right}; syntax fixity cons {arity: binary, assoc: right, above: [pair]}; syntax fixity step {arity: binary, assoc: right}; syntax fixity range {arity: binary, assoc: right, above: [step]}; syntax fixity additive {arity: binary, assoc: left, above: [comparison, range, cons]}; syntax fixity multiplicative {arity: binary, assoc: left, above: [additive]}; syntax fixity composition {arity: binary, assoc: right, above: [multiplicative]}; ``` The fixities are identifiers in a separate namespace (different from symbol and module namespaces). They can be exported/imported and then used in operator declarations: ``` import Stdlib.Data.Fixity open; syntax operator && logical; syntax operator || logical; syntax operator + additive; syntax operator * multiplicative; ```
2023-08-09 19:15:51 +03:00
KNameFixity -> impossible
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
printDoc mdoc
where
printDoc :: Maybe (Concrete.Judoc 'Concrete.Scoped) -> Repl ()
printDoc = \case
Nothing -> do
s' <- ppConcrete s
Add `Semigroup` instance for `AnsiText` (#2140) `AnsiText` is a type that represents some text that can be printed with `Ansi` formatting annotations, or as plain text. It is expected that it should have a `Semigroup` instance. This pr adds that. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-05-31 10:53:08 +03:00
renderOut (mkAnsiText @Text "No documentation available for ")
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
renderOutLn s'
Just ju -> printConcrete ju
getDocFunction :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
getDocFunction fun = do
tbl :: Scoped.InfoTable <- getInfoTable
let def :: Scoped.FunctionInfo = tbl ^?! Scoped.infoFunctions . at fun . _Just
New syntax for function definitions (#2243) - Closes #2060 - Closes #2189 - This pr adds support for the syntax described in #2189. It does not drop support for the old syntax. It is possible to automatically translate juvix files to the new syntax by using the formatter with the `--new-function-syntax` flag. E.g. ``` juvix format --in-place --new-function-syntax ``` # Syntax changes Type signatures follow this pattern: ``` f (a1 : Expr) .. (an : Expr) : Expr ``` where each `ai` is a non-empty list of symbols. Braces are used instead of parentheses when the argument is implicit. Then, we have these variants: 1. Simple body. After the signature we have `:= Expr;`. 2. Clauses. The function signature is followed by a non-empty sequence of clauses. Each clause has the form: ``` | atomPat .. atomPat := Expr ``` # Mutual recursion Now identifiers **do not need to be defined before they are used**, making it possible to define mutually recursive functions/types without any special syntax. There are some exceptions to this. We cannot forward reference a symbol `f` in some statement `s` if between `s` and the definition of `f` there is one of the following statements: 1. Local module 2. Import statement 3. Open statement I think it should be possible to drop the restriction for local modules and import statements
2023-07-10 20:57:55 +03:00
return (def ^. Scoped.functionInfoDoc)
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
getDocInductive :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
getDocInductive ind = do
tbl :: Scoped.InfoTable <- (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
let def :: Concrete.InductiveDef 'Concrete.Scoped = tbl ^?! Scoped.infoInductives . at ind . _Just . Scoped.inductiveInfoDef
return (def ^. Concrete.inductiveDoc)
getDocAxiom :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
getDocAxiom ax = do
tbl :: Scoped.InfoTable <- (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
let def :: Concrete.AxiomDef 'Concrete.Scoped = tbl ^?! Scoped.infoAxioms . at ax . _Just . Scoped.axiomInfoDef
return (def ^. Concrete.axiomDoc)
getDocConstructor :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
getDocConstructor c = do
tbl :: Scoped.InfoTable <- (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
let def :: Scoped.ConstructorInfo = tbl ^?! Scoped.infoConstructors . at c . _Just
return (def ^. Scoped.constructorInfoDef . Concrete.constructorDoc)
printDefinition :: String -> Repl ()
printDefinition = replParseIdentifiers >=> printIdentifiers
where
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
printIdentifiers :: NonEmpty Concrete.ScopedIden -> Repl ()
printIdentifiers (d :| ds) = do
printIdentifier d
whenJust (nonEmpty ds) $ \ds' -> replNewline >> printIdentifiers ds'
where
getInfoTable :: Repl Scoped.InfoTable
getInfoTable = (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
printIdentifier :: Concrete.ScopedIden -> Repl ()
Separate modules namespace (#2257)
2023-07-26 10:59:50 +03:00
printIdentifier s =
Aliasing (#2301) - Closes #2188. This pr introduces a new syntactical statement for defining aliases: ``` syntax alias newName := oldName; ``` where `oldName` can be any name in the expression namespace. Fixity and module aliases are not supported at the moment. - The `newName` does not inherit the fixity of `oldName`. We have agreed that the goal is to inherit the fixity of `oldName` except if `newName` has a fixity statement, but this will be done in a separate pr as it requires #2310.
2023-08-25 16:28:58 +03:00
let n = s ^. Concrete.scopedIdenFinal . Scoped.nameId
Separate modules namespace (#2257)
2023-07-26 10:59:50 +03:00
in case getNameKind s of
KNameAxiom -> printAxiom n
KNameInductive -> printInductive n
KNameLocal -> return ()
KNameFunction -> printFunction n
KNameConstructor -> printConstructor n
KNameLocalModule -> impossible
KNameTopModule -> impossible
User-friendly operator declaration syntax (#2270) * Closes #1964 Adds the possibility to define operator fixities. They live in a separate namespace. Standard library defines a few in `Stdlib.Data.Fixity`: ``` syntax fixity rapp {arity: binary, assoc: right}; syntax fixity lapp {arity: binary, assoc: left, same: rapp}; syntax fixity seq {arity: binary, assoc: left, above: [lapp]}; syntax fixity functor {arity: binary, assoc: right}; syntax fixity logical {arity: binary, assoc: right, above: [seq]}; syntax fixity comparison {arity: binary, assoc: none, above: [logical]}; syntax fixity pair {arity: binary, assoc: right}; syntax fixity cons {arity: binary, assoc: right, above: [pair]}; syntax fixity step {arity: binary, assoc: right}; syntax fixity range {arity: binary, assoc: right, above: [step]}; syntax fixity additive {arity: binary, assoc: left, above: [comparison, range, cons]}; syntax fixity multiplicative {arity: binary, assoc: left, above: [additive]}; syntax fixity composition {arity: binary, assoc: right, above: [multiplicative]}; ``` The fixities are identifiers in a separate namespace (different from symbol and module namespaces). They can be exported/imported and then used in operator declarations: ``` import Stdlib.Data.Fixity open; syntax operator && logical; syntax operator || logical; syntax operator + additive; syntax operator * multiplicative; ```
2023-08-09 19:15:51 +03:00
KNameFixity -> impossible
Aliasing (#2301) - Closes #2188. This pr introduces a new syntactical statement for defining aliases: ``` syntax alias newName := oldName; ``` where `oldName` can be any name in the expression namespace. Fixity and module aliases are not supported at the moment. - The `newName` does not inherit the fixity of `oldName`. We have agreed that the goal is to inherit the fixity of `oldName` except if `newName` has a fixity statement, but this will be done in a separate pr as it requires #2310.
2023-08-25 16:28:58 +03:00
KNameAlias -> impossible
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
where
Update ci to use ormolu 0.5.3.0 and reformat project (#2313) Updates ormolu to 0.5.3.0 and formats the project
2023-08-25 19:37:23 +03:00
printLocation :: (HasLoc s) => s -> Repl ()
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
printLocation def = do
s' <- ppConcrete s
let txt :: Text = " is " <> prettyText (nameKindWithArticle (getNameKind s)) <> " defined at " <> prettyText (getLoc def)
Add `Semigroup` instance for `AnsiText` (#2140) `AnsiText` is a type that represents some text that can be printed with `Ansi` formatting annotations, or as plain text. It is expected that it should have a `Semigroup` instance. This pr adds that. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-05-31 10:53:08 +03:00
renderOutLn (s' <> mkAnsiText txt)
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
printFunction :: Scoped.NameId -> Repl ()
printFunction fun = do
tbl :: Scoped.InfoTable <- getInfoTable
Case value inlining (#2441) * Introduces the `inline: case` pragma which causes an identifier to be inlined if it is matched on. This is necessary to support GEB without compromising optimization for other targets. * Adapts to the new commits in https://github.com/anoma/juvix-stdlib/pull/86
2023-10-12 19:59:47 +03:00
case tbl ^. Scoped.infoFunctions . at fun of
Just def -> do
printLocation def
printConcreteLn def
Nothing -> return ()
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
printInductive :: Scoped.NameId -> Repl ()
printInductive ind = do
tbl :: Scoped.InfoTable <- (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
let def :: Concrete.InductiveDef 'Concrete.Scoped = tbl ^?! Scoped.infoInductives . at ind . _Just . Scoped.inductiveInfoDef
printLocation def
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
printConcreteLn def
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
printAxiom :: Scoped.NameId -> Repl ()
printAxiom ax = do
tbl :: Scoped.InfoTable <- (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
let def :: Concrete.AxiomDef 'Concrete.Scoped = tbl ^?! Scoped.infoAxioms . at ax . _Just . Scoped.axiomInfoDef
printLocation def
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
printConcreteLn def
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
printConstructor :: Scoped.NameId -> Repl ()
printConstructor c = do
tbl :: Scoped.InfoTable <- (^. replContextArtifacts . artifactScopeTable) <$> replGetContext
let ind :: Scoped.Symbol = tbl ^?! Scoped.infoConstructors . at c . _Just . Scoped.constructorInfoTypeName
printInductive (ind ^. Scoped.nameId)
inferType :: String -> Repl ()
inferType input = do
gopts <- State.gets (^. replStateGlobalOptions)
n <- replExpressionUpToTyped (strip (pack input))
renderOutLn (Internal.ppOut (project' @GenericOptions gopts) (n ^. Internal.typedType))
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
replCommands :: ReplOptions -> [(String, String -> Repl ())]
replCommands opts = catchable ++ nonCatchable
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
where
nonCatchable :: [(String, String -> Repl ())]
nonCatchable =
[ ("quit", quit)
]
catchable :: [(String, String -> Repl ())]
catchable =
map
(second (catchAll .))
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
[ ("help", const (printHelpTxt opts)),
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
-- `multiline` is included here for auto-completion purposes only.
-- `repline`'s `multilineCommand` logic overrides this no-op.
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
(multilineCmd, const (return ())),
("load", loadFile . pSomeFile),
("reload", reloadFile),
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
("root", printRoot),
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
("def", printDefinition),
Add `:doc` command to the repl (#2142)
2023-05-30 19:19:39 +03:00
("doc", printDocumentation),
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
("type", inferType),
Improvements to Juvix REPL (#1607) * REPL support reloading * Reformat :help and add :version command * repl: Display the currently loaded module in the banner * repl: Load the Prelude at launch unless --no-prelude or --no-stdlib are set
2022-11-07 20:43:30 +03:00
("version", displayVersion),
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
("core", core),
("dev", dev)
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
]
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
catchAll :: Repl () -> Repl ()
catchAll = Repline.dontCrash . catchJuvixError
where
catchJuvixError :: Repl () -> Repl ()
catchJuvixError (HaskelineT m) = HaskelineT (mapInputT_ catchErrorS m)
where
catchErrorS :: ReplS () -> ReplS ()
catchErrorS = (`Except.catchError` printErrorS)
defaultMatcher :: [(String, CompletionFunc ReplS)]
defaultMatcher = [(":load", fileCompleter)]
optsCompleter :: WordCompleter ReplS
optsCompleter n = do
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
opts <- Reader.asks (^. replOptions)
let names = (":" <>) . fst <$> replCommands opts
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
return (filter (isPrefixOf n) names)
replBanner :: MultiLine -> Repl String
replBanner = \case
MultiLine -> return "... "
SingleLine -> do
mmodulePath <-
State.gets
( ^?
replStateContext
. _Just
. replContextArtifacts
. artifactMainModuleScope
. _Just
. scopePath
. absTopModulePath
)
return $ case mmodulePath of
Just path -> [i|#{unpack (P.prettyText path)}> |]
Nothing -> "juvix> "
replPrefix :: Maybe Char
replPrefix = Just ':'
replMultilineCommand :: Maybe String
replMultilineCommand = Just multilineCmd
replInitialiser :: Repl ()
replInitialiser = do
gopts <- State.gets (^. replStateGlobalOptions)
opts <- Reader.asks (^. replOptions)
welcomeMsg
unless
(opts ^. replNoPrelude || gopts ^. globalNoStdlib)
(maybe loadDefaultPrelude (loadFile . (^. pathPath)) (opts ^. replInputFile))
replFinaliser :: Repl ExitDecision
replFinaliser = return Exit
replTabComplete :: CompleterStyle ReplS
replTabComplete = Prefix (wordCompleter optsCompleter) defaultMatcher
printRoot :: String -> Repl ()
printRoot _ = do
r <- State.gets (^. replStateRoots . rootsRootDir)
liftIO $ putStrLn (pack (toFilePath r))
Update ci to use ormolu 0.5.3.0 and reformat project (#2313) Updates ormolu to 0.5.3.0 and formats the project
2023-08-25 19:37:23 +03:00
runCommand :: (Members '[Embed IO, App] r) => ReplOptions -> Sem r ()
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
runCommand opts = do
roots <- askRoots
let replAction :: ReplS ()
Support basic dependencies (#1622)
2022-12-20 15:05:40 +03:00
replAction = do
evalReplOpts
ReplOpts
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
{ prefix = replPrefix,
multilineCommand = replMultilineCommand,
initialiser = replInitialiser,
finaliser = replFinaliser,
tabComplete = replTabComplete,
command = replCommand opts,
Add field projections for records (#2260) - Closes #2258 # Overview When we define a type with a single constructor and one ore more fields, a local module is generated with the same name as the inductive type. This module contains a projection for every field. Projections can be used as any other function. E.g. If we have ``` type Pair (A B : Type) := mkPair { fst : A; snd : B; }; ``` Then we generate ``` module Pair; fst {A B : Type} : Pair A B -> A | (mkPair a b) := a; snd : {A B : Type} : Pair A B -> B | (mkPair a b) := b; end; ```
2023-08-01 11:46:22 +03:00
options = replCommands opts,
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
banner = replBanner
Support basic dependencies (#1622)
2022-12-20 15:05:40 +03:00
}
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
globalOptions <- askGlobalOptions
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
let env =
ReplEnv
{ _replRoots = roots,
_replOptions = opts
}
iniState =
ReplState
{ _replStateRoots = roots,
_replStateContext = Nothing,
_replStateGlobalOptions = globalOptions
}
e <-
embed
. Except.runExceptT
. (`State.evalStateT` iniState)
. (`Reader.runReaderT` env)
$ replAction
case e of
Left {} -> error "impossible: uncaught exception"
Right () -> return ()
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Add juvix global project under xdg directory and other improvements (#1963) Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 12:27:39 +03:00
-- | If the package contains the stdlib as a dependency, loads the Prelude
defaultPreludeEntryPoint :: Repl (Maybe EntryPoint)
Compute new entrypoint root when loading a file in the REPL (#1615) * Add shelltests for `juvix repl` * repl: Compute entrypoint root when loading a file Previously the REPL would use app root (which could be the current directory or the project root of the initially loaded file). Thus files in a different project could not be loaded. The entrypoint root must be computed each time a new file is `:load`ed. Adds shell-tests for REPL commands * Move preludePath to Juvix.Extra.Paths
2022-11-10 14:26:38 +03:00
defaultPreludeEntryPoint = do
Add juvix global project under xdg directory and other improvements (#1963) Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 12:27:39 +03:00
roots <- State.gets (^. replStateRoots)
let buildDir = roots ^. rootsBuildDir
root = roots ^. rootsRootDir
pkg = roots ^. rootsPackage
Support more paths (#2000) - Closes #1993 This pr makes it possible to use `~`, `..` and environment variables in the `juvix.yaml` and all flags / input of the cli. In the CLI, the shell will be responsible for replacing environment variables with their value, so the usual syntax can be used. For the `dependencies` field, I have implemented a parser that has some restrictions: 1. Environment variables are given with the makefile-like syntax `$(VAR)` 2. The three characters `$` `(` `)` are reserved for the environment variables syntax. They cannot be part of the path. 3. `~` is reserved for `$(HOME)`. I.e. the prepath `~~` will expand to `$HOME$HOME`. 4. Nested environment variables are not allowed. Thanks @paulcadman for the feedback. I think we are ready to merge this nightmarish pr :ghost: --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-19 17:56:48 +03:00
mstdlibPath <- liftIO (runM (runFilesIO (packageStdlib root buildDir (pkg ^. packageDependencies))))
case mstdlibPath of
Add juvix global project under xdg directory and other improvements (#1963) Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 12:27:39 +03:00
Just stdlibPath ->
Global offline flag (#2335) This PR introduces a global `--offline` flag. ## Doctor This replaces the `--offline` flag on the doctor command. ## Juvix package builds The flag applies to juvix build commands like `juvix compile`, `juvix repl`. This is so that users can continue to build packages offline that have external dependencies when there's no network connection (as long as they built the same package online previously). Specifically, when the `--offline` flag is used in a package that has external git dependencies. * No `git clone` or `git fetch` commands are used * `git checkout` will continue to be used * Clones from previous builds are reused This means that you can update the `ref` field in a git dependency, as long as the ref existed the last time that the project was built without the `--offline` flag. * Closes https://github.com/anoma/juvix/issues/2333
2023-09-05 18:11:17 +03:00
Just
. set entryPointResolverRoot stdlibPath
Do not filter unreachable symbols when compiling for REPL (#2172) Say we have a module that import/open the Prelude: Test.juvix ``` module Test; import Stdlib.Prelude open; ``` When the module is compiled, we have a step in the compiler pipeline which filters out unreachable symbols. For this module all symbols are filtered because the module contains no definitions. So if the module is loaded in the REPL, no symbols will be available to process through the evaluator. The REPL is a place to explore the symbols in the module so (like with Haskell's GHCi) it would be useful if all symbols were available in the REPL session. That's what this PR implements. * Closes https://github.com/anoma/juvix/issues/2159 --------- Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
2023-06-05 18:52:52 +03:00
<$> getReplEntryPointFromPath (stdlibPath <//> preludePath)
Support more paths (#2000) - Closes #1993 This pr makes it possible to use `~`, `..` and environment variables in the `juvix.yaml` and all flags / input of the cli. In the CLI, the shell will be responsible for replacing environment variables with their value, so the usual syntax can be used. For the `dependencies` field, I have implemented a parser that has some restrictions: 1. Environment variables are given with the makefile-like syntax `$(VAR)` 2. The three characters `$` `(` `)` are reserved for the environment variables syntax. They cannot be part of the path. 3. `~` is reserved for `$(HOME)`. I.e. the prepath `~~` will expand to `$HOME$HOME`. 4. Nested environment variables are not allowed. Thanks @paulcadman for the feedback. I think we are ready to merge this nightmarish pr :ghost: --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-19 17:56:48 +03:00
Nothing -> return Nothing
Compute new entrypoint root when loading a file in the REPL (#1615) * Add shelltests for `juvix repl` * repl: Compute entrypoint root when loading a file Previously the REPL would use app root (which could be the current directory or the project root of the initially loaded file). Thus files in a different project could not be loaded. The entrypoint root must be computed each time a new file is `:load`ed. Adds shell-tests for REPL commands * Move preludePath to Juvix.Extra.Paths
2022-11-10 14:26:38 +03:00
Support basic dependencies (#1622)
2022-12-20 15:05:40 +03:00
replMakeAbsolute :: SomeBase b -> Repl (Path Abs b)
replMakeAbsolute = \case
Abs p -> return p
Rel r -> do
Add juvix global project under xdg directory and other improvements (#1963) Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-04-13 12:27:39 +03:00
invokeDir <- State.gets (^. replStateRoots . rootsInvokeDir)
Support basic dependencies (#1622)
2022-12-20 15:05:40 +03:00
return (invokeDir <//> r)
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
replExpressionUpToScopedAtoms :: Text -> Repl (Concrete.ExpressionAtoms 'Concrete.Scoped)
replExpressionUpToScopedAtoms txt = do
ctx <- replGetContext
x <-
liftIO
. runM
. runError
. evalState (ctx ^. replContextArtifacts)
. runReader (ctx ^. replContextEntryPoint)
$ expressionUpToAtomsScoped replPath txt
replFromEither x
replExpressionUpToTyped :: Text -> Repl Internal.TypedExpression
replExpressionUpToTyped txt = do
ctx <- replGetContext
x <-
liftIO
. runM
. runError
. evalState (ctx ^. replContextArtifacts)
. runReader (ctx ^. replContextEntryPoint)
$ expressionUpToTyped replPath txt
replFromEither x
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Support module imports in Juvix REPL (#2029) This PR adds support for importing modules from within a Juvix project in the Juvix REPL. The imported module is checked (parsed, arity-checked, type-checked etc) as normal and added to the REPL session scope. Any errors during the checking phase is reported to the user. ### Notes: * You must load a file before using `import`. This is because the REPL needs to know which Juvix project is active. * You may only import modules from within the same Juvix project. ### Examples After launching `juvix repl`: #### `open import` ``` Stdlib.Prelude> open import Stdlib.Data.Int.Ord Stdlib.Prelude> 1 == 1 true ``` #### `import as` ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int Stdlib.Prelude> 1 Int.== 1 true ``` #### `import`then `open` ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int Stdlib.Prelude> open Int Stdlib.Prelude> 1 == 1 true ``` #### Line-terminating semicolons are ignored: ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int;;;;; Stdlib.Prelude> 1 Int.== 1 true ``` * Closes https://github.com/anoma/juvix/issues/1951 --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-05-08 13:23:15 +03:00
compileReplInputIO' :: ReplContext -> Text -> IO (Artifacts, (Either JuvixError (Maybe Core.Node)))
compileReplInputIO' ctx txt =
Fix REPL state to include enough information to rerun the pipeline (#1911) Previously we were: * discarding the types table * discarding the name ids state after processing an expression in the REPL. For example evaluating: ``` let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10 ``` would loop in the REPL. We noticed that the `n` in `suc n` was being given type `Type` instead of `Nat`. This was because the name id given to n was incorrect, the REPL started using name ids from 0 again. We fixed this issue by storing information, including the types table and name ids state in the Artifacts data structure that is returned when we run the pipeline for the first time. This information is then used when we call functions to compile / type check REPL expressions. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-03-30 14:39:27 +03:00
runM
Support module imports in Juvix REPL (#2029) This PR adds support for importing modules from within a Juvix project in the Juvix REPL. The imported module is checked (parsed, arity-checked, type-checked etc) as normal and added to the REPL session scope. Any errors during the checking phase is reported to the user. ### Notes: * You must load a file before using `import`. This is because the REPL needs to know which Juvix project is active. * You may only import modules from within the same Juvix project. ### Examples After launching `juvix repl`: #### `open import` ``` Stdlib.Prelude> open import Stdlib.Data.Int.Ord Stdlib.Prelude> 1 == 1 true ``` #### `import as` ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int Stdlib.Prelude> 1 Int.== 1 true ``` #### `import`then `open` ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int Stdlib.Prelude> open Int Stdlib.Prelude> 1 == 1 true ``` #### Line-terminating semicolons are ignored: ``` Stdlib.Prelude> import Stdlib.Data.Int.Ord as Int;;;;; Stdlib.Prelude> 1 Int.== 1 true ``` * Closes https://github.com/anoma/juvix/issues/1951 --------- Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
2023-05-08 13:23:15 +03:00
. runState (ctx ^. replContextArtifacts)
. runReader (ctx ^. replContextEntryPoint)
$ do
r <- compileReplInputIO replPath txt
return (extractNode <$> r)
where
extractNode :: ReplPipelineResult -> Maybe Core.Node
extractNode = \case
ReplPipelineResultNode n -> Just n
ReplPipelineResultImport {} -> Nothing
Allow open statements in let expressions (#2395) - Closes #2185
2023-10-03 00:13:45 +03:00
ReplPipelineResultOpen {} -> Nothing
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Compute new entrypoint root when loading a file in the REPL (#1615) * Add shelltests for `juvix repl` * repl: Compute entrypoint root when loading a file Previously the REPL would use app root (which could be the current directory or the project root of the initially loaded file). Thus files in a different project could not be loaded. The entrypoint root must be computed each time a new file is `:load`ed. Adds shell-tests for REPL commands * Move preludePath to Juvix.Extra.Paths
2022-11-10 14:26:38 +03:00
render' :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
render' t = do
opts <- State.gets (^. replStateGlobalOptions)
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stdout)
liftIO (P.renderIO (not (opts ^. globalNoColors) && hasAnsi) t)
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
replNewline :: Repl ()
replNewline = liftIO (putStrLn "")
Compute new entrypoint root when loading a file in the REPL (#1615) * Add shelltests for `juvix repl` * repl: Compute entrypoint root when loading a file Previously the REPL would use app root (which could be the current directory or the project root of the initially loaded file). Thus files in a different project could not be loaded. The entrypoint root must be computed each time a new file is `:load`ed. Adds shell-tests for REPL commands * Move preludePath to Juvix.Extra.Paths
2022-11-10 14:26:38 +03:00
renderOut :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
renderOut = render'
renderOutLn :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
renderOutLn t = renderOut t >> replNewline
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
Add `:def` command to the repl (#2119) This pr adds a new command, `:def` to the repl. This command expects a single identifier that must be in scope and then prints its definition. For constructors, the whole type definition is printed. It also applies some refactors to the code for repl command. 1. Before there was a mega `where` block of definitions. I have hoisted most of the definitions there to the top level. I feel like now it is easier to navigate and read. 2. Use `ExceptT` instead of local `case` expressions for errors. 3. Use forks of `haskeline` and `repline`. These forks are necessary because these libraries do not export the constructors `HaskelineT` and `InputT` respectively, thus, making it impossible to catch errors in their underlying monad.
2023-05-30 11:19:09 +03:00
printErrorS :: JuvixError -> ReplS ()
printErrorS e = do
Compute new entrypoint root when loading a file in the REPL (#1615) * Add shelltests for `juvix repl` * repl: Compute entrypoint root when loading a file Previously the REPL would use app root (which could be the current directory or the project root of the initially loaded file). Thus files in a different project could not be loaded. The entrypoint root must be computed each time a new file is `:load`ed. Adds shell-tests for REPL commands * Move preludePath to Juvix.Extra.Paths
2022-11-10 14:26:38 +03:00
opts <- State.gets (^. replStateGlobalOptions)
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stderr)
Add translation from Internal to Core (#1567)
2022-11-07 16:47:56 +03:00
liftIO $ hPutStrLn stderr $ run (runReader (project' @GenericOptions opts) (Error.render (not (opts ^. globalNoColors) && hasAnsi) False e))
Fix REPL state to include enough information to rerun the pipeline (#1911) Previously we were: * discarding the types table * discarding the name ids state after processing an expression in the REPL. For example evaluating: ``` let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10 ``` would loop in the REPL. We noticed that the `n` in `suc n` was being given type `Type` instead of `Nat`. This was because the name id given to n was incorrect, the REPL started using name ids from 0 again. We fixed this issue by storing information, including the types table and name ids state in the Artifacts data structure that is returned when we run the pipeline for the first time. This information is then used when we call functions to compile / type check REPL expressions. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-03-30 14:39:27 +03:00
runTransformations ::
repl: Run disambiguateNames on result node (#1961) There were two bugs here: 1. The _replNoDisambiguate option was set to True for `juvix repl`. 2. The disambiguateNames pass was being applied after the result node had already been fetched from the infotable. * Closes https://github.com/anoma/juvix/issues/1958
2023-04-03 11:58:08 +03:00
forall r.
Update ci to use ormolu 0.5.3.0 and reformat project (#2313) Updates ormolu to 0.5.3.0 and formats the project
2023-08-25 19:37:23 +03:00
(Members '[State Artifacts, Error JuvixError, Reader EntryPoint] r) =>
repl: Run disambiguateNames on result node (#1961) There were two bugs here: 1. The _replNoDisambiguate option was set to True for `juvix repl`. 2. The disambiguateNames pass was being applied after the result node had already been fetched from the infotable. * Closes https://github.com/anoma/juvix/issues/1958
2023-04-03 11:58:08 +03:00
Bool ->
Fix REPL state to include enough information to rerun the pipeline (#1911) Previously we were: * discarding the types table * discarding the name ids state after processing an expression in the REPL. For example evaluating: ``` let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10 ``` would loop in the REPL. We noticed that the `n` in `suc n` was being given type `Type` instead of `Nat`. This was because the name id given to n was incorrect, the REPL started using name ids from 0 again. We fixed this issue by storing information, including the types table and name ids state in the Artifacts data structure that is returned when we run the pipeline for the first time. This information is then used when we call functions to compile / type check REPL expressions. --------- Co-authored-by: Paul Cadman <git@paulcadman.dev>
2023-03-30 14:39:27 +03:00
[Core.TransformationId] ->
Core.Node ->
Sem r Core.Node
repl: Run disambiguateNames on result node (#1961) There were two bugs here: 1. The _replNoDisambiguate option was set to True for `juvix repl`. 2. The disambiguateNames pass was being applied after the result node had already been fetched from the infotable. * Closes https://github.com/anoma/juvix/issues/1958
2023-04-03 11:58:08 +03:00
runTransformations shouldDisambiguate ts n = runCoreInfoTableBuilderArtifacts $ do
sym <- addNode n
applyTransforms shouldDisambiguate ts
getNode sym
where
addNode :: Core.Node -> Sem (Core.InfoTableBuilder ': r) Core.Symbol
addNode node = do
sym <- Core.freshSymbol
Core.registerIdentNode sym node
-- `n` will get filtered out by the transformations unless it has a
-- corresponding entry in `infoIdentifiers`
tab <- Core.getInfoTable
let name = Core.freshIdentName tab "_repl"
idenInfo =
Core.IdentifierInfo
{ _identifierName = name,
_identifierSymbol = sym,
_identifierLocation = Nothing,
_identifierArgsNum = 0,
_identifierType = Core.mkDynamic',
_identifierIsExported = False,
Add: pragma support (#1997) * Closes #1965 * Implements the `unroll` pragma to control the unrolling depth on a per-function basis. * Implements parsing of the `inline` pragma. --------- Co-authored-by: janmasrovira <janmasrovira@gmail.com>
2023-04-26 16:26:13 +03:00
_identifierBuiltin = Nothing,
Allow to specify VampIR variable names (#2141) * Closes #2134 Adds the `argnames` pragma which specifies function argument names. These will be the names used in Core and subsequently in VampIR for the `main` function. ``` {-# argnames: [x, y] -#} main : Nat -> Nat -> Nat; ```
2023-06-01 18:36:47 +03:00
_identifierPragmas = mempty,
_identifierArgNames = []
repl: Run disambiguateNames on result node (#1961) There were two bugs here: 1. The _replNoDisambiguate option was set to True for `juvix repl`. 2. The disambiguateNames pass was being applied after the result node had already been fetched from the infotable. * Closes https://github.com/anoma/juvix/issues/1958
2023-04-03 11:58:08 +03:00
}
Core.registerIdent name idenInfo
return sym
applyTransforms :: Bool -> [Core.TransformationId] -> Sem (Core.InfoTableBuilder ': r) ()
applyTransforms shouldDisambiguate' ts' = do
tab <- Core.getInfoTable
tab' <- mapReader Core.fromEntryPoint $ Core.applyTransformations ts' tab
let tab'' =
if
| shouldDisambiguate' -> disambiguateNames tab'
| otherwise -> tab'
Core.setInfoTable tab''
getNode :: Core.Symbol -> Sem (Core.InfoTableBuilder ': r) Core.Node
Refactor Core datastructures (#1975) * Closes #1972 * Introduces lookup functions for the InfoTable to avoid using HashMap explicitly and reduce code duplication
2023-04-04 19:58:05 +03:00
getNode sym = fromMaybe impossible . flip Core.lookupIdentifierNode' sym <$> Core.getInfoTable
Reference in New Issue Copy Permalink