idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-20 17:57:38 +03:00
Code Issues Projects Releases Wiki Activity

Missing runElab decl check

Browse Source
This commit is contained in:
Giuseppe Lomurno 2020-09-15 23:29:48 +02:00 committed by G. Allais
parent 3c24bc5ed5
commit 98e54cea2f
4 changed files with 27 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/TTImp/Elab/RunElab.idr
View File

@ -179,7 +179,7 @@ checkRunElab : {vars : _} ->
checkRunElab rig elabinfo nest env fc script exp
= do expected <- mkExpected exp
defs <- get Ctxt
when (not (isExtension ElabReflection defs)) $
unless (isExtension ElabReflection defs) $
throw (GenericMsg fc "%language ElabReflection not enabled")
let n = NS reflectionNS (UN "Elab")
let ttn = reflectiontt "TT"

3
src/TTImp/ProcessRunElab.idr
View File

@ -4,6 +4,7 @@ import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Options
import Core.Normalise
import Core.Reflect
import Core.UnifyState
@ -25,6 +26,8 @@ processRunElab : {vars : _} ->
RawImp -> Core ()
processRunElab eopts nest env fc tm
= do defs <- get Ctxt
unless (isExtension ElabReflection defs) $
throw (GenericMsg fc "%language ElabReflection not enabled")
tidx <- resolveName (UN "[elaborator script]")
let n = NS reflectionNS (UN "Elab")
unit <- getCon fc defs (builtin "Unit")

14
tests/idris2/reflection001/expected
View File

@ -7,6 +7,20 @@ quote.idr:25:19--25:22
25 | xfn ~(val))
| ^^^
Error: %language ElabReflection not enabled
quote.idr:33:1--33:21
|
33 | %runElab noExtension
| ^^^^^^^^^^^^^^^^^^^^
Error: Error during reflection: Should not print this message
quote.idr:37:1--37:21
|
37 | %runElab noExtension
| ^^^^^^^^^^^^^^^^^^^^
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IApp (MkFC "quote.idr" (6, 13) (6, 14)) (IVar (MkFC "quote.idr" (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC "quote.idr" (6, 18) (6, 19)) (IVar (MkFC "quote.idr" (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 18) (6, 19)) (BI 4)))
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False"))
Main> ILocal (MkFC "quote.idr" (10, 8) (12, 22)) [IClaim (MkFC "quote.idr" (10, 12) (11, 15)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994)))))

9
tests/idris2/reflection001/quote.idr
View File

@ -26,3 +26,12 @@ bad val
names : List Name
names = [ `{{ names }}, `{{ Prelude.(+) }} ]
noExtension : Elab ()
noExtension = fail "Should not print this message"
%runElab noExtension
%language ElabReflection
%runElab noExtension