diff --git a/.gitignore b/.gitignore
index 336ec0c212d5d5b12985ee19646fae4c94b075b1..a46e2b70462bd196c68062f4dc42aa4f8d757e08 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,7 +1,7 @@
*~
-
.*.swp
.merlin
+.vscode
elpi.*
diff --git a/Makefile b/Makefile
index 090c890251b6e6fcc484dcc280728b3b16f7c30a..1fa547c69f0259746984877439006bd0d3846253 100644
--- a/Makefile
+++ b/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
diff --git a/docs/base/a.elpi b/docs/base/a.elpi
new file mode 100644
index 0000000000000000000000000000000000000000..61b3d2afbbee668d0826d095656fac8216c692b4
--- /dev/null
+++ b/docs/base/a.elpi
@@ -0,0 +1,7 @@
+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
diff --git a/docs/base/about.rst b/docs/base/about.rst
index 293eca7ccb847c45d1a48d0fc300317a8cbad623..0bb345c18976e00dd727ad0d5934f82041f80a6d 100644
--- a/docs/base/about.rst
+++ b/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
diff --git a/docs/base/index.rst b/docs/base/index.rst
index 3b1be42e9a9947b674cca5aa4c7b33405fa3bd4f..5865ab9711096358250aaf63a66f71b6ebbfc2fb 100644
--- a/docs/base/index.rst
+++ b/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://>
diff --git a/docs/base/playground.rst b/docs/base/playground.rst
index 6190a873f46b8f94997dad9a000ea9555c5bef27..91f67b44aa81869b70b8f5e3a5197f8dfa815157 100644
--- a/docs/base/playground.rst
+++ b/docs/base/playground.rst
@@ -1,7 +1,7 @@
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
diff --git a/docs/engine/engine.py b/docs/engine/engine.py
index eb81512f9af3358c9f061b211650a3a374d56880..bbe9d7d40ae8729a5a8e95e65816621ab8599300 100644
--- a/docs/engine/engine.py
+++ b/docs/engine/engine.py
@@ -1,36 +1,69 @@
#!/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'))