Adding P4's abstract syntax to formalization doc

[pataei]

@hackedy and @jnfoster can you please review the formalization of P4's abstract syntax (section 4)?

Keep in mind that there are some small differences between our formalization and P4 spec. I enumerate them here (by "we" refers to Petr4's implementation and the document formalization, "P4" refers to P4 spec):

1. We don't include annotations.
2. We don't have match-kind and bit in our data types, however, we have match-kind in the type of expressions.
3. We don't have the unary +.

In general, P4 spec tries to do some of the type checking through its grammar and we have a more general grammar.

[pataei]

@jnfoster @hackedy section 5.1 (type well-formedness) is ready to review.

Changes applied in the commit 4a14625:

• Merged tuple and list types into one.
• Removed don’t care type from the syntax of types of expressions
• Added enum without underlying type to syntax
• Changed \dir \var : \typ to \prm in expression types part of the syntax
• Revised \prm to \prm \typKind where type kind can either be \tau or \rho.
• Combined all record, header, header union, and struct types into one.
• Fixed env explanation in all rules of well-formed

Issue the following:

• [x] should we mention type saturation?
• [x] Petr4 doesn't check the length of a fixed-length integer, either signed or unsigned. However, P4 spec specifies that for signed integers the length must be more than 1 and for unsigned integers the length must be equal or more than zero. We should revise Petr4's rules accordingly, all agree?
• [x] In enum well-formedness rule: Petr4 doesn't allow for an enum to have default values (initializer) for constants, however, P4 spec does. Here's an example. The current type well-formedness rule of enum also ignores the initializer.
• [x] In control type well-formedness rule: P4 spec states that "The types parser, control, and package cannot be used as types of arguments for methods, parsers, controls, tables, actions. They can be used as types for the arguments passed to constructors." The formalization doesn't take this into account neither does Petr4's implementation. We could check this in the well-formedness of types or even when we're declaring a method, parser, control, table, or action, instead of when we're defining their type. p4 spec ref

[pataei]

Todos after this merge for the next one:

• divide type syntactic category. In doing so, write the rules that use each type to have a clear idea of how they're being used.
• revise type well-formed rules
• write type equivalence rules

[hackedy]

🎊 🎊 🪂