diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index d26cc6d5ee85cce40209627b33c8dad269c01e8b..5a55540e98dda69bec2298eea89cf6e5d61ed87c 100644
--- a/doc/acas_xu.rst
+++ b/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
diff --git a/doc/conf.py b/doc/conf.py
index b3991ef3949154f321b22bc44d3919e31d562080..42a6c97be5114c72b61c4f133852410c8dfac530 100644
--- a/doc/conf.py
+++ b/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.
diff --git a/doc/ext/why3.py b/doc/ext/why3.py
new file mode 100644
index 0000000000000000000000000000000000000000..29a8fd889715a39a543d0e40d454616247e870c0
--- /dev/null
+++ b/doc/ext/why3.py
@@ -0,0 +1,199 @@
+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,
+ }