[ elab ] Make %macro-function be callable without the ElabReflection extension

CHANGELOG.md

@@ -17,8 +17,9 @@
   [#1066](https://github.com/idris-lang/idris2/issues/1066)).
 * `%hide` directives can now hide conflicting fixities from other modules.
 * Fixity declarations can now be kept private with export modifiers.
-* New fromTTImp, fromName, and fromDecls names for custom TTImp, Name, and Decls
-  literals.
+* New `fromTTImp`, `fromName`, and `fromDecls` names for custom `TTImp`,
+  `Name`, and `Decls` literals.
+* Call to `%macro`-functions do not require the `ElabReflection` extension.
 
 ### REPL changes
 

src/Core/Binary.idr

@@ -25,11 +25,11 @@ import public Libraries.Utils.Binary
 %default covering
 
 ||| TTC files can only be compatible if the version number is the same
-||| Update with the current date in YYYYMMDD format, or bump the auxiliary
+||| Update with the current date in YYYY_MM_DD_00 format, or bump the auxiliary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 20230829 * 100 + 0
+ttcVersion = 2023_09_04_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Idris/Desugar.idr

@@ -372,7 +372,7 @@ mutual
   desugarB side ps (PUnquote fc tm)
       = pure $ IUnquote fc !(desugarB side ps tm)
   desugarB side ps (PRunElab fc tm)
-      = pure $ IRunElab fc !(desugarB side ps tm)
+      = pure $ IRunElab fc True !(desugarB side ps tm)
   desugarB side ps (PHole fc br holename)
       = do when br $ update Syn { bracketholes $= ((UN (Basic holename)) ::) }
            pure $ IHole fc holename

src/Idris/Resugar.idr

@@ -389,7 +389,7 @@ mutual
       = do ds' <- traverse toPDecl ds
            pure $ PQuoteDecl fc (catMaybes ds')
   toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
-  toPTerm p (IRunElab fc tm) = pure (PRunElab fc !(toPTerm argPrec tm))
+  toPTerm p (IRunElab fc _ tm) = pure (PRunElab fc !(toPTerm argPrec tm))
 
   toPTerm p (IUnifyLog fc _ tm) = toPTerm p tm
   toPTerm p (Implicit fc True) = pure (PImplicit fc)

src/TTImp/Elab/Ambiguity.idr

@@ -145,7 +145,7 @@ expandAmbigName mode nest env orig args (IVar fc x) exp
         = if (Context.Macro `elem` flags def) && notLHS mode
              then alternativeFirstSuccess $ reverse $
                     allSplits args <&> \(macroArgs, extArgs) =>
-                      (IRunElab fc $ ICoerced fc $ IVar fc n `buildAlt` macroArgs) `buildAlt` extArgs
+                      (IRunElab fc False $ ICoerced fc $ IVar fc n `buildAlt` macroArgs) `buildAlt` extArgs
              else wrapDot prim est mode n (map (snd . snd) args)
                     (definition def) (buildAlt (IVar fc n) args)
       where

src/TTImp/Elab/RunElab.idr

@@ -245,12 +245,12 @@ checkRunElab : {vars : _} ->
                {auto o : Ref ROpts REPLOpts} ->
                RigCount -> ElabInfo ->
                NestedNames vars -> Env Term vars ->
-               FC -> RawImp -> Maybe (Glued vars) ->
+               FC -> (requireExtension : Bool) -> RawImp -> Maybe (Glued vars) ->
                Core (Term vars, Glued vars)
-checkRunElab rig elabinfo nest env fc script exp
+checkRunElab rig elabinfo nest env fc reqExt script exp
     = do expected <- mkExpected exp
          defs <- get Ctxt
-         unless (isExtension ElabReflection defs) $
+         unless (not reqExt || isExtension ElabReflection defs) $
              throw (GenericMsg fc "%language ElabReflection not enabled")
          let n = NS reflectionNS (UN $ Basic "Elab")
          elabtt <- appCon fc defs n [expected]

src/TTImp/Elab/Term.idr

@@ -204,8 +204,8 @@ checkTerm rig elabinfo nest env (IQuoteDecl fc ds) exp
     = checkQuoteDecl rig elabinfo nest env fc ds exp
 checkTerm rig elabinfo nest env (IUnquote fc tm) exp
     = throw (GenericMsg fc "Can't escape outside a quoted term")
-checkTerm rig elabinfo nest env (IRunElab fc tm) exp
-    = checkRunElab rig elabinfo nest env fc tm exp
+checkTerm rig elabinfo nest env (IRunElab fc re tm) exp
+    = checkRunElab rig elabinfo nest env fc re tm exp
 checkTerm {vars} rig elabinfo nest env (IPrimVal fc c) exp
     = do let (cval, cty) = checkPrim {vars} fc c
          checkExp rig elabinfo env fc cval (gnf env cty) exp

src/TTImp/Reflect.idr

@@ -607,7 +607,7 @@ mutual
         = pure (Ref tfc Bound t)
     reflect fc defs lhs env (IUnquote tfc t)
         = throw (InternalError "Can't reflect an unquote: escapes should be lifted out")
-    reflect fc defs lhs env (IRunElab tfc t)
+    reflect fc defs lhs env (IRunElab tfc _ t)
         = throw (InternalError "Can't reflect a %runElab")
     reflect fc defs lhs env (IPrimVal tfc t)
         = do fc' <- reflect fc defs lhs env tfc

src/TTImp/TTImp.idr

@@ -119,7 +119,7 @@ mutual
        IQuoteName : FC -> Name -> RawImp' nm
        IQuoteDecl : FC -> List (ImpDecl' nm) -> RawImp' nm
        IUnquote : FC -> RawImp' nm -> RawImp' nm
-       IRunElab : FC -> RawImp' nm -> RawImp' nm
+       IRunElab : FC -> (requireExtension : Bool) -> RawImp' nm -> RawImp' nm
 
        IPrimVal : FC -> (c : Constant) -> RawImp' nm
        IType : FC -> RawImp' nm
@@ -207,7 +207,7 @@ mutual
       show (IQuoteName fc tm) = "(%quotename " ++ show tm ++ ")"
       show (IQuoteDecl fc tm) = "(%quotedecl " ++ show tm ++ ")"
       show (IUnquote fc tm) = "(%unquote " ++ show tm ++ ")"
-      show (IRunElab fc tm) = "(%runelab " ++ show tm ++ ")"
+      show (IRunElab fc _ tm) = "(%runelab " ++ show tm ++ ")"
       show (IPrimVal fc c) = show c
       show (IHole _ x) = "?" ++ x
       show (IUnifyLog _ lvl x) = "(%logging " ++ show lvl ++ " " ++ show x ++ ")"
@@ -608,7 +608,7 @@ findIBinds (IDelay fc tm) = findIBinds tm
 findIBinds (IForce fc tm) = findIBinds tm
 findIBinds (IQuote fc tm) = findIBinds tm
 findIBinds (IUnquote fc tm) = findIBinds tm
-findIBinds (IRunElab fc tm) = findIBinds tm
+findIBinds (IRunElab fc _ tm) = findIBinds tm
 findIBinds (IBindHere _ _ tm) = findIBinds tm
 findIBinds (IBindVar _ n) = [n]
 findIBinds (IUpdate fc updates tm)
@@ -644,7 +644,7 @@ findImplicits (IDelay fc tm) = findImplicits tm
 findImplicits (IForce fc tm) = findImplicits tm
 findImplicits (IQuote fc tm) = findImplicits tm
 findImplicits (IUnquote fc tm) = findImplicits tm
-findImplicits (IRunElab fc tm) = findImplicits tm
+findImplicits (IRunElab fc _ tm) = findImplicits tm
 findImplicits (IBindVar _ n) = [n]
 findImplicits (IUpdate fc updates tm)
     = findImplicits tm ++ concatMap (findImplicits . getFieldUpdateTerm) updates
@@ -877,7 +877,7 @@ getFC (IQuote x _) = x
 getFC (IQuoteName x _) = x
 getFC (IQuoteDecl x _) = x
 getFC (IUnquote x _) = x
-getFC (IRunElab x _) = x
+getFC (IRunElab x _ _) = x
 getFC (IAs x _ _ _ _) = x
 getFC (Implicit x _) = x
 getFC (IWithUnambigNames x _ _) = x

src/TTImp/TTImp/Functor.idr

@@ -62,8 +62,8 @@ mutual
       = IQuoteDecl fc (map (map f) ds)
     map f (IUnquote fc t)
       = IUnquote fc (map f t)
-    map f (IRunElab fc t)
-      = IRunElab fc (map f t)
+    map f (IRunElab fc re t)
+      = IRunElab fc re (map f t)
     map f (IPrimVal fc c)
       = IPrimVal fc c
     map f (IType fc)

src/TTImp/TTImp/TTC.idr

@@ -72,8 +72,8 @@ mutual
         = do tag 23; toBuf b fc; toBuf b t
     toBuf b (IUnquote fc t)
         = do tag 24; toBuf b fc; toBuf b t
-    toBuf b (IRunElab fc t)
-        = do tag 25; toBuf b fc; toBuf b t
+    toBuf b (IRunElab fc re t)
+        = do tag 25; toBuf b fc; toBuf b re; toBuf b t
 
     toBuf b (IPrimVal fc y)
         = do tag 26; toBuf b fc; toBuf b y
@@ -164,8 +164,8 @@ mutual
                         pure (IQuoteDecl fc y)
                24 => do fc <- fromBuf b; y <- fromBuf b
                         pure (IUnquote fc y)
-               25 => do fc <- fromBuf b; y <- fromBuf b
-                        pure (IRunElab fc y)
+               25 => do fc <- fromBuf b; re <- fromBuf b; y <- fromBuf b
+                        pure (IRunElab fc re y)
 
                26 => do fc <- fromBuf b; y <- fromBuf b
                         pure (IPrimVal fc y)

src/TTImp/TTImp/Traversals.idr

@@ -119,7 +119,7 @@ parameters (f : RawImp' nm -> RawImp' nm)
   mapTTImp (IQuoteName fc n) = f $ IQuoteName fc n
   mapTTImp (IQuoteDecl fc xs) = f $ IQuoteDecl fc (assert_total $ map mapImpDecl xs)
   mapTTImp (IUnquote fc t) = f $ IUnquote fc (mapTTImp t)
-  mapTTImp (IRunElab fc t) = f $ IRunElab fc (mapTTImp t)
+  mapTTImp (IRunElab fc re t) = f $ IRunElab fc re (mapTTImp t)
   mapTTImp (IPrimVal fc c) = f $ IPrimVal fc c
   mapTTImp (IType fc) = f $ IType fc
   mapTTImp (IHole fc str) = f $ IHole fc str

src/TTImp/Utils.idr

@@ -187,7 +187,7 @@ findBindableNamesQuot env used (IUnifyLog fc k x)
 findBindableNamesQuot env used (IQuote fc x) = []
 findBindableNamesQuot env used (IQuoteName fc x) = []
 findBindableNamesQuot env used (IQuoteDecl fc xs) = []
-findBindableNamesQuot env used (IRunElab fc x) = []
+findBindableNamesQuot env used (IRunElab fc _ x) = []
 
 export
 findUniqueBindableNames :

tests/idris2/reflection/reflection023/DeclMacro.idr

@@ -0,0 +1,11 @@
+module DeclMacro
+
+import public Language.Reflection
+
+export %macro
+macroFun : Nat -> Elab Nat
+macroFun x = pure $ x + 1
+
+export
+justScript : Nat -> Elab Nat
+justScript x = pure $ x + 2

tests/idris2/reflection/reflection023/UseMacroWithoutExtension.idr

@@ -0,0 +1,14 @@
+module UseMacroWithoutExtension
+
+import DeclMacro
+
+useMacro : Nat
+useMacro = macroFun 5
+
+useMacroCorr : UseMacroWithoutExtension.useMacro = 6
+useMacroCorr = Refl
+
+failing "%language ElabReflection not enabled"
+
+  stillCan'tUseRunElabWithoutExtension : Nat
+  stillCan'tUseRunElabWithoutExtension = %runElab justScript 4

tests/idris2/reflection/reflection023/expected

@@ -0,0 +1,2 @@
+1/2: Building DeclMacro (DeclMacro.idr)
+2/2: Building UseMacroWithoutExtension (UseMacroWithoutExtension.idr)

tests/idris2/reflection/reflection023/run

@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check UseMacroWithoutExtension.idr

tests/idris2/reflection/reflection023/test.ipkg

@@ -0,0 +1 @@
+package a-test