[doc] Add why3 extension for good highlighting.

doc/acas_xu.rst

@@ -112,7 +112,7 @@ basic programming data structures (arrays, queues, hash tables, *etc.*).
 Let us try to model the property :math:`\phi_1` defined earlier. We will call
 our theory ``ACASXU_P1``.
 
-.. code-block:: ocaml
+.. code-block:: whyml
 
    theory ACASXU_P1
    end
@@ -127,7 +127,7 @@ precision floating-point numbers. We thus import it in our theory using the
 
 Our file looks like this so far:
 
-.. code-block:: ocaml
+.. code-block:: whyml
 
    theory ACASXU_P1
      use ieee_float.Float64
@@ -144,7 +144,7 @@ will only consider the ``AsTuple`` subtheory for this tutorial.
 In particular, the theory built by CAISAR is equivalent to the following WhyML
 file:
 
-.. code-block:: ocaml
+.. code-block:: whyml
 
    theory NeuralNetworkFilename
      theory AsTuple
@@ -170,7 +170,7 @@ that takes a 5-elements tuple as input, and provides a 5-element tuple as
 output. Supposing we have a neural network named ``ACASXU_1_1.onnx``, our WhyML
 file looks like this:
 
-.. code-block:: ocaml
+.. code-block:: whyml
 
    theory ACASXU_P1
      use ACASXU_1_1.AsTuple
@@ -194,7 +194,7 @@ model the advisory *COC*.
 
 The final WhyML file looks like this:
 
-.. code-block:: ocaml
+.. code-block:: whyml
 
   theory ACASXU_P1
     use ACASXU_1_1.AsTuple
@@ -267,7 +267,7 @@ floating-point constant :math:`y_0` is greater than or equal to at least one of
 the other five outputs. This can be formalized in first-order logic as a
 disjunction of clauses, that can be directly encoded into WhyML as follows:
 
-.. code-block:: ocaml
+.. code-block:: whyml
 
     y0 .>= y1 \/ y0 .>= y2 \/ y0 .>= y3 \/ y0 .>= y4
 
@@ -287,7 +287,7 @@ from the verification goal into the theory general context as axioms.
 
 In the end, the WhyML file looks like this:
 
-.. code-block:: ocaml
+.. code-block:: whyml
 
   theory ACASXU_P3
     use ACASXU_1_1.AsTuple as N11

doc/conf.py

@@ -14,10 +14,13 @@
 # import sys
 # sys.path.insert(0, os.path.abspath('.'))
 
+import os
+import sys
+sys.path.append(os.path.abspath('./ext'))
 
 # -- Project information -----------------------------------------------------
 
-project = 'Caisar'
+project = 'CAISAR'
 copyright = '2022, Michele Alberti, Julien Girard, François Bobot'
 author = 'Michele Alberti, Julien Girard, François Bobot'
 
@@ -28,6 +31,10 @@ author = 'Michele Alberti, Julien Girard, François Bobot'
 # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom
 # ones.
 extensions = [
+    'sphinx.ext.mathjax',
+    'sphinx.ext.graphviz',
+  #  'sphinxcontrib.bibtex',
+    'why3'
 ]
 
 # Add any paths that contain templates here, relative to this directory.

doc/ext/why3.py

+from pygments.lexer import RegexLexer, words
+from pygments.token import Text, Comment, Operator, Keyword, Name, String, Number, Punctuation, Error
+
+class WhyMLLexer(RegexLexer):
+    name = 'WhyML'
+    aliases = 'whyml'
+
+    keywords = (
+        'abstract', 'absurd', 'alias', 'any', 'as', 'assert', 'assume', 'at', 'axiom',
+        'begin', 'break', 'by', 'check', 'clone', 'coinductive', 'constant', 'continue',
+        'diverges', 'do', 'done', 'downto',
+        'else', 'end', 'ensures', 'epsilon', 'exception', 'exists', 'export',
+        'false', 'float', 'for', 'forall', 'fun', 'function', 'ghost', 'goal',
+        'if', 'import', 'in', 'inductive', 'invariant', 'label', 'lemma', 'let',
+        'match', 'meta', 'module', 'mutable', 'not', 'old',
+        'partial', 'predicate', 'private', 'pure',
+        'raise', 'raises', 'range', 'reads', 'rec', 'ref', 'requires', 'return', 'returns',
+        'scope', 'so', 'then', 'theory', 'to', 'true', 'try', 'type', 'use', 'val', 'variant',
+        'while', 'with', 'writes',
+    )
+
+    tokens = {
+        'root': [
+            (r'\s+', Text),
+            (r'\(\*\)', Operator),
+            (r'\(\*', Comment, 'comment'),
+            (r'\[@[^]]*\]', Comment),
+            (words(keywords, suffix=r'\b'), Keyword),
+            (r'[-~!%^&*+=|?<>/\\]', Operator),
+            (r'[][{};:.,()]', Punctuation),
+            (r"[^\W\d][\w']*", Name),
+            (r'\bresult\b', Name.Builtin.Pseudo),
+
+            (r'-?\d\d*([.]\d*)?([eE][+-]?\d\d*)', Number.Float),
+            (r'-?0[xX][\da-fA-F][\da-fA-F]*([.][\da-fA-F]*)?([pP][+-]?\d\d*)', Number.Float),
+            (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex),
+            (r'0[oO][0-7][0-7_]*', Number.Oct),
+            (r'0[bB][01][01_]*', Number.Bin),
+            (r'\d[\d_]*', Number.Integer),
+
+            (r"'", Keyword),
+            (r'"', String.Double, 'string'),
+        ],
+        'comment': [
+            (r'[^(*)]+', Comment),
+            (r'\(\*', Comment, '#push'),
+            (r'\*\)', Comment, '#pop'),
+            (r'[(*)]', Comment),
+        ],
+        'string': [
+            (r'[^\\"]+', String.Double),
+            (r'\\[\\"\'ntbr]', String.Escape),
+            (r'\\[0-9]{3}', String.Escape),
+            (r'\\x[0-9a-fA-F]{2}', String.Escape),
+            (r'\\\n', String.Double),
+            (r'"', String.Double, '#pop'),
+        ],
+    }
+
+from sphinx.highlighting import lexers
+
+lexers['whyml'] = WhyMLLexer(startinline=True)
+
+import re
+from docutils import nodes
+from sphinx import addnodes
+from sphinx.directives import ObjectDescription
+from sphinx.domains import Domain
+from sphinx.roles import XRefRole
+from sphinx.util.docutils import SphinxDirective
+from sphinx.util.nodes import make_refnode
+
+ws_re = re.compile(r'\s+')
+
+class Why3ToolRole(XRefRole):
+    def process_link(self, env, refnode, has_explicit_title, title, target):
+        target = ws_re.sub(' ', target)
+        if target.startswith('why3 '):
+            target = target[5:]
+        return title, target
+
+attr_re = re.compile(r'\[@(.*)\]')
+
+class Why3AttributeRole(XRefRole):
+    def process_link(self, env, refnode, has_explicit_title, title, target):
+        target = ws_re.sub(' ', target)
+        m = attr_re.match(target)
+        if m:
+            target = m.group(1)
+        return title, target
+
+class Why3ToolDirective(SphinxDirective):
+    has_content = False
+    required_arguments = 1
+    optional_arguments = 0
+    final_argument_whitespace = True
+    option_spec = {}
+
+    def run(self):
+        fullname = ws_re.sub(' ', self.arguments[0].strip())
+        targetname = '%s-%s' % (self.name, fullname)
+        node = nodes.target('', '', ids = [targetname])
+        self.state.document.note_explicit_target(node)
+        indexentry = '%s; command' % (fullname,)
+        inode = addnodes.index(entries = [('pair', indexentry, targetname, '', None)])
+        domain = self.env.get_domain('why3')
+        domain.add_object('tool', fullname, targetname)
+        return [inode, node]
+
+class Why3Thing(ObjectDescription):
+    has_content = True
+    required_arguments = 1
+    optional_arguments = 0
+    final_argument_whitespace = True
+    option_spec = {}
+    thing_index = ''
+    thing_kind = ''
+
+    def handle_signature(self, sig, signode):
+        signode += addnodes.desc_name(text = sig)
+        return sig
+
+    def add_target_and_index(self, name, sig, signode):
+        targetname = '%s-%s' % (self.name, name)
+        signode['ids'].append(targetname)
+        indexentry = '%s; %s' % (name, self.thing_index)
+        self.indexnode['entries'].append(('pair', indexentry, targetname, '', None))
+        domain = self.env.get_domain('why3')
+        domain.add_object(self.thing_kind, name, targetname)
+
+class Why3Attribute(Why3Thing):
+    thing_index = 'attribute'
+    thing_kind = 'attribute'
+
+class Why3Debug(Why3Thing):
+    thing_index = 'debug flag'
+    thing_kind = 'debug'
+
+class Why3Meta(Why3Thing):
+    thing_index = 'meta'
+    thing_kind = 'meta'
+
+class Why3Transform(Why3Thing):
+    thing_index = 'transformation'
+    thing_kind = 'transform'
+
+class Why3Domain(Domain):
+    name = 'why3'
+    label = 'Why3'
+    roles = {
+        'attribute': Why3AttributeRole(),
+        'debug': XRefRole(),
+        'meta': XRefRole(),
+        'tool': Why3ToolRole(),
+        'transform': XRefRole(),
+    }
+    directives = {
+        'attribute': Why3Attribute,
+        'debug': Why3Debug,
+        'meta': Why3Meta,
+        'tool': Why3ToolDirective,
+        'transform': Why3Transform,
+    }
+    indices = {
+    }
+    initial_data = {}
+    initial_data['objects'] = {
+        'attribute': {},
+        'debug': {},
+        'meta': {},
+        'tool': {},
+        'transform': {},
+    }
+
+    def get_objects(self):
+        for role, objects in self.data['objects'].items():
+            prio = 0 # self.object_types[role].attrs['searchprio']
+            for name, (docname, targetname) in objects.items():
+                yield (name, name, role, docname, targetname, prio)
+
+    def resolve_xref(self, env, fromdocname, builder, role, targetname, node, contnode):
+        resolved = self.data['objects'][role].get(targetname)
+        if resolved:
+            (todocname, targetname) = resolved
+            return make_refnode(builder, fromdocname, todocname, targetname, contnode, targetname)
+        return None
+
+    def add_object(self, role, name, targetname):
+        self.data['objects'][role][name] = (self.env.docname, targetname)
+
+
+def setup(app):
+    app.add_domain(Why3Domain)
+
+    return {
+        'version': '0.1',
+        'parallel_read_safe': True,
+        'parallel_write_safe': True,
+    }