verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
74 stars 20 forks source link

all enums have an equality instance. no need to check. #378

Open pataei opened 1 year ago

pataei commented 1 year ago

Any enum type has an instance for equality. Remember that enums are declared so a type checked declared enum is a well-typed enum that can only have the underlying types of bit<w>, int<w>, or typedef and all of these types have equality instances. Thus, there is no need to check if the underlying type has such an instance. However, at the moment, Petr4 checks this which is unnecessary.

Petr4 code

 type_has_equality_tests env (typ: Typed.Type.t) =
  match reduce_type env typ with
  ...
  | Enum { typ; _ } -> 
     begin match typ with
     | Some typ -> type_has_equality_tests env typ
     | None -> true
     end
  ...

Fix: just drop the condition.