acfe1d1a4b
This PR enforces that Verso docstring extensions should always be meta at attribute application time, giving better error messages, and ensures that the generated argument parser helper is also meta and has the same visibility.
162 lines
4.5 KiB
Text
162 lines
4.5 KiB
Text
module
|
|
|
|
public import Lean
|
|
|
|
/-!
|
|
This file tests that custom Verso docstring extensions work in `module`s. The `@[doc_role]`,
|
|
`@[doc_code_block]`, `@[doc_directive]`, and `@[doc_command]` attributes should:
|
|
|
|
1. Enforce that the underlying definition is `meta` (since it is used during elaboration).
|
|
|
|
2. Work correctly. In particular, they should generate the `getArgs` wrapper as `meta`.
|
|
-/
|
|
|
|
set_option doc.verso true
|
|
|
|
open Lean Doc Elab Term
|
|
|
|
@[doc_role]
|
|
meta def r (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
|
|
return .empty
|
|
|
|
@[doc_code_block]
|
|
meta def c (s : StrLit) : DocM (Block ElabInline ElabBlock) :=
|
|
pure (Block.code (s.getString.toList.reverse |> String.ofList))
|
|
|
|
@[doc_directive]
|
|
meta def d (s : TSyntaxArray `block) : DocM (Block ElabInline ElabBlock) := do
|
|
.concat <$> s.reverse.mapM elabBlock
|
|
|
|
@[doc_command]
|
|
meta def cmd (_ : Ident) : DocM (Block ElabInline ElabBlock) := do
|
|
return .empty
|
|
|
|
/-- Uses the custom role: {r}`role here` -/
|
|
def useRole := ()
|
|
|
|
open Lean Elab Command in
|
|
/-- info: Uses the custom role: -/
|
|
#guard_msgs in
|
|
#eval show CommandElabM Unit from do
|
|
IO.print (← findDocString? (← getEnv) ``useRole).get!
|
|
|
|
/--
|
|
Uses the custom code block:
|
|
|
|
```c
|
|
hello
|
|
```
|
|
-/
|
|
def useCodeBlock := ()
|
|
|
|
open Lean Elab Command in
|
|
/--
|
|
info: Uses the custom code block:
|
|
|
|
```
|
|
|
|
olleh
|
|
```
|
|
-/
|
|
#guard_msgs in
|
|
#eval show CommandElabM Unit from do
|
|
IO.print (← findDocString? (← getEnv) ``useCodeBlock).get!
|
|
|
|
/--
|
|
Uses the custom directive:
|
|
|
|
:::d
|
|
|
|
text
|
|
|
|
:::
|
|
-/
|
|
def useDirective := ()
|
|
|
|
open Lean Elab Command in
|
|
/--
|
|
info: Uses the custom directive:
|
|
|
|
text
|
|
-/
|
|
#guard_msgs in
|
|
#eval show CommandElabM Unit from do
|
|
IO.print (← findDocString? (← getEnv) ``useDirective).get!
|
|
|
|
/--
|
|
Uses the custom command:
|
|
|
|
{cmd Foo}
|
|
-/
|
|
def useCommand := ()
|
|
|
|
open Lean Elab Command in
|
|
/-- info: Uses the custom command: -/
|
|
#guard_msgs in
|
|
#eval show CommandElabM Unit from do
|
|
IO.print (← findDocString? (← getEnv) ``useCommand).get!
|
|
|
|
-- Each attribute should refuse to apply to a definition that is not `meta`, since the generated
|
|
-- `.getArgs` wrapper is invoked at elaboration time.
|
|
|
|
def notMetaRole (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
|
|
return .empty
|
|
|
|
/-- error: `notMetaRole` must be marked `meta` to be used as a docstring role -/
|
|
#guard_msgs in
|
|
attribute [doc_role] notMetaRole
|
|
|
|
def notMetaCodeBlock (s : StrLit) : DocM (Block ElabInline ElabBlock) :=
|
|
pure (Block.code s.getString)
|
|
|
|
/-- error: `notMetaCodeBlock` must be marked `meta` to be used as a docstring code block -/
|
|
#guard_msgs in
|
|
attribute [doc_code_block] notMetaCodeBlock
|
|
|
|
def notMetaDirective (s : TSyntaxArray `block) : DocM (Block ElabInline ElabBlock) := do
|
|
.concat <$> s.mapM elabBlock
|
|
|
|
/-- error: `notMetaDirective` must be marked `meta` to be used as a docstring directive -/
|
|
#guard_msgs in
|
|
attribute [doc_directive] notMetaDirective
|
|
|
|
def notMetaCommand (_ : Ident) : DocM (Block ElabInline ElabBlock) := do
|
|
return .empty
|
|
|
|
/-- error: `notMetaCommand` must be marked `meta` to be used as a docstring command -/
|
|
#guard_msgs in
|
|
attribute [doc_command] notMetaCommand
|
|
|
|
-- The generated `getArgs` wrapper should have the same public/private visibility as the
|
|
-- definition it wraps. A private wrapper for a public def would mean the role couldn't be
|
|
-- used from importing modules.
|
|
|
|
@[doc_role]
|
|
public meta def publicRole (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
|
|
return .empty
|
|
|
|
@[doc_role]
|
|
meta def internalRole (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
|
|
return .empty
|
|
|
|
-- Same again, but applying the attribute as a separate command rather than inline:
|
|
public meta def publicRole' (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
|
|
return .empty
|
|
attribute [doc_role] publicRole'
|
|
|
|
meta def internalRole' (_ : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
|
|
return .empty
|
|
attribute [doc_role] internalRole'
|
|
|
|
/--
|
|
info: publicRole.getArgs visible publicly: true
|
|
internalRole.getArgs visible publicly: false
|
|
publicRole'.getArgs visible publicly: true
|
|
internalRole'.getArgs visible publicly: false
|
|
-/
|
|
#guard_msgs in
|
|
#eval show Lean.Elab.Command.CommandElabM Unit from withExporting do
|
|
IO.println s!"publicRole.getArgs visible publicly: {← hasConst ``publicRole.getArgs}"
|
|
IO.println s!"internalRole.getArgs visible publicly: {← hasConst ``internalRole.getArgs}"
|
|
IO.println s!"publicRole'.getArgs visible publicly: {← hasConst ``publicRole'.getArgs}"
|
|
IO.println s!"internalRole'.getArgs visible publicly: {← hasConst ``internalRole'.getArgs}"
|