Arch refactor typechecker #414
Conversation
|
Hi Parisa, I took a look at this. It is still parameterized by a Could you go through the whole IR and:
|
|
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. |
coq/lib/Surface/Syntax/Syntax.v
Outdated
| (typ: typPreT) | ||
| with typVarTyp := (*type variable or their assignment*) | ||
| | TypVarTyp (type_var: P4String) | ||
| (type: option typ) |
There was a problem hiding this comment.
I think typVarTyp shouldn't exist and uses of typVarTyp should just be bare p4strings. Type variables should be filled in by introducing TypSpecialization nodes, not by modifying type variable nodes to include a binding.
There was a problem hiding this comment.
yes, but we can't access the binding of type variables within a type without accessing the context and the idea is to instantly access the binding of variables within a type.
coq/lib/Surface/Syntax/Syntax.v
Outdated
| (code: block) | ||
| | StmtSwitchCaseFallThrough (tags: tags_t) | ||
| (lable: stmtSwitchLabel) | ||
| with statementPreT := (*why surface.ml has declaration in statements and p4light has variable and instantiation in it? *) |
There was a problem hiding this comment.
we can just do variables and instantiations and not full declarations, the parser I think enforces that the only declarations allowed in statement contexts are variables and instantiations anyway
There was a problem hiding this comment.
I already resolve this, but probably forgot to remove this comment in the code. I'll keep it as the declaration in statement since the parser enforces them to be either variables or instantiations.
coq/lib/Surface/Syntax/Syntax.v
Outdated
|
|
||
| Section Syntax. | ||
|
|
||
| Context {tags_t: Type}. |
There was a problem hiding this comment.
let's get rid of tags_t and use parsing info (I think Info.t or P4Info is the name in the codebase) everywhere we use tags_t
| (typ: typ) (*surface*) | ||
| (default_value: option expression) | ||
| (variable: P4String) | ||
| with expressionPreT := |
There was a problem hiding this comment.
Should expressions have (optional) type annotations?
There was a problem hiding this comment.
Do you mean parameters? expressions do have optional types but parameter's type shouldn't be optional.
coq/lib/Surface/Syntax/Syntax.v
Outdated
|
|
||
| Variant fieldType := | ||
| | FieldType (typ: typ) (*surface*) | ||
| (field: P4String). |
There was a problem hiding this comment.
why not use P4String.AList tags_t typ instead of list fieldType?
coq/lib/Surface/Syntax/Syntax.v
Outdated
| (matches: list tableOrParserMatch) | ||
| (next: P4String). | ||
|
|
||
| Variant methodPrototype := |
coq/lib/Surface/Syntax/Syntax.v
Outdated
| (args: list argument) | ||
| | StmtAssignment (lhs: expression) | ||
| (rhs: expression) | ||
| | StmtdirectApplication (typ: typ) (*surface*) |
|
Does this PR fix #5? Can we make sure it does? |
Yes, the statement now only allows constant, variable, and instantiation declarations. |
@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:
type_paramswhich isP4String * option type, where theoption typewill be initiated tononeafter parsing and after type inference, it will be replaced with the inferred type.