- Remove mutual recursion where possible
- Put env into its own module
- Get rid of DeclarationStatements
- make lvalue index have type nat, rather than Value [Ryan]
- Remove dependencies on Types AST
- turn @optional annotations into a boolean in Parameter [Ryan]
- remove Annotation from AST and only define it in OCaml [Ryan]
- Types.Expression in Parameter default values [Ryan]
- Assert_* functions from Prog should be monadic functions in their own module [Molly]
- Get the OCaml to build with the current Coq AST [Ryan]
- PPX annotations have to be added
-
Fix representation of environments
-
Use control-plane names for controllable entities
-
Provide "arbitrary annotations" rather than having annotations and info on every syntax node.
-
Go from this:
Inductive AST := | Add : AST -> AST -> AST | Var : string -> AST
-
To this:
Inductive AST (X:Type) := | Add : X -> AST -> AST -> AST | Var : X -> string -> AST
-
then we have
Definition AST_with_info := AST Info.t Definition AST_with_info_and_type := AST (Info.t * Typed.Type.t)
-
-
Better names (e.g.,
Stat_BlockStatementshould beStmtBlockand let's not mix CamelCase and underscore_separated_words) [Molly] -
Stratify types into 3 parts [Ryan]
-
Make externs nominal [Ryan]
-
Stratify values into 3 parts [Molly]
- Repair evaluator to handle indirect storage of packets
- Parametrize over targets with typeclasses the way the OCaml version uses modules
- Don't bother with type syntactic equality functions, leave them to OCaml
since they're only used in the typechecker
- Maybe revisiting the typing of table entries can fix this
- better representation for contents of tables?
- Can we avoid having info in our Coq code while still having it in OCaml