Some of the castings that Petr4 allows make sense as going through P4 spec. Specifically, P4 uses lists and records on the rhs of assignments for structs, headers, and tuples. This results in requiring an either implicit or explicit cast of list/record types to struct/header/tuple types.

The following recognizes the cast needed using examples and explanation from P4 spec along with todos needed to be applied to P4 spec.

list --> tuple (implicit)

P4 spec states that: "Tuples can be assigned to other tuples with the same type, passed as arguments and returned from functions, and can be initialized with list expressions."
tuple<bit<32>, bool> x = { 10, false };

We don't need such cast in our formalization since lists are actually of type list.

list --> struct/header

P4 spec states that: "List expressions can be assigned to expressions of type tuple, struct or header, and can also be passed as arguments to methods. A list may be used to initialize a structure if the list has the same number of elements as fields in the structure. The effect of such an initializer is to assign the nth element of the list to the nth field in the structure:"

    bit<32> a;
    bit<32> b;
}
const S x = { 10, 20 }; //a = 10, b = 20

It continues: "A list expression can have an explicit structure or header type specified, and then it is converted automatically to a structure-valued expression (see 8.13):"

    bit<32> a;
    bit<32> b;
}

extern void f<T>(in T data);

f((S){ 10, 20 }); // automatically converted to f((S){a = 10, b = 20});

The first example requires an implicit cast of list to struct to be legal while the second one requires the explicit cast of list to struct to be legal.

record --> struct/header

Somehow P4 spec (v1.2.3. section 8.13) fails to categorize '(' typeRef ')' expression as an explicit casting expression. Instead, it puts it as part of structure-valued expressions as follows:

expression ...
    | '{' kvList '}'
    | '(' typeRef ')' expression
    ;

kvList
    : kvPair
    | kvList "," kvPair
    ;

kvPair
    : name "=" expression
    ;

P4 spec states that: "For a structure-valued expression typeRef is the name of a struct or header type. The typeRef can be omitted if it can be inferred from context, e.g., when initializing a variable with a struct type. The following example shows a structure-valued expression used in an equality comparison expression:"

Example 1:

struct S {
    bit<32> a;
    bit<32> b;
}

S s;

// Compare s with a structure-valued expression
bool b = s == (S) { a = 1, b = 2 };

It continues: "Structure-valued expressions can be used in the right-hand side of assignments, in comparisons, in field selection expressions, and as arguments to functions, method or actions. Structure-valued expressions are not left values."

This means that we need to add the following explicit (becuase of example 1) and implicit (because of saying "the typeRef can be omitted if it can be inferred from the context") casts to P4 spec in order to allow the expression '(' typeRef ')' expression to make up the rhs of an assignment:

• record type --> header type
• record type --> struct type

Fix informal P4 spec

I'm not sure why P4 doesn't consider these casts at the moment. It might be how it categorizes its types, however, this can easily be resolved by stating that a cast of the type name to a type is legal if the type assigned to the name can be casted to the other type. Then, include a list of such underlying types casted to other types.

Casts to be added to informal P4 spec:

• list --> header (explicit and implicit)
• list --> struct (explicit and implicit)
• record --> header (explicit and implicit)
• record --> struct (explicit and implicit)

Note: As of now, the formalization of these casts checks for a recursive cast (e.g., the rule TupleToHeader-AE-1 below)or the type equality of the elements e.g., the rule TupleToHeader-AE-2 below). As an example, consider the rules for casting a tuple type to a header type:

@jnfoster and @hackedy This note makes sense. However, to the extent that I've read the P4 spec, P4 spec doesn't talk about allowing recursive cast. I want to double-check that 1) such recursion is legal in P4 and 2) we want to keep this recursion in our formalization.

For reference, here's how P4 categorizes its types:

typeRef
    : baseType
    | typeName
    | specializedType
    | headerStackType
    | tupleType
    ;

baseType
    : BOOL
    | ERROR
    | MATCH_KIND
    | STRING
    | INT
    | BIT
    | BIT '<' INTEGER '>'
    | INT '<' INTEGER '>'
    | VARBIT '<' INTEGER '>'
    | BIT '<' '(' expression ')' '>'
    | INT '<' '(' expression ')' '>'
    | VARBIT '<' '(' expression ')' '>'
    ;

typeName
    : prefixedType
    ;

prefixedType
    : TYPE_IDENTIFIER
    | dotPrefix TYPE_IDENTIFIER
    ;

tupleType
    : TUPLE '<' typeArgumentList '>'
    ;

headerStackType
    : typeName '[' expression ']'
    | specializedType '[' expression ']'
    ;

specializedType
    : prefixedType '<' typeArgumentList '>'
    ;

Additionally, it defines type declarations as:

typeDeclaration
    : derivedTypeDeclaration
    | typedefDeclaration
    | parserTypeDeclaration ';'
    | controlTypeDeclaration ';'
    | packageTypeDeclaration ';'
    ;

derivedTypeDeclaration
    : headerTypeDeclaration
    | headerUnionDeclaration
    | structTypeDeclaration
    | enumDeclaration
    ;

@pataei find potential examples of explicit casts that P4 spec is missing.

Here are the references: operations on struct types, example.

For some reason, the grammar in operations on structure-valued expressions doesn't consider '(' typeRef ')' expression as an explicit cast. It's weird.

• In the current spec, add grammar of explicit cast and state that typeRef must be a referable type while the expression's type can be synthesized. This is where our classification of types would be useful.

• In the current spec, add record type as a synthesized type. Might get some push back from the language committee.

@hackedy Petr4 doesn't generate any warnings, right? It'd be nice to document when it's reasonable for it to throw warnings for later refactors.