[ elab ] Make %runElab expressions have unrestricted quantity

Author: buzden

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

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) ->

src/TTImp/Elab/RunElab.idr

@@ -211,7 +211,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))

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

tests/Main.idr

@@ -211,7 +211,7 @@ idrisTests = MkTestPool "Misc" [] Nothing
        -- Quotation and reflection
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
-       "reflection009", "reflection010", "reflection011",
+       "reflection009", "reflection010", "reflection011", "reflection012",
        -- The 'with' rule
        "with001", "with002", "with004", "with005", "with006",
        -- with-disambiguation

tests/idris2/reflection012/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

tests/idris2/reflection012/expected

@@ -0,0 +1 @@
+1/1: Building RunElab0 (RunElab0.idr)

tests/idris2/reflection012/run

@@ -0,0 +1,3 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check RunElab0.idr