Make :typeat a useful command #998
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
More generally, save the types of any variable found in the nested names. In these cases, the lookup would return Just and getNameType, a function that also added the variable to the metadata, was not called. Now the Nothing case also adds it. This affects primarily vars defined in where clauses and in let clauses that had an explicit type.
'let's that bind a variable with the same name and value as an already existing one (essentially 'let x = x in ...') clutter the type of variables bound in where clauses, as their type can depend on the value of the arguments to the function.
Now it is much clearer what happens on each of the possibilities: global result or not X local result or not.
The previous behavior was to not show anything when there were both a global and a local definition for that name.
Will allow for a more exact mapping from names in the file to their types.
Previously, the file context for the type signature as a whole would be used for the name of the function, making TypeAt anywhere within the signature return the type of the function, instead of the type of the name the cursor was on. With this commit, a file context just for the function name is properly tracked and used. This required updating a test for reflection, as the ITy node can now have an additional file context, passed as `EmptyFC` in the test.
More specifically, let bindings without type signatures that don't pattern match. This requires storing an additional file context with the ILet RawImp constructor.
This makes is much easier to debug problems related to names in the metadata by showing which function adds the name. It's convenient to use it in isolation with `%logging metadata.names 7`. Logging level 7 was chosen pretty much arbitrarily
The file context for the desugared bind used to cover everything inside the expression, preventing TypeAt from showing types of variables like f and x in '!(f x)'.
The variables generated by desugaring the record update syntax were incorrectly using the file context of the whole expression, obstructing the file contexts of names inside the update or to which the update was being applied. This also deletes the unused `get` function
For example, :typeat in the name `x` in ``` f : a f = do let x = 5 ?a ``` used to give UndefinedName. Now, the type of the variable is correctly reported. `let`s that pattern matched on the variable already worked properly as they use the constructor DoLetPat and it's `PTerm`s already hold the necessary file contexts.
When desugaring a `PLam` (high level syntax lambda), a variable called "lamc" is created. Previously, it was using the file context of the argument to the lambda, obstructing the variables bound by the argument pattern in the metadata. Now, "lamc" has an empty file context (`EmptyFC`) as should all variables that don't exist in the original file (those that are generated by the compiler).
That is, `x` and `y` in `(\x, y => ?r)`. Those are now included in the metadata for interactive editing, and :typeat can now report their types properly (no more UndefinedName).
Now that variables bound by lambdas are added to the metadata, any lambdas generated by the desugaring process (those that don't exist in the source file) must have an empty file context (`EmptyFC`), otherwise compiler generated names enter the metadata and pollute the interactive editing commands (mainly :typeat).
Now the name to the left of the arrow in a bind (inside a do block) is properly placed in the metadata. When lambdas started adding their arguments to the metadata, the lhs of do binds (that desugar to lambdas) automatically started being added as well, although with a file context that corresponds to the whole expression (the left and the right of the `<-` arrow), obstructing the types of variables at the rhs. This fixes this problem.
It's necessary that compiler generated variables and lambdas that bind compiler generated variables have empty file contexts, otherwise they pollute the metadata with names that don't actually exist in the source file. An underscore variable is generated by desugaring a do bind that pattern matches in the left side of the arrow, `S n <- ?x` for example. It was being created with a non empty file context, covering expressions on the right side of the arrow as well.
`checkApp` was using the file context for the whole application as the file context for the variable being applied. This sometimes made :typeat report the type of a function when asked the type of an argument to such function. This was what was causing the test for :typeat with !-syntax to fail.
Those ended up polluting the type of variables declared in a let with a type signature inside a do block if there was previously a pattern matching bind in the block. Now all tests for :typeat pass.
This required storing an extra file context that refers to the position of the name in the PAs and IAs nodes. For example, it's now possible to use the :typeat command to get the type of `x` in: ``` f : Maybe Nat -> Nat f x@(Just _) = 1 f Nothing = 0 ```
This removes the file contexts of some compiler generated nodes when elaborating interface definitions and interface implementations, cleaning up the metadata a bit.
For this purpose, a `NonEmptyFC` type was created, a type for file contexts that cannot be empty. The projections from `FC` were replaced by projections from `NonEmptyFC`, as the original ones had to "silently" return values such as empty string and zero when called on an empty file context in order to satisfy the type signature. The functions that relied on the old projections now handle the EmptyFC case explicitly.
The projections generated in the elaboration process were using file contexts that referred to the whole definition, preventing :typeat from working inside the record definition.
The test itself is currently very very simple.
The command still ends up showing some compiler generated variables when using the new record update syntax (The one that doesn' need the `record` keyword), so there are no tests for those yet.
|
I've taken a look at the "build-api" job, and it looks like it's using the previous version to build and test the api of the current version, which seems a bit odd. Shouldn't the current version be the one required to build and work with the api? I've tested by pushing to a separate branch and if "build-api" is changed to use the artifact "idris2-nightly" (the current version) the test passes. However, I still couldn't understand why building the api with the previous version fails when the TTC version is increased. I can't imagine how the different versions get messed up if the current version of idris2 is not even installed at that point. (But there is always the possibility I understood the job wrong). |
|
#1030 should do it. Here is a merged run I did: https://github.com/Russoul/Idris2/runs/1833442179 |
|
Oh, sorry for taking so long here, looks like you took over. I had the start of the refactoring already done locally, I should have communicated better. Regardless, thanks for taking a look at the "build-api" problems, gallais and Russoul! |
|
We were starting to get merge conflicts so I figured I'd better get on |
|
Planning to merge this tomorrow afternoon. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Overview
The
:typeatcommand is very simple: It takes the cursor position in the file and then shows the type of the name under it. It works by using thenamesfield of the metadata: It is a mapping from file contexts, a type that holds a file name and start and end positions in the file, to the name and type of the variable.It is different from the regular
:tin that:tgets the information from the global definitions and thus doesn't work for local variables.The problem was that the
namesfield of the metadata was really messy. It was missing some stuff and also including some nodes that don't actually exist in the source code, making:typeatwork pretty poorly. This PR is about cleaning up some file context stuff to populate the metadata accurately and then be able to get types of local variables with:typeat.Note: I'm currently using the command through my fork of idris2-vim. I've submitted a pull request to include the changes in the main repo.
Improvements
whereandletletbindingsdobindingsAppnodes when evaluating to normal formFixes
:typeatwork within type signatures:typeatwork within !-notation:typeatwork around record update syntax:typeatwork within record definitionsI've also added tests for most of the fixes and improvements.
Breaking changes
Some of the modifications require storing more file context information in AST nodes. This means it's a breaking change for Elaborator Reflection, but fixing existing code is just a matter of adding more
EmptyFC.Since the nodes are saved to TTC, I'm pretty sure I should increase the TTC version. However, when I push the commit that does it, the "build-api" ci job fails (I've left it there so you can see the problem). Maybe it's not set up to handle a TTC version increase. Can someone help me figure out how to get it working?
Performance benchmarks
To make sure things were not made slower, I timed how long it took for each version of Idris2 (master and my branch typeat) to build master. This time I did an average of 5 builds to be a bit more precise. In the end, building using the branch with the changes took on average 1.6% longer, which I'd say is acceptable.
Things that are still broken
I also ran into some other problems, but I decided to leave them as is in order to not make this PR any longer than it already is. They are:
?_ [no locals in scope]as the type