Basic setup for examples in documentation (#6383)

7 files changed, 105 insertions, 3 deletions

diff --git a/docs/conf.py b/docs/conf.py
index fbe0e9131..3ec162d34 100644
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -10,9 +10,9 @@
 # add these directories to sys.path here. If the directory is relative to the
 # documentation root, use os.path.abspath to make it absolute, like shown here.
 #
-# import os
-# import sys
-# sys.path.insert(0, os.path.abspath('.'))
+import os
+import sys
+sys.path.insert(0, os.path.abspath('ext/'))
 
 
 # -- Project information -----------------------------------------------------
@@ -31,6 +31,8 @@ extensions = [
         'breathe',
         'sphinx.ext.autosectionlabel',
         'sphinxcontrib.bibtex',
+        'sphinx_tabs.tabs',
+        'examples',
 ]
 
 bibtex_bibfiles = ['references.bib']
diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst
new file mode 100644
index 000000000..8200ebb14
--- /dev/null
+++ b/docs/examples/datatypes.rst
@@ -0,0 +1,8 @@
+Datatypes
+===========
+
+
+.. api-examples::
+    ../../examples/api/datatypes.cpp
+    ../../examples/api/java/Datatypes.java
+    ../../examples/api/python/datatypes.py
diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst
new file mode 100644
index 000000000..ff3651857
--- /dev/null
+++ b/docs/examples/examples.rst
@@ -0,0 +1,9 @@
+Examples
+===========
+
+.. toctree::
+    :maxdepth: 2
+ 
+    helloworld
+    datatypes
+    lineararith
\ No newline at end of file
diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst
new file mode 100644
index 000000000..202952bb6
--- /dev/null
+++ b/docs/examples/helloworld.rst
@@ -0,0 +1,10 @@
+Hello World
+===========
+
+This example shows the very basic usage of the API.
+We create a solver, declare a Boolean variable and check whether it is entailed (by ``true``, as nothing has been asserted to the solver).
+
+.. api-examples::
+    ../../examples/api/helloworld.cpp
+    ../../examples/api/java/HelloWorld.java
+    ../../examples/api/python/helloworld.py
diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst
new file mode 100644
index 000000000..d772edbb3
--- /dev/null
+++ b/docs/examples/lineararith.rst
@@ -0,0 +1,8 @@
+Linear Arithmetic
+=================
+
+
+.. api-examples::
+    ../../examples/api/linear_arith.cpp
+    ../../examples/api/java/LinearArith.java
+    ../../examples/api/python/linear_arith.py
diff --git a/docs/ext/examples.py b/docs/ext/examples.py
new file mode 100644
index 000000000..befb6c175
--- /dev/null
+++ b/docs/ext/examples.py
@@ -0,0 +1,64 @@
+import os
+
+from docutils import nodes
+from docutils.parsers.rst import Directive
+from docutils.statemachine import StringList
+
+
+class APIExamples(Directive):
+    """Add directive `api-examples` to be used as follows:
+
+        .. api-examples::
+            file1
+            file2
+
+        The arguments should be proper filenames to source files.
+        This directives tries to detect the language from the file extension
+        and supports the file extensions specified in `self.exts`.
+    """
+
+    # Set tab title and language for syntax highlighting
+    exts = {
+        '.cpp': {'title': 'C++', 'lang': 'c++'},
+        '.java': {'title': 'Java', 'lang': 'java'},
+        '.py': {'title': 'Python', 'lang': 'python'},
+    }
+
+    # The "arguments" are actually the content of the directive
+    has_content = True
+
+    def run(self):
+        # collect everything in a list of strings
+        content = ['.. tabs::', '']
+
+        for file in self.content:
+            # detect file extension
+            _, ext = os.path.splitext(file)
+            if ext in self.exts:
+                title = self.exts[ext]['title']
+                lang = self.exts[ext]['lang']
+            else:
+                title = ext
+                lang = ext
+
+            # generate tabs
+            content.append(f'    .. tab:: {title}')
+            content.append(f'')
+            content.append(f'        .. literalinclude:: {file}')
+            content.append(f'            :language: {lang}')
+            content.append(f'            :linenos:')
+
+        # parse the string list
+        node = nodes.Element()
+        self.state.nested_parse(StringList(content), 0, node)
+        return node.children
+
+
+def setup(app):
+    app.setup_extension('sphinx_tabs.tabs')
+    app.add_directive("api-examples", APIExamples)
+    return {
+        'version': '0.1',
+        'parallel_read_safe': True,
+        'parallel_write_safe': True,
+    }
diff --git a/docs/index.rst b/docs/index.rst
index af8eb498f..7167d7230 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -17,3 +17,4 @@ cvc5 API Documentation
 
    cpp
    references
+   examples/examples