From dfe6f0e38e59c6fd3eb2cbe7010ff26f95169156 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sun, 17 Oct 2021 21:17:07 +0300 Subject: [PATCH] [ elab ] Make `%runElab` expressions to have unrestricted quantity --- src/Algebra/Preorder.idr | 6 ++++ src/Algebra/ZeroOneOmega.idr | 8 +++++ src/TTImp/Elab/RunElab.idr | 4 +-- src/TTImp/ProcessRunElab.idr | 3 +- tests/Main.idr | 3 +- tests/idris2/reflection021/NoEscape.idr | 16 ++++++++++ tests/idris2/reflection021/NoEscapePar.idr | 35 ++++++++++++++++++++++ tests/idris2/reflection021/RunElab0.idr | 13 ++++++++ tests/idris2/reflection021/expected | 3 ++ tests/idris2/reflection021/run | 5 ++++ 10 files changed, 92 insertions(+), 4 deletions(-) create mode 100644 tests/idris2/reflection021/NoEscape.idr create mode 100644 tests/idris2/reflection021/NoEscapePar.idr create mode 100644 tests/idris2/reflection021/RunElab0.idr create mode 100644 tests/idris2/reflection021/expected create mode 100755 tests/idris2/reflection021/run diff --git a/src/Algebra/Preorder.idr b/src/Algebra/Preorder.idr index 385c5861a2..ed9176c526 100644 --- a/src/Algebra/Preorder.idr +++ b/src/Algebra/Preorder.idr @@ -29,3 +29,9 @@ public export interface Preorder a => Top a where top : a topAbs : {x : a} -> x <= top = True + +||| The least bound of a bounded lattice +public export +interface Preorder a => Bot a where + bot : a + botAbs : {x : a} -> bot <= x = True diff --git a/src/Algebra/ZeroOneOmega.idr b/src/Algebra/ZeroOneOmega.idr index d50a5b4d65..e18e51e319 100644 --- a/src/Algebra/ZeroOneOmega.idr +++ b/src/Algebra/ZeroOneOmega.idr @@ -72,6 +72,14 @@ Top ZeroOneOmega where topAbs {x = Rig1} = Refl topAbs {x = RigW} = Refl +||| The bottom value of a lattice +export +Bot ZeroOneOmega where + bot = Rig0 + botAbs {x = Rig0} = Refl + botAbs {x = Rig1} = Refl + botAbs {x = RigW} = Refl + ---------------------------------------- rigPlusAssociative : (x, y, z : ZeroOneOmega) -> diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index f3edfbd4fd..2e45c9082d 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -254,8 +254,8 @@ checkRunElab rig elabinfo nest env fc script exp throw (GenericMsg fc "%language ElabReflection not enabled") let n = NS reflectionNS (UN $ Basic "Elab") elabtt <- appCon fc defs n [expected] - (stm, sty) <- runDelays (const True) $ - check rig elabinfo nest env script (Just (gnf env elabtt)) + (stm, _) <- runDelays (const True) $ + check bot elabinfo nest env script (Just (gnf env elabtt)) solveConstraints inTerm Normal defs <- get Ctxt -- checking might have resolved some holes ntm <- elabScript rig fc nest env diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr index 12e84e4525..786f20eae7 100644 --- a/src/TTImp/ProcessRunElab.idr +++ b/src/TTImp/ProcessRunElab.idr @@ -38,5 +38,6 @@ processRunElab eopts nest env fc tm unit <- getCon fc defs (builtin "Unit") exp <- appCon fc defs n [unit] - stm <- checkTerm tidx InExpr eopts nest env tm (gnf env exp) + e <- newRef EST $ initEStateSub tidx env SubRefl + (stm, _) <- check bot (initElabInfo InExpr) nest env tm $ Just $ gnf env exp ignore $ elabScript top fc nest env !(nfOpts withAll defs env stm) Nothing diff --git a/tests/Main.idr b/tests/Main.idr index 0944e6e618..1ff4fdd64f 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -250,7 +250,8 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing "reflection005", "reflection006", "reflection007", "reflection008", "reflection009", "reflection010", "reflection011", "reflection012", "reflection013", "reflection014", "reflection015", "reflection016", - "reflection017", "reflection018", "reflection019", "reflection020"] + "reflection017", "reflection018", "reflection019", "reflection020", + "reflection021"] idrisTestsWith : TestPool idrisTestsWith = MkTestPool "With abstraction" [] Nothing diff --git a/tests/idris2/reflection021/NoEscape.idr b/tests/idris2/reflection021/NoEscape.idr new file mode 100644 index 0000000000..3a5b50c33a --- /dev/null +++ b/tests/idris2/reflection021/NoEscape.idr @@ -0,0 +1,16 @@ +module NoEscape + +import Language.Reflection + +%language ElabReflection + +0 n : Nat +n = 3 + +0 elabScript : Elab Nat +elabScript = pure n + +failing "n is not accessible in this context" + + m : Nat + m = %runElab elabScript diff --git a/tests/idris2/reflection021/NoEscapePar.idr b/tests/idris2/reflection021/NoEscapePar.idr new file mode 100644 index 0000000000..1f37d7de66 --- /dev/null +++ b/tests/idris2/reflection021/NoEscapePar.idr @@ -0,0 +1,35 @@ +||| Check that we cannot implement function illegally escaping zero quantity using elaboration reflection +module NoEscapePar + +import Language.Reflection + +%language ElabReflection + +escScr : Elab $ (0 _ : a) -> a +escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x) + +failing "x is not accessible in this context" + + esc : (0 _ : a) -> a + esc = %runElab escScr + +escd : (0 _ : a) -> a + +0 escd' : (0 _ : a) -> a + +escDecl : Name -> Elab Unit +escDecl name = declare [ + IDef EmptyFC name [ + PatClause EmptyFC + -- lhs + (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x")) + -- rhs + `(x) + ] + ] + +%runElab escDecl `{escd'} + +failing "x is not accessible in this context" + + %runElab escDecl `{escd} diff --git a/tests/idris2/reflection021/RunElab0.idr b/tests/idris2/reflection021/RunElab0.idr new file mode 100644 index 0000000000..c72996546b --- /dev/null +++ b/tests/idris2/reflection021/RunElab0.idr @@ -0,0 +1,13 @@ +module RunElab0 + +import Language.Reflection + +%language ElabReflection + +0 elabScript : Elab Unit +elabScript = pure () + +x : Unit +x = %runElab elabScript + +%runElab elabScript diff --git a/tests/idris2/reflection021/expected b/tests/idris2/reflection021/expected new file mode 100644 index 0000000000..28bf1ab381 --- /dev/null +++ b/tests/idris2/reflection021/expected @@ -0,0 +1,3 @@ +1/1: Building RunElab0 (RunElab0.idr) +1/1: Building NoEscape (NoEscape.idr) +1/1: Building NoEscapePar (NoEscapePar.idr) diff --git a/tests/idris2/reflection021/run b/tests/idris2/reflection021/run new file mode 100755 index 0000000000..eba72d16a1 --- /dev/null +++ b/tests/idris2/reflection021/run @@ -0,0 +1,5 @@ +rm -rf build + +$1 --no-color --console-width 0 --check RunElab0.idr +$1 --no-color --console-width 0 --check NoEscape.idr +$1 --no-color --console-width 0 --check NoEscapePar.idr