Merge pull request #66 from Wasm-DSL/hookup

Hook up up spec build with SpecTec

.github/workflows/ci-spec.yml

@@ -20,6 +20,12 @@ jobs:
         uses: actions/checkout@v2
         with:
           submodules: "recursive"
+      - name: Setup OCaml
+        uses: ocaml/setup-ocaml@v2
+        with:
+          ocaml-compiler: 4.14.x
+      - name: Setup Dune
+        run: opam install --yes dune menhir mdx
       - name: Setup Node.js
         uses: actions/setup-node@v3
         with:

document/core/Makefile

@@ -5,6 +5,12 @@
 SPHINXOPTS    =
 SPHINXBUILD   = sphinx-build
 PAPER         = a4
+ROOTDIR       = $(shell dirname `ls -d ../core 2>/dev/null || ls -d ../../core`)/..
+SPECTECDIR    = $(ROOTDIR)/spectec
+SPECTECSPEC   = $(SPECTECDIR)/spec/wasm-3.0
+SPECTECEXT    = watsup
+SPECTEC       = $(SPECTECDIR)/watsup
+SPLICEDIR     = _spectec
 BUILDDIR      = _build
 STATICDIR     = _static
 DOWNLOADDIR   = _download
@@ -19,7 +25,7 @@ I18NSPHINXOPTS  = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
 
 .PHONY: usage
 usage:
-	@echo "Please use \`make <target>' where <target> is one of"
+	@echo "Usage: \`make <target>\`' where <target> is one of"
 	@echo "  html       to make standalone HTML files"
 	@echo "  pdf        to make standalone PDF file"
 	@echo "  bikeshed   to make a bikeshed wrapped single large HTML file"
@@ -28,41 +34,9 @@ usage:
 	@echo "  WD-echidna publish the Working Draft tar file via Echidna"
 	@echo "  all        to make all 3"
 	@echo "  publish    to make all and push to gh-pages"
-	@echo "  help       to see more options"
 
 .PHONY: help
-help:
-	@echo "Usage: \`make <target>' where <target> is one of"
-	@echo "  html       to make standalone HTML files"
-	@echo "  pdf        to make standalone PDF file"
-	@echo "  bikeshed   to make a bikeshed wrapped single large HTML file"
-	@echo "  all        to make all 3"
-	@echo "  publish    to make all and push to gh-pages"
-	@echo "  dirhtml    to make HTML files named index.html in directories"
-	@echo "  singlehtml to make a single large HTML file"
-	@echo "  pickle     to make pickle files"
-	@echo "  json       to make JSON files"
-	@echo "  htmlhelp   to make HTML files and a HTML help project"
-	@echo "  qthelp     to make HTML files and a qthelp project"
-	@echo "  applehelp  to make an Apple Help Book"
-	@echo "  devhelp    to make HTML files and a Devhelp project"
-	@echo "  epub       to make an epub"
-	@echo "  epub3      to make an epub3"
-	@echo "  latex      to make LaTeX files, you can set PAPER=a4 or PAPER=letter"
-	@echo "  latexpdf   to make LaTeX files and run them through pdflatex"
-	@echo "  latexpdfja to make LaTeX files and run them through platex/dvipdfmx"
-	@echo "  text       to make text files"
-	@echo "  man        to make manual pages"
-	@echo "  texinfo    to make Texinfo files"
-	@echo "  info       to make Texinfo files and run them through makeinfo"
-	@echo "  gettext    to make PO message catalogs"
-	@echo "  changes    to make an overview of all changed/added/deprecated items"
-	@echo "  xml        to make Docutils-native XML files"
-	@echo "  pseudoxml  to make pseudoxml-XML files for display purposes"
-	@echo "  linkcheck  to check all external links for integrity"
-	@echo "  doctest    to run all doctests embedded in the documentation (if enabled)"
-	@echo "  coverage   to run coverage check of the documentation (if enabled)"
-	@echo "  dummy      to check syntax errors of document sources"
+help: usage
 
 .PHONY: deploy
 deploy:
@@ -80,6 +54,55 @@ all:	pdf html bikeshed
 .PHONY: main
 main:	pdf html
 
+
+###############################
+## File generation and SpecTec splicing
+
+GENERATED = appendix/index-instructions.rst
+.INTERMEDIATE: $(GENERATED)
+
+%.rst: %.py
+	(cd `dirname $@`; ./`basename $^`)
+
+
+.PHONY: spectec
+spectec:
+	(cd $(SPECTECDIR); make exe >/dev/null)
+
+SPECTECFILES = $(shell ls $(SPECTECSPEC)/*.$(SPECTECEXT))
+RSTDIRS = $(shell ls -d [a-z]*/)
+RSTFILES = $(shell ls -d *.rst [a-z]*/*.rst) $(GENERATED)
+CTRLFILES = Makefile conf.py $(shell ls util/*.*) $(shell ls static/*)
+ALLFILES = $(RSTDIRS) $(RSTFILES) $(CTRLFILES)
+SPLICEDFILES = spectec $(ALLFILES:%=$(SPLICEDIR)/%) $(BUILDDIR)
+
+.PHONY: ls-spectec ls-splice
+ls-spectec:
+	@for F in $(SPECTECFILES); do echo $$F; done
+ls-splice:
+	@for F in $(ALLFILES); do echo $$F; done
+
+$(SPLICEDIR):
+	mkdir -p $@
+
+$(SPLICEDIR)/$(BUILDDIR): $(SPLICEDIR)
+	mkdir -p $@
+
+$(BUILDDIR): $(SPLICEDIR)/$(BUILDDIR)
+	ln -s $< $@
+
+$(RSTDIRS:%=$(SPLICEDIR)/%): $(SPLICEDIR)
+	mkdir -p $@
+
+$(RSTFILES:%=$(SPLICEDIR)/%): $(SPLICEDIR)/%: % $(SPECTEC) $(SPECTECFILES)
+	$(SPECTEC) $(SPECTECFILES) --splice-sphinx -p $< -o $@
+
+$(CTRLFILES:%=$(SPLICEDIR)/%): $(SPLICEDIR)/%: %
+	cp $< $@
+
+######
+
+
 # Dirty hack to avoid rebuilding the Bikeshed version for every push.
 .PHONY: bikeshed-keep
 bikeshed-keep:
@@ -89,26 +112,31 @@ bikeshed-keep:
 	  echo Downloaded Bikeshed.
 
 
-GENERATED = appendix/index-instructions.rst
-.INTERMEDIATE: $(GENERATED)
-
-%.rst: %.py
-	(cd `dirname $@`; ./`basename $^`)
+.PHONY: pdf pdf-nested
+pdf:	$(SPLICEDFILES)
+	(cd $(SPLICEDIR) && make pdf-nested)
+	@echo
+	@echo "Build finished. The PDF is at `pwd`/$(BUILDDIR)/latex/$(NAME).pdf"
 
-.PHONY: pdf
-pdf:	$(GENERATED) latexpdf
+pdf-nested:	$(GENERATED) latexpdf
 	mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR)
 	ln -f $(BUILDDIR)/latex/$(NAME).pdf $(BUILDDIR)/html/$(DOWNLOADDIR)/$(NAME).pdf
 
 
 .PHONY: clean
 clean:
+	rm -rf $(SPLICEDIR)
 	rm -rf $(BUILDDIR)
 	rm -rf $(STATICDIR)
 	rm -f $(GENERATED)
 
-.PHONY: html
-html: $(GENERATED)
+.PHONY: html html-nested
+html:	$(SPLICEDFILES)
+	(cd $(SPLICEDIR) && make html-nested)
+	@echo
+	@echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html/."
+
+html-nested: $(GENERATED)
 	$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
 	for file in `ls $(BUILDDIR)/html/*.html`; \
 	do \
@@ -120,23 +148,32 @@ html: $(GENERATED)
 	  sed s:BASEDIR:..:g <$$file >$$file.out; \
 	  mv -f $$file.out $$file; \
 	done
+
+.PHONY: dirhtml dirhtml-nested
+dirhtml:	$(SPLICEDFILES)
+	(cd $(SPLICEDIR) && make dirhtml-nested)
 	@echo
-	@echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html/."
+	@echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
 
-.PHONY: dirhtml
-dirhtml: $(GENERATED)
+dirhtml-nested: $(GENERATED)
 	$(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml
+
+.PHONY: singlehtml singlehtml-nested
+singlehtml:	$(SPLICEDFILES)
+	(cd $(SPLICEDIR) && make singlehtml-nested)
 	@echo
-	@echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml."
+	@echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
 
-.PHONY: singlehtml
-singlehtml: $(GENERATED)
+singlehtml-nested: $(GENERATED)
 	$(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/singlehtml
+
+.PHONY: bikeshed bikeshed-nested
+bikeshed:	$(SPLICEDFILES)
+	(cd $(SPLICEDIR) && make bikeshed-nested)
 	@echo
-	@echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
+	@echo "Build finished. The HTML page is in $(BUILDDIR)/html/bikeshed/."
 
-.PHONY: bikeshed
-bikeshed: $(GENERATED)
+bikeshed-nested: $(GENERATED)
 	$(SPHINXBUILD) -b singlehtml -c util/bikeshed \
 		$(ALLSPHINXOPTS) $(BUILDDIR)/bikeshed_singlehtml
 	python3 util/bikeshed_fixup.py $(BUILDDIR)/bikeshed_singlehtml/index.html \
@@ -159,8 +196,6 @@ bikeshed: $(GENERATED)
 		< util/katex_fix.patch
 	cp $(BUILDDIR)/bikeshed_singlehtml/_static/pygments.css \
 		$(BUILDDIR)/html/bikeshed/
-	@echo
-	@echo "Build finished. The HTML page is in $(BUILDDIR)/html/bikeshed/."
 
 .PHONY: WD-tar
 WD-tar: bikeshed

document/core/syntax/conventions.rst

@@ -20,22 +20,22 @@ Grammar Notation
 
 The following conventions are adopted in defining grammar rules for abstract syntax.
 
-* Terminal symbols (atoms) are written in sans-serif font or in symbolic form: :math:`\K{i32}, \K{end}, {\to}, [, ]`.
+* Terminal symbols (atoms) are written in sans-serif font or in symbolic form: ${valtype: I32}, ${instr:NOP}, :math:`\to`, :math:`[`, :math:`]`.
 
-* Nonterminal symbols are written in italic font: :math:`\X{valtype}, \X{instr}`.
+* Nonterminal symbols are written in italic font: ${:valtype}, ${:instr}.
 
-* :math:`A^n` is a sequence of :math:`n\geq 0` iterations  of :math:`A`.
+* ${:A^n} is a sequence of ${:n >= 0} iterations of ${:A}.
 
-* :math:`A^\ast` is a possibly empty sequence of iterations of :math:`A`.
-  (This is a shorthand for :math:`A^n` used where :math:`n` is not relevant.)
+* ${:A*} is a possibly empty sequence of iterations of ${:A}.
+  (This is a shorthand for ${:A^n} used where ${:n} is not relevant.)
 
-* :math:`A^+` is a non-empty sequence of iterations of :math:`A`.
-  (This is a shorthand for :math:`A^n` where :math:`n \geq 1`.)
+* ${:A+}` is a non-empty sequence of iterations of ${:A}.
+  (This is a shorthand for ${:A^n} where ${:n >= 1}.)
 
-* :math:`A^?` is an optional occurrence of :math:`A`.
-  (This is a shorthand for :math:`A^n` where :math:`n \leq 1`.)
+* ${:A?}` is an optional occurrence of ${:A}.
+  (This is a shorthand for ${:A^n} where ${:n <= 1}.)
 
-* Productions are written :math:`\X{sym} ::= A_1 ~|~ \dots ~|~ A_n`.
+* Productions are written ${syntax: sym}.
 
 * Large productions may be split into multiple definitions, indicated by ending the first one with explicit ellipses, :math:`\X{sym} ::= A_1 ~|~ \dots`, and starting continuations with ellipses, :math:`\X{sym} ::= \dots ~|~ A_2`.
 
@@ -60,11 +60,11 @@ Auxiliary Notation
 
 When dealing with syntactic constructs the following notation is also used:
 
-* :math:`\epsilon` denotes the empty sequence.
+* ${:eps} denotes the empty sequence.
 
-* :math:`|s|` denotes the length of a sequence :math:`s`.
+* ${:|s|} denotes the length of a sequence ${:s}.
 
-* :math:`s[i]` denotes the :math:`i`-th element of a sequence :math:`s`, starting from :math:`0`.
+* ${:s[i]} denotes the ${:i}-th element of a sequence ${:s}`, starting from ${:0}.
 
 * :math:`s[i \slice n]` denotes the sub-sequence :math:`s[i]~\dots~s[i+n-1]` of a sequence :math:`s`.
 

spectec/spec/wasm-3.0/C-conventions.watsup

@@ -0,0 +1,9 @@
+;;
+;; Auxiliary definitions used for describing meta conventions
+;;
+
+;; Syntax notation
+
+syntax A = nat
+
+syntax sym = $(A_1) | ... | $(A_n)

spectec/src/backend-latex/config.ml

@@ -1,5 +1,8 @@
 type config =
   {
+    (* Spacing for display math *)
+    display : bool;
+
     (* Generate ids as macro calls `\id` instead of `\mathit{id}` *)
     macros_for_ids : bool;
 
@@ -13,7 +16,8 @@ type config =
 type t = config
 
 let default =
-  { macros_for_ids = false;
+  { display = true;
+    macros_for_ids = false;
     macros_for_atoms = false;
     include_grammar_desc = false;
   }

spectec/src/backend-latex/render.ml

@@ -118,6 +118,12 @@ let env config script : env =
   List.iter (env_def env) script;
   env
 
+let config env : Config.t =
+  env.config
+
+let env_with_config env config : env =
+  {env with config}
+
 
 (* Helpers *)
 
@@ -890,16 +896,17 @@ let rec classify_rel e : rel_sort option =
 let rec render_defs env = function
   | [] -> ""
   | d::ds' as ds ->
+    let sp = if env.config.display then "" else "@{~}" in
     match d.it with
     | SynD _ ->
       let ds' = merge_syndefs ds in
       let deco = if env.deco_syn then "l" else "l@{}" in
-      "\\begin{array}{@{}" ^ deco ^ "rrl@{}l@{}}\n" ^
+      "\\begin{array}{@{}" ^ deco ^ "r" ^ sp ^ "r" ^ sp ^ "l@{}l@{}}\n" ^
         render_sep_defs (render_syndef env) ds' ^
       "\\end{array}"
     | GramD _ ->
       let ds' = merge_gramdefs ds in
-      "\\begin{array}{@{}l@{}rrlll@{}l@{}}\n" ^
+      "\\begin{array}{@{}l@{}r" ^ sp ^ "r" ^ sp ^ "lll@{}l@{}}\n" ^
         render_sep_defs (render_gramdef env) ds' ^
       "\\end{array}"
     | RelD (id, t, _hints) ->
@@ -915,13 +922,13 @@ let rec render_defs env = function
             (render_ruledef env) ds ^
         "\\end{array}"
       | Some ReductionRel ->
-        "\\begin{array}{@{}l@{}lcl@{}l@{}}\n" ^
+        "\\begin{array}{@{}l@{}l" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
           render_sep_defs (render_reddef env) ds ^
         "\\end{array}"
       | None -> error d.at "unrecognized form of relation"
       )
     | DefD _ ->
-      "\\begin{array}{@{}lcl@{}l@{}}\n" ^
+      "\\begin{array}{@{}l" ^ sp ^ "c" ^ sp ^ "l@{}l@{}}\n" ^
         render_sep_defs (render_funcdef env) ds ^
       "\\end{array}"
     | SepD ->

spectec/src/backend-latex/render.mli

@@ -6,6 +6,8 @@ open El.Ast
 type env
 
 val env : Config.t -> El.Ast.script -> env
+val env_with_config : env -> Config.t -> env
+val config : env -> Config.t
 
 val with_syntax_decoration : bool -> env -> env
 val with_rule_decoration : bool -> env -> env

spectec/src/backend-splice/config.ml

@@ -3,6 +3,7 @@ type anchor =
     token : string;   (* anchor token *)
     prefix : string;  (* prefix generated for math splice *)
     suffix : string;  (* suffix generated for math splice *)
+    newline : bool;   (* use newlines *)
     indent : string;  (* inserted after generated newlines *)
   }
 
@@ -22,17 +23,17 @@ type t = config
 
 let latex =
   { anchors = [
-      {token = "#"; prefix = "$"; suffix = "$"; indent = ""};
-      {token = "##"; prefix = "$$\n"; suffix = "\n$$"; indent = ""};
+      {token = "#"; prefix = "$"; suffix = "$"; newline = false; indent = ""};
+      {token = "##"; prefix = "$$\n"; suffix = "\n$$"; newline = true; indent = ""};
     ];
     latex = Backend_latex.Config.default;
     prose = Backend_prose.Config.default;
   }
 
 let sphinx =
   { anchors = [
-      {token = "$"; prefix = ":math:`"; suffix = "`"; indent = ""};
-      {token = "$$"; prefix = ".. math::\n   "; suffix = ""; indent = "   "};
+      {token = "$"; prefix = ":math:`"; suffix = "`"; newline = false; indent = ""};
+      {token = "$$"; prefix = ".. math::\n   "; suffix = ""; newline = true; indent = "   "};
     ];
     latex = Backend_latex.Config.default;
     prose = Backend_prose.Config.default;