diff --git a/docs/petr4spec/Makefile b/docs/petr4spec/Makefile
index 62c04f908..4990621ce 100644
--- a/docs/petr4spec/Makefile
+++ b/docs/petr4spec/Makefile
@@ -1,15 +1,9 @@
 
 SPEC=Petr4-spec
 
-all: build/${SPEC}.pdf
-
-build/${SPEC}.pdf: ${SPEC}.mdk
-	madoko --pdf -vv --png --odir=build $<
-
-build/${SPEC}.pdf: grammar.mdk p4.json
 
 html: ${SPEC}.mdk grammar.mdk p4.json
-	madoko -vv --png --odir=build $<
+	madoko -vv  --odir=build $<
 	
 clean:
 	${RM} -rf build
diff --git a/docs/petr4spec/Petr4-spec.mdk b/docs/petr4spec/Petr4-spec.mdk
index ded629735..16b02ded2 100644
--- a/docs/petr4spec/Petr4-spec.mdk
+++ b/docs/petr4spec/Petr4-spec.mdk
@@ -1,24 +1,31 @@
-Title : Petr4 Type System Formalization
-Title Footer: &date;
-Author: Parisa Ataei, Ryan Doenges, Nate Foster
-Affiliation: Cornell University
-Heading depth: 5
-Math Dpi    : 299
-Pdf Latex: xelatex
-Math Latex Full: pdflatex
-Document Class: [11pt]article
-Package: [top=1in, bottom=1.25in, left=1in, right=1in]geometry
-Package: fancyhdr
-Package: mathpartir
-MathJax Ext: AMScd
-Package: amscd
-MathJax Ext : mhchem
-Package     : [version=3]mhchem
+Title         : P4 Type System Formalization
+Title Footer  : &date;
+Author        : Petr4 Team
+Affiliation   : Cornell University
+Heading depth : 5
+Cite Style    : numeric
+BibTex        : False
+Bib           : reference
+
+Math Mode       : static
+Pdf Latex       : xelatex
+Math Latex Full : pdflatex
+
+Document Class : [11pt]article
+
+Package : mathtools
+Package : fancyhdr
+Package : mathpartir
+
 
 Tex Header:
   \setlength{\headheight}{30pt}
   \renewcommand{\footrulewidth}{0.5pt}
 
+.code: background-color=Gainsboro
+.code2: background-color=LightCoral
+.code3: background-color=Fuchsia
+
 @if html {
 body.madoko {
   font-family: utopia-std, serif;
@@ -130,7 +137,7 @@ p4grammar {
 @if tex {
 p4grammar {
   replace: "~ Begin P4GrammarBlock&nl;\
-                 ````&nl;&source;&nl;````&nl;\
+                 &source;&nl;\
                  ~ End P4GrammarBlock";
   breakable: true;
   margin-top: 6pt;
@@ -142,509 +149,3027 @@ p4grammar {
 }
 }
 
+@if html {
+p4syntax {
+  replace: "~ Begin P4SyntaxBlock&nl;\
+                 &source;&nl;\
+                 ~ End P4SyntaxBlock";
+  border: solid;
+  margin-top: 6pt;
+  margin-bottom: 6pt;
+  padding: 6pt;
+  background-color: #e6ffff;
+  border-width: 0.5pt;
+}
+}
+
+@if tex {
+p4syntax {
+  replace: "~ Begin P4SyntaxBlock&nl;\
+                 ````&nl;&source;&nl;````&nl;\
+                 ~ End P4SyntaxBlock";
+  breakable: true;
+  margin-top: 6pt;
+  margin-bottom: 6pt;
+  padding: 6pt;
+  background-color: #e6ffff;
+  border: solid;
+  border-width: 0.5pt;
+}
+}
+
+@if html {
+infrule {
+  replace: "~ Begin InfRuleBlock&nl;\
+              ~~ Center {padding:1ex}&nl;\
+              ~~~ Snippet&nl;\
+              \begin{mathpar}&nl;\
+              \small&nl;\
+              &source;&nl;\
+              \end{mathpar}&nl;\
+              ~~~&nl;\
+              ~~&nl;\
+              ~ End InfRuleBlock";
+  border: solid;
+  margin-top: 6pt;
+  margin-bottom: 6pt;
+  padding: 6pt;
+  background-color: #fffaf0;
+  border-width: 0.5pt;
+}
+}
+
+@if tex {
+infrule {
+  replace: "~ Begin InfRuleBlock&nl;\
+              ~~ Center {padding:1ex}&nl;\
+              ~~~ Snippet&nl;\
+              \begin{mathpar}&nl;\
+              \small&nl;\
+              &source;&nl;\
+              \end{mathpar}&nl;\
+              ~~~&nl;\
+              ~~&nl;\
+              ~ End InfRuleBlock";
+  breakable: true;
+  margin-top: 6pt;
+  margin-bottom: 6pt;
+  padding: 6pt;
+  background-color: #fffaf0;
+  border: solid;
+  border-width: 0.5pt;
+}
+}
+
+@if html {
+infrulehelper {
+  replace: "~ Begin InfRuleHelperBlock&nl;\
+              ~~ Center {padding:1ex}&nl;\
+              ~~~ Snippet&nl;\
+              \begin{mathpar}&nl;\
+              \small&nl;\
+              &source;&nl;\
+              \end{mathpar}&nl;\
+              ~~~&nl;\
+              ~~&nl;\
+              ~ End InfRuleHelperBlock";
+  border: solid;
+  margin-top: 6pt;
+  margin-bottom: 6pt;
+  padding: 6pt;
+  background-color: #ECE1FB;
+  border-width: 0.5pt;
+}
+}
+
+@if tex {
+infrulehelper {
+  replace: "~ Begin InfRuleHelperBlock&nl;\
+              ~~ Center {padding:1ex}&nl;\
+              ~~~ Snippet&nl;\
+              \begin{mathpar}&nl;\
+              \small&nl;\
+              &source;&nl;\
+              \end{mathpar}&nl;\
+              ~~~&nl;\
+              ~~&nl;\
+              ~ End InfRuleHelperBlock";
+  breakable: true;
+  margin-top: 6pt;
+  margin-bottom: 6pt;
+  padding: 6pt;
+  background-color: #ECE1FB;
+  border: solid;
+  border-width: 0.5pt;
+}
+}
+
+
 ~Aligned : replace:"~Math&nl;\begin{aligned}&nl;&source;&nl;\end{aligned}&nl;~" 
 
 
 [TITLE]
 
-~ TexRaw
-\mdDefineUnicode{10214}{\ensuremath{\llbracket}}
-\mdDefineUnicode{10215}{\ensuremath{\rrbracket}}
-~
 
 ~ Begin Abstract
-P4 is a language for programming the data plane of network
-devices. Petr4 provides a clean-slate definitional interpreter
-and a core calculus that models a fragment of P4. This document
-provides a definition of Petr4's type system that is consistent
-with its implementation. The target audience of this document
-includes developers and debuggers who work on P4 implementations
-such as Petr4 and P4C. In essence, this document may be of
-interest to programmers who are interested in understanding
-the implementation of Petr4 deeply.
+P4's type system is currently distributed between its language specification and its reference implementation p4c. Unfortunately, this state of affairs results in ambiguity while reasoning through the behavior of a P4 program, evident from the many issues opened on P4's GitHub repository. 
+In this document, we provide a formalization of P4's type system to unify the expected behavior of P4 programs. 
+The target audience of this document includes language designers and compiler experts
+that work (or starting to work) on P4 as well as developers and debuggers that work
+with P4 and require a deep understanding of it.
 ~ End Abstract
 
 ~ MathDefs
 [INCLUDE="ops.tex"]
 ~
 
+
 [TOC]
 
-# Overview { #sec-overview }
+# Introduction { #sec-intro }
 
-This document defines the type system of Petr4. The type system
-conducts three tasks simultaneously:
+P4's type system is currently distributed between its [language specification][p4spec] and its [reference implementation][p4cgit](p4c).
+P4 spec explains the type of (sub)programs in plain English
+while p4c implements a type system for P4.
+There are multiple problems with both:
 
-1. It type checks P4 programs.
-2. It conducts type inference.
-3. It does a pass from the surface syntax to the first IR. 
+[p4spec]: https://p4.org/p4-spec/docs/P4-16-v1.2.0.html
+[p4cgit]: https://p4.org/p4-spec/docs/P4-16-v1.2.0.html
 
+1. Figuring out how a program behaves and whether it type checks or not is extremely hard. In P4 spec, one has to jump from place to place to find whether each part of the program type checks or not since information regarding type checking a program is staggered all over the place and even worse in some cases it is missing. In p4c, one has to either write a sample program and compile it to see if it type checks or they have to go through all P4C's code to figure out the behavior of their program. For example, ``todo: add GitHub issues. add number of loc of P4C.``
+2. Adding a new feature to P4 requires extending its type system and often times results in revising parts of the current type system as well. Doing so for both P4 spec and p4c is rather burdensome and error-prone due to the distribution of explanation in P4 spec and implementation in p4c. 
+3. Even more concerning, despite lots of effort by the P4 language committee, there are discrepancies between P4 spec and P4C's implementation. For example, ``TODO: add GitHub issues``
 
-## Connecting To The Implementation { #sec-conn }
+In this document, we formalize P4's type system. Formalizing P4 benefits the community in different ways
 
-The following locates each data type in the implementation
-(<https://github.com/verified-network-toolchain/petr4>):
+1. It makes working with and on P4 easier for both people who are just picking it up and those who have been working with/on it for some time. This is because clear formalization makes understanding a language and the behavior of programs written in it less cumbersome. 
+2. It provides a place for experts and users to refer to check the behavior of a program. It also provides a unified place for ensuring all references and implementations of P4 are consistent with each other.
+3. It provides the bases for formally verifying P4's compilers and interpretors.
 
-- The surface AST is _types.program_
-- The type of programs of the surface syntax is _types.type.t_
-- The first IR is _prog.program_
-- The type of the first IR is _prog.type.t_
 
-For simplicity, we have removed the information that is needed to report when an error
-happens. Such information is passed around in the surface syntax as a field (called
-`tags`) of record for all data types.
+# Overview { #sec-overview }
 
-## Architecture { #sec-arch }
+A P4 program is mainly a list of declarations and a declaration could be declaring a
+parser or control plane, instantiating an object, calling a (extern) function or method,
+and defining a type or an object. Each declaration may contain multiple statements and
+expressions within it.
+Thus, in order to formalize P4's type system we need to:
+
+- have consistent and clear [notation][#sec-notation]
+- formalize [P4's syntax][#sec-syntax]
+- formalize type related rules, including [type well-formedness][#sec-type-well-formed], [type equality][#sec-type-eq], [type unification][#sec-type-unify]
+- formalize [expressions typing][#sec-exp-typing]
+- formalize [statements typing][#sec-stmt-typing]
+- formalize [declarations typing][#sec-decl-typing]
+
+Furthermore, for readers who are less familiar with programming languages fundamentals we provide a [summary of programming languages terminology][#sec-terminology] and a [developer's guide to reading inference rules][#sec-guide].
+
+Additionally, for developers and experts starting to work on Petr4 we provide a summary of its architecture and connect P4's formalization to Petr4's implementation in Appendix[#sec-petr4].
+
+# Notation { #sec-notation }
+
+In this section, we introduce the notation and naming convention that we use throughout this document. 
+
+## Naming Convention
+Each typing judgment may use auxiliary judgment and helper functions. The auxiliary
+judgments are included in this document while the helper functions are just explained
+in plain English.
+
+Conventionally, in this document we accompany rule names with four possible suffixes:
+
+- $\ruleNameT$ indicates that the rule is describing a rule for a type
+- $\ruleNameE$ and $\ruleNameAE$ indicate that the rules are for an expression and an auxiliary judgment for an expression
+- $\ruleNameS$ indicates that the rule is describing a rule for a statement
+- $\ruleNameD$ indicates that the rule is describing a rule for a declaration
+
+## rest
+
+``TODO: add followings.``
+
+- $\overline {\overline \anyTyp}$
+- $\overline {X:\typ}$ zips $\overline X$ and $\typs$.
+- $\concatList a b$
+
+Metavariables are place holders for values of a type. For example, $\bool$ stands for expressions $true$ or $false$. Keep in mind that $true$ and $false$ both are expressions that have the type $\boolTyp$. As another example, in most programming references $foo$, $bar$, and $baz$ are used as metavariables, often for functions. 
+
+- $\overline x$ denotes a list of $x$.
+- For simplicity, we omit mapping a function/judgment on a list of elements. Instead, we just apply the function/judgment to a list. So every time you see a function applied to a list, read it as mapping the function over all the elements of the list. 
+- An underscore (that is, $\_$) is used when we do not need to use some specific information returned by some helper in judgments. 
+- The notation $\maybe \anyTyp$ denotes an optional type, that is, the type of $\anyTyp$ has been extended with bottom (maybe type in Haskell, or option type in OCaml). So if $\anyTyp$ denotes an integer, $\maybe \anyTyp$ could either be an integer number or bottom. 
+
+The following describes the metavariables used in this document:
+
+~ Center
+| **metavariable**   |   **type represented** |
+|:----------------:|:------------------|
+| $\bool$ | booleans |
+| $\str$ | strings |
+| $\int$ | arbitrary length integer |
+| $\width$ | width of a data structure |
+| $\size$ | size of a data structure |
+| $\bitWidth \bit \width$ | fixed length integer |
+| $\intWidth \int \width$ | signed integer |
+| $\name$ | strings representing any kinds of names |
+| $\typ$ | types |
+| $\dir$ | directions |
+| $\typVar$ | type variables |
+| $\wildcardParam$ | wild card type parameters |
+| $\field$ | field names |
+| $\env$ | environments |
+| $\emp$ | empty list of elements |
+| $\anyTyp$ | a value of any type |
+| $\constraint$, $\optConstraint$, $\nonoptConstraint$ | constraints |
+~
 
-Figure [#fig-arch] depicts part of Petr4's architecture that contains the type system.
-After lexing and parsing a P4 program we get a program in our surface syntax. This
-program is then passed through the _elaborator_ where type variables are introduced
-instead of underscore and new type variable names are generated for variables with the
-same name but in different scopes. This document does not discuss the innerworkings of
-`elaborate`. Then, the program is passed through the type system (encoded in `checker`).
-This document discusses the innerworking of the type system extensively. Finally, the
-program is evaluated.
 
-~ Figure { #fig-arch; caption: "Part of Petr4's achitecture." }
-![arch]
-~
-[arch]: figs/petr4/arch.png { width: 100%; page-align: forcehere }
+## Signatures
+``TODO``
+function signature. judgment signature. environment signature. 
+
+## contexts and environments
+
+# Syntax { #sec-syntax }
+
+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.
+- Direction is optional in parameter declaration. However, for simpilicity, we just use $\less$ to denote a missing direction. 
+
+~ Begin P4Syntax
+**Data types used in P4 programs:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\baseTyp$ | $::=$ | $\boolTyp$ | $\qquad \text{booleans}$ |
+|   | $\vert$ | $\errTyp$ | $\qquad \text{errors}$ |
+|   | $\vert$ | $\integerTyp$ | $\qquad \text{infinite-precision integers}$ |
+|   | $\vert$ | $\intWidthTyp \exp$ | $\qquad \text{fixed-width signed integers}$ |
+|   | $\vert$ | $\bitWidthTyp \exp$ | $\qquad \text{fixed-width unsigned integers}$ |
+|   | $\vert$ | $\varBitTyp \exp$ | $\qquad \text{variable-width integers with a maximum width}$ |
+|   | $\vert$ | $\typVar$ | $\qquad \text{type variables}$ |
+|   | $\vert$ | $\spcTyp \baseTyp \baseTyps$ | $\qquad \text{specialized type}$ |
+|   | $\vert$ | $\stackTyp \baseTyp \exp$ | $\qquad \text{stacks}$ |
+|   | $\vert$ | $\tupleTyps \baseTyps$ | $\qquad \text{tuples}$ |
+|   | $\vert$ | $\stringTyp$ | $\qquad \text{strings}$ |
+|   | $\vert$ | $\voidTyp$ | $\qquad \text{void}$ |
+|   | $\vert$ | $\dontcareTyp$ | $\qquad \text{don't care}$ |
+{ .booktable }
+
+**Directions:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\dir$ | $::=$ | $\inDir$ | $\qquad \text{copy-in}$ |
+|   | $\vert$ | $\out$ | $\qquad \text{copy-out}$ |
+|   | $\vert$ | $\inout$ | $\qquad \text{copy-in-out}$ |
+|   | $\vert$ | $\less$ | $\qquad \text{direction-less}$ |
+{ .booktable }
+
+**Parameters:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\prmDef \typKind$ | $::=$ | $\dir \, \typKind \, \var$ | $\qquad \text{parameters}$ |
+|   | $\vert$ | $\dir \, \typKind \, \var = \exp$ | $\qquad \text{parameters with value}$ |
+{ .booktable }
+
+
+**Unary operations:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\unaryOp$ | $::=$ | $\intoOp !$ | $\qquad \text{logical negation}$ |
+|   | $\vert$ | $\bitComplement$ | $\qquad \text{bitwise complement}$ |
+|   | $\vert$ | $\intoOp -$ | $\qquad \text{unary minus}$ |
+{ .booktable }
+
+**Binary operations:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\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$ | $\intoOp \concat$ | $\qquad \text{bitwise concatenation}$ |
+|   | $\vert$ | $\shiftL$ | $\qquad \text{shift left}$ |
+|   | $\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:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\arg$ | $::=$ | $\argexp$ | $\qquad \text{expression}$ |
+|   | $\vert$ | $\argkv$ | $\qquad \text{key value}$ |
+|   | $\vert$ | $\missingarg$ | $\qquad \text{missing}$ |
+{ .booktable }
+
+**Expressions:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\exp$ | $::=$ | $\bool$ | $\qquad \text{booleans}$ |
+|   | $\vert$ | $\str$ | $\qquad \text{strings}$ |
+|   | $\vert$ | $\int$ | $\qquad \text{integers}$ |
+|   | $\vert$ | $\intWidth \int \width$ | $\qquad \text{fixed-width signed integers}$ |
+|   | $\vert$ | $\bitWidth \bit \width$ | $\qquad \text{fixed-width unsigned integers}$ |
+|   | $\vert$ | $\name$ | $\qquad \text{names (variables)}$ |
+|   | $\vert$ | $\arrayAccess {\exp_1} {\exp_2}$ | $\qquad \text{array accesses}$ |
+|   | $\vert$ | $\bitStringAccess {\exp_1} {\exp_2} {\exp_3}$ | $\qquad \text{bitstring slices}$ |
+|   | $\vert$ | $\list \exps$ | $\qquad \text{lists}$ |
+|   | $\vert$ | $\records \exp$ | $\qquad \text{records}$ |
+|   | $\vert$ | $\unaryOp \exp$ | $\qquad \text{unary operations}$ |
+|   | $\vert$ | $\exp_1 \binOp \exp_2$ | $\qquad \text{binary operations}$ |
+|   | $\vert$ | $\cast \baseTyp \exp$ | $\qquad \text{casts}$ |
+|   | $\vert$ | $\typMem \typVar \field$ | $\qquad \text{type members}$ |
+|   | $\vert$ | $\errMem \field$ | $\qquad \text{error members}$ |
+|   | $\vert$ | $\expMem \exp \field$ | $\qquad \text{expression members}$ |
+|   | $\vert$ | $\ternary {\exp_1} {\exp_2} {\exp_3}$ | $\qquad \text{conditionals}$ |
+|   | $\vert$ | $\funcCall \exp {\baseTyps} \args$ | $\qquad \text{function calls}$ |
+|   | $\vert$ | $\instantiation {\baseTyp} {\args}$ | $\qquad \text{anonymous instantiation}$ |
+|   | $\vert$ | $\mask {\exp_1} {\exp_2}$ | $\qquad \text{bit masks}$ |
+|   | $\vert$ | $\range {\exp_1} {\exp_2}$ | $\qquad \text{ranges}$ |
+{ .booktable }
+
+**Labels:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\lbl$ | $::=$ | $\defLbl$ | $\qquad \text{default}$ |
+|   | $\vert$ | $\str$ | $\qquad \text{string labels}$ |
+{ .booktable }
+
+**Switchs:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\switchCase$ | $::=$ | $\actionCase \stmts$ | $\qquad \text{labeled block}$ |
+|   | $\vert$ | $\lbl$ | $\qquad \text{fall through with label}$ |
+{ .booktable }
+
+**Statements:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\stmt$ | $::=$ | $\methodCall \exp \baseTyps \args$ | $\qquad \text{method call}$ |
+|   | $\vert$ | $\assign {\exp_1} {\exp_2}$ | $\qquad \text{assignment}$ |
+|   | $\vert$ | $\dirApp \baseTyp \args$ | $\qquad \text{direct application}$ |
+|   | $\vert$ | $\ifthen \exp \stmt$ | $\qquad \text{if then}$ |
+|   | $\vert$ | $\ifthenelse \exp {\stmt_1} {\stmt_2}$ | $\qquad \text{if then else}$ |
+|   | $\vert$ | $\block \stmts$ | $\qquad \text{sequencing}$ |
+|   | $\vert$ | $\exit$ | $\qquad \text{exit}$ |
+|   | $\vert$ | $\noop$ | $\qquad \text{noop}$ |
+|   | $\vert$ | $\return \exp$ | $\qquad \text{return}$ |
+|   | $\vert$ | $\retNothing$ | $\qquad \text{return nothing}$ |
+|   | $\vert$ | $\switch \exp \switchCases$ | $\qquad \text{switch}$ |
+|   | $\vert$ | $\dcl$ | $\qquad \text{declaration}$ |
+{ .booktable }
+
+**Parser states:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\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}$ |
+| $\case$ | $::=$ | $\expandCase \pmatches \nxt$ | $\qquad \text{match cases for the next state}$ |
+| $\parserTran$ | $::=$ | $\nxt$ | $\qquad \text{next state transition}$ |
+|   | $\vert$ | $\slctTran \exp \pcases$ | $\qquad \text{select next state transition}$ |
+| $\state$ | $::=$ | $\stateDef \var \stmts \parserTran$ | $\qquad \text{states}$ |
+{ .booktable }
+
+**Table properties:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\action$ | $::=$ | $\actionDef \var \arg$ | $\qquad \text{actions}$ |
+| $\prop$ | $::=$ | $\key \exp \var$ | $\qquad \text{keys}$ |
+|   | $\vert$ | $\action$ | $\qquad \text{actions}$ |
+|   | $\vert$ | $\entry \pmatch \action$ | $\qquad \text{entries}$ |
+|   | $\vert$ | $\custom \bool \var \exp$ | $\qquad \text{custom property}$ |
+{ .booktable }
+
+**Methods:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\extMethod$ | $::=$ | $\constructor \var {\prmDef \baseTyp}$ | $\qquad \text{constructors}$ |
+|   | $\vert$ | $\abstractMethod \baseTyp \var \typVar {\prmDef \baseTyp}$ | $\qquad \text{abstract methods}$ |
+|   | $\vert$ | $\methodDef \baseTyp \var \typVar {\prmDef \baseTyp}$ | $\qquad \text{methods}$ |
+{ .booktable }
+
+**Declarations:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\dcl$ | $::=$ | $\constDcl \baseTyp \var \exp$ | $\qquad \text{constants}$ |
+|   | $\vert$ | $\inst \baseTyp \args \var \stmts$ | $\qquad \text{instantiations (initialized)}$ |
+|   | $\vert$ | $\instNoBlock \baseTyp \args \var$ | $\qquad \text{instantiations (uninitialized)}$ |
+|   | $\vert$ | $\parserDcl \var \typVars {\overline { {\prmDef \baseTyp}}} {\overline {\VVal {\prmDef \baseTyp}}} \dcls \states$ | $\qquad \text{parsers}$ |
+|   | $\vert$ | $\controlDcl \var \typVars {\overline { {\prmDef \baseTyp}}} {\overline {\VVal {\prmDef \baseTyp}}} \dcls \stmts$ | $\qquad \text{controls}$ |
+|   | $\vert$ | $\funcDcl \baseTyp \var \typVars {\prmDefs \baseTyp} \stmts$ | $\qquad \text{functions}$ |
+|   | $\vert$ | $\externFuncDcl \baseTyp \var \typVars {\prmDefs \baseTyp}$ | $\qquad \text{extern functions}$ |
+|   | $\vert$ | $\varDclInit \baseTyp \var \exp$ | $\qquad \text{local variables (initialized)}$ |
+|   | $\vert$ | $\varDcl \baseTyp \var$ | $\qquad \text{local variables (uninitialized)}$ |
+|   | $\vert$ | $\valSetDcl \baseTyp \exp \var$ | $\qquad \text{parser value sets}$ |
+|   | $\vert$ | $\actionDcl \var {\prmDefs \baseTyp} \stmts$ | $\qquad \text{actions}$ |
+|   | $\vert$ | $\tableDcl \var \props$ | $\qquad \text{tables}$ |
+|   | $\vert$ | $\headerDcl \typVar \fieldTyps$ | $\qquad \text{header types}$ |
+|   | $\vert$ | $\headerUnionDcl \typVar \fieldTyps$ | $\qquad \text{header union types}$ |
+|   | $\vert$ | $\structDcl \typVar \fieldTyps$ | $\qquad \text{struct types}$ |
+|   | $\vert$ | $\errDcl \fields$ | $\qquad \text{error types}$ |
+|   | $\vert$ | $\matchkindDcl \fields$ | $\qquad \text{match kind types}$ |
+|   | $\vert$ | $\enumDcl \typVar \fields$ | $\qquad \text{enumerated types}$ |
+|   | $\vert$ | $\serEnumDcl \baseTyp \typVar \field \exp$ | $\qquad \text{serializable enumerated types}$ |
+|   | $\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  \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}$ |
+{ .booktable }
+
+**Programs:**
+
+|     |      |     |     |
+|~~~~:|:~~~~:|:~~~~|:~~~~|
+| $\prog$ | $::=$ | $\dcls$ | $\qquad \text{programs}$ |
+{ .booktable }
+
+~ End P4Syntax
+
+
+# Type Related Judgments { #sec-types-typing }
+
+Three judgments are provided for types of P4 expressions:
+
+[alpha-equiv-wiki]: https://en.wikipedia.org/wiki/Lambda_calculus#Alpha_equivalence
+
+- [type well-formedness][#sec-type-well-formed]: ensures the lack of specific errors in types, that is, types are well-formed.
+- [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. 
+
+All typing rules first saturate all types,
+that is, it eliminates all type references in type
+$\typ$ and replaces them with the type they refer to. Thus, the result of saturation
+contains no type synonym (_TypeName_ in Petr4) constructors that are used to give a name to a new type. Then it checks the well-formedness of the saturated type.
+For brevity, we don't include the saturation in rules.
+
+### Base Types { #sec-base-t }
+
+The following base types are well-formed unconditionally since there is not any room for an error while constructing a value of these types. For example, the $\boolTyp$ only has two constructors $\mathit{true}$ and $\mathit{false}$ which do not take any argument so there is no room to construct a value incorrectly.
+
+~ Begin InfRule
+
+  \inferrule
+     { }
+     { \typWellFormed \boolTyp }
+     \quad (\boolT)
 
-# Type System
+\and
 
-some general explanation of the type system and the judgments.
+  \inferrule
+     { }
+     { \typWellFormed \stringTyp }
+     \quad (\stringT)
 
-## Expression's Typing Rules
-translate typ translate a surface type to the IR's type. we don't present these types
-since their difference isn't much.
-saturate typ saturates a type. Eliminate all type references in typ and replace them with the type they refer to. The result of saturation will contain no TypeName constructors anywhere. It may contain TypeName constructors.
-e(name) looks up name in the environment and returns its type and direction.
-is array determines whether a type is an array type.
-is numberic determines whether a type is numeric.
-compile time evaluation evaluates the expression expr at compile time.
-explicit cast ok checks whether typ1 can be converted to typ2 under e based on P4's specification of 8.9.1. Explicit casts. 
+\and
 
-~ Center  {padding:1ex} 
-~~ Snippet
-\begin{mathpar}
-  \small
+  \inferrule
+     { }
+     { \typWellFormed \integerTyp }
+     \quad (\intT)
 
-  \inferrule[Bool]
-     {}
-     {\expenv \bool \bool \boolTyp \less}
+\and
 
-  \inferrule[String]
-     {}
-     {\expenv \str \str \stringTyp \less}
+  \inferrule
+     { }
+     { \typWellFormed {\varBitTyp \width} }
+     \quad (\varbitT)
 
-  \inferrule[Integer]
-     {}
-     {\expenv \int \int \integerTyp \less}
+\and
 
-  \inferrule[Bit]
-     {}
-     {\expenv {\bitWidth \bit \width} {\bitWidth \bit \width} {\bitWidthTyp \width} \less}
+  \inferrule
+     { }
+     { \typWellFormed \errTyp}
+     \quad (\errT)
 
-  \inferrule[Int]
-     {  }
-     {\expenv {\intWidth \int \width} {\intWidth \int \width} {\intWidthTyp \width} {\less}}
+\and
 
-  \inferrule[Name]
-     {\lookupEnv \name = (\typ, \dir)}
-     {\expenv \name \name \typ \dir}
+  \inferrule
+     { }
+     { \typWellFormed \voidTyp}
+     \quad (\voidT)
 
-  \inferrule[ArrayAccess]
-     {\expenv {\array} {\prim \array} {\arrayTyp \typ \size} \dir \\
-      \expenv \index {\prim \index} {\prim \typ} {\prim \dir} \\
-      \isArray {\arrayTyp \typ \size} \\
-      \isNumeric {\prim \typ}}
-     {\expenv {\arrayAccess \array \index} {\arrayAccess {\prim \array} {\prim \index}} \typ \dir }
-
-  \inferrule[BitStringAccess]
-     {\expenvWithCtxt \cte \high {\prim \high} {\typ_\high} {\dir_\high} \\
-      \isNumeric {\typ_\high} \\
-      \pprim \high = \compileTimeEval {\prim \high} \\
-      \expenvWithCtxt \cte \low {\prim \low} {\typ_\low} {\dir_\low} \\
-      \isNumeric {\typ_\low} \\
-      \pprim \low = \compileTimeEval {\prim \low} \\
-      0 \leq \pprim \low < \width \\
-      \pprim l \leq \pprim h < \width \\
-      \expenv \bitString {\prim \bitString} \typ \dir \\
-      \typ = \intWidthTyp \width \textOr \bitWidthTyp \width}
-     {\expenv {\bitStringAccess \bitString \low \high} {\bitStringAccess \bitString {\pprim \low} {\pprim \high}} {\bitStringTyp {\pprim \low} {\pprim \high}} \dir }
-
-  \inferrule[List]
-     {1 \leq i \leq n; \expenv {\exp_i} {\prim {\exp_i}} {\typ_i} {\dir_i}}
-     {\expenv {[\exp_1, \ldots, \exp_n]} {[\exp_1, \ldots, \exp_n]} {[\typ_1, \ldots, \typ_n]} \less }
-
-  \inferrule[Record]
-     {1 \leq i \leq n; \expenv {\exp_i} {\prim {\exp_i}} {\typ_i} {\dir_i}  }
-     {\expenv {\{\field_1 = \exp_1, \ldots, \field_n = \exp_n \}} {\{\field_1 = \prim {\exp_1}, \ldots, \field_n = \prim {\exp_n} \}} {\{\field_1 : \typ_1, \ldots, \field_n : \typ_n \}} \less  }
-
-  \inferrule[LogicalNegation]
-     { \expenv \exp {\prim \exp} \boolTyp \dir }
-     { \expenv {!\exp} {!\prim \exp} \boolTyp \dir }
+\and
 
-  \inferrule[BitwiseComplement]
-     { \expenv \exp {\prim \exp} {\bitWidthTyp \width} \dir }
-     { \expenv {\bitComplement\!\exp} {\bitComplement\!\prim \exp} {\bitWidthTyp \width} \dir }
+  \inferrule
+     { }
+     { \typWellFormed \matchKindTyp}
+     \quad (\matchKindT)
 
-  \inferrule[UnaryMinusCTK]
-     { \expenv \exp {\prim \exp} \intTyp \dir }
-     { \expenv {-\exp} {-\prim \exp} \intTyp \dir }
+\and
 
-  \inferrule[UnaryMinus]
-     { \expenv \exp {\prim \exp} {\intWidthTyp \width} \dir }
-     { \expenv {-\exp} {-\prim \exp} {\intWidthTyp \width} \dir }
+  \inferrule
+     { 1 < \width} % p4 spec has this
+     %% { }
+     { \typWellFormed {\intWidthTyp \width} }
+     \quad (\intWidthT)
 
-  \inferrule[BinaryOps]
-     {\coerceBinArgsEnv {\exp_1 \oplus \exp_2} {\prim {\exp_1}} {\prim {\exp_2}} \\
-      \binOpEnv {\prim {\exp_1} \oplus \prim {\exp_2}} {\pprim {\exp_1} \oplus \pprim {\exp_2}} \typ \dir }
-     { \expenv {\exp_1 \oplus \exp_2} {\prim {\exp_1} \oplus \prim {\exp_2}} \typ \dir }
+\and
 
-\end{mathpar}
-~~
-~
+  \inferrule
+     { 0 \leq \width} % p4 spec has this
+     %% { }
+     { \typWellFormed {\bitWidthTyp \width} }
+     \quad (\bitWidthT)
 
-~ Center  {padding:1ex} 
-~~ Snippet
-\begin{mathpar}
-  \small
+~ End InfRule
 
-  \inferrule[Cast]
-     { \expenv \exp {\exp_1} {\typ_1} \dir \\
-       \typ_2 = \sat {\typ_1} \\
-       \typ_3 = \trans {\typ_2} {\emp} \\
-       \typ_4 = \sat {\typ_3} \\
-       \typWellFormed {\typ_3} \\
-       \explicitCastOK {\typ_1} {\typ_3}}
-     { \expenv {\cast \typ \exp} {\cast {\typ_1} {\exp_1}} {\typ_3} \less  }
-
-  \inferrule[TypeMember]
-     {\lookupEnv {\typMem \typ \name} = (\typ, \dir)  }
-     {\expenv {\typMem \typ \name} {\typMem \typ \name} \typ \less  }
+### Array Type { #sec-array-t }
 
-  \inferrule[ErrorMember]
-     {\lookupEnv {\errMem \name} = (\errTyp, \dir)  }
-     {\expenv {\errMem \name} {\errMem \name} \errTyp \less  }
+An array type has a specific type and size.
+The rule $\arrayT$ states that under environment $\env$, an array is well-formed if its
+type is well-formed and it follows the nesting rules of P4.
 
-  \inferrule[ExpressionMember]
-     { blah }
-     { blah}
+- $\isValidNestedTyp \typ$ checks whether the nested type $\typ$ is valid, that is,
+it checks if all the subtypes in the type $\typ$ can actually be inner types of $\typ$ based on [P4's description of type nesting rules][sec7-2-7].
 
-  \inferrule[Ternary]
-     {\expenv {\exp_1} {\prim {\exp_1}} \boolTyp {\dir_1} \\
-      \expenv {\exp_2} {\prim {\exp_2}} {\typ_1} {\dir_2} \\
-      \expenv {\exp_3} {\prim {\exp_3}} {\typ_2} {\dir_3}\\
-      \typ_1 = \typ_2 \\
-      \typ_1 \neq \integerTyp}
-     {\expenv {\ternary {\exp_1} {\exp_2} {\exp_3}} {\ternary {\prim {\exp_1}} {\prim {\exp_2}} {\prim {\exp_3}}} {\typ_1} \less }
+[sec7-2-7]: https://p4.org/p4-spec/docs/P4-16-v1.2.0.html#sec-type-nesting 
 
-  \inferrule[FunctionCall]
-     { blah }
-     { blah }
-     % { \expenv {\exp (\typ_1 \arg_1, \ldots, \typ_n \arg_n)}  }
+~ Begin InfRule
 
-% function type: <return type> <function name>(x1,...,xn) {...}
+  \inferrule
+     { \typWellFormed \typ \\
+       \isValidNestedTyp {\arrayTyp \typ \size}}
+     { \typWellFormed {\arrayTyp \typ \size} }
+     \quad (\arrayT)
 
-  \inferrule[NamelessIinstantiation]
-     { blah }
-     { blah }
+~ End InfRule
 
-  \inferrule[Mask]
-     {\expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
-      \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\
-      \left( \so {\typ_1 = \typ_2 = \bitWidthTyp \width} {\typ = \bitWidthTyp \width}\right) \\
-      \textOr
-      \left( \so {\typ_1 = \typ_2 = \integerTyp} {\typ = \integerTyp}\right) \\
-      \textOr
-      \left( \so {\typ_1 = \bitWidthTyp \width, \typ_2 = \integerTyp} {\typ = \bitWidthTyp \width}\right) \\
-      \textOr
-      \left( \so {\typ_1 = \integerTyp, \typ_2 = \bitWidthTyp \width} {\typ = \bitWidthTyp \width}\right)
-      }
-     {\expenv {\mask {\exp_1} {\exp_2}} {\mask {\prim \exp_1} {\prim \exp_2}} {\setTyp \typ} \less  }
+### Tuple/List Type { #sec-tuple-t }
 
-  \inferrule[Range]
-     { \expenv \low {\prim \low} \typ {\dir_\low} \\
-       \expenv \high {\prim \high} \typ {\dir_\high} \\
-       \typ_\low = \typ_\high = \bitWidthTyp \width \textOr \intWidthTyp \width \textOr \integerTyp}
-     { \expenv {\range \low \high} {\range {\prim \low} {\prim \high}} {\setTyp \typ} \dir }
+Each element of a tuple/list can have a distinct type so a tuple type is simply a list of types. Note that lists also have a tuple type. The rule $\tupleT$ states that under
+environment $\env$, a tuple type is well-formed if all its types are well-formed and it
+follows the nesting typing rules of P4. 
 
+~ Begin InfRule
 
-\end{mathpar}
-~~
-~
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     { \typWellFormed \typs \\
+        \isValidNestedTyp {\tupleTyps \typs}}
+     { \typWellFormed {\tupleTyps \typs} }
+     \quad (\tupleT)}
 
-### Coerce Binary Operation Arguments Auxiliary Judgment
-Let implicitCast typ1 typ2 be defined as follows to describe P4's implicit
-casting behavior on operands in binary expressions:
-        
-cast typ exp produces a cast expression if the type of exp is different from the
-type typ.
+  % \inferrule[List]
+  %    { 1 \leq i \leq n. \typWellFormed {\typ_i} \\
+  %      1 \leq i \leq n.  \isValidNestedTyp {\listTyp {\typ_1} {\typ_n}} {\typ_i}}
+  %    { \typWellFormed {\listTyp {\typ_1} {\typ_n}} }
 
-The restJ rule stands for all other binary operations. 
+~ End InfRule
 
-~ Center  {padding:1ex} 
-~~ Snippet
-\begin{mathpar}
-  \small
+### Set Type { #sec-set-t }
 
-  \inferrule[ShiftRight]
-     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
-       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}}
-     { \coerceBinArgsEnv {\exp_1 \shiftR \exp_2} {\prim {\exp_1}, {\typ_1}, {\dir_1}} {\prim {\exp_2}, {\typ_2}, {\dir_2}}  }
+In P4, unlike tuples, elements of a set must all have the same type and the set type is well-formed if the type of its elements is well-formed, which is stated by the $\setT$ rule.
 
-  \inferrule[ShiftLeft]
-     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
-       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}}
-     { \coerceBinArgsEnv {\exp_1 \shiftL \exp_2} {\prim {\exp_1}} {\prim {\exp_2}} {\prim {\exp_1}, {\typ_1}, {\dir_1}} {\prim {\exp_2}, {\typ_2}, {\dir_2}} }
+~ Begin InfRule
 
-  \inferrule[BitConcatenation]
-     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
-       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}}
-     { \coerceBinArgsEnv {\exp_1 \concat \exp_2} {\prim {\exp_1}, {\typ_1}, {\dir_1}} {\prim {\exp_2}, {\typ_2}, {\dir_2}} }
+  \inferrule
+     { \typWellFormed \typ }
+     { \typWellFormed {\setTyp \typ} }
+     \quad (\setT)
 
-  \inferrule[Rest]
-     { \expenv  {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
-       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\
-       t = \implicitCast {\typ_1} {\typ_2} \\
-       {\pprim {\exp_1}} = \cast \typ {\prim {\exp_1}}, {\typ_1}, {\dir_1} \\
-       {\pprim {\exp_2}} = \cast \typ {\prim {\exp_2}}, {\typ_2}, {\dir_2}}
-     { \coerceBinArgsEnv {\exp_1 \restOps \exp_2} {\pprim {\exp_1}} {\pprim {\exp_2}} }
+~ End InfRule
 
-\end{mathpar}
-~~
-~
+### Enumeration Type { #sec-enum-t }
 
-### Check Binary Operation Auxiliary Judgment 
-reduce enums removes all the enums recursively after reducing a type.
-in_or_dirless(typ1, typ2) retunrs direction of In if both typ1 and typ2 have In direction, o.w., it returns a directionless direction. 
-is true if and only if expression type t1 is equivalent to expression type t2 under environment env. Alpha equivalent types are equal. it takes the list of variables of the two types.
-is nonneg and is pos evaluate an expression at compile time and check if it's a nonneg or pos numeric.
-compile time known determinez if the value of an expression can be known at compile time.
-   it returns true for externs, packages, controls, and parsers..
-
-~ Center  {padding:1ex}
-~~ Snippet
-\begin{mathpar}
-  \small
-
-  \inferrule[LogicalOps($\ops=\&,\vert$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \typ_1 = \typ_2 = \boolTyp}
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} \boolTyp \dir }
-
-  \inferrule[NumericOps($+, -, *$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \typ_1 = \typ_2 = \bitWidthTyp \width \textOr \integerTyp \textOr \intWidthTyp \width }
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} {\typ_1} \dir }
-
-  \inferrule[EqualityChecks($==, !=$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \typEq {\emp} {\typ_1} {\typ_2} \\
-       \typHasEq {\typ_1} }
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} \boolTyp \dir }
-
-  \inferrule[OpSat($\plusSat,\subSat$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \typ_1 = \typ_2 = \bitWidthTyp \width \textOr \intWidthTyp \width}
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} {\typ_1} \dir }
-
-  \inferrule[BitwiseOps($\bitAnd, \bitOr, \bitXor, \bitComplement$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \typ_1 = \typ_2 = \bitWidthTyp \width \textOr \intWidthTyp \width}
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} {\typ_1} \dir }
-
-  \inferrule[BitstringConcatenation]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \left( \so {\typ_1 = \bitWidthTyp {\width_1}, \typ_2 = \bitWidthTyp {\width_2} \textOr \intWidthTyp {\width_2}} {\typ = \bitWidthTyp {\width_1 + \width_2}} \right) \\
-       \textOr \left( \so {\typ_1 = \intWidthTyp {\width_1}, \typ_2 = \bitWidthTyp {\width_2} \textOr \intWidthTyp {\width_2}} {\typ = \intWidthTyp {\width_1 + \width_2}} \right) }
-     { \binOpEnv {\exp_1 \concat \exp_2} {\exp_1 \concat \exp_2} {\typ} \dir }
-
-  \inferrule[ComparisonOps($<, \leq, >, \geq$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \left( \typ_1 = \typ_2 = \integerTyp \right) \\
-       \textOr \left( \typ_1 = \typ_2 = \bitWidthTyp \width \right) \\
-       \textOr \left( \typ_1 = \typ_2 = \intWidthTyp \width \right)}
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} \boolTyp \dir }
-
-  \inferrule[DivOps($\div, \mod$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \left( \so {\typ_1 = \typ_2 = \integerTyp, \nonNeg {\exp_1}, \pos {\exp_2}}  {\typ = \integerTyp} \right) \\
-       \textOr \left( \so {\typ_1 = \typ_2 = \bitWidthTyp \width, \nonNeg {\exp_1}, \pos {\exp_2}}  {\typ = \bitWidthTyp \width} \right) }
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} \typ \dir }
-
-  \inferrule[ShiftOps($\shiftL,\shiftR$)]
-     { \typ_1 = \reduceEnums {\exp_1} \\
-       \typ_2 = \reduceEnums {\exp_2} \\
-       \dir = \inOrLess {\typ_1} {\typ_2} \\
-       \nonNeg {\exp_2} \\
-       \left( \typ_1 = \bitWidthTyp \width \textOr \intWidthTyp \width \right) \\
-       \textOr \left( \typ_1 = \integerTyp, \compTimeKnown {\exp_2} \right) }
-     { \binOpEnv {\exp_1 \restOps \exp_2} {\exp_1 \restOps \exp_2} {\typ_1} \dir }
+An enumeration type contains a number of constants of string type and its declaration introduces a new identifier in the current naming scope. It could also have an underlying representation which states what is the type of its constants.
+The rules below state that an enum type is well-formed if the underlying representation is well-formed, if it has one. 
 
-\end{mathpar}
-~~
-~
 
-### Type Well-Formed Auxiliary Judgment
-it saturates all types first and then checks well-formedness. for breviety, we don't
-include the saturation in rules.
-is valid nested type outer inner checks whether the nested type is taking valid types in its inner and outer type based on P4's description of type nesting rules section 7.2.7 (provide link). 
-no duplicate determines if there are duplicate fields in a structure/type.
-~ Center  {padding:1ex}
-~~ Snippet
-\begin{mathpar}
-  \small
+~ Begin InfRule
 
-  \inferrule[Bool]
+  \mprset {vskip=0.7ex}
+  {\inferrule
      { }
-     { \typWellFormed \boolTyp }
+     { \typWellFormed \enumTypNoTypDef }
+     \quad (\enumOneT)}
 
-  \inferrule[String]
-     { }
-     { \typWellFormed \stringTyp }
+\and
 
-  \inferrule[Integer]
-     { }
-     { \typWellFormed \integerTyp }
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     { \typWellFormed \typ }
+     { \typWellFormed \enumTypDef }
+     \quad (\enumTwoT)}
 
-  \inferrule[Int]
-     { }
-     { \typWellFormed {\intWidthTyp \width} }
+~ End InfRule
 
-  \inferrule[Bit]
-     { }
-     { \typWellFormed {\bitWidthTyp \width} }
+### Record Type { #sec-record-t }
 
-  \inferrule[VarBit]
-     { }
-     { \typWellFormed {\varBitTyp \width} }
+A record has zero or more fields, which each field has a name and a type.
+The rule $\recordT$ states that a record type is well-formed if all its fields have well-formed types, all fields have types that can be nested in a record, and fields have distinct names. 
 
-  \inferrule[Error]
-     { }
-     { \typWellFormed \errTyp}
+Note that headers, header unions, and struct also have the same type and their well-formedness is defined the same.
 
-  \inferrule[Void]
-     { }
-     { \typWellFormed \voidTyp}
+- $\noDup \names$ checks that there is no duplicate name in $\names$. Remember that fields are just names (strings).
 
-  \inferrule[MatchKind]
-     { }
-     { \typWellFormed \matchKindTyp}
+~ Begin InfRule
 
-  \inferrule[Array]
-     { \typWellFormed \typ \\
-       \isValidNestedTyp {\arrayTyp \typ \size} {\typ}}
-     { \typWellFormed {\arrayTyp \typ \size} }
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     { \typWellFormed \typs \\
+       \isValidNestedTyp {\recordTyps \field \typ} \\
+       \noDup \fields}
+     { \typWellFormed {\recordTyps \field \typ} }
+     \quad (\recordT)}
 
-  \inferrule[Tuple]
-     { 1 \leq i \leq; \typWellFormed {\typ_i} \\
-       1 \leq i \leq; \isValidNestedTyp {\tupleTyp {\typ_1} {\typ_n}} {\typ_i}}
-     { \typWellFormed {\tupleTyp {\typ_1} {\typ_n}} }
+\and
 
-  \inferrule[List]
-     { 1 \leq i \leq; \typWellFormed {\typ_i} \\
-       1 \leq i \leq; \isValidNestedTyp {\listTyp {\typ_1} {\typ_n}} {\typ_i}}
-     { \typWellFormed {\listTyp {\typ_1} {\typ_n}} }
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     {\typWellFormed \typs \\
+       \isValidNestedTyp {\headerUnionTyps \field \typ} \\\\
+       \noDup \fields}
+     { \typWellFormed {\headerUnionTyps \field \typ} }
+     \quad (\headerUnionT)}
 
-  \inferrule[Set]
-     { \typWellFormed \typ }
-     { \typWellFormed {\setTyp \typ} }
+\and
 
-  \inferrule[EnumWithType]
-     { \typWellFormed \typ }
-     { \typWellFormed \enumTyp }
-
-  \inferrule[EnumWithoutType]
-     {  }
-     { \typWellFormed \enumTypNoTyp }
-
-  \inferrule[Record]
-     { 1 \leq i \leq; \typWellFormed {\typ_i} \\
-       1 \leq i \leq; \isValidNestedTyp \recordTyp {\typ_i} \\
-       \noDup {\field_1, \ldots, \field_n}}
-     { \typWellFormed \recordTyp }
-
-  \inferrule[HeaderUnion]
-     { 1 \leq i \leq; \typWellFormed {\typ_i} \\
-       1 \leq i \leq; \isValidNestedTyp \headerUnionTyp {\typ_i} \\
-       \noDup {\field_1, \ldots, \field_n}}
-     { \typWellFormed \headerUnionTyp }
-
-  \inferrule[Struct]
-     { 1 \leq i \leq; \typWellFormed {\typ_i} \\
-       1 \leq i \leq; \isValidNestedTyp \structTyp {\typ_i} \\
-       \noDup {\field_1, \ldots, \field_n}}
-     { \typWellFormed \structTyp }
-
-  \inferrule[Header]
-     { 1 \leq i \leq; \typWellFormed {\typ_i} \\
-       1 \leq i \leq; \isValidNestedTyp \headerTyp {\typ_i} \\
-       \noDup {\field_1, \ldots, \field_n}}
-     { \typWellFormed \headerTyp }
-
-  \inferrule[NewType]
+  \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
+
+### New Type Type { #sec-newtype-t }
+
+New type assigns a name to a type. So the $\newTypeT$ checks if the assignee type $\typ$ is well-formed.
+
+~ Begin InfRule
+
+  \inferrule
      { \typWellFormed \typ }
-     { \typWellFormed {\newTypeTyp \typ \name} }
+     { \typWellFormed {\newTypeTyp \typVar \typ} }
+     \quad (\newTypeT)
 
-  \inferrule[Specialized]
-     { blah }
-     { blah }
+~ End InfRule
 
-  \inferrule[Package]
-     { blah }
-     { blah }
+### Specialized Type { #sec-specialized-t }
 
-  \inferrule[Control]
-     { blah }
-     { blah }
+An specialized type specifies the types of parameters in a generic type, the underlying generic type in an specialized type is called the base type. An specialized type is necessary when the compiler cannot infer type arguments.
 
-  \inferrule[Parser]
-     { blah }
-     { blah }
+The rule $\specializedExternT$ states that the specialization of an extern type is well-formed if the extern $\name$ exists in the environment $\env$ and the specialization specifies the type of all its type parameters. Similarly, the rule $\specializedRestT$ states that the specialization of a package/control/parser/function is well-formed if it specifies the type of all its type parameters.
 
-  \inferrule[Extern]
-     { blah }
-     { blah }
+- $\lookupExternEnv \name$ looks up a variable $\name$ in extern environment $\externEnv$ and it returns the type parameters and methods of the extern. Since the rule $\specializedExternT$ only cares about the parameters we do not care about the methods, thus, we don't assign a variable name to it and use an underscore instead of it. 
+- $\getTypeParams \typ$ returns the type parameters from types that have type parameters including package, control, parser, and function.
 
-  \inferrule[Function]
-     { blah }
-     { blah }
+~ Begin InfRule
 
-  \inferrule[Action]
-     { blah }
-     { blah }
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     { \lookupExternEnv \name = ([\params], \_ ) \\
+        % 1 \leq i \leq n. \typWellFormed {\typ_i} \\
+        \typWellFormed \typs\\
+        |\typs| = |\params|}
+     { \typWellFormed {\spcTyp {\externTyp \name} \typs} }
+     \quad (\specializedExternT)}
 
-  \inferrule[Constructor]
-     { blah }
-     { blah }
+\and
 
-  \inferrule[Table]
-     { blah }
-     { blah }
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     { \getTypeParams \typ = \{\params\}\\
+        \typWellFormed {\typs} \\
+        |\params| = |\typs|}
+     { \typWellFormed {\spcTyp \typ {\typs}} }
+     \quad (\specializedRestT)}
 
-  \inferrule[TypeName]
-     { blah }
-     { blah }
+~ End InfRule
+
+### Package Type { #sec-package-t }
+
+A package type describes the signature of a package and it defines the type parameters and parameters of a package. It may also have wildcard parameters. 
+The rule $\packageT$ states that a package type is well-formed under the environment $\typEnv$ extended with the package's type parameters if all its parameters are direction-less and their types are well-formed. 
+
+- $\extendTypEnv \typVar$ extends the type environment $\typEnv$ with type variable $\typParam$. Note that the type inserted in the environment for a type variable is a type name.
+- $\isDirectionless \dir$ checks that the direction of parameter $\dir$ is $\less$ or not.
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { \isDirectionless {\dir} \\
+         \typWellFormedWithEnv {\extendTypsEnv \typVar} \typs }
+       { \typWellFormed {\packageTyp {\typParams} {\prms} } }
+     \quad (\packageT)}
+
+~ End InfRule
+
+### Control and Parser Type { #sec-control-t }
+
+A control type is similar to a type signature of a function in that it defines the type parameters used in the control and its parameters, however, it does not have a return type. The rule $\controlT$ states that the control type is well-formed under the environment $\typEnv$ extended with type variables $\typParams$ if all the types of its parameters are well-formed.
+
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     {\typWellFormedWithEnv {\extendTypsEnv \typParam} {\typs}}
+       { \typWellFormed {\controlTyp {\typParams} {\prms} } }
+       \quad (\controlT)}
+
+\and
+
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     {\typWellFormedWithEnv {\extendTypsEnv \typParam} {\typs}}
+       { \typWellFormed {\parserTyp {\typParams} {\prms} } }
+       \quad (\parserT)}
+
+~ End InfRule
+
+### Extern Type { #sec-extern-t }
+
+The rule $\externT$ states that an extern type is well-formed if it has no type parameter in the environment. 
+$\lookupExternEnv \name$ where $\name$ is an extern returns an externMethods type which includes a list of strings as
+type parameters which must be empty for it to be well-typed and a function type which doesn't care for function type.
+
+
+~ Begin InfRule
+
+  \inferrule
+     { \lookupExternEnv \name = (\emp, \_ )}
+     { \typWellFormed {\externTyp \name} }
+     \quad (\externT)
+
+~ End InfRule
+
+### Function Type { #sec-func-t }
+
+A function type describes the return type of the function, its type parameters, and its parameters. The rule $\functionT$ states that the function type is well-formed if its return type is well-formed and the types of its parameters are well-formed under environment $\typEnv$, extended with function's type parameters. 
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     { \typWellFormed \typ \\
+       \typWellFormedWithEnv {\extendTypsEnv \typVar} \typs}
+       % 1 \leq i \leq n. \typWellFormedWithEnv {\insertToEnvv {\overline {\typParam : \typNameTyp \typParam}}} {\typ_i} }
+     % <return type> <function name>(x1,...,xn) {...}
+     { \typWellFormed {\funcType \kind {\typParams} {\prms} \typ} }
+     \quad (\functionT)}
+
+~ End InfRule
+
+### Action Type { #sec-action-t }
+
+An action type defines data and control parameters and it is well-formed if the types of all parameters are well-formed and the control parameters are direction-less.
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     {  \typWellFormed {\typs} \\
+        \typWellFormed {\overline {\prim \typ}} \\
+       \isDirectionless \dirs \\
+       \isDirectionless {\overline {\prim \dir}}}
+     { \typWellFormed {\actionTyp {\prms} {\prmss}} }
+     \quad (\actionT)}
+
+~ End InfRule
+
+### Constructor Type { #sec-constructor-t }
+
+The rule $\constructorT$ states that a constructor type is well-formed if its return type $\typ$ is well formed and the types of its parameters are well-formed under the environment $\typEnv$ extended with the constructor's type parameters. Note that \_ indicates the wildcard parameters. 
+ 
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+  {\inferrule
+     { \typWellFormed {\typ} \\
+       % \prim \env = \insertTypVars {\param_1, \ldots, \param_n} \\
+       \typWellFormedWithEnv {\extendTypEnv \typVars} {\typs} \\
+       \isDirectionless {\dirs}}
+     { \typWellFormed {\constructorTyp \typParams \prms {\typ}}}
+     \quad (\constructorT)}
+
+~ End InfRule
+
+### Table Type { #sec-table-t }
+
+A table type is well-formed under an environment if it exists in the environment.
+
+- $\lookupTypEnv \name $ Looks up $\name$ from the type environment $\typEnv$ and returns the type assigned to it.
+
+~ Begin InfRule
+
+  \inferrule
+     { \lookupTypEnv \name = \whatevs}
+     { \typWellFormed {\tableTyp \name} }
+     \quad (\tableT)
+
+~ End InfRule
+
+### Reference Type { #sec-typename-t }
+
+The rule $\typeNameT$ states that the type name $\name$ is well-formed under the environment $\env$ if it exists in the environment.
+
+~ Begin InfRule
+
+  \inferrule
+     { \lookupTypEnv \typVar = \whatevs}
+     { \typWellFormed {\typVar} }
+     \quad (\typeNameT)
+
+~ End InfRule
+
+## Type Equality Judgment { #sec-type-eq }
+```**TODO**: refer to type_equality and solve_types functions in impl. For type equality of p4 spec refer to to section 8, under each operation there's a one liner that talks about when two types are equal for the type it's covering. ```
+
+- The [type equality judgment][#sec-type-eq] checks the equality of two types. It has
+the form $\typEqEnv {\overline {(\var, \prim \var)}} {\typ_1} {\typ_2} $ which states that the types $\typ_1$ and $\typ_2$ are equivalent under the environment $\env$ with equivalent variable pairs $\overline {(\var, \prim \var)}$. Note that Alpha equivalent types are equivalent. 
+
+
+## Type Unification { #sec-type-unify }
+
+Type unification attempts to unify two expression types, that is, it attempts to come up with constraints that allow the two types to be equivalent. The constraints are just assignments of types to unknown type variables (given as $\typVars$). 
+
+- type unification for type produces by type checking, i.e., typed.type.t
+- both types are reduced first. for brevity we omit the reduction from rules. so type 1 and type 2 in rules are already reduced.
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \boolTyp \boolTyp {\overline {\typVar : \bot}}}
+     \quad (\rn{Bools})}
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \stringTyp \stringTyp {\overline {\typVar : \bot}}}
+     \quad (\rn{Strings})}
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \integerTyp \integerTyp {\overline {\typVar : \bot}}}
+     \quad (\rn{Integers})}
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \errTyp \errTyp {\overline {\typVar : \bot}}}
+     \quad (\rn{Errors})}
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \matchKindTyp \matchKindTyp {\overline {\typVar : \bot}}}
+     \quad (\rn{MatchKinds})}
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \voidTyp \voidTyp {\overline {\typVar : \bot}}}
+     \quad (\rn{Voids})}
+
+~ End InfRule
+
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Specializeds})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{TypeNames})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{NewTypes})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{FixedLengths})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Arrays})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Tuples})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+% check which one of record, header, header union, struct you used in well-formedness.
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Records})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Sets})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Enums})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Packages})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Controls})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Parsers})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Externs})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Actions})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Functions})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Constructors})}
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \mprset {vskip=0.7ex}
+    {\inferrule
+       { }
+       { \unify \env \typeEqs \typVars \ \ {\overline {\typVar : \bot}}}
+     \quad (\rn{Tables})}
+
+~ End InfRule
+
+``TODO: check see if you need implicit casting incorporated in unification of types.``
+
+# Expression's Typing Rules { #sec-exp-typing }
+
+The judgment form
+$\expenv {\exp} {\prim \exp} \typ \dir $ states that expression $\exp$
+written in surface syntax translates to expression $\prim \exp$ in the IR syntax with
+the type $\typ$ and direction $\dir$ under environment $\env$. For now, we do not
+present the syntax of the surface syntax and IR. Note that there is not much difference
+between the two.
+
+``**Restriction**``
+Petr4 doesn't have the product operation where multiple sets can be combined using
+Cartesian product and the type of a product of sets is a set of tuples. (refer to
+section 8.12.5. of P4 spec (**DISCUSS**))
+
+``**NOTE**``
+I couldn't find the followings in section 8 of p4 spec:
+array access, bits string access, type member, anonymous instant (this is probably method invocation or something).
+
+
+## Boolean, String, and Integer Constructor Rules { #sec-base-const-e }
+
+Base constructors such as boolean, string, and all integer constructors simply construct values of their type. 
+The rule $\boolE$ states that a boolean expression in surface syntax has the type $\boolTyp$, it translates to the same boolean expression in the IR syntax, and has the $\less$ direction.
+The rules $\stringE$, $\integerE$, $\bitStringE$, and $\signedIntE$ are similar to $\boolE$. 
+
+~ Begin InfRule
+
+  \inferrule
+     { }
+     {\expenv \bool \bool \boolTyp \less}
+     \quad (\boolE)
+
+  \inferrule
+     { }
+     {\expenv \str \str \stringTyp \less}
+     \quad (\stringE)
+
+  \inferrule
+     { }
+     {\expenv \int \int \integerTyp \less}
+     \quad (\integerE)
+
+  \inferrule
+     { }
+     {\expenv {\bitWidth \bit \width} {\bitWidth \bit \width} {\bitWidthTyp \width} \less}
+     \quad (\bitStringE)
+
+  \inferrule
+     { }
+     {\expenv {\intWidth \int \width} {\intWidth \int \width} {\intWidthTyp \width} {\less}}
+     \quad (\signedIntE)
+
+~ End InfRule
+
+## Name Rule { #sec-name-e }
+
+The rule $\nameE$ looks up the name of a variable from the environment and returns its type and direction. Note that if the environment doesn't contain the name the rule will fail.
+
+- When $\lookupEnv \name$ looks up a variable name in the environment, it returns its type and direction. When we only need the
+type or the direction of the variable we simply ignore the other one by using an underscore for it. So you could see
+formalization such as $\lookupEnv \name = (\typ, \_ )$ which states that we looked up variable
+$\name$ from the environment and we found out that its type is $\typ$. Similarly, the
+formalization $\lookupEnv \name = (\typ, \dir)$ states that we looked up variable
+$\name$ in the environment $\env$ and it has the type $\typ$ and direction $\dir$.
+
+~ Begin InfRule
+
+  \inferrule
+     {\lookupEnv \name = (\typ, \dir)}
+     {\expenv \name \name \typ \dir}
+     \quad (\nameE)
+
+~ End InfRule
+
+## Array Access Rule { #sec-array-access-e }
+
+$\arrayAccess {\exp_1} {\exp_2}$ denotes accessing the $\exp_2$^th^ element from the array $\exp_1$. 
+The rule $\arrayAccessE$ states that expression $\arrayAccess {\exp_1} {\exp_2}$
+translates to $\arrayAccess {\prim {\exp_1}} {\prim {\exp_2}}$
+when $\exp_1$ has the array type $\arrayTyp \typ \size$ and $\exp_2$ has a numeric type. 
+
+- $\mathit{is\_X} (\typ)$ checks if the type $\typ$ is of the specific kind/type/structure $X$.
+For example, $\isNumeric \typ$
+checks that the type $\typ$ is of numeric nature, that is, if it is fixed length signed or
+unsigned integer or arbitrary precision integer.
+
+~ Begin InfRule
+
+  \inferrule
+     {\expenv {\exp_1} {\prim {\exp_1}} {\arrayTyp \typ \size} \dir \\\\
+      \expenv {\exp_2} {\prim {\exp_2}} {\prim \typ} {\prim \dir} \\\\
+      % \isArray {\arrayTyp \typ \size} \\
+      \isNumeric {\prim \typ}}
+     {\expenv {\arrayAccess {\exp_1} {\exp_2}} {\arrayAccess {\prim {\exp_1}} {\prim {\exp_2}}} \typ \dir }
+     \quad (\arrayAccessE)
+
+~ End InfRule
+
+## Bitstring Access (Slice) Rule { #sec-bitstring-slice-e }
+
+$\bitStringAccess {\exp_1} {\exp_2} {\exp_3}$ denotes slicing a the bitstring $\exp_1$ from bit $\exp_2$ to $\exp_3$.
+The rule $\bitStringAccessE$ states that accessing $\exp_2$ to $\exp_1$ from the bit string $\exp_1$ translates to accessing $\int_1$ to $\int_2$ from the bit string $\prim {\exp_1}$ which has the type bit string of length $\int_2 - \int_1$ if $\exp_1$ either has the type $\bitWidthTyp \width$ or $\intWidthTyp \width$ and both expressions $\exp_2$ and $\exp_3$ are of numeric types under the $\cte$ context and their values can be known at the compile time and the values respectively are $\int_1$ and $\int_2$. It only makes sense that when slicing (accessing) a bit string, the start $\int_1$ must be smaller than or equal to the end of access $\int_2$ and both must be smaller than the length of the bit string $\width$. 
+
+- $\widthInt \typ$ checks if the type $\typ$ is a fixed-length integer, that is,
+if it is either $\bitWidthTyp \width$ or $\intWidthTyp \width$ and returns its width. 
+- $\sat \typ$ saturates a type.
+Remember that saturating a type eliminates all type references in type
+$\typ$ and replaces them with the type they refer to. Thus, the result of saturation
+contains no type synonym (_TypeName_ in Petr4) constructors that are used to give a name to a new type.
+- $\reduce \typ $ saturates the type $\typ$ saturates a type first and then applies the arguments to the parameters of a specialized type that its base has parameters.
+- $\compileTimeEval \exp$ evaluates the expression $\exp$ at compile time and returns its value if $\exp$ is a well-typed expression. 
+
+~ Begin InfRule
+
+  \inferrule
+     {\expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\\\
+      \expenvWithCtxt \cte {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\\\
+      \expenvWithCtxt \cte {\exp_3} {\prim {\exp_3}} {\typ_3} {\dir_3} \\\\
+      \widthInt {\reduce {\typ_1}} = \width \\\\
+      % = \intWidthTyp \width \textOr \bitWidthTyp \width\\
+      \isNumeric {\sat {\typ_2}} \\
+      \isNumeric {\sat {\typ_3}} \\\\
+      \compileTimeEval {\prim {\exp_2}} = \int_1 \\
+      \compileTimeEval {\prim {\exp_3}} = \int_2 \\\\
+      0 \leq \int_1 < \width \\
+      \int_1 \leq \int_2 < \width
+      }
+     {\expenv {\bitStringAccess {\exp_1} {\exp_2} {\exp_3}} {\bitStringAccess {\prim {\exp_1}} {\prim {\exp_2}} {\prim {\exp_3}}} {\bitStringTyp {\int_2 - \int_1}} {\dir_1} }
+     \quad (\bitStringAccessE)
+
+~ End InfRule
+
+## List Constructor Rule { #sec-list-e }
+
+$\list {\exps}$ constructs a list of expressions.
+The rule $\listE$ states that under environment $\env$ and context $\ctxt$,
+the list $\list {\exps}$ translates to
+$\list {\overline {\prim \exp}}$ in the IR and has the tuple type
+$\listTyps \typ$ with direction $\less$ if its expressions translate to
+$\overline {\prim \exp}$ with types $\typs$ and directions $\dirs$ under the
+same environment and context.
+
+~ Begin InfRule
+
+  % \inferrule
+  %    {1 \leq i \leq n. \expenv {\exp_i} {\prim {\exp_i}} {\typ_i} {\dir_i}}
+  %    {\expenv {\list {\exp_1, \ldots, \exp_n}} {\list {\prim {\exp_1}, \ldots, \prim {\exp_n}}} {\listTyp {\typ_1} {\typ_n}} \less }
+  %    \quad (\listE)
+
+  \inferrule
+     {\expenv {\exps} {\overline {\prim \exp}} {\typs} {\dirs}}
+     {\expenv {\list \exps} {\list {\overline {\prim \exp} }} {\listTyps \typ} \less }
+     \quad (\listE)
+
+~ End InfRule
+
+## Record Constructor Rule { #sec-record-e }
+
+$\records \exp$ denotes a record where an expression is assigned to each field of the record.
+The rule $\recordE$ is similar to $\listE$ rule. 
+
+~ Begin InfRule
+
+  % \inferrule[\recordE]
+  %    {1 \leq i \leq n. \expenv {\exp_i} {\prim {\exp_i}} {\typ_i} {\dir_i}  }
+  %    {\expenv {\record 1 n} {\recordd 1 n {\prim \exp}} {\recordTypDef} \less  }
+
+  \inferrule
+     {\expenv {\exps} {\overline {\prim \exp}} {\typs} {\dirs}}
+     {\expenv {\records \exp} {\records {\prim \exp}} {\recordTyps \field \typ} \less  }
+     \quad (\recordE)
+
+~ End InfRule
+
+## Unary Operations Rules { #sec-unary-ops-e }
+
+The rule $\logicalNegE$ states that under the environment $\env$ and context $\ctxt$
+the expression $!\exp$ translates to the expression $!\prim\exp$ with the type $\boolTyp$ and direction $\dir$ if expression $\exp$ translates to $\prim\exp$ with type $\boolTyp$ and direction $\dir$ under the same environment and context.
+
+Rules $\bitwiseComplementE$ and $\unaryMinusE$ are similar to the rule $\logicalNegE$.
+Additionally, they restrict the type of the $\exp$. 
+
+- $\isInt \typ$ checks if the type $\typ$ is either $\bitWidthTyp \width$, $\intWidthTyp \width$, or $\integerTyp$.
+
+``**Discrepancy**``
+P4 spec states that all expressions of type int MUST be compile-time known values but
+Petr4 doesn't always check this. (ref: section 8.7 spec. e.g., unaryminus or binaryops rules.)
+
+~ Begin InfRule
+
+  \inferrule
+     { \expenv \exp {\prim \exp} \boolTyp \dir }
+     { \expenv {!\exp} {!\prim \exp} \boolTyp \dir }
+     \quad (\logicalNegE)
+
+  \inferrule
+     { \expenv \exp {\prim \exp} \typ  \dir \\
+       \widthInt \typ = \_}
+       % \typ = {\bitWidthTyp \width} \textOr \intWidthTyp \width}
+     { \expenv {\bitComplement\exp} {\bitComplement\prim \exp} {\typ} \dir }
+     \quad (\bitwiseComplementE)
+
+  \inferrule
+     { \expenv \exp {\prim \exp} \typ  \dir \\
+       \isInt \typ}
+       % \typ = {\bitWidthTyp \width} \textOr \intWidthTyp \width \textOr \integerTyp}
+     { \expenv {-\exp} {-\prim \exp} {\typ} \dir }
+     \quad (\unaryMinusE)
+
+~ End InfRule
+
+``**DISCREPANCY**``
+
+- P4 spec defines bitwise complement only for bit<w> but Petr4 also allows it for int<w>. (ref: type_unary_op bitnot impl. section 8.5 spec. bitwisecomplement rule.)
+
+## Binary Operation Rules { #sec-bin-ops-e }
+
+A binary operation is applied to two operands and it is written as $\exp_1 \restOps \exp_2$ where $\restOps$ indicates one or more operators. The binary operation rules are organized line-by-line for readability:
+
+- The name of each rule is located on top of the rule and it contains the operators
+that it covers. For example, the rule
+$\rn{LogicalOps}\rAE(\ops=\&\&,\vert\vert)$
+applies to both **logical and** and **logical or**, that is, while reading the rule,
+one can substitute $\ops$ for either $\&\&$ or $\vert\vert$.
+- In all the binary operation rules, the first line states that the expression typing judgment is applied recursively to the operands.
+- Then if applicable in second line, the rule checks whether the type of one of the operands can be implicitly casted to the other one. If so, it casts the said operand. This is done for all binary operation rules **except** for $\rn{BitstringConcatenation}\rE$ and $\rn{ShiftOps}\rE(\ops=\shiftL,\shiftR)$.
+- Then, the type of the operands are reduced to remove all enums recursively and any condition that must hold for the operator(s) of the rule is checked.
+- Finally, the direction of the expression is determined. 
+
+The following helpers are used in the binary operation rules:
+
+- $\implicitCast {\typ_1} {\typ_2}$ denotes possible implicit casts between different kinds of integers and returns the type that the other type can be casted to. It is described below (Note that it follows P4's implicit
+casting behavior and it is defined in more details in [cast auxiliary judgment][#sec-cast-helper].):
+  * $\implicitCast {\bitWidthTyp \width} \integerTyp   = \bitWidthTyp \width$
+  * $\implicitCast \integerTyp  {\bitWidthTyp \width}  = \bitWidthTyp \width$
+  * $\implicitCast {\intWidthTyp \width} \integerTyp   = \intWidthTyp \width$
+  * $\implicitCast \integerTyp {\intWidthTyp \width}   = \intWidthTyp \width$
+- $\cast \typ \exp$ synthesizes a cast expression if the type of the expression $\exp$ is different from the type $\typ$.
+- $\reduceEnums \typ$ removes all the enums recursively from a type after reducing it.
+- $\inOrLess {\dir_1} {\dir_2}$ returns the $\inDir$ direction if both directions $\dir_1$ and $\dir_2$ are $\inDir$, otherwise, it returns the $\less$ direction.
+- $\typHasEq \typ$ checks if equality of two expressions from the type $\typ$ has been defined. Note that it first reduces the type $\typ$.
+- $\concatCond {\typ_1} {\typ_2}$ is a helper function that determines the type of a concatenation expression based on the types of its two operands:
+  + if $\typ_1 = \bitWidthTyp {\width_1}, \typ_2 = \bitWidthTyp {\width_2}$, then
+    $\concatCond {\typ_1} {\typ_2} = \bitWidthTyp {\width_1 + \width_2}$
+  + if $\typ_1 = \bitWidthTyp {\width_1}, \typ_2 = \intWidthTyp {\width_2}$, then
+    $\concatCond {\typ_1} {\typ_2} = \bitWidthTyp {\width_1 + \width_2}$
+  + if $\typ_1 = \intWidthTyp {\width_1}, \typ_2 = \bitWidthTyp {\width_2}$, then
+    $\concatCond {\typ_1} {\typ_2} = \intWidthTyp {\width_1 + \width_2}$
+  + if $\typ_1 = \intWidthTyp {\width_1}, \typ_2 = \intWidthTyp {\width_2}$, then
+    $\concatCond {\typ_1} {\typ_2} = \intWidthTyp {\width_1 + \width_2}$
+- $\bothInt  {\typ_1} {\typ_2}$ is a helper function that checks if both types are a fixed-length or arbitrary precision integer type. That is, it checks the conditions below and returns $\tr$ if one of them holds:
+  + $\typ_1 = \typ_2 = \integerTyp$
+  + $\typ_1 = \typ_2 = \bitWidthTyp \width$
+  + $\typ_1 = \typ_2 = \intWidthTyp \width$
+- $\nonNeg \exp$ and $\pos \exp$ evaluate an expression at compile time and check if it is a non-negative or positive number, respectively.
+- $\divCond {\typ_1} {\typ_2}$ is a helper function that checks the following conditions for a division/modulo expression and returns $\tr$ if one of them holds:
+  + if $\typ_1 = \typ_2 = \integerTyp$, then
+    $\divCond {\typ_1} {\typ_2} = \integerTyp$
+  + if $\typ_1 = \typ_2 = \bitWidthTyp \width$, then
+    $\divCond {\typ_1} {\typ_2} = \bitWidthTyp \width$
+- $\shiftCond {\typ} {\exp}$ is a helper function that checks the following conditions of the first expression and it returns $\tr$ if one of them holds:
+  + $\typ = \bitWidthTyp \width$
+  + $\typ = \intWidthTyp \width$
+  + $\typ = \integerTyp$ and $\compTimeKnown \exp$
+- $\compTimeKnown \exp$ checks if the value of expression $\exp$ is known during the
+compilation. It does so by evaluating the expression $\exp$ at compile time, if that is
+possible then we know the value at compile time. Otherwise, if the expression $\exp$ is
+a specialized type, extern, package, control, or parser but we cannot evaluate it at
+compile time we still consider it known at compile time.
+
+~ Begin InfRule
+
+  \inferrule[\rn{LogicalOps}\rAE($\ops=\&\&,\vert\vert$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}\\\\
+       \implicitCast {\typ_1} {\typ_2} = \typ \\
+       \cast \typ {\prim {\exp_1}} = \pprim {\exp_1}\\
+       \cast \typ {\prim {\exp_2}} = \pprim {\exp_2}\\\\
+       \reduceEnums {\typ_1} =
+       \reduceEnums {\typ_2} = \boolTyp \\\\
+       \inOrLess {\dir_1} {\dir_2} = \dir}
+     {\expenv {\exp_1 \restOps \exp_2} {\pprim {\exp_1} \restOps \pprim {\exp_2}} \boolTyp \dir }
+     % { \binOpEnv {\exp_1 \restOps \exp_2} \boolTyp \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2} }
+
+  \inferrule[\rn{NumericOps}\rE($\ops=+, -, *$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}\\\\
+       \implicitCast {\typ_1} {\typ_2} = \typ \\
+       \cast \typ {\prim {\exp_1}} = \pprim {\exp_1}\\
+       \cast \typ {\prim {\exp_2}} = \pprim {\exp_2}\\\\
+       \reduceEnums {\typ_1} = \reduceEnums {\typ_2} = \typ \\\\
+       \isInt \typ\\\\
+       \inOrLess {\dir_1} {\dir_2} = \dir 
+       }
+     {\expenv {\exp_1 \ops \exp_2} {\pprim {\exp_1} \ops \pprim {\exp_2}} \typ \dir }
+     % { \binOpEnv {\exp_1 \restOps \exp_2} {\typ} \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2}}
+
+  \inferrule[\rn{EqualityChecks}\rE($\ops=\ ==, !=$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}\\\\
+       \implicitCast {\typ_1} {\typ_2} = \typ \\
+       \cast \typ {\prim {\exp_1}} = \pprim {\exp_1}\\
+       \cast \typ {\prim {\exp_2}} = \pprim {\exp_2}\\\\
+       \typEqEnv {\emp} {\reduceEnums {\typ_1}} {\reduceEnums {\typ_2}} \\\\
+       % \typEq {\emp} {\typ_1} {\typ_2} \\
+       \typHasEq {\typ_1} \\\\
+       \inOrLess {\dir_1} {\dir_2} = \dir}
+     { \expenv {\exp_1 \ops \exp_2} {\pprim {\exp_1} \ops \pprim {\exp_2}} \boolTyp \dir }
+     % { \binOpEnv {\exp_1 \restOps \exp_2} \boolTyp \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2} }
+
+  \inferrule[\rn{OpSat}\rE($\ops = \plusSat,\subSat$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}\\\\
+       \implicitCast {\typ_1} {\typ_2} = \typ \\
+       \cast \typ {\prim {\exp_1}} = \pprim {\exp_1}\\
+       \cast \typ {\prim {\exp_2}} = \pprim {\exp_2}\\\\
+       \reduceEnums {\typ_1} = \reduceEnums {\typ_2} = \typ \\\\
+       \widthInt {\typ} = \_ \\\\
+       % \typ_2 = \bitWidthTyp \width \textOr \intWidthTyp \width \\
+       \inOrLess {\dir_1} {\dir_2} = \dir}
+     {\expenv {\exp_1 \ops \exp_2} {\pprim {\exp_1} \ops \pprim {\exp_2}} \typ \dir }
+       % { \binOpEnv {\exp_1 \restOps \exp_2} {\typ} \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2}}
+
+  \inferrule[\rn{BitwiseOps}\rE($\ops=\bitAnd, \bitOr, \bitXor, \bitComplement$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}\\\\
+       \implicitCast {\typ_1} {\typ_2} = \typ \\
+       \cast \typ {\prim {\exp_1}} = \pprim {\exp_1}\\
+       \cast \typ {\prim {\exp_2}} = \pprim {\exp_2}\\\\
+       \reduceEnums {\typ_1} = \reduceEnums {\typ_2} = \typ\\\\
+       \widthInt {\typ} = \_ \\\\
+       % \typ = \typ_2 = \bitWidthTyp \width \textOr \intWidthTyp \width \\
+       \inOrLess {\dir_1} {\dir_2} = \dir}
+     {\expenv {\exp_1 \ops \exp_2} {\pprim {\exp_1} \ops \pprim {\exp_2}} \typ \dir }
+       % { \binOpEnv {\exp_1 \restOps \exp_2} {\typ} \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2}}
+
+  \inferrule[\rn{BitstringConcatenation}\rE]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\\\
+       \reduceEnums {\typ_1} = \prim {\typ_1} \\
+       \reduceEnums {\typ_2} = \prim {\typ_2} \\\\
+       \concatCond {\prim {\typ_1}} {\prim {\typ_2}} = \typ\\\\
+       \inOrLess {\dir_1} {\dir_2} = \dir}
+     {\expenv {\exp_1 \concat \exp_2} {\pprim {\exp_1} \concat \pprim {\exp_2}} \typ \dir }
+     % { \binOpEnv {\exp_1 \concat \exp_2} {\typ} \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2}}
+
+  \inferrule[\rn{ComparisonOps}\rE($\ops= <, \leq, >, \geq$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}\\\\
+       \implicitCast {\typ_1} {\typ_2} = \typ \\
+       \cast \typ {\prim {\exp_1}} = \pprim {\exp_1}\\
+       \cast \typ {\prim {\exp_2}} = \pprim {\exp_2}\\\\
+       \reduceEnums {\typ_1} = \prim {\typ_1} \\
+       \reduceEnums {\typ_2} = \prim {\typ_2} \\\\
+       \bothInt {\prim {\typ_1}} {\prim {\typ_2}}\\\\
+       \inOrLess {\dir_1} {\dir_2} = \dir
+      }
+    { \expenv {\exp_1 \ops \exp_2} {\pprim {\exp_1} \ops \pprim {\exp_2}} \boolTyp \dir }
+     % { \binOpEnv {\exp_1 \restOps \exp_2} \boolTyp \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2}}
+
+  \inferrule[\rn{DivOps\rE}($\ops=\div, \mod$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2}\\\\
+       \implicitCast {\typ_1} {\typ_2} = \typ \\
+       \cast \typ {\prim {\exp_1}} = \pprim {\exp_1}\\
+       \cast \typ {\prim {\exp_2}} = \pprim {\exp_2}\\\\
+       \reduceEnums {\typ_1} = \prim {\typ_1}\\
+       \reduceEnums {\typ_2} = \prim {\typ_2}\\\\
+       \divCond {\prim {\typ_1}} {\prim {\typ_2}} = \typ \\
+       \nonNeg {\exp_1} \\
+       \pos {\exp_2}\\\\
+       \inOrLess {\dir_1} {\dir_2} = \dir}
+     {\expenv {\exp_1 \ops \exp_2} {\pprim {\exp_1} \ops \pprim {\exp_2}} \typ \dir }
+     % { \binOpEnv {\exp_1 \restOps \exp_2} \typ \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2}}
+
+  \inferrule[\rn{ShiftOps}\rE($\ops=\shiftL,\shiftR$)]
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\\\
+       \reduceEnums {\typ_1} = \prim {\typ_1}\\\\
+       % \typ_2 = \reduceEnums {\typ_2} \\
+       \nonNeg {\exp_2} \\
+       \shiftCond {\prim {\typ_1}} {\exp_2}\\\\
+       \inOrLess {\dir_1} {\dir_2} = \dir}
+     {\expenv {\exp_1 \ops \exp_2} {\pprim {\exp_1} \ops \pprim {\exp_2}} {\prim {\typ_1}} \dir }
+     % { \binOpEnv {\exp_1 \restOps \exp_2} {\prim {\typ_1}} \dir {\typ_1} {\typ_2} {\dir_1} {\dir_2}}
+
+~ End InfRule
+
+``**DISCREPANCY**``
+
+- P4 spec states that all expressions of type int MUST be compile-time known values but
+Petr4 doesn't always check this. (ref: section 8.7 spec. e.g., unaryminus or binaryops rules.)
+- P4 spec defines bitwise operations and concatenation for bit<w> but Petr4 also allows them for int<w>. (ref: bitwiseops and bitstringconcatenation rules. section 8.5. check_binary_op impl. )
+- P4 spec defines division and modulo only for arbitrary-precision integers but petr4 allows them for bit<w> too. (ref: divops rule. section 8.7. check_binary_op impl.)
+
+## Cast Rule { #sec-cast-e }
+
+The expression $\cast \typ \exp$ casts expression $\exp$ to type $\typ$. However, it is
+not possible to cast an expression from every type to another type. Thus, the $\castE$
+rule states which casts are possible. Specifically, it states that the cast expression
+$\cast \typ \exp$ translates to the expression $\cast {\typ_1} {\exp_1}$ in the IR with
+the type $\typ_3$ and direction $\less$ if expression $\exp$ is translated to $\exp_1$,
+the translation of type $\typ$ to types in the IR is well-formed, and the explicit cast
+of the type of expression $\exp_1$ (that is, $\typ_1$) to the
+translated type of casting type $\typ$ (that is, $\prim \typ$) is valid.
+
+- $\explicitCastOK {\typ_1} {\typ_2}$ is an auxiliary judgment for valid explicit cast
+of types.
+The [casting auxiliary judgment][#sec-cast-helper] defines rules for implicitly
+and/or explicitly casting one type to another. Specifically, the judgment
+$\castenv \ {\typ_1} {\typ_2}$ states that under environment $\env$,
+the type $\typ_1$ can be casted to type $\typ_2$ either explicitly or implicitly.
+However, if the arrow is subscripted with $i$ or $e$ it states that the cast is only
+done implicitly or explicitly, respectively.
+- $\trans \typ \emp$ ``TODO: complete``
+
+``**TODO**``
+The implementation saturates types both in the $\castE$ rule as well as saturating them
+in the helper judgment. Fix this later. 
+
+~ Begin InfRule
+
+  \inferrule
+     { \expenv \exp {\exp_1} {\typ_1} \dir \\
+       % \typ_2 = \sat {\typ_1} \\
+       \prim \typ = \trans {\typ} {\emp} \\
+       % \pprim \typ = \sat {\prim \typ} \\
+       \typWellFormed {\prim \typ} \\
+       \explicitCastOK {\typ_1} {\prim \typ}}
+       % \explicitCastOK {\typ_2} {\pprim \typ}}
+     { \expenv {\cast \typ \exp} {\cast {\prim \typ} {\exp_1}} {\prim \typ} \less  }
+     \quad (\castE)
+
+~ End InfRule
+
+### Cast Auxiliary Judgment { #sec-cast-helper }
+
+This auxiliary judgment states if casting of a type to another, either explicitly or implicitly or both, is valid. 
+The arrow subscription with $e$ or $i$ indicates if a rule only applies for explicit or implicit cast only, respectively. Otherwise, the arrow does not have a subscription,
+meaning that it applies for both explicit and implicit casts. 
+The cast first saturates both types and then checks if the cast is valid. For simplicity, we omitted type saturations from the rules.
+
+``**NOTE**``
+P4 spec specifies casts up to Sets rule. The rest might be stated throughout the spec but I haven't found them yet.
+
+``**Discrepancy**``
+P4 spec states during the cast between int and bit<w> or int<w> the compiler would complain about overflow (or conversion of negative value for bit<w>) but Petr4's type system doesn't check this. (ref: I'm not sure if any other part of petr4 takes care of this. section 8.9.1 spec. cast_ok impl. explicit cast judgment.)
+
+
+~ Begin InfRuleHelper
+
+  \inferrule
+     { }
+     { \explCast {\bitWidthTyp 1} \boolTyp }
+     \quad (\rn{BitToBool}\rAE)
+
+  \inferrule
+     { }
+     { \explCast \boolTyp {\bitWidthTyp 1} }
+     \quad (\rn{BoolToBit}\rAE)
+
+  \inferrule
+     { \width = \prim \width }
+     { \explCast {\bitWidthTyp {\width}} {\intWidthTyp {\prim \width}}}
+     \quad (\rn{UnsignedIntToSigned}\rAE)
+
+  \inferrule
+     { \width = \prim \width }
+     { \explCast {\intWidthTyp {\width}} {\bitWidthTyp {\prim \width}}}
+     \quad (\rn{SignedIntToUnsigned}\rAE)
+
+  \inferrule
+     { }
+     { \explCast {\bitWidthTyp {\width}} {\bitWidthTyp {\prim \width}}}
+     \quad (\rn{UnsignedIntToUnsignedInt}\rSep\rn{Explicit}\rAE)
+
+  \inferrule
+     { \width = \prim \width}
+     { \implCast {\bitWidthTyp {\width}} {\bitWidthTyp {\prim \width}}}
+     \quad (\rn{UnsignedIntToUnsignedInt}\rSep\rn{Implicit}\rAE)
+
+  \inferrule
+     { }
+     { \explCast {\intWidthTyp {\width}} {\intWidthTyp {\prim \width}}}
+     \quad (\rn{SignedIntToSignedInt}\rSep\rn{Explicit}\rAE)
+
+  \inferrule
+     { \width = \prim \width}
+     { \explCast {\intWidthTyp {\width}} {\intWidthTyp {\prim \width}}}
+     \quad (\rn{SignedIntToSignedInt}\rSep\rn{Implicit}\rAE)
+
+  \inferrule
+     { }
+     { \castenv \  \integerTyp {\bitWidthTyp \width}}
+     \quad (\rn{ArbitraryPrecisionIntToUnsignedInt}\rAE)
+
+  \inferrule
+     { }
+     { \castenv \  \integerTyp {\intWidthTyp \width}}
+     \quad (\rn{ArbitraryPrecisionIntToSignedInt}\rAE)
+
+  \inferrule
+     { (\typEqEnv \emp {\prim \typ} {\newTypeTyp \typVar { \typ}})}
+     { \castenv \  {\newTypeTyp \typVar {\typ}} {\newTypeTyp \typVar {\prim \typ}}}
+     \quad (\rn{TypeDefs}\rAE\rSep\rn{1})
+
+  \inferrule
+     { (\typEqEnv \emp {\typ} {\newTypeTyp \typVar {\prim \typ}})}
+     { \castenv \  {\newTypeTyp \typVar {\typ}} {\newTypeTyp \typVar {\prim \typ}}}
+     \quad (\rn{TypeDefs}\rAE\rSep\rn{2})
+
+  \inferrule
+     { \explCast {\typ} {\prim \typ}}
+     { \explCast {\newTypeTyp \typVar {\typ}} {\prim \typ}}
+     \quad (\rn{TypeDefToType}\rSep\rn{Explicit}\rAE)
+
+  \inferrule
+     { \implCast {\typ} {\prim \typ}}
+     { \implCast {\newTypeTyp \typVar {\typ}} {\prim \typ}}
+     \quad (\rn{TypeDefToType}\rSep\rn{Implicit}\rAE)
+
+  \inferrule
+     { \explCast {\typ} {\prim \typ}}
+     { \explCast {\typ} {\newTypeTyp \typVar {\prim \typ}}}
+     \quad (\rn{TypeToTypeDef}\rSep\rn{Explicit}\rAE)
+
+  \inferrule
+     { \implCast {\typ} {\prim \typ}}
+     { \implCast {\typ} {\newTypeTyp \typVar {\prim \typ}}}
+     \quad (\rn{TypeToTypeDef}\rSep\rn{Implicit}\rAE)
+
+  \inferrule
+     { \typEqEnv \emp {\typ} {\prim \typ}}
+     { \castenv \ {\enumTypDef} {\enumTyp {\prim \typ} {\prim \field} {\overline {\prim \field}}}}
+     \quad (\rn{Enums}\rAE)
+
+  \inferrule
+     { \typEqEnv \emp {\typ} {\prim \typ}}
+     { \castenv \ {\enumTypDef} {\prim \typ}}
+     \quad (\rn{EnumToUnderlyingType}\rAE)
+
+  \inferrule
+     { \typEqEnv \emp {\typ} {\prim \typ}}
+     { \castenv \ {\typ} {\enumTyp {\prim \typ} {\field} {\fields}}}
+     \quad (\rn{TypeToEnumWithUndrlyingType}\rAE)
+
+  \inferrule
+     { \typEqEnv \emp {\typ} {\prim \typ}}
+     { \castenv \ {\setTyp {\typ}} {\setTyp {\prim \typ}} }
+     \quad (\rn{Sets}\rAE)
+
+  \inferrule
+     { \typEqEnv \emp {\typ} {\prim \typ}}
+     { \implCast {\typ} {\setTyp {\prim \typ}}}
+     \quad (\rn{TypeToSet}\rSep\rn{Implicit}\rAE)
+
+  \inferrule
+     { \typEqEnv \emp {\tupleTyps {\typs}} {\tupleTyps {\overline {\prim \typ}}}}
+     { \castenv \  {\listTyps {\typs} } {\tupleTyps {\overline {\prim \typ}}}}
+     \quad (\rn{ListToTuple}\rAE)
+
+  \inferrule
+     {\explCast {\typs} {\overline {\prim \typ}} }
+     {\explCast {\listTyps {\typs}} {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{ListToHeader}\rSep\rn{Explicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\tupleTyps \typs} {\tupleTyps {\overline {\prim \typ}}}}
+     {\explCast {\listTyps \typs} {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{ListToHeader}\rSep\rn{Explicit}\rAE\rSep\rn{2})
+
+  \inferrule
+     {\implCast {\typs} {\overline {\prim \typ}}}
+     {\implCast {\listTyps \typs} {\headerTyps \field {\prim \typ} }}
+     \quad (\rn{ListToHeader}\rSep\rn{Implicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\tupleTyps {\typs}} {\tupleTyps {\overline {\prim \typ}}}}
+     {\implCast {\listTyps \typs} {\headerTyps \field {\prim \typ} }}
+     \quad (\rn{ListToHeader}\rSep\rn{Implicit}\rAE\rSep\rn{2})
+
+  \inferrule
+     {\explCast {\typs} {\overline {\prim \typ}}}
+     {\explCast {\listTyps \typs} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{ListToStruct}\rSep\rn{Explicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\tupleTyps \typs} {\tupleTyps {\overline {\prim \typ}}}}
+     {\explCast {\listTyps \typs} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{ListToStruct}\rSep\rn{Explicit}\rAE\rSep\rn{2})
+
+  \inferrule
+     {\implCast {\typs} {\overline {\prim \typ}}}
+     {\implCast {\listTyps \typs} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{ListToStruct}\rSep\rn{Implicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\tupleTyps \typs} {\tupleTyps {\overline {\prim \typ}}}}
+     {\implCast {\listTyps \typs} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{ListToStruct}\rSep\rn{Implicit}\rAE\rSep\rn{2})
+
+  \inferrule
+     {\explCast {\typs} {\overline {\prim \typ}}}
+     {\explCast {\recordTyps \field \typ} {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{RecordToHeader}\rSep\rn{Explicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\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 \field \typ} {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{RecordToHeader}\rSep\rn{Implicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\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 \field \typ } {\structTyps \field {\prim \typ}}}
+     \quad (\rn{RecordToStruct}\rSep\rn{Explicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\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 \field \typ } {\structTyps \field {\prim \typ}}}
+     \quad (\rn{RecordToStruct}\rSep\rn{Implicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\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
+     {\explCast {\typs} {\overline {\prim \typ}}}
+     {\explCast {\headerTyps \field \typ } {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{HeaderToHeader}\rSep\rn{Explicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\headerTyps \field \typ} {\headerTyps \field {\prim \typ}}}
+     {\explCast {\headerTyps \field \typ } {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{HeaderToHeader}\rSep\rn{Explicit}\rAE\rSep\rn{2})
+
+  \inferrule
+     {\implCast \typs {\overline {\prim \typ}}}
+     {\implCast {\headerTyps \field \typ} {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{HeaderToHeader}\rSep\rn{Implicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\headerTyps \field \typ} {\headerTyps \field {\prim \typ}}}
+     {\implCast {\headerTyps \field \typ} {\headerTyps \field {\prim \typ}}}
+     \quad (\rn{HeaderToHeader}\rSep\rn{Implicit}\rAE\rSep\rn{2})
+
+  \inferrule
+     {\explCast {\typs} {\overline {\prim {\typ}}}}
+     {\explCast {\structTyps \field \typ} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{StructToStruct}\rSep\rn{Explicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\structTyps \field \typ} {\structTyps \field {\prim \typ}}}
+     {\explCast {\structTyps \field \typ} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{StructToStruct}\rSep\rn{Explicit}\rAE\rSep\rn{2})
+
+  \inferrule
+     {\implCast {\typs} {\overline {\prim \typ}}}
+     {\implCast {\structTyps \field \typ} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{StructToStruct}\rSep\rn{Implicit}\rAE\rSep\rn{1})
+
+  \inferrule
+     {\typEqEnv \emp {\structTyps \field \typ} {\structTyps \field {\prim \typ}}}
+     {\implCast {\structTyps \field \typ} {\structTyps \field {\prim \typ}}}
+     \quad (\rn{StructToStruct}\rSep\rn{Implicit}\rAE\rSep\rn{2})
+
+  \inferrule
+    { \typ = \prim \typ}
+    {\implCast {\typ} {\prim \typ}}
+    \quad (\rn{ID}\rSep\rn{Implicit}\rAE)
+
+~ End InfRuleHelper
+
+## Membership Rules { #sec-mem-e }
+
+A membership expression denoted by a dot, that is, $a.\name$ looks if $\name$ exists in $a$. And it can be a type, error, or expression membership depending on what $a$ is.
+An expression member looks up a _member_ in an expression.
+The member could be a field in
+a record type such as struct and header, or it could be a method in an extern or specialized type, or a special look up of an element of an array such as next, last, size, and last index.  
+
+
+The rules $\typeMemE$ and $\errMemE$ are rather simple.
+They just look up $\name$ extended with the type or error, respectively, in the environment. For example, the $\typeMemE$ states that under the environment $\env$ and context $\ctxt$, the expression $\typMem \typ \name$ is the same in the IR and has the type $\typ$ and direction $\less$ if $\typMem \typ \name$ exists in $\env$.
+
+The rule $\expMemE$ states that under the environment $\env$ and context $\ctxt$, the
+expression $\expMem \exp \name$ translates to the expression $\expMem {\prim \exp} \name$ with type $\pprim \typ$ and direction $\less$ where $\prim \exp$ is the translation of the expression $\exp$ and $\pprim \typ$ is the type of the member $\name$ from the reduced type of expression $\exp$ (that is, $\reduce \typ$) which is returned by the expression member auxiliary judgment. 
+
+- The [expression member auxiliary judgment][#sec-exp-mem-helper] is a helper judgment
+for the $\expMemE$ rule.
+It has the form $\fieldAccessEnv \ctxt \name \typ {\prim \typ}$
+which states that under environment $\env$ and context $\ctxt$, the member $\name$
+has the type $\prim \typ$ in an expression of type $\typ$.
+Simply stated, it looks up the type of the member from the expression passed from the $\expMemE$ rule. 
+Note that the expression has to be of a one of the types: record, extern, specialized, or array.
+
+~ Begin InfRule
+
+  \inferrule
+     {\lookupEnv {\typMem \typ \name} = (\typ, \dir)  }
+     {\expenv {\typMem \typ \name} {\typMem \typ \name} \typ \less  }
+     \quad (\typeMemE)
+
+  \inferrule
+     {\lookupEnv {\errMem \name} = (\errTyp, \dir)  }
+     {\expenv {\errMem \name} {\errMem \name} \errTyp \less  }
+     \quad (\errMemE)
+
+  \inferrule
+     { \expenv \exp {\prim \exp} {\typ} \dir \\
+       \reduce \typ = \prim \typ \\
+       % \structTypDef = \prim \typ\\
+       \fieldAccessEnv \ctxt \name {\prim \typ} {\pprim \typ}
+       }
+     { \expenv {\expMem \exp \name} {\expMem {\prim \exp} \name} {\pprim \typ} {\less} }
+     \quad (\expMemE)
+
+~ End InfRule
+
+### Expression Member Auxiliary Judgment { #sec-exp-mem-helper }
+
+This judgment ensures that the type of an expression in an expression member is either
+a record type, a specialized type, an extern type, or an array. Then, it looks up the member that is being accessed by the expression member. 
+
+~ Begin InfRuleHelper
+
+  \inferrule
+     {
+       % \expenv \exp {\prim \exp} {\typ} \dir \\
+       % \structTypDef = \reduce \typ \\
+       % \structTypDef = \prim \typ\\
+       % (\field_{n+1},\typ_{n+1}) = (\isValid, \funcTyp \builtin \ \ \boolTyp )\\
+       (\field, \typ) \in \overline {\field, \typ} 
+       % \exists 1 \leq i \leq n+1. \field_i = \field
+       }
+     { \fieldAccessEnv \ctxt \field {\structTyps \field \typ} {\typ} }
+     \quad (\rn{Type:Struct}\rAE)
+
+  \inferrule
+     {
+       % \expenv \exp {\prim \exp} {\typ} \dir \\
+       % \structTypDef = \reduce \typ \\
+       % \structTypDef = \prim \typ\\
+       % (\field_{n+1},\typ_{n+1}) = (\isValid, \funcTyp \builtin \ \ \boolTyp )\\
+       % \exists 1 \leq i \leq n+1. \field_i = \field
+       }
+     { \fieldAccessEnv \ctxt \field {\structTyps \field \typ} {\funcTyp \builtin \ \ \boolTyp} }
+     \quad (\rn{Type:Struct}\rSep\rn{Mem:isValid}\rAE)
+
+  \inferrule
+     {
+       % names in the following are actually methods. have to see what they contain.
+       \lookupEnv {\prim \name} = (\typParams,\overline {\name:\simpFuncTyp {\typ_{\mathit{in}}} {\typ_{\mathit{out}}}}) \\
+       % \prim \env = \insertToEnv  \typParams \typs \\
+       \suchThat {\exists \name_i: \prim {\typ_i} \in \overline {\name:\simpFuncTyp {\typ_{\mathit{in}}} {\typ_{\mathit{out}}}}} {\name_i = \name} \\
+        \reduceWithEnv {\insertToEnvv  {\overline {\typParam : \typ}}} {\prim {\typ_i}} = \pprim {\typ_i}}
+     { \fieldAccessEnv \ctxt \name {\spcTyp {\externTyp {\prim \name}} {\typs}} {\pprim {\typ_i}}}
+     \quad (\rn{Type:Specialized}\rAE)
+
+  \inferrule
+     { \fieldAccessEnv \ctxt \name {\spcTyp {\externTyp {\prim \name}} \ } {\pprim \typ} }
+     { \fieldAccessEnv \ctxt  \name {\externTyp {\prim \name}}  {\pprim \typ}}
+     \quad (\rn{Type:Extern}\rAE)
+
+  \inferrule
+     { }
+     { \fieldAccessEnv \ctxt \sizeMem {\arrayTyp \typ \size} {\bitWidthTyp {32}}}
+     \quad (\rn{Type:Array}\rSep\rn{Mem:Size}\rAE)
+
+  \inferrule
+     { }
+     { \fieldAccessEnv \ctxt \lastIndex {\arrayTyp \typ \size} {\bitWidthTyp {32}}}
+     \quad (\rn{Type:Array}\rSep\rn{Mem:LastIndex}\rAE)
+
+  \inferrule
+     { }
+     { \fieldAccessEnv \parserCtxt \next {\arrayTyp \typ \size} {\typ}}
+     \quad (\rn{Type:Array}\rSep\rn{Mem:Next}\rAE)
+
+  \inferrule
+     { }
+     { \fieldAccessEnv \parserCtxt \last {\arrayTyp \typ \size} {\typ}}
+     \quad (\rn{Type:Array}\rSep\rn{Mem:Last}\rAE)
+
+~ End InfRuleHelper
+
+## Ternary Rule { #sec-ternary-e }
+
+The expression $\ternary {\exp_1} {\exp_2} {\exp_3}$ is a conditional expression.
+The rule $\ternaryE$ states that $\exp_1$ must be a boolean and expressions $\exp_2$
+and $\exp_3$ must have the same type but they cannot have the $\integerTyp$ type. In
+that case it translates the conditional expression by translating all its subexpressions. 
+
+~ Begin InfRule
+
+  \inferrule
+     {\expenv {\exp_1} {\prim {\exp_1}} \boolTyp {\dir_1} \\\\
+      \expenv {\exp_2} {\prim {\exp_2}} {\typ_1} {\dir_2} \\\\
+      \expenv {\exp_3} {\prim {\exp_3}} {\typ_2} {\dir_3}\\\\
+      \typ_1 = \typ_2 \\
+      \typ_1 \neq \integerTyp}
+     {\expenv {\ternary {\exp_1} {\exp_2} {\exp_3}} {\ternary {\prim {\exp_1}} {\prim {\exp_2}} {\prim {\exp_3}}} {\typ_1} \less }
+     \quad (\ternaryE)
+
+  % \inferrule[ Ternary(AllowedInP4ButNotePetr4)]
+     % {\expenv {\exp_1} {\prim {\exp_1}} \boolTyp {\dir_1} \\
+     %  \expenv {\exp_2} {\prim {\exp_2}} {\integerTyp} {\dir_2} \\
+     %  \expenv {\exp_3} {\prim {\exp_3}} {\integerTyp} {\dir_3}\\
+     %  % \typ_1 = \typ_2 \\
+     %  % \typ_1 \eq \integerTyp \\
+     %  \compTimeKnown {\exp_1}}
+     % {\expenv {\ternary {\exp_1} {\exp_2} {\exp_3}} {\ternary {\prim {\exp_1}} {\prim {\exp_2}} {\prim {\exp_3}}} {\typ_1} \less }
+
+~ End InfRule
+
+``**Restriction**``
+Petr4 doesn't support the case where both the
+true and the false expressions have the infinite precision integer type when the
+condition can be evaluated at compilation time. However, this is allowed by P4 spec.
+
+
+## Function Call Rule { #sec-func-call }
+
+Expressions $\funcCall \exp {\typs} \args$ and
+$\funcCallNoTypArgs \exp \args$ both indicate a function call where
+
+- $\exp$ is either a name or an expression member that is being called
+- $\args$ is the arguments passed to the function and they could be matched with parameters either based on name or position
+- $\typs$ is the type arguments passed to the function.
+
+A function call is well-typed if the called expression is an accepted function call and is well-typed and the passed (type) arguments do not violate any restrictions of (type) parameters. 
+
+- The [dispatch function call arguments auxiliary judgment][#sec-func-call-helper] carries out multiple roles:
+  1. it checks if the expression as a function call is acceptable, that is, if it is either a name or expression member
+  2. it checks if the type of the expression is either a function, an action, an extern, or a specialized type
+  3. it checks if the parameters and arguments match either based on their position or name.
+
+  And has the judgment form $\resolveFuncOver \exp \args {\prim \exp} \typVars \prms \kind {\typ_\ret}$ which states that the expression $\exp$ called as a function with arguments $\args$ under environment $\env$ and context $\ctxt$, translates to the expression $\prim \exp$ in the IR and has the type parameters $\typVars$, parameters $\prms$, kind $\kind$, and the return type $\typ_\ret$.
+- $\transMaybe \typ$ translates the surface type $\typ$ to underlying types and if the surface type is $\dontcareTyp$ it assigns $\bot$ to it. ``TODO: rewrite after adding syntax.``
+- $\matchParArg \prms \args$ matches parameters $\params$ to arguments $\args$. A parameter is used when defining a function/structure. It has a type and a variable name. Additionally, it can have a direction and an optional value. On the other hand, an argument is what is actually passed to the function/structure when it is called and it can either be an expression, a key-value, or don't care. So the role of this helper function is to match the parameters to the passed arguments. If all arguments are key-values it simply matches the arguments and parameters based on their names. If the arguments are expressions or don't care, it matches them based on their positions. Thus, it returns a list of pairs of parameter names and optional expressions.
+- $\types \constraint$ returns the types assigned to the vector of type variables in the constraint $\constraint$.
+- $\validatePars \singleprm \env \kind$ validates the parameter $\singleprm$ under the environment $\env$ and the function kind $\kind$. That is, it confirms that the parameter is valid if **none** of the following cases hold:
+  + $(\sat \typ) = \externTyp \whatevs$ and $\dir \neq \less$
+  + $\compTimeKnown {\sat \typ}$ and $\dir \neq \less$
+  + $\typNotWellFormed (\sat \typ)$
+
+  And **one** of the following holds: ```TODO: this is wrong. refer to is\_valid\_param\_type. however, I prefer finding a way to avoid writing all the cases in that function.```
+  + $\kind = \parserKind$ and  $\sat \typ=\externTyp \whatevs$
+  + $\kind = \controlKind$ and  $\sat \typ=\externTyp \whatevs$
+  + $\kind = \methodKind$ and  $\sat \typ=\externTyp \whatevs$
+- The [infer type arguments auxiliary judgment][#sec-infer-type-args] infers the type of type parameters of a function call using the
+arguments passed to it and to ensure that they all match.
+It has the judgment form $\inferTypParArg {{\maybe \constraint}} {\overline {\singleprm := {\maybe \exp}}} {\prim \constraint}$ which states that under environment $\env$ and context $\ctxt$,
+the assignment of arguments $\overline {\maybe \exp}$ to parameters $prms$ is valid under the constraints $\prim \constraint$ as long as the constraints $\prim \constraint$ do not contradict the constraints $\maybe \constraint$.
+Constraints $\constraint$ are assignments of types to type variables and optional constraints $\maybe \constraint$ are assignments of optional types to type variable. Note that constraints denoted by a letter have the same fixed vector of type variables. 
+- $\castParArg { {\singleprm := \maybe \exp}}$
+  + when $\exp \neq \bot$ it assigns the cast expression $\cast \typ \exp$ (which would be an IR expression $(\prim \exp, \prim \typ, \prim \dir$) to the parameter $\param$ if one of the following holds:
+    * $\dir = \less$
+    * $\dir = \inDir$ and $\prim \typ \neq \externTyp \whatevs$
+    * ($\dir = \out$ or $\dir = \inout$) and $\! \isLval (\prim \exp, \prim \typ, \prim \dir)$ and $\prim \dir \neq \inDir$ where $\isLval (\prim \exp, \prim \typ, \prim \dir)$ checks whether its input is lvalue.
+  + When $\exp = \bot$ it assigns bottom to the parameter if  $\typ \neq \voidTyp$ and either $\dir = \out$ or parameter is optional.
+- $\callOK \ctxt \kind$ checks if the function kind is valid in a context. The following cases valid: ``TODO: break up ctxt. here ctxt is exprctxt.``
+  + $\ctxt = \parserCtxt$ and $\kind = \parserKind$
+  + $\ctxt = \applyBlockCtxt$ and $\kind = \controlKind$
+  + $\ctxt \neq \funcCtxt \whatevs$ and $\kind = \externKind$
+  + $\ctxt = \applyBlockCtxt$ and $\kind = \tableKind$
+  + $\ctxt = \applyBlockCtxt$ and $\kind = \actionKind$
+  + $\ctxt = \actionCtxt$ and $\kind = \actionKind$
+  + $\ctxt = \tableActionCtxt$ and $\kind = \actionKind$
+  + $\ctxt = \parserCtxt$ and $\kind = \funcKind$
+  + $\ctxt = \applyBlockCtxt$ and $\kind = \funcKind$
+  + $\ctxt = \actionCtxt$ and $\kind = \funcKind$
+  + $\ctxt = \funcCtxt \whatevs$ and $\kind = \funcKind$
+  + $\ctxt = \declLocalCtxt$ and $\kind = \funcKind$
+  + $\kind = \builtin$
+
+
+~ Begin InfRule
+
+  % \mprset {vskip=0.7ex}
+  % {\inferrule 
+  %    {
+  %      \resolveFuncOver \exp \args {\prim \exp} \typVars \prms \kind {\typ_\ret} \\\\
+  %      \trans {\overline {\typ_0}} \emp = \overline {\typ_1}\\
+  %      |\overline {\typ_0}| = |\typVars|\\\\
+  %      % \overline {\typVar : \typ} = \zip \typVars {\overline {\prim \typ}}\\
+  %      \matchParArg \prms \args = \overline {\singleprm = \pprim {\maybe \exp}}\\
+  %      % \inferTypParArg {\typ_\ret} {\overline {\typVar : \typ_1}} {\overline {\param = \pprim {\maybe \exp}}} {\overline {\typVar :\typ_1}} {\overline {\typVar : \typ_2}}\\\\
+  %      \inferTypParArg {\overline {\typVar : \maybe {\typ_1}}} {\overline {\singleprm = \pprim {\maybe \exp}}} {\overline {\typVar : \typ_2}}\\\\
+  %      \validatePars {\typs} {\addTypEnvv {\overline {\typVar : \typ_2}} } \kind \\
+  %      \castParArg {\overline {\prm := \pprim {\maybe \exp}}} = \overline {\param := \maybe {(\ppprim \exp, \prim \typ, \dir)}}\\\\
+  %      \callOK \ctxt \kind \\
+  %      \sat {\typ_\ret} = {\prim \typ}_{\ret} 
+  %      }
+  %    { \expenv {\funcCall \exp {\overline {\typ_0}} \args} {\funcCall {\prim \exp} {\overline { \typ_2}} {\overline{\maybe {(\ppprim \exp, \prim \typ, \dir)}}} } {{\prim \typ}_{\ret}} \less }
+  %    \quad (\funcCallE)}
+
+% \\
+
+  \mprset {vskip=0.7ex}
+  {\inferrule 
+     {
+       \resolveFuncOver \exp \args {\prim \exp} \typVars \prms \kind {\typ_\ret} \\\\
+       \transMaybe {\overline {\typ_0}} = \overline {\maybe {\typ_1}}\\
+       |\overline {\typ_0}| = |\typVars|\\\\
+       % \overline {\typVar : \typ} = \zip \typVars {\overline {\prim \typ}}\\
+       \matchParArg \prms \args = \overline {\singleprm := \pprim {\maybe \exp}}\\
+        % {\overline {\typVar : \maybe {\typ_1}}} = \constraint\\
+       \inferTypParArg {\overline {\typVar : \maybe {\typ_1}}} {\overline {\singleprm := \pprim {\maybe \exp}}} { \constraint}\\\\
+       \types \constraint = \overline {\typ_2}\\
+       \validatePars {\typs} {\unionEnv \env { \constraint} }  \kind \\
+       \castParArg {\overline {\singleprm := \pprim {\maybe \exp}}} = \overline {\param := \maybe {(\ppprim \exp, \prim \typ, \prim \dir)}}\\\\
+       \callOK \ctxt \kind \\
+       \sat {\typ_\ret} = {\prim \typ}_{\ret} 
+       }
+     { \expenv {\funcCall \exp {\overline {\typ_0}} \args} {\funcCall {\prim \exp} {\overline { \typ_2}} {\overline{\maybe {(\ppprim \exp, \prim \typ, \prim \dir)}}} } {{\prim \typ}_{\ret}} \less }
+     \quad (\funcCallE)}
+
+\\
+
+  \mprset {vskip=0.7ex}
+  {\inferrule 
+     {
+       \resolveFuncOver \exp \args {\prim \exp} \typVars \prms \kind {\typ_\ret} \\\\
+       {\prim \typ} = \dontcareTyp\\
+       | \overline {\prim \typ} | = | \typVars |\\\\
+       \expenv {\funcCall \exp {\overline {\prim \typ}} \args} {\funcCall {\prim \exp} {\overline {\ppprim \typ}} {\overline{\maybe {(\pprim \exp, \pprim \typ, \prim \dir)}}} } {{\prim \typ}_{\ret}} \less}
+     { \expenv {\funcCallNoTypArgs \exp \args} {\funcCall {\prim \exp} {\overline {\ppprim \typ}} {\overline{\maybe {(\pprim \exp, \pprim \typ, \prim \dir)}}} } {{\prim \typ}_{\ret}} \less }
+     \quad (\funcCallNoTypeArgE)}
+
+~ End InfRule
+
+### Dispatch Function Call Arguments Auxiliary Judgment { #sec-func-call-helper }
+
+```TODO: change C bottom to just C. instead, define don't care as bot. this way you can simplify optional translate and C bot```
+
+This judgment checks the details of a function call:
+
+1) it checks if the expression as a function call is acceptable, that is, if it is either a name or expression member
+2) it checks if the type of the expression is either a function, an action, an extern, or a specialized type
+3) the parameters and arguments either match based on their position or name.
+
+It has the form $\resolveFuncOver \exp \args {\prim \exp} \typVars \prms \kind {\typ_\ret} $ which states that the expression $\exp$ called as a function with arguments $\args$ under environment $\env$ and context $\ctxt$, translates to the expression $\prim \exp$ in the IR and has the type parameters $\typVars$, parameters $\prms$, kind $\kind$, and the return type $\typ_\ret$.
+
+- Remember that parameters could be optional or have some default expression set as their expression. $\removeOptionalPars \params$ removes those parameters.
+- $\concatList {\overline \anyTyp} {\overline {\prim \anyTyp}}$ denotes concatenating two lists.
+
+~ Begin InfRuleHelper
+
+  \mprset {vskip=0.5ex}
+  {\inferrule
+     % [\nameFuncNameE]
+     { \lookupEnv {\name_0} = \overline {(\typ, \dir)}\\
+        (\funcType \kind \typParams {\overline {\prm 1}} {\typ_\ret},\dir_2)\in \overline {(\typ, \dir)}}
+       % \exists (\typ,\dir) \in (\overline {\typ, \dir}). \typ = \funcType \kind \typParams {\pars 1 n} {\typ_\ret} }
+     { \resolveFuncOver {\name_0} {\overline {\var_1 = \exp}} {\name_0} \typParams {\overline {\prm 1}} \kind {\typ_\ret} }
+     \quad (\nameFuncNameE)
+  }
+
+\\
+  \mprset {vskip=0.5ex}
+  {\inferrule
+     % [\nameFuncCountE]
+     { \lookupEnv {\name_0} = \overline {(\typ, \dir)}\\
+        (\funcType \kind \typParams {\overline {\prm 1}} {\typ_\ret},\dir_2) \in \overline {(\typ, \dir)}\\
+       % \exists (\typ,\dir) \in (\overline {\typ, \dir}). \typ = \funcType \kind \typParams \params {\typ_\ret}\\
+       |\removeOptionalPars \params| = |\argexps|}
+    { \resolveFuncOver {\name_0} {\argexps} {\name_0} \typParams {\overline {\prm 1}} \kind {\typ_\ret} }
+    \quad (\nameFuncCountE)
+  }
+
+\\
+  \mprset {vskip=0.5ex}
+  {\inferrule
+     { \expenv {\name_0} \exp {\actionTyp {\overline {\prm 1} } {\overline {\prm 2}}} \dir \\
+       \overline {\prm 3} = \concatList {\overline {\prm 1}} {\overline {\prm 2}}}
+     {\resolveFuncOver {\name_0} {\args} {\name_0} \emp {\overline {\prm 3}} \actionKind \voidTyp }
+     \quad (\nameActionE)
+   }
+
+
+\\
+  \mprset {vskip=0.5ex}
+  {\inferrule
+     % [\expMemExternNameE]
+     { \expenv {\expMem {\name_0} {\exp_0}} {\exp_1} {\typ_1} {\dir_1}\\
+       \reduce {\typ_1} = \externTyp {\name_1}\\\\
+       \lookupEnv { \name_1} = (\typParams, \methods {\name_2} {\typ_2})\\\\
+        (\name_0, \funcType \kind {\overline {\prim \typParam}} {\prms} {\typ_\ret}) \in {(\methods {\name_2} {\typ_2})}
+       }
+    {\resolveFuncOver {\expMem {\name_0} {\exp_0}} \argkvs {\exp_1} {\overline {\prim \typParam}} \prms \kind {\typ_\ret}}
+    \quad (\expMemExternNameE)
+  }
+
+\\
+  \mprset {vskip=0.5ex}
+  {\inferrule
+     % [\expMemExternCountE]
+     { \expenv {\expMem {\name_0} {\exp_0}} {\exp_1} {\typ_1} {\dir_1}\\
+       \reduce {\typ_1} = \externTyp {\name_1}\\\\
+       \lookupEnv { \name_1} = (\typParams, \methods {\name_2} {\typ_2})\\\\
+        (\name_0, \funcType \kind {\overline {\prim \typParam}} {\prms} {\typ_\ret}) \in {(\methods {\name_2} {\typ_2})}\\\\
+       |\prms| = |\argexps|
+       }
+    {\resolveFuncOver {\expMem {\name_0} {\exp_0}} \argexps {\exp_1} {\overline {\prim \typParam}} \prms \kind {\typ_\ret} }
+     \quad (\expMemExternCountE)
+   }
+
+\\
+  \mprset {vskip=0.5ex}
+  {\inferrule
+     % [\expMemSpcE]
+     { \expenv {\expMem {\name_0} {\exp_0}} {\exp_1} {\typ_1} {\dir_1}\\
+       \reduce {\typ_1} = \spcTyp {\name_1} {\overline {\prim \arg}} \\\\
+       \isExtern {\name_1} \\\\
+       \resolveFuncOver {\expMem {\name_0} {\name_1}} \args {\overline {\prim \typParam}} \prms \kind {\typ_\ret} {\dir_2} \\\\
+       \reduceWithEnv {\addTypEnvv {\overline {\prim \typParam} {\prim \arg}}} {\typ_\ret} = \prim {\typ_\ret}
+     }
+    {\resolveFuncOver {\expMem {\name_0} {\exp_0}} \args {\exp_1} {\overline {\prim \typParam}} \prms \kind {\prim {\typ_\ret}} }
+     \quad (\expMemSpcE)
+   }
+
+~ End InfRuleHelper
+
+### Infer Type Arguments Auxiliary Judgment { #sec-infer-type-args }
+
+This auxiliary judgment is used to infer the type of type parameters of a function call using the
+arguments passed to it and to ensure that there are no conflicts in the inferred types.
+It has the judgment form $\inferTypParArg {\maybe \constraint} {\overline {\singleprm = {\maybe \exp}}} {\prim \constraint}$ which reads as under environment $\env$ and context $\ctxt$, the types of type parameters in the constraints $\maybe \constraint$ are inferred and returned in constraints $\prim \constraint$ given the assignment of parameters $\prms$ to optional expressions $\overline {\maybe \exp}$.
+As a reminder, constraints $\constraint$ are assignment of type parameters to types and optional constraints $\maybe \constraint$ are assignment of type parameters to optional types. The vector of type parameters in each constraint denoted by a letter is fixed. Hence, we additionally use $\optConstraint$ and $\nonoptConstraint$ to denote constraints when we have different vectors of type parameters. This means, for example, $\maybe \constraint$ and $\prim \constraint$ have the same vector of type parameters but the assignment of types to type parameters has changed.
+
+The rule $\inferTypeArgAE$ states that
+under environment $\env$ and context $\ctxt$, the types of type parameters in the constraints $\maybe \constraint$ are inferred and returned in constraints $\prim \constraint$ given the assignment of parameters $\prms$ to optional expressions $\overline {\maybe \exp}$
+if the result of the unification of the type of arguments and their parameter types (which is the assignment of type parameters to types) does not include any inconsistency. For example, one does not state that type parameter $\typVar$ is $\integerTyp$ while the other states that it is $\tupleTyps \integerTyp$.
+
+
+- $\breakMaybes {\overline {\maybe \anyTyp}} {\overline {\prim \anyTyp}} {\overline {\pprim {\maybe \anyTyp}}}$ breaks down a list of optional things (reminder: $\anyTyp$ is a metavariable of any type you want) into two lists: one that only contains values other than $\bot$ (that is, $\overline {\prim \anyTyp}$) and another that only contains the ones that are $\bot$ (that is, $\overline {\pprim {\maybe \anyTyp}}$). So in the rule $\inferTypeArgAE$, the $\maybe \optConstraint$ is the list of type parameters that do not have a type assigned to them.
+- As a reminder $\unify \env \typeEqs {{\typVars}} \typ { {\prim \typ}} {\maybe \constraint}$ unifies the types $\typ$ and $\prim \typ$ under environment $\env$, equivalent type variables $\typeEqs$ (which expanded is ${\overline {\typVar_1 = \typVar_2}}$), and type variables $\typVars$ that do not have any type assigned to them yet and returns the constraints $\maybe \constraint$ that is required for the two types to be unified.
+For detailed rules of this judgment refer to Section [#sec-type-unify].
+- $\mergeConst {\overline {\maybe \constraint}}$ merges the types assigned to type variables in the list of constraints $\overline {\maybe \constraint}$ recursively. It starts from no assignment to any of the type variables as the base and recursively folds the merge of assigned types to a type variable from the list of assignments $\overline {\maybe \constraint}$. The merging of types, that is, $\mathit{merge}(\typVar_1 : \typ_1, \typVar_1 :\typ_2)$, tries the following and if none of them matches it fails:
+  + if $\typEqEnv \emp {\typ_1} {\typ_2}$, then $\typ_1$
+  + if $\implCast {\typ_1} {\typ_2}$, then $\typ_2$
+  + if $\implCast {\typ_2} {\typ_1}$, then $\typ_1$
+- $\toVoid {\overline {\maybe \constraint}}$ assigns the $\voidTyp$ type to the type variables in constraints $\maybe \constraint$ that do not have a type assigned to them, i.e., $\bot$ is assigned to them. It leaves the type variables that have type assignments untouched.
+
+
+~ Begin InfRuleHelper
+
+  % \mprset {vskip=0.5ex}
+%   {\inferrule
+%      { \breakMaybes {\overline {\typVar_1 : \maybe {\typ_1}}} {\overline {\typVar_2 : \typ_2}} {\overline {\typVar_3 : \bot}}\\\\
+%        \expenvvv {\addTypEnvv {\overline {\typVar_2 : \typ_2}}} {\exps} {\overline {\prim \exp, \prim \typ, \prim \dir}} \\\\
+%        \unify {\addTypEnvv {\overline {\typVar_2 : \typ_2}}} \emp {\overline {\typVar_3}} \typs {\overline {\prim \typ}} {\overline {\overline {\typVar_3 : \maybe {\typ_4}}}} \\\\
+%        \mergeConst {\overline {\typVar_3 : \bot}} {\overline {\overline {\typVar_3 : \maybe {\typ_4}}}} = {\overline {\typVar_3 : \maybe {\typ_5}}}\\\\
+%        \concatList {\overline {\typVar_2 : {\typ_2}}} { \toVoid {\overline {\typVar_3 : \maybe {\typ_5}}}} = {\overline {\typVar_1 : {\typ_6}}} }
+%      {\inferTypParArg {\overline {\typVar_1 : \maybe {\typ_1}}} {\overline {\singleprm = {\maybe \exp}}}  {\overline {\typVar_1 : {\typ_6}}}}
+%      \quad (\inferTypeArgAE)
+%   }
+
+% \\
+
+  \mprset {vskip=0.5ex}
+  {\inferrule
+     { \breakMaybes {\maybe \constraint} {\nonoptConstraint} {\maybe \optConstraint}\\\\
+       \prim \env = \unionEnv \env {\nonoptConstraint}\\
+       \expenvvv {\prim \env} {\exps} {\overline {\prim \exp, \prim \typ, \prim \dir}} \\\\
+       \unify {\prim \env} \emp {\maybe \optConstraint} \typs {\overline {\prim \typ}} {\overline {\maybe {\prim \optConstraint}}} \\\\
+       \mergeConst {\overline {\maybe {\prim \optConstraint}}} = \maybe {\pprim \optConstraint}\\\\
+       \unionEnv {\nonoptConstraint} {\toVoid{\maybe {\pprim \optConstraint}}} = \prim \constraint }
+       % \concatList {\overline {\typVar_2 : {\typ_2}}} { \toVoid {\overline {\typVar_3 : \maybe {\typ_5}}}} = {\overline {\typVar_1 : {\typ_6}}} }
+     {\inferTypParArg {\maybe \constraint} {\overline {\singleprm := {\maybe \exp}}}  {\prim \constraint}}
+     \quad (\inferTypeArgAE)
+  }
+
+
+~ End InfRuleHelper
+
+## Anonymous Instantiation Rule { #sec-inst-e }
+
+- validate par arg checks if optional is some and it passes if expression is compile time known or if it is none and parameter is none.
+
+~ Begin InfRule
+
+  \inferrule
+     { \transMaybe \typs = \overline {\prim {\maybe \typ}} \\
+       |\typs| = |\typParams| \\\\
+       \resolveConstOver \name \args \typParams \wildcardParams \prms \retTyp \\\\
+       \matchParArg \prms \args = \overline {\singleprm := \pprim {\maybe \exp}}\\
+       \constraint = \concatList {\overline {\typVar : \maybe {\typ_1}}} {\overline {\wildcardParam : \bot}}\\
+       \inferTypParArg {\constraint} {\overline {\singleprm := \pprim {\maybe \exp}}} {\prim \constraint}\\\\
+       \prim \env = \unionEnv \env {\prim \constraint} \\
+       \castParArg {\overline {\singleprm := \pprim {\maybe \exp}}} = \overline {\param := \maybe {(\ppprim \exp, \prim \typ, \prim \dir)}}\\\\
+       \validateParArg {\overline {\param := \maybe {(\ppprim \exp, \prim \typ, \dir)}}}\\
+       \sat \retTyp = \prim \retTyp}
+     { \expenv {\instantiation {\spcTyp \name {\typs}} {\args}} {\instantiation {\spcTyp \name {\typs}} {\overline {\prim \arg}}} {\prim \retTyp} \less}
+  \quad (\instE\rSep\rn{1})
+
+% typename of type_nameless_instantiation
+  \inferrule
+     { \expenv {\instantiation {\spcTyp \name {\ }} {\args}} {\prim \exp} \typ \dir}
+     %name in the following is typename
+     { \expenv {\instantiation {\name} {\args}} {\prim \exp} \typ \dir }
+     \quad (\instE\rSep\rn{2})
+
+~ End InfRule
+
+~ Begin InfRuleHelper
+
+  \mprset {vskip=0.5ex}
+  {  \inferrule
+         { \lookupEnv \name = \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  \prms \retTyp, \dir) \in \overline {(\typ, \dir)} \\
+           |\removeOptionalPars \params| = |\argexps|}
+         { \resolveConstOver \name \argexps \typParams \wildcardParams \prms \retTyp  }
+         \quad (blah)
+  }
+
+~ End InfRuleHelper
+
+## Mask Rule { #sec-mask-e }
+
+The expression $\mask {\exp_1} {\exp_2}$ denotes a masking expression where every 0 bit in $\exp_2$ is turned into don't care and the rest of the bits of expressions $\exp_1$ and $\exp_2$ are conjuncted. Thus, it returns a set of expressions:
+$\mask {\exp_1} {\exp_2} = \{\exp_3 | \exp_1\ \&\ \exp_2 = \exp_3\ \&\ \exp_2 \}$. Thus, as
+stated by the rule $\maskE$ both expressions $\exp_1$ and $\exp_2$ must have the same type of $\bitWidthTyp \width$, $\intWidthTyp \width$, or $\integerTyp$. 
+
+- $\maskTypeIs {\typ_1} {\typ_2}$ is a helper function that determines the type of a
+mask expression based on the type of its two operands and it is defined for the following cases:
+  + if $\typ_1 = \typ_2 = \bitWidthTyp \width$,
+  then $\maskTypeIs {\typ_1} {\typ_2} = \bitWidthTyp \width$
+  + if $\typ_1 = \bitWidthTyp \width, \typ_2 = \integerTyp$,
+  then $\maskTypeIs {\typ_1} {\typ_2} = \integerTyp$
+  + if $\typ_1 = \integerTyp, \typ_2 =  \bitWidthTyp \width$,
+  then $\maskTypeIs {\typ_1} {\typ_2} = \bitWidthTyp \width$
+
+``**ENSURE**``
+It might seem that petr4 allows mask operation to also operate on arbitrary precision integers while P4 spec doesn't. However, note that int can be implicitly casted to bit<w>. So the mask operation can also operate on int or combination of int and bit<w>. Similarly this applies to the range operation. 
+
+~ Begin InfRule
+
+  \inferrule
+     {\expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\\\
+      \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\
+      \maskTypeIs {\typ_1} {\typ_2} = \typ}
+     {\expenv {\mask {\exp_1} {\exp_2}} {\mask {\prim \exp_1} {\prim \exp_2}} {\setTyp \typ} \less  }
+     \quad (\maskE)
+
+~ End InfRule
+
+## Range Rule { #sec-range-e }
+
+The expression $\range {\exp_1} {\exp_2}$ is a range expression and it returns the values between $\exp_1$ and $\exp_2$, inclusively. The rule $\rangeE$ states that the type of expression $\exp_1$ and $\exp_2$ must be the same and it must either be $\bitWidthTyp \width$ or $\intWidthTyp \width$ (and by extension of implicit cast of types it can also be $\integerTyp$). 
+
+- As a reminder, the $\bothInt {\typ_1} {\typ_2}$ function checks the conditions
+  $\typ_1 = \typ_2 = \bitWidthTyp \width$ or $\typ_1 = \typ_2 = \intWidthTyp \width$ or
+  $\typ_1 = \typ_2 = \integerTyp$ and if one of them holds it returns $\tr$.
+
+``**ENSURE**``
+p4 spec only states that the type can be bit<w> or int<W> but petr4 also allows integer. It's because of implicit cast, right?
+
+~ Begin InfRule
+
+  \inferrule
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\\\
+       \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\
+       \bothInt {\typ_1} {\typ_2}}
+       % \typ_1 = \typ_2 = \bitWidthTyp \width \textOr \intWidthTyp \width \textOr \integerTyp}
+     { \expenv {\range {\exp_1} {\exp_2}} {\range {\prim {\exp_1}} {\prim {\exp_2}}} {\setTyp {\typ_1}} \dir }
+     \quad (\rangeE)
+
+~ End InfRule
+
+# Statement's Typing Rules { #sec-stmt-typing }
+this judgment type checks a statement written in surface syntax, generates the IR statement from it and if applicable updates the env and ctxt.
+is_lvalue checks if an IR expression is lvalue. 
+cast_expr takes a type and surface syntax expression. after generating the IR expression by type_expression, it checks if the given type and type of IR expression are equal it just returns the IR exp o.w. it casts (if possible) the IR expression to the given type.
+if void type  returns a void type if a (or two) type is (are) void and otherwise returns a unit type.
+get enum typ takes a type and checks if it's an enum. if so it returns the enums of it. 
+
+~ Begin InfRule
+
+  \inferrule
+     { \expenv {\exp_1} {\prim {\exp_1}} {\typ_1} {\dir_1} \\
+       \isLval {{\prim {\exp_1}}, {\typ_1}, {\dir_1}} \\ 
+       ({\prim {\exp_2}}, {\typ_2}, {\dir_2}) = \castExpression {\typ_1} {\exp_2}\\
+       % \expenv {\exp_2} {\prim {\exp_2}} {\typ_2} {\dir_2} \\
+       % \typ_1 = \typ_2 \\
+       }
+     { \stmtenv {\assign {\exp_1} {\exp_2}} {\assign {\prim {\exp_1}} {\prim {\exp_2}}} {\unitTyp} }
+     \quad (\assignmentS)
+
+
+  \inferrule
+     { }
+     { \stmtenv {\noop} {\noop} {\unitTyp}}
+     \quad (\emptyS)
+
+  \inferrule
+     { \stmtenvv 1 {\stmt_1} {\prim {\stmt_1}} {\typ_1} 2 \\
+       \prim \typ = \ifVoidTyp {\typ_1} \\
+       \stmtenvv 2 {\stmts} {\prim \stmts} {\prim \typ} 3 }
+     { \stmtenvv 1 {\block {\stmt_1; \stmts} } {\block {\prim {\stmt_1}; {\prim \stmts}} } {\prim \typ} 3 }
+     \quad (\blockS)
+
+  \inferrule
+     {
+     % \expenv \exp {\prim \exp} \typ \dir \\
+       \ctxt = \applyBlockCtxt \textOr \actionCtxt \\
+       ({\prim {\exp}}, {\typ}, {\dir}) = \castExpression {\voidTyp} {\exp}\\
+       }
+     { \stmtenv {\return \exp} {\return {({\prim {\exp}}, {\typ}, {\dir})}} \voidTyp  }
+     \quad (\returnS)
+
+  \inferrule
+     {
+     % \expenv \exp {\prim \exp} \typ \dir \\
+       \ctxt = \applyBlockCtxt \textOr \actionCtxt \textOr \funcCtxt \typ \\
+       }
+     { \stmtenv {\return {}} {\return {}} \voidTyp  }
+     \quad (\returnEmpS)
+
+  \inferrule
+     {
+     % \expenv \exp {\prim \exp} \typ \dir \\
+       \ctxt = \funcCtxt \typ \\
+       ({\prim {\exp}}, {\prim \typ}, {\dir}) = \castExpression {\typ} {\exp}\\
+       }
+     { \stmtenv {\return \exp} {\return {({\prim {\exp}}, {\prim \typ}, {\dir})}} \voidTyp  }
+     \quad (\returnFuncS)
+
+  \inferrule
+     { \ctxt \neq \parserCtxt }
+     { \stmtenv \exit \exit \voidTyp}
+     \quad (\exitS)
+
+  \inferrule
+     { \ctxt \neq \parserCtxt \\
+       (\prim \exp, \boolTyp, \dir) = \castExpression \boolTyp \exp \\
+       \stmtenvv 1 {\stmt_1} {\prim {\stmt_1}} {\typ_1} 2 }
+     { \stmtenvv 1 {\ifthen \exp {\stmt}} {\ifthen {\prim \exp} {\prim \stmt} } {\unitTyp} 1 }
+     \quad (\ifthenS)
+
+  \inferrule
+     { \ctxt \neq \parserCtxt \\
+       (\prim \exp, \boolTyp, \dir) = \castExpression \boolTyp \exp \\
+       \stmtenvv 1 {\stmt_1} {\prim {\stmt_1}} {\typ_1} 2 \\
+       \stmtenvv 1 {\stmt_2} {\prim {\stmt_2}} {\typ_2} 3 \\
+       \prim \typ = \ifVoidTyp {\typ_1, \typ_2}}
+     { \stmtenvv 1 {\ifthenelse \exp {\stmt_1} {\stmt_2}} {\ifthenelse {\prim \exp} {\prim {\stmt_1}} {\prim {\stmt_2}} } {\prim \typ} 1 }
+     \quad (\ifthenelseS)
+
+  \inferrule
+     { \ctxt_0 = \applyBlockCtxt \\
+       \expenvv \exp {\prim \exp} \typ \dir 0 \\
+       \prim \typ = \reduce \typ \\
+       \name_1, \ldots, \name_m = \getEnum {\prim \typ} \\
+       \lbl \notin \overline \lbl \\
+       \lbl \in \{\name_1, \ldots, \name_m \}\\
+       \stmtenvv 0 {\block {\stmts}} {\block {\prim {\stmts}}} {\typ_0} 1 \\
+       \stmtenvv 1 {\switch \exp {\overline {\actionCase \stmt}}} {\switch {\prim \exp} {\overline {\actionCase {\pprim \stmt} }}} \unitTyp 2
+       }
+     { \stmtenvv 0 {\switch \exp {\actionCase \stmts, \overline {\actionCase \stmt}} } {\switch {\prim \exp} {\actionCase {\prim \stmts}, {\overline {\actionCase {\pprim \stmt} }} } } \unitTyp 2 }
+     \quad (\switchS)
+
+  \inferrule
+     { \isConstant \dcl \textOr \isInstantiation \dcl \textOr \isVariable \dcl \\
+       \dclenvv 0 \dcl {\prim \dcl} 1}
+     { \stmtenvv 0 \dcl {\prim \dcl} \unitTyp 1 }
+     \quad (\declS)
+
+~ End InfRule
+
+
+# Declaration's Typing Rules { #sec-decl-typing }
+is allowed type for variable checks if a type is allowed for declaring a variable. it includes all types after saturation except for string, integer, list, set, void, specialized type, package, control, parser, extern, function, action, constructor, and table.
+check parameter shadowing takes two lists of parameters and checks if there is any duplicate in them. 
+
+~ Begin InfRule
+
+  \inferrule
+     { \prim \typ = \trans \typ \emp \\
+       (\prim \exp, \pprim \typ, \dir) = \castExpression \exp {\prim \typ}\\
+       \val = \compileTimeEval {\prim \exp} }
+     { \dclenvvv {\constDcl \typ \var \exp} {\constDcl {\prim \typ} \var \val} {\addConstEnv \var \val} {\addTypeEnv \var {(\prim \typ, \less)}}}
+     \quad (\constantD)
+
+  \inferrule
+     { \expenv {\instantiation {\var} \args} {\instantiation {\var} {\prim \args}} {\prim \typ} \dir \\
+       \ctxt \neq \toplevel \textOr \ctxt = \toplevel, ({\prim \typ} \neq \controlTyp {\_} {\_} \textOr \parserTyp {\_} {\_} )}
+     { \dclenvvv {\inst \typVar \args \var {\ } } {\inst \typVar \args \var {\ }} \constEnv {\addTypeEnv \var {(\prim \typ, \less)}} }
+     \quad (\instantD)
+
+  \inferrule
+    {}
+    {blah}
+    \quad (\parserD)
+     % { \checkParamShadow param constructorparam \\
+     %   }
+     % { \dclenvvv {} {} {} {} }
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\controlD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\funcD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\actionD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\externFuncD)
+
+  \inferrule
+     { \ctxt \neq \toplevel \\
+       \prim \typ = \trans \typ \emp \\
+       \allowedTypeForVar {\prim \typ} \\
+       \typWellFormed {\prim \typ}}
+     { \dclenvvv {\varDcl \typ \var } {\varDcl {\prim \typ} \var} \constEnv {\addTypeEnv \var {(\prim \typ, \inout)}} }
+     \quad (\varD)
+
+  \inferrule
+     { \ctxt \neq \toplevel \\
+       \prim \typ = \trans \typ \emp \\
+       \allowedTypeForVar {\prim \typ} \\
+       \typWellFormed {\prim \typ} \\
+       (\prim \exp, \prim \typ, \dir) = \castExpression  {\prim \typ} \exp}
+     { \dclenvvv {\varDclInit \typ \var \exp} {\varDclInit {\prim \typ} \var {(\prim \exp, \prim \typ, \dir)}} \constEnv {\addTypeEnv \var {(\prim \typ, \inout)}} }
+     \quad (\varInitD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\valueSetD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\tableD)
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\headerD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\headerUnionD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\structD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\errD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\matchkindD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\enumD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\serEnumD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\externObjD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\typDefD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\newtypeD)
+
+~ End InfRule
+
+~ Begin InfRule
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\controlTypD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\parserTypD)
+
+  \inferrule
+     { blah }
+     { blah }
+     \quad (\packageTypD)
+
+  % \inferrule[ ]
+  %    {  }
+  %    {  }
+
+  % \inferrule[]
+  %    {  }
+  %    {  }
+
+  % \inferrule[]
+  %    {  }
+  %    {  }
+
+  % \inferrule[]
+  %    {  }
+  %    {  }
+
+  % \inferrule[]
+  %    {  }
+  %    {  }
+
+  % \inferrule[]
+  %    {  }
+  %    {  }
+
+  % \inferrule[]
+  %    {  }
+  %    {  }
+
+~ End InfRule
+
+# References    { #sec-references }
+
+~ Bibliography { caption:"00" }
+~~Bibitem {#harper-types-PL}
+Robert Harper.
+Types and Programming Languages.
+<http://www.cs.cmu.edu/~rwh/courses/typesys/>
+~~
+~~Bibitem {#wiki-type-sys}
+Type System.
+<https://en.wikipedia.org/wiki/Type_system>
+~~
+~
+
+# Appendix: Programming Languages Terminology { #sec-terminology; @h1:"A" }
+
+It is important that the reader is familiar with the basic programming languages terminology. And more importantly, it is crucial for them to understand the reason for having a type system and what its role is. To this end, we introduce the main programming languages terminology used in this document.
+
+**First, what is a type?**
+You can simply think of types as a set of language elements that share some features.
+For example, the type natural number is the set of numbers that is either zero or an increment of zero for multiple repetitions.
+Grouping language elements into a set (called type) abstracts out some unnecessary details when reasoning about programs.
+That is why Harper states: "The central organizing principle of language design is the identification of language features with types."[@harper-types-PL]
+``TODO: add an example here of what a type looks like.``
+
+**Second, what is a type system?**
+A _type system_ is a collection of rules that assign a property called type to the various language constructs, such as variables, functions, expressions, etc.[@wiki-type-sys]
+Thus, a type system can be used as a simple reasoning tool for programs of a language.
+A type system formally defines many aspects of a programming language.
+Most importantly, it states which programs are allowed in the language, also known as a _well-typed_ program and if possible it assigns a type to such a program. Alternatively, you can think of a type system as a system that ensures the absence of certain group of errors in well-typed programs.
+
+**Third, what is surface syntax and intermediate representation (IR)?**
+The _surface syntax_ is the syntax used to write the source program by the developer
+which eventually will be passed to the compiler. 
+The compiler does multiple _passes_ between different representations to add or omit
+information that it may or may not need. Each of these representations is called an
+_intermediate representation_. 
+
+``this paragraph is disconnected from the rest.``
+Additionally, it is important for the reader to be able to read and understand typing
+rules which in essence are _inference rules_. Thus, we introduce inference rules by
+building a toy language gradually
+and providing its various typing rules at each step (Section [#sec-guide]).
+
+## A Developer's Guide to Reading Inference Rules { #sec-guide }
+
+- ``maybe highlight the new feature and rule as you're adding them``
+- ``say and show name can also be on the side of the rule.``
+- ``state your type system changes based on your need``
+- ``have explanation on inductive relation, grammar, and judgment``
+- ``what we're basically doing is writing function/relation. it's a mathematical format for historical reasons we write it this way.``
+- ``do not do build up``
+- ``have type checking with pseudo-language and show boilerplate and see how ugly. then massage it into inference rules and appeal to people's conciseness``
+- ``sigma v to t is total but the env itself is partial``
+- ``idea on some organization:``
+  + grammars are inductively defined. a complier/rewriter can be inductively defined.
+  + these are a bunch of relation/function. eg: exp to type. then add env. well-formedness is also a function but it has a different judgment.
+  + the totality of it. the set of well-typed terms is everything you can build with these rules. you can have a set.
+  + start at the bottom to show something type checks. 
+
+A type system is made up of typing _rules_. A typing rule has a specific _judgment form_ (which is the format it is written in and guides the reader on how to read all the typing rules using the judgment).
+A typing rule, in essence, is an _inference rule_.
+An inference rule contains zero or more _premises_ above the line
+and one _conclusion_ below the line
+with the name of the rule on top or next to the line.
+For example, the rule $\ruleName$ below reads as
+$C$ is concluded if premises $A$ and $B$ hold.
+
+~ Begin InfRule
+  \inferrule[\ruleName]
+    {A \\ B}
+    {C}
+~ End InfRule
+
+A rule without any premises is called an _axiom_ and it states that
+the conclusion holds unconditionally.
+
+Consider the simple toy expression language below that only consists of integers for now. Note
+that $i$ is a _metavariable_ that represents any possible integer values. 
+
+~ Begin P4Grammar
+i := (any integer) 
+e := i
+~ End P4Grammar
+
+We can have different typing systems for a language. For example, for our toy language we present two type systems.
+The first one has the judgment form $e$ which states that the expression $e$ is well-typed.
+For example, the rule $\rn{Integer1}\rE$ states that the expression $i$ is well-typed. Note that it does not 
+state what its type is. 
+
+~ Begin InfRule
+  \inferrule[\rn{Integer1}\rE]
+     {\ \ \ \ }
+     {i}
+~ End InfRule
+
+We can have a more detailed type system for our language.
+The second type system has the judgment form $e:t$ which states that the expression $e$
+is well-typed and it has the type $t$. Note that $t$ is a metavariable for all possible types of expressions. 
+The rule $\rn{Integer2}\rE$ states that the
+expression $i$ is well-typed and it has the type $\mathsf{int}$.
+
+~ Begin InfRule
+  \inferrule[\rn{Integer2}\rE]
+     { }
+     {i:\mathsf{int}}
+~ End InfRule
+
+We now extend our toy language by adding variable reference to expression which are
+simply strings. 
+
+~ Begin P4Grammar
+i := (any integer) 
+v := (any string)
+e := i
+   | v
+~ End P4Grammar
+
+``explain expression vs statement``
+``explain sigma: v to e is the type signature of env and say how to read it``
+
+Now our type systems have to include an environment.
+The environment $\Sigma$ is needed to keep track of variables that have been declared and assigned a value/expression. The environment is a mapping of variables to a feature about the variable. This feature can be the type of the variable, the expression it has been assigned, or the value resulting from evaluating the expression it has been assigned.
+
+Here, we consider the environment to be a mapping of variables to their assigned expressions, that is, $\Sigma : v \rightarrow e$. Note that assigning expressions to variables is done in statements and not expressions and that is where the environment is built up. We only focus on expression's typing here.
+
+``differentiate between the value of v which is a string and what it holds which is an expression and then it has the type int.``
+
+The judgment form of our first type systems changes to $\Sigma \vdash e$ which states that under the environment $\Sigma$, the expression $e$ is well-typed.
+The rule $\rn{Integer1}\rE$ states that under environment $\Sigma$, the expression $i$ is well-typed.
+The typing system is also extended by a rule for variable reference.
+The rule $\rn{Variable1}\rE$ states that under environment $\Sigma$, the expression $v$ is
+well-typed if it exists in the environment. Note that $\Sigma(v)$ looks up variable $v$ from the environment $\Sigma$ and returns the expression assigned to it but since the rule does not need to do anything with that expression we use \_ to denote that the variable $v$ exists in the environment $\Sigma$ but we don't care about its assignee expression.
+Note that in rule $\rn{Integer1}\rE$ we do not need to check the type of $i$ since $i$ only stands for integers and can only be constructed by integer values.
+
+~ Begin InfRule
+  \inferrule[\rn{Integer1}\rE]
+     { }
+     {\Sigma \vdash i}
+
+  \inferrule[\rn{Variable1}\rE]
+     {\Sigma(v)=\_}
+     {\Sigma \vdash v}
+~ End InfRule
+
+The judgment form of our second type system also changes to $\Sigma \vdash e:t$ which states that under the environment $\Sigma$, the expression $e$ has the type $t$.
+The rule $\rn{Integer2}\rE$ states that under environment $\Sigma$, the expression $i$ has the type $\mathsf{int}$.
+The rule $\rn{Variable2}\rE$ states that under environment $\Sigma$, the expression $v$ has the type $\mathsf{int}$ if it exists in the environment $\Sigma$.
+
+~ Begin InfRule
+  \inferrule[\rn{Integer2}\rE]
+     { }
+     {\Sigma \vdash i:\mathsf{int}}
+
+  \inferrule[\rn{Variable2}\rE]
+     {\Sigma(v)=\_}
+     {\Sigma \vdash v:\mathsf{int}}
+~ End InfRule
+
+Now we add booleans to our language.
+
+~ Begin P4Grammar
+i := (any integer)
+v := (any string)
+b := (any boolean)
+e := i
+   | v
+   | b
+~ End P4Grammar
+
+The $\rn{Integer1}\rE$ and $\rn{Variable1}\rE$ rules do not change.
+The rule $\rn{Boolean1}\rE$ states that under environment $\Sigma$, the expression $b$ is
+well-typed.
+
+~ Begin InfRule
+  \inferrule[\rn{Integer1}\rE]
+     { }
+     {\Sigma \vdash i}
+
+  \inferrule[\rn{Variable1}\rE]
+     {\Sigma(v)=\_}
+     {\Sigma \vdash v}
+
+\inferrule[\rn{Boolean1}\rE]
+     {\ \ \ \ }
+     {\Sigma \vdash b}
+~ End InfRule
+
+The $\rn{Integer2}\rE$ stays the same. However, the type of the expression assigned to
+a variable now matters. This is stated in the $\rn{Variable2}\rE$. It particularly states that under the environment $\Sigma$, the expression $v$ has the type $t$ if the type of the expression $e$ assigned to the variable $v$ is $t$. Note that in this rule, we can no longer ignore the expression assigned to variable $v$ which is returned by looking $v$ up in the environment since we need to know its type. 
+The $\rn{Boolean2}\rE$ simply states that under the environment $\Sigma$, the expression $b$ has the type $\mathsf{bool}$.
+
+~ Begin InfRule
+  \inferrule[\rn{Integer2}\rE]
+     { }
+     {\Sigma \vdash i:\mathsf{int}}
+
+  \inferrule[\rn{Variable2}\rE]
+     {\Sigma(v)=e \\
+      \Sigma \vdash e:t}
+     {\Sigma \vdash v:t}
+
+  \inferrule[\rn{Boolean2}\rE]
+     { }
+     {\Sigma \vdash b:\mathsf{bool}}
+~ End InfRule
+
+Now we extend our language by adding the integer addition operation.
+
+~ Begin P4Grammar
+i := (any integer)
+v := (any string)
+b := (any boolean)
+e := i
+   | v
+   | b
+   | e + e
+~ End P4Grammar
+
+The first type system (that consists of rules $\rn{Integer1}\rE$, $\rn{Variable1}\rE$, and $\rn{Boolean1}\rE$ is no longer sufficient because the addition operator requires both operands not only to be well-typed but also to be an integer.
+
+The typing rules of the second type system stay the same.
+The rule $\rn{Addition2}\rE$ states that under the environment $\Sigma$, the expression
+$e_1 + e_2$ has the type $\mathsf{int}$ if both expressions $e_1$ and $e_2$ have the type $\mathsf{int}$. 
+
+~ Begin InfRule
+  \inferrule[\rn{Integer2}\rE]
+     { }
+     {\Sigma \vdash i:\mathsf{int}}
+
+  \inferrule[\rn{Variable2}\rE]
+     {\Sigma(v)=e\\
+     \Sigma \vdash e:t}
+     {\Sigma \vdash v:t}
+
+  \inferrule[\rn{Boolean2}\rE]
+     { }
+     {\Sigma \vdash b:\mathsf{bool}}
+
+  \inferrule[\rn{Addition2}\rE]
+     {\Sigma \vdash e_1:\mathsf{int} \\
+      \Sigma \vdash e_2:\mathsf{int} }
+     {\Sigma \vdash e_1 + e_2 : \mathsf{int}}
+~ End InfRule
+
+We could have restrictions on the types of subexpression. For example, assume we extend
+our toy language with equality checking which checks the equality of two subexpressions of the same type. 
+
+~ Begin P4Grammar
+i := (any integer)
+v := (any string)
+b := (any boolean)
+e := i
+   | v
+   | b
+   | e + e
+   | e == e
+~ End P4Grammar
+
+The $\rn{Equality2}\rE$ rule states that under the environment $\Sigma$, the expression
+$e_1 == e_2$ has the $\mathsf{bool}$ type if expressions $e_1$ and $e_2$ both have the same type. 
+
+~ Begin InfRule
+  \inferrule[\rn{Integer2}\rE]
+     { }
+     {\Sigma \vdash i:\mathsf{int}}
+
+  \inferrule[\rn{Variable2}\rE]
+     {\Sigma(v)=e\\
+     \Sigma \vdash e:t}
+     {\Sigma \vdash v:t}
+
+  \inferrule[\rn{Boolean2}\rE]
+     { }
+     {\Sigma \vdash b:\mathsf{bool}}
+
+  \inferrule[\rn{Addition2}\rE]
+     {\Sigma \vdash e_1:\mathsf{int} \\
+      \Sigma \vdash e_2:\mathsf{int} }
+     {\Sigma \vdash e_1 + e_2 : \mathsf{int}}
+
+  \inferrule[\rn{Equality2}\rE]
+     {\Sigma \vdash e_1:t_1 \\
+      \Sigma \vdash e_2:t_2 \\
+      t_1 = t_2}
+     {\Sigma \vdash e_1 == e_2 : \mathsf{bool}}
+~ End InfRule
+
+An inference rule is not only used for specifying types of programs. In fact, inference
+rules are used to write translation of programs from one representation to another,
+program synthesis, type inference, program semantics, etc.
+For example, the rules below rewrite expressions in our toy language (which uses infix ordering of operators) to one that uses prefix ordering of operators
+and they have the judgment form $\Sigma \vdash e \rightarrow \prim e$ which states that under the environment $\Sigma$, the expression $e$ written in the infix ordering translates to expression $\prim e$ written in the prefix ordering.
+
+The rules $\rn{Integer3}\rE$, $\rn{Variable3}\rE$, and $\rn{Boolean3}\rE$ are rather simple. For example, the $\rn{Integer3}\rE$ rule states that under the environment $\Sigma$, the expression $i$ translates to $i$.
+The rules $\rn{Addition3}\rE$ and $\rn{Equality3}\rE$ recursively translate their subexpressions and reorder their operators.
+For example, the $\rn{Addition3}\rE$ rule states that the expression $e_1 + e_2$ translates to the expression $+ \ \prim {e_1} \ \prim {e_2}$ where expressions $\prim {e_1}$ and $\prim {e_2}$ are the translations of expressions $e_1$ and $e_2$, respectively. 
+
+~ Begin InfRule
+  \inferrule[\rn{Integer3}\rE]
+     { }
+     {\Sigma \vdash i \rightarrow i}
+
+  \inferrule[\rn{Variable3}\rE]
+     {\Sigma(v)=\_}
+     {\Sigma \vdash v \rightarrow v}
+
+  \inferrule[\rn{Boolean3}\rE]
+     { }
+     {\Sigma \vdash b \rightarrow b}
+
+  \inferrule[\rn{Addition3}\rE]
+     {\Sigma \vdash e_1 \rightarrow \prim {e_1} \\
+      \Sigma \vdash e_2 \rightarrow \prim {e_2}}
+     {\Sigma \vdash e_1 + e_2 \rightarrow \ + \ \prim {e_1} \ \prim {e_2}}
+
+  \inferrule[\rn{Equality3}\rE]
+     {\Sigma \vdash e_1 \rightarrow \prim {e_1}\\
+      \Sigma \vdash e_2 \rightarrow \prim {e_2} }
+     {\Sigma \vdash e_1 == e_2 \rightarrow \ == \prim {e_1} \ \prim {e_2}}
+~ End InfRule
+
+``phrase the following paragraph and its point differently: the main point is that inference rules define inductively defined relation. these relations can be simple or complicated. E.g., so far we have had simple ones but below we have more complicated ones. also use wiggly arrow and use colon for type, that is, i wiggly arrow i colon int``
+An inference rule can conduct multiple tasks at the same time. In other words, an inference rule can be a combination of two inference rules. For example, the typing rules below combine the typing and rewriting rules shown above and they have the judgment form
+$\Sigma \vdash e \rightarrow \prim e, t$ which states that under the environment $\Sigma$, the expression $e$ written in the infix ordering translates to the expression $\prim e$ written in the prefix ordering and has the type $t$. 
+As an example , the $\rn{Variable4}\rE$ rule reads as under the environment $\Sigma$, the expression $v$ translates to itself and has the type $t$ if the variable $v$ exists in environment $\Sigma$ and expression $e$ is assigned to it which has the type $t$. 
+
+~ Begin InfRule
+  \inferrule[\rn{Integer4}\rE]
+     { }
+     {\Sigma \vdash i \rightarrow i, \mathsf{int}}
+
+  \inferrule[\rn{Variable4}\rE]
+     {\Sigma(v)=e\\
+     \Sigma \vdash e \rightarrow \_, t}
+     {\Sigma \vdash v \rightarrow v, t}
+
+  \inferrule[\rn{Boolean4}\rE]
+     { }
+     {\Sigma \vdash b \rightarrow b, \mathsf{bool}}
+
+  \inferrule[\rn{Addition4}\rE]
+     {\Sigma \vdash e_1 \rightarrow \prim {e_1}, \mathsf{int} \\
+      \Sigma \vdash e_2 \rightarrow \prim {e_2}, \mathsf{int} }
+     {\Sigma \vdash e_1 + e_2 \rightarrow + \ \prim {e_1} \ \prim {e_2}, \mathsf{int}}
+
+  \inferrule[\rn{Equality4}\rE]
+     {\Sigma \vdash e_1 \rightarrow \prim {e_1}, t_1 \\
+      \Sigma \vdash e_2 \rightarrow \prim {e_2}, t_2 \\
+      t_1 = t_2}
+     {\Sigma \vdash e_1 == e_2 \rightarrow \ == \ \prim {e_1} \ \prim {e_2}, \mathsf{bool}}
+~ End InfRule
+
+# Appendix: Petr4 { #sec-petr4 }
+
+## Petr4's Architecture { #sec-arch }
+
+Figure [#fig-arch] depicts part of Petr4's architecture that contains the type system.
+After lexing and parsing a P4 program we get a program in our surface syntax. This
+program is then passed through the _elaborator_ where type variables are introduced
+instead of underscore and new type variable names are generated for variables with the
+same name but in different scopes. This document does not discuss the inner-workings of
+`elaborate`. Then, the program is passed through the type system (encoded in `checker`).
+This document discusses the inner-working of the type system extensively. Finally, the
+program is evaluated.
+
+~ Figure { #fig-arch; caption: "Part of Petr4's architecture." }
+![arch]
+~
+[arch]: figs/petr4/arch.png { width: 100%; page-align: forcehere }
+
+
+## Petr4's Type System { #sec-petr4-type-sys }
+
+The type system conducts three tasks simultaneously:
+
+1. It type checks P4 programs.
+2. It conducts type inference.
+3. It does a pass from the surface syntax to the first IR.
+
+```**TODO** maybe have more explanation on IR.```
+
+## Connecting Formalization to Petr4's Implementation { #sec-conn }
+
+The following locates each data type in the implementation
+(<https://github.com/verified-network-toolchain/petr4>):
+
+- The surface AST is _types.program_
+- The type of programs of the surface syntax is _types.type.t_
+- The first IR is _prog.program_
+- The type of the first IR is _prog.type.t_
+- The type system is implemented in _checker.ml_ file. 
+
+For simplicity, we have removed the information that is needed to report when an error
+happens. Such information is passed around in the surface syntax as a field (called
+`tags`) of record for all data types.
 
-% is_well_formed_type
-\end{mathpar}
-~~
-~
 
diff --git a/docs/petr4spec/figs/actions.png b/docs/petr4spec/figs/actions.png
deleted file mode 100644
index 7404a6cb0..000000000
Binary files a/docs/petr4spec/figs/actions.png and /dev/null differ
diff --git a/docs/petr4spec/figs/compileeval.png b/docs/petr4spec/figs/compileeval.png
deleted file mode 100644
index c0d5ad6cd..000000000
Binary files a/docs/petr4spec/figs/compileeval.png and /dev/null differ
diff --git a/docs/petr4spec/figs/evalmultiple.png b/docs/petr4spec/figs/evalmultiple.png
deleted file mode 100644
index 15f7185ad..000000000
Binary files a/docs/petr4spec/figs/evalmultiple.png and /dev/null differ
diff --git a/docs/petr4spec/figs/headerstack.png b/docs/petr4spec/figs/headerstack.png
deleted file mode 100644
index 6cbb1cbe4..000000000
Binary files a/docs/petr4spec/figs/headerstack.png and /dev/null differ
diff --git a/docs/petr4spec/figs/maudataflow.png b/docs/petr4spec/figs/maudataflow.png
deleted file mode 100644
index e8c124394..000000000
Binary files a/docs/petr4spec/figs/maudataflow.png and /dev/null differ
diff --git a/docs/petr4spec/figs/p4checksum.png b/docs/petr4spec/figs/p4checksum.png
deleted file mode 100644
index 8dcb197c4..000000000
Binary files a/docs/petr4spec/figs/p4checksum.png and /dev/null differ
diff --git a/docs/petr4spec/figs/p4interface.png b/docs/petr4spec/figs/p4interface.png
deleted file mode 100644
index af10a5a19..000000000
Binary files a/docs/petr4spec/figs/p4interface.png and /dev/null differ
diff --git a/docs/petr4spec/figs/p4prg.png b/docs/petr4spec/figs/p4prg.png
deleted file mode 100644
index 5032bb615..000000000
Binary files a/docs/petr4spec/figs/p4prg.png and /dev/null differ
diff --git a/docs/petr4spec/figs/p4transition.png b/docs/petr4spec/figs/p4transition.png
deleted file mode 100644
index 2270fe9c8..000000000
Binary files a/docs/petr4spec/figs/p4transition.png and /dev/null differ
diff --git a/docs/petr4spec/figs/packetfilter.png b/docs/petr4spec/figs/packetfilter.png
deleted file mode 100644
index abcdc65bf..000000000
Binary files a/docs/petr4spec/figs/packetfilter.png and /dev/null differ
diff --git a/docs/petr4spec/figs/parserstatemachine.png b/docs/petr4spec/figs/parserstatemachine.png
deleted file mode 100644
index bb5096e4c..000000000
Binary files a/docs/petr4spec/figs/parserstatemachine.png and /dev/null differ
diff --git a/docs/petr4spec/figs/prgswitch.png b/docs/petr4spec/figs/prgswitch.png
deleted file mode 100644
index 978d11b98..000000000
Binary files a/docs/petr4spec/figs/prgswitch.png and /dev/null differ
diff --git a/docs/petr4spec/figs/subparser.png b/docs/petr4spec/figs/subparser.png
deleted file mode 100644
index 6787874cc..000000000
Binary files a/docs/petr4spec/figs/subparser.png and /dev/null differ
diff --git a/docs/petr4spec/figs/switcharch.png b/docs/petr4spec/figs/switcharch.png
deleted file mode 100644
index c3de121ea..000000000
Binary files a/docs/petr4spec/figs/switcharch.png and /dev/null differ
diff --git a/docs/petr4spec/figs/vssarch.png b/docs/petr4spec/figs/vssarch.png
deleted file mode 100644
index 2ce0622e2..000000000
Binary files a/docs/petr4spec/figs/vssarch.png and /dev/null differ
diff --git a/docs/petr4spec/figs/vssmau.png b/docs/petr4spec/figs/vssmau.png
deleted file mode 100644
index 24249449e..000000000
Binary files a/docs/petr4spec/figs/vssmau.png and /dev/null differ
diff --git a/docs/petr4spec/make.bat b/docs/petr4spec/make.bat
index 6bbdd63d5..e04fcfcc9 100644
--- a/docs/petr4spec/make.bat
+++ b/docs/petr4spec/make.bat
@@ -1 +1 @@
-madoko --pdf -vv --png --odir=build Petr4-spec.mdk
+madoko --pdf -vv  --odir=build Petr4-spec.mdk
diff --git a/docs/petr4spec/ops.tex b/docs/petr4spec/ops.tex
index 7b825ef06..6dbcf3a14 100644
--- a/docs/petr4spec/ops.tex
+++ b/docs/petr4spec/ops.tex
@@ -1,4 +1,140 @@
+\newcommand{\VVal}[1]{#1'}
+\newcommand{\VVVal}[1]{#1''}
+
+
+%rule names:
+\newcommand{\rn}[1]{\TirName{#1}}
+\newcommand{\rSep}{\rn{-}}
+\newcommand*{\rE}{\rSep\rn{E}}
+\newcommand*{\rAE}{\rSep\rn{AE}}
+\newcommand*{\rT}{\rSep\rn{T}}
+\newcommand*{\rS}{\rSep\rn{S}}
+\newcommand*{\rAS}{\rSep\rn{AS}}
+\newcommand*{\rD}{\rSep\rn{D}}
+\newcommand*{\rAD}{\rSep\rn{AD}}
+
+\newcommand*{\ruleName}{\rn{RuleName}}
+\newcommand*{\ruleNameE}{\ruleName\rE}
+\newcommand*{\ruleNameAE}{\ruleName\rAE}
+\newcommand*{\ruleNameT}{\ruleName\rT}
+\newcommand*{\ruleNameS}{\ruleName\rS}
+\newcommand*{\ruleNameD}{\ruleName\rD}
+
+\newcommand*{\boolT}{\rn{Bool}\rT}
+\newcommand*{\stringT}{\rn{String}\rT}
+\newcommand*{\intT}{\rn{(InfinitPrecision)Integer}\rT}
+\newcommand*{\varbitT}{\rn{Varbit}\rT}
+\newcommand*{\errT}{\rn{Error}\rT}
+\newcommand*{\voidT}{\rn{Void}\rT}
+\newcommand*{\matchKindT}{\rn{MatchKind}\rT}
+\newcommand*{\enumOneT}{\rn{Enum}\rT}
+\newcommand*{\intWidthT}{\rn{SignedInt}\rT}
+\newcommand*{\bitWidthT}{\rn{BitString(UnsignedInteger)}\rT}
+\newcommand*{\arrayT}{\rn{Array}\rT}
+\newcommand*{\tupleT}{\rn{Tuple}\rT}
+\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}
+\newcommand*{\packageT}{\rn{Package}\rT}
+\newcommand*{\controlT}{\rn{Control}\rT}
+\newcommand*{\parserT}{\rn{Parser}\rT}
+\newcommand*{\externT}{\rn{Extern}\rT}
+\newcommand*{\functionT}{\rn{Function}\rT}
+\newcommand*{\actionT}{\rn{Action}\rT}
+\newcommand*{\constructorT}{\rn{Constructor}\rT}
+\newcommand*{\tableT}{\rn{Table}\rT}
+\newcommand*{\typeNameT}{\rn{Reference}\rT}
+
+\newcommand*{\boolE}{\rn{Bool}\rE}
+\newcommand*{\stringE}{\rn{String}\rE}
+\newcommand*{\integerE}{\rn{Integer}\rE}
+\newcommand*{\bitStringE}{\rn{FixedLengthInt}\rE}
+\newcommand*{\signedIntE}{\rn{SignedInt}\rE}
+\newcommand*{\nameE}{\rn{Name}\rE}
+\newcommand*{\arrayAccessE}{\rn{ArrayAccess}\rE}
+\newcommand*{\bitStringAccessE}{\rn{BitStringAccess}\rE}
+\newcommand*{\listE}{\rn{List}\rE}
+%% \newcommand*{\listAltE}{\rn{List}\rSep\rn{Alt}\rE}
+\newcommand*{\recordE}{\rn{Record}\rE}
+\newcommand*{\logicalNegE}{\rn{LogicalNegation}\rE}
+\newcommand*{\bitwiseComplementE}{\rn{BitwiseComplement}\rE}
+\newcommand*{\unaryMinusE}{\rn{UnaryMinus}\rE}
+\newcommand*{\binaryOpsE}{\rn{BinaryOps}\rE}
+\newcommand*{\castE}{\rn{cast}\rE}
+\newcommand*{\typeMemE}{\rn{TypeMember}\rE}
+\newcommand*{\errMemE}{\rn{ErrorMember}\rE}
+\newcommand*{\expMemE}{\rn{ExpressionMember}\rE}
+\newcommand*{\ternaryE}{\rn{Ternary}\rE} 
+\newcommand*{\funcCallE}{\rn{FunctionCall}\rE\rSep\rn{1}}
+\newcommand*{\funcCallNoTypeArgE}{\rn{FunctionCall}\rE\rSep\rn{2}}
+\newcommand*{\instE}{\rn{Instantiation}\rE}
+\newcommand*{\maskE}{\rn{Mask}\rE}
+\newcommand*{\rangeE}{\rn{Range}\rE}
+
+\newcommand*{\shiftRAE}{\rn{ShiftRight}\rAE}
+\newcommand*{\shiftLAE}{\rn{ShiftLeft}\rAE}
+\newcommand*{\bitConcatAE}{\rn{BitConcatenation}\rAE}
+\newcommand*{\restAE}{\rn{Rest}\rAE}
+
+
+%function call helper
+\newcommand*{\nameFuncNameE}{\rn{Name}\rSep\rn{Func}\rAE\rSep\rn{1}}
+\newcommand*{\nameFuncCountE}{\rn{Name}\rSep\rn{Func}\rAE\rSep\rn{2}}
+\newcommand*{\nameActionE}{\rn{Name}\rSep\rn{Action}\rAE}
+%% \newcommand*{\nameActionNameE}{\rn{NameExpression}\rSep\rn{ActionType}\rSep\rn{ResolveByName}\rE}
+%% \newcommand*{\nameActionCountE}{\rn{NameExpression}\rSep\rn{ActionType}\rSep\rn{ResolveByCount}\rE}
+\newcommand*{\expMemExternNameE}{\rn{ExpMem}\rSep\rn{Extern}\rAE\rSep\rn{1}}
+\newcommand*{\expMemExternCountE}{\rn{ExpMem}\rSep\rn{Extern}\rAE\rSep\rn{2}}
+\newcommand*{\expMemSpcE}{\rn{ExpMem}\rSep\rn{Specialized}\rAE}
+%% \newcommand*{\expMemSpcCountE}{\rn{Exp:ExpMem}\rSep\rn{Type:Specialized}\rSep\rn{Resolve:Count}\rE}
+
+\newcommand*{\inferTypeArgAE}{\rn{InferTypeArg}\rAE}
+
+\newcommand*{\assignmentS}{\rn{Assignment}\rS}
+\newcommand*{\emptyS}{\rn{Empty}\rS}
+\newcommand*{\blockS}{\rn{Block}\rS}
+\newcommand*{\returnS}{\rn{Return(inApplyBlockOrAction)}\rS}
+\newcommand*{\returnEmpS}{\rn{ReturnEmpty}\rS}
+\newcommand*{\returnFuncS}{\rn{Return(inFunction)}\rS}
+\newcommand*{\exitS}{\rn{Exit}\rS}
+\newcommand*{\ifthenS}{\rn{IfThen}\rS}
+\newcommand*{\ifthenelseS}{\rn{IfThenElse}\rS}
+\newcommand*{\switchS}{\rn{Switch}\rS}
+\newcommand*{\declS}{\rn{Declaration}\rS}
+
+\newcommand*{\constantD}{\rn{Constant}\rD}
+\newcommand*{\instantD}{\rn{Instantiation}\rD}
+\newcommand*{\parserD}{\rn{Parser}\rD}
+\newcommand*{\controlD}{\rn{Control}\rD}
+\newcommand*{\funcD}{\rn{Function}\rD}
+\newcommand*{\actionD}{\rn{Action}\rD}
+\newcommand*{\externFuncD}{\rn{ExternFunction}\rD}
+\newcommand*{\varD}{\rn{Variable}\rD}
+\newcommand*{\varInitD}{\rn{VariableInit}\rD}
+\newcommand*{\valueSetD}{\rn{ValueSet}\rD}
+\newcommand*{\tableD}{\rn{Table}\rD}
+\newcommand*{\headerD}{\rn{Header}\rD}
+\newcommand*{\headerUnionD}{\rn{HeaderUnion}\rD}
+\newcommand*{\structD}{\rn{Struct}\rD}
+\newcommand*{\errD}{\rn{Error}\rD}
+\newcommand*{\matchkindD}{\rn{MatchKind}\rD}
+\newcommand*{\enumD}{\rn{Enum}\rD}
+\newcommand*{\serEnumD}{\rn{SerializableEnum}\rD}
+\newcommand*{\externObjD}{\rn{ExternObject}\rD}
+\newcommand*{\typDefD}{\rn{TypeDefinition}\rD}
+\newcommand*{\newtypeD}{\rn{NewType}\rD}
+\newcommand*{\controlTypD}{\rn{ControlType}\rD}
+\newcommand*{\parserTypD}{\rn{ParserType}\rD}
+\newcommand*{\packageTypD}{\rn{PackageType}\rD}
+
 %stuff here and there:
+%TODO: fix mathit in the followings:
 \renewcommand{\or}{\ | \ }
 \newcommand{\whereBulletIs}{,\textit{ where } \bullet \textit{ is }}
 \newcommand{\whereIs}[1]{,\textit{ where } {#1} \textit{ is }}
@@ -9,64 +145,155 @@
 \newcommand{\cond}{\mathit{cond}}
 \newcommand{\prim}[1]{{#1}^\prime}
 \newcommand{\pprim}[1]{{#1}^{\prime\prime}}
+\newcommand{\ppprim}[1]{{#1}^{\prime\prime\prime}}
 \newcommand{\so}[2]{{#1} \Rightarrow {#2}}
 \newcommand{\lookupEnv}[1]{\env({#1})}
+\newcommand{\lookupExternEnv}[1]{\externEnv({#1})}
+\newcommand{\lookupTypEnv}[1]{\typEnv({#1})}
 \newcommand{\emp}{[\ ]}
+\newcommand{\insertToEnv}[2]{\env[{#1} : {#2} ]}
+\newcommand{\insertToEnvv}[1]{\env[{#1}]}
+\newcommand{\extendTypEnv}[1]{\typEnv[{#1} \ \mathsf{var}]}
+\newcommand{\extendTypsEnv}[1]{\typEnv[\overline{{#1} \ \mathsf{var}}]}
+\newcommand{\suchThat}[2]{{#1}\ . \ {#2}}
+\newcommand{\tr}{\mathsf{true}}
+\newcommand{\fl}{\mathsf{false}}
 
-% separator
-\newcommand{\rn}[1]{\TirName{#1}}
-\newcommand{\rSep}{\rn{-}}
+% renew these commands to change the size and indentation of program text
+%% \newcommand{\progind}{\parindent}
+%% \newcommand{\progfontsize}{\small}
+%% \newcommand{\progformat}{}
+%% % in-line code
+%% \newcommand{\prog}[1]{\textrm{\progfontsize\progformat\texttt{#1}}}
+%% \newcommand{\tr}{\prog{true}}
+%% \newcommand{\fl}{\prog{false}}
 
-\newcommand*{\rE}{\rSep\rn{E}}
-\newcommand*{\restJ}{\rn{Rest}}
+%% \newcommand{\iLeqLeq}[2]{{#1} \leq i \leq {#2}. \ } %TODO: refactor 1 < i < n
+%% \newcommand{\iLeqL}[2]{{#1} \leq i < {#2}. \ }
+%% \newcommand{\iEqLeq}[2]{{#1} < i \leq {#2}. \ }
+%% \newcommand{\iLL}[2]{{#1} < i < {#2}. \ }
+%% \newcommand{\leqLeq}[3]{{#1} \leq {#2} \leq {#3}. \ }
+%% \newcommand{\leqL}[3]{{#1} \leq {#2} < {#3}. \ }
+%% \newcommand{\lLeq}[3]{{#1} < {#2} \leq {#3}. \ }
+%% \newcommand{\lL}[3]{{#1} < {#2} < {#3}. \ }
+%% \newcommand{\forallcond}[3]{\forall {#1} \in {#2}\ . \ {#3}}
 
 %typing judgments:
 \newcommand{\envOne}[2]{\Delta, T, \Gamma \vdash {#1} : {#2}}
-\newcommand{\expenv}[4]{\env, \ctxt \vdash {#1} \leadsto {#2}, {#3}, {#4}}
-\newcommand{\expenvWithCtxt}[5]{\env, {#1} \vdash {#2} \leadsto {#3}, {#4}, {#5}}
-\newcommand{\coerceBinArgsEnv}[3]{\env, \ctxt \vdash {#1} \twoheadrightarrow ({#2}; {#3})}
-\newcommand{\binOpEnv}[4]{\env \vdash {#1} \hookrightarrow {#2}, {#3}, {#4}}
-\newcommand{\typWellFormed}[1]{\env \vdash {#1}}
+\newcommand{\expenv}[4]{\constEnv, \varEnv, \typEnv, \ctxt \vdash {#1} \leadsto {#2}, {#3}, {#4}}
+\newcommand{\expenvv}[5]{\constEnv_{#5}, \varEnv_{#5}, \typEnv_{#5}, \ctxt_{#5} \vdash {#1} \leadsto {#2}, {#3}, {#4}}
+\newcommand{\expenvvv}[3]{{#1}, \ctxt \vdash {#2} \leadsto {#3}} %%TODO: check where you've used this and correct the envs
+\newcommand{\expenvWithCtxt}[5]{\constEnv, \varEnv, \typEnv, {#1} \vdash {#2} \leadsto {#3}, {#4}, {#5}}
+\newcommand{\coerceBinArgsEnv}[3]{\env, \ctxt \vdash {#1} \twoheadrightarrow ({#2}), ({#3})}
+\newcommand{\binOpEnv}[7]{\env \vdash {#1}, ({#4}, {#5}), ({#6}, {#7}) : {#2}, {#3}}
+\newcommand{\typWellFormed}[1]{\typEnv, \externEnv \vdash {#1}}
+\newcommand{\typNotWellFormed}[1]{\typEnv, \externEnv \nvdash {#1}}
+\newcommand{\typWellFormedWithEnv}[2]{{#1}, \externEnv \vdash {#2}}
+\newcommand{\typEqEnv}[3]{ {#2} ==_{\env,{#1}} {#3}} %%todo: fix env
+%context. type of expression. type of returned name.exp
+\newcommand{\fieldAccessEnv}[4]{\env, {#1} \vdash {#2}, {#3} : {#4}}
+\newcommand{\stmtenv}[3]{\env, \ctxt \vdash {#1} \leadsto {#2}, {#3} \dashv \env}
+\newcommand{\stmtenvv}[5]{\env_{#1}, \ctxt_{#1} \vdash {#2} \leadsto {#3}, {#4} \dashv \env_{#5}}
+\newcommand{\dclenv}[2]{\env, \ctxt \vdash {#1} \leadsto {#2} \dashv \env}
+\newcommand{\dclenvv}[4]{\env_{#1}, \ctxt_{#1} \vdash {#2} \leadsto {#3} \dashv \env_{#4}}
+\newcommand{\dclenvvv}[4]{\constEnv, \typEnv \vdash {#1} \leadsto {#2} \dashv {#3}, {#4}}
+\newcommand{\explCast}[2]{\castenv {e} {#1} {#2}}
+\newcommand{\castenv}[3]{\env \vdash {#2} \rightarrow_{#1} {#3}}
+\newcommand{\implCast}[2]{\castenv {i} {#1} {#2}}
+%exp, args. exp', type pars, pars, kind, return type.
+%check if you need the dir to be returned as well. 
+\newcommand{\resolveFuncOver}[7]{\env, \ctxt \vdash \mathit{dispatch}({#1}, {#2}, {#3}, \funcType {#6} {#4} {#5} {#7})}
+%typ par : typ arg. par = exp. . typ par : typ arg (infered).
+% this has an extra input in code (which is constraints (init to typ par : typ arg)) but it's never used so i dropped it. same for return type.
+\newcommand{\inferTypParArg}[3]{\env, \ctxt \vdash {#1}, {#2} \mapsto {#3}}
+\newcommand{\unify}[6]{{#1}, {#2}, {#3} \vDash {#4} \Join {#5} \mapsto {#6}}
+\newcommand{\resolveConstOver}[6]{\env, \ctxt \vdash \mathit{dispatch} \left( {#1}, {#2} \constructorTyp {#3} {#4} {#5} {#6}\right)}
 
 %contexts:
-\newcommand{\cte}{\mathit{CONSTANT}}
+\newcommand{\cte}{\mathsf{constant}}
+\newcommand{\applyBlockCtxt}{\mathsf{applyBlock}}
+\newcommand{\actionCtxt}{\mathsf{action}}
+\newcommand{\tableActionCtxt}{\mathsf{tableAction}}
+\newcommand{\funcCtxt}[1]{\mathsf{function}\ {#1}}
+\newcommand{\parserCtxt}{\mathsf{parserState}}
+\newcommand{\toplevel}{\mathsf{topLevel}}
+\newcommand{\declLocalCtxt}{\mathsf{declLocal}}
 
 %operators:
-\newcommand{\mask}[2]{{#1} \&\&\& {#2}}
+\newcommand{\mask}[2]{{#1}\ \&\&\&\ {#2}}
 \newcommand{\range}[2]{{#1}..{#2}}
-\newcommand{\ternary}[3]{{#1} ? {#2} : {#3}}
-\newcommand{\errMem}[1]{\mathit{error}.{#1}}
+\newcommand{\ternary}[3]{{#1}\, ?\, {#2}\, : \, {#3}}
+\newcommand{\errMem}[1]{\mathsf{error}.{#1}}
 \newcommand{\typMem}[2]{{#1}.{#2}}
 \newcommand{\shiftR}{\gg}
 \newcommand{\shiftL}{\ll}
 \newcommand{\concat}{+\!+\ }
 \newcommand{\restOps}{\odot}
 \newcommand{\ops}{\odot}
-\newcommand{\cast}[2]{({#1}){#2}}
-\newcommand{\plusSat}{\vert+\vert}
-\newcommand{\subSat}{\vert-\vert}
+\newcommand{\unaryOp}{\ominus}
+\newcommand{\binOp}{\oplus}
+\newcommand{\cast}[2]{({#1})\,{#2}}
+\newcommand{\plusSat}{|+|}
+\newcommand{\subSat}{|-|}
+\newcommand{\logor}{||}
 \newcommand{\bitAnd}{\&}
-\newcommand{\bitOr}{\vert}
+\newcommand{\bitOr}{|}
 \newcommand{\bitXor}{\hat{}}
-\newcommand{\bitComplement}{\sim}
+\newcommand{\bitComplement}{\sim\!}
 \renewcommand{\div}{/}
 \renewcommand{\mod}{\%}
+\newcommand{\funcCall}[3]{{#1}\,\langle{#2}\rangle\,({#3})}
+\newcommand{\funcCallNoTypArgs}[2]{{#1}({#2})}
+\newcommand{\expMem}[2]{{#1}.{#2}}
+\newcommand{\instantiation}[2]{{#1}\, ({#2})} %%anonymous instantiation
+%name.
+%% \newcommand{\parserDecl}[]{\mathit{parser}\ {#1} (type_param param) {const_param locals states}
+\renewcommand{\list}[1]{\{{#1}\}}
+%% \newcommand{\record}[2]{\{\field_{#1} = \exp_{#1}, \ldots, \field_{#2} = \exp_{#2}\}}
+\newcommand{\recordd}[3]{\{\field_{#1} = {#3}_{#1}, \ldots, \field_{#2} = {#3}_{#2}\}}
+\newcommand{\record}[2]{\recordd {#1} {#2} {\exp} }
+\newcommand{\records}[1]{\{\overline {\field = {#1}} \}}
+
+
+%operators:
+\newcommand{\intoOp}[1]{\texttt{#1}}
 
 %metavariables:
-\newcommand{\env}{e}
-\newcommand{\typ}{t}
+\newcommand{\prmDef}[1]{\mathit{prm}_{#1}}
+\newcommand{\prmDefs}[1]{\overline {\prmDef {#1}}}
+\newcommand{\constraint}{C}
+\newcommand{\optConstraint}{B}
+\newcommand{\nonoptConstraint}{N}
+\newcommand{\typeEqs}{\Delta}
+\newcommand{\anyTyp}{a}
+\newcommand{\typEnv}{\Delta}
+\newcommand{\varEnv}{\Gamma}
+\newcommand{\constEnv}{\Sigma}
+\newcommand{\externEnv}{\Xi}
+\newcommand{\env}{\Gamma}
+%% \newcommand{\typEnv}{\Gamma}
+%% \newcommand{\constEnv}{\Sigma}
+\newcommand{\typ}{\tau}
+\newcommand{\typs}{\overline \typ}
+\newcommand{\baseTyp}{\rho}
+\newcommand{\baseTyps}{\overline \baseTyp}
+\newcommand{\typKind}{t}
 \newcommand{\ctxt}{c}
 \newcommand{\bool}{b}
 \newcommand{\str}{s}
 \newcommand{\width}{w}
 \newcommand{\val}{v}
-\newcommand{\bit}{\mathit{bit}}
+\newcommand{\bit}{b}
 \renewcommand{\int}{n}
-\newcommand{\bitWidth}[2]{{#1}_{#2}}
-\newcommand{\intWidth}[2]{{#1}_{#2}}
-\newcommand{\name}{\mathit{name}}
-\renewcommand{\array}{a}
-\renewcommand{\index}{i}
+\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}
 \newcommand{\arrayAccess}[2]{{#1}[{#2}]}
 \newcommand{\size}{n}
 \newcommand{\high}{h}
@@ -74,56 +301,308 @@
 \newcommand{\bitString}{bs}
 \newcommand{\bitStringAccess}[3]{{#1}[{#2}:{#3}]}
 \renewcommand{\exp}{\mathit{exp}}
+\newcommand{\exps}{\overline {\exp}}
 \newcommand{\field}{f}
+\newcommand{\fields}{\overline \field}
+\newcommand{\param}{x}
+\newcommand{\params}{\overline x}
+\newcommand{\prm}[1]{\dir_{#1}\  \param_{#1}:\typ_{#1}}
+\newcommand{\singleprm}{\dir \ \param: \typ }
+\newcommand{\prms}{\overline {\singleprm}}
+\newcommand{\prmss}{\overline {\prim \dir \ \prim \param: \prim \typ}}
+\newcommand{\typParam}{\typVar}
+\newcommand{\typParams}{\overline \typParam}
+\newcommand{\pari}[1]{\dir_{#1}\ \param_{#1}: \typ_{#1}}
+\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}}
+\newcommand{\args}{\overline \arg}
+\newcommand{\kind}{k}
+\newcommand{\ret}{\mathit{return}}
+\newcommand{\retTyp}{\typ_\ret}
+\newcommand{\argexp}{\exp}
+\newcommand{\argexps}{\overline \argexp}
+\newcommand{\argexpi}[1]{\argexp_{#1}}
+\newcommand{\argexpss}[2]{\argexpi {#1}, \ldots, \argexpi {#2}}
+\newcommand{\argkv}{\var = \exp}
+\newcommand{\argkvi}[1]{\var_{#1}=\exp_{#1}}
+\newcommand{\argkvs}{\overline \argkv}
+\newcommand{\argkvss}[2]{\argkvi {#1}, \ldots, \argkvi {#2}}
+\newcommand{\missingarg}{\mathsf{missing}}
+\newcommand{\names}{\overline \name}
+\newcommand{\methods}[2]{\overline {{#1}:{#2}}}
+
+% statements
+\newcommand{\stmt}{\mathit{stmt}}
+\newcommand{\stmts}{\overline \stmt}
+\newcommand{\block}[1]{\{ {#1} \}}
+\newcommand{\ifthen}[2]{\mathsf{if}\ {#1}\ \mathsf{then}\ {#2}}
+\newcommand{\ifthenelse}[3]{\mathsf{if}\ {#1}\ \mathsf{then}\ {#2}\ \mathsf{else}\ {#3}}
+\newcommand{\methodCall}[3]{{#1}\,\langle{#2}\rangle\, \left({#3}\right)}
+\newcommand{\assign}[2]{{#1}:={#2}}
+\newcommand{\noop}{;}
+\newcommand{\return}[1]{\mathsf{return}\ {#1}}
+\newcommand{\retNothing}{\mathsf{return ;}}
+\newcommand{\exit}{\mathsf{exit}}
+\newcommand{\switch}[2]{\mathsf{switch}\ ({#1})\, \{{#2}\}}
+\newcommand{\lbl}{l}
+\newcommand{\actionCase}[1]{\lbl : \block {#1}}
+\newcommand{\switchCase}{\mathit{switch\_case}}
+\newcommand{\switchCases}{\overline \switchCase}
+\newcommand{\dirApp}[2]{{#1} \left({#2}\right)}
+\newcommand{\defLbl}{\mathsf{default}}
+
+%% parser states
+\newcommand{\slctTran}[2]{({#1})\ \{{#2}\}}
+\newcommand{\expandCase}[2]{{#1} \ {#2}}
+\newcommand{\nxt}{\mathit{nxt}}
+\newcommand{\accept}{\mathsf{accept}}
+\newcommand{\reject}{\mathsf{reject}}
+\newcommand{\dontcareMatch}{\mathsf{dontcare}}
+\newcommand{\defMatch}{\mathsf{default}}
+\newcommand{\pmatch}{\mathit{mtch}}
+\newcommand{\pmatches}{\overline \pmatch}
+\newcommand{\case}{\mathit{case}}
+\newcommand{\pcases}{\overline \case}
+\newcommand{\parserTran}{t}
+\newcommand{\parserTrans}{\overline \parserTran}
+\newcommand{\stateDef}[3]{{#1}\ \{{#2}\} \ {#3}}
+\newcommand{\state}{\mathit{st}}
+\newcommand{\states}{\overline \state}
+
+
+%% table properties
+\newcommand{\custom}[3]{{#1}\,({#2},{#3})}
+\newcommand{\entry}[2]{\overline {#1} \, {#2}}
+\newcommand{\action}{\mathit{act}}
+\newcommand{\actionDef}[2]{{#1}\, ({#2})}
+\newcommand{\actions}{\overline \action}
+\newcommand{\key}[2]{{#1} : {#2}}
+\newcommand{\keys}[2]{\overline {\key {#1} {#2}}}
+\newcommand{\prop}{\mathit{prop}}
+\newcommand{\props}{\overline \prop}
 
+%% field type pairs
+\newcommand{\fieldTyp}{\field:\baseTyp}
+\newcommand{\fieldTyps}{\overline \fieldTyp}
+
+%% methods
+\newcommand{\constructor}[2]{{#1}\,(\overline {{#2}})}
+\newcommand{\abstractMethod}[4]{{#1}\, {#2}\, \langle\overline {{#3}}\rangle\,(\overline {{#4}})}
+\newcommand{\methodDef}[4]{{#1}\, {#2}\, \langle\overline {{#3}}\rangle\,(\overline {{#4}})}
+\newcommand{\extMethod}{\mathit{mth}}
+\newcommand{\extMethods}{\overline \extMethod}
+
+% declarations
+\newcommand{\dcl}{\mathit{dcl}}
+\newcommand{\dcls}{\overline \dcl}
+\newcommand{\constDcl}[3]{\mathsf{const}\ {#1}\ {#2} := {#3}}
+\newcommand{\inst}[4]{{#1}\, ({#2})\, {#3}\, \{{#4}\}}
+\newcommand{\instNoBlock}[3]{{#1}\, ({#2})\, {#3}}
+\newcommand{\parserDcl}[6]{\mathsf{parser}\ {#1}\, \langle {#2}\rangle\, ({#3})\, ({#4})\, \{{#5}\ {#6} \}}
+\newcommand{\controlDcl}[6]{\mathsf{control}\ {#1}\, \langle {#2}\rangle\, ({#3})\, ({#4})\, \{ {#5}\ {#6} \}}
+\newcommand{\funcDcl}[5]{\mathsf{function}\ {#1}\, {#2}\, \langle {#3}\rangle\, ({#4})\, \{ {#5}\}}
+\newcommand{\externFuncDcl}[4]{\mathsf{extern\_function}\ {#1}\, {#2}\, \langle {#3}\rangle\, ({#4})}
+\newcommand{\varDclInit}[3]{{#1}\ {#2} := {#3}}
+\newcommand{\varDcl}[2]{{#1}\, {#2}}
+%type. expression. name.
+\newcommand{\valSetDcl}[3]{{#1}\, {#3}:{#2}}
+\newcommand{\actionDcl}[3]{\mathsf{action}\ {#1}\, ({#2})\, \{{#3}\}}
+\newcommand{\tableDcl}[2]{\mathsf{table}\ {#1}\, \{{#2}\}}
+\newcommand{\headerDcl}[2]{\mathsf{header}\ {#1}\, \{{#2}\}}
+\newcommand{\headerUnionDcl}[2]{\mathsf{header\_union}\ {#1}\, \{{#2}\}}
+\newcommand{\structDcl}[2]{\mathsf{struct}\ {#1}\, \{{#2}\}}
+\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{\externObjDcl}[3]{\mathsf{extern}\ {#1}\, \langle{#2}\rangle\, \{{#3} \}}
+%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})}
+\newcommand{\packageTypDcl}[3]{\mathsf{package}\ {#1}\, \langle{#2}\rangle\, ({#3})}
+
+\newcommand{\prog}{\mathit{prog}}
 
 %function helpers
+\newcommand{\types}[1]{\mathit{types\_of}({#1})}
+\newcommand{\mergeConst}[1]{\mathit{merge\_types}({#1})}
+\newcommand{\toVoid}[1]{\mathit{voidify}({#1})}
+\newcommand{\breakMaybes}[3]{\mathit{break\_option}({#1})=\left({#2},{#3}\right)}
+\newcommand{\isExtern}[1]{\mathit{is\_extern}({#1})}
+\newcommand{\nothing}{\bot}
+\newcommand{\maskTypeIs}[2]{\mathit{mask\_type}({#1},{#2})}
+% \typ = \intWidthTyp \width \textOr \bitWidthTyp \width
+\newcommand{\widthInt}[1]{\mathit{width\_int}({#1})}
+%% - $\bothWidthInt {\typ_1} {\typ_2}$ is a helper function that checks if both types are fixed-length signed or unsigned integers. That is, it checks the conditions below and returns $\tr$ if one of them holds:
+%% + $\typ_1 = \typ_2 = \bitWidthTyp \width$
+%% + $\typ_1 = \typ_2 = \intWidthTyp \width$
+%% \newcommand{\bothWidthInt}[2]{\mathit{both\_width\_int}({#1},{#2})}
+%\typ = {\bitWidthTyp \width} \textOr \intWidthTyp \width \textOr \integerTyp
+\newcommand{\isInt}[1]{\mathit{is\_int}({#1})}
+% \left( \typ_1 = \typ_2 = \integerTyp \right) \\
+% \textOr \left( \prim {\typ_1} = \prim {\typ_2} = \bitWidthTyp \width \right) \\
+% \textOr \left( \prim {\typ_1} = \prim {\typ_2} = \intWidthTyp \width \right)
+\newcommand{\bothInt}[2]{\mathit{both\_int}({#1},{#2})}
+\newcommand{\concatCond}[2]{\mathit{concat\_type}({#1},{#2})}
+\newcommand{\divCond}[2]{\mathit{div\_type}({#1},{#2})}
+\newcommand{\shiftCond}[2]{\mathit{shift\_condition}({#1},{#2})}
+\newcommand{\addTypeEnv}[2]{\typEnv[{#1}:{#2}]}
+\newcommand{\addTypEnvv}[1]{\typEnv[{#1}]}
+\newcommand{\unionEnv}[2]{{#1}\cup{#2}}
+\newcommand{\addConstEnv}[2]{\constEnv[{#1}={#2}]}
 \newcommand{\isNumeric}[1]{\mathit{is\_numeric}({#1})}
-\newcommand{\isArray}[1]{\mathit{is\_array}({#1})}
-\newcommand{\compileTimeEval}[1]{\llbracket{#1}\rrbracket_\env}
-\newcommand{\implicitCast}[2]{\mathit{implicit\_cast}({#1},{#2})_\env}
-\newcommand{\reduceEnums}[1]{\mathit{reduce\_enums}({#1}.\typ)_\env} 
+%% \newcommand{\isArray}[1]{\mathit{is\_array}({#1})}
+\newcommand{\getEnum}[1]{\mathit{get\_enum}({#1})}
+\newcommand{\isConstant}[1]{\mathit{is\_constant} ({#1})}
+\newcommand{\isInstantiation}[1]{\mathit{is\_instantiation} ({#1})}
+\newcommand{\isVariable}[1]{\mathit{is\_variable} ({#1})}
+\newcommand{\compileTimeEval}[1]{\llbracket{#1}\rrbracket_{\constEnv, \typEnv}}
+\newcommand{\implicitCast}[2]{\mathit{implicit\_cast}({#1},{#2})}
+\newcommand{\reduceEnums}[1]{\mathit{reduce\_enums}({#1})_\env} 
 \newcommand{\inOrLess}[2]{\mathit{in\_or\_directionless}({#1},{#2})}
-\newcommand{\typEq}[3]{{#2} ==_{\env,{#1}} {#3}}
+%% \newcommand{\typEq}[3]{{#2} ==_{\env,{#1}} {#3}}
 \newcommand{\typHasEq}[1]{\mathit{has\_equality}({#1})_\env}
 \newcommand{\nonNeg}[1]{\mathit{is\_nonneg\_numeric}({#1})_\env}
 \newcommand{\pos}[1]{\mathit{is\_pos\_numeric}({#1})_\env}
-\newcommand{\compTimeKnown}[1]{\mathit{compile\_time\_known}({#1})_\env}
-\newcommand{\sat}[1]{\mathit{saturate}({#1})_\env}
+\newcommand{\compTimeKnown}[1]{\mathit{compile\_time\_known}({#1})_{\constEnv, \typEnv}}
+\newcommand{\sat}[1]{\mathit{saturate}({#1})_\typEnv}
 \newcommand{\trans}[2]{\mathit{translate}({#1})_{\env,{#2}}}
-\newcommand{\isValidNestedTyp}[2]{\mathit{is\_valid\_nested\_type}({#1},{#2})_\env}
+\newcommand{\transMaybe}[1]{\mathit{optional\_translate}({#1})_{\env}}
+\newcommand{\isValidNestedTyp}[1]{\mathit{is\_valid\_nested}({#1})_\typEnv}
 %{#1} is outer, 2 is inner
 \newcommand{\noDup}[1]{\mathit{no\_duplicate}({#1})}
-\newcommand{\explicitCastOK}[2]{\mathit{explicit\_cast\_ok} ({#1}, {#2})_\env}
+\newcommand{\explicitCastOK}[2]{\explCast {#1} {#2}}
+\newcommand{\insertTypVars}[1]{\mathit{insert\_type\_vars}({#1}, \env)}
+\newcommand{\getTypeParams}[1]{\mathit{get\_type\_params}({#1})}
+\newcommand{\reduce}[1]{\mathit{reduce}({#1})_\typEnv}
+\newcommand{\reduceWithEnv}[2]{\mathit{reduce}({#2})_{#1}} %%TODO: adjust env where it's used. 
+%% \newcommand{\fieldOrMethodTyp}[1]{\mathit{field\_or\_method\_type}({#1})}
+\newcommand{\isLval}[1]{\mathit{is\_lvalue}({#1})}
+%type. exp. 
+\newcommand{\castExpression}[2]{\mathit{cast\_expression}({#1},{#2})}
+\newcommand{\ifVoidTyp}[1]{\mathit{if\_void\_type}({#1})}
+\newcommand{\allowedTypeForVar}[1]{\mathit{is\_allowed\_type\_for\_variable}({#1})}
+\newcommand{\checkParamShadow}[2]{\mathit{check\_parameter\_shadowing}({#1}, {#2})}
+\newcommand{\match}[2]{\mathit{match}({#1},{#2})}
+%% \newcommand{\zip}[2]{\mathit{zip} ({#1},{#2})}
+\newcommand{\matchParArg}[2]{\mathit{macth\_parameter\_argument}({#1},{#2})}
+\newcommand{\validatePars}[3]{\mathit{validate\_parameter}({#1})_{{#2},{#3}}}
+\newcommand{\validateParArg}[1]{\mathit{validate\_parmeter\_argument}({#1})}
+\newcommand{\maybe}[1]{{#1}_{\bot}}
+\newcommand{\castParArg}[1]{\mathit{cast\_parameter\_argument}({#1})}
+\newcommand{\callOK}[2]{\mathit{call\_ok}({#1},{#2})}
+\newcommand{\removeOptionalPars}[1]{\mathit{remove\_optional\_parameteres}({#1})}
+\newcommand{\concatList}[2]{{#1}\ +\!+\ {#2}}
+\newcommand{\isDirectionless}[1]{\mathit{is\_directionless}({#1})}
+\newcommand{\whatevs}{\_\!\_}
+
+%fields 
+\newcommand{\isValid}{\mathsf{isValid}}
+\newcommand{\apply}{\mathsf{apply}}
+\newcommand{\minSizeBits}{\mathsf{minSizeInBits}}
+\newcommand{\minSizeBytes}{\mathsf{minSizeInBytes}}
+\newcommand{\setValid}{\mathsf{setValid}}
+\newcommand{\setInvalid}{\mathsf{setInvalid}}
+\newcommand{\pushFront}{\mathsf{push\_front}}
+\newcommand{\popFront}{\mathsf{pop\_front}}
+\newcommand{\sizeMem}{\mathsf{size}}
+\newcommand{\lastIndex}{\mathsf{lastIndex}}
+\renewcommand{\next}{\mathsf{next}}
+\newcommand{\last}{\mathsf{last}}
+
+
+%kinds
+\newcommand{\builtin}{\mathsf{builtin}}
+\newcommand{\actionKind}{\mathsf{action}}
+\newcommand{\parserKind}{\mathsf{parser}}
+\newcommand{\controlKind}{\mathsf{control}}
+\newcommand{\methodKind}{\mathsf{method}}
+\newcommand{\externKind}{\mathsf{extern}}
+\newcommand{\tableKind}{\mathsf{table}}
+\newcommand{\funcKind}{\mathsf{function}}
+
+%keywords
+\newcommand{\newtypKey}{\mathsf{newtype}}
 
 %types:
-\newcommand{\bitWidthTyp}[1]{\mathit{bit}<\!{#1}\!>}
-\newcommand{\intWidthTyp}[1]{\mathit{int}<\!{#1}\!>}
-\newcommand{\boolTyp}{\mathit{bool}}
-\newcommand{\stringTyp}{\mathit{string}}
-\newcommand{\integerTyp}{\mathit{integer}}
-\newcommand{\bitStringTyp}[2]{\mathit{bit[{#1}-{#2}]}}
-\newcommand{\intTyp}{\mathit{int}}
-\newcommand{\setTyp}[1]{\mathit{set}<\!{#1}\!>}
-\newcommand{\errTyp}{\mathit{error}}
-\newcommand{\varBitTyp}[1]{\mathit{varbit}<{#1}>}
-\newcommand{\matchKindTyp}{\mathit{match\_kind}}
-\newcommand{\voidTyp}{\mathit{void}}
+\newcommand{\dontcareTyp}{\mathsf{dontcare}}
+\newcommand{\bitWidthTyp}[1]{\mathsf{bit}\langle{#1}\rangle}
+\newcommand{\intWidthTyp}[1]{\mathsf{int}\langle{#1}\rangle}
+\newcommand{\boolTyp}{\mathsf{bool}}
+\newcommand{\stringTyp}{\mathsf{string}}
+\newcommand{\integerTyp}{\mathsf{int}}
+\newcommand{\bitStringTyp}[1]{\bitWidthTyp {#1}}
+\newcommand{\setTyp}[1]{\mathsf{set}\langle{#1}\rangle}
+\newcommand{\errTyp}{\mathsf{error}}
+\newcommand{\varBitTyp}[1]{\mathsf{varbit}\langle{#1}\rangle}
+\newcommand{\matchKindTyp}{\mathsf{match\_kind}}
+\newcommand{\voidTyp}{\mathsf{void}}
 \newcommand{\arrayTyp}[2]{{#1}[{#2}]}
-\newcommand{\tupleTyp}[2]{<{#1},\ldots,{#2}>}
-\newcommand{\listTyp}[2]{[{#1},\ldots,{#2}]}
-\newcommand{\enumTyp}{\mathit{enum}\ {\typ}\ {\name}\{\name_1,\ldots,\name_n\}}
-\newcommand{\enumTypNoTyp}{\mathit{enum} \ {\name}\{\name_1,\ldots,\name_n\}}
-\newcommand{\recordTyp}{\mathit{record}\{\field_1:\typ_1,\ldots,\field_n:\typ_n \}}
-\newcommand{\headerUnionTyp}{\mathit{header\_union}\{\field_1:\typ_1,\ldots,\field_n:\typ_n \}}
-\newcommand{\headerTyp}{\mathit{header}\{\field_1:\typ_1,\ldots,\field_n:\typ_n \}}
-\newcommand{\structTyp}{\mathit{struct}\{\field_1:\typ_1,\ldots,\field_n:\typ_n \}}
-\newcommand{\newTypeTyp}[2]{\mathit{type}\ {#1}\ {#2}}
+\newcommand{\tupleTyp}[2]{\mathsf{tuple}\langle{#1},\ldots,{#2}\rangle}
+\newcommand{\tupleTyps}[1]{\mathsf{tuple}\langle{#1}\rangle}
+\newcommand{\listTyp}[2]{\tupleTyp {#1} {#2}}
+\newcommand{\listTyps}[1]{\tupleTyps {#1}}
+\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{\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}\}}
+%% \newcommand{\headerTypp}[2]{\mathit{header}\{\prim {\field_{#1}}:\prim {\typ_{#1}};\ldots;\prim {\field_{#2}}:\prim {\typ_{#2}}\}}
+%% \newcommand{\structTypDef}{\structTyp 1 n}
+%% \newcommand{\structTyp}[2]{\mathit{struct}\{\field_{#1}:\typ_{#1};\ldots;\field_{#2}:\typ_{#2}\}}
+%% \newcommand{\structTypp}[2]{\mathit{struct}\{\prim {\field_{#1}}:\prim {\typ_{#1}};\ldots;\prim {\field_{#2}}:\prim {\typ_{#2}}\}}
+\newcommand{\newTypeTyp}[2]{\newtypKey \ {#1}\ {#2}}
+\newcommand{\funcTyp}[3]{\mathsf{function}\ {#1}\ \langle{#2}\rangle ({#3})}
+\newcommand{\simpFuncTyp}[2]{{#1} \rightarrow {#2}}
+%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.
+%% 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}[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}}
+\newcommand{\unitTyp}{()}
+\newcommand{\stackTyp}[2]{{#1}[{#2}]}
 
 %directions:
-\newcommand{\less}{\mathit{directionless}}
+\newcommand{\less}{\mathsf{directionless}}
 \newcommand{\dir}{d}
-\renewcommand{\in}{\mathit{in}}
-\newcommand{\out}{\mathit{out}}
-
+\newcommand{\direction}{\mathit{dir}} %%for the typed.direction
+\newcommand{\dirs}{\overline \dir}
+\newcommand{\inDir}{\mathsf{in}}
+\newcommand{\out}{\mathsf{out}}
+\newcommand{\inout}{\mathsf{in\_out}}
diff --git a/lib/checker.ml b/lib/checker.ml
index 74bc181df..45b317346 100644
--- a/lib/checker.ml
+++ b/lib/checker.ml
@@ -408,6 +408,7 @@ and saturate_type (env: CheckerEnv.t) (typ: Typed.Type.t) : Typed.Type.t =
   | Constructor ctor ->
      Constructor (saturate_constructor env ctor)
 
+(* applies the arguments to the parameters of a specialized type that its base has parameters. *)
 and reduce_type (env: CheckerEnv.t) (typ: Typed.Type.t) : Typed.Type.t =
   let typ = saturate_type env typ in
   match typ with
@@ -519,6 +520,7 @@ and gen_all_constraints (env: CheckerEnv.t) ctx unknowns params_args constraints
   | [] ->
      constraints
 
+(* DISCUSS WITH RYAN: constraints doesn't need to be passed here. it's being built and the inputed one is never used. same goes for ret. *)
 and infer_type_arguments env ctx ret type_params_args params_args constraints =
   let insert (env, args, unknowns) (type_var, type_arg) =
     match type_arg with
@@ -632,7 +634,8 @@ and type_vars_equal_under equiv_vars tv1 tv2 =
       else type_vars_equal_under rest tv1 tv2
   | [] ->
       tv1 = tv2
-
+(* saturates the type first and returns the base of a specialized type by removing all
+   its type parameters as long as the number of type params and type args match. *)
 and reduce_type : CheckerEnv.t -> Typed.Type.t -> Typed.Type.t =
   fun env typ ->
   let typ = saturate_type env typ in
@@ -659,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)
@@ -907,14 +912,12 @@ and type_expression (env: CheckerEnv.t) (ctx: Typed.ExprContext.t) (exp: Express
        type_unary_op env ctx op arg
     | BinaryOp { op; args; tags } ->
        type_binary_op env ctx op args
-    (*  *)
     | Cast { typ; expr; tags } ->
        type_cast env ctx typ expr
     | TypeMember { typ; name; tags } ->
        type_type_member env ctx typ name
     | ErrorMember {tags; err} ->
        type_error_member env ctx err
-    (*  *)
     | ExpressionMember { expr; name; tags } ->
        type_expression_member env ctx expr name
     | Ternary { cond; tru; fls; tags } ->
@@ -963,6 +966,7 @@ and cast_to_same_type (env: CheckerEnv.t) (ctx: Typed.ExprContext.t) (exp1: Expr
   then exp1, add_cast env exp2 typ1
   else failwith "cannot cast types so that they agree"
 
+(* takes a type and surface syntax expression. after generating the IR expression by type_expression, it checks if the given type and type of IR expression are equal it just returns the IR exp o.w. it casts (if possible) the IR expression to the given type.  NOTE: it already know the cast, if needed, is valid. *)
 and cast_expression (env: CheckerEnv.t) ctx (typ: Typed.Type.t) (exp: Expression.t) =
   let module E = Prog.Expression in
   let typ = reduce_type env typ in
@@ -1235,13 +1239,13 @@ and field_cmp (f1: RecordType.field) (f2: RecordType.field) : int =
 
 * Tuple type:
    1 <= i <= n; e |- ti
-   1 <= i <= n; ???
+   1 <= i <= n; is_valid_nested_type(<t1,...,tn>, ti)_e
    ----------------------------------
-   e |- (t1, ..., tn)
+   e |- tuple <t1, ..., tn>
 
 * List type
    1 <= i <= n; e |- ti
-   1 <= i <= n; ???
+   1 <= i <= n; is_valid_nested_type([t1,...,tn], ti)_e
    ----------------------------------
    e |- [t1, ..., tn]
 
@@ -1252,56 +1256,65 @@ and field_cmp (f1: RecordType.field) (f2: RecordType.field) : int =
 
 * Enum type:
    ** the case where typ is Some typ.
+   * X is the name of the enum.
+   * li is the name of the field.
 
    e |- t
    -----------------------------------
-   e |- X : t {l1, ..., ln}
+   e |- enum t X {l1, ..., ln}
 
    ** the case where type is None.
 
-   e |- X {l1, ..., ln}
+   e |- enum X {l1, ..., ln}
 
 * Record and struct and header union ({l1:h1, ..., ln:hn}) type:
    1 <= i <= n; e |- ti
-   1 <= i <= n; ???
-   1 <= i < j <= n; li != lj
+   1 <= i <= n; is_valid_nested_type(record {f1 : t1, ..., fn : tn}, ti)_e
+   1 <= i < j <= n; fi != fj
    ------------------------------------
-   e |- {l1 : t1, ..., ln : tn}
+   e |- record {f1 : t1, ..., fn : tn}
 
 * header: 
    1 <= i <= n; e |- ti
-   1 <= i <= n; ???
-   1 <= i < j <= n; li != lj
+   1 <= i <= n; is_valid_nested_type(header {f1 : t1, ..., fn : tn}, ti)_e
+   1 <= i < j <= n; fi != fj
    ------------------------------------
-   e |- {l1 : t1, ..., ln : tn}
+   e |- header {l1 : t1, ..., ln : tn}
 
-   TODO: complete!
 * new type (name = typ):
    e |- t
    ----------------------------------
-   e |- n = t
+   e |- type t n 
 
 * specialized type:
+   look at spec
 
 * package type:
+   look at spec
 
 * control type:
+   look at spec
 
 * parser type:
+   look at spec
 
 * extern type:
+   look at spec
 
 * function type (<return type> <function name> (x1, ..., xn) {...}):
-   ----------------------------------------------------
-   e |- 
+   look at spec
 
 * action type:
-   --------------------------------------------
-   e |- 
+   look at spec
 
 * constructor type:
+   look at spec
 
 * table type:
+   look at spec
+
+* type name:
+   look at spec
 *)
 (* Returns true if type typ is a well-formed type *)
 and is_well_formed_type env (typ: Typed.Type.t) : bool =
@@ -1351,7 +1364,6 @@ and is_well_formed_type env (typ: Typed.Type.t) : bool =
     let res1 : bool = (are_param_types_well_formed env data_params) in
     let res2 : bool = (are_construct_params_types_well_formed env ctrl_params) in
     res1 && res2
-  (* Type names *)
   | TypeName name ->
     CheckerEnv.resolve_type_name_opt name env <> None
   | Table {result_typ_name=name} ->
@@ -1371,6 +1383,9 @@ and is_well_formed_type env (typ: Typed.Type.t) : bool =
     | Some {type_params = []; _} -> true
     | _ -> false
     end
+    (*TODO: discuss! according to p4 spec parser, control, and package cannot be
+                     type args to methods, parsers, controls, tables, and actions.
+                     but we're not checking this.*)
   | Parser {type_params=tps; parameters=ps;_}
   | Control {type_params=tps; parameters=ps;_} ->
     let env = CheckerEnv.insert_type_vars tps env in
@@ -1468,6 +1483,8 @@ and is_valid_param_type_kind env (kind: FunctionType.kind) (typ: Typed.Type.t) =
   | Function -> is_valid_param_type env (Runtime Function) typ
   | Builtin -> is_valid_param_type env (Runtime Method) typ
 
+(*  TODO: discuss with Ryan. doesn't match p4 spec for outer header.
+          also, role of in_header. *)
 and is_valid_nested_type ?(in_header=false) (env: CheckerEnv.t) (outer_type: Typed.Type.t) (inner_type: Typed.Type.t) =
   let inner_type = reduce_to_underlying_type env inner_type in
   match reduce_to_underlying_type env outer_type with
@@ -1538,6 +1555,47 @@ and validate_param env ctx (typ: Typed.Type.t) dir tags =
   if not (is_valid_param_type env ctx typ)
   then raise_s [%message "Type cannot be passed as a parameter" ~info:(tags:Info.t)];
 
+  (** copied this ease of access and read for formalization doc. *)
+  (* and is_valid_param_type env (ctx: Typed.ParamContext.t) (typ: Typed.Type.t) = *)
+  (* let typ = reduce_to_underlying_type env typ in *)
+  (* match ctx with *)
+  (* | Constructor decl -> *)
+  (*    begin match typ, decl with *)
+  (*    | Package _, Package -> true *)
+  (*    | Package _, _ -> false *)
+  (*    | Parser _, Package *)
+  (*    | Parser _, Parser -> true *)
+  (*    | Parser _, _ -> false *)
+  (*    | Control _, Package *)
+  (*    | Control _, Control -> true *)
+  (*    | Control _, _ -> false *)
+  (*    | Extern _, Package *)
+  (*    | Extern _, Parser *)
+  (*    | Extern _, Control *)
+  (*    | Extern _, Method -> true *)
+  (*    | Extern _, _ -> false *)
+  (*    | Function _, _ -> false *)
+  (*    | Action _, _ -> false *)
+  (*    | Table _, _ -> false *)
+  (*    | Set _, _ -> false *)
+  (*    | _ -> true *)
+  (*    end *)
+  (* | Runtime decl -> *)
+  (*    begin match typ, decl with *)
+  (*    | Package _, _ -> false *)
+  (*    | Parser _, _ -> false *)
+  (*    | Control _, _ -> false *)
+  (*    | Extern _, Parser *)
+  (*    | Extern _, Control *)
+  (*    | Extern _, Method -> true *)
+  (*    | Extern _, _ -> false *)
+  (*    | Table _, _ -> false *)
+  (*    | Set _, _ -> false *)
+  (*    | Action _, _ -> false *)
+  (*    | Function _, _ -> false *)
+  (*    | _ -> true *)
+  (*    end *)
+
 and type_param' ?(gen_wildcards=false) env (ctx: Typed.ParamContext.t) (param : Types.Parameter.t) : Typed.Parameter.t * string list =
   let typ, wildcards = translate_type' ~gen_wildcards env [] param.typ in
   let env = CheckerEnv.insert_type_vars wildcards env in
@@ -2182,6 +2240,7 @@ and check_binary_op env (op: Op.bin) typed_l typed_r : Prog.Expression.t =
           raise_mismatch (tags) "Operand must have type int<w> or bit<w>" l
        end
     (* Bitwise operators are only defined on bitstrings of the same width *)
+       (* TODO: discuss with Ryan. discrepency with spec. *)
     | BitAnd {tags} | BitXor {tags} | BitOr {tags} ->
        begin match l_typ, r_typ with
        | Bit { width = l }, Bit { width = r } when l = r -> Bit { width = l }
@@ -2190,6 +2249,7 @@ and check_binary_op env (op: Op.bin) typed_l typed_r : Prog.Expression.t =
        | _, _ -> raise_mismatch (typed_l.tags) "unsigned int" l_typ
        end
     (* Bitstring concatentation is defined on any two bitstrings *)
+    (* TODO: discuss with Ryan. discrepency with spec. *)
     | PlusPlus {tags} ->
        begin match l_typ, r_typ with
        | Bit { width = l }, Bit { width = r }
@@ -2209,6 +2269,7 @@ and check_binary_op env (op: Op.bin) typed_l typed_r : Prog.Expression.t =
        | _, _ -> raise_type_error tags (Type_Difference (l_typ, r_typ))
        end
     (* Division is only defined on compile-time known arbitrary-precision positive integers *)
+       (* TODO: discuss with Ryan. then why do we allow it for bit<w> too?*)
     | Div {tags} | Mod {tags} ->
        begin match l_typ, r_typ with
        | Integer, Integer ->
@@ -2220,6 +2281,7 @@ and check_binary_op env (op: Op.bin) typed_l typed_r : Prog.Expression.t =
        | Integer, _ -> raise_mismatch (typed_r.tags) "arbitrary precision integer" r_typ
        | _, _ -> raise_mismatch (typed_l.tags) "arbitrary precision integer" l_typ
        end
+       (* TODO: check this with Ryan. section 8.5 of spec.  *)
     | Shl {tags} | Shr {tags} ->
        begin match l_typ, is_nonnegative_numeric env typed_r with
        | Bit _, true
@@ -2238,6 +2300,7 @@ and check_binary_op env (op: Op.bin) typed_l typed_r : Prog.Expression.t =
     tags = tags_bin op}
 
 (* See section 8.9.2 "Explicit casts" *)
+(* cast judgment in spec. *)
 and cast_ok ?(explicit = false) env original_type new_type =
   let original_type = saturate_type env original_type in
   let new_type = saturate_type env new_type in
@@ -2372,6 +2435,8 @@ and type_error_member env ctx (name: P4String.t) : Prog.Expression.t =
     dir = Directionless;
     tags = Info.dummy }
 
+(* takes a type and if it's a header it returns a list of record type that has
+   isValid as a built in function. ow. returns an empty list.*)
 and header_methods typ =
   let fake_fields: RecordType.field list =
     [{name = "isValid";
@@ -2381,6 +2446,9 @@ and header_methods typ =
   | Type.Header { fields; _ } -> fake_fields
   | _ -> []
 
+(* takes a type, name, context. if type is an array and name is either size or lastindex
+   it returns the type Bit<32>. if type is an array and name is next or last and
+   context is parser state it returns the initial type passed in. ow. error.*)
 and type_expression_member_builtin env (ctx: Typed.ExprContext.t) tags typ (name: P4String.t) : Typed.Type.t =
   let open Typed.Type in
   let fail () =
@@ -2485,11 +2553,10 @@ and type_expression_member_function_builtin env typ (name: P4String.t) : Typed.T
   | _ -> None
 
 (* Sections 6.6, 8.14 *)
-(*
-
-   ----------------------------------------------------------------
-
-*)
+(* look at spec. *)
+(* In cases where the field is being looked up and it is not found (i.e., None)
+   the builtin helper is called for ease maintanance of the code in case we
+   need to extend builtin fields. *)
 and type_expression_member env ctx expr (name: P4String.t) : Prog.Expression.t =
   let typed_expr = type_expression env ctx expr in
   let expr_typ = reduce_type env typed_expr.typ in
@@ -2591,6 +2658,12 @@ and match_params_to_args call_site_tags params (args: Argument.t list) : (Typed.
   | Some `Named ->
      match_named_args_to_params call_site_tags params args
 
+(* matches arguments to parameters based on position and returns [(parameter, option expression)].
+   if an argument is missing, it bundles up the parameter to none.
+   if the argument list becomes empty but there are still parameters, it checks if
+   the parameter has opt_value, if so it bundles the parameter with an expression that has the
+   value of opt_value. if the parameter doesn't have opt_value, it checks if the parameter is
+   optional, if so, it bundles up the parameter with a missing argument. ow., it raises an error.*)
 and match_positional_args_to_params call_site_tags params args =
   let conv param arg =
     let open Types.Argument in
@@ -2620,6 +2693,13 @@ and match_positional_args_to_params call_site_tags params args =
   in
   go params args
 
+(* matches the arguments to parameters based on parameter names.
+   if the parameter and argument have the same name it bundles up the parameter name and the
+   argument value.
+   if the parameter has opt_value and there is no argument with the name of parameter it
+   bundles up the parameter name with its opt_value. but if the paremeter doesn't have
+   opt_value and is optional, it bundles up the parameter name with none. ow., it raises a
+   mismatch error. *)
 and match_named_args_to_params call_site_tags (params: Typed.Parameter.t list) args =
   let open Types.Argument in
   let open Typed.Parameter in
@@ -2732,12 +2812,6 @@ and call_ok (ctx: ExprContext.t) (fn_kind: Typed.FunctionType.kind) : bool =
   | _, Builtin -> true
   end
 
-(*
-
-   --------------------------------------------------------
-   e, c |- exp (t1 a1, ..., tn an) ~~> 
-
-*)
 and type_function_call env ctx call_tags func type_args (args: Argument.t list) : Prog.Expression.t =
   let open Prog.Expression in
   (* Printf.printf "we're here!!!"; *)
@@ -2977,6 +3051,8 @@ and resolve_function_overload env ctx type_name args =
   | None ->
      resolve_function_overload_by ~f:(overload_param_count_ok args) env ctx type_name
 
+(*TODO
+  *)
 and type_constructor_invocation env ctx tags decl_name type_args args : Prog.Expression.t list * Typed.Type.t =
   let open Typed.ConstructorType in
   let type_args = List.map ~f:(translate_type_opt env []) type_args in(* determines if type is dontcare.*)
@@ -2986,6 +3062,7 @@ and type_constructor_invocation env ctx tags decl_name type_args args : Prog.Exp
   let params_args = match_params_to_args tags constructor_type.parameters args in
   let type_params_args = infer_constructor_type_args env ctx t_params w_params params_args type_args in
   let env' = CheckerEnv.insert_types type_params_args env in
+  (* have to add this. TODO*)
   let cast_arg (param, arg: Typed.Parameter.t * Types.Expression.t option) =
     match cast_param_arg env' ctx tags (param, arg) with
     | _, Some e ->
@@ -3006,15 +3083,7 @@ and type_constructor_invocation env ctx tags decl_name type_args args : Prog.Exp
 
 (* Section 14.1 *)
 (*
-
-   base ?= TypeName t
-   ----------------------------------------
-   e, c |- SpecializedType {base, args} @ [arg1, .., argn] ~~> { @ [], Directionless}
-
-   typ = SpecializedType {t, []}
-   e, c |- typ @ [arg1, .., argn] ~~> {e, t, d}
-   --------------------------------------------------------
-   e, c |- TypeName t @ [arg1, .., argn] ~~> {e, t, d}
+   look at spec
 *)
 and type_nameless_instantiation env ctx tags (typ : Types.Type.t) args =
   let open Prog.Expression in
@@ -3124,26 +3193,34 @@ and type_statement (env: CheckerEnv.t) (ctx: StmtContext.t) (stm: Statement.t) :
     match stm with
     | MethodCall { func; type_args; args; tags } ->
        type_method_call env ctx tags func type_args args
+      (*10.1 ipad version.*)
     | Assignment { lhs; rhs; tags } ->
        type_assignment env ctx lhs rhs
     | DirectApplication { typ; args; tags } ->
        type_direct_application env ctx typ args
+      (* 10.6 *)
     | Conditional { cond; tru; fls; tags } ->
        type_conditional env ctx cond tru fls
+      (* 10.3 *)
     | BlockStatement { block; tags } ->
        type_block env ctx block
+      (* 10.5*)
     | Exit {tags} ->
        { stmt = Exit {tags};
          typ = StmType.Void },
        env
+      (* 10.2 *)
     | EmptyStatement {tags} ->
        { stmt = EmptyStatement {tags};
          typ = StmType.Unit },
        env
+      (* 10.4 *)
     | Return { expr; tags } ->
        type_return env ctx tags expr
+      (* 10.7 *)
     | Switch { expr; cases; tags } ->
        type_switch env ctx tags expr cases
+      (* 9 *)
     | DeclarationStatement { decl; tags } ->
        type_declaration_statement env ctx decl
   in
@@ -3730,7 +3807,6 @@ and is_variable_type env (typ: Typed.Type.t) =
      false
 
 (* Section 10.2
- * NOTE: refers to p4 spec
  *          Δ, T, Γ |- e : t' = t
  * ---------------------------------------------
  *    Δ, T, Γ |- t x = e : Δ, T, Γ[x -> t]
@@ -4577,8 +4653,10 @@ and check_param_shadowing params constructor_params =
 
 and type_declaration (env: CheckerEnv.t) (ctx: DeclContext.t) (decl: Types.Declaration.t) : Prog.Declaration.t * CheckerEnv.t =
   match decl with
+    (* look into spec *)
   | Constant { annotations; typ; name; value; tags } ->
      type_constant env ctx tags annotations typ name value
+    (* look into spec *)
   | Instantiation { annotations; typ; args; name; init; tags } ->
      begin match init with
      | Some init -> failwith "initializer block in instantiation unsupported"
@@ -4600,6 +4678,7 @@ and type_declaration (env: CheckerEnv.t) (ctx: DeclContext.t) (decl: Types.Decla
   | ExternFunction { annotations; return; name; type_params; params; tags } ->
      check_param_shadowing params [];
      type_extern_function env tags annotations return name type_params params
+    (* look into spec *)
   | Variable { annotations; typ; name; init; tags } ->
      type_variable env ctx tags annotations typ name init
   | ValueSet { annotations; typ; size; name; tags } ->
diff --git a/lib/types.mli b/lib/types.mli
index 3927045af..f177e0035 100644
--- a/lib/types.mli
+++ b/lib/types.mli
@@ -196,7 +196,7 @@ and Type : sig
     | IntType of 
         { tags: 'a; 
           expr: Expression.t}
-      (** Fixed-with signed integers *)
+      (** Fixed-width signed integers *)
     | BitType of 
         { tags: 'a; 
           expr: Expression.t}