Poulet refactor

[rudynicolop]

Moved directories & files around for maybe better organization?

• Utility modules get their own shared, top-level directory.
• P4light has its own directory and sub-directories for syntax, semantics, etc.
• P4cub semantics directories collected together.
• P4cub has its own environment data type for its semantics. I attempted to categorize files by similarity & usage, but perhaps there is a better way to organize the files, especially in P4light & Utils.

[QinshiWang]

• [ ] I suggest we should put P4light/Architecture in top-level.

[QinshiWang]

• [ ] I think Hash.v should be in the Architecture folder.
• [ ] LocatorMap.v should be in Semantics/Utils
• [ ] Bitwise.v, Ops.v and P4Arith.v are shared with P4cub, but I don't know the best way to organize it.

[QinshiWang]

I think StringConstants.v can be removed.

[rudynicolop]

• [ ] I think Hash.v should be in the Architecture folder.

This is tricky because Hash.v depends on Bitwise.v which depends upon P4Arith.v. I don't know the best place for P4Arith.v, but P4light/Semantics depends upon P4light/Architecture, and I would prefer not to mix dependencies around.

• [ ] LocatorMap.v should be in Semantics/Utils

Maybe, although I don't know what else would go in a P4light/Semantics/Utils folder. Also LocatorMap.v is still unused...

• [ ] Bitwise.v, Ops.v and P4Arith.v are shared with P4cub, but I don't know the best way to organize it.

Actually P4cub only depends upon P4Arith.v. There are a few places where items in P4cub depend upon items in P4light & vice versa. I think this is reorganization is at least a start, & maybe some other desirable changes may be made later.

[rudynicolop]

• [ ] I suggest we should put P4light/Architecture in top-level.

That's tricky b/c P4light/Architecture/Target.v depends upon P4light/Syntax/Syntax.v & P4light/Syntax/Value.v. I would prefer to avoid further mixing dependencies between the top-level directories.

[rudynicolop]

I think StringConstants.v can be removed.

It's still used in Environment.v.

[QinshiWang]

I think StringConstants.v can be removed.

It's still used in Environment.v.

Is Environment.v still in use? I find removing it doesn't break building.

[rudynicolop]

I think StringConstants.v can be removed.

It's still used in Environment.v.

Is Environment.v still in use? I find removing it doesn't break building.

I removed Environment.v & StringConstants.v & the build broke for me.

It's possible that only a handful of definitions from Environment.v are actually used though.

rudys-mbp:poulet4 rudypeterson$ emacs _CoqProject 
rudys-mbp:poulet4 rudypeterson$ rm -r lib/Environment/
rudys-mbp:poulet4 rudypeterson$ rm lib/P4light/Syntax/StringConstants.v
rudys-mbp:poulet4 rudypeterson$ make clean
dune clean -p poulet4
rudys-mbp:poulet4 rudypeterson$ make
dune build -p poulet4
      coqdep lib/P4cub/Semantics/Dynamic/Architecture/Paquet.v.d
*** Warning: in file P4cub/Semantics/Dynamic/Architecture/Paquet.v, library Poulet4.Environment.Environment is required and has not been found in the loadpath!
      coqdep lib/Platform/Packet.v.d
*** Warning: in file Platform/Packet.v, library Poulet4.Environment.Environment is required and has not been found in the loadpath!
        coqc lib/P4automata/.BisimChecker.aux,lib/P4automata/BisimChecker.{glob,vo}
Unknown notation
        coqc lib/Platform/.Packet.aux,lib/Platform/Packet.{glob,vo} (exit 1)
(cd _build/default && /Users/rudypeterson/.opam/coq-8.13.0/bin/coqc -q -R lib Poulet4 lib/Platform/Packet.v)
File "./lib/Platform/Packet.v", line 10, characters 15-46:
Error: Cannot find a physical path bound to logical path matching suffix
Poulet4.Environment.

make: *** [build] Error 1

[QinshiWang]

I tried removing lib/Environment/Environment.v on poulet4-zlist branch (should be the same for poulet4 branch) and make clean; make. There's no problem.

[rudynicolop]

I tried removing lib/Environment/Environment.v on poulet4-zlist branch (should be the same for poulet4 branch) and make clean; make. There's no problem.

Sorry when I last built I forgot to remove the import commands my bad.

lib/Environment/Environment.v defines:

Inductive exception :=
| PacketTooShort
| Reject
| Exit
| Internal
| TypeError (error_msg: string)
| AssertError (error_msg: string)
| SupportError (error_msg: string)
.

which is used in a few places, including lib/Platform/Packet.v:

Definition packet_monad := @state_monad (list 𝔹) exception.

I moved exception to lib/Platform/Packet.v & deleted the other files.

[QinshiWang]

I tried removing lib/Environment/Environment.v on poulet4-zlist branch (should be the same for poulet4 branch) and make clean; make. There's no problem.

I see. Paquet.v imports Environment.v. I think the reason that I could build was that I have an installed copy.

[QinshiWang]

Why do you use exception rather than signal?

[rudynicolop]

Why do you use exception rather than signal?

My bad I just saw this. signal may be better than exception for packet_monad, I could change where this is used in Platform/Packet.v & Paquet.v if no one objects.

[hackedy]

OK my nits are in #324

[rudynicolop]

Looks great. I've left a few comments but I think we should just merge this now. All the remaining changes can go into a big issue for the time being and we can address it later in a separate PR.

Ok. I'll merge after the sigcomm deadline.