From d356782e3011c665a02a9811c1214b17c79367ed Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 28 Jun 2024 08:47:58 +0200 Subject: [PATCH] Do not group star splices by default --- document/core/valid/matching.rst | 9 +++++---- document/core/valid/modules.rst | 8 ++++---- spectec/src/backend-splice/splice.ml | 8 +++++--- spectec/test-splice/TEST.md | 4 ++-- 4 files changed, 16 insertions(+), 13 deletions(-) diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 09a7572543..c9012be26c 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -94,7 +94,7 @@ A :ref:`reference type ` ${reftype: REF nul1 heaptype_1} matches * :math:`\NULL_1` is absent or :math:`\NULL_2` is present. -$${rule: Reftype_sub/*} +$${rule: {Reftype_sub/*}} .. index:: value type, number type, reference type @@ -197,7 +197,7 @@ A :ref:`composite type ` ${:comptype_1} matches a type ${:compt * The :ref:`field type ` :math:`\fieldtype_1` :ref:`matches ` :math:`\fieldtype_2`. -$${rule: Comptype_sub/*} +$${rule: {Comptype_sub/*}} .. index:: field type, storage type, value type, packed type, mutability @@ -216,7 +216,8 @@ A :ref:`field type ` ${fieldtype: (mut1 storagetype_1)} matche * Or both :math:`\mut_1` and :math:`\mut_2` are :math:`\MVAR` and :math:`\storagetype_2` :ref:`matches ` :math:`\storagetype_1` as well. -$${rule: Fieldtype_sub/*} +$${rule: {Fieldtype_sub/*}} + A :ref:`storage type ` :math:`\storagetype_1` matches a type :math:`\storagetype_2` if and only if: @@ -320,7 +321,7 @@ A :ref:`global type ` ${globaltype: (mut1 valtype_1)} matches * Or both :math:`\mut_1` and :math:`\mut_2` are |MCONST| and :math:`t_1` :ref:`matches ` :math:`t_2`. -$${rule: Globaltype_sub/*} +$${rule: {Globaltype_sub/*}} .. index:: external type, function type, table type, memory type, global type diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 22ae375179..c14ec6e089 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -47,7 +47,7 @@ $${rule: Type_ok} * Then the type sequence is valid. -$${rule: Types_ok/*} +$${rule: {Types_ok/*}} .. index:: function, local, function index, local index, type index, function type, value type, local type, expression, import @@ -88,7 +88,7 @@ Functions ${:func} are classified by :ref:`defined types ` that * Then the function definition is valid with type :math:`C.\CTYPES[x]`. -$${rule: Func_ok Local_ok} +$${rule: Func_ok} .. index:: local, local type, value type @@ -114,7 +114,7 @@ Locals ${:local} are classified with :ref:`local types `. * The local is valid with :ref:`local type ` :math:`\UNSET~\valtype`. -$${rule: Local_ok/*} +$${rule: {Local_ok/*}} .. note:: For cases where both rules are applicable, the former yields the more permissable type. @@ -209,7 +209,7 @@ $${rule: Global_ok} * Then the sequence is valid with the sequence of :ref:`global types ` consisting of :math:`\X{gt}_1` prepended to :math:`\X{gt}^\ast`. -$${rule: Globals_ok/*} +$${rule: {Globals_ok/*}} .. index:: element, table, table index, expression, constant, function index diff --git a/spectec/src/backend-splice/splice.ml b/spectec/src/backend-splice/splice.ml index aa8efd09b7..31de252024 100644 --- a/spectec/src/backend-splice/splice.ml +++ b/spectec/src/backend-splice/splice.ml @@ -196,19 +196,21 @@ let find_entry space src id1 id2 entries = error src ("duplicate " ^ space ^ " identifier `" ^ id1 ^ "/" ^ id2 ^ "`") *) +let ungroup = List.map (fun x -> [x]) + let find_syntax env src id1 id2 = match Map.find_opt id1 env.syn with | None -> error src ("unknown syntax identifier `" ^ id1 ^ "`") | Some syntax -> let defs = find_entries "syntax" src id1 id2 syntax.sfragments in - if id2 = "" then [defs] else List.map (fun def -> [def]) defs + if id2 = "" then [defs] else ungroup defs let find_grammar env src id1 id2 = match Map.find_opt id1 env.gram with | None -> error src ("unknown grammar identifier `" ^ id1 ^ "`") | Some grammar -> let defs = find_entries "grammar" src id1 id2 grammar.gfragments in - if id2 = "" then [defs] else List.map (fun def -> [def]) defs + if id2 = "" then [defs] else ungroup defs let find_relation env src id1 id2 = find_nosub "relation" src id1 id2; @@ -219,7 +221,7 @@ let find_relation env src id1 id2 = let find_rule env src id1 id2 = match Map.find_opt id1 env.rel with | None -> error src ("unknown relation identifier `" ^ id1 ^ "`") - | Some relation -> [find_entries "rule" src id1 id2 relation.rules] + | Some relation -> ungroup (find_entries "rule" src id1 id2 relation.rules) let find_def env src id1 id2 = find_nosub "definition" src id1 id2; diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md index 23c4b483d9..6c6585ad57 100644 --- a/spectec/test-splice/TEST.md +++ b/spectec/test-splice/TEST.md @@ -155,7 +155,7 @@ $$ }{ C \vdash \epsilon : \epsilon \rightarrow \epsilon } \, {[\textsc{\scriptsize T{-}instr*{-}empty}]} -\qquad +\\[3ex]\displaystyle \frac{ C \vdash {{\mathit{instr}}^\ast} : {t_1^\ast}~{\rightarrow}_{({x^\ast})}\,{t_2^\ast} \qquad @@ -297,7 +297,7 @@ $$ $$ \begin{array}{@{}l@{}rcl@{}l@{}} {[\textsc{\scriptsize E{-}if{-}true}]} \quad & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c)~(\mathsf{if}~{\mathit{bt}}~{{\mathit{instr}}_1^\ast}~\mathsf{else}~{{\mathit{instr}}_2^\ast}) &\hookrightarrow& (\mathsf{block}~{\mathit{bt}}~{{\mathit{instr}}_1^\ast}) - &\qquad \mbox{if}~c \neq 0 \\ + &\qquad \mbox{if}~c \neq 0 \\[0.8ex] {[\textsc{\scriptsize E{-}if{-}false}]} \quad & (\mathsf{i{\scriptstyle 32}}{.}\mathsf{const}~c)~(\mathsf{if}~{\mathit{bt}}~{{\mathit{instr}}_1^\ast}~\mathsf{else}~{{\mathit{instr}}_2^\ast}) &\hookrightarrow& (\mathsf{block}~{\mathit{bt}}~{{\mathit{instr}}_2^\ast}) &\qquad \mbox{if}~c = 0 \\ \end{array}