From 491629caa7d3d539dcd577ac2b437882bcf72636 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 +- .../reflection/reflection022/NoEscape.idr | 16 +++++++++ .../reflection/reflection022/NoEscapePar.idr | 35 +++++++++++++++++++ .../reflection/reflection022/RunElab0.idr | 13 +++++++ .../idris2/reflection/reflection022/expected | 3 ++ tests/idris2/reflection/reflection022/run | 5 +++ 9 files changed, 90 insertions(+), 3 deletions(-) create mode 100644 tests/idris2/reflection/reflection022/NoEscape.idr create mode 100644 tests/idris2/reflection/reflection022/NoEscapePar.idr create mode 100644 tests/idris2/reflection/reflection022/RunElab0.idr create mode 100644 tests/idris2/reflection/reflection022/expected create mode 100755 tests/idris2/reflection/reflection022/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 d50a5b4d659..e18e51e319d 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 f3edfbd4fdb..2e45c9082db 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 12e84e4525e..786f20eae7a 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/idris2/reflection/reflection022/NoEscape.idr b/tests/idris2/reflection/reflection022/NoEscape.idr new file mode 100644 index 00000000000..3a5b50c33a9 --- /dev/null +++ b/tests/idris2/reflection/reflection022/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/reflection/reflection022/NoEscapePar.idr b/tests/idris2/reflection/reflection022/NoEscapePar.idr new file mode 100644 index 00000000000..1f37d7de66f --- /dev/null +++ b/tests/idris2/reflection/reflection022/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/reflection/reflection022/RunElab0.idr b/tests/idris2/reflection/reflection022/RunElab0.idr new file mode 100644 index 00000000000..c72996546bc --- /dev/null +++ b/tests/idris2/reflection/reflection022/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/reflection/reflection022/expected b/tests/idris2/reflection/reflection022/expected new file mode 100644 index 00000000000..28bf1ab381a --- /dev/null +++ b/tests/idris2/reflection/reflection022/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/reflection/reflection022/run b/tests/idris2/reflection/reflection022/run new file mode 100755 index 00000000000..d08d68d0627 --- /dev/null +++ b/tests/idris2/reflection/reflection022/run @@ -0,0 +1,5 @@ +. ../../../testutils.sh + +check RunElab0.idr +check NoEscape.idr +check NoEscapePar.idr