diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index bb19d1dc8..7fe18dd6a 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -53,10 +53,10 @@ elabScript : {vars : _} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> - FC -> NestedNames vars -> + RigCount -> FC -> NestedNames vars -> Env Term vars -> NF vars -> Maybe (Glued vars) -> Core (NF vars) -elabScript fc nest env script@(NDCon nfc nm t ar args) exp +elabScript rig fc nest env script@(NDCon nfc nm t ar args) exp = do defs <- get Ctxt fnm <- toFullNames nm case fnm of @@ -91,12 +91,12 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp -- 2) Evaluate the resulting act -- 3) apply k to the result of (2) -- 4) Run elabScript on the result stripping off Elab - = do act <- elabScript fc nest env + = do act <- elabScript rig fc nest env !(evalClosure defs act) exp act <- quote defs env act k <- evalClosure defs k r <- applyToStack defs withAll env k [(getLoc act, toClosure withAll env act)] - elabScript fc nest env r exp + elabScript rig fc nest env r exp elabCon defs "Fail" [_, mbfc, msg] = do msg' <- evalClosure defs msg let customFC = case !(evalClosure defs mbfc >>= reify defs) of @@ -105,13 +105,13 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp throw $ RunElabFail $ GenericMsg customFC !(reify defs msg') elabCon defs "Try" [_, elab1, elab2] = tryUnify (do constart <- getNextEntry - res <- elabScript fc nest env !(evalClosure defs elab1) exp + res <- elabScript rig fc nest env !(evalClosure defs elab1) exp -- We ensure that all of the constraints introduced during the elab script -- have been solved. This guarantees that we do not mistakenly succeed even -- though e.g. a proof search got delayed. solveConstraintsAfter constart inTerm LastChance pure res) - (elabScript fc nest env !(evalClosure defs elab2) exp) + (elabScript rig fc nest env !(evalClosure defs elab2) exp) elabCon defs "LogMsg" [topic, verb, str] = do topic' <- evalClosure defs topic verb' <- evalClosure defs verb @@ -143,7 +143,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp tidx <- resolveName (UN $ Basic "[elaborator script]") e <- newRef EST (initEState tidx env) (checktm, _) <- runDelays (const True) $ - check top (initElabInfo InExpr) nest env !(reify defs ttimp') + check rig (initElabInfo InExpr) nest env !(reify defs ttimp') (Just (glueBack defs env exp')) empty <- clearDefs defs nf empty env checktm @@ -164,7 +164,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp qty <- quote empty env ty let env' = Lam fc' c qp qty :: env - runsc <- elabScript fc (weaken nest) env' + runsc <- elabScript rig fc (weaken nest) env' !(nf defs env' lamsc) Nothing -- (map weaken exp) nf empty env (Bind bfc x (Lam fc' c qp qty) !(quote empty env' runsc)) where @@ -224,7 +224,7 @@ elabScript fc nest env script@(NDCon nfc nm t ar args) exp scriptRet () elabCon defs n args = failWith defs $ "unexpected Elab constructor " ++ n ++ ", or incorrect count of arguments: " ++ show (length args) -elabScript fc nest env script exp +elabScript rig fc nest env script exp = do defs <- get Ctxt empty <- clearDefs defs throw (BadRunElab fc env !(quote empty env script) "script is not a data value") @@ -252,7 +252,7 @@ checkRunElab rig elabinfo nest env fc script exp check rig elabinfo nest env script (Just (gnf env elabtt)) solveConstraints inTerm Normal defs <- get Ctxt -- checking might have resolved some holes - ntm <- elabScript fc nest env + ntm <- elabScript rig fc nest env !(nfOpts withAll defs env stm) (Just (gnf env expected)) defs <- get Ctxt -- might have updated as part of the script empty <- clearDefs defs diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr index 487538577..12e84e452 100644 --- a/src/TTImp/ProcessRunElab.idr +++ b/src/TTImp/ProcessRunElab.idr @@ -39,4 +39,4 @@ processRunElab eopts nest env fc tm exp <- appCon fc defs n [unit] stm <- checkTerm tidx InExpr eopts nest env tm (gnf env exp) - ignore $ elabScript fc nest env !(nfOpts withAll defs env stm) Nothing + ignore $ elabScript top fc nest env !(nfOpts withAll defs env stm) Nothing diff --git a/tests/Main.idr b/tests/Main.idr index 92466741f..294740308 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -231,7 +231,8 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing ["reflection001", "reflection002", "reflection003", "reflection004", "reflection005", "reflection006", "reflection007", "reflection008", "reflection009", "reflection010", "reflection011", "reflection012", - "reflection013", "reflection014", "reflection015", "reflection016"] + "reflection013", "reflection014", "reflection015", "reflection016", + "reflection017"] idrisTestsWith : TestPool idrisTestsWith = MkTestPool "With abstraction" [] Nothing diff --git a/tests/idris2/reflection017/CanElabType.idr b/tests/idris2/reflection017/CanElabType.idr new file mode 100644 index 000000000..e114178c6 --- /dev/null +++ b/tests/idris2/reflection017/CanElabType.idr @@ -0,0 +1,36 @@ +module CanElabType + +import Data.Vect + +import Language.Reflection + +%language ElabReflection + +0 T : Nat -> Type +T n = Vect n Nat + +desiredType : TTImp +desiredType = IApp EmptyFC (IVar EmptyFC `{CanElabType.T}) `(3) + +elabDecl : Name -> Elab Unit +elabDecl n = declare [ + IClaim EmptyFC MW Public [] $ MkTy EmptyFC EmptyFC n desiredType + ] + +%runElab elabDecl `{x1} +x1 = [1, 2, 3] + +export +elabExpr : Elab Type +elabExpr = check desiredType + +-- should typecheck because the rig of calling is zero + +x2 : %runElab elabExpr +x2 = [1, 2, 3] + +-- Check that zero can't escape +failing "CanElabType.T is not accessible in this context" + + T' : Type + T' = %runElab elabExpr diff --git a/tests/idris2/reflection017/StillCantEscape.idr b/tests/idris2/reflection017/StillCantEscape.idr new file mode 100644 index 000000000..fca2c50f6 --- /dev/null +++ b/tests/idris2/reflection017/StillCantEscape.idr @@ -0,0 +1,13 @@ +module StillCantEscape + +import CanElabType + +import Language.Reflection + +%language ElabReflection + +-- check that zero does not leak, should not typecheck +failing "CanElabType.T is private" + + T' : Type + T' = %runElab elabExpr diff --git a/tests/idris2/reflection017/expected b/tests/idris2/reflection017/expected new file mode 100644 index 000000000..4177d203f --- /dev/null +++ b/tests/idris2/reflection017/expected @@ -0,0 +1,2 @@ +1/1: Building CanElabType (CanElabType.idr) +2/2: Building StillCantEscape (StillCantEscape.idr) diff --git a/tests/idris2/reflection017/run b/tests/idris2/reflection017/run new file mode 100755 index 000000000..42f9e04a6 --- /dev/null +++ b/tests/idris2/reflection017/run @@ -0,0 +1,4 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner --check CanElabType.idr +$1 --no-color --console-width 0 --no-banner --check StillCantEscape.idr