Module Incr_map

Functions for using maps efficiently within Incremental. The goal of the algorithms here is to do work on the output of the computation proportional to the amount of work done on the input. i.e., k modifications to the input map for some computation will result in k modifications to the output map. The changes to the input map are typically computed using Map.symmetric_diff.

Unless stated otherwise, the non-incremental semantics of these functions (i.e.., ignoring performance) is the same as the corresponding function in Core_kernel's Map module.