Open michaelmesser opened 2 years ago
Isn't %asserteval
just a Refl
proof?
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.
--%eval 2 + 2
and LSP independently parse the file to find --%
commands (does the Idris API expose comments or would LSP have to parse them on its own?) and Idris API functions to evaluate them.
However, this would complicate showing errors, semantic highlighting, and hover on the contents of the input.
It looks like %runElab logMsg "" 0 $ show $ 2 + 2
does exactly what you want except for additional logging-related printing.
You can consider addition of a function like print : Show a => a -> m Unit
to the Elaboration
interface and then expression %runElab print $ 2 + 2
would do what you want from %eval 2 + 2
mostly reusing what's already in the compiler.
If you can %runElab $ print …
then can’t you make print
(or whatever you want to name the function) into a macro and get exactly the syntax %print …
? Never done it before, but thought I saw a test case that did something like this once.
@mattpolzin Not that I know of. As far as I know %marco f
will expand f
to %runElab f
in an expression, but not at the top level.
@buzden close but not quite
logMsg
to show up inline in their editorI think so, but it would only require one line instead of two and would not require a name.
In Agda it's legal to name a throwaway toplevel definition _
precisely so that you can write
tests without polluting the scope. I'd rather add this principled thing than a new pragma. The
one line vs. two is moot as it's legal to write ; _ = Refl
at the end.
Can this proposed feature be reduced to normalise term (which isn't yet implemented in idris2)?
Is it not? If I type an expression in the REPL it'll be evaluated.
In Agda it's legal to name a throwaway toplevel definition precisely so that you can write tests without polluting the scope. I'd rather add this principled thing than a new pragma. The one line vs. two is moot as it's legal to write ; = Refl at the end.
%asserteval
is probably not needed then.
Is it not? If I type an expression in the REPL it'll be evaluated.
%eval
is intended have the same behavior as evaluating an expression at the REPL, but the interface would be very different. Are you saying %eval
isn't needed at all? Or, that I should do --%eval
and have LSP call normalize term on the expression? Or something else?
Are you saying %eval isn't needed at all? Or, that I should do --%eval and have LSP call normalize term on the expression? Or something else?
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 replacing a span of code in the source file with what it normalises to), I can see a design: some kind of open+close span tokens that delimit a subexpression & provokes the compiler to generate extra metadata annotations associated to that span.
e.g. using (|
and |)
as the opening & closing tokens for the sake of argument
test : (n : Nat) -> 3 + n === (| 3 + n |)
test n = Refl
would mean that on top of syntax highlighting messages stating that:
test
is a functionNat
and (===)
are type constructors3
and Refl
are data constructorsn
is a bound variable of type Nat
we would also get some metadata telling us 3 + n
at location so-and-so reduces to S (S (S n))
.
The client can then decide to replace the expression by its normal form, display it in a bubble or whatever else it wants.
You should then be able to define e.g.
data Eval : a -> Type where
and write your top-level evaluation tests as
_ : Eval (| 2 + 2 |)
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?
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 hole
you get:
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 %eval
?
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: https://github.com/idris-community/idris2-lsp/issues/129