1
1
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-26 13:11:30 +03:00
Commit Graph

6 Commits

Author SHA1 Message Date
G. Allais
c1ebc0535d
[ new ] semantic highlighting in REPL & holes () 2021-08-13 16:00:54 +01:00
Edwin Brady
f303e469fb Improve elaborator reflection performance
In a 'Bind', normalise the result of the first action, rather than
quoting the HNF. This improves performance since the HNF could be quite
big when quoted back.

Ideally, we wouldn't have to quote and unquote here, and we can probably
achieve this by tinkering with the evaluator.

This has an unfortunate effect on the reflection002 test, in that the
"typed template Idris" example now evaluates too much. But, I think the
overall performance is too important for the primary motivation
behind elaborator reflection. I will return to this!
2020-07-17 15:18:23 +01:00
Edwin Brady
c682ded9c4 Reduce amount of normalisation in elab scripts
We don't want to unfold definitions in 'pure' or 'check' or 'bind' since
we want the exact expression that the script author has used.
2020-06-03 00:22:03 +01:00
Edwin Brady
d8d13d912e Add alternative example to reflection002
A bit more typesafe...
2020-06-02 23:56:30 +01:00
Edwin Brady
2a75731916 In reflection, check now takes a concrete type
So the type of Elab now gives the expected type that's being elaborated
to, meaning that we can run 'check' in the middle of scripts and use the
result.
2020-06-02 22:41:37 +01:00
Edwin Brady
85c002c771 Progress on elaborator reflection
Add %runElab and start on scripts, although all they can do so far is
check a term. This does gives us, sort of, "template Idris" (as
demonstrated in test reflection002)
2020-05-31 01:36:54 +01:00