4. Extensions🔗

Verso's markup language features four extension points:

These can be used to extend Verso to support new documentation features.

4.1. Syntax🔗

All four extension points share a common syntax. They are invoked by name, with a sequence of arguments. These arguments may be positional or by name, and their values may be identifiers, string literals, or numbers. Boolean flags may be passed by preceding their name with - or + for false or true, respectively.

In this example, the directive syntax is invoked with the positional argument term and the named argument title set to "Example". The flag check is set to false. It contains a descriptive paragraph and the code block grammar, which is invoked with no arguments:

:::syntax term (title := example) -check
This is an example grammar:
```grammar
term ::= term "<+-+>" term
```
:::

More formally, an invocation of an extension should match this grammar:

CALL := IDENT ARG*
ARG := VAL | "(" IDENT ":=" VAL ")" | "+" IDENT | "-" IDENT
VAL := IDENT | STRING | NUM

A CALL may occur after an opening fence on a code block. It is mandatory after the opening colons of a directive, in the opening curly braces of a role, or in a command.

4.2. Elaborating Extensions🔗

Each kind of extension has a table that maps names to expanders. An expander converts Verso's syntax to Lean terms. When the elaborator encounters a code block, role, directive, or command invocation, it resolves the name and looks up an expander in the table. Expanders are attempted until one of them either throws an error or succeeds. Expanders use the monad DocElabM, which is an extension of Lean's term elaboration monad TermElabM with document-specific features. Expanders first parse their arguments into a suitable configuration type, typically via a FromArgs instance, after which they return Lean syntax.

There are two ways to associate an expander with a name: the @[code_block], @[role], @[directive], and @[block_command] attributes (preferred) or the @[code_block_expander], @[role_expander], and @[directive_expander] attributes. Using the former attributes results in an expander that invokes the argument parser automatically, and they enable Verso to automatically compute usage information from a FromArgs instance. The latter are lower-level, and require manual parsing of arguments.

4.2.1. Parsing Arguments🔗

This grammar is fairly restrictive, so each extension is responsible for parsing their arguments in order to afford sufficient flexibility. Arguments are parsed via instances of FromArgs:

type class

Verso.ArgParse.FromArgs (α : Type) (m : Type → Type) : Type 1
Verso.ArgParse.FromArgs (α : Type)
  (m : Type → Type) : Type 1

A canonical way to convert a sequence of Verso arguments into a given type.

Instance Constructor

Verso.ArgParse.FromArgs.mk

Methods

fromArgs : ArgParse m α

Converts a sequence of arguments into a value.

Implementations of FromArgs.fromArgs specify parsers written using ArgParse:

inductive type

Verso.ArgParse (m : Type → Type) : Type → Type 1
Verso.ArgParse (m : Type → Type) :
  Type → Type 1

A parser for arguments in some underlying monad.

Constructors

fail {m : Type → Type} {α : Type}
  (stx? : Option Lean.Syntax)
  (message? : Option ArgParse.SigDoc) : ArgParse m α

Fails with the provided error message.

pure {m : Type → Type} {α : Type} (val : α) : ArgParse m α

Returns a value without parsing any arguments.

lift {m : Type → Type} {α : Type} (desc : String)
  (act : m α) : ArgParse m α

Provides an argument value by lifting an action from the underlying monad.

positional {m : Type → Type} {α : Type}
  (nameHint : Lean.Name) (val : ArgParse.ValDesc m α)
  (doc? : Option ArgParse.SigDoc := none) : ArgParse m α

Matches a positional argument.

named {m : Type → Type} {α : Type} (name : Lean.Name)
  (val : ArgParse.ValDesc m α) (optional : Bool)
  (doc? : Option ArgParse.SigDoc := none) :
  ArgParse m (if optional = true then Option α else α)

Matches an argument with the provided name.

anyNamed {m : Type → Type} {α : Type} (name : Lean.Name)
  (val : ArgParse.ValDesc m α)
  (doc? : Option ArgParse.SigDoc := none) :
  ArgParse m (Lean.Ident × α)

Matches any named argument.

flag {m : Type → Type} (name : Lean.Name) (default : Bool)
  (doc? : Option ArgParse.SigDoc := none) : ArgParse m Bool

Matches a flag with the provided name.

flagM {m : Type → Type} (name : Lean.Name)
  (default : m Bool)
  (doc? : Option ArgParse.SigDoc := none) : ArgParse m Bool

Matches a flag with the provided name, deriving a default value from the monad

done {m : Type → Type} : ArgParse m Unit

No further arguments are allowed.

orElse {m : Type → Type} {α : Type} (p1 : ArgParse m α)
  (p2 : Unit → ArgParse m α) : ArgParse m α

Error recovery.

seq {m : Type → Type} {α β : Type} (p1 : ArgParse m (α → β))
  (p2 : Unit → ArgParse m α) : ArgParse m β

The sequencing operation of an applicative functor.

many {m : Type → Type} {α : Type} :
  ArgParse m α → ArgParse m (List α)

Zero or more repetitions.

remaining {m : Type → Type} : ArgParse m (Array Doc.Arg)

Returns all remaining arguments. This is useful for consuming some, then forwarding the rest.

Individual argument values are matched using ValDesc:

structure

Verso.ArgParse.ValDesc (m : Type → Type) (α : Type) : Type
Verso.ArgParse.ValDesc (m : Type → Type)
  (α : Type) : Type

A means of transforming a Verso argument value into a given type.

Constructor

Verso.ArgParse.ValDesc.mk

Fields

description : ArgParse.SigDoc

How should this argument be documented in automatically-generated signatures?

signature : ArgParse.CanMatch

Which of the three kinds of values can match this argument?

get : Doc.ArgVal → m α

How to transform the value into the given type.

A canonical value description for a Lean type can be registered via an instance of FromArgVal:

type class

Verso.ArgParse.FromArgVal (α : Type) (m : Type → Type) : Type
Verso.ArgParse.FromArgVal (α : Type)
  (m : Type → Type) : Type

A canonical way to convert a Verso argument into a given type.

Instance Constructor

Verso.ArgParse.FromArgVal.mk

Methods

fromArgVal : ArgParse.ValDesc m α

A canonical way to convert a Verso argument into a given type.

In addition to the constructors of ArgParse, the Applicative and Functor instances are important, as well as the following helpers:

def

Verso.ArgParse.namedD {α : Type} {m : Type → Type} (name : Lean.Name)
  (val : ArgParse.ValDesc m α) (default : α) : ArgParse m α
Verso.ArgParse.namedD {α : Type}
  {m : Type → Type} (name : Lean.Name)
  (val : ArgParse.ValDesc m α)
  (default : α) : ArgParse m α

Matches an argument with the provided name. If the argument is not present, default is returned.

def

Verso.ArgParse.positional' {α : Type} {m : Type → Type}
  [ArgParse.FromArgVal α m] (nameHint : Lean.Name)
  (doc? : Option ArgParse.SigDoc := none) : ArgParse m α
Verso.ArgParse.positional' {α : Type}
  {m : Type → Type}
  [ArgParse.FromArgVal α m]
  (nameHint : Lean.Name)
  (doc? : Option ArgParse.SigDoc :=
    none) :
  ArgParse m α

Matches a positional argument using the type's FromArgVal instance.

def

Verso.ArgParse.named' {α : Type} {m : Type → Type}
  [ArgParse.FromArgVal α m] (name : Lean.Name) (optional : Bool)
  (doc? : Option ArgParse.SigDoc := none) :
  ArgParse m (if optional = true then Option α else α)
Verso.ArgParse.named' {α : Type}
  {m : Type → Type}
  [ArgParse.FromArgVal α m]
  (name : Lean.Name) (optional : Bool)
  (doc? : Option ArgParse.SigDoc :=
    none) :
  ArgParse m
    (if optional = true then Option α
    else α)

Matches a named argument using the type's FromArgVal instance.

def

Verso.ArgParse.namedD' {α : Type} {m : Type → Type}
  [ArgParse.FromArgVal α m] (name : Lean.Name) (default : α) :
  ArgParse m α
Verso.ArgParse.namedD' {α : Type}
  {m : Type → Type}
  [ArgParse.FromArgVal α m]
  (name : Lean.Name) (default : α) :
  ArgParse m α

Matches an argument with the provided name using the type's FromArgVal instance. If the argument is not present, default is returned.