Skip to content

Commit

Permalink
[ elab ] Make %runElab expressions to have unrestricted quantity
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Dec 30, 2023
1 parent 2f2102c commit de82e35
Show file tree
Hide file tree
Showing 10 changed files with 93 additions and 3 deletions.
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,9 @@

### Compiler changes

* Elaborator script's expression under the `%runElab` is not typechecked in the context
of quantity `0`, because it is present and works only at compile time

### Library changes

#### Prelude
Expand Down
6 changes: 6 additions & 0 deletions src/Algebra/Preorder.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
8 changes: 8 additions & 0 deletions src/Algebra/ZeroOneOmega.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down
4 changes: 2 additions & 2 deletions src/TTImp/Elab/RunElab.idr
Original file line number Diff line number Diff line change
Expand Up @@ -353,8 +353,8 @@ checkRunElab rig elabinfo nest env fc reqExt 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
Expand Down
3 changes: 2 additions & 1 deletion src/TTImp/ProcessRunElab.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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
16 changes: 16 additions & 0 deletions tests/idris2/reflection/reflection027/NoEscape.idr
Original file line number Diff line number Diff line change
@@ -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
35 changes: 35 additions & 0 deletions tests/idris2/reflection/reflection027/NoEscapePar.idr
Original file line number Diff line number Diff line change
@@ -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}
13 changes: 13 additions & 0 deletions tests/idris2/reflection/reflection027/RunElab0.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
module RunElab0

import Language.Reflection

%language ElabReflection

0 elabScript : Elab Unit
elabScript = pure ()

x : Unit
x = %runElab elabScript

%runElab elabScript
3 changes: 3 additions & 0 deletions tests/idris2/reflection/reflection027/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
1/1: Building RunElab0 (RunElab0.idr)
1/1: Building NoEscape (NoEscape.idr)
1/1: Building NoEscapePar (NoEscapePar.idr)
5 changes: 5 additions & 0 deletions tests/idris2/reflection/reflection027/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
. ../../../testutils.sh

check RunElab0.idr
check NoEscape.idr
check NoEscapePar.idr

0 comments on commit de82e35

Please sign in to comment.