DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
204 stars 51 forks source link

Flatten file hierarchy #80

Closed Lysxia closed 5 years ago

Lysxia commented 5 years ago

Right now, extraction dumps all the modules in a flat hierarchy, flattening out all directories. Since this library is partly concerned with extraction, to make the output of extraction less confusing, I propose to use a similarly flat organization for our Coq files, using _ as a virtual separator instead of the real path separator /.

Another potential issue is that our most generic filenames may conflict with other OCaml libraries, but ocaml must have ways to deal with that, so let's not worry about it.

gmalecha commented 5 years ago

Personally, I don't think we should dictate the way that we write the Coq by the fact that extraction isn't great. There might be ways to mitigate this, but it is worth thinking about based on how we expect people to use extraction. Do we expect them to mostly write Coq code and then extract and run? Possibly adding an Ocaml handler here or there. In that case, most people won't spend a lot of time writing Ocaml code that links to this, and we might be able to mitigate some of the complexity by writing a single Ocaml file by hand that has a bunch of type synonyms and such that point to the extracted files.

Lysxia commented 5 years ago

Indeed I expect that most people would prefer writing everything in Coq and not look at the OCaml output. But this also seems like a self-fulfilling prophecy as long as the default is that extracted code is messy. I was thinking that a flat file hierarchy would be a small price to pay to tidy things up, but I'm still not sure how things would work even with that change, so let's keep this aside for the moment.