Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Arch refactor typechecker #414

Draft
wants to merge 25 commits into
base: main
Choose a base branch
from
Draft

Arch refactor typechecker #414

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
1e602ad
starting on surface syntax
pataei Mar 10, 2023
eeeff1e
working on synthesized types syntax
pataei Mar 23, 2023
c4e3ac4
types syntax
pataei Mar 23, 2023
cfa36ae
remove unfinished code
pataei Mar 23, 2023
5a45c6b
fix some errors
pataei Mar 24, 2023
45463ce
syntax done
pataei Mar 28, 2023
a94117a
comments
pataei Mar 28, 2023
90c41ff
all types in one
pataei Mar 28, 2023
d1b72e6
surface ir to represent before and after type inference
pataei Mar 29, 2023
b33b964
added stmt decl
pataei Mar 30, 2023
8c4a377
applied comments..inlined tags except for expr stmt and decl
pataei Apr 2, 2023
b83d349
syntax fixed
pataei Apr 6, 2023
7edd710
putting structure in for simple type checker
pataei Apr 8, 2023
a647a5f
working on expr typing
pataei Apr 8, 2023
981b6fc
next up membership rules
pataei Apr 8, 2023
4e625e3
switching to spec
pataei Apr 8, 2023
ae21c14
have to clean up exp mem in doc
pataei Apr 9, 2023
b8efdb0
list almost done..only func call and instantiatio left
pataei Apr 9, 2023
f3cf4c6
changes in meeting
pataei Apr 13, 2023
345aaf8
added some comments
pataei Apr 14, 2023
d564e2c
added comment
pataei Apr 17, 2023
c18f08b
break checker and utils
pataei May 2, 2023
83561c1
binop helper ready for Harim to be filled out
pataei May 2, 2023
c1f69d8
structure for type eq
pataei May 2, 2023
0f45e72
added sufficient comments for all helpers
pataei May 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
355 changes: 355 additions & 0 deletions coq/lib/Surface/Syntax/Syntax.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,355 @@
Require Import Coq.Lists.List.
Require Import Coq.Strings.String.

From Coq Require Import Numbers.BinNums Classes.EquivDec.

From Poulet4.P4light.Syntax Require P4String P4Int.


Section Syntax.

Context {tags_t: Type}.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Notation P4String := (P4String.t tags_t).
Notation P4Int := (P4Int.t tags_t).

Variant name :=
| BareName (name: P4String)
| QualifiedName (namespaces: list P4String)
(name: P4String).

Variant direction :=
| In
| Out
| InOut
| Directionless.

Variant functionKind :=
| FunParser
| FunControl
| FunExtern
| FunTable
| FunAction
| FunFunction
| FunBuiltin.

Variant uniOp : Type :=
| Not
| BitNot
| UMinus.

Variant binOp : Type :=
| Plus
| PlusSat
| Minus
| MinusSat
| Mul
| Div
| Mod
| Shl
| Shr
| Le
| Ge
| Lt
| Gt
| Eq
| NotEq
| BitAnd
| BitXor
| BitOr
| PlusPlus
| And
| Or.

Inductive typPreT :=
| TypBool
| TypError
| TypMatchKind
| TypInteger
| TypString
| TypInt (width: N)
| TypBit (width: N)
| TypVarBit (width: N)
| TypIdentifier (name: P4String)
| TypSpecialization (base: typ) (*surface*)
(args: list typ) (*type arg*)
| TypHeaderStack (typ: typ) (*surface*)
(size: expression)
| TypTuple (types: list typ) (*surface*)
| TypHeader (type_params: list typVarTyp)
(fields: P4String.AList tags_t typ) (*surface*)
| TypHeaderUnion (type_params: list typVarTyp) (*variable type*)
(fields: P4String.AList tags_t typ) (*surface*)
| TypStruct (type_params: list typVarTyp) (*variable type*)
(fields: P4String.AList tags_t typ) (*surface*)
| TypEnum (name: P4String)
(typ: option typ) (*surface*)
(members: list P4String)
| TypParser (type_params: list typVarTyp) (*type variable*)
(parameters: list parameter)
| TypControl (type_params: list typVarTyp) (*type variable*)
(parameters: list parameter)
| TypPackage (type_params: list typVarTyp) (*type variable*)
(wildcard_params: list P4String)
(parameters: list parameter)
| TypFunction (type_params: list typVarTyp) (*type variable*)
(parameters: list parameter)
(kind: functionKind)
(ret: typ) (*surface+void+type variable*)
| TypSet (typ: typ) (*surface*)
| TypExtern (extern_name: P4String)
| TypRecord (type_params: list typVarTyp) (*type variable*)
(fields: P4String.AList tags_t typ) (*surface*)
| TypNewTyp (name: P4String)
(typ: typ) (*surface*)
| TypAction (data_params: list parameter)
(ctrl_params: list parameter)
| TypConstructor (type_params: list typVarTyp) (*type variable*)
(wildcard_params: list typVarTyp)
(params: list parameter)
(ret: typ) (*surface+void+type variable*)
| TypTable (result_typ_name: P4String)
| TypVoid
with typ :=
| MkType (tags: tags_t)
(typ: typPreT)
with typVarTyp := (*type variable or their assignment*)
| TypVarTyp (type_var: P4String)
(type: option typ)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator Author

@pataei pataei Apr 2, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

with parameter :=
| Param (dir: direction)
(typ: typ) (*surface*)
(default_value: option expression)
(variable: P4String)
with expressionPreT :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should expressions have (optional) type annotations?

Copy link
Collaborator Author

@pataei pataei Apr 2, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you mean parameters? expressions do have optional types but parameter's type shouldn't be optional.

| ExpBool (b: bool)
| ExpString (s: P4String)
| ExpInt (i: P4Int)
| ExpName (name: name)
| ExpArrayAccess (array: expression)
(index: expression)
| ExpBitStringAccess (bits: expression)
(lo: expression)
(high: expression)
| ExpList (value: list expression)
| ExpRecord (entries: P4String.AList tags_t expression)
| ExpUnaryOp (op: uniOp)
(arg: expression)
| ExpBinaryOp (op: binOp)
(arg1: expression)
(arg2: expression)
| ExpCast (typ: typ) (*surface*)
(expr: expression)
| ExpTypeMember (typ: P4String)
(mem: P4String)
| ExpErrorMember (mem: P4String)
| ExpExpressionMember (expr: expression)
(mem: P4String)
| ExpTernary (cond: expression)
(tru: expression)
(fls: expression)
| ExpFunctionCall (func: expression)
(type_args: list typ) (*surface*)
(args: list argument)
| ExpAnonymousInstantiation (typ: typ) (*surface*)
(args: list argument)
| ExpBitmask (expr: expression)
(mask: expression)
| ExpRange (low: expression)
(high: expression)
with expression :=
| MkExpression (tags: tags_t)
(expr: expressionPreT)
(typ: option typ)
(* (dir: direction) *)
with argument :=
| ExpArg (value: expression)
| KeyValueArg (key: P4String)
(value: expression)
| MissingArg.

Variant fieldType :=
| FieldType (typ: typ) (*surface*)
(field: P4String).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why not use P4String.AList tags_t typ instead of list fieldType?


Variant stmtSwitchLabel :=
| StmtSwitchLabelDefault (tags: tags_t)
| StmtSwitchLabelName (tags: tags_t)
(label: P4String).

Variant tableOrParserMatch :=
| MatchDefault (tags: tags_t)
| MatchDontCare (tags: tags_t)
| MatchExpression (tags: tags_t)
(expr: expression).

Variant parserCase :=
| ParserCase (tags: tags_t)
(matches: list tableOrParserMatch)
(next: P4String).

Variant methodPrototype :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

indent

| ProtoConstructor (tags: tags_t)
(name: P4String)
(params: list parameter)
| ProtoAbstractMethod (tags: tags_t)
(ret_type: typ) (*surface*)
(name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
| ProtoMethod (tags: tags_t)
(ret_type: typ) (*surfce*)
(name: P4String)
(type_params: list typVarTyp)
(params: list parameter).

Variant tableKey :=
| TabKey (tags: tags_t)
(key: expression)
(match_kind: P4String).

Variant actionRef :=
| TabActionRef (tags: tags_t)
(name: name)
(args: list argument).

Variant tableEntry :=
| TabEntry (tags: tags_t)
(matches: list tableOrParserMatch)
(action: actionRef).

Variant tableProperty :=
| TableKey (tags: tags_t)
(keys: list tableKey)
| TableActions (tags: tags_t)
(actions: list actionRef)
| TableEntries (tags: tags_t)
(entries: list tableEntry)
| TableDefaultAction (tags: tags_t)
(action: actionRef)
(const: bool)
| TableCustom (tags: tags_t)
(name: P4String)
(value: expression)
(const: bool).

Inductive stmtSwitchCases :=
| StmtSwitchCaseAction (tags: tags_t)
(lable: stmtSwitchLabel)
(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? *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

| StmtMethodCall (func: expression)
(type_args: list typ) (*surface*)
(args: list argument)
| StmtAssignment (lhs: expression)
(rhs: expression)
| StmtdirectApplication (typ: typ) (*surface*)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

caps on Direct

(args: list argument)
| StmtConditional (cond: expression)
(tru: statement)
(fls: option statement)
| StmtBlock (block: block)
| StmtExit
| StmtEmpty
| StmtReturn (expr: option expression)
| StmtSwitch (expr: expression)
(cases: list stmtSwitchCases)
| StmtDeclaration (dcl: declaration) (*can only be variable or constant decl.*)
with statement :=
| MkStatement (tags: tags_t)
(stmt: statementPreT)
(typ: option typ)
with block :=
| BlockEmpty (tags: tags_t)
| BlockCons (statement: statement)
(rest: block)
with parserTransition :=
| ParserDirect (tags: tags_t)
(next: P4String)
| ParserSelect (tags: tags_t)
(exprs: list expression)
(cases: list parserCase)
with parserState :=
| ParserState (tags: tags_t)
(name: P4String)
(statements: list statement)
(transistion: parserTransition)
with declarationPreT :=
| DeclConstant (typ: typ) (*surface*)
(name: P4String)
(value: expression)
| DeclInstantiation (typ: typ) (*surface*)
(args: list argument)
(name: P4String)
(init: list declaration)
| DeclParser (name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
(constructor_params: list parameter)
(locals: declaration)
(states: list parserState)
| DeclControl (name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
(constructor_params: list parameter)
(locals: list declaration)
(apply: block)
| DeclFunction (ret_typ: typ) (*surface+void+type variable*)
(name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
(body: block)
| DeclExternFunction (ret_type: typ) (*surface*)
(name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
| DeclVariable (typ: typ) (*surface*)
(name: P4String)
(init: option expression)
| DeclValueSet (typ: typ) (*surface*)
(name: P4String)
(size: expression)
| DeclAction (name: P4String)
(data_params: list parameter)
(ctrl_params: list parameter)
(body: block)
| DeclTable (name: P4String)
(props: list tableProperty)
| DeclHeaderTyp (name: P4String)
(fields: list fieldType)
| DeclHeaderUnionTyp (name: P4String)
(fields: list fieldType)
| DeclStructTyp (name: P4String)
(fields: list fieldType)
| DeclError (members: list P4String)
| DeclMatchKind (members: list P4String)
| DeclEnumTyp (name: P4String)
(members: list P4String)
| DeclSerializableEnum (typ: typ) (*surface*)
(name: P4String)
(members: P4String.AList tags_t expression)
| DeclControlTyp (name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
| DeclParserTyp (name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
| DeclPackageTyp (name: P4String)
(type_params: list typVarTyp)
(params: list parameter)
| DeclExternObject (name: P4String)
(type_params: list typVarTyp)
(methods: list methodPrototype)
| DeclTypeDef (name: P4String)
(typ_or_dcl: (typ + declaration)) (*surface*)
| DeclNewType (name: P4String)
(typ_or_dcl: (typ + declaration)) (*surface*)
with declaration :=
| MkDeclaration (tags: tags_t)
(decl: declarationPreT)
(typ: option typ).


End Syntax.

16 changes: 4 additions & 12 deletions lib/checker.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -871,20 +871,12 @@ and compile_time_known_expr (env: Checker_env.t) (expr: P4light.coq_Expression)
| _ -> false

(*
judgment rule is as follows. it type check exp under environment e and context c.
it also infers type as well as doing a pass from types to prog.
judgment rule of expression typing is:

e, c |- exp ~~> prog_exp
env, ctx |- exp ~~> ss_exp, type, dir

Note: prog_exp is a record with three fields: expr, typ, dir.
For simplicity, I omitted the name of the fields but the order is kept.
Also, for simplicity, I omitted tags.
Data constructors start with a capital letter.
Where possible data constructors are omitted and instead the name of the
expression implies the data constructor, e.g., str indicates an expression
that is a string.

e, c |- True {tags} ~~> {True {tags}; Bool; Directionless; tags}
It does type checking and type inference. generates an expression in surface syntax
written in Coq.

*)

Expand Down