Update Sail documentation

THIRD_PARTY_FILES.md

@@ -7,6 +7,13 @@ CIL https://github.com/cil-project/cil
 | BSD 3-Clause | src/lib/visitor.ml     | ASLi/CIL |
 | BSD 3-Clause | src/lib/jib_visitor.ml | ASLi     |
 
+The following file is from Asciidoctor
+https://github.com/asciidoctor/asciidoctor
+
+| License      | Files                   | Source      |
+| ------------ | ----------------------- | ----------- |
+| MIT          | doc/asciidoc/manual.css | Asciidoctor |
+
 CIL
 ===
 
@@ -78,3 +85,31 @@ CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ```
+
+Asciidoctor
+===========
+
+```
+MIT License
+
+Copyright (C) 2012-present Dan Allen, Sarah White, Ryan Waldron, and the
+individual contributors to Asciidoctor.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.
+```

doc/asciidoc/Makefile

@@ -3,33 +3,73 @@ SAIL_PLUGIN ?= asciidoctor-sail
 SAIL_DOCS = sail_doc/riscv_duopod.json
 SAIL_DOCS += sail_doc/pattern_matching.json
 SAIL_DOCS += sail_doc/my_replicate_bits.json
+SAIL_DOCS += sail_doc/bitfield.json
 SAIL_DOCS += sail_doc/exn.json
+SAIL_DOCS += sail_doc/mapping.json
+SAIL_DOCS += sail_doc/scattered.json
+SAIL_DOCS += sail_doc/tuples.json
+SAIL_DOCS += sail_doc/string.json
+SAIL_DOCS += module_sail_doc/simple_mod.json
+SAIL_DOCS += module_sail_doc/simple_mod_err.error
+SAIL_DOCS += module_sail_doc/cond.rigging
+SAIL_DOCS += custom_sail_doc/cannot_wildcard.json
+SAIL_DOCS += lib_sail_doc/concurrency_interface/read_write.json
 
-CUSTOM_SAIL_DOCS = custom_sail_doc/cannot_wildcard.json
+TIKZ_FIGURES = ordering-tikz.png
 
-LIB_SAIL_DOCS = lib_sail_doc/concurrency_interface/read_write.json
+EXTRAS = ../examples/simple_mod.rigging
 
 default: manual.pdf
 
 sail_doc/%.json: ../examples/%.sail
 	mkdir -p sail_doc
-	sail -doc $< -doc_file $< -doc_embed plain -doc_bundle $(notdir $@)
+	sail -doc -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) $<
 
 lib_sail_doc/%.json: ../../lib/%.sail
 	mkdir -p lib_sail_doc
 	mkdir -p lib_sail_doc/concurrency_interface
-	sail -doc $< -doc_file $< -doc_embed plain -doc_bundle $(patsubst lib_sail_doc/%,%,$@) -o lib_sail_doc
+	sail -doc -doc_file $< -doc_embed plain -doc_bundle $(patsubst lib_sail_doc/%,%,$@) -o lib_sail_doc $<
+
+.SECONDEXPANSION:
+
+module_sail_doc/%.json: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files)
+	mkdir -p module_sail_doc
+	sail -doc $(addprefix -doc_file ,$(shell sail $< -list_files)) -doc_embed plain -doc_bundle $(notdir $@) -o module_sail_doc $<
+
+module_sail_doc/%.error: ../examples/%.rigging $$(shell sail ../examples/%.rigging -list_files)
+	mkdir -p module_sail_doc
+	-sail -no_color $< 2> $@
+
+module_sail_doc/%.rigging: ../examples/%.rigging
+	mkdir -p module_sail_doc
+	sail $< -list_files
+	cp $< $@
 
 custom_sail_doc/cannot_wildcard.json: ../examples/cannot_wildcard.sail
 	mkdir -p custom_sail_doc
-	sail -no_color -doc $< -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) -o custom_sail_doc 2> custom_sail_doc/cannot_wildcard_warning
+	sail -no_color -doc -doc_file $< -doc_embed plain -doc_bundle $(notdir $@) -o custom_sail_doc 2> custom_sail_doc/cannot_wildcard_warning $<
+
+ordering-tikz.pdf: latex/ordering.tex
+	pdflatex --jobname=ordering-tikz $<
+
+%.png: %.pdf
+	pdftoppm -r 300 -png $< > $@
+
+parser.txt: ../../src/lib/parser.mly parser.sed
+	obelisk -i $< | tr '\n' '+' | sed 's/+[ ][ ]*\([^| ]\)/ \1/g' | tr '+' '\n' > $@
+	sed -i.bak -f parser.sed $@
 
-manual.pdf: *.adoc $(SAIL_DOCS) $(LIB_SAIL_DOCS) $(CUSTOM_SAIL_DOCS)
+manual.pdf: *.adoc $(SAIL_DOCS) $(EXTRAS) $(TIKZ_FIGURES) parser.txt
 	asciidoctor-pdf manual.adoc -r $(SAIL_PLUGIN) -r asciidoctor-bibtex
 
-manual.html: *.adoc $(SAIL_DOCS) $(LIB_SAIL_DOCS) $(CUSTOM_SAIL_DOCS)
+manual.html: *.adoc $(SAIL_DOCS) $(EXTRAS) $(TIKZ_FIGURES) parser.txt manual.css
 	asciidoctor manual.adoc -r $(SAIL_PLUGIN) -r asciidoctor-bibtex
 
+.PHONY: clean
 clean:
-	-rm manual.pdf
+	-rm *.pdf
+	-rm *.png
+	-rm *.log
+	-rm *.aux
+	-rm parser.txt
 	-rm manual.html

doc/asciidoc/docinfo.html

@@ -0,0 +1,23 @@
+<style>
+#toc img.logo {
+  width: 100px;
+  height: 100px;
+  margin-left: auto;
+  margin-right: auto;
+  margin-bottom: 10px;
+  display: block;
+}
+</style>
+
+<script>
+  document.addEventListener("DOMContentLoaded", () => {
+    var image = document.createElement('img')
+    image.setAttribute('src', '../../etc/logo/sail_logo_square.png')
+    image.setAttribute('alt', 'Sail Logo')
+    image.classList.add('logo')
+    var toc = document.querySelector('#toc')
+    if (toc) {
+      toc.insertAdjacentElement('afterbegin', image)
+    }
+  });
+</script>

doc/asciidoc/grammar.adoc

@@ -0,0 +1,41 @@
+This appendix contains a grammar for the Sail language that is
+automatically generated from the
+https://gallium.inria.fr/~fpottier/menhir[Menhir] parser definition.
+
+NOTE: This means that the grammar is stated in such a way that the
+parser generator can see it is free of LR shift/reduce and
+reduce/reduce conflicts, rather than being optimised for human
+readability.
+
+First, we need some lexical conventions:
+
+* `ID` is any valid Sail identifier
+
+* `OPERATOR` is any valid Sail operator, as defined in <<Operators>>.
+
+* `TYPE_VARIABLE` is a valid Sail identifier with a leading single quote `'`.
+
+* `NUMBER` is a non-empty sequence of decimal digits `[0-9]+`.
+
+* `HEXADECIMAL_LITERAL` is `0x[A-Ba-f0-9_]+`
+
+* `BINARY_LITERAL` is `0b[0-1_]+`
+
+* `STRING_LITERAL` is a Sail string literal.
+
+`$[ATTRIBUTE]` and `$LINE_DIRECTIVE` represent attributes and single
+line directives. Examples of line directives would be things like
+`$include`, `$ifdef` and so on. These start with a leading `$`, are
+followed by the directive name (which follows the same lexical rules
+as a Sail identifier), is followed by one or more spaces, then
+proceeds to the end of the line, with everything between the
+identifier and the line ending being the line directive's argument
+(with leading and trailing whitespace removed). An attribute starts
+with `$[` and ends with `]`, and in between consists of an attribute
+name, followed by at least one whitespace character, then any
+arbitrary sequence of characters that does not contain `]`.
+
+[source,sail]
+----
+include::parser.txt[]
+----