search

DmxLarchey / Breadth-First-Numbering

Coq implementation of Breadth-First Numbering à la Okasaki
Other
0 stars 0 forks source link

Cleanup intf #13

Closed DmxLarchey closed 5 years ago

DmxLarchey commented 5 years ago

Hi Ralph,

This branch separate the FIFO interface in fifo.v from its implementations in fifo_[triv,2lists,3llists].v. I did remove fifo_axm.v which is now somehow redundant with the FIFO module interface. Extraction looks very good now: make extraction.vo.

Best,

D.

rmatthes commented 5 years ago

This looks very fine to me. By using the module type FIFO right in the beginning for the implementations, the extracted code is free from name clashes. The new names for the components of FIFO are lighter. I do not see the advantage of exporting M only inside the section (but no disadvantage either). It is true that the axiomatic FIFO became redundant with the module approach.