mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Check delay is allowed before delaying
We can't nest delayed elaborators (this is an efficiency constraint, to prevent excessive searching for ambiguous names) to run elaborator immediately if delays aren't allowed in delayElab
This commit is contained in:
parent
a9895771ab
commit
0d5dc8cc26
@ -18,6 +18,7 @@ beyond work on the language core, are (in no particular order):
|
||||
- Syntax highlighting support for output
|
||||
- Several functions from the version 1 IDE protocol are not yet implemented,
|
||||
and I haven't confirmed it works in everything.
|
||||
- (Not really part of Idris 2, but an editing mode for vim would be lovely!)
|
||||
* Some parts of the Idris 1 Prelude are not yet implemented and should be
|
||||
added to base/
|
||||
* Partial evaluation, especially for specialisation of interface
|
||||
@ -26,7 +27,6 @@ beyond work on the language core, are (in no particular order):
|
||||
errors would be good.
|
||||
- In particular, large sections commented out with {- -} can take a while
|
||||
to lex!
|
||||
* Windows support - it is tested on macOS and Linux only so far.
|
||||
* An alternative, high performance, back end. OCaml seems worth a try.
|
||||
* JS and Node back ends would be nice.
|
||||
|
||||
|
8
Makefile
8
Makefile
@ -22,13 +22,13 @@ base: prelude
|
||||
|
||||
libs : prelude base
|
||||
|
||||
clean: lib_clean
|
||||
clean: clean-libs
|
||||
make -C src clean
|
||||
make -C tests clean
|
||||
rm -f runtests
|
||||
rm -f idris2
|
||||
|
||||
lib_clean:
|
||||
clean-libs:
|
||||
make -C libs/prelude clean
|
||||
make -C libs/base clean
|
||||
|
||||
@ -36,7 +36,9 @@ test:
|
||||
idris --build tests.ipkg
|
||||
make -C tests
|
||||
|
||||
install: all install-libs
|
||||
install: all install-exec install-libs
|
||||
|
||||
install-exec: idris2
|
||||
install idris2 ${PREFIX}/bin
|
||||
install support/chez/* ${PREFIX}/idris2/support/chez
|
||||
install support/chicken/* ${PREFIX}/idris2/support/chicken
|
||||
|
@ -60,6 +60,7 @@ delayOnFailure fc rig env expected pred elab
|
||||
do nm <- genName "delayed"
|
||||
(ci, dtm) <- newDelayed fc Rig1 env nm !(getTerm expected)
|
||||
logGlueNF 5 ("Postponing elaborator " ++ show nm ++
|
||||
" at " ++ show fc ++
|
||||
" for") env expected
|
||||
log 10 ("Due to error " ++ show err)
|
||||
ust <- get UST
|
||||
@ -86,22 +87,25 @@ delayElab : {auto c : Ref Ctxt Defs} ->
|
||||
Core (Term vars, Glued vars)
|
||||
delayElab {vars} fc rig env exp elab
|
||||
= do est <- get EST
|
||||
nm <- genName "delayed"
|
||||
expected <- mkExpected exp
|
||||
(ci, dtm) <- newDelayed fc Rig1 env nm !(getTerm expected)
|
||||
logGlueNF 5 ("Postponing elaborator " ++ show nm ++
|
||||
" for") env expected
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab $=
|
||||
((ci, mkClosedElab fc env
|
||||
(do est <- get EST
|
||||
put EST (record { allowDelay = False } est)
|
||||
tm <- elab
|
||||
est <- get EST
|
||||
put EST (record { allowDelay = True } est)
|
||||
pure tm)) :: ) }
|
||||
ust)
|
||||
pure (dtm, expected)
|
||||
if not (allowDelay est)
|
||||
then elab
|
||||
else do
|
||||
nm <- genName "delayed"
|
||||
expected <- mkExpected exp
|
||||
(ci, dtm) <- newDelayed fc Rig1 env nm !(getTerm expected)
|
||||
logGlueNF 5 ("Postponing elaborator " ++ show nm ++
|
||||
" for") env expected
|
||||
ust <- get UST
|
||||
put UST (record { delayedElab $=
|
||||
((ci, mkClosedElab fc env
|
||||
(do est <- get EST
|
||||
put EST (record { allowDelay = False } est)
|
||||
tm <- elab
|
||||
est <- get EST
|
||||
put EST (record { allowDelay = True } est)
|
||||
pure tm)) :: ) }
|
||||
ust)
|
||||
pure (dtm, expected)
|
||||
where
|
||||
mkExpected : Maybe (Glued vars) -> Core (Glued vars)
|
||||
mkExpected (Just ty) = pure ty
|
||||
@ -121,6 +125,7 @@ retryDelayed ((i, elab) :: ds)
|
||||
= do defs <- get Ctxt
|
||||
Just Delayed <- lookupDefExact (Resolved i) (gamma defs)
|
||||
| _ => retryDelayed ds
|
||||
log 5 ("Retrying delayed hole " ++ show !(getFullName (Resolved i)))
|
||||
tm <- elab
|
||||
updateDef (Resolved i) (const (Just
|
||||
(PMDef True [] (STerm tm) (STerm tm) [])))
|
||||
|
Loading…
Reference in New Issue
Block a user