8000 Fix tt again · WebAssembly/spec@5cf8e64 · GitHub
[go: up one dir, main page]
Skip to content

Commit 5cf8e64

Browse files
rossbergrossberg
committed
Fix tt again
1 parent e920cee commit 5cf8e64

File tree

8 files changed

+1338
-1288
lines changed

8 files changed

+1338
-1288
lines changed

‎specification/wasm-3.0/6.3-text.modules.spectec‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -312,7 +312,7 @@ def $exportsd(export decl'*) = export $exportsd(decl'*)
312312
def $exportsd(decl decl'*) = $exportsd(decl'*) -- otherwise
313313

314314
def $ordered(decl*) : bool
315-
def $ordered(decl'*) = ($importsd(decl'*) = eps)
315+
def $ordered(decl'*) = true -- if $importsd(decl'*) = eps
316316
def $ordered(decl_1* import decl_2*) =
317317
$importsd(decl_1*) = eps /\ $tagsd(decl_1*) = eps /\
318318
$globalsd(decl_1*) = eps /\ $memsd(decl_1*) = eps /\

‎spectec/doc/example/output/NanoWasm.pdf‎

0 Bytes
Binary file not shown.

‎spectec/src/backend-latex/render.ml‎

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1073,7 +1073,7 @@ Printf.eprintf "[render_atom %s @ %s] id=%s def=%s macros: %s (%s)\n%!"
10731073

10741074
let render_text s =
10751075
let buf = Buffer.create (String.length s + 32) in
1076-
Buffer.add_string buf "\\mbox{‘}\\mathtt{";
1076+
Buffer.add_string buf "\\mbox{‘\\texttt{";
10771077
for i = 0 to String.length s - 1 do
10781078
match s.[i] with
10791079
| '\'' -> Buffer.add_string buf "\\kern0.03em{'}\\kern0.03em" (* TODO: not typeset in TT *)
@@ -1086,20 +1086,20 @@ let render_text s =
10861086
| '=' -> Buffer.add_string buf "{=}"
10871087
| '<' -> Buffer.add_string buf "{<}"
10881088
| '>' -> Buffer.add_string buf "{>}"
1089-
| '-' -> Buffer.add_string buf "\\mbox{\\tt-}"
1090-
| '(' -> Buffer.add_string buf "\\mbox{\\tt(}"
1091-
| ')' -> Buffer.add_string buf "\\mbox{\\tt)}"
1092-
| '{' -> Buffer.add_string buf "\\mbox{\\tt\\{}"
1093-
| '}' -> Buffer.add_string buf "\\mbox{\\tt\\}}"
1094-
| '[' -> Buffer.add_string buf "\\mbox{\\tt[}"
1095-
| ']' -> Buffer.add_string buf "\\mbox{\\tt]}"
1096-
| '\\' -> Buffer.add_string buf "{\\backslash}" (* TODO: not typeset in TT *)
1097-
| '^' -> Buffer.add_string buf "\\hat{~~}"
1098-
| '`' -> Buffer.add_string buf "\\grave{~~}"
1099-
| '~' -> Buffer.add_string buf "\\tilde{~~}"
1089+
| '-' -> Buffer.add_string buf "{-}"
1090+
| '(' -> Buffer.add_string buf "{(}"
1091+
| ')' -> Buffer.add_string buf "{)}"
1092+
| '{' -> Buffer.add_string buf "{\\{}"
1093+
| '}' -> Buffer.add_string buf "{\\}}"
1094+
| '[' -> Buffer.add_string buf "{[}"
1095+
| ']' -> Buffer.add_string buf "{]}"
1096+
| '\\' -> Buffer.add_string buf "$\\mathtt{\\backslash}$" (* TODO: not typeset in TT *)
1097+
| '^' -> Buffer.add_string buf "$\\mathtt{\\hat{~~}}$"
1098+
| '`' -> Buffer.add_string buf "$\\mathtt{\\grave{~~}}$"
1099+
| '~' -> Buffer.add_string buf "$\\mathtt{\\tilde{~~}}$"
11001100
| c -> Buffer.add_char buf c
11011101
done;
1102-
Buffer.add_string buf "}\\mbox{’}";
1102+
Buffer.add_string buf "}’}";
11031103
Buffer.contents buf
11041104

11051105

‎spectec/test-frontend/TEST.md‎

Lines changed: 97 additions & 98 deletions
Large diffs are not rendered by default.

‎spectec/test-latex/TEST.md‎

Lines changed: 899 additions & 847 deletions
Large diffs are not rendered by default.

‎spectec/test-middlend/TEST.md‎

Lines changed: 291 additions & 294 deletions
Large diffs are not rendered by default.

‎spectec/test-prose/TEST.md‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -26488,8 +26488,8 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
2648826488
#. Return :math:`{{\mathit{val}'}^{k}}`.
2648926489

2649026490

26491-
:math:`{\mathrm{concat}}_{\mathit{idctxt}}({{\mathit{idctxt}}^\ast})`
26492-
.....................................................................
26491+
:math:`{\bigoplus}\, {{\mathit{idctxt}}^\ast}`
26492+
..............................................
2649326493

2649426494

2649526495
1. If :math:`{{\mathit{idctxt}}^\ast} = \epsilon`, then:
@@ -26648,12 +26648,10 @@ The instruction sequence :math:`(\mathsf{block}~{\mathit{blocktype}}~{{\mathit{i
2664826648
..................................................
2664926649

2665026650

26651-
1. If :math:`{{\mathit{decl}}^\ast} = \epsilon`, then:
26651+
1. If :math:`{\mathrm{imports}}({{\mathit{decl}}^\ast}) = \epsilon`, then:
2665226652

2665326653
a. Return true.
2665426654

26655-
#. Return :math:`{\mathrm{imports}}({{\mathit{decl}}^\ast}) = \epsilon`.
26656-
2665726655
#. Assert: Due to validation, YetE: Nondeterministic assignment target: decl_1*{decl_1 <- decl_1*} :: [import] :: decl_2*{decl_2 <- decl_2*}.
2665826656

2665926657
#. Let :math:`{{\mathit{decl}}_1^\ast}~{\mathit{import}}~{{\mathit{decl}}_2^\ast}` be :math:`{{\mathit{decl}}^\ast}`.
@@ -32954,12 +32952,11 @@ exportsd decl'*
3295432952
3. Return [export] :: $exportsd(decl'*).
3295532953

3295632954
ordered decl*
32957-
1. If (decl* = []), then:
32955+
1. If ($importsd(decl*) = []), then:
3295832956
a. Return true.
32959-
2. Return ($importsd(decl*) = []).
32960-
3. Assert: Due to validation, YetE (Nondeterministic assignment target: decl_1*{decl_1 <- decl_1*} :: [import] :: decl_2*{decl_2 <- decl_2*}).
32961-
4. Let decl_1* :: [import] :: decl_2* be decl*.
32962-
5. Return (((((($importsd(decl_1*) = []) /\ ($tagsd(decl_1*) = [])) /\ ($globalsd(decl_1*) = [])) /\ ($memsd(decl_1*) = [])) /\ ($tablesd(decl_1*) = [])) /\ ($funcsd(decl_1*) = [])).
32957+
2. Assert: Due to validation, YetE (Nondeterministic assignment target: decl_1*{decl_1 <- decl_1*} :: [import] :: decl_2*{decl_2 <- decl_2*}).
32958+
3. Let decl_1* :: [import] :: decl_2* be decl*.
32959+
4. Return (((((($importsd(decl_1*) = []) /\ ($tagsd(decl_1*) = [])) /\ ($globalsd(decl_1*) = [])) /\ ($memsd(decl_1*) = [])) /\ ($tablesd(decl_1*) = [])) /\ ($funcsd(decl_1*) = [])).
3296332960

3296432961
allocXs `X `Y s X''* Y''*
3296532962
1. If (X''* = []), then:

‎spectec/test-splice/TEST.md‎

Lines changed: 30 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,6 @@ $$
5959
& & | & \mathsf{block}~{\mathit{blocktype}}~{{\mathit{instr}}^\ast} \\
6060
& & | & \mathsf{loop}~{\mathit{blocktype}}~{{\mathit{instr}}^\ast} \\
6161
& & | & \mathsf{if}~{\mathit{blocktype}}~{{\mathit{instr}}^\ast}~\mathsf{else}~{{\mathit{instr}}^\ast} \\
62-
& & | & \dots \\
6362
\end{array}
6463
$$
6564

@@ -87,8 +86,7 @@ $$
8786
& & | & \mathsf{memory{.}grow}~{\mathit{memidx}} \\
8887
& & | & \mathsf{memory{.}fill}~{\mathit{memidx}} \\
8988
& & | & \mathsf{memory{.}copy}~{\mathit{memidx}}~{\mathit{memidx}} \\
90-
& & | & \mathsf{memory{.}init}~{\mathit{memidx}}~{\mathit{dataidx}} \\
91-
& & | & \dots \\[0.8ex]
89+
& & | & \mathsf{memory{.}init}~{\mathit{memidx}}~{\mathit{dataidx}} \\[0.8ex]
9290
& {\mathit{expr}} & ::= & {{\mathit{instr}}^\ast} \\
9391
\end{array}
9492
$$
@@ -693,7 +691,7 @@ warning: grammar `Tannot` was never spliced
693691
warning: grammar `Tannotid` was never spliced
694692
warning: grammar `Tblockchar` was never spliced
695693
warning: grammar `Tblockcomment` was never spliced
696-
warning: grammar `Tblockinstr_` was never spliced
694+
warning: grammar `Tblockinstr_/plain` was never spliced
697695
warning: grammar `Tblockinstr_/abbrev` was never spliced
698696
warning: grammar `Tblocktype_` was never spliced
699697
warning: grammar `Tcatch_` was never spliced
@@ -702,15 +700,17 @@ warning: grammar `Tcomment` was never spliced
702700
warning: grammar `Tcomptype_` was never spliced
703701
warning: grammar `Tdata_` was never spliced
704702
warning: grammar `Tdataidx_` was never spliced
705-
warning: grammar `Tdatamemory_/abbrev` was never spliced
703+
warning: grammar `Tdatamem_/abbrev` was never spliced
706704
warning: grammar `Tdatastring` was never spliced
707705
warning: grammar `Tdecl_` was never spliced
706+
warning: grammar `Tdecldots_` was never spliced
708707
warning: grammar `Tdigit` was never spliced
709-
warning: grammar `Telem_` was never spliced
710-
warning: grammar `Telemexpr_` was never spliced
708+
warning: grammar `Telem_/plain` was never spliced
709+
warning: grammar `Telem_/abbrev` was never spliced
710+
warning: grammar `Telemexpr_/plain` was never spliced
711711
warning: grammar `Telemexpr_/abbrev` was never spliced
712712
warning: grammar `Telemidx_` was never spliced
713-
warning: grammar `Telemlist_` was never spliced
713+
warning: grammar `Telemlist_/plain` was never spliced
714714
warning: grammar `Telemlist_/abbrev` was never spliced
715715
warning: grammar `Telemtable_/abbrev` was never spliced
716716
warning: grammar `Teof` was never spliced
@@ -720,8 +720,8 @@ warning: grammar `Texportfunc_/abbrev` was never spliced
720720
warning: grammar `Texportfuncdots_` was never spliced
721721
warning: grammar `Texportglobal_/abbrev` was never spliced
722722
warning: grammar `Texportglobaldots_` was never spliced
723-
warning: grammar `Texportmemory_/abbrev` was never spliced
724-
warning: grammar `Texportmemorydots_` was never spliced
723+
warning: grammar `Texportmem_/abbrev` was never spliced
724+
warning: grammar `Texportmemdots_` was never spliced
725725
warning: grammar `Texporttable_/abbrev` was never spliced
726726
warning: grammar `Texporttabledots_` was never spliced
727727
warning: grammar `Texporttag_/abbrev` was never spliced
@@ -764,11 +764,15 @@ warning: grammar `TiN` was never spliced
764764
warning: grammar `Tid` 4020 was never spliced
765765
warning: grammar `Tidchar` was never spliced
766766
warning: grammar `Tidx_` was never spliced
767-
warning: grammar `Timport_` was never spliced
768-
warning: grammar `Timport_/abbrev` was never spliced
767+
warning: grammar `Timport_/plain` was never spliced
768+
warning: grammar `Timport_/abbrev-tag` was never spliced
769+
warning: grammar `Timport_/abbrev-global` was never spliced
770+
warning: grammar `Timport_/abbrev-mem` was never spliced
771+
warning: grammar `Timport_/abbrev-table` was never spliced
772+
warning: grammar `Timport_/abbrev-func` was never spliced
769773
warning: grammar `Timportdots` was never spliced
770774
warning: grammar `Tinstr_` was never spliced
771-
warning: grammar `Tinstrs_` was never spliced
775+
warning: grammar `Tinstrs_/unfolded` was never spliced
772776
warning: grammar `Tinstrs_/folded` was never spliced
773777
warning: grammar `Tkeyword` was never spliced
774778
warning: grammar `Tlabel_` was never spliced
@@ -778,41 +782,41 @@ warning: grammar `Tlimits` was never spliced
778782
warning: grammar `Tlinechar` was never spliced
779783
warning: grammar `Tlinecomment` was never spliced
780784
warning: grammar `Tlist` was never spliced
781-
warning: grammar `Tlocal_` was never spliced
785+
warning: grammar `Tlocal_/plain` was never spliced
782786
warning: grammar `Tlocal_/abbrev` was never spliced
783787
warning: grammar `Tlocalidx_` was never spliced
784788
warning: grammar `Tmant` was never spliced
785789
warning: grammar `Tmem_` was never spliced
786790
warning: grammar `Tmemarg_` was never spliced
787791
warning: grammar `Tmemidx_` was never spliced
788792
warning: grammar `Tmemtype_` was never spliced
789-
warning: grammar `Tmemuse_` was never spliced
793+
warning: grammar `Tmemuse_/plain` was never spliced
790794
warning: grammar `Tmemuse_/abbrev` was never spliced
791-
warning: grammar `Tmodule` was never spliced
795+
warning: grammar `Tmodule/plain` was never spliced
792796
warning: grammar `Tmodule/abbrev` was never spliced
793797
warning: grammar `Tname` was never spliced
794798
warning: grammar `Tnewline` was never spliced
795799
warning: grammar `Tnull` was never spliced
796800
warning: grammar `Tnum` was never spliced
797801
warning: grammar `Tnumtype` was never spliced
798802
warning: grammar `Toffset` was never spliced
799-
warning: grammar `Toffset_` was never spliced
803+
warning: grammar `Toffset_/plain` was never spliced
800804
warning: grammar `Toffset_/abbrev` was never spliced
801805
warning: grammar `Tpacktype` was never spliced
802806
warning: grammar `Tparam_/base` was never spliced
803807
warning: grammar `Tparam_/abbrev` was never spliced
804808
warning: grammar `Tplaininstr_/parametric` was never spliced
805809
warning: grammar `Tplaininstr_/br` was never spliced
806-
warning: grammar `Tplaininstr_/func` was never spliced
807-
warning: grammar `Tplaininstr_/func/abbrev` was never spliced
810+
warning: grammar `Tplaininstr_/func-plain` was never spliced
811+
warning: grammar `Tplaininstr_/func-abbrev` was never spliced
808812
warning: grammar `Tplaininstr_/exn` was never spliced
809813
warning: grammar `Tplaininstr_/local` was never spliced
810814
warning: grammar `Tplaininstr_/global` was never spliced
811-
warning: grammar `Tplaininstr_/table` was never spliced
812-
warning: grammar `Tplaininstr_/table/abbrev` was never spliced
815+
warning: grammar `Tplaininstr_/table-plain` was never spliced
816+
warning: grammar `Tplaininstr_/table-abbrev` was never spliced
813817
warning: grammar `Tplaininstr_/elem` was never spliced
814-
warning: grammar `Tplaininstr_/memory` was never spliced
815-
warning: grammar `Tplaininstr_/memory/abbrev` was never spliced
818+
warning: grammar `Tplaininstr_/memory-plain` was never spliced
819+
warning: grammar `Tplaininstr_/memory-abbrev` was never spliced
816820
warning: grammar `Tplaininstr_/data` was never spliced
817821
warning: grammar `Tplaininstr_/ref` was never spliced
818822
warning: grammar `Tplaininstr_/i31` was never spliced
@@ -918,11 +922,11 @@ warning: grammar `Tsubtype_/abbrev` was never spliced
918922
warning: grammar `Tsym` was never spliced
919923
warning: grammar `Tsymsplit/1` was never spliced
920924
warning: grammar `Tsymsplit/2` was never spliced
921-
warning: grammar `Ttable_` was never spliced
925+
warning: grammar `Ttable_/plain` was never spliced
922926
warning: grammar `Ttable_/abbrev` was never spliced
923927
warning: grammar `Ttableidx_` was never spliced
924928
warning: grammar `Ttabletype_` was never spliced
925-
warning: grammar `Ttableuse_` was never spliced
929+
warning: grammar `Ttableuse_/plain` was never spliced
926930
warning: grammar `Ttableuse_/abbrev` was never spliced
927931
warning: grammar `Ttag_` was never spliced
928932
warning: grammar `Ttagidx_` was never spliced
@@ -1517,6 +1521,7 @@ warning: definition `demote__` was never spliced
15171521
warning: definition `diffrt` was never spliced
15181522
warning: definition `dim` was never spliced
15191523
warning: definition `disjoint_` was never spliced
1524+
warning: definition `dots` was never spliced
15201525
warning: definition `elem` was never spliced
15211526
warning: definition `eleminst` was never spliced
15221527
warning: definition `elemsd` was never spliced

0 commit comments

Comments
 (0)
0