diff --git a/CHANGELOG.md b/CHANGELOG.md index e0e411d6b62..0a81b52bd73 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 087af856929..51835016635 100644 --- a/src/Core/Binary.idr +++ b/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 () diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 140b046f58b..d8aa6e32df2 100644 --- a/src/Idris/Desugar.idr +++ b/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 diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 85ccd0b6bb4..47b02b54bb4 100644 --- a/src/Idris/Resugar.idr +++ b/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) diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 3e45e772cd7..09567214c7c 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/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 diff --git a/src/TTImp/Elab/RunElab.idr b/src/TTImp/Elab/RunElab.idr index f3edfbd4fdb..05515a3d568 100644 --- a/src/TTImp/Elab/RunElab.idr +++ b/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] diff --git a/src/TTImp/Elab/Term.idr b/src/TTImp/Elab/Term.idr index a552d20f391..b0a49bc7f84 100644 --- a/src/TTImp/Elab/Term.idr +++ b/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 diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index cc007cbf0d2..edf9d4ce173 100644 --- a/src/TTImp/Reflect.idr +++ b/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 diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 71f68579407..979fa054236 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -112,7 +112,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 @@ -200,7 +200,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 ++ ")" @@ -601,7 +601,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) @@ -637,7 +637,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 @@ -870,7 +870,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 diff --git a/src/TTImp/TTImp/Functor.idr b/src/TTImp/TTImp/Functor.idr index 8504c72f394..55452ed4d11 100644 --- a/src/TTImp/TTImp/Functor.idr +++ b/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) diff --git a/src/TTImp/TTImp/TTC.idr b/src/TTImp/TTImp/TTC.idr index 4548995c57a..c4521b194c1 100644 --- a/src/TTImp/TTImp/TTC.idr +++ b/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) diff --git a/src/TTImp/TTImp/Traversals.idr b/src/TTImp/TTImp/Traversals.idr index 110d684213c..8f63e5fe8d2 100644 --- a/src/TTImp/TTImp/Traversals.idr +++ b/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 diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 5fa57d8f337..9f7f562c1fc 100644 --- a/src/TTImp/Utils.idr +++ b/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 : diff --git a/tests/Main.idr b/tests/Main.idr index e30b721df24..be41bf236f3 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -254,7 +254,7 @@ idrisTestsReflection = MkTestPool "Quotation and Reflection" [] Nothing "reflection009", "reflection010", "reflection011", "reflection012", "reflection013", "reflection014", "reflection015", "reflection016", "reflection017", "reflection018", "reflection019", "reflection020", - "reflection021"] + "reflection021", "reflection022"] idrisTestsWith : TestPool idrisTestsWith = MkTestPool "With abstraction" [] Nothing diff --git a/tests/idris2/reflection022/DeclMacro.idr b/tests/idris2/reflection022/DeclMacro.idr new file mode 100644 index 00000000000..17c06852441 --- /dev/null +++ b/tests/idris2/reflection022/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 diff --git a/tests/idris2/reflection022/UseMacroWithoutExtension.idr b/tests/idris2/reflection022/UseMacroWithoutExtension.idr new file mode 100644 index 00000000000..53807aba5c3 --- /dev/null +++ b/tests/idris2/reflection022/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 diff --git a/tests/idris2/reflection022/expected b/tests/idris2/reflection022/expected new file mode 100644 index 00000000000..4f5eed7b642 --- /dev/null +++ b/tests/idris2/reflection022/expected @@ -0,0 +1,2 @@ +1/2: Building DeclMacro (DeclMacro.idr) +2/2: Building UseMacroWithoutExtension (UseMacroWithoutExtension.idr) diff --git a/tests/idris2/reflection022/run b/tests/idris2/reflection022/run new file mode 100644 index 00000000000..63a90724a41 --- /dev/null +++ b/tests/idris2/reflection022/run @@ -0,0 +1,3 @@ +rm -rf build + +$1 --no-color --console-width 0 --no-banner --check UseMacroWithoutExtension.idr diff --git a/tests/idris2/reflection022/test.ipkg b/tests/idris2/reflection022/test.ipkg new file mode 100644 index 00000000000..2c5b5ab52de --- /dev/null +++ b/tests/idris2/reflection022/test.ipkg @@ -0,0 +1 @@ +package a-test