-
Notifications
You must be signed in to change notification settings - Fork 373
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Allow expression evaluation in files similar to Lean4's #eval #2503
Comments
Isn't |
I think so, but it would only require one line instead of two and would not require a name. Perhaps elaborator reflection would be a better way to achieve that. |
The IDE protocol supports a message for normalising a term. Can this proposed feature be reduced to normalise term (which isn't yet implemented in idris2)? |
It has similar functionality to normalize term. I suppose it could be implemented in comments without Idris2 support.
and LSP independently parse the file to find However, this would complicate showing errors, semantic highlighting, and hover on the contents of the input. |
It looks like You can consider addition of a function like |
If you can |
@mattpolzin Not that I know of. As far as I know |
@buzden close but not quite
|
In Agda it's legal to name a throwaway toplevel definition
Is it not? If I type an expression in the REPL it'll be evaluated. |
|
I don't like that it's a top-level pragma. That feels unprincipled: surely there are cases where I'd like to evaluate in a context? Now that @ohad has clarified (privately) what he means by normalising an expression (essentially: automatically e.g. using
would mean that on top of syntax highlighting messages stating that:
we would also get some metadata telling us You should then be able to define e.g.
and write your top-level evaluation tests as
|
I guess my original plan for evaluate in context would be to have the user select text and trigger an evaluate in context action. I'm still trying to decide if your idea is better. Can you describe a situation where evaluating in a context would be useful? |
One example comes up in @madman-bob 's work on tabular data. We have operations on tabular data that change the schema: result : Table ?hole
result = join students grades ["name", "age"] and when you search/refine result : Table ([< "name" :! String, "age" :! Nat, "matriculation year" :! Nat] ++ [< "name" :! String, "age" :! Nat, "linear algebra 1" :< Nat, "introduction to programming with Idris" :< Nat] |-| ["name", "age"])
result = join students grades ["name", "age"] Which you'd then want to normalise into: result : Table ([< "name" :! String, "age" :! Nat, "matriculation year" :! Nat, "linear algebra 1" :< Nat, "introduction to programming with Idris" :< Nat]) |
Based on that use case, I feel my select and action idea would make the most sense for evaluating in a context. Is there a case where you would want continuous feedback on evaluating in a context like I am proposing with |
Summary
In a Lean file
displays
4
.It would be nice if Idris had something similar.
Motivation
Using a REPL requires manually loading the file and running the expression on every change. This would allow continuous automatic feedback. This design is stateless which makes reasoning about it easier.
The proposal
#eval
would evaluate the expression that followsExample
In a
.idr
filewould allow something like
= 4
would be displayed in the editor after the expression.Technical implementation
A field with
PosMap (NonEmptyFC, DocIdris Ann)
could be added toMetadata
. I'm not sure what the type of the result should be. PotentiallyREPLResult
or something else would be better.While traversing the definitions in a file, these evaluations would be computed and the results would be stored in the
PosMap
.Alternatives considered
Potential Extensions
If this is positively received, I may extend it to replicate other REPL functionality directly in a file. Also, perhaps clicking on the result could turn in to an assertion. Something like
%eval 2 + 2
to%asserteval (2 + 2) = 4
, but I haven't thought much about that yet.Conclusion
I'm not certain if this is the best approach, but I have been unable to think of anything better.
Related Issue on the LSP: idris-community/idris2-lsp#129
The text was updated successfully, but these errors were encountered: