Progress on instructions; improved makefiles

document/core/.gitignore

@@ -1,3 +1,4 @@
 _build
 _static
+_spectec
 document/*.pyc

document/core/Makefile

@@ -69,11 +69,12 @@ GENERATED = appendix/index-instructions.rst
 spectec:
 	(cd $(SPECTECDIR); make exe >/dev/null)
 
-SPECTECFILES = $(shell ls $(SPECTECSPEC)/*.$(SPECTECEXT))
+SPECTECPAT = $(SPECTECSPEC)/*.$(SPECTECEXT)
+SPECTECFILES = $(shell ls $(SPECTECPAT))
 RSTDIRS = $(shell ls -d [a-z]*/ util/[a-z]*/)
 RSTFILES = $(shell ls -d *.rst [a-z]*/*.rst) $(GENERATED)
 CTRLFILES = $(shell ls Makefile *.* util/*.* util/bikeshed/*.*) $(shell ls static/*)
-ALLFILES = $(RSTDIRS) $(RSTFILES) $(CTRLFILES)
+ALLFILES = $(RSTDIRS) $(CTRLFILES) _splice  #$(RSTFILES)
 SPLICEDFILES = spectec $(ALLFILES:%=$(SPLICEDIR)/%) $(BUILDDIR)
 
 .PHONY: ls-spectec ls-splice
@@ -91,14 +92,20 @@ $(SPLICEDIR)/$(BUILDDIR): $(SPLICEDIR)
 $(BUILDDIR): $(SPLICEDIR)/$(BUILDDIR)
 	ln -s $< $@
 
-$(RSTDIRS:%=$(SPLICEDIR)/%): $(SPLICEDIR)
+$(RSTDIRS:%=$(SPLICEDIR)/%):: $(SPLICEDIR)
 	mkdir -p $@
 
-$(SPLICEDIR)/util/katex: util/katex
+$(SPLICEDIR)/util/katex:: util/katex
 	cp -R $< $@   # F it!
 
-$(RSTFILES:%=$(SPLICEDIR)/%): $(SPLICEDIR)/%: % $(SPECTECFILES)
-	$(SPECTEC) $(SPECTECFILES) --splice-sphinx -p $< -o $@
+$(SPLICEDIR)/_splice: $(SPLICEDIR) $(RSTFILES) $(SPECTECFILES)
+	@echo Modified $?
+	@echo ${if ${filter %.$(SPECTECEXT), $?}, $(RSTFILES), ${filter %.rst, $?}} >$@
+	@echo Splicing `cat $@`
+	@$(SPECTEC) $(SPECTECPAT) --splice-sphinx -p `cat $@` -o $(SPLICEDIR)
+
+#$(RSTFILES:%=$(SPLICEDIR)/%): $(SPLICEDIR)/%: % $(SPECTECFILES)
+#	$(SPECTEC) $(SPECTECFILES) --splice-sphinx -p $< -o $@
 
 $(CTRLFILES:%=$(SPLICEDIR)/%): $(SPLICEDIR)/%: %
 	cp $< $@

document/core/syntax/instructions.rst

@@ -21,15 +21,12 @@ The following sections group instructions into a number of different categories.
 .. index:: ! numeric instruction, value, value type, integer, floating-point, two's complement
    pair: abstract syntax; instruction
 .. _syntax-sx:
+.. _syntax-num:
 .. _syntax-const:
-.. _syntax-iunop:
-.. _syntax-ibinop:
-.. _syntax-itestop:
-.. _syntax-irelop:
-.. _syntax-funop:
-.. _syntax-fbinop:
-.. _syntax-ftestop:
-.. _syntax-frelop:
+.. _syntax-unop:
+.. _syntax-binop:
+.. _syntax-testop:
+.. _syntax-relop:
 .. _syntax-instr-numeric:
 
 Numeric Instructions
@@ -38,85 +35,7 @@ Numeric Instructions
 Numeric instructions provide basic operations over numeric :ref:`values <syntax-value>` of specific :ref:`type <syntax-numtype>`.
 These operations closely match respective operations available in hardware.
 
-.. math::
-   \begin{array}{llrl}
-   \production{width} & \X{nn}, \X{mm} &::=&
-     \K{32} ~|~ \K{64} \\
-   \production{signedness} & \sx &::=&
-     \K{u} ~|~ \K{s} \\
-   \production{instruction} & \instr &::=&
-     \K{i}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-int}{\uX{\X{nn}}} ~|~
-     \K{f}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-float}{\fX{\X{nn}}} \\&&|&
-     \K{i}\X{nn}\K{.}\iunop ~|~
-     \K{f}\X{nn}\K{.}\funop \\&&|&
-     \K{i}\X{nn}\K{.}\ibinop ~|~
-     \K{f}\X{nn}\K{.}\fbinop \\&&|&
-     \K{i}\X{nn}\K{.}\itestop \\&&|&
-     \K{i}\X{nn}\K{.}\irelop ~|~
-     \K{f}\X{nn}\K{.}\frelop \\&&|&
-     \K{i}\X{nn}\K{.}\EXTEND\K{8\_s} ~|~
-     \K{i}\X{nn}\K{.}\EXTEND\K{16\_s} ~|~
-     \K{i64.}\EXTEND\K{32\_s} \\&&|&
-     \K{i32.}\WRAP\K{\_i64} ~|~
-     \K{i64.}\EXTEND\K{\_i32}\K{\_}\sx ~|~
-     \K{i}\X{nn}\K{.}\TRUNC\K{\_f}\X{mm}\K{\_}\sx \\&&|&
-     \K{i}\X{nn}\K{.}\TRUNC\K{\_sat\_f}\X{mm}\K{\_}\sx \\&&|&
-     \K{f32.}\DEMOTE\K{\_f64} ~|~
-     \K{f64.}\PROMOTE\K{\_f32} ~|~
-     \K{f}\X{nn}\K{.}\CONVERT\K{\_i}\X{mm}\K{\_}\sx \\&&|&
-     \K{i}\X{nn}\K{.}\REINTERPRET\K{\_f}\X{nn} ~|~
-     \K{f}\X{nn}\K{.}\REINTERPRET\K{\_i}\X{nn} \\&&|&
-     \dots \\
-   \production{integer unary operator} & \iunop &::=&
-     \K{clz} ~|~
-     \K{ctz} ~|~
-     \K{popcnt} \\
-   \production{integer binary operator} & \ibinop &::=&
-     \K{add} ~|~
-     \K{sub} ~|~
-     \K{mul} ~|~
-     \K{div\_}\sx ~|~
-     \K{rem\_}\sx \\&&|&
-     \K{and} ~|~
-     \K{or} ~|~
-     \K{xor} ~|~
-     \K{shl} ~|~
-     \K{shr\_}\sx ~|~
-     \K{rotl} ~|~
-     \K{rotr} \\
-   \production{floating-point unary operator} & \funop &::=&
-     \K{abs} ~|~
-     \K{neg} ~|~
-     \K{sqrt} ~|~
-     \K{ceil} ~|~ 
-     \K{floor} ~|~ 
-     \K{trunc} ~|~ 
-     \K{nearest} \\
-   \production{floating-point binary operator} & \fbinop &::=&
-     \K{add} ~|~
-     \K{sub} ~|~
-     \K{mul} ~|~
-     \K{div} ~|~
-     \K{min} ~|~
-     \K{max} ~|~
-     \K{copysign} \\
-   \production{integer test operator} & \itestop &::=&
-     \K{eqz} \\
-   \production{integer relational operator} & \irelop &::=&
-     \K{eq} ~|~
-     \K{ne} ~|~
-     \K{lt\_}\sx ~|~
-     \K{gt\_}\sx ~|~
-     \K{le\_}\sx ~|~
-     \K{ge\_}\sx \\
-   \production{floating-point relational operator} & \frelop &::=&
-     \K{eq} ~|~
-     \K{ne} ~|~
-     \K{lt} ~|~
-     \K{gt} ~|~
-     \K{le} ~|~
-     \K{ge} \\
-   \end{array}
+$${syntax: sx num_ instr/num unop_ binop_ testop_ relop_ cvtop}
 
 Numeric instructions are divided by :ref:`number type <syntax-numtype>`.
 For each type, several subcategories can be distinguished:
@@ -132,45 +51,13 @@ For each type, several subcategories can be distinguished:
 * *Comparisons*: consume two operands of the respective type and produce a Boolean integer result.
 
 * *Conversions*: consume a value of one type and produce a result of another
-  (the source type of the conversion is the one after the ":math:`\K{\_}`").
+  (the source type of the conversion is the one after the "${:_}").
 
 Some integer instructions come in two flavors,
-where a signedness annotation |sx| distinguishes whether the operands are to be :ref:`interpreted <aux-signed>` as :ref:`unsigned <syntax-uint>` or :ref:`signed <syntax-sint>` integers.
+where a signedness annotation ${:sx} distinguishes whether the operands are to be :ref:`interpreted <aux-signed>` as :ref:`unsigned <syntax-uint>` or :ref:`signed <syntax-sint>` integers.
 For the other integer instructions, the use of two's complement for the signed interpretation means that they behave the same regardless of signedness.
 
 
-.. _syntax-unop:
-.. _syntax-binop:
-.. _syntax-testop:
-.. _syntax-relop:
-.. _syntax-cvtop:
-
-Conventions
-...........
-
-Occasionally, it is convenient to group operators together according to the following grammar shorthands:
-
-.. math::
-   \begin{array}{llrl}
-   \production{unary operator} & \unop &::=&
-     \iunop ~|~
-     \funop ~|~
-     \EXTEND{N}\K{\_s} \\
-   \production{binary operator} & \binop &::=& \ibinop ~|~ \fbinop \\
-   \production{test operator} & \testop &::=& \itestop \\
-   \production{relational operator} & \relop &::=& \irelop ~|~ \frelop \\
-   \production{conversion operator} & \cvtop &::=&
-     \WRAP ~|~
-     \EXTEND ~|~
-     \TRUNC ~|~
-     \TRUNC\K{\_sat} ~|~
-     \CONVERT ~|~
-     \DEMOTE ~|~
-     \PROMOTE ~|~
-     \REINTERPRET \\
-   \end{array}
-
-
 .. index:: ! vector instruction, numeric vector, number, value, value type, SIMD
    pair: abstract syntax; instruction
 .. _syntax-laneidx:
@@ -180,13 +67,11 @@ Occasionally, it is convenient to group operators together according to the foll
 .. _syntax-vvbinop:
 .. _syntax-vvternop:
 .. _syntax-vvtestop:
-.. _syntax-vitestop:
-.. _syntax-virelop:
-.. _syntax-vfrelop:
-.. _syntax-vishiftop:
-.. _syntax-viunop:
-.. _syntax-vibinop:
-.. _syntax-viminmaxop:
+.. _syntax-vtestop:
+.. _syntax-vrelop:
+.. _syntax-vshiftop:
+.. _syntax-vunop:
+.. _syntax-vbinop:
 .. _syntax-visatbinop:
 .. _syntax-vfunop:
 .. _syntax-vfbinop:
@@ -197,6 +82,13 @@ Vector Instructions
 
 Vector instructions (also known as *SIMD* instructions, *single instruction multiple data*) provide basic operations over :ref:`values <syntax-value>` of :ref:`vector type <syntax-vectype>`.
 
+$${syntax: lanetype dim shape half laneidx instr/vec}
+
+$${syntax:
+  vvunop vvbinop vvternop vvtestop
+  vunop_ vbinop_ vtestop_ vrelop_ vshiftop_ vextunop_ vextbinop_
+}
+
 .. math::
    \begin{array}{llrl}
    \production{ishape} & \ishape &::=&

document/core/syntax/values.rst

@@ -123,6 +123,8 @@ Conventions
 
 * The meta variable ${:z} ranges over floating-point values where clear from context.
 
+* Where clear from context, shorthands like ${:$fone} or ${:$fzero} denote floating point values like ${:POS $($(NORM 1 0))} or ${:POS $($(SUBNORM 0))}.
+
 
 .. index:: ! numeric vector, integer, floating-point, lane, SIMD
    pair: abstract syntax; vector

spectec/Makefile

@@ -54,14 +54,14 @@ test: exe $(TESTDIRS) dunetest
 
 dunetest:
 	@echo "#### Running (dune runtest)"
-	@dune runtest && echo OK || (echo "=>" Failure running dune test. && echo "=>" Run \`make testpromote\` to accept changes in test expectations. && false)
+	@dune runtest && echo OK || (echo "####>" Failure running dune test. && echo "####>" Run \`make testpromote\` to accept changes in test expectations. && false)
 
 testpromote:
 	dune promote
 
 $(TESTDIRS): test-%: exe
 	@echo "#### Running (cd $@; make test)"
-	@(cd $@ && (make test >$(LOG) || (cat $(LOG) && echo "=>" Failure running $@. See log above. && false)))
+	@(cd $@ && ((make test >$(LOG) 2>&1 && (grep warning $(LOG) || true)) || (cat $(LOG) && echo "####>" Failure running $@. See log above. && false)))
 
 
 # Cleanup

spectec/spec/wasm-1.0/1-syntax.watsup

@@ -160,12 +160,12 @@ syntax binop_(fnn) =
 
 syntax testop_(valtype)
 syntax testop_(inn) = | EQZ
-syntax testop_(fnn) = |      ;; uninhabited
+;; syntax testop_(fnn) = |      ;; uninhabited
 
 syntax relop_(valtype)
 syntax relop_(inn) =
-  | EQ | NE
-  | LT sx hint(show LT_#%) | GT sx hint(show GT_#%)
+  | EQ | NE \
+  | LT sx hint(show LT_#%) | GT sx hint(show GT_#%) \
   | LE sx hint(show LE_#%) | GE sx hint(show GE_#%)
 syntax relop_(fnn) =
   | EQ | NE | LT | GT | LE | GE
@@ -200,13 +200,13 @@ syntax instr/control hint(desc "control instruction") =
   | RETURN
   | ...
 
-syntax instr/numeric hint(desc "numeric instruction") = ...
+syntax instr/num hint(desc "numeric instruction") = ...
   | CONST valtype val_(valtype)      hint(show %.CONST %)
   | UNOP valtype unop_(valtype)      hint(show %.%)
   | BINOP valtype binop_(valtype)    hint(show %.%)
   | TESTOP valtype testop_(valtype)  hint(show %.%)
   | RELOP valtype relop_(valtype)    hint(show %.%)
-  | CVTOP valtype cvtop valtype sx?  hint(show %.%#_#%#_#%)
+  | CVTOP valtype_1 cvtop valtype_2 sx?  hint(show %.%#_#%#_#%)
   | ...
 
 syntax instr/local hint(desc "local instruction") = ...

spectec/spec/wasm-2.0/1-syntax.watsup

@@ -231,26 +231,26 @@ syntax binop_(fnn) =
 
 syntax testop_(numtype)
 syntax testop_(inn) = | EQZ
-syntax testop_(fnn) = |      ;; uninhabited
+;; syntax testop_(fnn) = |      ;; uninhabited
 
 syntax relop_(numtype)
 syntax relop_(inn) =
-  | EQ | NE
-  | LT sx hint(show LT_#%) | GT sx hint(show GT_#%)
+  | EQ | NE \
+  | LT sx hint(show LT_#%) | GT sx hint(show GT_#%) \
   | LE sx hint(show LE_#%) | GE sx hint(show GE_#%)
 syntax relop_(fnn) =
   | EQ | NE | LT | GT | LE | GE
 
-syntax cvtop = | CONVERT | REINTERPRET | CONVERT_SAT
+syntax cvtop = | CONVERT | CONVERT_SAT | REINTERPRET
 
 
 ;; Vector operators
 
 syntax dim hint(desc "dimension") = 1 | 2 | 4 | 8 | 16
-syntax shape hint(desc "shape") = lanetype X dim
-syntax ishape hint(desc "shape") = imm X dim
-syntax fshape hint(desc "shape") = fnn X dim
-syntax pshape hint(desc "shape") = pnn X dim
+syntax shape hint(desc "shape") = lanetype X dim  ;; TODO: hint(show %#X#%)
+syntax ishape hint(desc "shape") = imm X dim      ;; TODO: hint(show %#X#%)
+syntax fshape hint(desc "shape") = fnn X dim      ;; TODO: hint(show %#X#%)
+syntax pshape hint(desc "shape") = pnn X dim      ;; TODO: hint(show %#X#%)
 
 def $dim(shape) : dim
 def $shsize(shape) : nat  hint(show |%|)
@@ -279,7 +279,7 @@ syntax vbinop_(fnn X N) = | ADD | SUB | MUL | DIV | MIN | MAX | PMIN | PMAX
 
 syntax vtestop_(shape)
 syntax vtestop_(imm X N) = | ALL_TRUE
-syntax vtestop_(fnn X N) = |           ;; uninhabited
+;; syntax vtestop_(fnn X N) = |           ;; uninhabited
 
 syntax vrelop_(shape)
 syntax vrelop_(imm X N) = | EQ | NE | LT sx | GT sx | LE sx | GE sx
@@ -346,20 +346,20 @@ syntax instr/control hint(desc "control instruction") =
   | RETURN
   | ...
 
-syntax instr/numeric hint(desc "numeric instruction") = ...
+syntax instr/num hint(desc "numeric instruction") = ...
   | CONST numtype num_(numtype)      hint(show %.CONST %)
   | UNOP numtype unop_(numtype)      hint(show %.%)
   | BINOP numtype binop_(numtype)    hint(show %.%)
   | TESTOP numtype testop_(numtype)  hint(show %.%)
   | RELOP numtype relop_(numtype)    hint(show %.%)
-  | CVTOP numtype cvtop numtype sx?  hint(show %.%#_#%#_#%)
-  | EXTEND numtype n                 hint(show %.EXTEND#%)
+  | CVTOP numtype_1 cvtop numtype_1 sx?  hint(show %.%#_#%#_#%)
+  | EXTEND numtype N                 hint(show %.EXTEND#%#_S)
   | ...
 
 syntax half hint(desc "lane part") = | LOW | HIGH
 syntax zero = ZERO?
 
-syntax instr/vector hint(desc "vector instruction") = ...
+syntax instr/vec hint(desc "vector instruction") = ...
   | VCONST vectype vec_(vectype)        hint(show %.CONST %)
   | VVUNOP vectype vvunop               hint(show %.%)
   | VVBINOP vectype vvbinop             hint(show %.%)
@@ -388,7 +388,7 @@ syntax instr/vector hint(desc "vector instruction") = ...
   | ...
 ;; TODO: check for missing constraints
 
-syntax instr/reference hint(desc "reference instruction") = ...
+syntax instr/ref hint(desc "reference instruction") = ...
   | REF.NULL reftype
   | REF.FUNC funcidx
   | REF.IS_NULL