Sorry this pr is longer than it should have been. My main goal is to build something that can automatically run test cases. And there are three subgoals here. I started working a little bit on all of them.
first: I need to implement extract. And for that purpose, I needed to record which variable is of what extract type. I also needed to change the structure of the code to enable implementing extern-related functions in a separate coq file. [Related Files: files under poulet4/Ccomp/ and poulet_Ccomp ]
second: I want to write a pretty printer. I figured it would be better to write it in Ocaml rather than in coq. [Related Files: all the ocaml files]
third: there's a mismatch between the representation of a p4cub program that the Ccomp expects and the p4cub program that ToP4cub generate. ToP4cub creates a declaration context, while I was only expecting a single TopDecl.d. I currently can't figure out a way to translate the former into the latter, because I don't know which TopDecl.d should I plug all the Control.d into. We really should discuss this.
Sorry this pr is longer than it should have been. My main goal is to build something that can automatically run test cases. And there are three subgoals here. I started working a little bit on all of them.
first: I need to implement extract. And for that purpose, I needed to record which variable is of what extract type. I also needed to change the structure of the code to enable implementing extern-related functions in a separate coq file. [Related Files: files under poulet4/Ccomp/ and poulet_Ccomp ]
second: I want to write a pretty printer. I figured it would be better to write it in Ocaml rather than in coq. [Related Files: all the ocaml files]
third: there's a mismatch between the representation of a p4cub program that the Ccomp expects and the p4cub program that ToP4cub generate. ToP4cub creates a declaration context, while I was only expecting a single TopDecl.d. I currently can't figure out a way to translate the former into the latter, because I don't know which TopDecl.d should I plug all the Control.d into. We really should discuss this.