git.iko.soy/Idris-dev
on master help sign in
Apply Nat optimisation for :exec

This is an important missing step because otherwise expressions containing Nats can't be run with :exec Fixes #3610

commit96076832a09547af9d4b10298e7f25f22b51a62d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 8 Mar 2017, 09:59 (10 years ago) parentdf7cb1a
1 file changed+3−1
compare with master
unifiedsplit
src/Idris/REPL.hs+3−1
src/Idris/REPL.hs+3−1
@@ -46,6 +46,7 @@ import Idris.Core.TT
4646import Idris.Core.Unify
4747import Idris.Core.WHNF
4848import Idris.Coverage
49+import Idris.DataOpts
4950import Idris.Delaborate
5051import Idris.Docs
5152import Idris.Docstrings (overview, renderDocTerm, renderDocstring)
@@ -1236,7 +1237,8 @@ process fn (TestInline t)
12361237process fn (Execute tm)
12371238 = idrisCatch
12381239 (do ist <- getIState
1239− (m, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS (elabExec fc tm)
1240+ (m_in, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS (elabExec fc tm)
1241+ m <- applyOpts m_in
12401242 (tmpn, tmph) <- runIO $ tempfile ""
12411243 runIO $ hClose tmph
12421244 t <- codegen