search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Generate metadata/"interface" files #23

Closed antalsz closed 6 years ago

antalsz commented 7 years ago

In order to support things such as correctly knowing data type constructors or default modules outside of base, or correctly extending skip method to modules that import a type class, we need to generate metadata files. Current plan:

  1. When translating Mod/File.hs, to $OUTPUT/Mod/File.v, also generate $METADATA/Mod/File.h2c, where $METADATA = $OUTPUT by default.

  2. Pass in search directories when converting a file. For example, if working with base, you'd specify -M path/to/base/output (flag name subject to change).

  3. When translating a file that does import M, hs-to-coq would go and load M.h2c. That would specify (a) what other h2c files to import; (b) metadata, e.g. constructor names; and (c) "persistent" edits, such as skip method or (I think) skip module. If it had already been loaded or generated, this would be brought in from memory, instead of from disk.

Re. 3, however, one question is: would these changes have to be specific to the module that imported them, or could they be globally loaded? Information about the constructors of Full.Mod.Type is always applicable because it's fully qualified. In that case, we could eagerly load all the .h2c files, or possibly even only generate one per library rather than one per module.

nomeata commented 7 years ago

My guts say: They should be applied globally, and they should be loaded eagerly (with lazy loading a possible optimization).