preping to break up type syntactic category

docs/petr4spec/Petr4-spec.mdk

@@ -392,7 +392,7 @@ function signature. judgment signature. environment signature.
 
 In the following we present P4 syntax. Note that we omitted annotations and meta-information since they are not required for type checking. Some notes about the syntax follows:
 
-
+- Type variables, denoted by $\typVar$, can also potentially be wildcards, denoted by \wildcard$.
 - Two types are provided. The first one is denoted by $\baseTyp$ which is the data types availabe in P4 language. The second one is denoted by $\typ$ and is the type generated by the type system which could be the result of a type declaration in a P4 program. 
 - Parameters, denoted by $\prmDef \typKind$, are paremeterized by the type they have, that is, $\typKind$ represent a type where it can either be $\baseTyp$ or $\typ$. This is because they are used in different places and depending on where they are used they may have a different type. 
 - For simplicity, we use the expanded format of parameter in most rules to have fine access to its direction and type. However, we often don't need its initializer so we omit that. Keep in mind that a parameter could or could not have an initializer.
@@ -437,38 +437,6 @@ In the following we present P4 syntax. Note that we omitted annotations and meta
 { .booktable }
 
 
-**Types of P4 expressions:**
-
-|     |      |     |     |
-|~~~~:|:~~~~:|:~~~~|:~~~~|
-| $\typ$ | $::=$ | $\boolTyp$ | $\qquad \text{booleans}$ |
-|   | $\vert$ | $\errTyp$ | $\qquad \text{errors}$ |
-|   | $\vert$ | $\integerTyp$ | $\qquad \text{infinite-precision integers}$ |
-|   | $\vert$ | $\intWidthTyp \width$ | $\qquad \text{fixed-width signed integers}$ |
-|   | $\vert$ | $\bitWidthTyp \width$ | $\qquad \text{fixed-width unsigned integers}$ |
-|   | $\vert$ | $\varBitTyp \width$ | $\qquad \text{variable-width integers}$ |
-|   | $\vert$ | $\typVar$ | $\qquad \text{type variables}$ |
-|   | $\vert$ | $\spcTyp \typ \typs$ | $\qquad \text{specialized type}$ |
-|   | $\vert$ | $\arrayTyp \typ \width$ | $\qquad \text{arrays}$ |
-|   | $\vert$ | $\tupleTyps \typs$ | $\qquad \text{tuples/lists}$ |
-|   | $\vert$ | $\stringTyp$ | $\qquad \text{strings}$ |
-|   | $\vert$ | $\voidTyp$ | $\qquad \text{void}$ |
-|   | $\vert$ | $\recordTyps$ | $\qquad \text{records/headers/header unions/structs}$ |
-|   | $\vert$ | $\setTyp \typ$ | $\qquad \text{sets}$ |
-|   | $\vert$ | $\matchKindTyp$ | $\qquad \text{match kinds}$ |
-|   | $\vert$ | $\newTypeTyp \typVar \typ$ | $\qquad \text{reference}$ |
-|   | $\vert$ | $\enumTypDef$ | $\qquad \text{serializable enums}$ |
-|   | $\vert$ | $\enumTypNoTypDef$ | $\qquad \text{enums}$ |
-|   | $\vert$ | $\packageTyp \typParams {\prmDefs \typ} \wildcardParams$ | $\qquad \text{packages}$ |
-|   | $\vert$ | $\controlTyp \typParams {\prmDefs \typ}$ | $\qquad \text{controls}$ |
-|   | $\vert$ | $\parserTyp \typParams {\prmDefs \typ}$ | $\qquad \text{parsers}$ |
-|   | $\vert$ | $\externTyp \name$ | $\qquad \text{externs}$ |
-|   | $\vert$ | $\funcType \kind \typParams \params \typ$ | $\qquad \text{functions}$ |
-|   | $\vert$ | $\actionTyp {\overline { {\prmDef \typ}}} {\overline {\VVal {\prmDef \typ}}}$ | $\qquad \text{actions}$ |
-|   | $\vert$ | $\constructorTyp \typParams {\prmDefs \typ} \wildcardParams \typ$ | $\qquad \text{constructors}$ |
-|   | $\vert$ | $\tableTyp \name$ | $\qquad \text{tables}$ |
-{ .booktable }
-
 **Unary operations:**
 
 |     |      |     |     |
@@ -663,10 +631,55 @@ Three judgments are provided for types of P4 expressions:
 - [type equality][#sec-type-eq]: checks the [alpha equalency][alpha-equiv-wiki] of two types.
 - [type unification][#sec-type-unify]: tries to unify two types by providing constraints of assignment of types to type variables. 
 
+``todo: type categories:
+surface type
+derived type
+synthesized type``
+``todo: check what's the difference of base type and reftype in p4 spec``
 
+~ Begin P4Syntax
+**Types produced by the type system:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\typ$ | $::=$ | $\boolTyp$ | $\qquad \text{booleans}$ |
+|   | $\vert$ | $\errTyp$ | $\qquad \text{errors}$ |
+|   | $\vert$ | $\integerTyp$ | $\qquad \text{infinite-precision integers}$ |
+|   | $\vert$ | $\intWidthTyp \width$ | $\qquad \text{fixed-width signed integers}$ |
+|   | $\vert$ | $\bitWidthTyp \width$ | $\qquad \text{fixed-width unsigned integers}$ |
+|   | $\vert$ | $\varBitTyp \width$ | $\qquad \text{variable-width integers}$ |
+|   | $\vert$ | $\typVar$ | $\qquad \text{type variables}$ |
+|   | $\vert$ | $\spcTyp \typ \typs$ | $\qquad \text{specialized type}$ |
+|   | $\vert$ | $\arrayTyp \typ \width$ | $\qquad \text{arrays}$ |
+|   | $\vert$ | $\tupleTyps \typs$ | $\qquad \text{tuples/lists}$ |
+|   | $\vert$ | $\stringTyp$ | $\qquad \text{strings}$ |
+|   | $\vert$ | $\voidTyp$ | $\qquad \text{void}$ |
+|   | $\vert$ | $\recordTyps \field \typ$ | $\qquad \text{records}$ |
+|   | $\vert$ | $\headerTyps \field \typ$ | $\qquad \text{headers}$ |
+|   | $\vert$ | $\headerUnionTyps \field \typ$ | $\qquad \text{header unions}$ |
+|   | $\vert$ | $\structTyps \field \typ$ | $\qquad \text{structs}$ |
+|   | $\vert$ | $\setTyp \typ$ | $\qquad \text{sets}$ |
+|   | $\vert$ | $\matchKindTyp$ | $\qquad \text{match kinds}$ |
+|   | $\vert$ | $\newTypeTyp \typVar \typ$ | $\qquad \text{reference}$ |
+|   | $\vert$ | $\enumTypDef$ | $\qquad \text{serializable enums}$ |
+|   | $\vert$ | $\enumTypNoTypDef$ | $\qquad \text{enums}$ |
+|   | $\vert$ | $\packageTyp \typParams {\prmDefs \typ}$ | $\qquad \text{packages}$ |
+|   | $\vert$ | $\controlTyp \typParams {\prmDefs \typ}$ | $\qquad \text{controls}$ |
+|   | $\vert$ | $\parserTyp \typParams {\prmDefs \typ}$ | $\qquad \text{parsers}$ |
+|   | $\vert$ | $\externTyp \name$ | $\qquad \text{externs}$ |
+|   | $\vert$ | $\funcType \kind \typParams {\prmDefs \typ} \typ$ | $\qquad \text{functions}$ |
+|   | $\vert$ | $\actionTyp {\overline { {\prmDef \typ}}} {\overline {\VVal {\prmDef \typ}}}$ | $\qquad \text{actions}$ |
+|   | $\vert$ | $\constructorTyp \typParams {\prmDefs \typ} \typ$ | $\qquad \text{constructors}$ |
+|   | $\vert$ | $\tableTyp \name$ | $\qquad \text{tables}$ |
+{ .booktable }
+
+
+~ End P4Syntax
 
 ## Type Well-Formed Judgment { #sec-type-well-formed }
 
+``todo: this must be defined on surface types.``
+
 This judgment checks if a type is well-formed. Note that this judgment is defined over the expression types and not P4's data types.
 It has the form $\typWellFormed \typ$ which states that the type $\typ$
 is well-formed under the type environment $\typEnv$ and extern environment $\externEnv$, that is, the type is syntactically correct. 
@@ -842,29 +855,40 @@ Note that headers, header unions, and struct also have the same type and their w
   \mprset {vskip=0.7ex}
   {\inferrule
      { \typWellFormed \typs \\
-       \isValidNestedTyp \recordTyps \\
+       \isValidNestedTyp {\recordTyps \field \typ} \\
        \noDup \fields}
-     { \typWellFormed \recordTyps }
+     { \typWellFormed {\recordTyps \field \typ} }
      \quad (\recordT)}
 
-  % \inferrule[HeaderUnion]
-  %    { 1 \leq i \leq n. \typWellFormed {\typ_i} \\
-  %      1 \leq i \leq n. \isValidNestedTyp \headerUnionTyp {\typ_i} \\
-  %      % \noDup {\field_1, \ldots, \field_n}\\
-  %      1 \leq i < j \leq n. \field_i \neq \field_j}
-  %    { \typWellFormed \headerUnionTyp }
+\and
 
-  % \inferrule[Struct]
-  %    { 1 \leq i \leq n. \typWellFormed {\typ_i} \\
-  %      1 \leq i \leq n. \isValidNestedTyp \structTypDef {\typ_i} \\
-  %      1 \leq i < j \leq n. \field_i \neq \field_j}
-  %    { \typWellFormed \structTypDef }
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     {\typWellFormed \typs \\
+       \isValidNestedTyp {\headerUnionTyps \field \typ} \\\\
+       \noDup \fields}
+     { \typWellFormed {\headerUnionTyps \field \typ} }
+     \quad (\headerUnionT)}
 
-  % \inferrule[Header]
-  %    { 1 \leq i \leq n. \typWellFormed {\typ_i} \\
-  %      1 \leq i \leq n. \isValidNestedTyp \headerTypDef {\typ_i} \\
-  %      1 \leq i < j \leq n. \field_i \neq \field_j}
-  %    { \typWellFormed \headerTypDef }
+\and
+
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     {\typWellFormed \typs \\
+       \isValidNestedTyp {\structTyps \field \typ} \\
+       \noDup \fields}
+     { \typWellFormed {\structTyps \field \typ} }
+     \quad (\structT)}
+
+\and
+
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     {\typWellFormed \typs \\
+       \isValidNestedTyp {\headerTyps \field \typ} \\
+       \noDup \fields}
+     { \typWellFormed {\headerTyps \field \typ} }
+     \quad (\headerT)}
 
 ~ End InfRule
 
@@ -927,7 +951,7 @@ The rule $\packageT$ states that a package type is well-formed under the environ
     {\inferrule
        { \isDirectionless {\dir} \\
          \typWellFormedWithEnv {\extendTypsEnv \typVar} \typs }
-       { \typWellFormed {\packageTyp {\typParams} {\prms} {\wildcardParams}} }
+       { \typWellFormed {\packageTyp {\typParams} {\prms} } }
      \quad (\packageT)}
 
 ~ End InfRule
@@ -1017,7 +1041,7 @@ The rule $\constructorT$ states that a constructor type is well-formed if its re
        % \prim \env = \insertTypVars {\param_1, \ldots, \param_n} \\
        \typWellFormedWithEnv {\extendTypEnv \typVars} {\typs} \\
        \isDirectionless {\dirs}}
-     { \typWellFormed {\constructorTyp \typParams \prms \wildcardParams {\typ}}}
+     { \typWellFormed {\constructorTyp \typParams \prms {\typ}}}
      \quad (\constructorT)}
 
 ~ End InfRule
@@ -1447,7 +1471,7 @@ The rule $\recordE$ is similar to $\listE$ rule.
 
   \inferrule
      {\expenv {\exps} {\overline {\prim \exp}} {\typs} {\dirs}}
-     {\expenv {\records \exp} {\records {\prim \exp}} {\recordTyps} \less  }
+     {\expenv {\records \exp} {\records {\prim \exp}} {\recordTyps \field \typ} \less  }
      \quad (\recordE)
 
 ~ End InfRule
@@ -1881,42 +1905,42 @@ P4 spec states during the cast between int and bit<w> or int<w> the compiler wou
 
   \inferrule
      {\explCast {\typs} {\overline {\prim \typ}}}
-     {\explCast {\recordTyps} {\headerTyps \field {\prim \typ}}}
+     {\explCast {\recordTyps \field \typ} {\headerTyps \field {\prim \typ}}}
      \quad (\rn{RecordToHeader}\rSep\rn{Explicit}\rAE\rSep\rn{1})
 
   \inferrule
-     {\typEqEnv \emp {\recordTyps} {\recordTypss \field {\prim \typ}}}
-     {\explCast {\recordTyps} {\headerTyps \field {\prim \typ}}}
+     {\typEqEnv \emp {\recordTyps \field \typ} {\recordTyps \field {\prim \typ}}}
+     {\explCast {\recordTyps \field \typ} {\headerTyps \field {\prim \typ}}}
      \quad (\rn{RecordToHeader}\rSep\rn{Explicit}\rAE\rSep\rn{2})
 
   \inferrule
      {\implCast {\typs} {\overline {\prim \typ}}}
-     {\implCast {\recordTyps} {\headerTyps \field {\prim \typ}}}
+     {\implCast {\recordTyps \field \typ} {\headerTyps \field {\prim \typ}}}
      \quad (\rn{RecordToHeader}\rSep\rn{Implicit}\rAE\rSep\rn{1})
 
   \inferrule
-     {\typEqEnv \emp {\recordTyps} {\recordTypss \field {\prim \typ}}}
-     {\implCast {\recordTyps} {\headerTyps \field {\prim \typ}}}
+     {\typEqEnv \emp {\recordTyps \field \typ} {\recordTyps \field {\prim \typ}}}
+     {\implCast {\recordTyps \field \typ} {\headerTyps \field {\prim \typ}}}
      \quad (\rn{RecordToHeader}\rSep\rn{Implicit}\rAE\rSep\rn{2})
 
   \inferrule
      {\explCast {\typs} {\overline {\prim \typ}}}
-     {\explCast {\recordTyps } {\structTyps \field {\prim \typ}}}
+     {\explCast {\recordTyps \field \typ } {\structTyps \field {\prim \typ}}}
      \quad (\rn{RecordToStruct}\rSep\rn{Explicit}\rAE\rSep\rn{1})
 
   \inferrule
-     {\typEqEnv \emp {\recordTyps} {\recordTypss \field {\prim \typ}}}
-     {\explCast {\recordTyps } {\structTyps \field {\prim \typ}}}
+     {\typEqEnv \emp {\recordTyps \field \typ} {\recordTyps \field {\prim \typ}}}
+     {\explCast {\recordTyps \field \typ } {\structTyps \field {\prim \typ}}}
      \quad (\rn{RecordToStruct}\rSep\rn{Explicit}\rAE\rSep\rn{2})
 
   \inferrule
      {\implCast {\typs} {\overline {\prim \typ}}}
-     {\implCast {\recordTyps } {\structTyps \field {\prim \typ}}}
+     {\implCast {\recordTyps \field \typ } {\structTyps \field {\prim \typ}}}
      \quad (\rn{RecordToStruct}\rSep\rn{Implicit}\rAE\rSep\rn{1})
 
   \inferrule
-     {\typEqEnv \emp {\recordTyps} {\recordTypss \field {\prim \typ}}}
-     {\implCast {\recordTyps } {\structTyps \field {\prim \typ}}}
+     {\typEqEnv \emp {\recordTyps \field \typ} {\recordTyps \field {\prim \typ}}}
+     {\implCast {\recordTyps \field \typ } {\structTyps \field {\prim \typ}}}
      \quad (\rn{RecordToStruct}\rSep\rn{Implicit}\rAE\rSep\rn{2})
 
   \inferrule
@@ -2403,15 +2427,15 @@ For detailed rules of this judgment refer to Section [#sec-type-unify].
   \mprset {vskip=0.5ex}
   {  \inferrule
          { \lookupEnv \name = \overline {(\typ, \dir)} \\
-            (\constructorTyp \typParams \wildcardParams \prms \retTyp, \dir) \in \overline {(\typ, \dir)}}
+            (\constructorTyp \typParams  \prms \retTyp, \dir) \in \overline {(\typ, \dir)}}
          { \resolveConstOver \name {\overline {\var = \exp}} \typParams \wildcardParams \prms \retTyp  }
          \quad (blah)
   }
 
   \mprset {vskip=0.5ex}
   {  \inferrule
          { \lookupEnv \name = \overline {(\typ, \dir)} \\
-            (\constructorTyp \typParams \wildcardParams \prms \retTyp, \dir) \in \overline {(\typ, \dir)} \\
+            (\constructorTyp \typParams  \prms \retTyp, \dir) \in \overline {(\typ, \dir)} \\
            |\removeOptionalPars \params| = |\argexps|}
          { \resolveConstOver \name \argexps \typParams \wildcardParams \prms \retTyp  }
          \quad (blah)

docs/petr4spec/ops.tex

@@ -1,5 +1,5 @@
 \newcommand{\VVal}[1]{#1'}
-%% \newcommand{\VVVal}[1]{#1''}
+\newcommand{\VVVal}[1]{#1''}
 
 
 %rule names:
@@ -35,6 +35,9 @@
 \newcommand*{\setT}{\rn{Set}\rT}
 \newcommand*{\enumTwoT}{\rn{SerializableEnum}\rT}
 \newcommand*{\recordT}{\rn{Record}\rT}
+\newcommand*{\headerUnionT}{\rn{HeaderUnion}\rT}
+\newcommand*{\headerT}{\rn{Header}\rT}
+\newcommand*{\structT}{\rn{Struct}\rT}
 \newcommand*{\newTypeT}{\rn{NewType}\rT}
 \newcommand*{\specializedExternT}{\rn{SpecializedType}\rSep\rn{ExternBase}\rT}
 \newcommand*{\specializedRestT}{\rn{SpecializedType}\rSep\rn{Rest}\rT}
@@ -278,11 +281,12 @@
 \newcommand{\val}{v}
 \newcommand{\bit}{b}
 \renewcommand{\int}{n}
-\newcommand{\bitWidth}[2]{{#2}\mathsf{b}{#1}}
-\newcommand{\intWidth}[2]{{#2}\mathsf{w}{#1}}
+\newcommand{\bitWidth}[2]{{#2}\mathsf{w}{#1}}
+\newcommand{\intWidth}[2]{{#2}\mathsf{s}{#1}}
 \newcommand{\name}{x}
 \newcommand{\var}{x}
 \newcommand{\typVar}{X}
+\newcommand{\typName}{x}
 \newcommand{\typVars}{\overline \typVar}
 %% \renewcommand{\array}{a}
 %% \renewcommand{\index}{i}
@@ -308,6 +312,7 @@
 \newcommand{\paris}[1]{\overline {\pari {#1}}}
 \newcommand{\pars}[2]{\pari {#1}, \ldots, \pari {#2}}
 % wildcard param for wild card type vars.
+\newcommand{\wildcard}{\_\!\_}
 \newcommand{\wildcardParam}{W}
 \newcommand{\wildcardParams}{\overline \wildcardParam}
 \renewcommand{\arg}{\mathit{arg}}
@@ -537,24 +542,26 @@
 \newcommand{\tupleTyps}[1]{\mathsf{tuple}\langle{#1}\rangle}
 \newcommand{\listTyp}[2]{\tupleTyp {#1} {#2}}
 \newcommand{\listTyps}[1]{\tupleTyps {#1}}
-\newcommand{\enumTypDef}{\mathsf{enum}\ {\typ}\ {\typVar}\ \{\fields\}}
+\newcommand{\enumTypDef}{\mathsf{enum}\ {\typ}\ {\typName}\ \{\fields\}}
 \newcommand{\enumTyp}[3]{\mathsf{enum}\ {#1}\ {#2}\ \{{#3}\}}
 \newcommand{\enumTypNoTypDef}{\mathsf{enum} \ {\name}\ \{\fields\}}
 \newcommand{\enumTypNoTyp}[2]{\mathsf{enum} \ {#1}\ \{{#2}\}}
 \newcommand{\recordTypDef}{\recordTyp 1 n}
-\newcommand{\recordTyp}[2]{\{\field_{#1}:\typ_{#1};\ldots;\field_{#2}:\typ_{#2}\}}
-\newcommand{\recordTypp}[2]{\{\prim {\field_{#1}}:\prim {\typ_{#1}};\ldots;\prim {\field_{#2}}:\prim {\typ_{#2}}\}}
-\newcommand{\recordTyps}{\{\overline {\field : \typ}\}}
-\newcommand{\recordTypss}[2]{\{\overline {{#1} : {#2}}\}}
-\newcommand{\headerUnionTyp}[2]{\recordTyp {#1} {#2}}
-\newcommand{\headerUnionTyps}[2]{\recordTypss {#1} {#2}}
-\newcommand{\headerTyp}[2]{\recordTyp {#1} {#2}}
-\newcommand{\structTyp}[2]{\recordTyp {#1} {#2}}
-\newcommand{\headerTyps}[2]{\recordTypss {#1} {#2}}
-\newcommand{\headerTypp}[2]{\recordTypp {#1} {#2}}
-\newcommand{\structTypp}[2]{\recordTypp {#1} {#2}}
-\newcommand{\structTypDef}{\recordTypDef}
-\newcommand{\structTyps}[2]{\recordTypss {#1} {#2}}
+\newcommand{\recordTypStructureOpen}[2]{\{\field_{#1}:\typ_{#1};\ldots;\field_{#2}:\typ_{#2}\}}
+\newcommand{\recordTypStructureClose}[2]{\{\overline {{#1} : {#2}}\}}
+\newcommand{\recordTyp}[2]{\mathsf{record} \{\field_{#1}:\typ_{#1};\ldots;\field_{#2}:\typ_{#2}\}}
+\newcommand{\recordTypp}[2]{\mathsf{record} \{\prim {\field_{#1}}:\prim {\typ_{#1}};\ldots;\prim {\field_{#2}}:\prim {\typ_{#2}}\}}
+%% \newcommand{\recordTyps}{\mathsf{record} \recordTypStructureClose \field \typ}
+\newcommand{\recordTyps}[2]{\mathsf{record} \recordTypStructureClose {#1} {#2}}
+\newcommand{\headerUnionTyp}[2]{\mathsf{header\_union} \recordTypStructureOpen {#1} {#2}}
+\newcommand{\headerUnionTyps}[2]{\mathsf{header\_union} \recordTypStructureClose {#1} {#2}}
+\newcommand{\headerTyp}[2]{\mathsf{header}\recordTypStructureOpen {#1} {#2}}
+\newcommand{\structTyp}[2]{\mathsf{struct} \recordTypStructureOpen {#1} {#2}}
+\newcommand{\headerTyps}[2]{\mathsf{header} \recordTypStructureClose {#1} {#2}}
+%% \newcommand{\headerTypp}[2]{\mathsf{header} \recordTypp {#1} {#2}}
+%% \newcommand{\structTypp}[2]{\mathsf{struct} \recordTypp {#1} {#2}}
+\newcommand{\structTypDef}{\mathsf{struct} \recordTypStructureOpen 1 n}
+\newcommand{\structTyps}[2]{\mathsf{struct} \recordTypStructureClose {#1} {#2}}
 %% \newcommand{\headerUnionTyp}{\mathit{header\_union}\{\field_1:\typ_1;\ldots;\field_n:\typ_n \}}
 %% \newcommand{\headerTypDef}{\headerTyp 1 n}
 %% \newcommand{\headerTyp}[2]{\mathit{header}\{\field_{#1}:\typ_{#1};\ldots;\field_{#2}:\typ_{#2}\}}
@@ -568,12 +575,16 @@
 %kind.type param. param. return type. 
 \newcommand{\funcType}[4]{\mathsf{function}\ {#1}\ \langle{#2}\rangle ({#3})\rightarrow {#4}}
 % type params: list of name. wildcard param: list of name. params: list of type dir name. return: typed.
-\newcommand{\constructorTyp}[4]{\mathsf{constructor}\langle{#1},{#2}\rangle\ ({#3}) \rightarrow {#4}}
+%% second arg is wildcard which is omitted for now. 
+%% \newcommand{\constructorTyp}[4]{\mathsf{constructor}\langle{#1},{#2}\rangle\ ({#3}) \rightarrow {#4}}
+\newcommand{\constructorTyp}[3]{\mathsf{constructor}\langle{#1},{#2}\rangle \rightarrow {#3}}
 \newcommand{\externTyp}[1]{\mathsf{extern} \  {#1}}
 \newcommand{\spcTyp}[2]{{#1}\langle{#2}\rangle}
 \newcommand{\parserTyp}[2]{\mathsf{parser}\langle{#1}\rangle({#2})}
 \newcommand{\controlTyp}[2]{\mathsf{control}\langle{#1}\rangle({#2})}
-\newcommand{\packageTyp}[3]{\mathsf{package}\langle{#1}\rangle({#2},{#3})}
+\newcommand{\packageTyp}[2]{\mathsf{package}\langle{#1}\rangle({#2})}
+%% the third arg is wildcard which is omitted for now.
+%% \newcommand{\packageTyp}[3]{\mathsf{package}\langle{#1}\rangle({#2},{#3})}
 \newcommand{\actionTyp}[2]{\mathsf{action}(\mathsf{data:}\ {#1},\mathsf{control:}\ {#2})}
 \newcommand{\tableTyp}[1]{\mathsf{table}\ {#1}}
 %% \newcommand{\typNameTyp}[1]{\mathsf{type\_name}\ {#1}}

lib/checker.ml

@@ -662,6 +662,8 @@ and reduce_type : CheckerEnv.t -> Typed.Type.t -> Typed.Type.t =
 (* [type_equality env t1 t2] is true if and only if expression type t1
  * is equivalent to expression type t2 under environment env.
  *  Alpha equivalent types are equal. *)
+
+(* so type equality is solve type with cast set to false and an empty unknowns*)
 and solve_types ?(casts=true)
                 (env: CheckerEnv.t)
                 (equiv_vars: (string * string) list)