Arch refactor typechecker

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4

Apache License 2.0

75 stars 21 forks source link

Arch refactor typechecker #414

Open pataei opened 1 year ago

pataei commented 1 year ago

@hackedy and @jnfoster Submitting this PR for review of surface IR, after the review I'll make this a draft PR. So please don't merge this.

The main goal of the IR is:

to be simple.
to represent P4 programs before and after type inference and cast insertion (notice the type for type_params which is P4String * option type, where the option type will be initiated to none after parsing and after type inference, it will be replaced with the inferred type.

jnfoster commented 1 year ago

Hi Parisa,

I took a look at this. It is still parameterized by a tags_t type. So, unless I misunderstood, the refactor seems possibly incomplete?

Could you go through the whole IR and:

Add parsing info everywhere (and I do mean pretty much everywhere -- even ints, strings, operators, etc.)
Add an optional type where appropriate (again pretty much everywhere, but some terms may not need types).

jnfoster commented 1 year ago

Another thing to consider: we may want to inline the parsing info and optional type into every constructor rather than using the "X" and "PreX" scheme.

If you do this, use a consistent names and always include those fields as the first 2 (or 1 if no type is needed) elements.

hackedy commented 1 year ago

Does this PR fix #5? Can we make sure it does?

pataei commented 1 year ago

Does this PR fix #5? Can we make sure it does?

Yes, the statement now only allows constant, variable, and instantiation declarations.