search

DmxLarchey / Breadth-First-Numbering

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

Implementation of a generic BFN and queues as lazy lists #4

Closed DmxLarchey closed 6 years ago

DmxLarchey commented 6 years ago

The generic BFN (bfn_fifo_gen.v) is based on axiomatized fifos. These axioms are instantiated with fifos as pairs of lists or pairs of lazy lists following Okasaki's JFP95 paper on "Simple and efficient purely functional queues and deques."

Comparing with direct use of fifo2q* (fifo.v & bfn_fifo_2l.v), the generic BFN of bfn_fifo_gen.v does not have a so nice extraction.

DmxLarchey commented 6 years ago

I just added the O(1) with implementation of fifos with 3 lazy lists in fifo.v ... only minor changes from the 3 llist version. Extraction looks pretty close to Okasaki's paper ... I am happy with that one.

DmxLarchey commented 6 years ago

The file bfn_fifo_3q.v extracts to nice and efficient (we will see but this depends on Okasaki's claims ;-) implementation of BFN with 2 queues composed of 3 lazy lists.

rmatthes commented 6 years ago

I just tried to compile the branch queues and get File "./bfn_fifo.v", line 86, characters 6-34: Error: Found no subterm matching "fifo_void ?q = true -> fifo_list ?q = nil" in the current goal.

DmxLarchey commented 6 years ago

Well that file was a bit outdated ... but I corrected it and it should compile now. Make all works for me now.

DmxLarchey commented 6 years ago

The interesting file for benchmarks is bfn_fifo_3q.v.

rmatthes commented 6 years ago

Okay, this compiles for me too. I downloaded the Okasaki paper and will have to study a lot of material. I think it best that you merge your commits and then transfer everything into the master branch. Afterwards, it would be good style to always create a new branch and ask for pull requests from those branches into master.