- Apply elpi syntax highlighting

- Embed dune build $(DUNE_OPTS) @doc output
- Add a regexp based validation mechanism
- Connection with gh-pages, through sphinx.ext.githubpages

.gitignore

 *~
-
 .*.swp
 .merlin
+.vscode
 
 elpi.*
 

Makefile

@@ -51,11 +51,21 @@ install:
 doc:
 	dune build $(DUNE_OPTS) @doc
 
-doc-sphinx:
+doc-sphinx: doc
 	cp -r docs/base docs/source
-	python docs/engine/engine.py
+	python3 docs/engine/engine.py
 	cd docs && make html
 	rm -rf docs/source
+	cp -r _build/default/_doc/_html/elpi docs/build/html/
+	cp -r _build/default/_doc/_html/elpi-option-legacy-parser docs/build/html/
+	cp -r _build/default/_doc/_html/highlight.pack.js docs/build/html/
+	cp -r _build/default/_doc/_html/odoc.css docs/build/html/
+
+gh-pages: doc-sphinx
+	rm -rf /tmp/gh-pages
+	cp -r docs/build/html/ /tmp/gh-pages
+	git checkout gh-pages
+	rm -rf * && cp -r /tmp/gh-pages/* ./ && rm -rf /tmp/gh-pages && git add . && git commit -m "Updated gh-pages" && git push origin gh-pages && git checkout feature/doc
 
 clean:
 	rm -rf _build
@@ -117,4 +127,4 @@ menhir-complete-errormsgs:
 menhir-strip-errormsgs:
 	sed -e "/^##/d" -i.bak src/parser/error_messages.txt
 
-.PHONY: tests help install build clean
+.PHONY: tests help install build clean gh-pages

docs/base/a.elpi

+type s num -> num.
+type zero num.
+pred ack i:num, i:num, o:num.
+ack zero N V :- !, V = (s N).
+ack M zero V :- !, (s M2) = M, ack M2 (s zero) V.
+ack M N V :- (s M2) = M, (s N2) = N, ack M N2 V2, ack M2 V2 V.
+main :- ack (s (s (s zero))) (s zero) V, print "V =" V.
\ No newline at end of file

docs/base/about.rst

@@ -19,16 +19,24 @@ To match the visuals used in the community (*e.g.* https://coq.inria.fr/distrib/
 
    pip install sphinx-rtd-theme
 
+On debian based systems, one can use the package manager:
+
+.. code-block:: console
+
+   apt install sphinx-doc
+   apt install python3-sphinx-rtd-theme
+   pip install in-place
+
 Extensions
 ----------
 
-This documentation can me use of the following plugins:
+This documentation can make use of the following plugins:
 
 .. code-block:: python
 
    extensions = [
-       'sphinx.ext.intersphinx',
-       'sphinx.ext.githubpages'
+      'sphinx.ext.intersphinx',
+      'sphinx.ext.githubpages'
    ]
 
 Namely, ``intersphinx`` (https://www.sphinx-doc.org/en/master/usage/extensions/intersphinx.html) can generate links to the documentation of objects in external projects, either explicitly through the external role, or as a fallback resolution for any other cross-reference, and, ``githubpages`` (https://www.sphinx-doc.org/en/master/usage/extensions/githubpages.html#module-sphinx.ext.githubpages) which creates a ``.nojekyll`` file on generated HTML directory to publish the document on GitHub Pages.
@@ -43,3 +51,9 @@ Instead, use the ``doc-sphinx`` target of the source tree's root's ``Makefile``
 .. code-block:: python
 
     make doc-sphinx
+ 
+Or, to build and publish the documentation to github pages:
+
+.. code-block:: python
+
+    make gh-pages

docs/base/index.rst

@@ -13,9 +13,9 @@ Welcome to Elpi's documentation!
    about
    playground
 
-.. Indices and tables
-.. ==================
-
-.. * :ref:`genindex`
-.. * :ref:`modindex`
-.. * :ref:`search`
+.. toctree::
+   :maxdepth: 2
+   :caption: API:
+   
+   elpi <elpi/index.html#http://>
+   elpi-option-legacy-parser <elpi-option-legacy-parser/index.html#http://>

docs/base/playground.rst

 Playground
 ==========
 
-This page will be used to test hooks in order to run ``elpi`` on code snippets and inject its output within ``sphinx`` documentation sources.
+This page is used to test hooks in order to run ``elpi`` on code snippets and inject its output within ``sphinx`` documentation sources.
 
 Prerequisites
 -------------
@@ -22,19 +22,22 @@ It doesn't hurt to check that ``dune`` runs the locally built ``elpi`` correctly
 Syntax
 ------
 
-Elpi code blocks to be evaluated and injection from ``docs/base`` to ``docs/source`` are conventionally denoted in ``reStructuredText`` as ``.. elpi:: FILE``.
+Elpi code blocks to be evaluated and which output is to be injected from ``docs/base`` to ``docs/source`` are conventionally denoted in ``reStructuredText`` as ``.. elpi:: FILE``.
 
 .. literalinclude:: ../../tests/sources/chr.elpi
    :linenos:
    :language: elpi
 
-The injection engine will:
+The injection engine:
 
-* Retrieve all ``.. elpi::`` directives
-* Change them into ``literalinclude`` in the generated source with relevant options
-* Run ``dune exec elpi -- -test FILE`` on the ``FILE`` containing the ``elpi`` snippet, test or example.
-* Capture its output (``stdout``)
-* Create a ``code-block:: console`` just after it to inject the captured console output
+* Retrieves all ``.. elpi::`` directives
+* Changes them into ``literalinclude`` in the generated source with relevant options
+* Runs ``dune exec elpi -- -test FILE`` on the ``FILE`` containing the ``elpi`` snippet, test or example.
+* Captures its output (``stdout``)
+* Creates a ``code-block:: console`` just after it to inject the captured console output
+* Captures its output (``stderr``)
+* Creates a ``code-block:: console`` just after it to inject the captured console erros
+* In case of an assertion option for the ``elpi`` directive, the output is injected only if matched
 
 Result should look as follows:
 
@@ -71,11 +74,156 @@ Result should look as follows:
 
    State:
 
+Regexp Matching
+---------------
+
+This ``elpi`` directive should pass validation:
+
+.. code-block:: console
+   
+   .. elpi:: ./a.elpi
+      :assert: V = s \(.*\)
+
+.. elpi:: ./a.elpi
+   :assert: V = s \(.*\)
+
+This one should fail validation, only a message stating the regexp matching error will be printed:
+
+.. code-block:: console
+   
+   .. elpi:: ./a.elpi
+      :assert: /(?!)/
+
+.. elpi:: ./a.elpi
+   :assert: /(?!)/
+
 Test Bed
 --------
 
+.. elpi:: ../../tests/sources/accumulate_twice1.elpi
+.. elpi:: ../../tests/sources/accumulate_twice2.elpi
 .. elpi:: ../../tests/sources/accumulated.elpi
-
 .. elpi:: ../../tests/sources/ackermann.elpi
-
+.. elpi:: ../../tests/sources/asclause.elpi
+.. elpi:: ../../tests/sources/beta.elpi
+.. elpi:: ../../tests/sources/block.elpi
 .. elpi:: ../../tests/sources/chr.elpi
+.. elpi:: ../../tests/sources/chrGCD.elpi
+.. elpi:: ../../tests/sources/chrLEQ.elpi
+.. elpi:: ../../tests/sources/chr_nokey.elpi
+.. elpi:: ../../tests/sources/chr_nokey2.elpi
+.. elpi:: ../../tests/sources/chr_not_clique.elpi
+.. elpi:: ../../tests/sources/chr_sem.elpi
+.. elpi:: ../../tests/sources/conj2.elpi
+.. elpi:: ../../tests/sources/ctx_loading.elpi
+.. elpi:: ../../tests/sources/cut.elpi
+.. elpi:: ../../tests/sources/cut2.elpi
+.. elpi:: ../../tests/sources/cut3.elpi
+.. elpi:: ../../tests/sources/cut4.elpi
+.. elpi:: ../../tests/sources/cut5.elpi
+.. elpi:: ../../tests/sources/cut6.elpi
+.. elpi:: ../../tests/sources/deep_indexing.elpi
+.. elpi:: ../../tests/sources/discard.elpi
+.. elpi:: ../../tests/sources/elpi_only_llam.elpi
+.. elpi:: ../../tests/sources/end_comment.elpi
+.. elpi:: ../../tests/sources/eta.elpi
+.. elpi:: ../../tests/sources/eta_as.elpi
+.. elpi:: ../../tests/sources/even-odd.elpi
+.. elpi:: ../../tests/sources/findall.elpi
+.. elpi:: ../../tests/sources/fragment_exit.elpi
+.. elpi:: ../../tests/sources/fragment_exit2.elpi
+.. elpi:: ../../tests/sources/fragment_exit3.elpi
+.. elpi:: ../../tests/sources/general_case.elpi
+.. elpi:: ../../tests/sources/general_case2.elpi
+.. elpi:: ../../tests/sources/general_case3.elpi
+.. elpi:: ../../tests/sources/hc_interp.elpi
+.. elpi:: ../../tests/sources/hdclause.elpi
+.. elpi:: ../../tests/sources/heap_discard.elpi
+.. elpi:: ../../tests/sources/ho.elpi
+.. elpi:: ../../tests/sources/hollight.elpi
+.. elpi:: ../../tests/sources/hollight_legacy.elpi
+.. elpi:: ../../tests/sources/hyp_uvar.elpi
+.. elpi:: ../../tests/sources/impl.elpi
+.. elpi:: ../../tests/sources/impl2.elpi
+.. elpi:: ../../tests/sources/index2.elpi
+.. elpi:: ../../tests/sources/io_colon.elpi
+.. elpi:: ../../tests/sources/lambda.elpi
+.. elpi:: ../../tests/sources/lambda2.elpi
+.. elpi:: ../../tests/sources/lambda3.elpi
+.. elpi:: ../../tests/sources/list_as_conj.elpi
+.. elpi:: ../../tests/sources/list_comma.elpi
+.. elpi:: ../../tests/sources/llam.elpi
+.. elpi:: ../../tests/sources/llamchr.elpi
+.. elpi:: ../../tests/sources/map.elpi
+.. elpi:: ../../tests/sources/map_list.elpi
+.. elpi:: ../../tests/sources/map_list_opt.elpi
+.. elpi:: ../../tests/sources/name_builtin.elpi
+.. elpi:: ../../tests/sources/named_clauses00.elpi
+.. elpi:: ../../tests/sources/named_clauses01.elpi
+.. elpi:: ../../tests/sources/named_clauses02.elpi
+.. elpi:: ../../tests/sources/namespaces00.elpi
+.. elpi:: ../../tests/sources/namespaces01.elpi
+.. elpi:: ../../tests/sources/namespaces02.elpi
+.. elpi:: ../../tests/sources/namespaces03.elpi
+.. elpi:: ../../tests/sources/nil_cons.elpi
+.. elpi:: ../../tests/sources/notation.elpi
+.. elpi:: ../../tests/sources/notation_error.elpi
+.. elpi:: ../../tests/sources/notation_legacy.elpi
+.. elpi:: ../../tests/sources/patternunif.elpi
+.. elpi:: ../../tests/sources/patternunif2.elpi
+.. elpi:: ../../tests/sources/pi.elpi
+.. elpi:: ../../tests/sources/pi3.elpi
+.. elpi:: ../../tests/sources/pi5.elpi
+.. elpi:: ../../tests/sources/pnf.elpi
+.. elpi:: ../../tests/sources/polymorphic_variants.elpi
+.. elpi:: ../../tests/sources/printer.elpi
+.. elpi:: ../../tests/sources/queens.elpi
+.. elpi:: ../../tests/sources/quote_syntax.elpi
+.. elpi:: ../../tests/sources/random.elpi
+.. elpi:: ../../tests/sources/reduce_cbn.elpi
+.. elpi:: ../../tests/sources/reduce_cbv.elpi
+.. elpi:: ../../tests/sources/restriction.elpi
+.. elpi:: ../../tests/sources/restriction3.elpi
+.. elpi:: ../../tests/sources/restriction4.elpi
+.. elpi:: ../../tests/sources/restriction5.elpi
+.. elpi:: ../../tests/sources/restriction6.elpi
+.. elpi:: ../../tests/sources/rev.elpi
+.. elpi:: ../../tests/sources/rev14.elpi
+.. elpi:: ../../tests/sources/same_term.elpi
+.. elpi:: ../../tests/sources/self_assignment.elpi
+.. elpi:: ../../tests/sources/set.elpi
+.. elpi:: ../../tests/sources/shorten.elpi
+.. elpi:: ../../tests/sources/shorten2.elpi
+.. elpi:: ../../tests/sources/shorten_aux.elpi
+.. elpi:: ../../tests/sources/shorten_aux2.elpi
+.. elpi:: ../../tests/sources/shorten_builtin.elpi
+.. elpi:: ../../tests/sources/shorten_trie.elpi
+.. elpi:: ../../tests/sources/spill_and.elpi
+.. elpi:: ../../tests/sources/spill_impl.elpi
+.. elpi:: ../../tests/sources/spill_lam.elpi
+.. elpi:: ../../tests/sources/trace.elpi
+.. elpi:: ../../tests/sources/trace2.elpi
+.. elpi:: ../../tests/sources/trace_chr.elpi
+.. elpi:: ../../tests/sources/trace_cut.elpi
+.. elpi:: ../../tests/sources/trace_findall.elpi
+.. elpi:: ../../tests/sources/trail.elpi
+.. elpi:: ../../tests/sources/typeabbrv.elpi
+.. elpi:: ../../tests/sources/typeabbrv1.elpi
+.. elpi:: ../../tests/sources/typeabbrv10.elpi
+.. elpi:: ../../tests/sources/typeabbrv11.elpi
+.. elpi:: ../../tests/sources/typeabbrv12.elpi
+.. elpi:: ../../tests/sources/typeabbrv2.elpi
+.. elpi:: ../../tests/sources/typeabbrv3.elpi
+.. elpi:: ../../tests/sources/typeabbrv4.elpi
+.. elpi:: ../../tests/sources/typeabbrv5.elpi
+.. elpi:: ../../tests/sources/typeabbrv6.elpi
+.. elpi:: ../../tests/sources/typeabbrv7.elpi
+.. elpi:: ../../tests/sources/typeabbrv8.elpi
+.. elpi:: ../../tests/sources/typeabbrv9.elpi
+.. elpi:: ../../tests/sources/uminus.elpi
+.. elpi:: ../../tests/sources/uvar_chr.elpi
+.. elpi:: ../../tests/sources/var.elpi
+.. elpi:: ../../tests/sources/variadic_declare_constraints.elpi
+.. elpi:: ../../tests/sources/w.elpi
+.. elpi:: ../../tests/sources/w_legacy.elpi
+.. elpi:: ../../tests/sources/zebra.elpi
\ No newline at end of file

docs/engine/engine.py

 #!/usr/bin/env python3
 
-import os, sys, in_place, pathlib, subprocess
+import os, sys, in_place, pathlib, subprocess, re
+
+def check(input, expression):
+    pattern = re.compile(expression, re.IGNORECASE)
+    return pattern.match(input)
 
 def exec(path, base_path):
     file = base_path / path
-    print('  - Executing elpi on', file.as_posix())
+    print('  - Executing elpi on', file.as_posix().rstrip())
     elpi = subprocess.Popen(['dune', 'exec', 'elpi', '--', '-test', file.as_posix()[:-1]], stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True)
     output, errors = elpi.communicate()
     elpi.wait()
     return output, errors
 
 def process(source, base_path):
+    atext = '   :assert:'
     stext = '.. elpi::'
     rtext = '.. literalinclude::'
 
+    file_ = open(source, 'r')
+    lines = file_.readlines()
+
     with in_place.InPlace(source) as file:
+
+        index = 0
+        
         for line in file:
 
+            path = ''
+
             output = ''
             errors = ''
+            matchr = ''
+
+            if line.startswith(atext):
+                index += 1
+                file.write('')
+                continue
 
             if line.startswith(stext):
                 path = line[10:]
-                output, errors = exec(path, base_path)
-                # print('  - STDOUT:')
-                # print(output)
-                # print('  - STDERR:')
-                # print(errors)
 
-            line = line.replace(stext, rtext)
+                output, errors = exec(path, base_path)
+                
+                if index < len(lines)-1:
+                    next = lines[index+1]
+                    
+                    if next.startswith(atext):
+                        
+                        expression = next[12:].rstrip()
+                        
+                        if check(output, expression) is None:
+                            output = ''
+                            errors = ''
+                            matchr = 'Injection failure: result did not pass regexp check (' + expression + ')'
 
-            file.write(line)
+            if line.startswith(stext):
+                block = '**' + path + ':' + '**' + '\n' + '\n'
+                block += line.replace(stext, rtext)
+                block += '   :linenos:' + '\n'
+                block += '   :language: elpi' + '\n'
+                file.write(block)
+            else:
+                file.write(line)
 
             if len(output) > 0:
                 block  = '\n'
@@ -39,7 +72,7 @@ def process(source, base_path):
                 block += output.replace('\n', '\n   ')
                 block += '\n'
                 file.write(block)
-
+                
             if len(errors) > 0:
                 block  = '\n'
                 block += '.. code-block:: console' + '\n'
@@ -48,6 +81,17 @@ def process(source, base_path):
                 block += '\n'
                 file.write(block)
 
+            if len(matchr) > 0:
+                block  = '\n'
+                block += '.. raw:: html' + '\n'
+                block += '\n   '
+                block += '<div class="highlight-console notranslate"><div class="highlight" style="background-color: rgb(248, 148, 148);"><pre>'
+                block += matchr
+                block += '</pre></div></div>'
+                block += '\n'
+                file.write(block)
+            
+            index += 1
 
 def find(path):
     files = sorted(path.glob('**/**/*.rst'))