applied pr comments

verified-network-toolchain · Oct 10, 2022 · 73bfc0b · 73bfc0b
1 parent f0b0c05
commit 73bfc0b
Show file tree

Hide file tree

Showing 2 changed files with 39 additions and 30 deletions.
diff --git a/docs/petr4spec/Petr4-spec.mdk b/docs/petr4spec/Petr4-spec.mdk
@@ -441,37 +441,37 @@ In the following we present P4 syntax. Note that we omitted annotations and meta
 
 |     |      |     |     |
 |~~~~:|:~~~~:|:~~~~|:~~~~|
-| $\unaryOp$ | $::=$ | $!$ | $\qquad \text{logical negation}$ |
+| $\unaryOp$ | $::=$ | $\intoOp !$ | $\qquad \text{logical negation}$ |
 |   | $\vert$ | $\bitComplement$ | $\qquad \text{bitwise complement}$ |
-|   | $\vert$ | $-$ | $\qquad \text{unary minus}$ |
+|   | $\vert$ | $\intoOp -$ | $\qquad \text{unary minus}$ |
 { .booktable }
 
 **Binary operations:**
 
 |     |      |     |     |
 |~~~~:|:~~~~:|:~~~~|:~~~~|
-| $\binOp$ | $::=$ | $\&\&$ | $\qquad \text{logical and}$ |
-|   | $\vert$ | $\vert\vert$ | $\qquad \text{logical or}$ |
-|   | $\vert$ | $+$ | $\qquad \text{numerical addition}$ |
-|   | $\vert$ | $-$ | $\qquad \text{numerical subtraction}$ |
-|   | $\vert$ | $*$ | $\qquad \text{numerical multiplication}$ |
-|   | $\vert$ | $\div$ | $\qquad \text{numerical division}$ |
-|   | $\vert$ | $\mod$ | $\qquad \text{numerical modulo}$ |
-|   | $\vert$ | $==$ | $\qquad \text{equality check}$ |
-|   | $\vert$ | $!=$ | $\qquad \text{inequality check}$ |
-|   | $\vert$ | $\plusSat$ | $\qquad \text{saturating addition}$ |
-|   | $\vert$ | $\subSat$ | $\qquad \text{saturation subtraction}$ |
-|   | $\vert$ | $\bitAnd$ | $\qquad \text{bitwise and}$ |
-|   | $\vert$ | $\bitOr$ | $\qquad \text{bitwise or}$ |
+| $\binOp$ | $::=$ | $\intoOp{\&\&}$ | $\qquad \text{logical and}$ |
+|   | $\vert$ | $\intoOp \logor $ | $\qquad \text{logical or}$ |
+|   | $\vert$ | $\intoOp +$ | $\qquad \text{numerical addition}$ |
+|   | $\vert$ | $\intoOp -$ | $\qquad \text{numerical subtraction}$ |
+|   | $\vert$ | $\intoOp *$ | $\qquad \text{numerical multiplication}$ |
+|   | $\vert$ | $\intoOp \div$ | $\qquad \text{numerical division}$ |
+|   | $\vert$ | $\intoOp \mod$ | $\qquad \text{numerical modulo}$ |
+|   | $\vert$ | $\intoOp{==}$ | $\qquad \text{equality check}$ |
+|   | $\vert$ | $\intoOp{!=}$ | $\qquad \text{inequality check}$ |
+|   | $\vert$ | $\intoOp \plusSat$ | $\qquad \text{saturating addition}$ |
+|   | $\vert$ | $\intoOp \subSat$ | $\qquad \text{saturation subtraction}$ |
+|   | $\vert$ | $\intoOp \bitAnd$ | $\qquad \text{bitwise and}$ |
+|   | $\vert$ | $\intoOp \bitOr$ | $\qquad \text{bitwise or}$ |
 |   | $\vert$ | $\bitXor$ | $\qquad \text{bitwise xor}$ |
 |   | $\vert$ | $\bitComplement$ | $\qquad \text{bitwise complement}$ |
-|   | $\vert$ | $\concat$ | $\qquad \text{bitwise concatenation}$ |
+|   | $\vert$ | $\intoOp \concat$ | $\qquad \text{bitwise concatenation}$ |
 |   | $\vert$ | $\shiftL$ | $\qquad \text{shift left}$ |
-|   | $\vert$ | $\shiftR$ | $\qquad \text{shift right}$ |
-|   | $\vert$ | $<$ | $\qquad \text{less than}$ |
-|   | $\vert$ | $\leq$ | $\qquad \text{less than or equal}$ |
-|   | $\vert$ | $>$ | $\qquad \text{greater than}$ |
-|   | $\vert$ | $\geq$ | $\qquad \text{greater than or equal}$ |
+|   | $\vert$ | $ \shiftR$ | $\qquad \text{shift right}$ |
+|   | $\vert$ | $\intoOp <$ | $\qquad \text{less than}$ |
+|   | $\vert$ | $ \leq$ | $\qquad \text{less than or equal}$ |
+|   | $\vert$ | $\intoOp >$ | $\qquad \text{greater than}$ |
+|   | $\vert$ | $ \geq$ | $\qquad \text{greater than or equal}$ |
 { .booktable }
 
 **Arguments:**
@@ -549,6 +549,8 @@ In the following we present P4 syntax. Note that we omitted annotations and meta
 |     |      |     |     |
 |~~~~:|:~~~~:|:~~~~|:~~~~|
 | $\nxt$ | $::=$ | $\str$ | $\qquad \text{next state}$ |
+|   | $\vert$ | $\accept$ | $\qquad \text{accept state}$|
+|   | $\vert$ | $\reject$ | $\qquad \text{reject state}$|
 | $\pmatch$ | $::=$ | $\defMatch$ | $\qquad \text{default match}$ |
 |   | $\vert$ | $\dontcareMatch$ | $\qquad \text{don't care match}$ |
 |   | $\vert$ | $\exp$ | $\qquad \text{expression match}$ |
@@ -604,8 +606,8 @@ In the following we present P4 syntax. Note that we omitted annotations and meta
 |   | $\vert$ | $\externObjDcl \var \typVars \extMethods$ | $\qquad \text{extern objects}$ |
 |   | $\vert$ | $\typdefDcl \typVar \baseTyp$ | $\qquad \text{type definitions}$ |
 |   | $\vert$ | $\typdefDcl \typVar \dcl$ | $\qquad \text{type definitions (declarations)}$ |
-|   | $\vert$ | $\newtypeDcl \typVar \baseTyp$ | $\qquad \text{generative type definitions}$ |
-|   | $\vert$ | $\newtypeDcl \typVar \dcl$ | $\qquad \text{generative type definitions (declarations)}$ |
+|   | $\vert$ | $\newtypeDcl  \baseTyp \typVar$ | $\qquad \text{generative type definitions}$ |
+|   | $\vert$ | $\newtypeDcl  \dcl \typVar$ | $\qquad \text{generative type definitions (declarations)}$ |
 |   | $\vert$ | $\controlTypDcl \typVar \typVars {\prmDefs \baseTyp}$ | $\qquad \text{control types}$ |
 |   | $\vert$ | $\parserTypDcl \typVar \typVars {\prmDefs \baseTyp}$ | $\qquad \text{parser types}$ |
 |   | $\vert$ | $\packageTypDcl \typVar \typVars {\prmDefs \baseTyp}$ | $\qquad \text{package types}$ |

diff --git a/docs/petr4spec/ops.tex b/docs/petr4spec/ops.tex
@@ -233,10 +233,11 @@
 \newcommand{\unaryOp}{\ominus}
 \newcommand{\binOp}{\oplus}
 \newcommand{\cast}[2]{({#1})\,{#2}}
-\newcommand{\plusSat}{\vert+\vert}
-\newcommand{\subSat}{\vert-\vert}
+\newcommand{\plusSat}{|+|}
+\newcommand{\subSat}{|-|}
+\newcommand{\logor}{||}
 \newcommand{\bitAnd}{\&}
-\newcommand{\bitOr}{\vert}
+\newcommand{\bitOr}{|}
 \newcommand{\bitXor}{\hat{}}
 \newcommand{\bitComplement}{\sim\!}
 \renewcommand{\div}{/}
@@ -254,6 +255,9 @@
 \newcommand{\records}[1]{\{\overline {\field = {#1}} \}}
 
 
+%operators:
+\newcommand{\intoOp}[1]{\texttt{#1}}
+
 %metavariables:
 \newcommand{\prmDef}[1]{\mathit{prm}_{#1}}
 \newcommand{\prmDefs}[1]{\overline {\prmDef {#1}}}
@@ -356,7 +360,9 @@
 \newcommand{\slctTran}[2]{({#1})\ \{{#2}\}}
 \newcommand{\expandCase}[2]{{#1} \ {#2}}
 \newcommand{\nxt}{\mathit{nxt}}
-\newcommand{\dontcareMatch}{\mathsf{dont\_care}}
+\newcommand{\accept}{\mathsf{accept}}
+\newcommand{\reject}{\mathsf{reject}}
+\newcommand{\dontcareMatch}{\mathsf{dontcare}}
 \newcommand{\defMatch}{\mathsf{default}}
 \newcommand{\pmatch}{\mathit{mtch}}
 \newcommand{\pmatches}{\overline \pmatch}
@@ -413,9 +419,10 @@
 \newcommand{\errDcl}[1]{\mathsf{error}\ \{ {#1} \}}
 \newcommand{\matchkindDcl}[1]{\mathsf{match\_kind}\ \{{#1}\}}
 \newcommand{\enumDcl}[2]{\mathsf{enum}\ {#1}\, \{{#2} \}}
-\newcommand{\serEnumDcl}[4]{\mathsf{enum}\ {#1} \, {#2}\, \{\overline {{#3}:{#4}} \}}
+\newcommand{\serEnumDcl}[4]{\mathsf{enum}\ {#1} \, {#2}\, \{\overline {{#3}={#4}} \}}
 \newcommand{\externObjDcl}[3]{\mathsf{extern}\ {#1}\, \langle{#2}\rangle\, \{{#3} \}}
-\newcommand{\newtypeDcl}[2]{{#1}={#2}}
+%type \rho \typename
+\newcommand{\newtypeDcl}[2]{\mathsf{type} \ {#1}\ {#2}}
 \newcommand{\typdefDcl}[2]{\mathsf{typedef}\ {#2}\, {#1}}
 \newcommand{\controlTypDcl}[3]{\mathsf{control}\ {#1}\, \langle{#2}\rangle\, ({#3})}
 \newcommand{\parserTypDcl}[3]{\mathsf{parser}\ {#1}\, \langle{#2}\rangle\, ({#3})}
@@ -525,7 +532,7 @@
 \newcommand{\newtypKey}{\mathsf{newtype}}
 
 %types:
-\newcommand{\dontcareTyp}{\mathsf{dont\_care}}
+\newcommand{\dontcareTyp}{\mathsf{dontcare}}
 \newcommand{\bitWidthTyp}[1]{\mathsf{bit}\langle{#1}\rangle}
 \newcommand{\intWidthTyp}[1]{\mathsf{int}\langle{#1}\rangle}
 \newcommand{\boolTyp}{\mathsf{bool}}