refman: generate JSON indices

.gitignore

@@ -107,6 +107,7 @@ result
 doc/unreleased.rst
 doc/refman-html
 doc/refman-pdf
+doc/refman-indices
 doc/common/version.tex
 doc/faq/html/
 doc/faq/axioms.eps

Makefile

@@ -11,7 +11,7 @@
 # Dune Makefile for Rocq
 
 .PHONY: help help-install states world rocqide watch check    # Main developer targets
-.PHONY: refman-html refman-pdf corelib-html apidoc     # Documentation targets
+.PHONY: refman-html refman-pdf refman-indices corelib-html apidoc     # Documentation targets
 .PHONY: test-suite dev-targets
 .PHONY: fmt ocheck obuild ireport clean               # Maintenance targets
 .PHONY: dunestrap release install                 # Miscellaneous
@@ -63,6 +63,7 @@ help:
 	@echo ""
 	@echo "  - refman-html: build Rocq's reference manual [HTML version]"
 	@echo "  - refman-pdf:  build Rocq's reference manual [PDF version]"
+	@echo "  - refman-indices: build Rocq's JSON indices"
 	@echo "  - corelib-html: build Rocq's Corelib documentation [HTML version]"
 	@echo "  - apidoc:      build ML API documentation"
 	@echo ""
@@ -192,6 +193,10 @@ refman-pdf: world doc/unreleased.rst
 	+$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b latex doc/sphinx doc/refman-pdf
 	$(MAKE) -C doc/refman-pdf LATEXMKOPTS=-silent
 
+refman-indices: world doc/unreleased.rst
+	rm -rf doc/refman-indices
+	$(WITHPYPATH) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices
+
 corelib-html: dunestrap
 	dune build @corelib-html
 

doc/README.md

@@ -71,6 +71,71 @@ Or if you want to use less disk space:
     apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
                 latexmk fonts-freefont-otf
 
+### JSON indices
+
+The documentation generator can also produce computer-readable JSON files for individual indices
+with `make refman-indices`. These files are meant to be useful for tool developers, for instance
+to power autocompletion in editors. They output files are found in `doc/refman-indices/*.json`.
+
+Each JSON index has the following shape:
+
+```typescript
+{
+  // a key is the name of the index entry
+  [string]: {
+    // the refman documentation page path for that entry
+    "documentation_path": string.
+    // the anchor on that page that leads to the documentation entry
+    "documentation_anchor": string,
+    // the grammar description
+    "syntax": Syntax,
+    // a simpler, plain text documentation
+    "documentation": string,
+  }
+}
+```
+
+Where `Syntax` can be used to match some text against the index entry or to propose the
+user a code snippet. It is of the following shape:
+
+```ts
+type Syntax =
+  | ["Literal", Literal]
+  | ["Reference", Reference]
+  | ["Alternative", Alternative]
+  | ["Repeat", Repeat]
+
+// the literal string
+type Literal = {
+  value: string
+  // an optional subscript, for example "1" which should be rendered as "₁"
+  subscript: string | null
+}
+
+// a reference to a different entry in the documentation
+type Reference = {
+  value: string
+  // an optional subscript, for example "1" which should be rendered as "₁"
+  subscript: string | null
+}
+
+// an alternative between a list of options
+type Alternative = {
+  children: Syntax[]
+}
+
+// repetition of a list of syntax nodes
+type Repeat = {
+  // nodes have to repeat at least this many times
+  min: number
+  // nodes can repeat up to and including this many times
+  max: number | null
+  // each repetition has to be separated with this
+  separator: string | null
+  children: Syntax[]
+}
+```
+
 ### Setting the locale for Python
 
 Make sure that the locale is configured on your platform so that Python encodes
@@ -106,6 +171,9 @@ The current documentation targets are:
 - `make corelib-html`
   Build Rocq core library documentation into `_build/default/doc/corelib/html`
 
+- `make refman-indices`
+  Build the JSON indices into `doc/refman-indices`
+
 - `make apidoc`
   Build the ML API's documentation into `_build/default/_doc/_html`
 

doc/tools/rocqrst/notations/object.py

@@ -0,0 +1,122 @@
+from dataclasses import asdict, dataclass
+from typing import Self
+
+from .parsing import parse
+from .TacticNotationsParser import TacticNotationsParser
+from .TacticNotationsVisitor import TacticNotationsVisitor
+
+
+class NotationObject:
+    def asdict(self):
+        return asdict(self)
+
+TaggedNotationObject = tuple[str, NotationObject]
+
+@dataclass
+class Literal(NotationObject):
+    value: str
+    subscript: str | None
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Literal", value)
+
+@dataclass
+class Reference(NotationObject):
+    value: str
+    subscript: str | None
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Reference", value)
+
+@dataclass
+class Alternative(NotationObject):
+    children: list[TaggedNotationObject]
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Alternative", value)
+
+@dataclass
+class Repeat(NotationObject):
+    min: int
+    max: int | None
+    separator: str | None
+    children: list[TaggedNotationObject]
+    @classmethod
+    def new(cls, value: Self) -> tuple[str, Self]:
+        return ("Repeat", value)
+
+class TacticNotationsToObjectVisitor(TacticNotationsVisitor):
+    def defaultResult(self):
+        return []
+
+    def aggregateResult(self, aggregate, nextResult):
+        # Flattening results into a single list of nodes
+        if nextResult:
+            if isinstance(nextResult, list):
+                aggregate.extend(nextResult)
+            else:
+                aggregate.append(nextResult)
+        return aggregate
+
+    def visitAlternative(self, ctx: TacticNotationsParser.AlternativeContext):
+        return [Alternative.new(Alternative(children=self.visitChildren(ctx)))]
+
+    def visitAltblock(self, ctx: TacticNotationsParser.AltblockContext):
+        return self.visitChildren(ctx)
+
+    def visitRepeat(self, ctx: TacticNotationsParser.RepeatContext):
+        separator = ctx.ATOM() or ctx.PIPE()
+        # skip the '{'
+        repeat_marker = ctx.LGROUP().getText()[1]
+
+        min_rep, max_rep = None, None
+        match repeat_marker:
+            case "?":
+                min_rep, max_rep = 0, 1
+            case "+":
+                min_rep, max_rep = 1, None
+            case "*":
+                min_rep, max_rep = 0, None
+            case _:
+                raise ValueError(f"Unexpected repeat marker: {repeat_marker}")
+
+        return [Repeat.new(Repeat(
+            min=min_rep,
+            max=max_rep,
+            separator=separator.getText() if separator else None,
+            children=self.visitChildren(ctx)
+        ))]
+
+    def visitCurlies(self, ctx: TacticNotationsParser.CurliesContext):
+        return [
+            Literal.new(Literal(value=ctx.LBRACE().getText(), subscript=None)),
+            *self.visitChildren(ctx),
+            Literal.new(Literal(value=ctx.RBRACE().getText(), subscript=None))]
+
+    def visitAtomic(self, ctx: TacticNotationsParser.AtomicContext):
+        return [Literal.new(Literal(
+            value=ctx.ATOM().getText(),
+            # skip '__'
+            subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None
+        ))]
+
+    def visitHole(self, ctx: TacticNotationsParser.HoleContext):
+        return [Reference.new(Reference(
+            value=ctx.ID().getText()[1:],
+            # skip '__'
+            subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None
+        ))]
+
+    def visitEscaped(self, ctx: TacticNotationsParser.EscapedContext):
+        return [Literal.new(Literal(
+            value=ctx.ESCAPED().getText().replace("%", ""),
+            subscript=None
+        ))]
+
+def objectify(notation: str) -> list[TaggedNotationObject]:
+    """Translate a notation into an object.
+
+    It is essentially a simplified and normalized version of the ANTLR AST.
+    """
+    visitor = TacticNotationsToObjectVisitor()
+    return visitor.visit(parse(notation))