From 3ae7ce027c03e0c8dbb3ef7071206f61ce50f4f6 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 | 2 +- src/TTImp/ProcessRunElab.idr | 2 +- tests/Main.idr | 1 + tests/idris2/reflection013/NoEscape.idr | 14 +++++++++ tests/idris2/reflection013/NoEscapePar.idr | 31 ++++++++++++++++++++ tests/idris2/reflection013/RunElab0.idr | 13 +++++++++ tests/idris2/reflection013/expected | 33 ++++++++++++++++++++++ tests/idris2/reflection013/run | 5 ++++ 10 files changed, 113 insertions(+), 2 deletions(-) create mode 100644 tests/idris2/reflection013/NoEscape.idr create mode 100644 tests/idris2/reflection013/NoEscapePar.idr create mode 100644 tests/idris2/reflection013/RunElab0.idr create mode 100644 tests/idris2/reflection013/expected create mode 100755 tests/idris2/reflection013/run diff --git a/src/Algebra/Preorder.idr b/src/Algebra/Preorder.idr index 385c5861a22..ed9176c526f 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 da0f1c6478c..b1558ec354d 100644 --- a/src/Algebra/ZeroOneOmega.idr +++ b/src/Algebra/ZeroOneOmega.idr @@ -70,6 +70,14 @@ Top ZeroOneOmega where topAbs {x = Rig1} = Refl topAbs {x = RigW} = Refl +||| The bottm 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 f163e1f855a..266e6cc7187 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/src/TTImp/Elab/RunElab.idr @@ -236,7 +236,7 @@ checkRunElab rig elabinfo nest env fc script exp let ttn = reflectiontt "TT" elabtt <- appCon fc defs n [expected] (stm, sty) <- runDelays (const True) $ - check rig elabinfo nest env script (Just (gnf env elabtt)) + check bot elabinfo nest env script (Just (gnf env elabtt)) defs <- get Ctxt -- checking might have resolved some holes ntm <- elabScript fc nest env !(nfOpts withAll defs env stm) (Just (gnf env expected)) diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr index 4e8553bea4a..ec8aa0a43fd 100644 --- a/src/TTImp/ProcessRunElab.idr +++ b/src/TTImp/ProcessRunElab.idr @@ -36,5 +36,5 @@ 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) + stm <- checkTerm tidx InType eopts nest env tm (gnf env exp) ignore $ elabScript fc nest env !(nfOpts withAll defs env stm) Nothing diff --git a/tests/Main.idr b/tests/Main.idr index e001b1fbe54..62bec169247 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -214,6 +214,7 @@ idrisTests = MkTestPool "Misc" [] Nothing "reflection001", "reflection002", "reflection003", "reflection004", "reflection005", "reflection006", "reflection007", "reflection008", "reflection009", "reflection010", "reflection011", "reflection012", + "reflection013", -- The 'with' rule "with001", "with002", "with004", "with005", "with006", -- with-disambiguation diff --git a/tests/idris2/reflection013/NoEscape.idr b/tests/idris2/reflection013/NoEscape.idr new file mode 100644 index 00000000000..d825cf5de7a --- /dev/null +++ b/tests/idris2/reflection013/NoEscape.idr @@ -0,0 +1,14 @@ +module NoEscape + +import Language.Reflection + +%language ElabReflection + +0 n : Nat +n = 3 + +0 elabScript : Elab Nat +elabScript = pure n + +m : Nat +m = %runElab elabScript diff --git a/tests/idris2/reflection013/NoEscapePar.idr b/tests/idris2/reflection013/NoEscapePar.idr new file mode 100644 index 00000000000..693ef4e9862 --- /dev/null +++ b/tests/idris2/reflection013/NoEscapePar.idr @@ -0,0 +1,31 @@ +||| 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) + +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'} + +%runElab escDecl `{escd} diff --git a/tests/idris2/reflection013/RunElab0.idr b/tests/idris2/reflection013/RunElab0.idr new file mode 100644 index 00000000000..c72996546bc --- /dev/null +++ b/tests/idris2/reflection013/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/reflection013/expected b/tests/idris2/reflection013/expected new file mode 100644 index 00000000000..94f15a2d72c --- /dev/null +++ b/tests/idris2/reflection013/expected @@ -0,0 +1,33 @@ +1/1: Building RunElab0 (RunElab0.idr) +1/1: Building NoEscape (NoEscape.idr) +Error: While processing right hand side of m. NoEscape.n is not accessible in this context. + +NoEscape:11:19--11:20 + 07 | 0 n : Nat + 08 | n = 3 + 09 | + 10 | 0 elabScript : Elab Nat + 11 | elabScript = pure n + ^ + +1/1: Building NoEscapePar (NoEscapePar.idr) +Error: While processing right hand side of esc. x is not accessible in this context. + +NoEscape:9:65--9:66 + 5 | + 6 | %language ElabReflection + 7 | + 8 | escScr : Elab $ (0 _ : a) -> a + 9 | escScr = check $ ILam EmptyFC M0 ExplicitArg (Just `{x}) `(a) `(x) + ^ + +Error: While processing right hand side of escd. x is not accessible in this context. + +NoEscape:25:24--25:25 + 21 | PatClause EmptyFC + 22 | -- lhs + 23 | (IApp EmptyFC (IVar EmptyFC name) (IBindVar EmptyFC "x")) + 24 | -- rhs + 25 | `(x) + ^ + diff --git a/tests/idris2/reflection013/run b/tests/idris2/reflection013/run new file mode 100755 index 00000000000..eba72d16a13 --- /dev/null +++ b/tests/idris2/reflection013/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